1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../src/crypto/poly1305/limbs.bend as Li
4	import ../../lib/nat.bend as N
5	import ../../lib/logic.bend as L
6	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
7	import ../../math/typed/width.bend as WW
8	import ../../math/typed/w64mul.bend as WM
9	import ../../math/typed/w64add.bend as WA
10	import ../../math/typed/w64sh.bend as SH
11	import ../../math/typed/shrn.bend as SHN
12	import ../../math/typed/f64bits.bend as FB
13	import ./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	
21	def v(+x: U32) -> Nat:
22	  U32.to_nat(x)
23	
24	def 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	
29	def 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	
34	def 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	
37	def 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	
40	def 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	
43	law 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	
51	def 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
60	def 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	
63	law 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	
73	def 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	
87	law 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	
97	def 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	
110	def 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	
114	law 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	
124	def 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	
137	law 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	
147	def 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	
158	law 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	
168	def 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	
181	law 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	
191	def 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)
219	def pos(n: Nat, +y: Nat) -> Nat:
220	  match n:
221	    case 0n: y
222	    case 1n+k: C.shift(8n, pos(k, y))
223	
224	law pos_zero:
225	  for +n: Nat
226	  {pos(n, 0n) == 0n : Nat}
227	
228	def 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	
233	law 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	
239	def 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	
244	law skip_nil:
245	  for +n: Nat
246	  {Li.skip(n, []) == [] : List<&2, U32>}
247	
248	def 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)
254	law 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	
259	def 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	
270	law take_nil_ev:
271	  for +n: Nat
272	  {ev(Li.take(n, [])) == 0n : Nat}
273	
274	def take_nil_ev(n):
275	  match n:
276	    case 0n: {==}
277	    case 1n+k: {==}
278	
279	law 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	
284	def 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	
292	def 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	
297	law fits_zero:
298	  for +k: Nat
299	  {C.fits(k, 0n) == True{} : Bool}
300	
301	def fits_zero(k):
302	  match k:
303	    case 0n: {==}
304	    case 1n+p: fits_zero(p)
305	
306	def 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	
311	def 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	
316	def 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	
321	def 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)
327	def 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	
332	def 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
338	def 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	
341	def 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
345	def 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.
353	law 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	
363	def 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
408	law 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	
414	def 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
424	law 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	
434	def 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	
441	law 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	
447	def 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	
456	law 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	
461	def 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	
493	def len(xs: List<&2, U32>) -> Nat:
494	  List.length(&2, U32, xs)
495	
496	law 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	
504	def 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	
513	law len_scale:
514	  for +c: U32
515	  for +a: List<&2, U32>
516	  {len(Li.scale(c, a)) == len(a) : Nat}
517	
518	def 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	
523	law 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	
530	def 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	
538	law 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	
543	def 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	
549	law 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	
556	def 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	
562	law 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	
568	def 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	
577	law 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	
584	def 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	
590	law 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	
597	def 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	
603	law 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	
611	def 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	
616	law 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	
626	def 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	
631	law 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	
639	def 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	
644	law 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	
651	def 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)
658	law 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	
665	def 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	
677	law fit_take_nil:
678	  for +n: Nat
679	  for +k: Nat
680	  {fit_all(Li.take(n, []), k) == True{} : Bool}
681	
682	def fit_take_nil(n, k):
683	  match n:
684	    case 0n: {==}
685	    case 1n+m: {==}
686	
687	law 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	
693	def 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	
703	law 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	
711	def 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	
717	law 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	
722	def 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	
728	law 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	
733	def 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))