def mul_inv_aes.s11101

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

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

1947def mul_inv_aes.s11101(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, b5, b6, b7})))) == 1 : U32}:
1948  match b5:
1949    case True{}:
1950      match b6:
1951        case True{}:
1952          match b7:
1953            case True{}:
1954              {==}
1955            case False{}:
1956              {==}
1957        case False{}:
1958          match b7:
1959            case True{}:
1960              {==}
1961            case False{}:
1962              {==}
1963    case False{}:
1964      match b6:
1965        case True{}:
1966          match b7:
1967            case True{}:
1968              {==}
1969            case False{}:
1970              {==}
1971        case False{}:
1972          match b7:
1973            case True{}:
1974              {==}
1975            case False{}:
1976              {==}