law block_ev

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

import Base
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/proofs/crypto/poly1305/value.bend as V

375# (h + c) r == block(r, h, c) + bk p
376law block_ev:
377  for +one: Nat
378  for +h1: {one == 1n : Nat}
379  for +r: List<&2, U32>
380  for +h: List<&2, U32>
381  for +c: List<&2, U32>
382  for +hh: {inv(h) == True{} : Bool}
383  for +hcl: {Nat.is_le(V.len(c), 17n) == True{} : Bool}
384  for +hcf: {V.fit_all(c, 8n) == True{} : Bool}
385  for +hrl: {V.len(r) == 16n : Nat}
386  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
387  {Nat.mul(Nat.add(V.ev(h), V.ev(c)), V.ev(r)) == Nat.add(V.ev(Li.block(r, h, c)), Nat.mul(bk(r, h, c), pm(one))) : Nat}