def step_mod

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/mac.bend:248

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as ST
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/modp.bend as MP

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))