From 98a985cf19380539ec826945620f27fef72e164d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 1 Jun 2026 02:46:50 +0000 Subject: [PATCH 01/12] booster/unit-tests/Pattern/MatchImplies: add failing tests for variable-rebind with mixed-determinacy subject When the matcher (in Implies mode) sees a pattern variable bound first to a domain value and then to a function application (or vice versa), it currently returns a decisive MatchFailed VariableConflict, even though the function application could simplify into the domain value (or anything equivalent). The pyk team's recover-mode sweep depends on a sound MatchIndeterminate verdict here so the implies handler's existing simplify-LHS / simplify-RHS retry ladder can attempt the discharge, and a residual non-match can be reported with indeterminate:true rather than as a decisive valid:false. Pin both orderings of the rebind. Tests are expected to fail until Match.bindVariable in Implies mode mirrors Rewrite mode's addIndeterminate. (cherry picked from commit 1700d2d0f5dd89836c86a92f057275ac15756a64) --- .../Test/Booster/Pattern/MatchImplies.hs | 54 +++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs index 7d50efb673..8473705f32 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs @@ -28,6 +28,7 @@ test_match_implies = [ constructors , functions , varsAndValues + , variableRebindMixedDeterminacy , andTerms , sorts , injections @@ -213,6 +214,46 @@ 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) — is currently reported as a decisive +'MatchFailed VariableConflict' in 'Implies' mode. That matches what the +matcher does for 'Eval' but diverges from 'Rewrite', which routes the same +shape through 'addIndeterminate' because the second term might simplify +into something equivalent to the first (the comment on 'bindVariable' says +exactly this). + +For 'Implies' this asymmetry causes a soundness gap: the implies handler +trusts the matcher's decisive verdict and returns a non-'indeterminate' +@valid:false@, even though kore would simplify the function application +and find the subsumption. The tests below pin both orderings of the +rebind; they are expected to fail until 'Implies' mirrors 'Rewrite' in +'Match.bindVariable'. +-} +variableRebindMixedDeterminacy :: TestTree +variableRebindMixedDeterminacy = + testGroup + "Variable rebinding with mixed-determinacy subject (currently failing)" + [ 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 +558,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 From 549056c922bfbdc6ce8ab2de546f99271c8bd01b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 1 Jun 2026 02:50:49 +0000 Subject: [PATCH 02/12] booster/Pattern/Match, unit-tests/Pattern/MatchImplies: route Implies mode through addIndeterminate on mixed-determinacy rebind MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit In Match.bindVariable, when a variable is bound a second time and the two terms are not both constructor-like, the matcher previously failed with a decisive VariableConflict in both Eval and Implies modes. That is sound for Eval (the equation evaluator skips to the next priority on MatchFailed) but unsound for Implies: the comment two lines up — "the term in the binding could be equivalent (not necessarily syntactically equal)" — captures exactly why such a decision should be deferred. Routing this case through addIndeterminate lets the existing simplify-LHS / simplify-RHS retry ladder in Pattern.Implies attempt to discharge the equivalence and, on residual failure, mark the implication indeterminate so recover-mode pyk can escalate to a kore-enabled retry. Eval keeps the failWith path pending a separate soundness review of the function-equation evaluator, which currently treats MatchFailed as "skip and try next priority" while it treats MatchIndeterminate as "abort". The comment on the carve-out documents this distinction. Also flip the pre-existing "Matching the same variable in a constructor" test in MatchImplies from MatchFailed to the new MatchIndeterminate expectation, mirroring MatchRewrite's analogous case. (cherry picked from commit 262d49858688eced23a309c7be83489c0a258a09) --- booster/library/Booster/Pattern/Match.hs | 16 ++++++++++++---- .../Test/Booster/Pattern/MatchImplies.hs | 5 ++--- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 64d56776a2..c991d8129f 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -811,11 +811,19 @@ bindVariable matchType var term@(Term termAttrs _) = do , oldTermAttrs.isConstructorLike -> failWith $ VariableConflict var oldTerm term | otherwise -> - -- the term in the binding could be _equivalent_ - -- (not necessarily syntactically equal) to term' + -- The term in the binding could be _equivalent_ (not + -- necessarily syntactically equal) to 'term'. For 'Rewrite' + -- and 'Implies', the indeterminate verdict lets the caller + -- attempt to discharge the equivalence — e.g. via the + -- 'MatchIndeterminate' simplify-LHS / simplify-RHS retry + -- ladder in 'Pattern.Implies', or via the partial-substitution + -- pruning in 'Pattern.Rewrite' — instead of committing to a + -- (possibly unsound) decisive 'MatchFailed'. 'Eval' keeps + -- 'failWith' because the equation evaluator uses priority + -- ordering and treats 'MatchFailed' as "skip and try next." case matchType of - Rewrite -> addIndeterminate oldTerm term - _ -> failWith $ VariableConflict var oldTerm term + Eval -> failWith $ VariableConflict var oldTerm term + _ -> addIndeterminate oldTerm term Nothing -> do let -- apply existing substitutions to term diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs index 8473705f32..e7ffa11d1f 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs @@ -127,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 From c9e1c3f2903574a704007a49428fa376634d556d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 1 Jun 2026 03:12:03 +0000 Subject: [PATCH 03/12] booster/unit-tests/Pattern/{MatchEval,ApplyEquations}: add failing tests for Eval matcher soundness gap In Eval mode the matcher today returns a decisive MatchFailed when: - a pattern variable rebinds to two terms that aren't both constructor-like (Match.hs:825), and - a function-application pattern is matched against a concrete structured subject (Injection/KMap/KList/KSet, match1 lines 289, 291, 293, 295). The "truth" verdict for both shapes is MatchIndeterminate: the function side could simplify into something equivalent to the constructor-like side, and the matcher cannot decide that without further work. Because handleFunctionEquation (ApplyEquations.hs) routes FailedMatch _ to continue but IndeterminateMatch{} to abort, the current decisive verdict silently skips a higher-priority equation and commits to a lower-priority catch-all, violating the priority contract function equations rely on. This adds six matcher-level tests (MatchEval.hs) and a paired function/simplification soundness-regression test (ApplyEquations.hs) that pin the post-fix contract. All seven new tests are expected to fail until Match.bindVariable and the five Eval-specific match1 lines mirror the catch-all behaviour. The simplification companion already passes today and serves to pin that simplifications are unaffected by the proposed fix. (cherry picked from commit a61e40fb842f002b1d315b5785b4a61610b332b0) --- .../Test/Booster/Pattern/ApplyEquations.hs | 78 +++++++++++++ .../Test/Booster/Pattern/MatchEval.hs | 107 ++++++++++++++++++ 2 files changed, 185 insertions(+) diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index b2353bae83..8d8ec41dd5 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -13,6 +13,7 @@ module Test.Booster.Pattern.ApplyEquations ( test_simplifyPattern, test_simplifyConstraint, test_errors, + test_soundnessGap, ) where import Control.Monad.Logger (runNoLoggingT) @@ -248,6 +249,43 @@ test_errors = isLoop _ (Left err) = assertFailure $ "Unexpected error " <> show err isLoop _ (Right r) = assertFailure $ "Unexpected result " <> show r +{- | Soundness gap 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 today returns a +decisive @MatchFailed VariableConflict@. 'handleFunctionEquation' +(ApplyEquations.hs) routes @FailedMatch _@ to @continue@, which silently +skips a higher-priority equation and commits to a lower-priority +catch-all. Because function-equation priorities are semantically binding, +this violates the priority contract. + +Under the proposed fix, the matcher returns @MatchIndeterminate@ for the +same shape, which routes through @IndeterminateMatch{} -> abort@ and +leaves the term unchanged so the caller can decide what to do. + +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 @@ -327,6 +365,46 @@ 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' in +'Eval' mode currently returns @MatchFailed VariableConflict@; under the +proposed fix it would return @MatchIndeterminate@ instead. +-} +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)) diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs index 18f9c8533d..2ce83a6d7f 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs @@ -30,6 +30,8 @@ test_match_eval = , composite , kmapTerms , internalSets + , variableRebindMixedDeterminacy + , functionApplicationAgainstConcreteCategories ] symbols :: TestTree @@ -306,6 +308,94 @@ internalSets = (success []) ] +{- | The matcher in 'Eval' mode currently returns a decisive +'MatchFailed VariableConflict' 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 +"truth" verdict here is 'MatchIndeterminate', because the function +application could simplify into the constructor-like term. + +Because 'handleFunctionEquation' (Pattern.ApplyEquations) routes +@FailedMatch _@ to @continue@ but @IndeterminateMatch{}@ to @abort@, the +current behaviour silently skips a higher-priority equation and commits +to a lower-priority one — a soundness gap for function-equation +priorities. The tests below pin both orderings of the rebind; they are +expected to fail until 'Eval' mode mirrors 'Rewrite' / 'Implies' in +'Match.bindVariable'. + +The companion soundness regression test lives in +"Test.Booster.Pattern.ApplyEquations.test_soundnessGap". +-} +variableRebindMixedDeterminacy :: TestTree +variableRebindMixedDeterminacy = + testGroup + "Variable rebinding with mixed-determinacy subject (currently failing)" + [ 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)]) + ] + +{- | When the pattern (rule LHS) contains a function application and the +subject in that position is a structured term — an injection, a map, a +list, or a set — 'Eval' currently returns a decisive +'MatchFailed DifferentSymbols'. The "truth" verdict is +'MatchIndeterminate', because the function application could in +principle simplify into the corresponding category. The four tests +mirror the four 'match1' lines that currently @failWith@ in Eval mode +(@FunctionApplication{}@ paired with @Injection{} / KMap{} / KList{} / +KSet{}@). The companion case for @DomainValue{}@ is covered by an +existing test in the 'symbols' group; both flips happen in the impl +commit. +-} +functionApplicationAgainstConcreteCategories :: TestTree +functionApplicationAgainstConcreteCategories = + testGroup + "FunctionApplication pattern against concrete categories (currently failing)" + [ let pat = app f1 [var "X" someSort] + subj = Injection aSubsort someSort (dv aSubsort "x") + in test + "FunctionApplication pattern with Injection subject is indeterminate" + pat + subj + (remainder [(pat, subj)]) + , let pat = app f1 [var "X" someSort] + subj = emptyKMap + in test + "FunctionApplication pattern with KMap subject is indeterminate" + pat + subj + (remainder [(pat, subj)]) + , let pat = app f1 [var "X" someSort] + subj = emptyList + in test + "FunctionApplication pattern with KList subject is indeterminate" + pat + subj + (remainder [(pat, subj)]) + , let pat = app f1 [var "X" someSort] + subj = emptySet + in test + "FunctionApplication pattern with KSet subject is indeterminate" + pat + subj + (remainder [(pat, subj)]) + ] + ---------------------------------------- test :: String -> Term -> Term -> MatchResult -> TestTree @@ -323,6 +413,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 $ From fa5ede6307a38e60c012c8b47f86e0c2ccea9a6e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 1 Jun 2026 03:19:37 +0000 Subject: [PATCH 04/12] booster/Pattern/Match, unit-tests/Pattern/MatchEval: route Eval mode through addIndeterminate on mixed-determinacy match MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The matcher's job is to return the truth — terms either definitely cannot match (MatchFailed) or cannot be decided without simplification (MatchIndeterminate) — and to let the caller decide what to do. Eval mode previously short-circuited in two places where the terms involved could in fact simplify to be equivalent: - Match.bindVariable rebind where the two terms are not both constructor-like (e.g. a domain value and a function application): previously failWith $ VariableConflict; now addIndeterminate, like Rewrite and Implies. - Five match1 lines that pair a FunctionApplication pattern with a concrete structured subject (DomainValue, Injection, KMap, KList, KSet): previously failWith $ DifferentSymbols in Eval mode; the Eval-specific lines are now dropped so the same catch-all that handles Rewrite/Implies (addIndeterminate) handles Eval too. The downstream contract — handleFunctionEquation routes @IndeterminateMatch{} -> abort@ while @FailedMatch _ -> continue@ — now correctly stops function-equation iteration at an indeterminate match instead of silently skipping a higher-priority equation and committing to a lower-priority catch-all. Function-equation priorities are "semantically binding" (per the comment on handleFunctionEquation), so preserving priority order under the matcher's deferred verdict is the sound thing to do. handleSimplificationEquation routes both verdicts to @continue@, so simplification behaviour is unchanged. The simplification companion in test_soundnessGap pins this. Also flip the two pre-existing MatchEval tests whose expectations become stale ("function and something else" and "Matching two constructor argument to be the same (failing)") from MatchFailed to the new MatchIndeterminate verdict. (cherry picked from commit b004b6f5270a57ff620877bbdd783a369c924a24) --- booster/library/Booster/Pattern/Match.hs | 29 ++++++++----------- .../Test/Booster/Pattern/MatchEval.hs | 8 ++--- 2 files changed, 16 insertions(+), 21 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index c991d8129f..314951de85 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -284,15 +284,10 @@ match1 Rewrite t1@ConsApplication{} (Var t2) match1 _ t1@ConsApplication{} t2@Var{} = addIndeterminate t1 t2 match1 Eval t1@FunctionApplication{} t2@AndTerm{} = addIndeterminate t1 t2 match1 _ t1@FunctionApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 Eval t1@FunctionApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@FunctionApplication{} t2@DomainValue{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@FunctionApplication{} t2@Injection{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@FunctionApplication{} t2@KMap{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@FunctionApplication{} t2@KList{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@FunctionApplication{} t2@KSet{} = addIndeterminate t1 t2 match1 Eval (FunctionApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 match1 _ t1@FunctionApplication{} t2@ConsApplication{} = addIndeterminate t1 t2 @@ -812,18 +807,18 @@ bindVariable matchType var term@(Term termAttrs _) = do failWith $ VariableConflict var oldTerm term | otherwise -> -- The term in the binding could be _equivalent_ (not - -- necessarily syntactically equal) to 'term'. For 'Rewrite' - -- and 'Implies', the indeterminate verdict lets the caller - -- attempt to discharge the equivalence — e.g. via the - -- 'MatchIndeterminate' simplify-LHS / simplify-RHS retry - -- ladder in 'Pattern.Implies', or via the partial-substitution - -- pruning in 'Pattern.Rewrite' — instead of committing to a - -- (possibly unsound) decisive 'MatchFailed'. 'Eval' keeps - -- 'failWith' because the equation evaluator uses priority - -- ordering and treats 'MatchFailed' as "skip and try next." - case matchType of - Eval -> failWith $ VariableConflict var oldTerm term - _ -> addIndeterminate oldTerm term + -- necessarily syntactically equal) to 'term'. Defer to the + -- caller via 'addIndeterminate' so it can attempt to + -- discharge the equivalence — e.g. via the + -- 'MatchIndeterminate' simplify retry ladder in + -- 'Pattern.Implies', the partial-substitution pruning in + -- 'Pattern.Rewrite', or 'handleFunctionEquation's + -- @IndeterminateMatch{} -> abort@ contract in + -- 'Pattern.ApplyEquations'. Returning 'MatchFailed' here + -- (the previous 'Eval'-only behaviour) silently skipped + -- higher-priority function equations and committed to a + -- lower-priority catch-all, violating priority semantics. + addIndeterminate oldTerm term Nothing -> do let -- apply existing substitutions to term diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs index 2ce83a6d7f..a77e4543b2 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs @@ -70,8 +70,8 @@ symbols = 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) + in test "function and something else (indeterminate)" pat subj $ + remainder [(pat, subj)] ] composite :: TestTree @@ -99,8 +99,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 From 533abf82df2c74a4397fa629708b3d223e74ea20 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 8 Jun 2026 21:04:54 +0000 Subject: [PATCH 05/12] booster/Pattern/Match: trim bindVariable indeterminate-rebind comment The mixed-determinacy rebind comment had grown to a verbose paragraph. Restore master's concise wording, keeping only the one new fact: all modes now defer (a decisive MatchFailed would skip higher-priority equations) rather than re-listing every caller's discharge mechanism. Co-Authored-By: Claude Opus 4.8 --- booster/library/Booster/Pattern/Match.hs | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 314951de85..9ff560229b 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -806,18 +806,10 @@ bindVariable matchType var term@(Term termAttrs _) = do , oldTermAttrs.isConstructorLike -> failWith $ VariableConflict var oldTerm term | otherwise -> - -- The term in the binding could be _equivalent_ (not - -- necessarily syntactically equal) to 'term'. Defer to the - -- caller via 'addIndeterminate' so it can attempt to - -- discharge the equivalence — e.g. via the - -- 'MatchIndeterminate' simplify retry ladder in - -- 'Pattern.Implies', the partial-substitution pruning in - -- 'Pattern.Rewrite', or 'handleFunctionEquation's - -- @IndeterminateMatch{} -> abort@ contract in - -- 'Pattern.ApplyEquations'. Returning 'MatchFailed' here - -- (the previous 'Eval'-only behaviour) silently skipped - -- higher-priority function equations and committed to a - -- lower-priority catch-all, violating priority semantics. + -- the term in the binding could be _equivalent_ + -- (not necessarily syntactically equal) to term, so we + -- defer rather than fail in every mode: a decisive + -- MatchFailed here would skip higher-priority equations. addIndeterminate oldTerm term Nothing -> do let From af47403c8fe42ed1eb53dc6142fe446f59d9c1c1 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 11 Jun 2026 20:34:06 +0000 Subject: [PATCH 06/12] booster/unit-tests/Pattern/{MatchEval,MatchImplies,ApplyEquations}: reword test docs to post-fix framing The test-first commits documented the soundness gap as present ("currently failing", "under the proposed fix"), and the fix commits never updated the wording, leaving group names claiming tests fail while they pass. Reword to describe the pinned contract, mentioning the pre-fix behaviour as history. Co-Authored-By: Claude Fable 5 --- .../Test/Booster/Pattern/ApplyEquations.hs | 31 ++++++------- .../Test/Booster/Pattern/MatchEval.hs | 45 +++++++++---------- .../Test/Booster/Pattern/MatchImplies.hs | 22 +++++---- 3 files changed, 47 insertions(+), 51 deletions(-) diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index bfe53eebd2..0839726ccf 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -321,18 +321,18 @@ test_errors = isLoop _ (Left err) = assertFailure $ "Unexpected error " <> show err isLoop _ (Right r) = assertFailure $ "Unexpected result " <> show r -{- | Soundness gap 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 today returns a -decisive @MatchFailed VariableConflict@. 'handleFunctionEquation' -(ApplyEquations.hs) routes @FailedMatch _@ to @continue@, which silently -skips a higher-priority equation and commits to a lower-priority -catch-all. Because function-equation priorities are semantically binding, -this violates the priority contract. - -Under the proposed fix, the matcher returns @MatchIndeterminate@ for the -same shape, which routes through @IndeterminateMatch{} -> abort@ and -leaves the term unchanged so the caller can decide what to do. +{- | 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 @@ -447,9 +447,10 @@ two equations on @f1@: 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' in -'Eval' mode currently returns @MatchFailed VariableConflict@; under the -proposed fix it would return @MatchIndeterminate@ instead. +'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 = diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs index a77e4543b2..e0bb362fc1 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs @@ -308,20 +308,18 @@ internalSets = (success []) ] -{- | The matcher in 'Eval' mode currently returns a decisive -'MatchFailed VariableConflict' 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 -"truth" verdict here is 'MatchIndeterminate', because the function -application could simplify into the constructor-like term. +{- | 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. -Because 'handleFunctionEquation' (Pattern.ApplyEquations) routes -@FailedMatch _@ to @continue@ but @IndeterminateMatch{}@ to @abort@, the -current behaviour silently skips a higher-priority equation and commits -to a lower-priority one — a soundness gap for function-equation -priorities. The tests below pin both orderings of the rebind; they are -expected to fail until 'Eval' mode mirrors 'Rewrite' / 'Implies' in -'Match.bindVariable'. +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". @@ -329,7 +327,7 @@ The companion soundness regression test lives in variableRebindMixedDeterminacy :: TestTree variableRebindMixedDeterminacy = testGroup - "Variable rebinding with mixed-determinacy subject (currently failing)" + "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] @@ -352,20 +350,19 @@ variableRebindMixedDeterminacy = {- | When the pattern (rule LHS) contains a function application and the subject in that position is a structured term — an injection, a map, a -list, or a set — 'Eval' currently returns a decisive -'MatchFailed DifferentSymbols'. The "truth" verdict is -'MatchIndeterminate', because the function application could in -principle simplify into the corresponding category. The four tests -mirror the four 'match1' lines that currently @failWith@ in Eval mode -(@FunctionApplication{}@ paired with @Injection{} / KMap{} / KList{} / -KSet{}@). The companion case for @DomainValue{}@ is covered by an -existing test in the 'symbols' group; both flips happen in the impl -commit. +list, or a set — the verdict must be 'MatchIndeterminate', because the +function application could in principle simplify into the corresponding +category. A decisive 'MatchFailed DifferentSymbols' (as 'Eval' mode +returned before this was fixed) would unsoundly skip a higher-priority +function equation. The four tests pin the @FunctionApplication{}@ +pattern paired with @Injection{} / KMap{} / KList{} / KSet{}@ subjects; +the companion case for @DomainValue{}@ is covered by an existing test +in the 'symbols' group. -} functionApplicationAgainstConcreteCategories :: TestTree functionApplicationAgainstConcreteCategories = testGroup - "FunctionApplication pattern against concrete categories (currently failing)" + "FunctionApplication pattern against concrete categories" [ let pat = app f1 [var "X" someSort] subj = Injection aSubsort someSort (dv aSubsort "x") in test diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs index e7ffa11d1f..44f861cb9e 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs @@ -215,24 +215,22 @@ varsAndValues = {- | A pattern variable that gets matched against two different subject positions — one a domain value (constructor-like), one a function -application (not constructor-like) — is currently reported as a decisive -'MatchFailed VariableConflict' in 'Implies' mode. That matches what the -matcher does for 'Eval' but diverges from 'Rewrite', which routes the same -shape through 'addIndeterminate' because the second term might simplify -into something equivalent to the first (the comment on 'bindVariable' says +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). -For 'Implies' this asymmetry causes a soundness gap: the implies handler -trusts the matcher's decisive verdict and returns a non-'indeterminate' -@valid:false@, even though kore would simplify the function application -and find the subsumption. The tests below pin both orderings of the -rebind; they are expected to fail until 'Implies' mirrors 'Rewrite' in -'Match.bindVariable'. +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 (currently failing)" + "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] From 3b3453e0b197386af392460ec43d88450b3cf2e1 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 11 Jun 2026 20:36:23 +0000 Subject: [PATCH 07/12] booster/Pattern/Match: collapse uniform FunctionApplication match1 rows into a catch-all All non-special-case rows for a FunctionApplication pattern resolve to addIndeterminate in every mode, so replace the per-subject-constructor rows (DomainValue/Injection/KMap/KList/KSet in all modes, ConsApplication and FunctionApplication outside Eval, Var outside Rewrite) with a single trailing catch-all. The mode-specific rows (AndTerm handling, Eval symbol-application descent, Rewrite subject-variable match) stay explicit above it. No behaviour change; addresses review feedback on #4152. Co-Authored-By: Claude Fable 5 --- booster/library/Booster/Pattern/Match.hs | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 9ff560229b..ee7a627ab6 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -284,17 +284,12 @@ match1 Rewrite t1@ConsApplication{} (Var t2) match1 _ t1@ConsApplication{} t2@Var{} = addIndeterminate t1 t2 match1 Eval t1@FunctionApplication{} t2@AndTerm{} = addIndeterminate t1 t2 match1 _ t1@FunctionApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@FunctionApplication{} t2@DomainValue{} = addIndeterminate t1 t2 -match1 _ t1@FunctionApplication{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@FunctionApplication{} t2@KMap{} = addIndeterminate t1 t2 -match1 _ t1@FunctionApplication{} t2@KList{} = addIndeterminate t1 t2 -match1 _ t1@FunctionApplication{} t2@KSet{} = addIndeterminate t1 t2 match1 Eval (FunctionApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 _ t1@FunctionApplication{} t2@ConsApplication{} = addIndeterminate t1 t2 match1 Eval (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 _ t1@FunctionApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 match1 Rewrite t1@FunctionApplication{} (Var t2) = subjectVariableMatch t1 t2 -match1 _ t1@FunctionApplication{} t2@Var{} = addIndeterminate t1 t2 +-- a function application pattern may evaluate to any shape, so matching it +-- against any other subject is indeterminate in every mode +match1 _ t1@FunctionApplication{} t2 = addIndeterminate t1 t2 match1 Eval t1@Var{} t2@AndTerm{} = addIndeterminate t1 t2 match1 _ t1@Var{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b match1 matchTy (Var var1) t2@DomainValue{} = matchVar matchTy var1 t2 From 4148df9c47dd410eeebffe41c0c6e20ef52db011 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 8 Jun 2026 21:10:11 +0000 Subject: [PATCH 08/12] booster/Pattern/Match, unit-tests/Pattern/MatchEval: make Injection-vs-builtin-collection match indeterminate both ways in Eval match1 was asymmetric for Injection paired with a builtin collection (KMap/KList/KSet) under Eval: the collection-pattern/Injection-subject direction returned addIndeterminate while the commuted Injection-pattern/collection-subject direction returned a decisive failWith DifferentSymbols. A spurious MatchFailed silently skips a higher-priority function equation, so the sound verdict is indeterminate in both directions. Add the Eval indeterminate carve-out to the Injection rows; Rewrite/Implies stay decisive. Co-Authored-By: Claude Opus 4.8 --- booster/library/Booster/Pattern/Match.hs | 6 +++ .../Test/Booster/Pattern/MatchEval.hs | 47 +++++++++++++++++++ 2 files changed, 53 insertions(+) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index ee7a627ab6..f6eb493f0e 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -227,8 +227,14 @@ match1 Eval t1@Injection{} t2@AndTerm{} match1 _ t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b match1 _ t1@Injection{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 match1 matchTy (Injection source1 target1 trm1) (Injection source2 target2 trm2) = matchInj matchTy source1 target1 trm1 source2 target2 trm2 +-- injection-vs-builtin-collection is indeterminate in both directions under Eval: the injected term +-- may simplify, so a decisive failure would unsoundly skip a higher-priority function equation. This +-- mirrors the commuted KMap/KList/KSet-vs-Injection Eval rows below; non-Eval modes stay decisive. +match1 Eval t1@Injection{} t2@KMap{} = addIndeterminate t1 t2 match1 _ t1@Injection{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 +match1 Eval t1@Injection{} t2@KList{} = addIndeterminate t1 t2 match1 _ t1@Injection{} t2@KList{} = failWith $ DifferentSymbols t1 t2 +match1 Eval t1@Injection{} t2@KSet{} = addIndeterminate t1 t2 match1 _ t1@Injection{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@Injection{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@Injection{} t2@FunctionApplication{} = addIndeterminate t1 t2 diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs index e0bb362fc1..ef72152f3a 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs @@ -32,6 +32,7 @@ test_match_eval = , internalSets , variableRebindMixedDeterminacy , functionApplicationAgainstConcreteCategories + , injectionAgainstBuiltinCollections ] symbols :: TestTree @@ -393,6 +394,52 @@ functionApplicationAgainstConcreteCategories = (remainder [(pat, subj)]) ] +{- | An injection paired with a builtin collection ('KMap' / 'KList' / +'KSet') must be 'MatchIndeterminate' in *both* directions under 'Eval': +the injected term may simplify, so a decisive 'MatchFailed' would +unsoundly skip a higher-priority function equation. The collection-pattern +/ injection-subject direction was already indeterminate; the commuted +injection-pattern / collection-subject direction previously returned a +decisive 'MatchFailed DifferentSymbols'. Both orderings are pinned here to +lock in the symmetry. +-} +injectionAgainstBuiltinCollections :: TestTree +injectionAgainstBuiltinCollections = + let injection = Injection aSubsort someSort (dv aSubsort "x") + in testGroup + "Injection against builtin collections (indeterminate both ways)" + [ test + "Injection pattern with KMap subject is indeterminate" + injection + emptyKMap + (remainder [(injection, emptyKMap)]) + , test + "KMap pattern with Injection subject is indeterminate" + emptyKMap + injection + (remainder [(emptyKMap, injection)]) + , test + "Injection pattern with KList subject is indeterminate" + injection + emptyList + (remainder [(injection, emptyList)]) + , test + "KList pattern with Injection subject is indeterminate" + emptyList + injection + (remainder [(emptyList, injection)]) + , test + "Injection pattern with KSet subject is indeterminate" + injection + emptySet + (remainder [(injection, emptySet)]) + , test + "KSet pattern with Injection subject is indeterminate" + emptySet + injection + (remainder [(emptySet, injection)]) + ] + ---------------------------------------- test :: String -> Term -> Term -> MatchResult -> TestTree From f7ef4d9a425fdc68521b09569cc258b574004d93 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 12 Jun 2026 00:14:42 +0000 Subject: [PATCH 09/12] booster/Pattern/Match, unit-tests/Pattern/Match{Eval,Implies,Rewrite}: defer matchVar sort mismatch when the subject can narrow A pattern variable matched against a subject whose static sort is not a subsort of the variable's sort decisively failed with DifferentSorts. That is only sound when the subject's sort is exact: a function application may evaluate to a term of a narrower sort (matchInj already defers on exactly this ground), and a subject variable may be instantiated with one. Defer as indeterminate when the subject is a FunctionApplication or Var and the two sorts share a subsort; sort-disjoint pairs and rigid subjects keep the decisive failure. New helper sortsOverlap intersects the reflexive-transitive subsort closures from the SortTable. Co-Authored-By: Claude Fable 5 --- booster/library/Booster/Pattern/Match.hs | 29 ++++++++++++++++++- .../Test/Booster/Pattern/MatchEval.hs | 14 ++++++++- .../Test/Booster/Pattern/MatchImplies.hs | 6 +++- .../Test/Booster/Pattern/MatchRewrite.hs | 6 +++- 4 files changed, 51 insertions(+), 4 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index f6eb493f0e..4281c2c852 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -473,7 +473,20 @@ matchVar if termSort == variableSort then term2 else Injection termSort variableSort term2 - else failWith $ DifferentSorts (Var var) term2 + else case term2 of + -- The subject's static sort is only an upper bound when + -- the subject can still change shape: a function + -- application may evaluate to a term of a narrower sort, + -- and a variable may be instantiated with one. If the two + -- sorts share a subsort, a match may yet be possible, so + -- defer instead of failing decisively. + FunctionApplication{} + | sortsOverlap subsorts termSort variableSort -> + addIndeterminate (Var var) term2 + Var{} + | sortsOverlap subsorts termSort variableSort -> + addIndeterminate (Var var) term2 + _ -> failWith $ DifferentSorts (Var var) term2 -- Subject variable matches are currently marked as indeterminate. -- The code may be extended to collect these as separate conditional @@ -852,6 +865,20 @@ checkSubsort subsorts sub sup argsCheck <- zipWithM (checkSubsort subsorts) subArgs supArgs pure $ and argsCheck +{- | Whether two sorts can have a common inhabitant, i.e., share a + subsort. The subsort sets in the 'SortTable' are reflexive-transitive + closures (each sort is a member of its own set), so a non-empty + intersection is exactly sort overlap. Sort variables, parametric + sorts, and sorts missing from the table cannot be decided here and + are conservatively reported as overlapping. +-} +sortsOverlap :: SortTable -> Sort -> Sort -> Bool +sortsOverlap subsorts (SortApp name1 []) (SortApp name2 []) + | Just subs1 <- Map.lookup name1 subsorts + , Just subs2 <- Map.lookup name2 subsorts = + not $ subs1 `Set.disjoint` subs2 +sortsOverlap _ _ _ = True + data SortError = FoundSortVariable VarName | FoundUnknownSort Sort diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs index ef72152f3a..d25f1d705d 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs @@ -118,8 +118,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 $ diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs index 44f861cb9e..c46e77a458 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs @@ -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 diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs b/booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs index d478861741..ce93b6b78d 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs @@ -205,7 +205,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 From 8b3ecb90e96219a1f0d86ba824e250ad6fb025fa Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 12 Jun 2026 00:17:14 +0000 Subject: [PATCH 10/12] booster/Pattern/Match, unit-tests/Pattern/MatchEval: defer matchInj when a child on the wider-sorted side can narrow The inj-vs-inj fall-through decisively failed with DifferentSorts whenever the sources differed and the special cases (subject function child, pattern variable child) did not apply. That is only sound for rigid children: a subject variable child of the wider sort may be instantiated in the pattern's source sort, and a pattern function child of the wider sort may evaluate into the subject's. Restructure the post-subsort-check dispatch as a single case over both children, deferring those two shapes and keeping the decisive failure for rigid children at incompatible sorts. Co-Authored-By: Claude Fable 5 --- booster/library/Booster/Pattern/Match.hs | 48 ++++++++++++------- .../Test/Booster/Pattern/MatchEval.hs | 43 +++++++++++++++++ 2 files changed, 73 insertions(+), 18 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 4281c2c852..9cae622817 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -363,24 +363,36 @@ matchInj -- source2 is already handled) unless (s1IsSubsort || s2IsSubsort) $ failWith (DifferentSorts trm1 trm2) - -- Functions may have a more general sort than the actual result. - -- This means we cannot simply fail the rewrite: the match is - -- indeterminate if the function result is. - case (s1IsSubsort, trm2) of - (True, FunctionApplication{}) -> - addIndeterminate trm1 trm2 - _ -> do - -- If the rule has a variable with a supersort of the - -- subject, trm2 can be bound with a suitable injection - case (s2IsSubsort, trm1) of - (True, Var v) -> - bindVariable matchType v (Injection source2 source1 trm2) - _ -> - -- truly different sorts, safe to just fail - failWith $ - DifferentSorts - (Injection source1 target1 trm1) - (Injection source2 target2 trm2) + -- A decisive failure is only sound when neither child can + -- change sort: a function application may have a more general + -- sort than the actual result, and a variable may be + -- instantiated at any subsort of its declared sort. Exactly + -- one of the subsort relations holds here (sources differ, + -- and the subsort order is antisymmetric). + case (trm1, trm2) of + (_, FunctionApplication{}) + | s1IsSubsort -> + -- the subject child may evaluate into source1 + addIndeterminate trm1 trm2 + (_, Var{}) + | s1IsSubsort -> + -- the subject child may be instantiated in source1 + addIndeterminate trm1 trm2 + (Var v, _) + | s2IsSubsort -> + -- pattern variable with a supersort of the subject: + -- bind with a suitable injection + bindVariable matchType v (Injection source2 source1 trm2) + (FunctionApplication{}, _) + | s2IsSubsort -> + -- the pattern child may evaluate into source2 + addIndeterminate trm1 trm2 + _ -> + -- both children rigid at incompatible sorts, safe to fail + failWith $ + DifferentSorts + (Injection source1 target1 trm1) + (Injection source2 target2 trm2) {-# INLINE matchInj #-} ----- Symbol Applications diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs index d25f1d705d..2c9047be42 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs @@ -33,6 +33,7 @@ test_match_eval = , variableRebindMixedDeterminacy , functionApplicationAgainstConcreteCategories , injectionAgainstBuiltinCollections + , injectionChildNarrowing ] symbols :: TestTree @@ -452,6 +453,48 @@ injectionAgainstBuiltinCollections = (remainder [(emptySet, injection)]) ] +{- | 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 + 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) + ) + ] + ---------------------------------------- test :: String -> Term -> Term -> MatchResult -> TestTree From 2d2234ac1949b3fe1d830f3d3ef1940ba85cf8f4 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 12 Jun 2026 00:21:57 +0000 Subject: [PATCH 11/12] booster/Pattern/Match: regroup match1 into per-pattern blocks with catch-alls, drop dead MatchType params Pure refactor, no behaviour change. The match1 table shrinks from ~108 rows to 46 by: hoisting the per-block \and-subject rows into two generic rows after the \and-pattern block; closing every pattern block with a catch-all (the bulk indeterminate or decisive-fail outcome) so only special rows are explicit; collapsing the Var-pattern block into a single matchVar dispatch; merging the Rewrite/Implies DomainValue-vs-Var rows; and deleting the Eval ConsApplication/FunctionApplication cross-kind descents through matchSymbolAplications, which always resolved to addIndeterminate because constructor and function symbol names never coincide. A header comment states the block order and the rigidity principle governing decisive vs indeterminate outcomes. bindVariable and matchInj no longer inspect their MatchType argument (all modes defer identically since the mixed-determinacy fix), so the dead parameters are removed. Co-Authored-By: Claude Fable 5 --- booster/library/Booster/Pattern/Match.hs | 128 ++++++++--------------- 1 file changed, 45 insertions(+), 83 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 9cae622817..0283982988 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -196,116 +196,81 @@ match1 :: Term -> StateT MatchState (Except MatchResult) () {- FOURMOLU_DISABLE -} +-- The table is grouped by the pattern (t1) constructor, in a fixed block +-- order: \and patterns/subjects first, then DomainValue, Injection, KMap, +-- KList, KSet, ConsApplication, FunctionApplication, Var. Within each block, +-- rows needing special treatment come first and a catch-all closes the block, +-- so a new Term constructor must be threaded through each block deliberately. +-- Decisive failure is only sound when both sides are rigid (cannot change +-- shape or sort under evaluation or instantiation) and distinct; anything +-- that may still change defers via addIndeterminate. match1 Implies t1 t2 | t1 == t2 = pure () +-- \and in the pattern: defer in Eval mode, decompose otherwise match1 Eval t1@AndTerm{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ (AndTerm t1a t1b) t2@AndTerm{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@DomainValue{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@Injection{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@KMap{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@KList{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@KSet{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@ConsApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@FunctionApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 match1 Eval t1@AndTerm{} t2@Var{} = addIndeterminate t1 t2 -match1 _ (AndTerm t1a t1b) t2@Var{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 Eval t1@DomainValue{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@DomainValue{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 _ (AndTerm t1a t1b) t2 = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +-- \and in the subject (the pattern is \and-free from here on) +match1 Eval t1 t2@AndTerm{} = addIndeterminate t1 t2 +match1 _ t1 (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +-- domain value patterns match1 _ (DomainValue s1 t1) (DomainValue s2 t2) = matchDV s1 t1 s2 t2 -match1 _ t1@DomainValue{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@DomainValue{} t2@FunctionApplication{} = addIndeterminate t1 t2 -- match with var on the RHS must be indeterminate when evaluating functions. see: https://github.com/runtimeverification/hs-backend-booster/issues/231 match1 Eval t1@DomainValue{} t2@Var{} = addIndeterminate t1 t2 -- match with var on RHS may lead to branching during rewriting, see https://github.com/runtimeverification/haskell-backend/issues/4100 -- Related cases are currently marked with a special function so they can be identified and changed together later (extending branching functionality) -match1 Rewrite t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2 -match1 Implies t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2 -match1 Eval t1@Injection{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@Injection{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 matchTy (Injection source1 target1 trm1) (Injection source2 target2 trm2) = matchInj matchTy source1 target1 trm1 source2 target2 trm2 +match1 _ t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2 +match1 _ t1@DomainValue{} t2 = failWith $ DifferentSymbols t1 t2 +-- injection patterns +match1 _ (Injection source1 target1 trm1) (Injection source2 target2 trm2) = matchInj source1 target1 trm1 source2 target2 trm2 -- injection-vs-builtin-collection is indeterminate in both directions under Eval: the injected term -- may simplify, so a decisive failure would unsoundly skip a higher-priority function equation. This -- mirrors the commuted KMap/KList/KSet-vs-Injection Eval rows below; non-Eval modes stay decisive. match1 Eval t1@Injection{} t2@KMap{} = addIndeterminate t1 t2 -match1 _ t1@Injection{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 match1 Eval t1@Injection{} t2@KList{} = addIndeterminate t1 t2 -match1 _ t1@Injection{} t2@KList{} = failWith $ DifferentSymbols t1 t2 match1 Eval t1@Injection{} t2@KSet{} = addIndeterminate t1 t2 -match1 _ t1@Injection{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@Injection{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@Injection{} t2@FunctionApplication{} = addIndeterminate t1 t2 match1 Rewrite t1@Injection{} (Var v2) = subjectVariableMatch t1 v2 match1 _ t1@Injection{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@KMap{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@KMap{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@KMap{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 Eval t1@KMap{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KMap{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@Injection{} t2 = failWith $ DifferentSymbols t1 t2 +-- builtin map patterns match1 _ t1@(KMap def1 patKeyVals patRest) t2@(KMap def2 subjKeyVals subjRest) = if def1 == def2 then matchMaps def1 patKeyVals patRest subjKeyVals subjRest else failWith $ DifferentSorts t1 t2 -match1 _ t1@KMap{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KMap{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KMap{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 +match1 Eval t1@KMap{} t2@Injection{} = addIndeterminate t1 t2 match1 _ t1@KMap{} t2@FunctionApplication{} = addIndeterminate t1 t2 match1 Rewrite t1@KMap{} (Var v2) = subjectVariableMatch t1 v2 match1 _ t1@KMap{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@KList{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@KList{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@KList{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 Eval t1@KList{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KList{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KList{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KMap{} t2 = failWith $ DifferentSymbols t1 t2 +-- builtin list patterns match1 _ t1@(KList def1 heads1 rest1) t2@(KList def2 heads2 rest2) = if def1 == def2 then matchLists def1 heads1 rest1 heads2 rest2 else failWith $ DifferentSorts t1 t2 -match1 _ t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 +match1 Eval t1@KList{} t2@Injection{} = addIndeterminate t1 t2 match1 _ t1@KList{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@KList{} (Var t2) = subjectVariableMatch t1 t2 +match1 Rewrite t1@KList{} (Var v2) = subjectVariableMatch t1 v2 match1 _ t1@KList{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@KSet{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@KSet{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@KSet{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 Eval t1@KSet{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KSet{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KSet{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KSet{} t2@KList{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KList{} t2 = failWith $ DifferentSymbols t1 t2 +-- builtin set patterns match1 _ t1@(KSet def1 patElements patRest) t2@(KSet def2 subjElements subjRest) = if def1 == def2 then matchSets def1 patElements patRest subjElements subjRest else failWith $ DifferentSorts t1 t2 -match1 _ t1@KSet{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 +match1 Eval t1@KSet{} t2@Injection{} = addIndeterminate t1 t2 match1 _ t1@KSet{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@KSet{} (Var t2) = subjectVariableMatch t1 t2 +match1 Rewrite t1@KSet{} (Var v2) = subjectVariableMatch t1 v2 match1 _ t1@KSet{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@ConsApplication{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@ConsApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@ConsApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@ConsApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@ConsApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@ConsApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@ConsApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KSet{} t2 = failWith $ DifferentSymbols t1 t2 +-- constructor patterns match1 matchTy (ConsApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications matchTy symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 Eval (ConsApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 +-- a function-application subject may evaluate to any shape (constructor and +-- function symbol names never coincide, so the former Eval descent through +-- matchSymbolAplications also resolved to indeterminate) match1 _ t1@ConsApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@ConsApplication{} (Var t2) = subjectVariableMatch t1 t2 +match1 Rewrite t1@ConsApplication{} (Var v2) = subjectVariableMatch t1 v2 match1 _ t1@ConsApplication{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@FunctionApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 Eval (FunctionApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 +match1 _ t1@ConsApplication{} t2 = failWith $ DifferentSymbols t1 t2 +-- function application patterns match1 Eval (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 Rewrite t1@FunctionApplication{} (Var t2) = subjectVariableMatch t1 t2 +match1 Rewrite t1@FunctionApplication{} (Var v2) = subjectVariableMatch t1 v2 -- a function application pattern may evaluate to any shape, so matching it -- against any other subject is indeterminate in every mode match1 _ t1@FunctionApplication{} t2 = addIndeterminate t1 t2 -match1 Eval t1@Var{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@Var{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 matchTy (Var var1) t2@DomainValue{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@Injection{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@KMap{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@KList{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@KSet{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@ConsApplication{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@FunctionApplication{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@Var{} = matchVar matchTy var1 t2 +-- variable patterns +match1 matchTy (Var var1) t2 = matchVar matchTy var1 t2 {- FOURMOLU_ENABLE -} matchDV :: Sort -> ByteString -> Sort -> ByteString -> StateT s (Except MatchResult) () @@ -323,7 +288,6 @@ matchDV s1 t1 s2 t2 = -- the contained pattern term is just a variable, otherwise they need -- to be identical. matchInj :: - MatchType -> Sort -> Sort -> Term -> @@ -332,7 +296,6 @@ matchInj :: Term -> StateT MatchState (Except MatchResult) () matchInj - _matchType source1 target1 trm1 @@ -344,7 +307,6 @@ matchInj | source1 == source2 = do enqueueRegularProblem trm1 trm2 matchInj - matchType source1 target1 trm1 @@ -382,7 +344,7 @@ matchInj | s2IsSubsort -> -- pattern variable with a supersort of the subject: -- bind with a suitable injection - bindVariable matchType v (Injection source2 source1 trm2) + bindVariable v (Injection source2 source1 trm2) (FunctionApplication{}, _) | s2IsSubsort -> -- the pattern child may evaluate into source2 @@ -470,7 +432,7 @@ matchVar failWith $ VariableConflict var1 (Var var1) (Var var2) matchVar -- term1 variable (target): introduce a new binding - matchType + _matchType var@Variable{variableSort} term2 = do @@ -481,7 +443,7 @@ matchVar checkSubsort subsorts termSort variableSort if isSubsort then - bindVariable matchType var $ + bindVariable var $ if termSort == variableSort then term2 else Injection termSort variableSort term2 @@ -822,8 +784,8 @@ enqueueRegularProblems ts = binding to a term is added. This avoids repeated traversals while guarding against substitution loops. -} -bindVariable :: MatchType -> Variable -> Term -> StateT MatchState (Except MatchResult) () -bindVariable matchType var term@(Term termAttrs _) = do +bindVariable :: Variable -> Term -> StateT MatchState (Except MatchResult) () +bindVariable var term@(Term termAttrs _) = do State{mSubstitution = currentSubst} <- get case Map.lookup var currentSubst of Just oldTerm@(Term oldTermAttrs _) From d790b71ab57c68584e916e7b4813180fd8280b1c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 12 Jun 2026 03:11:30 +0000 Subject: [PATCH 12/12] booster/Pattern/Match: invert match1 to defer-by-default with a single generic addIndeterminate fall-through MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pure refactor, no behaviour change. Instead of per-pattern blocks each closed by their own catch-all, the table now ends in one generic rule resolving every unhandled pair to addIndeterminate — the always-sound outcome — and every row above it must justify something stronger: \and decomposition, variable binding via matchVar, same-category descent, or decisive failure. The decisive cross-category rule is a single guarded row over a new isRigidCategory predicate (domain values, injections, collections, constructor applications), making the rigidity principle executable rather than commentary. Explicit addIndeterminate rows remain only where they must shadow a more generic stronger row: the Eval \and quirks and the Eval injection-vs-collection carve-out (now two isCollection-guarded rows covering both directions). The subjectVariableMatch marker now uniformly covers all non-Eval rigid-or-function patterns against a variable subject (outcome unchanged: addIndeterminate). 46 rows become 18. Co-Authored-By: Claude Fable 5 --- booster/library/Booster/Pattern/Match.hs | 118 +++++++++++------------ 1 file changed, 54 insertions(+), 64 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 0283982988..7b66861394 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -196,83 +196,73 @@ match1 :: Term -> StateT MatchState (Except MatchResult) () {- FOURMOLU_DISABLE -} --- The table is grouped by the pattern (t1) constructor, in a fixed block --- order: \and patterns/subjects first, then DomainValue, Injection, KMap, --- KList, KSet, ConsApplication, FunctionApplication, Var. Within each block, --- rows needing special treatment come first and a catch-all closes the block, --- so a new Term constructor must be threaded through each block deliberately. --- Decisive failure is only sound when both sides are rigid (cannot change --- shape or sort under evaluation or instantiation) and distinct; anything --- that may still change defers via addIndeterminate. +-- The matcher defers by default: the final generic rule resolves every pair +-- not handled earlier to addIndeterminate, which is always sound (the caller +-- decides what to do with an indeterminate verdict). Every row above it must +-- justify a stronger outcome: decomposition (\and, same-category descent), +-- variable binding, or decisive failure. Decisive failure is only sound for +-- two terms whose top-level categories are rigid (cannot change under +-- evaluation or instantiation, see isRigidCategory) and distinct. The few +-- explicit addIndeterminate rows below exist only to shadow a more generic +-- stronger row that would otherwise capture their cells. match1 Implies t1 t2 | t1 == t2 = pure () --- \and in the pattern: defer in Eval mode, decompose otherwise -match1 Eval t1@AndTerm{} t2@AndTerm{} = addIndeterminate t1 t2 +-- \and: Eval mode defers on a subject \and and on a pattern \and facing a +-- variable (shadowing the decomposition rules below); all other \and cells +-- decompose, pattern side first +match1 Eval t1 t2@AndTerm{} = addIndeterminate t1 t2 match1 Eval t1@AndTerm{} t2@Var{} = addIndeterminate t1 t2 match1 _ (AndTerm t1a t1b) t2 = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 --- \and in the subject (the pattern is \and-free from here on) -match1 Eval t1 t2@AndTerm{} = addIndeterminate t1 t2 match1 _ t1 (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b --- domain value patterns -match1 _ (DomainValue s1 t1) (DomainValue s2 t2) = matchDV s1 t1 s2 t2 -match1 _ t1@DomainValue{} t2@FunctionApplication{} = addIndeterminate t1 t2 --- match with var on the RHS must be indeterminate when evaluating functions. see: https://github.com/runtimeverification/hs-backend-booster/issues/231 -match1 Eval t1@DomainValue{} t2@Var{} = addIndeterminate t1 t2 +-- variable patterns: bind (or defer/fail on sort grounds, inside matchVar) +match1 matchTy (Var var1) t2 = matchVar matchTy var1 t2 +-- variable subjects: indeterminate. see https://github.com/runtimeverification/hs-backend-booster/issues/231 (Eval) +match1 Eval t1 t2@Var{} = addIndeterminate t1 t2 -- match with var on RHS may lead to branching during rewriting, see https://github.com/runtimeverification/haskell-backend/issues/4100 --- Related cases are currently marked with a special function so they can be identified and changed together later (extending branching functionality) -match1 _ t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2 -match1 _ t1@DomainValue{} t2 = failWith $ DifferentSymbols t1 t2 --- injection patterns +-- Related cases are marked with a special function so they can be identified and changed together later (extending branching functionality) +match1 _ t1 (Var v2) = subjectVariableMatch t1 v2 +-- same-category pairs descend into their contents +match1 _ (DomainValue s1 t1) (DomainValue s2 t2) = matchDV s1 t1 s2 t2 match1 _ (Injection source1 target1 trm1) (Injection source2 target2 trm2) = matchInj source1 target1 trm1 source2 target2 trm2 --- injection-vs-builtin-collection is indeterminate in both directions under Eval: the injected term --- may simplify, so a decisive failure would unsoundly skip a higher-priority function equation. This --- mirrors the commuted KMap/KList/KSet-vs-Injection Eval rows below; non-Eval modes stay decisive. -match1 Eval t1@Injection{} t2@KMap{} = addIndeterminate t1 t2 -match1 Eval t1@Injection{} t2@KList{} = addIndeterminate t1 t2 -match1 Eval t1@Injection{} t2@KSet{} = addIndeterminate t1 t2 -match1 _ t1@Injection{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@Injection{} (Var v2) = subjectVariableMatch t1 v2 -match1 _ t1@Injection{} t2@Var{} = addIndeterminate t1 t2 -match1 _ t1@Injection{} t2 = failWith $ DifferentSymbols t1 t2 --- builtin map patterns match1 _ t1@(KMap def1 patKeyVals patRest) t2@(KMap def2 subjKeyVals subjRest) = if def1 == def2 then matchMaps def1 patKeyVals patRest subjKeyVals subjRest else failWith $ DifferentSorts t1 t2 -match1 Eval t1@KMap{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KMap{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@KMap{} (Var v2) = subjectVariableMatch t1 v2 -match1 _ t1@KMap{} t2@Var{} = addIndeterminate t1 t2 -match1 _ t1@KMap{} t2 = failWith $ DifferentSymbols t1 t2 --- builtin list patterns match1 _ t1@(KList def1 heads1 rest1) t2@(KList def2 heads2 rest2) = if def1 == def2 then matchLists def1 heads1 rest1 heads2 rest2 else failWith $ DifferentSorts t1 t2 -match1 Eval t1@KList{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KList{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@KList{} (Var v2) = subjectVariableMatch t1 v2 -match1 _ t1@KList{} t2@Var{} = addIndeterminate t1 t2 -match1 _ t1@KList{} t2 = failWith $ DifferentSymbols t1 t2 --- builtin set patterns match1 _ t1@(KSet def1 patElements patRest) t2@(KSet def2 subjElements subjRest) = if def1 == def2 then matchSets def1 patElements patRest subjElements subjRest else failWith $ DifferentSorts t1 t2 -match1 Eval t1@KSet{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KSet{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@KSet{} (Var v2) = subjectVariableMatch t1 v2 -match1 _ t1@KSet{} t2@Var{} = addIndeterminate t1 t2 -match1 _ t1@KSet{} t2 = failWith $ DifferentSymbols t1 t2 --- constructor patterns match1 matchTy (ConsApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications matchTy symbol1 sorts1 args1 symbol2 sorts2 args2 --- a function-application subject may evaluate to any shape (constructor and --- function symbol names never coincide, so the former Eval descent through --- matchSymbolAplications also resolved to indeterminate) -match1 _ t1@ConsApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@ConsApplication{} (Var v2) = subjectVariableMatch t1 v2 -match1 _ t1@ConsApplication{} t2@Var{} = addIndeterminate t1 t2 -match1 _ t1@ConsApplication{} t2 = failWith $ DifferentSymbols t1 t2 --- function application patterns match1 Eval (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 Rewrite t1@FunctionApplication{} (Var v2) = subjectVariableMatch t1 v2 --- a function application pattern may evaluate to any shape, so matching it --- against any other subject is indeterminate in every mode -match1 _ t1@FunctionApplication{} t2 = addIndeterminate t1 t2 --- variable patterns -match1 matchTy (Var var1) t2 = matchVar matchTy var1 t2 +-- injection-vs-builtin-collection is indeterminate in both directions under +-- Eval (the injected term may simplify, and equation LHS sorts may be +-- misaligned with the subject); these rows shadow the decisive rule below +match1 Eval t1@Injection{} t2 | isCollection t2 = addIndeterminate t1 t2 +match1 Eval t1 t2@Injection{} | isCollection t1 = addIndeterminate t1 t2 +-- the remaining rigid pairs are cross-category and can never become equal +match1 _ t1 t2 | isRigidCategory t1, isRigidCategory t2 = failWith $ DifferentSymbols t1 t2 +-- everything else (a function application somewhere, or a future Term +-- constructor): cannot be decided here, defer +match1 _ t1 t2 = addIndeterminate t1 t2 {- FOURMOLU_ENABLE -} +{- | Whether the term's top-level category is rigid: it cannot change under + evaluation or instantiation. Domain values, injections, internalised + collections, and constructor applications are rigid: two such terms of + different categories can never become equal, so a decisive mismatch is + sound. Function applications, variables, and \and terms are not rigid. +-} +isRigidCategory :: Term -> Bool +isRigidCategory = \case + DomainValue{} -> True + Injection{} -> True + KMap{} -> True + KList{} -> True + KSet{} -> True + ConsApplication{} -> True + _ -> False + +isCollection :: Term -> Bool +isCollection = \case + KMap{} -> True + KList{} -> True + KSet{} -> True + _ -> False + matchDV :: Sort -> ByteString -> Sort -> ByteString -> StateT s (Except MatchResult) () matchDV s1 t1 s2 t2 = do