Return MatchIndeterminate (not MatchFailed) for mixed-determinacy matches in Eval and Implies modes (#4152)

The booster matcher's job is to return the truth — terms either
*definitely* cannot match (`MatchFailed`) or *cannot be decided* without
further simplification (`MatchIndeterminate`) — and leave it to the
caller to decide what to do with an indeterminate verdict. In `Eval` and
`Implies` modes the matcher previously short-circuited to a decisive
`MatchFailed` in several cases where the two terms could in fact
simplify or instantiate to something equivalent, so the deferral never
reached the caller. The unifying principle applied here: a decisive
`MatchFailed` is sound only when the mismatch is between *rigid* shapes
or sorts that cannot change under evaluation or instantiation; every
other mismatch must defer.

This matters most for function-equation evaluation:
`handleFunctionEquation` routes `FailedMatch _ -> continue` but
`IndeterminateMatch{} -> abort`. A spurious decisive `MatchFailed`
caused the evaluator to silently skip a higher-priority equation and
commit to a lower-priority catch-all, violating the priority contract
function equations rely on. For `Implies`, the indeterminate verdict
lets the existing simplify-LHS / simplify-RHS retry ladder in
`Pattern.Implies` attempt the discharge and report a residual non-match
as `indeterminate` rather than a decisive `valid:false`. Simplification
behaviour is unchanged — `handleSimplificationEquation` routes both
verdicts to `continue`.

**Behavioural changes (each previously a decisive `MatchFailed`, now
`addIndeterminate`):**
- `bindVariable`: a pattern variable rebinding to two terms that are not
both constructor-like (e.g. a domain value and a function application),
in all modes — matching what `Rewrite` already did.
- `match1`: a `FunctionApplication` pattern against a concrete
structured subject (`DomainValue`/`Injection`/`KMap`/`KList`/`KSet`) in
`Eval` — falls through to the shared catch-all.
- `match1`: an `Injection` pattern against a builtin collection
(`KMap`/`KList`/`KSet`) in `Eval`, making both directions of this pair
indeterminate (the reverse direction already was).
- `matchVar`: a pattern variable against a subject whose static sort is
not a subsort of the variable's, when the subject is a
`FunctionApplication` or `Var` and the two sorts share a subsort (the
subject can still narrow). Sort-disjoint pairs and rigid subjects keep
the decisive `DifferentSorts` failure.
- `matchInj`: an injection-vs-injection pair with differing sources
where a child on the wider-sorted side can narrow (a subject variable
child, or a pattern function child). Rigid children at incompatible
sorts keep the decisive failure.

**Refactor (no behaviour change):**
- `match1` is inverted to defer-by-default: the table now ends in one
generic `addIndeterminate` fall-through — the always-sound outcome — and
every row above it justifies something stronger (\and decomposition,
variable binding, same-category descent, or decisive failure). The
decisive cross-category rule is a single guarded row over a new
`isRigidCategory` predicate, making the rigidity principle executable
rather than commentary. The table shrinks from ~108 rows to 18.
`bindVariable` and `matchInj` no longer inspect their now-dead
`MatchType` argument.

**Tests:**
- Matcher-level cases pinning the post-fix contract in `MatchEval`,
`MatchImplies`, and `MatchRewrite`, plus a paired
function/simplification soundness-regression test in `ApplyEquations`
(`test_soundnessGap`) showing a high-priority indeterminate match
correctly aborts function-equation evaluation rather than falling
through to a lower-priority rule.
- A new exhaustive dispatch-class grid test (`MatchDispatch`) pinning
the result class (`S`/`F`/`I`) of all 3 × 9 × 9 = 243 (mode,
pattern-constructor, subject-constructor) combinations, so any future
`match1` change surfaces as a reviewable grid-cell diff.

**Validation:**
- Full booster unit-test suite passes (979 tests). The behavioural tests
were authored to fail against the pre-fix matcher and turn green only
with the `Match.hs` changes applied; the `MatchDispatch` grid was first
pinned on `master` and shows exactly the eight `Eval` cells
(`Injection`-vs-collection and `FunctionApplication`-vs-rigid) that this
branch flips from `F` to `I`.
- Tested downstream on KMIR, KEVM, and Kontrol and saw that it does not
cause any proofs to fail or performance regressions.

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: ehildenb

booster/library/Booster/Pattern/Match.hs

@@ -14,6 +14,7 @@ module Test.Booster.Pattern.ApplyEquations (
     test_simplifyConstraint,
     test_localFixpoint,
     test_errors,
+    test_soundnessGap,
 ) where
 
 import Control.Exception (finally)
@@ -320,6 +321,43 @@ test_errors =
     isLoop _ (Left err) = assertFailure $ "Unexpected error " <> show err
     isLoop _ (Right r) = assertFailure $ "Unexpected result " <> show r
 
+{- | Soundness regression test for 'Eval' mode of 'matchTerms': when a
+pattern variable rebinds to two terms that are not both constructor-like
+(e.g. a domain value and a function application), the matcher must
+return @MatchIndeterminate@, which routes through
+@IndeterminateMatch{} -> abort@ in 'handleFunctionEquation' and leaves
+the term unchanged so the caller can decide what to do.
+
+Before this was fixed, the matcher returned a decisive
+@MatchFailed VariableConflict@, which 'handleFunctionEquation' routes to
+@continue@ — silently skipping a higher-priority equation and committing
+to a lower-priority catch-all. Because function-equation priorities are
+semantically binding, that violated the priority contract.
+
+The simplification companion is the dual: simplification priorities are
+advisory, so both @FailedMatch@ and @IndeterminateMatch@ route to
+@continue@ and the behaviour is unchanged. The companion is included to
+pin that simplifications are unaffected by the fix.
+-}
+test_soundnessGap :: TestTree
+test_soundnessGap =
+    testGroup
+        "Eval matcher soundness: mixed-determinacy rebind"
+        [ testCase
+            "Function equations: high-priority indeterminate match aborts, lower-priority rule NOT tried"
+            $ do
+                let subj = [trm| f1{}(con3{}(\dv{SomeSort{}}("a"), f2{}(\dv{SomeSort{}}("x")))) |]
+                ns <- noSolver
+                runNoLoggingT (fst <$> evaluateTerm TopDown soundnessGapFunDef Nothing ns mempty mempty subj)
+                    @?>>= Right subj
+        , testCase "Simplifications: high-priority indeterminate match continues, lower-priority rule fires" $ do
+            let subj = [trm| f1{}(con3{}(\dv{SomeSort{}}("a"), f2{}(\dv{SomeSort{}}("x")))) |]
+                result = [trm| con2{}(con3{}(\dv{SomeSort{}}("a"), f2{}(\dv{SomeSort{}}("x")))) |]
+            ns <- noSolver
+            runNoLoggingT (fst <$> evaluateTerm TopDown soundnessGapSimplDef Nothing ns mempty mempty subj)
+                @?>>= Right result
+        ]
+
 ----------------------------------------
 
 index :: (ByteString -> CellIndex) -> SymbolName -> TermIndex
@@ -399,6 +437,47 @@ loopDef =
                 ]
         }
 
