[CatarinaGamboa]

Closes #522, part 3: origin note F4, a value returned by a call. Design: #522 (comment)

Stacked on #528 (CallResult and the Origin rename). Retarget this PR to main before #528 is merged with --delete-branch, or GitHub closes it.

A refinement error whose Expected is about a call argument that is itself a call to a refined method now says what that method's return refinement guarantees. This is the UX sign-off's amendment 1 for A2_10: instantiated as the error writes it, with the ghost-defining conjunct dropped.

When it is printed

For each variable of Expected that is an argument instance with no variable of its own (shown as the call), holding the CallResult of a refined method whose refinement has a source position. Locals assigned from a call are left to #528's state notes. A refinement-error form for them (Origin: line 44, read() guarantees only n >= -1) is a question for the PM.

It is also left out when the refinement still names an argument the verifier calls after the callee's parameter (twice(0) for _ == b * 2), which would read as that parameter.

Text: Origin: <File>:<line>, <call> guarantees only <R'>, or Origin: <File>:<line>, <call> guarantees nothing about <call> when nothing is left. This is the shape #528 gives every origin note.

Why "only" is sound. R' is the instantiated return refinement minus each conjunct _ == g(…) where all hold:

• g is a declared ghost (@Ghost), and never a built-in name like length, even when some class declares a ghost of that name;
• g, on any arguments, appears in no other conjunct and not in Expected. Any arguments, because an alias of the receiver may constrain the ghost under another name;
• every fact of the error's Found that applies g is the argument's own equality with it;
• no alias application in the refinement, Expected or Found may hide a use of g.

Then nothing constrains g(…) but that equality, and ∃g. (_ == g ∧ Q()) ≡ Q(), since g := _ is a witness. So R' is exactly what the refinement says about the value. Nothing else is dropped. Otherwise the equality is kept, e.g. Origin: …, count(xs) guarantees only count(xs) == length(xs).

A2_10, before and after

 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
 75 |     public Failure get() {

This is the amended mock-up, in the Origin shape. The other notes are unchanged from #528, and every task still gives one error on its reportedLine.

Across all refinement-error fixtures, the only new notes are the two call arguments in classes/found_binders_error: items.size() and count().

Test

TestOriginNotes.callArgumentIsTracedToWhatItsReturnRefinementGuaranteesAboutIt, on the existing classes/found_binders_error (the A2_10 reproducer, line 25): Origin: ArrayListRefinements.java:13, items.size() guarantees only items.size() >= 0. It fails without the change.

mvn test: 737 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, RefinementError headline): none in the files changed here. MethodsFunctionsChecker.createVariableRepresentingArgument gets one line, and Utils gets isBuiltin(name) over its existing DEFAULT_NAMES.

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

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

Fixed, while writing it:

• [core-dry] It reuses Origin note: say where the wrong state of a receiver comes from #528's CallResult (recorded once per call) and From note: name an unrefined parameter as the unknown value's origin #526's FromNotes, rather than a second record of what an argument call returned.
• [name-meaningful] The ghost rule has its own helpers (withoutGhostDefinitions, ghostDefined), so the "only" claim reads off one place.
• [core-yagni] My first version also fired for locals assigned from a call (n (…) guarantees only n >= -1 in ErrorLoopCondition). That reads badly and is outside F4's scope (a value shown as the call), so it is restricted to call arguments.

Declined:

• [solid-srp] FromNotes now has two note kinds. Both restate a declaration about Expected's variables, and a class per note would be one function each.

[CatarinaGamboa]

Codex review, round 1

codex exec review:

[P2] Preserve ghost equalities when they matter to the failed check. If the return refinement is _ == size(this) and the failed check refers to that ghost value, dropping the equality makes the note say the call "guarantees nothing", although the equality relates the value to size(this).

Soundness prompt. It found one underlying defect, shown in six programs (static, instance, generic overload, varargs, external String.length()). ghostDefined treated every function application as a ghost, including the built-in length, which the context fixes:

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

It found no wrong method, file or line.

My argument for "only" was too weak. ∃g. (_ == g ∧ Q) ≡ Q holds only if nothing else constrains g(…).

Fixed, both, in "Drop a ghost definition only when nothing else constrains that ghost". The conjunct _ == g(…) is dropped only if all hold:

