Poly1305.absorb: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as Poly1305
Lines 38-48 of bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend&start_line=38&end_line=48

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as L

# The accumulator over 16-byte blocks (the last one possibly shorter); fuel
# bounds the number of blocks. (A one-byte message is its own case only so
# that a proof about a message b <> rest with rest unknown stays small.)
def absorb(fuel: Nat, +msg: List<&2, U32>, +r: List<&2, U32>, h: List<&2, U32>) -> List<&2, U32>:
  match fuel msg:
    case 0n _: h
    case 1n+k Nil{}: h
    case 1n+k b <> Nil{}:
      absorb(k, L.skip(16n, [b]), r, L.block(r, h, load(L.take(16n, [b]))))
    case 1n+k b <> c <> rest:
      absorb(k, L.skip(16n, b <> c <> rest), r, L.block(r, h, load(L.take(16n, b <> c <> rest))))

Uses (7):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend&name=block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend&name=skip
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend&name=load