def pick

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
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

303# J1 || J2: the address block's lane idx mod 128 (data-independent), or the
304# first lane of the previous block (data-dependent).
305def pick(indep: Bool, +addr: A.Block, +idx: Nat, +prev: A.Block) -> T.Lane:
306  match indep:
307    case True{}:
308      G.lane(addr, Nat.mod(idx, 128n))
309    case False{}:
310      G.lane(prev, 0n)