[CatarinaGamboa]

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

[CatarinaGamboa]

Codex review, round 1

(Codex v0.164.0, codex exec review, on commit dff0e86. Its shell sandbox cannot start on this machine, so it was given the PR description, the diff against origin/main and the full changed and related files on stdin.)

The new removal rule can hide a generated boolean binder that Expected references directly. The added tests do not cover that case.

• [P2] Keep generated boolean binders named in Expected — liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java:85-88
  When Expected directly mentions a generated boolean binder but its refinement does not repeat that name—for example, ∀##if_condition_1:boolean. p with Expected ##if_condition_1—this test marks the binder unlinked and removes its row, potentially leaving Found as true. Check expectedTerms.contains(row.getName()) before marking the binder removable, and add a test for this case.

[CatarinaGamboa]

Round 1, my response:

• [P2] Keep generated boolean binders named in Expected: fixed in 0a207e9. I reproduced it first with the new unit test keepsPathConditionExpectedNames (Expected ##if_condition_1, rows ∀##if_condition_1 p and ∀##if_condition_2 q). Before the fix it gave q; now it gives p. NeededVariables.isLinked now counts a binder as linked when its own variable is in the linked terms, not only when a term of its refinement is. Full suite: 695 tests, 0 failures.

[CatarinaGamboa]

Codex review, round 2

(On commit 0a207e9, same setup as round 1.)

The new removal rule preserves guards linked to Expected or referenced by another row, and the counterexample logic retains its existing term function. I found no concrete correctness bug in the supplied diff.

No findings, so there is nothing to fix or decline, and the review loop ends here.

[CatarinaGamboa]

Codex review, round 1

(Codex v0.164.0, codex exec review --base origin/main, on commit 39c531f, the rebase onto #485/#486.)

The new binder-removal logic can discard a path condition that directly constrains a ghost call in the expected refinement, producing an incomplete error derivation.

• [P2] Preserve constant-argument calls when linking path conditions — liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java:84-87
  When an expected refinement contains both a variable constraint and a ghost call with a literal argument, such as f(1) > 1 && x > 0, termsOf now omits f(1) because termName accepts only variable arguments. A generated Boolean binder containing f(1) > 0 is therefore classified as unlinked and removed, even though it states a fact about the expected refinement. Keep such calls in the dependency analysis before removing their binders.

[CatarinaGamboa]

Round 1, my response:

• [P2] Preserve constant-argument calls when linking path conditions: fixed in c95bb86. The bug came from merging the two termsOf copies: the one from RefinementError skipped applications whose arguments are not all variables. termsOf now keeps those as written (f(1)). Applications over variables are still named as in the SMT model, which the counterexample needs. I extended keepsPathConditionExpectedNames (now keepsPathConditionsExpectedNames) with a guard f(1) > 0 under Expected ##if_condition_1 || f(1) > 1. Without the fix the test fails because the guard is dropped; with it, the test passes. Full suite: 702 tests, 0 failures.

[CatarinaGamboa]

Codex review, round 2

(On commit c95bb86, same setup as round 1.)

I found no actionable regressions in the diff. The targeted simplification and generated-name tests passed.

Codex had no findings, so the review loop ends here.