[CatarinaGamboa]

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

@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:

"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

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main on 91b3dc2 found one issue:

• [P2] Preserve whitespace inside alias string literals (AliasWrapper.java): the definition shown in where lines collapsed every whitespace run, so x == "a b" would print as x == "a b", which is a different predicate from the one checked.

Fixed in the latest commit: whitespace is now collapsed only outside string and char literals. Checked with @RefinementAlias("Pair(int x) { x == 2 && \"a b\" == \"a b\" }"), which now prints where Pair(x) = x == 2 && "a b" == "a b". Full verifier suite: 700 tests, 0 failures.

Declined: none.

[CatarinaGamboa]

Codex review, round 2

codex exec review --base origin/main on 8ae2cf3 found one issue:

• [P2] Deduplicate alias invocations by identity, not display text (AliasExpansion.java): invocations were deduplicated by their display string, so two invocations whose arguments differ only in qualifier, e.g. P(a.x) and P(b.x), could both display as P(x) and the second expansion would be dropped.

Fixed in the latest commit: invocations are now keyed by the invocation itself (toString(), which keeps full names). The invocation field still holds the display text. Full verifier suite: 700 tests, 0 failures.

Declined: none.

[CatarinaGamboa]

Codex review, round 3

codex exec review --base origin/main on ff6ee0b found no actionable issues, and the targeted alias-expansion and refinement-error tests pass. Review loop closed.