proofs/crypto/random/proof.bend
bend-collections-laws-crypto@1.0.0.0 · 70 lines · 10 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
3import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
4import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend as C8
5import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as CR
7import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC
8import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as SC
9import bend-collections-laws-crypto@1.0.0.0/spec/math/random.bend as SRM
10import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend as CS
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/seed.bend as SEED
13import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bounded.bend as BD
14import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/shuffle.bend as SH
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend as BY
16
17
18
19
20
21
22def kp_fst(+p: List<&2, U32>, q: W.U64 & C8.ChaCha8) -> {SRC.fst64(CR.Gen, CR.keep_pending(p, q)) == SRC.fst64(C8.ChaCha8, q) : W.U64}:
23 match q:
24 case Tuple{x, c}:
25 {==}
26
27def kp_snd(+p: List<&2, U32>, q: W.U64 & C8.ChaCha8) -> {SRC.snd64(CR.Gen, CR.keep_pending(p, q)) == CR.G{SRC.snd64(C8.ChaCha8, q), p} : CR.Gen}:
28 match q:
29 case Tuple{x, c}:
30 {==}
31
32
33def gen_outputs(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>) -> {SRC.outputs(~CR.Gen, ~CR.next, n, CR.G{c, p}) == SRC.outputs(~C8.ChaCha8, ~C8.next, n, c) : List<&2, W.U64>}:
34 match n:
35 case 0n:
36 {==}
37 case 1n+m:
38 %Equal.sym(W.U64, SRC.fst64(CR.Gen, CR.keep_pending(p, C8.next(c))), SRC.fst64(C8.ChaCha8, C8.next(c)), kp_fst(p, C8.next(c))) : {Con{_, SRC.outputs(~CR.Gen, ~CR.next, m, SRC.snd64(CR.Gen, CR.keep_pending(p, C8.next(c))))} == SRC.outputs(~C8.ChaCha8, ~C8.next, 1n+m, c) : List<&2, W.U64>}
39 %Equal.sym(CR.Gen, SRC.snd64(CR.Gen, CR.keep_pending(p, C8.next(c))), CR.G{SRC.snd64(C8.ChaCha8, C8.next(c)), p}, kp_snd(p, C8.next(c))) : {Con{SRC.fst64(C8.ChaCha8, C8.next(c)), SRC.outputs(~CR.Gen, ~CR.next, m, _)} == SRC.outputs(~C8.ChaCha8, ~C8.next, 1n+m, c) : List<&2, W.U64>}
40 Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{SRC.fst64(C8.ChaCha8, C8.next(c)), l}, SRC.outputs(~CR.Gen, ~CR.next, m, CR.G{SRC.snd64(C8.ChaCha8, C8.next(c)), p}), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.next(c))), gen_outputs(m, SRC.snd64(C8.ChaCha8, C8.next(c)), p))
41
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))
47
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, []))
54
55def Random.seeded(+n: Nat, +seed: List<&2, U32>) -> SCR.Random.seeded(n, seed):
56 Equal.trans(Maybe<&2, List<&2, W.U64>>, SCR.map_outputs(n, CR.wrap(C8.new(seed))), SRM.map_outputs(n, C8.new(seed)), SRM.map_stream(n, SC.key_of_seed(seed)),
57 wrap_map(n, C8.new(seed)),
58 SEED.seeded(n, seed))
59
60def Random.bytes(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>) -> SCR.Random.bytes(n, c, p):
61 BY.bytes(n, c, p)
62
63def Random.bytes_lt(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>, +hp: {SCR.below256(p) == True{} : Bool}) -> SCR.Random.bytes_lt(n, c, p, hp):
64 BY.bytes_lt(n, c, p, hp)
65
66def Random.uint_below(+g: CR.Gen, +n: W.U64, +hn: {X.is_zero(n) == False{} : Bool}) -> SCR.Random.uint_below(g, n, hn):
67 BD.uint64n_lt(~CR.Gen, ~CR.next, g, n, hn)
68
69def Random.shuffle(~A: Data, ~V: Data, ~rel: A -> V -> Bool, +g: CR.Gen, +items: List<&2, A>, +v: V) -> SCR.Random.shuffle(~A, ~V, ~rel, g, items, v):
70 SH.shuffle_perm(~A, ~V, ~rel, ~CR.Gen, ~CR.next, g, items, v)