def ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/phc.bend:15

import Base

15# Every byte is below 256.
16def ok(bs: List<&2, U32>) -> Bool:
17  match bs:
18    case Nil{}:
19      True{}
20    case x <> r:
21      Bool.and(Nat.is_lt(U32.to_nat(x), 256n), ok(r))