def and255
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/password.bend:150
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend as Password
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/hash/hash.bend as HH
150def and255(+w: U32) -> {Nat.is_lt(U32.to_nat(U32.and(w, 255)), 256n) == True{} : Bool}:
151 N.le_lt_succ(U32.to_nat(U32.and(w, 255)), 255n, HH.and_le32(w, 255))