[CatarinaGamboa]

Closes #522, part 4 of 5: counterexample for state errors. Design: #522 (comment)

State refinement errors had no counterexample. Now, when a state error is reported, one more solver call asks for a model of Found ∧ ¬Expected. It is the same VC, with the same context gathering, as the failed check. The model is shown restricted as S2 asks.

What is shown

Only the assignments to variables of the Found the headline shows. Left out:

• every ghost or state application, such as display(host) = 1: a state is an unconstrained number (S3);
• generated names (#…);
• object values (T!val!n);
• values that a Found fact x == c already states (RefinementError.isKnown, reused).

If the headline shows no Found (expected … but could not prove it), there is no counterexample. What is shown is a sub-assignment of a model of Found ∧ ¬Expected. If the solver fails, the error is reported without one.

Study tasks, before and after

A1_09:

 State Refinement Error: found newMode == BORDERLESS && (previousMode == BORDERLESS && newMode != BORDERLESS ? … : …) but expected display(host) == notDisplayable
 51 |       case BORDERLESS:
 52 |         host.setResizable(false);
 53 |         host.setUndecorated(true);
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^
 54 |         host.setExtendedState(Frame.MAXIMIZED_BOTH);
 55 |         host.setVisible(true);
+ --> Counterexample: previousMode == BORDERLESS

newMode is left out because Found states it.

• A1_38, A1_01, A1_56: no counterexample (states only, or no Found shown), as the review asked.
• A2_10, A2_04, practice, practice2: unchanged.

Each task still gives exactly one error, on its reportedLine.

Changes

• TypeChecker.throwStateRefinementError asks for the model (best effort) and passes it through VCChecker.
• StateRefinementError.showCounterexample filters the model.
• RefinementError.isKnown becomes package-private so the filter can reuse it.
• Test: TestCounterexamples, on the existing ErrorStateHintPathDependent.java, gives ready == false. It fails without the change.

Conflicts

• Independent of the From-note PRs (From note: name an unrefined parameter as the unknown value's origin #526 and the stacked ones). They also add a parameter to throwStateRefinementError, so whichever merges second needs a one-line rebase.
• May touch the same files as One headline frame: found … but expected … for refinement errors #520/Drop the general UNKNOWN hint and show every from in declared-here #521 (RefinementError) only at isKnown's modifier.

Tests: mvn test, 729 run, 0 failures.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main: "I found no actionable regressions in the diff."

Soundness prompt: a program whose model assignment is real but irrelevant.

State Refinement Error: found noise ? closed(f) : created(f) but expected open(f)
 --> Counterexample: noise == false

Both arms violate open(f), so noise says nothing about why the call fails. No ghost or state value was printed.

Fixed in "Show no state counterexample when every value fails the call". Before asking for a model, one solver check asks whether Found ⇒ ¬Expected. If it holds, no value lets the call through, and there is no counterexample.

• That program now shows none.
• ErrorStateHintPathDependent still gives ready == false.
• A1_09 still gives previousMode == BORDERLESS.
• A1_38, A1_01 and A1_56 still give none.

Tests: 729 run, 0 failures.

[CatarinaGamboa]

Clean-code review

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

Fixed:

• [core-dry] The filter reuses RefinementError.isKnown (now package-private) instead of a second "Found already states it" check.
• [core-fail-fast / separation] The solver calls live in TypeChecker.counterexample, which is best effort. A solver failure logs under -d and the error is reported without a counterexample, as receiverStates does for hints.

Declined:

• [solid-srp] StateRefinementError.showCounterexample both filters the model and formats it. Splitting it would make a one-use helper. RefinementError keeps filtering and formatting together too.
• [func-few-arguments] VCChecker.throwStateRefinementError gains a tenth parameter. Bundling them is a refactor of an existing signature, outside this small PR.

[CatarinaGamboa]

Codex review, round 2

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

Soundness prompt: no case printed a state or ghost value, named a variable missing from Found, or gave a value outside a model of Found ∧ ¬Expected. It reported one redundant value:

State Refinement Error: found #if_condition == flag && #if_condition && (flag && choice ? open(f) : created(f)) but expected open(f)
 --> Counterexample: flag == true && choice == false

Found entails flag == true through the guard (#if_condition == flag && #if_condition), but does not state it as a direct fact.

Declined. The value is real and part of a model, so the line is sound. The filter drops only values Found states as x == c, which is the same syntactic isKnown refinement-error counterexamples use. Catching entailed values would need one solver call per shown variable, and it would make the two kinds of error filter differently. Found also shows the generated #if_condition there, which is a separate display issue.

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