[CatarinaGamboa]

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

 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

 State Refinement Error: found compression(wParam) == compressionNotExplicit but expected compression(wParam) == compressionExplicit || compression(wParam) == compressionTypeSet
+  Origin: line 130, writer.getDefaultWriteParam() returns compression(wParam) == compressionNotExplicit

 State Refinement Error: expected redoState(undoManager) == redoable but could not prove it
+  Origin: line 69, frame.getUndoManager() says nothing about redoState(undoManager)

 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 One headline frame: found … but expected … for refinement errors #520/Drop the general UNKNOWN hint and show every from in declared-here #521 (another agent: AuxStateHandler declared-here): the one throwStateRefinementError call in changeState, which gets a messageNotes argument. The rest is additive.
• With Drop the guard hint when a call-sequence hint exists, and reword it #518/State hints: name only the state the call leads to #519 (StateHints): none.
• With Show a counterexample for state errors, restricted to the shown Found #527 (state counterexample, mine): both add a parameter to throwStateRefinementError, a one-line rebase.

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

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

Fixed, while writing it:

• [solid-srp] The walk and the three note kinds are in their own class, StateOrigin. AuxStateHandler only calls it, best effort, as it calls the hint and category helpers.
• [core-fail-fast] The call's code is read from its source position, and it is left out when the position or source is missing. Spoon's getOriginalSourceFragment threw on A1_09's applyDisplayMode call and aborted verification. I caught that on the study tasks before pushing.
• [core-dry] One factsOn helper projects every predicate (Found, a to, a return refinement) on the shown sets. One implies helper wraps StateSolver.
• [name-meaningful] CallResult / getReturnedBy instead of reusing StateChange for returned values. It also keeps DecidingArgument's walk unchanged.

Declined:

• [func-few-arguments] StateOrigin.note(...) and AuxStateHandler.fromNote(...) take 10 and 9 arguments. They mirror the neighbouring best-effort helpers (checkedElsewhere, stateHints), which pass the same pieces. A parameter object for one call site is a refactor of changeState, outside this PR.
• [core-dry] StateOrigin.setsOf repeats the three-line "sets a predicate names" stream in DecidingArgument.find. Sharing it would edit DecidingArgument, which Drop the guard hint when a call-sequence hint exists, and reword it #518/State hints: name only the state the call leads to #519 work near. It is left for a follow-up.

[CatarinaGamboa]

Codex review, round 1

codex exec review:

[P2] Check the returned call after crossing unrelated state changes. After task = create() and a lock-only transition, a later phase error loses its note: the walk reaches the original instance but calls creationNote instead of checking returnedBy.

Soundness prompt. It found three programs with misleading notes:

Program	Printed	Why it is wrong
x.start(); LastSetTask y = x; y.finish(); x.needsIdle();	From: phase(x) == running, last set at line 14: x.start()	y.finish() changed the same object later
x = new BranchTask(); if (flag) { x.start(); x.reset(); } x.await();	From: x is created at line 13 by new BranchTask(), which makes it phase(x) == idle	on the flag path, reset() gave the state
x = create(); y = x; y.start(); x.await();	From: x = ReturnedAliasTask.create(), line 14, which returns phase(x) == idle	y.start() changed it

