[CatarinaGamboa]

Closes #520
Closes #521

What and why

1. One headline frame (One headline frame: found … but expected … for refinement errors #520). Refinement errors used X is not a subtype of Y, while state errors use found X but expected Y. Refinement errors now use found %s but expected %s too (RefinementError). An empty Found keeps expected Y but could not prove it.
2. No general UNKNOWN hint (Drop the general UNKNOWN hint and show every from in declared-here #521, part 1). "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it." is gone. Both fixes it suggests are graded wrong in the study (A2_04).
3. Every from in declared-here (Drop the general UNKNOWN hint and show every from in declared-here #521, part 2). When Expected is the disjunction of several @StateRefinement entry states, the "Refinement declared here" excerpt marks every from, and each one gets its where … means … line. Before, AuxStateHandler took a findFirst().
   • StateRefinementError now carries the list of declaration positions. LJDiagnostic.getDeclarationPositions() returns it, and getDeclarationPosition() still returns the first one, so the IDE's Locations and State Machine are unchanged.
   • Fixing this exposed a position bug: each from was found by its text in any LiquidJava annotation of the method. In A1_01, line 111's from = "compressionTypeSet(this)" was placed at line 110's to = "compressionTypeSet(this)". from/to positions now come from the annotation's own value, and the text search is only a fallback.

Soundness: no message claims anything new. The excerpt and where lines quote the spec, and the Expected they explain is already the disjunction of these same froms.

Study tasks: before (main) → after

Each task still gives exactly one error, on its reportedLine. A1_38, A1_56 and A1_09 are unchanged.

A2_10

- Refinement Error: failures.size() == size(this.failures) && failures.size() >= 0 is not a subtype of failures.size() > 0
+ Refinement Error: found failures.size() == size(this.failures) && failures.size() >= 0 but expected failures.size() > 0

practice

- Refinement Error: toPay == price - discount is not a subtype of toPay >= 0
+ Refinement Error: found toPay == price - discount but expected toPay >= 0

practice2

- Refinement Error: delay == atMinute - nowMinute is not a subtype of delay >= 0
+ Refinement Error: found delay == atMinute - nowMinute but expected delay >= 0

A2_04: the headline is unchanged (expected timeout >= 0 but could not prove it), and the hint block is gone:

- Hints:
-   - Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.

A1_01: declared-here, after:

--> Refinement declared here:
109 |      */
110 |     @StateRefinement(from = "compressionExplicit(this)", to = "compressionTypeSet(this)")
    |                              ^^^^^^^^^^^^^^^^^^^^^^^^^
111 |     @StateRefinement(from = "compressionTypeSet(this)", to = "compressionTypeSet(this)")
    |                              ^^^^^^^^^^^^^^^^^^^^^^^^
112 |     void setCompressionType(String compressionType);
  where compressionExplicit(this) means compression(this) == compressionExplicit
  where compressionTypeSet(this) means compression(this) == compressionTypeSet

Before, only line 110 was marked, and only its where line was shown.

Tests

• Updated the 6 expectations that assert is not a subtype of (TestFoundBinders, TestStaticConstantNames, RefinementErrorCounterexampleTest).
• RefinementErrorCounterexampleTest.messageWithNothingFoundGivesNoHint: an empty Found gives no hint.
• TestDeclarationPositions.stateErrorPointsToEveryEntryStateWithWhatItMeans with the new fixture ErrorStateRefinementEveryFrom.java, a named set with two froms where the second from repeats the first annotation's to. It checks both positions and both where lines.
• Each new or changed test fails on main. mvn test: 731 tests, 0 failures.

Study env: re-run after release (not edited here)

• test/verify-tasks.py → test/out/verify-new.json: the practice, practice2 and A2_10 headlines, and the A2_04 hint.
• The recorded CLI outputs of practice and practice2, and of A2_10, A2_04 and A1_01.
• Tour screenshots (test/e2e.mjs): test/out/B-01…B-07-tour-step*.png (the tour runs on the practice file, whose headline changes).
• Practice hover/repair screenshots: B-02-practice2-hover.png, B-11-practice2-hover.png, B-01/B-10-practice2-repair.png, and the block-1 practice equivalents.
• A2_10: A-run2/A-03-A2_10-hover.png, A-run2/A-04-A2_10-liquidjava-view.png (headline).
• A2_04: A-19-A2_04-hover.png, A-20-A2_04-liquidjava-view.png (hint removed).
• A1_01: the hover and panel are unchanged. The IDE gets only the first declaration position, so showing both froms in the panel needs an extension change (it can read getDeclarationPositions()).

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

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

Fixed:

• TestDeclarationPositions — [core-dry] the new test computed the offset of a from value twice, inline. It is now one fromStart(source, from) helper. The existing position assertions are reused through assertPosition, which was split out of assertPredicatePosition.
• AuxStateHandler.getStates — [core-dry] from and to positions share one valuePosition helper: the annotation's own value first, the text search as fallback.

Declined:

• LJDiagnostic.getSnippet — [func-small] the marker block is now one loop deeper. It could move into its own method, but that method would take eight parameters (func-few-arguments), and the PR should stay small. The loop keeps the code as it was, just repeated for each position.
• StateRefinementError — [solid-isp] declaration positions and notes stay as two parallel lists, not one Declaration record. A record would change more signatures (VCChecker, TypeChecker) that other open work touches. The notes are not one per position anyway: a from that writes no named-set state has no where line.
• TypeChecker.throwStateRefinementError short overload — [core-fail-fast] it wraps its single position in List.of. Its only caller passes a type position, which is never null.

[CatarinaGamboa]

Codex review, round 1

• [P2] Handle concatenated state annotations when locating values (AuxStateHandler.java:438-439): for a value such as from = "open(" + "this)", getAnnotationValuePosition gets the whole binary expression and strips its first and last characters as if it were one quoted literal, so the highlight covers expression syntax. Use the literal's own position only for a single string literal, and fall back otherwise.

[CatarinaGamboa]

Round 1 reply: fixed. valuePosition now uses the annotation's own position only when the value is a CtLiteral. A concatenated value falls back to the text search, which is what main does (main's search never matches a concatenation either, so it ends up at the element position). No test added: concatenated state values are rare, and the fallback is the unchanged main path. Suite: 731 tests, 0 failures.

[CatarinaGamboa]

Codex review, round 2

No findings: "I found no actionable regressions in the diff. The focused declaration-position and diagnostic tests pass." The loop ends here.