law horner_mod

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

import Base

61# horner only depends on its start value mod n.
62law horner_mod:
63  for +bp: Nat
64  for +bs: List<&2, List<&2, U32>>
65  for +r: Nat
66  for +x: Nat
67  {Nat.mod(horner(bs, r, Nat.mod(x, 1n+bp)), 1n+bp) == Nat.mod(horner(bs, r, x), 1n+bp) : Nat}