def Random.bytes_lt

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/random.bend:94

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend as C8
import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as CR

94def Random.bytes_lt(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>, +hp: {below256(p) == True{} : Bool}) -> Type:
95  {below256(fst_bytes(CR.Gen, CR.bytes(CR.G{c, p}, n))) == True{} : Bool}