def depth_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/top.bend:122

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as M

122def depth_lt(+n: Nat, +h: {Nat.is_le(M.levels(n), 23n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(8n, M.levels(n)), 32n) == True{} : Bool}:
123  N.le_lt_succ(M.levels(n), 23n, h)