From 808256c04d1c393c4140b408328feedfaac09495 Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <catarina.vg@hotmail.com>
Date: Wed, 11 Nov 2026 21:26:57 +0000
Subject: [PATCH 1/2] Explain the verifier's generated names on hover and link
 them to their lines

Names the verifier gives values of the code, such as #if_condition,
#getUndoManager_result or #case_condition@74, now say on hover what they
stand for in plain words, with the line when it is known, and go to that
line on click. This applies in Expected, the Found steps and their diff,
the counterexample and the Context tab's refinements.

The error's translation table already has a position for each of these
names, keyed by the name as shown. For the Context tab, the server now
sends where each generated value comes from (generatedPlaces).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 client/src/types/context.ts                   |  3 +-
 client/src/webview/generated-names.ts         | 73 +++++++++++++++++++
 client/src/webview/highlighting.ts            | 60 ++++++++++++---
 client/src/webview/script.spec.ts             |  1 +
 client/src/webview/styles.ts                  | 12 +++
 .../src/webview/views/context/context.spec.ts | 17 ++++-
 client/src/webview/views/context/context.ts   |  2 +-
 client/src/webview/views/context/variables.ts |  9 ++-
 .../views/diagnostics/counterexample.ts       |  6 +-
 .../src/webview/views/diagnostics/errors.ts   |  6 +-
 .../views/diagnostics/vc-changes.spec.ts      | 24 ++++++
 .../webview/views/diagnostics/vc-changes.ts   | 38 ++++++----
 .../java/dtos/context/ContextHistoryDTO.java  |  5 +-
 .../java/utils/ContextHistoryConverter.java   | 14 +++-
 .../utils/ContextHistoryConverterTest.java    |  8 ++
 15 files changed, 238 insertions(+), 40 deletions(-)
 create mode 100644 client/src/webview/generated-names.ts

diff --git a/client/src/types/context.ts b/client/src/types/context.ts
index 90ec9d7..174fcd2 100644
--- a/client/src/types/context.ts
+++ b/client/src/types/context.ts
@@ -1,4 +1,4 @@
-import { SourcePosition } from "./diagnostics";
+import { SourcePosition, TranslationTable } from "./diagnostics";
 
 // Type definitions used for LiquidJava context information
 
