def coeff

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/poly1305.bend:129

import Base

129# RFC 8439 2.5 describes the accumulator as the evaluation, at r and
130# modulo p, of the polynomial whose coefficients are the blocks (each with
131# its 0x01 byte): with q blocks n_1 .. n_q,
132#   poly(r) = n_1 r^q + n_2 r^(q-1) + ... + n_q r
133# (as Spec.Poly1305 in HACL* and the field statements of Mathlib's ZMod p).
134# Clause absorb_poly (proofs/crypto/poly1305/poly.bend) proves
135# absorb(blocks, r, 0) == poly(blocks, r) mod (2^130 - 5).
136def coeff(b: List<&2, U32>) -> Nat:
137  le_num(List.append(&2, U32, b, [1]))