proofs/lib/u32alg.bend

bend-collections-laws-crypto@1.0.0.0 · 330 lines · 36 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as AD
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as DQ
8
9# Modular (U32) addition algebra, derived from Base's Word adder through
10# the retained LRU carry-conservation law
11#   unsigned(adc a b c) + 2^n * carry == c + unsigned a + unsigned b
12# and uniqueness of the representation r + 2^n * k with r < 2^n.
13
14def sc(+n: Nat, +k: Nat) -> Nat:
15  S.scale_binary(n, k)
16
17def uw(+n: Nat, +w: Word(n)) -> Nat:
18  S.unsigned(n, w)
19
20def cy(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool) -> Nat:
21  S.bit_value(AD.carry_out(n, a, b, c))
22
23# ---- Nat helpers ----
24
25def add_cancel_r(+a: Nat, +b: Nat, +c: Nat, +e: {Nat.add(a, c) == Nat.add(b, c) : Nat}) -> {a == b : Nat}:
26  match c:
27    case 0n:
28      Equal.trans(Nat, a, Nat.add(a, 0n), b, Equal.sym(Nat, Nat.add(a, 0n), a, N.add_zero(a)), Equal.trans(Nat, Nat.add(a, 0n), Nat.add(b, 0n), b, e, N.add_zero(b)))
29    case 1n+k:
30      add_cancel_r(a, b, k, N.succ_inj(Nat.add(a, k), Nat.add(b, k), Equal.trans(Nat, 1n+Nat.add(a, k), Nat.add(a, 1n+k), 1n+Nat.add(b, k), Equal.sym(Nat, Nat.add(a, 1n+k), 1n+Nat.add(a, k), N.add_succ(a, k)), Equal.trans(Nat, Nat.add(a, 1n+k), Nat.add(b, 1n+k), 1n+Nat.add(b, k), e, N.add_succ(b, k)))))
31
32# (a + b) + c == (a + c) + b
33def add_rot(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}:
34  %Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), N.add_assoc(a, b, c)) : {_ == Nat.add(Nat.add(a, c), b) : Nat}
35  %Equal.sym(Nat, Nat.add(Nat.add(a, c), b), Nat.add(a, Nat.add(c, b)), N.add_assoc(a, c, b)) : {Nat.add(a, Nat.add(b, c)) == _ : Nat}
36  %N.add_comm(c, b) : {Nat.add(a, _) == Nat.add(a, Nat.add(c, b)) : Nat}
37  {==}
38
39def sc_zero(+n: Nat) -> {sc(n, 0n) == 0n : Nat}:
40  match n:
41    case 0n:
42      {==}
43    case 1n+p:
44      %Equal.sym(Nat, sc(p, 0n), 0n, sc_zero(p)) : {Nat.double(_) == 0n : Nat}
45      {==}
46
47def sc_add(+n: Nat, +x: Nat, +y: Nat) -> {Nat.add(sc(n, x), sc(n, y)) == sc(n, Nat.add(x, y)) : Nat}:
48  match n:
49    case 0n:
50      {==}
51    case 1n+p:
52      %Equal.sym(Nat, Nat.add(Nat.double(sc(p, x)), Nat.double(sc(p, y))), Nat.double(Nat.add(sc(p, x), sc(p, y))), N.add_double(sc(p, x), sc(p, y))) : {_ == Nat.double(sc(p, Nat.add(x, y))) : Nat}
53      Equal.cong(Nat, Nat, Nat.double, Nat.add(sc(p, x), sc(p, y)), sc(p, Nat.add(x, y)), sc_add(p, x, y))
54
55# M <= r + (M + s)
56def le_shift(+r: Nat, +m: Nat, +s: Nat) -> {Nat.is_le(m, Nat.add(r, Nat.add(m, s))) == True{} : Bool}:
57  %N.add_comm(Nat.add(m, s), r) : {Nat.is_le(m, _) == True{} : Bool}
58  %Equal.sym(Nat, Nat.add(Nat.add(m, s), r), Nat.add(m, Nat.add(s, r)), N.add_assoc(m, s, r)) : {Nat.is_le(m, _) == True{} : Bool}
59  N.le_add_right(m, Nat.add(s, r))
60
61def sc_succ(+n: Nat, +x: Nat) -> {sc(n, 1n+x) == Nat.add(sc(n, 1n), sc(n, x)) : Nat}:
62  Equal.sym(Nat, Nat.add(sc(n, 1n), sc(n, x)), sc(n, Nat.add(1n, x)), sc_add(n, 1n, x))
63
64# r1 < 2^n cannot equal r2 + 2^n (1 + q).
65def uniq_gap(+n: Nat, +r1: Nat, +r2: Nat, +q: Nat, +h: {Nat.add(r1, sc(n, 0n)) == Nat.add(r2, sc(n, 1n+q)) : Nat}, +b1: {Nat.is_lt(r1, sc(n, 1n)) == True{} : Bool}) -> Empty:
66  +e = Equal.trans(Nat, r1, Nat.add(r1, sc(n, 0n)), Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))),
67    %Equal.sym(Nat, sc(n, 0n), 0n, sc_zero(n)) : {r1 == Nat.add(r1, _) : Nat}
68    Equal.sym(Nat, Nat.add(r1, 0n), r1, N.add_zero(r1)),
69    %sc_succ(n, q) : {Nat.add(r1, sc(n, 0n)) == Nat.add(r2, _) : Nat}
70    h)
71  L.true_false(Equal.trans(Bool, True{}, Nat.is_le(sc(n, 1n), r1), False{}, Equal.sym(Bool, Nat.is_le(sc(n, 1n), r1), True{}, L.subst(Nat, z => {Nat.is_le(sc(n, 1n), z) == True{} : Bool}, Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), r1, Equal.sym(Nat, r1, Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), e), le_shift(r2, sc(n, 1n), sc(n, q)))), N.lt_not_le(r1, sc(n, 1n), b1)))
72
73# r1 + 2^n x == r2 + 2^n y with r1, r2 < 2^n forces r1 == r2.
74def uniq(+n: Nat, +r1: Nat, +r2: Nat, +x: Nat, +y: Nat, +h: {Nat.add(r1, sc(n, x)) == Nat.add(r2, sc(n, y)) : Nat}, +b1: {Nat.is_lt(r1, sc(n, 1n)) == True{} : Bool}, +b2: {Nat.is_lt(r2, sc(n, 1n)) == True{} : Bool}) -> {r1 == r2 : Nat}:
75  match x y:
76    case 0n 0n:
77      +h0 = L.subst(Nat, q => {Nat.add(r1, q) == Nat.add(r2, q) : Nat}, sc(n, 0n), 0n, sc_zero(n), h)
78      add_cancel_r(r1, r2, 0n, h0)
79    case 0n 1n+q:
80      Empty.absurd({r1 == r2 : Nat}, uniq_gap(n, r1, r2, q, h, b1))
81    case 1n+p 0n:
82      Empty.absurd({r1 == r2 : Nat}, uniq_gap(n, r2, r1, p, Equal.sym(Nat, Nat.add(r1, sc(n, 1n+p)), Nat.add(r2, sc(n, 0n)), h), b2))
83    case 1n+p 1n+q:
84      -Mn = sc(n, 1n)
85      +h1 = L.subst(Nat, z => {Nat.add(r1, z) == Nat.add(r2, sc(n, 1n+q)) : Nat}, sc(n, 1n+p), Nat.add(sc(n, 1n), sc(n, p)), sc_succ(n, p), h)
86      +h2 = L.subst(Nat, z => {Nat.add(r1, Nat.add(sc(n, 1n), sc(n, p))) == Nat.add(r2, z) : Nat}, sc(n, 1n+q), Nat.add(sc(n, 1n), sc(n, q)), sc_succ(n, q), h1)
87      +l1 = Equal.trans(Nat, Nat.add(Nat.add(r1, sc(n, p)), sc(n, 1n)), Nat.add(r1, Nat.add(sc(n, p), sc(n, 1n))), Nat.add(r1, Nat.add(sc(n, 1n), sc(n, p))), N.add_assoc(r1, sc(n, p), sc(n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(r1, z), Nat.add(sc(n, p), sc(n, 1n)), Nat.add(sc(n, 1n), sc(n, p)), N.add_comm(sc(n, p), sc(n, 1n))))
88      +l2 = Equal.trans(Nat, Nat.add(Nat.add(r2, sc(n, q)), sc(n, 1n)), Nat.add(r2, Nat.add(sc(n, q), sc(n, 1n))), Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), N.add_assoc(r2, sc(n, q), sc(n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(r2, z), Nat.add(sc(n, q), sc(n, 1n)), Nat.add(sc(n, 1n), sc(n, q)), N.add_comm(sc(n, q), sc(n, 1n))))
89      uniq(n, r1, r2, p, q, add_cancel_r(Nat.add(r1, sc(n, p)), Nat.add(r2, sc(n, q)), sc(n, 1n), Equal.trans(Nat, Nat.add(Nat.add(r1, sc(n, p)), sc(n, 1n)), Nat.add(r1, Nat.add(sc(n, 1n), sc(n, p))), Nat.add(Nat.add(r2, sc(n, q)), sc(n, 1n)), l1, Equal.trans(Nat, Nat.add(r1, Nat.add(sc(n, 1n), sc(n, p))), Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), Nat.add(Nat.add(r2, sc(n, q)), sc(n, 1n)), h2, Equal.sym(Nat, Nat.add(Nat.add(r2, sc(n, q)), sc(n, 1n)), Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), l2)))), b1, b2)
90
91# ---- words ----
92
93def w_inj(+n: Nat, +a: Word(n), +b: Word(n), +e: {uw(n, a) == uw(n, b) : Nat}) -> {a == b : Word(n)}:
94  Equal.trans(Word(n), a, S.from_nat(n, uw(n, a)), b, Equal.sym(Word(n), S.from_nat(n, uw(n, a)), a, DQ.reconstruct(n, a)),
95    Equal.trans(Word(n), S.from_nat(n, uw(n, a)), S.from_nat(n, uw(n, b)), b, Equal.cong(Nat, Word(n), v => S.from_nat(n, v), uw(n, a), uw(n, b), e), DQ.reconstruct(n, b)))
96
97def cons(+n: Nat, +a: Word(n), +b: Word(n)) -> {Nat.add(uw(n, Word.add(n, a, b)), sc(n, cy(n, a, b, False{}))) == Nat.add(uw(n, a), uw(n, b)) : Nat}:
98  AD.adc_conservation(n, a, b, False{})
99
100def uw_zero(+n: Nat) -> {uw(n, Word.zero(n)) == 0n : Nat}:
101  match n:
102    case 0n:
103      {==}
104    case 1n+p:
105      %Equal.sym(Nat, uw(p, Word.zero(p)), 0n, uw_zero(p)) : {Nat.add(0n, Nat.double(_)) == 0n : Nat}
106      {==}
107
108def w_zero_add(+n: Nat, +b: Word(n)) -> {Word.add(n, Word.zero(n), b) == b : Word(n)}:
109  +e = cons(n, Word.zero(n), b)
110  +e2 = Equal.trans(Nat, Nat.add(uw(n, Word.add(n, Word.zero(n), b)), sc(n, cy(n, Word.zero(n), b, False{}))), Nat.add(uw(n, Word.zero(n)), uw(n, b)), Nat.add(uw(n, b), sc(n, 0n)), e,
111    %Equal.sym(Nat, uw(n, Word.zero(n)), 0n, uw_zero(n)) : {Nat.add(_, uw(n, b)) == Nat.add(uw(n, b), sc(n, 0n)) : Nat}
112    %Equal.sym(Nat, sc(n, 0n), 0n, sc_zero(n)) : {uw(n, b) == Nat.add(uw(n, b), _) : Nat}
113    Equal.sym(Nat, Nat.add(uw(n, b), 0n), uw(n, b), N.add_zero(uw(n, b))))
114  w_inj(n, Word.add(n, Word.zero(n), b), b, uniq(n, uw(n, Word.add(n, Word.zero(n), b)), uw(n, b), cy(n, Word.zero(n), b, False{}), 0n, e2, U.WB_unsigned(n, Word.add(n, Word.zero(n), b)), U.WB_unsigned(n, b)))
115
116def w_assoc(+n: Nat, +a: Word(n), +b: Word(n), +c: Word(n)) -> {Word.add(n, Word.add(n, a, b), c) == Word.add(n, a, Word.add(n, b, c)) : Word(n)}:
117  -s = Word.add(n, a, b)
118  -t = Word.add(n, b, c)
119  +ua = uw(n, a)
120  +ub = uw(n, b)
121  +uc = uw(n, c)
122  +us = uw(n, Word.add(n, a, b))
123  +ut = uw(n, Word.add(n, b, c))
124  +uL = uw(n, Word.add(n, Word.add(n, a, b), c))
125  +uR = uw(n, Word.add(n, a, Word.add(n, b, c)))
126  +c1 = cy(n, a, b, False{})
127  +c2 = cy(n, b, c, False{})
128  +c3 = cy(n, Word.add(n, a, b), c, False{})
129  +c4 = cy(n, a, Word.add(n, b, c), False{})
130  +e1 = cons(n, Word.add(n, a, b), c)
131  +e2 = cons(n, a, b)
132  +e3 = cons(n, a, Word.add(n, b, c))
133  +e4 = cons(n, b, c)
134  # uL + sc(c3 + c1) == (ua + ub) + uc
135  +left = Equal.trans(Nat, Nat.add(uL, sc(n, Nat.add(c3, c1))), Nat.add(Nat.add(uL, sc(n, c3)), sc(n, c1)), Nat.add(Nat.add(ua, ub), uc),
136    %sc_add(n, c3, c1) : {Nat.add(uL, _) == Nat.add(Nat.add(uL, sc(n, c3)), sc(n, c1)) : Nat}
137    Equal.sym(Nat, Nat.add(Nat.add(uL, sc(n, c3)), sc(n, c1)), Nat.add(uL, Nat.add(sc(n, c3), sc(n, c1))), N.add_assoc(uL, sc(n, c3), sc(n, c1))),
138    %Equal.sym(Nat, Nat.add(uL, sc(n, c3)), Nat.add(us, uc), e1) : {Nat.add(_, sc(n, c1)) == Nat.add(Nat.add(ua, ub), uc) : Nat}
139    %Equal.sym(Nat, Nat.add(Nat.add(us, uc), sc(n, c1)), Nat.add(Nat.add(us, sc(n, c1)), uc), add_rot(us, uc, sc(n, c1))) : {_ == Nat.add(Nat.add(ua, ub), uc) : Nat}
140    %Equal.sym(Nat, Nat.add(us, sc(n, c1)), Nat.add(ua, ub), e2) : {Nat.add(_, uc) == Nat.add(Nat.add(ua, ub), uc) : Nat}
141    {==})
142  # uR + sc(c4 + c2) == (ua + ub) + uc
143  +right = Equal.trans(Nat, Nat.add(uR, sc(n, Nat.add(c4, c2))), Nat.add(Nat.add(uR, sc(n, c4)), sc(n, c2)), Nat.add(Nat.add(ua, ub), uc),
144    %sc_add(n, c4, c2) : {Nat.add(uR, _) == Nat.add(Nat.add(uR, sc(n, c4)), sc(n, c2)) : Nat}
145    Equal.sym(Nat, Nat.add(Nat.add(uR, sc(n, c4)), sc(n, c2)), Nat.add(uR, Nat.add(sc(n, c4), sc(n, c2))), N.add_assoc(uR, sc(n, c4), sc(n, c2))),
146    %Equal.sym(Nat, Nat.add(uR, sc(n, c4)), Nat.add(ua, ut), e3) : {Nat.add(_, sc(n, c2)) == Nat.add(Nat.add(ua, ub), uc) : Nat}
147    %Equal.sym(Nat, Nat.add(Nat.add(ua, ut), sc(n, c2)), Nat.add(ua, Nat.add(ut, sc(n, c2))), N.add_assoc(ua, ut, sc(n, c2))) : {_ == Nat.add(Nat.add(ua, ub), uc) : Nat}
148    %Equal.sym(Nat, Nat.add(ut, sc(n, c2)), Nat.add(ub, uc), e4) : {Nat.add(ua, _) == Nat.add(Nat.add(ua, ub), uc) : Nat}
149    Equal.sym(Nat, Nat.add(Nat.add(ua, ub), uc), Nat.add(ua, Nat.add(ub, uc)), N.add_assoc(ua, ub, uc)))
150  w_inj(n, Word.add(n, Word.add(n, a, b), c), Word.add(n, a, Word.add(n, b, c)), uniq(n, uL, uR, Nat.add(c3, c1), Nat.add(c4, c2), Equal.trans(Nat, Nat.add(uL, sc(n, Nat.add(c3, c1))), Nat.add(Nat.add(ua, ub), uc), Nat.add(uR, sc(n, Nat.add(c4, c2))), left, Equal.sym(Nat, Nat.add(uR, sc(n, Nat.add(c4, c2))), Nat.add(Nat.add(ua, ub), uc), right)), U.WB_unsigned(n, Word.add(n, Word.add(n, a, b), c)), U.WB_unsigned(n, Word.add(n, a, Word.add(n, b, c)))))
151
152# ---- subtraction ----
153
154def adc_con_not(+p: Nat, +at: Word(p), +bt: Word(p), sk: Bool & Bool, ih: @+k: Bool -> {Word.adc(p, at, bt, True{}, k) == Word.adc(p, at, Word.not(p, bt), False{}, k) : Word(p)}) -> {Word.adc.con(p, at, bt, True{}, sk) == Word.adc.con(p, at, Word.not(p, bt), False{}, sk) : Word(1n+p)}:
155  match sk:
156    case Tuple{s, k}:
157      Equal.cong(Word(p), Word(1n+p), w => WCon{s, w}, Word.adc(p, at, bt, True{}, k), Word.adc(p, at, Word.not(p, bt), False{}, k), ih(k))
158
159# Subtraction is addition of the complement with an incoming carry.
160def adc_not(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool) -> {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}:
161  match n:
162    case 0n:
163      {==}
164    case 1n+p:
165      match a b:
166        case WCon{x, at} WCon{y, bt}:
167          adc_con_not(p, at, bt, Bool.full_add(x, Bool.not(y), c), k => adc_not(p, at, bt, k))
168
169# 1 + unsigned(not b) + unsigned(b) == 2^n
170def not_value(+n: Nat, +b: Word(n)) -> {Nat.add(1n, Nat.add(uw(n, Word.not(n, b)), uw(n, b))) == sc(n, 1n) : Nat}:
171  match n:
172    case 0n:
173      {==}
174    case 1n+p:
175      match b:
176        case WCon{True{}, bt}:
177          +ih = not_value(p, bt)
178          -A = uw(p, Word.not(p, bt))
179          -B = uw(p, bt)
180          # 1 + (0 + 2A) + (1 + 2B) == 2 (1 + (A + B))
181          %Equal.sym(Nat, Nat.add(Nat.double(uw(p, Word.not(p, bt))), 1n+Nat.double(uw(p, bt))), 1n+Nat.add(Nat.double(uw(p, Word.not(p, bt))), Nat.double(uw(p, bt))), N.add_succ(Nat.double(uw(p, Word.not(p, bt))), Nat.double(uw(p, bt)))) : {1n+_ == Nat.double(sc(p, 1n)) : Nat}
182          %Equal.sym(Nat, sc(p, 1n), Nat.add(1n, Nat.add(uw(p, Word.not(p, bt)), uw(p, bt))), Equal.sym(Nat, Nat.add(1n, Nat.add(uw(p, Word.not(p, bt)), uw(p, bt))), sc(p, 1n), ih)) : {2n+Nat.add(Nat.double(uw(p, Word.not(p, bt))), Nat.double(uw(p, bt))) == Nat.double(_) : Nat}
183          Equal.cong(Nat, Nat, z => 2n+z, Nat.add(Nat.double(uw(p, Word.not(p, bt))), Nat.double(uw(p, bt))), Nat.double(Nat.add(uw(p, Word.not(p, bt)), uw(p, bt))), N.add_double(uw(p, Word.not(p, bt)), uw(p, bt)))
184        case WCon{False{}, bt}:
185          +ih = not_value(p, bt)
186          %Equal.sym(Nat, sc(p, 1n), Nat.add(1n, Nat.add(uw(p, Word.not(p, bt)), uw(p, bt))), Equal.sym(Nat, Nat.add(1n, Nat.add(uw(p, Word.not(p, bt)), uw(p, bt))), sc(p, 1n), ih)) : {2n+Nat.add(Nat.double(uw(p, Word.not(p, bt))), Nat.double(uw(p, bt))) == Nat.double(_) : Nat}
187          Equal.cong(Nat, Nat, z => 2n+z, Nat.add(Nat.double(uw(p, Word.not(p, bt))), Nat.double(uw(p, bt))), Nat.double(Nat.add(uw(p, Word.not(p, bt)), uw(p, bt))), N.add_double(uw(p, Word.not(p, bt)), uw(p, bt)))
188
189def cons_sub(+n: Nat, +x: Word(n), +a: Word(n)) -> {Nat.add(uw(n, Word.sub(n, x, a)), sc(n, cy(n, x, Word.not(n, a), True{}))) == Nat.add(1n, Nat.add(uw(n, x), uw(n, Word.not(n, a)))) : Nat}:
190  %Equal.sym(Word(n), Word.adc(n, x, a, True{}, True{}), Word.adc(n, x, Word.not(n, a), False{}, True{}), adc_not(n, x, a, True{})) : {Nat.add(uw(n, _), sc(n, cy(n, x, Word.not(n, a), True{}))) == Nat.add(1n, Nat.add(uw(n, x), uw(n, Word.not(n, a)))) : Nat}
191  AD.adc_conservation(n, x, Word.not(n, a), True{})
192
193# (a + b) - a == b
194def arith_sub(+ux: Nat, +un: Nat, +ua: Nat, +ub: Nat, +k: Nat, +e: {Nat.add(ux, k) == Nat.add(ua, ub) : Nat}) -> {Nat.add(Nat.add(1n, Nat.add(ux, un)), k) == Nat.add(ub, Nat.add(1n, Nat.add(un, ua))) : Nat}:
195  # both sides are 1 + ((ua + ub) + un)
196  +p1 = N.succ_cong(Nat.add(Nat.add(ux, un), k), Nat.add(Nat.add(ua, ub), un), Equal.trans(Nat, Nat.add(Nat.add(ux, un), k), Nat.add(Nat.add(ux, k), un), Nat.add(Nat.add(ua, ub), un), add_rot(ux, un, k), Equal.cong(Nat, Nat, z => Nat.add(z, un), Nat.add(ux, k), Nat.add(ua, ub), e)))
197  +q = Equal.trans(Nat, Nat.add(Nat.add(ua, ub), un), Nat.add(ua, Nat.add(ub, un)), Nat.add(ub, Nat.add(un, ua)), N.add_assoc(ua, ub, un), Equal.trans(Nat, Nat.add(ua, Nat.add(ub, un)), Nat.add(Nat.add(ub, un), ua), Nat.add(ub, Nat.add(un, ua)), N.add_comm(ua, Nat.add(ub, un)), N.add_assoc(ub, un, ua)))
198  Equal.trans(Nat, Nat.add(Nat.add(1n, Nat.add(ux, un)), k), 1n+Nat.add(Nat.add(ua, ub), un), Nat.add(ub, Nat.add(1n, Nat.add(un, ua))), p1,
199    Equal.trans(Nat, 1n+Nat.add(Nat.add(ua, ub), un), 1n+Nat.add(ub, Nat.add(un, ua)), Nat.add(ub, 1n+Nat.add(un, ua)), N.succ_cong(Nat.add(Nat.add(ua, ub), un), Nat.add(ub, Nat.add(un, ua)), q), Equal.sym(Nat, Nat.add(ub, 1n+Nat.add(un, ua)), 1n+Nat.add(ub, Nat.add(un, ua)), N.add_succ(ub, Nat.add(un, ua)))))
200
201# (v - a) + a == v
202def w_add_sub(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.sub(n, Word.add(n, a, b), a) == b : Word(n)}:
203  +ux = uw(n, Word.add(n, a, b))
204  +ua = uw(n, a)
205  +ub = uw(n, b)
206  +un = uw(n, Word.not(n, a))
207  +r = uw(n, Word.sub(n, Word.add(n, a, b), a))
208  +c1 = cy(n, a, b, False{})
209  +c5 = cy(n, Word.add(n, a, b), Word.not(n, a), True{})
210  +e2 = cons(n, a, b)
211  +e5 = cons_sub(n, Word.add(n, a, b), a)
212  +nv = not_value(n, a)
213  # r + sc(c5 + c1) == ub + sc(1)
214  +chain = Equal.trans(Nat, Nat.add(r, sc(n, Nat.add(c5, c1))), Nat.add(Nat.add(r, sc(n, c5)), sc(n, c1)), Nat.add(ub, sc(n, 1n)),
215    %sc_add(n, c5, c1) : {Nat.add(r, _) == Nat.add(Nat.add(r, sc(n, c5)), sc(n, c1)) : Nat}
216    Equal.sym(Nat, Nat.add(Nat.add(r, sc(n, c5)), sc(n, c1)), Nat.add(r, Nat.add(sc(n, c5), sc(n, c1))), N.add_assoc(r, sc(n, c5), sc(n, c1))),
217    %Equal.sym(Nat, Nat.add(r, sc(n, c5)), Nat.add(1n, Nat.add(ux, un)), e5) : {Nat.add(_, sc(n, c1)) == Nat.add(ub, sc(n, 1n)) : Nat}
218    %nv : {Nat.add(Nat.add(1n, Nat.add(ux, un)), sc(n, c1)) == Nat.add(ub, _) : Nat}
219    arith_sub(ux, un, ua, ub, sc(n, c1), e2))
220  w_inj(n, Word.sub(n, Word.add(n, a, b), a), b, uniq(n, r, ub, Nat.add(c5, c1), 1n, chain, U.WB_unsigned(n, Word.sub(n, Word.add(n, a, b), a)), U.WB_unsigned(n, b)))
221
222# (v - a) + a == v
223def w_sub_add(+n: Nat, +v: Word(n), +a: Word(n)) -> {Word.add(n, Word.sub(n, v, a), a) == v : Word(n)}:
224  +uv = uw(n, v)
225  +ua = uw(n, a)
226  +un = uw(n, Word.not(n, a))
227  +us = uw(n, Word.sub(n, v, a))
228  +ut = uw(n, Word.add(n, Word.sub(n, v, a), a))
229  +c5 = cy(n, v, Word.not(n, a), True{})
230  +c6 = cy(n, Word.sub(n, v, a), a, False{})
231  +e5 = cons_sub(n, v, a)
232  +e6 = cons(n, Word.sub(n, v, a), a)
233  +nv = not_value(n, a)
234  +tail = Equal.trans(Nat, Nat.add(Nat.add(1n, Nat.add(uv, un)), ua), 1n+Nat.add(uv, Nat.add(un, ua)), Nat.add(uv, sc(n, 1n)),
235    N.succ_cong(Nat.add(Nat.add(uv, un), ua), Nat.add(uv, Nat.add(un, ua)), N.add_assoc(uv, un, ua)),
236    Equal.trans(Nat, 1n+Nat.add(uv, Nat.add(un, ua)), Nat.add(uv, 1n+Nat.add(un, ua)), Nat.add(uv, sc(n, 1n)), Equal.sym(Nat, Nat.add(uv, 1n+Nat.add(un, ua)), 1n+Nat.add(uv, Nat.add(un, ua)), N.add_succ(uv, Nat.add(un, ua))), Equal.cong(Nat, Nat, z => Nat.add(uv, z), Nat.add(1n, Nat.add(un, ua)), sc(n, 1n), nv)))
237  +chain = Equal.trans(Nat, Nat.add(ut, sc(n, Nat.add(c6, c5))), Nat.add(Nat.add(ut, sc(n, c6)), sc(n, c5)), Nat.add(uv, sc(n, 1n)),
238    %sc_add(n, c6, c5) : {Nat.add(ut, _) == Nat.add(Nat.add(ut, sc(n, c6)), sc(n, c5)) : Nat}
239    Equal.sym(Nat, Nat.add(Nat.add(ut, sc(n, c6)), sc(n, c5)), Nat.add(ut, Nat.add(sc(n, c6), sc(n, c5))), N.add_assoc(ut, sc(n, c6), sc(n, c5))),
240    %Equal.sym(Nat, Nat.add(ut, sc(n, c6)), Nat.add(us, ua), e6) : {Nat.add(_, sc(n, c5)) == Nat.add(uv, sc(n, 1n)) : Nat}
241    %Equal.sym(Nat, Nat.add(Nat.add(us, ua), sc(n, c5)), Nat.add(Nat.add(us, sc(n, c5)), ua), add_rot(us, ua, sc(n, c5))) : {_ == Nat.add(uv, sc(n, 1n)) : Nat}
242    %Equal.sym(Nat, Nat.add(us, sc(n, c5)), Nat.add(1n, Nat.add(uv, un)), e5) : {Nat.add(_, ua) == Nat.add(uv, sc(n, 1n)) : Nat}
243    tail)
244  w_inj(n, Word.add(n, Word.sub(n, v, a), a), v, uniq(n, ut, uv, Nat.add(c6, c5), 1n, chain, U.WB_unsigned(n, Word.add(n, Word.sub(n, v, a), a)), U.WB_unsigned(n, v)))
245
246# Doubling by shifting: shl.put n c w == w + w + c.
247def shl_adc(+n: Nat, +w: Word(n), +c: Bool) -> {Word.shl.put(n, c, w) == Word.adc(n, w, w, False{}, c) : Word(n)}:
248  match n:
249    case 0n:
250      match w:
251        case WNil{}:
252          {==}
253    case 1n+p:
254      match w:
255        case WCon{True{}, t}:
256          match c:
257            case True{}:
258              Equal.cong(Word(p), Word(1n+p), x => WCon{True{}, x}, Word.shl.put(p, True{}, t), Word.adc(p, t, t, False{}, True{}), shl_adc(p, t, True{}))
259            case False{}:
260              Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.shl.put(p, True{}, t), Word.adc(p, t, t, False{}, True{}), shl_adc(p, t, True{}))
261        case WCon{False{}, t}:
262          match c:
263            case True{}:
264              Equal.cong(Word(p), Word(1n+p), x => WCon{True{}, x}, Word.shl.put(p, False{}, t), Word.adc(p, t, t, False{}, False{}), shl_adc(p, t, False{}))
265            case False{}:
266              Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.shl.put(p, False{}, t), Word.adc(p, t, t, False{}, False{}), shl_adc(p, t, False{}))
267
268def w_shl(+n: Nat, +w: Word(n)) -> {Word.shl(n, w) == Word.add(n, w, w) : Word(n)}:
269  match n:
270    case 0n:
271      match w:
272        case WNil{}:
273          {==}
274    case 1n+p:
275      match w:
276        case WCon{b, t}:
277          shl_adc(1n+p, WCon{b, t}, False{})
278
279# ---- U32 ----
280
281def assoc(+a: U32, +b: U32, +c: U32) -> {U32.add(U32.add(a, b), c) == U32.add(a, U32.add(b, c)) : U32}:
282  match a b c:
283    case U32{x} U32{y} U32{z}:
284      Equal.cong(Word(32n), U32, w => U32{w}, Word.add(32n, Word.add(32n, x, y), z), Word.add(32n, x, Word.add(32n, y, z)), w_assoc(32n, x, y, z))
285
286def comm(+a: U32, +b: U32) -> {U32.add(a, b) == U32.add(b, a) : U32}:
287  U32.add_comm(a, b)
288
289def zero_add(+b: U32) -> {U32.add(0, b) == b : U32}:
290  match b:
291    case U32{y}:
292      Equal.cong(Word(32n), U32, w => U32{w}, Word.add(32n, Word.zero(32n), y), y, w_zero_add(32n, y))
293
294def add_zero(+b: U32) -> {U32.add(b, 0) == b : U32}:
295  Equal.trans(U32, U32.add(b, 0), U32.add(0, b), b, U32.add_comm(b, 0), zero_add(b))
296
297def add_sub(+a: U32, +b: U32) -> {U32.sub(U32.add(a, b), a) == b : U32}:
298  match a b:
299    case U32{x} U32{y}:
300      Equal.cong(Word(32n), U32, w => U32{w}, Word.sub(32n, Word.add(32n, x, y), x), y, w_add_sub(32n, x, y))
301
302def sub_add(+v: U32, +a: U32) -> {U32.add(U32.sub(v, a), a) == v : U32}:
303  match v a:
304    case U32{x} U32{y}:
305      Equal.cong(Word(32n), U32, w => U32{w}, Word.add(32n, Word.sub(32n, x, y), y), x, w_sub_add(32n, x, y))
306
307def shl_add(+x: U32) -> {U32.shl(x) == U32.add(x, x) : U32}:
308  match x:
309    case U32{w}:
310      Equal.cong(Word(32n), U32, v => U32{v}, Word.shl(32n, w), Word.add(32n, w, w), w_shl(32n, w))
311
312# a + (b + c) == b + (a + c)
313def swap(+a: U32, +b: U32, +c: U32) -> {U32.add(a, U32.add(b, c)) == U32.add(b, U32.add(a, c)) : U32}:
314  %assoc(a, b, c) : {_ == U32.add(b, U32.add(a, c)) : U32}
315  %assoc(b, a, c) : {U32.add(U32.add(a, b), c) == _ : U32}
316  %U32.add_comm(a, b) : {U32.add(U32.add(a, b), c) == U32.add(_, c) : U32}
317  {==}
318
319# ---- U32 equality as a Bool ----
320
321def eq_of(+a: U32, +b: U32, +h: {U32.is_eq(a, b) == True{} : Bool}) -> {a == b : U32}:
322  U.injective(a, b, N.eq_from_is_eq(U32.to_nat(a), U32.to_nat(b), L.subst(Cmp, c => {Cmp.is_eq(c) == True{} : Bool}, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U.u32_cmp(a, b), h)))
323
324def eq_refl(+a: U32) -> {U32.is_eq(a, a) == True{} : Bool}:
325  %Equal.sym(Cmp, U32.cmp(a, a), Nat.cmp(U32.to_nat(a), U32.to_nat(a)), U.u32_cmp(a, a)) : {Cmp.is_eq(_) == True{} : Bool}
326  N.is_eq_refl(U32.to_nat(a))
327
328def eq_true(+a: U32, +b: U32, +e: {a == b : U32}) -> {U32.is_eq(a, b) == True{} : Bool}:
329  %e : {U32.is_eq(a, _) == True{} : Bool}
330  eq_refl(a)