Laws.absorb_poly: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/laws.bend as Laws
Lines 58-66 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/laws.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/laws.bend&start_line=58&end_line=66

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R

# The RFC's polynomial reading of the accumulator: absorbing the blocks
# (reducing after every block) is evaluating the polynomial of the blocks at
# r and reducing once mod 2^130 - 5 (2^130 written C.shift(130n, one)).
law absorb_poly:
  for +one: Nat
  for +h1: {one == 1n : Nat}
  for +bs: List<&2, List<&2, U32>>
  for +r: Nat
  {R.absorb(bs, r, 0n) == Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)) : Nat}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  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/proofs/crypto/poly1305/poly.bend&name=absorb_poly
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend&name=absorb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend&name=poly
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift