Show the definitions of the aliases a refinement error uses (#489)

Closes #295.

A refinement error now says what the aliases in Found and Expected mean,
both as structured data for the IDE and as text in the CLI.

## CLI
The message keeps the alias names. Under it, one `where` line per alias
the message uses, in order of appearance (Found first, then Expected),
each alias once. The definition is printed as the spec wrote it:
parameter names and named constants unchanged, whitespace collapsed to
one line.

**Nested aliases.** When a definition uses another alias, that alias
gets its own `where` line after the one that uses it, and so on down.
Recursive aliases are not expanded again.

### Repro 1: minimal, aliases in both Found and Expected
```java
@RefinementAlias("Positive(int x) { x > 0 }")
@RefinementAlias("Nat(int x) { x >= 0 }")
public class Probe {
    static void need(@refinement("Positive(_)") int v) {}
    static void run(@refinement("Nat(_)") int n) { need(n); }
}
```
Before:
```
Refinement Error: Nat(n) is not a subtype of Positive(n)
```
After:
```
Refinement Error: Nat(n) is not a subtype of Positive(n)
  where Nat(x) = x >= 0
  where Positive(x) = x > 0
```

### Repro 2: external spec with named constants
The `x_e_oss_a1_01_sliderecoder` exercise, with the `ImageWriteMode`
alias from the issue on the `javax.imageio.ImageWriteParam` spec,
`setCompressionMode(@refinement("ImageWriteMode(_)") int mode)`, and
`wParam.setCompressionMode(4);` after `getDefaultWriteParam()`.

Before:
```
Refinement Error: mode³⁰⁶ == 4 is not a subtype of ImageWriteMode(mode³⁰⁶)
```
After:
```
Refinement Error: mode³⁰⁶ == 4 is not a subtype of ImageWriteMode(mode³⁰⁶)
  where ImageWriteMode(m) = m == ImageWriteParam.MODE_DISABLED || m == ImageWriteParam.MODE_DEFAULT || m == ImageWriteParam.MODE_EXPLICIT || m == ImageWriteParam.MODE_COPY_FROM_METADATA
```

### Repro 3: `Port` alias
The `y_e_oss_a2_04_vmwarecimprobe` exercise plus `static
InetSocketAddress agentAt(String host, int port) { return new
InetSocketAddress(host, port); }`.

Before:
```
Refinement Error: expected Port(port⁶⁵) but could not prove it
 --> Counterexample: port⁶⁵ == 65536
```
After:
```
Refinement Error: expected Port(port⁶⁵) but could not prove it
  where Port(p) = 0 <= p && p <= 65535
 --> Counterexample: port⁶⁵ == 65536
```
The exercise's other error (`expected timeout >= 0 but could not prove
it`) uses no alias and is unchanged.

### Nested aliases and argument order
```
Refinement Error: expected Small(n) but could not prove it
  where Small(x) = Nat(x) && x < 10
  where Nat(x) = x >= 0

Refinement Error: Below(3, b) is not a subtype of Below(b, 5)
  where Below(a, b) = a < b
```

## Structured data for the IDE
`RefinementError` has two new accessors:
- `getFoundAliases()`: one entry per distinct alias invocation in the
final simplified Found VC chain, the chain the extension renders as
Found.
- `getExpectedAliases()`: the same for Expected.

Each returns a `List<liquidjava.diagnostics.AliasExpansion>`. Entries
come in order of appearance, followed by the aliases their definitions
use. `AliasExpansion` is a record:

| field | example | meaning |
|---|---|---|
| `invocation` | `Nat(n)` | the invocation as the diagnostic displays
it, so the client can find it in the Found/Expected text |
| `expansion` | `n >= 0` | the definition with the parameters replaced
by the arguments (all at once). Nested alias invocations are kept and
have their own entry |
| `alias` | `Nat` | alias name |
| `parameters` | `["x"]` | parameter names |
| `definition` | `x >= 0` | definition as written in the
`@RefinementAlias` |
| `declarationPosition` | `SourcePosition` | the `@RefinementAlias`
annotation value, for go-to-definition |

`declaration()` gives `Nat(x) = x >= 0`. `getMessageNotes()`, new on
`LJDiagnostic` and empty by default, returns the CLI `where` lines.

The extension would need to add these to `RefinementErrorDTO`, e.g.
`foundAliases` / `expectedAliases` built from a small
`AliasExpansionDTO`, with `declarationPosition` converted via
`SourcePositionDTO.from`. For repro 1 that gives:
```json
"foundAliases": [
  { "invocation": "Nat(n)", "expansion": "n >= 0", "alias": "Nat", "parameters": ["x"],
    "definition": "x >= 0", "declarationPosition": { "file": ".../Probe.java", "lineStart": …, "colStart": …, "lineEnd": …, "colEnd": … } }
],
"expectedAliases": [
  { "invocation": "Positive(n)", "expansion": "n > 0", "alias": "Positive", "parameters": ["x"],
    "definition": "x > 0", "declarationPosition": { "file": ".../Probe.java", "lineStart": …, "colStart": …, "lineEnd": …, "colEnd": … } }
]
```
Positions are elided above; they are the `@RefinementAlias` value range
in the extension's 0-based `SourcePositionDTO` form. With that DTO, the
webview can show each invocation's expansion next to Found and Expected
(hover or an expandable row) and link `alias` to `declarationPosition`.
The extension is not changed in this PR.

## Changes
- `AliasWrapper` keeps the definition text as written (whitespace
collapsed to one line, except inside string and char literals) and the
declaration position. `AliasDTO` exposes the raw text it already parsed.
- `AliasExpansion` (new) collects and substitutes the invocations.
- `RefinementError` takes the context aliases (from `VCChecker`) and
computes the expansions and the `where` lines.
- `LJDiagnostic.toString` prints the message notes under the message.

The earlier derivation-based expansion from #184, removed in #261,
attached alias bodies as origins in the expression derivation tree. The
VC chain has no such per-node origins, so this PR records the expansions
alongside the chain instead. It reuses the old approach of substituting
the arguments into the alias body.

`StateRefinementError` is not covered. Its Expected is states, and it
has its own Found shape.

## Tests
`TestAliasExpansions` (2 tests, existing fixtures, no new ones):
- `ErrorAlias`: Found and Expected each record their substituted
`InRange` invocation, with parameters and declaration line.
- `ErrorStaticFinalInAlias`: one `where` line with the constants as
written, printed right under the message.

Full verifier module (rebased on main): 708 tests, 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/AliasExpansion.java

@@ -0,0 +1,96 @@
+package liquidjava.diagnostics;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import liquidjava.processor.context.AliasWrapper;
+import liquidjava.rj_language.ast.AliasInvocation;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.Var;
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * An alias invocation in a diagnostic and what it stands for
+ *
+ * @param invocation
+ *            the invocation as shown in the diagnostic, e.g. {@code Nat(n)}
+ * @param expansion
+ *            the definition with the parameters replaced by the arguments, e.g. {@code n >= 0}; aliases it uses are
+ *            kept and have their own expansions
+ * @param alias
+ *            the alias name
+ * @param parameters
+ *            the parameter names of the alias
+ * @param definition
+ *            the definition as written in the alias declaration
+ * @param declarationPosition
+ *            where the alias is declared
+ */
+public record AliasExpansion(String invocation, String expansion, String alias, List<String> parameters,
+        String definition, SourcePosition declarationPosition) {
+
+    /** The alias as it is declared, e.g. {@code Nat(x) = x >= 0} */
+    public String declaration() {
+        return alias + "(" + String.join(", ", parameters) + ") = " + definition;
+    }
+
+    /**
+     * The expansions of the alias invocations in an expression, each invocation once in order of appearance, followed
+     * by those of the aliases their definitions use
+     */
+    public static List<AliasExpansion> of(Expression expression, List<AliasWrapper> aliases) {
+        Map<String, AliasWrapper> byName = new LinkedHashMap<>();
+        for (AliasWrapper alias : aliases)
+            byName.put(alias.getName(), alias);
+        Map<String, AliasExpansion> expansions = new LinkedHashMap<>();
+        collect(expression, byName, expansions, new HashSet<>());
+        return new ArrayList<>(expansions.values());
+    }
+
+    // Expands the invocations under expression, skipping aliases already being expanded so recursive ones end
+    private static void collect(Expression expression, Map<String, AliasWrapper> aliases,
+            Map<String, AliasExpansion> expansions, Set<String> expanding) {
+        List<AliasInvocation> invocations = new ArrayList<>();
+        invocationsOf(expression, invocations);
+        Map<String, Expression> bodies = new LinkedHashMap<>();
+        for (AliasInvocation invocation : invocations) {
+            AliasWrapper alias = aliases.get(invocation.getName());
+            // keyed by the invocation itself, since different names can display the same
+            String key = invocation.toString();
+            if (alias == null || expanding.contains(alias.getName()) || expansions.containsKey(key))
+                continue;
+            Expression body = substituteArguments(alias, invocation.getArgs());
+            expansions.put(key, new AliasExpansion(invocation.toDisplayString(), body.toDisplayString(),
+                    alias.getName(), alias.getVarNames(), alias.getDefinition(), alias.getPosition()));
+            bodies.put(key, body);
+        }
+        for (Map.Entry<String, Expression> body : bodies.entrySet()) {
+            Set<String> inner = new HashSet<>(expanding);
+            inner.add(expansions.get(body.getKey()).alias());
+            collect(body.getValue(), aliases, expansions, inner);
+        }
+    }
+
+    private static void invocationsOf(Expression expression, List<AliasInvocation> invocations) {
+        if (expression instanceof AliasInvocation invocation)
+            invocations.add(invocation);
+        for (Expression child : expression.getChildren())
+            invocationsOf(child, invocations);
+    }
+
+    // Replaces all parameters at once, through placeholders, so an argument naming another parameter is kept
+    private static Expression substituteArguments(AliasWrapper alias, List<Expression> args) {
+        Expression body = alias.getClonedPredicate().getExpression();
+        List<String> parameters = alias.getVarNames();
+        int n = Math.min(parameters.size(), args.size());
+        for (int i = 0; i < n; i++)
+            body = body.substitute(new Var(parameters.get(i)), new Var("#alias_parameter_" + i));
+        for (int i = 0; i < n; i++)
+            body = body.substitute(new Var("#alias_parameter_" + i), args.get(i).clone());
+        return body;
+    }
+}

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

@@ -70,6 +70,11 @@ public SourcePosition getDeclarationPosition() {
         return null;
     }
 
+    /** Lines printed under the message that explain it, such as what the names it uses mean */
+    public List<String> getMessageNotes() {
+        return List.of();
+    }
+
     public void setPosition(SourcePosition pos) {
         if (pos == null || pos.getFile() == null)
             return;
@@ -108,6 +113,8 @@ public String toString() {
         // title
         sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message)
                 .append("\n");
+        for (String note : getMessageNotes())
+            sb.append("  ").append(note).append("\n");
 
         // snippet
         String snippet = getSnippet();

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

@@ -3,13 +3,17 @@
 import java.util.ArrayList;
 import java.util.Comparator;
 import java.util.HashSet;
+import java.util.LinkedHashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 import java.util.stream.Collectors;
 
+import liquidjava.diagnostics.AliasExpansion;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint;
+import liquidjava.processor.context.AliasWrapper;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Enum;
@@ -41,13 +45,21 @@ public class RefinementError extends LJError {
     private final VCSimplificationResult found;
     private final Counterexample counterexample;
     private final SourcePosition declarationPosition;
+    private final List<AliasExpansion> foundAliases;
+    private final List<AliasExpansion> expectedAliases;
+    private final List<String> aliasDeclarations;
 
     public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
-            String customMessage) {
+            String customMessage, List<AliasWrapper> aliases) {
         super("Refinement Error", message(expected, found), position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
+        Expression foundExpression = found.getImplication().toPredicate().getExpression();
+        this.foundAliases = AliasExpansion.of(foundExpression, aliases);
+        this.expectedAliases = AliasExpansion.of(expected.getExpression(), aliases);
+        this.aliasDeclarations = aliasDeclarations(linkedToExpected(foundExpression, expected.getExpression()),
+                expected.getExpression(), aliases);
         this.counterexample = filterCounterexample(counterexample);
         this.declarationPosition = declarationPosition;
         if (!this.counterexample.isEmpty()) {
@@ -73,6 +85,16 @@ private static String message(Predicate expected, VCSimplificationResult found)
                 expected.getExpression().toDisplayString());
     }
 
+    // Each alias the message uses once, with those their definitions use, as declared
+    private static List<String> aliasDeclarations(Expression shownFound, Expression expected,
+            List<AliasWrapper> aliases) {
+        Map<String, String> declarations = new LinkedHashMap<>();
+        for (Expression shown : List.of(shownFound, expected))
+            for (AliasExpansion expansion : AliasExpansion.of(shown, aliases))
+                declarations.putIfAbsent(expansion.alias(), expansion.declaration());
+        return new ArrayList<>(declarations.values());
+    }
+
     /** Unknown when what was found says nothing about the values the expected refinement constrains */
     private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) {
         List<String> foundVariables = found.getImplication().toPredicate().getVariableNames();
@@ -97,6 +119,22 @@ public VCSimplificationResult getFound() {
         return found;
     }
 
+    /** The alias invocations in found and what they stand for */
+    public List<AliasExpansion> getFoundAliases() {
+        return foundAliases;
+    }
+
+    /** The alias invocations in expected and what they stand for */
+    public List<AliasExpansion> getExpectedAliases() {
+        return expectedAliases;
+    }
+
+    /** A where line declaring each alias the message uses */
+    @Override
+    public List<String> getMessageNotes() {
+        return aliasDeclarations.stream().map(declaration -> "where " + declaration).toList();
+    }
+
     // Keeps the counterexample assignments to the terms of expected and of the found facts linked to them, except
     // values found already states, so there is none when found fixes every value expected depends on. The terms of
     // expected come first, those found says nothing about before the rest, then the linked terms in the order of the

liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java

@@ -2,9 +2,12 @@
 
 import java.util.ArrayList;
 import java.util.List;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.Predicate;
 import liquidjava.utils.Utils;
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -13,10 +16,17 @@ public class AliasWrapper {
     private final List<CtTypeReference<?>> varTypes;
     private final List<String> varNames;
     private final Predicate expression;
+    private final String definition;
+    private final SourcePosition position;
 
-    public AliasWrapper(AliasDTO a, Factory factory, String klass, String path) {
+    private static final Pattern LITERAL_OR_SPACES = Pattern
+            .compile("\"(?:\\\\.|[^\"\\\\])*\"|'(?:\\\\.|[^'\\\\])*'|\\s+");
+
+    public AliasWrapper(AliasDTO a, Factory factory, String klass, String path, SourcePosition position) {
         name = a.getName();
         expression = new Predicate(a.getExpression());
+        definition = a.getRef() == null ? expression.getExpression().toDisplayString() : oneLine(a.getRef());
+        this.position = position;
         varTypes = new ArrayList<>();
         varNames = a.getVarNames();
         for (String s : a.getVarTypes()) {
@@ -37,6 +47,22 @@ public List<String> getVarNames() {
         return varNames;
     }
 
+    // Collapses each run of whitespace into one space, except inside string and char literals
+    private static String oneLine(String definition) {
+        return LITERAL_OR_SPACES.matcher(definition.strip())
+                .replaceAll(m -> m.group().isBlank() ? " " : Matcher.quoteReplacement(m.group()));
+    }
+
+    /** The definition as written in the declaration, on one line */
+    public String getDefinition() {
+        return definition;
+    }
+
+    /** Position of the alias declaration */
+    public SourcePosition getPosition() {
+        return position;
+    }
+
     public Predicate getClonedPredicate() {
         return expression.clone();
     }

liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java

@@ -65,4 +65,9 @@ public List<String> getVarNames() {
     public Expression getExpression() {
         return expression;
     }
+
+    /** The definition as written in the alias declaration, or null when built from an expression */
+    public String getRef() {
+        return ref;
+    }
 }

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

@@ -339,7 +339,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
                     throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression",
                             ref);
                 }
-                AliasWrapper aw = new AliasWrapper(a, factory, klass, path);
+                AliasWrapper aw = new AliasWrapper(a, factory, klass, path, position);
                 context.addAlias(aw);
             }
         } catch (LJError e) {

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

@@ -85,7 +85,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         if (result.isError()) {
             throw new RefinementError(element.getPosition(), declarationPosition, expectedType,
                     implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map,
-                    result.getCounterexample(), customMessage);
+                    result.getCounterexample(), customMessage, context.getAliases());
         }
     }
 
@@ -445,7 +445,8 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl
         TranslationTable map = new TranslationTable();
         VCImplication premises = buildPremiseChain(map, expected, found);
         throw new RefinementError(position, declarationPosition, expected,
-                premises.simplify(NeededVariables.forRefinementError(expected)), map, counterexample, customMessage);
+                premises.simplify(NeededVariables.forRefinementError(expected)), map, counterexample, customMessage,
+                context.getAliases());
     }
 
     /** What a state refinement error shows as found: what is known about the variables of both predicates */

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

@@ -0,0 +1,53 @@
+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.AliasExpansion;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.errors.RefinementError;
+
+class TestAliasExpansions {
+
+    private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/";
+
+    @Test
+    void foundAndExpectedRecordTheirSubstitutedAliases() {
+        RefinementError error = verify("ErrorAlias.java");
+        assertExpansion(error.getFoundAliases(), "InRange(j, 10, 16)", "10 < j && j < 16");
+        assertExpansion(error.getExpectedAliases(), "InRange(j, 10, 15)", "10 < j && j < 15");
+        AliasExpansion expected = error.getExpectedAliases().get(0);
+        assertEquals("InRange", expected.alias());
+        assertEquals(List.of("val", "low", "up"), expected.parameters());
+        assertEquals(7, expected.declarationPosition().getLine());
+    }
+
+    @Test
+    void messageDeclaresEachAliasOnceAsWritten() {
+        RefinementError error = verify("ErrorStaticFinalInAlias.java");
+        assertEquals(
+                List.of("where Mode(x) = x == ImageWriteParam.MODE_DISABLED || x == ImageWriteParam.MODE_DEFAULT "
+                        + "|| x == ImageWriteParam.MODE_EXPLICIT || x == ImageWriteParam.MODE_COPY_FROM_METADATA"),
+                error.getMessageNotes());
+        assertTrue(error.toString().contains(error.getMessage() + "\n  where Mode(x) = "));
+    }
+
+    private static void assertExpansion(List<AliasExpansion> expansions, String invocation, String expansion) {
+        assertEquals(1, expansions.size());
+        // instance numbers of variables are shown as superscripts
+        assertEquals(invocation, expansions.get(0).invocation().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
+        assertEquals(expansion, expansions.get(0).expansion().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
+    }
+
+    private static RefinementError 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 assertInstanceOf(RefinementError.class, errors.get(0));
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java

@@ -174,7 +174,7 @@ private static RefinementError error(String expected, VCImplication found, Strin
         Counterexample counterexample = new Counterexample(
                 Arrays.stream(assignments).map(a -> a.split("=")).map(parts -> pair(parts[0], parts[1])).toList());
         return new RefinementError(null, null, new Predicate(RefinementsParser.createAST(expected, "")),
-                found.simplify(), new TranslationTable(), counterexample, null);
+                found.simplify(), new TranslationTable(), counterexample, null, List.of());
     }
 
     private static Pair<String, String> pair(String name, String value) {