law fold_ev

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

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/src/crypto/poly1305/limbs.bend as Li
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V

80law fold_ev:
81  for +one: Nat
82  for +h1: {one == 1n : Nat}
83  for +z: List<&2, U32>
84  for +hz: {V.le_all(z, s21(one)) == True{} : Bool}
85  {V.ev(z) == Nat.add(V.ev(Li.fold(z)), Nat.mul(C.shift(6n, V.ev(Li.skip(17n, z))), pm(one))) : Nat}