def step_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/fill.bend:194

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
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/argon2.bend as SA

194def step_len(+r: Nat, +l: Nat, +s: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +cur: Nat, +indep: Bool, +addr: A.Block, +pb: A.Block, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.step(r, l, s, idx, p, q, sl, cur, indep, addr, pb, mem)) == SC.length(A.Block, mem) : Nat}:
195  +r0 = Nat.is_eq(r, 0n)
196  store_len(r0, cur, pb, SA.get(mem, ixs(r0, s, l, idx, p, q, sl, SA.pick(indep, addr, idx, pb))), mem)