~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0xb13667d52aa56e002b4d09883d7fce3e/LAWS.bend as LAWS

wordlib: laws about Base's fixed-width words. Word(n) is n Bools, least significant bit first; U32 wraps Word(32n).

2 imports
import Base
import ./word.bend as W

Laws

law xor_comm provedin PROOF.bendsource · line 11 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> {Word.xor(n, a, b) == Word.xor(n, b, a) : Word(n)}

LAW: xor is commutative

law xor_assoc provedin PROOF.bendsource · line 18 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @c:Word(n) -> {Word.xor(n, a, Word.xor(n, b, c)) == Word.xor(n, Word.xor(n, a, b), c) : Word(n)}

LAW: xor is associative

law xor_zero provedin PROOF.bendsource · line 26 · raw

@n:Nat -> @a:Word(n) -> {Word.xor(n, a, Word.zero(n)) == a : Word(n)}

LAW: zero is the identity of xor

law xor_self provedin PROOF.bendsource · line 32 · raw

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

LAW: every word is its own xor inverse

law and_comm provedin PROOF.bendsource · line 38 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> {Word.and(n, a, b) == Word.and(n, b, a) : Word(n)}

LAW: and is commutative

law and_assoc provedin PROOF.bendsource · line 45 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @c:Word(n) -> {Word.and(n, a, Word.and(n, b, c)) == Word.and(n, Word.and(n, a, b), c) : Word(n)}

LAW: and is associative

law or_comm provedin PROOF.bendsource · line 53 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> {Word.or(n, a, b) == Word.or(n, b, a) : Word(n)}

LAW: or is commutative

law or_assoc provedin PROOF.bendsource · line 60 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @c:Word(n) -> {Word.or(n, a, Word.or(n, b, c)) == Word.or(n, Word.or(n, a, b), c) : Word(n)}

LAW: or is associative

law not_not provedin PROOF.bendsource · line 68 · raw

@n:Nat -> @a:Word(n) -> {Word.not(n, Word.not(n, a)) == a : Word(n)}

LAW: not is an involution

law not_and provedin PROOF.bendsource · line 74 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> {Word.not(n, Word.and(n, a, b)) == Word.or(n, Word.not(n, a), Word.not(n, b)) : Word(n)}

LAW: De Morgan: not (a and b) is (not a) or (not b)

law add_zero provedin PROOF.bendsource · line 84 · raw

@n:Nat -> @a:Word(n) -> {Word.add(n, a, Word.zero(n)) == a : Word(n)}

LAW: zero is the identity of add

law adc_nat provedin PROOF.bendsource · line 93 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @c:Bool -> {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), 0xb13667d52aa56e002b4d09883d7fce3e/word.scale(0xb13667d52aa56e002b4d09883d7fce3e/word.carry(n, a, b, c), 0xb13667d52aa56e002b4d09883d7fce3e/word.pow2(n))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), 0xb13667d52aa56e002b4d09883d7fce3e/word.b2n(c))) : Nat}

LAW: the adder is exact. An n-bit add with carry-in c yields a word and a carry-out; the word plus the carry-out's weight 2^n is the true sum a + b + c. Together with the bound on words, this pins Word.add to addition mod 2^n.

law not_nat provedin PROOF.bendsource · line 102 · raw

@n:Nat -> @w:Word(n) -> {1n+Nat.add(Word.to_nat(n, w), Word.to_nat(n, Word.not(n, w))) == 0xb13667d52aa56e002b4d09883d7fce3e/word.pow2(n) : Nat}

LAW: a word and its complement sum to 2^n - 1. So every word's value is below 2^n, with to_nat(not w) as the gap.

law to_nat_inj provedin PROOF.bendsource · line 108 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @h:{Word.to_nat(n, a) == Word.to_nat(n, b) : Nat} -> {a == b : Word(n)}

LAW: to_nat is injective: words with the same value are the same word

law adc_sub provedin PROOF.bendsource · line 117 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @c:Bool -> {Word.adc(n, a, Word.not(n, b), False{}, c) == Word.adc(n, a, b, True{}, c) : Word(n)}

