proofs/crypto/blake/blake2s/compress.bend

bend-collections-laws-crypto@1.0.0.0 · 517 lines · 37 definitions

1# Generated by tools/generators/blake2s_gen.py; do not edit.
2# The unrolled compression function refines the list-based RFC 7693 F.
3#
4# The implementation runs ten explicit rounds. A proof-side model runs the
5# same round function r times, selecting the permuted words by round index;
6# for an abstract r both the model and the specification stay symbolic, so
7# every comparison below is between one round at most. The theorem is then
8# instantiated at r = 10, where the model coincides with the implementation.
9import Base
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend as T
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/compress.bend as C
12import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend as R
13
14# The work vector as the RFC list v[0..15], one projection per entry, so
15# that the list has its shape even when the vector is abstract.
16def p0(v: T.Vector) -> U32:
17  match v:
18    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a0
19
20def p1(v: T.Vector) -> U32:
21  match v:
22    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a1
23
24def p2(v: T.Vector) -> U32:
25  match v:
26    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a2
27
28def p3(v: T.Vector) -> U32:
29  match v:
30    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a3
31
32def p4(v: T.Vector) -> U32:
33  match v:
34    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a4
35
36def p5(v: T.Vector) -> U32:
37  match v:
38    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a5
39
40def p6(v: T.Vector) -> U32:
41  match v:
42    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a6
43
44def p7(v: T.Vector) -> U32:
45  match v:
46    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a7
47
48def p8(v: T.Vector) -> U32:
49  match v:
50    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a8
51
52def p9(v: T.Vector) -> U32:
53  match v:
54    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a9
55
56def p10(v: T.Vector) -> U32:
57  match v:
58    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a10
59
60def p11(v: T.Vector) -> U32:
61  match v:
62    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a11
63
64def p12(v: T.Vector) -> U32:
65  match v:
66    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a12
67
68def p13(v: T.Vector) -> U32:
69  match v:
70    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a13
71
72def p14(v: T.Vector) -> U32:
73  match v:
74    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a14
75
76def p15(v: T.Vector) -> U32:
77  match v:
78    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a15
79
80def vec(+v: T.Vector) -> List<&2,U32>:
81  [p0(v),p1(v),p2(v),p3(v),p4(v),p5(v),p6(v),p7(v),p8(v),p9(v),p10(v),p11(v),p12(v),p13(v),p14(v),p15(v)]
82
83# Model: round i of the implementation reads the words in SIGMA[i mod 10] order.
84def round_at(i: Nat, v: T.Vector,+m0: U32,+m1: U32,+m2: U32,+m3: U32,+m4: U32,+m5: U32,+m6: U32,+m7: U32,+m8: U32,+m9: U32,+m10: U32,+m11: U32,+m12: U32,+m13: U32,+m14: U32,+m15: U32) -> T.Vector:
85  match i:
86    case 0n: C.round(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
87    case 1n: C.round(v,m14,m10,m4,m8,m9,m15,m13,m6,m1,m12,m0,m2,m11,m7,m5,m3)
88    case 2n: C.round(v,m11,m8,m12,m0,m5,m2,m15,m13,m10,m14,m3,m6,m7,m1,m9,m4)
89    case 3n: C.round(v,m7,m9,m3,m1,m13,m12,m11,m14,m2,m6,m5,m10,m4,m0,m15,m8)
90    case 4n: C.round(v,m9,m0,m5,m7,m2,m4,m10,m15,m14,m1,m11,m12,m6,m8,m3,m13)
91    case 5n: C.round(v,m2,m12,m6,m10,m0,m11,m8,m3,m4,m13,m7,m5,m15,m14,m1,m9)
92    case 6n: C.round(v,m12,m5,m1,m15,m14,m13,m4,m10,m0,m7,m6,m3,m9,m2,m8,m11)
93    case 7n: C.round(v,m13,m11,m7,m14,m12,m1,m3,m9,m5,m0,m15,m4,m8,m6,m2,m10)
94    case 8n: C.round(v,m6,m15,m14,m9,m11,m3,m0,m8,m12,m2,m13,m7,m1,m4,m10,m5)
95    case 9n: C.round(v,m10,m2,m8,m4,m7,m6,m1,m5,m15,m11,m9,m14,m3,m12,m13,m0)
96    case 10n+p: round_at(p,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
97
98def rounds(n: Nat, +i: Nat, v: T.Vector,+m0: U32,+m1: U32,+m2: U32,+m3: U32,+m4: U32,+m5: U32,+m6: U32,+m7: U32,+m8: U32,+m9: U32,+m10: U32,+m11: U32,+m12: U32,+m13: U32,+m14: U32,+m15: U32) -> T.Vector:
99  match n:
100    case 0n: v
101    case 1n+p: rounds(p,1n+i,round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
102
103def model(+r: Nat, +h: T.State,+m0: U32,+m1: U32,+m2: U32,+m3: U32,+m4: U32,+m5: U32,+m6: U32,+m7: U32,+m8: U32,+m9: U32,+m10: U32,+m11: U32,+m12: U32,+m13: U32,+m14: U32,+m15: U32,t0: U32,t1: U32,last: Bool) -> T.State:
104  C.finish(h,rounds(r,0n,C.init(h,t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15))
105
106law round0_correct:
107  for +v: T.Vector
108  for +m0: U32
109  for +m1: U32
110  for +m2: U32
111  for +m3: U32
112  for +m4: U32
113  for +m5: U32
114  for +m6: U32
115  for +m7: U32
116  for +m8: U32
117  for +m9: U32
118  for +m10: U32
119  for +m11: U32
120  for +m12: U32
121  for +m13: U32
122  for +m14: U32
123  for +m15: U32
124  {vec(round_at(0n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(0n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
125
126def round0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
127  match v:
128    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
129
130law round1_correct:
131  for +v: T.Vector
132  for +m0: U32
133  for +m1: U32
134  for +m2: U32
135  for +m3: U32
136  for +m4: U32
137  for +m5: U32
138  for +m6: U32
139  for +m7: U32
140  for +m8: U32
141  for +m9: U32
142  for +m10: U32
143  for +m11: U32
144  for +m12: U32
145  for +m13: U32
146  for +m14: U32
147  for +m15: U32
148  {vec(round_at(1n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(1n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
149
150def round1_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
151  match v:
152    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
153
154law round2_correct:
155  for +v: T.Vector
156  for +m0: U32
157  for +m1: U32
158  for +m2: U32
159  for +m3: U32
160  for +m4: U32
161  for +m5: U32
162  for +m6: U32
163  for +m7: U32
164  for +m8: U32
165  for +m9: U32
166  for +m10: U32
167  for +m11: U32
168  for +m12: U32
169  for +m13: U32
170  for +m14: U32
171  for +m15: U32
172  {vec(round_at(2n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(2n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
173
174def round2_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
175  match v:
176    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
177
178law round3_correct:
179  for +v: T.Vector
180  for +m0: U32
181  for +m1: U32
182  for +m2: U32
183  for +m3: U32
184  for +m4: U32
185  for +m5: U32
186  for +m6: U32
187  for +m7: U32
188  for +m8: U32
189  for +m9: U32
190  for +m10: U32
191  for +m11: U32
192  for +m12: U32
193  for +m13: U32
194  for +m14: U32
195  for +m15: U32
196  {vec(round_at(3n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(3n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
197
198def round3_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
199  match v:
200    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
201
202law round4_correct:
203  for +v: T.Vector
204  for +m0: U32
205  for +m1: U32
206  for +m2: U32
207  for +m3: U32
208  for +m4: U32
209  for +m5: U32
210  for +m6: U32
211  for +m7: U32
212  for +m8: U32
213  for +m9: U32
214  for +m10: U32
215  for +m11: U32
216  for +m12: U32
217  for +m13: U32
218  for +m14: U32
219  for +m15: U32
220  {vec(round_at(4n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(4n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
221
222def round4_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
223  match v:
224    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
225
226law round5_correct:
227  for +v: T.Vector
228  for +m0: U32
229  for +m1: U32
230  for +m2: U32
231  for +m3: U32
232  for +m4: U32
233  for +m5: U32
234  for +m6: U32
235  for +m7: U32
236  for +m8: U32
237  for +m9: U32
238  for +m10: U32
239  for +m11: U32
240  for +m12: U32
241  for +m13: U32
242  for +m14: U32
243  for +m15: U32
244  {vec(round_at(5n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(5n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
245
246def round5_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
247  match v:
248    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
249
250law round6_correct:
251  for +v: T.Vector
252  for +m0: U32
253  for +m1: U32
254  for +m2: U32
255  for +m3: U32
256  for +m4: U32
257  for +m5: U32
258  for +m6: U32
259  for +m7: U32
260  for +m8: U32
261  for +m9: U32
262  for +m10: U32
263  for +m11: U32
264  for +m12: U32
265  for +m13: U32
266  for +m14: U32
267  for +m15: U32
268  {vec(round_at(6n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(6n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
269
270def round6_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
271  match v:
272    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
273
274law round7_correct:
275  for +v: T.Vector
276  for +m0: U32
277  for +m1: U32
278  for +m2: U32
279  for +m3: U32
280  for +m4: U32
281  for +m5: U32
282  for +m6: U32
283  for +m7: U32
284  for +m8: U32
285  for +m9: U32
286  for +m10: U32
287  for +m11: U32
288  for +m12: U32
289  for +m13: U32
290  for +m14: U32
291  for +m15: U32
292  {vec(round_at(7n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(7n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
293
294def round7_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
295  match v:
296    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
297
298law round8_correct:
299  for +v: T.Vector
300  for +m0: U32
301  for +m1: U32
302  for +m2: U32
303  for +m3: U32
304  for +m4: U32
305  for +m5: U32
306  for +m6: U32
307  for +m7: U32
308  for +m8: U32
309  for +m9: U32
310  for +m10: U32
311  for +m11: U32
312  for +m12: U32
313  for +m13: U32
314  for +m14: U32
315  for +m15: U32
316  {vec(round_at(8n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(8n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
317
318def round8_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
319  match v:
320    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
321
322law round9_correct:
323  for +v: T.Vector
324  for +m0: U32
325  for +m1: U32
326  for +m2: U32
327  for +m3: U32
328  for +m4: U32
329  for +m5: U32
330  for +m6: U32
331  for +m7: U32
332  for +m8: U32
333  for +m9: U32
334  for +m10: U32
335  for +m11: U32
336  for +m12: U32
337  for +m13: U32
338  for +m14: U32
339  for +m15: U32
340  {vec(round_at(9n,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(9n),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
341
342def round9_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
343  match v:
344    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
345
346law round_correct:
347  for +i: Nat
348  for +v: T.Vector
349  for +m0: U32
350  for +m1: U32
351  for +m2: U32
352  for +m3: U32
353  for +m4: U32
354  for +m5: U32
355  for +m6: U32
356  for +m7: U32
357  for +m8: U32
358  for +m9: U32
359  for +m10: U32
360  for +m11: U32
361  for +m12: U32
362  for +m13: U32
363  for +m14: U32
364  for +m15: U32
365  {vec(round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.round(vec(v),R.sigma(i),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
366
367def round_correct(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
368  match i:
369    case 0n: round0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
370    case 1n: round1_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
371    case 2n: round2_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
372    case 3n: round3_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
373    case 4n: round4_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
374    case 5n: round5_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
375    case 6n: round6_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
376    case 7n: round7_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
377    case 8n: round8_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
378    case 9n: round9_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
379    case 10n+p: round_correct(p,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
380
381law rounds_correct:
382  for +n: Nat
383  for +i: Nat
384  for +v: T.Vector
385  for +m0: U32
386  for +m1: U32
387  for +m2: U32
388  for +m3: U32
389  for +m4: U32
390  for +m5: U32
391  for +m6: U32
392  for +m7: U32
393  for +m8: U32
394  for +m9: U32
395  for +m10: U32
396  for +m11: U32
397  for +m12: U32
398  for +m13: U32
399  for +m14: U32
400  for +m15: U32
401  {vec(rounds(n,i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)) == R.rounds(n,i,vec(v),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}
402
403def rounds_correct(n,i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
404  match n:
405    case 0n: {==}
406    case 1n+p:
407      Equal.trans(List<&2,U32>,
408        vec(rounds(p,1n+i,round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
409        R.rounds(p,1n+i,vec(round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),
410        R.rounds(p,1n+i,R.round(vec(v),R.sigma(i),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),
411        rounds_correct(p,1n+i,round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),
412        Equal.cong(List<&2,U32>,List<&2,U32>,x => R.rounds(p,1n+i,x,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),vec(round_at(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),R.round(vec(v),R.sigma(i),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),round_correct(i,v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)))
413
414def fin(h0: U32,h1: U32,h2: U32,h3: U32,h4: U32,h5: U32,h6: U32,h7: U32,+l: List<&2,U32>) -> T.State:
415  T.H{U32.xor(U32.xor(h0,R.get(l,0n)),R.get(l,8n)),U32.xor(U32.xor(h1,R.get(l,1n)),R.get(l,9n)),U32.xor(U32.xor(h2,R.get(l,2n)),R.get(l,10n)),U32.xor(U32.xor(h3,R.get(l,3n)),R.get(l,11n)),U32.xor(U32.xor(h4,R.get(l,4n)),R.get(l,12n)),U32.xor(U32.xor(h5,R.get(l,5n)),R.get(l,13n)),U32.xor(U32.xor(h6,R.get(l,6n)),R.get(l,14n)),U32.xor(U32.xor(h7,R.get(l,7n)),R.get(l,15n))}
416
417law finish_correct:
418  for +h0: U32
419  for +h1: U32
420  for +h2: U32
421  for +h3: U32
422  for +h4: U32
423  for +h5: U32
424  for +h6: U32
425  for +h7: U32
426  for +v: T.Vector
427  {C.finish(T.H{h0,h1,h2,h3,h4,h5,h6,h7},v) == fin(h0,h1,h2,h3,h4,h5,h6,h7,vec(v)) : T.State}
428
429def finish_correct(h0,h1,h2,h3,h4,h5,h6,h7,v):
430  match v:
431    case T.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
432
433law init_correct:
434  for +h0: U32
435  for +h1: U32
436  for +h2: U32
437  for +h3: U32
438  for +h4: U32
439  for +h5: U32
440  for +h6: U32
441  for +h7: U32
442  for +t0: U32
443  for +t1: U32
444  for +last: Bool
445  {vec(C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last)) == R.invert(last,[h0,h1,h2,h3,h4,h5,h6,h7,1779033703,3144134277,1013904242,2773480762,U32.xor(1359893119,t0),U32.xor(2600822924,t1),528734635,1541459225]) : List<&2,U32>}
446
447def init_correct(h0,h1,h2,h3,h4,h5,h6,h7,t0,t1,last):
448  match last:
449    case True{}: {==}
450    case False{}: {==}
451
452law model_correct:
453  for +r: Nat
454  for +h: T.State
455  for +m0: U32
456  for +m1: U32
457  for +m2: U32
458  for +m3: U32
459  for +m4: U32
460  for +m5: U32
461  for +m6: U32
462  for +m7: U32
463  for +m8: U32
464  for +m9: U32
465  for +m10: U32
466  for +m11: U32
467  for +m12: U32
468  for +m13: U32
469  for +m14: U32
470  for +m15: U32
471  for +t0: U32
472  for +t1: U32
473  for +last: Bool
474  {model(r,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last) == R.compress(r,h,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last) : T.State}
475
476def model_correct(r,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last):
477  match h:
478    case T.H{h0,h1,h2,h3,h4,h5,h6,h7}:
479      Equal.trans(T.State,
480        C.finish(T.H{h0,h1,h2,h3,h4,h5,h6,h7},rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
481        fin(h0,h1,h2,h3,h4,h5,h6,h7,vec(rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15))),
482        R.compress(r,T.H{h0,h1,h2,h3,h4,h5,h6,h7},[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last),
483        finish_correct(h0,h1,h2,h3,h4,h5,h6,h7,rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
484        Equal.trans(T.State,
485          fin(h0,h1,h2,h3,h4,h5,h6,h7,vec(rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15))),
486          fin(h0,h1,h2,h3,h4,h5,h6,h7,R.rounds(r,0n,vec(C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15])),
487          R.compress(r,T.H{h0,h1,h2,h3,h4,h5,h6,h7},[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last),
488          Equal.cong(List<&2,U32>,T.State,l => fin(h0,h1,h2,h3,h4,h5,h6,h7,l),vec(rounds(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),R.rounds(r,0n,vec(C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]),rounds_correct(r,0n,C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
489          Equal.cong(List<&2,U32>,T.State,l => fin(h0,h1,h2,h3,h4,h5,h6,h7,R.rounds(r,0n,l,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15])),vec(C.init(T.H{h0,h1,h2,h3,h4,h5,h6,h7},t0,t1,last)),R.invert(last,[h0,h1,h2,h3,h4,h5,h6,h7,1779033703,3144134277,1013904242,2773480762,U32.xor(1359893119,t0),U32.xor(2600822924,t1),528734635,1541459225]),init_correct(h0,h1,h2,h3,h4,h5,h6,h7,t0,t1,last))))
490
491# F as implemented (ten unrolled rounds) is F of the specification with r = 10.
492law compress_correct:
493  for +h: T.State
494  for +m0: U32
495  for +m1: U32
496  for +m2: U32
497  for +m3: U32
498  for +m4: U32
499  for +m5: U32
500  for +m6: U32
501  for +m7: U32
502  for +m8: U32
503  for +m9: U32
504  for +m10: U32
505  for +m11: U32
506  for +m12: U32
507  for +m13: U32
508  for +m14: U32
509  for +m15: U32
510  for +t0: U32
511  for +t1: U32
512  for +last: Bool
513  {C.compress(h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last) == R.compress(10n,h,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last) : T.State}
514
515def compress_correct(h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last):
516  Equal.trans(T.State,C.compress(h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last),model(10n,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last),R.compress(10n,h,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],t0,t1,last),
517    {==},model_correct(10n,h,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,t0,t1,last))