1 import Base 2 import ../../../spec/crypto/aes/aes.bend as S 3 import ../../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 11 law 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 47 def 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 562 law 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 567 def 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 572 law inverse_zero: 573 {S.inverse(0) == 0 : U32} 574 575 def inverse_zero(): 576 {==}