From note: name an unrefined parameter as the unknown value's origin (#526)

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)
```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
 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 #520/#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 #522 (F1/F2, F4) stack on this branch.

Tests: `mvn test`, 729 run, 0 failures.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -22,6 +22,7 @@ public class LJDiagnostic extends RuntimeException {
     private String file;
     private SourcePosition position;
     private final List<Hint> hints = new ArrayList<>();
+    private final List<String> messageNotes = new ArrayList<>();
     private String counterexample;
     private ErrorCategory category;
     private static final String PIPE = " | ";
@@ -78,7 +79,12 @@ public List<SourcePosition> getDeclarationPositions() {
 
     /** Lines printed under the message that explain it, such as what the names it uses mean */
     public List<String> getMessageNotes() {
-        return List.of();
+        return Collections.unmodifiableList(messageNotes);
+    }
+
+    /** Adds a line printed under the message, such as where the value it is about comes from */
+    public void addMessageNote(String note) {
+        messageNotes.add(note);
     }
 
     /** Lines printed under the excerpt of where the refinement is declared that explain it */

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -116,10 +116,13 @@ public List<AliasExpansion> getExpectedAliases() {
         return expectedAliases;
     }
 
-    /** A where line declaring each alias the message uses */
+    /** A where line declaring each alias the message uses, then the other notes */
     @Override
     public List<String> getMessageNotes() {
-        return aliasDeclarations.stream().map(declaration -> "where " + declaration).toList();
+        List<String> notes = new ArrayList<>(
+                aliasDeclarations.stream().map(declaration -> "where " + declaration).toList());
+        notes.addAll(super.getMessageNotes());
+        return notes;
     }
 
     // Keeps the counterexample assignments to the terms of expected and of the found facts linked to them, except

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/FromNotes.java

@@ -0,0 +1,90 @@
+package liquidjava.processor.refinement_checker;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Optional;
+import java.util.stream.Collectors;
+
+import liquidjava.diagnostics.categories.ErrorCategory;
+import liquidjava.diagnostics.errors.RefinementError;
+import liquidjava.processor.context.Context;
+import liquidjava.processor.context.Variable;
+import spoon.reflect.declaration.CtConstructor;
+import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.CtExecutable;
+import spoon.reflect.declaration.CtMethod;
+import spoon.reflect.declaration.CtParameter;
+import spoon.reflect.declaration.CtType;
+import liquidjava.utils.Utils;
+
+/**
+ * The notes of a refinement error that say where the values its expected refinement is about come from. Each is given
+ * only when it restates what the verifier used, and is left out otherwise
+ */
+final class FromNotes {
+
+    private FromNotes() {
+    }
+
+    /**
+     * When nothing is known about the values expected constrains and each is a parameter of the enclosing method that
+     * is declared with no refinement, a note per parameter saying so. Nothing is said about the callers
+     */
+    static List<String> unrefinedParameters(RefinementError error, CtElement checked, Context context) {
+        Optional<CtExecutable<?>> method = enclosingMethod(checked);
+        List<String> variables = error.getExpected().getVariableNames().stream().distinct().toList();
+        if (error.getCategory().filter(ErrorCategory.UNKNOWN::equals).isEmpty() || method.isEmpty()
+                || variables.isEmpty())
+            return List.of();
+
+        List<String> notes = new ArrayList<>();
+        for (String variable : variables) {
+            Optional<CtParameter<?>> parameter = method.get().getParameters().stream()
+                    .filter(p -> p.getSimpleName().equals(variable)).findFirst();
+            // a written parameter has an instance, which expected would name instead
+            if (parameter.isEmpty() || !parameter.get().getPosition().isValidPosition()
+                    || !(context.getVariableByName(variable)instanceof Variable declared)
+                    || !declared.getMainRefinement().isBooleanTrue() || isRefined(parameter.get(), context))
+                return List.of();
+            notes.add(String.format("From: %s is a parameter of %s (line %d) with no refinement",
+                    error.getDisplayNames().get(variable), signature(method.get()),
+                    parameter.get().getPosition().getLine()));
+        }
+        return notes;
+    }
+
+    /**
+     * Whether the parameter is written with a refinement, even {@code true}, or a specification of its method refines
+     * it, such as an external one, which the method's body is not checked against
+     */
+    private static boolean isRefined(CtParameter<?> parameter, Context context) {
+        if (parameter.getAnnotations().stream()
+                .anyMatch(a -> a.getAnnotationType().getQualifiedName().equals("liquidjava.specification.Refinement")))
+            return true;
+        CtExecutable<?> method = parameter.getParent();
+        int index = method.getParameters().indexOf(parameter);
+        String owner = method.getParent(CtType.class).getQualifiedName();
+        String name = method instanceof CtConstructor<?> ? Utils.getSimpleName(owner) : method.getSimpleName();
+        List<String> types = method.getParameters().stream().map(p -> p.getType().getQualifiedName()).toList();
+        return context.getCtxFunctions().stream()
+                .filter(f -> owner.equals(f.getTargetClass()) && name.equals(Utils.getSimpleName(f.getName()))
+                        && types.equals(f.getArguments().stream()
+                                .map(a -> a.getType() == null ? null : a.getType().getQualifiedName()).toList()))
+                .anyMatch(f -> !f.getArguments().get(index).getMainRefinement().isBooleanTrue());
+    }
+
+    private static Optional<CtExecutable<?>> enclosingMethod(CtElement element) {
+        CtElement parent = element.getParent();
+        while (parent != null && !(parent instanceof CtMethod<?> || parent instanceof CtConstructor<?>))
+            parent = parent.getParent();
+        return Optional.ofNullable((CtExecutable<?>) parent);
+    }
+
+    /** The method as {@code name(ParameterType, ...)}, a constructor by its class name */
+    private static String signature(CtExecutable<?> method) {
+        String name = method instanceof CtConstructor<?> constructor ? constructor.getDeclaringType().getSimpleName()
+                : method.getSimpleName();
+        return name + method.getParameters().stream().map(p -> p.getType().getSimpleName())
+                .collect(Collectors.joining(", ", "(", ")"));
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -87,9 +87,11 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         }
         DebugLog.smtResult(result);
         if (result.isError()) {
-            throw new RefinementError(element.getPosition(), declarationPosition, expectedType,
+            RefinementError error = new RefinementError(element.getPosition(), declarationPosition, expectedType,
                     implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map,
                     result.getCounterexample(), customMessage, context.getAliases());
+            FromNotes.unrefinedParameters(error, element, context).forEach(error::addMessageNote);
+            throw error;
         }
     }
 

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java

@@ -0,0 +1,31 @@
+package liquidjava.api.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
+
+class TestFromNotes {
+
+    private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/";
+
+    @Test
+    void unrefinedParameterIsNamedWithItsMethod() {
+        LJError error = verify("ErrorUnknownArgument.java");
+        assertEquals(List.of("From: amount is a parameter of use(int) (line 10) with no refinement"),
+                error.getMessageNotes());
+        assertTrue(error.toString().contains(error.getMessage() + "\n  From: amount is a parameter"));
+    }
+
+    private static LJError verify(String test) {
+        CommandLineLauncher.launch(TEST_SUITE + test);
+        List<LJError> errors = Diagnostics.getInstance().getErrors().stream().toList();
+        assertEquals(1, errors.size(), "Expected exactly one error from " + test);
+        return errors.get(0);
+    }
+}