From 7c61cb51eec26c236bd5493fedaa47fbf6631d6c Mon Sep 17 00:00:00 2001
From: John Dvorak <john@johnsdvorak.com>
Date: Thu, 21 May 2026 17:17:06 -0700
Subject: [PATCH] fix: propagate formula metrics into FOL diagnostic mapping

- mapFolDiagnostic now accepts optional metrics parameter
- adaptFOLResultToImhotepResult matches solver diagnostics to
  formula results by clauseId/formulaId and passes formula-level
  metrics (gap, dimensions, stacking context, overflow, etc.)
  into the diagnostics output
- Previously mapFolDiagnostic always returned metrics: {} and
  sourceRef: {}, making compound/quantified failures undiagnosable
  for users investigating contracts
---
 packages/imhotep-playwright/src/extraction.ts | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/packages/imhotep-playwright/src/extraction.ts b/packages/imhotep-playwright/src/extraction.ts
index 264e684..17edeaf 100644
--- a/packages/imhotep-playwright/src/extraction.ts
+++ b/packages/imhotep-playwright/src/extraction.ts
@@ -1518,7 +1518,10 @@ const PREDICATE_TO_DIAGNOSTIC_CODE: Record<string, DiagnosticCode> = {
   between: 'IMH_SIZE_BETWEEN_FAILED',
 }
 
-export function mapFolDiagnostic(d: { code: string; severity: 'error' | 'warning' | 'info'; category?: string; message: string; clauseId?: string }): ImhotepDiagnostic {
+export function mapFolDiagnostic(
+  d: { code: string; severity: 'error' | 'warning' | 'info'; category?: string; message: string; clauseId?: string },
+  metrics?: Record<string, number>,
+): ImhotepDiagnostic {
   let code = d.code as DiagnosticCode
   let message = d.message
   const fixHints: string[] = []
@@ -1606,7 +1609,7 @@ export function mapFolDiagnostic(d: { code: string; severity: 'error' | 'warning
     source: 'imhotep-solver',
     related: [],
     fixHints,
-    metrics: {},
+    metrics: metrics ?? {},
     sourceRef: {},
   }
 }
@@ -1931,8 +1934,14 @@ export function adaptFOLResultToImhotepResult(
   clauseId?: string,
   traceMeta?: TraceMetadata,
 ): ImhotepResult {
+  const formulaMetricsById = new Map<string, Record<string, number> | undefined>()
+  for (const fr of folResult.formulaResults) {
+    formulaMetricsById.set(fr.formulaId, fr.metrics)
+  }
+
   const diagnostics: ImhotepDiagnostic[] = folResult.diagnostics.map((d) => {
-    const mapped = mapFolDiagnostic(d)
+    const metrics = d.clauseId ? formulaMetricsById.get(d.clauseId) : undefined
+    const mapped = mapFolDiagnostic(d, metrics)
     if (traceMeta?.sourceRef) mapped.sourceRef = traceMeta.sourceRef
     if (traceMeta?.clauseLabel) mapped.clauseLabel = traceMeta.clauseLabel
     return mapped