1 import Base 2 import ../../../src/crypto/aes/sbox.bend as B 3 import ../../../spec/crypto/aes/aes.bend as S 4 5 # Generated by tools/generators/aes/sbox.py. The constant-time byte 6 # functions equal FIPS 197 on every U32 (both read only the low 8 bits). 7 8 law 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 19 def 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 534 law 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 569 def 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 573 law sbox_ok: 574 for +x: U32 575 {B.sbox(x) == S.sbox(x) : U32} 576 577 def 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 582 law 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 617 def 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 1132 law xtime_ok: 1133 for +x: U32 1134 {B.xtime(x) == S.mul(2, x) : U32} 1135 1136 def 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 1141 law 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 1176 def 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 1691 law mul3_ok: 1692 for +x: U32 1693 {B.mul3(x) == S.mul(3, x) : U32} 1694 1695 def 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)