def ap.e_sbl
bend-osdev-aes@0.1.0.0 · PROOF.bend:50
import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-collections@1.0.0.0/src/crypto/aes/sbox.bend as SB
50def ap.e_sbl(c0: Bool, c1: Bool, c2: Bool, c3: Bool, c4: Bool, c5: Bool, c6: Bool, c7: Bool) -> {SB.sbox(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}}) == U32.and(255, SB.sbox(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}})) : U32}:
51 match c0 c1 c2 c3 c4 c5 c6 c7:
52 case False{} False{} False{} False{} False{} False{} False{} False{}:
53 {==}
54 case True{} False{} False{} False{} False{} False{} False{} False{}:
55 {==}
56 case False{} True{} False{} False{} False{} False{} False{} False{}:
57 {==}
58 case True{} True{} False{} False{} False{} False{} False{} False{}:
59 {==}
60 case False{} False{} True{} False{} False{} False{} False{} False{}:
61 {==}
62 case True{} False{} True{} False{} False{} False{} False{} False{}:
63 {==}
64 case False{} True{} True{} False{} False{} False{} False{} False{}:
65 {==}
66 case True{} True{} True{} False{} False{} False{} False{} False{}:
67 {==}
68 case False{} False{} False{} True{} False{} False{} False{} False{}:
69 {==}
70 case True{} False{} False{} True{} False{} False{} False{} False{}:
71 {==}
72 case False{} True{} False{} True{} False{} False{} False{} False{}:
73 {==}
74 case True{} True{} False{} True{} False{} False{} False{} False{}:
75 {==}
76 case False{} False{} True{} True{} False{} False{} False{} False{}:
77 {==}
78 case True{} False{} True{} True{} False{} False{} False{} False{}:
79 {==}
80 case False{} True{} True{} True{} False{} False{} False{} False{}:
81 {==}
82 case True{} True{} True{} True{} False{} False{} False{} False{}:
83 {==}
84 case False{} False{} False{} False{} True{} False{} False{} False{}:
85 {==}
86 case True{} False{} False{} False{} True{} False{} False{} False{}:
87 {==}
88 case False{} True{} False{} False{} True{} False{} False{} False{}:
89 {==}
90 case True{} True{} False{} False{} True{} False{} False{} False{}:
91 {==}
92 case False{} False{} True{} False{} True{} False{} False{} False{}:
93 {==}
94 case True{} False{} True{} False{} True{} False{} False{} False{}:
95 {==}
96 case False{} True{} True{} False{} True{} False{} False{} False{}:
97 {==}
98 case True{} True{} True{} False{} True{} False{} False{} False{}:
99 {==}
100 case False{} False{} False{} True{} True{} False{} False{} False{}:
101 {==}
102 case True{} False{} False{} True{} True{} False{} False{} False{}:
103 {==}
104 case False{} True{} False{} True{} True{} False{} False{} False{}:
105 {==}
106 case True{} True{} False{} True{} True{} False{} False{} False{}:
107 {==}
108 case False{} False{} True{} True{} True{} False{} False{} False{}:
109 {==}
110 case True{} False{} True{} True{} True{} False{} False{} False{}:
111 {==}
112 case False{} True{} True{} True{} True{} False{} False{} False{}:
113 {==}
114 case True{} True{} True{} True{} True{} False{} False{} False{}:
115 {==}
116 case False{} False{} False{} False{} False{} True{} False{} False{}:
117 {==}
118 case True{} False{} False{} False{} False{} True{} False{} False{}:
119 {==}
120 case False{} True{} False{} False{} False{} True{} False{} False{}:
121 {==}
122 case True{} True{} False{} False{} False{} True{} False{} False{}:
123 {==}
124 case False{} False{} True{} False{} False{} True{} False{} False{}:
125 {==}
126 case True{} False{} True{} False{} False{} True{} False{} False{}:
127 {==}
128 case False{} True{} True{} False{} False{} True{} False{} False{}:
129 {==}
130 case True{} True{} True{} False{} False{} True{} False{} False{}:
131 {==}
132 case False{} False{} False{} True{} False{} True{} False{} False{}:
133 {==}
134 case True{} False{} False{} True{} False{} True{} False{} False{}:
135 {==}
136 case False{} True{} False{} True{} False{} True{} False{} False{}:
137 {==}
138 case True{} True{} False{} True{} False{} True{} False{} False{}:
139 {==}
140 case False{} False{} True{} True{} False{} True{} False{} False{}:
141 {==}
142 case True{} False{} True{} True{} False{} True{} False{} False{}:
143 {==}
144 case False{} True{} True{} True{} False{} True{} False{} False{}:
145 {==}
146 case True{} True{} True{} True{} False{} True{} False{} False{}:
147 {==}
148 case False{} False{} False{} False{} True{} True{} False{} False{}:
149 {==}
150 case True{} False{} False{} False{} True{} True{} False{} False{}:
151 {==}
152 case False{} True{} False{} False{} True{} True{} False{} False{}:
153 {==}
154 case True{} True{} False{} False{} True{} True{} False{} False{}:
155 {==}
156 case False{} False{} True{} False{} True{} True{} False{} False{}:
157 {==}
158 case True{} False{} True{} False{} True{} True{} False{} False{}:
159 {==}
160 case False{} True{} True{} False{} True{} True{} False{} False{}:
161 {==}
162 case True{} True{} True{} False{} True{} True{} False{} False{}:
163 {==}
164 case False{} False{} False{} True{} True{} True{} False{} False{}:
165 {==}
166 case True{} False{} False{} True{} True{} True{} False{} False{}:
167 {==}
168 case False{} True{} False{} True{} True{} True{} False{} False{}:
169 {==}
170 case True{} True{} False{} True{} True{} True{} False{} False{}:
171 {==}
172 case False{} False{} True{} True{} True{} True{} False{} False{}:
173 {==}
174 case True{} False{} True{} True{} True{} True{} False{} False{}:
175 {==}
176 case False{} True{} True{} True{} True{} True{} False{} False{}:
177 {==}
178 case True{} True{} True{} True{} True{} True{} False{} False{}:
179 {==}
180 case False{} False{} False{} False{} False{} False{} True{} False{}:
181 {==}
182 case True{} False{} False{} False{} False{} False{} True{} False{}:
183 {==}
184 case False{} True{} False{} False{} False{} False{} True{} False{}:
185 {==}
186 case True{} True{} False{} False{} False{} False{} True{} False{}:
187 {==}
188 case False{} False{} True{} False{} False{} False{} True{} False{}:
189 {==}
190 case True{} False{} True{} False{} False{} False{} True{} False{}:
191 {==}
192 case False{} True{} True{} False{} False{} False{} True{} False{}:
193 {==}
194 case True{} True{} True{} False{} False{} False{} True{} False{}:
195 {==}
196 case False{} False{} False{} True{} False{} False{} True{} False{}:
197 {==}
198 case True{} False{} False{} True{} False{} False{} True{} False{}:
199 {==}
200 case False{} True{} False{} True{} False{} False{} True{} False{}:
201 {==}
202 case True{} True{} False{} True{} False{} False{} True{} False{}:
203 {==}
204 case False{} False{} True{} True{} False{} False{} True{} False{}:
205 {==}
206 case True{} False{} True{} True{} False{} False{} True{} False{}:
207 {==}
208 case False{} True{} True{} True{} False{} False{} True{} False{}:
209 {==}
210 case True{} True{} True{} True{} False{} False{} True{} False{}:
211 {==}
212 case False{} False{} False{} False{} True{} False{} True{} False{}:
213 {==}
214 case True{} False{} False{} False{} True{} False{} True{} False{}:
215 {==}
216 case False{} True{} False{} False{} True{} False{} True{} False{}:
217 {==}
218 case True{} True{} False{} False{} True{} False{} True{} False{}:
219 {==}
220 case False{} False{} True{} False{} True{} False{} True{} False{}:
221 {==}
222 case True{} False{} True{} False{} True{} False{} True{} False{}:
223 {==}
224 case False{} True{} True{} False{} True{} False{} True{} False{}:
225 {==}
226 case True{} True{} True{} False{} True{} False{} True{} False{}:
227 {==}
228 case False{} False{} False{} True{} True{} False{} True{} False{}:
229 {==}
230 case True{} False{} False{} True{} True{} False{} True{} False{}:
231 {==}
232 case False{} True{} False{} True{} True{} False{} True{} False{}:
233 {==}
234 case True{} True{} False{} True{} True{} False{} True{} False{}:
235 {==}
236 case False{} False{} True{} True{} True{} False{} True{} False{}:
237 {==}
238 case True{} False{} True{} True{} True{} False{} True{} False{}:
239 {==}
240 case False{} True{} True{} True{} True{} False{} True{} False{}:
241 {==}
242 case True{} True{} True{} True{} True{} False{} True{} False{}:
243 {==}
244 case False{} False{} False{} False{} False{} True{} True{} False{}:
245 {==}
246 case True{} False{} False{} False{} False{} True{} True{} False{}:
247 {==}
248 case False{} True{} False{} False{} False{} True{} True{} False{}:
249 {==}
250 case True{} True{} False{} False{} False{} True{} True{} False{}:
251 {==}
252 case False{} False{} True{} False{} False{} True{} True{} False{}:
253 {==}
254 case True{} False{} True{} False{} False{} True{} True{} False{}:
255 {==}
256 case False{} True{} True{} False{} False{} True{} True{} False{}:
257 {==}
258 case True{} True{} True{} False{} False{} True{} True{} False{}:
259 {==}
260 case False{} False{} False{} True{} False{} True{} True{} False{}:
261 {==}
262 case True{} False{} False{} True{} False{} True{} True{} False{}:
263 {==}
264 case False{} True{} False{} True{} False{} True{} True{} False{}:
265 {==}
266 case True{} True{} False{} True{} False{} True{} True{} False{}:
267 {==}
268 case False{} False{} True{} True{} False{} True{} True{} False{}:
269 {==}
270 case True{} False{} True{} True{} False{} True{} True{} False{}:
271 {==}
272 case False{} True{} True{} True{} False{} True{} True{} False{}:
273 {==}
274 case True{} True{} True{} True{} False{} True{} True{} False{}:
275 {==}
276 case False{} False{} False{} False{} True{} True{} True{} False{}:
277 {==}
278 case True{} False{} False{} False{} True{} True{} True{} False{}:
279 {==}
280 case False{} True{} False{} False{} True{} True{} True{} False{}:
281 {==}
282 case True{} True{} False{} False{} True{} True{} True{} False{}:
283 {==}
284 case False{} False{} True{} False{} True{} True{} True{} False{}:
285 {==}
286 case True{} False{} True{} False{} True{} True{} True{} False{}:
287 {==}
288 case False{} True{} True{} False{} True{} True{} True{} False{}:
289 {==}
290 case True{} True{} True{} False{} True{} True{} True{} False{}:
291 {==}
292 case False{} False{} False{} True{} True{} True{} True{} False{}:
293 {==}
294 case True{} False{} False{} True{} True{} True{} True{} False{}:
295 {==}
296 case False{} True{} False{} True{} True{} True{} True{} False{}:
297 {==}
298 case True{} True{} False{} True{} True{} True{} True{} False{}:
299 {==}
300 case False{} False{} True{} True{} True{} True{} True{} False{}:
301 {==}
302 case True{} False{} True{} True{} True{} True{} True{} False{}:
303 {==}
304 case False{} True{} True{} True{} True{} True{} True{} False{}:
305 {==}
306 case True{} True{} True{} True{} True{} True{} True{} False{}:
307 {==}
308 case False{} False{} False{} False{} False{} False{} False{} True{}:
309 {==}
310 case True{} False{} False{} False{} False{} False{} False{} True{}:
311 {==}
312 case False{} True{} False{} False{} False{} False{} False{} True{}:
313 {==}
314 case True{} True{} False{} False{} False{} False{} False{} True{}:
315 {==}
316 case False{} False{} True{} False{} False{} False{} False{} True{}:
317 {==}
318 case True{} False{} True{} False{} False{} False{} False{} True{}:
319 {==}
320 case False{} True{} True{} False{} False{} False{} False{} True{}:
321 {==}
322 case True{} True{} True{} False{} False{} False{} False{} True{}:
323 {==}
324 case False{} False{} False{} True{} False{} False{} False{} True{}:
325 {==}
326 case True{} False{} False{} True{} False{} False{} False{} True{}:
327 {==}
328 case False{} True{} False{} True{} False{} False{} False{} True{}:
329 {==}
330 case True{} True{} False{} True{} False{} False{} False{} True{}:
331 {==}
332 case False{} False{} True{} True{} False{} False{} False{} True{}:
333 {==}
334 case True{} False{} True{} True{} False{} False{} False{} True{}:
335 {==}
336 case False{} True{} True{} True{} False{} False{} False{} True{}:
337 {==}
338 case True{} True{} True{} True{} False{} False{} False{} True{}:
339 {==}
340 case False{} False{} False{} False{} True{} False{} False{} True{}:
341 {==}
342 case True{} False{} False{} False{} True{} False{} False{} True{}:
343 {==}
344 case False{} True{} False{} False{} True{} False{} False{} True{}:
345 {==}
346 case True{} True{} False{} False{} True{} False{} False{} True{}:
347 {==}
348 case False{} False{} True{} False{} True{} False{} False{} True{}:
349 {==}
350 case True{} False{} True{} False{} True{} False{} False{} True{}:
351 {==}
352 case False{} True{} True{} False{} True{} False{} False{} True{}:
353 {==}
354 case True{} True{} True{} False{} True{} False{} False{} True{}:
355 {==}
356 case False{} False{} False{} True{} True{} False{} False{} True{}:
357 {==}
358 case True{} False{} False{} True{} True{} False{} False{} True{}:
359 {==}
360 case False{} True{} False{} True{} True{} False{} False{} True{}:
361 {==}
362 case True{} True{} False{} True{} True{} False{} False{} True{}:
363 {==}
364 case False{} False{} True{} True{} True{} False{} False{} True{}:
365 {==}
366 case True{} False{} True{} True{} True{} False{} False{} True{}:
367 {==}
368 case False{} True{} True{} True{} True{} False{} False{} True{}:
369 {==}
370 case True{} True{} True{} True{} True{} False{} False{} True{}:
371 {==}
372 case False{} False{} False{} False{} False{} True{} False{} True{}:
373 {==}
374 case True{} False{} False{} False{} False{} True{} False{} True{}:
375 {==}
376 case False{} True{} False{} False{} False{} True{} False{} True{}:
377 {==}
378 case True{} True{} False{} False{} False{} True{} False{} True{}:
379 {==}
380 case False{} False{} True{} False{} False{} True{} False{} True{}:
381 {==}
382 case True{} False{} True{} False{} False{} True{} False{} True{}:
383 {==}
384 case False{} True{} True{} False{} False{} True{} False{} True{}:
385 {==}
386 case True{} True{} True{} False{} False{} True{} False{} True{}:
387 {==}
388 case False{} False{} False{} True{} False{} True{} False{} True{}:
389 {==}
390 case True{} False{} False{} True{} False{} True{} False{} True{}:
391 {==}
392 case False{} True{} False{} True{} False{} True{} False{} True{}:
393 {==}
394 case True{} True{} False{} True{} False{} True{} False{} True{}:
395 {==}
396 case False{} False{} True{} True{} False{} True{} False{} True{}:
397 {==}
398 case True{} False{} True{} True{} False{} True{} False{} True{}:
399 {==}
400 case False{} True{} True{} True{} False{} True{} False{} True{}:
401 {==}
402 case True{} True{} True{} True{} False{} True{} False{} True{}:
403 {==}
404 case False{} False{} False{} False{} True{} True{} False{} True{}:
405 {==}
406 case True{} False{} False{} False{} True{} True{} False{} True{}:
407 {==}
408 case False{} True{} False{} False{} True{} True{} False{} True{}:
409 {==}
410 case True{} True{} False{} False{} True{} True{} False{} True{}:
411 {==}
412 case False{} False{} True{} False{} True{} True{} False{} True{}:
413 {==}
414 case True{} False{} True{} False{} True{} True{} False{} True{}:
415 {==}
416 case False{} True{} True{} False{} True{} True{} False{} True{}:
417 {==}
418 case True{} True{} True{} False{} True{} True{} False{} True{}:
419 {==}
420 case False{} False{} False{} True{} True{} True{} False{} True{}:
421 {==}
422 case True{} False{} False{} True{} True{} True{} False{} True{}:
423 {==}
424 case False{} True{} False{} True{} True{} True{} False{} True{}:
425 {==}
426 case True{} True{} False{} True{} True{} True{} False{} True{}:
427 {==}
428 case False{} False{} True{} True{} True{} True{} False{} True{}:
429 {==}
430 case True{} False{} True{} True{} True{} True{} False{} True{}:
431 {==}
432 case False{} True{} True{} True{} True{} True{} False{} True{}:
433 {==}
434 case True{} True{} True{} True{} True{} True{} False{} True{}:
435 {==}
436 case False{} False{} False{} False{} False{} False{} True{} True{}:
437 {==}
438 case True{} False{} False{} False{} False{} False{} True{} True{}:
439 {==}
440 case False{} True{} False{} False{} False{} False{} True{} True{}:
441 {==}
442 case True{} True{} False{} False{} False{} False{} True{} True{}:
443 {==}
444 case False{} False{} True{} False{} False{} False{} True{} True{}:
445 {==}
446 case True{} False{} True{} False{} False{} False{} True{} True{}:
447 {==}
448 case False{} True{} True{} False{} False{} False{} True{} True{}:
449 {==}
450 case True{} True{} True{} False{} False{} False{} True{} True{}:
451 {==}
452 case False{} False{} False{} True{} False{} False{} True{} True{}:
453 {==}
454 case True{} False{} False{} True{} False{} False{} True{} True{}:
455 {==}
456 case False{} True{} False{} True{} False{} False{} True{} True{}:
457 {==}
458 case True{} True{} False{} True{} False{} False{} True{} True{}:
459 {==}
460 case False{} False{} True{} True{} False{} False{} True{} True{}:
461 {==}
462 case True{} False{} True{} True{} False{} False{} True{} True{}:
463 {==}
464 case False{} True{} True{} True{} False{} False{} True{} True{}:
465 {==}
466 case True{} True{} True{} True{} False{} False{} True{} True{}:
467 {==}
468 case False{} False{} False{} False{} True{} False{} True{} True{}:
469 {==}
470 case True{} False{} False{} False{} True{} False{} True{} True{}:
471 {==}
472 case False{} True{} False{} False{} True{} False{} True{} True{}:
473 {==}
474 case True{} True{} False{} False{} True{} False{} True{} True{}:
475 {==}
476 case False{} False{} True{} False{} True{} False{} True{} True{}:
477 {==}
478 case True{} False{} True{} False{} True{} False{} True{} True{}:
479 {==}
480 case False{} True{} True{} False{} True{} False{} True{} True{}:
481 {==}
482 case True{} True{} True{} False{} True{} False{} True{} True{}:
483 {==}
484 case False{} False{} False{} True{} True{} False{} True{} True{}:
485 {==}
486 case True{} False{} False{} True{} True{} False{} True{} True{}:
487 {==}
488 case False{} True{} False{} True{} True{} False{} True{} True{}:
489 {==}
490 case True{} True{} False{} True{} True{} False{} True{} True{}:
491 {==}
492 case False{} False{} True{} True{} True{} False{} True{} True{}:
493 {==}
494 case True{} False{} True{} True{} True{} False{} True{} True{}:
495 {==}
496 case False{} True{} True{} True{} True{} False{} True{} True{}:
497 {==}
498 case True{} True{} True{} True{} True{} False{} True{} True{}:
499 {==}
500 case False{} False{} False{} False{} False{} True{} True{} True{}:
501 {==}
502 case True{} False{} False{} False{} False{} True{} True{} True{}:
503 {==}
504 case False{} True{} False{} False{} False{} True{} True{} True{}:
505 {==}
506 case True{} True{} False{} False{} False{} True{} True{} True{}:
507 {==}
508 case False{} False{} True{} False{} False{} True{} True{} True{}:
509 {==}
510 case True{} False{} True{} False{} False{} True{} True{} True{}:
511 {==}
512 case False{} True{} True{} False{} False{} True{} True{} True{}:
513 {==}
514 case True{} True{} True{} False{} False{} True{} True{} True{}:
515 {==}
516 case False{} False{} False{} True{} False{} True{} True{} True{}:
517 {==}
518 case True{} False{} False{} True{} False{} True{} True{} True{}:
519 {==}
520 case False{} True{} False{} True{} False{} True{} True{} True{}:
521 {==}
522 case True{} True{} False{} True{} False{} True{} True{} True{}:
523 {==}
524 case False{} False{} True{} True{} False{} True{} True{} True{}:
525 {==}
526 case True{} False{} True{} True{} False{} True{} True{} True{}:
527 {==}
528 case False{} True{} True{} True{} False{} True{} True{} True{}:
529 {==}
530 case True{} True{} True{} True{} False{} True{} True{} True{}:
531 {==}
532 case False{} False{} False{} False{} True{} True{} True{} True{}:
533 {==}
534 case True{} False{} False{} False{} True{} True{} True{} True{}:
535 {==}
536 case False{} True{} False{} False{} True{} True{} True{} True{}:
537 {==}
538 case True{} True{} False{} False{} True{} True{} True{} True{}:
539 {==}
540 case False{} False{} True{} False{} True{} True{} True{} True{}:
541 {==}
542 case True{} False{} True{} False{} True{} True{} True{} True{}:
543 {==}
544 case False{} True{} True{} False{} True{} True{} True{} True{}:
545 {==}
546 case True{} True{} True{} False{} True{} True{} True{} True{}:
547 {==}
548 case False{} False{} False{} True{} True{} True{} True{} True{}:
549 {==}
550 case True{} False{} False{} True{} True{} True{} True{} True{}:
551 {==}
552 case False{} True{} False{} True{} True{} True{} True{} True{}:
553 {==}
554 case True{} True{} False{} True{} True{} True{} True{} True{}:
555 {==}
556 case False{} False{} True{} True{} True{} True{} True{} True{}:
557 {==}
558 case True{} False{} True{} True{} True{} True{} True{} True{}:
559 {==}
560 case False{} True{} True{} True{} True{} True{} True{} True{}:
561 {==}
562 case True{} True{} True{} True{} True{} True{} True{} True{}:
563 {==}