Argon2.final_go: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as Argon2
Lines 398-405 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&start_line=398&end_line=405

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as G

# C = B[0][q-1] XOR B[1][q-1] XOR .. XOR B[p-1][q-1]: b is B[l][q-1], n more
# lanes follow.
def final_go(n: Nat, +l: Nat, +q: Nat, c: A.Block, b: A.Block, +mem: List<&2, A.Block>) -> A.Block:
  match n:
    case 0n:
      G.xor(c, b)
    case 1n+rest:
      final_go(rest, Nat.add(l, 1n), q, G.xor(c, b), get(mem, Nat.add(Nat.mul(Nat.add(l, 1n), q), Nat.sub(q, 1n))), mem)

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=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=get
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block