LAWS.bend source
LAWS.bend on the hub · documented module
# wordlib: laws about Base's fixed-width words. Word(n) is n Bools,# least significant bit first; U32 wraps Word(32n).import Baseimport ./word.bend as W# Bitwise algebra# ---------------# LAW: xor is commutativelaw xor_comm: for n: Nat for a: Word(n) for b: Word(n) {Word.xor(n, a, b) == Word.xor(n, b, a) : Word(n)}# LAW: xor is associativelaw xor_assoc: for n: Nat for a: Word(n) for b: Word(n) for c: Word(n) {Word.xor(n, a, Word.xor(n, b, c)) == Word.xor(n, Word.xor(n, a, b), c) : Word(n)}# LAW: zero is the identity of xorlaw xor_zero: for n: Nat for a: Word(n) {Word.xor(n, a, Word.zero(n)) == a : Word(n)}# LAW: every word is its own xor inverselaw xor_self: for n: Nat for +a: Word(n) {Word.xor(n, a, a) == Word.zero(n) : Word(n)}# LAW: and is commutativelaw and_comm: for n: Nat for a: Word(n) for b: Word(n) {Word.and(n, a, b) == Word.and(n, b, a) : Word(n)}# LAW: and is associativelaw and_assoc: for n: Nat for a: Word(n) for b: Word(n) for c: Word(n) {Word.and(n, a, Word.and(n, b, c)) == Word.and(n, Word.and(n, a, b), c) : Word(n)}# LAW: or is commutativelaw or_comm: for n: Nat for a: Word(n) for b: Word(n) {Word.or(n, a, b) == Word.or(n, b, a) : Word(n)}# LAW: or is associativelaw or_assoc: for n: Nat for a: Word(n) for b: Word(n) for c: Word(n) {Word.or(n, a, Word.or(n, b, c)) == Word.or(n, Word.or(n, a, b), c) : Word(n)}# LAW: not is an involutionlaw not_not: for n: Nat for a: Word(n) {Word.not(n, Word.not(n, a)) == a : Word(n)}# LAW: De Morgan: not (a and b) is (not a) or (not b)law not_and: for n: Nat for a: Word(n) for b: Word(n) {Word.not(n, Word.and(n, a, b)) == Word.or(n, Word.not(n, a), Word.not(n, b)) : Word(n)}# Arithmetic# ----------# LAW: zero is the identity of addlaw add_zero: for n: Nat for a: Word(n) {Word.add(n, a, Word.zero(n)) == a : Word(n)}# 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 adc_nat: for n: Nat for a: Word(n) for b: Word(n) for c: Bool {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), W.scale(W.carry(n, a, b, c), W.pow2(n))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), W.b2n(c))) : 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 not_nat: for n: Nat for w: Word(n) {1n+Nat.add(Word.to_nat(n, w), Word.to_nat(n, Word.not(n, w))) == W.pow2(n) : Nat}# LAW: to_nat is injective: words with the same value are the same wordlaw to_nat_inj: for n: Nat for a: Word(n) for b: Word(n) for h: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat} {a == b : 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 adc_sub: for n: Nat for a: Word(n) for b: Word(n) for c: Bool {Word.adc(n, a, Word.not(n, b), False{}, c) == Word.adc(n, a, b, True{}, c) : Word(n)}# LAW: subtraction without wrap: when a = b + d, a - b is exactly dlaw sub_nat: for +n: Nat for +a: Word(n) for +b: Word(n) for +d: Nat for 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: word addition is associativelaw add_assoc: for +n: Nat for +a: Word(n) for +b: Word(n) for +c: Word(n) {Word.add(n, a, Word.add(n, b, c)) == Word.add(n, Word.add(n, a, b), c) : Word(n)}# LAW: addition without overflow: when a + b < 2^n, the word sum is exactlaw add_exact: for +n: Nat for +a: Word(n) for +b: Word(n) for +g: Nat for h: {1n+Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), g) == W.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: shifting c in from below doubles the value, adds c and drops the# top bit, whose weight is 2^nlaw shl_put: for n: Nat for +c: Bool for +w: Word(n) {Nat.add(Word.to_nat(n, Word.shl.put(n, c, w)), W.scale(W.top(n, c, w), W.pow2(n))) == Nat.add(W.b2n(c), Nat.double(Word.to_nat(n, w))) : Nat}# LAW: shl doubles, less the top bit's 2^nlaw shl_nat: for n: Nat for w: Word(n) {Nat.add(Word.to_nat(n, Word.shl(n, w)), W.scale(W.top(n, False{}, w), W.pow2(n))) == Nat.double(Word.to_nat(n, w)) : Nat}# LAW: padding a zero on top keeps the valuelaw shr_pad: for n: Nat for w: Word(n) {Word.to_nat(1n+n, Word.shr.pad(n, w)) == Word.to_nat(n, w) : Nat}# LAW: shr halves, rounding down: twice the result plus the lost bit is wlaw shr_nat: for n: Nat for w: Word(n) {Nat.add(W.b2n(W.lsb(n, w)), Nat.double(Word.to_nat(n, Word.shr(n, w)))) == Word.to_nat(n, w) : Nat}# LAW: comparing words is comparing their valueslaw cmp_nat: for n: Nat for a: Word(n) for b: Word(n) {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}# U32# ---# LAW: U32.xor is commutativelaw u32_xor_comm: for a: U32 for b: U32 {U32.xor(a, b) == U32.xor(b, a) : U32}# LAW: U32.and is commutativelaw u32_and_comm: for a: U32 for b: U32 {U32.and(a, b) == U32.and(b, a) : U32}# LAW: U32.or is commutativelaw u32_or_comm: for a: U32 for b: U32 {U32.or(a, b) == U32.or(b, a) : U32}# LAW: U32.xor is associativelaw u32_xor_assoc: for a: U32 for b: U32 for c: U32 {U32.xor(a, U32.xor(b, c)) == U32.xor(U32.xor(a, b), c) : U32}# LAW: U32.and is associativelaw u32_and_assoc: for a: U32 for b: U32 for c: U32 {U32.and(a, U32.and(b, c)) == U32.and(U32.and(a, b), c) : U32}# LAW: U32.or is associativelaw u32_or_assoc: for a: U32 for b: U32 for c: U32 {U32.or(a, U32.or(b, c)) == U32.or(U32.or(a, b), c) : U32}# LAW: U32.add is associativelaw u32_add_assoc: for a: U32 for b: U32 for c: U32 {U32.add(a, U32.add(b, c)) == U32.add(U32.add(a, b), c) : U32}# LAW: 0 is the identity of U32.add and U32.xor; xor self-cancelslaw u32_add_zero: for a: U32 {U32.add(a, 0) == a : U32}law u32_xor_zero: for a: U32 {U32.xor(a, 0) == a : U32}law u32_xor_self: for +a: U32 {U32.xor(a, a) == 0 : U32}# LAW: U32.not is an involutionlaw u32_not_not: for a: U32 {U32.not(U32.not(a)) == a : U32}# LAW: U32s with the same value are equallaw u32_to_nat_inj: for a: U32 for b: U32 for h: {U32.to_nat(a) == U32.to_nat(b) : Nat} {a == b : U32}# LAW: U32 subtraction without wrap: when a = b + d, a - b is exactly dlaw u32_sub_nat: for +a: U32 for +b: U32 for +d: Nat for h: {U32.to_nat(a) == Nat.add(U32.to_nat(b), d) : Nat} {U32.to_nat(U32.sub(a, b)) == d : Nat}# LAW: U32 comparison is comparison of valueslaw u32_cmp_nat: for a: U32 for b: U32 {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}law u32_lt_nat: for +a: U32 for +b: U32 {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}law u32_le_nat: for +a: U32 for +b: U32 {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}# Multiplication# --------------# LAW: each step of the shift-and-add multiplier keeps# result + q*2^n == acc + a*b, with q = mulq counting the wrapslaw mul_go_nat: for +n: Nat for +m: Nat for +a: Word(m) for +b: Word(n) for +acc: Word(n) {Nat.add(Word.to_nat(n, Word.mul.go(n, m, a, b, acc)), Nat.mul(W.mulq(n, m, a, b, acc), W.pow2(n))) == Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(m, a), Word.to_nat(n, b))) : Nat}# LAW: the product is a*b less some multiple of 2^nlaw mul_nat: for +n: Nat for +a: Word(n) for +b: Word(n) {Nat.add(Word.to_nat(n, Word.mul(n, a, b)), Nat.mul(W.mulq(n, n, a, b, Word.zero(n)), W.pow2(n))) == 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 exactlaw mul_exact: for +n: Nat for +a: Word(n) for +b: Word(n) for +g: Nat for h: {1n+Nat.add(Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), g) == W.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: word multiplication is commutativelaw mul_comm: for +n: Nat for +a: Word(n) for +b: Word(n) {Word.mul(n, a, b) == Word.mul(n, b, a) : Word(n)}# LAW: U32.mul is commutativelaw u32_mul_comm: for a: U32 for b: U32 {U32.mul(a, b) == U32.mul(b, a) : U32}