def inv16.s

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

import Base
import bend-osdev-gf@0.1.1.0/gfm.bend as M

7564def inv16.s(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), fixm(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, Word.zero(28n)}}}}}), M.Gfm.elt(M.Gfm.gf16(), M.gfm.pow.start(M.Gfm.gf16(), fixm(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, Word.zero(28n)}}}}}), U32.sub(M.Gfm.mask(M.Gfm.gf16()), 1)))) == 1 : U32}:
7565  match b0:
7566    case True{}:
7567      match b1:
7568        case True{}:
7569          match b2:
7570            case True{}:
7571              match b3:
7572                case True{}:
7573                  {==}
7574                case False{}:
7575                  {==}
7576            case False{}:
7577              match b3:
7578                case True{}:
7579                  {==}
7580                case False{}:
7581                  {==}
7582        case False{}:
7583          match b2:
7584            case True{}:
7585              match b3:
7586                case True{}:
7587                  {==}
7588                case False{}:
7589                  {==}
7590            case False{}:
7591              match b3:
7592                case True{}:
7593                  {==}
7594                case False{}:
7595                  {==}
7596    case False{}:
7597      match b1:
7598        case True{}:
7599          match b2:
7600            case True{}:
7601              match b3:
7602                case True{}:
7603                  {==}
7604                case False{}:
7605                  {==}
7606            case False{}:
7607              match b3:
7608                case True{}:
7609                  {==}
7610                case False{}:
7611                  {==}
7612        case False{}:
7613          match b2:
7614            case True{}:
7615              match b3:
7616                case True{}:
7617                  {==}
7618                case False{}:
7619                  {==}
7620            case False{}:
7621              match b3:
7622                case True{}:
7623                  {==}
7624                case False{}:
7625                  {==}