proofs/math/random/chacha8/seed.bend
1import Base
2import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
3import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8.bend as C8
4import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as B
5import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as S
6import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as SRM
7import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/stream.bend as CS
8import bend-collections-laws-math@1.0.0.0/spec/math/random/source.bend as SRC
9
10# A seed is 32 bytes below 256, read as eight little-endian words; any other
11# list is rejected.
12
13def bytes_eq(+bs: List<&2, U32>) -> {C8.all_bytes(bs) == S.bytes_ok(bs) : Bool}:
14 match bs:
15 case Nil{}:
16 {==}
17 case Con{+b, +rest}:
18 Equal.cong(Bool, Bool, z => Bool.and(U32.is_lt(b, 256), z), C8.all_bytes(rest), S.bytes_ok(rest), bytes_eq(rest))
19
20def seeded_ok(+n: Nat, +seed: List<&2, U32>) -> {SRM.map_outputs(n, C8.lift(C8.key_of(seed))) == SRM.map_stream(n, S.key_if(seed, Nat.is_eq(S.length(seed), 32n))) : Maybe<&2, List<&2, W.U64>>}:
21 match seed:
22 case Nil{}:
23 {==}
24 case Con{+a0, +r0}:
25 match r0:
26 case Nil{}:
27 {==}
28 case Con{+a1, +r1}:
29 match r1:
30 case Nil{}:
31 {==}
32 case Con{+a2, +r2}:
33 match r2:
34 case Nil{}:
35 {==}
36 case Con{+a3, +r3}:
37 match r3:
38 case Nil{}:
39 {==}
40 case Con{+b0, +r4}:
41 match r4:
42 case Nil{}:
43 {==}
44 case Con{+b1, +r5}:
45 match r5:
46 case Nil{}:
47 {==}
48 case Con{+b2, +r6}:
49 match r6:
50 case Nil{}:
51 {==}
52 case Con{+b3, +r7}:
53 match r7:
54 case Nil{}:
55 {==}
56 case Con{+c0, +r8}:
57 match r8:
58 case Nil{}:
59 {==}
60 case Con{+c1, +r9}:
61 match r9:
62 case Nil{}:
63 {==}
64 case Con{+c2, +r10}:
65 match r10:
66 case Nil{}:
67 {==}
68 case Con{+c3, +r11}:
69 match r11:
70 case Nil{}:
71 {==}
72 case Con{+d0, +r12}:
73 match r12:
74 case Nil{}:
75 {==}
76 case Con{+d1, +r13}:
77 match r13:
78 case Nil{}:
79 {==}
80 case Con{+d2, +r14}:
81 match r14:
82 case Nil{}:
83 {==}
84 case Con{+d3, +r15}:
85 match r15:
86 case Nil{}:
87 {==}
88 case Con{+e0, +r16}:
89 match r16:
90 case Nil{}:
91 {==}
92 case Con{+e1, +r17}:
93 match r17:
94 case Nil{}:
95 {==}
96 case Con{+e2, +r18}:
97 match r18:
98 case Nil{}:
99 {==}
100 case Con{+e3, +r19}:
101 match r19:
102 case Nil{}:
103 {==}
104 case Con{+f0, +r20}:
105 match r20:
106 case Nil{}:
107 {==}
108 case Con{+f1, +r21}:
109 match r21:
110 case Nil{}:
111 {==}
112 case Con{+f2, +r22}:
113 match r22:
114 case Nil{}:
115 {==}
116 case Con{+f3, +r23}:
117 match r23:
118 case Nil{}:
119 {==}
120 case Con{+g0, +r24}:
121 match r24:
122 case Nil{}:
123 {==}
124 case Con{+g1, +r25}:
125 match r25:
126 case Nil{}:
127 {==}
128 case Con{+g2, +r26}:
129 match r26:
130 case Nil{}:
131 {==}
132 case Con{+g3, +r27}:
133 match r27:
134 case Nil{}:
135 {==}
136 case Con{+h0, +r28}:
137 match r28:
138 case Nil{}:
139 {==}
140 case Con{+h1, +r29}:
141 match r29:
142 case Nil{}:
143 {==}
144 case Con{+h2, +r30}:
145 match r30:
146 case Nil{}:
147 {==}
148 case Con{+h3, +r31}:
149 match r31:
150 case Nil{}:
151 +k = {B.K{C8.le32(a0, a1, a2, a3), C8.le32(b0, b1, b2, b3), C8.le32(c0, c1, c2, c3), C8.le32(d0, d1, d2, d3), C8.le32(e0, e1, e2, e3), C8.le32(f0, f1, f2, f3), C8.le32(g0, g1, g2, g3), C8.le32(h0, h1, h2, h3)} : B.Key}
152 Equal.cong(List<&2, W.U64>, Maybe<&2, List<&2, W.U64>>, l => Some{l}, SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.of_key(k)), S.stream(n, S.key_list(k)), CS.stream(n, k))
153 case Con{x, rr}:
154 {==}
155
156def seeded_c(+n: Nat, +seed: List<&2, U32>, +b: Bool) -> {SRM.map_outputs(n, C8.seed_ok(seed, b)) == SRM.map_stream(n, S.key_if(seed, Bool.and(b, Nat.is_eq(S.length(seed), 32n)))) : Maybe<&2, List<&2, W.U64>>}:
157 match b:
158 case False{}:
159 {==}
160 case True{}:
161 seeded_ok(n, seed)
162
163# THEOREM (ChaCha8.seeded)
164def seeded(+n: Nat, +seed: List<&2, U32>) -> SRM.ChaCha8.seeded(n, seed):
165 %Equal.sym(Bool, C8.all_bytes(seed), S.bytes_ok(seed), bytes_eq(seed)) : {SRM.map_outputs(n, C8.seed_ok(seed, _)) == SRM.map_stream(n, S.key_if(seed, Bool.and(S.bytes_ok(seed), Nat.is_eq(S.length(seed), 32n)))) : Maybe<&2, List<&2, W.U64>>}
166 seeded_c(n, seed, S.bytes_ok(seed))