spec/crypto/poly1305.bend checks

p = 2^130 - 5

x = lo + 2^130 hi is congruent to lo + 5 hi mod p (2^130 = p + 5); the fold strictly decreases x while hi > 0, so x folds bring x below 2^130.

y < 2^130: y itself when y < p, else y - p = (y + 5) - 2^130.

x mod p

le_bytes_to_num

num_to_n_le_bytes: the low n bytes of x.

clamp(r): r &= 0x0ffffffc0ffffffc0ffffffc0fffffff, i.e. r[3], r[7], r[11] and r[15] keep their low four bits, r[4], r[8] and r[12] lose their low two.

The message cut into 16-byte blocks, the last one possibly shorter; fuel bounds the number of blocks (the length of the message is enough).

for each block: n = le_bytes_to_num(block | [0x01]); a += n; a = (r * a) % p

poly1305_mac(msg, key): r = clamp(key[0..16]), s = key[16..32]; a = 0, absorb every block, a += s; the tag is num_to_16_le_bytes(a).

The same function, split on the message first so that a proof about an unknown message does not unfold it.

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).