List Found as facts and show only readable simplification steps

client/src/webview/styles.ts

@@ -600,6 +600,23 @@ export function getStyles(): string {
         .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;
+            gap: 0.25rem;
+            min-width: 0;
+        }
+        .vc-step-info {
+            display: inline-flex;
+            color: var(--vscode-descriptionForeground);
+            cursor: help;
+        }
         .vc-step-controls {
             display: inline-flex;
             align-items: center;

client/src/webview/views/diagnostics/vc-implications.spec.ts

@@ -0,0 +1,88 @@
+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: ReadonlyArray<readonly [string, string]>): VCImplication {
+    return rows.reduceRight<VCImplication | null>(
+        (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<VCSimplificationResult | null>(
+        (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(),
+        // each line of the chain, its binder and the lines its predicate is laid out on
+        lines: Array.from(document.querySelectorAll('.vc-line'), line => Array.from(
+            line.querySelectorAll('.vc-binder, .lj-line'), part => part.textContent?.replace(/\s+/gu, ' ').trim(),
+        ).join(' ')),
+    };
+}
+
+function previous(): void {
+    handleVCImplicationStepClick(document.querySelector('.vc-step-previous-btn')!);
+}
+
+afterEach(() => { document.body.innerHTML = ''; });
+
+describe('Found', () => {
+    it('shows every step of the verifier, each under its name with what changed in the tooltip', () => {
+        const states = 'tiling(p) == tilingNotExplicit && compression(p) == compressionNotExplicit';
+        render(derivation(
+            [null, chain(['#if_condition', '#if_condition'], ['p', states])],
+            ['Binder', chain(['#if_condition', 'true'], ['p', states])],
+            ['Binder', chain(['p', states])],
+            ['Relevant to Expected', chain(['p', 'compression(p) == compressionNotExplicit'])],
+        ));
+
+        expect(shown()).toEqual({
+            label: 'Relevant to Expected', info: 'Kept only the facts that Expected depends on, directly or through other facts.',
+            position: '4/4', lines: ['∀p compression(p) == compressionNotExplicit'],
+        });
+        previous();
+        expect(shown()).toMatchObject({
+            label: 'Simplified', info: 'Removed facts that say nothing, and conditions that Expected does not depend on.',
+            position: '3/4',
+        });
+        previous();
+        expect(shown()).toMatchObject({ label: 'Simplified', position: '2/4' });
+        previous();
+        expect(shown()).toMatchObject({
+            label: 'Original', info: 'What is known here, before simplifying.', position: '1/4',
+            lines: ['∀#if_condition #if_condition →', `∀p ${states}`],
+        });
+    });
+
+    it('says that nothing known proves Expected when the verifier could not prove it, with the steps a step back', () => {
+        render(
+            derivation([null, chain(['undoManager', 'undoManager == #getUndoManager_result'])]),
+            'expected `redoState(undoManager) == redoable` but could not prove it',
+        );
+
+        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.');
+        previous();
+        expect(document.querySelector('.vc-nothing-known')).toBeNull();
+        expect(shown()).toMatchObject({
+            label: 'Original', position: '1/2', lines: ['∀undoManager undoManager == #getUndoManager_result'],
+        });
+    });
+});

client/src/webview/views/diagnostics/vc-implications.ts

@@ -5,34 +5,64 @@ import { renderCodicon } from "../../icons";
 import { escapeHtml } from "../../utils";
 import { renderImplication, renderImplicationChange } from "./vc-changes";
 
+// A step of Found as it is shown: a step of the verifier, or a summary in front of the newest one, which says that
+// nothing known proves Expected instead of showing the chain
+type VCStep = VCSimplificationResult & { nothingKnown?: boolean };
+
 // state to preserve across re-renders
 type VCState = {
-    steps: VCSimplificationResult[];
+    steps: VCStep[];
     translationTable: TranslationTable;
     stepIndex: number;
 };
 
 const vcStates = new Map<string, VCState>(); // 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<string, string> = {
+    "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.",
+    "Constraint": "Removed facts that other facts already imply.",
+};
+const DISPLAY_STEP_DESCRIPTIONS: Record<string, string> = {
+    "Relevant to Expected": "Kept only the facts that Expected depends on, directly or through other facts.",
+};
+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.";
+// the end of the verifier's message when nothing it found is about what Expected constrains
+const NOT_PROVEN = / but could not prove it$/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 `<button class="vc-step-btn vc-step-${step}-btn" data-error-id="${errorId}" data-vc-step="${step}" title="${label}" aria-label="${label}" ${disabled ? "disabled" : ""} type="button">${renderCodicon(icon)}</button>`;
 }
 
-function renderStepHeader(
-    errorId: string,
-    current: VCSimplificationResult,
-    index: number,
-    stepCount: number,
-): string {
+function getStepLabel(step: VCStep): { label: string; description: string } {
+    if (step.nothingKnown) return { label: "Summary", description: NOTHING_KNOWN_DESCRIPTION };
+    const pass = step.simplification?.trim();
+    if (!pass) return { label: "Original", description: ORIGINAL_DESCRIPTION };
+    if (pass in PASS_DESCRIPTIONS) return { label: "Simplified", description: PASS_DESCRIPTIONS[pass] };
+    return { label: pass, description: DISPLAY_STEP_DESCRIPTIONS[pass] ?? "" };
+}
+
+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*/`
         <div class="vc-step-header">
-            <span class="vc-step-name" title="${label}">${label}</span>
+            <span class="vc-step-title">
+                <span class="vc-step-name" title="${escapeHtml(label)}">${escapeHtml(label)}</span>
+                ${description ? /*html*/`<span class="vc-step-info" title="${escapeHtml(description)}" aria-label="${escapeHtml(description)}">${renderCodicon("info")}</span>` : ""}
+            </span>
             <div class="vc-step-navigation">
                 <span class="vc-step-position" aria-label="Simplification step ${currStep} of ${stepCount}">
                     ${currStep}/${stepCount}
@@ -62,10 +92,13 @@ function renderSelectedStep(errorId: string, previousIndex?: number): string {
 
     const { steps, translationTable, stepIndex } = state;
     const current = steps[stepIndex];
-    const previous = previousIndex === undefined ? undefined : steps[previousIndex];
-    const implication = previous
-        ? `<div class="vc-chain">${renderImplicationChange(previous.implication, current.implication, translationTable)}</div>`
-        : `<div class="vc-chain">${renderImplication(current.implication, translationTable)}</div>`;
+    // a change is shown from a step whose chain was shown
+    const previous = previousIndex === undefined || steps[previousIndex].nothingKnown ? undefined : steps[previousIndex];
+    const implication = current.nothingKnown
+        ? `<p class="vc-nothing-known">${NOTHING_KNOWN}</p>`
+        : previous
+            ? `<div class="vc-chain">${renderImplicationChange(previous.implication, current.implication, translationTable)}</div>`
+            : `<div class="vc-chain">${renderImplication(current.implication, translationTable)}</div>`;
 
     return /*html*/`
         ${steps.length > 1 ? renderStepHeader(errorId, current, stepIndex, steps.length) : ""}
@@ -104,7 +137,9 @@ export function renderVCImplication(
         error.title,
         error.message
     ]));
-    const steps: VCSimplificationResult[] = [];
+    const steps: VCStep[] = [];
+    // when the verifier could not prove Expected, Found opens on a summary that says so, with the steps a step back
+    if (NOT_PROVEN.test(error.message)) steps.push({ ...result, nothingKnown: true });
     for (let current: VCSimplificationResult | null = result; current; current = current.origin) {
         steps.push(current);
     }