Blake2s.mix: 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 60-70 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=60&end_line=70

import Base

# G(v[0..15], a, b, c, d, x, y) with BLAKE2s rotations R1..R4 = 16, 12, 8, 7.
def mix(+v: List<&2,U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, x: U32, y: U32) -> List<&2,U32>:
  +va = U32.add(U32.add(get(v, a), get(v, b)), x)
  +vd = rotr(U32.xor(get(v, d), va), 16n)
  +vc = U32.add(get(v, c), vd)
  +vb = rotr(U32.xor(get(v, b), vc), 12n)
  +va2 = U32.add(U32.add(va, vb), y)
  +vd2 = rotr(U32.xor(vd, va2), 8n)
  +vc2 = U32.add(vc, vd2)
  +vb2 = rotr(U32.xor(vb, vc2), 7n)
  put(put(put(put(v, a, va2), b, vb2), c, vc2), d, vd2)

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=Base/base.bend&name=U32.add
  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=put
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=rotr