Argon2.init_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 388-396 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=388&end_line=396

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

# B[l][0] = H'^1024(H0 || LE32(0) || LE32(l)), B[l][1] = H'^1024(H0 || LE32(1) || LE32(l)).
def init_go(n: Nat, +l: Nat, +q: Nat, +hh: List<&2, U32>, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
  match n:
    case 0n:
      mem
    case 1n+rest:
      +b0 = block_of(hprime(1024n, cat(hh, cat(le32(0n), le32(l)))))
      +b1 = block_of(hprime(1024n, cat(hh, cat(le32(1n), le32(l)))))
      init_go(rest, Nat.add(l, 1n), q, hh, set(set(mem, Nat.mul(l, q), b0), Nat.add(Nat.mul(l, q), 1n), b1))

Uses (11):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=block_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=cat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=hprime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=le32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=set
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block