GeezerVison

Copy link

Copy Markdown

Collaborator

CatarinaGamboa force-pushed the from-note-f4 branch from c90ad42 to 10efb8e Compare November 10, 2026 17:09

Refinement Error: count(xs) == 2 is not a subtype of count(xs) < 0
  From: count(xs) (ArrayLength.java:4) guarantees nothing about count(xs)

CatarinaGamboa force-pushed the from-note-f4 branch 2 times, most recently from 670a69c to b9ad243 Compare November 10, 2026 17:44

Refinement Error: b.size() == 5 is not a subtype of b.size() > 10
  From: b.size() (ReceiverAlias.java:12) guarantees nothing about b.size()

Refinement Error: value() == mark(this) is not a subtype of AboveMark(value(), this)
  where AboveMark(value, obj) = value > mark(obj)
  From: value() (AliasExpected.java:8) guarantees nothing about value()

Refinement Error: len(a) == length(a) is not a subtype of len(a) > 10
  From: len(a) (UnrelatedLengthGhost.java:9) guarantees nothing about len(a)

CatarinaGamboa force-pushed the from-note-state branch from 4757b3b to 51666ee Compare November 10, 2026 20:06

CatarinaGamboa force-pushed the from-note-f4 branch from 7d24ec8 to 1861bb5 Compare November 10, 2026 20:06

Closes #522, part 2: **origin notes F1 and F2**, where the wrong state
comes from. Design:
#522 (comment)

**Base: `main`.** #526 is merged. #530 is stacked on this PR, so
retarget it to `main` before merging this one with `--delete-branch`.

## The Origin note
The PM's review renamed the note from **"From:"** to **"Origin:"**,
because "From" read like `@StateRefinement(from = …)` in declared-here.
Every origin note now has one shape, `Origin: <where>, <call or
variable> <verb> <state or refinement>`, and only the verb changes. The
first commit renames the note #526 merged (`FromNotes` → `OriginNotes`,
`TestFromNotes` → `TestOriginNotes`). The soundness conditions are
unchanged.

| Case | Text |
|---|---|
| F1, the call that last set the sets | `Origin: line 134, new
BufferedInputStream(stream) makes markState(buffered) == unmarked` |
| F2, a returned value | `Origin: line 130,
writer.getDefaultWriteParam() returns compression(wParam) ==
compressionNotExplicit` |
| F2, nothing known | `Origin: line 69, frame.getUndoManager() says
nothing about redoState(undoManager)` |
| F1 fallback, creation | `Origin: line L, new T(…) creates x with
<state>` |
| F3 (#526) | `Origin: line 94, timeout is a parameter of
checkCimReachable(String, int) with no refinement` |

"Makes" is used only for the call the walk proves last set the shown
sets. The fallback says "creates … with", because a later call may have
set the state again. That is a fact about the constructor, not about the
current state.

## When there is no note at all
No origin note is given when the receiver may change state out of the
verifier's sight before the call. That covers three cases:
- **Another name may hold it.** A local, a parameter or `this` is used,
before the call, other than as the target of a call or field access or
in `==`/`!=`. That means copied, passed as an argument (including to the
failing call itself), stored in an array, returned, bound in a method
reference (`x::start`), or used in a lambda or a local class. "Before"
means earlier in the source, in the failing call's arguments, or in a
loop around the call, unless the use is inside a `return`/`throw`.
- **A method of the analyzed code with no state refinement is called on
it before.** The verifier assumes such a call keeps the state.
- **It is a field.**

Declared state contracts are trusted, as the verifier trusts them. A
body that breaks its own declared contract is a verifier issue, outside
the notes (see the round 3 reply).

## Which sets
The note covers the sets that the failing call's `from` checks. When the
state machine models the call, it narrows them to the sets where some
state the receiver may be in is the state of no allowed state. This only
selects what is shown (S1).

## F1, a state set by a call
Walk back from the receiver through `StateChange`/`previous()` to the
first change whose `to` names a shown set. The note is printed only if:
- every instance on the way has a `StateChange`, so the walk crosses no
join, loop head or unknown origin;
- every change crossed names none of the shown sets. Each `to` keeps the
sets it does not name, through `set(this) == set(old(this))`;
- `StateSolver.implies(<instance after that change>, <Found's facts on
the shown sets>)` holds.

Text: `Origin: line L, <call> makes <Found on the sets that change
names>`. With two wrong sets, a change to one is not given the other.

**Fallback, when the walk breaks.** The note gives the creation fact
only if all hold:
- the receiver is a local whose only write is its initializer, a
constructor call with a single state refinement;
- no other call on it is to a method that changes state, and no loop may
repeat the failing call;
- Found's facts on the shown sets imply what that constructor gives.

Text: `Origin: line L, new T(…) creates x with <state>`. It is a fact
about the constructor. The last condition stops it from speaking when
the state may have changed since (A1_09).

## F2, a state from a returned value
Printed only if the walk reaches, possibly after crossing changes to
other sets, an instance with no `StateChange` that holds the call result
it was assigned. Instances now record a `CallResult` when a local is
declared or assigned from a call to a refined method. A state-preserving
call keeps it, as it keeps the `StateChange`. Joins, loop heads and
transitions make new instances without one.
- `Origin: line L, <call> returns <facts>`: the conjuncts of the
instantiated return refinement on the shown sets. Printed only if they
imply Found's facts on those sets.
- `Origin: line L, <call> says nothing about <set>(x)`: printed only if
all hold:
  - Found has no fact on the sets;
- the method has no state refinement with a `to` (as `to =
"running(_)"`);
- the return refinement names no state of them, mentions no variable but
`_`, and uses no alias. This rules out `_ == this`-style returns;
- no shown set has a generated name (`state1`), which the message would
otherwise never show.

## DebugLog check for A1_38 (asked before coding F1)
With `-d`, the VC at `buffered.reset()` (line 157) has a single
`buffered` instance, `#buffered_259 : (stream == open) ∧ (markState ==
unmarked)`. That is the constructor's state, with no ITE and no
loop-head instance. The note also took the F1 path, which needs a
`StateChange` on that instance. So neither loop (lines 136 and 150)
creates a join for `buffered`.

A broken walk now logs `[WARN] Origin note: no known call gives #x_n its
state, e.g. a join of branches`. A1_09 logs it for `#host_95`.

