Show Simplification Pass Names

client/src/types/vc-implications.ts

@@ -8,4 +8,5 @@ export type VCImplication = {
 export type VCSimplificationResult = {
     implication: VCImplication;
     origin: VCSimplificationResult | null;
+    simplification: string | null;
 }

client/src/webview/styles.ts

@@ -324,13 +324,43 @@ export function getStyles(): string {
         }
         .vc-container {
             display: flex;
-            justify-content: space-between;
-            align-items: flex-start;
-            gap: 1rem;
+            flex-direction: column;
+            gap: 0.375rem;
             margin: 0.5rem 0;
         }
+        .vc-step-header {
+            display: flex;
+            align-items: center;
+            justify-content: space-between;
+            gap: 0.75rem;
+            min-width: 0;
+            padding-bottom: 0.25rem;
+            border-bottom: 1px solid var(--vscode-widget-border, var(--vscode-panel-border));
+            font-family: var(--vscode-font-family);
+            font-size: 0.8rem;
+            line-height: 1.25rem;
+        }
+        .vc-step-name {
+            min-width: 0;
+            overflow: hidden;
+            color: var(--vscode-descriptionForeground);
+            font-weight: 600;
+            text-overflow: ellipsis;
+            white-space: nowrap;
+        }
+        .vc-step-navigation {
+            display: inline-flex;
+            align-items: center;
+            gap: 0.25rem;
+            flex-shrink: 0;
+        }
+        .vc-step-position {
+            min-width: 2.5rem;
+            color: var(--vscode-descriptionForeground);
+            font-variant-numeric: tabular-nums;
+            text-align: right;
+        }
         .vc-chain {
-            flex: 1;
             display: flex;
             flex-direction: column;
             gap: 0.25rem;

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

@@ -28,6 +28,32 @@ function renderStepButton(errorId: string, step: "previous" | "next", disabled:
     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 {
+    const chronologicalStep = stepCount - index;
+    const simplification = current.simplification?.trim();
+    const label = simplification || "Original";
+
+    return /*html*/`
+        <div class="vc-step-header">
+            <span class="vc-step-name" title="${escapeHtml(label)}">${escapeHtml(label)}</span>
+            <div class="vc-step-navigation">
+                <span class="vc-step-position" aria-label="Simplification step ${chronologicalStep} of ${stepCount}">
+                    ${chronologicalStep}/${stepCount}
+                </span>
+                <div class="vc-step-controls">
+                    ${renderStepButton(errorId, "previous", index === stepCount - 1)}
+                    ${renderStepButton(errorId, "next", index === 0)}
+                </div>
+            </div>
+        </div>
+    `;
+}
+
 export function handleVCImplicationStepClick(target: Element): boolean {
     const errorId = target.getAttribute("data-error-id");
     const step = target.getAttribute("data-vc-step");
@@ -53,21 +79,19 @@ export function renderVCImplication(
         error.title,
         error.message
     ]));
-    const history: VCSimplificationResult[] = [];
+    const steps: VCSimplificationResult[] = [];
     for (let current: VCSimplificationResult | null = result; current; current = current.origin) {
-        history.push(current);
+        steps.push(current);
     }
 
-    const index = Math.min(stepIndexes.get(errorId) ?? 0, history.length - 1);
+    const index = Math.min(stepIndexes.get(errorId) ?? 0, steps.length - 1);
     stepIndexes.set(errorId, index);
+    const current = steps[index];
 
     return /*html*/ `
         <div class="container vc-container" data-error-id="${errorId}">
-            <div class="vc-chain">${renderImplication(history[index].implication)}</div>
-            <div class="vc-step-controls">
-                ${renderStepButton(errorId, "previous", index === history.length - 1)}
-                ${renderStepButton(errorId, "next", index === 0)}
-            </div>
+            ${steps.length > 1 ? renderStepHeader(errorId, current, index, steps.length) : ""}
+            <div class="vc-chain">${renderImplication(current.implication)}</div>
         </div>
     `;
 }

server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java

@@ -5,14 +5,16 @@
 /**
  * DTO for serializing a simplified VC and its complete predecessor states.
  */
-public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin) {
+public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin, String simplification) {
 
     public static VCSimplificationResultDTO from(VCSimplificationResult result) {
         if (result == null)
             return null;
 
         return new VCSimplificationResultDTO(
                 VCImplicationDTO.from(result.getImplication()),
-                from(result.getOrigin()));
+                from(result.getOrigin()),
+                result.getSimplification()
+        );
     }
 }