law absorb_poly

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

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

58# The RFC's polynomial reading of the accumulator: absorbing the blocks
59# (reducing after every block) is evaluating the polynomial of the blocks at
60# r and reducing once mod 2^130 - 5 (2^130 written C.shift(130n, one)).
61law absorb_poly:
62  for +one: Nat
63  for +h1: {one == 1n : Nat}
64  for +bs: List<&2, List<&2, U32>>
65  for +r: Nat
66  {R.absorb(bs, r, 0n) == Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)) : Nat}