def mul_inv_aes.s01100

bend-osdev-gf@0.1.1.0 · PROOF.bend:2474

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

2474def mul_inv_aes.s01100(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, b5, b6, b7})))) == 1 : U32}:
2475  match b5:
2476    case True{}:
2477      match b6:
2478        case True{}:
2479          match b7:
2480            case True{}:
2481              {==}
2482            case False{}:
2483              {==}
2484        case False{}:
2485          match b7:
2486            case True{}:
2487              {==}
2488            case False{}:
2489              {==}
2490    case False{}:
2491      match b6:
2492        case True{}:
2493          match b7:
2494            case True{}:
2495              {==}
2496            case False{}:
2497              {==}
2498        case False{}:
2499          match b7:
2500            case True{}:
2501              {==}
2502            case False{}:
2503              {==}