proofs/crypto/sha512/conformance.bend

bend-collections-laws-crypto@1.0.0.0 · 309 lines · 15 definitions

1# Generated by tools/generators/sha512_gen.py; do not edit by hand.
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as F
6
7# src/crypto/sha512/core.bend refines spec/crypto/sha512.bend, the structure
8# of proofs/crypto/sha/conformance.bend (SHA-256) at 64-bit words: one round
9# and the feedforward are equal after opening every word into its halves;
10# the rolling window computes the spec's recurrence over the reverse history;
11# a block's rounds, the blocks, the parsing and the padding follow by
12# induction, each short tail by enumeration.
13
14law step_correct:
15  for +s: T.State
16  for +k: T.Lane
17  for +w: T.Lane
18  {C.step(s, k, w) == F.step(s, k, w) : T.State}
19
20def step_correct(s, k, w):
21  match s k w:
22    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}} T.W{kh, kl} T.W{wh, wl}:
23      {==}
24
25law feedforward_correct:
26  for +x: T.State
27  for +y: T.State
28  {C.feedforward(x, y) == F.feedforward(x, y) : T.State}
29
30def feedforward_correct(x, y):
31  match x y:
32    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}} T.H{T.W{ih, il}, T.W{jh, jl}, T.W{kh, kl}, T.W{lh, ll}, T.W{mh, ml}, T.W{nh, nl}, T.W{oh, ol}, T.W{ph, pl}}:
33      {==}
34
35law next_correct:
36  for +a: T.Lane
37  for +b: T.Lane
38  for +c: T.Lane
39  for +d: T.Lane
40  for +e: T.Lane
41  for +f: T.Lane
42  for +g: T.Lane
43  for +h: T.Lane
44  for +i: T.Lane
45  for +j: T.Lane
46  for +k: T.Lane
47  for +l: T.Lane
48  for +m: T.Lane
49  for +n: T.Lane
50  for +o: T.Lane
51  for +p: T.Lane
52  for +rest: List<&2, T.Lane>
53  {C.next(b, g, o, p) == F.recurrence(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest) : T.Lane}
54
55def next_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest):
56  match b g o p:
57    case T.W{bh, bl} T.W{gh, gl} T.W{oh, ol} T.W{ph, pl}:
58      {==}
59
60law window_rounds_correct:
61  for +q: Nat
62  for +a: T.Lane
63  for +b: T.Lane
64  for +c: T.Lane
65  for +d: T.Lane
66  for +e: T.Lane
67  for +f: T.Lane
68  for +g: T.Lane
69  for +h: T.Lane
70  for +i: T.Lane
71  for +j: T.Lane
72  for +k: T.Lane
73  for +l: T.Lane
74  for +m: T.Lane
75  for +n: T.Lane
76  for +o: T.Lane
77  for +p: T.Lane
78  for +rest: List<&2, T.Lane>
79  for +ks: List<&2, T.Lane>
80  for +s: T.State
81  {C.window_rounds(q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == F.rounds(ks, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(s) : T.State}
82
83def window_rounds_correct(q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s):
84  match q ks:
85    case 0n Nil{}:
86      {==}
87    case 0n x <> xt:
88      {==}
89    case 1n+r Nil{}:
90      {==}
91    case 1n+r x <> xt:
92      %next_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest) :
93        {C.window_rounds(1n+r, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
94          F.rounds(xt, F.extension(r, _ <> a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(F.step(s, x, _)) : T.State}
95      %step_correct(s, x, C.next(b, g, o, p)) :
96        {C.window_rounds(1n+r, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
97          F.rounds(xt, F.extension(r, C.next(b, g, o, p) <> a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(_) : T.State}
98      window_rounds_correct(r, C.next(b, g, o, p), a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p <> rest, xt,
99        C.step(s, x, C.next(b, g, o, p)))
100
101law block_rounds_correct:
102  for +ws: List<&2, T.Lane>
103  for +q: Nat
104  for +a: T.Lane
105  for +b: T.Lane
106  for +c: T.Lane
107  for +d: T.Lane
108  for +e: T.Lane
109  for +f: T.Lane
110  for +g: T.Lane
111  for +h: T.Lane
112  for +i: T.Lane
113  for +j: T.Lane
114  for +k: T.Lane
115  for +l: T.Lane
116  for +m: T.Lane
117  for +n: T.Lane
118  for +o: T.Lane
119  for +p: T.Lane
120  for +rest: List<&2, T.Lane>
121  for +ks: List<&2, T.Lane>
122  for +s: T.State
123  {C.block_rounds(ws, q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) ==
124    F.rounds(ks, List.append(&2, T.Lane, ws, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)))(s) : T.State}
125
126def block_rounds_correct(ws, q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s):
127  match ws ks:
128    case Nil{} _:
129      window_rounds_correct(q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s)
130    case w <> wt Nil{}:
131      {==}
132    case w <> wt x <> xt:
133      %step_correct(s, x, w) :
134        {C.block_rounds(w <> wt, q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
135          F.rounds(xt, List.append(&2, T.Lane, wt, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)))(_) : T.State}
136      block_rounds_correct(wt, q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, xt, C.step(s, x, w))
137
138law compress16_correct:
139  for +a: T.Lane
140  for +b: T.Lane
141  for +c: T.Lane
142  for +d: T.Lane
143  for +e: T.Lane
144  for +f: T.Lane
145  for +g: T.Lane
146  for +h: T.Lane
147  for +i: T.Lane
148  for +j: T.Lane
149  for +k: T.Lane
150  for +l: T.Lane
151  for +m: T.Lane
152  for +n: T.Lane
153  for +o: T.Lane
154  for +p: T.Lane
155  for +q: Nat
156  for +ks: List<&2, T.Lane>
157  for +s: T.State
158  {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == F.compress(F.schedule(q, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]), ks, s) : T.State}
159
160def compress16_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s):
161  +r = F.rounds(ks, List.append(&2, T.Lane, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], F.extension(q, List.reverse(&2, T.Lane, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]))))(s)
162  %feedforward_correct(s, r) : {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == _ : T.State}
163  Equal.cong(T.State, T.State, t => C.feedforward(s, t),
164    C.block_rounds([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, C.Win{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s), r,
165    block_rounds_correct([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a, Nil{}, ks, s))
166
167law blocks_correct:
168  for +ws: List<&2, T.Lane>
169  for +q: Nat
170  for +ks: List<&2, T.Lane>
171  for +s: T.State
172  {C.blocks(ws, q, ks, s) == F.blocks(F.schedules(ws, q), ks)(s) : T.State}
173
174def blocks_correct(ws, q, ks, s):
175  match ws:
176    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest:
177      %compress16_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) :
178        {C.blocks(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, q, ks, s) == F.blocks(F.schedules(rest, q), ks)(_) : T.State}
179      blocks_correct(rest, q, ks, C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s))
180    case Nil{}:
181      {==}
182    case a <> Nil{}:
183      {==}
184    case a <> b <> Nil{}:
185      {==}
186    case a <> b <> c <> Nil{}:
187      {==}
188    case a <> b <> c <> d <> Nil{}:
189      {==}
190    case a <> b <> c <> d <> e <> Nil{}:
191      {==}
192    case a <> b <> c <> d <> e <> f <> Nil{}:
193      {==}
194    case a <> b <> c <> d <> e <> f <> g <> Nil{}:
195      {==}
196    case a <> b <> c <> d <> e <> f <> g <> h <> Nil{}:
197      {==}
198    case a <> b <> c <> d <> e <> f <> g <> h <> i <> Nil{}:
199      {==}
200    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> Nil{}:
201      {==}
202    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> Nil{}:
203      {==}
204    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> Nil{}:
205      {==}
206    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> Nil{}:
207      {==}
208    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> Nil{}:
209      {==}
210    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> Nil{}:
211      {==}
212
213law lanes_correct:
214  for +bytes: List<&2, U32>
215  {C.lanes(bytes) == F.words(bytes) : List<&2, T.Lane>}
216
217def lanes_correct(bytes):
218  match bytes:
219    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
220      %lanes_correct(rest) :
221        {C.lanes(b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest) == T.W{F.decode(b0, b1, b2, b3), F.decode(b4, b5, b6, b7)} <> _ : List<&2, T.Lane>}
222      {==}
223    case Nil{}:
224      {==}
225    case b0 <> Nil{}:
226      {==}
227    case b0 <> b1 <> Nil{}:
228      {==}
229    case b0 <> b1 <> b2 <> Nil{}:
230      {==}
231    case b0 <> b1 <> b2 <> b3 <> Nil{}:
232      {==}
233    case b0 <> b1 <> b2 <> b3 <> b4 <> Nil{}:
234      {==}
235    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> Nil{}:
236      {==}
237    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> Nil{}:
238      {==}
239
240law zeros_correct:
241  for +r: Nat
242  for +fits: Bool
243  {C.zeros_if(r, fits) == F.zero_count_if(r, fits) : Nat}
244
245def zeros_correct(r, fits):
246  match fits:
247    case True{}:
248      {==}
249    case False{}:
250      {==}
251
252law suffix_correct:
253  for +n: Nat
254  {C.suffix(n) == F.padding_suffix(n) : List<&2, U32>}
255
256def suffix_correct(n):
257  %zeros_correct(Nat.mod(n, 128n), Nat.is_le(Nat.mod(n, 128n), 111n)) :
258    {C.suffix(n) == 128 <> List.append(&2, U32, List.replicate(U32, _, 0), F.length_field(n)) : List<&2, U32>}
259  {==}
260
261law digest_correct:
262  for +s: T.State
263  {C.digest_bytes(s) == F.digest_octets(F.digest(s)) : List<&2, U32>}
264
265def digest_correct(s):
266  match s:
267    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}}:
268      {==}
269
270law digest_length:
271  for +s: T.State
272  {List.length(&2, U32, C.digest_bytes(s)) == 64n : Nat}
273
274def digest_length(s):
275  match s:
276    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}}:
277      {==}
278
279law constants_correct:
280  {C.round_constants() == F.constants() : List<&2, T.Lane>}
281
282def constants_correct():
283  {==}
284
285law initial_correct:
286  {C.initial() == F.initial() : T.State}
287
288def initial_correct():
289  {==}
290
291law sha512_correct:
292  for +bytes: List<&2, U32>
293  {C.sha512(bytes) == F.sha512_bytes(bytes) : List<&2, U32>}
294
295def sha512_correct(bytes):
296  +n = List.length(&2, U32, bytes)
297  %suffix_correct(n) :
298    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(F.words(
299      List.append(&2, U32, bytes, _)), 64n), F.constants())(F.initial()))) : List<&2, U32>}
300  +padded = List.append(&2, U32, bytes, C.suffix(n))
301  %lanes_correct(padded) :
302    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(_, 64n), F.constants())(F.initial()))) : List<&2, U32>}
303  %Equal.sym(List<&2, T.Lane>, C.round_constants(), F.constants(), constants_correct()) :
304    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(C.lanes(padded), 64n), _)(F.initial()))) : List<&2, U32>}
305  %Equal.sym(T.State, C.initial(), F.initial(), initial_correct()) :
306    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(C.lanes(padded), 64n), C.round_constants())(_))) : List<&2, U32>}
307  %blocks_correct(C.lanes(padded), 64n, C.round_constants(), C.initial()) :
308    {C.sha512(bytes) == F.digest_octets(F.digest(_)) : List<&2, U32>}
309  digest_correct(C.blocks(C.lanes(padded), 64n, C.round_constants(), C.initial()))