def mbound

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/step.bend:318

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/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
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

318# len(r) * (2^9 * 2^8) == 2^21
319def mbound(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, U32>, +hrl: {V.len(r) == 16n : Nat}) -> {Nat.mul(V.len(r), Nat.mul(Nat.add(C.shift(8n, one), C.shift(8n, one)), C.shift(8n, one))) == s21(one) : Nat}:
320  +s8 = C.shift(8n, one)
321  +m = Nat.mul(Nat.add(s8, s8), s8)
322  +em = A.tr(m, Nat.mul(C.shift(9n, one), s8), C.shift(17n, one), A.cmul(Nat.add(s8, s8), C.shift(9n, one), s8, s8, A.sy(Nat.double(s8), Nat.add(s8, s8), NA.double_self(s8)), {==}), A.shmul(9n, 8n, one, h1))
323  A.tr(Nat.mul(V.len(r), m), Nat.mul(16n, m), s21(one), Equal.cong(Nat, Nat, t => Nat.mul(t, m), V.len(r), 16n, hrl),
324    A.tr(Nat.mul(16n, m), Nat.mul(m, 16n), s21(one), NA.mul_comm(16n, m),
325      A.tr(Nat.mul(m, 16n), C.shift(4n, m), s21(one), A.mul_pow(4n, m), A.csh(4n, m, C.shift(17n, one), em))))