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

[ehildenb]

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.

[jberthold]

This code has gone through several reorganisations and was organised very verbosely in pattern shape - subject shape order to make it easy to find the cases that need attention.
I recommend keeping it organised in the previous way, and adding footnotes to explain rationales for all cases where no helper function wraps the logic.
Will try to review the changes but it is tricky to keep the overview of all cases in the proposed form.

[ehildenb]

I'd like to keep the inverted, defer-by-default form. The exhaustive "see every case at a glance" overview that the old pattern-shape × subject-shape layout provided now lives in the MatchDispatch test, which pins the S/F/I outcome of all 3×9×9 cells — any match1 change shows up there as a grid-cell diff, which is a more reliable map than 100+ hand-maintained rows.

More importantly, the eventual goal is for match1 to have no distinctions or branching on the first argument (Eval/Implies/Rewrite) at all, other than pure performance optimizations: the matcher should just report the truth (definite non-match vs. cannot-decide) and leave it to the caller to decide what an indeterminate verdict means in its mode. The defer-by-default structure is a step toward that — the mode-specific rows that remain are exactly the ones still to be eliminated, and keeping them as explicit shadows of the generic rule makes them easy to spot and remove. The verbose per-mode layout would entrench the per-mode distinctions we're trying to delete.

[jberthold]

(minor) Maybe this could be defined in Booster.Pattern.Util?
Reminded me of the indexing: all non-rigid terms get an index of Anything

[ehildenb]

Left it in Match.hs for now — it's only used by the matcher, and Util doesn't yet have a peer predicate to group it with. You're right it's conceptually the indexing rule (Index.hs:45, variables/functions → Anything); if a second caller appears I'll lift it to Util (or unify with the index computation) then.

[jberthold]

Subtlety: And terms are never expected as trm2 (or trm1) in this code, therefore safe to use the _ -> catch-all case?
This is currently true but only because of the arrangement (ordering) of the matches in the caller (match1). Maybe better to use isRigidCategory here. Which will also make it so that the default is indeterminate, in the spirit of the new comment above match1.

[ehildenb]

Done: 1910818 — the final failure is now guarded by isRigidCategory trm1, isRigidCategory trm2, with a non-rigid child deferring to addIndeterminate. Soundness no longer depends on match1 never routing an \and (or subject variable) here. No tests changed: the precise Var/FunctionApplication deferrals are still handled by the explicit cases above the catch-all.

[ehildenb]

I tried this and reverted it. Gating the catch-all on isRigidCategory (deferring when either child is non-rigid) regressed rpc-integration test-3934-smt: a KEVM execution that branched at depth 33 instead aborted at depth 31, because an injection child that cannot actually match now defers and aborts the rewrite.

The decisive failure should be sound, or at least preserves existing behavior: the narrowable directions (a function/variable child that can narrow into the other side) are already deferred by the explicit cases above the catch-all, so the catch-all only sees children that are rigid, or non-rigid at a sort that can't bridge — normalising the narrower injection wraps the child in an inj{narrow -> wide}(...), which the rigid wider-sorted pattern child can never equal regardless of how it resolves. And an \and child never reaches matchInj (match1 decomposes a subject \and first). I kept the decisive failure, documented that invariant in the catch-all comment (e7d4b2b), and added a regression test pinning it (464b0f8) — verified it fails under the isRigidCategory variant and passes with the decisive failure kept.

[jberthold]

Certainly safer to addIndeterminate here, but I don't understand the comment about "higher-priority equations". Was this a problem in the Eval mode? (maybe just rephrase the comment or provide an issue link?)

[ehildenb]

Done: 1910818 — rephrased and linked #231, and fixed the priority wording: priorities count up from 1, so the hazard is evaluation falling through to a lower-priority equation (a higher priority number) that should not have been reached. To answer your question directly: yes, this is the Eval/function-evaluation concern — handleFunctionEquation routes FailedMatch → continue (try next priority) but IndeterminateMatch → abort, so a spurious decisive failure here would skip the abort and reach a lower-priority equation.

[ehildenb]

The issue I was having was running the Pyk prover in proxy mode, where it basically would run the haskell backend in booster-only mode, then fallback on its own to calling Kore directly. We were getting some cases where the booster was reporting "nothing else can apply, for sure" (definite match failed), where actually it should be indeterminate. We were trying to use the definite failure as a reason to skip invoking Kore, but then some proofs that were passing before are now failing (get stuck). So we need to always default to indeterminate, and only go to definite succes/failure on cases where it actually is definite. That was for the implies endpoint.

For the equation application, if we get a definite failure, then we are free t otry lower priority (higher priority number) rules. Those rules should not be tried on indeterminate (for equations). So this actually would be a soundness bug in some cases. In reality, I doubt this case was exercised in practice.

[jberthold]

Again maybe good to use isRigidCategory for the failWith case (and variableSort <= termSort instead of the overlap), although no And terms are expected here..

[ehildenb]

Done: 3f74ec6, but only partially, on purpose. I adopted the spirit (documented why the catch-all is sound) but kept sortsOverlap rather than switching to isRigidCategory + variableSort <= termSort.

The reason: here the _ branch is reached only for a rigid subject (exact sort) or a function/variable subject whose sort is disjoint from the variable's — sortsOverlap already deferred the overlapping case just above. A disjoint function/variable genuinely cannot match (its result/instantiation is a subsort of a sort sharing nothing with the variable's), so failing decisively is sound and precise. Gating on isRigidCategory would defer those disjoint cases too, trading real precision for robustness against an \and that match1 never routes here (it decomposes a subject \and before dispatching a variable pattern). I added a comment stating that invariant instead.