From 3888668ae65d56f92df8d9de5ec0bad4bf1858ea Mon Sep 17 00:00:00 2001
From: waleedcodes <110061477+waleedcodes@users.noreply.github.com>
Date: Fri, 9 Oct 2026 21:22:05 +0500
Subject: [PATCH 1/3] feat(ui): scaffold ProofCodeCodeLensProvider structure

---
 src/ui/codeLensProvider.ts | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 src/ui/codeLensProvider.ts

diff --git a/src/ui/codeLensProvider.ts b/src/ui/codeLensProvider.ts
new file mode 100644
index 0000000..656f840
--- /dev/null
+++ b/src/ui/codeLensProvider.ts
@@ -0,0 +1,24 @@
+import * as vscode from 'vscode';
+import { VerificationReport } from '../types';
+
+export class ProofCodeCodeLensProvider implements vscode.CodeLensProvider {
+  private report: VerificationReport | null = null;
+  private onDidChangeCodeLensesEmitter = new vscode.EventEmitter<void>();
+  public readonly onDidChangeCodeLenses = this.onDidChangeCodeLensesEmitter.event;
+
+  public setReport(report: VerificationReport | null): void {
+    this.report = report;
+    this.onDidChangeCodeLensesEmitter.fire();
+  }
+
+  public provideCodeLenses(
+    document: vscode.TextDocument,
+    _token: vscode.CancellationToken
+  ): vscode.CodeLens[] {
+    if (!this.report) return [];
+
+    const lenses: vscode.CodeLens[] = [];
+    const docPath = document.fileName.replace(/\\/g, '/');
+
+    // Find symbols in this file from impact analysis
+    const fileSymbols = this.report.impact.changedSymbols.filter(

From 24f259f845bd48783e4ecdb1a08691c92c08d0b5 Mon Sep 17 00:00:00 2001
From: waleedcodes <110061477+waleedcodes@users.noreply.github.com>
Date: Fri, 9 Oct 2026 21:22:05 +0500
Subject: [PATCH 2/3] feat(ui): match document functions against impact
 analysis symbols

---
 src/ui/codeLensProvider.ts | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/src/ui/codeLensProvider.ts b/src/ui/codeLensProvider.ts
index 656f840..f190e33 100644
--- a/src/ui/codeLensProvider.ts
+++ b/src/ui/codeLensProvider.ts
@@ -22,3 +22,32 @@ export class ProofCodeCodeLensProvider implements vscode.CodeLensProvider {
 
     // Find symbols in this file from impact analysis
     const fileSymbols = this.report.impact.changedSymbols.filter(
+      (s) => s.filePath.replace(/\\/g, '/') === docPath || docPath.endsWith(s.filePath)
+    );
+
+    // Find risks in this file
+    const fileRisks = this.report.risks.filter(
+      (r) => r.file.replace(/\\/g, '/') === docPath || docPath.endsWith(r.file)
+    );
+
+    for (const sym of fileSymbols) {
+      const callersCount = sym.callers.length;
+      const untestedCount = sym.callers.filter((c) => !c.hasTest).length;
+
+      // Find line number in document for this symbol
+      for (let i = 0; i < Math.min(document.lineCount, 500); i++) {
+        const lineText = document.lineAt(i).text;
+        if (
+          lineText.includes(`function ${sym.symbolName}`) ||
+          lineText.includes(`const ${sym.symbolName}`) ||
+          lineText.includes(`export async function ${sym.symbolName}`) ||
+          lineText.includes(`export function ${sym.symbolName}`)
+        ) {
+          const range = new vscode.Range(i, 0, i, lineText.length);
+          const relatedRisks = fileRisks.filter((r) => r.line >= i + 1 && r.line <= i + 15);
+
+          let title = `🛡️ ProofCode: ${callersCount} caller${callersCount === 1 ? '' : 's'}`;
+          if (untestedCount > 0) {
+            title += ` (${untestedCount} untested)`;
+          }
+          if (relatedRisks.length > 0) {

From 10ad48973d634d978df6a4f41b686451219305f8 Mon Sep 17 00:00:00 2001
From: waleedcodes <110061477+waleedcodes@users.noreply.github.com>
Date: Fri, 9 Oct 2026 21:22:05 +0500
Subject: [PATCH 3/3] feat(ui): render caller counts, risk indicators, and
 dashboard navigation commands

---
 src/ui/codeLensProvider.ts | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/ui/codeLensProvider.ts b/src/ui/codeLensProvider.ts
index f190e33..bb1bb5a 100644
--- a/src/ui/codeLensProvider.ts
+++ b/src/ui/codeLensProvider.ts
@@ -51,3 +51,21 @@ export class ProofCodeCodeLensProvider implements vscode.CodeLensProvider {
             title += ` (${untestedCount} untested)`;
           }
           if (relatedRisks.length > 0) {
+            title += ` | ⚠️ ${relatedRisks.length} risk${relatedRisks.length === 1 ? '' : 's'}`;
+          }
+
+          lenses.push(
+            new vscode.CodeLens(range, {
+              title,
+              command: 'proofcode.openDashboard',
+              tooltip: 'Click to open ProofCode Change Verification Dashboard'
+            })
+          );
+          break;
+        }
+      }
+    }
+
+    return lenses;
+  }
+}