Prune indeterminate-match rules using the matcher's partial substitution

[ehildenb]

When applyRule hits a MatchIndeterminate result, it currently aborts immediately with RuleApplicationUnclear and hands off to Kore — even when the rule's requires clause is already unsatisfiable under the bindings the matcher did resolve. The matcher accumulates a partial substitution while processing pairs, so any successful extension of the indeterminate match must extend that substitution; if a requires clause already evaluates to FalseBool under it, no extension can rescue the rule and it can be pruned in favour of the next-priority alternative.

This PR exposes that partial substitution on the MatchIndeterminate result and uses it in applyRule to invoke checkRequires before the existing abort. On returnNotApplied from checkConstraint's onBottom, the rule is pruned; on smtUnclear or successful clauses, control falls through to the unchanged RuleApplicationUnclear abort (the match itself is still indeterminate, so we cannot apply the rule). The standard LLVM-discharge / equation-evaluator / SMT-discharge chain is reused via checkRequires directly.

The motivating case is the KEVM #addr [OP:OpCode], where the earlier rules in the priority chain have requires that are falsified by the partial sub but booster was bailing to Kore instead. See here for the rules, basically whenever the workstack was symbolic, the booster would fail on every opcode because it could not tell if there were sufficient items to fire the rule. But it does partially match the <k> cell, which frequently (usually) produces an opcode that fails the #isAddr1Op and #isAddr2Op side-conditions, so it can definitely throw out the rule and fall-through to the owise case.

Changes:

• Pattern/Match: MatchIndeterminate carries the partial Substitution alongside the remainder pairs; checkIndeterminate threads it through.
• Pattern/Rewrite: applyRule's MatchIndeterminate branch invokes checkRequires with the partial sub; on returnNotApplied, prunes the rule and continues with the next-priority alternative.
• Pattern/ApplyEquations, Pattern/Implies: pattern-match the new field as _partialSubst — no behavioural change in the equation evaluator or implies handler.
• Unit tests:
  • MatchRewrite: new "structured/var pattern with mixed-determinacy subject" case that mirrors the #addr [OP] shape and asserts the partial sub the matcher always produced but the API was previously discarding.
  • Pattern/Rewrite + Fixture.conBoolPair: rewrite tests covering prune-on-FalseBool (catch-all fires), prune-not-fired-on-TrueBool (still aborts — match is still indeterminate), and a deferred free-SortBool-variable SMT case noted for the rpc-integration suite.
  • Existing matcher test "Matching the same variable in a constructor (indeterminate)" updated to assert the partial sub it always produced.
• RPC-integration test test-escalate-partial-match (booster-dev only): minimal K module pinning the end-to-end behaviour — pre-fix booster aborts at depth=0 with two Uncertain about unification of rule log entries; post-fix booster prunes the higher-priority rule and fires the catch-all in a single step.

Validation:

• All 721 booster unit tests pass.
• Confirmed that test-escalate-partial-match fails at the test-only commit (first in the chain) and passes at the tip.
• Run this against KEVM and confirmed:
  • No meaningful change in performance.
  • No more tests enabled in booster-dev mode (mostly blocked by implication checking).
  • The cases of execute fallbacks that this was designed to address, it does address.

[jberthold]

Nice one! 👍