Hash.absorb256: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/crypto/hash.bend as Hash
Lines 180-191 of bend-collections@1.0.0.0/src/crypto/hash.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/crypto/hash.bend&start_line=180&end_line=191

import Base
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S256
import bend-collections@1.0.0.0/src/crypto/sha/core.bend as C256

# Compress every whole block (fuel bounds the count: any fuel >= the number of
# blocks reads them all; fewer leaves the rest buffered, still correct). The
# chaining state and the unread bytes; orig is the list the read r started at.
# q is the algorithm's round parameter (48n), kept a variable for the proofs.
def absorb256(fuel: Nat, r: Read256, orig: List<&2, U32>, +q: Nat, s: S256.State) -> Sha256State:
  match fuel r:
    case 0n _:
      St256{s, orig}
    case 1n+p Short256{}:
      St256{s, orig}
    case 1n+p Blk256{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, +rest}:
      absorb256(p, read256_0(rest), rest, q, C256.fips_compress16(w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, q, s))

Uses (8):
  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@1.0.0.0/src/crypto/hash.bend&name=Read256
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/hash.bend&name=Sha256State
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/hash.bend&name=read256_0
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=fips_compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/state.bend&name=State