def bytes

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

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

147# THEOREM (Random.bytes)
148def bytes(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>) -> SCR.Random.bytes(n, c, p):
149  Equal.trans(List<&2, U32>, SCR.fst_bytes(CR.Gen, CR.done(CR.fill(n, CR.FS{[], c, p}))), rev(facc(CR.fill(n, CR.FS{[], c, p}))), SCR.take(n, SCR.append(p, SCR.flat(outs(n, c)))),
150    done_bytes(CR.fill(n, CR.FS{[], c, p})),
151    fill_inv(n, CR.FS{[], c, p}))