Blake3.g: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as Blake3
Lines 83-93 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&start_line=83&end_line=93

import Base

# The quarter-round G on state positions a, b, c, d with message words mx, my.
def g(+v: List<&2,U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +mx: U32, +my: U32) -> List<&2,U32>:
  +va = U32.add(U32.add(at(v,a),at(v,b)),mx)
  +vd = rotr(U32.xor(at(v,d),va),16n)
  +vc = U32.add(at(v,c),vd)
  +vb = rotr(U32.xor(at(v,b),vc),12n)
  +va2 = U32.add(U32.add(va,vb),my)
  +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/blake3.bend&name=at
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=put
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=rotr