law absorb_horner

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

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

90# absorb(bs, r, a) == horner(bs, r, a) mod p, for a < p.
91law absorb_horner:
92  for +one: Nat
93  for +h1: {one == 1n : Nat}
94  for +bs: List<&2, List<&2, U32>>
95  for +r: Nat
96  for +a: Nat
97  for +ha: {Nat.is_lt(a, 1n+M.bpv(one)) == True{} : Bool}
98  {R.absorb(bs, r, a) == Nat.mod(horner(bs, r, a), 1n+M.bpv(one)) : Nat}