def init_go

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/argon2/argon2.bend:388

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

388# B[l][0] = H'^1024(H0 || LE32(0) || LE32(l)), B[l][1] = H'^1024(H0 || LE32(1) || LE32(l)).
389def init_go(n: Nat, +l: Nat, +q: Nat, +hh: List<&2, U32>, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
390  match n:
391    case 0n:
392      mem
393    case 1n+rest:
394      +b0 = block_of(hprime(1024n, cat(hh, cat(le32(0n), le32(l)))))
395      +b1 = block_of(hprime(1024n, cat(hh, cat(le32(1n), le32(l)))))
396      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))