proofs/crypto/curve25519/limbs.bend

bend-collections-laws-crypto@1.0.0.0 · 293 lines · 37 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as UD
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as PD
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
14
15# Limb lists: their value (FS.value, radix 2^8), shapes and bounds, the U32
16# steps of the field code, and the carry pass (src/crypto/curve25519/field.bend
17# `carry`): value(limbs) + 2^(8 n) carry_out == value(xs) + carry_in, every
18# limb below 2^8, and every U32 sum below 2^32 (no wrap; the invariants of
19# Fiat-Crypto's carry chains, Erbsen et al. 2019, and of HACL*'s
20# Hacl.Spec.Curve25519.Field51 carry_wide).
21
22def v(+x: U32) -> Nat:
23  U32.to_nat(x)
24
25# 2^(8 len(xs)) x
26def sh(xs: List<&2, U32>, +x: Nat) -> Nat:
27  match xs:
28    case Nil{}:
29      x
30    case Con{h, t}:
31      C.shift(8n, sh(t, x))
32
33# 2^(8 n) x
34def shn(n: Nat, +x: Nat) -> Nat:
35  match n:
36    case 0n:
37      x
38    case 1n+m:
39      C.shift(8n, shn(m, x))
40
41# exactly n limbs, each at most b
42def okb(n: Nat, xs: List<&2, U32>, +b: Nat) -> Bool:
43  match n:
44    case 0n:
45      match xs:
46        case Nil{}:
47          True{}
48        case Con{x, xt}:
49          False{}
50    case 1n+m:
51      match xs:
52        case Nil{}:
53          False{}
54        case Con{x, xt}:
55          Bool.and(Nat.is_le(U32.to_nat(x), b), okb(m, xt, b))
56
57# every limb at most b
58def lea(xs: List<&2, U32>, +b: Nat) -> Bool:
59  match xs:
60    case Nil{}:
61      True{}
62    case Con{x, xt}:
63      Bool.and(Nat.is_le(U32.to_nat(x), b), lea(xt, b))
64
65def cl(r: F.Cr) -> List<&2, U32>:
66  F.cr_limbs(r)
67
68def cc(r: F.Cr) -> U32:
69  F.cr_out(r)
70
71# ---- shapes ----
72
73def okb_head(+n: Nat, +h: U32, +t: List<&2, U32>, +b: Nat, +e: {okb(1n+n, Con{h, t}, b) == True{} : Bool}) -> {Nat.is_le(v(h), b) == True{} : Bool}:
74  L.and_left(Nat.is_le(v(h), b), okb(n, t, b), e)
75
76def okb_tail(+n: Nat, +h: U32, +t: List<&2, U32>, +b: Nat, +e: {okb(1n+n, Con{h, t}, b) == True{} : Bool}) -> {okb(n, t, b) == True{} : Bool}:
77  L.and_right(Nat.is_le(v(h), b), okb(n, t, b), e)
78
79def okb_lea(+n: Nat, +xs: List<&2, U32>, +b: Nat, +e: {okb(n, xs, b) == True{} : Bool}) -> {lea(xs, b) == True{} : Bool}:
80  match n xs:
81    case 0n Nil{}:
82      {==}
83    case 0n Con{x, xt}:
84      Empty.absurd({lea(Con{x, xt}, b) == True{} : Bool}, L.false_true(e))
85    case 1n+m Nil{}:
86      Empty.absurd({lea(Nil{}, b) == True{} : Bool}, L.false_true(e))
87    case 1n+ +m Con{+x, +xt}:
88      L.and_intro(Nat.is_le(v(x), b), lea(xt, b), okb_head(m, x, xt, b, e), okb_lea(m, xt, b, okb_tail(m, x, xt, b, e)))
89
90def lea_head(+h: U32, +t: List<&2, U32>, +b: Nat, +e: {lea(Con{h, t}, b) == True{} : Bool}) -> {Nat.is_le(v(h), b) == True{} : Bool}:
91  L.and_left(Nat.is_le(v(h), b), lea(t, b), e)
92
93def lea_tail(+h: U32, +t: List<&2, U32>, +b: Nat, +e: {lea(Con{h, t}, b) == True{} : Bool}) -> {lea(t, b) == True{} : Bool}:
94  L.and_right(Nat.is_le(v(h), b), lea(t, b), e)
95
96# a weaker bound
97def lea_mono(+xs: List<&2, U32>, +b: Nat, +c: Nat, +hb: {Nat.is_le(b, c) == True{} : Bool}, +e: {lea(xs, b) == True{} : Bool}) -> {lea(xs, c) == True{} : Bool}:
98  match xs:
99    case Nil{}:
100      {==}
101    case Con{+x, +xt}:
102      L.and_intro(Nat.is_le(v(x), c), lea(xt, c), N.le_trans(v(x), b, c, lea_head(x, xt, b, e), hb), lea_mono(xt, b, c, hb, lea_tail(x, xt, b, e)))
103
104def sh_okb(+n: Nat, +xs: List<&2, U32>, +b: Nat, +x: Nat, +e: {okb(n, xs, b) == True{} : Bool}) -> {sh(xs, x) == shn(n, x) : Nat}:
105  match n xs:
106    case 0n Nil{}:
107      {==}
108    case 0n Con{y, yt}:
109      Empty.absurd({sh(Con{y, yt}, x) == x : Nat}, L.false_true(e))
110    case 1n+m Nil{}:
111      Empty.absurd({x == shn(1n+m, x) : Nat}, L.false_true(e))
112    case 1n+ +m Con{+y, +yt}:
113      Equal.cong(Nat, Nat, z => C.shift(8n, z), sh(yt, x), shn(m, x), sh_okb(m, yt, b, x, okb_tail(m, y, yt, b, e)))
114
115# the spec's tight (bytes_ok 32: limbs below 256) is okb 32 with bound 255
116def bytes_okb(+n: Nat, +xs: List<&2, U32>, +e: {FS.bytes_ok(n, xs) == True{} : Bool}) -> {okb(n, xs, 255n) == True{} : Bool}:
117  match n xs:
118    case 0n Nil{}:
119      {==}
120    case 0n Con{y, yt}:
121      Empty.absurd({okb(0n, Con{y, yt}, 255n) == True{} : Bool}, L.false_true(e))
122    case 1n+m Nil{}:
123      Empty.absurd({okb(1n+m, Nil{}, 255n) == True{} : Bool}, L.false_true(e))
124    case 1n+ +m Con{+y, +yt}:
125      +h = L.and_left(Nat.is_lt(v(y), 256n), FS.bytes_ok(m, yt), e)
126      +t = L.and_right(Nat.is_lt(v(y), 256n), FS.bytes_ok(m, yt), e)
127      L.and_intro(Nat.is_le(v(y), 255n), okb(m, yt, 255n), N.lt_succ_le(v(y), 255n, h), bytes_okb(m, yt, t))
128
129def okb_bytes(+n: Nat, +xs: List<&2, U32>, +e: {okb(n, xs, 255n) == True{} : Bool}) -> {FS.bytes_ok(n, xs) == True{} : Bool}:
130  match n xs:
131    case 0n Nil{}:
132      {==}
133    case 0n Con{y, yt}:
134      Empty.absurd({FS.bytes_ok(0n, Con{y, yt}) == True{} : Bool}, L.false_true(e))
135    case 1n+m Nil{}:
136      Empty.absurd({FS.bytes_ok(1n+m, Nil{}) == True{} : Bool}, L.false_true(e))
137    case 1n+ +m Con{+y, +yt}:
138      L.and_intro(Nat.is_lt(v(y), 256n), FS.bytes_ok(m, yt), N.le_lt_succ(v(y), 255n, okb_head(m, y, yt, 255n, e)), okb_bytes(m, yt, okb_tail(m, y, yt, 255n, e)))
139
140# ---- constants ----
141
142def k256(+one: Nat, +h1: {one == 1n : Nat}) -> {256n == WD.sc(8n, one) : Nat}:
143  L.subst(Nat, o => {256n == WD.sc(8n, o) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
144
145def sc_pos1(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(0n, WD.sc(k, one)) == True{} : Bool}:
146  L.subst(Nat, o => {Nat.is_lt(0n, WD.sc(k, o)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), WD.sc_pos(k))
147
148# 2^k < 2^(k+1)
149def sc_lt_succ(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(WD.sc(k, one), WD.sc(1n+k, one)) == True{} : Bool}:
150  +x = WD.sc(k, one)
151  +a = N.lt_add_left(0n, x, x, sc_pos1(k, one, h1))
152  %N.add_zero(x) : {Nat.is_lt(_, WD.sc(1n+k, one)) == True{} : Bool}
153  %M.sc_dbl(k, one) : {Nat.is_lt(Nat.add(x, 0n), _) == True{} : Bool}
154  a
155
156# 2^a < 2^(d + 1 + a)
157def sc_lt(+d: Nat, +a: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(WD.sc(a, one), WD.sc(Nat.add(d, 1n+a), one)) == True{} : Bool}:
158  N.lt_le_trans(WD.sc(a, one), WD.sc(1n+a, one), WD.sc(Nat.add(d, 1n+a), one), sc_lt_succ(a, one, h1), M.sc_mono(d, 1n+a, one))
159
160# ---- U32 steps ----
161
162def add_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +h: {Nat.is_lt(Nat.add(v(x), v(y)), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}:
163  PD.add32(one, h1, x, y, h)
164
165def mul_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +h: {Nat.is_lt(Nat.mul(v(x), v(y)), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.mul(x, y)) == Nat.mul(v(x), v(y)) : Nat}:
166  PD.mul32(one, h1, x, y, h)
167
168def mod256(+x: U32) -> {v(U32.mod(x, 256)) == Nat.mod(v(x), 256n) : Nat}:
169  UD.mod_nat(x, 256, {==})
170
171def div256(+x: U32) -> {v(U32.div(x, 256)) == Nat.div(v(x), 256n) : Nat}:
172  UD.div_nat(x, 256, {==})
173
174def m256(+x: Nat) -> {Nat.mul(x, 256n) == C.shift(8n, x) : Nat}:
175  PD.mul_pow(1n, {==}, 8n, x, 256n, {==})
176
177# n == (n mod 256) + 2^8 (n div 256)
178def dm256(+n: Nat) -> {Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))) == n : Nat}:
179  +e = Equal.sym(Nat, n, Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), NR.dm_eq(255n, n))
180  +e2 = Equal.trans(Nat, Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))), Nat.add(Nat.mod(n, 256n), Nat.mul(Nat.div(n, 256n), 256n)), Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), M.cong_r(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n)), Nat.mul(Nat.div(n, 256n), 256n), Equal.sym(Nat, Nat.mul(Nat.div(n, 256n), 256n), C.shift(8n, Nat.div(n, 256n)), m256(Nat.div(n, 256n)))), NA.add_comm(Nat.mod(n, 256n), Nat.mul(Nat.div(n, 256n), 256n)))
181  Equal.trans(Nat, Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))), Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), n, e2, e)
182
183# a U32 split into its low byte and the rest
184def split_v(+s: U32) -> {Nat.add(v(U32.mod(s, 256)), C.shift(8n, v(U32.div(s, 256)))) == v(s) : Nat}:
185  %Equal.sym(Nat, v(U32.mod(s, 256)), Nat.mod(v(s), 256n), mod256(s)) : {Nat.add(_, C.shift(8n, v(U32.div(s, 256)))) == v(s) : Nat}
186  %Equal.sym(Nat, v(U32.div(s, 256)), Nat.div(v(s), 256n), div256(s)) : {Nat.add(Nat.mod(v(s), 256n), C.shift(8n, _)) == v(s) : Nat}
187  dm256(v(s))
188
189def lo_le(+s: U32) -> {Nat.is_le(v(U32.mod(s, 256)), 255n) == True{} : Bool}:
190  %Equal.sym(Nat, v(U32.mod(s, 256)), Nat.mod(v(s), 256n), mod256(s)) : {Nat.is_le(_, 255n) == True{} : Bool}
191  N.lt_succ_le(Nat.mod(v(s), 256n), 255n, NR.dm_lt(255n, v(s)))
192
193# (s div 256) < 2^k when s < 2^(k + 8)
194def hi_lt(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +s: U32, +h: {Nat.is_lt(v(s), WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}) -> {Nat.is_lt(v(U32.div(s, 256)), WD.sc(k, one)) == True{} : Bool}:
195  %Equal.sym(Nat, v(U32.div(s, 256)), Nat.div(v(s), 256n), div256(s)) : {Nat.is_lt(_, WD.sc(k, one)) == True{} : Bool}
196  +n = v(s)
197  +q = Nat.div(n, 256n)
198  +r = Nat.mod(n, 256n)
199  +e = NR.dm_eq(255n, n)
200  +h2 = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}, n, Nat.add(Nat.mul(q, 256n), r), e, h)
201  +h3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(q, 256n), r), z) == True{} : Bool}, WD.sc(Nat.add(k, 8n), one), WD.sc(k, WD.sc(8n, one)), AR.sc_idx(k, 8n, one), h2)
202  +h4 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(q, 256n), r), WD.sc(k, z)) == True{} : Bool}, WD.sc(8n, one), 256n, Equal.sym(Nat, 256n, WD.sc(8n, one), k256(one, h1)), h3)
203  AR.quot_lt(k, one, h1, q, 256n, r, h4)
204
205# ---- the carry pass ----
206
207def cl_con(+l: U32, +r: F.Cr) -> {cl(F.carry_con(l, r)) == Con{l, cl(r)} : List<&2, U32>}:
208  match r:
209    case F.Cr{a, c}:
210      {==}
211
212def cc_con(+l: U32, +r: F.Cr) -> {cc(F.carry_con(l, r)) == cc(r) : U32}:
213  match r:
214    case F.Cr{a, c}:
215      {==}
216
217# carry-in at most 2^21 and a limb at most 2^28: their sum is below 2^29
218def s_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +hx: {Nat.is_le(v(x), WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(v(x), v(c)), WD.sc(29n, one)) == True{} : Bool}:
219  +c28 = N.lt_le(v(c), WD.sc(28n, one), N.le_lt_trans(v(c), WD.sc(21n, one), WD.sc(28n, one), hc, sc_lt(6n, 21n, one, h1)))
220  +lt = N.le_lt_trans(Nat.add(v(x), v(c)), Nat.add(WD.sc(28n, one), WD.sc(21n, one)), Nat.add(WD.sc(28n, one), WD.sc(28n, one)), M.le_add2(v(x), v(c), WD.sc(28n, one), WD.sc(21n, one), hx, hc), N.lt_add_left(WD.sc(21n, one), WD.sc(28n, one), WD.sc(28n, one), sc_lt(6n, 21n, one, h1)))
221  %M.sc_dbl(28n, one) : {Nat.is_lt(Nat.add(v(x), v(c)), _) == True{} : Bool}
222  lt
223
224def s_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +hx: {Nat.is_le(v(x), WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {v(U32.add(x, c)) == Nat.add(v(x), v(c)) : Nat}:
225  add_v(one, h1, x, c, N.lt_trans(Nat.add(v(x), v(c)), WD.sc(29n, one), WD.sc(32n, one), s_lt(one, h1, x, c, hx, hc), sc_lt(2n, 29n, one, h1)))
226
227def c_next(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +hx: {Nat.is_le(v(x), WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.is_le(v(U32.div(U32.add(x, c), 256)), WD.sc(21n, one)) == True{} : Bool}:
228  +s = U32.add(x, c)
229  +hs = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(29n, one)) == True{} : Bool}, Nat.add(v(x), v(c)), v(s), Equal.sym(Nat, v(s), Nat.add(v(x), v(c)), s_v(one, h1, x, c, hx, hc)), s_lt(one, h1, x, c, hx, hc))
230  N.lt_le(v(U32.div(s, 256)), WD.sc(21n, one), hi_lt(21n, one, h1, s, hs))
231
232# value(limbs) + 2^(8 n) carry_out == value(xs) + carry_in
233def carry_val(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +c: U32, +hx: {lea(xs, WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.add(FS.value(cl(F.carry(xs, c))), sh(xs, v(cc(F.carry(xs, c))))) == Nat.add(FS.value(xs), v(c)) : Nat}:
234  match xs:
235    case Nil{}:
236      {==}
237    case Con{+h, +t}:
238      +hh = lea_head(h, t, WD.sc(28n, one), hx)
239      +ht = lea_tail(h, t, WD.sc(28n, one), hx)
240      +s = U32.add(h, c)
241      +lo = U32.mod(s, 256)
242      +hi = U32.div(s, 256)
243      +r = F.carry(t, hi)
244      +ih = carry_val(one, h1, t, hi, ht, c_next(one, h1, h, c, hh, hc))
245      %Equal.sym(List<&2, U32>, cl(F.carry_con(lo, r)), Con{lo, cl(r)}, cl_con(lo, r)) : {Nat.add(FS.value(_), C.shift(8n, sh(t, v(cc(F.carry_con(lo, r)))))) == Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)) : Nat}
246      %Equal.sym(U32, cc(F.carry_con(lo, r)), cc(r), cc_con(lo, r)) : {Nat.add(FS.value(Con{lo, cl(r)}), C.shift(8n, sh(t, v(_)))) == Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)) : Nat}
247      +A = FS.value(cl(r))
248      +B = sh(t, v(cc(r)))
249      +e1 = Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, A)), C.shift(8n, B)), Nat.add(v(lo), Nat.add(C.shift(8n, A), C.shift(8n, B))), Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), NA.add_assoc(v(lo), C.shift(8n, A), C.shift(8n, B)), M.cong_r(v(lo), Nat.add(C.shift(8n, A), C.shift(8n, B)), C.shift(8n, Nat.add(A, B)), M.sc_add(8n, A, B)))
250      +e2 = M.cong_r(v(lo), C.shift(8n, Nat.add(A, B)), C.shift(8n, Nat.add(FS.value(t), v(hi))), M.cong_sc(8n, Nat.add(A, B), Nat.add(FS.value(t), v(hi)), ih))
251      +e3 = Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), M.cong_r(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi))), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), Equal.sym(Nat, Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), C.shift(8n, Nat.add(FS.value(t), v(hi))), M.sc_add(8n, FS.value(t), v(hi)))),
252        Equal.trans(Nat, Nat.add(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Nat.add(v(lo), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), M.cong_r(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t))), NA.add_comm(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Equal.sym(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(v(lo), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t)))), NA.add_assoc(v(lo), C.shift(8n, v(hi)), C.shift(8n, FS.value(t))))))
253      +e4 = M.cong_l(Nat.add(v(lo), C.shift(8n, v(hi))), v(s), C.shift(8n, FS.value(t)), split_v(s))
254      +e5 = M.cong_l(v(s), Nat.add(v(h), v(c)), C.shift(8n, FS.value(t)), s_v(one, h1, h, c, hh, hc))
255      +e6 = Equal.trans(Nat, Nat.add(Nat.add(v(h), v(c)), C.shift(8n, FS.value(t))), Nat.add(v(h), Nat.add(v(c), C.shift(8n, FS.value(t)))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), NA.add_assoc(v(h), v(c), C.shift(8n, FS.value(t))),
256        Equal.trans(Nat, Nat.add(v(h), Nat.add(v(c), C.shift(8n, FS.value(t)))), Nat.add(v(h), Nat.add(C.shift(8n, FS.value(t)), v(c))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), M.cong_r(v(h), Nat.add(v(c), C.shift(8n, FS.value(t))), Nat.add(C.shift(8n, FS.value(t)), v(c)), NA.add_comm(v(c), C.shift(8n, FS.value(t)))), Equal.sym(Nat, Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), Nat.add(v(h), Nat.add(C.shift(8n, FS.value(t)), v(c))), NA.add_assoc(v(h), C.shift(8n, FS.value(t)), v(c)))))
257      Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, A)), C.shift(8n, B)), Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e1,
258        Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e2,
259          Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e3,
260            Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(v(s), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e4,
261              Equal.trans(Nat, Nat.add(v(s), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), v(c)), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e5, e6)))))
262
263# every output limb below 2^8, the same count
264def carry_ok(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +c: U32, +hn: {okb(n, xs, WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {okb(n, cl(F.carry(xs, c)), 255n) == True{} : Bool}:
265  match n xs:
266    case 0n Nil{}:
267      {==}
268    case 0n Con{y, yt}:
269      Empty.absurd({okb(0n, cl(F.carry(Con{y, yt}, c)), 255n) == True{} : Bool}, L.false_true(hn))
270    case 1n+m Nil{}:
271      Empty.absurd({okb(1n+m, cl(F.carry(Nil{}, c)), 255n) == True{} : Bool}, L.false_true(hn))
272    case 1n+ +m Con{+h, +t}:
273      +hh = okb_head(m, h, t, WD.sc(28n, one), hn)
274      +ht = okb_tail(m, h, t, WD.sc(28n, one), hn)
275      +s = U32.add(h, c)
276      +lo = U32.mod(s, 256)
277      +r = F.carry(t, U32.div(s, 256))
278      %Equal.sym(List<&2, U32>, cl(F.carry_con(lo, r)), Con{lo, cl(r)}, cl_con(lo, r)) : {okb(1n+m, _, 255n) == True{} : Bool}
279      L.and_intro(Nat.is_le(v(lo), 255n), okb(m, cl(r), 255n), lo_le(s), carry_ok(one, h1, m, t, U32.div(s, 256), ht, c_next(one, h1, h, c, hh, hc)))
280
281# the carry out is at most 2^21
282def carry_cb(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +c: U32, +hx: {lea(xs, WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.is_le(v(cc(F.carry(xs, c))), WD.sc(21n, one)) == True{} : Bool}:
283  match xs:
284    case Nil{}:
285      hc
286    case Con{+h, +t}:
287      +hh = lea_head(h, t, WD.sc(28n, one), hx)
288      +ht = lea_tail(h, t, WD.sc(28n, one), hx)
289      +s = U32.add(h, c)
290      +lo = U32.mod(s, 256)
291      +r = F.carry(t, U32.div(s, 256))
292      %Equal.sym(U32, cc(F.carry_con(lo, r)), cc(r), cc_con(lo, r)) : {Nat.is_le(v(_), WD.sc(21n, one)) == True{} : Bool}
293      carry_cb(one, h1, t, U32.div(s, 256), ht, c_next(one, h1, h, c, hh, hc))