def step

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

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

333def step(+r: Nat, +l: Nat, +s: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +cur: Nat, +indep: Bool, +addr: A.Block, +prev: A.Block, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
334  +r0 = Nat.is_eq(r, 0n)
335  +pr = pick(indep, addr, idx, prev)
336  +rl = ref_lane(Bool.and(r0, Nat.is_eq(s, 0n)), l, hi(pr), p)
337  +w = area(area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l))
338  +ri = Nat.mod(Nat.add(start(r0, s, sl), rel(w, lo(pr))), q)
339  store(r0, cur, prev, get(mem, Nat.add(Nat.mul(rl, q), ri)), mem)