law q29

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

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

142# v(quot) fits 29 bits: the pass-1 top limb fits 31
143law q29:
144  for +d: List<&2, U32>
145  for +hd: {V.fit_all(d, 30n) == True{} : Bool}
146  {C.fits(29n, pv(d)) == True{} : Bool}