PROOF.bend source
PROOF.bend on the hub · documented module
# wordlib: the proofs of LAWS.bend. Each word law is an induction on the# width: the head bit follows from a Bool lemma, the tail from the# self-call.import Baseimport ./LAWS.bend as Lawsimport ./word.bend as Wimport ./nat.bend as Nimport ./ac.bend as Aimport ./mul.bend as MUL# Bool# ----def bool_xor_comm(a: Bool, b: Bool) -> {Bool.xor(a, b) == Bool.xor(b, a) : Bool}: match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}def bool_xor_assoc(a: Bool, b: Bool, c: Bool) -> {Bool.xor(a, Bool.xor(b, c)) == Bool.xor(Bool.xor(a, b), c) : Bool}: match a b c: case False{} False{} False{}: {==} case False{} False{} True{}: {==} case False{} True{} False{}: {==} case False{} True{} True{}: {==} case True{} False{} False{}: {==} case True{} False{} True{}: {==} case True{} True{} False{}: {==} case True{} True{} True{}: {==}def bool_and_comm(a: Bool, b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}: match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}def bool_and_assoc(a: Bool, b: Bool, c: Bool) -> {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}: match a b c: case False{} False{} False{}: {==} case False{} False{} True{}: {==} case False{} True{} False{}: {==} case False{} True{} True{}: {==} case True{} False{} False{}: {==} case True{} False{} True{}: {==} case True{} True{} False{}: {==} case True{} True{} True{}: {==}def bool_or_comm(a: Bool, b: Bool) -> {Bool.or(a, b) == Bool.or(b, a) : Bool}: match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}def bool_or_assoc(a: Bool, b: Bool, c: Bool) -> {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}: match a b c: case False{} False{} False{}: {==} case False{} False{} True{}: {==} case False{} True{} False{}: {==} case False{} True{} True{}: {==} case True{} False{} False{}: {==} case True{} False{} True{}: {==} case True{} True{} False{}: {==} case True{} True{} True{}: {==}def bool_not_and(a: Bool, b: Bool) -> {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}: match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}# Bitwise algebra# ---------------def Laws.xor_comm(n, a, b): match n: case 0n: match a b: case WNil{} WNil{}: {==} case 1n+p: match a b: case WCon{+ab, at} WCon{+bb, bt}: %bool_xor_comm(ab, bb) : {WCon{Bool.xor(ab, bb), Word.xor(p, at, bt)} == WCon{_, Word.xor(p, bt, at)} : Word.Con<p>} %Laws.xor_comm(p, at, bt) : {WCon{Bool.xor(ab, bb), Word.xor(p, at, bt)} == WCon{Bool.xor(ab, bb), _} : Word.Con<p>} {==}def Laws.xor_assoc(n, a, b, c): match n: case 0n: match a b c: case WNil{} WNil{} WNil{}: {==} case 1n+p: match a b c: case WCon{+ab, at} WCon{+bb, bt} WCon{+cb, ct}: %bool_xor_assoc(ab, bb, cb) : {WCon{Bool.xor(ab, Bool.xor(bb, cb)), Word.xor(p, at, Word.xor(p, bt, ct))} == WCon{_, Word.xor(p, Word.xor(p, at, bt), ct)} : Word.Con<p>} %Laws.xor_assoc(p, at, bt, ct) : {WCon{Bool.xor(ab, Bool.xor(bb, cb)), Word.xor(p, at, Word.xor(p, bt, ct))} == WCon{Bool.xor(ab, Bool.xor(bb, cb)), _} : Word.Con<p>} {==}def Laws.xor_zero(n, a): match n: case 0n: match a: case WNil{}: {==} case 1n+p: match a: case WCon{False{}, at}: %Laws.xor_zero(p, at) : {WCon{False{}, Word.xor(p, at, Word.zero(p))} == WCon{False{}, _} : Word.Con<p>} {==} case WCon{True{}, at}: %Laws.xor_zero(p, at) : {WCon{True{}, Word.xor(p, at, Word.zero(p))} == WCon{True{}, _} : Word.Con<p>} {==}def Laws.xor_self(n, a): match n: case 0n: match a: case WNil{}: {==} case 1n+p: match a: case WCon{False{}, at}: %Laws.xor_self(p, at) : {WCon{False{}, Word.xor(p, at, at)} == WCon{False{}, _} : Word.Con<p>} {==} case WCon{True{}, at}: %Laws.xor_self(p, at) : {WCon{False{}, Word.xor(p, at, at)} == WCon{False{}, _} : Word.Con<p>} {==}def Laws.and_comm(n, a, b): match n: case 0n: match a b: case WNil{} WNil{}: {==} case 1n+p: match a b: case WCon{+ab, at} WCon{+bb, bt}: %bool_and_comm(ab, bb) : {WCon{Bool.and(ab, bb), Word.and(p, at, bt)} == WCon{_, Word.and(p, bt, at)} : Word.Con<p>} %Laws.and_comm(p, at, bt) : {WCon{Bool.and(ab, bb), Word.and(p, at, bt)} == WCon{Bool.and(ab, bb), _} : Word.Con<p>} {==}def Laws.and_assoc(n, a, b, c): match n: case 0n: match a b c: case WNil{} WNil{} WNil{}: {==} case 1n+p: match a b c: case WCon{+ab, at} WCon{+bb, bt} WCon{+cb, ct}: %bool_and_assoc(ab, bb, cb) : {WCon{Bool.and(ab, Bool.and(bb, cb)), Word.and(p, at, Word.and(p, bt, ct))} == WCon{_, Word.and(p, Word.and(p, at, bt), ct)} : Word.Con<p>} %Laws.and_assoc(p, at, bt, ct) : {WCon{Bool.and(ab, Bool.and(bb, cb)), Word.and(p, at, Word.and(p, bt, ct))} == WCon{Bool.and(ab, Bool.and(bb, cb)), _} : Word.Con<p>} {==}def Laws.or_comm(n, a, b): match n: case 0n: match a b: case WNil{} WNil{}: {==} case 1n+p: match a b: case WCon{+ab, at} WCon{+bb, bt}: %bool_or_comm(ab, bb) : {WCon{Bool.or(ab, bb), Word.or(p, at, bt)} == WCon{_, Word.or(p, bt, at)} : Word.Con<p>} %Laws.or_comm(p, at, bt) : {WCon{Bool.or(ab, bb), Word.or(p, at, bt)} == WCon{Bool.or(ab, bb), _} : Word.Con<p>} {==}def Laws.or_assoc(n, a, b, c): match n: case 0n: match a b c: case WNil{} WNil{} WNil{}: {==} case 1n+p: match a b c: case WCon{+ab, at} WCon{+bb, bt} WCon{+cb, ct}: %bool_or_assoc(ab, bb, cb) : {WCon{Bool.or(ab, Bool.or(bb, cb)), Word.or(p, at, Word.or(p, bt, ct))} == WCon{_, Word.or(p, Word.or(p, at, bt), ct)} : Word.Con<p>} %Laws.or_assoc(p, at, bt, ct) : {WCon{Bool.or(ab, Bool.or(bb, cb)), Word.or(p, at, Word.or(p, bt, ct))} == WCon{Bool.or(ab, Bool.or(bb, cb)), _} : Word.Con<p>} {==}def Laws.not_not(n, a): match n: case 0n: match a: case WNil{}: {==} case 1n+p: match a: case WCon{False{}, at}: %Laws.not_not(p, at) : {WCon{False{}, Word.not(p, Word.not(p, at))} == WCon{False{}, _} : Word.Con<p>} {==} case WCon{True{}, at}: %Laws.not_not(p, at) : {WCon{True{}, Word.not(p, Word.not(p, at))} == WCon{True{}, _} : Word.Con<p>} {==}def Laws.not_and(n, a, b): match n: case 0n: match a b: case WNil{} WNil{}: {==} case 1n+p: match a b: case WCon{+ab, at} WCon{+bb, bt}: %bool_not_and(ab, bb) : {WCon{Bool.not(Bool.and(ab, bb)), Word.not(p, Word.and(p, at, bt))} == WCon{_, Word.or(p, Word.not(p, at), Word.not(p, bt))} : Word.Con<p>} %Laws.not_and(p, at, bt) : {WCon{Bool.not(Bool.and(ab, bb)), Word.not(p, Word.and(p, at, bt))} == WCon{Bool.not(Bool.and(ab, bb)), _} : Word.Con<p>} {==}# Arithmetic# ----------def Laws.add_zero(n, a): match n: case 0n: match a: case WNil{}: {==} case 1n+p: match a: case WCon{False{}, at}: %Laws.add_zero(p, at) : {WCon{False{}, Word.add(p, at, Word.zero(p))} == WCon{False{}, _} : Word.Con<p>} {==} case WCon{True{}, at}: %Laws.add_zero(p, at) : {WCon{True{}, Word.add(p, at, Word.zero(p))} == WCon{True{}, _} : Word.Con<p>} {==}# The adder is exact# ------------------def scale_dbl(K: Bool, +P: Nat) -> {Nat.double(W.scale(K, P)) == W.scale(K, Nat.double(P)) : Nat}: match K: case False{}: {==} case True{}: {==}# one bit of the adder, over Nats: S and k are the sum and carry bits,# a0 b0 c the input bits, R the tail sum, K its carry, P = 2^pdef adc_step(+S: Nat, +k: Nat, +a0: Nat, +b0: Nat, +c: Nat, +R: Nat, +K: Bool, +P: Nat, +A0: Nat, +B0: Nat, ih: {Nat.add(R, W.scale(K, P)) == Nat.add(A0, Nat.add(B0, k)) : Nat}, fa: {Nat.add(S, Nat.double(k)) == Nat.add(a0, Nat.add(b0, c)) : Nat}) -> {Nat.add(Nat.add(S, Nat.double(R)), W.scale(K, Nat.double(P))) == Nat.add(Nat.add(a0, Nat.double(A0)), Nat.add(Nat.add(b0, Nat.double(B0)), c)) : Nat}: %scale_dbl(K, P) : {Nat.add(Nat.add(S, Nat.double(R)), _) == Nat.add(Nat.add(a0, Nat.double(A0)), Nat.add(Nat.add(b0, Nat.double(B0)), c)) : Nat} %A.ac([S, R, W.scale(K, P)], A.EAdd{A.EAtom{0n}, A.EDbl{A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EDbl{A.EAtom{1n}}}, A.EDbl{A.EAtom{2n}}}, {==}) : {_ == Nat.add(Nat.add(a0, Nat.double(A0)), Nat.add(Nat.add(b0, Nat.double(B0)), c)) : Nat} %Equal.sym(Nat, Nat.add(R, W.scale(K, P)), Nat.add(A0, Nat.add(B0, k)), ih) : {Nat.add(S, Nat.double(_)) == Nat.add(Nat.add(a0, Nat.double(A0)), Nat.add(Nat.add(b0, Nat.double(B0)), c)) : Nat} %A.ac([a0, A0, b0, B0, c], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{2n}, A.EAtom{4n}}}, A.EAdd{A.EDbl{A.EAtom{1n}}, A.EDbl{A.EAtom{3n}}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EDbl{A.EAtom{1n}}}, A.EAdd{A.EAdd{A.EAtom{2n}, A.EDbl{A.EAtom{3n}}}, A.EAtom{4n}}}, {==}) : {Nat.add(S, Nat.double(Nat.add(A0, Nat.add(B0, k)))) == _ : Nat} %fa : {Nat.add(S, Nat.double(Nat.add(A0, Nat.add(B0, k)))) == Nat.add(_, Nat.add(Nat.double(A0), Nat.double(B0))) : Nat} A.ac([S, A0, B0, k], A.EAdd{A.EAtom{0n}, A.EDbl{A.EAdd{A.EAtom{1n}, A.EAdd{A.EAtom{2n}, A.EAtom{3n}}}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EDbl{A.EAtom{3n}}}, A.EAdd{A.EDbl{A.EAtom{1n}}, A.EDbl{A.EAtom{2n}}}}, {==})def Laws.adc_nat(n, a, b, c): match n: case 0n: match a b c: case WNil{} WNil{} False{}: {==} case WNil{} WNil{} 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{})), W.carry(p, at, bt, False{}), W.pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), Laws.adc_nat(p, at, bt, False{}), {==}) case WCon{False{}, +at} WCon{False{}, +bt} True{}: adc_step(1n, 0n, 0n, 0n, 1n, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), W.carry(p, at, bt, False{}), W.pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), Laws.adc_nat(p, at, bt, False{}), {==}) case WCon{False{}, +at} WCon{True{}, +bt} False{}: adc_step(1n, 0n, 0n, 1n, 0n, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), W.carry(p, at, bt, False{}), W.pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), Laws.adc_nat(p, at, bt, False{}), {==}) case WCon{False{}, +at} WCon{True{}, +bt} True{}: adc_step(0n, 1n, 0n, 1n, 1n, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), W.carry(p, at, bt, True{}), W.pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), Laws.adc_nat(p, at, bt, True{}), {==}) case WCon{True{}, +at} WCon{False{}, +bt} False{}: adc_step(1n, 0n, 1n, 0n, 0n, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), W.carry(p, at, bt, False{}), W.pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), Laws.adc_nat(p, at, bt, False{}), {==}) case WCon{True{}, +at} WCon{False{}, +bt} True{}: adc_step(0n, 1n, 1n, 0n, 1n, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), W.carry(p, at, bt, True{}), W.pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), Laws.adc_nat(p, at, bt, True{}), {==}) case WCon{True{}, +at} WCon{True{}, +bt} False{}: adc_step(0n, 1n, 1n, 1n, 0n, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), W.carry(p, at, bt, True{}), W.pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), Laws.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{})), W.carry(p, at, bt, True{}), W.pow2(p), Word.to_nat(p, at), Word.to_nat(p, bt), Laws.adc_nat(p, at, bt, True{}), {==})# Bounds and injectivity# ----------------------def Laws.not_nat(n, w): match n: case 0n: match w: case WNil{}: {==} case 1n++p: match w: case WCon{False{}, +t}: %Laws.not_nat(p, t) : {1n+Nat.add(Nat.double(Word.to_nat(p, t)), 1n+Nat.double(Word.to_nat(p, Word.not(p, t)))) == Nat.double(_) : Nat} A.ac([Word.to_nat(p, t), Word.to_nat(p, Word.not(p, t)), 1n], A.EAdd{A.EAtom{2n}, A.EAdd{A.EDbl{A.EAtom{0n}}, A.EAdd{A.EAtom{2n}, A.EDbl{A.EAtom{1n}}}}}, A.EDbl{A.EAdd{A.EAtom{2n}, A.EAdd{A.EAtom{0n}, A.EAtom{1n}}}}, {==}) case WCon{True{}, +t}: %Laws.not_nat(p, t) : {1n+Nat.add(1n+Nat.double(Word.to_nat(p, t)), Nat.double(Word.to_nat(p, Word.not(p, t)))) == Nat.double(_) : Nat} A.ac([Word.to_nat(p, t), Word.to_nat(p, Word.not(p, t)), 1n], A.EAdd{A.EAtom{2n}, A.EAdd{A.EAdd{A.EAtom{2n}, A.EDbl{A.EAtom{0n}}}, A.EDbl{A.EAtom{1n}}}}, A.EDbl{A.EAdd{A.EAtom{2n}, A.EAdd{A.EAtom{0n}, A.EAtom{1n}}}}, {==})def Laws.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}: %Laws.to_nat_inj(p, at, bt, N.double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), h)) : {WCon{False{}, at} == WCon{False{}, _} : Word.Con<p>} {==} case WCon{True{}, +at} WCon{True{}, +bt}: %Laws.to_nat_inj(p, at, bt, N.double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), N.succ_inj(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), h))) : {WCon{True{}, at} == WCon{True{}, _} : Word.Con<p>} {==} case WCon{False{}, +at} WCon{True{}, +bt}: Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word.Con<p>}, N.parity(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.Con<p>}, N.parity(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)))# Subtraction# -----------def Laws.adc_sub(n, a, b, c): match n: case 0n: match a b: case WNil{} WNil{}: {==} case 1n++p: match a b c: case WCon{False{}, +at} WCon{False{}, +bt} False{}: %Laws.adc_sub(p, at, bt, False{}) : {WCon{True{}, Word.adc(p, at, Word.not(p, bt), False{}, False{})} == WCon{True{}, _} : Word.Con<p>} {==} case WCon{False{}, +at} WCon{False{}, +bt} True{}: %Laws.adc_sub(p, at, bt, True{}) : {WCon{False{}, Word.adc(p, at, Word.not(p, bt), False{}, True{})} == WCon{False{}, _} : Word.Con<p>} {==} case WCon{False{}, +at} WCon{True{}, +bt} False{}: %Laws.adc_sub(p, at, bt, False{}) : {WCon{False{}, Word.adc(p, at, Word.not(p, bt), False{}, False{})} == WCon{False{}, _} : Word.Con<p>} {==} case WCon{False{}, +at} WCon{True{}, +bt} True{}: %Laws.adc_sub(p, at, bt, False{}) : {WCon{True{}, Word.adc(p, at, Word.not(p, bt), False{}, False{})} == WCon{True{}, _} : Word.Con<p>} {==} case WCon{True{}, +at} WCon{False{}, +bt} False{}: %Laws.adc_sub(p, at, bt, True{}) : {WCon{False{}, Word.adc(p, at, Word.not(p, bt), False{}, True{})} == WCon{False{}, _} : Word.Con<p>} {==} case WCon{True{}, +at} WCon{False{}, +bt} True{}: %Laws.adc_sub(p, at, bt, True{}) : {WCon{True{}, Word.adc(p, at, Word.not(p, bt), False{}, True{})} == WCon{True{}, _} : Word.Con<p>} {==} case WCon{True{}, +at} WCon{True{}, +bt} False{}: %Laws.adc_sub(p, at, bt, False{}) : {WCon{True{}, Word.adc(p, at, Word.not(p, bt), False{}, False{})} == WCon{True{}, _} : Word.Con<p>} {==} case WCon{True{}, +at} WCon{True{}, +bt} True{}: %Laws.adc_sub(p, at, bt, True{}) : {WCon{False{}, Word.adc(p, at, Word.not(p, bt), False{}, True{})} == WCon{False{}, _} : Word.Con<p>} {==}# a value below P plus a full P cannot fit below Pdef no_wrap.eq(+d: Nat, +G: Nat, +P: Nat, e: {1n+Nat.add(Nat.add(d, P), G) == P : Nat}) -> {Nat.add(1n+Nat.add(d, G), P) == Nat.add(0n, P) : Nat}: %A.ac([d, G, P, 1n], A.EAdd{A.EAtom{3n}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{2n}}, A.EAtom{1n}}}, A.EAdd{A.EAdd{A.EAtom{3n}, A.EAdd{A.EAtom{0n}, A.EAtom{1n}}}, A.EAtom{2n}}, {==}) : {_ == P : Nat} edef no_wrap(+d: Nat, +G: Nat, +P: Nat, e: {1n+Nat.add(Nat.add(d, P), G) == P : Nat}) -> Empty: N.succ_ne_zero(Nat.add(d, G), N.add_cancel_r(1n+Nat.add(d, G), 0n, P, no_wrap.eq(d, G, P, e)))def wrap_exact.sub(+R: Nat, +d: Nat, +G: Nat, +P: Nat, e: {Nat.add(R, 0n) == Nat.add(d, P) : Nat}, bound: {1n+Nat.add(R, G) == P : Nat}) -> {1n+Nat.add(Nat.add(d, P), G) == P : Nat}: %e : {1n+Nat.add(_, G) == P : Nat} %N.add_zero(R) : {1n+Nat.add(_, G) == P : Nat} bound# R + K*P == d + P with R below P forces the carry and R == ddef wrap_exact(K: Bool, +R: Nat, +d: Nat, +P: Nat, +G: Nat, e: {Nat.add(R, W.scale(K, P)) == Nat.add(d, P) : Nat}, bound: {1n+Nat.add(R, G) == P : Nat}) -> {R == d : Nat}: match K: case True{}: N.add_cancel_r(R, d, P, e) case False{}: Empty.absurd({R == d : Nat}, no_wrap(d, G, P, wrap_exact.sub(R, d, G, P, e, bound)))def sub_eq.rest(+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}) -> {Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, Word.not(n, b)), 1n)) == Nat.add(d, W.pow2(n)) : Nat}: %Laws.not_nat(n, b) : {Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, Word.not(n, b)), 1n)) == Nat.add(d, _) : Nat} %Equal.sym(Nat, Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), d), h) : {Nat.add(_, Nat.add(Word.to_nat(n, Word.not(n, b)), 1n)) == Nat.add(d, 1n+Nat.add(Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)))) : Nat} A.ac([Word.to_nat(n, b), d, Word.to_nat(n, Word.not(n, b)), 1n], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAdd{A.EAtom{2n}, A.EAtom{3n}}}, A.EAdd{A.EAtom{1n}, A.EAdd{A.EAtom{3n}, A.EAdd{A.EAtom{0n}, A.EAtom{2n}}}}, {==})def sub_eq(+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}) -> {Nat.add(Word.to_nat(n, Word.sub(n, a, b)), W.scale(W.carry(n, a, Word.not(n, b), True{}), W.pow2(n))) == Nat.add(d, W.pow2(n)) : Nat}: %Laws.adc_sub(n, a, b, True{}) : {Nat.add(Word.to_nat(n, _), W.scale(W.carry(n, a, Word.not(n, b), True{}), W.pow2(n))) == Nat.add(d, W.pow2(n)) : Nat} Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), W.scale(W.carry(n, a, Word.not(n, b), True{}), W.pow2(n))), Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, Word.not(n, b)), 1n)), Nat.add(d, W.pow2(n)), Laws.adc_nat(n, a, Word.not(n, b), True{}), sub_eq.rest(n, a, b, d, h))def Laws.sub_nat(n, a, b, d, h): wrap_exact(W.carry(n, a, Word.not(n, b), True{}), Word.to_nat(n, Word.sub(n, a, b)), d, W.pow2(n), Word.to_nat(n, Word.not(n, Word.sub(n, a, b))), sub_eq(n, a, b, d, h), Laws.not_nat(n, Word.sub(n, a, b)))# Associativity# -------------# X + k*P == Y + j*P with X, Y below P forces X == Ydef uniq.shuffle(+X: Nat, +M: Nat, +Y: Nat, +M2: Nat, +P: Nat, e: {Nat.add(X, Nat.add(P, M)) == Nat.add(Y, Nat.add(P, M2)) : Nat}) -> {Nat.add(Nat.add(X, M), P) == Nat.add(Nat.add(Y, M2), P) : Nat}: %A.ac([X, M, P], A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{2n}, A.EAtom{1n}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAtom{2n}}, {==}) : {_ == Nat.add(Nat.add(Y, M2), P) : Nat} %A.ac([Y, M2, P], A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{2n}, A.EAtom{1n}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAtom{2n}}, {==}) : {Nat.add(X, Nat.add(P, M)) == _ : Nat} edef uniq.lift(+X: Nat, +Y: Nat, +M: Nat, +P: Nat, e: {Nat.add(X, 0n) == Nat.add(Y, Nat.add(P, M)) : Nat}) -> {Nat.add(X, 0n) == Nat.add(Nat.add(Y, M), P) : Nat}: %A.ac([Y, M, P], A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{2n}, A.EAtom{1n}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAtom{2n}}, {==}) : {Nat.add(X, 0n) == _ : Nat} edef uniq(+X: Nat, +Y: Nat, +P: Nat, +GX: Nat, +GY: Nat, +k: Nat, +j: Nat, e: {Nat.add(X, Nat.mul(k, P)) == Nat.add(Y, Nat.mul(j, P)) : Nat}, bX: {1n+Nat.add(X, GX) == P : Nat}, bY: {1n+Nat.add(Y, GY) == P : Nat}) -> {X == Y : Nat}: match k j: case 0n 0n: N.add_cancel_r(X, Y, 0n, e) case 1n++kp 1n++jp: uniq(X, Y, P, GX, GY, kp, jp, N.add_cancel_r(Nat.add(X, Nat.mul(kp, P)), Nat.add(Y, Nat.mul(jp, P)), P, uniq.shuffle(X, Nat.mul(kp, P), Y, Nat.mul(jp, P), P, e)), bX, bY) case 0n 1n++jp: Empty.absurd({X == Y : Nat}, no_wrap(Nat.add(Y, Nat.mul(jp, P)), GX, P, wrap_exact.sub(X, Nat.add(Y, Nat.mul(jp, P)), GX, P, uniq.lift(X, Y, Nat.mul(jp, P), P, e), bX))) case 1n++kp 0n: Empty.absurd({X == Y : Nat}, no_wrap(Nat.add(X, Nat.mul(kp, P)), GY, P, wrap_exact.sub(Y, Nat.add(X, Nat.mul(kp, P)), GY, P, uniq.lift(Y, X, Nat.mul(kp, P), P, Equal.sym(Nat, Nat.add(X, Nat.add(P, Nat.mul(kp, P))), Nat.add(Y, 0n), e)), bY)))def uniq.conv(+X: Nat, +Y: Nat, +L: Nat, +L2: Nat, +R: Nat, +R2: Nat, e: {Nat.add(X, L) == Nat.add(Y, R) : Nat}, hl: {L == L2 : Nat}, hr: {R == R2 : Nat}) -> {Nat.add(X, L2) == Nat.add(Y, R2) : Nat}: %hl : {Nat.add(X, _) == Nat.add(Y, R2) : Nat} %hr : {Nat.add(X, L) == Nat.add(Y, _) : Nat} edef assoc.cases(J2: Bool, J1: Bool, K2: Bool, K1: Bool, +Y: Nat, +X: Nat, +P: Nat, +GY: Nat, +GX: Nat, e: {Nat.add(Y, Nat.add(W.scale(J2, P), W.scale(J1, P))) == Nat.add(X, Nat.add(W.scale(K2, P), W.scale(K1, P))) : Nat}, bY: {1n+Nat.add(Y, GY) == P : Nat}, bX: {1n+Nat.add(X, GX) == P : Nat}) -> {Y == X : Nat}: match J2 J1 K2 K1: case False{} False{} False{} False{}: uniq(Y, X, P, GY, GX, 0n, 0n, uniq.conv(Y, X, Nat.add(0n, 0n), Nat.mul(0n, P), Nat.add(0n, 0n), Nat.mul(0n, P), e, A.ac([P], A.EAdd{A.EZero{}, A.EZero{}}, A.EZero{}, {==}), A.ac([P], A.EAdd{A.EZero{}, A.EZero{}}, A.EZero{}, {==})), bY, bX) case False{} False{} False{} True{}: uniq(Y, X, P, GY, GX, 0n, 1n, uniq.conv(Y, X, Nat.add(0n, 0n), Nat.mul(0n, P), Nat.add(0n, P), Nat.mul(1n, P), e, A.ac([P], A.EAdd{A.EZero{}, A.EZero{}}, A.EZero{}, {==}), A.ac([P], A.EAdd{A.EZero{}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==})), bY, bX) case False{} False{} True{} False{}: uniq(Y, X, P, GY, GX, 0n, 1n, uniq.conv(Y, X, Nat.add(0n, 0n), Nat.mul(0n, P), Nat.add(P, 0n), Nat.mul(1n, P), e, A.ac([P], A.EAdd{A.EZero{}, A.EZero{}}, A.EZero{}, {==}), A.ac([P], A.EAdd{A.EAtom{0n}, A.EZero{}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==})), bY, bX) case False{} False{} True{} True{}: uniq(Y, X, P, GY, GX, 0n, 2n, uniq.conv(Y, X, Nat.add(0n, 0n), Nat.mul(0n, P), Nat.add(P, P), Nat.mul(2n, P), e, A.ac([P], A.EAdd{A.EZero{}, A.EZero{}}, A.EZero{}, {==}), A.ac([P], A.EAdd{A.EAtom{0n}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, {==})), bY, bX) case False{} True{} False{} False{}: uniq(Y, X, P, GY, GX, 1n, 0n, uniq.conv(Y, X, Nat.add(0n, P), Nat.mul(1n, P), Nat.add(0n, 0n), Nat.mul(0n, P), e, A.ac([P], A.EAdd{A.EZero{}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==}), A.ac([P], A.EAdd{A.EZero{}, A.EZero{}}, A.EZero{}, {==})), bY, bX) case False{} True{} False{} True{}: uniq(Y, X, P, GY, GX, 1n, 1n, uniq.conv(Y, X, Nat.add(0n, P), Nat.mul(1n, P), Nat.add(0n, P), Nat.mul(1n, P), e, A.ac([P], A.EAdd{A.EZero{}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==}), A.ac([P], A.EAdd{A.EZero{}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==})), bY, bX) case False{} True{} True{} False{}: uniq(Y, X, P, GY, GX, 1n, 1n, uniq.conv(Y, X, Nat.add(0n, P), Nat.mul(1n, P), Nat.add(P, 0n), Nat.mul(1n, P), e, A.ac([P], A.EAdd{A.EZero{}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==}), A.ac([P], A.EAdd{A.EAtom{0n}, A.EZero{}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==})), bY, bX) case False{} True{} True{} True{}: uniq(Y, X, P, GY, GX, 1n, 2n, uniq.conv(Y, X, Nat.add(0n, P), Nat.mul(1n, P), Nat.add(P, P), Nat.mul(2n, P), e, A.ac([P], A.EAdd{A.EZero{}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==}), A.ac([P], A.EAdd{A.EAtom{0n}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, {==})), bY, bX) case True{} False{} False{} False{}: uniq(Y, X, P, GY, GX, 1n, 0n, uniq.conv(Y, X, Nat.add(P, 0n), Nat.mul(1n, P), Nat.add(0n, 0n), Nat.mul(0n, P), e, A.ac([P], A.EAdd{A.EAtom{0n}, A.EZero{}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==}), A.ac([P], A.EAdd{A.EZero{}, A.EZero{}}, A.EZero{}, {==})), bY, bX) case True{} False{} False{} True{}: uniq(Y, X, P, GY, GX, 1n, 1n, uniq.conv(Y, X, Nat.add(P, 0n), Nat.mul(1n, P), Nat.add(0n, P), Nat.mul(1n, P), e, A.ac([P], A.EAdd{A.EAtom{0n}, A.EZero{}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==}), A.ac([P], A.EAdd{A.EZero{}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==})), bY, bX) case True{} False{} True{} False{}: uniq(Y, X, P, GY, GX, 1n, 1n, uniq.conv(Y, X, Nat.add(P, 0n), Nat.mul(1n, P), Nat.add(P, 0n), Nat.mul(1n, P), e, A.ac([P], A.EAdd{A.EAtom{0n}, A.EZero{}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==}), A.ac([P], A.EAdd{A.EAtom{0n}, A.EZero{}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==})), bY, bX) case True{} False{} True{} True{}: uniq(Y, X, P, GY, GX, 1n, 2n, uniq.conv(Y, X, Nat.add(P, 0n), Nat.mul(1n, P), Nat.add(P, P), Nat.mul(2n, P), e, A.ac([P], A.EAdd{A.EAtom{0n}, A.EZero{}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==}), A.ac([P], A.EAdd{A.EAtom{0n}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, {==})), bY, bX) case True{} True{} False{} False{}: uniq(Y, X, P, GY, GX, 2n, 0n, uniq.conv(Y, X, Nat.add(P, P), Nat.mul(2n, P), Nat.add(0n, 0n), Nat.mul(0n, P), e, A.ac([P], A.EAdd{A.EAtom{0n}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, {==}), A.ac([P], A.EAdd{A.EZero{}, A.EZero{}}, A.EZero{}, {==})), bY, bX) case True{} True{} False{} True{}: uniq(Y, X, P, GY, GX, 2n, 1n, uniq.conv(Y, X, Nat.add(P, P), Nat.mul(2n, P), Nat.add(0n, P), Nat.mul(1n, P), e, A.ac([P], A.EAdd{A.EAtom{0n}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, {==}), A.ac([P], A.EAdd{A.EZero{}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==})), bY, bX) case True{} True{} True{} False{}: uniq(Y, X, P, GY, GX, 2n, 1n, uniq.conv(Y, X, Nat.add(P, P), Nat.mul(2n, P), Nat.add(P, 0n), Nat.mul(1n, P), e, A.ac([P], A.EAdd{A.EAtom{0n}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, {==}), A.ac([P], A.EAdd{A.EAtom{0n}, A.EZero{}}, A.EAdd{A.EAtom{0n}, A.EZero{}}, {==})), bY, bX) case True{} True{} True{} True{}: uniq(Y, X, P, GY, GX, 2n, 2n, uniq.conv(Y, X, Nat.add(P, P), Nat.mul(2n, P), Nat.add(P, P), Nat.mul(2n, P), e, A.ac([P], A.EAdd{A.EAtom{0n}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, {==}), A.ac([P], A.EAdd{A.EAtom{0n}, A.EAtom{0n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, {==})), bY, bX)# (a + b) + c, by value: X + 2^n*(K2 + K1) == A + (B + C)def assoc.r(+n: Nat, +a: Word(n), +b: Word(n), +c: Word(n)) -> {Nat.add(Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), Nat.add(W.scale(W.carry(n, Word.add(n, a, b), c, False{}), W.pow2(n)), W.scale(W.carry(n, a, b, False{}), W.pow2(n)))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat}: %A.ac([Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), W.scale(W.carry(n, Word.add(n, a, b), c, False{}), W.pow2(n)), W.scale(W.carry(n, a, b, False{}), W.pow2(n))], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAtom{2n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}, {==}) : {_ == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), W.scale(W.carry(n, Word.add(n, a, b), c, False{}), W.pow2(n))), Nat.add(Word.to_nat(n, Word.add(n, a, b)), Nat.add(Word.to_nat(n, c), 0n)), Laws.adc_nat(n, Word.add(n, a, b), c, False{})) : {Nat.add(_, W.scale(W.carry(n, a, b, False{}), W.pow2(n))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat} %A.ac([Word.to_nat(n, Word.add(n, a, b)), Word.to_nat(n, c), W.scale(W.carry(n, a, b, False{}), W.pow2(n))], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{2n}}, A.EAdd{A.EAtom{1n}, A.EZero{}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EZero{}}}, A.EAtom{2n}}, {==}) : {_ == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.add(n, a, b)), W.scale(W.carry(n, a, b, False{}), W.pow2(n))), Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), 0n)), Laws.adc_nat(n, a, b, False{})) : {Nat.add(_, Nat.add(Word.to_nat(n, c), 0n)) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat} A.ac([Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, c)], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EZero{}}}, A.EAdd{A.EAtom{2n}, A.EZero{}}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}, {==})# a + (b + c), by value: Y + 2^n*(J2 + J1) == A + (B + C)def assoc.l(+n: Nat, +a: Word(n), +b: Word(n), +c: Word(n)) -> {Nat.add(Word.to_nat(n, Word.add(n, a, Word.add(n, b, c))), Nat.add(W.scale(W.carry(n, a, Word.add(n, b, c), False{}), W.pow2(n)), W.scale(W.carry(n, b, c, False{}), W.pow2(n)))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat}: %A.ac([Word.to_nat(n, Word.add(n, a, Word.add(n, b, c))), W.scale(W.carry(n, a, Word.add(n, b, c), False{}), W.pow2(n)), W.scale(W.carry(n, b, c, False{}), W.pow2(n))], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAtom{2n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}, {==}) : {_ == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.add(n, a, Word.add(n, b, c))), W.scale(W.carry(n, a, Word.add(n, b, c), False{}), W.pow2(n))), Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, Word.add(n, b, c)), 0n)), Laws.adc_nat(n, a, Word.add(n, b, c), False{})) : {Nat.add(_, W.scale(W.carry(n, b, c, False{}), W.pow2(n))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat} %A.ac([Word.to_nat(n, a), Word.to_nat(n, Word.add(n, b, c)), W.scale(W.carry(n, b, c, False{}), W.pow2(n))], A.EAdd{A.EAdd{A.EAtom{1n}, A.EAtom{2n}}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EZero{}}}, A.EAtom{2n}}, {==}) : {_ == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.add(n, b, c)), W.scale(W.carry(n, b, c, False{}), W.pow2(n))), Nat.add(Word.to_nat(n, b), Nat.add(Word.to_nat(n, c), 0n)), Laws.adc_nat(n, b, c, False{})) : {Nat.add(_, Nat.add(Word.to_nat(n, a), 0n)) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat} A.ac([Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, c)], A.EAdd{A.EAdd{A.EAtom{1n}, A.EAdd{A.EAtom{2n}, A.EZero{}}}, A.EAdd{A.EAtom{0n}, A.EZero{}}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}, {==})def assoc.eq(+n: Nat, +a: Word(n), +b: Word(n), +c: Word(n)) -> {Nat.add(Word.to_nat(n, Word.add(n, a, Word.add(n, b, c))), Nat.add(W.scale(W.carry(n, a, Word.add(n, b, c), False{}), W.pow2(n)), W.scale(W.carry(n, b, c, False{}), W.pow2(n)))) == Nat.add(Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), Nat.add(W.scale(W.carry(n, Word.add(n, a, b), c, False{}), W.pow2(n)), W.scale(W.carry(n, a, b, False{}), W.pow2(n)))) : Nat}: Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.add(n, a, Word.add(n, b, c))), Nat.add(W.scale(W.carry(n, a, Word.add(n, b, c), False{}), W.pow2(n)), W.scale(W.carry(n, b, c, False{}), W.pow2(n)))), Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))), Nat.add(Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), Nat.add(W.scale(W.carry(n, Word.add(n, a, b), c, False{}), W.pow2(n)), W.scale(W.carry(n, a, b, False{}), W.pow2(n)))), assoc.l(n, a, b, c), Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), Nat.add(W.scale(W.carry(n, Word.add(n, a, b), c, False{}), W.pow2(n)), W.scale(W.carry(n, a, b, False{}), W.pow2(n)))), Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))), assoc.r(n, a, b, c)))def Laws.add_assoc(n, a, b, c): Laws.to_nat_inj(n, Word.add(n, a, Word.add(n, b, c)), Word.add(n, Word.add(n, a, b), c), assoc.cases(W.carry(n, a, Word.add(n, b, c), False{}), W.carry(n, b, c, False{}), W.carry(n, Word.add(n, a, b), c, False{}), W.carry(n, a, b, False{}), Word.to_nat(n, Word.add(n, a, Word.add(n, b, c))), Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), W.pow2(n), Word.to_nat(n, Word.not(n, Word.add(n, a, Word.add(n, b, c)))), Word.to_nat(n, Word.not(n, Word.add(n, Word.add(n, a, b), c))), assoc.eq(n, a, b, c), Laws.not_nat(n, Word.add(n, a, Word.add(n, b, c))), Laws.not_nat(n, Word.add(n, Word.add(n, a, b), c))))# Addition without overflow# -------------------------def no_carry.sub(+R: Nat, +S: Nat, +P: Nat, +g: Nat, e: {Nat.add(R, P) == S : Nat}, h: {1n+Nat.add(S, g) == P : Nat}) -> {1n+Nat.add(Nat.add(R, P), g) == P : Nat}: %Equal.sym(Nat, Nat.add(R, P), S, e) : {1n+Nat.add(_, g) == P : Nat} h# R + K*P == S with S below P rules the carry outdef no_carry(K: Bool, +R: Nat, +S: Nat, +P: Nat, +g: Nat, e: {Nat.add(R, W.scale(K, P)) == S : Nat}, h: {1n+Nat.add(S, g) == P : Nat}) -> {R == S : Nat}: match K: case False{}: Equal.trans(Nat, R, Nat.add(R, 0n), S, N.add_zero(R), e) case True{}: Empty.absurd({R == S : Nat}, no_wrap(R, g, P, no_carry.sub(R, S, P, g, e, h)))def add_eq(+n: Nat, +a: Word(n), +b: Word(n)) -> {Nat.add(Word.to_nat(n, Word.add(n, a, b)), W.scale(W.carry(n, a, b, False{}), W.pow2(n))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}: %Equal.sym(Nat, Word.to_nat(n, b), Nat.add(Word.to_nat(n, b), 0n), N.add_zero(Word.to_nat(n, b))) : {Nat.add(Word.to_nat(n, Word.add(n, a, b)), W.scale(W.carry(n, a, b, False{}), W.pow2(n))) == Nat.add(Word.to_nat(n, a), _) : Nat} Laws.adc_nat(n, a, b, False{})def Laws.add_exact(n, a, b, g, h): no_carry(W.carry(n, a, b, False{}), Word.to_nat(n, Word.add(n, a, b)), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), W.pow2(n), g, add_eq(n, a, b), h)# Shifts# ------# one step of shl.put over Nats: c the bit shifted in, R the tail, K the# bit shifted out, P = 2^p, bb and T the input's head and taildef shl_step(+c: Nat, +R: Nat, +K: Bool, +P: Nat, +bb: Nat, +T: Nat, ih: {Nat.add(R, W.scale(K, P)) == Nat.add(bb, Nat.double(T)) : Nat}) -> {Nat.add(Nat.add(c, Nat.double(R)), W.scale(K, Nat.double(P))) == Nat.add(c, Nat.double(Nat.add(bb, Nat.double(T)))) : Nat}: %scale_dbl(K, P) : {Nat.add(Nat.add(c, Nat.double(R)), _) == Nat.add(c, Nat.double(Nat.add(bb, Nat.double(T)))) : Nat} %A.ac([c, R, W.scale(K, P)], A.EAdd{A.EAtom{0n}, A.EDbl{A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EDbl{A.EAtom{1n}}}, A.EDbl{A.EAtom{2n}}}, {==}) : {_ == Nat.add(c, Nat.double(Nat.add(bb, Nat.double(T)))) : Nat} %Equal.sym(Nat, Nat.add(R, W.scale(K, P)), Nat.add(bb, Nat.double(T)), ih) : {Nat.add(c, Nat.double(_)) == Nat.add(c, Nat.double(Nat.add(bb, Nat.double(T)))) : Nat} {==}def Laws.shl_put(n, c, w): match n: case 0n: match c w: case False{} WNil{}: {==} case True{} WNil{}: {==} case 1n++p: match c w: case False{} WCon{False{}, +t}: shl_step(0n, Word.to_nat(p, Word.shl.put(p, False{}, t)), W.top(p, False{}, t), W.pow2(p), 0n, Word.to_nat(p, t), Laws.shl_put(p, False{}, t)) case False{} WCon{True{}, +t}: shl_step(0n, Word.to_nat(p, Word.shl.put(p, True{}, t)), W.top(p, True{}, t), W.pow2(p), 1n, Word.to_nat(p, t), Laws.shl_put(p, True{}, t)) case True{} WCon{False{}, +t}: shl_step(1n, Word.to_nat(p, Word.shl.put(p, False{}, t)), W.top(p, False{}, t), W.pow2(p), 0n, Word.to_nat(p, t), Laws.shl_put(p, False{}, t)) case True{} WCon{True{}, +t}: shl_step(1n, Word.to_nat(p, Word.shl.put(p, True{}, t)), W.top(p, True{}, t), W.pow2(p), 1n, Word.to_nat(p, t), Laws.shl_put(p, True{}, t))def Laws.shl_nat(n, w): match n: case 0n: match w: case WNil{}: {==} case 1n++p: match w: case WCon{+b, +t}: Laws.shl_put(1n+p, False{}, WCon{b, t})def Laws.shr_pad(n, w): match n: case 0n: match w: case WNil{}: {==} case 1n++p: match w: case WCon{False{}, +t}: %Laws.shr_pad(p, t) : {Nat.double(Word.to_nat(1n+p, Word.shr.pad(p, t))) == Nat.double(_) : Nat} {==} case WCon{True{}, +t}: %Laws.shr_pad(p, t) : {1n+Nat.double(Word.to_nat(1n+p, Word.shr.pad(p, t))) == 1n+Nat.double(_) : Nat} {==}def Laws.shr_nat(n, w): match n: case 0n: match w: case WNil{}: {==} case 1n++p: match w: case WCon{False{}, +t}: %Laws.shr_pad(p, t) : {Nat.double(Word.to_nat(1n+p, Word.shr.pad(p, t))) == Nat.double(_) : Nat} {==} case WCon{True{}, +t}: %Laws.shr_pad(p, t) : {1n+Nat.double(Word.to_nat(1n+p, Word.shr.pad(p, t))) == 1n+Nat.double(_) : Nat} {==}# Comparison# ----------def cmp_bits_00(+x: Nat, +y: Nat) -> {Word.cmp.fin(False{}, False{}, Nat.cmp(x, y)) == Nat.cmp(Nat.double(x), Nat.double(y)) : Cmp}: match x y: case 0n 0n: {==} case 0n 1n++q: {==} case 1n++p 0n: {==} case 1n++p 1n++q: cmp_bits_00(p, q)def cmp_bits_01(+x: Nat, +y: Nat) -> {Word.cmp.fin(False{}, True{}, Nat.cmp(x, y)) == Nat.cmp(Nat.double(x), 1n+Nat.double(y)) : Cmp}: match x y: case 0n 0n: {==} case 0n 1n++q: {==} case 1n++p 0n: {==} case 1n++p 1n++q: cmp_bits_01(p, q)def cmp_bits_10(+x: Nat, +y: Nat) -> {Word.cmp.fin(True{}, False{}, Nat.cmp(x, y)) == Nat.cmp(1n+Nat.double(x), Nat.double(y)) : Cmp}: match x y: case 0n 0n: {==} case 0n 1n++q: {==} case 1n++p 0n: {==} case 1n++p 1n++q: cmp_bits_10(p, q)def cmp_bits_11(+x: Nat, +y: Nat) -> {Word.cmp.fin(True{}, True{}, Nat.cmp(x, y)) == Nat.cmp(1n+Nat.double(x), 1n+Nat.double(y)) : Cmp}: match x y: case 0n 0n: {==} case 0n 1n++q: {==} case 1n++p 0n: {==} case 1n++p 1n++q: cmp_bits_11(p, q)def Laws.cmp_nat(n, a, b): match n: case 0n: match a b: case WNil{} WNil{}: {==} case 1n++p: match a b: case WCon{False{}, +at} WCon{False{}, +bt}: %cmp_bits_00(Word.to_nat(p, at), Word.to_nat(p, bt)) : {Word.cmp.fin(False{}, False{}, Word.cmp(p, at, bt)) == _ : Cmp} %Laws.cmp_nat(p, at, bt) : {Word.cmp.fin(False{}, False{}, Word.cmp(p, at, bt)) == Word.cmp.fin(False{}, False{}, _) : Cmp} {==} case WCon{False{}, +at} WCon{True{}, +bt}: %cmp_bits_01(Word.to_nat(p, at), Word.to_nat(p, bt)) : {Word.cmp.fin(False{}, True{}, Word.cmp(p, at, bt)) == _ : Cmp} %Laws.cmp_nat(p, at, bt) : {Word.cmp.fin(False{}, True{}, Word.cmp(p, at, bt)) == Word.cmp.fin(False{}, True{}, _) : Cmp} {==} case WCon{True{}, +at} WCon{False{}, +bt}: %cmp_bits_10(Word.to_nat(p, at), Word.to_nat(p, bt)) : {Word.cmp.fin(True{}, False{}, Word.cmp(p, at, bt)) == _ : Cmp} %Laws.cmp_nat(p, at, bt) : {Word.cmp.fin(True{}, False{}, Word.cmp(p, at, bt)) == Word.cmp.fin(True{}, False{}, _) : Cmp} {==} case WCon{True{}, +at} WCon{True{}, +bt}: %cmp_bits_11(Word.to_nat(p, at), Word.to_nat(p, bt)) : {Word.cmp.fin(True{}, True{}, Word.cmp(p, at, bt)) == _ : Cmp} %Laws.cmp_nat(p, at, bt) : {Word.cmp.fin(True{}, True{}, Word.cmp(p, at, bt)) == Word.cmp.fin(True{}, True{}, _) : Cmp} {==}# U32# ---def Laws.u32_xor_comm(a, b): match a b: case U32{x} U32{y}: %Laws.xor_comm(32n, x, y) : {U32{Word.xor(32n, x, y)} == U32{_} : U32} {==}def Laws.u32_and_comm(a, b): match a b: case U32{x} U32{y}: %Laws.and_comm(32n, x, y) : {U32{Word.and(32n, x, y)} == U32{_} : U32} {==}def Laws.u32_or_comm(a, b): match a b: case U32{x} U32{y}: %Laws.or_comm(32n, x, y) : {U32{Word.or(32n, x, y)} == U32{_} : U32} {==}def Laws.u32_xor_assoc(a, b, c): match a b c: case U32{+x} U32{+y} U32{+z}: %Laws.xor_assoc(32n, x, y, z) : {U32{Word.xor(32n, x, Word.xor(32n, y, z))} == U32{_} : U32} {==}def Laws.u32_and_assoc(a, b, c): match a b c: case U32{+x} U32{+y} U32{+z}: %Laws.and_assoc(32n, x, y, z) : {U32{Word.and(32n, x, Word.and(32n, y, z))} == U32{_} : U32} {==}def Laws.u32_or_assoc(a, b, c): match a b c: case U32{+x} U32{+y} U32{+z}: %Laws.or_assoc(32n, x, y, z) : {U32{Word.or(32n, x, Word.or(32n, y, z))} == U32{_} : U32} {==}def Laws.u32_add_assoc(a, b, c): match a b c: case U32{+x} U32{+y} U32{+z}: %Laws.add_assoc(32n, x, y, z) : {U32{Word.add(32n, x, Word.add(32n, y, z))} == U32{_} : U32} {==}def Laws.u32_add_zero(a): match a: case U32{x}: %Laws.add_zero(32n, x) : {U32{Word.add(32n, x, Word.zero(32n))} == U32{_} : U32} {==}def Laws.u32_xor_zero(a): match a: case U32{x}: %Laws.xor_zero(32n, x) : {U32{Word.xor(32n, x, Word.zero(32n))} == U32{_} : U32} {==}def Laws.u32_xor_self(a): match a: case U32{+x}: %Laws.xor_self(32n, x) : {U32{Word.xor(32n, x, x)} == U32{_} : U32} {==}def Laws.u32_not_not(a): match a: case U32{x}: %Laws.not_not(32n, x) : {U32{Word.not(32n, Word.not(32n, x))} == U32{_} : U32} {==}def Laws.u32_to_nat_inj(a, b, h): match a b: case U32{+x} U32{+y}: %Laws.to_nat_inj(32n, x, y, h) : {U32{x} == U32{_} : U32} {==}def Laws.u32_sub_nat(a, b, d, h): match a b: case U32{+x} U32{+y}: Laws.sub_nat(32n, x, y, d, h)def Laws.u32_cmp_nat(a, b): match a b: case U32{x} U32{y}: Laws.cmp_nat(32n, x, y)def Laws.u32_lt_nat(a, b): match a b: case U32{+x} U32{+y}: %Laws.cmp_nat(32n, x, y) : {Cmp.is_lt(Word.cmp(32n, x, y)) == Cmp.is_lt(_) : Bool} {==}def Laws.u32_le_nat(a, b): match a b: case U32{+x} U32{+y}: %Laws.cmp_nat(32n, x, y) : {Cmp.is_le(Word.cmp(32n, x, y)) == Cmp.is_le(_) : Bool} {==}# Multiplication# --------------def scale_mul(K: Bool, +P: Nat) -> {W.scale(K, P) == Nat.mul(W.b2n(K), P) : Nat}: match K: case False{}: {==} case True{}: N.add_zero(P)def to_nat_zero(+n: Nat) -> {0n == Word.to_nat(n, Word.zero(n)) : Nat}: match n: case 0n: {==} case 1n++p: %to_nat_zero(p) : {0n == Nat.double(_) : Nat} {==}def Laws.mul_go_nat(n, m, a, b, acc): match m: case 0n: {==} case 1n++mp: match a: case WCon{False{}, +at}: %MUL.mul_add_r_rev(W.mulq(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), W.b2n(W.top(n, False{}, b))), W.pow2(n)) : {Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), _) == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %MUL.mul_assoc(Word.to_nat(mp, at), W.b2n(W.top(n, False{}, b)), W.pow2(n)) : {Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), Nat.add(Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), acc), W.pow2(n)), _)) == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %scale_mul(W.top(n, False{}, b), W.pow2(n)) : {Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), Nat.add(Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), acc), W.pow2(n)), Nat.mul(Word.to_nat(mp, at), _))) == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %A.ac([Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), acc), W.pow2(n)), Nat.mul(Word.to_nat(mp, at), W.scale(W.top(n, False{}, b), W.pow2(n)))], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAtom{2n}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}, {==}) : {_ == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), acc), W.pow2(n))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), Laws.mul_go_nat(n, mp, at, Word.shl(n, b), acc)) : {Nat.add(_, Nat.mul(Word.to_nat(mp, at), W.scale(W.top(n, False{}, b), W.pow2(n)))) == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %A.ac([Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b))), Nat.mul(Word.to_nat(mp, at), W.scale(W.top(n, False{}, b), W.pow2(n)))], A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAtom{2n}}, {==}) : {_ == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %MUL.mul_add_l(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)), W.scale(W.top(n, False{}, b), W.pow2(n))) : {Nat.add(Word.to_nat(n, acc), _) == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.shl(n, b)), W.scale(W.top(n, False{}, b), W.pow2(n))), Nat.double(Word.to_nat(n, b)), Laws.shl_nat(n, b)) : {Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), _)) == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %MUL.mul_double_r(Word.to_nat(mp, at), Word.to_nat(n, b)) : {Nat.add(Word.to_nat(n, acc), _) == Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))) : Nat} %MUL.mul_double_l(Word.to_nat(mp, at), Word.to_nat(n, b)) : {Nat.add(Word.to_nat(n, acc), Nat.double(Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, b)))) == Nat.add(Word.to_nat(n, acc), _) : Nat} {==} case WCon{True{}, +at}: %MUL.mul_add_r_rev(W.mulq(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(Nat.mul(Word.to_nat(mp, at), W.b2n(W.top(n, False{}, b))), W.b2n(W.carry(n, acc, b, False{}))), W.pow2(n)) : {Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), _) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %MUL.mul_add_r_rev(Nat.mul(Word.to_nat(mp, at), W.b2n(W.top(n, False{}, b))), W.b2n(W.carry(n, acc, b, False{})), W.pow2(n)) : {Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), Nat.add(Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), W.pow2(n)), _)) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %MUL.mul_assoc(Word.to_nat(mp, at), W.b2n(W.top(n, False{}, b)), W.pow2(n)) : {Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), Nat.add(Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), W.pow2(n)), Nat.add(_, Nat.mul(W.b2n(W.carry(n, acc, b, False{})), W.pow2(n))))) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %scale_mul(W.top(n, False{}, b), W.pow2(n)) : {Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), Nat.add(Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), W.pow2(n)), Nat.add(Nat.mul(Word.to_nat(mp, at), _), Nat.mul(W.b2n(W.carry(n, acc, b, False{})), W.pow2(n))))) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %scale_mul(W.carry(n, acc, b, False{}), W.pow2(n)) : {Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), Nat.add(Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), W.pow2(n)), Nat.add(Nat.mul(Word.to_nat(mp, at), W.scale(W.top(n, False{}, b), W.pow2(n))), _))) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %A.ac([Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), W.pow2(n)), Nat.mul(Word.to_nat(mp, at), W.scale(W.top(n, False{}, b), W.pow2(n))), W.scale(W.carry(n, acc, b, False{}), W.pow2(n))], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAdd{A.EAtom{2n}, A.EAtom{3n}}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EAdd{A.EAtom{2n}, A.EAtom{3n}}}}, {==}) : {_ == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), Nat.mul(W.mulq(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), W.pow2(n))), Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), Laws.mul_go_nat(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))) : {Nat.add(_, Nat.add(Nat.mul(Word.to_nat(mp, at), W.scale(W.top(n, False{}, b), W.pow2(n))), W.scale(W.carry(n, acc, b, False{}), W.pow2(n)))) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %A.ac([Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b))), Nat.mul(Word.to_nat(mp, at), W.scale(W.top(n, False{}, b), W.pow2(n))), W.scale(W.carry(n, acc, b, False{}), W.pow2(n))], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{3n}}, A.EAdd{A.EAtom{1n}, A.EAtom{2n}}}, A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAdd{A.EAtom{2n}, A.EAtom{3n}}}, {==}) : {_ == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.add(n, acc, b)), W.scale(W.carry(n, acc, b, False{}), W.pow2(n))), Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), 0n)), Laws.adc_nat(n, acc, b, False{})) : {Nat.add(_, Nat.add(Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b))), Nat.mul(Word.to_nat(mp, at), W.scale(W.top(n, False{}, b), W.pow2(n))))) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %MUL.mul_add_l(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)), W.scale(W.top(n, False{}, b), W.pow2(n))) : {Nat.add(Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), 0n)), _) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.shl(n, b)), W.scale(W.top(n, False{}, b), W.pow2(n))), Nat.double(Word.to_nat(n, b)), Laws.shl_nat(n, b)) : {Nat.add(Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), 0n)), Nat.mul(Word.to_nat(mp, at), _)) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %MUL.mul_double_r(Word.to_nat(mp, at), Word.to_nat(n, b)) : {Nat.add(Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), 0n)), _) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)))) : Nat} %MUL.mul_double_l(Word.to_nat(mp, at), Word.to_nat(n, b)) : {Nat.add(Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), 0n)), Nat.double(Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, b)))) == Nat.add(Word.to_nat(n, acc), Nat.add(Word.to_nat(n, b), _)) : Nat} A.ac([Word.to_nat(n, acc), Word.to_nat(n, b), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, b))], A.EAdd{A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EZero{}}}, A.EDbl{A.EAtom{2n}}}, A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{1n}, A.EDbl{A.EAtom{2n}}}}, {==})def mul_nat.z(+n: Nat, +M: Nat) -> {Nat.add(Word.to_nat(n, Word.zero(n)), M) == M : Nat}: %to_nat_zero(n) : {Nat.add(_, M) == M : Nat} {==}def Laws.mul_nat(n, a, b): Equal.trans(Nat, 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.add(Word.to_nat(n, Word.zero(n)), Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), Laws.mul_go_nat(n, n, a, b, Word.zero(n)), mul_nat.z(n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))))def mul_exact.e(+n: Nat, +a: Word(n), +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.add(Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), 0n) : Nat}: %N.add_zero(Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))) : {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} Laws.mul_nat(n, a, b)def Laws.mul_exact(n, a, b, g, h): uniq(Word.to_nat(n, Word.mul(n, a, b)), Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), W.pow2(n), Word.to_nat(n, Word.not(n, Word.mul(n, a, b))), g, W.mulq(n, n, a, b, Word.zero(n)), 0n, mul_exact.e(n, a, b), Laws.not_nat(n, Word.mul(n, a, b)), h)def mul_comm.e(+n: Nat, +a: Word(n), +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.add(Word.to_nat(n, Word.mul(n, b, a)), Nat.mul(W.mulq(n, n, b, a, Word.zero(n)), W.pow2(n))) : Nat}: Equal.trans(Nat, 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.add(Word.to_nat(n, Word.mul(n, b, a)), Nat.mul(W.mulq(n, n, b, a, Word.zero(n)), W.pow2(n))), Laws.mul_nat(n, a, b), Equal.trans(Nat, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.mul(Word.to_nat(n, b), Word.to_nat(n, a)), Nat.add(Word.to_nat(n, Word.mul(n, b, a)), Nat.mul(W.mulq(n, n, b, a, Word.zero(n)), W.pow2(n))), MUL.mul_comm(Word.to_nat(n, a), Word.to_nat(n, b)), Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.mul(n, b, a)), Nat.mul(W.mulq(n, n, b, a, Word.zero(n)), W.pow2(n))), Nat.mul(Word.to_nat(n, b), Word.to_nat(n, a)), Laws.mul_nat(n, b, a))))def Laws.mul_comm(n, a, b): Laws.to_nat_inj(n, Word.mul(n, a, b), Word.mul(n, b, a), uniq(Word.to_nat(n, Word.mul(n, a, b)), Word.to_nat(n, Word.mul(n, b, a)), W.pow2(n), Word.to_nat(n, Word.not(n, Word.mul(n, a, b))), Word.to_nat(n, Word.not(n, Word.mul(n, b, a))), W.mulq(n, n, a, b, Word.zero(n)), W.mulq(n, n, b, a, Word.zero(n)), mul_comm.e(n, a, b), Laws.not_nat(n, Word.mul(n, a, b)), Laws.not_nat(n, Word.mul(n, b, a))))def Laws.u32_mul_comm(a, b): match a b: case U32{+x} U32{+y}: %Laws.mul_comm(32n, x, y) : {U32{Word.mul(32n, x, y)} == U32{_} : U32} {==}