proofs/crypto/random/bytes.bend
bend-collections-laws-crypto@1.0.0.0 · 213 lines · 26 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/random/chacha8.bend as C8
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as CR
5import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
10import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend as BI
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend as BL
13
14
15
16
17
18def rev(xs: List<&2, U32>) -> List<&2, U32>:
19 List.reverse(&2, U32, xs)
20
21def app_nil(+xs: List<&2, U32>) -> {SCR.append(xs, []) == xs : List<&2, U32>}:
22 match xs:
23 case Nil{}:
24 {==}
25 case Con{+x, +rest}:
26 Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{x, l}, SCR.append(rest, []), rest, app_nil(rest))
27
28def app_assoc(+xs: List<&2, U32>, +ys: List<&2, U32>, +zs: List<&2, U32>) -> {SCR.append(SCR.append(xs, ys), zs) == SCR.append(xs, SCR.append(ys, zs)) : List<&2, U32>}:
29 match xs:
30 case Nil{}:
31 {==}
32 case Con{+x, +rest}:
33 Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{x, l}, SCR.append(SCR.append(rest, ys), zs), SCR.append(rest, SCR.append(ys, zs)), app_assoc(rest, ys, zs))
34
35
36def rgo(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {List.reverse.go(&2, U32, xs, ys) == SCR.append(rev(xs), ys) : List<&2, U32>}:
37 match xs:
38 case Nil{}:
39 {==}
40 case Con{+h, +t}:
41 Equal.trans(List<&2, U32>, List.reverse.go(&2, U32, t, Con{h, ys}), SCR.append(rev(t), Con{h, ys}), SCR.append(List.reverse.go(&2, U32, t, [h]), ys),
42 rgo(t, Con{h, ys}),
43 Equal.trans(List<&2, U32>, SCR.append(rev(t), Con{h, ys}), SCR.append(SCR.append(rev(t), [h]), ys), SCR.append(List.reverse.go(&2, U32, t, [h]), ys),
44 Equal.sym(List<&2, U32>, SCR.append(SCR.append(rev(t), [h]), ys), SCR.append(rev(t), SCR.append([h], ys)), app_assoc(rev(t), [h], ys)),
45 Equal.cong(List<&2, U32>, List<&2, U32>, l => SCR.append(l, ys), SCR.append(rev(t), [h]), List.reverse.go(&2, U32, t, [h]), Equal.sym(List<&2, U32>, List.reverse.go(&2, U32, t, [h]), SCR.append(rev(t), [h]), rgo(t, [h])))))
46
47
48def rev_cons(+b: U32, +acc: List<&2, U32>, +ts: List<&2, U32>) -> {SCR.append(rev(Con{b, acc}), ts) == SCR.append(rev(acc), Con{b, ts}) : List<&2, U32>}:
49 Equal.trans(List<&2, U32>, SCR.append(List.reverse.go(&2, U32, acc, [b]), ts), SCR.append(SCR.append(rev(acc), [b]), ts), SCR.append(rev(acc), Con{b, ts}),
50 Equal.cong(List<&2, U32>, List<&2, U32>, l => SCR.append(l, ts), List.reverse.go(&2, U32, acc, [b]), SCR.append(rev(acc), [b]), rgo(acc, [b])),
51 app_assoc(rev(acc), [b], ts))
52
53
54def b0(x: W.U64) -> U32:
55 match x:
56 case W.U64{+l, +h}:
57 SCR.byte_of(l, 0n)
58
59def b7(x: W.U64) -> List<&2, U32>:
60 match x:
61 case W.U64{+l, +h}:
62 [SCR.byte_of(l, 8n), SCR.byte_of(l, 16n), SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)]
63
64def le_split(+x: W.U64) -> {SCR.le_bytes(x) == Con{b0(x), b7(x)} : List<&2, U32>}:
65 match x:
66 case W.U64{+l, +h}:
67 {==}
68
69def outs(+k: Nat, +c: C8.ChaCha8) -> List<&2, W.U64>:
70 SRC.outputs(~C8.ChaCha8, ~C8.next, k, c)
71
72
73def prefix(+j: Nat, +r: List<&2, U32>, +c: C8.ChaCha8, +d: Nat) -> {SCR.take(j, SCR.append(r, SCR.flat(outs(Nat.add(j, d), c)))) == SCR.take(j, SCR.append(r, SCR.flat(outs(j, c)))) : List<&2, U32>}:
74 match j r:
75 case 0n _:
76 {==}
77 case 1n+i Con{+b, +rest}:
78 Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{b, l}, SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+Nat.add(i, d), c)))), SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+i, c)))),
79 Equal.trans(List<&2, U32>, SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+Nat.add(i, d), c)))), SCR.take(i, SCR.append(rest, SCR.flat(outs(i, c)))), SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+i, c)))),
80 %N.add_succ(i, d) : {SCR.take(i, SCR.append(rest, SCR.flat(outs(_, c)))) == SCR.take(i, SCR.append(rest, SCR.flat(outs(i, c)))) : List<&2, U32>}
81 prefix(i, rest, c, 1n+d),
82 Equal.sym(List<&2, U32>, SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+i, c)))), SCR.take(i, SCR.append(rest, SCR.flat(outs(i, c)))),
83 %Equal.trans(Nat, Nat.add(i, 1n), 1n+Nat.add(i, 0n), 1n+i, N.add_succ(i, 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(i, 0n), i, N.add_zero(i))) : {SCR.take(i, SCR.append(rest, SCR.flat(outs(_, c)))) == SCR.take(i, SCR.append(rest, SCR.flat(outs(i, c)))) : List<&2, U32>}
84 prefix(i, rest, c, 1n))))
85 case 1n+i Nil{}:
86 +x = SRC.fst64(C8.ChaCha8, C8.next(c))
87 +c1 = SRC.snd64(C8.ChaCha8, C8.next(c))
88 %Equal.sym(List<&2, U32>, SCR.le_bytes(x), Con{b0(x), b7(x)}, le_split(x)) : {SCR.take(1n+i, SCR.append(_, SCR.flat(outs(Nat.add(i, d), c1)))) == SCR.take(1n+i, SCR.append(_, SCR.flat(outs(i, c1)))) : List<&2, U32>}
89 Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{b0(x), l}, SCR.take(i, SCR.append(b7(x), SCR.flat(outs(Nat.add(i, d), c1)))), SCR.take(i, SCR.append(b7(x), SCR.flat(outs(i, c1)))), prefix(i, b7(x), c1, d))
90
91
92
93def facc(f: CR.Fill) -> List<&2, U32>:
94 match f:
95 case CR.FS{a, c, p}:
96 a
97
98def fsrc(f: CR.Fill) -> C8.ChaCha8:
99 match f:
100 case CR.FS{a, c, p}:
101 c
102
103def fpend(f: CR.Fill) -> List<&2, U32>:
104 match f:
105 case CR.FS{a, c, p}:
106 p
107
108def step_nil(+j: Nat, +acc: List<&2, U32>, q: W.U64 & C8.ChaCha8) -> {SCR.append(rev(facc(CR.split(acc, q))), SCR.take(j, SCR.append(fpend(CR.split(acc, q)), SCR.flat(outs(j, fsrc(CR.split(acc, q))))))) == SCR.append(rev(acc), SCR.take(1n+j, SCR.flat(Con{SRC.fst64(C8.ChaCha8, q), outs(j, SRC.snd64(C8.ChaCha8, q))}))) : List<&2, U32>}:
109 match q:
110 case Tuple{x, +c1}:
111 match x:
112 case W.U64{+l, +h}:
113 +r7 = {[U32.and(U32.shrn(l, 8n), 255), U32.and(U32.shrn(l, 16n), 255), U32.and(U32.shrn(l, 24n), 255), U32.and(h, 255), U32.and(U32.shrn(h, 8n), 255), U32.and(U32.shrn(h, 16n), 255), U32.and(U32.shrn(h, 24n), 255)] : List<&2, U32>}
114 rev_cons(U32.and(l, 255), acc, SCR.take(j, SCR.append(r7, SCR.flat(outs(j, c1)))))
115
116
117def step(+j: Nat, +f: CR.Fill) -> {SCR.append(rev(facc(CR.take1(f))), SCR.take(j, SCR.append(fpend(CR.take1(f)), SCR.flat(outs(j, fsrc(CR.take1(f))))))) == SCR.append(rev(facc(f)), SCR.take(1n+j, SCR.append(fpend(f), SCR.flat(outs(1n+j, fsrc(f)))))) : List<&2, U32>}:
118 match f:
119 case CR.FS{+acc, +c, +p}:
120 match p:
121 case Con{+b, +rest}:
122 Equal.trans(List<&2, U32>, SCR.append(rev(Con{b, acc}), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))), SCR.append(rev(acc), Con{b, SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))}), SCR.append(rev(acc), Con{b, SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c))))}),
123 rev_cons(b, acc, SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))),
124 Equal.cong(List<&2, U32>, List<&2, U32>, z => SCR.append(rev(acc), Con{b, z}), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))), SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c)))),
125 Equal.sym(List<&2, U32>, SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c)))), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))),
126 %Equal.trans(Nat, Nat.add(j, 1n), 1n+Nat.add(j, 0n), 1n+j, N.add_succ(j, 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(j, 0n), j, N.add_zero(j))) : {SCR.take(j, SCR.append(rest, SCR.flat(outs(_, c)))) == SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))) : List<&2, U32>}
127 prefix(j, rest, c, 1n))))
128 case Nil{}:
129 step_nil(j, acc, C8.next(c))
130
131
132
133def fill_inv(+k: Nat, +f: CR.Fill) -> {rev(facc(CR.fill(k, f))) == SCR.append(rev(facc(f)), SCR.take(k, SCR.append(fpend(f), SCR.flat(outs(k, fsrc(f)))))) : List<&2, U32>}:
134 match k:
135 case 0n:
136 Equal.sym(List<&2, U32>, SCR.append(rev(facc(f)), []), rev(facc(f)), app_nil(rev(facc(f))))
137 case 1n+j:
138 Equal.trans(List<&2, U32>, rev(facc(CR.fill(j, CR.take1(f)))), SCR.append(rev(facc(CR.take1(f))), SCR.take(j, SCR.append(fpend(CR.take1(f)), SCR.flat(outs(j, fsrc(CR.take1(f))))))), SCR.append(rev(facc(f)), SCR.take(1n+j, SCR.append(fpend(f), SCR.flat(outs(1n+j, fsrc(f)))))),
139 fill_inv(j, CR.take1(f)),
140 step(j, f))
141
142def done_bytes(+f: CR.Fill) -> {SCR.fst_bytes(CR.Gen, CR.done(f)) == rev(facc(f)) : List<&2, U32>}:
143 match f:
144 case CR.FS{a, c, p}:
145 {==}
146
147
148def bytes(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>) -> SCR.Random.bytes(n, c, p):
149 Equal.trans(List<&2, U32>, SCR.fst_bytes(CR.Gen, CR.done(CR.fill(n, CR.FS{[], c, p}))), rev(facc(CR.fill(n, CR.FS{[], c, p}))), SCR.take(n, SCR.append(p, SCR.flat(outs(n, c)))),
150 done_bytes(CR.fill(n, CR.FS{[], c, p})),
151 fill_inv(n, CR.FS{[], c, p}))
152
153
154
155def and_true_r(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
156 match b:
157 case True{}:
158 {==}
159 case False{}:
160 {==}
161
162def below_take(+n: Nat, +xs: List<&2, U32>, +h: {SCR.below256(xs) == True{} : Bool}) -> {SCR.below256(SCR.take(n, xs)) == True{} : Bool}:
163 match n xs:
164 case 0n _:
165 {==}
166 case 1n+p Nil{}:
167 {==}
168 case 1n+p Con{+x, +rest}:
169 %Equal.sym(Bool, U32.is_lt(x, 256), True{}, L.and_left(U32.is_lt(x, 256), SCR.below256(rest), h)) : {Bool.and(_, SCR.below256(SCR.take(p, rest))) == True{} : Bool}
170 below_take(p, rest, L.and_right(U32.is_lt(x, 256), SCR.below256(rest), h))
171
172def below_app(+xs: List<&2, U32>, +ys: List<&2, U32>, +hx: {SCR.below256(xs) == True{} : Bool}, +hy: {SCR.below256(ys) == True{} : Bool}) -> {SCR.below256(SCR.append(xs, ys)) == True{} : Bool}:
173 match xs:
174 case Nil{}:
175 hy
176 case Con{+x, +rest}:
177 %Equal.sym(Bool, U32.is_lt(x, 256), True{}, L.and_left(U32.is_lt(x, 256), SCR.below256(rest), hx)) : {Bool.and(_, SCR.below256(SCR.append(rest, ys))) == True{} : Bool}
178 below_app(rest, ys, L.and_right(U32.is_lt(x, 256), SCR.below256(rest), hx), hy)
179
180
181def byte_lt(+y: U32) -> {U32.is_lt(U32.and(y, 255), 256) == True{} : Bool}:
182 Equal.trans(Bool, U32.is_lt(U32.and(y, 255), 256), Nat.is_lt(U32.to_nat(U32.and(y, 255)), 256n), True{},
183 U.is_lt_nat(U32.and(y, 255), 256),
184 %Equal.sym(Nat, U32.to_nat(U32.and(y, 255)), SR.and_bits(32n, U32.to_nat(y), 255n), BI.uand(y, 255)) : {Nat.is_lt(_, 256n) == True{} : Bool}
185 N.le_lt_succ(SR.and_bits(32n, U32.to_nat(y), 255n), 255n, BL.and_le(32n, U32.to_nat(y), 255n)))
186
187def byte_of_lt(+w: U32, +k: Nat) -> {U32.is_lt(SCR.byte_of(w, k), 256) == True{} : Bool}:
188 byte_lt(U32.shrn(w, k))
189
190def le_below(+x: W.U64) -> {SCR.below256(SCR.le_bytes(x)) == True{} : Bool}:
191 match x:
192 case W.U64{+l, +h}:
193 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 0n), 256), True{}, byte_of_lt(l, 0n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 8n), SCR.byte_of(l, 16n), SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
194 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 8n), 256), True{}, byte_of_lt(l, 8n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 16n), SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
195 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 16n), 256), True{}, byte_of_lt(l, 16n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
196 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 24n), 256), True{}, byte_of_lt(l, 24n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
197 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 0n), 256), True{}, byte_of_lt(h, 0n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
198 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 8n), 256), True{}, byte_of_lt(h, 8n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
199 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 16n), 256), True{}, byte_of_lt(h, 16n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 24n)])) == True{} : Bool}
200 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 24n), 256), True{}, byte_of_lt(h, 24n)) : {Bool.and(_, True{}) == True{} : Bool}
201 {==}
202
203def flat_below(+os: List<&2, W.U64>) -> {SCR.below256(SCR.flat(os)) == True{} : Bool}:
204 match os:
205 case Nil{}:
206 {==}
207 case Con{+x, +rest}:
208 below_app(SCR.le_bytes(x), SCR.flat(rest), le_below(x), flat_below(rest))
209
210
211def 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):
212 %Equal.sym(List<&2, U32>, SCR.fst_bytes(CR.Gen, CR.bytes(CR.G{c, p}, n)), SCR.take(n, SCR.append(p, SCR.flat(outs(n, c)))), bytes(n, c, p)) : {SCR.below256(_) == True{} : Bool}
213 below_take(n, SCR.append(p, SCR.flat(outs(n, c))), below_app(p, SCR.flat(outs(n, c)), hp, flat_below(outs(n, c))))