def stream

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/chacha8/stream.bend:82

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/block.bend as B
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/spec/math/random/chacha8rand.bend as S
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC

82# THEOREM: the generator keyed by k outputs C2SP's ChaCha8Rand stream keyed
83# by k's eight words, for every key and every number of outputs
84def stream(+n: Nat, +k: B.Key) -> {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.of_key(k)) == S.stream(n, S.key_list(k)) : List<&2, W.U64>}:
85  inv(n, k, [], C8.G0{})