1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/crypto/poly1305.bend as R
4	import ../../../src/crypto/poly1305/limbs.bend as Li
5	import ../../lib/nat.bend as N
6	import ../../lib/logic.bend as L
7	import ../../lib/arith.bend as AR
8	import ../../lib/u32.bend as U3
9	import ../../lib/u32alg.bend as UA
10	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
11	import ../../math/typed/width.bend as WW
12	import ../../math/typed/w64mul.bend as WM
13	import ../../math/typed/w64sh.bend as SH
14	import ../../math/typed/shrn.bend as SHN
15	import ../../math/typed/f64bits.bend as FB
16	import ../../math/natural/arith.bend as NR
17	import ./arith.bend as A
18	import ./value.bend as V
19	import ./step.bend as ST
20	
21	# The last steps: freeze (the canonical value mod p, by a masked choice) and
22	# the 16 tag bytes (h + s mod 2^128, little-endian).
23	
24	# ---- words ----
25	
26	def wones(n: Nat) -> Word(n):
27	  match n:
28	    case 0n: WNil{}
29	    case 1n+p: WCon{True{}, wones(p)}
30	
31	law wand0:
32	  for +n: Nat
33	  for +w: Word(n)
34	  {Word.and(n, Word.zero(n), w) == Word.zero(n) : Word(n)}
35	
36	def wand0(n, w):
37	  match n:
38	    case 0n:
39	      match w:
40	        case WNil{}: {==}
41	    case 1n+p:
42	      match w:
43	        case WCon{b, t}: Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.and(p, Word.zero(p), t), Word.zero(p), wand0(p, t))
44	
45	law wand1:
46	  for +n: Nat
47	  for +w: Word(n)
48	  {Word.and(n, wones(n), w) == w : Word(n)}
49	
50	def wand1(n, w):
51	  match n:
52	    case 0n:
53	      match w:
54	        case WNil{}: {==}
55	    case 1n+p:
56	      match w:
57	        case WCon{b, t}: Equal.cong(Word(p), Word(1n+p), x => WCon{b, x}, Word.and(p, wones(p), t), t, wand1(p, t))
58	
59	law wxor0:
60	  for +n: Nat
61	  for +w: Word(n)
62	  {Word.xor(n, w, Word.zero(n)) == w : Word(n)}
63	
64	def wxor0(n, w):
65	  match n:
66	    case 0n:
67	      match w:
68	        case WNil{}: {==}
69	    case 1n+p:
70	      match w:
71	        case WCon{b, t}:
72	          match b:
73	            case False{}: Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.xor(p, t, Word.zero(p)), t, wxor0(p, t))
74	            case True{}: Equal.cong(Word(p), Word(1n+p), x => WCon{True{}, x}, Word.xor(p, t, Word.zero(p)), t, wxor0(p, t))
75	
76	law wxor2:
77	  for +n: Nat
78	  for +x: Word(n)
79	  for +y: Word(n)
80	  {Word.xor(n, x, Word.xor(n, x, y)) == y : Word(n)}
81	
82	def wxor2(n, x, y):
83	  match n:
84	    case 0n:
85	      match x y:
86	        case WNil{} WNil{}: {==}
87	    case 1n+p:
88	      match x y:
89	        case WCon{False{}, s} WCon{False{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{False{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))
90	        case WCon{False{}, s} WCon{True{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{True{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))
91	        case WCon{True{}, s} WCon{False{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{False{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))
92	        case WCon{True{}, s} WCon{True{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{True{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))
93	
94	def pick0(+x: U32, +y: U32) -> {Li.pick(0, x, y) == x : U32}:
95	  match x y:
96	    case U32{a} U32{b}:
97	      Equal.trans(U32, U32{Word.xor(32n, a, Word.and(32n, Word.zero(32n), Word.xor(32n, a, b)))}, U32{Word.xor(32n, a, Word.zero(32n))}, U32{a},
98	        Equal.cong(Word(32n), U32, w => U32{Word.xor(32n, a, w)}, Word.and(32n, Word.zero(32n), Word.xor(32n, a, b)), Word.zero(32n), wand0(32n, Word.xor(32n, a, b))),
99	        Equal.cong(Word(32n), U32, w => U32{w}, Word.xor(32n, a, Word.zero(32n)), a, wxor0(32n, a)))
100	
101	def pick1(+x: U32, +y: U32) -> {Li.pick(4294967295, x, y) == y : U32}:
102	  match x y:
103	    case U32{a} U32{b}:
104	      Equal.trans(U32, U32{Word.xor(32n, a, Word.and(32n, wones(32n), Word.xor(32n, a, b)))}, U32{Word.xor(32n, a, Word.xor(32n, a, b))}, U32{b},
105	        Equal.cong(Word(32n), U32, w => U32{Word.xor(32n, a, w)}, Word.and(32n, wones(32n), Word.xor(32n, a, b)), Word.xor(32n, a, b), wand1(32n, Word.xor(32n, a, b))),
106	        Equal.cong(Word(32n), U32, w => U32{w}, Word.xor(32n, a, Word.xor(32n, a, b)), b, wxor2(32n, a, b)))
107	
108	law sel0:
109	  for +a: List<&2, U32>
110	  for +b: List<&2, U32>
111	  for +h: {V.len(a) == V.len(b) : Nat}
112	  {Li.select(0, a, b) == a : List<&2, U32>}
113	
114	def sel0(a, b, h):
115	  match a b:
116	    case Nil{} Nil{}: {==}
117	    case Nil{} y <> bt: Empty.absurd({Li.select(0, [], y <> bt) == [] : List<&2, U32>}, N.zero_succ(V.len(bt), h))
118	    case x <> at Nil{}: Empty.absurd({Li.select(0, x <> at, []) == x <> at : List<&2, U32>}, N.succ_zero(V.len(at), h))
119	    case x <> at y <> bt:
120	      Equal.trans(List<&2, U32>, Li.pick(0, x, y) <> Li.select(0, at, bt), x <> Li.select(0, at, bt), x <> at,
121	        Equal.cong(U32, List<&2, U32>, z => z <> Li.select(0, at, bt), Li.pick(0, x, y), x, pick0(x, y)),
122	        Equal.cong(List<&2, U32>, List<&2, U32>, z => x <> z, Li.select(0, at, bt), at, sel0(at, bt, N.succ_inj(V.len(at), V.len(bt), h))))
123	
124	law sel1:
125	  for +a: List<&2, U32>
126	  for +b: List<&2, U32>
127	  for +h: {V.len(a) == V.len(b) : Nat}
128	  {Li.select(4294967295, a, b) == b : List<&2, U32>}
129	
130	def sel1(a, b, h):
131	  match a b:
132	    case Nil{} Nil{}: {==}
133	    case Nil{} y <> bt: Empty.absurd({Li.select(4294967295, [], y <> bt) == y <> bt : List<&2, U32>}, N.zero_succ(V.len(bt), h))
134	    case x <> at Nil{}: Empty.absurd({Li.select(4294967295, x <> at, []) == [] : List<&2, U32>}, N.succ_zero(V.len(at), h))
135	    case x <> at y <> bt:
136	      Equal.trans(List<&2, U32>, Li.pick(4294967295, x, y) <> Li.select(4294967295, at, bt), y <> Li.select(4294967295, at, bt), y <> bt,
137	        Equal.cong(U32, List<&2, U32>, z => z <> Li.select(4294967295, at, bt), Li.pick(4294967295, x, y), y, pick1(x, y)),
138	        Equal.cong(List<&2, U32>, List<&2, U32>, z => y <> z, Li.select(4294967295, at, bt), bt, sel1(at, bt, N.succ_inj(V.len(at), V.len(bt), h))))
139	
140	law len_take_eq:
141	  for +n: Nat
142	  for +xs: List<&2, U32>
143	  for +h: {Nat.is_le(n, V.len(xs)) == True{} : Bool}
144	  {V.len(Li.take(n, xs)) == n : Nat}
145	
146	def len_take_eq(n, xs, h):
147	  match n xs:
148	    case 0n _: {==}
149	    case 1n+k Nil{}: Empty.absurd({V.len(Li.take(1n+k, [])) == 1n+k : Nat}, L.false_true(h))
150	    case 1n+k x <> t: Equal.cong(Nat, Nat, z => 1n+z, V.len(Li.take(k, t)), k, len_take_eq(k, t, h))
151	
152	# ---- freeze ----
153	
154	# x < 2x for x >= 1
155	def lt_dbl(+x: Nat, +h: {Nat.is_le(1n, x) == True{} : Bool}) -> {Nat.is_lt(x, Nat.double(x)) == True{} : Bool}:
156	  A.lt_subst(x, Nat.add(x, x), Nat.double(x), A.sy(Nat.double(x), Nat.add(x, x), NA.double_self(x)),
157	    A.lt_substl(Nat.add(x, 0n), x, Nat.add(x, x), N.add_zero(x), N.lt_add_left(0n, x, x, N.succ_le_lt(0n, x, h))))
158	
159	# the facts about h, g = carry(h + 5) and the choice bit shared by both cases
160	def hval(+h: List<&2, U32>) -> Nat:
161	  V.ev(h)
162	
163	def gg(+h: List<&2, U32>) -> List<&2, U32>:
164	  Li.carry(16n, Li.add(h, [5]), 0)
165	
166	def qq(+h: List<&2, U32>) -> Nat:
167	  C.high(130n, Nat.add(V.ev(h), 5n))
168	
169	law g_ev:
170	  for +one: Nat
171	  for +h1: {one == 1n : Nat}
172	  for +h: List<&2, U32>
173	  for +hh: {ST.inv(h) == True{} : Bool}
174	  {V.ev(gg(h)) == Nat.add(V.ev(h), 5n) : Nat}
175	
176	def g_ev(one, h1, h, hh):
177	  +s8 = C.shift(8n, one)
178	  +hl = N.eq_from_is_eq(V.len(h), 17n, L.and_left(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))
179	  +hr2 = L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh)
180	  +hf = L.and_left(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), hr2)
181	  +a = Li.add(h, [5])
182	  +h5 = V.cons_le(5, [], s8, L.subst(Nat, z => {Nat.is_le(5n, C.shift(8n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), {==})
183	  +hf1 = ST.s8fit(one, h1)
184	  +ea = V.add_ev(h, [5], s8, s8, V.fit_le(h, 8n, one, h1, hf), h5, hf1)
185	  +s9 = C.shift(9n, one)
186	  +l10 = A.lt_substl(s9, Nat.add(s8, s8), Nat.double(s9), NA.double_self(s8), lt_dbl(s9, A.one_le_shift(9n, one, h1)))
187	  +ha = V.le_fit(a, Nat.add(s8, s8), 10n, one, h1, l10, V.add_le(h, [5], s8, s8, V.fit_le(h, 8n, one, h1, hf), h5, hf1))
188	  +hal = V.len_add(h, [5], 17n, N.eq_le(V.len(h), 17n, hl), {==})
189	  +ce = V.carry_ev(16n, a, 0, 2n, {==}, ha, {==})
190	  +sk = V.skip_long(17n, a, hal)
191	  A.tr(V.ev(gg(h)), Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), Nat.add(V.ev(h), 5n),
192	    A.tr(V.ev(gg(h)), Nat.add(V.ev(gg(h)), 0n), Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), A.sy(Nat.add(V.ev(gg(h)), 0n), V.ev(gg(h)), N.add_zero(V.ev(gg(h)))),
193	      Equal.cong(List<&2, U32>, Nat, l => Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(l))), [], Li.skip(17n, a), Equal.sym(List<&2, U32>, Li.skip(17n, a), [], sk))),
194	    A.tr(Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), V.ev(a), Nat.add(V.ev(h), 5n), ce, ea))
195	
196	def lenh(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(h) == 17n : Nat}:
197	  N.eq_from_is_eq(V.len(h), 17n, L.and_left(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))
198	
199	def fith(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.fit_all(h, 8n) == True{} : Bool}:
200	  L.and_left(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))
201	
202	def toph(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n) == True{} : Bool}:
203	  L.and_right(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))
204	
205	def len16(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(Li.take(16n, h)) == 16n : Nat}:
206	  len_take_eq(16n, h, A.le_subst(16n, 17n, V.len(h), A.sy(V.len(h), 17n, lenh(h, hh)), {==}))
207	
208	law hsplit:
209	  for +h: List<&2, U32>
210	  for +hh: {ST.inv(h) == True{} : Bool}
211	  {V.ev(h) == Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.v(Li.hd0(Li.skip(16n, h))))) : Nat}
212	
213	def hsplit(h, hh):
214	  +sk = Li.skip(16n, h)
215	  A.tr(V.ev(h), Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.ev(sk))), Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.v(Li.hd0(sk)))), V.ts_ev(16n, h),
216	    WM.cong_r(V.ev(Li.take(16n, h)), V.pos(16n, V.ev(sk)), V.pos(16n, V.v(Li.hd0(sk))), Equal.cong(Nat, Nat, z => V.pos(16n, z), V.ev(sk), V.v(Li.hd0(sk)),
217	      V.ev_one(sk, V.len_skip(16n, h, 1n, N.eq_le(V.len(h), 17n, lenh(h, hh)))))))
218	
219	# ev(h) < 2^128 + 2^130
220	law hlt:
221	  for +one: Nat
222	  for +h1: {one == 1n : Nat}
223	  for +h: List<&2, U32>
224	  for +hh: {ST.inv(h) == True{} : Bool}
225	  {Nat.is_lt(V.ev(h), Nat.add(V.pos(16n, one), C.shift(130n, one))) == True{} : Bool}
226	
227	def hlt(one, h1, h, hh):
228	  +lh = V.ev(Li.take(16n, h))
229	  +vt = V.v(Li.hd0(Li.skip(16n, h)))
230	  +u = V.pos(16n, one)
231	  +l1 = A.lt_subst(lh, V.pos(V.len(Li.take(16n, h)), one), u, Equal.cong(Nat, Nat, z => V.pos(z, one), V.len(Li.take(16n, h)), 16n, len16(h, hh)), V.ev_lt(Li.take(16n, h), one, h1, V.fit_take(16n, h, 8n, fith(h, hh))))
232	  +e4 = A.sy(C.shift(2n, one), 4n, Equal.cong(Nat, Nat, z => C.shift(2n, z), one, 1n, h1))
233	  +l2 = WW.shift_mono(128n, vt, C.shift(2n, one), A.le_subst(vt, 4n, C.shift(2n, one), e4, toph(h, hh)))
234	  A.lt_substl(Nat.add(lh, V.pos(16n, vt)), V.ev(h), Nat.add(u, C.shift(130n, one)), A.sy(V.ev(h), Nat.add(lh, V.pos(16n, vt)), hsplit(h, hh)), A.lt_le_add(lh, V.pos(16n, vt), u, C.shift(130n, one), l1, l2))
235	
236	def lg(+h: List<&2, U32>) -> Nat:
237	  V.ev(Li.take(16n, gg(h)))
238	
239	def tg(+h: List<&2, U32>) -> Nat:
240	  Nat.add(V.v(Li.hd0(Li.skip(16n, gg(h)))), 0n)
241	
242	law gsplit:
243	  for +one: Nat
244	  for +h1: {one == 1n : Nat}
245	  for +h: List<&2, U32>
246	  for +hh: {ST.inv(h) == True{} : Bool}
247	  {Nat.add(V.ev(h), 5n) == Nat.add(lg(h), C.shift(128n, tg(h))) : Nat}
248	
249	def gsplit(one, h1, h, hh):
250	  A.tr(Nat.add(V.ev(h), 5n), V.ev(gg(h)), Nat.add(lg(h), C.shift(128n, tg(h))), A.sy(V.ev(gg(h)), Nat.add(V.ev(h), 5n), g_ev(one, h1, h, hh)), V.ts_ev(16n, gg(h)))
251	
252	def flg(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>) -> {C.fits(128n, lg(h)) == True{} : Bool}:
253	  WW.fits_one(128n, one, h1, lg(h), V.ev_lt(Li.take(16n, gg(h)), one, h1, V.carry_lo(16n, Li.add(h, [5]), 0)))
254	
255	def bb(+h: List<&2, U32>) -> U32:
256	  U32.shrn(Li.hd0(Li.skip(16n, gg(h))), 2n)
257	
258	law bval:
259	  for +one: Nat
260	  for +h1: {one == 1n : Nat}
261	  for +h: List<&2, U32>
262	  for +hh: {ST.inv(h) == True{} : Bool}
263	  {V.v(bb(h)) == qq(h) : Nat}
264	
265	def bval(one, h1, h, hh):
266	  +x = Nat.add(V.ev(h), 5n)
267	  +tp = V.v(Li.hd0(Li.skip(16n, gg(h))))
268	  +ehi = A.tr(C.high(128n, x), C.high(128n, Nat.add(lg(h), C.shift(128n, tg(h)))), tg(h), Equal.cong(Nat, Nat, z => C.high(128n, z), x, Nat.add(lg(h), C.shift(128n, tg(h))), gsplit(one, h1, h, hh)), WW.high_u(128n, lg(h), tg(h), flg(one, h1, h)))
269	  A.tr(V.v(bb(h)), C.high(2n, tp), qq(h), SHN.shrn_high(Li.hd0(Li.skip(16n, gg(h))), 2n),
270	    A.tr(C.high(2n, tp), C.high(2n, C.high(128n, x)), qq(h), Equal.cong(Nat, Nat, z => C.high(2n, z), tp, C.high(128n, x), A.tr(tp, tg(h), C.high(128n, x), A.sy(tg(h), tp, N.add_zero(tp)), A.sy(C.high(128n, x), tg(h), ehi))),
271	      A.sy(qq(h), C.high(2n, C.high(128n, x)), WW.high_comp(2n, 128n, x))))
272	
273	# 2^128 + 5 <= 2^130, 16 <= 2^128
274	def u16(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(16n, V.pos(16n, one)) == True{} : Bool}:
275	  N.le_trans(16n, C.shift(4n, one), V.pos(16n, one), L.subst(Nat, z => {Nat.is_le(16n, C.shift(4n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), WW.shift_ge(124n, C.shift(4n, one)))
276	
277	def uu(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(V.pos(16n, one), V.pos(16n, one)), C.shift(130n, one)) == True{} : Bool}:
278	  +u = V.pos(16n, one)
279	  A.le_substl(Nat.double(u), Nat.add(u, u), C.shift(130n, one), NA.double_self(u), WW.shift_ge(1n, Nat.double(u)))
280	
281	law qlt2:
282	  for +one: Nat
283	  for +h1: {one == 1n : Nat}
284	  for +h: List<&2, U32>
285	  for +hh: {ST.inv(h) == True{} : Bool}
286	  {Nat.is_lt(qq(h), 2n) == True{} : Bool}
287	
288	def qlt2(one, h1, h, hh):
289	  +u = V.pos(16n, one)
290	  +s = C.shift(130n, one)
291	  +x = Nat.add(V.ev(h), 5n)
292	  +l1 = N.lt_add_r2(V.ev(h), Nat.add(u, s), 5n, hlt(one, h1, h, hh))
293	  +e1 = A.tr(Nat.add(Nat.add(u, s), 5n), Nat.add(u, Nat.add(s, 5n)), Nat.add(s, Nat.add(u, 5n)), N.add_assoc(u, s, 5n), A.tr(Nat.add(u, Nat.add(s, 5n)), Nat.add(u, Nat.add(5n, s)), Nat.add(s, Nat.add(u, 5n)), WM.cong_r(u, Nat.add(s, 5n), Nat.add(5n, s), N.add_comm(s, 5n)), A.tr(Nat.add(u, Nat.add(5n, s)), Nat.add(Nat.add(u, 5n), s), Nat.add(s, Nat.add(u, 5n)), A.sy(Nat.add(Nat.add(u, 5n), s), Nat.add(u, Nat.add(5n, s)), N.add_assoc(u, 5n, s)), N.add_comm(Nat.add(u, 5n), s))))
294	  +l2 = N.le_add_left(Nat.add(u, 5n), s, s, N.le_trans(Nat.add(u, 5n), Nat.add(u, u), s, N.le_add_left(5n, u, u, N.le_trans(5n, 16n, u, {==}, u16(one, h1))), uu(one, h1)))
295	  +l3 = N.lt_le_trans(x, Nat.add(s, Nat.add(u, 5n)), Nat.add(s, s), A.lt_subst(x, Nat.add(Nat.add(u, s), 5n), Nat.add(s, Nat.add(u, 5n)), e1, l1), l2)
296	  +f131 = WW.fits_one(131n, one, h1, x, A.lt_subst(x, Nat.add(s, s), Nat.double(s), A.sy(Nat.double(s), Nat.add(s, s), NA.double_self(s)), l3))
297	  WW.lt_of_fits(1n, qq(h), SH.fits_high(130n, 1n, x, f131))
298	
299	def heqlen(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(Li.take(16n, h)) == V.len(Li.take(16n, gg(h))) : Nat}:
300	  A.tr(V.len(Li.take(16n, h)), 16n, V.len(Li.take(16n, gg(h))), len16(h, hh), {==})
301	
302	def qone(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == False{} : Bool}) -> {qq(h) == 1n : Nat}:
303	  N.le_antisym(qq(h), 1n, N.lt_succ_le(qq(h), 1n, qlt2(one, h1, h, hh)), N.lt_succ_le_succ(0n, qq(h), N.lt_or_eq(0n, qq(h), N.zero_le(qq(h)), N.is_eq_sym_false(qq(h), 0n, hc))))
304	
305	def which0(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == True{} : Bool}) -> {Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}:
306	  +eb = U3.injective(bb(h), 0, A.tr(V.v(bb(h)), qq(h), 0n, bval(one, h1, h, hh), N.eq_from_is_eq(qq(h), 0n, hc)))
307	  Equal.trans(List<&2, U32>, Li.freeze(h), Li.select(U32.sub(0, 0), Li.take(16n, h), Li.take(16n, gg(h))), Li.take(16n, h),
308	    Equal.cong(U32, List<&2, U32>, w => Li.select(U32.sub(0, w), Li.take(16n, h), Li.take(16n, gg(h))), bb(h), 0, eb),
309	    sel0(Li.take(16n, h), Li.take(16n, gg(h)), heqlen(h, hh)))
310	
311	def which1(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == False{} : Bool}) -> {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>}:
312	  +eb = U3.injective(bb(h), 1, A.tr(V.v(bb(h)), qq(h), 1n, bval(one, h1, h, hh), qone(one, h1, h, hh, hc)))
313	  Equal.trans(List<&2, U32>, Li.freeze(h), Li.select(U32.sub(0, 1), Li.take(16n, h), Li.take(16n, gg(h))), Li.take(16n, gg(h)),
314	    Equal.cong(U32, List<&2, U32>, w => Li.select(U32.sub(0, w), Li.take(16n, h), Li.take(16n, gg(h))), bb(h), 1, eb),
315	    sel1(Li.take(16n, h), Li.take(16n, gg(h)), heqlen(h, hh)))
316	
317	def which_c(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(qq(h), 0n) == c : Bool}) -> Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>}):
318	  match c:
319	    case True{}: Inl{which0(one, h1, h, hh, hc)}
320	    case False{}: Inr{which1(one, h1, h, hh, hc)}
321	
322	def fz_fit_o(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, o: Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>})) -> {V.fit_all(Li.freeze(h), 8n) == True{} : Bool}:
323	  match o:
324	    case Inl{e}: L.subst(List<&2, U32>, l => {V.fit_all(l, 8n) == True{} : Bool}, Li.take(16n, h), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, h), e), V.fit_take(16n, h, 8n, fith(h, hh)))
325	    case Inr{e}: L.subst(List<&2, U32>, l => {V.fit_all(l, 8n) == True{} : Bool}, Li.take(16n, gg(h)), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, gg(h)), e), V.carry_lo(16n, Li.add(h, [5]), 0))
326	
327	law freeze_fit:
328	  for +one: Nat
329	  for +h1: {one == 1n : Nat}
330	  for +h: List<&2, U32>
331	  for +hh: {ST.inv(h) == True{} : Bool}
332	  {V.fit_all(Li.freeze(h), 8n) == True{} : Bool}
333	
334	def freeze_fit(one, h1, h, hh):
335	  fz_fit_o(h, hh, which_c(one, h1, h, hh, Nat.is_eq(qq(h), 0n), {==}))
336	
337	law freeze_len:
338	  for +one: Nat
339	  for +h1: {one == 1n : Nat}
340	  for +h: List<&2, U32>
341	  for +hh: {ST.inv(h) == True{} : Bool}
342	  {Nat.is_le(V.len(Li.freeze(h)), 16n) == True{} : Bool}
343	
344	def fz_len_o(+h: List<&2, U32>, o: Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>})) -> {Nat.is_le(V.len(Li.freeze(h)), 16n) == True{} : Bool}:
345	  match o:
346	    case Inl{e}: L.subst(List<&2, U32>, l => {Nat.is_le(V.len(l), 16n) == True{} : Bool}, Li.take(16n, h), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, h), e), V.len_take(16n, h))
347	    case Inr{e}: L.subst(List<&2, U32>, l => {Nat.is_le(V.len(l), 16n) == True{} : Bool}, Li.take(16n, gg(h)), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, gg(h)), e), V.len_take(16n, gg(h)))
348	
349	def freeze_len(one, h1, h, hh):
350	  fz_len_o(h, which_c(one, h1, h, hh, Nat.is_eq(qq(h), 0n), {==}))
351	
352	# the value: the low 128 bits of h mod p
353	# lgv == low(k, d) when x = lgv + 2^k tgv with lgv < 2^k and x = d + 2^k s2,
354	# for a symbolic k (so that no check unfolds low(128, _) level by level).
355	law elg_k:
356	  for +k: Nat
357	  for +x: Nat
358	  for +lgv: Nat
359	  for +tgv: Nat
360	  for +d: Nat
361	  for +s2: Nat
362	  for +hs: {x == Nat.add(lgv, C.shift(k, tgv)) : Nat}
363	  for +hf: {C.fits(k, lgv) == True{} : Bool}
364	  for +hx: {x == Nat.add(d, C.shift(k, s2)) : Nat}
365	  {lgv == C.low(k, d) : Nat}
366	
367	def elg_k(k, x, lgv, tgv, d, s2, hs, hf, hx):
368	  A.tr(lgv, C.low(k, x), C.low(k, d),
369	    A.sy(C.low(k, x), lgv, A.tr(C.low(k, x), C.low(k, Nat.add(lgv, C.shift(k, tgv))), lgv, Equal.cong(Nat, Nat, z => C.low(k, z), x, Nat.add(lgv, C.shift(k, tgv)), hs), WW.low_u(k, lgv, tgv, hf))),
370	    A.tr(C.low(k, x), C.low(k, Nat.add(d, C.shift(k, s2))), C.low(k, d), Equal.cong(Nat, Nat, z => C.low(k, z), x, Nat.add(d, C.shift(k, s2)), hx), WW.low_add_shift(k, d, s2)))
371	
372	law fin_k:
373	  for +k: Nat
374	  for +a: Nat
375	  for +b: Nat
376	  for +c: Nat
377	  for +m: Nat
378	  for +e1: {a == b : Nat}
379	  for +e2: {b == C.low(k, c) : Nat}
380	  for +e3: {m == c : Nat}
381	  {a == C.low(k, m) : Nat}
382	
383	def fin_k(k, a, b, c, m, e1, e2, e3):
384	  A.tr(a, b, C.low(k, m), e1, A.tr(b, C.low(k, c), C.low(k, m), e2, Equal.cong(Nat, Nat, z => C.low(k, z), c, m, A.sy(m, c, e3))))
385	
386	law fe_k:
387	  for +k: Nat
388	  for +x: Nat
389	  for +lgv: Nat
390	  for +tgv: Nat
391	  for +d: Nat
392	  for +s2: Nat
393	  for +a: Nat
394	  for +m: Nat
395	  for +hs: {x == Nat.add(lgv, C.shift(k, tgv)) : Nat}
396	  for +hf: {C.fits(k, lgv) == True{} : Bool}
397	  for +hx: {x == Nat.add(d, C.shift(k, s2)) : Nat}
398	  for +e1: {a == lgv : Nat}
399	  for +e3: {m == d : Nat}
400	  {a == C.low(k, m) : Nat}
401	
402	def fe_k(k, x, lgv, tgv, d, s2, a, m, hs, hf, hx, e1, e3):
403	  fin_k(k, a, lgv, d, m, e1, elg_k(k, x, lgv, tgv, d, s2, hs, hf, hx), e3)
404	
405	def frz_c(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(qq(h), 0n) == c : Bool}) -> {V.ev(Li.freeze(h)) == C.low(128n, Nat.mod(V.ev(h), 1n+bp)) : Nat}:
406	  match c:
407	    case True{}:
408	      +pp = {1n+bp : Nat}
409	      +x = Nat.add(V.ev(h), 5n)
410	      +lh = V.ev(Li.take(16n, h))
411	      +vt = V.v(Li.hd0(Li.skip(16n, h)))
412	      +ef = Equal.cong(List<&2, U32>, Nat, l => V.ev(l), Li.freeze(h), Li.take(16n, h), which0(one, h1, h, hh, hc))
413	      +lx = A.lt_subst(x, C.shift(130n, one), Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), C.shift(130n, one), h5), WW.lt_one(130n, one, h1, x, hc))
414	      +lp = A.btrue(Nat.is_lt(V.ev(h), pp), Nat.is_lt(x, Nat.add(pp, 5n)), Equal.sym(Bool, Nat.is_lt(x, Nat.add(pp, 5n)), Nat.is_lt(V.ev(h), pp), WW.lt_cancel_r(V.ev(h), pp, 5n)), lx)
415	      +em = NR.mod_of(0n, bp, V.ev(h), lp)
416	      +flh = WW.fits_one(128n, one, h1, lh, A.lt_subst(lh, V.pos(V.len(Li.take(16n, h)), one), V.pos(16n, one), Equal.cong(Nat, Nat, z => V.pos(z, one), V.len(Li.take(16n, h)), 16n, len16(h, hh)), V.ev_lt(Li.take(16n, h), one, h1, V.fit_take(16n, h, 8n, fith(h, hh)))))
417	      +el = A.tr(C.low(128n, V.ev(h)), C.low(128n, Nat.add(lh, V.pos(16n, vt))), lh, Equal.cong(Nat, Nat, z => C.low(128n, z), V.ev(h), Nat.add(lh, V.pos(16n, vt)), hsplit(h, hh)), WW.low_u(128n, lh, vt, flh))
418	      A.tr(V.ev(Li.freeze(h)), lh, C.low(128n, Nat.mod(V.ev(h), pp)), ef,
419	        A.sy(C.low(128n, Nat.mod(V.ev(h), pp)), lh, A.tr(C.low(128n, Nat.mod(V.ev(h), pp)), C.low(128n, V.ev(h)), lh, Equal.cong(Nat, Nat, z => C.low(128n, z), Nat.mod(V.ev(h), pp), V.ev(h), em), el)))
420	    case False{}:
421	      +pp = {1n+bp : Nat}
422	      +s = C.shift(130n, one)
423	      +u = V.pos(16n, one)
424	      +x = Nat.add(V.ev(h), 5n)
425	      +d = C.low(130n, x)
426	      +q = qq(h)
427	      +ef = Equal.cong(List<&2, U32>, Nat, l => V.ev(l), Li.freeze(h), Li.take(16n, gg(h)), which1(one, h1, h, hh, hc))
428	      +eq1 = qone(one, h1, h, hh, hc)
429	      +es = A.tr(C.shift(130n, q), Nat.mul(q, s), s, WW.shift_mul_one(130n, one, h1, q), A.tr(Nat.mul(q, s), Nat.mul(1n, s), s, Equal.cong(Nat, Nat, z => Nat.mul(z, s), q, 1n, eq1), AR.one_mul(s)))
430	      +ex = A.tr(x, Nat.add(d, C.shift(130n, q)), Nat.add(d, s), WW.low_high(130n, x), WM.cong_r(d, C.shift(130n, q), s, es))
431	      +ex2 = A.tr(Nat.add(V.ev(h), 5n), Nat.add(d, Nat.add(pp, 5n)), Nat.add(Nat.add(d, pp), 5n), A.tr(x, Nat.add(d, s), Nat.add(d, Nat.add(pp, 5n)), ex, WM.cong_r(d, s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5))), A.sy(Nat.add(Nat.add(d, pp), 5n), Nat.add(d, Nat.add(pp, 5n)), N.add_assoc(d, pp, 5n)))
432	      +eh = UA.add_cancel_r(V.ev(h), Nat.add(d, pp), 5n, ex2)
433	      # d < 2^128 + 5 <= p
434	      +l1 = N.lt_add_r2(V.ev(h), Nat.add(u, s), 5n, hlt(one, h1, h, hh))
435	      +e1 = A.tr(Nat.add(Nat.add(u, s), 5n), Nat.add(u, Nat.add(s, 5n)), Nat.add(Nat.add(u, 5n), s), N.add_assoc(u, s, 5n), A.tr(Nat.add(u, Nat.add(s, 5n)), Nat.add(u, Nat.add(5n, s)), Nat.add(Nat.add(u, 5n), s), WM.cong_r(u, Nat.add(s, 5n), Nat.add(5n, s), N.add_comm(s, 5n)), A.sy(Nat.add(Nat.add(u, 5n), s), Nat.add(u, Nat.add(5n, s)), N.add_assoc(u, 5n, s))))
436	      +l2 = A.lt_substl(x, Nat.add(d, s), Nat.add(Nat.add(u, 5n), s), ex, A.lt_subst(x, Nat.add(Nat.add(u, s), 5n), Nat.add(Nat.add(u, 5n), s), e1, l1))
437	      +ld = A.btrue(Nat.is_lt(d, Nat.add(u, 5n)), Nat.is_lt(Nat.add(d, s), Nat.add(Nat.add(u, 5n), s)), Equal.sym(Bool, Nat.is_lt(Nat.add(d, s), Nat.add(Nat.add(u, 5n), s)), Nat.is_lt(d, Nat.add(u, 5n)), WW.lt_cancel_r(d, Nat.add(u, 5n), s)), l2)
438	      +l9 = N.lt_le_trans(Nat.add(u, 9n), Nat.add(u, u), s, N.lt_add_left(9n, u, u, N.lt_le_trans(9n, 16n, u, {==}, u16(one, h1))), uu(one, h1))
439	      +l9b = A.lt_substl(Nat.add(u, 9n), Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n), A.sy(Nat.add(Nat.add(u, 4n), 5n), Nat.add(u, 9n), N.add_assoc(u, 4n, 5n)), A.lt_subst(Nat.add(u, 9n), s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5), l9))
440	      +l4 = A.btrue(Nat.is_lt(Nat.add(u, 4n), pp), Nat.is_lt(Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n)), Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n)), Nat.is_lt(Nat.add(u, 4n), pp), WW.lt_cancel_r(Nat.add(u, 4n), pp, 5n)), l9b)
441	      +l5 = A.le_substl(1n+Nat.add(u, 4n), Nat.add(u, 5n), pp, A.sy(Nat.add(u, 5n), 1n+Nat.add(u, 4n), N.add_succ(u, 4n)), N.lt_succ_le_succ(Nat.add(u, 4n), pp, l4))
442	      +ldp = N.lt_le_trans(d, Nat.add(u, 5n), pp, ld, l5)
443	      +em = A.tr(Nat.mod(V.ev(h), pp), Nat.mod(Nat.add(Nat.mul(1n, pp), d), pp), d,
444	        Equal.cong(Nat, Nat, z => Nat.mod(z, pp), V.ev(h), Nat.add(Nat.mul(1n, pp), d), A.tr(V.ev(h), Nat.add(d, pp), Nat.add(Nat.mul(1n, pp), d), eh, A.tr(Nat.add(d, pp), Nat.add(pp, d), Nat.add(Nat.mul(1n, pp), d), N.add_comm(d, pp), WM.cong_l(pp, Nat.mul(1n, pp), d, A.sy(Nat.mul(1n, pp), pp, AR.one_mul(pp)))))),
445	        NR.mod_of(1n, bp, d, ldp))
446	      fe_k(128n, x, lg(h), tg(h), d, C.shift(2n, one), V.ev(Li.freeze(h)), Nat.mod(V.ev(h), pp), gsplit(one, h1, h, hh), flg(one, h1, h), ex, ef, em)
447	
448	law freeze_ev:
449	  for +one: Nat
450	  for +h1: {one == 1n : Nat}
451	  for +bp: Nat
452	  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
453	  for +h: List<&2, U32>
454	  for +hh: {ST.inv(h) == True{} : Bool}
455	  {V.ev(Li.freeze(h)) == C.low(128n, Nat.mod(V.ev(h), 1n+bp)) : Nat}
456	
457	def freeze_ev(one, h1, bp, h5, h, hh):
458	  frz_c(one, h1, bp, h5, h, hh, Nat.is_eq(qq(h), 0n), {==})
459	
460	# ---- the tag bytes ----
461	
462	law bytes_le:
463	  for +n: Nat
464	  for +ds: List<&2, U32>
465	  for +u: U32
466	  for +k: Nat
467	  for +j: Nat
468	  for +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}
469	  for +hd: {V.fit_all(ds, Nat.add(8n, j)) == True{} : Bool}
470	  for +hu: {C.fits(Nat.add(8n, j), V.v(u)) == True{} : Bool}
471	  {Li.bytes(n, ds, u) == R.le_bytes(n, Nat.add(Nat.add(V.v(u), V.ev(ds)), V.pos(n, k))) : List<&2, U32>}
472	
473	def bytes_le(n, ds, u, k, j, hj, hd, hu):
474	  match n:
475	    case 0n: {==}
476	    case 1n+m:
477	      +h = Li.hd0(ds)
478	      +s = U32.add(u, h)
479	      +vs = V.v(s)
480	      +u2 = U32.shrn(s, 8n)
481	      +et = V.ev(Li.tl(ds))
482	      +pk = V.pos(m, k)
483	      +y = Nat.add(Nat.add(V.v(u), V.ev(ds)), C.shift(8n, pk))
484	      +y2 = Nat.add(vs, C.shift(8n, Nat.add(et, pk)))
485	      +es = V.step_ev(ds, u, j, hj, hd, hu)
486	      +ey = A.tr(y, Nat.add(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk)), y2,
487	        WM.cong_l(Nat.add(V.v(u), V.ev(ds)), Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk), WM.cong_r(V.v(u), V.ev(ds), Nat.add(V.v(h), C.shift(8n, et)), V.hd_tl_ev(ds))),
488	        A.tr(Nat.add(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk)), Nat.add(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk)), y2,
489	          WM.cong_l(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk), A.sy(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), N.add_assoc(V.v(u), V.v(h), C.shift(8n, et)))),
490	          A.tr(Nat.add(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk)), Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, Nat.add(et, pk))), y2,
491	            V.sh3(Nat.add(V.v(u), V.v(h)), et, pk),
492	            WM.cong_l(Nat.add(V.v(u), V.v(h)), vs, C.shift(8n, Nat.add(et, pk)), A.sy(vs, Nat.add(V.v(u), V.v(h)), es)))))
493	      +elo = WW.low_add_shift(8n, vs, Nat.add(et, pk))
494	      +ehi = A.tr(C.high(8n, y2), Nat.add(C.high(8n, vs), Nat.add(et, pk)), Nat.add(Nat.add(V.v(u2), et), pk), WW.high_add_shift(8n, vs, Nat.add(et, pk)),
495	        A.tr(Nat.add(C.high(8n, vs), Nat.add(et, pk)), Nat.add(V.v(u2), Nat.add(et, pk)), Nat.add(Nat.add(V.v(u2), et), pk), WM.cong_l(C.high(8n, vs), V.v(u2), Nat.add(et, pk), A.sy(V.v(u2), C.high(8n, vs), SHN.shrn_high(s, 8n))), A.sy(Nat.add(Nat.add(V.v(u2), et), pk), Nat.add(V.v(u2), Nat.add(et, pk)), N.add_assoc(V.v(u2), et, pk))))
496	      +lo8 = C.low(8n, vs)
497	      +eb = U3.injective(U32.and(s, 255), U32.from_nat(lo8), A.tr(V.v(U32.and(s, 255)), lo8, V.v(U32.from_nat(lo8)), FB.andm(s, 8n, 255, {==}), A.sy(V.v(U32.from_nat(lo8)), lo8, U3.to_nat_from_nat(lo8, 8n, {==}, WW.low_lt(8n, vs)))))
498	      +ih = bytes_le(m, Li.tl(ds), u2, k, j, hj, V.tl_fit(ds, Nat.add(8n, j), hd), V.next_fit(ds, u, j, hj, hd, hu))
499	      Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), R.le_bytes(1n+m, y2), R.le_bytes(1n+m, y),
500	        Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), R.le_bytes(1n+m, y2),
501	          Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)),
502	            Equal.cong(U32, List<&2, U32>, z => z <> Li.bytes(m, Li.tl(ds), u2), U32.and(s, 255), U32.from_nat(lo8), eb),
503	            Equal.cong(List<&2, U32>, List<&2, U32>, z => U32.from_nat(lo8) <> z, Li.bytes(m, Li.tl(ds), u2), R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), ih)),
504	          Equal.trans(List<&2, U32>, U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), U32.from_nat(C.low(8n, y2)) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), R.le_bytes(1n+m, y2),
505	            Equal.cong(Nat, List<&2, U32>, z => U32.from_nat(z) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), lo8, C.low(8n, y2), A.sy(C.low(8n, y2), lo8, elo)),
506	            Equal.cong(Nat, List<&2, U32>, z => U32.from_nat(C.low(8n, y2)) <> R.le_bytes(m, z), Nat.add(Nat.add(V.v(u2), et), pk), C.high(8n, y2), A.sy(C.high(8n, y2), Nat.add(Nat.add(V.v(u2), et), pk), ehi)))),
507	        Equal.cong(Nat, List<&2, U32>, z => R.le_bytes(1n+m, z), y2, y, A.sy(y, y2, ey)))
508	
509	# bytes_le with the target value rewritten, for any n (so that the
510	# rewrite does not unfold le_bytes n levels on both sides).
511	law bytes_le_to:
512	  for +n: Nat
513	  for +ds: List<&2, U32>
514	  for +k: Nat
515	  for +t: Nat
516	  for +hb: {Li.bytes(n, ds, 0) == R.le_bytes(n, Nat.add(Nat.add(V.v(0), V.ev(ds)), V.pos(n, k))) : List<&2, U32>}
517	  for +ht: {Nat.add(V.ev(ds), V.pos(n, k)) == t : Nat}
518	  {Li.bytes(n, ds, 0) == R.le_bytes(n, t) : List<&2, U32>}
519	
520	def bytes_le_to(n, ds, k, t, hb, ht):
521	  Equal.trans(List<&2, U32>, Li.bytes(n, ds, 0), R.le_bytes(n, Nat.add(V.ev(ds), V.pos(n, k))), R.le_bytes(n, t), hb,
522	    Equal.cong(Nat, List<&2, U32>, z => R.le_bytes(n, z), Nat.add(V.ev(ds), V.pos(n, k)), t, ht))
523	
524	# the tag: (h mod p + s) mod 2^128 as 16 bytes
525	law tag_eq:
526	  for +one: Nat
527	  for +h1: {one == 1n : Nat}
528	  for +bp: Nat
529	  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
530	  for +h: List<&2, U32>
531	  for +hh: {ST.inv(h) == True{} : Bool}
532	  for +s: List<&2, U32>
533	  for +hs: {V.fit_all(s, 8n) == True{} : Bool}
534	  {Li.bytes(16n, Li.add(Li.freeze(h), s), 0) == R.le_bytes(16n, Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s))) : List<&2, U32>}
535	
536	def tag_eq(one, h1, bp, h5, h, hh, s, hs):
537	  +s8 = C.shift(8n, one)
538	  +s9 = C.shift(9n, one)
539	  +fz = Li.freeze(h)
540	  +a = Nat.mod(V.ev(h), 1n+bp)
541	  +lo = C.low(128n, a)
542	  +kk = C.high(128n, a)
543	  +ds = Li.add(fz, s)
544	  +hf = freeze_fit(one, h1, h, hh)
545	  +hf1 = ST.s8fit(one, h1)
546	  +ed = V.add_ev(fz, s, s8, s8, V.fit_le(fz, 8n, one, h1, hf), V.fit_le(s, 8n, one, h1, hs), hf1)
547	  +l10 = A.lt_substl(s9, Nat.add(s8, s8), Nat.double(s9), NA.double_self(s8), lt_dbl(s9, A.one_le_shift(9n, one, h1)))
548	  +hd = V.le_fit(ds, Nat.add(s8, s8), 10n, one, h1, l10, V.add_le(fz, s, s8, s8, V.fit_le(fz, 8n, one, h1, hf), V.fit_le(s, 8n, one, h1, hs), hf1))
549	  +bl = bytes_le(16n, ds, 0, kk, 2n, {==}, hd, {==})
550	  # ev ds + 2^128 kk == a + ev s
551	  +e1 = A.tr(Nat.add(V.ev(ds), V.pos(16n, kk)), Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(a, V.ev(s)),
552	    WM.cong_l(V.ev(ds), Nat.add(lo, V.ev(s)), V.pos(16n, kk), A.tr(V.ev(ds), Nat.add(V.ev(fz), V.ev(s)), Nat.add(lo, V.ev(s)), ed, WM.cong_l(V.ev(fz), lo, V.ev(s), freeze_ev(one, h1, bp, h5, h, hh)))),
553	    A.tr(Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(Nat.add(lo, V.pos(16n, kk)), V.ev(s)), Nat.add(a, V.ev(s)),
554	      A.tr(Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(lo, Nat.add(V.ev(s), V.pos(16n, kk))), Nat.add(Nat.add(lo, V.pos(16n, kk)), V.ev(s)), N.add_assoc(lo, V.ev(s), V.pos(16n, kk)), ST.rot(lo, V.ev(s), V.pos(16n, kk))),
555	      WM.cong_l(Nat.add(lo, V.pos(16n, kk)), a, V.ev(s), A.sy(a, Nat.add(lo, V.pos(16n, kk)), WW.low_high(128n, a)))))
556	  bytes_le_to(16n, ds, kk, Nat.add(a, V.ev(s)), bl, e1)
557	
558	# tag_eq through Li.fin (the implementation's entry point).
559	law fin_eq:
560	  for +one: Nat
561	  for +h1: {one == 1n : Nat}
562	  for +bp: Nat
563	  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
564	  for +h: List<&2, U32>
565	  for +hh: {ST.inv(h) == True{} : Bool}
566	  for +s: List<&2, U32>
567	  for +hs: {V.fit_all(s, 8n) == True{} : Bool}
568	  {Li.fin(h, s) == R.le_bytes(16n, Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s))) : List<&2, U32>}
569	
570	def fin_eq(one, h1, bp, h5, h, hh, s, hs):
571	  match s:
572	    case Nil{}: tag_eq(one, h1, bp, h5, h, hh, Nil{}, hs)
573	    case y <> ys: tag_eq(one, h1, bp, h5, h, hh, y <> ys, hs)