GeezerVison

Refs #375.

Follow-up to #476 and #485, approved by the PM. The simplified Found (the last step the VS Code panel shows) no longer lists path conditions that Expected does not depend on.

Problem

#485 trims the message to the facts linked to Expected. The panel's last step still listed every if/loop guard, so the message and the panel disagreed. In the study exercises:

• A1_56: the message is expected redoable(undoManager) but could not prove it, but the panel still shows two switch guards.
• A1_01: the panel shows baseline || extended, which says nothing about wParam.

Rule

A binder of a generated boolean (a path condition such as #if_condition) is dropped when both hold:

• Not linked to Expected: neither its variable nor any term of its refinement shares a term with Expected, directly or through other facts of Found.
• Not mentioned by another row, so no remaining row refers to a variable whose binder was dropped.

Rows that are not generated booleans are never dropped by this rule; the message still trims those (#485), so the message is always a subset of the panel's last step. Without expected terms (NeededVariables.NONE), nothing is dropped.

Each removal is a step of the existing Binder pass. Stepping back in the panel still shows the original facts: the root of the VCSimplificationResult origin chain keeps every dropped guard. I checked this for the A1_56 shape (each guard is its own Binder step and the root has both), and TestGeneratedNames now reads the original Found, so it checks it on every run.

One source for the linking. factsOf, linkedTerms, termsOf, termName and linkedToExpected moved from RefinementError to VCSimplificationUtils, so simplification no longer needs anything from diagnostics. RefinementError (message and counterexample), StateRefinementError (message) and NeededVariables (panel) now all use them. VCSimplificationUtils had its own termsOf that named applications by toString(). Now applications over variables are named as in the SMT model (size(x)), which the counterexample needs, and the other applications are named as written (f(1)). All tests pass with that change.

The "could not prove it" frame, the shortcut that keeps Found as written when every fact is linked, and the counterexample are unchanged.

Before / after (the panel's last step)

The rows below are the simplified chain exactly as VCImplication.toString() prints it, from origin/main and this branch.

A1_56 (JabRef EditAction, line 69). The message is unchanged on both: expected redoable(undoManager¹⁴¹) but could not prove it.

before: ∀##if_condition_122:boolean, !##operation_result_121  =>
        ∀##if_condition_136:boolean, !##operation_result_134 || ##operation_result_135  =>
        ∀#undoManager_141:CountingUndoManager, #undoManager_141 == ##getUndoManager_result_139
after:  ∀#undoManager_141:CountingUndoManager, #undoManager_141 == ##getUndoManager_result_139

A1_01 (dcm4che SlideRecoder, line 131). The message is unchanged: found startTiling(wParam²⁹⁷) && startCompression(wParam²⁹⁷) but expected compressionExplicit(wParam²⁹⁷).

before: ∀##if_condition_302:boolean, #baseline_298 || #extended_299  =>
        ∀#wParam_297:ImageWriteParam, startTiling(#wParam_297) && startCompression(#wParam_297)
after:  ∀#wParam_297:ImageWriteParam, startTiling(#wParam_297) && startCompression(#wParam_297)

A guard Expected depends on stays (ErrorCounterexampleLinkedPathCondition). The message is unchanged: !(port < 0) && timeout¹⁰ == port - 1 is not a subtype of timeout¹⁰ >= 0.

before: ∀##if_condition_0:boolean, !retries > 3  =>
        ∀##if_condition_4:boolean, !port < 0  =>
        ∀#timeout_10:int,    #timeout_10 == port - 1
after:  ∀##if_condition_4:boolean, !port < 0  =>
        ∀#timeout_10:int,    #timeout_10 == port - 1

retries > 3 is dropped. port < 0 is linked through timeout == port - 1 and stays.

In all three cases the original step still shows every guard.

No screenshots: the liquidjava-dev harness has no panel-capture script yet, and the extension server would need this verifier built into it, so I skipped them.

Tests

VCBinderSimplificationTest has 4 new tests. Each fails without the change.

• removesPathConditionsExpectedDoesNotDependOn: the A1_56 shape, including a negated disjunction.
• keepsPathConditionExpectedDependsOnThroughAnotherRow: a guard linked through y == x - 10 stays while an unlinked one goes.
• keepsPathConditionAnotherRowMentions: a guard whose variable a ternary row uses stays.
• keepsPathConditionsExpectedNames: a guard whose own variable Expected names stays, and so does a guard on a call Expected names (f(1), Codex round 1).

Changed: TestGeneratedNames now reads the original Found instead of the simplified one, because the simplified one no longer has the guards whose names it checks. Only line 54 changes: it is now isNull == #operation_result && #if_condition == isNull && #if_condition && x == 0, the alias as written before simplification.

mvn test: 702 tests, 0 failures.

Size: +192 / −108 over 7 files. About 90 of the removed lines are the helpers that moved out of RefinementError.

🤖 Generated with Claude Code