~/jendhub

def byte_of_lt

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

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend as Bytes
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

187def byte_of_lt(+w: U32, +k: Nat) -> {U32.is_lt(SCR.byte_of(w, k), 256) == True{} : Bool}:
188  byte_lt(U32.shrn(w, k))

Uses (7)

Used by (1)