law absorb_poly

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/poly.bend:114

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/spec/crypto/poly1305.bend as R

114# The accumulator is the polynomial at r, reduced mod 2^130 - 5.
115law absorb_poly:
116  for +one: Nat
117  for +h1: {one == 1n : Nat}
118  for +bs: List<&2, List<&2, U32>>
119  for +r: Nat
120  {R.absorb(bs, r, 0n) == Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)) : Nat}