def ChaCha8.stream

bend-collections-laws-math@1.0.0.0 · spec/math/random.bend:77

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8.bend as C8
import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as B
import bend-collections-laws-math@1.0.0.0/spec/math/random/source.bend as SRC
import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as SC

77def ChaCha8.stream(+n: Nat, +k: B.Key) -> Type:
78  {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.of_key(k)) == SC.stream(n, SC.key_list(k)) : List<&2, W.U64>}