proofs/crypto/aes/sbox.bend
bend-collections-laws-crypto@1.0.0.0 · 1,698 lines · 7 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/sbox.bend as B
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
4
5
6
7
8law sbox_byte_bits:
9 for +b0: Bool
10 for +b1: Bool
11 for +b2: Bool
12 for +b3: Bool
13 for +b4: Bool
14 for +b5: Bool
15 for +b6: Bool
16 for +b7: Bool
17 {B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}
18
19def sbox_byte_bits(b0, b1, b2, b3, b4, b5, b6, b7):
20 match b0 b1 b2 b3 b4 b5 b6 b7:
21 case False{} False{} False{} False{} False{} False{} False{} False{}:
22 {==}
23 case True{} False{} False{} False{} False{} False{} False{} False{}:
24 {==}
25 case False{} True{} False{} False{} False{} False{} False{} False{}:
26 {==}
27 case True{} True{} False{} False{} False{} False{} False{} False{}:
28 {==}
29 case False{} False{} True{} False{} False{} False{} False{} False{}:
30 {==}
31 case True{} False{} True{} False{} False{} False{} False{} False{}:
32 {==}
33 case False{} True{} True{} False{} False{} False{} False{} False{}:
34 {==}
35 case True{} True{} True{} False{} False{} False{} False{} False{}:
36 {==}
37 case False{} False{} False{} True{} False{} False{} False{} False{}:
38 {==}
39 case True{} False{} False{} True{} False{} False{} False{} False{}:
40 {==}
41 case False{} True{} False{} True{} False{} False{} False{} False{}:
42 {==}
43 case True{} True{} False{} True{} False{} False{} False{} False{}:
44 {==}
45 case False{} False{} True{} True{} False{} False{} False{} False{}:
46 {==}
47 case True{} False{} True{} True{} False{} False{} False{} False{}:
48 {==}
49 case False{} True{} True{} True{} False{} False{} False{} False{}:
50 {==}
51 case True{} True{} True{} True{} False{} False{} False{} False{}:
52 {==}
53 case False{} False{} False{} False{} True{} False{} False{} False{}:
54 {==}
55 case True{} False{} False{} False{} True{} False{} False{} False{}:
56 {==}
57 case False{} True{} False{} False{} True{} False{} False{} False{}:
58 {==}
59 case True{} True{} False{} False{} True{} False{} False{} False{}:
60 {==}
61 case False{} False{} True{} False{} True{} False{} False{} False{}:
62 {==}
63 case True{} False{} True{} False{} True{} False{} False{} False{}:
64 {==}
65 case False{} True{} True{} False{} True{} False{} False{} False{}:
66 {==}
67 case True{} True{} True{} False{} True{} False{} False{} False{}:
68 {==}
69 case False{} False{} False{} True{} True{} False{} False{} False{}:
70 {==}
71 case True{} False{} False{} True{} True{} False{} False{} False{}:
72 {==}
73 case False{} True{} False{} True{} True{} False{} False{} False{}:
74 {==}
75 case True{} True{} False{} True{} True{} False{} False{} False{}:
76 {==}
77 case False{} False{} True{} True{} True{} False{} False{} False{}:
78 {==}
79 case True{} False{} True{} True{} True{} False{} False{} False{}:
80 {==}
81 case False{} True{} True{} True{} True{} False{} False{} False{}:
82 {==}
83 case True{} True{} True{} True{} True{} False{} False{} False{}:
84 {==}
85 case False{} False{} False{} False{} False{} True{} False{} False{}:
86 {==}
87 case True{} False{} False{} False{} False{} True{} False{} False{}:
88 {==}
89 case False{} True{} False{} False{} False{} True{} False{} False{}:
90 {==}
91 case True{} True{} False{} False{} False{} True{} False{} False{}:
92 {==}
93 case False{} False{} True{} False{} False{} True{} False{} False{}:
94 {==}
95 case True{} False{} True{} False{} False{} True{} False{} False{}:
96 {==}
97 case False{} True{} True{} False{} False{} True{} False{} False{}:
98 {==}
99 case True{} True{} True{} False{} False{} True{} False{} False{}:
100 {==}
101 case False{} False{} False{} True{} False{} True{} False{} False{}:
102 {==}
103 case True{} False{} False{} True{} False{} True{} False{} False{}:
104 {==}
105 case False{} True{} False{} True{} False{} True{} False{} False{}:
106 {==}
107 case True{} True{} False{} True{} False{} True{} False{} False{}:
108 {==}
109 case False{} False{} True{} True{} False{} True{} False{} False{}:
110 {==}
111 case True{} False{} True{} True{} False{} True{} False{} False{}:
112 {==}
113 case False{} True{} True{} True{} False{} True{} False{} False{}:
114 {==}
115 case True{} True{} True{} True{} False{} True{} False{} False{}:
116 {==}
117 case False{} False{} False{} False{} True{} True{} False{} False{}:
118 {==}
119 case True{} False{} False{} False{} True{} True{} False{} False{}:
120 {==}
121 case False{} True{} False{} False{} True{} True{} False{} False{}:
122 {==}
123 case True{} True{} False{} False{} True{} True{} False{} False{}:
124 {==}
125 case False{} False{} True{} False{} True{} True{} False{} False{}:
126 {==}
127 case True{} False{} True{} False{} True{} True{} False{} False{}:
128 {==}
129 case False{} True{} True{} False{} True{} True{} False{} False{}:
130 {==}
131 case True{} True{} True{} False{} True{} True{} False{} False{}:
132 {==}
133 case False{} False{} False{} True{} True{} True{} False{} False{}:
134 {==}
135 case True{} False{} False{} True{} True{} True{} False{} False{}:
136 {==}
137 case False{} True{} False{} True{} True{} True{} False{} False{}:
138 {==}
139 case True{} True{} False{} True{} True{} True{} False{} False{}:
140 {==}
141 case False{} False{} True{} True{} True{} True{} False{} False{}:
142 {==}
143 case True{} False{} True{} True{} True{} True{} False{} False{}:
144 {==}
145 case False{} True{} True{} True{} True{} True{} False{} False{}:
146 {==}
147 case True{} True{} True{} True{} True{} True{} False{} False{}:
148 {==}
149 case False{} False{} False{} False{} False{} False{} True{} False{}:
150 {==}
151 case True{} False{} False{} False{} False{} False{} True{} False{}:
152 {==}
153 case False{} True{} False{} False{} False{} False{} True{} False{}:
154 {==}
155 case True{} True{} False{} False{} False{} False{} True{} False{}:
156 {==}
157 case False{} False{} True{} False{} False{} False{} True{} False{}:
158 {==}
159 case True{} False{} True{} False{} False{} False{} True{} False{}:
160 {==}
161 case False{} True{} True{} False{} False{} False{} True{} False{}:
162 {==}
163 case True{} True{} True{} False{} False{} False{} True{} False{}:
164 {==}
165 case False{} False{} False{} True{} False{} False{} True{} False{}:
166 {==}
167 case True{} False{} False{} True{} False{} False{} True{} False{}:
168 {==}
169 case False{} True{} False{} True{} False{} False{} True{} False{}:
170 {==}
171 case True{} True{} False{} True{} False{} False{} True{} False{}:
172 {==}
173 case False{} False{} True{} True{} False{} False{} True{} False{}:
174 {==}
175 case True{} False{} True{} True{} False{} False{} True{} False{}:
176 {==}
177 case False{} True{} True{} True{} False{} False{} True{} False{}:
178 {==}
179 case True{} True{} True{} True{} False{} False{} True{} False{}:
180 {==}
181 case False{} False{} False{} False{} True{} False{} True{} False{}:
182 {==}
183 case True{} False{} False{} False{} True{} False{} True{} False{}:
184 {==}
185 case False{} True{} False{} False{} True{} False{} True{} False{}:
186 {==}
187 case True{} True{} False{} False{} True{} False{} True{} False{}:
188 {==}
189 case False{} False{} True{} False{} True{} False{} True{} False{}:
190 {==}
191 case True{} False{} True{} False{} True{} False{} True{} False{}:
192 {==}
193 case False{} True{} True{} False{} True{} False{} True{} False{}:
194 {==}
195 case True{} True{} True{} False{} True{} False{} True{} False{}:
196 {==}
197 case False{} False{} False{} True{} True{} False{} True{} False{}:
198 {==}
199 case True{} False{} False{} True{} True{} False{} True{} False{}:
200 {==}
201 case False{} True{} False{} True{} True{} False{} True{} False{}:
202 {==}
203 case True{} True{} False{} True{} True{} False{} True{} False{}:
204 {==}
205 case False{} False{} True{} True{} True{} False{} True{} False{}:
206 {==}
207 case True{} False{} True{} True{} True{} False{} True{} False{}:
208 {==}
209 case False{} True{} True{} True{} True{} False{} True{} False{}:
210 {==}
211 case True{} True{} True{} True{} True{} False{} True{} False{}:
212 {==}
213 case False{} False{} False{} False{} False{} True{} True{} False{}:
214 {==}
215 case True{} False{} False{} False{} False{} True{} True{} False{}:
216 {==}
217 case False{} True{} False{} False{} False{} True{} True{} False{}:
218 {==}
219 case True{} True{} False{} False{} False{} True{} True{} False{}:
220 {==}
221 case False{} False{} True{} False{} False{} True{} True{} False{}:
222 {==}
223 case True{} False{} True{} False{} False{} True{} True{} False{}:
224 {==}
225 case False{} True{} True{} False{} False{} True{} True{} False{}:
226 {==}
227 case True{} True{} True{} False{} False{} True{} True{} False{}:
228 {==}
229 case False{} False{} False{} True{} False{} True{} True{} False{}:
230 {==}
231 case True{} False{} False{} True{} False{} True{} True{} False{}:
232 {==}
233 case False{} True{} False{} True{} False{} True{} True{} False{}:
234 {==}
235 case True{} True{} False{} True{} False{} True{} True{} False{}:
236 {==}
237 case False{} False{} True{} True{} False{} True{} True{} False{}:
238 {==}
239 case True{} False{} True{} True{} False{} True{} True{} False{}:
240 {==}
241 case False{} True{} True{} True{} False{} True{} True{} False{}:
242 {==}
243 case True{} True{} True{} True{} False{} True{} True{} False{}:
244 {==}
245 case False{} False{} False{} False{} True{} True{} True{} False{}:
246 {==}
247 case True{} False{} False{} False{} True{} True{} True{} False{}:
248 {==}
249 case False{} True{} False{} False{} True{} True{} True{} False{}:
250 {==}
251 case True{} True{} False{} False{} True{} True{} True{} False{}:
252 {==}
253 case False{} False{} True{} False{} True{} True{} True{} False{}:
254 {==}
255 case True{} False{} True{} False{} True{} True{} True{} False{}:
256 {==}
257 case False{} True{} True{} False{} True{} True{} True{} False{}:
258 {==}
259 case True{} True{} True{} False{} True{} True{} True{} False{}:
260 {==}
261 case False{} False{} False{} True{} True{} True{} True{} False{}:
262 {==}
263 case True{} False{} False{} True{} True{} True{} True{} False{}:
264 {==}
265 case False{} True{} False{} True{} True{} True{} True{} False{}:
266 {==}
267 case True{} True{} False{} True{} True{} True{} True{} False{}:
268 {==}
269 case False{} False{} True{} True{} True{} True{} True{} False{}:
270 {==}
271 case True{} False{} True{} True{} True{} True{} True{} False{}:
272 {==}
273 case False{} True{} True{} True{} True{} True{} True{} False{}:
274 {==}
275 case True{} True{} True{} True{} True{} True{} True{} False{}:
276 {==}
277 case False{} False{} False{} False{} False{} False{} False{} True{}:
278 {==}
279 case True{} False{} False{} False{} False{} False{} False{} True{}:
280 {==}
281 case False{} True{} False{} False{} False{} False{} False{} True{}:
282 {==}
283 case True{} True{} False{} False{} False{} False{} False{} True{}:
284 {==}
285 case False{} False{} True{} False{} False{} False{} False{} True{}:
286 {==}
287 case True{} False{} True{} False{} False{} False{} False{} True{}:
288 {==}
289 case False{} True{} True{} False{} False{} False{} False{} True{}:
290 {==}
291 case True{} True{} True{} False{} False{} False{} False{} True{}:
292 {==}
293 case False{} False{} False{} True{} False{} False{} False{} True{}:
294 {==}
295 case True{} False{} False{} True{} False{} False{} False{} True{}:
296 {==}
297 case False{} True{} False{} True{} False{} False{} False{} True{}:
298 {==}
299 case True{} True{} False{} True{} False{} False{} False{} True{}:
300 {==}
301 case False{} False{} True{} True{} False{} False{} False{} True{}:
302 {==}
303 case True{} False{} True{} True{} False{} False{} False{} True{}:
304 {==}
305 case False{} True{} True{} True{} False{} False{} False{} True{}:
306 {==}
307 case True{} True{} True{} True{} False{} False{} False{} True{}:
308 {==}
309 case False{} False{} False{} False{} True{} False{} False{} True{}:
310 {==}
311 case True{} False{} False{} False{} True{} False{} False{} True{}:
312 {==}
313 case False{} True{} False{} False{} True{} False{} False{} True{}:
314 {==}
315 case True{} True{} False{} False{} True{} False{} False{} True{}:
316 {==}
317 case False{} False{} True{} False{} True{} False{} False{} True{}:
318 {==}
319 case True{} False{} True{} False{} True{} False{} False{} True{}:
320 {==}
321 case False{} True{} True{} False{} True{} False{} False{} True{}:
322 {==}
323 case True{} True{} True{} False{} True{} False{} False{} True{}:
324 {==}
325 case False{} False{} False{} True{} True{} False{} False{} True{}:
326 {==}
327 case True{} False{} False{} True{} True{} False{} False{} True{}:
328 {==}
329 case False{} True{} False{} True{} True{} False{} False{} True{}:
330 {==}
331 case True{} True{} False{} True{} True{} False{} False{} True{}:
332 {==}
333 case False{} False{} True{} True{} True{} False{} False{} True{}:
334 {==}
335 case True{} False{} True{} True{} True{} False{} False{} True{}:
336 {==}
337 case False{} True{} True{} True{} True{} False{} False{} True{}:
338 {==}
339 case True{} True{} True{} True{} True{} False{} False{} True{}:
340 {==}
341 case False{} False{} False{} False{} False{} True{} False{} True{}:
342 {==}
343 case True{} False{} False{} False{} False{} True{} False{} True{}:
344 {==}
345 case False{} True{} False{} False{} False{} True{} False{} True{}:
346 {==}
347 case True{} True{} False{} False{} False{} True{} False{} True{}:
348 {==}
349 case False{} False{} True{} False{} False{} True{} False{} True{}:
350 {==}
351 case True{} False{} True{} False{} False{} True{} False{} True{}:
352 {==}
353 case False{} True{} True{} False{} False{} True{} False{} True{}:
354 {==}
355 case True{} True{} True{} False{} False{} True{} False{} True{}:
356 {==}
357 case False{} False{} False{} True{} False{} True{} False{} True{}:
358 {==}
359 case True{} False{} False{} True{} False{} True{} False{} True{}:
360 {==}
361 case False{} True{} False{} True{} False{} True{} False{} True{}:
362 {==}
363 case True{} True{} False{} True{} False{} True{} False{} True{}:
364 {==}
365 case False{} False{} True{} True{} False{} True{} False{} True{}:
366 {==}
367 case True{} False{} True{} True{} False{} True{} False{} True{}:
368 {==}
369 case False{} True{} True{} True{} False{} True{} False{} True{}:
370 {==}
371 case True{} True{} True{} True{} False{} True{} False{} True{}:
372 {==}
373 case False{} False{} False{} False{} True{} True{} False{} True{}:
374 {==}
375 case True{} False{} False{} False{} True{} True{} False{} True{}:
376 {==}
377 case False{} True{} False{} False{} True{} True{} False{} True{}:
378 {==}
379 case True{} True{} False{} False{} True{} True{} False{} True{}:
380 {==}
381 case False{} False{} True{} False{} True{} True{} False{} True{}:
382 {==}
383 case True{} False{} True{} False{} True{} True{} False{} True{}:
384 {==}
385 case False{} True{} True{} False{} True{} True{} False{} True{}:
386 {==}
387 case True{} True{} True{} False{} True{} True{} False{} True{}:
388 {==}
389 case False{} False{} False{} True{} True{} True{} False{} True{}:
390 {==}
391 case True{} False{} False{} True{} True{} True{} False{} True{}:
392 {==}
393 case False{} True{} False{} True{} True{} True{} False{} True{}:
394 {==}
395 case True{} True{} False{} True{} True{} True{} False{} True{}:
396 {==}
397 case False{} False{} True{} True{} True{} True{} False{} True{}:
398 {==}
399 case True{} False{} True{} True{} True{} True{} False{} True{}:
400 {==}
401 case False{} True{} True{} True{} True{} True{} False{} True{}:
402 {==}
403 case True{} True{} True{} True{} True{} True{} False{} True{}:
404 {==}
405 case False{} False{} False{} False{} False{} False{} True{} True{}:
406 {==}
407 case True{} False{} False{} False{} False{} False{} True{} True{}:
408 {==}
409 case False{} True{} False{} False{} False{} False{} True{} True{}:
410 {==}
411 case True{} True{} False{} False{} False{} False{} True{} True{}:
412 {==}
413 case False{} False{} True{} False{} False{} False{} True{} True{}:
414 {==}
415 case True{} False{} True{} False{} False{} False{} True{} True{}:
416 {==}
417 case False{} True{} True{} False{} False{} False{} True{} True{}:
418 {==}
419 case True{} True{} True{} False{} False{} False{} True{} True{}:
420 {==}
421 case False{} False{} False{} True{} False{} False{} True{} True{}:
422 {==}
423 case True{} False{} False{} True{} False{} False{} True{} True{}:
424 {==}
425 case False{} True{} False{} True{} False{} False{} True{} True{}:
426 {==}
427 case True{} True{} False{} True{} False{} False{} True{} True{}:
428 {==}
429 case False{} False{} True{} True{} False{} False{} True{} True{}:
430 {==}
431 case True{} False{} True{} True{} False{} False{} True{} True{}:
432 {==}
433 case False{} True{} True{} True{} False{} False{} True{} True{}:
434 {==}
435 case True{} True{} True{} True{} False{} False{} True{} True{}:
436 {==}
437 case False{} False{} False{} False{} True{} False{} True{} True{}:
438 {==}
439 case True{} False{} False{} False{} True{} False{} True{} True{}:
440 {==}
441 case False{} True{} False{} False{} True{} False{} True{} True{}:
442 {==}
443 case True{} True{} False{} False{} True{} False{} True{} True{}:
444 {==}
445 case False{} False{} True{} False{} True{} False{} True{} True{}:
446 {==}
447 case True{} False{} True{} False{} True{} False{} True{} True{}:
448 {==}
449 case False{} True{} True{} False{} True{} False{} True{} True{}:
450 {==}
451 case True{} True{} True{} False{} True{} False{} True{} True{}:
452 {==}
453 case False{} False{} False{} True{} True{} False{} True{} True{}:
454 {==}
455 case True{} False{} False{} True{} True{} False{} True{} True{}:
456 {==}
457 case False{} True{} False{} True{} True{} False{} True{} True{}:
458 {==}
459 case True{} True{} False{} True{} True{} False{} True{} True{}:
460 {==}
461 case False{} False{} True{} True{} True{} False{} True{} True{}:
462 {==}
463 case True{} False{} True{} True{} True{} False{} True{} True{}:
464 {==}
465 case False{} True{} True{} True{} True{} False{} True{} True{}:
466 {==}
467 case True{} True{} True{} True{} True{} False{} True{} True{}:
468 {==}
469 case False{} False{} False{} False{} False{} True{} True{} True{}:
470 {==}
471 case True{} False{} False{} False{} False{} True{} True{} True{}:
472 {==}
473 case False{} True{} False{} False{} False{} True{} True{} True{}:
474 {==}
475 case True{} True{} False{} False{} False{} True{} True{} True{}:
476 {==}
477 case False{} False{} True{} False{} False{} True{} True{} True{}:
478 {==}
479 case True{} False{} True{} False{} False{} True{} True{} True{}:
480 {==}
481 case False{} True{} True{} False{} False{} True{} True{} True{}:
482 {==}
483 case True{} True{} True{} False{} False{} True{} True{} True{}:
484 {==}
485 case False{} False{} False{} True{} False{} True{} True{} True{}:
486 {==}
487 case True{} False{} False{} True{} False{} True{} True{} True{}:
488 {==}
489 case False{} True{} False{} True{} False{} True{} True{} True{}:
490 {==}
491 case True{} True{} False{} True{} False{} True{} True{} True{}:
492 {==}
493 case False{} False{} True{} True{} False{} True{} True{} True{}:
494 {==}
495 case True{} False{} True{} True{} False{} True{} True{} True{}:
496 {==}
497 case False{} True{} True{} True{} False{} True{} True{} True{}:
498 {==}
499 case True{} True{} True{} True{} False{} True{} True{} True{}:
500 {==}
501 case False{} False{} False{} False{} True{} True{} True{} True{}:
502 {==}
503 case True{} False{} False{} False{} True{} True{} True{} True{}:
504 {==}
505 case False{} True{} False{} False{} True{} True{} True{} True{}:
506 {==}
507 case True{} True{} False{} False{} True{} True{} True{} True{}:
508 {==}
509 case False{} False{} True{} False{} True{} True{} True{} True{}:
510 {==}
511 case True{} False{} True{} False{} True{} True{} True{} True{}:
512 {==}
513 case False{} True{} True{} False{} True{} True{} True{} True{}:
514 {==}
515 case True{} True{} True{} False{} True{} True{} True{} True{}:
516 {==}
517 case False{} False{} False{} True{} True{} True{} True{} True{}:
518 {==}
519 case True{} False{} False{} True{} True{} True{} True{} True{}:
520 {==}
521 case False{} True{} False{} True{} True{} True{} True{} True{}:
522 {==}
523 case True{} True{} False{} True{} True{} True{} True{} True{}:
524 {==}
525 case False{} False{} True{} True{} True{} True{} True{} True{}:
526 {==}
527 case True{} False{} True{} True{} True{} True{} True{} True{}:
528 {==}
529 case False{} True{} True{} True{} True{} True{} True{} True{}:
530 {==}
531 case True{} True{} True{} True{} True{} True{} True{} True{}:
532 {==}
533
534law sbox_bits:
535 for +b0: Bool
536 for +b1: Bool
537 for +b2: Bool
538 for +b3: Bool
539 for +b4: Bool
540 for +b5: Bool
541 for +b6: Bool
542 for +b7: Bool
543 for +b8: Bool
544 for +b9: Bool
545 for +b10: Bool
546 for +b11: Bool
547 for +b12: Bool
548 for +b13: Bool
549 for +b14: Bool
550 for +b15: Bool
551 for +b16: Bool
552 for +b17: Bool
553 for +b18: Bool
554 for +b19: Bool
555 for +b20: Bool
556 for +b21: Bool
557 for +b22: Bool
558 for +b23: Bool
559 for +b24: Bool
560 for +b25: Bool
561 for +b26: Bool
562 for +b27: Bool
563 for +b28: Bool
564 for +b29: Bool
565 for +b30: Bool
566 for +b31: Bool
567 {B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}
568
569def sbox_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31):
570 Equal.trans(U32, B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), {==},
571 Equal.trans(U32, B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), sbox_byte_bits(b0, b1, b2, b3, b4, b5, b6, b7), {==}))
572
573law sbox_ok:
574 for +x: U32
575 {B.sbox(x) == S.sbox(x) : U32}
576
577def sbox_ok(x):
578 match x:
579 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
580 sbox_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31)
581
582law xtime_bits:
583 for b0: Bool
584 for b1: Bool
585 for b2: Bool
586 for b3: Bool
587 for b4: Bool
588 for b5: Bool
589 for b6: Bool
590 for b7: Bool
591 for b8: Bool
592 for b9: Bool
593 for b10: Bool
594 for b11: Bool
595 for b12: Bool
596 for b13: Bool
597 for b14: Bool
598 for b15: Bool
599 for b16: Bool
600 for b17: Bool
601 for b18: Bool
602 for b19: Bool
603 for b20: Bool
604 for b21: Bool
605 for b22: Bool
606 for b23: Bool
607 for b24: Bool
608 for b25: Bool
609 for b26: Bool
610 for b27: Bool
611 for b28: Bool
612 for b29: Bool
613 for b30: Bool
614 for b31: Bool
615 {B.xtime(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == S.mul(2, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}
616
617def xtime_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31):
618 match b0 b1 b2 b3 b4 b5 b6 b7:
619 case False{} False{} False{} False{} False{} False{} False{} False{}:
620 {==}
621 case True{} False{} False{} False{} False{} False{} False{} False{}:
622 {==}
623 case False{} True{} False{} False{} False{} False{} False{} False{}:
624 {==}
625 case True{} True{} False{} False{} False{} False{} False{} False{}:
626 {==}
627 case False{} False{} True{} False{} False{} False{} False{} False{}:
628 {==}
629 case True{} False{} True{} False{} False{} False{} False{} False{}:
630 {==}
631 case False{} True{} True{} False{} False{} False{} False{} False{}:
632 {==}
633 case True{} True{} True{} False{} False{} False{} False{} False{}:
634 {==}
635 case False{} False{} False{} True{} False{} False{} False{} False{}:
636 {==}
637 case True{} False{} False{} True{} False{} False{} False{} False{}:
638 {==}
639 case False{} True{} False{} True{} False{} False{} False{} False{}:
640 {==}
641 case True{} True{} False{} True{} False{} False{} False{} False{}:
642 {==}
643 case False{} False{} True{} True{} False{} False{} False{} False{}:
644 {==}
645 case True{} False{} True{} True{} False{} False{} False{} False{}:
646 {==}
647 case False{} True{} True{} True{} False{} False{} False{} False{}:
648 {==}
649 case True{} True{} True{} True{} False{} False{} False{} False{}:
650 {==}
651 case False{} False{} False{} False{} True{} False{} False{} False{}:
652 {==}
653 case True{} False{} False{} False{} True{} False{} False{} False{}:
654 {==}
655 case False{} True{} False{} False{} True{} False{} False{} False{}:
656 {==}
657 case True{} True{} False{} False{} True{} False{} False{} False{}:
658 {==}
659 case False{} False{} True{} False{} True{} False{} False{} False{}:
660 {==}
661 case True{} False{} True{} False{} True{} False{} False{} False{}:
662 {==}
663 case False{} True{} True{} False{} True{} False{} False{} False{}:
664 {==}
665 case True{} True{} True{} False{} True{} False{} False{} False{}:
666 {==}
667 case False{} False{} False{} True{} True{} False{} False{} False{}:
668 {==}
669 case True{} False{} False{} True{} True{} False{} False{} False{}:
670 {==}
671 case False{} True{} False{} True{} True{} False{} False{} False{}:
672 {==}
673 case True{} True{} False{} True{} True{} False{} False{} False{}:
674 {==}
675 case False{} False{} True{} True{} True{} False{} False{} False{}:
676 {==}
677 case True{} False{} True{} True{} True{} False{} False{} False{}:
678 {==}
679 case False{} True{} True{} True{} True{} False{} False{} False{}:
680 {==}
681 case True{} True{} True{} True{} True{} False{} False{} False{}:
682 {==}
683 case False{} False{} False{} False{} False{} True{} False{} False{}:
684 {==}
685 case True{} False{} False{} False{} False{} True{} False{} False{}:
686 {==}
687 case False{} True{} False{} False{} False{} True{} False{} False{}:
688 {==}
689 case True{} True{} False{} False{} False{} True{} False{} False{}:
690 {==}
691 case False{} False{} True{} False{} False{} True{} False{} False{}:
692 {==}
693 case True{} False{} True{} False{} False{} True{} False{} False{}:
694 {==}
695 case False{} True{} True{} False{} False{} True{} False{} False{}:
696 {==}
697 case True{} True{} True{} False{} False{} True{} False{} False{}:
698 {==}
699 case False{} False{} False{} True{} False{} True{} False{} False{}:
700 {==}
701 case True{} False{} False{} True{} False{} True{} False{} False{}:
702 {==}
703 case False{} True{} False{} True{} False{} True{} False{} False{}:
704 {==}
705 case True{} True{} False{} True{} False{} True{} False{} False{}:
706 {==}
707 case False{} False{} True{} True{} False{} True{} False{} False{}:
708 {==}
709 case True{} False{} True{} True{} False{} True{} False{} False{}:
710 {==}
711 case False{} True{} True{} True{} False{} True{} False{} False{}:
712 {==}
713 case True{} True{} True{} True{} False{} True{} False{} False{}:
714 {==}
715 case False{} False{} False{} False{} True{} True{} False{} False{}:
716 {==}
717 case True{} False{} False{} False{} True{} True{} False{} False{}:
718 {==}
719 case False{} True{} False{} False{} True{} True{} False{} False{}:
720 {==}
721 case True{} True{} False{} False{} True{} True{} False{} False{}:
722 {==}
723 case False{} False{} True{} False{} True{} True{} False{} False{}:
724 {==}
725 case True{} False{} True{} False{} True{} True{} False{} False{}:
726 {==}
727 case False{} True{} True{} False{} True{} True{} False{} False{}:
728 {==}
729 case True{} True{} True{} False{} True{} True{} False{} False{}:
730 {==}
731 case False{} False{} False{} True{} True{} True{} False{} False{}:
732 {==}
733 case True{} False{} False{} True{} True{} True{} False{} False{}:
734 {==}
735 case False{} True{} False{} True{} True{} True{} False{} False{}:
736 {==}
737 case True{} True{} False{} True{} True{} True{} False{} False{}:
738 {==}
739 case False{} False{} True{} True{} True{} True{} False{} False{}:
740 {==}
741 case True{} False{} True{} True{} True{} True{} False{} False{}:
742 {==}
743 case False{} True{} True{} True{} True{} True{} False{} False{}:
744 {==}
745 case True{} True{} True{} True{} True{} True{} False{} False{}:
746 {==}
747 case False{} False{} False{} False{} False{} False{} True{} False{}:
748 {==}
749 case True{} False{} False{} False{} False{} False{} True{} False{}:
750 {==}
751 case False{} True{} False{} False{} False{} False{} True{} False{}:
752 {==}
753 case True{} True{} False{} False{} False{} False{} True{} False{}:
754 {==}
755 case False{} False{} True{} False{} False{} False{} True{} False{}:
756 {==}
757 case True{} False{} True{} False{} False{} False{} True{} False{}:
758 {==}
759 case False{} True{} True{} False{} False{} False{} True{} False{}:
760 {==}
761 case True{} True{} True{} False{} False{} False{} True{} False{}:
762 {==}
763 case False{} False{} False{} True{} False{} False{} True{} False{}:
764 {==}
765 case True{} False{} False{} True{} False{} False{} True{} False{}:
766 {==}
767 case False{} True{} False{} True{} False{} False{} True{} False{}:
768 {==}
769 case True{} True{} False{} True{} False{} False{} True{} False{}:
770 {==}
771 case False{} False{} True{} True{} False{} False{} True{} False{}:
772 {==}
773 case True{} False{} True{} True{} False{} False{} True{} False{}:
774 {==}
775 case False{} True{} True{} True{} False{} False{} True{} False{}:
776 {==}
777 case True{} True{} True{} True{} False{} False{} True{} False{}:
778 {==}
779 case False{} False{} False{} False{} True{} False{} True{} False{}:
780 {==}
781 case True{} False{} False{} False{} True{} False{} True{} False{}:
782 {==}
783 case False{} True{} False{} False{} True{} False{} True{} False{}:
784 {==}
785 case True{} True{} False{} False{} True{} False{} True{} False{}:
786 {==}
787 case False{} False{} True{} False{} True{} False{} True{} False{}:
788 {==}
789 case True{} False{} True{} False{} True{} False{} True{} False{}:
790 {==}
791 case False{} True{} True{} False{} True{} False{} True{} False{}:
792 {==}
793 case True{} True{} True{} False{} True{} False{} True{} False{}:
794 {==}
795 case False{} False{} False{} True{} True{} False{} True{} False{}:
796 {==}
797 case True{} False{} False{} True{} True{} False{} True{} False{}:
798 {==}
799 case False{} True{} False{} True{} True{} False{} True{} False{}:
800 {==}
801 case True{} True{} False{} True{} True{} False{} True{} False{}:
802 {==}
803 case False{} False{} True{} True{} True{} False{} True{} False{}:
804 {==}
805 case True{} False{} True{} True{} True{} False{} True{} False{}:
806 {==}
807 case False{} True{} True{} True{} True{} False{} True{} False{}:
808 {==}
809 case True{} True{} True{} True{} True{} False{} True{} False{}:
810 {==}
811 case False{} False{} False{} False{} False{} True{} True{} False{}:
812 {==}
813 case True{} False{} False{} False{} False{} True{} True{} False{}:
814 {==}
815 case False{} True{} False{} False{} False{} True{} True{} False{}:
816 {==}
817 case True{} True{} False{} False{} False{} True{} True{} False{}:
818 {==}
819 case False{} False{} True{} False{} False{} True{} True{} False{}:
820 {==}
821 case True{} False{} True{} False{} False{} True{} True{} False{}:
822 {==}
823 case False{} True{} True{} False{} False{} True{} True{} False{}:
824 {==}
825 case True{} True{} True{} False{} False{} True{} True{} False{}:
826 {==}
827 case False{} False{} False{} True{} False{} True{} True{} False{}:
828 {==}
829 case True{} False{} False{} True{} False{} True{} True{} False{}:
830 {==}
831 case False{} True{} False{} True{} False{} True{} True{} False{}:
832 {==}
833 case True{} True{} False{} True{} False{} True{} True{} False{}:
834 {==}
835 case False{} False{} True{} True{} False{} True{} True{} False{}:
836 {==}
837 case True{} False{} True{} True{} False{} True{} True{} False{}:
838 {==}
839 case False{} True{} True{} True{} False{} True{} True{} False{}:
840 {==}
841 case True{} True{} True{} True{} False{} True{} True{} False{}:
842 {==}
843 case False{} False{} False{} False{} True{} True{} True{} False{}:
844 {==}
845 case True{} False{} False{} False{} True{} True{} True{} False{}:
846 {==}
847 case False{} True{} False{} False{} True{} True{} True{} False{}:
848 {==}
849 case True{} True{} False{} False{} True{} True{} True{} False{}:
850 {==}
851 case False{} False{} True{} False{} True{} True{} True{} False{}:
852 {==}
853 case True{} False{} True{} False{} True{} True{} True{} False{}:
854 {==}
855 case False{} True{} True{} False{} True{} True{} True{} False{}:
856 {==}
857 case True{} True{} True{} False{} True{} True{} True{} False{}:
858 {==}
859 case False{} False{} False{} True{} True{} True{} True{} False{}:
860 {==}
861 case True{} False{} False{} True{} True{} True{} True{} False{}:
862 {==}
863 case False{} True{} False{} True{} True{} True{} True{} False{}:
864 {==}
865 case True{} True{} False{} True{} True{} True{} True{} False{}:
866 {==}
867 case False{} False{} True{} True{} True{} True{} True{} False{}:
868 {==}
869 case True{} False{} True{} True{} True{} True{} True{} False{}:
870 {==}
871 case False{} True{} True{} True{} True{} True{} True{} False{}:
872 {==}
873 case True{} True{} True{} True{} True{} True{} True{} False{}:
874 {==}
875 case False{} False{} False{} False{} False{} False{} False{} True{}:
876 {==}
877 case True{} False{} False{} False{} False{} False{} False{} True{}:
878 {==}
879 case False{} True{} False{} False{} False{} False{} False{} True{}:
880 {==}
881 case True{} True{} False{} False{} False{} False{} False{} True{}:
882 {==}
883 case False{} False{} True{} False{} False{} False{} False{} True{}:
884 {==}
885 case True{} False{} True{} False{} False{} False{} False{} True{}:
886 {==}
887 case False{} True{} True{} False{} False{} False{} False{} True{}:
888 {==}
889 case True{} True{} True{} False{} False{} False{} False{} True{}:
890 {==}
891 case False{} False{} False{} True{} False{} False{} False{} True{}:
892 {==}
893 case True{} False{} False{} True{} False{} False{} False{} True{}:
894 {==}
895 case False{} True{} False{} True{} False{} False{} False{} True{}:
896 {==}
897 case True{} True{} False{} True{} False{} False{} False{} True{}:
898 {==}
899 case False{} False{} True{} True{} False{} False{} False{} True{}:
900 {==}
901 case True{} False{} True{} True{} False{} False{} False{} True{}:
902 {==}
903 case False{} True{} True{} True{} False{} False{} False{} True{}:
904 {==}
905 case True{} True{} True{} True{} False{} False{} False{} True{}:
906 {==}
907 case False{} False{} False{} False{} True{} False{} False{} True{}:
908 {==}
909 case True{} False{} False{} False{} True{} False{} False{} True{}:
910 {==}
911 case False{} True{} False{} False{} True{} False{} False{} True{}:
912 {==}
913 case True{} True{} False{} False{} True{} False{} False{} True{}:
914 {==}
915 case False{} False{} True{} False{} True{} False{} False{} True{}:
916 {==}
917 case True{} False{} True{} False{} True{} False{} False{} True{}:
918 {==}
919 case False{} True{} True{} False{} True{} False{} False{} True{}:
920 {==}
921 case True{} True{} True{} False{} True{} False{} False{} True{}:
922 {==}
923 case False{} False{} False{} True{} True{} False{} False{} True{}:
924 {==}
925 case True{} False{} False{} True{} True{} False{} False{} True{}:
926 {==}
927 case False{} True{} False{} True{} True{} False{} False{} True{}:
928 {==}
929 case True{} True{} False{} True{} True{} False{} False{} True{}:
930 {==}
931 case False{} False{} True{} True{} True{} False{} False{} True{}:
932 {==}
933 case True{} False{} True{} True{} True{} False{} False{} True{}:
934 {==}
935 case False{} True{} True{} True{} True{} False{} False{} True{}:
936 {==}
937 case True{} True{} True{} True{} True{} False{} False{} True{}:
938 {==}
939 case False{} False{} False{} False{} False{} True{} False{} True{}:
940 {==}
941 case True{} False{} False{} False{} False{} True{} False{} True{}:
942 {==}
943 case False{} True{} False{} False{} False{} True{} False{} True{}:
944 {==}
945 case True{} True{} False{} False{} False{} True{} False{} True{}:
946 {==}
947 case False{} False{} True{} False{} False{} True{} False{} True{}:
948 {==}
949 case True{} False{} True{} False{} False{} True{} False{} True{}:
950 {==}
951 case False{} True{} True{} False{} False{} True{} False{} True{}:
952 {==}
953 case True{} True{} True{} False{} False{} True{} False{} True{}:
954 {==}
955 case False{} False{} False{} True{} False{} True{} False{} True{}:
956 {==}
957 case True{} False{} False{} True{} False{} True{} False{} True{}:
958 {==}
959 case False{} True{} False{} True{} False{} True{} False{} True{}:
960 {==}
961 case True{} True{} False{} True{} False{} True{} False{} True{}:
962 {==}
963 case False{} False{} True{} True{} False{} True{} False{} True{}:
964 {==}
965 case True{} False{} True{} True{} False{} True{} False{} True{}:
966 {==}
967 case False{} True{} True{} True{} False{} True{} False{} True{}:
968 {==}
969 case True{} True{} True{} True{} False{} True{} False{} True{}:
970 {==}
971 case False{} False{} False{} False{} True{} True{} False{} True{}:
972 {==}
973 case True{} False{} False{} False{} True{} True{} False{} True{}:
974 {==}
975 case False{} True{} False{} False{} True{} True{} False{} True{}:
976 {==}
977 case True{} True{} False{} False{} True{} True{} False{} True{}:
978 {==}
979 case False{} False{} True{} False{} True{} True{} False{} True{}:
980 {==}
981 case True{} False{} True{} False{} True{} True{} False{} True{}:
982 {==}
983 case False{} True{} True{} False{} True{} True{} False{} True{}:
984 {==}
985 case True{} True{} True{} False{} True{} True{} False{} True{}:
986 {==}
987 case False{} False{} False{} True{} True{} True{} False{} True{}:
988 {==}
989 case True{} False{} False{} True{} True{} True{} False{} True{}:
990 {==}
991 case False{} True{} False{} True{} True{} True{} False{} True{}:
992 {==}
993 case True{} True{} False{} True{} True{} True{} False{} True{}:
994 {==}
995 case False{} False{} True{} True{} True{} True{} False{} True{}:
996 {==}
997 case True{} False{} True{} True{} True{} True{} False{} True{}:
998 {==}
999 case False{} True{} True{} True{} True{} True{} False{} True{}:
1000 {==}
1001 case True{} True{} True{} True{} True{} True{} False{} True{}:
1002 {==}
1003 case False{} False{} False{} False{} False{} False{} True{} True{}:
1004 {==}
1005 case True{} False{} False{} False{} False{} False{} True{} True{}:
1006 {==}
1007 case False{} True{} False{} False{} False{} False{} True{} True{}:
1008 {==}
1009 case True{} True{} False{} False{} False{} False{} True{} True{}:
1010 {==}
1011 case False{} False{} True{} False{} False{} False{} True{} True{}:
1012 {==}
1013 case True{} False{} True{} False{} False{} False{} True{} True{}:
1014 {==}
1015 case False{} True{} True{} False{} False{} False{} True{} True{}:
1016 {==}
1017 case True{} True{} True{} False{} False{} False{} True{} True{}:
1018 {==}
1019 case False{} False{} False{} True{} False{} False{} True{} True{}:
1020 {==}
1021 case True{} False{} False{} True{} False{} False{} True{} True{}:
1022 {==}
1023 case False{} True{} False{} True{} False{} False{} True{} True{}:
1024 {==}
1025 case True{} True{} False{} True{} False{} False{} True{} True{}:
1026 {==}
1027 case False{} False{} True{} True{} False{} False{} True{} True{}:
1028 {==}
1029 case True{} False{} True{} True{} False{} False{} True{} True{}:
1030 {==}
1031 case False{} True{} True{} True{} False{} False{} True{} True{}:
1032 {==}
1033 case True{} True{} True{} True{} False{} False{} True{} True{}:
1034 {==}
1035 case False{} False{} False{} False{} True{} False{} True{} True{}:
1036 {==}
1037 case True{} False{} False{} False{} True{} False{} True{} True{}:
1038 {==}
1039 case False{} True{} False{} False{} True{} False{} True{} True{}:
1040 {==}
1041 case True{} True{} False{} False{} True{} False{} True{} True{}:
1042 {==}
1043 case False{} False{} True{} False{} True{} False{} True{} True{}:
1044 {==}
1045 case True{} False{} True{} False{} True{} False{} True{} True{}:
1046 {==}
1047 case False{} True{} True{} False{} True{} False{} True{} True{}:
1048 {==}
1049 case True{} True{} True{} False{} True{} False{} True{} True{}:
1050 {==}
1051 case False{} False{} False{} True{} True{} False{} True{} True{}:
1052 {==}
1053 case True{} False{} False{} True{} True{} False{} True{} True{}:
1054 {==}
1055 case False{} True{} False{} True{} True{} False{} True{} True{}:
1056 {==}
1057 case True{} True{} False{} True{} True{} False{} True{} True{}:
1058 {==}
1059 case False{} False{} True{} True{} True{} False{} True{} True{}:
1060 {==}
1061 case True{} False{} True{} True{} True{} False{} True{} True{}:
1062 {==}
1063 case False{} True{} True{} True{} True{} False{} True{} True{}:
1064 {==}
1065 case True{} True{} True{} True{} True{} False{} True{} True{}:
1066 {==}
1067 case False{} False{} False{} False{} False{} True{} True{} True{}:
1068 {==}
1069 case True{} False{} False{} False{} False{} True{} True{} True{}:
1070 {==}
1071 case False{} True{} False{} False{} False{} True{} True{} True{}:
1072 {==}
1073 case True{} True{} False{} False{} False{} True{} True{} True{}:
1074 {==}
1075 case False{} False{} True{} False{} False{} True{} True{} True{}:
1076 {==}
1077 case True{} False{} True{} False{} False{} True{} True{} True{}:
1078 {==}
1079 case False{} True{} True{} False{} False{} True{} True{} True{}:
1080 {==}
1081 case True{} True{} True{} False{} False{} True{} True{} True{}:
1082 {==}
1083 case False{} False{} False{} True{} False{} True{} True{} True{}:
1084 {==}
1085 case True{} False{} False{} True{} False{} True{} True{} True{}:
1086 {==}
1087 case False{} True{} False{} True{} False{} True{} True{} True{}:
1088 {==}
1089 case True{} True{} False{} True{} False{} True{} True{} True{}:
1090 {==}
1091 case False{} False{} True{} True{} False{} True{} True{} True{}:
1092 {==}
1093 case True{} False{} True{} True{} False{} True{} True{} True{}:
1094 {==}
1095 case False{} True{} True{} True{} False{} True{} True{} True{}:
1096 {==}
1097 case True{} True{} True{} True{} False{} True{} True{} True{}:
1098 {==}
1099 case False{} False{} False{} False{} True{} True{} True{} True{}:
1100 {==}
1101 case True{} False{} False{} False{} True{} True{} True{} True{}:
1102 {==}
1103 case False{} True{} False{} False{} True{} True{} True{} True{}:
1104 {==}
1105 case True{} True{} False{} False{} True{} True{} True{} True{}:
1106 {==}
1107 case False{} False{} True{} False{} True{} True{} True{} True{}:
1108 {==}
1109 case True{} False{} True{} False{} True{} True{} True{} True{}:
1110 {==}
1111 case False{} True{} True{} False{} True{} True{} True{} True{}:
1112 {==}
1113 case True{} True{} True{} False{} True{} True{} True{} True{}:
1114 {==}
1115 case False{} False{} False{} True{} True{} True{} True{} True{}:
1116 {==}
1117 case True{} False{} False{} True{} True{} True{} True{} True{}:
1118 {==}
1119 case False{} True{} False{} True{} True{} True{} True{} True{}:
1120 {==}
1121 case True{} True{} False{} True{} True{} True{} True{} True{}:
1122 {==}
1123 case False{} False{} True{} True{} True{} True{} True{} True{}:
1124 {==}
1125 case True{} False{} True{} True{} True{} True{} True{} True{}:
1126 {==}
1127 case False{} True{} True{} True{} True{} True{} True{} True{}:
1128 {==}
1129 case True{} True{} True{} True{} True{} True{} True{} True{}:
1130 {==}
1131
1132law xtime_ok:
1133 for +x: U32
1134 {B.xtime(x) == S.mul(2, x) : U32}
1135
1136def xtime_ok(x):
1137 match x:
1138 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
1139 xtime_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31)
1140
1141law mul3_bits:
1142 for b0: Bool
1143 for b1: Bool
1144 for b2: Bool
1145 for b3: Bool
1146 for b4: Bool
1147 for b5: Bool
1148 for b6: Bool
1149 for b7: Bool
1150 for b8: Bool
1151 for b9: Bool
1152 for b10: Bool
1153 for b11: Bool
1154 for b12: Bool
1155 for b13: Bool
1156 for b14: Bool
1157 for b15: Bool
1158 for b16: Bool
1159 for b17: Bool
1160 for b18: Bool
1161 for b19: Bool
1162 for b20: Bool
1163 for b21: Bool
1164 for b22: Bool
1165 for b23: Bool
1166 for b24: Bool
1167 for b25: Bool
1168 for b26: Bool
1169 for b27: Bool
1170 for b28: Bool
1171 for b29: Bool
1172 for b30: Bool
1173 for b31: Bool
1174 {B.mul3(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == S.mul(3, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}
1175
1176def mul3_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31):
1177 match b0 b1 b2 b3 b4 b5 b6 b7:
1178 case False{} False{} False{} False{} False{} False{} False{} False{}:
1179 {==}
1180 case True{} False{} False{} False{} False{} False{} False{} False{}:
1181 {==}
1182 case False{} True{} False{} False{} False{} False{} False{} False{}:
1183 {==}
1184 case True{} True{} False{} False{} False{} False{} False{} False{}:
1185 {==}
1186 case False{} False{} True{} False{} False{} False{} False{} False{}:
1187 {==}
1188 case True{} False{} True{} False{} False{} False{} False{} False{}:
1189 {==}
1190 case False{} True{} True{} False{} False{} False{} False{} False{}:
1191 {==}
1192 case True{} True{} True{} False{} False{} False{} False{} False{}:
1193 {==}
1194 case False{} False{} False{} True{} False{} False{} False{} False{}:
1195 {==}
1196 case True{} False{} False{} True{} False{} False{} False{} False{}:
1197 {==}
1198 case False{} True{} False{} True{} False{} False{} False{} False{}:
1199 {==}
1200 case True{} True{} False{} True{} False{} False{} False{} False{}:
1201 {==}
1202 case False{} False{} True{} True{} False{} False{} False{} False{}:
1203 {==}
1204 case True{} False{} True{} True{} False{} False{} False{} False{}:
1205 {==}
1206 case False{} True{} True{} True{} False{} False{} False{} False{}:
1207 {==}
1208 case True{} True{} True{} True{} False{} False{} False{} False{}:
1209 {==}
1210 case False{} False{} False{} False{} True{} False{} False{} False{}:
1211 {==}
1212 case True{} False{} False{} False{} True{} False{} False{} False{}:
1213 {==}
1214 case False{} True{} False{} False{} True{} False{} False{} False{}:
1215 {==}
1216 case True{} True{} False{} False{} True{} False{} False{} False{}:
1217 {==}
1218 case False{} False{} True{} False{} True{} False{} False{} False{}:
1219 {==}
1220 case True{} False{} True{} False{} True{} False{} False{} False{}:
1221 {==}
1222 case False{} True{} True{} False{} True{} False{} False{} False{}:
1223 {==}
1224 case True{} True{} True{} False{} True{} False{} False{} False{}:
1225 {==}
1226 case False{} False{} False{} True{} True{} False{} False{} False{}:
1227 {==}
1228 case True{} False{} False{} True{} True{} False{} False{} False{}:
1229 {==}
1230 case False{} True{} False{} True{} True{} False{} False{} False{}:
1231 {==}
1232 case True{} True{} False{} True{} True{} False{} False{} False{}:
1233 {==}
1234 case False{} False{} True{} True{} True{} False{} False{} False{}:
1235 {==}
1236 case True{} False{} True{} True{} True{} False{} False{} False{}:
1237 {==}
1238 case False{} True{} True{} True{} True{} False{} False{} False{}:
1239 {==}
1240 case True{} True{} True{} True{} True{} False{} False{} False{}:
1241 {==}
1242 case False{} False{} False{} False{} False{} True{} False{} False{}:
1243 {==}
1244 case True{} False{} False{} False{} False{} True{} False{} False{}:
1245 {==}
1246 case False{} True{} False{} False{} False{} True{} False{} False{}:
1247 {==}
1248 case True{} True{} False{} False{} False{} True{} False{} False{}:
1249 {==}
1250 case False{} False{} True{} False{} False{} True{} False{} False{}:
1251 {==}
1252 case True{} False{} True{} False{} False{} True{} False{} False{}:
1253 {==}
1254 case False{} True{} True{} False{} False{} True{} False{} False{}:
1255 {==}
1256 case True{} True{} True{} False{} False{} True{} False{} False{}:
1257 {==}
1258 case False{} False{} False{} True{} False{} True{} False{} False{}:
1259 {==}
1260 case True{} False{} False{} True{} False{} True{} False{} False{}:
1261 {==}
1262 case False{} True{} False{} True{} False{} True{} False{} False{}:
1263 {==}
1264 case True{} True{} False{} True{} False{} True{} False{} False{}:
1265 {==}
1266 case False{} False{} True{} True{} False{} True{} False{} False{}:
1267 {==}
1268 case True{} False{} True{} True{} False{} True{} False{} False{}:
1269 {==}
1270 case False{} True{} True{} True{} False{} True{} False{} False{}:
1271 {==}
1272 case True{} True{} True{} True{} False{} True{} False{} False{}:
1273 {==}
1274 case False{} False{} False{} False{} True{} True{} False{} False{}:
1275 {==}
1276 case True{} False{} False{} False{} True{} True{} False{} False{}:
1277 {==}
1278 case False{} True{} False{} False{} True{} True{} False{} False{}:
1279 {==}
1280 case True{} True{} False{} False{} True{} True{} False{} False{}:
1281 {==}
1282 case False{} False{} True{} False{} True{} True{} False{} False{}:
1283 {==}
1284 case True{} False{} True{} False{} True{} True{} False{} False{}:
1285 {==}
1286 case False{} True{} True{} False{} True{} True{} False{} False{}:
1287 {==}
1288 case True{} True{} True{} False{} True{} True{} False{} False{}:
1289 {==}
1290 case False{} False{} False{} True{} True{} True{} False{} False{}:
1291 {==}
1292 case True{} False{} False{} True{} True{} True{} False{} False{}:
1293 {==}
1294 case False{} True{} False{} True{} True{} True{} False{} False{}:
1295 {==}
1296 case True{} True{} False{} True{} True{} True{} False{} False{}:
1297 {==}
1298 case False{} False{} True{} True{} True{} True{} False{} False{}:
1299 {==}
1300 case True{} False{} True{} True{} True{} True{} False{} False{}:
1301 {==}
1302 case False{} True{} True{} True{} True{} True{} False{} False{}:
1303 {==}
1304 case True{} True{} True{} True{} True{} True{} False{} False{}:
1305 {==}
1306 case False{} False{} False{} False{} False{} False{} True{} False{}:
1307 {==}
1308 case True{} False{} False{} False{} False{} False{} True{} False{}:
1309 {==}
1310 case False{} True{} False{} False{} False{} False{} True{} False{}:
1311 {==}
1312 case True{} True{} False{} False{} False{} False{} True{} False{}:
1313 {==}
1314 case False{} False{} True{} False{} False{} False{} True{} False{}:
1315 {==}
1316 case True{} False{} True{} False{} False{} False{} True{} False{}:
1317 {==}
1318 case False{} True{} True{} False{} False{} False{} True{} False{}:
1319 {==}
1320 case True{} True{} True{} False{} False{} False{} True{} False{}:
1321 {==}
1322 case False{} False{} False{} True{} False{} False{} True{} False{}:
1323 {==}
1324 case True{} False{} False{} True{} False{} False{} True{} False{}:
1325 {==}
1326 case False{} True{} False{} True{} False{} False{} True{} False{}:
1327 {==}
1328 case True{} True{} False{} True{} False{} False{} True{} False{}:
1329 {==}
1330 case False{} False{} True{} True{} False{} False{} True{} False{}:
1331 {==}
1332 case True{} False{} True{} True{} False{} False{} True{} False{}:
1333 {==}
1334 case False{} True{} True{} True{} False{} False{} True{} False{}:
1335 {==}
1336 case True{} True{} True{} True{} False{} False{} True{} False{}:
1337 {==}
1338 case False{} False{} False{} False{} True{} False{} True{} False{}:
1339 {==}
1340 case True{} False{} False{} False{} True{} False{} True{} False{}:
1341 {==}
1342 case False{} True{} False{} False{} True{} False{} True{} False{}:
1343 {==}
1344 case True{} True{} False{} False{} True{} False{} True{} False{}:
1345 {==}
1346 case False{} False{} True{} False{} True{} False{} True{} False{}:
1347 {==}
1348 case True{} False{} True{} False{} True{} False{} True{} False{}:
1349 {==}
1350 case False{} True{} True{} False{} True{} False{} True{} False{}:
1351 {==}
1352 case True{} True{} True{} False{} True{} False{} True{} False{}:
1353 {==}
1354 case False{} False{} False{} True{} True{} False{} True{} False{}:
1355 {==}
1356 case True{} False{} False{} True{} True{} False{} True{} False{}:
1357 {==}
1358 case False{} True{} False{} True{} True{} False{} True{} False{}:
1359 {==}
1360 case True{} True{} False{} True{} True{} False{} True{} False{}:
1361 {==}
1362 case False{} False{} True{} True{} True{} False{} True{} False{}:
1363 {==}
1364 case True{} False{} True{} True{} True{} False{} True{} False{}:
1365 {==}
1366 case False{} True{} True{} True{} True{} False{} True{} False{}:
1367 {==}
1368 case True{} True{} True{} True{} True{} False{} True{} False{}:
1369 {==}
1370 case False{} False{} False{} False{} False{} True{} True{} False{}:
1371 {==}
1372 case True{} False{} False{} False{} False{} True{} True{} False{}:
1373 {==}
1374 case False{} True{} False{} False{} False{} True{} True{} False{}:
1375 {==}
1376 case True{} True{} False{} False{} False{} True{} True{} False{}:
1377 {==}
1378 case False{} False{} True{} False{} False{} True{} True{} False{}:
1379 {==}
1380 case True{} False{} True{} False{} False{} True{} True{} False{}:
1381 {==}
1382 case False{} True{} True{} False{} False{} True{} True{} False{}:
1383 {==}
1384 case True{} True{} True{} False{} False{} True{} True{} False{}:
1385 {==}
1386 case False{} False{} False{} True{} False{} True{} True{} False{}:
1387 {==}
1388 case True{} False{} False{} True{} False{} True{} True{} False{}:
1389 {==}
1390 case False{} True{} False{} True{} False{} True{} True{} False{}:
1391 {==}
1392 case True{} True{} False{} True{} False{} True{} True{} False{}:
1393 {==}
1394 case False{} False{} True{} True{} False{} True{} True{} False{}:
1395 {==}
1396 case True{} False{} True{} True{} False{} True{} True{} False{}:
1397 {==}
1398 case False{} True{} True{} True{} False{} True{} True{} False{}:
1399 {==}
1400 case True{} True{} True{} True{} False{} True{} True{} False{}:
1401 {==}
1402 case False{} False{} False{} False{} True{} True{} True{} False{}:
1403 {==}
1404 case True{} False{} False{} False{} True{} True{} True{} False{}:
1405 {==}
1406 case False{} True{} False{} False{} True{} True{} True{} False{}:
1407 {==}
1408 case True{} True{} False{} False{} True{} True{} True{} False{}:
1409 {==}
1410 case False{} False{} True{} False{} True{} True{} True{} False{}:
1411 {==}
1412 case True{} False{} True{} False{} True{} True{} True{} False{}:
1413 {==}
1414 case False{} True{} True{} False{} True{} True{} True{} False{}:
1415 {==}
1416 case True{} True{} True{} False{} True{} True{} True{} False{}:
1417 {==}
1418 case False{} False{} False{} True{} True{} True{} True{} False{}:
1419 {==}
1420 case True{} False{} False{} True{} True{} True{} True{} False{}:
1421 {==}
1422 case False{} True{} False{} True{} True{} True{} True{} False{}:
1423 {==}
1424 case True{} True{} False{} True{} True{} True{} True{} False{}:
1425 {==}
1426 case False{} False{} True{} True{} True{} True{} True{} False{}:
1427 {==}
1428 case True{} False{} True{} True{} True{} True{} True{} False{}:
1429 {==}
1430 case False{} True{} True{} True{} True{} True{} True{} False{}:
1431 {==}
1432 case True{} True{} True{} True{} True{} True{} True{} False{}:
1433 {==}
1434 case False{} False{} False{} False{} False{} False{} False{} True{}:
1435 {==}
1436 case True{} False{} False{} False{} False{} False{} False{} True{}:
1437 {==}
1438 case False{} True{} False{} False{} False{} False{} False{} True{}:
1439 {==}
1440 case True{} True{} False{} False{} False{} False{} False{} True{}:
1441 {==}
1442 case False{} False{} True{} False{} False{} False{} False{} True{}:
1443 {==}
1444 case True{} False{} True{} False{} False{} False{} False{} True{}:
1445 {==}
1446 case False{} True{} True{} False{} False{} False{} False{} True{}:
1447 {==}
1448 case True{} True{} True{} False{} False{} False{} False{} True{}:
1449 {==}
1450 case False{} False{} False{} True{} False{} False{} False{} True{}:
1451 {==}
1452 case True{} False{} False{} True{} False{} False{} False{} True{}:
1453 {==}
1454 case False{} True{} False{} True{} False{} False{} False{} True{}:
1455 {==}
1456 case True{} True{} False{} True{} False{} False{} False{} True{}:
1457 {==}
1458 case False{} False{} True{} True{} False{} False{} False{} True{}:
1459 {==}
1460 case True{} False{} True{} True{} False{} False{} False{} True{}:
1461 {==}
1462 case False{} True{} True{} True{} False{} False{} False{} True{}:
1463 {==}
1464 case True{} True{} True{} True{} False{} False{} False{} True{}:
1465 {==}
1466 case False{} False{} False{} False{} True{} False{} False{} True{}:
1467 {==}
1468 case True{} False{} False{} False{} True{} False{} False{} True{}:
1469 {==}
1470 case False{} True{} False{} False{} True{} False{} False{} True{}:
1471 {==}
1472 case True{} True{} False{} False{} True{} False{} False{} True{}:
1473 {==}
1474 case False{} False{} True{} False{} True{} False{} False{} True{}:
1475 {==}
1476 case True{} False{} True{} False{} True{} False{} False{} True{}:
1477 {==}
1478 case False{} True{} True{} False{} True{} False{} False{} True{}:
1479 {==}
1480 case True{} True{} True{} False{} True{} False{} False{} True{}:
1481 {==}
1482 case False{} False{} False{} True{} True{} False{} False{} True{}:
1483 {==}
1484 case True{} False{} False{} True{} True{} False{} False{} True{}:
1485 {==}
1486 case False{} True{} False{} True{} True{} False{} False{} True{}:
1487 {==}
1488 case True{} True{} False{} True{} True{} False{} False{} True{}:
1489 {==}
1490 case False{} False{} True{} True{} True{} False{} False{} True{}:
1491 {==}
1492 case True{} False{} True{} True{} True{} False{} False{} True{}:
1493 {==}
1494 case False{} True{} True{} True{} True{} False{} False{} True{}:
1495 {==}
1496 case True{} True{} True{} True{} True{} False{} False{} True{}:
1497 {==}
1498 case False{} False{} False{} False{} False{} True{} False{} True{}:
1499 {==}
1500 case True{} False{} False{} False{} False{} True{} False{} True{}:
1501 {==}
1502 case False{} True{} False{} False{} False{} True{} False{} True{}:
1503 {==}
1504 case True{} True{} False{} False{} False{} True{} False{} True{}:
1505 {==}
1506 case False{} False{} True{} False{} False{} True{} False{} True{}:
1507 {==}
1508 case True{} False{} True{} False{} False{} True{} False{} True{}:
1509 {==}
1510 case False{} True{} True{} False{} False{} True{} False{} True{}:
1511 {==}
1512 case True{} True{} True{} False{} False{} True{} False{} True{}:
1513 {==}
1514 case False{} False{} False{} True{} False{} True{} False{} True{}:
1515 {==}
1516 case True{} False{} False{} True{} False{} True{} False{} True{}:
1517 {==}
1518 case False{} True{} False{} True{} False{} True{} False{} True{}:
1519 {==}
1520 case True{} True{} False{} True{} False{} True{} False{} True{}:
1521 {==}
1522 case False{} False{} True{} True{} False{} True{} False{} True{}:
1523 {==}
1524 case True{} False{} True{} True{} False{} True{} False{} True{}:
1525 {==}
1526 case False{} True{} True{} True{} False{} True{} False{} True{}:
1527 {==}
1528 case True{} True{} True{} True{} False{} True{} False{} True{}:
1529 {==}
1530 case False{} False{} False{} False{} True{} True{} False{} True{}:
1531 {==}
1532 case True{} False{} False{} False{} True{} True{} False{} True{}:
1533 {==}
1534 case False{} True{} False{} False{} True{} True{} False{} True{}:
1535 {==}
1536 case True{} True{} False{} False{} True{} True{} False{} True{}:
1537 {==}
1538 case False{} False{} True{} False{} True{} True{} False{} True{}:
1539 {==}
1540 case True{} False{} True{} False{} True{} True{} False{} True{}:
1541 {==}
1542 case False{} True{} True{} False{} True{} True{} False{} True{}:
1543 {==}
1544 case True{} True{} True{} False{} True{} True{} False{} True{}:
1545 {==}
1546 case False{} False{} False{} True{} True{} True{} False{} True{}:
1547 {==}
1548 case True{} False{} False{} True{} True{} True{} False{} True{}:
1549 {==}
1550 case False{} True{} False{} True{} True{} True{} False{} True{}:
1551 {==}
1552 case True{} True{} False{} True{} True{} True{} False{} True{}:
1553 {==}
1554 case False{} False{} True{} True{} True{} True{} False{} True{}:
1555 {==}
1556 case True{} False{} True{} True{} True{} True{} False{} True{}:
1557 {==}
1558 case False{} True{} True{} True{} True{} True{} False{} True{}:
1559 {==}
1560 case True{} True{} True{} True{} True{} True{} False{} True{}:
1561 {==}
1562 case False{} False{} False{} False{} False{} False{} True{} True{}:
1563 {==}
1564 case True{} False{} False{} False{} False{} False{} True{} True{}:
1565 {==}
1566 case False{} True{} False{} False{} False{} False{} True{} True{}:
1567 {==}
1568 case True{} True{} False{} False{} False{} False{} True{} True{}:
1569 {==}
1570 case False{} False{} True{} False{} False{} False{} True{} True{}:
1571 {==}
1572 case True{} False{} True{} False{} False{} False{} True{} True{}:
1573 {==}
1574 case False{} True{} True{} False{} False{} False{} True{} True{}:
1575 {==}
1576 case True{} True{} True{} False{} False{} False{} True{} True{}:
1577 {==}
1578 case False{} False{} False{} True{} False{} False{} True{} True{}:
1579 {==}
1580 case True{} False{} False{} True{} False{} False{} True{} True{}:
1581 {==}
1582 case False{} True{} False{} True{} False{} False{} True{} True{}:
1583 {==}
1584 case True{} True{} False{} True{} False{} False{} True{} True{}:
1585 {==}
1586 case False{} False{} True{} True{} False{} False{} True{} True{}:
1587 {==}
1588 case True{} False{} True{} True{} False{} False{} True{} True{}:
1589 {==}
1590 case False{} True{} True{} True{} False{} False{} True{} True{}:
1591 {==}
1592 case True{} True{} True{} True{} False{} False{} True{} True{}:
1593 {==}
1594 case False{} False{} False{} False{} True{} False{} True{} True{}:
1595 {==}
1596 case True{} False{} False{} False{} True{} False{} True{} True{}:
1597 {==}
1598 case False{} True{} False{} False{} True{} False{} True{} True{}:
1599 {==}
1600 case True{} True{} False{} False{} True{} False{} True{} True{}:
1601 {==}
1602 case False{} False{} True{} False{} True{} False{} True{} True{}:
1603 {==}
1604 case True{} False{} True{} False{} True{} False{} True{} True{}:
1605 {==}
1606 case False{} True{} True{} False{} True{} False{} True{} True{}:
1607 {==}
1608 case True{} True{} True{} False{} True{} False{} True{} True{}:
1609 {==}
1610 case False{} False{} False{} True{} True{} False{} True{} True{}:
1611 {==}
1612 case True{} False{} False{} True{} True{} False{} True{} True{}:
1613 {==}
1614 case False{} True{} False{} True{} True{} False{} True{} True{}:
1615 {==}
1616 case True{} True{} False{} True{} True{} False{} True{} True{}:
1617 {==}
1618 case False{} False{} True{} True{} True{} False{} True{} True{}:
1619 {==}
1620 case True{} False{} True{} True{} True{} False{} True{} True{}:
1621 {==}
1622 case False{} True{} True{} True{} True{} False{} True{} True{}:
1623 {==}
1624 case True{} True{} True{} True{} True{} False{} True{} True{}:
1625 {==}
1626 case False{} False{} False{} False{} False{} True{} True{} True{}:
1627 {==}
1628 case True{} False{} False{} False{} False{} True{} True{} True{}:
1629 {==}
1630 case False{} True{} False{} False{} False{} True{} True{} True{}:
1631 {==}
1632 case True{} True{} False{} False{} False{} True{} True{} True{}:
1633 {==}
1634 case False{} False{} True{} False{} False{} True{} True{} True{}:
1635 {==}
1636 case True{} False{} True{} False{} False{} True{} True{} True{}:
1637 {==}
1638 case False{} True{} True{} False{} False{} True{} True{} True{}:
1639 {==}
1640 case True{} True{} True{} False{} False{} True{} True{} True{}:
1641 {==}
1642 case False{} False{} False{} True{} False{} True{} True{} True{}:
1643 {==}
1644 case True{} False{} False{} True{} False{} True{} True{} True{}:
1645 {==}
1646 case False{} True{} False{} True{} False{} True{} True{} True{}:
1647 {==}
1648 case True{} True{} False{} True{} False{} True{} True{} True{}:
1649 {==}
1650 case False{} False{} True{} True{} False{} True{} True{} True{}:
1651 {==}
1652 case True{} False{} True{} True{} False{} True{} True{} True{}:
1653 {==}
1654 case False{} True{} True{} True{} False{} True{} True{} True{}:
1655 {==}
1656 case True{} True{} True{} True{} False{} True{} True{} True{}:
1657 {==}
1658 case False{} False{} False{} False{} True{} True{} True{} True{}:
1659 {==}
1660 case True{} False{} False{} False{} True{} True{} True{} True{}:
1661 {==}
1662 case False{} True{} False{} False{} True{} True{} True{} True{}:
1663 {==}
1664 case True{} True{} False{} False{} True{} True{} True{} True{}:
1665 {==}
1666 case False{} False{} True{} False{} True{} True{} True{} True{}:
1667 {==}
1668 case True{} False{} True{} False{} True{} True{} True{} True{}:
1669 {==}
1670 case False{} True{} True{} False{} True{} True{} True{} True{}:
1671 {==}
1672 case True{} True{} True{} False{} True{} True{} True{} True{}:
1673 {==}
1674 case False{} False{} False{} True{} True{} True{} True{} True{}:
1675 {==}
1676 case True{} False{} False{} True{} True{} True{} True{} True{}:
1677 {==}
1678 case False{} True{} False{} True{} True{} True{} True{} True{}:
1679 {==}
1680 case True{} True{} False{} True{} True{} True{} True{} True{}:
1681 {==}
1682 case False{} False{} True{} True{} True{} True{} True{} True{}:
1683 {==}
1684 case True{} False{} True{} True{} True{} True{} True{} True{}:
1685 {==}
1686 case False{} True{} True{} True{} True{} True{} True{} True{}:
1687 {==}
1688 case True{} True{} True{} True{} True{} True{} True{} True{}:
1689 {==}
1690
1691law mul3_ok:
1692 for +x: U32
1693 {B.mul3(x) == S.mul(3, x) : U32}
1694
1695def mul3_ok(x):
1696 match x:
1697 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
1698 mul3_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31)