proofs/crypto/aes/inverse.bend

bend-collections-laws-crypto@1.0.0.0 · 576 lines · 3 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
4
5# Generated by tools/generators/aes/sbox.py. FIPS 197 section 4.4: the
6# multiplicative inverse b of a nonzero byte a satisfies a * b = {01}; the
7# specification computes it as a^254 (spec/crypto/aes/aes.bend). Proved here
8# for every U32 (both functions read only its low 8 bits): one closed
9# evaluation of 13 field products per byte value.
10
11law inverse_unit_bits:
12  for +b0: Bool
13  for +b1: Bool
14  for +b2: Bool
15  for +b3: Bool
16  for +b4: Bool
17  for +b5: Bool
18  for +b6: Bool
19  for +b7: Bool
20  for +b8: Bool
21  for +b9: Bool
22  for +b10: Bool
23  for +b11: Bool
24  for +b12: Bool
25  for +b13: Bool
26  for +b14: Bool
27  for +b15: Bool
28  for +b16: Bool
29  for +b17: Bool
30  for +b18: Bool
31  for +b19: Bool
32  for +b20: Bool
33  for +b21: Bool
34  for +b22: Bool
35  for +b23: Bool
36  for +b24: Bool
37  for +b25: Bool
38  for +b26: Bool
39  for +b27: Bool
40  for +b28: Bool
41  for +b29: Bool
42  for +b30: Bool
43  for +b31: Bool
44  for +h: {U32.is_eq(U32.and(255, 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), 0) == False{} : Bool}
45  {S.mul(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.inverse(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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})) == 1 : U32}
46
47def inverse_unit_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, h):
48  match b0 b1 b2 b3 b4 b5 b6 b7:
49    case False{} False{} False{} False{} False{} False{} False{} False{}:
50      Empty.absurd({S.mul(U32{WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, 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.inverse(U32{WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})) == 1 : U32}, L.true_false(h))
51    case True{} False{} False{} False{} False{} False{} False{} False{}:
52      {==}
53    case False{} True{} False{} False{} False{} False{} False{} False{}:
54      {==}
55    case True{} True{} False{} False{} False{} False{} False{} False{}:
56      {==}
57    case False{} False{} True{} False{} False{} False{} False{} False{}:
58      {==}
59    case True{} False{} True{} False{} False{} False{} False{} False{}:
60      {==}
61    case False{} True{} True{} False{} False{} False{} False{} False{}:
62      {==}
63    case True{} True{} True{} False{} False{} False{} False{} False{}:
64      {==}
65    case False{} False{} False{} True{} False{} False{} False{} False{}:
66      {==}
67    case True{} False{} False{} True{} False{} False{} False{} False{}:
68      {==}
69    case False{} True{} False{} True{} False{} False{} False{} False{}:
70      {==}
71    case True{} True{} False{} True{} False{} False{} False{} False{}:
72      {==}
73    case False{} False{} True{} True{} False{} False{} False{} False{}:
74      {==}
75    case True{} False{} True{} True{} False{} False{} False{} False{}:
76      {==}
77    case False{} True{} True{} True{} False{} False{} False{} False{}:
78      {==}
79    case True{} True{} True{} True{} False{} False{} False{} False{}:
80      {==}
81    case False{} False{} False{} False{} True{} False{} False{} False{}:
82      {==}
83    case True{} False{} False{} False{} True{} False{} False{} False{}:
84      {==}
85    case False{} True{} False{} False{} True{} False{} False{} False{}:
86      {==}
87    case True{} True{} False{} False{} True{} False{} False{} False{}:
88      {==}
89    case False{} False{} True{} False{} True{} False{} False{} False{}:
90      {==}
91    case True{} False{} True{} False{} True{} False{} False{} False{}:
92      {==}
93    case False{} True{} True{} False{} True{} False{} False{} False{}:
94      {==}
95    case True{} True{} True{} False{} True{} False{} False{} False{}:
96      {==}
97    case False{} False{} False{} True{} True{} False{} False{} False{}:
98      {==}
99    case True{} False{} False{} True{} True{} False{} False{} False{}:
100      {==}
101    case False{} True{} False{} True{} True{} False{} False{} False{}:
102      {==}
103    case True{} True{} False{} True{} True{} False{} False{} False{}:
104      {==}
105    case False{} False{} True{} True{} True{} False{} False{} False{}:
106      {==}
107    case True{} False{} True{} True{} True{} False{} False{} False{}:
108      {==}
109    case False{} True{} True{} True{} True{} False{} False{} False{}:
110      {==}
111    case True{} True{} True{} True{} True{} False{} False{} False{}:
112      {==}
113    case False{} False{} False{} False{} False{} True{} False{} False{}:
114      {==}
115    case True{} False{} False{} False{} False{} True{} False{} False{}:
116      {==}
117    case False{} True{} False{} False{} False{} True{} False{} False{}:
118      {==}
119    case True{} True{} False{} False{} False{} True{} False{} False{}:
120      {==}
121    case False{} False{} True{} False{} False{} True{} False{} False{}:
122      {==}
123    case True{} False{} True{} False{} False{} True{} False{} False{}:
124      {==}
125    case False{} True{} True{} False{} False{} True{} False{} False{}:
126      {==}
127    case True{} True{} True{} False{} False{} True{} False{} False{}:
128      {==}
129    case False{} False{} False{} True{} False{} True{} False{} False{}:
130      {==}
131    case True{} False{} False{} True{} False{} True{} False{} False{}:
132      {==}
133    case False{} True{} False{} True{} False{} True{} False{} False{}:
134      {==}
135    case True{} True{} False{} True{} False{} True{} False{} False{}:
136      {==}
137    case False{} False{} True{} True{} False{} True{} False{} False{}:
138      {==}
139    case True{} False{} True{} True{} False{} True{} False{} False{}:
140      {==}
141    case False{} True{} True{} True{} False{} True{} False{} False{}:
142      {==}
143    case True{} True{} True{} True{} False{} True{} False{} False{}:
144      {==}
145    case False{} False{} False{} False{} True{} True{} False{} False{}:
146      {==}
147    case True{} False{} False{} False{} True{} True{} False{} False{}:
148      {==}
149    case False{} True{} False{} False{} True{} True{} False{} False{}:
150      {==}
151    case True{} True{} False{} False{} True{} True{} False{} False{}:
152      {==}
153    case False{} False{} True{} False{} True{} True{} False{} False{}:
154      {==}
155    case True{} False{} True{} False{} True{} True{} False{} False{}:
156      {==}
157    case False{} True{} True{} False{} True{} True{} False{} False{}:
158      {==}
159    case True{} True{} True{} False{} True{} True{} False{} False{}:
160      {==}
161    case False{} False{} False{} True{} True{} True{} False{} False{}:
162      {==}
163    case True{} False{} False{} True{} True{} True{} False{} False{}:
164      {==}
165    case False{} True{} False{} True{} True{} True{} False{} False{}:
166      {==}
167    case True{} True{} False{} True{} True{} True{} False{} False{}:
168      {==}
169    case False{} False{} True{} True{} True{} True{} False{} False{}:
170      {==}
171    case True{} False{} True{} True{} True{} True{} False{} False{}:
172      {==}
173    case False{} True{} True{} True{} True{} True{} False{} False{}:
174      {==}
175    case True{} True{} True{} True{} True{} True{} False{} False{}:
176      {==}
177    case False{} False{} False{} False{} False{} False{} True{} False{}:
178      {==}
179    case True{} False{} False{} False{} False{} False{} True{} False{}:
180      {==}
181    case False{} True{} False{} False{} False{} False{} True{} False{}:
182      {==}
183    case True{} True{} False{} False{} False{} False{} True{} False{}:
184      {==}
185    case False{} False{} True{} False{} False{} False{} True{} False{}:
186      {==}
187    case True{} False{} True{} False{} False{} False{} True{} False{}:
188      {==}
189    case False{} True{} True{} False{} False{} False{} True{} False{}:
190      {==}
191    case True{} True{} True{} False{} False{} False{} True{} False{}:
192      {==}
193    case False{} False{} False{} True{} False{} False{} True{} False{}:
194      {==}
195    case True{} False{} False{} True{} False{} False{} True{} False{}:
196      {==}
197    case False{} True{} False{} True{} False{} False{} True{} False{}:
198      {==}
199    case True{} True{} False{} True{} False{} False{} True{} False{}:
200      {==}
201    case False{} False{} True{} True{} False{} False{} True{} False{}:
202      {==}
203    case True{} False{} True{} True{} False{} False{} True{} False{}:
204      {==}
205    case False{} True{} True{} True{} False{} False{} True{} False{}:
206      {==}
207    case True{} True{} True{} True{} False{} False{} True{} False{}:
208      {==}
209    case False{} False{} False{} False{} True{} False{} True{} False{}:
210      {==}
211    case True{} False{} False{} False{} True{} False{} True{} False{}:
212      {==}
213    case False{} True{} False{} False{} True{} False{} True{} False{}:
214      {==}
215    case True{} True{} False{} False{} True{} False{} True{} False{}:
216      {==}
217    case False{} False{} True{} False{} True{} False{} True{} False{}:
218      {==}
219    case True{} False{} True{} False{} True{} False{} True{} False{}:
220      {==}
221    case False{} True{} True{} False{} True{} False{} True{} False{}:
222      {==}
223    case True{} True{} True{} False{} True{} False{} True{} False{}:
224      {==}
225    case False{} False{} False{} True{} True{} False{} True{} False{}:
226      {==}
227    case True{} False{} False{} True{} True{} False{} True{} False{}:
228      {==}
229    case False{} True{} False{} True{} True{} False{} True{} False{}:
230      {==}
231    case True{} True{} False{} True{} True{} False{} True{} False{}:
232      {==}
233    case False{} False{} True{} True{} True{} False{} True{} False{}:
234      {==}
235    case True{} False{} True{} True{} True{} False{} True{} False{}:
236      {==}
237    case False{} True{} True{} True{} True{} False{} True{} False{}:
238      {==}
239    case True{} True{} True{} True{} True{} False{} True{} False{}:
240      {==}
241    case False{} False{} False{} False{} False{} True{} True{} False{}:
242      {==}
243    case True{} False{} False{} False{} False{} True{} True{} False{}:
244      {==}
245    case False{} True{} False{} False{} False{} True{} True{} False{}:
246      {==}
247    case True{} True{} False{} False{} False{} True{} True{} False{}:
248      {==}
249    case False{} False{} True{} False{} False{} True{} True{} False{}:
250      {==}
251    case True{} False{} True{} False{} False{} True{} True{} False{}:
252      {==}
253    case False{} True{} True{} False{} False{} True{} True{} False{}:
254      {==}
255    case True{} True{} True{} False{} False{} True{} True{} False{}:
256      {==}
257    case False{} False{} False{} True{} False{} True{} True{} False{}:
258      {==}
259    case True{} False{} False{} True{} False{} True{} True{} False{}:
260      {==}
261    case False{} True{} False{} True{} False{} True{} True{} False{}:
262      {==}
263    case True{} True{} False{} True{} False{} True{} True{} False{}:
264      {==}
265    case False{} False{} True{} True{} False{} True{} True{} False{}:
266      {==}
267    case True{} False{} True{} True{} False{} True{} True{} False{}:
268      {==}
269    case False{} True{} True{} True{} False{} True{} True{} False{}:
270      {==}
271    case True{} True{} True{} True{} False{} True{} True{} False{}:
272      {==}
273    case False{} False{} False{} False{} True{} True{} True{} False{}:
274      {==}
275    case True{} False{} False{} False{} True{} True{} True{} False{}:
276      {==}
277    case False{} True{} False{} False{} True{} True{} True{} False{}:
278      {==}
279    case True{} True{} False{} False{} True{} True{} True{} False{}:
280      {==}
281    case False{} False{} True{} False{} True{} True{} True{} False{}:
282      {==}
283    case True{} False{} True{} False{} True{} True{} True{} False{}:
284      {==}
285    case False{} True{} True{} False{} True{} True{} True{} False{}:
286      {==}
287    case True{} True{} True{} False{} True{} True{} True{} False{}:
288      {==}
289    case False{} False{} False{} True{} True{} True{} True{} False{}:
290      {==}
291    case True{} False{} False{} True{} True{} True{} True{} False{}:
292      {==}
293    case False{} True{} False{} True{} True{} True{} True{} False{}:
294      {==}
295    case True{} True{} False{} True{} True{} True{} True{} False{}:
296      {==}
297    case False{} False{} True{} True{} True{} True{} True{} False{}:
298      {==}
299    case True{} False{} True{} True{} True{} True{} True{} False{}:
300      {==}
301    case False{} True{} True{} True{} True{} True{} True{} False{}:
302      {==}
303    case True{} True{} True{} True{} True{} True{} True{} False{}:
304      {==}
305    case False{} False{} False{} False{} False{} False{} False{} True{}:
306      {==}
307    case True{} False{} False{} False{} False{} False{} False{} True{}:
308      {==}
309    case False{} True{} False{} False{} False{} False{} False{} True{}:
310      {==}
311    case True{} True{} False{} False{} False{} False{} False{} True{}:
312      {==}
313    case False{} False{} True{} False{} False{} False{} False{} True{}:
314      {==}
315    case True{} False{} True{} False{} False{} False{} False{} True{}:
316      {==}
317    case False{} True{} True{} False{} False{} False{} False{} True{}:
318      {==}
319    case True{} True{} True{} False{} False{} False{} False{} True{}:
320      {==}
321    case False{} False{} False{} True{} False{} False{} False{} True{}:
322      {==}
323    case True{} False{} False{} True{} False{} False{} False{} True{}:
324      {==}
325    case False{} True{} False{} True{} False{} False{} False{} True{}:
326      {==}
327    case True{} True{} False{} True{} False{} False{} False{} True{}:
328      {==}
329    case False{} False{} True{} True{} False{} False{} False{} True{}:
330      {==}
331    case True{} False{} True{} True{} False{} False{} False{} True{}:
332      {==}
333    case False{} True{} True{} True{} False{} False{} False{} True{}:
334      {==}
335    case True{} True{} True{} True{} False{} False{} False{} True{}:
336      {==}
337    case False{} False{} False{} False{} True{} False{} False{} True{}:
338      {==}
339    case True{} False{} False{} False{} True{} False{} False{} True{}:
340      {==}
341    case False{} True{} False{} False{} True{} False{} False{} True{}:
342      {==}
343    case True{} True{} False{} False{} True{} False{} False{} True{}:
344      {==}
345    case False{} False{} True{} False{} True{} False{} False{} True{}:
346      {==}
347    case True{} False{} True{} False{} True{} False{} False{} True{}:
348      {==}
349    case False{} True{} True{} False{} True{} False{} False{} True{}:
350      {==}
351    case True{} True{} True{} False{} True{} False{} False{} True{}:
352      {==}
353    case False{} False{} False{} True{} True{} False{} False{} True{}:
354      {==}
355    case True{} False{} False{} True{} True{} False{} False{} True{}:
356      {==}
357    case False{} True{} False{} True{} True{} False{} False{} True{}:
358      {==}
359    case True{} True{} False{} True{} True{} False{} False{} True{}:
360      {==}
361    case False{} False{} True{} True{} True{} False{} False{} True{}:
362      {==}
363    case True{} False{} True{} True{} True{} False{} False{} True{}:
364      {==}
365    case False{} True{} True{} True{} True{} False{} False{} True{}:
366      {==}
367    case True{} True{} True{} True{} True{} False{} False{} True{}:
368      {==}
369    case False{} False{} False{} False{} False{} True{} False{} True{}:
370      {==}
371    case True{} False{} False{} False{} False{} True{} False{} True{}:
372      {==}
373    case False{} True{} False{} False{} False{} True{} False{} True{}:
374      {==}
375    case True{} True{} False{} False{} False{} True{} False{} True{}:
376      {==}
377    case False{} False{} True{} False{} False{} True{} False{} True{}:
378      {==}
379    case True{} False{} True{} False{} False{} True{} False{} True{}:
380      {==}
381    case False{} True{} True{} False{} False{} True{} False{} True{}:
382      {==}
383    case True{} True{} True{} False{} False{} True{} False{} True{}:
384      {==}
385    case False{} False{} False{} True{} False{} True{} False{} True{}:
386      {==}
387    case True{} False{} False{} True{} False{} True{} False{} True{}:
388      {==}
389    case False{} True{} False{} True{} False{} True{} False{} True{}:
390      {==}
391    case True{} True{} False{} True{} False{} True{} False{} True{}:
392      {==}
393    case False{} False{} True{} True{} False{} True{} False{} True{}:
394      {==}
395    case True{} False{} True{} True{} False{} True{} False{} True{}:
396      {==}
397    case False{} True{} True{} True{} False{} True{} False{} True{}:
398      {==}
399    case True{} True{} True{} True{} False{} True{} False{} True{}:
400      {==}
401    case False{} False{} False{} False{} True{} True{} False{} True{}:
402      {==}
403    case True{} False{} False{} False{} True{} True{} False{} True{}:
404      {==}
405    case False{} True{} False{} False{} True{} True{} False{} True{}:
406      {==}
407    case True{} True{} False{} False{} True{} True{} False{} True{}:
408      {==}
409    case False{} False{} True{} False{} True{} True{} False{} True{}:
410      {==}
411    case True{} False{} True{} False{} True{} True{} False{} True{}:
412      {==}
413    case False{} True{} True{} False{} True{} True{} False{} True{}:
414      {==}
415    case True{} True{} True{} False{} True{} True{} False{} True{}:
416      {==}
417    case False{} False{} False{} True{} True{} True{} False{} True{}:
418      {==}
419    case True{} False{} False{} True{} True{} True{} False{} True{}:
420      {==}
421    case False{} True{} False{} True{} True{} True{} False{} True{}:
422      {==}
423    case True{} True{} False{} True{} True{} True{} False{} True{}:
424      {==}
425    case False{} False{} True{} True{} True{} True{} False{} True{}:
426      {==}
427    case True{} False{} True{} True{} True{} True{} False{} True{}:
428      {==}
429    case False{} True{} True{} True{} True{} True{} False{} True{}:
430      {==}
431    case True{} True{} True{} True{} True{} True{} False{} True{}:
432      {==}
433    case False{} False{} False{} False{} False{} False{} True{} True{}:
434      {==}
435    case True{} False{} False{} False{} False{} False{} True{} True{}:
436      {==}
437    case False{} True{} False{} False{} False{} False{} True{} True{}:
438      {==}
439    case True{} True{} False{} False{} False{} False{} True{} True{}:
440      {==}
441    case False{} False{} True{} False{} False{} False{} True{} True{}:
442      {==}
443    case True{} False{} True{} False{} False{} False{} True{} True{}:
444      {==}
445    case False{} True{} True{} False{} False{} False{} True{} True{}:
446      {==}
447    case True{} True{} True{} False{} False{} False{} True{} True{}:
448      {==}
449    case False{} False{} False{} True{} False{} False{} True{} True{}:
450      {==}
451    case True{} False{} False{} True{} False{} False{} True{} True{}:
452      {==}
453    case False{} True{} False{} True{} False{} False{} True{} True{}:
454      {==}
455    case True{} True{} False{} True{} False{} False{} True{} True{}:
456      {==}
457    case False{} False{} True{} True{} False{} False{} True{} True{}:
458      {==}
459    case True{} False{} True{} True{} False{} False{} True{} True{}:
460      {==}
461    case False{} True{} True{} True{} False{} False{} True{} True{}:
462      {==}
463    case True{} True{} True{} True{} False{} False{} True{} True{}:
464      {==}
465    case False{} False{} False{} False{} True{} False{} True{} True{}:
466      {==}
467    case True{} False{} False{} False{} True{} False{} True{} True{}:
468      {==}
469    case False{} True{} False{} False{} True{} False{} True{} True{}:
470      {==}
471    case True{} True{} False{} False{} True{} False{} True{} True{}:
472      {==}
473    case False{} False{} True{} False{} True{} False{} True{} True{}:
474      {==}
475    case True{} False{} True{} False{} True{} False{} True{} True{}:
476      {==}
477    case False{} True{} True{} False{} True{} False{} True{} True{}:
478      {==}
479    case True{} True{} True{} False{} True{} False{} True{} True{}:
480      {==}
481    case False{} False{} False{} True{} True{} False{} True{} True{}:
482      {==}
483    case True{} False{} False{} True{} True{} False{} True{} True{}:
484      {==}
485    case False{} True{} False{} True{} True{} False{} True{} True{}:
486      {==}
487    case True{} True{} False{} True{} True{} False{} True{} True{}:
488      {==}
489    case False{} False{} True{} True{} True{} False{} True{} True{}:
490      {==}
491    case True{} False{} True{} True{} True{} False{} True{} True{}:
492      {==}
493    case False{} True{} True{} True{} True{} False{} True{} True{}:
494      {==}
495    case True{} True{} True{} True{} True{} False{} True{} True{}:
496      {==}
497    case False{} False{} False{} False{} False{} True{} True{} True{}:
498      {==}
499    case True{} False{} False{} False{} False{} True{} True{} True{}:
500      {==}
501    case False{} True{} False{} False{} False{} True{} True{} True{}:
502      {==}
503    case True{} True{} False{} False{} False{} True{} True{} True{}:
504      {==}
505    case False{} False{} True{} False{} False{} True{} True{} True{}:
506      {==}
507    case True{} False{} True{} False{} False{} True{} True{} True{}:
508      {==}
509    case False{} True{} True{} False{} False{} True{} True{} True{}:
510      {==}
511    case True{} True{} True{} False{} False{} True{} True{} True{}:
512      {==}
513    case False{} False{} False{} True{} False{} True{} True{} True{}:
514      {==}
515    case True{} False{} False{} True{} False{} True{} True{} True{}:
516      {==}
517    case False{} True{} False{} True{} False{} True{} True{} True{}:
518      {==}
519    case True{} True{} False{} True{} False{} True{} True{} True{}:
520      {==}
521    case False{} False{} True{} True{} False{} True{} True{} True{}:
522      {==}
523    case True{} False{} True{} True{} False{} True{} True{} True{}:
524      {==}
525    case False{} True{} True{} True{} False{} True{} True{} True{}:
526      {==}
527    case True{} True{} True{} True{} False{} True{} True{} True{}:
528      {==}
529    case False{} False{} False{} False{} True{} True{} True{} True{}:
530      {==}
531    case True{} False{} False{} False{} True{} True{} True{} True{}:
532      {==}
533    case False{} True{} False{} False{} True{} True{} True{} True{}:
534      {==}
535    case True{} True{} False{} False{} True{} True{} True{} True{}:
536      {==}
537    case False{} False{} True{} False{} True{} True{} True{} True{}:
538      {==}
539    case True{} False{} True{} False{} True{} True{} True{} True{}:
540      {==}
541    case False{} True{} True{} False{} True{} True{} True{} True{}:
542      {==}
543    case True{} True{} True{} False{} True{} True{} True{} True{}:
544      {==}
545    case False{} False{} False{} True{} True{} True{} True{} True{}:
546      {==}
547    case True{} False{} False{} True{} True{} True{} True{} True{}:
548      {==}
549    case False{} True{} False{} True{} True{} True{} True{} True{}:
550      {==}
551    case True{} True{} False{} True{} True{} True{} True{} True{}:
552      {==}
553    case False{} False{} True{} True{} True{} True{} True{} True{}:
554      {==}
555    case True{} False{} True{} True{} True{} True{} True{} True{}:
556      {==}
557    case False{} True{} True{} True{} True{} True{} True{} True{}:
558      {==}
559    case True{} True{} True{} True{} True{} True{} True{} True{}:
560      {==}
561
562law inverse_unit:
563  for +x: U32
564  for +h: {U32.is_eq(U32.and(255, x), 0) == False{} : Bool}
565  {S.mul(x, S.inverse(x)) == 1 : U32}
566
567def inverse_unit(x, h):
568  match x:
569    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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
570      inverse_unit_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, h)
571
572law inverse_zero:
573  {S.inverse(0) == 0 : U32}
574
575def inverse_zero():
576  {==}