[CatarinaGamboa]

Closes #522, part 5 of 5: A1_09's nested if-then-else Found, folded under the shown path condition. Design: #522 (comment)

What it does

A new pass, VCPathFolding, runs once on the shown Found of a state error, after VCRelevantFacts:

1. It collects the facts x == c that the chain states. c is a literal (int, long, real, boolean, char), an Enum node, or a Java enum constant. A Java enum constant enters the VC as a variable named Type.CONST; it counts as a constant only when the unsimplified chain binds it with an enum type that declares that constant.

2. In the conditions of the chain's if-then-else facts, it writes c for x. It then folds the condition with the existing VCFolding/VCLogicalSimplification, plus A == B/A != B between two such enum constants (distinct values of a datatype).

3. A branch is dropped only when its condition folds to true or false. Otherwise the ITE stays, with its simplified condition. No SMT check is used.

4. VCChecker keeps the fold only if every fact of the unfolded shown Found that has no if-then-else is still shown. Otherwise, when a settled branch would make the headline drop the path fact that chose it (mode == A), it shows the unfolded Found.

Why it is sound: every fact of the premise chain holds wherever the others are checked. Writing c for x where x == c is a premise keeps Found equivalent, and the fact x == c itself stays. The chain the pass gets has no Expected node (joinPredicates clones it before appending Expected), so nothing is assumed from Expected.

The pass is a normal simplification step ("Path Folding"), so the panel's steps can show it.

A1_09, before and after

-State Refinement Error: found newMode == BORDERLESS && (previousMode == BORDERLESS && newMode != BORDERLESS ? display(host) == notDisplayable : (previousMode != BORDERLESS && newMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable)) but expected display(host) == notDisplayable
+State Refinement Error: found newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) but expected display(host) == notDisplayable

• This is the review's mock-up, with otherwise left to the panel rows (extension side).
• The other seven tasks are byte-identical. Each still gives exactly one error, on its reportedLine.
• Every state-error fixture of the suite gives the same headline as before.

Test

TestFoundBinders.stateFoundFoldsTheBranchesItsPathConditionRulesOut, on a new fixture shaped like A1_09: ErrorStatePathFolding.java, an enum mode with a two-arm if/else-if and a switch case. No existing fixture has a path-condition constant inside an ITE. The test fails without the change.

mvn test: 730 run, 0 failures.

Conflicts

• One hunk in VCChecker.throwStateRefinementError (where shown is computed). The From-note PRs (Origin note: say where the wrong state of a receiver comes from #528) and Show a counterexample for state errors, restricted to the shown Found #527 change the lines just after it, so whichever merges second needs a trivial rebase.
• None with Drop the guard hint when a call-sequence hint exists, and reword it #518–Drop the general UNKNOWN hint and show every from in declared-here #521.

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

I audited the diff with the clean-code-principles checklist.

Fixed, while writing it:

• [core-dry] Folding reuses VCFolding and VCLogicalSimplification, run to a fixed point on the condition, instead of a second set of folding rules. The only new rule compares two enum constants that enter the VC as variables, which neither pass can know about.
• [core-fail-fast] The enum constants come from the chain before binder simplification. My first version looked at the simplified chain, where the DisplayMode.BORDERLESS binder was already dropped, so it silently did nothing. A1_09 showed that before I pushed.
• [solid-ocp] It is a separate VCSimplificationPass. The existing passes are unchanged, and only state errors run it.

Declined:

• [func-few-arguments] foldConditions(expression, constants, enumConstants) passes the enum set down the recursion. A field would do the same (the constructor already keeps it), but constants is per chain, so both stay parameters, alike.
• [solid-srp] Constant collection, substitution and folding are in one 150-line class. Each step is one private method, and splitting them across classes would scatter a single rule.

[CatarinaGamboa]

Codex review, round 1

codex exec review: "I found no actionable bugs in the diff."

Soundness prompt. It found a real gap. Once a fold removes the last condition that mentions x, the headline's relevance filter (linkedToExpected) also drops the fact x == c that chose the branch:

Program	This PR (before the fix)	main
DroppedEnumGuard	found phase(cell) == b but expected phase(cell) == a	found mode == A && (mode == A ? phase(cell) == b : phase(cell) == a) but …
DroppedIntGuard	found phase(cell) == b …	found n == 1 && (n == 1 ? … : …) …
DroppedBooleanGuard	found phase(cell) == b …	found flag == true && (flag == true ? … : …) …
NestedEnum	found flag ? phase(cell) == b : phase(cell) == a …	found mode == A && (flag ? (mode == A ? …) : (mode == B ? …)) …

The shorter headline is still a fact the verifier knew (S1), but the path condition that explains the branch disappears. That is not "folded under the shown path condition".

Fixed in "Keep a state Found unfolded when folding would hide a fact it showed". VCChecker keeps the fold only if every fact of the unfolded shown Found that has no if-then-else is still shown after folding. Otherwise it shows the unfolded Found.

• All four programs now print main's headline.
• A1_09 and the new fixture still fold. There the path condition newMode == BORDERLESS stays shown after the fold.

Tests: 730 run, 0 failures.

[CatarinaGamboa]

Codex review, round 2

Soundness prompt. Eight new programs, built and compared with origin/main: ints, chars, longs, booleans, static final constants, switch, nested ifs, loops, an enum from another file, and an equality inside Expected. It found no incorrect Found headline and no dropped reachable branch.

• One program folds further than main, correctly: second == ONE rules out a first == ONE && second == TWO arm.
• The Expected equality is not used to fold, as intended.

codex exec review:

[P2] Preserve path facts when folding the last conditional. When a path equality settles every conditional on its variable, the folded fact no longer mentions it, linkedToExpected drops the equality, and keepsShownFacts falls back to the unfolded Found (e.g. mode == ON && (mode == ON ? … : …)).

Declined for this PR. It is the round 1 fix working as designed: when keeping a fold would hide the path fact, we show the unfolded Found, which is sound and complete. Keeping a settled path fact visible needs ErrorMessage's fact selection (linkedToExpected) to treat facts used by a fold as linked. That is shared by every error message and touched by #520. A1_09, the case this PR is for, still folds: its newMode == BORDERLESS stays shown after the fold. I'll list it as a follow-up.

This ends the Codex loop for this PR: nothing relevant is left.