Origin note: say what a call's return refinement guarantees about an argument it gives by CatarinaGamboa · Pull Request #530 · liquid-java/liquidjava

CatarinaGamboa · 2026-11-10T16:55:27Z

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 · 2026-11-10T17:09:22Z

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 · 2026-11-10T17:32:01Z

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 · 2026-11-10T17:44:12Z

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 · 2026-11-10T17:51:13Z

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 · 2026-11-10T18:04:38Z

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 · 2026-11-10T18:11:24Z

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 · 2026-11-10T20:17:40Z

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.

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 <noreply@anthropic.com>

…ives A refinement error whose Expected is about a call argument that is a call to a refined method now has the note "From: <call> (<File>:<line>) guarantees only <refinement>", instantiated as the error writes it. An equality _ == g(...) defining a ghost is left out when the ghost is nowhere else in the refinement: then it constrains no value, so what is left is exactly what the refinement says about the value. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The conjunct _ == g(...) is left out only when g is a declared ghost (a built-in such as length may be interpreted), g(...) is in no other conjunct and not in Expected, and every fact of Found that mentions it is the argument's own equality with it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…tees ... Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…rameter Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa · 2026-11-11T12:17:58Z

Codex review, round 7

Run after the rebase onto main (#528 squash-merged; code unchanged). This round covers "Leave out the returned-value note when it names an argument by its parameter", the round-6 fix that had not been reviewed yet.

codex exec review --base origin/main:

No actionable regressions were identified. The verifier test suite passes.

Nothing left to fix.

…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 <noreply@anthropic.com>

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

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

This was referenced Nov 10, 2026

Say where the wrong state or value comes from (From note), and counterexamples for state errors #522

Closed

Mark code in every message with backticks: blue in the CLI, code font in the IDE #532

Closed

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

CatarinaGamboa mentioned this pull request Nov 10, 2026

Origin note: say where the wrong state of a receiver comes from #528

Merged

CatarinaGamboa mentioned this pull request Nov 10, 2026

Mark code in every message with backticks, and name the lines they refer to #533

Merged

CatarinaGamboa changed the title ~~From note: say what a call's return refinement guarantees about an argument it gives~~ Origin note: say what a call's return refinement guarantees about an argument it gives Nov 10, 2026

CatarinaGamboa and others added 7 commits November 11, 2026 12:06

Keep a ghost definition when the ghost is applied anywhere else

9d2d9e7

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Keep a ghost definition when an alias may apply the ghost

edaba46

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Never take a built-in function for a ghost of the same name

b7df716

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Write the returned-value note as Origin: <File>:<line>, <call> guaran…

7b0cf52

…tees ... Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Leave out the returned-value note when it names an argument by its pa…

fa84640

…rameter Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

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

CatarinaGamboa merged commit 590268e into main Nov 11, 2026
1 check passed

Navigation Menu

Repository navigation

Origin note: say what a call's return refinement guarantees about an argument it gives - #530

Origin note: say what a call's return refinement guarantees about an argument it gives#530
CatarinaGamboa merged 7 commits into
mainfrom
from-note-f4

CatarinaGamboa commented Nov 10, 2026 •

edited

Loading

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 11, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

CatarinaGamboa commented Nov 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

When it is printed

A2_10, before and after

Test

Conflicts

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Clean-code review

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 1

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 2

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 3

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 4

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 5

Uh oh!

CatarinaGamboa commented Nov 10, 2026

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

Uh oh!

CatarinaGamboa commented Nov 11, 2026

Codex review, round 7

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

CatarinaGamboa commented Nov 10, 2026 •

edited

Loading