GeezerVison

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]>