The verifier itself does not follow state changes through aliases (#393 is open), so Found is already wrong in cases 1 and 3. A From note must not present that as a cause.

Fixed, all four, in "Leave out the From note for an aliased receiver, and follow a returned value across other sets":

1. No note when another name may hold the receiver before the call. That covers a local or parameter copied (T y = x, y = x, ?:), returned, or used in a lambda or a local or anonymous class, where that use comes earlier or sits in a loop around the call. A field receiver also gets no note; this keeps it.
   • Uses after the call do not count: A1_01 returns wParam after line 136 and keeps its note.
   • Passing the receiver as an argument does not count either. The verifier does not model a callee changing an argument's state, so the note would still agree with Found. I'll raise this with the PM.
2. The creation fallback also needs no other call on the local to a method that changes state, and no failing call that a loop may repeat.
3. The walk now checks returnedBy wherever it stops, also after crossing changes to other sets. It reads Found's facts about the instance it reached when Found has none about the receiver itself. The P2 program now gives From: task = TwoSetTask.create(), line 16, which returns phase(task) == idle.

All four programs now print no note, or a sound one. The study tasks are unchanged: A1_38, A1_01 and A1_56 keep their mock-up notes, and A1_09 has none.

In the suite's fixtures:

• ErrorDeferredCallbackState loses its 4 notes (the receiver is captured, or a field);
• the ErrorLoopStateNone fallback is gone (the failing call has a to and a loop repeats it);
• ErrorArgumentPicksTheStateEarlier gains From: tilingOff(param), last set at line 25: param.setTilingMode(1), across compress(). That is correct.

New test: stateOfAReceiverAnotherNameMayHoldIsNotTraced, on the lambda case of the existing ErrorDeferredCallbackState. It fails without the fix.

Tests: 733 run, 0 failures.

[CatarinaGamboa]

Codex review, round 2

codex exec review:

• [P2] Treat passing the receiver to another method as possible aliasing. A callee may keep a reference and change the state.
• [P2] Limit the last-set note to the states that call changed. With two wrong sets, the note attributed both to a call that changed one.

Soundness prompt. It found five programs, all found phase(task) == idle but expected phase(task) == running, where task escapes before the call:

• mutate(task) calls start() (also on one branch);
• ArrayTask[] all = {task}; all[0].start();
• all.add(task); all.get(0).start();
• task = create(); mutate(task).

In each one, the note named the constructor or the factory as the origin.

Fixed, all, in "Count a receiver passed to a method as aliased, and say only what a change set":

1. Any use of the receiver local or parameter that may run before the call counts as a possible alias, other than as a call's receiver or in ==/!=. That covers arguments, array initializers, copies, returns, conditionals, and lambda or local-class uses.
   • A use inside a return or throw cannot run again in a loop around the call. This keeps A1_38's note: its createTaskIterator(buffered, …) is in a return inside the loop around reset().
2. The last-set note shows only the facts on the shown sets the change names. d.lockIt(); d.walkThrough() (needs opened && unlocked) now gives From: lock(d) == locked, last set at line 15: d.lockIt(), not the door state too.

Checks:

• All eight programs from rounds 1 and 2 now print no note, except the round 1 P2 case, which is sound (From: task = TwoSetTask.create(), line 16, which returns phase(task) == idle).
• The study tasks are unchanged: A1_38, A1_01 and A1_56 keep their notes; A1_09 has none.
• The fixture notes are unchanged from round 1.

Tests: 733 run, 0 failures.

[CatarinaGamboa]

Codex review, round 3

codex exec review: "No actionable regressions were identified."

Soundness prompt. It found three misleading notes:

Program	Printed	Why
@StateRefinement(to = "running(_)") static T makeRunning(), then x = makeRunning(); x.needIdle()	From: x = makeRunning(), line 15, which says nothing about phase(x)	the method's state refinement does give the value a state
x.start(); x.resetInternally(); x.needIdle(), where resetInternally is @StateRefinement(from = "running(this)") but its body calls reset()	From: phase(x) == running, last set at line 13: x.start()	the body changes the state, against its contract
a constructor @StateRefinement(to = "idle(this)") whose body calls start()	From: phase(x) == idle, last set at line 10: new ConstructorCallsMethod()	the body breaks the constructor's contract

Fixed (1) in "Leave out the From note after an unspecified method body on the receiver". "Says nothing" also needs the called method to have no state refinement with a to.

Fixed, a related gap, while looking at (2). No note when a method of the analyzed code with no state refinement is called on the receiver before the failing call. The verifier assumes such a call keeps the state, but that is an assumption, not a contract. ErrorUnknownMethodInComparisonState (where count() has a body) loses its note as a result, which is conservative.

Declined (2) and (3). In both, a method or constructor body breaks its declared state contract, and the verifier does not check bodies against state contracts. The error trusts the contract (its Found is running / idle), and the note quotes the same contract. Dropping notes whenever a body might break its own spec would drop every note on source classes. I'll flag the unchecked bodies to the PM as a verifier issue, separate from the messages.

Checks:

• The study tasks are unchanged: A1_38, A1_01 and A1_56 keep their notes; A1_09 has none.
• The earlier Codex programs are still silent or sound.

Tests: 733 run, 0 failures.

[CatarinaGamboa]

Codex review, round 4

codex exec review:

1. [P2] Check earlier helper calls before attributing this state. The alias and unspecified-body checks returned early for a this receiver.
2. [P2] Keep note-generation errors from replacing the state error. An LJError from the note's implies query is not caught.

Soundness prompt. It found three programs, all with a note where the alias rule asks for none:

• hold(this); this.needsIdle(): hold stores this in a static field;
• x.needsIdle(hold(x)): the argument runs before the call but comes later in the source, so the "before the call" test missed it;
• the same with a factory-assigned x (F2).

Fixed (1) and all three programs in "Apply the alias checks to this and to the failing call's own arguments":

• For a this receiver, the same checks now run over every this access of the method in the same class, explicit or implicit: any escape, and any call to an unspecified source method. A field access or a call on this is not an escape.
• A use inside the failing call's arguments counts as running before the call.

All three programs now print no note. ErrorLoopPostState (implicit this) loses its note, which is conservative. The study tasks are unchanged: A1_38, A1_01 and A1_56 keep their notes; A1_09 has none.

Declined (2): it does not happen. LJError extends RuntimeException, and AuxStateHandler.fromNote catches RuntimeException and returns no note. My first version had catch (LJError | RuntimeException e), and javac rejected it: "Alternative LJError is a subclass of alternative RuntimeException". So a failing implies query never replaces the state error.

Tests: 733 run, 0 failures.

[CatarinaGamboa]

Codex review, round 5 (last)

Soundness prompt. A bound method reference keeps the receiver: Runnable later = task::start; …; later.run(); before the failing call. Since task was the target of the method reference, it counted as a safe use, and notes named the constructor, task.start() or the factory as the origin.

Fixed in "Count a method reference to the receiver as aliasing it". Only the target of a call or a field access is a safe use, and a method reference counts as an escape. The two programs (three errors) now print no note. The study tasks and fixture notes are unchanged.

codex exec review:

[P2] Preserve the state error when origin lookup fails.

This is round 4's point again. Declined, as there: LJError extends RuntimeException, and javac rejects catch (LJError | RuntimeException e) for that reason, so fromNote's catch (RuntimeException e) already turns a failed or unknown solver query into "no note", and the error is still reported. I added a one-line comment at the catch so the next reader doesn't have to check.

Tests: 733 run, 0 failures.

This is the fifth round, the agreed limit. Each round found narrower cases, from aliases to arguments, this, argument order and now method references. They all share one root cause: the verifier does not follow state changes through other names (#393 is open). The note now leaves itself out whenever the receiver may escape before the call. The remaining risk is the same as the verifier's own Found: a declared contract whose body breaks it.

[CatarinaGamboa]

Origin rename (PM review), and Codex review of it

What changed:

• "From:" is now "Origin:", and every origin note has one shape, Origin: <where>, <call or variable> <verb> <state or refinement>:
  • makes for the call that last set the state sets;
  • returns or says nothing about for a returned value;
  • creates x with for the constructor fallback, so it doesn't claim the current state;
  • is a parameter of … with no refinement for the parameter note.
• From note: name an unrefined parameter as the unknown value's origin #526 was merged with the old text. So this PR's first commit renames it: FromNotes → OriginNotes, the test file too, and the text becomes Origin: line 94, timeout is a parameter of checkCimReachable(String, int) with no refinement.
• The PR is rebased onto main (which now has State hints: name only the state the call leads to, and no guard when a call sequence works #524, Use found … but expected … for refinement errors, drop the general hint, declare every from #525 and From note: name an unrefined parameter as the unknown value's origin #526) and retargeted to main. The only overlap was Use found … but expected … for refinement errors, drop the general hint, declare every from #525's declarationPositions list in throwStateRefinementError, kept with messageNotes beside it.
• The soundness conditions are unchanged. The PR body has the new before/after.

Codex review (one round, as asked):

• codex exec review: "I found no actionable regressions in the diff. The targeted origin-note tests pass."
• Soundness prompt: "I found no Java program where the new origin text is false or misleading. The rename preserves the note conditions… the constructor fallback uses 'creates … with,' not 'makes.'"

Tests: 736 run, 0 failures.