def bk

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

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

296# the multiple of p dropped by one block
297def bk(+r: List<&2, U32>, +h: List<&2, U32>, +c: List<&2, U32>) -> Nat:
298  Nat.add(C.shift(6n, V.ev(Li.skip(17n, zz(r, h, c)))), pv(Li.fold(zz(r, h, c))))