+{- | Rules used by 'test_soundnessGap'. Both definitions hold the same
+two equations on @f1@:
+
+* Priority 40: @f1(con3(X, X)) = con1(X)@ — narrow pattern that requires
+  the two arguments of @con3@ to be the same.
+* Priority 50: @f1(X) = con2(X)@ — catch-all.
+
+The test subject is @f1(con3(\\dv "a", f2(\\dv "x")))@: when matching
+the priority-40 rule's LHS, the variable @X@ is bound first to
+@\\dv "a"@ (constructor-like) and then to @f2(\\dv "x")@ (a
+'FunctionApplication', not constructor-like). 'Match.bindVariable'
+returns @MatchIndeterminate@ for this mixed-determinacy rebind (it
+returned a decisive @MatchFailed VariableConflict@ in 'Eval' mode
+before this was fixed).
+-}
+soundnessGapRules :: [RewriteRule t]
+soundnessGapRules =
+    [ equation
+        (Just "soundness-gap-pri40")
+        [trm| f1{}(con3{}(X:SomeSort{}, X:SomeSort{})) |]
+        [trm| con1{}(X:SomeSort{}) |]
+        40
+    , equation
+        (Just "soundness-gap-pri50")
+        [trm| f1{}(X:SomeSort{}) |]
+        [trm| con2{}(X:SomeSort{}) |]
+        50
+    ]
+
+soundnessGapFunDef, soundnessGapSimplDef :: KoreDefinition
+soundnessGapFunDef =
+    testDefinition
+        { functionEquations =
+            mkTheory [(index IdxFun "f1", soundnessGapRules)]
+        }
+soundnessGapSimplDef =
+    testDefinition
+        { simplifications =
+            mkTheory [(index IdxFun "f1", soundnessGapRules)]
+        }
+
 f1Equations, f2Equations :: [RewriteRule t]
 f1Equations =
     [ equation -- f1(con1(X)) == con2(f1(X))

booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs

@@ -108,12 +108,12 @@ grid Eval =
     --  And DV  Inj Map List Set Cons Fun Var
     [ [I, S, S, F, F, F, S, S, I] -- AndTerm
     , [I, S, F, F, F, F, F, I, I] -- DomainValue
-    , [I, F, S, F, F, F, F, I, I] -- Injection
+    , [I, F, S, I, I, I, F, I, I] -- Injection
     , [I, F, I, S, F, F, F, I, I] -- KMap
     , [I, F, I, F, S, F, F, I, I] -- KList
     , [I, F, I, F, F, S, F, I, I] -- KSet
     , [I, F, F, F, F, F, S, I, I] -- ConsApplication
-    , [I, F, F, F, F, F, I, S, I] -- FunctionApplication
+    , [I, I, I, I, I, I, I, S, I] -- FunctionApplication
     , [I, S, S, F, F, F, S, S, S] -- Var
     ]
 grid Implies =

booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs

@@ -30,6 +30,8 @@ test_match_eval =
         , composite
         , kmapTerms
         , internalSets
+        , variableRebindMixedDeterminacy
+        , injectionChildNarrowing
         ]
 
 symbols :: TestTree
