From 2c41f1e9e593a91d511e1ac35934f73d47e0dd08 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 02:07:59 +0000 Subject: [PATCH 1/9] List Found as facts and show only readable simplification steps Found listed every row of the VC chain with a forall binder column and implication arrows, including rows that state nothing and binders with generated names, and its steps walked through each raw pass. It now lists the facts, one per line; says that nothing known proves Expected when the message could not prove it; and keeps only the steps whose facts use no generated name, one per pass, labelled Original, Simplified or by their display step name, with a tooltip saying what changed. Closes #183 Closes #176 Co-Authored-By: Claude Opus 5.5 --- client/src/webview/styles.ts | 56 +++------ .../views/diagnostics/vc-changes.spec.ts | 40 ------- .../webview/views/diagnostics/vc-changes.ts | 94 ++++----------- .../views/diagnostics/vc-implications.spec.ts | 89 ++++++++++++++ .../views/diagnostics/vc-implications.ts | 113 ++++++++++++++---- 5 files changed, 216 insertions(+), 176 deletions(-) delete mode 100644 client/src/webview/views/diagnostics/vc-changes.spec.ts create mode 100644 client/src/webview/views/diagnostics/vc-implications.spec.ts diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index e682ed1..4ecd621 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -467,46 +467,25 @@ export function getStyles(): string { text-align: right; } .vc-chain { - display: grid; - grid-template-columns: fit-content(40%) minmax(0, 1fr); - row-gap: 0.25rem; - width: 100%; - min-width: 0; - } - .counterexample-container .vc-chain { display: flex; flex-direction: column; gap: 0.25rem; + width: 100%; + min-width: 0; } .counterexample-line { overflow-wrap: anywhere; } .vc-line { - display: contents; - } - .vc-binder-cell, - .vc-predicate-cell { min-width: 0; padding: 0.0625rem 0.25rem; overflow-wrap: anywhere; } - .vc-binder-cell { - min-height: 1.2em; - padding-right: 0.75rem; - color: var(--vscode-descriptionForeground); - white-space: normal; - } - .vc-predicate-cell { - color: var(--vscode-editor-foreground); - } - .vc-arrow { - font-size: 1.5em; - line-height: 0; - vertical-align: middle; + .vc-nothing-known { + margin: 0; + padding: 0.0625rem 0.25rem; color: var(--vscode-descriptionForeground); - } - .vc-predicate-cell:only-child { - grid-column: 1 / -1; + font-family: var(--vscode-font-family); } .vc-node { display: inline; @@ -566,8 +545,16 @@ export function getStyles(): string { animation: none; } } - .vc-binder { + .vc-step-title { + display: inline-flex; + align-items: center; + gap: 0.25rem; + min-width: 0; + } + .vc-step-info { + display: inline-flex; color: var(--vscode-descriptionForeground); + cursor: help; } .vc-step-controls { display: inline-flex; @@ -899,10 +886,6 @@ export function getStyles(): string { .highlight-var-btn.selected { background-color: var(--vscode-button-background); } - .vc-binder.highlight-var-btn { - margin: 0; - padding: 0 0.15rem; - } .highlight-var-btn.clickable { text-decoration-color: var(--vscode-textLink-foreground); text-decoration-thickness: 1.5px; @@ -911,15 +894,6 @@ export function getStyles(): string { .highlight-var-btn.clickable:hover { font-weight: inherit; } - .vc-binder.highlight-var-btn:not(.selected):hover { - background-color: color-mix(in srgb, var(--vscode-button-background) 35%, transparent); - } - .vc-binder.highlight-var-btn.clickable { - text-decoration-color: currentColor; - } - .vc-binder.highlight-var-btn.selected { - color: var(--lj-token-identifier); - } .highlight-var-btn.error, .diagnostic-reveal-btn.error { background-color: color-mix(in srgb, var(--vscode-errorForeground) 80%, transparent); diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts deleted file mode 100644 index 06527fb..0000000 --- a/client/src/webview/views/diagnostics/vc-changes.spec.ts +++ /dev/null @@ -1,40 +0,0 @@ -import { afterEach, describe, expect, it } from 'vitest'; -import type { VCImplication } from '../../../types/vc-implications'; -import { renderImplication, renderImplicationChange } from './vc-changes'; - -const conclusion: VCImplication = { name: null, type: null, predicate: 'x > 0', next: null }; -const implication: VCImplication = { - name: 'x', type: 'int', predicate: 'x == 1', - next: { name: 'y', type: 'int', predicate: 'y == 2', next: conclusion }, -}; - -afterEach(() => { document.body.innerHTML = ''; }); - -describe('verification implications', () => { - it.each([ - ['initial rendering', () => renderImplication(implication)], - ['simplification change', () => renderImplicationChange( - { ...implication, predicate: 'x > 0' }, implication, - )], - ] as const)('adds an implication arrow after each nonterminal predicate during %s', (_label, render) => { - document.body.innerHTML = render(); - - const binders = Array.from(document.querySelectorAll('.vc-binder-cell')); - expect(binders.map(cell => cell.textContent?.trim())).toEqual(['∀x', '∀y']); - expect(binders.map(cell => cell.querySelector('.vc-binder')?.textContent)).toEqual(['∀x', '∀y']); - expect(document.querySelector('.vc-line:last-child')?.textContent?.trim()).toBe('x > 0'); - expect(Array.from(document.querySelectorAll('.vc-predicate-cell')).map(cell => cell.textContent?.trim())) - .toEqual(['x == 1 →', 'y == 2 →', 'x > 0']); - expect(document.querySelectorAll('.vc-predicate-cell > .vc-arrow')).toHaveLength(2); - }); - it.each([ - ['initial rendering', () => renderImplication({ ...implication, next: null })], - ['simplification change', () => renderImplicationChange(implication, { ...implication, next: null })], - ] as const)('omits the arrow on a terminal node with a binder during %s', (_label, render) => { - document.body.innerHTML = render(); - - expect(document.querySelector('.vc-binder')?.textContent).toBe('∀x'); - expect(document.querySelector('.vc-predicate-cell')?.textContent?.trim()).toBe('x == 1'); - expect(document.querySelector('.vc-arrow')).toBeNull(); - }); -}); diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index a5c0d37..42b4995 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -1,8 +1,5 @@ import type { VCImplication } from "../../../types/vc-implications"; -import type { TranslationTable } from "../../../types/diagnostics"; import { renderHighlightedInlineExpression } from "../../highlighting"; -import { escapeHtml } from "../../utils"; -import { renderSourceHighlightButton } from "../sections"; type ChangeKind = "unchanged" | "removed" | "added"; type DiffOperation = { kind: ChangeKind; value: T }; @@ -10,56 +7,23 @@ type DiffOperation = { kind: ChangeKind; value: T }; const MIN_LINE_SIMILARITY = 0.3; const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu; const WHITESPACE_PATTERN = /^\s+$/u; -const VC_LINE_SEPARATOR = "\t"; -function hasBinder(node: VCImplication): boolean { - return typeof node.name === "string" && node.name.length > 0; -} - -function formatImplicationLine(node: VCImplication): string { - const binder = hasBinder(node) ? `∀${node.name}` : ""; - const type = typeof node.type === "string" ? node.type : ""; - return [binder, type, node.predicate, node.next ? "next" : ""].join(VC_LINE_SEPARATOR); -} - -function parseImplicationLine(line: string): { binder: string; type: string; predicate: string; hasNext: boolean } { - const [binder = "", type = "", predicate = "", next = ""] = line.split(VC_LINE_SEPARATOR); - return { binder, type, predicate, hasNext: next === "next" }; -} - -function getImplicationLines(node: VCImplication): string[] { - const lines: string[] = []; +/** + * The facts of a VC chain, one per row, leaving out rows that state nothing. All of them hold, so they are shown + * without the binders and implications of the chain + */ +export function getFacts(node: VCImplication): string[] { + const facts: string[] = []; for (let current: VCImplication | null = node; current; current = current.next) { - if (current.next && !hasBinder(current)) continue; - lines.push(formatImplicationLine(current)); - } - return lines; -} - -function renderBinder(binder: string, type: string, translationTable?: TranslationTable): string { - const placement = translationTable?.[binder.slice(1)]; - if (!placement?.position?.file) { - return `${escapeHtml(binder)}`; + if (current.predicate.trim() !== "true") facts.push(current.predicate); } - return renderSourceHighlightButton( - escapeHtml(binder), - type ? `Go to source (${type})` : "Go to source", - placement.position, - "vc-node vc-binder clickable", - ); + return facts; } -export function renderVCLine( - line: string, - className = "", - predicateContent?: string, - translationTable?: TranslationTable, -): string { - const { binder, type, predicate, hasNext } = parseImplicationLine(line); +function renderFact(fact: string, className = "", content?: string): string { return /*html*/`
- ${binder ? /*html*/`
${renderBinder(binder, type, translationTable)}
` : ""} -
${predicateContent ?? renderHighlightedInlineExpression(predicate)}${hasNext ? ' →' : ""}
+ ${content ?? renderHighlightedInlineExpression(fact)}
`; } @@ -188,48 +152,30 @@ function alignChangedLines(removed: string[], added: string[]): Array<[string | return lines; } -function renderChangedDestinationLines( - removed: string[], - added: string[], - translationTable?: TranslationTable, -): string { +function renderChangedFacts(removed: string[], added: string[]): string { if (added.length === 0) return ""; return alignChangedLines(removed, added) .map(([before, after]) => { if (after === undefined) return ""; - if (before === undefined) return renderVCLine(after, "vc-change-line", undefined, translationTable); - const change = renderDestinationTokenDiff( - parseImplicationLine(before).predicate, - parseImplicationLine(after).predicate, - ); - return renderVCLine( - after, - change.hasAddedContent ? "" : "vc-change-line", - change.content, - translationTable, - ); + if (before === undefined) return renderFact(after, "vc-change-line"); + const change = renderDestinationTokenDiff(before, after); + return renderFact(after, change.hasAddedContent ? "" : "vc-change-line", change.content); }) .join(""); } -export function renderImplication(node: VCImplication, translationTable?: TranslationTable): string { - return getImplicationLines(node) - .map(line => renderVCLine(line, "", undefined, translationTable)) - .join(""); +export function renderFacts(facts: string[]): string { + return facts.map(fact => renderFact(fact)).join(""); } -export function renderImplicationChange( - before: VCImplication, - after: VCImplication, - translationTable?: TranslationTable, -): string { - const operations = diffSequence(getImplicationLines(before), getImplicationLines(after)); +export function renderFactsChange(before: string[], after: string[]): string { + const operations = diffSequence(before, after); let html = ""; const changed = { removed: [] as string[], added: [] as string[] }; const flushChanges = () => { - html += renderChangedDestinationLines(changed.removed, changed.added, translationTable); + html += renderChangedFacts(changed.removed, changed.added); changed.removed.length = 0; changed.added.length = 0; }; @@ -237,7 +183,7 @@ export function renderImplicationChange( for (const operation of operations) { if (operation.kind === "unchanged") { flushChanges(); - html += renderVCLine(operation.value, "", undefined, translationTable); + html += renderFact(operation.value); continue; } changed[operation.kind].push(operation.value); diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts new file mode 100644 index 0000000..b311975 --- /dev/null +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -0,0 +1,89 @@ +import { afterEach, describe, expect, it } from 'vitest'; +import type { RefinementError } from '../../../types/diagnostics'; +import type { VCImplication, VCSimplificationResult } from '../../../types/vc-implications'; +import { handleVCImplicationStepClick, renderVCImplication } from './vc-implications'; + +// a VC chain from its rows, each a binder and its predicate +function chain(...rows: Array<[string, string]>): VCImplication { + return rows.reduceRight( + (next, [name, predicate]) => ({ name, type: 'int', predicate, next }), null, + ) as VCImplication; +} + +// a derivation from its steps, oldest first, each the pass that produced it and its chain +function derivation(...steps: Array<[string | null, VCImplication]>): VCSimplificationResult { + return steps.reduce( + (origin, [simplification, implication]) => ({ implication, origin, simplification }), null, + ) as VCSimplificationResult; +} + +function render(found: VCSimplificationResult, message = 'found ... but expected ...'): void { + const error = { file: 'A.java', position: null, title: 'Refinement Error', message } as unknown as RefinementError; + document.body.innerHTML = renderVCImplication(error, found); +} + +function shown() { + return { + label: document.querySelector('.vc-step-name')?.textContent, + info: document.querySelector('.vc-step-info')?.getAttribute('title'), + position: document.querySelector('.vc-step-position')?.textContent?.trim(), + facts: Array.from(document.querySelectorAll('.vc-line')).map(line => line.textContent?.trim()), + }; +} + +function previous(): void { + handleVCImplicationStepClick(document.querySelector('.vc-step-previous-btn')!); +} + +afterEach(() => { document.body.innerHTML = ''; }); + +describe('Found', () => { + it('lists the facts without binders, implications or rows that state nothing', () => { + const size = 'failures.size() == size(this.failures) && failures.size() >= 0'; + render(derivation( + [null, chain(['this.failures', 'true'], ['failures', 'failures == this.failures'], + ['failures.size()', 'failures.size() == size(failures) && failures.size() >= 0'])], + ['Substitution', chain(['this.failures', 'true'], ['failures.size()', size])], + ['Binder', chain(['failures.size()', size])], + )); + + expect(document.body.textContent).not.toMatch(/[∀→]/u); + expect(shown()).toEqual({ + label: 'Simplified', info: 'Replaced variables with the values they are equal to.', position: '2/2', + facts: [size], + }); + previous(); + expect(shown()).toEqual({ + label: 'Original', info: 'What is known here, before simplifying.', position: '1/2', + facts: ['failures == this.failures', 'failures.size() == size(failures) && failures.size() >= 0'], + }); + }); + + it('shows a display step by name and skips steps with generated names or the same pass', () => { + const states = 'tiling(p) == tilingNotExplicit && compression(p) == compressionNotExplicit'; + render(derivation( + [null, chain(['#if_condition', '#if_condition'], ['x', 'x > 0'], ['p', states])], + ['Binder', chain(['x', 'x > 0'], ['p', states])], + ['Binder', chain(['p', states])], + ['Relevant to Expected', chain(['p', 'compression(p) == compressionNotExplicit'])], + ), 'found compression(p) == compressionNotExplicit but expected ...'); + + expect(shown()).toEqual({ + label: 'Relevant to Expected', info: 'Kept only the facts that share a term with Expected.', + position: '2/2', facts: ['compression(p) == compressionNotExplicit'], + }); + previous(); + expect(shown()).toMatchObject({ label: 'Simplified', position: '1/2', facts: [states] }); + }); + + it('says that nothing known proves Expected when the message could not prove it', () => { + render( + derivation([null, chain(['undoManager', 'undoManager == #getUndoManager_result'])]), + 'expected redo(undoManager) == redoable but could not prove it', + ); + + expect(document.querySelector('.vc-nothing-known')?.textContent) + .toBe('Nothing is known here that could prove Expected.'); + expect(document.querySelector('.vc-line')).toBeNull(); + }); +}); diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index f433e2b..0669cc2 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -1,38 +1,71 @@ -import type { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics"; +import type { RefinementMismatchError } from "../../../types/diagnostics"; import type { VCSimplificationResult } from "../../../types/vc-implications"; import { renderHighlightedExpression } from "../../highlighting"; import { renderCodicon } from "../../icons"; import { escapeHtml } from "../../utils"; -import { renderImplication, renderImplicationChange } from "./vc-changes"; +import { getFacts, renderFacts, renderFactsChange } from "./vc-changes"; + +// A step of Found as it is shown: its facts, and the passes that changed them since the step before +type VCStep = { + facts: string[]; + passes: string[]; +}; // state to preserve across re-renders type VCState = { - steps: VCSimplificationResult[]; - translationTable: TranslationTable; + steps: VCStep[]; stepIndex: number; }; const vcStates = new Map(); // errorId => VCState +// What each simplification pass of the verifier does, in the words of the step's tooltip; any other step, such as +// "Relevant to Expected", is a display step and is shown by its name +const PASS_DESCRIPTIONS: Record = { + "Substitution": "Replaced variables with the values they are equal to.", + "Function Substitution": "Replaced calls with the values they are equal to.", + "Binder": "Removed facts that say nothing, and conditions that Expected does not depend on.", + "Folding": "Computed constant expressions.", + "Arithmetic": "Simplified arithmetic.", + "Logical": "Simplified logical operators.", + "Constraint": "Removed facts that other facts already imply.", +}; +const DISPLAY_STEP_DESCRIPTIONS: Record = { + "Relevant to Expected": "Kept only the facts that share a term with Expected.", +}; +const ORIGINAL_DESCRIPTION = "What is known here, before simplifying."; +const NOTHING_KNOWN = "Nothing is known here that could prove Expected."; +// the verifier's message when found says nothing about what expected constrains +const COULD_NOT_PROVE = /but could not prove it$/u; +// names the verifier makes up (#if_condition) or numbers (x#1), which do not appear in the code +const GENERATED_NAME = /#\w/u; + function renderStepButton(errorId: string, step: "previous" | "next", disabled: boolean): string { const label = `${step === "previous" ? "Previous" : "Next"} simplification`; const icon = step === "previous" ? "arrow-small-left" : "arrow-small-right"; return ``; } -function renderStepHeader( - errorId: string, - current: VCSimplificationResult, - index: number, - stepCount: number, -): string { +function getStepLabel(step: VCStep): { label: string; description: string } { + if (step.passes.length === 0) return { label: "Original", description: ORIGINAL_DESCRIPTION }; + const displayStep = step.passes.find(pass => !(pass in PASS_DESCRIPTIONS)); + const description = step.passes + .map(pass => PASS_DESCRIPTIONS[pass] ?? DISPLAY_STEP_DESCRIPTIONS[pass]) + .filter(Boolean) + .join(" "); + return { label: displayStep ?? "Simplified", description }; +} + +function renderStepHeader(errorId: string, step: VCStep, index: number, stepCount: number): string { const currStep = stepCount - index; - const simplification = current.simplification?.trim(); - const label = escapeHtml(index === 0 ? "Simplified" : simplification || "Original"); + const { label, description } = getStepLabel(step); return /*html*/`
- ${label} + + ${escapeHtml(label)} + ${description ? /*html*/`${renderCodicon("info")}` : ""} +
${currStep}/${stepCount} @@ -46,6 +79,44 @@ function renderStepHeader( `; } +/** + * The steps of a derivation worth showing, newest first. The newest is always shown; an older one only when its facts + * use no generated name, and not when it looks like the step after it or only continues the same pass. Each step keeps + * the passes that changed the facts since the step before it + */ +function getVCSteps(result: VCSimplificationResult): VCStep[] { + const derivation: VCSimplificationResult[] = []; + for (let current: VCSimplificationResult | null = result; current; current = current.origin) { + derivation.unshift(current); + } + const facts = derivation.map(current => getFacts(current.implication)); + + const shown: number[] = []; + facts.forEach((stepFacts, index) => { + const isNewest = index === derivation.length - 1; + if (!isNewest && stepFacts.some(fact => GENERATED_NAME.test(fact))) return; + const last = shown[shown.length - 1]; + const samePass = last > 0 && derivation[last].simplification === derivation[index].simplification; + if (last !== undefined && (samePass || sameFacts(facts[last], stepFacts))) shown.pop(); + shown.push(index); + }); + + let previous = 0; + return shown.map(index => { + const passes = new Set(); + for (let i = previous + 1; i <= index; i++) { + const pass = derivation[i].simplification; + if (pass && !sameFacts(facts[i - 1], facts[i])) passes.add(pass); + } + previous = index; + return { facts: facts[index], passes: [...passes] }; + }).reverse(); +} + +function sameFacts(a: string[], b: string[]): boolean { + return a.length === b.length && a.every((fact, i) => fact === b[i]); +} + function getTargetStepIndex(state: VCState, step: string | null): number | undefined { const targetIndex = step === "previous" ? state.stepIndex + 1 @@ -60,12 +131,12 @@ function renderSelectedStep(errorId: string, previousIndex?: number): string { const state = vcStates.get(errorId); if (!state) return ""; - const { steps, translationTable, stepIndex } = state; + const { steps, stepIndex } = state; const current = steps[stepIndex]; const previous = previousIndex === undefined ? undefined : steps[previousIndex]; const implication = previous - ? `
${renderImplicationChange(previous.implication, current.implication, translationTable)}
` - : `
${renderImplication(current.implication, translationTable)}
`; + ? `
${renderFactsChange(previous.facts, current.facts)}
` + : `
${renderFacts(current.facts)}
`; return /*html*/` ${steps.length > 1 ? renderStepHeader(errorId, current, stepIndex, steps.length) : ""} @@ -97,6 +168,9 @@ export function renderVCImplication( result: VCSimplificationResult ): string { if (!result?.implication) return renderHighlightedExpression(String(result)); + if (COULD_NOT_PROVE.test(error.message)) { + return `

${NOTHING_KNOWN}

`; + } const errorId = encodeURIComponent(JSON.stringify([ error.file, @@ -104,12 +178,9 @@ export function renderVCImplication( error.title, error.message ])); - const steps: VCSimplificationResult[] = []; - for (let current: VCSimplificationResult | null = result; current; current = current.origin) { - steps.push(current); - } + const steps = getVCSteps(result); const stepIndex = Math.min(vcStates.get(errorId)?.stepIndex ?? 0, steps.length - 1); - vcStates.set(errorId, { steps, translationTable: error.translationTable, stepIndex }); + vcStates.set(errorId, { steps, stepIndex }); return /*html*/ `
From 0f68b5f71eda194ab052c1aa718b0161db10d112 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 02:11:05 +0000 Subject: [PATCH 2/9] Make the step merge condition explicit about the first step Co-Authored-By: Claude Opus 5.5 --- client/src/webview/views/diagnostics/vc-implications.ts | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 0669cc2..ee564b0 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -95,9 +95,11 @@ function getVCSteps(result: VCSimplificationResult): VCStep[] { facts.forEach((stepFacts, index) => { const isNewest = index === derivation.length - 1; if (!isNewest && stepFacts.some(fact => GENERATED_NAME.test(fact))) return; - const last = shown[shown.length - 1]; - const samePass = last > 0 && derivation[last].simplification === derivation[index].simplification; - if (last !== undefined && (samePass || sameFacts(facts[last], stepFacts))) shown.pop(); + const last: number | undefined = shown[shown.length - 1]; + if (last !== undefined && (sameFacts(facts[last], stepFacts) + || (last > 0 && derivation[last].simplification === derivation[index].simplification))) { + shown.pop(); + } shown.push(index); }); From 3209ab8a5150554a8f63dbe29e02de6c8aa9cbb9 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 02:21:22 +0000 Subject: [PATCH 3/9] Send the error category to the client and key "Nothing is known" off it The verifier categorizes an error as unknown exactly when its message says it could not prove what was expected. The server now sends that category (lowercase, hyphenated, absent when the verifier gives none), and Found says that nothing known proves Expected from it instead of from the message text. Co-Authored-By: Claude Opus 5.5 --- client/src/types/diagnostics.ts | 7 +++++++ .../views/diagnostics/vc-implications.spec.ts | 13 ++++++++----- .../webview/views/diagnostics/vc-implications.ts | 4 +--- server/src/main/java/dtos/errors/LJErrorDTO.java | 9 +++++++-- .../test/java/utils/DiagnosticConverterTest.java | 2 ++ 5 files changed, 25 insertions(+), 10 deletions(-) diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 36ab1c4..84172e0 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -27,6 +27,9 @@ export type LJWarning = CustomWarning | ExternalClassNotFoundWarning | ExternalM export type LJHintKind = 'general' | 'deciding-argument' | 'call-sequence' | 'available-calls' | 'unreachable-state' | 'path-dependent-state' | 'final-state' | 'reaching-calls'; +// the kind of mistake an error shows, as the verifier names it, e.g. 'unknown' when nothing known could prove what was expected +export type LJErrorCategory = 'out-of-order' | 'out-of-domain' | 'argument-picks-the-state' | 'path-dependent-state' | 'unknown'; + export type LJHint = { kind: LJHintKind; message: string; @@ -68,6 +71,8 @@ export type RefinementError = BaseDiagnostic & { category: 'error'; type: 'refinement-error'; translationTable: TranslationTable; + // absent when the verifier gives none, as lsp4j leaves out null fields + errorCategory?: LJErrorCategory; expected: string; found: VCSimplificationResult; customMessage: string; @@ -95,6 +100,8 @@ export type StateRefinementError = BaseDiagnostic & { category: 'error'; type: 'state-refinement-error'; translationTable: TranslationTable; + // absent when the verifier gives none, as lsp4j leaves out null fields + errorCategory?: LJErrorCategory; expected: string; found: VCSimplificationResult; customMessage: string; diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts index b311975..3fb3e86 100644 --- a/client/src/webview/views/diagnostics/vc-implications.spec.ts +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -1,5 +1,5 @@ import { afterEach, describe, expect, it } from 'vitest'; -import type { RefinementError } from '../../../types/diagnostics'; +import type { LJErrorCategory, RefinementError } from '../../../types/diagnostics'; import type { VCImplication, VCSimplificationResult } from '../../../types/vc-implications'; import { handleVCImplicationStepClick, renderVCImplication } from './vc-implications'; @@ -17,8 +17,10 @@ function derivation(...steps: Array<[string | null, VCImplication]>): VCSimplifi ) as VCSimplificationResult; } -function render(found: VCSimplificationResult, message = 'found ... but expected ...'): void { - const error = { file: 'A.java', position: null, title: 'Refinement Error', message } as unknown as RefinementError; +function render(found: VCSimplificationResult, message = 'found ... but expected ...', errorCategory?: LJErrorCategory): void { + const error = { + file: 'A.java', position: null, title: 'Refinement Error', message, errorCategory, + } as unknown as RefinementError; document.body.innerHTML = renderVCImplication(error, found); } @@ -76,10 +78,11 @@ describe('Found', () => { expect(shown()).toMatchObject({ label: 'Simplified', position: '1/2', facts: [states] }); }); - it('says that nothing known proves Expected when the message could not prove it', () => { + it('says that nothing known proves Expected when its category is unknown', () => { render( derivation([null, chain(['undoManager', 'undoManager == #getUndoManager_result'])]), - 'expected redo(undoManager) == redoable but could not prove it', + 'expected redo(undoManager) == redoable', + 'unknown', ); expect(document.querySelector('.vc-nothing-known')?.textContent) diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index ee564b0..125960e 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -35,8 +35,6 @@ const DISPLAY_STEP_DESCRIPTIONS: Record = { }; const ORIGINAL_DESCRIPTION = "What is known here, before simplifying."; const NOTHING_KNOWN = "Nothing is known here that could prove Expected."; -// the verifier's message when found says nothing about what expected constrains -const COULD_NOT_PROVE = /but could not prove it$/u; // names the verifier makes up (#if_condition) or numbers (x#1), which do not appear in the code const GENERATED_NAME = /#\w/u; @@ -170,7 +168,7 @@ export function renderVCImplication( result: VCSimplificationResult ): string { if (!result?.implication) return renderHighlightedExpression(String(result)); - if (COULD_NOT_PROVE.test(error.message)) { + if (error.errorCategory === "unknown") { return `

${NOTHING_KNOWN}

`; } diff --git a/server/src/main/java/dtos/errors/LJErrorDTO.java b/server/src/main/java/dtos/errors/LJErrorDTO.java index 9293491..02f0c5e 100644 --- a/server/src/main/java/dtos/errors/LJErrorDTO.java +++ b/server/src/main/java/dtos/errors/LJErrorDTO.java @@ -1,6 +1,7 @@ package dtos.errors; import java.util.List; +import java.util.Locale; import dtos.diagnostics.HintDTO; import dtos.diagnostics.LJDiagnosticDTO; @@ -14,21 +15,25 @@ public class LJErrorDTO extends LJDiagnosticDTO { public final TranslationTableDTO translationTable; + /** The kind of mistake, e.g. {@code unknown} when nothing known could prove what was expected, or null */ + public final String errorCategory; public LJErrorDTO(String type, LJError error) { - super("error", type, error); - this.translationTable = TranslationTableDTO.from(error.getTranslationTable()); + this("error", type, error); } protected LJErrorDTO(String category, String type, LJError error) { super(category, type, error); this.translationTable = TranslationTableDTO.from(error.getTranslationTable()); + this.errorCategory = error.getCategory() + .map(kind -> kind.name().toLowerCase(Locale.ROOT).replace('_', '-')).orElse(null); } public LJErrorDTO(String category, String type, String title, String message, List hints, String file, SourcePositionDTO position, TranslationTableDTO translationTable) { super(category, type, title, message, hints, file, position); this.translationTable = translationTable; + this.errorCategory = null; } public static LJErrorDTO from(LJError error) { diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java index 1e24658..6776562 100644 --- a/server/src/test/java/utils/DiagnosticConverterTest.java +++ b/server/src/test/java/utils/DiagnosticConverterTest.java @@ -165,6 +165,7 @@ void preservesRefinementDetailsAndSimplificationHistory() { assertNull(dto.found.origin().origin()); assertNull(dto.found.origin().simplification()); assertTrue(dto.counterexample.assignments().isEmpty()); + assertEquals("unknown", dto.errorCategory); } @Test @@ -180,6 +181,7 @@ void preservesStateRefinementDetailsWithoutDeclarationFile() { assertEquals("expected closed", dto.customMessage); assertNull(dto.declarationPosition); assertEquals(List.of(), dto.stateMachines); + assertNull(dto.errorCategory); } @Test From 02de6716f215ed43ec91d1fa09030f73c2d83112 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 02:24:03 +0000 Subject: [PATCH 4/9] Say that nothing known proves Expected when Found states nothing Co-Authored-By: Claude Opus 5.5 --- .../views/diagnostics/vc-implications.spec.ts | 13 ++++++------- .../webview/views/diagnostics/vc-implications.ts | 5 +++-- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts index 3fb3e86..e877e1a 100644 --- a/client/src/webview/views/diagnostics/vc-implications.spec.ts +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -4,7 +4,7 @@ import type { VCImplication, VCSimplificationResult } from '../../../types/vc-im import { handleVCImplicationStepClick, renderVCImplication } from './vc-implications'; // a VC chain from its rows, each a binder and its predicate -function chain(...rows: Array<[string, string]>): VCImplication { +function chain(...rows: ReadonlyArray): VCImplication { return rows.reduceRight( (next, [name, predicate]) => ({ name, type: 'int', predicate, next }), null, ) as VCImplication; @@ -78,12 +78,11 @@ describe('Found', () => { expect(shown()).toMatchObject({ label: 'Simplified', position: '1/2', facts: [states] }); }); - it('says that nothing known proves Expected when its category is unknown', () => { - render( - derivation([null, chain(['undoManager', 'undoManager == #getUndoManager_result'])]), - 'expected redo(undoManager) == redoable', - 'unknown', - ); + it.each([ + ['its category is unknown', [['undoManager', 'undoManager == #getUndoManager_result']], 'unknown'], + ['found states nothing', [['timeout', 'true']], undefined], + ] as const)('says that nothing known proves Expected when %s', (_label, rows, errorCategory) => { + render(derivation([null, chain(...rows)]), 'found ... but expected ...', errorCategory); expect(document.querySelector('.vc-nothing-known')?.textContent) .toBe('Nothing is known here that could prove Expected.'); diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 125960e..7e4ba30 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -168,7 +168,9 @@ export function renderVCImplication( result: VCSimplificationResult ): string { if (!result?.implication) return renderHighlightedExpression(String(result)); - if (error.errorCategory === "unknown") { + const steps = getVCSteps(result); + // also when found states nothing, which a state error the verifier leaves uncategorized can have + if (error.errorCategory === "unknown" || steps[0].facts.length === 0) { return `

${NOTHING_KNOWN}

`; } @@ -178,7 +180,6 @@ export function renderVCImplication( error.title, error.message ])); - const steps = getVCSteps(result); const stepIndex = Math.min(vcStates.get(errorId)?.stepIndex ?? 0, steps.length - 1); vcStates.set(errorId, { steps, stepIndex }); From 0f2a9802bf0de4429e07800be8c741fefbf21e83 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 12:39:25 +0000 Subject: [PATCH 5/9] Found: keep the binders and implications, with a line per conjunct Found shows the chain again, each binder linked to its source and an arrow after each fact, and splits each fact at its top-level && into a line per conjunct. When nothing known proves Expected, the newest step says so and the older steps stay a step back. Co-Authored-By: Claude Opus 5.5 --- client/src/webview/styles.ts | 55 +++++++- .../views/diagnostics/vc-changes.spec.ts | 40 ++++++ .../webview/views/diagnostics/vc-changes.ts | 119 +++++++++++++++--- .../views/diagnostics/vc-implications.spec.ts | 34 ++--- .../views/diagnostics/vc-implications.ts | 64 ++++++---- 5 files changed, 249 insertions(+), 63 deletions(-) create mode 100644 client/src/webview/views/diagnostics/vc-changes.spec.ts diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 4ecd621..74c5748 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -467,25 +467,46 @@ export function getStyles(): string { text-align: right; } .vc-chain { + display: grid; + grid-template-columns: fit-content(40%) minmax(0, 1fr); + row-gap: 0.25rem; + width: 100%; + min-width: 0; + } + .counterexample-container .vc-chain { display: flex; flex-direction: column; gap: 0.25rem; - width: 100%; - min-width: 0; } .counterexample-line { overflow-wrap: anywhere; } .vc-line { + display: contents; + } + .vc-binder-cell, + .vc-predicate-cell { min-width: 0; padding: 0.0625rem 0.25rem; overflow-wrap: anywhere; } - .vc-nothing-known { - margin: 0; - padding: 0.0625rem 0.25rem; + .vc-binder-cell { + min-height: 1.2em; + padding-right: 0.75rem; + color: var(--vscode-descriptionForeground); + white-space: normal; + } + .vc-predicate-cell { + color: var(--vscode-editor-foreground); + } + .vc-arrow { + font-size: 1.5em; + line-height: 0; + vertical-align: middle; color: var(--vscode-descriptionForeground); - font-family: var(--vscode-font-family); + } + .vc-predicate-cell:only-child { + grid-column: 1 / -1; } .vc-node { display: inline; @@ -545,6 +566,15 @@ export function getStyles(): string { animation: none; } } + .vc-binder { + color: var(--vscode-descriptionForeground); + } + .vc-nothing-known { + margin: 0; + padding: 0.0625rem 0.25rem; + color: var(--vscode-descriptionForeground); + font-family: var(--vscode-font-family); + } .vc-step-title { display: inline-flex; align-items: center; @@ -886,6 +916,10 @@ export function getStyles(): string { .highlight-var-btn.selected { background-color: var(--vscode-button-background); } + .vc-binder.highlight-var-btn { + margin: 0; + padding: 0 0.15rem; + } .highlight-var-btn.clickable { text-decoration-color: var(--vscode-textLink-foreground); text-decoration-thickness: 1.5px; @@ -894,6 +928,15 @@ export function getStyles(): string { .highlight-var-btn.clickable:hover { font-weight: inherit; } + .vc-binder.highlight-var-btn:not(.selected):hover { + background-color: color-mix(in srgb, var(--vscode-button-background) 35%, transparent); + } + .vc-binder.highlight-var-btn.clickable { + text-decoration-color: currentColor; + } + .vc-binder.highlight-var-btn.selected { + color: var(--lj-token-identifier); + } .highlight-var-btn.error, .diagnostic-reveal-btn.error { background-color: color-mix(in srgb, var(--vscode-errorForeground) 80%, transparent); diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts new file mode 100644 index 0000000..06527fb --- /dev/null +++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts @@ -0,0 +1,40 @@ +import { afterEach, describe, expect, it } from 'vitest'; +import type { VCImplication } from '../../../types/vc-implications'; +import { renderImplication, renderImplicationChange } from './vc-changes'; + +const conclusion: VCImplication = { name: null, type: null, predicate: 'x > 0', next: null }; +const implication: VCImplication = { + name: 'x', type: 'int', predicate: 'x == 1', + next: { name: 'y', type: 'int', predicate: 'y == 2', next: conclusion }, +}; + +afterEach(() => { document.body.innerHTML = ''; }); + +describe('verification implications', () => { + it.each([ + ['initial rendering', () => renderImplication(implication)], + ['simplification change', () => renderImplicationChange( + { ...implication, predicate: 'x > 0' }, implication, + )], + ] as const)('adds an implication arrow after each nonterminal predicate during %s', (_label, render) => { + document.body.innerHTML = render(); + + const binders = Array.from(document.querySelectorAll('.vc-binder-cell')); + expect(binders.map(cell => cell.textContent?.trim())).toEqual(['∀x', '∀y']); + expect(binders.map(cell => cell.querySelector('.vc-binder')?.textContent)).toEqual(['∀x', '∀y']); + expect(document.querySelector('.vc-line:last-child')?.textContent?.trim()).toBe('x > 0'); + expect(Array.from(document.querySelectorAll('.vc-predicate-cell')).map(cell => cell.textContent?.trim())) + .toEqual(['x == 1 →', 'y == 2 →', 'x > 0']); + expect(document.querySelectorAll('.vc-predicate-cell > .vc-arrow')).toHaveLength(2); + }); + it.each([ + ['initial rendering', () => renderImplication({ ...implication, next: null })], + ['simplification change', () => renderImplicationChange(implication, { ...implication, next: null })], + ] as const)('omits the arrow on a terminal node with a binder during %s', (_label, render) => { + document.body.innerHTML = render(); + + expect(document.querySelector('.vc-binder')?.textContent).toBe('∀x'); + expect(document.querySelector('.vc-predicate-cell')?.textContent?.trim()).toBe('x == 1'); + expect(document.querySelector('.vc-arrow')).toBeNull(); + }); +}); diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 42b4995..8d89909 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -1,5 +1,8 @@ import type { VCImplication } from "../../../types/vc-implications"; +import type { TranslationTable } from "../../../types/diagnostics"; import { renderHighlightedInlineExpression } from "../../highlighting"; +import { escapeHtml } from "../../utils"; +import { renderSourceHighlightButton } from "../sections"; type ChangeKind = "unchanged" | "removed" | "added"; type DiffOperation = { kind: ChangeKind; value: T }; @@ -7,23 +10,85 @@ type DiffOperation = { kind: ChangeKind; value: T }; const MIN_LINE_SIMILARITY = 0.3; const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu; const WHITESPACE_PATTERN = /^\s+$/u; +const VC_LINE_SEPARATOR = "\t"; + +function hasBinder(node: VCImplication): boolean { + return typeof node.name === "string" && node.name.length > 0; +} + +// one line per conjunct of a node's predicate; the lines after the first keep its binder to tell nodes apart, but do not show it +function formatImplicationLines(node: VCImplication): string[] { + const binder = hasBinder(node) ? `∀${node.name}` : ""; + const type = typeof node.type === "string" ? node.type : ""; + const conjuncts = splitConjuncts(node.predicate); + return conjuncts.map((conjunct, index) => { + const isLast = index === conjuncts.length - 1; + const predicate = isLast ? conjunct : `${conjunct} &&`; + return [binder, type, predicate, isLast && node.next ? "next" : "", index > 0 ? "continued" : ""] + .join(VC_LINE_SEPARATOR); + }); +} + +function parseImplicationLine(line: string): { + binder: string; type: string; predicate: string; hasNext: boolean; isContinued: boolean; +} { + const [binder = "", type = "", predicate = "", next = "", continued = ""] = line.split(VC_LINE_SEPARATOR); + return { binder, type, predicate, hasNext: next === "next", isContinued: continued === "continued" }; +} + +// splits a predicate on the && outside parentheses +function splitConjuncts(predicate: string): string[] { + const conjuncts: string[] = []; + let depth = 0; + let start = 0; + for (let i = 0; i < predicate.length; i++) { + if (predicate[i] === "(") depth++; + else if (predicate[i] === ")") depth--; + else if (depth === 0 && predicate.startsWith("&&", i)) { + conjuncts.push(predicate.slice(start, i).trim()); + start = i + 2; + } + } + return [...conjuncts, predicate.slice(start).trim()]; +} /** - * The facts of a VC chain, one per row, leaving out rows that state nothing. All of them hold, so they are shown - * without the binders and implications of the chain + * The lines of a VC chain: one per conjunct of each node with a binder, and of the conclusion */ -export function getFacts(node: VCImplication): string[] { - const facts: string[] = []; +export function getImplicationLines(node: VCImplication): string[] { + const lines: string[] = []; for (let current: VCImplication | null = node; current; current = current.next) { - if (current.predicate.trim() !== "true") facts.push(current.predicate); + if (current.next && !hasBinder(current)) continue; + lines.push(...formatImplicationLines(current)); } - return facts; + return lines; } -function renderFact(fact: string, className = "", content?: string): string { +function renderBinder(binder: string, type: string, translationTable?: TranslationTable): string { + const placement = translationTable?.[binder.slice(1)]; + if (!placement?.position?.file) { + return `${escapeHtml(binder)}`; + } + return renderSourceHighlightButton( + escapeHtml(binder), + type ? `Go to source (${type})` : "Go to source", + placement.position, + "vc-node vc-binder clickable", + ); +} + +export function renderVCLine( + line: string, + className = "", + predicateContent?: string, + translationTable?: TranslationTable, +): string { + const { binder, type, predicate, hasNext, isContinued } = parseImplicationLine(line); + const binderCell = isContinued ? "" : renderBinder(binder, type, translationTable); return /*html*/`
- ${content ?? renderHighlightedInlineExpression(fact)} + ${binder ? /*html*/`
${binderCell}
` : ""} +
${predicateContent ?? renderHighlightedInlineExpression(predicate)}${hasNext ? ' →' : ""}
`; } @@ -152,30 +217,48 @@ function alignChangedLines(removed: string[], added: string[]): Array<[string | return lines; } -function renderChangedFacts(removed: string[], added: string[]): string { +function renderChangedDestinationLines( + removed: string[], + added: string[], + translationTable?: TranslationTable, +): string { if (added.length === 0) return ""; return alignChangedLines(removed, added) .map(([before, after]) => { if (after === undefined) return ""; - if (before === undefined) return renderFact(after, "vc-change-line"); - const change = renderDestinationTokenDiff(before, after); - return renderFact(after, change.hasAddedContent ? "" : "vc-change-line", change.content); + if (before === undefined) return renderVCLine(after, "vc-change-line", undefined, translationTable); + const change = renderDestinationTokenDiff( + parseImplicationLine(before).predicate, + parseImplicationLine(after).predicate, + ); + return renderVCLine( + after, + change.hasAddedContent ? "" : "vc-change-line", + change.content, + translationTable, + ); }) .join(""); } -export function renderFacts(facts: string[]): string { - return facts.map(fact => renderFact(fact)).join(""); +export function renderImplication(node: VCImplication, translationTable?: TranslationTable): string { + return getImplicationLines(node) + .map(line => renderVCLine(line, "", undefined, translationTable)) + .join(""); } -export function renderFactsChange(before: string[], after: string[]): string { - const operations = diffSequence(before, after); +export function renderImplicationChange( + before: VCImplication, + after: VCImplication, + translationTable?: TranslationTable, +): string { + const operations = diffSequence(getImplicationLines(before), getImplicationLines(after)); let html = ""; const changed = { removed: [] as string[], added: [] as string[] }; const flushChanges = () => { - html += renderChangedFacts(changed.removed, changed.added); + html += renderChangedDestinationLines(changed.removed, changed.added, translationTable); changed.removed.length = 0; changed.added.length = 0; }; @@ -183,7 +266,7 @@ export function renderFactsChange(before: string[], after: string[]): string { for (const operation of operations) { if (operation.kind === "unchanged") { flushChanges(); - html += renderFact(operation.value); + html += renderVCLine(operation.value, "", undefined, translationTable); continue; } changed[operation.kind].push(operation.value); diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts index e877e1a..6c4e21f 100644 --- a/client/src/webview/views/diagnostics/vc-implications.spec.ts +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -29,7 +29,7 @@ function shown() { label: document.querySelector('.vc-step-name')?.textContent, info: document.querySelector('.vc-step-info')?.getAttribute('title'), position: document.querySelector('.vc-step-position')?.textContent?.trim(), - facts: Array.from(document.querySelectorAll('.vc-line')).map(line => line.textContent?.trim()), + lines: Array.from(document.querySelectorAll('.vc-line')).map(line => line.textContent?.replace(/\s+/gu, ' ').trim()), }; } @@ -40,25 +40,24 @@ function previous(): void { afterEach(() => { document.body.innerHTML = ''; }); describe('Found', () => { - it('lists the facts without binders, implications or rows that state nothing', () => { + it('keeps the binders and implications, with a line per conjunct', () => { const size = 'failures.size() == size(this.failures) && failures.size() >= 0'; render(derivation( [null, chain(['this.failures', 'true'], ['failures', 'failures == this.failures'], ['failures.size()', 'failures.size() == size(failures) && failures.size() >= 0'])], ['Substitution', chain(['this.failures', 'true'], ['failures.size()', size])], - ['Binder', chain(['failures.size()', size])], )); - expect(document.body.textContent).not.toMatch(/[∀→]/u); expect(shown()).toEqual({ label: 'Simplified', info: 'Replaced variables with the values they are equal to.', position: '2/2', - facts: [size], + lines: ['∀this.failures true →', '∀failures.size() failures.size() == size(this.failures) &&', 'failures.size() >= 0'], }); + // a conjunct after the first sits under its binder, which is shown once + expect(Array.from(document.querySelectorAll('.vc-binder'), binder => binder.textContent)) + .toEqual(['∀this.failures', '∀failures.size()']); previous(); - expect(shown()).toEqual({ - label: 'Original', info: 'What is known here, before simplifying.', position: '1/2', - facts: ['failures == this.failures', 'failures.size() == size(failures) && failures.size() >= 0'], - }); + expect(shown()).toMatchObject({ label: 'Original', position: '1/2' }); + expect(shown().lines).toContain('∀failures failures == this.failures →'); }); it('shows a display step by name and skips steps with generated names or the same pass', () => { @@ -72,20 +71,27 @@ describe('Found', () => { expect(shown()).toEqual({ label: 'Relevant to Expected', info: 'Kept only the facts that share a term with Expected.', - position: '2/2', facts: ['compression(p) == compressionNotExplicit'], + position: '2/2', lines: ['∀p compression(p) == compressionNotExplicit'], }); previous(); - expect(shown()).toMatchObject({ label: 'Simplified', position: '1/2', facts: [states] }); + expect(shown()).toMatchObject({ + label: 'Simplified', position: '1/2', + lines: ['∀p tiling(p) == tilingNotExplicit &&', 'compression(p) == compressionNotExplicit'], + }); }); it.each([ - ['its category is unknown', [['undoManager', 'undoManager == #getUndoManager_result']], 'unknown'], + ['its category is unknown', [['undoManager', 'undoManager == undoManager@12']], 'unknown'], ['found states nothing', [['timeout', 'true']], undefined], - ] as const)('says that nothing known proves Expected when %s', (_label, rows, errorCategory) => { - render(derivation([null, chain(...rows)]), 'found ... but expected ...', errorCategory); + ] as const)('says that nothing known proves Expected when %s, with the steps before it a step back', (label, rows, errorCategory) => { + render(derivation([null, chain(['x', 'x > 0'], ...rows)], ['Binder', chain(...rows)]), `found ${label}`, errorCategory); expect(document.querySelector('.vc-nothing-known')?.textContent) .toBe('Nothing is known here that could prove Expected.'); expect(document.querySelector('.vc-line')).toBeNull(); + previous(); + expect(document.querySelector('.vc-nothing-known')).toBeNull(); + expect(shown()).toMatchObject({ label: 'Original', position: '1/2' }); + expect(shown().lines[0]).toBe('∀x x > 0 →'); }); }); diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 7e4ba30..56bb767 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -1,20 +1,24 @@ -import type { RefinementMismatchError } from "../../../types/diagnostics"; -import type { VCSimplificationResult } from "../../../types/vc-implications"; +import type { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics"; +import type { VCImplication, VCSimplificationResult } from "../../../types/vc-implications"; import { renderHighlightedExpression } from "../../highlighting"; import { renderCodicon } from "../../icons"; import { escapeHtml } from "../../utils"; -import { getFacts, renderFacts, renderFactsChange } from "./vc-changes"; +import { getImplicationLines, renderImplication, renderImplicationChange } from "./vc-changes"; -// A step of Found as it is shown: its facts, and the passes that changed them since the step before +// A step of Found as it is shown: its chain, the lines it is shown in, and the passes that changed them since the step before type VCStep = { - facts: string[]; + implication: VCImplication; + lines: string[]; passes: string[]; }; // state to preserve across re-renders type VCState = { steps: VCStep[]; + translationTable: TranslationTable; stepIndex: number; + // whether the newest step is replaced by saying that nothing known proves Expected + nothingKnown: boolean; }; const vcStates = new Map(); // errorId => VCState @@ -78,23 +82,23 @@ function renderStepHeader(errorId: string, step: VCStep, index: number, stepCoun } /** - * The steps of a derivation worth showing, newest first. The newest is always shown; an older one only when its facts + * The steps of a derivation worth showing, newest first. The newest is always shown; an older one only when its lines * use no generated name, and not when it looks like the step after it or only continues the same pass. Each step keeps - * the passes that changed the facts since the step before it + * the passes that changed the lines since the step before it */ function getVCSteps(result: VCSimplificationResult): VCStep[] { const derivation: VCSimplificationResult[] = []; for (let current: VCSimplificationResult | null = result; current; current = current.origin) { derivation.unshift(current); } - const facts = derivation.map(current => getFacts(current.implication)); + const lines = derivation.map(current => getImplicationLines(current.implication)); const shown: number[] = []; - facts.forEach((stepFacts, index) => { + lines.forEach((stepLines, index) => { const isNewest = index === derivation.length - 1; - if (!isNewest && stepFacts.some(fact => GENERATED_NAME.test(fact))) return; + if (!isNewest && stepLines.some(line => GENERATED_NAME.test(line))) return; const last: number | undefined = shown[shown.length - 1]; - if (last !== undefined && (sameFacts(facts[last], stepFacts) + if (last !== undefined && (sameLines(lines[last], stepLines) || (last > 0 && derivation[last].simplification === derivation[index].simplification))) { shown.pop(); } @@ -106,15 +110,23 @@ function getVCSteps(result: VCSimplificationResult): VCStep[] { const passes = new Set(); for (let i = previous + 1; i <= index; i++) { const pass = derivation[i].simplification; - if (pass && !sameFacts(facts[i - 1], facts[i])) passes.add(pass); + if (pass && !sameLines(lines[i - 1], lines[i])) passes.add(pass); } previous = index; - return { facts: facts[index], passes: [...passes] }; + return { implication: derivation[index].implication, lines: lines[index], passes: [...passes] }; }).reverse(); } -function sameFacts(a: string[], b: string[]): boolean { - return a.length === b.length && a.every((fact, i) => fact === b[i]); +function sameLines(a: string[], b: string[]): boolean { + return a.length === b.length && a.every((line, i) => line === b[i]); +} + +// a chain states nothing when every predicate in it is true +function statesNothing(node: VCImplication): boolean { + for (let current: VCImplication | null = node; current; current = current.next) { + if (current.predicate.trim() !== "true") return false; + } + return true; } function getTargetStepIndex(state: VCState, step: string | null): number | undefined { @@ -131,12 +143,15 @@ function renderSelectedStep(errorId: string, previousIndex?: number): string { const state = vcStates.get(errorId); if (!state) return ""; - const { steps, stepIndex } = state; + const { steps, translationTable, stepIndex, nothingKnown } = state; const current = steps[stepIndex]; - const previous = previousIndex === undefined ? undefined : steps[previousIndex]; - const implication = previous - ? `
${renderFactsChange(previous.facts, current.facts)}
` - : `
${renderFacts(current.facts)}
`; + // a change is shown from a step whose chain was shown + const previous = previousIndex === undefined || (nothingKnown && previousIndex === 0) ? undefined : steps[previousIndex]; + const implication = nothingKnown && stepIndex === 0 + ? `

${NOTHING_KNOWN}

` + : previous + ? `
${renderImplicationChange(previous.implication, current.implication, translationTable)}
` + : `
${renderImplication(current.implication, translationTable)}
`; return /*html*/` ${steps.length > 1 ? renderStepHeader(errorId, current, stepIndex, steps.length) : ""} @@ -169,10 +184,9 @@ export function renderVCImplication( ): string { if (!result?.implication) return renderHighlightedExpression(String(result)); const steps = getVCSteps(result); - // also when found states nothing, which a state error the verifier leaves uncategorized can have - if (error.errorCategory === "unknown" || steps[0].facts.length === 0) { - return `

${NOTHING_KNOWN}

`; - } + // also when found states nothing, which a state error the verifier leaves uncategorized can have; + // the older steps stay a step back + const nothingKnown = error.errorCategory === "unknown" || statesNothing(steps[0].implication); const errorId = encodeURIComponent(JSON.stringify([ error.file, @@ -181,7 +195,7 @@ export function renderVCImplication( error.message ])); const stepIndex = Math.min(vcStates.get(errorId)?.stepIndex ?? 0, steps.length - 1); - vcStates.set(errorId, { steps, stepIndex }); + vcStates.set(errorId, { steps, translationTable: error.translationTable, stepIndex, nothingKnown }); return /*html*/ `
From 4fb1a77e10f4d2ffdb115775322d346abe4efbc2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 12:53:09 +0000 Subject: [PATCH 6/9] Found: open on a summary step when nothing known proves Expected, so the chain is a step back Co-Authored-By: Claude Opus 5.5 --- .../views/diagnostics/vc-implications.spec.ts | 9 ++++---- .../views/diagnostics/vc-implications.ts | 22 +++++++++++-------- 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts index 6c4e21f..2f25914 100644 --- a/client/src/webview/views/diagnostics/vc-implications.spec.ts +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -83,15 +83,14 @@ describe('Found', () => { it.each([ ['its category is unknown', [['undoManager', 'undoManager == undoManager@12']], 'unknown'], ['found states nothing', [['timeout', 'true']], undefined], - ] as const)('says that nothing known proves Expected when %s, with the steps before it a step back', (label, rows, errorCategory) => { - render(derivation([null, chain(['x', 'x > 0'], ...rows)], ['Binder', chain(...rows)]), `found ${label}`, errorCategory); + ] as const)('says that nothing known proves Expected when %s, with the steps a step back', (label, rows, errorCategory) => { + render(derivation([null, chain(...rows)]), `found ${label}`, errorCategory); + expect(shown()).toMatchObject({ label: 'Summary', info: 'Go back to see what is known here.', position: '2/2', lines: [] }); expect(document.querySelector('.vc-nothing-known')?.textContent) .toBe('Nothing is known here that could prove Expected.'); - expect(document.querySelector('.vc-line')).toBeNull(); previous(); expect(document.querySelector('.vc-nothing-known')).toBeNull(); - expect(shown()).toMatchObject({ label: 'Original', position: '1/2' }); - expect(shown().lines[0]).toBe('∀x x > 0 →'); + expect(shown()).toMatchObject({ label: 'Original', position: '1/2', lines: [`∀${rows[0][0]} ${rows[0][1]}`] }); }); }); diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 56bb767..98f399a 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -10,6 +10,8 @@ type VCStep = { implication: VCImplication; lines: string[]; passes: string[]; + // a step before the newest that says nothing known proves Expected, instead of showing the chain + nothingKnown?: boolean; }; // state to preserve across re-renders @@ -17,8 +19,6 @@ type VCState = { steps: VCStep[]; translationTable: TranslationTable; stepIndex: number; - // whether the newest step is replaced by saying that nothing known proves Expected - nothingKnown: boolean; }; const vcStates = new Map(); // errorId => VCState @@ -39,6 +39,7 @@ const DISPLAY_STEP_DESCRIPTIONS: Record = { }; const ORIGINAL_DESCRIPTION = "What is known here, before simplifying."; const NOTHING_KNOWN = "Nothing is known here that could prove Expected."; +const NOTHING_KNOWN_DESCRIPTION = "Go back to see what is known here."; // names the verifier makes up (#if_condition) or numbers (x#1), which do not appear in the code const GENERATED_NAME = /#\w/u; @@ -49,6 +50,7 @@ function renderStepButton(errorId: string, step: "previous" | "next", disabled: } function getStepLabel(step: VCStep): { label: string; description: string } { + if (step.nothingKnown) return { label: "Summary", description: NOTHING_KNOWN_DESCRIPTION }; if (step.passes.length === 0) return { label: "Original", description: ORIGINAL_DESCRIPTION }; const displayStep = step.passes.find(pass => !(pass in PASS_DESCRIPTIONS)); const description = step.passes @@ -143,11 +145,11 @@ function renderSelectedStep(errorId: string, previousIndex?: number): string { const state = vcStates.get(errorId); if (!state) return ""; - const { steps, translationTable, stepIndex, nothingKnown } = state; + const { steps, translationTable, stepIndex } = state; const current = steps[stepIndex]; // a change is shown from a step whose chain was shown - const previous = previousIndex === undefined || (nothingKnown && previousIndex === 0) ? undefined : steps[previousIndex]; - const implication = nothingKnown && stepIndex === 0 + const previous = previousIndex === undefined || steps[previousIndex].nothingKnown ? undefined : steps[previousIndex]; + const implication = current.nothingKnown ? `

${NOTHING_KNOWN}

` : previous ? `
${renderImplicationChange(previous.implication, current.implication, translationTable)}
` @@ -183,10 +185,12 @@ export function renderVCImplication( result: VCSimplificationResult ): string { if (!result?.implication) return renderHighlightedExpression(String(result)); - const steps = getVCSteps(result); + const derivedSteps = getVCSteps(result); // also when found states nothing, which a state error the verifier leaves uncategorized can have; - // the older steps stay a step back - const nothingKnown = error.errorCategory === "unknown" || statesNothing(steps[0].implication); + // the steps stay a step back + const steps = error.errorCategory === "unknown" || statesNothing(derivedSteps[0].implication) + ? [{ ...derivedSteps[0], passes: [], nothingKnown: true }, ...derivedSteps] + : derivedSteps; const errorId = encodeURIComponent(JSON.stringify([ error.file, @@ -195,7 +199,7 @@ export function renderVCImplication( error.message ])); const stepIndex = Math.min(vcStates.get(errorId)?.stepIndex ?? 0, steps.length - 1); - vcStates.set(errorId, { steps, translationTable: error.translationTable, stepIndex, nothingKnown }); + vcStates.set(errorId, { steps, translationTable: error.translationTable, stepIndex }); return /*html*/ `
From fbd6f8abe06e38a138c5a4740c10584ec3458179 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 12:55:23 +0000 Subject: [PATCH 7/9] Found: do not split a conjunct at an && inside a string literal Co-Authored-By: Claude Opus 5.5 --- .../src/webview/views/diagnostics/vc-changes.spec.ts | 6 ++++++ client/src/webview/views/diagnostics/vc-changes.ts | 10 ++++++++-- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts index 06527fb..40d366d 100644 --- a/client/src/webview/views/diagnostics/vc-changes.spec.ts +++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts @@ -37,4 +37,10 @@ describe('verification implications', () => { expect(document.querySelector('.vc-predicate-cell')?.textContent?.trim()).toBe('x == 1'); expect(document.querySelector('.vc-arrow')).toBeNull(); }); + it('puts each conjunct outside parentheses and strings on its own line', () => { + document.body.innerHTML = renderImplication({ ...conclusion, predicate: 'a > 0 && (b || c && d) && s == "x&&y"' }); + + expect(Array.from(document.querySelectorAll('.vc-predicate-cell'), cell => cell.textContent?.trim())) + .toEqual(['a > 0 &&', '(b || c && d) &&', 's == "x&&y"']); + }); }); diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 8d89909..451240b 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -36,13 +36,19 @@ function parseImplicationLine(line: string): { return { binder, type, predicate, hasNext: next === "next", isContinued: continued === "continued" }; } -// splits a predicate on the && outside parentheses +// splits a predicate on the && outside parentheses and string literals function splitConjuncts(predicate: string): string[] { const conjuncts: string[] = []; let depth = 0; let start = 0; + let inString = false; for (let i = 0; i < predicate.length; i++) { - if (predicate[i] === "(") depth++; + if (inString) { + if (predicate[i] === "\\") i++; + else if (predicate[i] === '"') inString = false; + } + else if (predicate[i] === '"') inString = true; + else if (predicate[i] === "(") depth++; else if (predicate[i] === ")") depth--; else if (depth === 0 && predicate.startsWith("&&", i)) { conjuncts.push(predicate.slice(start, i).trim()); From 44622f136dd6d5eb933e37424e5ad31d2c7591e6 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 12:58:31 +0000 Subject: [PATCH 8/9] Found: keep a fact on one line when an operator weaker than && is outside parentheses Co-Authored-By: Claude Opus 5.5 --- client/src/webview/views/diagnostics/vc-changes.spec.ts | 6 ++++++ client/src/webview/views/diagnostics/vc-changes.ts | 8 ++++++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts index 40d366d..ece89c8 100644 --- a/client/src/webview/views/diagnostics/vc-changes.spec.ts +++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts @@ -43,4 +43,10 @@ describe('verification implications', () => { expect(Array.from(document.querySelectorAll('.vc-predicate-cell'), cell => cell.textContent?.trim())) .toEqual(['a > 0 &&', '(b || c && d) &&', 's == "x&&y"']); }); + + it.each(['a || b && c', 'a && b --> c', 'a && b ? c : d'])('keeps %s on one line', predicate => { + document.body.innerHTML = renderImplication({ ...conclusion, predicate }); + + expect(document.querySelectorAll('.vc-predicate-cell')).toHaveLength(1); + }); }); diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 451240b..d5a97ec 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -11,6 +11,7 @@ const MIN_LINE_SIMILARITY = 0.3; const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu; const WHITESPACE_PATTERN = /^\s+$/u; const VC_LINE_SEPARATOR = "\t"; +const WEAKER_THAN_AND = ["||", "-->", "?"]; function hasBinder(node: VCImplication): boolean { return typeof node.name === "string" && node.name.length > 0; @@ -36,7 +37,8 @@ function parseImplicationLine(line: string): { return { binder, type, predicate, hasNext: next === "next", isContinued: continued === "continued" }; } -// splits a predicate on the && outside parentheses and string literals +// splits a predicate on the && outside parentheses and string literals, unless a weaker operator outside them +// (||, -->, ?:) would make its parts look like conjuncts of the whole predicate function splitConjuncts(predicate: string): string[] { const conjuncts: string[] = []; let depth = 0; @@ -50,7 +52,9 @@ function splitConjuncts(predicate: string): string[] { else if (predicate[i] === '"') inString = true; else if (predicate[i] === "(") depth++; else if (predicate[i] === ")") depth--; - else if (depth === 0 && predicate.startsWith("&&", i)) { + else if (depth > 0) continue; + else if (WEAKER_THAN_AND.some(operator => predicate.startsWith(operator, i))) return [predicate]; + else if (predicate.startsWith("&&", i)) { conjuncts.push(predicate.slice(start, i).trim()); start = i + 2; } From f6c39599141c16498529222f16996b5b35adbad7 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 19:18:12 +0000 Subject: [PATCH 9/9] Found: describe the Known Enum Values pass of the verifier Co-Authored-By: Claude Opus 5.5 --- client/src/webview/views/diagnostics/vc-implications.ts | 1 + 1 file changed, 1 insertion(+) diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 98f399a..bd2140e 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -29,6 +29,7 @@ const PASS_DESCRIPTIONS: Record = { "Substitution": "Replaced variables with the values they are equal to.", "Function Substitution": "Replaced calls with the values they are equal to.", "Binder": "Removed facts that say nothing, and conditions that Expected does not depend on.", + "Known Enum Values": "Decided comparisons of variables whose enum value is known.", "Folding": "Computed constant expressions.", "Arithmetic": "Simplified arithmetic.", "Logical": "Simplified logical operators.",