def mul_inv_aes.s01010

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

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

2536def mul_inv_aes.s01010(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, b5, b6, b7})))) == 1 : U32}:
2537  match b5:
2538    case True{}:
2539      match b6:
2540        case True{}:
2541          match b7:
2542            case True{}:
2543              {==}
2544            case False{}:
2545              {==}
2546        case False{}:
2547          match b7:
2548            case True{}:
2549              {==}
2550            case False{}:
2551              {==}
2552    case False{}:
2553      match b6:
2554        case True{}:
2555          match b7:
2556            case True{}:
2557              {==}
2558            case False{}:
2559              {==}
2560        case False{}:
2561          match b7:
2562            case True{}:
2563              {==}
2564            case False{}:
2565              {==}