law reduce_ev
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/step.bend:205
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as Step
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
205law reduce_ev:
206 for +one: Nat
207 for +h1: {one == 1n : Nat}
208 for +d: List<&2, U32>
209 for +hd: {V.fit_all(d, 30n) == True{} : Bool}
210 for +hl: {Nat.is_le(V.len(d), 17n) == True{} : Bool}
211 {V.ev(d) == Nat.add(V.ev(Li.reduce(d)), Nat.mul(pv(d), pm(one))) : Nat}