def valid

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

import Base

409# RFC 9106 section 3.1: 1 <= p <= 2^24 - 1, 4 <= T <= 2^32 - 1,
410# 8p <= m <= 2^32 - 1, 1 <= t <= 2^32 - 1, 8 <= |S| <= 2^32 - 1 and |P|, |K|,
411# |X| <= 2^32 - 1.
412def valid(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> Bool:
413  Bool.and(Bool.and(Bool.and(Nat.is_le(1n, p), Nat.is_le(p, 16777215n)), Bool.and(Nat.is_le(4n, tl), Nat.is_le(tl, 4294967295n))),
414    Bool.and(Bool.and(Bool.and(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n)), Bool.and(Nat.is_le(1n, t), Nat.is_le(t, 4294967295n))),
415      Bool.and(Bool.and(Nat.is_le(8n, len(salt)), Nat.is_le(len(salt), 4294967295n)), Bool.and(Nat.is_le(len(pw), 4294967295n), Bool.and(Nat.is_le(len(key), 4294967295n), Nat.is_le(len(ad), 4294967295n))))))