@@ -54,6 +54,7 @@ export type LJContext = {
   visibleVars: LJVariable[]; // variables visible in the current selection
   allVars: LJVariable[]; // instance vars + global vars + vars in scope
   fileScopes: Record<string, Range[]>; // file -> scopes
+  generatedPlaces: TranslationTable; // where each value the verifier introduces, such as #if_condition, comes from
 }
 
 export type Range = {
diff --git a/client/src/webview/generated-names.ts b/client/src/webview/generated-names.ts
new file mode 100644
index 0000000..890d3ed
--- /dev/null
+++ b/client/src/webview/generated-names.ts
@@ -0,0 +1,73 @@
+import type { PlacementInCode, SourcePosition } from "../types/diagnostics";
+import { escapeHtml } from "./utils";
+
+// what a value the verifier names stands for, given where it is (" at line 12", or empty when unknown)
+type Description = (at: string) => string;
+
+const NAMED_VALUES = new Map<string, Description>(Object.entries({
+    if_condition: at => `the condition of the if${at}`,
+    loop_condition: at => `the condition of the loop${at}`,
+    ternary_condition: at => `the condition of the ? :${at}`,
+    switch_selector: at => `the value the switch${at} checks`,
+    case_condition: at => `whether the case${at} matches`,
+    try_branch: at => `whether the try block${at} runs to its end, rather than a catch block`,
+    catch_branch: at => `whether this catch block of the try${at} runs, rather than a later one`,
+    array_length: at => `the length of the array created${at}`,
+    operation_result: at => `the result of the operation${at}`,
+    expression_value: at => `the value of the expression${at}`,
+} satisfies Record<string, Description>));
+
+// values named after the code they come from: a call, a new object or a field read
+const VALUES_OF_CODE: [RegExp, (code: string) => Description][] = [
+    [/^new_(\w+)$/, type => at => `the new ${type} object created${at}`],
+    [/^(\w+)_result$/, method => at => `the value returned by the call to ${method}()${at}`],
+    [/^(\w+)_value$/, field => at => `the value of the field ${field} read${at}`],
+];
+
+function describe(name: string): Description | undefined {
+    const kind = name.slice(1);
+    if (!name.startsWith("#") || !kind) return undefined;
+    const named = NAMED_VALUES.get(kind);
+    if (named) return named;
+    for (const [pattern, describeCode] of VALUES_OF_CODE) {
+        const code = pattern.exec(kind)?.[1];
+        if (code) return describeCode(code);
+    }
+    return undefined;
+}
+
+/** Whether a name, written without its line tag, is one the verifier gives a value of the code, such as #if_condition */
+export function isGeneratedName(name: string): boolean {
+    return describe(name) !== undefined;
+}
+
+// says in plain words what a value the verifier names stands for, such as "The condition of the if at line 12"
+function explain(name: string, line?: number): string {
+    const description = describe(name)?.(line === undefined ? "" : ` at line ${line}`) ?? "";
+    return `${description.charAt(0).toUpperCase()}${description.slice(1)}. LiquidJava gives it the name ${name}.`;
+}
+
+/**
+ * The hover text of a name the verifier gives a value of the code: what the value is, and where when it is known
+ * @param name the name without its line tag
+ * @param position where the value comes from, if known; it is a link when it has a file
+ * @param tagLine the line of the name's line tag, used when the position is not known
+ */
+export function generatedNameTitle(name: string, position?: SourcePosition | null, tagLine?: number): string {
+    const explanation = explain(name, position ? position.lineStart + 1 : tagLine);
+    return position?.file ? `${explanation} Click to go to it.` : explanation;
+}
+
+/**
+ * Renders a name the verifier gives a value of the code, explained on hover and, when its place is known, a link to it
+ * @param name the name without its line tag
+ * @param content the name as rendered, with its line tag
+ * @param tagLine the line of its line tag, if it has one
+ * @param place where the value comes from, if known
+ */
+export function renderGeneratedName(name: string, content: string, tagLine?: number, place?: PlacementInCode): string {
+    const position = place?.position;
+    const title = escapeHtml(generatedNameTitle(name, position, tagLine));
+    if (!position?.file) return `<span class="lj-generated-name" title="${title}">${content}</span>`;
+    return /*html*/`<span class="lj-generated-name location-link" title="${title}" data-file="${escapeHtml(position.file)}" data-line="${position.lineStart}" data-column="${position.colStart}">${content}</span>`;
+}
diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts
index 4c46924..ce9d03a 100644
--- a/client/src/webview/highlighting.ts
+++ b/client/src/webview/highlighting.ts
@@ -1,4 +1,6 @@
 import * as liquidJavaGrammar from "../../syntaxes/liquidjava.json";
+import type { TranslationTable } from "../types/diagnostics";
+import { isGeneratedName, renderGeneratedName } from "./generated-names";
 import { escapeHtml } from "./utils";
 
 type GrammarPattern = {
@@ -22,6 +24,8 @@ type ScopeColorRule = {
 // numbered when values share a line or have none, x@12#2 and x#2
 export const LINE_TAG = "@\\d+(?:#\\d+)?\\b|(?<=[\\w)])#\\d+\\b";
 const LINE_TAG_SCOPE = "line-tag";
+const VARIABLE_SCOPE = "variable.other.liquidjava";
+const LINE_TAG_AT_INDEX = new RegExp(LINE_TAG, "y");
 // string and character literals, whose text is shown as it is even where it looks like a line tag
 export const LITERAL = `"(?:\\\\.|[^"\\\\])*"|'(?:\\\\.|[^'\\\\])*'`;
 const LINE_TAGS_OUTSIDE_LITERALS = new RegExp(`${LITERAL}|${LINE_TAG}`, "g");
@@ -44,7 +48,7 @@ const expressionPatterns: GrammarPattern[] = [
     { match: "\\bnull\\b", name: "constant.language.null.liquidjava.webview" },
     ...patterns("literals"),
     { match: "[(){}.,;\\[\\]]", name: "punctuation.separator.liquidjava" },
-    { match: "#*[a-zA-Z_](?:[a-zA-Z0-9_]|#(?!\\d))*", name: "variable.other.liquidjava" }
+    { match: "#*[a-zA-Z_](?:[a-zA-Z0-9_]|#(?!\\d))*", name: VARIABLE_SCOPE }
 ];
 
 const highlightRules: HighlightRule[] = expressionPatterns
@@ -122,7 +126,28 @@ export function withoutLineTag(name: string): string {
     return name.replace(new RegExp(`(?:${LINE_TAG})$`), "");
 }
 
-function renderHighlightedContent(expression: string): string {
+function renderToken(content: string, scope: string): string {
+    return `<span style="color:${colorForScope(scope)}">${escapeHtml(content)}</span>`;
+}
+
+/**
+ * Renders a name the verifier gives a value of the code, with the line tag after it if any
+ * @returns the html and the length of the text it renders
+ */
+function renderGeneratedNameAt(expression: string, index: number, name: string, places?: TranslationTable): [string, number] {
+    LINE_TAG_AT_INDEX.lastIndex = index + name.length;
+    const tag = LINE_TAG_AT_INDEX.exec(expression)?.[0] ?? "";
+    const tagLine = /^@(\d+)/.exec(tag)?.[1];
+    const content = renderToken(name, VARIABLE_SCOPE) + (tag ? renderLineTag(tag, name) : "");
+    const html = renderGeneratedName(name, content, tagLine ? Number(tagLine) : undefined, places?.[name + tag]);
+    return [html, name.length + tag.length];
+}
+
+/**
+ * Renders an expression with its tokens colored
+ * @param places where the variables of the expression come from, by name, such as the translation table of an error
+ */
+function renderHighlightedContent(expression: string, places?: TranslationTable): string {
     let html = "";
     let index = 0;
 
@@ -140,25 +165,31 @@ function renderHighlightedContent(expression: string): string {
         const match = matchingRule.regex.exec(expression);
         const content = match?.[0] || expression[index] || "";
 
+        if (matchingRule.scope === VARIABLE_SCOPE && isGeneratedName(content)) {
+            const [generated, length] = renderGeneratedNameAt(expression, index, content, places);
+            html += generated;
+            index += length;
+            continue;
+        }
         html += matchingRule.scope === LINE_TAG_SCOPE
             ? renderLineTag(content, variableBefore(expression, index))
-            : `<span style="color:${colorForScope(matchingRule.scope)}">${escapeHtml(content)}</span>`;
+            : renderToken(content, matchingRule.scope);
         index += content.length;
     }
     return html;
 }
 
-function renderExpression(expression: string, wrap: boolean): string {
+function renderExpression(expression: string, wrap: boolean, places?: TranslationTable): string {
     if (!expression) return "";
 
-    const content = renderHighlightedContent(expression);
+    const content = renderHighlightedContent(expression, places);
     return wrap
         ? `<pre class="lj-expression-block"><code class="lj-expression-code">${content}</code></pre>`
         : content;
 }
 
-export function renderHighlightedExpression(expression: string): string {
-    return renderExpression(expression, true);
+export function renderHighlightedExpression(expression: string, places?: TranslationTable): string {
+    return renderExpression(expression, true, places);
 }
 
 const WEAKER_THAN_AND = ["||", "-->", "?"];
@@ -239,7 +270,7 @@ export function getExpressionLines(expression: string): ExpressionLine[] {
  */
 export function renderExpressionLines(
     lines: ExpressionLine[],
-    renderText: (text: string, index: number) => string = renderHighlightedContent,
+    renderText: (text: string, index: number) => string = text => renderHighlightedContent(text),
     trailing = "",
 ): string {
     return lines.map((line, index) => {
@@ -250,14 +281,19 @@ export function renderExpressionLines(
 
 /**
  * Renders an expression on the lines of getExpressionLines, in an expression block as renderHighlightedExpression does
+ * @param places where the variables of the expression come from, by name
  */
-export function renderHighlightedLines(expression: string): string {
+export function renderHighlightedLines(expression: string, places?: TranslationTable): string {
     if (!expression) return "";
 
-    const html = renderExpressionLines(getExpressionLines(expression));
+    const html = renderExpressionLines(getExpressionLines(expression), text => renderHighlightedContent(text, places));
     return `<pre class="lj-expression-block"><code class="lj-expression-code">${html}</code></pre>`;
 }
 
-export function renderHighlightedInlineExpression(expression: string): string {
-    return renderExpression(expression, false);
+/**
+ * Renders an expression inline, with its tokens colored
+ * @param places where the variables of the expression come from, by name
+ */
+export function renderHighlightedInlineExpression(expression: string, places?: TranslationTable): string {
+    return renderExpression(expression, false, places);
 }
diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts
index 97ba956..247ee76 100644
--- a/client/src/webview/script.spec.ts
+++ b/client/src/webview/script.spec.ts
@@ -47,6 +47,7 @@ function context(file = currentFile): LJContext {
         visibleVars: [variable],
         allVars: [variable],
         fileScopes: {},
+        generatedPlaces: {},
     };
 }
 
diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
index 5c1e47d..88ddb27 100644
--- a/client/src/webview/styles.ts
+++ b/client/src/webview/styles.ts
@@ -399,6 +399,18 @@ export function getStyles(): string {
             color: var(--vscode-descriptionForeground);
             cursor: help;
         }
+        /* a name LiquidJava gives a value of the code, explained on hover */
+        .lj-generated-name {
+            text-decoration: underline dotted var(--vscode-descriptionForeground);
+            text-underline-offset: 2px;
+            cursor: help;
+        }
+        .lj-generated-name.location-link {
+            cursor: pointer;
+        }
+        .lj-generated-name.location-link:hover {
+            text-decoration-style: solid;
+        }
         .lj-expression,
         .lj-expression-code {
             font-family: var(--vscode-editor-font-family);
diff --git a/client/src/webview/views/context/context.spec.ts b/client/src/webview/views/context/context.spec.ts
index a0546bb..56def08 100644
--- a/client/src/webview/views/context/context.spec.ts
+++ b/client/src/webview/views/context/context.spec.ts
@@ -15,7 +15,7 @@ function ghost(name: string, file = currentFile, stateSet: string | null = null)
 function context(overrides: Partial<LJContext> = {}): LJContext {
     return {
         localVars: [], globalVars: [], ghosts: [], aliases: [], methods: [],
-        visibleVars: [], allVars: [], fileScopes: {}, ...overrides,
+        visibleVars: [], allVars: [], fileScopes: {}, generatedPlaces: {}, ...overrides,
     };
 }
 
@@ -50,6 +50,21 @@ describe('context view', () => {
         expect(document.querySelectorAll('.context-section-content.collapsed')).toHaveLength(0);
     });
 
+    it('links the names LiquidJava gives values of the code in refinements to their lines', () => {
+        document.body.innerHTML = renderContextView(context({
+            allVars: [{
+                name: 'a', displayName: 'a', internalName: 'a', type: 'int', refinement: 'a == #pos_result',
+                mainRefinement: '', position: null, annotationPosition: null,
+            }],
+            generatedPlaces: { '#pos_result': { text: 'pos(x)', position: { file: '/w/A.java', lineStart: 6, colStart: 16, lineEnd: 6, colEnd: 22 } } },
+        }), currentFile, sectionState);
+
+        const name = document.querySelector('#context-vars .lj-generated-name.location-link');
+        expect(name?.getAttribute('title')).toBe(
+            'The value returned by the call to pos() at line 7. LiquidJava gives it the name #pos_result. Click to go to it.');
+        expect([name?.getAttribute('data-file'), name?.getAttribute('data-line')]).toEqual(['/w/A.java', '6']);
+    });
+
     it('honors each section collapse state independently', () => {
         document.body.innerHTML = renderContextView(context({ ghosts: [ghost('size')] }), currentFile, {
             aliases: false, ghosts: true, vars: false,
diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts
index 421de3b..4696f91 100644
--- a/client/src/webview/views/context/context.ts
+++ b/client/src/webview/views/context/context.ts
@@ -23,7 +23,7 @@ export function renderContextView(context: LJContext | undefined, currentFile: s
                 ? 'No context information available at the cursor position'
                 : `${renderContextAliases(aliases, sectionState.aliases)}
                    ${renderContextGhosts(ghosts, sectionState.ghosts)}
-                   ${renderContextVariables(allVars, sectionState.vars, errorAtCursor)}
+                   ${renderContextVariables(allVars, sectionState.vars, errorAtCursor, context?.generatedPlaces)}
             `}
         </div>
     `;
diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts
index 75d4817..353d36b 100644
--- a/client/src/webview/views/context/variables.ts
+++ b/client/src/webview/views/context/variables.ts
@@ -1,10 +1,13 @@
 import { LJVariable } from "../../../types/context";
-import { RefinementMismatchError } from "../../../types/diagnostics";
+import { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics";
 import { renderHighlightedInlineExpression, withoutLineTag } from "../../highlighting";
 import { escapeHtml, getSimpleName } from "../../utils";
 import { renderToggleSection, renderVariableHighlightButton, renderDiagnosticRevealButton } from "../sections";
 
-export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string {
+/**
+ * @param generatedPlaces where each value the verifier introduces comes from, by name
+ */
+export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError, generatedPlaces?: TranslationTable): string {
     const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {}).map(withoutLineTag));
     return /*html*/`
         <div class="context-section">
@@ -28,7 +31,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool
                                 return /*html*/`
                                 <tr class="${isRelevant ? 'context-variable-relevant' : ''}">
                                     <td>${renderVariableHighlightButton(variable)}</td>
-                                    <td><code>${renderHighlightedInlineExpression(variable.refinement)}</code></td>
+                                    <td><code>${renderHighlightedInlineExpression(variable.refinement, generatedPlaces)}</code></td>
                                 </tr>
                             `;}).join('')}
                             ${errorAtCursor ? renderFailingRefinement(errorAtCursor) : ''}
diff --git a/client/src/webview/views/diagnostics/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts
index 904d14f..3e3e2a7 100644
--- a/client/src/webview/views/diagnostics/counterexample.ts
+++ b/client/src/webview/views/diagnostics/counterexample.ts
@@ -1,7 +1,7 @@
-import type { Counterexample } from "../../../types/diagnostics";
+import type { Counterexample, TranslationTable } from "../../../types/diagnostics";
 import { renderHighlightedInlineExpression } from "../../highlighting";
 
-export function renderCounterexample(counterexample: Counterexample): string {
+export function renderCounterexample(counterexample: Counterexample, translationTable?: TranslationTable): string {
     if (counterexample.assignments.length === 0) return "";
 
     return /*html*/`
@@ -10,7 +10,7 @@ export function renderCounterexample(counterexample: Counterexample): string {
                 ${counterexample.assignments.map(assignment => /*html*/`
                     <div class="counterexample-line">
                         <span class="vc-node">${renderHighlightedInlineExpression(
-                            `${assignment.variable} == ${assignment.value}`
+                            `${assignment.variable} == ${assignment.value}`, translationTable
                         )}</span>
                     </div>
                 `).join("")}
diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts
index 2e423f6..93a1a1f 100644
--- a/client/src/webview/views/diagnostics/errors.ts
+++ b/client/src/webview/views/diagnostics/errors.ts
@@ -39,14 +39,14 @@ type ErrorRendererMap = { [E in LJError as E['type']]: (error: E) => string };
 
 const errorContentRenderers: ErrorRendererMap = {
     'refinement-error': (e: RefinementError) => /*html*/ `
-        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected, e.translationTable))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
         ${e.counterexample.assignments.length > 0
-            ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample))
+            ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample, e.translationTable))
             : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/ `
-        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected, e.translationTable))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
     `,
     'invalid-refinement-error': (e: InvalidRefinementError) => /*html*/ `
diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts
index 14a2d0c..08b500b 100644
--- a/client/src/webview/views/diagnostics/vc-changes.spec.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts
@@ -69,6 +69,30 @@ describe('verification implications', () => {
         expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.innerHTML))
             .toEqual([expect.stringMatching(/^<span [^>]*>x<\/span><sub [^>]*>l13<\/sub>$/)]);
     });
+    it('explains the names LiquidJava gives values of the code, linking each to its line when it is known', () => {
+        const at = (lineStart: number) => ({ text: '', position: { file: '/w/A.java', lineStart, colStart: 4, lineEnd: lineStart, colEnd: 9 } });
+        const table = { '#if_condition': at(9), '#size_result': at(14) };
+        const chain: VCImplication = {
+            name: '#if_condition', type: 'boolean', predicate: 'x > 0',
+            next: { ...conclusion, predicate: 'a == #size_result + #new_File + #case_condition@20#1 + #ret' },
+        };
+        const names = () => Array.from(document.querySelectorAll('.lj-generated-name'), name =>
+            [name.textContent, name.getAttribute('title'), name.getAttribute('data-line')]);
+
+        document.body.innerHTML = renderImplication(chain, table);
+        expect(document.querySelector('.vc-binder')?.getAttribute('title')).toBe(
+            'The condition of the if at line 10. LiquidJava gives it the name #if_condition. Click to go to it.');
+        expect(names()).toEqual([
+            ['#size_result', 'The value returned by the call to size() at line 15. LiquidJava gives it the name #size_result. Click to go to it.', '14'],
+            ['#new_File', 'The new File object created. LiquidJava gives it the name #new_File.', null],
+            ['#case_conditionl20#1', 'Whether the case at line 20 matches. LiquidJava gives it the name #case_condition.', null],
+        ]);
+
+        document.body.innerHTML = renderImplicationChange(
+            { ...conclusion, predicate: 'a == x + y + z' }, { ...conclusion, predicate: 'a == x + y + #size_result' }, table,
+        );
+        expect(document.querySelector('.vc-change-fragment .lj-generated-name')?.getAttribute('data-line')).toBe('14');
+    });
     it.each([
         ['initial rendering', () => renderImplication({ ...implication, next: null })],
         ['simplification change', () => renderImplicationChange(implication, { ...implication, next: null })],
diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts
index a3ec82e..448b56c 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -2,9 +2,11 @@ import type { VCImplication } from "../../../types/vc-implications";
 import type { TranslationTable } from "../../../types/diagnostics";
 import {
     getExpressionLines, LINE_TAG, LITERAL, renderExpressionLines, renderHighlightedInlineExpression, renderLineTags,
+    withoutLineTag,
 } from "../../highlighting";
 import { escapeHtml } from "../../utils";
 import { renderSourceHighlightButton } from "../sections";
+import { generatedNameTitle, isGeneratedName } from "../../generated-names";
 
 type ChangeKind = "unchanged" | "removed" | "added";
 type DiffOperation<T> = { kind: ChangeKind; value: T };
@@ -41,13 +43,16 @@ function getImplicationLines(node: VCImplication): string[] {
 
 function renderBinder(binder: string, type: string, translationTable?: TranslationTable): string {
     const placement = translationTable?.[binder.slice(1)];
-    if (!placement?.position?.file) {
-        return `<span class="vc-node vc-binder" title="${escapeHtml(type)}">${renderLineTags(binder)}</span>`;
+    const position = placement?.position;
+    const name = withoutLineTag(binder.slice(1));
+    const explanation = isGeneratedName(name) ? generatedNameTitle(name, position) : "";
+    if (!position?.file) {
+        return `<span class="vc-node vc-binder" title="${escapeHtml(explanation || type)}">${renderLineTags(binder)}</span>`;
     }
     return renderSourceHighlightButton(
         renderLineTags(binder),
-        type ? `Go to source (${type})` : "Go to source",
-        placement.position,
+        explanation || (type ? `Go to source (${type})` : "Go to source"),
+        position,
         "vc-node vc-binder clickable",
     );
 }
@@ -63,11 +68,12 @@ export function renderVCLine(
     translationTable?: TranslationTable,
 ): string {
     const { binder, type, predicate, hasNext } = parseImplicationLine(line);
+    const renderPredicateLine = renderText ?? (text => renderHighlightedInlineExpression(text, translationTable));
     const arrow = hasNext ? ' <span class="vc-arrow">→</span>' : "";
     return /*html*/`
         <div class="vc-line ${className}">
             ${binder ? /*html*/`<div class="vc-binder-cell">${renderBinder(binder, type, translationTable)}</div>` : ""}
-            <div class="vc-predicate-cell"><span class="vc-node">${renderExpressionLines(getExpressionLines(predicate), renderText, arrow)}</span></div>
+            <div class="vc-predicate-cell"><span class="vc-node">${renderExpressionLines(getExpressionLines(predicate), renderPredicateLine, arrow)}</span></div>
         </div>
     `;
 }
@@ -112,11 +118,15 @@ function tokenizeExpression(expression: string): string[] {
     return expression.match(TOKEN_PATTERN) || [];
 }
 
-function renderChangedFragment(content: string): string {
-    return `<span class="vc-change-fragment">${renderHighlightedInlineExpression(content)}</span>`;
+function renderChangedFragment(content: string, translationTable?: TranslationTable): string {
+    return `<span class="vc-change-fragment">${renderHighlightedInlineExpression(content, translationTable)}</span>`;
 }
 
-function renderDestinationTokenDiff(before: string, after: string): { content: string; hasAddedContent: boolean } {
+function renderDestinationTokenDiff(
+    before: string,
+    after: string,
+    translationTable?: TranslationTable,
+): { content: string; hasAddedContent: boolean } {
     const operations = diffSequence(tokenizeExpression(before), tokenizeExpression(after));
     let html = "";
     let changedContent = "";
@@ -126,7 +136,7 @@ function renderDestinationTokenDiff(before: string, after: string): { content: s
         if (!changedContent) return;
         const trailingWhitespace = changedContent.match(/\s+$/u)?.[0] ?? "";
         const content = changedContent.slice(0, changedContent.length - trailingWhitespace.length);
-        if (content) html += renderChangedFragment(content);
+        if (content) html += renderChangedFragment(content, translationTable);
         html += trailingWhitespace;
         changedContent = "";
     };
@@ -143,7 +153,7 @@ function renderDestinationTokenDiff(before: string, after: string): { content: s
                 return;
             }
             flushChangedContent();
-            html += renderHighlightedInlineExpression(operation.value);
+            html += renderHighlightedInlineExpression(operation.value, translationTable);
         }
     });
     flushChangedContent();
@@ -197,14 +207,14 @@ function alignChangedLines(removed: string[], added: string[]): Array<[string |
 }
 
 // each line of a changed predicate, diffed against the line of the old predicate it replaces, or all marked if none
-function renderChangedPredicateLines(before: string, after: string): string[] {
+function renderChangedPredicateLines(before: string, after: string, translationTable?: TranslationTable): string[] {
     const lines = (predicate: string) => getExpressionLines(predicate).map(line => line.text);
     return alignChangedLines(lines(before), lines(after))
         .flatMap(([beforeLine, afterLine]) => {
             if (afterLine === undefined) return [];
             return [beforeLine === undefined
-                ? renderChangedFragment(afterLine)
-                : renderDestinationTokenDiff(beforeLine, afterLine).content];
+                ? renderChangedFragment(afterLine, translationTable)
+                : renderDestinationTokenDiff(beforeLine, afterLine, translationTable).content];
         });
 }
 
@@ -222,7 +232,7 @@ function renderChangedDestinationLines(
             const beforePredicate = parseImplicationLine(before).predicate;
             const afterPredicate = parseImplicationLine(after).predicate;
             const change = renderDestinationTokenDiff(beforePredicate, afterPredicate);
-            const lines = renderChangedPredicateLines(beforePredicate, afterPredicate);
+            const lines = renderChangedPredicateLines(beforePredicate, afterPredicate, translationTable);
             return renderVCLine(
                 after,
                 change.hasAddedContent ? "" : "vc-change-line",
diff --git a/server/src/main/java/dtos/context/ContextHistoryDTO.java b/server/src/main/java/dtos/context/ContextHistoryDTO.java
index 19debbd..3327b7a 100644
--- a/server/src/main/java/dtos/context/ContextHistoryDTO.java
+++ b/server/src/main/java/dtos/context/ContextHistoryDTO.java
@@ -3,6 +3,7 @@
 import java.util.List;
 import java.util.Map;
 
+import dtos.diagnostics.PlacementInCodeDTO;
 import dtos.diagnostics.SourcePositionDTO;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -15,7 +16,9 @@ public record ContextHistoryDTO(
     List<GhostDTO> ghosts,
     List<AliasDTO> aliases,
     List<MethodDTO> methods,
-    Map<String, List<SourcePositionDTO>> fileScopes
+    Map<String, List<SourcePositionDTO>> fileScopes,
+    // where each value the verifier introduces, such as #if_condition, comes from, by the name the context shows it with
+    Map<String, PlacementInCodeDTO> generatedPlaces
 ) {
     public static String stringifyType(CtTypeReference<?> typeReference) {
         if (typeReference == null)
diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java
index 1685aba..e65ad19 100644
--- a/server/src/main/java/utils/ContextHistoryConverter.java
+++ b/server/src/main/java/utils/ContextHistoryConverter.java
@@ -6,6 +6,7 @@
 import java.util.Map;
 import java.util.Set;
 import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
 import dtos.context.AliasDTO;
 import dtos.context.ContextDisplay;
@@ -13,6 +14,7 @@
 import dtos.context.MethodDTO;
 import dtos.context.GhostDTO;
 import dtos.context.VariableDTO;
+import dtos.diagnostics.PlacementInCodeDTO;
 import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.processor.context.ContextHistory;
 import liquidjava.processor.context.GhostFunction;
@@ -47,7 +49,8 @@ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) {
             contextHistory.getGhosts().stream().sorted(GHOST_ORDER).map(GhostDTO::from).collect(Collectors.toList()),
             contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()),
             contextHistory.getMethods().stream().map(MethodDTO::from).filter(f -> f != null).collect(Collectors.toList()),
-            parseFileScopes(contextHistory.getFileScopes())
+            parseFileScopes(contextHistory.getFileScopes()),
+            convertGeneratedPlaces(contextHistory, display)
         );
     }
 
@@ -72,6 +75,15 @@ private static List<VariableDTO> convertVariables(Set<RefinedVariable> variables
             .collect(Collectors.toList());
     }
 
+    // where each value the verifier introduces comes from, by the name the context shows it with
+    private static Map<String, PlacementInCodeDTO> convertGeneratedPlaces(ContextHistory history, ContextDisplay display) {
+        Map<String, PlacementInCodeDTO> places = new HashMap<>();
+        Stream.concat(history.getLocalVars().stream(), history.getGlobalVars().stream())
+            .filter(v -> GeneratedNames.isGenerated(v.getName()) && v.getPlacementInCode() != null)
+            .forEach(v -> places.put(display.name(v.getName()), PlacementInCodeDTO.from(v.getPlacementInCode())));
+        return places;
+    }
+
     private static Map<String, List<SourcePositionDTO>> parseFileScopes(Map<String, Set<String>> fileScopes) {
         return fileScopes.entrySet().stream().collect(Collectors.toMap(
             Map.Entry::getKey,
diff --git a/server/src/test/java/utils/ContextHistoryConverterTest.java b/server/src/test/java/utils/ContextHistoryConverterTest.java
index b44d55b..f5bf9a6 100644
--- a/server/src/test/java/utils/ContextHistoryConverterTest.java
+++ b/server/src/test/java/utils/ContextHistoryConverterTest.java
@@ -15,6 +15,7 @@
 import dtos.context.ContextHistoryDTO;
 import dtos.context.GhostDTO;
 import dtos.context.VariableDTO;
+import dtos.diagnostics.PlacementInCodeDTO;
 import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.processor.context.ContextHistory;
@@ -88,6 +89,13 @@ void showsVariablesAsErrorMessagesDo() {
         assertTrue(variables.stream().noneMatch(v -> v.displayName().startsWith("#")), refinements.toString());
     }
 
+    @Test
+    void sendsWhereTheValuesTheVerifierIntroducesComeFrom() {
+        PlacementInCodeDTO length = verify(DOOR).generatedPlaces().get("#array_length");
+        assertEquals("2", length.text());
+        assertEquals(13, length.position().lineStart()); // new int[2], from line zero
+    }
+
     @Test
     void showsTheStatesOfANamedSetAsValuesOfTheSet() {
         List<GhostDTO> ghosts = verify(DOOR).ghosts();

From 1e96c37baaa4602a9c373738d9154e2677962c2d Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <catarina.vg@hotmail.com>
Date: Wed, 11 Nov 2026 21:28:33 +0000
Subject: [PATCH 2/2] Use the line tag of a generated binder when its position
 is not known

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 client/src/webview/highlighting.ts                      | 9 +++++++--
 client/src/webview/views/diagnostics/vc-changes.spec.ts | 4 ++++
 client/src/webview/views/diagnostics/vc-changes.ts      | 4 ++--
 3 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts
index ce9d03a..c89bfd4 100644
--- a/client/src/webview/highlighting.ts
+++ b/client/src/webview/highlighting.ts
@@ -121,6 +121,12 @@ export function renderLineTags(text: string): string {
     return html + escapeHtml(text.slice(index));
 }
 
+/** The line of the line tag a name ends with, x@12 or x@12#2, if it has one */
+export function lineOfTag(name: string): number | undefined {
+    const line = /@(\d+)(?:#\d+)?$/.exec(name)?.[1];
+    return line === undefined ? undefined : Number(line);
+}
+
 /** The name of a variable without its line tag, as it is written in code */
 export function withoutLineTag(name: string): string {
     return name.replace(new RegExp(`(?:${LINE_TAG})$`), "");
@@ -137,9 +143,8 @@ function renderToken(content: string, scope: string): string {
 function renderGeneratedNameAt(expression: string, index: number, name: string, places?: TranslationTable): [string, number] {
     LINE_TAG_AT_INDEX.lastIndex = index + name.length;
     const tag = LINE_TAG_AT_INDEX.exec(expression)?.[0] ?? "";
-    const tagLine = /^@(\d+)/.exec(tag)?.[1];
     const content = renderToken(name, VARIABLE_SCOPE) + (tag ? renderLineTag(tag, name) : "");
-    const html = renderGeneratedName(name, content, tagLine ? Number(tagLine) : undefined, places?.[name + tag]);
+    const html = renderGeneratedName(name, content, lineOfTag(tag), places?.[name + tag]);
     return [html, name.length + tag.length];
 }
 
diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts
index 08b500b..da1769f 100644
--- a/client/src/webview/views/diagnostics/vc-changes.spec.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts
@@ -88,6 +88,10 @@ describe('verification implications', () => {
             ['#case_conditionl20#1', 'Whether the case at line 20 matches. LiquidJava gives it the name #case_condition.', null],
         ]);
 
+        document.body.innerHTML = renderImplication({ ...chain, name: '#case_condition@74' });
+        expect(document.querySelector('.vc-binder')?.getAttribute('title')).toBe(
+            'Whether the case at line 74 matches. LiquidJava gives it the name #case_condition.');
+
         document.body.innerHTML = renderImplicationChange(
             { ...conclusion, predicate: 'a == x + y + z' }, { ...conclusion, predicate: 'a == x + y + #size_result' }, table,
         );
diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts
index 448b56c..c710958 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -2,7 +2,7 @@ import type { VCImplication } from "../../../types/vc-implications";
 import type { TranslationTable } from "../../../types/diagnostics";
 import {
     getExpressionLines, LINE_TAG, LITERAL, renderExpressionLines, renderHighlightedInlineExpression, renderLineTags,
-    withoutLineTag,
+    lineOfTag, withoutLineTag,
 } from "../../highlighting";
 import { escapeHtml } from "../../utils";
 import { renderSourceHighlightButton } from "../sections";
@@ -45,7 +45,7 @@ function renderBinder(binder: string, type: string, translationTable?: Translati
     const placement = translationTable?.[binder.slice(1)];
     const position = placement?.position;
     const name = withoutLineTag(binder.slice(1));
-    const explanation = isGeneratedName(name) ? generatedNameTitle(name, position) : "";
+    const explanation = isGeneratedName(name) ? generatedNameTitle(name, position, lineOfTag(binder)) : "";
     if (!position?.file) {
         return `<span class="vc-node vc-binder" title="${escapeHtml(explanation || type)}">${renderLineTags(binder)}</span>`;
     }