Hash.absorb512: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/crypto/hash.bend as Hash
Lines 327-338 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=327&end_line=338

import Base
import bend-collections@1.0.0.0/src/crypto/sha512/types.bend as T512
import bend-collections@1.0.0.0/src/crypto/sha512/core.bend as C512

# 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 (64n), kept a variable for the proofs.
def absorb512(fuel: Nat, r: Read512, orig: List<&2, U32>, +q: Nat, s: T512.State) -> Sha512State:
  match fuel r:
    case 0n _:
      St512{s, orig}
    case 1n+p Short512{}:
      St512{s, orig}
    case 1n+p Blk512{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, +rest}:
      absorb512(p, read512_0(rest), rest, q, C512.compress16(w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, q, C512.round_constants(), s))

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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/hash.bend&name=Read512
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/hash.bend&name=Sha512State
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/hash.bend&name=read512_0
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha512/core.bend&name=compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha512/core.bend&name=round_constants
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha512/types.bend&name=State