Poly.reduce: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as Poly
Lines 65-72 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend&start_line=65&end_line=72

import Base

# p(x) modulo m(x) = x^n + low(x), by Horner's rule:
# p(x) = c + x*q(x), so p mod m = c + x*(q mod m) mod m.
def reduce(+n: Nat, +low: Word(n), p: List<&2, Bool>) -> Word(n):
  match p:
    case Nil{}:
      Word.zero(n)
    case c <> q:
      Word.xor(n, constant(n, c), times_x(n, low, reduce(n, low, q)))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.xor
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend&name=constant
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend&name=times_x