def mul_inv_aes.s10110

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

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

2164def mul_inv_aes.s10110(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, b5, b6, b7})))) == 1 : U32}:
2165  match b5:
2166    case True{}:
2167      match b6:
2168        case True{}:
2169          match b7:
2170            case True{}:
2171              {==}
2172            case False{}:
2173              {==}
2174        case False{}:
2175          match b7:
2176            case True{}:
2177              {==}
2178            case False{}:
2179              {==}
2180    case False{}:
2181      match b6:
2182        case True{}:
2183          match b7:
2184            case True{}:
2185              {==}
2186            case False{}:
2187              {==}
2188        case False{}:
2189          match b7:
2190            case True{}:
2191              {==}
2192            case False{}:
2193              {==}