## Study tasks, before (main) and after
```diff
 State Refinement Error: found stream(buffered) == open && markState(buffered) == unmarked but expected markState(buffered) == marked && stream(buffered) == open
+  Origin: line 134, new BufferedInputStream(stream) makes markState(buffered) == unmarked
```
```diff
 State Refinement Error: found compression(wParam) == compressionNotExplicit but expected compression(wParam) == compressionExplicit || compression(wParam) == compressionTypeSet
+  Origin: line 130, writer.getDefaultWriteParam() returns compression(wParam) == compressionNotExplicit
```
```diff
 State Refinement Error: expected redoState(undoManager) == redoable but could not prove it
+  Origin: line 69, frame.getUndoManager() says nothing about redoState(undoManager)
```
```diff
 Refinement Error: expected timeout >= 0 but could not prove it
-  From: timeout is a parameter of checkCimReachable(String, int) (line 94) with no refinement
+  Origin: line 94, timeout is a parameter of checkCimReachable(String, int) with no refinement
```
- A1_09: no origin note. Its receiver is a join, and Found does not say
the state `new JFrame(…)` gives.
- A2_10, practice and practice2: unchanged.

Each task still gives exactly one error, on its `reportedLine`. All
three notes are the review's mock-ups, word for word.

I checked every state-error fixture of the suite. Each note names the
creating or the last call. After the Codex rounds, the fallback fires in
none, and fixtures where the receiver is captured, a field, `this` in a
loop, or given an unspecified call get no note.

## Tests
`TestOriginNotes`, three tests that fail without the change:
- `ErrorStateHintMultipleSets` (existing): `Origin: line 27, d.lock()
makes lockState(d) == locked`. Only the wrong set is named, and the walk
stops at the change to it;
- `ErrorStateFromReturnedValue` (new, small; no existing fixture assigns
a state from a return refinement): `Origin: line 27,
FromReturnedTask.create() returns phase(task) == idle`.

- `ErrorDeferredCallbackState` (existing): the receiver captured by a
lambda gets no note.

`mvn test`: 736 run, 0 failures.

## Conflicts
- With #520/#521 (another agent: `AuxStateHandler` declared-here): the
one `throwStateRefinementError` call in `changeState`, which gets a
`messageNotes` argument. The rest is additive.
- With #518/#519 (`StateHints`): none.
- With #527 (state counterexample, mine): both add a parameter to
`throwStateRefinementError`, a one-line rebase.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>

CatarinaGamboa force-pushed the from-note-f4 branch from ef36014 to fa84640 Compare November 11, 2026 12:06

CatarinaGamboa changed the base branch from from-note-state to main November 11, 2026 12:06

1 check passed