@@ -66,10 +68,6 @@ symbols =
               subj = app con1 [d]
            in test "same constructor, different argument sorts" pat subj $
                 failed (DifferentSorts x d)
-        , let pat = app f1 [var "X" someSort]
-              subj = dv someSort "something"
-           in test "function and something else" pat subj $
-                failed (DifferentSymbols pat subj)
         ]
 
 composite :: TestTree
@@ -97,8 +95,8 @@ composite =
               b = var "B" someSort
               pat = app con3 [var "X" someSort, var "X" someSort] -- same!
               subj = app con3 [a, b]
-           in test "Matching two constructor argument to be the same (failing)" pat subj $
-                failed (VariableConflict (Variable someSort "X") a b)
+           in test "Matching two constructor argument to be the same (indeterminate)" pat subj $
+                remainderWith [("X", someSort, a)] [(a, b)]
         ]
 
 varsAndValues :: TestTree
@@ -115,8 +113,20 @@ varsAndValues =
                 success [("X", someSort, inj aSubsort someSort v2)]
         , let v1 = var "X" aSubsort
               v2 = var "Y" someSort
-           in test "two variables (v1 subsort v2)" v1 v2 $
+           in test "two variables (v1 subsort v2): indeterminate, Y may narrow" v1 v2 $
+                remainder [(v1, v2)]
+        , let v1 = var "X" aSubsort
+              v2 = var "Y" differentSort
+           in test "two variables (disjoint sorts): fail" v1 v2 $
                 failed (DifferentSorts v1 v2)
+        , let v1 = var "X" aSubsort
+              f = app f1 [dv someSort "y"]
+           in test "var against function call of wider sort: indeterminate, result may narrow" v1 f $
+                remainder [(v1, f)]
+        , let v1 = var "X" differentSort
+              f = app f1 [dv someSort "y"]
+           in test "var against function call of disjoint sort: fail" v1 f $
+                failed (DifferentSorts v1 f)
         , let v1 = var "X" someSort
               v2 = var "X" differentSort
            in test "same variable name, different sort" v1 v2 $
@@ -306,6 +316,109 @@ internalSets =
             (success [])
         ]
 
