[CatarinaGamboa]

Closes #480.

Problem

The message's Found listed every path condition of the method, so a guard on another variable read as the reason for the error, and nothing was said about the variable Expected constrains.

Change

The message keeps only the facts of Found linked to the terms of Expected: the same factsOf/linkedTerms the counterexample already uses, exposed as one package-private RefinementError.linkedToExpected that StateRefinementError reuses.

• When facts remain, the frames are unchanged: X is not a subtype of Y and found X but expected Y. When every fact is linked, Found is shown as written (e.g. !(x < 0 || x > 5), not split).
• When none remains (for a state error: none applies a ghost or state; an alias such as box == getBox says nothing about the state), the message reads expected <refinement> but could not prove it.

Only the message text changes. The counterexample, hints, the Found the IDE shows and the verification query are unchanged. TestGeneratedNames now reads the whole Found of refinement errors, since the message no longer lists unrelated generated names.

Before / after

Reproducer 1 (refinement):

before: Refinement Error: !(port < 0 || port > 65535) is not a subtype of timeout >= 0
after:  Refinement Error: expected timeout >= 0 but could not prove it
        Counterexample: timeout == -1 (unchanged)

Reproducer 2 (state):

before: State Refinement Error: found !(#isEmpty_result¹⁶ || #isEmpty_result¹⁷) && box¹⁵ == getBox¹³ but expected full(box¹⁵)
after:  State Refinement Error: expected full(box¹⁵) but could not prove it

Study exercise (JabRef EditCommand, fixture state_hint_study_undo_manager_error):

after:  expected redoable(undoManager) but could not prove it

Facts that relate to Expected stay in the usual frame:

• !(port < 0 || retries > t) with Expected t >= 0 shows !(retries > t) is not a subtype of t >= 0;
• a state reaching Expected through an alias: found empty(b1) && box == b1 but expected full(box).

Tests

Each fails without the fix:

• RefinementErrorCounterexampleTest: refinement reproducer, partial guard, Found kept as written when every fact is linked, state kept through an alias.
• TestStateHints: the study's undo manager (state reproducer).

Full suite passes locally (697 tests). Size: +99 / −18 over 5 files.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

• [P2] Format unconstrained variable names together — FoundFacts.java:52-53
  When the expected refinement contains two qualified variables with the same simple name and neither is constrained by the found facts, formatting each Var separately loses the ambiguity context. Both names can appear as x, producing a misleading message such as x, x (no constraint). Format the variables in one expression so the name resolver can retain the necessary qualifiers.

[CatarinaGamboa]

Round 1 response:

• Fixed: format unconstrained variable names together. New ExpressionFormatter.formatVariables names each variable with the resolver of the whole expected refinement, so qualifiers stay when simple names collide and the names match how Expected is written; one test in ExpressionFormatterTest.
• Declined: none.

[CatarinaGamboa]

Codex review, round 2

• [P2] Distinguish ghost values from their receiver variables — FoundFacts.java:38-40
  When the expected refinement is size(x) > 0 and found only establishes x != null, this term match retains x != null as a relevant constraint. The resulting message omits the “no constraint” wording and hint even though nothing constrains size(x). Treat variables used only as ghost arguments separately from values the expected refinement constrains.

• [P2] Require state information relevant to the expected application — StateRefinementError.java:59-61
  If found establishes size(x) == 0 but the method requires open(x), any function invocation makes isKnown return true. The error then presents the size fact as known state information and suppresses the unknown-state hint, although it says nothing about open(x). Check whether the found application constrains the state required by the expected refinement.

[CatarinaGamboa]

Round 2 response:

• Declined: ghost arguments vs values. x != null is a fact about a variable of Expected, so showing it is accurate; the linking is the same one the counterexample already uses, and the "(no constraint)" wording is reserved for when Found says nothing at all about Expected's variables. Splitting ghost arguments from values would make the message and the counterexample disagree.
• Declined: require the same ghost application. Requiring the found application to match the expected one would hide the most useful case, found closed(x) but expected opened(x) (another state of the same set). Any ghost application over the object is information about it; on main the general hint was likewise suppressed whenever Found was not true, so this is no regression.

Nothing relevant left, so the review loop stops here.

[CatarinaGamboa]

Codex review, round 3

• [P2] Limit unknown-state descriptions to state receivers — StateRefinementError.java:51-52
  When a state precondition includes an ordinary guard, such as closed(this) && attempts > 0, and the found facts contain no state application, describeVariables labels every expected variable as being “in an unknown state.” The resulting message says that the integer attempts has an unknown state. Select the receivers of the expected state applications for this wording, rather than all variables in the predicate.

[CatarinaGamboa]

Round 3 response:

• Fixed: limit unknown-state descriptions to state receivers. FoundFacts.describeStateReceivers names only the arguments of Expected's ghost/state applications (all variables if it has none), so closed(box) && attempts > 0 reads found box in an unknown state; one test in RefinementErrorCounterexampleTest.
• Declined: none.

[CatarinaGamboa]

Codex review, round 4

• [P2] Check state information for the expected object — StateRefinementError.java:63-64
  When the expected refinement combines a receiver state with a ghost predicate on another value—for example, full(box) && capacity(other) > 3—and found contains only capacity(other) > 3, this check treats the state as known because some ghost application appears in shown. The error then reports the guard as the found state and omits the “No state information is known” hint, even though nothing is known about box. Check whether the shown application concerns the object whose state is required.

[CatarinaGamboa]

Round 4 response:

• Declined: check state information for the expected object. other is itself an object Expected applies a ghost to, so found capacity(other) > 3 but expected full(box) && capacity(other) > 3 shows a true state fact about Expected's objects, which is the agreed rule for keeping the found X but expected Y frame. The specific state hints (NEEDED_STATE etc.) are computed separately and still name box; the general hint was already suppressed on main whenever Found was not true.

Nothing relevant left.

[CatarinaGamboa]

Codex review, round 5

• [P2] Distinguish state predicates from other ghost calls — StateRefinementError.java:55-57
  When a state check expects full(box) but Found contains only a linked value ghost such as size(box) > 0, appliesGhost returns true and the message says found size(box) > 0 but expected full(box). A FunctionInvocation can represent a value ghost, not a state, so this bypasses the intended “could not prove it” message despite no known state for box. Check whether the linked fact supplies state information rather than treating every ghost call as one.

[CatarinaGamboa]

Round 5 response:

• Declined: distinguish state predicates from value ghosts. A ghost value of the object is part of what its typestate refines (states may be defined over ghosts, e.g. from = "size(this) > 0"), so found size(box) > 0 but expected full(box) shows a true, relevant fact about box. Telling the two apart would need the context's state sets in the error, for a case no test or study exercise reaches (same point as round 2).

Nothing relevant left.

[CatarinaGamboa]

Codex review, round 6

I found no actionable regressions in the diff. The targeted tests pass.

[CatarinaGamboa]

Round 6 response: no findings, nothing to fix or decline. Review loop done.