…fer to (#533)

Closes #532. **Stacked on #530** (→ #528 → `main`). Retarget it to
`main` before #530 is merged with `--delete-branch`.

Every message that shows code now marks it with backticks, inside the
message string:
- headlines (`found … but expected …`, `expected … but could not prove
it`);
- hints;
- origin notes;
- the declared-here gloss (`where … means …`);
- alias `where` lines;
- counterexamples.

## How each client sees it
- **Plain text** (`getMessage()`, `getMessageNotes()`, `Hint.message()`,
`getCounterexampleStr()`, `getDeclarationNotes()`, and so the Problems
tab and the hover): the string with backticks, as rustc writes its
messages.
- **CLI:** each span in blue (the existing `Colors.BLUE`), without
backticks. The backticks stay when colour is off: `NO_COLOR` set
(https://no-color.org) or no console (output piped or redirected). The
colour switch applies to code spans only; the CLI's other colours are
unchanged.
- **IDE:** the same backticked strings, plus
`LJDiagnostic.getReferences()`, a `List<SourceReference>` with one entry
per line reference. See below.

**Escaping:** `Code.of` fences code that holds backticks with a longer
run, and pads it with one space on each side when it holds a backtick or
starts or ends with a space: ``` `` c == '`' `` ```. `Code.render`
strips exactly that padding, so it shows any non-empty code exactly as
marked.

## Source references (for vscode-liquidjava#192)
`record SourceReference(String message, String text, int start, String
file, int line, int column)`:
- `message`: the whole message line it belongs to, exactly as
`getMessageNotes()` or `Hint.message()` gives it;
- `text`: the words of `message` that name the place, e.g. `line 134` or
`ArrayListRefinements.java:162`;
- `start`: where `text` starts in `message`, as a UTF-16 index (a
Java/JS string index), so `message.substring(start, start +
text.length())` is `text`. Use it instead of searching, because the code
of a call can hold the same words (`d.lock("line 18")` on line 18);
- `file`: the absolute path; `line`, `column`: 1-based, from Spoon.

Who carries one:
- every origin note: the call, parameter, constructor or
return-refinement declaration it names;
- the deciding-argument hint (`… on line 20 decides …`), through the new
`Hint.reference()`, which is null for other hints.

`getReferences()` returns the notes' references first, then the hints'.

## Before → after (CLI piped, so backticks shown)
```text
A1_38  State Refinement Error: found `stream(buffered) == open && markState(buffered) == unmarked` but expected `markState(buffered) == marked && stream(buffered) == open`
         Origin: line 134, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`
         - Call `buffered.mark(int)` before this call; afterwards `markState(buffered) == marked`
         where `marked(this)` means `markState(this) == marked`, `open(this)` means `stream(this) == open`
A1_01    Origin: line 130, `writer.getDefaultWriteParam()` returns `compression(wParam) == compressionNotExplicit`
         - Call `wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT)` before this call; afterwards `compression(wParam) == compressionExplicit`
A2_04  Refinement Error: expected `timeout >= 0` but could not prove it
         Origin: line 94, `timeout` is a parameter of `checkCimReachable(String, int)` with no refinement
          --> Counterexample: `timeout == -1`
A1_56    Origin: line 69, `frame.getUndoManager()` says nothing about `redoState(undoManager)`
         - Guard this call with `if (undoManager.canRedo())`; inside it, `redoState(undoManager) == redoable`
A2_10  Refinement Error: found `failures.size() == size(this.failures) && failures.size() >= 0` but expected `failures.size() > 0`
         Origin: ArrayListRefinements.java:162, `failures.size()` guarantees only `failures.size() >= 0`
```
For all eight tasks (six study tasks and both practice tasks), the
output with backticks removed is byte-identical to #530's. Each task
still gives exactly one error, on its `reportedLine`. On a terminal the
spans are blue and the backticks are gone. With `NO_COLOR=1` the
backticks stay.

## Changes
- `Code` (`of`, `render`), `SourceReference`, and `Colors.enabled()`.
- `LJDiagnostic`:
  - `addMessageNote(SourceReference)` and `getReferences()`;
- `toString` renders the message, notes, counterexample, hints and
declaration notes.
- Marked at the leaves where messages are built:
  - `ErrorMessage` (both headline frames);
  - `RefinementError` (counterexample, alias lines);
  - `AuxStateHandler.addMeanings` (gloss);
- `StateHints`: each state name, call, receiver and constructor, with
the prose words `or`, `and`, `then`, `with` left unmarked;
  - `OriginNotes`/`StateOrigin`, whose notes are now `SourceReference`s.
- `NotFoundError` marks the missing name and the suggestion (``Alias
`Positiv` could not be found``, ``Did you mean `Positive`?``).
- Not marked: the other error kinds (state conflicts, syntax errors) and
warnings, which the issue does not list. They are a follow-up if wanted.

## Tests
- 59 existing expectations gained backticks. Each change was made by a
script that accepts a new string only if removing its backticks gives
exactly the old one.
- `TestStateHints.assertHints` compares kind and message.
- New tests, each failing without the change:
  - `CodeTest` (fence, colour on and off);
  - `TestOriginNotes.noteNamesTheLineOfTheCallForClientsToLinkTo`;
  - a reference check in the deciding-argument hint test.

`mvn test`: 740 run, 0 failures.

## Conflicts
- **#524 and #525 are merged**, and this branch sits on top of them (via
#528's rebase), so it does not conflict with them. The lines of their
code it changes are:
- `StateHints.java`, on main: the hint templates at 116–119, 131–132,
182–184, 234, 239–240, 249, 252, 258, 260, 269, 295–297, 301, 303–305,
349, and `stateName` at 387–389;
- `RefinementError.java`, on main: 71 (counterexample) and 123 (alias
`where` lines);
  - `ErrorMessage.java` 39–41 (headline);
  - `AuxStateHandler.java` 865–866 (gloss).
- With the #529 agent's work: both may touch
`VCChecker.throwStateRefinementError`. This PR changes only the notes'
parameter type there.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>