law horner_poly

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R

44# horner(bs, r, a) == a r^q + poly(bs, r)
45law horner_poly:
46  for +bs: List<&2, List<&2, U32>>
47  for +r: Nat
48  for +a: Nat
49  {horner(bs, r, a) == Nat.add(Nat.mul(a, Nat.pow(r, len(bs))), R.poly(bs, r)) : Nat}