~/jendhub

proofs/crypto/poly1305/mac.bend

bend-collections-laws-crypto@1.0.0.0 · 374 lines · 24 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as P
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as SH
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend as FB
13import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as ST
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/modp.bend as MP
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/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
29law mask_ev:
30  for +xs: List<&2, U32>
31  {V.ev(P.mask(xs)) == R.le_num(xs) : Nat}
32
33def 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
38law mask_fit:
39  for +xs: List<&2, U32>
40  {V.fit_all(P.mask(xs), 8n) == True{} : Bool}
41
42def 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
50law mask_len:
51  for +xs: List<&2, U32>
52  {V.len(P.mask(xs)) == V.len(xs) : Nat}
53
54def 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
59law 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
64def 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
70law 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
75def 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
81law cmask:
82  for +i: Nat
83  {P.clamp_mask(i) == R.clamp_mask(i) : U32}
84
85def 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
105law 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
110def 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
118law clamp_len:
119  for +xs: List<&2, U32>
120  for +i: Nat
121  {V.len(P.clamp(xs, i)) == V.len(xs) : Nat}
122
123def 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
128law 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
134def 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
139law 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
145def 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
153law 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
157def 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
167law 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
171def 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
178law app1:
179  for +t: List<&2, U32>
180  {V.len(List.append(&2, U32, t, [1])) == Nat.add(V.len(t), 1n) : Nat}
181
182def 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
188law 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
195def 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
201def 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
207law 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
223law 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
235def 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
249def 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
277def 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
304def bpv(+one: Nat) -> Nat:
305  Nat.sub(C.shift(130n, one), 6n)
306
307law bp5:
308  for +one: Nat
309  for +h1: {one == 1n : Nat}
310  {Nat.add(1n+bpv(one), 5n) == C.shift(130n, one) : Nat}
311
312def 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
317law 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
324def 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.
345law 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
350def 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
355law le_bytes_len:
356  for +n: Nat
357  for +x: Nat
358  {List.length(&2, U32, R.le_bytes(n, x)) == n : Nat}
359
360def 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.
366law 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
371def 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)))))