def pick_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/password.bend:119

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/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as H
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as A2

119def pick_len(+tl: Nat, +x: List<&2, U32>, +short: Bool, +es: {Nat.is_le(tl, 64n) == short : Bool}) -> {len(A2.hp_pick(tl, x, short)) == tl : Nat}:
120  match short:
121    case True{}:
122      hash_len(tl, x, es)
123    case False{}:
124      +a = Nat.add(tl, 31n)
125      +ht = N.lt_succ_le_succ(64n, tl, N.not_le_lt(tl, 64n, es))
126      long_len(tl, Nat.div(a, 32n), Nat.mod(a, 32n), H.hash(64n, x), NR.dm_eq(31n, a), NR.dm_lt(31n, a), ht, hash_len(64n, x, {==}))