LAW: subtracting is adding the complement: Word.sub(a, b) is a + not b with carry-in 1, i.e. a + (2^n - b) mod 2^n.

law sub_nat provedin PROOF.bendsource · line 125 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+d:Nat -> @h:{Word.to_nat(n, a) == Nat.add(Word.to_nat(n, b), d) : Nat} -> {Word.to_nat(n, Word.sub(n, a, b)) == d : Nat}

LAW: subtraction without wrap: when a = b + d, a - b is exactly d

law add_assoc provedin PROOF.bendsource · line 134 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+c:Word(n) -> {Word.add(n, a, Word.add(n, b, c)) == Word.add(n, Word.add(n, a, b), c) : Word(n)}

LAW: word addition is associative

law add_exact provedin PROOF.bendsource · line 142 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+g:Nat -> @h:{1n+Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), g) == 0xb13667d52aa56e002b4d09883d7fce3e/word.pow2(n) : Nat} -> {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}

LAW: addition without overflow: when a + b < 2^n, the word sum is exact

law shl_put provedin PROOF.bendsource · line 152 · raw

@n:Nat -> @+c:Bool -> @+w:Word(n) -> {Nat.add(Word.to_nat(n, Word.shl.put(n, c, w)), 0xb13667d52aa56e002b4d09883d7fce3e/word.scale(0xb13667d52aa56e002b4d09883d7fce3e/word.top(n, c, w), 0xb13667d52aa56e002b4d09883d7fce3e/word.pow2(n))) == Nat.add(0xb13667d52aa56e002b4d09883d7fce3e/word.b2n(c), Nat.double(Word.to_nat(n, w))) : Nat}

LAW: shifting c in from below doubles the value, adds c and drops the top bit, whose weight is 2^n

law shl_nat provedin PROOF.bendsource · line 159 · raw

@n:Nat -> @w:Word(n) -> {Nat.add(Word.to_nat(n, Word.shl(n, w)), 0xb13667d52aa56e002b4d09883d7fce3e/word.scale(0xb13667d52aa56e002b4d09883d7fce3e/word.top(n, False{}, w), 0xb13667d52aa56e002b4d09883d7fce3e/word.pow2(n))) == Nat.double(Word.to_nat(n, w)) : Nat}

LAW: shl doubles, less the top bit's 2^n

law shr_pad provedin PROOF.bendsource · line 165 · raw

@n:Nat -> @w:Word(n) -> {Word.to_nat(1n+n, Word.shr.pad(n, w)) == Word.to_nat(n, w) : Nat}

LAW: padding a zero on top keeps the value

law shr_nat provedin PROOF.bendsource · line 171 · raw

@n:Nat -> @w:Word(n) -> {Nat.add(0xb13667d52aa56e002b4d09883d7fce3e/word.b2n(0xb13667d52aa56e002b4d09883d7fce3e/word.lsb(n, w)), Nat.double(Word.to_nat(n, Word.shr(n, w)))) == Word.to_nat(n, w) : Nat}

LAW: shr halves, rounding down: twice the result plus the lost bit is w

law cmp_nat provedin PROOF.bendsource · line 177 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}

LAW: comparing words is comparing their values

law u32_xor_comm provedin PROOF.bendsource · line 187 · raw

@a:U32 -> @b:U32 -> {U32.xor(a, b) == U32.xor(b, a) : U32}

LAW: U32.xor is commutative

law u32_and_comm provedin PROOF.bendsource · line 193 · raw

@a:U32 -> @b:U32 -> {U32.and(a, b) == U32.and(b, a) : U32}

LAW: U32.and is commutative

law u32_or_comm provedin PROOF.bendsource · line 199 · raw

@a:U32 -> @b:U32 -> {U32.or(a, b) == U32.or(b, a) : U32}

LAW: U32.or is commutative

law u32_xor_assoc provedin PROOF.bendsource · line 205 · raw

@a:U32 -> @b:U32 -> @c:U32 -> {U32.xor(a, U32.xor(b, c)) == U32.xor(U32.xor(a, b), c) : U32}

LAW: U32.xor is associative

law u32_and_assoc provedin PROOF.bendsource · line 212 · raw

