def wrap_map

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

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/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.bend as SRM
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

48def wrap_map(+n: Nat, m: Maybe<&2, C8.ChaCha8>) -> {SCR.map_outputs(n, CR.wrap(m)) == SRM.map_outputs(n, m) : Maybe<&2, List<&2, W.U64>>}:
49  match m:
50    case None{}:
51      {==}
52    case Some{+c}:
53      Equal.cong(List<&2, W.U64>, Maybe<&2, List<&2, W.U64>>, l => Some{l}, SRC.outputs(~CR.Gen, ~CR.next, n, CR.G{c, []}), SRC.outputs(~C8.ChaCha8, ~C8.next, n, c), gen_outputs(n, c, []))