def byte_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/random/bytes.bend:180

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/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend as BI
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend as BL

180# y & 255 < 256
181def byte_lt(+y: U32) -> {U32.is_lt(U32.and(y, 255), 256) == True{} : Bool}:
182  Equal.trans(Bool, U32.is_lt(U32.and(y, 255), 256), Nat.is_lt(U32.to_nat(U32.and(y, 255)), 256n), True{},
183    U.is_lt_nat(U32.and(y, 255), 256),
184    %Equal.sym(Nat, U32.to_nat(U32.and(y, 255)), SR.and_bits(32n, U32.to_nat(y), 255n), BI.uand(y, 255)) : {Nat.is_lt(_, 256n) == True{} : Bool}
185    N.le_lt_succ(SR.and_bits(32n, U32.to_nat(y), 255n), 255n, BL.and_le(32n, U32.to_nat(y), 255n)))