+{- | When a pattern variable is bound first to one term and then to
+another where the two terms are not both constructor-like (e.g. a
+domain value and a function application), the verdict must be
+'MatchIndeterminate', because the function application could simplify
+into the constructor-like term.
+
+A decisive 'MatchFailed VariableConflict' here would be a soundness gap
+for function-equation priorities: 'handleFunctionEquation'
+(Pattern.ApplyEquations) routes @FailedMatch _@ to @continue@ but
+@IndeterminateMatch{}@ to @abort@, so a spurious failure silently skips
+a higher-priority equation and commits to a lower-priority one. The
+tests below pin both orderings of the rebind.
+
+The companion soundness regression test lives in
+"Test.Booster.Pattern.ApplyEquations.test_soundnessGap".
+-}
+variableRebindMixedDeterminacy :: TestTree
+variableRebindMixedDeterminacy =
+    testGroup
+        "Variable rebinding with mixed-determinacy subject"
+        [ let d = dv someSort "1"
+              fnApp = app f1 [dv someSort "x"]
+              t1 = app con3 [var "X" someSort, var "X" someSort]
+              t2 = app con3 [d, fnApp]
+           in test
+                "Rebind X to a domain value then to a function application is indeterminate"
+                t1
+                t2
+                (remainderWith [("X", someSort, d)] [(d, fnApp)])
+        , let d = dv someSort "1"
+              fnApp = app f1 [dv someSort "x"]
+              t1 = app con3 [var "X" someSort, var "X" someSort]
+              t2 = app con3 [fnApp, d]
+           in test
+                "Rebind X to a function application then to a domain value is indeterminate"
+                t1
+                t2
+                (remainderWith [("X", someSort, fnApp)] [(fnApp, d)])
+        ]
+
+{- | Two injections with the same target but different source sorts can
+only be decisively distinguished when neither child can change sort: a
+function-application child may evaluate to a term of a narrower sort,
+and a variable child may be instantiated with one. Whenever the
+narrowable child sits on the wider-sorted side, the verdict is
+'MatchIndeterminate'; only rigid children at incompatible sorts fail
+decisively.
+-}
+injectionChildNarrowing :: TestTree
+injectionChildNarrowing =
+    let dSub = dv aSubsort "x"
+        dSome = dv someSort "y"
+        varSome = var "Y" someSort
+        varSub = var "Z" aSubsort
+        fnSome = app f1 [dSome]
+     in testGroup
+            "Injection children that may narrow"
+            [ test
+                "subject variable child of wider sort is indeterminate"
+                (Injection aSubsort kItemSort dSub)
+                (Injection someSort kItemSort varSome)
+                (remainder [(dSub, varSome)])
+            , test
+                "subject function child of wider sort is indeterminate"
+                (Injection aSubsort kItemSort dSub)
+                (Injection someSort kItemSort fnSome)
+                (remainder [(dSub, fnSome)])
+            , test
+                "pattern function child of wider sort is indeterminate"
+                (Injection someSort kItemSort fnSome)
+                (Injection aSubsort kItemSort dSub)
+                (remainder [(fnSome, dSub)])
+            , test
+                "rigid children at incompatible sorts fail"
+                (Injection aSubsort kItemSort dSub)
+                (Injection someSort kItemSort dSome)
+                ( failed $
+                    DifferentSorts
+                        (Injection aSubsort kItemSort dSub)
+                        (Injection someSort kItemSort dSome)
+                )
+            , -- Mirror of the wider-sort cases above, but with the non-rigid
+              -- child on the *narrower-sorted* side. Here no evaluation or
+              -- instantiation can bridge the sorts: normalising the narrower
+              -- injection wraps the child in an inj{aSubsort -> someSort}(...),
+              -- which the rigid wider-sorted pattern child (a domain value) can
+              -- never equal, whatever the variable resolves to. So the decisive
+              -- failure is kept rather than deferred. This pins the regression
+              -- behind keeping matchInj's catch-all decisive: broadening it to
+              -- addIndeterminate on any non-rigid child made a KEVM execution
+              -- abort instead of branch (rpc-integration test-3934-smt, where a
+              -- subject function child of a narrower sort took this same path).
+              test
+                "subject variable child of narrower sort fails"
+                (Injection someSort kItemSort dSome)
+                (Injection aSubsort kItemSort varSub)
+                ( failed $
+                    DifferentSorts
+                        (Injection someSort kItemSort dSome)
+                        (Injection aSubsort kItemSort varSub)
+                )
+            ]
+
 ----------------------------------------
 
 test :: String -> Term -> Term -> MatchResult -> TestTree
@@ -323,6 +436,23 @@ success assocs =
 failed :: FailReason -> MatchResult
 failed = MatchFailed
 
+remainder :: [(Term, Term)] -> MatchResult
+remainder = MatchIndeterminate mempty . NE.fromList
+
+{- | Like 'remainder' but also asserts a non-empty partial substitution
+from pairs that the matcher resolved before reaching the indeterminate
+pairs.
+-}
+remainderWith :: [(VarName, Sort, Term)] -> [(Term, Term)] -> MatchResult
+remainderWith assocs pairs =
+    MatchIndeterminate
+        ( Map.fromList
+            [ (Variable{variableSort, variableName}, term)
+            | (variableName, variableSort, term) <- assocs
+            ]
+        )
+        (NE.fromList pairs)
+
 errors :: String -> Term -> Term -> TestTree
 errors name pat subj =
     testCase name $

