proofs/crypto/poly1305/value.bend

bend-collections-laws-crypto@1.0.0.0 · 739 lines · 57 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/src/crypto/poly1305/limbs.bend as Li
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
7import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
8import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as SH
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn.bend as SHN
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend as FB
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A
14
15# The value of a limb list (radix 2^8, least significant limb first) and the
16# limb operations of src/crypto/poly1305/limbs.bend against it: sums and
17# products are exact (Fiat-Crypto / HACL* Field32xN style: the limb value is
18# the number, as long as no U32 operation wraps), under limb bounds
19# le_all(xs, B) (every limb <= B) whose sums and products fit 32 bits.
20
21def v(+x: U32) -> Nat:
22  U32.to_nat(x)
23
24def ev(xs: List<&2, U32>) -> Nat:
25  match xs:
26    case Nil{}: 0n
27    case x <> t: Nat.add(v(x), C.shift(8n, ev(t)))
28
29def le_all(xs: List<&2, U32>, +b: Nat) -> Bool:
30  match xs:
31    case Nil{}: True{}
32    case x <> t: Bool.and(Nat.is_le(v(x), b), le_all(t, b))
33
34def hd_le(+x: U32, +t: List<&2, U32>, +b: Nat, +h: {le_all(x <> t, b) == True{} : Bool}) -> {Nat.is_le(v(x), b) == True{} : Bool}:
35  L.and_left(Nat.is_le(v(x), b), le_all(t, b), h)
36
37def tl_le(+x: U32, +t: List<&2, U32>, +b: Nat, +h: {le_all(x <> t, b) == True{} : Bool}) -> {le_all(t, b) == True{} : Bool}:
38  L.and_right(Nat.is_le(v(x), b), le_all(t, b), h)
39
40def cons_le(+x: U32, +t: List<&2, U32>, +b: Nat, +hx: {Nat.is_le(v(x), b) == True{} : Bool}, +ht: {le_all(t, b) == True{} : Bool}) -> {le_all(x <> t, b) == True{} : Bool}:
41  L.and_intro(Nat.is_le(v(x), b), le_all(t, b), hx, ht)
42
43law le_mono:
44  for +xs: List<&2, U32>
45  for +b: Nat
46  for +c: Nat
47  for +hb: {Nat.is_le(b, c) == True{} : Bool}
48  for +h: {le_all(xs, b) == True{} : Bool}
49  {le_all(xs, c) == True{} : Bool}
50
51def le_mono(xs, b, c, hb, h):
52  match xs:
53    case Nil{}: {==}
54    case x <> t:
55      cons_le(x, t, c, N.le_trans(v(x), b, c, hd_le(x, t, b, h), hb), le_mono(t, b, c, hb, tl_le(x, t, b, h)))
56
57# ---- sums ----
58
59# the exact U32 sum of two limbs whose bounds add up within 32 bits
60def add1(+x: U32, +y: U32, +b1: Nat, +b2: Nat, +hx: {Nat.is_le(v(x), b1) == True{} : Bool}, +hy: {Nat.is_le(v(y), b2) == True{} : Bool}, +hf: {C.fits(32n, Nat.add(b1, b2)) == True{} : Bool}) -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}:
61  WA.add_exact(1n, {==}, x, y, A.fits_le(32n, Nat.add(v(x), v(y)), Nat.add(b1, b2), A.le_add2(v(x), v(y), b1, b2, hx, hy), hf))
62
63law add_ev:
64  for +a: List<&2, U32>
65  for +b: List<&2, U32>
66  for +b1: Nat
67  for +b2: Nat
68  for +ha: {le_all(a, b1) == True{} : Bool}
69  for +hb: {le_all(b, b2) == True{} : Bool}
70  for +hf: {C.fits(32n, Nat.add(b1, b2)) == True{} : Bool}
71  {ev(Li.add(a, b)) == Nat.add(ev(a), ev(b)) : Nat}
72
73def add_ev(a, b, b1, b2, ha, hb, hf):
74  match a b:
75    case Nil{} _: {==}
76    case x <> at Nil{}: A.sy(Nat.add(ev(x <> at), 0n), ev(x <> at), N.add_zero(ev(x <> at)))
77    case x <> at y <> bt:
78      +e1 = add1(x, y, b1, b2, hd_le(x, at, b1, ha), hd_le(y, bt, b2, hb), hf)
79      +e2 = add_ev(at, bt, b1, b2, tl_le(x, at, b1, ha), tl_le(y, bt, b2, hb), hf)
80      +s1 = C.shift(8n, ev(at))
81      +s2 = C.shift(8n, ev(bt))
82      A.tr(Nat.add(v(U32.add(x, y)), C.shift(8n, ev(Li.add(at, bt)))), Nat.add(Nat.add(v(x), v(y)), Nat.add(s1, s2)), Nat.add(Nat.add(v(x), s1), Nat.add(v(y), s2)),
83        A.cadd(v(U32.add(x, y)), Nat.add(v(x), v(y)), C.shift(8n, ev(Li.add(at, bt))), Nat.add(s1, s2), e1,
84          A.tr(C.shift(8n, ev(Li.add(at, bt))), C.shift(8n, Nat.add(ev(at), ev(bt))), Nat.add(s1, s2), A.csh(8n, ev(Li.add(at, bt)), Nat.add(ev(at), ev(bt)), e2), WW.shift_add(8n, ev(at), ev(bt)))),
85        WM.add4(v(x), v(y), s1, s2))
86
87law add_le:
88  for +a: List<&2, U32>
89  for +b: List<&2, U32>
90  for +b1: Nat
91  for +b2: Nat
92  for +ha: {le_all(a, b1) == True{} : Bool}
93  for +hb: {le_all(b, b2) == True{} : Bool}
94  for +hf: {C.fits(32n, Nat.add(b1, b2)) == True{} : Bool}
95  {le_all(Li.add(a, b), Nat.add(b1, b2)) == True{} : Bool}
96
97def add_le(a, b, b1, b2, ha, hb, hf):
98  match a b:
99    case Nil{} _: le_mono(b, b2, Nat.add(b1, b2), A.le_add_l(b1, b2), hb)
100    case x <> at Nil{}: le_mono(x <> at, b1, Nat.add(b1, b2), N.le_add_right(b1, b2), ha)
101    case x <> at y <> bt:
102      +hx = hd_le(x, at, b1, ha)
103      +hy = hd_le(y, bt, b2, hb)
104      cons_le(U32.add(x, y), Li.add(at, bt), Nat.add(b1, b2),
105        L.subst(Nat, z => {Nat.is_le(z, Nat.add(b1, b2)) == True{} : Bool}, Nat.add(v(x), v(y)), v(U32.add(x, y)), A.sy(v(U32.add(x, y)), Nat.add(v(x), v(y)), add1(x, y, b1, b2, hx, hy, hf)), A.le_add2(v(x), v(y), b1, b2, hx, hy)),
106        add_le(at, bt, b1, b2, tl_le(x, at, b1, ha), tl_le(y, bt, b2, hb), hf))
107
108# ---- products by a limb ----
109
110def mul1(+x: U32, +c: U32, +b: Nat, +bc: Nat, +hx: {Nat.is_le(v(x), b) == True{} : Bool}, +hc: {Nat.is_le(v(c), bc) == True{} : Bool}, +hf: {C.fits(32n, Nat.mul(b, bc)) == True{} : Bool}) -> {v(U32.mul(x, c)) == Nat.mul(v(x), v(c)) : Nat}:
111  A.tr(v(U32.mul(x, c)), C.low(32n, Nat.mul(v(x), v(c))), Nat.mul(v(x), v(c)), SH.mul_low(x, c),
112    WW.low_fit(32n, Nat.mul(v(x), v(c)), A.fits_le(32n, Nat.mul(v(x), v(c)), Nat.mul(b, bc), A.le_mul2(v(x), v(c), b, bc, hx, hc), hf)))
113
114law scale_ev:
115  for +c: U32
116  for +a: List<&2, U32>
117  for +b: Nat
118  for +bc: Nat
119  for +ha: {le_all(a, b) == True{} : Bool}
120  for +hc: {Nat.is_le(v(c), bc) == True{} : Bool}
121  for +hf: {C.fits(32n, Nat.mul(b, bc)) == True{} : Bool}
122  {ev(Li.scale(c, a)) == Nat.mul(ev(a), v(c)) : Nat}
123
124def scale_ev(c, a, b, bc, ha, hc, hf):
125  match a:
126    case Nil{}: {==}
127    case x <> t:
128      +e1 = mul1(x, c, b, bc, hd_le(x, t, b, ha), hc, hf)
129      +e2 = scale_ev(c, t, b, bc, tl_le(x, t, b, ha), hc, hf)
130      A.tr(Nat.add(v(U32.mul(x, c)), C.shift(8n, ev(Li.scale(c, t)))), Nat.add(Nat.mul(v(x), v(c)), C.shift(8n, Nat.mul(ev(t), v(c)))), Nat.mul(Nat.add(v(x), C.shift(8n, ev(t))), v(c)),
131        A.cadd(v(U32.mul(x, c)), Nat.mul(v(x), v(c)), C.shift(8n, ev(Li.scale(c, t))), C.shift(8n, Nat.mul(ev(t), v(c))), e1, A.csh(8n, ev(Li.scale(c, t)), Nat.mul(ev(t), v(c)), e2)),
132        A.sy(Nat.mul(Nat.add(v(x), C.shift(8n, ev(t))), v(c)), Nat.add(Nat.mul(v(x), v(c)), C.shift(8n, Nat.mul(ev(t), v(c)))),
133          A.tr(Nat.mul(Nat.add(v(x), C.shift(8n, ev(t))), v(c)), Nat.add(Nat.mul(v(x), v(c)), Nat.mul(C.shift(8n, ev(t)), v(c))), Nat.add(Nat.mul(v(x), v(c)), C.shift(8n, Nat.mul(ev(t), v(c)))),
134            NA.mul_add_right(v(x), C.shift(8n, ev(t)), v(c)),
135            WM.cong_r(Nat.mul(v(x), v(c)), Nat.mul(C.shift(8n, ev(t)), v(c)), C.shift(8n, Nat.mul(ev(t), v(c))), WW.shift_mul_l(8n, ev(t), v(c))))))
136
137law scale_le:
138  for +c: U32
139  for +a: List<&2, U32>
140  for +b: Nat
141  for +bc: Nat
142  for +ha: {le_all(a, b) == True{} : Bool}
143  for +hc: {Nat.is_le(v(c), bc) == True{} : Bool}
144  for +hf: {C.fits(32n, Nat.mul(b, bc)) == True{} : Bool}
145  {le_all(Li.scale(c, a), Nat.mul(b, bc)) == True{} : Bool}
146
147def scale_le(c, a, b, bc, ha, hc, hf):
148  match a:
149    case Nil{}: {==}
150    case x <> t:
151      +hx = hd_le(x, t, b, ha)
152      cons_le(U32.mul(x, c), Li.scale(c, t), Nat.mul(b, bc),
153        L.subst(Nat, z => {Nat.is_le(z, Nat.mul(b, bc)) == True{} : Bool}, Nat.mul(v(x), v(c)), v(U32.mul(x, c)), A.sy(v(U32.mul(x, c)), Nat.mul(v(x), v(c)), mul1(x, c, b, bc, hx, hc, hf)), A.le_mul2(v(x), v(c), b, bc, hx, hc)),
154        scale_le(c, t, b, bc, tl_le(x, t, b, ha), hc, hf))
155
156# ---- schoolbook products ----
157
158law mul_le:
159  for +x: List<&2, U32>
160  for +r: List<&2, U32>
161  for +bx: Nat
162  for +br: Nat
163  for +hx: {le_all(x, bx) == True{} : Bool}
164  for +hr: {le_all(r, br) == True{} : Bool}
165  for +hf: {C.fits(32n, Nat.mul(List.length(&2, U32, r), Nat.mul(bx, br))) == True{} : Bool}
166  {le_all(Li.mul(x, r), Nat.mul(List.length(&2, U32, r), Nat.mul(bx, br))) == True{} : Bool}
167
168def mul_le(x, r, bx, br, hx, hr, hf):
169  match r:
170    case Nil{}: {==}
171    case r0 <> rs:
172      +m = Nat.mul(bx, br)
173      +k = Nat.mul(List.length(&2, U32, rs), m)
174      +hm = A.fits_add_l(32n, m, k, hf)
175      +hk = A.fits_add_r(32n, m, k, hf)
176      add_le(Li.scale(r0, x), 0 <> Li.mul(x, rs), m, k,
177        scale_le(r0, x, bx, br, hx, hd_le(r0, rs, br, hr), hm),
178        cons_le(0, Li.mul(x, rs), k, N.zero_le(k), mul_le(x, rs, bx, br, hx, tl_le(r0, rs, br, hr), hk)),
179        hf)
180
181law mul_ev:
182  for +x: List<&2, U32>
183  for +r: List<&2, U32>
184  for +bx: Nat
185  for +br: Nat
186  for +hx: {le_all(x, bx) == True{} : Bool}
187  for +hr: {le_all(r, br) == True{} : Bool}
188  for +hf: {C.fits(32n, Nat.mul(List.length(&2, U32, r), Nat.mul(bx, br))) == True{} : Bool}
189  {ev(Li.mul(x, r)) == Nat.mul(ev(x), ev(r)) : Nat}
190
191def mul_ev(x, r, bx, br, hx, hr, hf):
192  match r:
193    case Nil{}: A.sy(Nat.mul(ev(x), 0n), 0n, NA.mul_zero(ev(x)))
194    case r0 <> rs:
195      +m = Nat.mul(bx, br)
196      +k = Nat.mul(List.length(&2, U32, rs), m)
197      +hm = A.fits_add_l(32n, m, k, hf)
198      +hk = A.fits_add_r(32n, m, k, hf)
199      +hr0 = hd_le(r0, rs, br, hr)
200      +hrs = tl_le(r0, rs, br, hr)
201      +e1 = add_ev(Li.scale(r0, x), 0 <> Li.mul(x, rs), m, k,
202        scale_le(r0, x, bx, br, hx, hr0, hm),
203        cons_le(0, Li.mul(x, rs), k, N.zero_le(k), mul_le(x, rs, bx, br, hx, hrs, hk)),
204        hf)
205      +e2 = scale_ev(r0, x, bx, br, hx, hr0, hm)
206      +e3 = mul_ev(x, rs, bx, br, hx, hrs, hk)
207      +ex = ev(x)
208      A.tr(ev(Li.add(Li.scale(r0, x), 0 <> Li.mul(x, rs))), Nat.add(ev(Li.scale(r0, x)), C.shift(8n, ev(Li.mul(x, rs)))), Nat.mul(ex, Nat.add(v(r0), C.shift(8n, ev(rs)))), e1,
209        A.tr(Nat.add(ev(Li.scale(r0, x)), C.shift(8n, ev(Li.mul(x, rs)))), Nat.add(Nat.mul(ex, v(r0)), C.shift(8n, Nat.mul(ex, ev(rs)))), Nat.mul(ex, Nat.add(v(r0), C.shift(8n, ev(rs)))),
210          A.cadd(ev(Li.scale(r0, x)), Nat.mul(ex, v(r0)), C.shift(8n, ev(Li.mul(x, rs))), C.shift(8n, Nat.mul(ex, ev(rs))), e2, A.csh(8n, ev(Li.mul(x, rs)), Nat.mul(ex, ev(rs)), e3)),
211          A.sy(Nat.mul(ex, Nat.add(v(r0), C.shift(8n, ev(rs)))), Nat.add(Nat.mul(ex, v(r0)), C.shift(8n, Nat.mul(ex, ev(rs)))),
212            A.tr(Nat.mul(ex, Nat.add(v(r0), C.shift(8n, ev(rs)))), Nat.add(Nat.mul(ex, v(r0)), Nat.mul(ex, C.shift(8n, ev(rs)))), Nat.add(Nat.mul(ex, v(r0)), C.shift(8n, Nat.mul(ex, ev(rs)))),
213              NA.mul_add_left(ex, v(r0), C.shift(8n, ev(rs))),
214              WM.cong_r(Nat.mul(ex, v(r0)), Nat.mul(ex, C.shift(8n, ev(rs))), C.shift(8n, Nat.mul(ex, ev(rs))), WW.shift_mul_r(8n, ex, ev(rs)))))))
215
216# ---- positions ----
217
218# y at limb position n: y * 2^(8n)
219def pos(n: Nat, +y: Nat) -> Nat:
220  match n:
221    case 0n: y
222    case 1n+k: C.shift(8n, pos(k, y))
223
224law pos_zero:
225  for +n: Nat
226  {pos(n, 0n) == 0n : Nat}
227
228def pos_zero(n):
229  match n:
230    case 0n: {==}
231    case 1n+k: A.tr(C.shift(8n, pos(k, 0n)), C.shift(8n, 0n), 0n, A.csh(8n, pos(k, 0n), 0n, pos_zero(k)), {==})
232
233law pos_add:
234  for +n: Nat
235  for +x: Nat
236  for +y: Nat
237  {pos(n, Nat.add(x, y)) == Nat.add(pos(n, x), pos(n, y)) : Nat}
238
239def pos_add(n, x, y):
240  match n:
241    case 0n: {==}
242    case 1n+k: A.tr(C.shift(8n, pos(k, Nat.add(x, y))), C.shift(8n, Nat.add(pos(k, x), pos(k, y))), Nat.add(C.shift(8n, pos(k, x)), C.shift(8n, pos(k, y))), A.csh(8n, pos(k, Nat.add(x, y)), Nat.add(pos(k, x), pos(k, y)), pos_add(k, x, y)), WW.shift_add(8n, pos(k, x), pos(k, y)))
243
244law skip_nil:
245  for +n: Nat
246  {Li.skip(n, []) == [] : List<&2, U32>}
247
248def skip_nil(n):
249  match n:
250    case 0n: {==}
251    case 1n+k: {==}
252
253# ev(xs) = ev(take n xs) + 2^(8n) ev(skip n xs)
254law ts_ev:
255  for +n: Nat
256  for +xs: List<&2, U32>
257  {ev(xs) == Nat.add(ev(Li.take(n, xs)), pos(n, ev(Li.skip(n, xs)))) : Nat}
258
259def ts_ev(n, xs):
260  match n xs:
261    case 0n _: {==}
262    case 1n+k Nil{}: A.sy(C.shift(8n, pos(k, 0n)), 0n, A.tr(C.shift(8n, pos(k, 0n)), C.shift(8n, 0n), 0n, A.csh(8n, pos(k, 0n), 0n, pos_zero(k)), {==}))
263    case 1n+k x <> t:
264      +a = ev(Li.take(k, t))
265      +b = pos(k, ev(Li.skip(k, t)))
266      A.tr(Nat.add(v(x), C.shift(8n, ev(t))), Nat.add(v(x), Nat.add(C.shift(8n, a), C.shift(8n, b))), Nat.add(Nat.add(v(x), C.shift(8n, a)), C.shift(8n, b)),
267        WM.cong_r(v(x), C.shift(8n, ev(t)), Nat.add(C.shift(8n, a), C.shift(8n, b)), A.tr(C.shift(8n, ev(t)), C.shift(8n, Nat.add(a, b)), Nat.add(C.shift(8n, a), C.shift(8n, b)), A.csh(8n, ev(t), Nat.add(a, b), ts_ev(k, t)), WW.shift_add(8n, a, b))),
268        A.sy(Nat.add(Nat.add(v(x), C.shift(8n, a)), C.shift(8n, b)), Nat.add(v(x), Nat.add(C.shift(8n, a), C.shift(8n, b))), N.add_assoc(v(x), C.shift(8n, a), C.shift(8n, b))))
269
270law take_nil_ev:
271  for +n: Nat
272  {ev(Li.take(n, [])) == 0n : Nat}
273
274def take_nil_ev(n):
275  match n:
276    case 0n: {==}
277    case 1n+k: {==}
278
279law fit_ev:
280  for +n: Nat
281  for +xs: List<&2, U32>
282  {ev(Li.fit(n, xs)) == ev(Li.take(n, xs)) : Nat}
283
284def fit_ev(n, xs):
285  match n xs:
286    case 0n _: {==}
287    case 1n+k Nil{}: A.tr(C.shift(8n, ev(Li.fit(k, []))), C.shift(8n, 0n), 0n, A.csh(8n, ev(Li.fit(k, [])), 0n, A.tr(ev(Li.fit(k, [])), ev(Li.take(k, [])), 0n, fit_ev(k, []), take_nil_ev(k))), {==})
288    case 1n+k x <> t: WM.cong_r(v(x), C.shift(8n, ev(Li.fit(k, t))), C.shift(8n, ev(Li.take(k, t))), A.csh(8n, ev(Li.fit(k, t)), ev(Li.take(k, t)), fit_ev(k, t)))
289
290# ---- carry passes ----
291
292def fit_all(xs: List<&2, U32>, +k: Nat) -> Bool:
293  match xs:
294    case Nil{}: True{}
295    case x <> t: Bool.and(C.fits(k, v(x)), fit_all(t, k))
296
297law fits_zero:
298  for +k: Nat
299  {C.fits(k, 0n) == True{} : Bool}
300
301def fits_zero(k):
302  match k:
303    case 0n: {==}
304    case 1n+p: fits_zero(p)
305
306def hd0_fit(+ds: List<&2, U32>, +k: Nat, +h: {fit_all(ds, k) == True{} : Bool}) -> {C.fits(k, v(Li.hd0(ds))) == True{} : Bool}:
307  match ds:
308    case Nil{}: fits_zero(k)
309    case x <> t: L.and_left(C.fits(k, v(x)), fit_all(t, k), h)
310
311def tl_fit(+ds: List<&2, U32>, +k: Nat, +h: {fit_all(ds, k) == True{} : Bool}) -> {fit_all(Li.tl(ds), k) == True{} : Bool}:
312  match ds:
313    case Nil{}: {==}
314    case x <> t: L.and_right(C.fits(k, v(x)), fit_all(t, k), h)
315
316def hd_tl_ev(+ds: List<&2, U32>) -> {ev(ds) == Nat.add(v(Li.hd0(ds)), C.shift(8n, ev(Li.tl(ds)))) : Nat}:
317  match ds:
318    case Nil{}: {==}
319    case x <> t: {==}
320
321def skip_succ(+k: Nat, +ds: List<&2, U32>) -> {Li.skip(1n+k, ds) == Li.skip(k, Li.tl(ds)) : List<&2, U32>}:
322  match ds:
323    case Nil{}: Equal.sym(List<&2, U32>, Li.skip(k, []), [], skip_nil(k))
324    case x <> t: {==}
325
326# (a + 2^8 b) + 2^8 c == a + 2^8 (b + c)
327def sh3(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(Nat.add(a, C.shift(8n, b)), C.shift(8n, c)) == Nat.add(a, C.shift(8n, Nat.add(b, c))) : Nat}:
328  A.tr(Nat.add(Nat.add(a, C.shift(8n, b)), C.shift(8n, c)), Nat.add(a, Nat.add(C.shift(8n, b), C.shift(8n, c))), Nat.add(a, C.shift(8n, Nat.add(b, c))),
329    N.add_assoc(a, C.shift(8n, b), C.shift(8n, c)),
330    WM.cong_r(a, Nat.add(C.shift(8n, b), C.shift(8n, c)), C.shift(8n, Nat.add(b, c)), A.sy(C.shift(8n, Nat.add(b, c)), Nat.add(C.shift(8n, b), C.shift(8n, c)), WW.shift_add(8n, b, c))))
331
332def sh4(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {Nat.add(Nat.add(Nat.add(a, C.shift(8n, b)), C.shift(8n, c)), C.shift(8n, d)) == Nat.add(a, C.shift(8n, Nat.add(Nat.add(b, c), d))) : Nat}:
333  A.tr(Nat.add(Nat.add(Nat.add(a, C.shift(8n, b)), C.shift(8n, c)), C.shift(8n, d)), Nat.add(Nat.add(a, C.shift(8n, Nat.add(b, c))), C.shift(8n, d)), Nat.add(a, C.shift(8n, Nat.add(Nat.add(b, c), d))),
334    WM.cong_l(Nat.add(Nat.add(a, C.shift(8n, b)), C.shift(8n, c)), Nat.add(a, C.shift(8n, Nat.add(b, c))), C.shift(8n, d), sh3(a, b, c)),
335    sh3(a, Nat.add(b, c), d))
336
337# the sum u + ds[0] of one carry step, exact and within 9 + j bits
338def step_fit(+ds: List<&2, U32>, +u: U32, +j: Nat, +hd: {fit_all(ds, Nat.add(8n, j)) == True{} : Bool}, +hu: {C.fits(Nat.add(8n, j), v(u)) == True{} : Bool}) -> {C.fits(Nat.add(9n, j), Nat.add(v(u), v(Li.hd0(ds)))) == True{} : Bool}:
339  A.fits_add(Nat.add(8n, j), v(u), v(Li.hd0(ds)), hu, hd0_fit(ds, Nat.add(8n, j), hd))
340
341def step_ev(+ds: List<&2, U32>, +u: U32, +j: Nat, +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}, +hd: {fit_all(ds, Nat.add(8n, j)) == True{} : Bool}, +hu: {C.fits(Nat.add(8n, j), v(u)) == True{} : Bool}) -> {v(U32.add(u, Li.hd0(ds))) == Nat.add(v(u), v(Li.hd0(ds))) : Nat}:
342  WA.add_exact(1n, {==}, u, Li.hd0(ds), SH.fits_mono(Nat.add(9n, j), 32n, Nat.add(v(u), v(Li.hd0(ds))), hj, step_fit(ds, u, j, hd, hu)))
343
344# the next carry high(8, s) fits 8 + j bits again
345def next_fit(+ds: List<&2, U32>, +u: U32, +j: Nat, +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}, +hd: {fit_all(ds, Nat.add(8n, j)) == True{} : Bool}, +hu: {C.fits(Nat.add(8n, j), v(u)) == True{} : Bool}) -> {C.fits(Nat.add(8n, j), v(U32.shrn(U32.add(u, Li.hd0(ds)), 8n))) == True{} : Bool}:
346  +s = U32.add(u, Li.hd0(ds))
347  +h1 = A.fits_subst(Nat.add(9n, j), Nat.add(v(u), v(Li.hd0(ds))), v(s), A.sy(v(s), Nat.add(v(u), v(Li.hd0(ds))), step_ev(ds, u, j, hj, hd, hu)), step_fit(ds, u, j, hd, hu))
348  +h2 = SH.fits_high(8n, 1n+j, v(s), h1)
349  +h3 = SH.fits_mono(1n+j, Nat.add(8n, j), C.high(8n, v(s)), A.le_add_l(7n, j), h2)
350  A.fits_subst(Nat.add(8n, j), C.high(8n, v(s)), v(U32.shrn(s, 8n)), A.sy(v(U32.shrn(s, 8n)), C.high(8n, v(s)), SHN.shrn_high(s, 8n)), h3)
351
352# A carry pass over n limbs keeps the value: carry(n, ds, u) + 2^(8(n+1)) ds[n+1..] == u + ds.
353law carry_ev:
354  for +n: Nat
355  for +ds: List<&2, U32>
356  for +u: U32
357  for +j: Nat
358  for +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}
359  for +hd: {fit_all(ds, Nat.add(8n, j)) == True{} : Bool}
360  for +hu: {C.fits(Nat.add(8n, j), v(u)) == True{} : Bool}
361  {Nat.add(ev(Li.carry(n, ds, u)), pos(1n+n, ev(Li.skip(1n+n, ds)))) == Nat.add(v(u), ev(ds)) : Nat}
362
363def carry_ev(n, ds, u, j, hj, hd, hu):
364  match n:
365    case 0n:
366      +h = Li.hd0(ds)
367      +s = U32.add(u, h)
368      +es = step_ev(ds, u, j, hj, hd, hu)
369      +et = ev(Li.tl(ds))
370      A.tr(Nat.add(Nat.add(v(s), 0n), C.shift(8n, ev(Li.skip(1n, ds)))), Nat.add(v(s), C.shift(8n, et)), Nat.add(v(u), ev(ds)),
371        A.cadd(Nat.add(v(s), 0n), v(s), C.shift(8n, ev(Li.skip(1n, ds))), C.shift(8n, et), N.add_zero(v(s)), A.csh(8n, ev(Li.skip(1n, ds)), et, Equal.cong(List<&2, U32>, Nat, l => ev(l), Li.skip(1n, ds), Li.tl(ds), skip_succ(0n, ds)))),
372        A.tr(Nat.add(v(s), C.shift(8n, et)), Nat.add(Nat.add(v(u), v(h)), C.shift(8n, et)), Nat.add(v(u), ev(ds)),
373          WM.cong_l(v(s), Nat.add(v(u), v(h)), C.shift(8n, et), es),
374          A.tr(Nat.add(Nat.add(v(u), v(h)), C.shift(8n, et)), Nat.add(v(u), Nat.add(v(h), C.shift(8n, et))), Nat.add(v(u), ev(ds)), N.add_assoc(v(u), v(h), C.shift(8n, et)),
375            WM.cong_r(v(u), Nat.add(v(h), C.shift(8n, et)), ev(ds), A.sy(ev(ds), Nat.add(v(h), C.shift(8n, et)), hd_tl_ev(ds))))))
376    case 1n+k:
377      +h = Li.hd0(ds)
378      +s = U32.add(u, h)
379      +es = step_ev(ds, u, j, hj, hd, hu)
380      +et = ev(Li.tl(ds))
381      +u2 = U32.shrn(s, 8n)
382      +lo = v(U32.and(s, 255))
383      +c1 = ev(Li.carry(k, Li.tl(ds), u2))
384      +p1 = pos(1n+k, ev(Li.skip(1n+k, Li.tl(ds))))
385      +ih = carry_ev(k, Li.tl(ds), u2, j, hj, tl_fit(ds, Nat.add(8n, j), hd), next_fit(ds, u, j, hj, hd, hu))
386      +e0 = WM.cong_r(Nat.add(lo, C.shift(8n, c1)), C.shift(8n, pos(1n+k, ev(Li.skip(2n+k, ds)))), C.shift(8n, p1),
387        A.csh(8n, pos(1n+k, ev(Li.skip(2n+k, ds))), p1, Equal.cong(List<&2, U32>, Nat, l => pos(1n+k, ev(l)), Li.skip(2n+k, ds), Li.skip(1n+k, Li.tl(ds)), skip_succ(1n+k, ds))))
388      +e1 = sh3(lo, c1, p1)
389      +e2 = WM.cong_r(lo, C.shift(8n, Nat.add(c1, p1)), C.shift(8n, Nat.add(v(u2), et)), A.csh(8n, Nat.add(c1, p1), Nat.add(v(u2), et), ih))
390      +e3 = A.sy(Nat.add(Nat.add(lo, C.shift(8n, v(u2))), C.shift(8n, et)), Nat.add(lo, C.shift(8n, Nat.add(v(u2), et))), sh3(lo, v(u2), et))
391      +elo = A.tr(lo, C.low(8n, v(s)), C.low(8n, v(s)), FB.andm(s, 8n, 255, {==}), {==})
392      +ehi = SHN.shrn_high(s, 8n)
393      +e4 = A.tr(Nat.add(lo, C.shift(8n, v(u2))), Nat.add(C.low(8n, v(s)), C.shift(8n, C.high(8n, v(s)))), v(s),
394        A.cadd(lo, C.low(8n, v(s)), C.shift(8n, v(u2)), C.shift(8n, C.high(8n, v(s))), elo, A.csh(8n, v(u2), C.high(8n, v(s)), ehi)),
395        A.sy(v(s), Nat.add(C.low(8n, v(s)), C.shift(8n, C.high(8n, v(s)))), WW.low_high(8n, v(s))))
396      +e5 = WM.cong_l(Nat.add(lo, C.shift(8n, v(u2))), v(s), C.shift(8n, et), e4)
397      +e6 = A.tr(Nat.add(v(s), C.shift(8n, et)), Nat.add(Nat.add(v(u), v(h)), C.shift(8n, et)), Nat.add(v(u), ev(ds)),
398          WM.cong_l(v(s), Nat.add(v(u), v(h)), C.shift(8n, et), es),
399          A.tr(Nat.add(Nat.add(v(u), v(h)), C.shift(8n, et)), Nat.add(v(u), Nat.add(v(h), C.shift(8n, et))), Nat.add(v(u), ev(ds)), N.add_assoc(v(u), v(h), C.shift(8n, et)),
400            WM.cong_r(v(u), Nat.add(v(h), C.shift(8n, et)), ev(ds), A.sy(ev(ds), Nat.add(v(h), C.shift(8n, et)), hd_tl_ev(ds)))))
401      A.tr(Nat.add(Nat.add(lo, C.shift(8n, c1)), C.shift(8n, pos(1n+k, ev(Li.skip(2n+k, ds))))), Nat.add(Nat.add(lo, C.shift(8n, c1)), C.shift(8n, p1)), Nat.add(v(u), ev(ds)), e0,
402        A.tr(Nat.add(Nat.add(lo, C.shift(8n, c1)), C.shift(8n, p1)), Nat.add(lo, C.shift(8n, Nat.add(c1, p1))), Nat.add(v(u), ev(ds)), e1,
403          A.tr(Nat.add(lo, C.shift(8n, Nat.add(c1, p1))), Nat.add(lo, C.shift(8n, Nat.add(v(u2), et))), Nat.add(v(u), ev(ds)), e2,
404            A.tr(Nat.add(lo, C.shift(8n, Nat.add(v(u2), et))), Nat.add(Nat.add(lo, C.shift(8n, v(u2))), C.shift(8n, et)), Nat.add(v(u), ev(ds)), e3,
405              A.tr(Nat.add(Nat.add(lo, C.shift(8n, v(u2))), C.shift(8n, et)), Nat.add(v(s), C.shift(8n, et)), Nat.add(v(u), ev(ds)), e5, e6)))))
406
407# every limb below the top one has 8 bits
408law carry_lo:
409  for +n: Nat
410  for +ds: List<&2, U32>
411  for +u: U32
412  {fit_all(Li.take(n, Li.carry(n, ds, u)), 8n) == True{} : Bool}
413
414def carry_lo(n, ds, u):
415  match n:
416    case 0n: {==}
417    case 1n+k:
418      +s = U32.add(u, Li.hd0(ds))
419      L.and_intro(C.fits(8n, v(U32.and(s, 255))), fit_all(Li.take(k, Li.carry(k, Li.tl(ds), U32.shrn(s, 8n))), 8n),
420        A.fits_subst(8n, C.low(8n, v(s)), v(U32.and(s, 255)), A.sy(v(U32.and(s, 255)), C.low(8n, v(s)), FB.andm(s, 8n, 255, {==})), WW.low_fits(8n, v(s))),
421        carry_lo(k, Li.tl(ds), U32.shrn(s, 8n)))
422
423# the top limb fits 9 + j bits
424law carry_top:
425  for +n: Nat
426  for +ds: List<&2, U32>
427  for +u: U32
428  for +j: Nat
429  for +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}
430  for +hd: {fit_all(ds, Nat.add(8n, j)) == True{} : Bool}
431  for +hu: {C.fits(Nat.add(8n, j), v(u)) == True{} : Bool}
432  {C.fits(Nat.add(9n, j), v(Li.hd0(Li.skip(n, Li.carry(n, ds, u))))) == True{} : Bool}
433
434def carry_top(n, ds, u, j, hj, hd, hu):
435  match n:
436    case 0n:
437      A.fits_subst(Nat.add(9n, j), Nat.add(v(u), v(Li.hd0(ds))), v(U32.add(u, Li.hd0(ds))), A.sy(v(U32.add(u, Li.hd0(ds))), Nat.add(v(u), v(Li.hd0(ds))), step_ev(ds, u, j, hj, hd, hu)), step_fit(ds, u, j, hd, hu))
438    case 1n+k:
439      carry_top(k, Li.tl(ds), U32.shrn(U32.add(u, Li.hd0(ds)), 8n), j, hj, tl_fit(ds, Nat.add(8n, j), hd), next_fit(ds, u, j, hj, hd, hu))
440
441law carry_len:
442  for +n: Nat
443  for +ds: List<&2, U32>
444  for +u: U32
445  {List.length(&2, U32, Li.carry(n, ds, u)) == 1n+n : Nat}
446
447def carry_len(n, ds, u):
448  match n:
449    case 0n: {==}
450    case 1n+k:
451      +s = U32.add(u, Li.hd0(ds))
452      Equal.cong(Nat, Nat, t => 1n+t, List.length(&2, U32, Li.carry(k, Li.tl(ds), U32.shrn(s, 8n))), 1n+k, carry_len(k, Li.tl(ds), U32.shrn(s, 8n)))
453
454# ---- the 2^130 split of limb n ----
455
456law sq_ev:
457  for +n: Nat
458  for +xs: List<&2, U32>
459  {Nat.add(Nat.add(ev(Li.split(n, xs)), pos(n, C.shift(2n, v(Li.quot(n, xs))))), pos(1n+n, ev(Li.skip(1n+n, xs)))) == ev(xs) : Nat}
460
461def sq_ev(n, xs):
462  match n:
463    case 0n:
464      +h = Li.hd0(xs)
465      +la = v(U32.and(h, 3))
466      +vq = v(U32.shrn(h, 2n))
467      +et = ev(Li.tl(xs))
468      +e0 = A.cadd(Nat.add(Nat.add(la, 0n), C.shift(2n, vq)), Nat.add(la, C.shift(2n, vq)), C.shift(8n, ev(Li.skip(1n, xs))), C.shift(8n, et),
469        WM.cong_l(Nat.add(la, 0n), la, C.shift(2n, vq), N.add_zero(la)),
470        A.csh(8n, ev(Li.skip(1n, xs)), et, Equal.cong(List<&2, U32>, Nat, l => ev(l), Li.skip(1n, xs), Li.tl(xs), skip_succ(0n, xs))))
471      +e1 = A.tr(Nat.add(la, C.shift(2n, vq)), Nat.add(C.low(2n, v(h)), C.shift(2n, C.high(2n, v(h)))), v(h),
472        A.cadd(la, C.low(2n, v(h)), C.shift(2n, vq), C.shift(2n, C.high(2n, v(h))), FB.andm(h, 2n, 3, {==}), A.csh(2n, vq, C.high(2n, v(h)), SHN.shrn_high(h, 2n))),
473        A.sy(v(h), Nat.add(C.low(2n, v(h)), C.shift(2n, C.high(2n, v(h)))), WW.low_high(2n, v(h))))
474      A.tr(Nat.add(Nat.add(Nat.add(la, 0n), C.shift(2n, vq)), C.shift(8n, ev(Li.skip(1n, xs)))), Nat.add(Nat.add(la, C.shift(2n, vq)), C.shift(8n, et)), ev(xs), e0,
475        A.tr(Nat.add(Nat.add(la, C.shift(2n, vq)), C.shift(8n, et)), Nat.add(v(h), C.shift(8n, et)), ev(xs), WM.cong_l(Nat.add(la, C.shift(2n, vq)), v(h), C.shift(8n, et), e1),
476          A.sy(ev(xs), Nat.add(v(h), C.shift(8n, et)), hd_tl_ev(xs))))
477    case 1n+k:
478      +h = Li.hd0(xs)
479      +sp = ev(Li.split(k, Li.tl(xs)))
480      +pq = pos(k, C.shift(2n, v(Li.quot(k, Li.tl(xs)))))
481      +pr = pos(1n+k, ev(Li.skip(1n+k, Li.tl(xs))))
482      +et = ev(Li.tl(xs))
483      +e0 = WM.cong_r(Nat.add(Nat.add(v(h), C.shift(8n, sp)), C.shift(8n, pq)), C.shift(8n, pos(1n+k, ev(Li.skip(2n+k, xs)))), C.shift(8n, pr),
484        A.csh(8n, pos(1n+k, ev(Li.skip(2n+k, xs))), pr, Equal.cong(List<&2, U32>, Nat, l => pos(1n+k, ev(l)), Li.skip(2n+k, xs), Li.skip(1n+k, Li.tl(xs)), skip_succ(1n+k, xs))))
485      A.tr(Nat.add(Nat.add(Nat.add(v(h), C.shift(8n, sp)), C.shift(8n, pq)), C.shift(8n, pos(1n+k, ev(Li.skip(2n+k, xs))))), Nat.add(Nat.add(Nat.add(v(h), C.shift(8n, sp)), C.shift(8n, pq)), C.shift(8n, pr)), ev(xs), e0,
486        A.tr(Nat.add(Nat.add(Nat.add(v(h), C.shift(8n, sp)), C.shift(8n, pq)), C.shift(8n, pr)), Nat.add(v(h), C.shift(8n, Nat.add(Nat.add(sp, pq), pr))), ev(xs), sh4(v(h), sp, pq, pr),
487          A.tr(Nat.add(v(h), C.shift(8n, Nat.add(Nat.add(sp, pq), pr))), Nat.add(v(h), C.shift(8n, et)), ev(xs),
488            WM.cong_r(v(h), C.shift(8n, Nat.add(Nat.add(sp, pq), pr)), C.shift(8n, et), A.csh(8n, Nat.add(Nat.add(sp, pq), pr), et, sq_ev(k, Li.tl(xs)))),
489            A.sy(ev(xs), Nat.add(v(h), C.shift(8n, et)), hd_tl_ev(xs)))))
490
491# ---- lengths ----
492
493def len(xs: List<&2, U32>) -> Nat:
494  List.length(&2, U32, xs)
495
496law len_add:
497  for +a: List<&2, U32>
498  for +b: List<&2, U32>
499  for +n: Nat
500  for +ha: {Nat.is_le(len(a), n) == True{} : Bool}
501  for +hb: {Nat.is_le(len(b), n) == True{} : Bool}
502  {Nat.is_le(len(Li.add(a, b)), n) == True{} : Bool}
503
504def len_add(a, b, n, ha, hb):
505  match a b:
506    case Nil{} _: hb
507    case x <> at Nil{}: ha
508    case x <> at y <> bt:
509      match n:
510        case 0n: Empty.absurd({Nat.is_le(len(Li.add(x <> at, y <> bt)), 0n) == True{} : Bool}, L.false_true(ha))
511        case 1n+m: len_add(at, bt, m, ha, hb)
512
513law len_scale:
514  for +c: U32
515  for +a: List<&2, U32>
516  {len(Li.scale(c, a)) == len(a) : Nat}
517
518def len_scale(c, a):
519  match a:
520    case Nil{}: {==}
521    case x <> t: Equal.cong(Nat, Nat, z => 1n+z, len(Li.scale(c, t)), len(t), len_scale(c, t))
522
523law len_mul:
524  for +x: List<&2, U32>
525  for +r: List<&2, U32>
526  for +n: Nat
527  for +hx: {Nat.is_le(len(x), n) == True{} : Bool}
528  {Nat.is_le(len(Li.mul(x, r)), Nat.add(len(r), n)) == True{} : Bool}
529
530def len_mul(x, r, n, hx):
531  match r:
532    case Nil{}: N.zero_le(n)
533    case r0 <> rs:
534      len_add(Li.scale(r0, x), 0 <> Li.mul(x, rs), Nat.add(1n+len(rs), n),
535        A.le_substl(len(x), len(Li.scale(r0, x)), Nat.add(1n+len(rs), n), A.sy(len(Li.scale(r0, x)), len(x), len_scale(r0, x)), N.le_trans(len(x), n, Nat.add(1n+len(rs), n), hx, A.le_add_l(1n+len(rs), n))),
536        len_mul(x, rs, n, hx))
537
538law len_take:
539  for +n: Nat
540  for +xs: List<&2, U32>
541  {Nat.is_le(len(Li.take(n, xs)), n) == True{} : Bool}
542
543def len_take(n, xs):
544  match n xs:
545    case 0n _: {==}
546    case 1n+k Nil{}: {==}
547    case 1n+k x <> t: len_take(k, t)
548
549law len_skip:
550  for +n: Nat
551  for +xs: List<&2, U32>
552  for +b: Nat
553  for +h: {Nat.is_le(len(xs), Nat.add(n, b)) == True{} : Bool}
554  {Nat.is_le(len(Li.skip(n, xs)), b) == True{} : Bool}
555
556def len_skip(n, xs, b, h):
557  match n xs:
558    case 0n _: h
559    case 1n+k Nil{}: N.zero_le(b)
560    case 1n+k x <> t: len_skip(k, t, b, h)
561
562law skip_long:
563  for +n: Nat
564  for +xs: List<&2, U32>
565  for +h: {Nat.is_le(len(xs), n) == True{} : Bool}
566  {Li.skip(n, xs) == [] : List<&2, U32>}
567
568def skip_long(n, xs, h):
569  match n xs:
570    case 0n Nil{}: {==}
571    case 0n x <> t: Empty.absurd({Li.skip(0n, x <> t) == [] : List<&2, U32>}, L.false_true(h))
572    case 1n+k Nil{}: {==}
573    case 1n+k x <> t: skip_long(k, t, h)
574
575# ---- bounds ----
576
577law le_take:
578  for +n: Nat
579  for +xs: List<&2, U32>
580  for +b: Nat
581  for +h: {le_all(xs, b) == True{} : Bool}
582  {le_all(Li.take(n, xs), b) == True{} : Bool}
583
584def le_take(n, xs, b, h):
585  match n xs:
586    case 0n _: {==}
587    case 1n+k Nil{}: {==}
588    case 1n+k x <> t: cons_le(x, Li.take(k, t), b, hd_le(x, t, b, h), le_take(k, t, b, tl_le(x, t, b, h)))
589
590law le_skip:
591  for +n: Nat
592  for +xs: List<&2, U32>
593  for +b: Nat
594  for +h: {le_all(xs, b) == True{} : Bool}
595  {le_all(Li.skip(n, xs), b) == True{} : Bool}
596
597def le_skip(n, xs, b, h):
598  match n xs:
599    case 0n _: h
600    case 1n+k Nil{}: {==}
601    case 1n+k x <> t: le_skip(k, t, b, tl_le(x, t, b, h))
602
603law fit_le:
604  for +xs: List<&2, U32>
605  for +k: Nat
606  for +one: Nat
607  for +h1: {one == 1n : Nat}
608  for +h: {fit_all(xs, k) == True{} : Bool}
609  {le_all(xs, C.shift(k, one)) == True{} : Bool}
610
611def fit_le(xs, k, one, h1, h):
612  match xs:
613    case Nil{}: {==}
614    case x <> t: cons_le(x, t, C.shift(k, one), A.le_one(k, one, h1, v(x), L.and_left(C.fits(k, v(x)), fit_all(t, k), h)), fit_le(t, k, one, h1, L.and_right(C.fits(k, v(x)), fit_all(t, k), h)))
615
616law le_fit:
617  for +xs: List<&2, U32>
618  for +b: Nat
619  for +k: Nat
620  for +one: Nat
621  for +h1: {one == 1n : Nat}
622  for +hb: {Nat.is_lt(b, C.shift(k, one)) == True{} : Bool}
623  for +h: {le_all(xs, b) == True{} : Bool}
624  {fit_all(xs, k) == True{} : Bool}
625
626def le_fit(xs, b, k, one, h1, hb, h):
627  match xs:
628    case Nil{}: {==}
629    case x <> t: L.and_intro(C.fits(k, v(x)), fit_all(t, k), WW.fits_one(k, one, h1, v(x), N.le_lt_trans(v(x), b, C.shift(k, one), hd_le(x, t, b, h), hb)), le_fit(t, b, k, one, h1, hb, tl_le(x, t, b, h)))
630
631law fit_mono:
632  for +xs: List<&2, U32>
633  for +a: Nat
634  for +b: Nat
635  for +hab: {Nat.is_le(a, b) == True{} : Bool}
636  for +h: {fit_all(xs, a) == True{} : Bool}
637  {fit_all(xs, b) == True{} : Bool}
638
639def fit_mono(xs, a, b, hab, h):
640  match xs:
641    case Nil{}: {==}
642    case x <> t: L.and_intro(C.fits(b, v(x)), fit_all(t, b), SH.fits_mono(a, b, v(x), hab, L.and_left(C.fits(a, v(x)), fit_all(t, a), h)), fit_mono(t, a, b, hab, L.and_right(C.fits(a, v(x)), fit_all(t, a), h)))
643
644law fit_take:
645  for +n: Nat
646  for +xs: List<&2, U32>
647  for +k: Nat
648  for +h: {fit_all(xs, k) == True{} : Bool}
649  {fit_all(Li.take(n, xs), k) == True{} : Bool}
650
651def fit_take(n, xs, k, h):
652  match n xs:
653    case 0n _: {==}
654    case 1n+m Nil{}: {==}
655    case 1n+m x <> t: L.and_intro(C.fits(k, v(x)), fit_all(Li.take(m, t), k), L.and_left(C.fits(k, v(x)), fit_all(t, k), h), fit_take(m, t, k, L.and_right(C.fits(k, v(x)), fit_all(t, k), h)))
656
657# limbs of 8 bits: the value is below 2^(8 len)
658law ev_lt:
659  for +xs: List<&2, U32>
660  for +one: Nat
661  for +h1: {one == 1n : Nat}
662  for +h: {fit_all(xs, 8n) == True{} : Bool}
663  {Nat.is_lt(ev(xs), pos(len(xs), one)) == True{} : Bool}
664
665def ev_lt(xs, one, h1, h):
666  match xs:
667    case Nil{}: A.lt_subst(0n, 1n, one, A.sy(one, 1n, h1), {==})
668    case x <> t:
669      +ht = ev_lt(t, one, h1, L.and_right(C.fits(8n, v(x)), fit_all(t, 8n), h))
670      +hx = WW.lt_of_fits(8n, v(x), L.and_left(C.fits(8n, v(x)), fit_all(t, 8n), h))
671      +p = pos(len(t), one)
672      # v x + 2^8 ev t < 2^8 + 2^8 ev t = 2^8 (1 + ev t) <= 2^8 p
673      +a1 = A.lt_le_add(v(x), C.shift(8n, ev(t)), C.pow2(8n), C.shift(8n, ev(t)), hx, N.le_refl(C.shift(8n, ev(t))))
674      +e1 = A.tr(Nat.add(C.pow2(8n), C.shift(8n, ev(t))), Nat.add(C.shift(8n, 1n), C.shift(8n, ev(t))), C.shift(8n, 1n+ev(t)), {==}, A.sy(C.shift(8n, 1n+ev(t)), Nat.add(C.shift(8n, 1n), C.shift(8n, ev(t))), WW.shift_add(8n, 1n, ev(t))))
675      N.lt_le_trans(Nat.add(v(x), C.shift(8n, ev(t))), C.shift(8n, 1n+ev(t)), C.shift(8n, p), A.lt_subst(Nat.add(v(x), C.shift(8n, ev(t))), Nat.add(C.pow2(8n), C.shift(8n, ev(t))), C.shift(8n, 1n+ev(t)), e1, a1), WW.shift_mono(8n, 1n+ev(t), p, N.lt_succ_le_succ(ev(t), p, ht)))
676
677law fit_take_nil:
678  for +n: Nat
679  for +k: Nat
680  {fit_all(Li.take(n, []), k) == True{} : Bool}
681
682def fit_take_nil(n, k):
683  match n:
684    case 0n: {==}
685    case 1n+m: {==}
686
687law split_fit:
688  for +n: Nat
689  for +xs: List<&2, U32>
690  for +h: {fit_all(Li.take(n, xs), 8n) == True{} : Bool}
691  {fit_all(Li.split(n, xs), 8n) == True{} : Bool}
692
693def split_fit(n, xs, h):
694  match n:
695    case 0n:
696      +x = Li.hd0(xs)
697      L.and_intro(C.fits(8n, v(U32.and(x, 3))), True{}, SH.fits_mono(2n, 8n, v(U32.and(x, 3)), {==}, A.fits_subst(2n, C.low(2n, v(x)), v(U32.and(x, 3)), A.sy(v(U32.and(x, 3)), C.low(2n, v(x)), FB.andm(x, 2n, 3, {==})), WW.low_fits(2n, v(x)))), {==})
698    case 1n+k:
699      match xs:
700        case Nil{}: L.and_intro(C.fits(8n, 0n), fit_all(Li.split(k, []), 8n), {==}, split_fit(k, [], fit_take_nil(k, 8n)))
701        case x <> t: L.and_intro(C.fits(8n, v(x)), fit_all(Li.split(k, t), 8n), L.and_left(C.fits(8n, v(x)), fit_all(Li.take(k, t), 8n), h), split_fit(k, t, L.and_right(C.fits(8n, v(x)), fit_all(Li.take(k, t), 8n), h)))
702
703law fit_split:
704  for +n: Nat
705  for +xs: List<&2, U32>
706  for +k: Nat
707  for +h1: {fit_all(Li.take(n, xs), k) == True{} : Bool}
708  for +h2: {fit_all(Li.skip(n, xs), k) == True{} : Bool}
709  {fit_all(xs, k) == True{} : Bool}
710
711def fit_split(n, xs, k, h1, h2):
712  match n xs:
713    case 0n _: h2
714    case 1n+m Nil{}: {==}
715    case 1n+m x <> t: L.and_intro(C.fits(k, v(x)), fit_all(t, k), L.and_left(C.fits(k, v(x)), fit_all(Li.take(m, t), k), h1), fit_split(m, t, k, L.and_right(C.fits(k, v(x)), fit_all(Li.take(m, t), k), h1), h2))
716
717law quot_top:
718  for +n: Nat
719  for +xs: List<&2, U32>
720  {Li.quot(n, xs) == U32.shrn(Li.hd0(Li.skip(n, xs)), 2n) : U32}
721
722def quot_top(n, xs):
723  match n:
724    case 0n: {==}
725    case 1n+k: Equal.trans(U32, Li.quot(k, Li.tl(xs)), U32.shrn(Li.hd0(Li.skip(k, Li.tl(xs))), 2n), U32.shrn(Li.hd0(Li.skip(1n+k, xs)), 2n), quot_top(k, Li.tl(xs)),
726      Equal.cong(List<&2, U32>, U32, l => U32.shrn(Li.hd0(l), 2n), Li.skip(k, Li.tl(xs)), Li.skip(1n+k, xs), Equal.sym(List<&2, U32>, Li.skip(1n+k, xs), Li.skip(k, Li.tl(xs)), skip_succ(k, xs))))
727
728law ev_one:
729  for +xs: List<&2, U32>
730  for +h: {Nat.is_le(len(xs), 1n) == True{} : Bool}
731  {ev(xs) == v(Li.hd0(xs)) : Nat}
732
733def ev_one(xs, h):
734  match xs:
735    case Nil{}: {==}
736    case x <> t:
737      match t:
738        case Nil{}: N.add_zero(v(x))
739        case y <> u: Empty.absurd({ev(x <> y <> u) == v(x) : Nat}, L.false_true(h))