def outputs
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as Sourceimport Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
17# the first n outputs of the source from state s
18def outputs(~S: Data, ~next: S -> W.U64 & S, n: Nat, +s: S) -> List<&2, W.U64>:
19 match n:
20 case 0n:
21 []
22 case 1n+p:
23 Con{fst64(S, next(s)), outputs(~S, ~next, p, snd64(S, next(s)))}
Uses (6)
Used by (12)
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes:outs
- bend-collections-laws-crypto@1.0.0.0/spec/math/random:map_outputs
- bend-collections-laws-crypto@1.0.0.0/spec/crypto/random:map_outputs
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/proof:gen_outputs
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream:stream
- …