law pass2_ev

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

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

155# pass 2 on the split: its value is 5 q + the split
156law pass2_ev:
157  for +d: List<&2, U32>
158  for +hd: {V.fit_all(d, 30n) == True{} : Bool}
159  {V.ev(Li.reduce(d)) == Nat.add(Nat.mul(pv(d), 5n), V.ev(Li.split(16n, Li.carry(16n, d, 0)))) : Nat}