@a:U32 -> @b:U32 -> @c:U32 -> {U32.and(a, U32.and(b, c)) == U32.and(U32.and(a, b), c) : U32}

LAW: U32.and is associative

law u32_or_assoc provedin PROOF.bendsource · line 219 · raw

@a:U32 -> @b:U32 -> @c:U32 -> {U32.or(a, U32.or(b, c)) == U32.or(U32.or(a, b), c) : U32}

LAW: U32.or is associative

law u32_add_assoc provedin PROOF.bendsource · line 226 · raw

@a:U32 -> @b:U32 -> @c:U32 -> {U32.add(a, U32.add(b, c)) == U32.add(U32.add(a, b), c) : U32}

LAW: U32.add is associative

law u32_add_zero provedin PROOF.bendsource · line 233 · raw

@a:U32 -> {U32.add(a, 0) == a : U32}

LAW: 0 is the identity of U32.add and U32.xor; xor self-cancels

law u32_xor_zero provedin PROOF.bendsource · line 237 · raw

@a:U32 -> {U32.xor(a, 0) == a : U32}

law u32_xor_self provedin PROOF.bendsource · line 241 · raw

@+a:U32 -> {U32.xor(a, a) == 0 : U32}

law u32_not_not provedin PROOF.bendsource · line 246 · raw

@a:U32 -> {U32.not(U32.not(a)) == a : U32}

LAW: U32.not is an involution

law u32_to_nat_inj provedin PROOF.bendsource · line 251 · raw

@a:U32 -> @b:U32 -> @h:{U32.to_nat(a) == U32.to_nat(b) : Nat} -> {a == b : U32}

LAW: U32s with the same value are equal

law u32_sub_nat provedin PROOF.bendsource · line 258 · raw

@+a:U32 -> @+b:U32 -> @+d:Nat -> @h:{U32.to_nat(a) == Nat.add(U32.to_nat(b), d) : Nat} -> {U32.to_nat(U32.sub(a, b)) == d : Nat}

LAW: U32 subtraction without wrap: when a = b + d, a - b is exactly d

law u32_cmp_nat provedin PROOF.bendsource · line 266 · raw

@a:U32 -> @b:U32 -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}

LAW: U32 comparison is comparison of values

law u32_lt_nat provedin PROOF.bendsource · line 271 · raw

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

law u32_le_nat provedin PROOF.bendsource · line 276 · raw

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

law mul_go_nat provedin PROOF.bendsource · line 286 · raw

@+n:Nat -> @+m:Nat -> @+a:Word(m) -> @+b:Word(n) -> @+acc:Word(n) -> {Nat.add(Word.to_nat(n, Word.mul.go(n, m, a, b, acc)), Nat.mul(0xb13667d52aa56e002b4d09883d7fce3e/word.mulq(n, m, a, b, acc), 0xb13667d52aa56e002b4d09883d7fce3e/word.pow2(n))) == Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(m, a), Word.to_nat(n, b))) : Nat}

LAW: each step of the shift-and-add multiplier keeps result + q*2^n == acc + a*b, with q = mulq counting the wraps

law mul_nat provedin PROOF.bendsource · line 295 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Nat.add(Word.to_nat(n, Word.mul(n, a, b)), Nat.mul(0xb13667d52aa56e002b4d09883d7fce3e/word.mulq(n, n, a, b, Word.zero(n)), 0xb13667d52aa56e002b4d09883d7fce3e/word.pow2(n))) == Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}

LAW: the product is a*b less some multiple of 2^n

law mul_exact provedin PROOF.bendsource · line 302 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+g:Nat -> @h:{1n+Nat.add(Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), g) == 0xb13667d52aa56e002b4d09883d7fce3e/word.pow2(n) : Nat} -> {Word.to_nat(n, Word.mul(n, a, b)) == Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}

LAW: multiplication without overflow: when a*b < 2^n, the product is exact

law mul_comm provedin PROOF.bendsource · line 311 · raw

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

LAW: word multiplication is commutative

law u32_mul_comm provedin PROOF.bendsource · line 318 · raw

@a:U32 -> @b:U32 -> {U32.mul(a, b) == U32.mul(b, a) : U32}

LAW: U32.mul is commutative