def Random.stream

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/random/proof.bend:42

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/math/random/chacha8.bend as C8
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
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
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend as CS

42def Random.stream(+n: Nat, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32) -> SCR.Random.stream(n, k0, k1, k2, k3, k4, k5, k6, k7):
43  +k = {B.K{k0, k1, k2, k3, k4, k5, k6, k7} : B.Key}
44  Equal.trans(List<&2, W.U64>, SRC.outputs(~CR.Gen, ~CR.next, n, CR.G{C8.of_key(k), []}), SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.of_key(k)), SC.stream(n, SC.key_list(k)),
45    gen_outputs(n, C8.of_key(k), []),
46    CS.stream(n, k))