• g is a declared ghost. A @Ghost on an external interface is registered as a parentless GhostState, so both registries are checked. A built-in like length is not;
• g(…) is in no other conjunct of the refinement;
• Expected does not mention g(…);
• every fact of the error's original Found that mentions g(…) is the argument's own equality with it, #arg == g(…).

Results:

• All six programs now print the full equality, e.g. From: count(xs) (ArrayLength.java:4) guarantees only count(xs) == length(xs).
• A2_10 keeps the mock-up note, From: failures.size() (ArrayListRefinements.java:162) guarantees only failures.size() >= 0, because size(#failures) is a declared ghost that nothing else constrains.

Tests: 734 run, 0 failures.

[CatarinaGamboa]

Codex review, round 2

codex exec review: "I found no actionable regressions in the diff."

Soundness prompt. It found a false note through an alias. With b = a and tally(a) == 5 known (from the constructor, or a.clear()), b.size() has _ == tally(#b). Found mentions tally(#a), not the exact term tally(#b), so the equality was dropped:

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

It also found the same with @RefinementAlias and with a second conjunct (guarantees only b.size() >= 0).

Fixed in "Keep a ghost definition when the ghost is applied anywhere else". The equality is dropped only if the ghost function appears, on any arguments, in no other conjunct, not in Expected, and in no fact of Found except the argument's own equality with it.

• All four programs now print From: b.size() (…) guarantees only b.size() == tally(b) (with && b.size() >= 0 where it applies).
• A2_10 keeps its mock-up note, because size appears only in that equality.

Tests: 734 run, 0 failures.

[CatarinaGamboa]

Codex review, round 3

Soundness prompt. It found a ghost use hidden in a @RefinementAlias, so the ghost-use check missed it. One case was in Expected:

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()

The other was in Found (MarkFive(obj) && obj.value() == mark(obj)).

Fixed in "Keep a ghost definition when an alias may apply the ghost". Any alias application in the refinement, Expected or Found now counts as a possible use of the ghost, so the equality is kept.

• Both programs now give … guarantees only value() == mark(this) and … guarantees only obj.value() == mark(obj).
• The alias, length and earlier cases keep their fixes.
• A2_10 is unchanged.

Tests: 734 run, 0 failures.

[CatarinaGamboa]

Codex review, round 4

codex exec review: "I found no actionable regressions in the diff."

Soundness prompt. It found one case. An unrelated class declares @Ghost("int length"). Since isGhost matched by name alone, the built-in array length(a) was taken for that ghost:

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)

Fixed in "Never take a built-in function for a ghost of the same name". A name the refinement language provides (length, addToIndex, getFromIndex, old) is never a ghost here. Utils gains isBuiltin(name) over its existing DEFAULT_NAMES, instead of a second list. The program now gives From: len(a) (…) guarantees only len(a) == length(a). Earlier cases and A2_10 are unchanged.

Tests: 734 run, 0 failures.

[CatarinaGamboa]

Codex review, round 5

codex exec review: "No actionable defects were found. The targeted and full verifier test suites passed."

Soundness prompt: "I found no new Java program that produces a false, misleading, or incorrectly attributed note."

Nothing relevant is left, so this ends the Codex loop for this PR.

[CatarinaGamboa]

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

What changed:

• The note now reads Origin: <File>:<line>, <call> guarantees only <R>, the shape Origin note: say where the wrong state of a receiver comes from #528 gives every origin note. For A2_10: Origin: ArrayListRefinements.java:162, failures.size() guarantees only failures.size() >= 0.
• The PR is rebased onto Origin note: say where the wrong state of a receiver comes from #528's new base (main).

Codex review (one round):

• Soundness prompt: "I found no Java program where the new note was false or misleading… each note pointed to the return refinement declaration."

• codex exec review:

  [P2] Substitute call arguments before formatting the return note. For @Refinement("_ == b * 2") int twice(int b) called as twice(0), the argument's generated instance prints as the parameter b.

  Fixed in "Leave out the returned-value note when it names an argument by its parameter". The note is printed only when every variable left in the refinement, besides the value, is one the code names (a variable or an instance of one). take(twice(0)) now prints no note. A2_10, found_binders_error and the earlier Codex cases are unchanged.

Tests: 737 run, 0 failures.