booster/unit-tests/Test/Booster/Pattern/MatchEval.hs

@@ -28,6 +28,7 @@ test_match_implies =
         [ constructors
         , functions
         , varsAndValues
+        , variableRebindMixedDeterminacy
         , andTerms
         , sorts
         , injections
@@ -126,9 +127,8 @@ constructors =
               z = var "Z" someSort
               t1 = app con3 [var "X" someSort, var "X" someSort]
               t2 = app con3 [y, z]
-           in test "Matching the same variable in a constructor (fail)" t1 t2 $
-                failed $
-                    VariableConflict (Variable someSort "X") y z
+           in test "Matching the same variable in a constructor (indeterminate)" t1 t2 $
+                remainderWith [("X", someSort, y)] [(y, z)]
         ]
 
 functions :: TestTree
@@ -181,7 +181,11 @@ varsAndValues =
                 success [("X", someSort, inj aSubsort someSort v2)]
         , let v1 = var "X" aSubsort
               v2 = var "Y" someSort
-           in test "two variables (v1 subsort v2)" v1 v2 $
+           in test "two variables (v1 subsort v2): indeterminate, Y may narrow" v1 v2 $
+                remainder [(v1, v2)]
+        , let v1 = var "X" aSubsort
+              v2 = var "Y" differentSort
+           in test "two variables (disjoint sorts): fail" v1 v2 $
                 failed (DifferentSorts v1 v2)
         , let v1 = var "X" someSort
               v2 = var "X" differentSort
@@ -213,6 +217,44 @@ varsAndValues =
                 failed (DifferentSorts v d)
         ]
 
+{- | A pattern variable that gets matched against two different subject
+positions — one a domain value (constructor-like), one a function
+application (not constructor-like) — must be reported as
+'MatchIndeterminate', because the second term might simplify into
+something equivalent to the first (the comment on 'bindVariable' says
+exactly this).
+
+A decisive 'MatchFailed VariableConflict' here (as 'Implies' mode
+returned before this was fixed) would be a soundness gap: the implies
+handler trusts the matcher's decisive verdict and returns a
+non-'indeterminate' @valid:false@, even though simplifying the function
+application could reveal the subsumption. The tests below pin both
+orderings of the rebind.
+-}
+variableRebindMixedDeterminacy :: TestTree
+variableRebindMixedDeterminacy =
+    testGroup
+        "Variable rebinding with mixed-determinacy subject"
+        [ let d = dv someSort "1"
+              fnApp = app f1 [dv someSort "x"]
+              t1 = app con3 [var "X" someSort, var "X" someSort]
+              t2 = app con3 [d, fnApp]
+           in test
+                "Rebind X to a domain value then to a function application is indeterminate"
+                t1
+                t2
+                (remainderWith [("X", someSort, d)] [(d, fnApp)])
+        , let d = dv someSort "1"
+              fnApp = app f1 [dv someSort "x"]
+              t1 = app con3 [var "X" someSort, var "X" someSort]
+              t2 = app con3 [fnApp, d]
+           in test
+                "Rebind X to a function application then to a domain value is indeterminate"
+                t1
+                t2
+                (remainderWith [("X", someSort, fnApp)] [(fnApp, d)])
+        ]
+
 andTerms :: TestTree
 andTerms =
     testGroup
@@ -517,6 +559,19 @@ failed = MatchFailed
 remainder :: [(Term, Term)] -> MatchResult
 remainder = MatchIndeterminate mempty . NE.fromList
 
+{- | Like 'remainder' but also asserts a non-empty partial substitution from
+pairs that the matcher resolved before reaching the indeterminate pairs.
+-}
+remainderWith :: [(VarName, Sort, Term)] -> [(Term, Term)] -> MatchResult
+remainderWith assocs pairs =
+    MatchIndeterminate
+        ( Map.fromList
+            [ (Variable{variableSort, variableName}, term)
+            | (variableName, variableSort, term) <- assocs
+            ]
+        )
+        (NE.fromList pairs)
+
 sortErr :: SortError -> MatchResult
 sortErr = MatchFailed . SubsortingError