~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0x340691c4c9cfde2764a3ed46e48d644a/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)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, a, b, c), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), 0x340691c4c9cfde2764a3ed46e48d644a/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))) == 0x340691c4c9cfde2764a3ed46e48d644a/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) == 0x340691c4c9cfde2764a3ed46e48d644a/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)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.top(n, c, w), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n))) == Nat.add(0x340691c4c9cfde2764a3ed46e48d644a/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)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.top(n, False{}, w), 0x340691c4c9cfde2764a3ed46e48d644a/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(0x340691c4c9cfde2764a3ed46e48d644a/word.b2n(0x340691c4c9cfde2764a3ed46e48d644a/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}