def Random.bytes

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

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/math/random/source.bend as SRC

91def Random.bytes(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>) -> Type:
92  {fst_bytes(CR.Gen, CR.bytes(CR.G{c, p}, n)) == take(n, append(p, flat(SRC.outputs(~C8.ChaCha8, ~C8.next, n, c)))) : List<&2, U32>}