lemmas.bend source
lemmas.bend on the hub · documented module
# Proved laws that relate Word and U32 arithmetic to Nat. Source: https://github.com/paymog/bend-kit/tree/main/lemmasimport Baseimport bend-mathlib@0.7.2.0/nat.bend as MNat# 2^n, by the doubling that Word.to_nat uses.def pow2(n: Nat) -> Nat: match n: case 0n: 1n case 1n+p: Nat.double(pow2(p))# The value of a word whose low bit is x and whose upper bits have value t.def bit(x: Bool, t: Nat) -> Nat: match x: case False{}: Nat.double(t) case True{}: 1n+Nat.double(t)law to_nat_con: for -p: Nat for x: Bool for -t: Word(p) {bit(x, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{x, t}) : Nat}def to_nat_con(p, x, t): match x: case False{}: {==} case True{}: {==}law cmp_bit: for a: Nat for b: Nat for x: Bool for y: Bool {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(bit(x, a), bit(y, b)) : Cmp}def cmp_bit(a, b, x, y): match a b: case 0n 0n: match x y: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==} case 0n 1n+q: match x y: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==} case 1n+p 0n: match x y: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==} case 1n+p 1n+q: match x y: case False{} False{}: cmp_bit(p, q, False{}, False{}) case False{} True{}: cmp_bit(p, q, False{}, True{}) case True{} False{}: cmp_bit(p, q, True{}, False{}) case True{} True{}: cmp_bit(p, q, True{}, True{})# Comparing two words compares their values.law word_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}def word_cmp_nat(n, a, b): match n: case 0n: {==} case 1n+ +p: match a b: case WCon{+x, +at} WCon{+y, +bt}: %to_nat_con(p, x, at) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == Nat.cmp(_, Word.to_nat(1n+p, WCon{y, bt})) : Cmp} %to_nat_con(p, y, bt) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == Nat.cmp(bit(x, Word.to_nat(p, at)), _) : Cmp} %cmp_bit(Word.to_nat(p, at), Word.to_nat(p, bt), x, y) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == _ : Cmp} %word_cmp_nat(p, at, bt) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == Word.cmp.fin(x, y, _) : Cmp} {==}law u32_cmp_nat: for a: U32 for b: U32 {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}def u32_cmp_nat(a, b): match a b: case U32{x} U32{y}: word_cmp_nat(32n, x, y)law u32_is_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}def u32_is_lt_nat(a, b): Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))law u32_is_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}def u32_is_le_nat(a, b): Equal.cong(Cmp, Bool, c => Cmp.is_le(c), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))law u32_is_eq_nat: for a: U32 for b: U32 {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}def u32_is_eq_nat(a, b): Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))law odd_lt_double: for a: Nat for b: Nat for h: MNat.lt(a, b) MNat.lt(1n+Nat.double(a), Nat.double(b))def odd_lt_double(a, b, h): match a b: case 0n 0n: Empty.absurd(MNat.lt(1n, 0n), MNat.lt_zero(0n)(h)) case 0n 1n+q: {==} case 1n+p 0n: Empty.absurd(MNat.lt(1n+Nat.double(1n+p), 0n), MNat.lt_zero(1n+p)(h)) case 1n+p 1n+q: odd_lt_double(p, q, h)# A word of n bits has a value below 2^n.law word_to_nat_lt: for n: Nat for w: Word(n) MNat.lt(Word.to_nat(n, w), pow2(n))def word_to_nat_lt(n, w): match n: case 0n: {==} case 1n+ +p: match w: case WCon{False{}, +t}: MNat.double_lt_double(Word.to_nat(p, t), pow2(p), word_to_nat_lt(p, t)) case WCon{True{}, +t}: odd_lt_double(Word.to_nat(p, t), pow2(p), word_to_nat_lt(p, t))law u32_to_nat_word: for -x: Word(32n) {Word.to_nat(32n, x) == U32.to_nat(U32{x}) : Nat}def u32_to_nat_word(x): {==}law u32_to_nat_lt: for a: U32 MNat.lt(U32.to_nat(a), pow2(32n))def u32_to_nat_lt(a): match a: case U32{+x}: # A conversion here expands pow2(32n) and overflows the checker stack (bendlang/bend#1071). %u32_to_nat_word(x) : MNat.lt(_, pow2(32n)) word_to_nat_lt(32n, x)law double_inj: for a: Nat for b: Nat for h: {Nat.double(a) == Nat.double(b) : Nat} {a == b : Nat}def double_inj(a, b, h): match a b: case 0n 0n: {==} case 0n 1n+q: Empty.absurd({0n == 1n+q : Nat}, MNat.zero_ne_succ(1n+Nat.double(q))(h)) case 1n+p 0n: Empty.absurd({1n+p == 0n : Nat}, MNat.succ_ne_zero(1n+Nat.double(p))(h)) case 1n+p 1n+q: Equal.cong(Nat, Nat, k => 1n+k, p, q, double_inj(p, q, MNat.succ_inj(Nat.double(p), Nat.double(q), MNat.succ_inj(1n+Nat.double(p), 1n+Nat.double(q), h))))law double_ne_odd: for a: Nat for b: Nat for h: {Nat.double(a) == 1n+Nat.double(b) : Nat} Emptydef double_ne_odd(a, b, h): match a b: case 0n 0n: MNat.zero_ne_succ(0n)(h) case 0n 1n+q: MNat.zero_ne_succ(2n+Nat.double(q))(h) case 1n+p 0n: MNat.succ_ne_zero(Nat.double(p))(MNat.succ_inj(1n+Nat.double(p), 0n, h)) case 1n+p 1n+q: double_ne_odd(p, q, MNat.succ_inj(Nat.double(p), 1n+Nat.double(q), MNat.succ_inj(1n+Nat.double(p), 2n+Nat.double(q), h)))# Two words with the same value are the same word.law word_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)}def word_to_nat_inj(n, a, b, h): match n: case 0n: match a b: case WNil{} WNil{}: {==} case 1n+ +p: match a b: case WCon{False{}, +at} WCon{False{}, +bt}: Equal.cong(Word(p), Word(1n+p), t => WCon{False{}, t}, at, bt, word_to_nat_inj(p, at, bt, double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), h))) case WCon{True{}, +at} WCon{True{}, +bt}: Equal.cong(Word(p), Word(1n+p), t => WCon{True{}, t}, at, bt, word_to_nat_inj(p, at, bt, double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), MNat.succ_inj(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), h)))) case WCon{False{}, +at} WCon{True{}, +bt}: Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word(1n+p)}, double_ne_odd(Word.to_nat(p, at), Word.to_nat(p, bt), h)) case WCon{True{}, +at} WCon{False{}, +bt}: Empty.absurd({WCon{True{}, at} == WCon{False{}, bt} : Word(1n+p)}, double_ne_odd(Word.to_nat(p, bt), Word.to_nat(p, at), Equal.sym(Nat, 1n+Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), h)))law u32_to_nat_inj: for a: U32 for b: U32 for h: {U32.to_nat(a) == U32.to_nat(b) : Nat} {a == b : U32}def u32_to_nat_inj(a, b, h): match a b: case U32{+x} U32{+y}: Equal.cong(Word(32n), U32, w => U32{w}, x, y, word_to_nat_inj(32n, x, y, h))def b2n(b: Bool) -> Nat: match b: case False{}: 0n case True{}: 1n# m when q is set, else 0.def scale(q: Bool, m: Nat) -> Nat: match q: case False{}: 0n case True{}: m# The carry out of a full adder: set when two or three of the bits are set.def maj(x: Bool, y: Bool, c: Bool) -> Bool: match x y: case False{} False{}: False{} case True{} True{}: True{} case False{} True{}: c case True{} False{}: c# The carry out of Word.adc(n, a, b, False{}, c): the bit that a + b + c overflows into.def carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool: match n: case 0n: c case 1n+p: match a b: case WCon{x, at} WCon{y, bt}: carry(p, at, bt, maj(x, y, c))law scale_double: for q: Bool for -m: Nat {Nat.double(scale(q, m)) == scale(q, Nat.double(m)) : Nat}def scale_double(q, m): match q: case False{}: {==} case True{}: {==}# One bit of the adder: s + 2k is the sum c + x + y of the three input bits.law adc_step: for +s: Nat for +x: Nat for +y: Nat for +c: Nat for +k: Nat for +r: Nat for +q: Bool for +m: Nat for +a: Nat for +b: Nat for ih: {Nat.add(r, scale(q, m)) == Nat.add(k, Nat.add(a, b)) : Nat} for fa: {Nat.add(c, Nat.add(x, y)) == Nat.add(s, Nat.double(k)) : Nat} {Nat.add(Nat.add(s, Nat.double(r)), scale(q, Nat.double(m))) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}def adc_step(s, x, y, c, k, r, q, m, a, b, ih, fa): %scale_double(q, m) : {Nat.add(Nat.add(s, Nat.double(r)), _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat} %MNat.add_assoc_sym(s, Nat.double(r), Nat.double(scale(q, m))) : {_ == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat} %MNat.double_add(r, scale(q, m)) : {Nat.add(s, _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat} %Equal.sym(Nat, Nat.add(r, scale(q, m)), Nat.add(k, Nat.add(a, b)), ih) : {Nat.add(s, Nat.double(_)) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat} %MNat.double_add_sym(k, Nat.add(a, b)) : {Nat.add(s, _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat} %MNat.double_add_sym(a, b) : {Nat.add(s, Nat.add(Nat.double(k), _)) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat} %MNat.add_assoc(s, Nat.double(k), Nat.add(Nat.double(a), Nat.double(b))) : {_ == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat} %fa : {Nat.add(_, Nat.add(Nat.double(a), Nat.double(b))) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat} %MNat.add_add_add_comm(x, y, Nat.double(a), Nat.double(b)) : {Nat.add(Nat.add(c, Nat.add(x, y)), Nat.add(Nat.double(a), Nat.double(b))) == Nat.add(c, _) : Nat} %MNat.add_assoc(c, Nat.add(x, y), Nat.add(Nat.double(a), Nat.double(b))) : {Nat.add(Nat.add(c, Nat.add(x, y)), Nat.add(Nat.double(a), Nat.double(b))) == _ : Nat} {==}# The adder is exact: the word sum plus the carry-out weight 2^n is c + a + b.law word_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)), scale(carry(n, a, b, c), pow2(n))) == Nat.add(b2n(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}def word_adc_nat(n, a, b, c): match n: case 0n: match c: case False{}: {==} case True{}: {==} case 1n+ +p: match a b c: case WCon{False{}, +at} WCon{False{}, +bt} False{}: adc_step(0n, 0n, 0n, 0n, 0n, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==}) case WCon{False{}, +at} WCon{False{}, +bt} True{}: adc_step(1n, 0n, 0n, 1n, 0n, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==}) case WCon{False{}, +at} WCon{True{}, +bt} False{}: adc_step(1n, 0n, 1n, 0n, 0n, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==}) case WCon{False{}, +at} WCon{True{}, +bt} True{}: adc_step(0n, 0n, 1n, 1n, 1n, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==}) case WCon{True{}, +at} WCon{False{}, +bt} False{}: adc_step(1n, 1n, 0n, 0n, 0n, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==}) case WCon{True{}, +at} WCon{False{}, +bt} True{}: adc_step(0n, 1n, 0n, 1n, 1n, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==}) case WCon{True{}, +at} WCon{True{}, +bt} False{}: adc_step(0n, 1n, 1n, 0n, 1n, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==}) case WCon{True{}, +at} WCon{True{}, +bt} True{}: adc_step(1n, 1n, 1n, 1n, 1n, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})# Moves a strict upper bound across an equation without a conversion check.law lt_rw: for -a: Nat for -b: Nat for -c: Nat for e: {a == b : Nat} for h: MNat.lt(b, c) MNat.lt(a, c)def lt_rw(a, b, c, e, h): %Equal.sym(Nat, a, b, e) : MNat.lt(_, c) hlaw add_no_carry: for q: Bool for +r: Nat for +m: Nat for +s: Nat for e: {Nat.add(r, scale(q, m)) == s : Nat} for h: MNat.lt(s, m) {r == s : Nat}def add_no_carry(q, r, m, s, e, h): match q: case False{}: Equal.trans(Nat, r, Nat.add(r, 0n), s, MNat.add_zero_sym(r), e) case True{}: Empty.absurd({r == s : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, Nat.add(r, m), m, MNat.le_add_left(m, r), lt_rw(Nat.add(r, m), s, m, e, h))))law add_mod_carry: for q: Bool for +r: Nat for +m: Nat for +s: Nat for e: {Nat.add(r, scale(q, m)) == s : Nat} for h: MNat.lt(r, m) {r == Nat.mod(s, m) : Nat}def add_mod_carry(q, r, m, s, e, h): match q: case False{}: %e : {r == Nat.mod(_, m) : Nat} %MNat.add_zero_sym(r) : {r == Nat.mod(_, m) : Nat} Equal.sym(Nat, Nat.mod(r, m), r, MNat.mod_eq_of_lt(r, m, h)) case True{}: %e : {r == Nat.mod(_, m) : Nat} %MNat.add_comm(m, r) : {r == Nat.mod(_, m) : Nat} %MNat.add_mod_left_sym(r, m) : {r == _ : Nat} Equal.sym(Nat, Nat.mod(r, m), r, MNat.mod_eq_of_lt(r, m, h))# Addition without overflow is exact.law word_add_nat: for +n: Nat for +a: Word(n) for +b: Word(n) for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)) {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}def word_add_nat(n, a, b, h): add_no_carry(carry(n, a, b, False{}), Word.to_nat(n, Word.adc(n, a, b, False{}, False{})), pow2(n), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_adc_nat(n, a, b, False{}), h)# Addition wraps modulo 2^n.law word_add_mod: for +n: Nat for +a: Word(n) for +b: Word(n) {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)) : Nat}def word_add_mod(n, a, b): add_mod_carry(carry(n, a, b, False{}), Word.to_nat(n, Word.adc(n, a, b, False{}, False{})), pow2(n), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_adc_nat(n, a, b, False{}), word_to_nat_lt(n, Word.adc(n, a, b, False{}, False{})))law u32_add_word: for -x: Word(32n) for -y: Word(32n) {Word.to_nat(32n, Word.add(32n, x, y)) == U32.to_nat(U32.add(U32{x}, U32{y})) : Nat}def u32_add_word(x, y): {==}law u32_add_nat: for a: U32 for b: U32 for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n)) {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}def u32_add_nat(a, b, h): match a b: case U32{+x} U32{+y}: word_add_nat(32n, x, y, lt_rw(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), Nat.add(U32.to_nat(U32{x}), U32.to_nat(U32{y})), pow2(32n), {==}, h))law u32_add_mod: for a: U32 for b: U32 {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n)) : Nat}def u32_add_mod(a, b): match a b: case U32{+x} U32{+y}: %u32_add_word(x, y) : {_ == Nat.mod(Nat.add(U32.to_nat(U32{x}), U32.to_nat(U32{y})), pow2(32n)) : Nat} %u32_to_nat_word(x) : {Word.to_nat(32n, Word.add(32n, x, y)) == Nat.mod(Nat.add(_, U32.to_nat(U32{y})), pow2(32n)) : Nat} %u32_to_nat_word(y) : {Word.to_nat(32n, Word.add(32n, x, y)) == Nat.mod(Nat.add(Word.to_nat(32n, x), _), pow2(32n)) : Nat} word_add_mod(32n, x, y)# The bitwise complement of w has value 2^n - 1 - w.law word_not_nat: for n: Nat for w: Word(n) {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == pow2(n) : Nat}def word_not_nat(n, w): match n: case 0n: {==} case 1n+ +p: match w: case WCon{False{}, +t}: %word_not_nat(p, t) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == Nat.double(_) : Nat} %MNat.double_add_sym(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == 2n+_ : Nat} {==} case WCon{True{}, +t}: %MNat.add_succ_sym(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) : {1n+_ == pow2(1n+p) : Nat} %word_not_nat(p, t) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == Nat.double(_) : Nat} %MNat.double_add_sym(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == 2n+_ : Nat} {==}# Subtraction is addition of the complement with a carry in.law word_sub_not: for n: Nat for a: Word(n) for b: Word(n) for +c: Bool {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}def word_sub_not(n, a, b, c): match n: case 0n: {==} case 1n+ +p: match a b: case WCon{False{}, +at} WCon{+y, +bt}: Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.xor(Bool.not(y), c), w}, Word.adc(p, at, bt, True{}, Bool.and(Bool.not(y), c)), Word.adc(p, at, Word.not(p, bt), False{}, Bool.and(Bool.not(y), c)), word_sub_not(p, at, bt, Bool.and(Bool.not(y), c))) case WCon{True{}, +at} WCon{+y, +bt}: Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.not(Bool.xor(Bool.not(y), c)), w}, Word.adc(p, at, bt, True{}, Bool.or(Bool.not(y), c)), Word.adc(p, at, Word.not(p, bt), False{}, Bool.or(Bool.not(y), c)), word_sub_not(p, at, bt, Bool.or(Bool.not(y), c)))law sub_arith: for +a: Nat for +b: Nat for +nb: Nat for +m: Nat for h: MNat.le(b, a) for hn: {1n+Nat.add(nb, b) == m : Nat} {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), m) : Nat}def sub_arith(a, b, nb, m, h, hn): %hn : {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), _) : Nat} %MNat.add_succ_sym(Nat.sub(a, b), Nat.add(nb, b)) : {1n+Nat.add(a, nb) == _ : Nat} %MNat.sub_add_cancel(a, b, h) : {1n+Nat.add(_, nb) == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat} %MNat.add_assoc_sym(Nat.sub(a, b), b, nb) : {1n+_ == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat} %MNat.add_comm(nb, b) : {1n+Nat.add(Nat.sub(a, b), _) == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat} {==}law sub_fin: for q: Bool for +r: Nat for +d: Nat for +m: Nat for e: {Nat.add(r, scale(q, m)) == Nat.add(d, m) : Nat} for h: MNat.lt(r, m) {r == d : Nat}def sub_fin(q, r, d, m, e, h): match q: case False{}: Empty.absurd({r == d : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, Nat.add(d, m), m, MNat.le_add_left(m, d), lt_rw(Nat.add(d, m), r, m, Equal.sym(Nat, r, Nat.add(d, m), Equal.trans(Nat, r, Nat.add(r, 0n), Nat.add(d, m), MNat.add_zero_sym(r), e)), h)))) case True{}: MNat.add_right_cancel(r, m, d, e)# Subtraction without wrap is exact.law word_sub_nat: for +n: Nat for +a: Word(n) for +b: Word(n) for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a)) {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}def word_sub_nat(n, a, b, h): %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}), Word.adc(n, a, Word.not(n, b), False{}, True{}), word_sub_not(n, a, b, True{})) : {Word.to_nat(n, _) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat} sub_fin(carry(n, a, Word.not(n, b), True{}), Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), scale(carry(n, a, Word.not(n, b), True{}), pow2(n))), 1n+Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))), Nat.add(Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)), word_adc_nat(n, a, Word.not(n, b), True{}), sub_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), pow2(n), h, word_not_nat(n, b))), word_to_nat_lt(n, Word.adc(n, a, Word.not(n, b), False{}, True{})))law u32_sub_nat: for a: U32 for b: U32 for h: MNat.le(U32.to_nat(b), U32.to_nat(a)) {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}def u32_sub_nat(a, b, h): match a b: case U32{x} U32{y}: word_sub_nat(32n, x, y, h)law lt_of_double_lt: for a: Nat for b: Nat for h: MNat.lt(Nat.double(a), Nat.double(b)) MNat.lt(a, b)def lt_of_double_lt(a, b, h): match a b: case 0n 0n: Empty.absurd(MNat.lt(0n, 0n), MNat.lt_zero(0n)(h)) case 1n+p 0n: Empty.absurd(MNat.lt(1n+p, 0n), MNat.lt_zero(2n+Nat.double(p))(h)) case 0n 1n+q: {==} case 1n+p 1n+q: lt_of_double_lt(p, q, h)# Incrementing without overflow adds one.law word_inc_nat: for n: Nat for w: Word(n) for h: MNat.lt(1n+Word.to_nat(n, w), pow2(n)) {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}def word_inc_nat(n, w, h): match n: case 0n: Empty.absurd({0n == 1n : Nat}, MNat.lt_irrefl(1n)(h)) case 1n+ +p: match w: case WCon{False{}, t}: {==} case WCon{True{}, +t}: Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.inc(p, t)), 1n+Word.to_nat(p, t), word_inc_nat(p, t, lt_of_double_lt(1n+Word.to_nat(p, t), pow2(p), h)))law u32_inc_nat: for a: U32 for h: MNat.lt(1n+U32.to_nat(a), pow2(32n)) {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}def u32_inc_nat(a, h): match a: case U32{+x}: word_inc_nat(32n, x, lt_rw(1n+Word.to_nat(32n, x), 1n+U32.to_nat(U32{x}), pow2(32n), {==}, h))law u32_to_from_nat: for k: Nat for +h: MNat.lt(k, pow2(32n)) {U32.to_nat(U32.from_nat(k)) == k : Nat}def u32_to_from_nat(k, h): match k: case 0n: {==} case 1n+ +j: +ih = u32_to_from_nat(j, MNat.lt_trans(j, 1n+j, pow2(32n), MNat.lt_succ_self(j), h)) Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(j))), 1n+U32.to_nat(U32.from_nat(j)), 1n+j, u32_inc_nat(U32.from_nat(j), lt_rw(1n+U32.to_nat(U32.from_nat(j)), 1n+j, pow2(32n), Equal.cong(Nat, Nat, v => 1n+v, U32.to_nat(U32.from_nat(j)), j, ih), h)), Equal.cong(Nat, Nat, v => 1n+v, U32.to_nat(U32.from_nat(j)), j, ih))law u32_from_to_nat: for +a: U32 {U32.from_nat(U32.to_nat(a)) == a : U32}def u32_from_to_nat(a): u32_to_nat_inj(U32.from_nat(U32.to_nat(a)), a, u32_to_from_nat(U32.to_nat(a), u32_to_nat_lt(a)))law and_le_sub: for c: Bool for +a: Nat for +b: Nat for +l: Nat for -s: Nat for +hc: {Nat.is_le(a, l) == c : Bool} for hs: MNat.le(a, l) -> {s == Nat.sub(l, a) : Nat} {Bool.and(c, Nat.is_le(b, s)) == Nat.is_le(Nat.add(a, b), l) : Bool}def and_le_sub(c, a, b, l, s, hc, hs): match c: case True{}: %Equal.sym(Nat, s, Nat.sub(l, a), hs(hc)) : {Bool.and(True{}, Nat.is_le(b, _)) == Nat.is_le(Nat.add(a, b), l) : Bool} %hc : {Bool.and(_, Nat.is_le(b, Nat.sub(l, a))) == Nat.is_le(Nat.add(a, b), l) : Bool} MNat.le_and_le_sub_iff_add_le(a, b, l) case False{}: %MNat.le_and_le_sub_iff_add_le(a, b, l) : {Bool.and(False{}, Nat.is_le(b, s)) == _ : Bool} %Equal.sym(Bool, Nat.is_le(a, l), False{}, hc) : {Bool.and(False{}, Nat.is_le(b, s)) == Bool.and(_, Nat.is_le(b, Nat.sub(l, a))) : Bool} {==}# The overflow-safe bounds check n <= len and i <= len - n holds exactly when i + n <= len.law u32_fits_nat: for +len: U32 for +i: U32 for +n: U32 {Bool.and(U32.is_le(n, len), U32.is_le(i, U32.sub(len, n))) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool}def u32_fits_nat(len, i, n): %Equal.sym(Bool, U32.is_le(n, len), Nat.is_le(U32.to_nat(n), U32.to_nat(len)), u32_is_le_nat(n, len)) : {Bool.and(_, U32.is_le(i, U32.sub(len, n))) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool} %Equal.sym(Bool, U32.is_le(i, U32.sub(len, n)), Nat.is_le(U32.to_nat(i), U32.to_nat(U32.sub(len, n))), u32_is_le_nat(i, U32.sub(len, n))) : {Bool.and(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), _) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool} %MNat.add_comm(U32.to_nat(n), U32.to_nat(i)) : {Bool.and(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), Nat.is_le(U32.to_nat(i), U32.to_nat(U32.sub(len, n)))) == Nat.is_le(_, U32.to_nat(len)) : Bool} and_le_sub(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), U32.to_nat(n), U32.to_nat(i), U32.to_nat(len), U32.to_nat(U32.sub(len, n)), {==}, h => u32_sub_nat(len, n, h))