def Random.stream

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
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
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as SC

85def Random.stream(+n: Nat, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32) -> Type:
86  {SRC.outputs(~CR.Gen, ~CR.next, n, CR.of_words(k0, k1, k2, k3, k4, k5, k6, k7)) == SC.stream(n, [k0, k1, k2, k3, k4, k5, k6, k7]) : List<&2, W.U64>}