Blake2s.compress: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend as Blake2s
Lines 96-112 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&start_line=96&end_line=112

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend as T

# F(h, m, t, f) with r rounds (r = 10 for BLAKE2s): t = t0 + 2^32 * t1 is the
# byte counter, f the final-block flag.
def compress(+r: Nat, h: T.State, +m: List<&2,U32>, +t0: U32, +t1: U32, last: Bool) -> T.State:
  match h:
    case T.H{+h0, +h1, +h2, +h3, +h4, +h5, +h6, +h7}:
      +v0 = List.append(&2, U32, [h0, h1, h2, h3, h4, h5, h6, h7], iv())
      +v1 = put(v0, 12n, U32.xor(get(v0, 12n), t0))
      +v2 = put(v1, 13n, U32.xor(get(v1, 13n), t1))
      +v = rounds(r, 0n, invert(last, v2), m)
      T.H{U32.xor(U32.xor(h0, get(v, 0n)), get(v, 8n)),
          U32.xor(U32.xor(h1, get(v, 1n)), get(v, 9n)),
          U32.xor(U32.xor(h2, get(v, 2n)), get(v, 10n)),
          U32.xor(U32.xor(h3, get(v, 3n)), get(v, 11n)),
          U32.xor(U32.xor(h4, get(v, 4n)), get(v, 12n)),
          U32.xor(U32.xor(h5, get(v, 5n)), get(v, 13n)),
          U32.xor(U32.xor(h6, get(v, 6n)), get(v, 14n)),
          U32.xor(U32.xor(h7, get(v, 7n)), get(v, 15n))}

Uses (12):
  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=List.append
  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=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=get
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=invert
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=iv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=put
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend&name=State