Sha3.absorb: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as Sha3
Lines 84-91 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend&start_line=84&end_line=91

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/permutation.bend as K

# Section 4, step 6: S = f(S XOR (P_i || 0^c)) for each r-bit block P_i.
def absorb(ls: List<&2, T.Lane>, +rounds: Nat, s: T.State) -> T.State:
  match ls:
    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest:
      absorb(rest, rounds, K.rounds(rounds, 0n, of_lanes(xor_lanes(to_lanes(s),
        [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16]))))
    case _:
      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=bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/permutation.bend&name=rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend&name=of_lanes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend&name=to_lanes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend&name=xor_lanes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend&name=Lane
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend&name=State