proofs/word_multiplication.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/word_multiplication.bend as Word_multiplication

4 imports

import Base
import ./natural_addition.bend as Addition
import ./word_arithmetic.bend as WordArithmetic
import ./nat_to_u32_bounds.bend as Bounds

Laws

law word_roundtrip provedsource · line 66 · raw

@+n:Nat -> @+w:Word(n) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(Word.to_nat(n, w), n) == w : Word(n)}

law multiply_go provedsource · line 99 · raw

@+m:Nat -> @+n:Nat -> @+w:Word(m) -> @+b:Nat -> @+acc:Nat -> {Word.mul.go(n, m, w, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(b, n), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(acc, n)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(Nat.add(acc, Nat.mul(Word.to_nat(m, w), b)), n) : Word(n)}

Definitions

def truncate source · line 6 · raw

@n:Nat -> @w:Word(1n+n) -> Word(n)

def truncate_zero source · line 14 · raw

@+n:Nat -> {truncate(n, Word.zero(1n+n)) == Word.zero(n) : Word(n)}

def truncate_inc source · line 22 · raw

@+n:Nat -> @+w:Word(1n+n) -> {truncate(n, Word.inc(1n+n, w)) == Word.inc(n, truncate(n, w)) : Word(n)}

def truncate_encode source · line 34 · raw

@+a:Nat -> @+n:Nat -> {truncate(n, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(a, 1n+n)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(a, n) : Word(n)}

def put source · line 44 · raw

@+n:Nat -> @+b:Bool -> @+w:Word(n) -> {Word.shl.put(n, b, w) == truncate(n, WCon{b, w}) : Word(n)}

def shift source · line 53 · raw

@+n:Nat -> @+w:Word(1n+n) -> {Word.shl(1n+n, w) == WCon{False{}, truncate(n, w)} : Word(1n+n)}

def encoded_double source · line 58 · raw

@+a:Nat -> @+n:Nat -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(Nat.double(a), 1n+n) == WCon{False{}, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(a, n)} : Word(1n+n)}

def double_mul source · line 88 · raw

@+a:Nat -> @+b:Nat -> {Nat.mul(Nat.double(a), b) == Nat.mul(a, Nat.double(b)) : Nat}

def multiply source · line 134 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.mul(n, a, b) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.encode(Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), n) : Word(n)}

def native_multiply source · line 138 · raw

@+a:U32 -> @+b:U32 -> {U32.mul(a, b) == U32.from_nat(Nat.mul(U32.to_nat(a), U32.to_nat(b))) : U32}

def bounded_multiply source · line 147 · raw

@+a:U32 -> @+b:U32 -> @+cap:U32 -> @cap_ok:{U32.is_le(cap, 2147483648) == True{} : Bool} -> @h:{Nat.is_le(Nat.mul(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(cap)) == True{} : Bool} -> {U32.to_nat(U32.mul(a, b)) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}