[CatarinaGamboa]

Closes #522, part 1 of 5: From note F3, unrefined parameter. Design: #522 (comment)

A refinement error whose Expected says nothing the verifier knows now gets a message note naming the cause, when the value is an unrefined parameter of the enclosing method. The CLI prints the note under the headline. getMessageNotes() carries it to the extension, which is meant to show it in the hover (vscode-liquidjava#188).

When the note is printed

All of these must hold, or there is no note:

• the category is UNKNOWN;
• every variable of Expected is a parameter of the enclosing method or constructor, by name. A reassigned parameter has an instance, which Expected would name instead;
• each such parameter's context Variable has the declared refinement true.

The note restates the declaration. It says nothing about callers and adds no fact to Found.

A2_04, before and after (only study task that changes)

 Refinement Error: expected timeout >= 0 but could not prove it
+  From: timeout is a parameter of checkCimReachable(String, int) (line 94) with no refinement
 103 |
 104 |         try (Socket socket = new Socket()) {
 105 |             socket.connect(new InetSocketAddress(host, port), timeout);

A2_10, A1_38, A1_01, A1_56, A1_09, practice and practice2 are byte-identical to main. Each task still gives exactly one error, on its reportedLine.

Changes

• LJDiagnostic.addMessageNote: getMessageNotes() returns these notes, and RefinementError puts them after its alias where lines. This is the hook the later From PRs use.
• FromNotes.unrefinedParameters, called where VCChecker builds the refinement error.
• Test: TestFromNotes on the existing fixture ErrorUnknownArgument.java. It fails without the change.

Conflicts

• May conflict 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: headline and general hint in RefinementError). The overlap is only the getMessageNotes override, and it is a trivial rebase.
• The later parts of Say where the wrong state or value comes from (From note), and counterexamples for state errors #522 (F1/F2, F4) stack on this branch.

Tests: mvn test, 729 run, 0 failures.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main: "I found no actionable bugs in the diff."

Custom prompt asking for soundness counterexamples (programs where the note is printed but false). It found two:

1. An external spec refines the parameter. @ExternalRefinementsFor("LJExternFirst") interface … { void use(@Refinement("_ > 0") int amount); } printed From: amount is a parameter of use(int) (line 8) with no refinement. The verifier does not check the body against that spec, but "with no refinement" is false.
2. Explicit @Refinement("true") on the parameter. The note said "with no refinement".

Fixed (both), in b-commit "Leave out the From note for an annotated or externally refined parameter". There is no note when:

• the parameter carries any @Refinement annotation, or
• a context function for the same method (class, name, arity) refines that parameter.

Both programs now print no note. Tests: 729 run, 0 failures.

No regression test added. Each case would need a new fixture file, and the PM asked for lean tests. I'll add them if wanted.

[CatarinaGamboa]

Clean-code review

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

Fixed:

• FromNotes.java - [core-fail-fast] A parameter without a valid source position would have printed (line -1). Now there is no note.
• FromNotes.java - [solid-srp] The "is the parameter refined anywhere" check is its own method (isRefined), apart from building the note text.

Declined:

• [pattern-strategy] An interface for the kinds of From note. There is one kind here, and the later PRs add one function each. That would be YAGNI for this PR.
• [func-few-arguments] unrefinedParameters(error, checked, context) keeps three arguments. Bundling them would add a type for one call site.

[CatarinaGamboa]

Codex review, round 2

codex exec review:

[P2] Match the exact overload before suppressing a parameter note. With two same-arity overloads, a refinement on one overload's parameter suppresses the note for an unrefined parameter of the other.

Fixed in "Match a parameter's specification by its method's parameter types". isRefined now compares the qualified parameter types too.

• Check: void use(int amount) { take(amount); } next to void use(@Refinement("_ != 0") long amount) {} prints the note for use(int) again.
• The round 1 cases (external spec, @Refinement("true")) still print no note.

Tests: 729 run, 0 failures.

Custom soundness prompt: stopped by Codex's content filter partway through, with no findings. I'll rephrase it in round 3.

[CatarinaGamboa]

Codex review, round 3

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

Soundness prompt (rephrased, so the content filter let it through). It tried inner, anonymous and local classes, lambdas, constructors, records, varargs, generics and inherited specs. It found no case where the note names the wrong parameter, method or line, or calls a refined parameter unrefined. It reported two formatting differences:

• use(List<String> names, int n) is shown as use(List, int);
• use(int n, String... labels) is shown as use(int, String[]).

Declined, both. The signature is written the way the state hints already write methods (StateHints.parameters: CtTypeReference::getSimpleName, so read(byte[], int, int)). One convention across the messages beats Java source syntax in one note. Neither form states anything false.

This ends the Codex loop for this PR: nothing relevant is left.