Poly1305.coeff: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as Poly1305
Lines 129-137 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend&start_line=129&end_line=137

import Base

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend&name=le_num