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 ../../../src/crypto/poly1305/poly1305.bend as P
6	import ../../lib/nat.bend as N
7	import ../../lib/logic.bend as L
8	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
9	import ../../math/typed/width.bend as WW
10	import ../../math/typed/w64mul.bend as WM
11	import ../../math/typed/w64sh.bend as SH
12	import ../../math/typed/f64bits.bend as FB
13	import ../../math/natural/arith.bend as NR
14	import ./arith.bend as A
15	import ./value.bend as V
16	import ./step.bend as ST
17	import ./modp.bend as MP
18	import ./final.bend as F
19	
20	# The implementation's Poly1305 tag is the RFC 8439 tag (spec/crypto/
21	# poly1305.bend) for every key and message: the limb accumulator stays
22	# congruent to the spec's accumulator mod p block by block, and the final
23	# freeze and byte serialization give the spec's num_to_16_le_bytes.
24	# mac_correct and mac_length are the clauses of laws.bend (proof.bend fills
25	# the laws with them; other proofs may import this file).
26	
27	# ---- bytes to limbs ----
28	
29	law mask_ev:
30	  for +xs: List<&2, U32>
31	  {V.ev(P.mask(xs)) == R.le_num(xs) : Nat}
32	
33	def mask_ev(xs):
34	  match xs:
35	    case Nil{}: {==}
36	    case x <> t: WM.cong_r(U32.to_nat(U32.and(x, 255)), C.shift(8n, V.ev(P.mask(t))), C.shift(8n, R.le_num(t)), A.csh(8n, V.ev(P.mask(t)), R.le_num(t), mask_ev(t)))
37	
38	law mask_fit:
39	  for +xs: List<&2, U32>
40	  {V.fit_all(P.mask(xs), 8n) == True{} : Bool}
41	
42	def mask_fit(xs):
43	  match xs:
44	    case Nil{}: {==}
45	    case x <> t:
46	      L.and_intro(C.fits(8n, V.v(U32.and(x, 255))), V.fit_all(P.mask(t), 8n),
47	        A.fits_subst(8n, C.low(8n, V.v(x)), V.v(U32.and(x, 255)), A.sy(V.v(U32.and(x, 255)), C.low(8n, V.v(x)), FB.andm(x, 8n, 255, {==})), WW.low_fits(8n, V.v(x))),
48	        mask_fit(t))
49	
50	law mask_len:
51	  for +xs: List<&2, U32>
52	  {V.len(P.mask(xs)) == V.len(xs) : Nat}
53	
54	def mask_len(xs):
55	  match xs:
56	    case Nil{}: {==}
57	    case x <> t: Equal.cong(Nat, Nat, z => 1n+z, V.len(P.mask(t)), V.len(t), mask_len(t))
58	
59	law take_prefix:
60	  for +n: Nat
61	  for +xs: List<&2, U32>
62	  {Li.take(n, xs) == R.prefix(n, xs) : List<&2, U32>}
63	
64	def take_prefix(n, xs):
65	  match n xs:
66	    case 0n _: {==}
67	    case 1n+k Nil{}: {==}
68	    case 1n+k x <> t: Equal.cong(List<&2, U32>, List<&2, U32>, z => x <> z, Li.take(k, t), R.prefix(k, t), take_prefix(k, t))
69	
70	law skip_suffix:
71	  for +n: Nat
72	  for +xs: List<&2, U32>
73	  {Li.skip(n, xs) == R.suffix(n, xs) : List<&2, U32>}
74	
75	def skip_suffix(n, xs):
76	  match n xs:
77	    case 0n _: {==}
78	    case 1n+k Nil{}: {==}
79	    case 1n+k x <> t: skip_suffix(k, t)
80	
81	law cmask:
82	  for +i: Nat
83	  {P.clamp_mask(i) == R.clamp_mask(i) : U32}
84	
85	def cmask(i):
86	  match i:
87	    case 0n: {==}
88	    case 1n: {==}
89	    case 2n: {==}
90	    case 3n: {==}
91	    case 4n: {==}
92	    case 5n: {==}
93	    case 6n: {==}
94	    case 7n: {==}
95	    case 8n: {==}
96	    case 9n: {==}
97	    case 10n: {==}
98	    case 11n: {==}
99	    case 12n: {==}
100	    case 13n: {==}
101	    case 14n: {==}
102	    case 15n: {==}
103	    case 16n+p: {==}
104	
105	law clamp_eq:
106	  for +xs: List<&2, U32>
107	  for +i: Nat
108	  {P.clamp(xs, i) == R.clamp_from(xs, i) : List<&2, U32>}
109	
110	def clamp_eq(xs, i):
111	  match xs:
112	    case Nil{}: {==}
113	    case x <> t:
114	      Equal.trans(List<&2, U32>, U32.and(x, P.clamp_mask(i)) <> P.clamp(t, 1n+i), U32.and(x, R.clamp_mask(i)) <> P.clamp(t, 1n+i), U32.and(x, R.clamp_mask(i)) <> R.clamp_from(t, 1n+i),
115	        Equal.cong(U32, List<&2, U32>, z => U32.and(x, z) <> P.clamp(t, 1n+i), P.clamp_mask(i), R.clamp_mask(i), cmask(i)),
116	        Equal.cong(List<&2, U32>, List<&2, U32>, z => U32.and(x, R.clamp_mask(i)) <> z, P.clamp(t, 1n+i), R.clamp_from(t, 1n+i), clamp_eq(t, 1n+i)))
117	
118	law clamp_len:
119	  for +xs: List<&2, U32>
120	  for +i: Nat
121	  {V.len(P.clamp(xs, i)) == V.len(xs) : Nat}
122	
123	def clamp_len(xs, i):
124	  match xs:
125	    case Nil{}: {==}
126	    case x <> t: Equal.cong(Nat, Nat, z => 1n+z, V.len(P.clamp(t, 1n+i)), V.len(t), clamp_len(t, 1n+i))
127	
128	law fit_fit:
129	  for +n: Nat
130	  for +xs: List<&2, U32>
131	  for +h: {V.fit_all(xs, 8n) == True{} : Bool}
132	  {V.fit_all(Li.fit(n, xs), 8n) == True{} : Bool}
133	
134	def fit_fit(n, xs, h):
135	  match n:
136	    case 0n: {==}
137	    case 1n+k: L.and_intro(C.fits(8n, V.v(Li.hd0(xs))), V.fit_all(Li.fit(k, Li.tl(xs)), 8n), V.hd0_fit(xs, 8n, h), fit_fit(k, Li.tl(xs), V.tl_fit(xs, 8n, h)))
138	
139	law take_all:
140	  for +n: Nat
141	  for +xs: List<&2, U32>
142	  for +h: {Nat.is_le(V.len(xs), n) == True{} : Bool}
143	  {Li.take(n, xs) == xs : List<&2, U32>}
144	
145	def take_all(n, xs, h):
146	  match n xs:
147	    case 0n Nil{}: {==}
148	    case 0n x <> t: Empty.absurd({Li.take(0n, x <> t) == x <> t : List<&2, U32>}, L.false_true(h))
149	    case 1n+k Nil{}: {==}
150	    case 1n+k x <> t: Equal.cong(List<&2, U32>, List<&2, U32>, z => x <> z, Li.take(k, t), t, take_all(k, t, h))
151	
152	# the key's r and s limbs
153	law r_ev:
154	  for +key: List<&2, U32>
155	  {V.ev(P.r_key(key)) == R.le_num(R.clamp(R.prefix(16n, key))) : Nat}
156	
157	def r_ev(key):
158	  +t = Li.take(16n, key)
159	  +m = P.mask(P.clamp(t, 0n))
160	  +hl = A.le_substl(V.len(t), V.len(m), 16n, A.sy(V.len(m), V.len(t), A.tr(V.len(m), V.len(P.clamp(t, 0n)), V.len(t), mask_len(P.clamp(t, 0n)), clamp_len(t, 0n))), V.len_take(16n, key))
161	  A.tr(V.ev(P.r_key(key)), V.ev(Li.take(16n, m)), R.le_num(R.clamp(R.prefix(16n, key))), V.fit_ev(16n, m),
162	    A.tr(V.ev(Li.take(16n, m)), V.ev(m), R.le_num(R.clamp(R.prefix(16n, key))), Equal.cong(List<&2, U32>, Nat, l => V.ev(l), Li.take(16n, m), m, take_all(16n, m, hl)),
163	      A.tr(V.ev(m), R.le_num(P.clamp(t, 0n)), R.le_num(R.clamp(R.prefix(16n, key))), mask_ev(P.clamp(t, 0n)),
164	        Equal.cong(List<&2, U32>, Nat, l => R.le_num(l), P.clamp(t, 0n), R.clamp(R.prefix(16n, key)),
165	          Equal.trans(List<&2, U32>, P.clamp(t, 0n), R.clamp_from(t, 0n), R.clamp(R.prefix(16n, key)), clamp_eq(t, 0n), Equal.cong(List<&2, U32>, List<&2, U32>, l => R.clamp_from(l, 0n), t, R.prefix(16n, key), take_prefix(16n, key)))))))
166	
167	law s_ev:
168	  for +key: List<&2, U32>
169	  {V.ev(P.s_key(key)) == R.le_num(R.prefix(16n, R.suffix(16n, key))) : Nat}
170	
171	def s_ev(key):
172	  A.tr(V.ev(P.s_key(key)), R.le_num(Li.take(16n, Li.skip(16n, key))), R.le_num(R.prefix(16n, R.suffix(16n, key))), mask_ev(Li.take(16n, Li.skip(16n, key))),
173	    Equal.cong(List<&2, U32>, Nat, l => R.le_num(l), Li.take(16n, Li.skip(16n, key)), R.prefix(16n, R.suffix(16n, key)),
174	      Equal.trans(List<&2, U32>, Li.take(16n, Li.skip(16n, key)), R.prefix(16n, Li.skip(16n, key)), R.prefix(16n, R.suffix(16n, key)), take_prefix(16n, Li.skip(16n, key)),
175	        Equal.cong(List<&2, U32>, List<&2, U32>, l => R.prefix(16n, l), Li.skip(16n, key), R.suffix(16n, key), skip_suffix(16n, key)))))
176	
177	
178	law app1:
179	  for +t: List<&2, U32>
180	  {V.len(List.append(&2, U32, t, [1])) == Nat.add(V.len(t), 1n) : Nat}
181	
182	def app1(t):
183	  match t:
184	    case Nil{}: {==}
185	    case x <> u: Equal.cong(Nat, Nat, z => 1n+z, V.len(List.append(&2, U32, u, [1])), Nat.add(V.len(u), 1n), app1(u))
186	
187	# p == 1 + bp
188	law pp_eq:
189	  for +one: Nat
190	  for +h1: {one == 1n : Nat}
191	  for +bp: Nat
192	  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
193	  {Nat.sub(C.shift(130n, one), 5n) == 1n+bp : Nat}
194	
195	def pp_eq(one, h1, bp, h5):
196	  A.tr(Nat.sub(C.shift(130n, one), 5n), Nat.sub(Nat.add(1n+bp, 5n), 5n), 1n+bp, Equal.cong(Nat, Nat, z => Nat.sub(z, 5n), C.shift(130n, one), Nat.add(1n+bp, 5n), A.sy(Nat.add(1n+bp, 5n), C.shift(130n, one), h5)),
197	    A.tr(Nat.sub(Nat.add(1n+bp, 5n), 5n), Nat.sub(Nat.add(5n, 1n+bp), 5n), 1n+bp, Equal.cong(Nat, Nat, z => Nat.sub(z, 5n), Nat.add(1n+bp, 5n), Nat.add(5n, 1n+bp), N.add_comm(1n+bp, 5n)), N.add_sub_cancel(5n, 1n+bp)))
198	
199	# ---- the accumulator ----
200	
201	def load_len(+b: List<&2, U32>) -> {Nat.is_le(V.len(P.load(Li.take(16n, b))), 17n) == True{} : Bool}:
202	  +t = Li.take(16n, b)
203	  A.le_substl(V.len(List.append(&2, U32, t, [1])), V.len(P.load(t)), 17n, A.sy(V.len(P.load(t)), V.len(List.append(&2, U32, t, [1])), mask_len(List.append(&2, U32, t, [1]))),
204	    A.le_substl(Nat.add(V.len(t), 1n), V.len(List.append(&2, U32, t, [1])), 17n, A.sy(V.len(List.append(&2, U32, t, [1])), Nat.add(V.len(t), 1n), app1(t)),
205	      A.le_substl(1n+V.len(t), Nat.add(V.len(t), 1n), 17n, A.sy(Nat.add(V.len(t), 1n), 1n+V.len(t), A.tr(Nat.add(V.len(t), 1n), 1n+Nat.add(V.len(t), 0n), 1n+V.len(t), N.add_succ(V.len(t), 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(V.len(t), 0n), V.len(t), N.add_zero(V.len(t))))), V.len_take(16n, b))))
206	
207	law absorb_ok:
208	  for +one: Nat
209	  for +h1: {one == 1n : Nat}
210	  for +bp: Nat
211	  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
212	  for +fuel: Nat
213	  for +msg: List<&2, U32>
214	  for +r: List<&2, U32>
215	  for +h: List<&2, U32>
216	  for +a: Nat
217	  for +hrl: {V.len(r) == 16n : Nat}
218	  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
219	  for +hh: {ST.inv(h) == True{} : Bool}
220	  for +ha: {Nat.mod(V.ev(h), 1n+bp) == a : Nat}
221	  {Nat.mod(V.ev(P.absorb(fuel, msg, r, h)), 1n+bp) == R.absorb(R.blocks(fuel, msg), V.ev(r), a) : Nat}
222	
223	law absorb_inv:
224	  for +one: Nat
225	  for +h1: {one == 1n : Nat}
226	  for +fuel: Nat
227	  for +msg: List<&2, U32>
228	  for +r: List<&2, U32>
229	  for +h: List<&2, U32>
230	  for +hrl: {V.len(r) == 16n : Nat}
231	  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
232	  for +hh: {ST.inv(h) == True{} : Bool}
233	  {ST.inv(P.absorb(fuel, msg, r, h)) == True{} : Bool}
234	
235	def absorb_inv(one, h1, fuel, msg, r, h, hrl, hrf, hh):
236	  match fuel msg:
237	    case 0n _: hh
238	    case 1n+k Nil{}: hh
239	    case 1n+k b <> Nil{}:
240	      +m = {[b] : List<&2, U32>}
241	      +c = P.load(Li.take(16n, m))
242	      absorb_inv(one, h1, k, Li.skip(16n, m), r, Li.block(r, h, c), hrl, hrf, ST.block_inv(one, h1, r, h, c, hh, mask_fit(List.append(&2, U32, Li.take(16n, m), [1])), hrl, hrf))
243	    case 1n+k b <> d <> rest:
244	      +m = {b <> d <> rest : List<&2, U32>}
245	      +c = P.load(Li.take(16n, m))
246	      absorb_inv(one, h1, k, Li.skip(16n, m), r, Li.block(r, h, c), hrl, hrf, ST.block_inv(one, h1, r, h, c, hh, mask_fit(List.append(&2, U32, Li.take(16n, m), [1])), hrl, hrf))
247	
248	# one block: (r (a + n)) mod p == ev(block) mod p
249	def step_mod(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}, +r: List<&2, U32>, +h: List<&2, U32>, +m: List<&2, U32>, +a: Nat, +hrl: {V.len(r) == 16n : Nat}, +hrf: {V.fit_all(r, 8n) == True{} : Bool}, +hh: {ST.inv(h) == True{} : Bool}, +ha: {Nat.mod(V.ev(h), 1n+bp) == a : Nat}) -> {R.modp(Nat.mul(V.ev(r), Nat.add(a, R.le_num(List.append(&2, U32, R.prefix(16n, m), [1]))))) == Nat.mod(V.ev(Li.block(r, h, P.load(Li.take(16n, m)))), 1n+bp) : Nat}:
250	  +pp = {1n+bp : Nat}
251	  +c = P.load(Li.take(16n, m))
252	  +n = R.le_num(List.append(&2, U32, R.prefix(16n, m), [1]))
253	  +er = V.ev(r)
254	  +eh = V.ev(h)
255	  +ec = A.tr(V.ev(c), R.le_num(List.append(&2, U32, Li.take(16n, m), [1])), n, mask_ev(List.append(&2, U32, Li.take(16n, m), [1])),
256	    Equal.cong(List<&2, U32>, Nat, l => R.le_num(List.append(&2, U32, l, [1])), Li.take(16n, m), R.prefix(16n, m), take_prefix(16n, m)))
257	  +eb = ST.block_ev(one, h1, r, h, c, hh, load_len(m), mask_fit(List.append(&2, U32, Li.take(16n, m), [1])), hrl, hrf)
258	  +pm = ST.pm(one)
259	  +ep = A.tr(pm, Nat.sub(C.shift(130n, one), 5n), pp, {==}, pp_eq(one, h1, bp, h5))
260	  +bv = V.ev(Li.block(r, h, c))
261	  +k = ST.bk(r, h, c)
262	  +e1 = A.tr(Nat.mul(Nat.add(eh, V.ev(c)), er), Nat.add(bv, Nat.mul(k, pm)), Nat.add(Nat.mul(k, pp), bv), eb,
263	    A.tr(Nat.add(bv, Nat.mul(k, pm)), Nat.add(Nat.mul(k, pm), bv), Nat.add(Nat.mul(k, pp), bv), N.add_comm(bv, Nat.mul(k, pm)), WM.cong_l(Nat.mul(k, pm), Nat.mul(k, pp), bv, Equal.cong(Nat, Nat, z => Nat.mul(k, z), pm, pp, ep))))
264	  +e2 = A.tr(Nat.mod(Nat.mul(Nat.add(eh, V.ev(c)), er), pp), Nat.mod(Nat.add(Nat.mul(k, pp), bv), pp), Nat.mod(bv, pp), Equal.cong(Nat, Nat, z => Nat.mod(z, pp), Nat.mul(Nat.add(eh, V.ev(c)), er), Nat.add(Nat.mul(k, pp), bv), e1), NR.absorb(bp, k, bv))
265	  # mod(r (a + n)) == mod((eh + n) r)
266	  +e3 = A.tr(Nat.mod(Nat.mul(er, Nat.add(a, n)), pp), Nat.mod(Nat.mul(er, Nat.mod(Nat.add(a, n), pp)), pp), Nat.mod(Nat.mul(Nat.add(eh, V.ev(c)), er), pp),
267	    A.sy(Nat.mod(Nat.mul(er, Nat.mod(Nat.add(a, n), pp)), pp), Nat.mod(Nat.mul(er, Nat.add(a, n)), pp), NR.mod_mul_r(bp, er, Nat.add(a, n))),
268	    A.tr(Nat.mod(Nat.mul(er, Nat.mod(Nat.add(a, n), pp)), pp), Nat.mod(Nat.mul(er, Nat.mod(Nat.add(eh, n), pp)), pp), Nat.mod(Nat.mul(Nat.add(eh, V.ev(c)), er), pp),
269	      Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(er, z), pp), Nat.mod(Nat.add(a, n), pp), Nat.mod(Nat.add(eh, n), pp),
270	        A.tr(Nat.mod(Nat.add(a, n), pp), Nat.mod(Nat.add(Nat.mod(eh, pp), n), pp), Nat.mod(Nat.add(eh, n), pp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(z, n), pp), a, Nat.mod(eh, pp), A.sy(Nat.mod(eh, pp), a, ha)), NR.mod_add_l(bp, eh, n))),
271	      A.tr(Nat.mod(Nat.mul(er, Nat.mod(Nat.add(eh, n), pp)), pp), Nat.mod(Nat.mul(er, Nat.add(eh, n)), pp), Nat.mod(Nat.mul(Nat.add(eh, V.ev(c)), er), pp), NR.mod_mul_r(bp, er, Nat.add(eh, n)),
272	        Equal.cong(Nat, Nat, z => Nat.mod(z, pp), Nat.mul(er, Nat.add(eh, n)), Nat.mul(Nat.add(eh, V.ev(c)), er),
273	          A.tr(Nat.mul(er, Nat.add(eh, n)), Nat.mul(Nat.add(eh, n), er), Nat.mul(Nat.add(eh, V.ev(c)), er), NA.mul_comm(er, Nat.add(eh, n)), Equal.cong(Nat, Nat, z => Nat.mul(Nat.add(eh, z), er), n, V.ev(c), A.sy(V.ev(c), n, ec)))))))
274	  A.tr(R.modp(Nat.mul(er, Nat.add(a, n))), Nat.mod(Nat.mul(er, Nat.add(a, n)), pp), Nat.mod(bv, pp), MP.modp_mod(one, h1, bp, h5, Nat.mul(er, Nat.add(a, n))),
275	    A.tr(Nat.mod(Nat.mul(er, Nat.add(a, n)), pp), Nat.mod(Nat.mul(Nat.add(eh, V.ev(c)), er), pp), Nat.mod(bv, pp), e3, e2))
276	
277	def absorb_ok(one, h1, bp, h5, fuel, msg, r, h, a, hrl, hrf, hh, ha):
278	  match fuel msg:
279	    case 0n _: ha
280	    case 1n+k Nil{}: ha
281	    case 1n+k b <> Nil{}:
282	      +m = {[b] : List<&2, U32>}
283	      +c = P.load(Li.take(16n, m))
284	      +h2 = Li.block(r, h, c)
285	      +a2 = R.modp(Nat.mul(V.ev(r), Nat.add(a, R.le_num(List.append(&2, U32, R.prefix(16n, m), [1])))))
286	      +hh2 = ST.block_inv(one, h1, r, h, c, hh, mask_fit(List.append(&2, U32, Li.take(16n, m), [1])), hrl, hrf)
287	      +ha2 = A.sy(a2, Nat.mod(V.ev(h2), 1n+bp), step_mod(one, h1, bp, h5, r, h, m, a, hrl, hrf, hh, ha))
288	      +ih = absorb_ok(one, h1, bp, h5, k, Li.skip(16n, m), r, h2, a2, hrl, hrf, hh2, ha2)
289	      A.tr(Nat.mod(V.ev(P.absorb(k, Li.skip(16n, m), r, h2)), 1n+bp), R.absorb(R.blocks(k, Li.skip(16n, m)), V.ev(r), a2), R.absorb(R.blocks(k, R.suffix(16n, m)), V.ev(r), a2), ih,
290	        Equal.cong(List<&2, U32>, Nat, l => R.absorb(R.blocks(k, l), V.ev(r), a2), Li.skip(16n, m), R.suffix(16n, m), skip_suffix(16n, m)))
291	    case 1n+k b <> d <> rest:
292	      +m = {b <> d <> rest : List<&2, U32>}
293	      +c = P.load(Li.take(16n, m))
294	      +h2 = Li.block(r, h, c)
295	      +a2 = R.modp(Nat.mul(V.ev(r), Nat.add(a, R.le_num(List.append(&2, U32, R.prefix(16n, m), [1])))))
296	      +hh2 = ST.block_inv(one, h1, r, h, c, hh, mask_fit(List.append(&2, U32, Li.take(16n, m), [1])), hrl, hrf)
297	      +ha2 = A.sy(a2, Nat.mod(V.ev(h2), 1n+bp), step_mod(one, h1, bp, h5, r, h, m, a, hrl, hrf, hh, ha))
298	      +ih = absorb_ok(one, h1, bp, h5, k, Li.skip(16n, m), r, h2, a2, hrl, hrf, hh2, ha2)
299	      A.tr(Nat.mod(V.ev(P.absorb(k, Li.skip(16n, m), r, h2)), 1n+bp), R.absorb(R.blocks(k, Li.skip(16n, m)), V.ev(r), a2), R.absorb(R.blocks(k, R.suffix(16n, m)), V.ev(r), a2), ih,
300	        Equal.cong(List<&2, U32>, Nat, l => R.absorb(R.blocks(k, l), V.ev(r), a2), Li.skip(16n, m), R.suffix(16n, m), skip_suffix(16n, m)))
301	
302	# ---- the tag ----
303	
304	def bpv(+one: Nat) -> Nat:
305	  Nat.sub(C.shift(130n, one), 6n)
306	
307	law bp5:
308	  for +one: Nat
309	  for +h1: {one == 1n : Nat}
310	  {Nat.add(1n+bpv(one), 5n) == C.shift(130n, one) : Nat}
311	
312	def bp5(one, h1):
313	  +s = C.shift(130n, one)
314	  +h6 = N.le_trans(6n, C.shift(3n, one), s, L.subst(Nat, z => {Nat.is_le(6n, C.shift(3n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), WW.shift_ge(127n, C.shift(3n, one)))
315	  A.tr(Nat.add(1n+bpv(one), 5n), Nat.add(5n, 1n+bpv(one)), s, N.add_comm(1n+bpv(one), 5n), N.sub_add(s, 6n, h6))
316	
317	law tag_main:
318	  for +one: Nat
319	  for +h1: {one == 1n : Nat}
320	  for +key: List<&2, U32>
321	  for +msg: List<&2, U32>
322	  {P.tag(key, msg) == R.poly1305_mac(key, msg) : List<&2, U32>}
323	
324	def tag_main(one, h1, key, msg):
325	  +bp = bpv(one)
326	  +h5 = bp5(one, h1)
327	  +r = P.r_key(key)
328	  +s = P.s_key(key)
329	  +hrf = fit_fit(16n, P.mask(P.clamp(Li.take(16n, key), 0n)), mask_fit(P.clamp(Li.take(16n, key), 0n)))
330	  +fuel = List.length(&2, U32, msg)
331	  +h = P.absorb(fuel, msg, r, P.zero())
332	  +hh = absorb_inv(one, h1, fuel, msg, r, P.zero(), {==}, hrf, {==})
333	  +ea = absorb_ok(one, h1, bp, h5, fuel, msg, r, P.zero(), 0n, {==}, hrf, {==}, {==})
334	  +rs = R.le_num(R.clamp(R.prefix(16n, key)))
335	  +ss = R.le_num(R.prefix(16n, R.suffix(16n, key)))
336	  +bs = R.blocks(fuel, msg)
337	  +te = F.fin_eq(one, h1, bp, h5, h, hh, s, mask_fit(Li.take(16n, Li.skip(16n, key))))
338	  +e1 = A.tr(Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s)), Nat.add(R.absorb(bs, V.ev(r), 0n), ss), Nat.add(R.absorb(bs, rs, 0n), ss),
339	    A.cadd(Nat.mod(V.ev(h), 1n+bp), R.absorb(bs, V.ev(r), 0n), V.ev(s), ss, ea, s_ev(key)),
340	    WM.cong_l(R.absorb(bs, V.ev(r), 0n), R.absorb(bs, rs, 0n), ss, Equal.cong(Nat, Nat, z => R.absorb(bs, z, 0n), V.ev(r), rs, r_ev(key))))
341	  Equal.trans(List<&2, U32>, P.tag(key, msg), R.le_bytes(16n, Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s))), R.poly1305_mac(key, msg), te,
342	    Equal.cong(Nat, List<&2, U32>, z => R.le_bytes(16n, z), Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s)), Nat.add(R.absorb(bs, rs, 0n), ss), e1))
343	
344	# The implementation's tag is the RFC 8439 tag, for every key and message.
345	law mac_correct:
346	  for +key: List<&2, U32>
347	  for +msg: List<&2, U32>
348	  {P.mac(key, msg) == R.mac(key, msg) : List<&2, U32>}
349	
350	def mac_correct(key, msg):
351	  match msg:
352	    case Nil{}: tag_main(1n, {==}, key, [])
353	    case b <> rest: tag_main(1n, {==}, key, b <> rest)
354	
355	law le_bytes_len:
356	  for +n: Nat
357	  for +x: Nat
358	  {List.length(&2, U32, R.le_bytes(n, x)) == n : Nat}
359	
360	def le_bytes_len(n, x):
361	  match n:
362	    case 0n: {==}
363	    case 1n+k: Equal.cong(Nat, Nat, z => 1n+z, List.length(&2, U32, R.le_bytes(k, C.high(8n, x))), k, le_bytes_len(k, C.high(8n, x)))
364	
365	# The tag has 16 bytes.
366	law mac_length:
367	  for +key: List<&2, U32>
368	  for +msg: List<&2, U32>
369	  {List.length(&2, U32, R.mac(key, msg)) == 16n : Nat}
370	
371	def mac_length(key, msg):
372	  match msg:
373	    case Nil{}: le_bytes_len(16n, Nat.add(R.absorb(R.blocks(0n, []), R.le_num(R.clamp(R.prefix(16n, key))), 0n), R.le_num(R.prefix(16n, R.suffix(16n, key)))))
374	    case b <> rest: le_bytes_len(16n, Nat.add(R.absorb(R.blocks(List.length(&2, U32, b <> rest), b <> rest), R.le_num(R.clamp(R.prefix(16n, key))), 0n), R.le_num(R.prefix(16n, R.suffix(16n, key)))))