def bytes_lt

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

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
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

210# THEOREM (Random.bytes_lt)
211def bytes_lt(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>, +hp: {SCR.below256(p) == True{} : Bool}) -> SCR.Random.bytes_lt(n, c, p, hp):
212  %Equal.sym(List<&2, U32>, SCR.fst_bytes(CR.Gen, CR.bytes(CR.G{c, p}, n)), SCR.take(n, SCR.append(p, SCR.flat(outs(n, c)))), bytes(n, c, p)) : {SCR.below256(_) == True{} : Bool}
213  below_take(n, SCR.append(p, SCR.flat(outs(n, c))), below_app(p, SCR.flat(outs(n, c)), hp, flat_below(outs(n, c))))