diff --git a/packages/imhotep-playwright/src/extraction.ts b/packages/imhotep-playwright/src/extraction.ts
new file mode 100644
index 0000000..6ffbce8
--- /dev/null
+++ b/packages/imhotep-playwright/src/extraction.ts
@@ -0,0 +1,1935 @@
+/**
+ * World extraction pipeline for Imhotep Playwright.
+ *
+ * Handles collecting geometry from the browser (fast path via page.evaluate
+ * or CDP protocol), building the solver-ready world, and evaluating FOL
+ * assertions against it.  Also includes compatibility reporting.
+ */
+
+import path from 'path'
+import fs from 'fs'
+import { createRequire } from 'module'
+import type { Page } from 'playwright'
+import {
+  FluentRelation,
+  FluentQuantifier,
+  parseSpec,
+  lowerToCanonical,
+} from 'imhotep-dsl'
+import type { FluentAssertion, CanonicalClauseDescriptor } from 'imhotep-dsl'
+import type {
+  ImhotepResult,
+  ClauseResult,
+  ImhotepDiagnostic,
+  DiagnosticCode,
+  NormalizedContract,
+  DomainValue,
+  SourceReference,
+} from 'imhotep-core'
+import { adaptCanonicalWorldToSolver } from 'imhotep-core'
+import type { DomainRef, FormulaNode } from 'imhotep-core'
+import {
+  computeGeometryCacheKey,
+  readCachedExtractionResult,
+  writeCachedExtractionResult,
+  getDefaultCacheDir,
+} from 'imhotep-core'
+import type { GeometryWorld } from 'imhotep-solver'
+import {
+  evaluateLogic,
+  registerDefaultPredicates,
+  getPredicateEvaluator,
+  getRequiredFactsForPredicate,
+  type DomainResolver,
+} from 'imhotep-solver'
+import { buildGeometryWorld } from './world-builder.js'
+import {
+  materializeSemanticSelector,
+  type SelectorPlan,
+} from './semantic-subjects.js'
+import {
+  CDPExtractor,
+  createSessionManager,
+  resolveSelector,
+  adaptSnapshotToCanonical,
+} from 'imhotep-cdp'
+import { lookupCode } from 'imhotep-reporter'
+import type { ImhotepUi, CompatibilityReport, CompatibilityCheck } from './public-types.js'
+
+const cjsRequire = createRequire(import.meta.url)
+
+const assertionStore = new WeakMap<ImhotepUi, (FluentRelation | FluentAssertion | FluentQuantifier)[]>()
+const specStore = new WeakMap<ImhotepUi, string[]>()
+
+const extractionPathStats = {
+  fastPathHits: 0,
+  cdpFallbacks: 0,
+}
+
+const pageCacheNamespace = new WeakMap<Page, string>()
+let pageCacheNamespaceCounter = 0
+
+function getPageCacheNamespace(page: Page): string {
+  const existing = pageCacheNamespace.get(page)
+  if (existing) return existing
+  const ns = `page-${++pageCacheNamespaceCounter}`
+  pageCacheNamespace.set(page, ns)
+  return ns
+}
+
+let extractionStatsHookInstalled = false
+let compatibilityWarningEmitted = false
+
+function maybeInstallExtractionStatsHook(): void {
+  if (extractionStatsHookInstalled) return
+  if (process.env.IMHOTEP_EXTRACT_STATS !== '1') return
+  extractionStatsHookInstalled = true
+  process.on('exit', () => {
+    const total = extractionPathStats.fastPathHits + extractionPathStats.cdpFallbacks
+    const fastPct = total > 0 ? ((extractionPathStats.fastPathHits / total) * 100).toFixed(1) : '0.0'
+    const cdpPct = total > 0 ? ((extractionPathStats.cdpFallbacks / total) * 100).toFixed(1) : '0.0'
+    console.log(
+      `[imhotep] extraction path stats: fast=${extractionPathStats.fastPathHits} (${fastPct}%), cdp=${extractionPathStats.cdpFallbacks} (${cdpPct}%), total=${total}`,
+    )
+  })
+}
+
+export {
+  assertionStore,
+  specStore,
+  extractionPathStats,
+  getPageCacheNamespace,
+  maybeInstallExtractionStatsHook,
+}
+
+// ---------------------------------------------------------------------------
+// Formula AST walkers
+// ---------------------------------------------------------------------------
+
+/**
+ * Walk a formula AST and collect all predicate names.
+ */
+export function collectPredicates(formula: FormulaNode): string[] {
+  const predicates: string[] = []
+  function walk(node: FormulaNode) {
+    if (node.kind === 'predicate') {
+      predicates.push((node as any).predicate)
+    } else if (node.kind === 'forall' || node.kind === 'exists') {
+      walk((node as any).body)
+    } else if (node.kind === 'and' || node.kind === 'or') {
+      walk((node as any).left)
+      walk((node as any).right)
+    } else if (node.kind === 'not') {
+      walk((node as any).operand)
+    } else if (node.kind === 'implies') {
+      walk((node as any).antecedent)
+      walk((node as any).consequent)
+    }
+  }
+  walk(formula)
+  return predicates
+}
+
+export function formulaNeedsCssLengthMetrics(formula: FormulaNode): boolean {
+  let needs = false
+  const scanValue = (value: unknown): void => {
+    if (needs || value == null) return
+    if (Array.isArray(value)) {
+      for (const item of value) scanValue(item)
+      return
+    }
+    if (typeof value !== 'object') return
+    const obj = value as Record<string, unknown>
+    if (typeof obj.unit === 'string') {
+      const unit = obj.unit.toLowerCase()
+      if (unit === 'ch' || unit === 'em' || unit === 'rem') {
+        needs = true
+        return
+      }
+    }
+    for (const child of Object.values(obj)) scanValue(child)
+  }
+  const walk = (node: FormulaNode): void => {
+    if (needs) return
+    if (node.kind === 'predicate') {
+      scanValue((node as any).options)
+      return
+    }
+    if (node.kind === 'forall' || node.kind === 'exists') {
+      walk((node as any).body)
+      return
+    }
+    if (node.kind === 'and' || node.kind === 'or') {
+      walk((node as any).left)
+      walk((node as any).right)
+      return
+    }
+    if (node.kind === 'not') {
+      walk((node as any).operand)
+      return
+    }
+    if (node.kind === 'implies') {
+      walk((node as any).antecedent)
+      walk((node as any).consequent)
+    }
+  }
+  walk(formula)
+  return needs
+}
+
+/**
+ * Compute the minimal set of facts required by a collection of formulas.
+ */
+export function computeRequiredFacts(formulas: FormulaNode[]): {
+  geometry: boolean
+  topology: boolean
+  styles: boolean
+  fragments: boolean
+} {
+  const facts = new Set<string>()
+  for (const formula of formulas) {
+    const predicates = collectPredicates(formula)
+    for (const p of predicates) {
+      const required = getRequiredFactsForPredicate(p)
+      for (const f of required) {
+        facts.add(f)
+      }
+    }
+  }
+
+  const needsCssLengthMetrics = formulas.some((formula) => formulaNeedsCssLengthMetrics(formula))
+
+  return {
+    geometry: true, // Always required for subject resolution
+    topology: facts.has('topology.stackingContextOf') || facts.has('subject.clipChain'),
+    styles: facts.has('styles') || facts.has('computedStyle') || needsCssLengthMetrics,
+    fragments: facts.has('subject.fragmentCount') || facts.has('subject.firstFragmentId'),
+  }
+}
+
+export function usesLayoutSpace(formula: FormulaNode): boolean {
+  let found = false
+  function walk(node: FormulaNode) {
+    if (found) return
+    if (node.kind === 'predicate') {
+      const options = (node as any).options
+      if (options?.space === 'layout') {
+        found = true
+      }
+    } else if (node.kind === 'forall' || node.kind === 'exists') {
+      walk((node as any).body)
+    } else if (node.kind === 'and' || node.kind === 'or') {
+      walk((node as any).left)
+      walk((node as any).right)
+    } else if (node.kind === 'not') {
+      walk((node as any).operand)
+    } else if (node.kind === 'implies') {
+      walk((node as any).antecedent)
+      walk((node as any).consequent)
+    }
+  }
+  walk(formula)
+  return found
+}
+
+// ---------------------------------------------------------------------------
+// ch Width Measurement
+// ---------------------------------------------------------------------------
+
+export async function measureChWidthsByPlan(
+  playwrightPage: Page,
+  plans: SelectorPlan[],
+): Promise<Map<string, number[]>> {
+  const measured = await playwrightPage.evaluate((inputPlans: Array<{ key: string; queries: string[] }>) => {
+    const out: Array<[string, number[]]> = []
+    const canvas = document.createElement('canvas')
+    const ctx = canvas.getContext('2d')
+    const fallbackMeasure = (el: HTMLElement): number => {
+      const probe = document.createElement('span')
+      probe.textContent = '0'
+      probe.style.position = 'absolute'
+      probe.style.visibility = 'hidden'
+      probe.style.left = '-99999px'
+      probe.style.top = '0'
+      const cs = window.getComputedStyle(el)
+      probe.style.font = cs.font
+      probe.style.letterSpacing = cs.letterSpacing
+      probe.style.fontKerning = cs.fontKerning as any
+      probe.style.fontVariant = cs.fontVariant
+      document.body.appendChild(probe)
+      const w = probe.getBoundingClientRect().width
+      probe.remove()
+      return w
+    }
+
+    const measure = (el: HTMLElement): number => {
+      const cs = window.getComputedStyle(el)
+      if (ctx) {
+        ctx.font = cs.font
+        const w = ctx.measureText('0').width
+        if (Number.isFinite(w) && w > 0) return w
+      }
+      const fallback = fallbackMeasure(el)
+      if (Number.isFinite(fallback) && fallback > 0) return fallback
+      const fontSize = Number.parseFloat(cs.fontSize)
+      return Number.isFinite(fontSize) && fontSize > 0 ? fontSize * 0.5 : 8
+    }
+
+    for (const plan of inputPlans) {
+      const widths: number[] = []
+      for (const query of plan.queries) {
+        const nodes = document.querySelectorAll(query)
+        for (let i = 0; i < nodes.length; i++) {
+          widths.push(measure(nodes[i] as HTMLElement))
+        }
+      }
+      out.push([plan.key, widths])
+    }
+    return out
+  }, plans)
+  return new Map<string, number[]>(measured)
+}
+
+export function attachMeasuredChWidths(
+  world: GeometryWorld,
+  selectorToIds: Map<string, number[]>,
+  chWidthsBySelector: Map<string, number[]>,
+): void {
+  const worldAny = world as any
+  const styles = worldAny.styles as {
+    subjectId?: number[]
+    fontSize?: number[]
+    chWidth?: number[]
+  } | undefined
+  if (!styles) return
+  const bySubject = new Map<number, number>()
+  for (const [key, ids] of selectorToIds) {
+    const widths = chWidthsBySelector.get(key)
+    if (!widths || widths.length === 0) continue
+    const n = Math.min(ids.length, widths.length)
+    for (let i = 0; i < n; i++) {
+      const subjectId = ids[i]
+      const width = Number(widths[i])
+      if (!Number.isFinite(subjectId) || !Number.isFinite(width) || width <= 0) continue
+      if (!bySubject.has(subjectId)) bySubject.set(subjectId, width)
+    }
+  }
+  if (bySubject.size === 0) return
+
+  const styleSubjectIds = styles.subjectId
+  if (styleSubjectIds && styleSubjectIds.length > 0) {
+    const chWidth = new Array(styleSubjectIds.length)
+    for (let i = 0; i < styleSubjectIds.length; i++) {
+      const subjectId = Number(styleSubjectIds[i])
+      const measured = bySubject.get(subjectId)
+      if (measured !== undefined) {
+        chWidth[i] = measured
+        continue
+      }
+      const fs = Number(styles.fontSize?.[i])
+      chWidth[i] = Number.isFinite(fs) && fs > 0 ? fs * 0.5 : 8
+    }
+    styles.chWidth = chWidth
+    return
+  }
+
+  const subjectIds = world.subjects?.ids ?? []
+  const chWidth = new Array(subjectIds.length)
+  for (let i = 0; i < subjectIds.length; i++) {
+    const measured = bySubject.get(subjectIds[i])
+    if (measured !== undefined) {
+      chWidth[i] = measured
+      continue
+    }
+    const fs = Number(styles.fontSize?.[i])
+    chWidth[i] = Number.isFinite(fs) && fs > 0 ? fs * 0.5 : 8
+  }
+  styles.chWidth = chWidth
+}
+
+// ---------------------------------------------------------------------------
+// Fast Geometry Extraction
+// ---------------------------------------------------------------------------
+
+export async function extractWorldFastGeometry(
+  playwrightPage: Page,
+  selectors: string[],
+  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean },
+): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
+  interface FastExtractedElement {
+    tagName: string
+    rect: { x: number; y: number; width: number; height: number }
+    fragments?: Array<{ left: number; top: number; right: number; bottom: number }>
+    transform?: { matrix: number[]; originX: number; originY: number }
+    style?: {
+      display: string
+      position: string
+      overflowX: string
+      overflowY: string
+      visibility: string
+      pointerEvents: string
+      opacity: number
+      zIndex: string
+      lineHeight: number
+      fontFamily: string
+      fontSize: number
+      fontWeight: number
+      chWidth: number
+    }
+  }
+  interface FastExtractedPayload {
+    elements: FastExtractedElement[]
+    selectorToIds: Array<[string, number[]]>
+  }
+
+  const selectorPlans: SelectorPlan[] = await Promise.all(
+    selectors.map(async (key, i) => {
+      const queries = await materializeSemanticSelector(playwrightPage, key, i)
+      return { key, queries }
+    }),
+  )
+
+  try {
+    const extracted = await playwrightPage.evaluate(({ plans, needs }: any) => {
+      const elements: FastExtractedElement[] = []
+      const selectorToIds: Array<[string, number[]]> = []
+
+      for (const plan of plans) {
+        const ids: number[] = []
+        for (const query of plan.queries) {
+          const matches = document.querySelectorAll(query)
+          for (let i = 0; i < matches.length; i++) {
+            const el = matches[i] as HTMLElement
+            const rect = el.getBoundingClientRect()
+            const subjectId = elements.length + 1
+            elements.push({
+              tagName: el.tagName.toLowerCase(),
+              rect: {
+                x: rect.left,
+                y: rect.top,
+                width: rect.width,
+                height: rect.height,
+              },
+              ...(needs.fragments
+                ? {
+                    fragments: Array.from(el.getClientRects()).map((r) => ({
+                      left: r.left,
+                      top: r.top,
+                      right: r.right,
+                      bottom: r.bottom,
+                    })),
+                  }
+                : {}),
+              ...(needs.styles || needs.geometry
+                ? {
+                    transform: (() => {
+                      const cs = window.getComputedStyle(el)
+                      const t = cs.transform
+                      let matrix = [1, 0, 0, 1, 0, 0]
+                      if (t && t !== 'none') {
+                        const m = t.match(/matrix\(([^)]+)\)/)
+                        if (m) matrix = m[1].split(',').map(Number)
+                      }
+                      const origin = cs.transformOrigin.split(' ').map(parseFloat)
+                      return { matrix, originX: origin[0] || 0, originY: origin[1] || 0 }
+                    })(),
+                  }
+                : {}),
+              ...(needs.styles
+                ? {
+                    style: (() => {
+                      const cs = window.getComputedStyle(el)
+                      const canvas = document.createElement('canvas')
+                      const ctx = canvas.getContext('2d')
+                      let chWidth = 0
+                      if (ctx) {
+                        ctx.font = cs.font
+                        chWidth = ctx.measureText('0').width
+                      }
+                      if (!(Number.isFinite(chWidth) && chWidth > 0)) {
+                        const probe = document.createElement('span')
+                        probe.textContent = '0'
+                        probe.style.position = 'absolute'
+                        probe.style.visibility = 'hidden'
+                        probe.style.left = '-99999px'
+                        probe.style.top = '0'
+                        probe.style.font = cs.font
+                        document.body.appendChild(probe)
+                        chWidth = probe.getBoundingClientRect().width
+                        probe.remove()
+                      }
+                      return {
+                        display: cs.display,
+                        position: cs.position,
+                        overflowX: cs.overflowX,
+                        overflowY: cs.overflowY,
+                        visibility: cs.visibility,
+                        pointerEvents: cs.pointerEvents,
+                        opacity: Number.parseFloat(cs.opacity) || 1,
+                        zIndex: cs.zIndex,
+                        lineHeight: Number.parseFloat(cs.lineHeight) || 0,
+                        fontFamily: cs.fontFamily || '',
+                        fontSize: Number.parseFloat(cs.fontSize) || 0,
+                        fontWeight: Number.parseInt(cs.fontWeight, 10) || 400,
+                        chWidth: Number.isFinite(chWidth) && chWidth > 0
+                          ? chWidth
+                          : (Number.parseFloat(cs.fontSize) || 16) * 0.5,
+                      }
+                    })(),
+                  }
+                : {}),
+            })
+            ids.push(subjectId)
+          }
+        }
+        selectorToIds.push([plan.key, ids])
+      }
+
+      return { elements, selectorToIds }
+    }, {
+      plans: selectorPlans,
+      needs: {
+        fragments: requiredFacts?.fragments === true,
+        styles: requiredFacts?.styles === true,
+        geometry: requiredFacts?.geometry !== false,
+      },
+    }) as FastExtractedPayload
+
+    const world = buildGeometryWorld(extracted.elements) as GeometryWorld
+    const worldAny = world as any
+
+    if (requiredFacts?.fragments) {
+      const fragmentId: number[] = []
+      const subjectId: number[] = []
+      const fragmentKind: number[] = []
+      const boxLeft: number[] = []
+      const boxTop: number[] = []
+      const boxRight: number[] = []
+      const boxBottom: number[] = []
+      const lineIndex: number[] = []
+      const flowIndex: number[] = []
+      const parentFragmentId: number[] = []
+
+      const firstFragmentIds: number[] = Array.from({ length: extracted.elements.length }, () => 0)
+      const fragmentCounts: number[] = Array.from({ length: extracted.elements.length }, () => 0)
+
+      for (let i = 0; i < extracted.elements.length; i++) {
+        const frags = extracted.elements[i].fragments ?? []
+        if (frags.length > 0) {
+          firstFragmentIds[i] = fragmentId.length
+          fragmentCounts[i] = frags.length
+        }
+        for (let j = 0; j < frags.length; j++) {
+          const f = frags[j]
+          fragmentId.push(fragmentId.length)
+          subjectId.push(i + 1)
+          fragmentKind.push(1)
+          boxLeft.push(f.left)
+          boxTop.push(f.top)
+          boxRight.push(f.right)
+          boxBottom.push(f.bottom)
+          lineIndex.push(j)
+          flowIndex.push(0)
+          parentFragmentId.push(0)
+        }
+      }
+
+      worldAny.fragments = {
+        fragmentId,
+        subjectId,
+        fragmentKind,
+        boxLeft,
+        boxTop,
+        boxRight,
+        boxBottom,
+        lineIndex,
+        flowIndex,
+        parentFragmentId,
+      }
+      worldAny.subjects.firstFragmentId = firstFragmentIds
+      worldAny.subjects.fragmentCount = fragmentCounts
+    }
+
+    if (requiredFacts?.geometry) {
+      const transformId: number[] = []
+      const transformSubjectId: number[] = []
+      const matrixStart: number[] = []
+      const matrixLength: number[] = []
+      const originX: number[] = []
+      const originY: number[] = []
+      const matrices: number[] = []
+
+      for (let i = 0; i < extracted.elements.length; i++) {
+        const t = extracted.elements[i].transform
+        if (!t) continue
+        const start = matrices.length
+        matrices.push(...t.matrix)
+        transformId.push(transformId.length)
+        transformSubjectId.push(i + 1)
+        matrixStart.push(start)
+        matrixLength.push(t.matrix.length)
+        originX.push(t.originX)
+        originY.push(t.originY)
+      }
+
+      worldAny.transforms = {
+        transformId,
+        subjectId: transformSubjectId,
+        matrixStart,
+        matrixLength,
+        originX,
+        originY,
+      }
+      worldAny.matrices = { values: matrices }
+    }
+
+    if (requiredFacts?.styles) {
+      const strings = worldAny.strings?.values ?? []
+      const stringToId = new Map<string, number>()
+      for (let i = 0; i < strings.length; i++) stringToId.set(strings[i], i)
+      const intern = (value: string): number => {
+        const existing = stringToId.get(value)
+        if (existing !== undefined) return existing
+        const id = strings.length
+        strings.push(value)
+        stringToId.set(value, id)
+        return id
+      }
+
+      const styleSubjectId: number[] = []
+      const display: number[] = []
+      const position: number[] = []
+      const zIndexKind: number[] = []
+      const zIndexValue: number[] = []
+      const overflowX: number[] = []
+      const overflowY: number[] = []
+      const opacity: number[] = []
+      const visibility: number[] = []
+      const containFlags: number[] = []
+      const pointerEvents: number[] = []
+      const lineHeight: number[] = []
+      const fontFamilyStringId: number[] = []
+      const fontSize: number[] = []
+      const fontWeight: number[] = []
+      const chWidth: number[] = []
+
+      for (let i = 0; i < extracted.elements.length; i++) {
+        const s = extracted.elements[i].style
+        if (!s) continue
+        styleSubjectId.push(i + 1)
+        display.push(intern(s.display))
+        position.push(intern(s.position))
+        overflowX.push(intern(s.overflowX))
+        overflowY.push(intern(s.overflowY))
+        visibility.push(intern(s.visibility))
+        pointerEvents.push(intern(s.pointerEvents))
+        zIndexKind.push(s.zIndex === 'auto' ? 0 : 1)
+        zIndexValue.push(s.zIndex === 'auto' ? 0 : Number.parseInt(s.zIndex, 10) || 0)
+        opacity.push(s.opacity)
+        containFlags.push(0)
+        lineHeight.push(s.lineHeight)
+        fontFamilyStringId.push(intern(s.fontFamily))
+        fontSize.push(s.fontSize)
+        fontWeight.push(s.fontWeight)
+        chWidth.push(s.chWidth)
+      }
+
+      worldAny.strings = { values: strings }
+      worldAny.styles = {
+        subjectId: styleSubjectId,
+        display,
+        position,
+        zIndexKind,
+        zIndexValue,
+        overflowX,
+        overflowY,
+        opacity,
+        visibility,
+        containFlags,
+        pointerEvents,
+        lineHeight,
+        fontFamilyStringId,
+        fontSize,
+        fontWeight,
+        chWidth,
+      }
+    }
+
+    const selectorToIds = new Map<string, number[]>(extracted.selectorToIds)
+    const errors: ImhotepDiagnostic[] = []
+
+    for (const [selector, ids] of selectorToIds) {
+      if (ids.length === 0 && !selector.startsWith('$')) {
+        errors.push({
+          code: 'IMH_SELECTOR_ZERO_MATCHES',
+          severity: 'error',
+          category: 'extraction-error',
+          message: `Selector "${selector}" resolved to 0 elements.`,
+          source: 'imhotep-playwright',
+          related: [],
+          fixHints: [
+            `Check that "${selector}" is a valid CSS selector or semantic reference.`,
+            `Use ui.extract('${selector}') to verify the selector resolves to at least one element.`,
+          ],
+          metrics: {},
+          sourceRef: { selector },
+        })
+      }
+    }
+
+    return { world, selectorToIds, errors }
+  } finally {
+    await playwrightPage.evaluate(() => {
+      const nodes = Array.from(document.querySelectorAll('[data-imhotep-runtime-id]'))
+      for (const el of nodes) {
+        el.removeAttribute('data-imhotep-runtime-id')
+      }
+    }).catch(() => {})
+  }
+}
+
+// ---------------------------------------------------------------------------
+// CDP Extraction
+// ---------------------------------------------------------------------------
+
+export async function extractWorldCdp(
+  playwrightPage: Page,
+  selectors: string[],
+  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean },
+): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
+  const errors: ImhotepDiagnostic[] = []
+  const selectorToNodeIds = new Map<string, number[]>()
+
+  const selectorPlans: SelectorPlan[] = await Promise.all(
+    selectors.map(async (key, i) => {
+      const queries = await materializeSemanticSelector(playwrightPage, key, i)
+      return { key, queries }
+    }),
+  )
+
+  const sessionManager = createSessionManager(playwrightPage)
+  try {
+    await sessionManager.enableDomain('DOM')
+
+    const session = sessionManager.getSession()
+    await session.send('DOM.getDocument', { depth: -1 })
+
+    const allQueries = selectorPlans.flatMap((plan) =>
+      plan.queries.map((query) => ({ key: plan.key, query })),
+    )
+    const allMatches = await Promise.all(
+      allQueries.map(({ query }) => resolveSelector(sessionManager, query)),
+    )
+    const resolvedSubjects: Array<{ id: string; selector: string; nodeId: number; backendNodeId: number }> = []
+    for (let i = 0; i < allQueries.length; i++) {
+      const { key, query } = allQueries[i]
+      const matches = allMatches[i]
+      const ids = selectorToNodeIds.get(key) ?? []
+      for (const m of matches) {
+        ids.push(m.backendNodeId)
+        resolvedSubjects.push({
+          id: `sel_${resolvedSubjects.length}`,
+          selector: query,
+          nodeId: m.nodeId,
+          backendNodeId: m.backendNodeId,
+        })
+      }
+      selectorToNodeIds.set(key, ids)
+    }
+    for (const plan of selectorPlans) {
+      const ids = selectorToNodeIds.get(plan.key) ?? []
+      if (ids.length === 0) {
+        errors.push({
+          code: 'IMH_SELECTOR_ZERO_MATCHES',
+          severity: 'error',
+          category: 'extraction-error',
+          message: `Selector "${plan.key}" resolved to 0 elements.`,
+          source: 'imhotep-cdp',
+          related: [],
+          fixHints: [
+            `Check that "${plan.key}" is a valid CSS selector or semantic reference.`,
+            `Use ui.extract('${plan.key}') to verify the selector resolves to at least one element.`,
+          ],
+          metrics: {},
+          sourceRef: { selector: plan.key },
+        })
+      }
+    }
+
+    const extractor = new CDPExtractor(sessionManager)
+    const cdpRequest = {
+      requestId: `req_${Date.now()}`,
+      sceneTarget: { pageRef: playwrightPage as unknown, url: playwrightPage.url?.() ?? '' },
+      env: {
+        viewportWidth: 0,
+        viewportHeight: 0,
+        colorScheme: 'light',
+        pointer: 'fine',
+      },
+      subjects: resolvedSubjects,
+      requiredFacts: requiredFacts ?? {
+        geometry: true,
+        fragments: true,
+        styles: true,
+        topology: true,
+      },
+    }
+    const cdpResponse = await extractor.extract(cdpRequest)
+    if (cdpResponse.status === 'error') {
+      throw new Error('CDP extraction failed for relational evaluation')
+    }
+
+    const snapshot = cdpResponse.snapshots[0]
+    const canonical = adaptSnapshotToCanonical(snapshot)
+    const world = adaptCanonicalWorldToSolver(canonical as any) as GeometryWorld
+    ;(world as any).styles = {
+      subjectId: Array.from(canonical.styles.subjectId),
+      lineHeight: Array.from(canonical.styles.lineHeight),
+      fontFamilyStringId: Array.from(canonical.styles.fontFamilyStringId),
+      fontSize: Array.from(canonical.styles.fontSize),
+      fontWeight: Array.from(canonical.styles.fontWeight),
+    }
+
+    const selectorToIds = new Map<string, number[]>()
+    for (const [selectorKey, nodeIds] of selectorToNodeIds) {
+      const idSet = new Set(nodeIds)
+      const matches: number[] = []
+      for (let i = 0; i < world.subjects.ids.length; i++) {
+        const domNodeId = world.subjects.domNodeId[i]
+        if (idSet.has(domNodeId)) {
+          matches.push(world.subjects.ids[i])
+        }
+      }
+      selectorToIds.set(selectorKey, matches)
+    }
+
+    return { world, selectorToIds, errors }
+  } finally {
+    await playwrightPage.evaluate(() => {
+      const nodes = Array.from(document.querySelectorAll('[data-imhotep-runtime-id]'))
+      for (const el of nodes) {
+        el.removeAttribute('data-imhotep-runtime-id')
+      }
+    }).catch(() => {})
+    await sessionManager.detach()
+  }
+}
+
+// ---------------------------------------------------------------------------
+// Orchestrator
+// ---------------------------------------------------------------------------
+
+export async function extractWorld(
+  playwrightPage: Page,
+  selectors: string[],
+  cacheDir?: string | null,
+  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean },
+  allowFastGeometry = false,
+): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
+  async function resolveViewport(): Promise<{ width: number; height: number }> {
+    const direct = typeof playwrightPage.viewportSize === 'function' ? playwrightPage.viewportSize() : null
+    if (direct && direct.width > 0 && direct.height > 0) {
+      return { width: direct.width, height: direct.height }
+    }
+    try {
+      const measured = await playwrightPage.evaluate(() => ({
+        width: window.innerWidth || document.documentElement?.clientWidth || 0,
+        height: window.innerHeight || document.documentElement?.clientHeight || 0,
+      }))
+      return {
+        width: Number.isFinite(measured?.width) ? Number(measured.width) : 0,
+        height: Number.isFinite(measured?.height) ? Number(measured.height) : 0,
+      }
+    } catch {
+      return { width: 0, height: 0 }
+    }
+  }
+
+  maybeInstallExtractionStatsHook()
+  const filteredSelectors = selectors.filter((s) => typeof s === 'string' && s.length > 0)
+  const pageUrl = playwrightPage.url?.() ?? ''
+  const viewport = await resolveViewport()
+  const env = {
+    viewportWidth: viewport.width,
+    viewportHeight: viewport.height,
+    colorScheme: 'light',
+    pointer: 'fine',
+  }
+
+  const resolvedCacheDir = cacheDir === null ? null : (cacheDir ?? getDefaultCacheDir())
+  const cacheNamespace = getPageCacheNamespace(playwrightPage)
+  const cacheSelectors = requiredFacts
+    ? [...filteredSelectors, `__imhotep_facts:${requiredFacts.geometry ? 'g' : ''}${requiredFacts.topology ? 't' : ''}${requiredFacts.styles ? 's' : ''}${requiredFacts.fragments ? 'f' : ''}:${allowFastGeometry ? 'fast' : 'cdp'}`, `__imhotep_page_ns:${cacheNamespace}`]
+    : [...filteredSelectors, `__imhotep_page_ns:${cacheNamespace}`]
+
+  if (resolvedCacheDir !== null) {
+    const cacheKey = computeGeometryCacheKey(pageUrl, cacheSelectors, env)
+    const cached = await readCachedExtractionResult(resolvedCacheDir, cacheKey)
+    if (cached) {
+      return {
+        world: cached.world as unknown as GeometryWorld,
+        selectorToIds: cached.selectorToIds,
+        errors: cached.errors as unknown as ImhotepDiagnostic[],
+      }
+    }
+  }
+
+  const useFastGeometry = allowFastGeometry
+    && requiredFacts?.geometry === true
+    && requiredFacts.topology === false
+
+  const result = useFastGeometry
+    ? await extractWorldFastGeometry(playwrightPage, filteredSelectors, requiredFacts)
+    : await extractWorldCdp(playwrightPage, filteredSelectors, requiredFacts)
+
+  ;(result.world as any).env = {
+    ...(result.world as any).env,
+    viewportWidth: env.viewportWidth,
+    viewportHeight: env.viewportHeight,
+  }
+
+  if (requiredFacts?.styles) {
+    try {
+      const plans: SelectorPlan[] = await Promise.all(
+        filteredSelectors.map(async (key, i) => {
+          const queries = await materializeSemanticSelector(playwrightPage, key, i)
+          return { key, queries }
+        }),
+      )
+      const chWidthsBySelector = await measureChWidthsByPlan(playwrightPage, plans)
+      attachMeasuredChWidths(result.world, result.selectorToIds, chWidthsBySelector)
+    } catch {
+      // Best effort only; solver falls back to font-size heuristic.
+    }
+  }
+
+  if (useFastGeometry) {
+    extractionPathStats.fastPathHits += 1
+  } else {
+    extractionPathStats.cdpFallbacks += 1
+  }
+
+  if (resolvedCacheDir !== null) {
+    const cacheKey = computeGeometryCacheKey(pageUrl, cacheSelectors, env)
+    await writeCachedExtractionResult(
+      resolvedCacheDir,
+      cacheKey,
+      result.world as unknown as import('imhotep-core').GeometryWorld,
+      result.selectorToIds,
+      result.errors as any,
+    )
+  }
+
+  return result
+}
+
+// ---------------------------------------------------------------------------
+// Domain Resolver
+// ---------------------------------------------------------------------------
+
+export class SelectorDomainResolver implements DomainResolver {
+  private domains = new Map<string, DomainValue>()
+
+  register(selector: string, subjectIds: number[]) {
+    this.domains.set(selector, {
+      domainId: `dom_${selector}`,
+      subjectIds: new Uint32Array(subjectIds),
+      provenance: `elements(${selector})`,
+      closed: true,
+    })
+  }
+
+  resolve(domain: DomainRef): DomainValue | undefined {
+    return this.domains.get(domain.selector ?? domain.domain)
+  }
+}
+
+// ---------------------------------------------------------------------------
+// Canonical Clause → Formula Compilation
+// ---------------------------------------------------------------------------
+
+export function compileCanonicalClauseToFormula(clause: CanonicalClauseDescriptor): FormulaNode {
+  const extended = clause as CanonicalClauseDescriptor & {
+    space?: 'layout' | 'visual'
+    options?: Record<string, unknown>
+  }
+  const subjectVar = { type: 'VariableRef' as const, name: '$subject' }
+  const referenceVar = { type: 'VariableRef' as const, name: '$reference' }
+
+  const options: Record<string, unknown> = {}
+  if (clause.bounds?.minGap !== undefined) options.minGap = clause.bounds.minGap
+  if (clause.bounds?.maxGap !== undefined) options.maxGap = clause.bounds.maxGap
+  if (clause.tolerance?.value !== undefined) options.tolerance = clause.tolerance.value
+  if (extended.space) options.space = extended.space
+  if (extended.options) {
+    for (const [k, v] of Object.entries(extended.options)) {
+      options[k] = v
+    }
+  }
+
+  let body: FormulaNode
+
+  if (clause.relation === 'between') {
+    const minVal = extended.options?.min as number | undefined
+    const maxVal = extended.options?.max as number | undefined
+    const atLeastOpts: Record<string, unknown> = {}
+    const atMostOpts: Record<string, unknown> = {}
+    if (extended.options?.dimension !== undefined) {
+      atLeastOpts.dimension = extended.options.dimension
+      atMostOpts.dimension = extended.options.dimension
+    }
+    body = {
+      type: 'FormulaNode',
+      kind: 'and',
+      left: {
+        type: 'FormulaNode',
+        kind: 'predicate',
+        predicate: 'atLeast',
+        args: [subjectVar],
+        ...(minVal !== undefined ? { options: { ...atLeastOpts, value: minVal } } : { options: atLeastOpts }),
+      } as FormulaNode,
+      right: {
+        type: 'FormulaNode',
+        kind: 'predicate',
+        predicate: 'atMost',
+        args: [subjectVar],
+        ...(maxVal !== undefined ? { options: { ...atMostOpts, value: maxVal } } : { options: atMostOpts }),
+      } as FormulaNode,
+    }
+  } else if (clause.relation === 'separatedFrom') {
+    const overlapsOpts: Record<string, unknown> = { ...options }
+    body = {
+      type: 'FormulaNode',
+      kind: 'not',
+      operand: {
+        type: 'FormulaNode',
+        kind: 'predicate',
+        predicate: 'overlaps',
+        args: [subjectVar, referenceVar],
+        ...(Object.keys(overlapsOpts).length > 0 ? { options: overlapsOpts } : {}),
+      } as FormulaNode,
+    }
+  } else {
+    const unaryPredicate = clause.relation === 'atLeast'
+      || clause.relation === 'atMost'
+      || clause.relation === 'aspectRatio'
+
+    body = {
+      type: 'FormulaNode',
+      kind: 'predicate',
+      predicate: clause.relation,
+      args: unaryPredicate ? [subjectVar] : [subjectVar, referenceVar],
+      ...(Object.keys(options).length > 0 ? { options } : {}),
+    } as FormulaNode
+
+    if ((clause.flags & 8) !== 0 && !unaryPredicate) {
+      body = {
+        type: 'FormulaNode',
+        kind: 'and',
+        left: body,
+        right: {
+          type: 'FormulaNode',
+          kind: 'predicate',
+          predicate: 'inStackingContext',
+          args: [subjectVar, referenceVar],
+        },
+      }
+    }
+  }
+
+  if (clause.negated) {
+    body = {
+      type: 'FormulaNode',
+      kind: 'not',
+      operand: body,
+    }
+  }
+
+  const subjectBinding = {
+    type: 'TupleBinding' as const,
+    variables: ['$subject'],
+    domain: { type: 'DomainRef' as const, domain: 'elements', selector: clause.subject },
+  }
+  const referenceBinding = {
+    type: 'TupleBinding' as const,
+    variables: ['$reference'],
+    domain: { type: 'DomainRef' as const, domain: 'elements', selector: clause.reference },
+  }
+
+  const isUnary = clause.relation === 'atLeast'
+    || clause.relation === 'atMost'
+    || clause.relation === 'between'
+    || clause.relation === 'aspectRatio'
+
+  if (isUnary) {
+    return {
+      type: 'FormulaNode',
+      kind: 'forall',
+      bindings: [subjectBinding],
+      body,
+    }
+  }
+
+  if (clause.quantifier === 'any') {
+    return {
+      type: 'FormulaNode',
+      kind: 'exists',
+      bindings: [subjectBinding],
+      body: {
+        type: 'FormulaNode',
+        kind: 'forall',
+        bindings: [referenceBinding],
+        body,
+      },
+    }
+  }
+
+  if (clause.quantifier === 'none') {
+    return {
+      type: 'FormulaNode',
+      kind: 'forall',
+      bindings: [subjectBinding],
+      body: {
+        type: 'FormulaNode',
+        kind: 'not',
+        operand: {
+          type: 'FormulaNode',
+          kind: 'exists',
+          bindings: [referenceBinding],
+          body,
+        },
+      },
+    }
+  }
+
+  return {
+    type: 'FormulaNode',
+    kind: 'forall',
+    bindings: [subjectBinding, referenceBinding],
+    body,
+  }
+}
+
+// ---------------------------------------------------------------------------
+// Selector Extraction from Assertions / Formulas
+// ---------------------------------------------------------------------------
+
+export function getSelectorsFromAssertion(assertion: FluentRelation | FluentAssertion | FluentQuantifier): string[] {
+  const selectors = new Set<string>()
+  const rel = assertion as any
+  if (rel.assertion?.getSubject) {
+    selectors.add(rel.assertion.getSubject())
+  }
+  if (rel.referenceSelector) {
+    selectors.add(rel.referenceSelector)
+  }
+  // Extract selectors from compound relation parts (.and / .or chaining)
+  if (Array.isArray(rel._compoundParts)) {
+    for (const part of rel._compoundParts) {
+      if (part.referenceSelector) {
+        selectors.add(part.referenceSelector)
+      }
+    }
+  }
+  if (Array.isArray(rel.bindings)) {
+    for (const b of rel.bindings) {
+      if (b?.selector) selectors.add(b.selector)
+      // Extract reference selectors from assertions inside FluentQuantifier bindings
+      if (typeof b?.getAssertions === 'function') {
+        for (const assertion of b.getAssertions()) {
+          if (assertion?.reference?.value) {
+            selectors.add(assertion.reference.value)
+          }
+        }
+      }
+    }
+  }
+  return Array.from(selectors)
+}
+
+export function getSelectorsFromFormula(formula: FormulaNode): string[] {
+  const selectors = new Set<string>()
+  const visit = (node: FormulaNode) => {
+    if (node.kind === 'forall' || node.kind === 'exists') {
+      for (const b of node.bindings) {
+        if (b.domain.selector && !b.domain.selector.startsWith('$')) {
+          selectors.add(b.domain.selector)
+        }
+      }
+      visit(node.body)
+      return
+    }
+    if (node.kind === 'and' || node.kind === 'or') {
+      visit(node.left)
+      visit(node.right)
+      return
+    }
+    if (node.kind === 'not') {
+      visit(node.operand)
+      return
+    }
+    if (node.kind === 'implies') {
+      visit(node.antecedent)
+      visit(node.consequent)
+    }
+  }
+  visit(formula)
+  return Array.from(selectors)
+}
+
+// ---------------------------------------------------------------------------
+// Clause Label Builders
+// ---------------------------------------------------------------------------
+
+export function buildFluentLabel(assertion: FluentRelation | FluentAssertion | FluentQuantifier): string {
+  const rel = assertion as any
+
+  // FluentQuantifier
+  if (rel.bindings && Array.isArray(rel.bindings)) {
+    const firstBinding = rel.bindings[0]
+    const selector = firstBinding?.selector || 'unknown'
+    return `quantified assertion over '${selector}'`
+  }
+
+  // FluentRelation
+  if (rel.relation && rel.assertion?.getSubject) {
+    const subject = rel.assertion.getSubject()
+    const ref = rel.referenceSelector || ''
+    const opts = rel.options || {}
+    const parts: string[] = [`'${subject}' ${rel.relation}`]
+    if (ref) parts.push(`'${ref}'`)
+    if (opts.minGap !== undefined) parts.push(`gap ${opts.minGap}px`)
+    if (opts.maxGap !== undefined) parts.push(`maxGap ${opts.maxGap}px`)
+    if (opts.tolerance !== undefined) parts.push(`tolerance ${opts.tolerance}px`)
+    if (opts.axis) parts.push(`axis ${opts.axis}`)
+    return parts.join(' ')
+  }
+
+  return 'fluent assertion'
+}
+
+export function buildDenseLabel(clause: CanonicalClauseDescriptor): string {
+  const parts: string[] = [`'${clause.subject}' ${clause.relation}`]
+  if (clause.reference) parts.push(`'${clause.reference}'`)
+  if (clause.bounds?.minGap !== undefined) parts.push(`gap ${clause.bounds.minGap}px`)
+  if (clause.bounds?.maxGap !== undefined) parts.push(`maxGap ${clause.bounds.maxGap}px`)
+  if (clause.tolerance) parts.push(`tolerance ${clause.tolerance.value}${clause.tolerance.unit}`)
+  if (clause.quantifier && clause.quantifier !== 'all') parts.unshift(clause.quantifier)
+  return parts.join(' ')
+}
+
+export function buildFOLLabel(folAst: any): string {
+  switch (folAst.type) {
+    case 'ForAll':
+      return `forall ${folAst.variable?.name} in ${folAst.domain?.kind}(${folAst.domain?.selector ?? ''})`
+    case 'Exists':
+      return `exists ${folAst.variable?.name} in ${folAst.domain?.kind}(${folAst.domain?.selector ?? ''})`
+    case 'And':
+      return `${buildFOLLabel(folAst.left)} and ${buildFOLLabel(folAst.right)}`
+    case 'Or':
+      return `${buildFOLLabel(folAst.left)} or ${buildFOLLabel(folAst.right)}`
+    case 'Not':
+      return `not ${buildFOLLabel(folAst.operand)}`
+    case 'Implies':
+      return `${buildFOLLabel(folAst.left)} implies ${buildFOLLabel(folAst.right)}`
+    case 'PredicateCall':
+      return `${folAst.name}(${folAst.args.map((a: any) => a.name ?? a).join(', ')})`
+    default:
+      return 'FOL formula'
+  }
+}
+
+// ---------------------------------------------------------------------------
+// Normalized Contract Builder
+// ---------------------------------------------------------------------------
+
+export function extractCanonicalFromAssertion(
+  assertion: FluentRelation | FluentAssertion | FluentQuantifier,
+): CanonicalClauseDescriptor[] {
+  if (assertion instanceof FluentRelation) {
+    const ast = assertion.toAst()
+    return lowerToCanonical(ast)
+  }
+  if (assertion instanceof FluentQuantifier) {
+    const descriptors: CanonicalClauseDescriptor[] = []
+    for (const binding of assertion.bindings) {
+      for (const a of binding.getAssertions()) {
+        descriptors.push(...lowerToCanonical(a))
+      }
+    }
+    return descriptors
+  }
+  return []
+}
+
+export function buildNormalizedContracts(
+  assertions: (FluentRelation | FluentAssertion | FluentQuantifier)[],
+  specs: string[],
+): NormalizedContract[] {
+  const contracts: NormalizedContract[] = []
+  let index = 0
+
+  for (const assertion of assertions) {
+    const descriptors = extractCanonicalFromAssertion(assertion)
+    for (const desc of descriptors) {
+      contracts.push(descriptorToContract(desc, index++))
+    }
+  }
+
+  for (const source of specs) {
+    if (source.trim().length === 0) continue
+    const parsed = parseSpec(source)
+    if (parsed.diagnostics.some((d) => d.severity === 'error')) continue
+    const descriptors = lowerToCanonical(parsed.ast)
+    for (const desc of descriptors) {
+      contracts.push(descriptorToContract(desc, index++))
+    }
+  }
+
+  return contracts
+}
+
+export function descriptorToContract(
+  desc: CanonicalClauseDescriptor,
+  index: number,
+): NormalizedContract {
+  const options: Record<string, unknown> = {}
+  if (desc.bounds) {
+    if (desc.bounds.minGap !== undefined) options.minGap = desc.bounds.minGap
+    if (desc.bounds.maxGap !== undefined) options.maxGap = desc.bounds.maxGap
+  }
+  if (desc.tolerance) {
+    options.tolerance = desc.tolerance.value
+    options.toleranceUnit = desc.tolerance.unit
+  }
+  if (desc.options) {
+    for (const [k, v] of Object.entries(desc.options)) {
+      if (options[k] === undefined) options[k] = v
+    }
+  }
+  if (desc.quantifier) {
+    options.quantifier = desc.quantifier
+  }
+  if (desc.space) {
+    options.space = desc.space
+  }
+
+  const labelParts: string[] = []
+  labelParts.push(`'${desc.subject}'`)
+  labelParts.push(desc.relation)
+  if (desc.reference) {
+    labelParts.push(`'${desc.reference}'`)
+  }
+
+  const optionEntries = Object.entries(options)
+  if (optionEntries.length > 0) {
+    const optionStr = optionEntries
+      .map(([k, v]) => `${k}: ${JSON.stringify(v)}`)
+      .join(', ')
+    labelParts.push(`with ${optionStr}`)
+  }
+
+  return {
+    clauseId: `contract_${index}`,
+    clauseLabel: labelParts.join(' '),
+    relation: desc.relation,
+    subject: desc.subject,
+    reference: desc.reference || '',
+    options,
+  }
+}
+
+// ---------------------------------------------------------------------------
+// Cardinality Assertion Evaluation
+// ---------------------------------------------------------------------------
+
+export interface CardinalityResult {
+  clauseId: string
+  status: ClauseResult['status']
+  truth: ClauseResult['truth']
+  diagnostics: ImhotepDiagnostic[]
+  selector: string
+  expectedCount: number
+  label: string
+}
+
+export function buildCardinalityLabel(kind: 'exactlyOne' | 'atLeastN' | 'atMostN', selector: string, expectedCount: number): string {
+  if (kind === 'exactlyOne') return `'${selector}' exactlyOne`
+  if (kind === 'atLeastN') return `'${selector}' atLeastN ${expectedCount}`
+  return `'${selector}' atMostN ${expectedCount}`
+}
+
+export function evaluateCardinalityAssertion(
+  assertion: any,
+  clauseId: string,
+  selectorToIds: Map<string, number[]>,
+): CardinalityResult {
+  const selector = assertion.assertion?.getSubject?.() ?? assertion.selector ?? ''
+  const kind = assertion.kind as 'exactlyOne' | 'atLeastN' | 'atMostN'
+  const expectedCount = assertion.expectedCount as number
+  const ids = selectorToIds.get(selector) ?? []
+  const observedCount = ids.length
+  const label = buildCardinalityLabel(kind, selector, expectedCount)
+
+  let pass = false
+  let expectedDescription = ''
+
+  switch (kind) {
+    case 'exactlyOne':
+      pass = observedCount === 1
+      expectedDescription = 'exactly 1'
+      break
+    case 'atLeastN':
+      pass = observedCount >= expectedCount
+      expectedDescription = `at least ${expectedCount}`
+      break
+    case 'atMostN':
+      pass = observedCount <= expectedCount
+      expectedDescription = `at most ${expectedCount}`
+      break
+  }
+
+  const diagnostics: ImhotepDiagnostic[] = []
+  if (!pass) {
+    diagnostics.push({
+      code: `IMH_CARDINALITY_${kind.toUpperCase()}_FAILED` as DiagnosticCode,
+      severity: 'error',
+      category: 'contract-failure',
+      message: `Selector "${selector}" resolved to ${observedCount} element(s), but expected ${expectedDescription}.`,
+      source: 'imhotep-playwright',
+      related: [],
+      fixHints: [
+        `Check that "${selector}" matches the intended number of elements.`,
+        `Use ui.extract('${selector}') to verify the selector resolves to the expected count.`,
+      ],
+      metrics: { observedCount, expectedCount },
+      sourceRef: { selector },
+      clauseLabel: label,
+    })
+  }
+
+  return {
+    clauseId,
+    status: pass ? 'pass' : 'fail',
+    truth: 'determinate',
+    diagnostics,
+    selector,
+    expectedCount,
+    label,
+  }
+}
+
+// ---------------------------------------------------------------------------
+// Result Adapter: FOL → Public API shape
+// ---------------------------------------------------------------------------
+
+const PREDICATE_TO_DIAGNOSTIC_CODE: Record<string, DiagnosticCode> = {
+  leftOf: 'IMH_RELATION_LEFT_OF_FAILED',
+  rightOf: 'IMH_RELATION_RIGHT_OF_FAILED',
+  above: 'IMH_RELATION_ABOVE_FAILED',
+  below: 'IMH_RELATION_BELOW_FAILED',
+  inside: 'IMH_RELATION_INSIDE_FAILED',
+  contains: 'IMH_RELATION_CONTAINS_FAILED',
+  alignedWith: 'IMH_ALIGNMENT_FAILED',
+  centeredWithin: 'IMH_RELATION_CENTERED_FAILED',
+  overlaps: 'IMH_RELATION_OVERLAPS_FAILED',
+  atLeast: 'IMH_SIZE_AT_LEAST_FAILED',
+  atMost: 'IMH_SIZE_AT_MOST_FAILED',
+  between: 'IMH_SIZE_BETWEEN_FAILED',
+}
+
+export function mapFolDiagnostic(d: { code: string; severity: 'error' | 'warning' | 'info'; category?: string; message: string; clauseId?: string }): ImhotepDiagnostic {
+  let code = d.code as DiagnosticCode
+  let message = d.message
+  const fixHints: string[] = []
+
+  if ((code as string) === 'IMH_LOGIC_PREDICATE_MISSING') {
+    code = 'IMH_INTERNAL_UNKNOWN_CLAUSE_KIND'
+    fixHints.push('The assertion uses an unsupported relation or predicate.')
+    fixHints.push('Supported relations: leftOf, rightOf, above, below, alignedWith, centeredWithin, inside, contains, overlaps.')
+  }
+
+  if ((code as string) === 'IMH_PREDICATE_FAILED') {
+    const match = message.match(/Predicate "([^"]+)" failed/)
+    const predicateName = match?.[1]
+    if (predicateName && PREDICATE_TO_DIAGNOSTIC_CODE[predicateName]) {
+      code = PREDICATE_TO_DIAGNOSTIC_CODE[predicateName]
+      const gapMatch = message.match(/gap=([\d.-]+)/)
+      const observedGap = gapMatch ? parseFloat(gapMatch[1]) : undefined
+      const minGapMatch = message.match(/minGap=([\d.-]+)/)
+      const minGap = minGapMatch ? parseFloat(minGapMatch[1]) : undefined
+      const maxGapMatch = message.match(/maxGap=([\d.-]+)/)
+      const maxGap = maxGapMatch ? parseFloat(maxGapMatch[1]) : undefined
+      const gapKind = observedGap !== undefined && maxGap !== undefined && minGap !== undefined
+        ? (observedGap < minGap ? 'min' : observedGap > maxGap ? 'max' : 'min')
+        : 'min'
+      const expectedGap = gapKind === 'min' ? (minGap ?? 0) : (maxGap ?? 0)
+      const boundDescription = gapKind === 'min' ? 'minimum required gap' : 'maximum required gap'
+      if (predicateName === 'leftOf' && observedGap !== undefined) {
+        message = `leftOf assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
+        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
+      } else if (predicateName === 'above' && observedGap !== undefined) {
+        message = `above assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
+        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
+      } else if (predicateName === 'below' && observedGap !== undefined) {
+        message = `below assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
+        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
+      } else if (predicateName === 'rightOf' && observedGap !== undefined) {
+        message = `rightOf assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
+        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
+      } else if (predicateName === 'atLeast' || predicateName === 'atMost' || predicateName === 'between') {
+        fixHints.push(`Check the expected size threshold and the actual element dimensions using ui.extract(selector).`)
+      } else {
+        fixHints.push(`Verify the expected layout and consider adjusting thresholds.`)
+      }
+    } else {
+      fixHints.push(`Verify the expected layout and consider adjusting thresholds.`)
+    }
+  }
+
+  if (code === 'IMH_SELECTOR_ZERO_MATCHES') {
+    fixHints.push('Check that the selector is valid and matches an element in the DOM.')
+    fixHints.push('Use ui.extract(selector) to verify the selector resolves to at least one element.')
+  }
+
+  if (code === 'IMH_EXTRACT_PROTOCOL_ERROR') {
+    fixHints.push('Verify the page is fully loaded before running assertions.')
+    fixHints.push('Check that selectors are valid CSS selectors or semantic references.')
+    fixHints.push('Use ui.extract(selector) to debug selector resolution.')
+  }
+
+  if ((code as string) === 'IMH_FEATURE_NOT_YET_IMPLEMENTED') {
+    fixHints.push('This assertion uses a relation that is documented but not yet implemented.')
+    fixHints.push('Use a supported relation such as leftOf, rightOf, above, below, inside, overlaps, alignedWith, or centeredWithin.')
+  }
+
+  const codeStr = code as string
+  if (codeStr === 'IMH_PARSE_ERROR' || codeStr === 'IMH_PARSE_INVALID_SYNTAX' || codeStr === 'IMH_PARSE_UNEXPECTED_TOKEN') {
+    fixHints.push('Selectors must be single-quoted strings, e.g. \'[data-testid="x"]\'.')
+    fixHints.push('Use relation keywords directly without "is": e.g. \'a\' leftOf \'b\'.')
+    fixHints.push('Gap values require units: e.g. gap 8px.')
+  }
+
+  if (fixHints.length === 0) {
+    const entry = lookupCode(code)
+    if (entry?.fixHints && entry.fixHints.length > 0) {
+      fixHints.push(...entry.fixHints)
+    }
+  }
+
+  return {
+    code,
+    severity: d.severity,
+    category: (d.category ?? 'internal-error') as ImhotepDiagnostic['category'],
+    message,
+    clauseId: d.clauseId,
+    source: 'imhotep-solver',
+    related: [],
+    fixHints,
+    metrics: {},
+    sourceRef: {},
+  }
+}
+
+interface TraceMetadata {
+  sourceRef?: SourceReference
+  clauseLabel?: string
+}
+
+export function isDuckTypedFluentQuantifier(value: unknown): boolean {
+  return !!value
+    && typeof value === 'object'
+    && Array.isArray((value as any).bindings)
+    && typeof (value as any).toFormula === 'function'
+}
+
+export function hasSubjectQuantifier(value: unknown): boolean {
+  if (!value || typeof value !== 'object') return false
+  const assertion = (value as any).assertion
+  return !!assertion && typeof assertion.getQuantifier === 'function' && assertion.getQuantifier() !== undefined
+}
+
+// ---------------------------------------------------------------------------
+// Package Fingerprint & Compatibility
+// ---------------------------------------------------------------------------
+
+export function findNearestPackageJson(startPath: string): string | null {
+  let current = path.dirname(startPath)
+  for (let i = 0; i < 16; i++) {
+    const candidate = path.join(current, 'package.json')
+    if (fs.existsSync(candidate)) return candidate
+    const parent = path.dirname(current)
+    if (parent === current) break
+    current = parent
+  }
+  return null
+}
+
+export function resolvePackageFingerprint(name: string): { name: string; version: string; resolvedFrom: string } {
+  try {
+    const resolvedEntry = cjsRequire.resolve(name)
+    const pkgJson = findNearestPackageJson(resolvedEntry)
+    if (!pkgJson) {
+      return {
+        name,
+        version: 'unknown',
+        resolvedFrom: resolvedEntry,
+      }
+    }
+    const content = fs.readFileSync(pkgJson, 'utf8')
+    const parsed = JSON.parse(content) as { version?: string }
+    return {
+      name,
+      version: typeof parsed.version === 'string' ? parsed.version : 'unknown',
+      resolvedFrom: pkgJson,
+    }
+  } catch (err) {
+    return {
+      name,
+      version: 'unresolved',
+      resolvedFrom: err instanceof Error ? err.message : String(err),
+    }
+  }
+}
+
+export function collectPackageFingerprints(): Array<{ name: string; version: string; resolvedFrom: string }> {
+  return [
+    resolvePackageFingerprint('imhotep-playwright'),
+    resolvePackageFingerprint('imhotep-dsl'),
+    resolvePackageFingerprint('imhotep-solver'),
+  ]
+}
+
+export function buildCompatibilityReport(ui: ImhotepUi): CompatibilityReport {
+  const checks: CompatibilityCheck[] = []
+  const packageFingerprints = collectPackageFingerprints()
+
+  const packageResolutionOk = packageFingerprints.every((p) => p.version !== 'unresolved')
+  checks.push({
+    id: 'package-fingerprints-resolved',
+    ok: packageResolutionOk,
+    details: packageFingerprints.map((p) => `${p.name}@${p.version}`).join(', '),
+  })
+
+  const unitsSource = "in viewport:\n  '.probe' atMost 85vw wide\n  '.probe' atMost 60ch wide"
+  const parsedUnits = parseSpec(unitsSource)
+  const hasUnitsParseError = parsedUnits.diagnostics.some((d) => d.severity === 'error')
+  const unitsClauses = hasUnitsParseError ? 0 : lowerToCanonical(parsedUnits.ast).length
+  checks.push({
+    id: 'dsl-units-vw-ch',
+    ok: !hasUnitsParseError && unitsClauses === 2,
+    details: hasUnitsParseError
+      ? `parse errors: ${parsedUnits.diagnostics.map((d) => String(d.code)).join(', ')}`
+      : `parsed clauses=${unitsClauses}`,
+  })
+
+  const loweredUnits = hasUnitsParseError ? [] : lowerToCanonical(parsedUnits.ast)
+  const firstMax = loweredUnits[0]?.options?.max as any
+  const secondMax = loweredUnits[1]?.options?.max as any
+  const loweredUnitsOk =
+    !!firstMax
+    && typeof firstMax === 'object'
+    && firstMax.value === 85
+    && firstMax.unit === 'vw'
+    && !!secondMax
+    && typeof secondMax === 'object'
+    && secondMax.value === 60
+    && secondMax.unit === 'ch'
+  checks.push({
+    id: 'dsl-size-unit-lowering',
+    ok: loweredUnitsOk,
+    details: `first=${JSON.stringify(firstMax ?? null)}, second=${JSON.stringify(secondMax ?? null)}`,
+  })
+
+  const hasQuantifierHelpers = typeof ui.expect.all === 'function' && typeof ui.expect.any === 'function' && typeof ui.expect.none === 'function'
+  checks.push({
+    id: 'expect-quantifier-helpers',
+    ok: hasQuantifierHelpers,
+    details: `all=${typeof ui.expect.all}, any=${typeof ui.expect.any}, none=${typeof ui.expect.none}`,
+  })
+
+  const priorAssertions = [...(assertionStore.get(ui) || [])]
+  const priorSpecs = [...(specStore.get(ui) || [])]
+  let expectAllInvocationOk = false
+  let expectAllInvocationDetails = 'not executed'
+  try {
+    const chain = ui.expect.all('.__imhotep_compat_none__').to.be.atLeast(1, 'height') as any
+    expectAllInvocationOk = !!chain && typeof chain === 'object' && !!chain.assertion && chain.assertion.getQuantifier?.() === 'all'
+    expectAllInvocationDetails = `chain=${typeof chain}, quantifier=${chain?.assertion?.getQuantifier?.()}`
+  } catch (err) {
+    expectAllInvocationDetails = err instanceof Error ? err.message : String(err)
+  } finally {
+    assertionStore.set(ui, priorAssertions)
+    specStore.set(ui, priorSpecs)
+  }
+  checks.push({
+    id: 'expect-all-chain-invocation',
+    ok: expectAllInvocationOk,
+    details: expectAllInvocationDetails,
+  })
+
+  const emptyResolver: DomainResolver = {
+    resolve(domain) {
+      if (domain.selector === '.none') {
+        return {
+          domainId: 'dom_none',
+          subjectIds: new Uint32Array([]),
+          provenance: 'elements(.none)',
+          closed: true,
+        }
+      }
+      return undefined
+    },
+  }
+
+  const emptyWorld = buildGeometryWorld([]) as unknown as GeometryWorld
+  const forallEmpty = evaluateLogic({
+    formula: {
+      type: 'FormulaNode',
+      kind: 'forall',
+      bindings: [{
+        type: 'TupleBinding',
+        variables: ['$x'],
+        domain: { type: 'DomainRef', domain: 'elements', selector: '.none' },
+      }],
+      body: {
+        type: 'FormulaNode',
+        kind: 'predicate',
+        predicate: 'atLeast',
+        args: [{ type: 'VariableRef', name: '$x' }],
+        options: { value: 1, dimension: 'height' },
+      },
+    } as FormulaNode,
+    world: emptyWorld,
+    resolver: emptyResolver,
+    options: { trace: false },
+  })
+  const existsEmpty = evaluateLogic({
+    formula: {
+      type: 'FormulaNode',
+      kind: 'exists',
+      bindings: [{
+        type: 'TupleBinding',
+        variables: ['$x'],
+        domain: { type: 'DomainRef', domain: 'elements', selector: '.none' },
+      }],
+      body: {
+        type: 'FormulaNode',
+        kind: 'predicate',
+        predicate: 'atLeast',
+        args: [{ type: 'VariableRef', name: '$x' }],
+        options: { value: 1, dimension: 'height' },
+      },
+    } as FormulaNode,
+    world: emptyWorld,
+    resolver: emptyResolver,
+    options: { trace: false },
+  })
+  const quantifierEmptyDomainOk =
+    forallEmpty.passed
+    && existsEmpty.passed === false
+    && existsEmpty.diagnostics.some((d) => d.code === 'IMH_LOGIC_EMPTY_DOMAIN_EXISTS')
+  checks.push({
+    id: 'quantifier-empty-domain-semantics',
+    ok: quantifierEmptyDomainOk,
+    details: `forallPassed=${forallEmpty.passed}, existsPassed=${existsEmpty.passed}`,
+  })
+
+  const insideWorld = buildGeometryWorld([
+    { tagName: 'div', rect: { x: 47, y: 537, width: 231, height: 47 } },
+    { tagName: 'div', rect: { x: 47, y: 482, width: 619, height: 518 } },
+  ]) as unknown as GeometryWorld
+  registerDefaultPredicates()
+  const insideEvaluator = getPredicateEvaluator('inside')
+  const insideEval = insideEvaluator?.evaluateTuple(insideWorld, [1, 2], {})
+  const insideMetrics = ((insideEval?.metrics ?? {}) as Record<string, number>)
+  const hasOverflowMetrics =
+    typeof insideMetrics.overflowTop === 'number'
+    || typeof insideMetrics.overflowBottom === 'number'
+    || typeof insideMetrics.overflowLeft === 'number'
+    || typeof insideMetrics.overflowRight === 'number'
+  const insideMetricsOk =
+    insideEval?.truth === 'true'
+    && (
+      !hasOverflowMetrics
+      || (
+        (insideMetrics.overflowTop ?? 0) === 0
+        && (insideMetrics.overflowBottom ?? 0) === 0
+        && (insideMetrics.overflowLeft ?? 0) === 0
+        && (insideMetrics.overflowRight ?? 0) === 0
+      )
+    )
+  checks.push({
+    id: 'inside-overflow-orientation',
+    ok: insideMetricsOk,
+    details: hasOverflowMetrics
+      ? `top=${insideMetrics.overflowTop ?? 'na'}, bottom=${insideMetrics.overflowBottom ?? 'na'}, left=${insideMetrics.overflowLeft ?? 'na'}, right=${insideMetrics.overflowRight ?? 'na'}`
+      : 'overflow metrics unavailable in solver output',
+  })
+
+  const sizeWorld = buildGeometryWorld([
+    { tagName: 'div', rect: { x: 0, y: 0, width: 527, height: 100 } },
+  ]) as unknown as GeometryWorld
+  ;(sizeWorld as any).env = {
+    ...((sizeWorld as any).env || {}),
+    viewportWidth: 1280,
+    viewportHeight: 720,
+  }
+  ;(sizeWorld as any).styles = {
+    subjectId: [1],
+    fontSize: [16],
+    chWidth: [9],
+  }
+  registerDefaultPredicates()
+  const atMostEvaluator = getPredicateEvaluator('atMost')
+  const vwResult = atMostEvaluator?.evaluateTuple(sizeWorld, [1], { dimension: 'width', max: { value: 85, unit: 'vw' } })
+  const chResult = atMostEvaluator?.evaluateTuple(sizeWorld, [1], { dimension: 'width', max: { value: 60, unit: 'ch' } })
+  const solverUnitsOk =
+    vwResult?.truth === 'true'
+    && (vwResult.metrics?.max ?? 0) > 1000
+    && chResult?.truth === 'true'
+    && Math.abs((chResult.metrics?.max ?? 0) - 540) < 0.0001
+  checks.push({
+    id: 'solver-size-unit-conversion',
+    ok: !!solverUnitsOk,
+    details: `vwTruth=${vwResult?.truth ?? 'na'}, vwMax=${vwResult?.metrics?.max ?? 'na'}, chTruth=${chResult?.truth ?? 'na'}, chMax=${chResult?.metrics?.max ?? 'na'}`,
+  })
+
+  return {
+    ok: checks.every((c) => c.ok),
+    generatedAt: new Date().toISOString(),
+    checks,
+    packageFingerprints,
+  }
+}
+
+export function maybeEmitCompatibilityWarning(ui: ImhotepUi): void {
+  if (compatibilityWarningEmitted) return
+  const report = buildCompatibilityReport(ui)
+  if (report.ok) return
+  compatibilityWarningEmitted = true
+  const failed = report.checks.filter((c) => !c.ok)
+  const detail = failed.map((c) => `${c.id}: ${c.details}`).join(' | ')
+  const fingerprints = report.packageFingerprints
+    .map((p) => `${p.name}@${p.version} (${p.resolvedFrom})`)
+    .join(' | ')
+  // eslint-disable-next-line no-console
+  console.warn(`[imhotep-playwright] compatibility warning: ${detail}; fingerprints=${fingerprints}`)
+}
+
+export function buildCompatibilityDiagnostic(report: CompatibilityReport): ImhotepDiagnostic | null {
+  if (report.ok) return null
+  const failed = report.checks.filter((c) => !c.ok)
+  const detail = failed.map((c) => `${c.id}: ${c.details}`).join(' | ')
+  const fingerprints = report.packageFingerprints
+    .map((p) => `${p.name}@${p.version}`)
+    .join(', ')
+  return {
+    code: 'IMH_INTERNAL_COMPAT_WARNING' as DiagnosticCode,
+    severity: 'warning',
+    category: 'internal-error',
+    message: `Runtime compatibility checks reported issues: ${detail}`,
+    source: 'imhotep-playwright',
+    related: [],
+    fixHints: [
+      `Resolved packages: ${fingerprints}`,
+      'Reinstall imhotep-playwright, imhotep-dsl, and imhotep-solver together from the same build.',
+    ],
+    metrics: {},
+    sourceRef: { file: 'public.ts' },
+    clauseLabel: 'compatibility',
+  }
+}
+
+// ---------------------------------------------------------------------------
+// FOL Result Adapter
+// ---------------------------------------------------------------------------
+
+export function adaptFOLResultToImhotepResult(
+  folResult: ReturnType<typeof evaluateLogic>,
+  assertionCount: number,
+  clauseId?: string,
+  traceMeta?: TraceMetadata,
+): ImhotepResult {
+  const diagnostics: ImhotepDiagnostic[] = folResult.diagnostics.map((d) => {
+    const mapped = mapFolDiagnostic(d)
+    if (traceMeta?.sourceRef) mapped.sourceRef = traceMeta.sourceRef
+    if (traceMeta?.clauseLabel) mapped.clauseLabel = traceMeta.clauseLabel
+    return mapped
+  })
+
+  const clauseResults: ClauseResult[] = folResult.formulaResults.map((fr, idx) => {
+    const status: ClauseResult['status'] =
+      fr.outcome === 'indeterminate' ? 'error' : fr.outcome
+
+    const normalizedMetrics = (() => {
+      const raw = (fr.metrics || {}) as Record<string, unknown>
+      const hasInsideGeometry =
+        typeof raw.subjectTop === 'number'
+        && typeof raw.subjectBottom === 'number'
+        && typeof raw.subjectLeft === 'number'
+        && typeof raw.subjectRight === 'number'
+        && typeof raw.refTop === 'number'
+        && typeof raw.refBottom === 'number'
+        && typeof raw.refLeft === 'number'
+        && typeof raw.refRight === 'number'
+      if (!hasInsideGeometry) {
+        const hasOverflowOnly =
+          typeof raw.overflowTop === 'number'
+          || typeof raw.overflowBottom === 'number'
+          || typeof raw.overflowLeft === 'number'
+          || typeof raw.overflowRight === 'number'
+        if (hasOverflowOnly && fr.outcome === 'pass') {
+          return {
+            ...raw,
+            overflowTop: 0,
+            overflowBottom: 0,
+            overflowLeft: 0,
+            overflowRight: 0,
+          }
+        }
+        return raw
+      }
+
+      const subjectTop = raw.subjectTop as number
+      const subjectBottom = raw.subjectBottom as number
+      const subjectLeft = raw.subjectLeft as number
+      const subjectRight = raw.subjectRight as number
+      const refTop = raw.refTop as number
+      const refBottom = raw.refBottom as number
+      const refLeft = raw.refLeft as number
+      const refRight = raw.refRight as number
+
+      return {
+        ...raw,
+        overflowTop: Math.max(0, refTop - subjectTop),
+        overflowBottom: Math.max(0, subjectBottom - refBottom),
+        overflowLeft: Math.max(0, refLeft - subjectLeft),
+        overflowRight: Math.max(0, subjectRight - refRight),
+      }
+    })()
+
+    return {
+      clauseId: clauseId ?? (fr.formulaId ?? `clause_${idx}`),
+      status,
+      truth: fr.truth,
+      metrics: normalizedMetrics as any,
+      witness: fr.witness
+        ? { subjectId: fr.witness[0] ?? 0, frameId: 0 }
+        : { subjectId: 0, frameId: 0 },
+      diagnostics: [fr.outcome === 'fail' ? 'IMH_PREDICATE_FAILED' : ''].filter(Boolean),
+      sourceRef: traceMeta?.sourceRef,
+      clauseLabel: traceMeta?.clauseLabel,
+    }
+  })
+
+  const passed = folResult.passed && clauseResults.every((r) => r.status === 'pass')
+
+  return {
+    schemaVersion: '1.0',
+    passed,
+    summary: `${assertionCount} assertion(s), ${diagnostics.length} diagnostic(s)`,
+    clauseResults,
+    diagnostics,
+  }
+}
diff --git a/packages/imhotep-playwright/src/public.ts b/packages/imhotep-playwright/src/public.ts
index 6f87ef2..55019a2 100644
--- a/packages/imhotep-playwright/src/public.ts
+++ b/packages/imhotep-playwright/src/public.ts
@@ -9,17 +9,24 @@
  */
 
 import path from 'path'
-import fs from 'fs'
-import { createRequire } from 'module'
 import type { Page } from 'playwright'
 import type { FluentAssertion } from 'imhotep-dsl'
-import { FluentRelation, FluentQuantifier, expect as dslExpect, parseSpec, lowerToCanonical, extractFOLFormulas, compileDenseFOLToFormula, type CanonicalClauseDescriptor, validateRelation } from 'imhotep-dsl'
+import {
+  FluentRelation,
+  FluentQuantifier,
+  expect as dslExpect,
+  parseSpec,
+  lowerToCanonical,
+  extractFOLFormulas,
+  compileDenseFOLToFormula,
+  type CanonicalClauseDescriptor,
+  validateRelation,
+} from 'imhotep-dsl'
 import { wrapPage, ImhotepPage, ImhotepPageOptions, type StateMaterializationNote, type MaterializeStateOptions } from './page.js'
 import { ImhotepRuntime, createRuntime, SinglePageRuntime, RuntimeLike } from './runtime.js'
 import type { ImhotepResult, ClauseResult, ImhotepDiagnostic, DiagnosticCode, NormalizedContract } from 'imhotep-core'
-import type { SubjectReference, ExecutionContext, DomainValue } from 'imhotep-core'
+import type { SubjectReference, ExecutionContext } from 'imhotep-core'
 import { subjectReferenceToString, createDeterministicContext, createVolatileContext } from 'imhotep-core'
-import { adaptCanonicalWorldToSolver } from 'imhotep-core'
 import type { SceneTarget, RenderCase } from 'imhotep-core/scene-target'
 import {
   reactComponentTarget,
@@ -34,10 +41,7 @@ import type { GeometryWorld } from 'imhotep-solver'
 import {
   evaluateLogic,
   registerDefaultPredicates,
-  getPredicateEvaluator,
-  getRequiredFactsForPredicate,
   type LogicEngineInput,
-  type DomainResolver,
 } from 'imhotep-solver'
 import type { FormulaNode, DomainRef, SourceReference } from 'imhotep-core'
 import type { InputDomain } from 'imhotep-core/property-contracts'
@@ -53,20 +57,8 @@ import {
 import type { FastCheckAdapter } from './fast-check-adapter.js'
 import { buildGeometryWorld } from './world-builder.js'
 import { compileAssertionsToFOL } from './fol-compiler.js'
-import {
-  CDPExtractor,
-  createSessionManager,
-  resolveSelector,
-  adaptSnapshotToCanonical,
-} from 'imhotep-cdp'
-import { attachFailureAnalysis, lookupCode } from 'imhotep-reporter'
-import {
-  computeGeometryCacheKey,
-  readCachedExtractionResult,
-  writeCachedExtractionResult,
-  clearGeometryCache,
-  getDefaultCacheDir,
-} from 'imhotep-core'
+import { attachFailureAnalysis } from 'imhotep-reporter'
+import { clearGeometryCache, getDefaultCacheDir } from 'imhotep-core'
 import type { EnvironmentCase } from './environment.js'
 import type {
   ImhotepUi,
@@ -96,44 +88,87 @@ export type {
   ComponentPropertyRunHandle,
 }
 
-const cjsRequire = createRequire(import.meta.url)
+// ---------------------------------------------------------------------------
+// Extraction pipeline (imported from extraction.ts)
+// ---------------------------------------------------------------------------
 
-// Internal assertion accumulator per UI handle
-const assertionStore = new WeakMap<ImhotepUi, (FluentRelation | FluentAssertion | FluentQuantifier)[]>()
-const specStore = new WeakMap<ImhotepUi, string[]>()
+import {
+  assertionStore,
+  specStore,
+  extractWorld,
+  SelectorDomainResolver,
+  compileCanonicalClauseToFormula,
+  getSelectorsFromAssertion,
+  getSelectorsFromFormula,
+  buildFluentLabel,
+  buildDenseLabel,
+  buildFOLLabel,
+  extractCanonicalFromAssertion,
+  buildNormalizedContracts,
+  descriptorToContract,
+  evaluateCardinalityAssertion,
+  mapFolDiagnostic,
+  isDuckTypedFluentQuantifier,
+  hasSubjectQuantifier,
+  buildCompatibilityReport,
+  maybeEmitCompatibilityWarning,
+  buildCompatibilityDiagnostic,
+  adaptFOLResultToImhotepResult,
+  computeRequiredFacts,
+  usesLayoutSpace,
+  type CardinalityResult,
+} from './extraction.js'
 
-const extractionPathStats = {
-  fastPathHits: 0,
-  cdpFallbacks: 0,
-}
+// Re-export extraction functions for backward compatibility with any
+// internal consumers that import directly from './public.js'.
+export {
+  assertionStore,
+  specStore,
+  extractWorld,
+  extractWorldFastGeometry,
+  extractWorldCdp,
+  SelectorDomainResolver,
+  compileCanonicalClauseToFormula,
+  getSelectorsFromAssertion,
+  getSelectorsFromFormula,
+  buildFluentLabel,
+  buildDenseLabel,
+  buildFOLLabel,
+  extractCanonicalFromAssertion,
+  buildNormalizedContracts,
+  descriptorToContract,
+  evaluateCardinalityAssertion,
+  mapFolDiagnostic,
+  isDuckTypedFluentQuantifier,
+  hasSubjectQuantifier,
+  buildCompatibilityReport,
+  maybeEmitCompatibilityWarning,
+  buildCompatibilityDiagnostic,
+  adaptFOLResultToImhotepResult,
+  computeRequiredFacts,
+  usesLayoutSpace,
+  collectPredicates,
+  formulaNeedsCssLengthMetrics,
+  measureChWidthsByPlan,
+  attachMeasuredChWidths,
+  findNearestPackageJson,
+  resolvePackageFingerprint,
+  collectPackageFingerprints,
+  buildCardinalityLabel,
+  getPageCacheNamespace,
+  extractionPathStats,
+  maybeInstallExtractionStatsHook,
+  type CardinalityResult,
+} from './extraction.js'
 
-const pageCacheNamespace = new WeakMap<Page, string>()
-let pageCacheNamespaceCounter = 0
+import {
+  normalizeCssSelector,
+  parseQuotedValue,
+  materializeSemanticSelector,
+  type SelectorPlan,
+} from './semantic-subjects.js'
 
-function getPageCacheNamespace(page: Page): string {
-  const existing = pageCacheNamespace.get(page)
-  if (existing) return existing
-  const ns = `page-${++pageCacheNamespaceCounter}`
-  pageCacheNamespace.set(page, ns)
-  return ns
-}
-
-let extractionStatsHookInstalled = false
-let compatibilityWarningEmitted = false
-
-function maybeInstallExtractionStatsHook(): void {
-  if (extractionStatsHookInstalled) return
-  if (process.env.IMHOTEP_EXTRACT_STATS !== '1') return
-  extractionStatsHookInstalled = true
-  process.on('exit', () => {
-    const total = extractionPathStats.fastPathHits + extractionPathStats.cdpFallbacks
-    const fastPct = total > 0 ? ((extractionPathStats.fastPathHits / total) * 100).toFixed(1) : '0.0'
-    const cdpPct = total > 0 ? ((extractionPathStats.cdpFallbacks / total) * 100).toFixed(1) : '0.0'
-    console.log(
-      `[imhotep] extraction path stats: fast=${extractionPathStats.fastPathHits} (${fastPct}%), cdp=${extractionPathStats.cdpFallbacks} (${cdpPct}%), total=${total}`,
-    )
-  })
-}
+export { normalizeCssSelector, parseQuotedValue, materializeSemanticSelector, type SelectorPlan }
 
 // ---------------------------------------------------------------------------
 // Runtime normalization helper (accepts Page for backward compat)
@@ -159,1248 +194,6 @@ async function normalizeRuntime(runtime: Page | ImhotepRuntime): Promise<Runtime
   return new SinglePageRuntime(page)
 }
 
-// ---------------------------------------------------------------------------
-// World Extraction for FOL
-// ---------------------------------------------------------------------------
-
-import {
-  normalizeCssSelector,
-  parseQuotedValue,
-  materializeSemanticSelector,
-  type SelectorPlan,
-} from './semantic-subjects.js'
-
-export { normalizeCssSelector, parseQuotedValue, materializeSemanticSelector, type SelectorPlan }
-
-/**
- * Walk a formula AST and collect all predicate names.
- */
-function collectPredicates(formula: FormulaNode): string[] {
-  const predicates: string[] = []
-  function walk(node: FormulaNode) {
-    if (node.kind === 'predicate') {
-      predicates.push((node as any).predicate)
-    } else if (node.kind === 'forall' || node.kind === 'exists') {
-      walk((node as any).body)
-    } else if (node.kind === 'and' || node.kind === 'or') {
-      walk((node as any).left)
-      walk((node as any).right)
-    } else if (node.kind === 'not') {
-      walk((node as any).operand)
-    } else if (node.kind === 'implies') {
-      walk((node as any).antecedent)
-      walk((node as any).consequent)
-    }
-  }
-  walk(formula)
-  return predicates
-}
-
-function formulaNeedsCssLengthMetrics(formula: FormulaNode): boolean {
-  let needs = false
-  const scanValue = (value: unknown): void => {
-    if (needs || value == null) return
-    if (Array.isArray(value)) {
-      for (const item of value) scanValue(item)
-      return
-    }
-    if (typeof value !== 'object') return
-    const obj = value as Record<string, unknown>
-    if (typeof obj.unit === 'string') {
-      const unit = obj.unit.toLowerCase()
-      if (unit === 'ch' || unit === 'em' || unit === 'rem') {
-        needs = true
-        return
-      }
-    }
-    for (const child of Object.values(obj)) scanValue(child)
-  }
-  const walk = (node: FormulaNode): void => {
-    if (needs) return
-    if (node.kind === 'predicate') {
-      scanValue((node as any).options)
-      return
-    }
-    if (node.kind === 'forall' || node.kind === 'exists') {
-      walk((node as any).body)
-      return
-    }
-    if (node.kind === 'and' || node.kind === 'or') {
-      walk((node as any).left)
-      walk((node as any).right)
-      return
-    }
-    if (node.kind === 'not') {
-      walk((node as any).operand)
-      return
-    }
-    if (node.kind === 'implies') {
-      walk((node as any).antecedent)
-      walk((node as any).consequent)
-    }
-  }
-  walk(formula)
-  return needs
-}
-
-/**
- * Compute the minimal set of facts required by a collection of formulas.
- */
-function computeRequiredFacts(formulas: FormulaNode[]): {
-  geometry: boolean
-  topology: boolean
-  styles: boolean
-  fragments: boolean
-} {
-  const facts = new Set<string>()
-  for (const formula of formulas) {
-    const predicates = collectPredicates(formula)
-    for (const p of predicates) {
-      const required = getRequiredFactsForPredicate(p)
-      for (const f of required) {
-        facts.add(f)
-      }
-    }
-  }
-
-  const needsCssLengthMetrics = formulas.some((formula) => formulaNeedsCssLengthMetrics(formula))
-
-  return {
-    geometry: true, // Always required for subject resolution
-    topology: facts.has('topology.stackingContextOf') || facts.has('subject.clipChain'),
-    styles: facts.has('styles') || facts.has('computedStyle') || needsCssLengthMetrics,
-    fragments: facts.has('subject.fragmentCount') || facts.has('subject.firstFragmentId'),
-  }
-}
-
-function usesLayoutSpace(formula: FormulaNode): boolean {
-  let found = false
-  function walk(node: FormulaNode) {
-    if (found) return
-    if (node.kind === 'predicate') {
-      const options = (node as any).options
-      if (options?.space === 'layout') {
-        found = true
-      }
-    } else if (node.kind === 'forall' || node.kind === 'exists') {
-      walk((node as any).body)
-    } else if (node.kind === 'and' || node.kind === 'or') {
-      walk((node as any).left)
-      walk((node as any).right)
-    } else if (node.kind === 'not') {
-      walk((node as any).operand)
-    } else if (node.kind === 'implies') {
-      walk((node as any).antecedent)
-      walk((node as any).consequent)
-    }
-  }
-  walk(formula)
-  return found
-}
-
-async function measureChWidthsByPlan(
-  playwrightPage: Page,
-  plans: SelectorPlan[],
-): Promise<Map<string, number[]>> {
-  const measured = await playwrightPage.evaluate((inputPlans: Array<{ key: string; queries: string[] }>) => {
-    const out: Array<[string, number[]]> = []
-    const canvas = document.createElement('canvas')
-    const ctx = canvas.getContext('2d')
-    const fallbackMeasure = (el: HTMLElement): number => {
-      const probe = document.createElement('span')
-      probe.textContent = '0'
-      probe.style.position = 'absolute'
-      probe.style.visibility = 'hidden'
-      probe.style.left = '-99999px'
-      probe.style.top = '0'
-      const cs = window.getComputedStyle(el)
-      probe.style.font = cs.font
-      probe.style.letterSpacing = cs.letterSpacing
-      probe.style.fontKerning = cs.fontKerning as any
-      probe.style.fontVariant = cs.fontVariant
-      document.body.appendChild(probe)
-      const w = probe.getBoundingClientRect().width
-      probe.remove()
-      return w
-    }
-
-    const measure = (el: HTMLElement): number => {
-      const cs = window.getComputedStyle(el)
-      if (ctx) {
-        ctx.font = cs.font
-        const w = ctx.measureText('0').width
-        if (Number.isFinite(w) && w > 0) return w
-      }
-      const fallback = fallbackMeasure(el)
-      if (Number.isFinite(fallback) && fallback > 0) return fallback
-      const fontSize = Number.parseFloat(cs.fontSize)
-      return Number.isFinite(fontSize) && fontSize > 0 ? fontSize * 0.5 : 8
-    }
-
-    for (const plan of inputPlans) {
-      const widths: number[] = []
-      for (const query of plan.queries) {
-        const nodes = document.querySelectorAll(query)
-        for (let i = 0; i < nodes.length; i++) {
-          widths.push(measure(nodes[i] as HTMLElement))
-        }
-      }
-      out.push([plan.key, widths])
-    }
-    return out
-  }, plans)
-  return new Map<string, number[]>(measured)
-}
-
-function attachMeasuredChWidths(
-  world: GeometryWorld,
-  selectorToIds: Map<string, number[]>,
-  chWidthsBySelector: Map<string, number[]>,
-): void {
-  const worldAny = world as any
-  const styles = worldAny.styles as {
-    subjectId?: number[]
-    fontSize?: number[]
-    chWidth?: number[]
-  } | undefined
-  if (!styles) return
-  const bySubject = new Map<number, number>()
-  for (const [key, ids] of selectorToIds) {
-    const widths = chWidthsBySelector.get(key)
-    if (!widths || widths.length === 0) continue
-    const n = Math.min(ids.length, widths.length)
-    for (let i = 0; i < n; i++) {
-      const subjectId = ids[i]
-      const width = Number(widths[i])
-      if (!Number.isFinite(subjectId) || !Number.isFinite(width) || width <= 0) continue
-      if (!bySubject.has(subjectId)) bySubject.set(subjectId, width)
-    }
-  }
-  if (bySubject.size === 0) return
-
-  const styleSubjectIds = styles.subjectId
-  if (styleSubjectIds && styleSubjectIds.length > 0) {
-    const chWidth = new Array(styleSubjectIds.length)
-    for (let i = 0; i < styleSubjectIds.length; i++) {
-      const subjectId = Number(styleSubjectIds[i])
-      const measured = bySubject.get(subjectId)
-      if (measured !== undefined) {
-        chWidth[i] = measured
-        continue
-      }
-      const fs = Number(styles.fontSize?.[i])
-      chWidth[i] = Number.isFinite(fs) && fs > 0 ? fs * 0.5 : 8
-    }
-    styles.chWidth = chWidth
-    return
-  }
-
-  const subjectIds = world.subjects?.ids ?? []
-  const chWidth = new Array(subjectIds.length)
-  for (let i = 0; i < subjectIds.length; i++) {
-    const measured = bySubject.get(subjectIds[i])
-    if (measured !== undefined) {
-      chWidth[i] = measured
-      continue
-    }
-    const fs = Number(styles.fontSize?.[i])
-    chWidth[i] = Number.isFinite(fs) && fs > 0 ? fs * 0.5 : 8
-  }
-  styles.chWidth = chWidth
-}
-
-async function extractWorldFastGeometry(
-  playwrightPage: Page,
-  selectors: string[],
-  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean },
-): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
-  interface FastExtractedElement {
-    tagName: string
-    rect: { x: number; y: number; width: number; height: number }
-    fragments?: Array<{ left: number; top: number; right: number; bottom: number }>
-    transform?: { matrix: number[]; originX: number; originY: number }
-    style?: {
-      display: string
-      position: string
-      overflowX: string
-      overflowY: string
-      visibility: string
-      pointerEvents: string
-      opacity: number
-      zIndex: string
-      lineHeight: number
-      fontFamily: string
-      fontSize: number
-      fontWeight: number
-      chWidth: number
-    }
-  }
-  interface FastExtractedPayload {
-    elements: FastExtractedElement[]
-    selectorToIds: Array<[string, number[]]>
-  }
-
-  const selectorPlans: SelectorPlan[] = await Promise.all(
-    selectors.map(async (key, i) => {
-      const queries = await materializeSemanticSelector(playwrightPage, key, i)
-      return { key, queries }
-    }),
-  )
-
-  try {
-    const extracted = await playwrightPage.evaluate(({ plans, needs }: any) => {
-      const elements: FastExtractedElement[] = []
-      const selectorToIds: Array<[string, number[]]> = []
-
-      for (const plan of plans) {
-        const ids: number[] = []
-        for (const query of plan.queries) {
-          const matches = document.querySelectorAll(query)
-          for (let i = 0; i < matches.length; i++) {
-            const el = matches[i] as HTMLElement
-            const rect = el.getBoundingClientRect()
-            const subjectId = elements.length + 1
-            elements.push({
-              tagName: el.tagName.toLowerCase(),
-              rect: {
-                x: rect.left,
-                y: rect.top,
-                width: rect.width,
-                height: rect.height,
-              },
-              ...(needs.fragments
-                ? {
-                    fragments: Array.from(el.getClientRects()).map((r) => ({
-                      left: r.left,
-                      top: r.top,
-                      right: r.right,
-                      bottom: r.bottom,
-                    })),
-                  }
-                : {}),
-              ...(needs.styles || needs.geometry
-                ? {
-                    transform: (() => {
-                      const cs = window.getComputedStyle(el)
-                      const t = cs.transform
-                      let matrix = [1, 0, 0, 1, 0, 0]
-                      if (t && t !== 'none') {
-                        const m = t.match(/matrix\(([^)]+)\)/)
-                        if (m) matrix = m[1].split(',').map(Number)
-                      }
-                      const origin = cs.transformOrigin.split(' ').map(parseFloat)
-                      return { matrix, originX: origin[0] || 0, originY: origin[1] || 0 }
-                    })(),
-                  }
-                : {}),
-              ...(needs.styles
-                ? {
-                    style: (() => {
-                      const cs = window.getComputedStyle(el)
-                      const canvas = document.createElement('canvas')
-                      const ctx = canvas.getContext('2d')
-                      let chWidth = 0
-                      if (ctx) {
-                        ctx.font = cs.font
-                        chWidth = ctx.measureText('0').width
-                      }
-                      if (!(Number.isFinite(chWidth) && chWidth > 0)) {
-                        const probe = document.createElement('span')
-                        probe.textContent = '0'
-                        probe.style.position = 'absolute'
-                        probe.style.visibility = 'hidden'
-                        probe.style.left = '-99999px'
-                        probe.style.top = '0'
-                        probe.style.font = cs.font
-                        document.body.appendChild(probe)
-                        chWidth = probe.getBoundingClientRect().width
-                        probe.remove()
-                      }
-                      return {
-                        display: cs.display,
-                        position: cs.position,
-                        overflowX: cs.overflowX,
-                        overflowY: cs.overflowY,
-                        visibility: cs.visibility,
-                        pointerEvents: cs.pointerEvents,
-                        opacity: Number.parseFloat(cs.opacity) || 1,
-                        zIndex: cs.zIndex,
-                        lineHeight: Number.parseFloat(cs.lineHeight) || 0,
-                        fontFamily: cs.fontFamily || '',
-                        fontSize: Number.parseFloat(cs.fontSize) || 0,
-                        fontWeight: Number.parseInt(cs.fontWeight, 10) || 400,
-                        chWidth: Number.isFinite(chWidth) && chWidth > 0
-                          ? chWidth
-                          : (Number.parseFloat(cs.fontSize) || 16) * 0.5,
-                      }
-                    })(),
-                  }
-                : {}),
-            })
-            ids.push(subjectId)
-          }
-        }
-        selectorToIds.push([plan.key, ids])
-      }
-
-      return { elements, selectorToIds }
-    }, {
-      plans: selectorPlans,
-      needs: {
-        fragments: requiredFacts?.fragments === true,
-        styles: requiredFacts?.styles === true,
-        geometry: requiredFacts?.geometry !== false,
-      },
-    }) as FastExtractedPayload
-
-    const world = buildGeometryWorld(extracted.elements) as GeometryWorld
-    const worldAny = world as any
-
-    if (requiredFacts?.fragments) {
-      const fragmentId: number[] = []
-      const subjectId: number[] = []
-      const fragmentKind: number[] = []
-      const boxLeft: number[] = []
-      const boxTop: number[] = []
-      const boxRight: number[] = []
-      const boxBottom: number[] = []
-      const lineIndex: number[] = []
-      const flowIndex: number[] = []
-      const parentFragmentId: number[] = []
-
-      const firstFragmentIds: number[] = Array.from({ length: extracted.elements.length }, () => 0)
-      const fragmentCounts: number[] = Array.from({ length: extracted.elements.length }, () => 0)
-
-      for (let i = 0; i < extracted.elements.length; i++) {
-        const frags = extracted.elements[i].fragments ?? []
-        if (frags.length > 0) {
-          firstFragmentIds[i] = fragmentId.length
-          fragmentCounts[i] = frags.length
-        }
-        for (let j = 0; j < frags.length; j++) {
-          const f = frags[j]
-          fragmentId.push(fragmentId.length)
-          subjectId.push(i + 1)
-          fragmentKind.push(1)
-          boxLeft.push(f.left)
-          boxTop.push(f.top)
-          boxRight.push(f.right)
-          boxBottom.push(f.bottom)
-          lineIndex.push(j)
-          flowIndex.push(0)
-          parentFragmentId.push(0)
-        }
-      }
-
-      worldAny.fragments = {
-        fragmentId,
-        subjectId,
-        fragmentKind,
-        boxLeft,
-        boxTop,
-        boxRight,
-        boxBottom,
-        lineIndex,
-        flowIndex,
-        parentFragmentId,
-      }
-      worldAny.subjects.firstFragmentId = firstFragmentIds
-      worldAny.subjects.fragmentCount = fragmentCounts
-    }
-
-    if (requiredFacts?.geometry) {
-      const transformId: number[] = []
-      const transformSubjectId: number[] = []
-      const matrixStart: number[] = []
-      const matrixLength: number[] = []
-      const originX: number[] = []
-      const originY: number[] = []
-      const matrices: number[] = []
-
-      for (let i = 0; i < extracted.elements.length; i++) {
-        const t = extracted.elements[i].transform
-        if (!t) continue
-        const start = matrices.length
-        matrices.push(...t.matrix)
-        transformId.push(transformId.length)
-        transformSubjectId.push(i + 1)
-        matrixStart.push(start)
-        matrixLength.push(t.matrix.length)
-        originX.push(t.originX)
-        originY.push(t.originY)
-      }
-
-      worldAny.transforms = {
-        transformId,
-        subjectId: transformSubjectId,
-        matrixStart,
-        matrixLength,
-        originX,
-        originY,
-      }
-      worldAny.matrices = { values: matrices }
-    }
-
-    if (requiredFacts?.styles) {
-      const strings = worldAny.strings?.values ?? []
-      const stringToId = new Map<string, number>()
-      for (let i = 0; i < strings.length; i++) stringToId.set(strings[i], i)
-      const intern = (value: string): number => {
-        const existing = stringToId.get(value)
-        if (existing !== undefined) return existing
-        const id = strings.length
-        strings.push(value)
-        stringToId.set(value, id)
-        return id
-      }
-
-      const styleSubjectId: number[] = []
-      const display: number[] = []
-      const position: number[] = []
-      const zIndexKind: number[] = []
-      const zIndexValue: number[] = []
-      const overflowX: number[] = []
-      const overflowY: number[] = []
-      const opacity: number[] = []
-      const visibility: number[] = []
-      const containFlags: number[] = []
-      const pointerEvents: number[] = []
-      const lineHeight: number[] = []
-      const fontFamilyStringId: number[] = []
-      const fontSize: number[] = []
-      const fontWeight: number[] = []
-      const chWidth: number[] = []
-
-      for (let i = 0; i < extracted.elements.length; i++) {
-        const s = extracted.elements[i].style
-        if (!s) continue
-        styleSubjectId.push(i + 1)
-        display.push(intern(s.display))
-        position.push(intern(s.position))
-        overflowX.push(intern(s.overflowX))
-        overflowY.push(intern(s.overflowY))
-        visibility.push(intern(s.visibility))
-        pointerEvents.push(intern(s.pointerEvents))
-        zIndexKind.push(s.zIndex === 'auto' ? 0 : 1)
-        zIndexValue.push(s.zIndex === 'auto' ? 0 : Number.parseInt(s.zIndex, 10) || 0)
-        opacity.push(s.opacity)
-        containFlags.push(0)
-        lineHeight.push(s.lineHeight)
-        fontFamilyStringId.push(intern(s.fontFamily))
-        fontSize.push(s.fontSize)
-        fontWeight.push(s.fontWeight)
-        chWidth.push(s.chWidth)
-      }
-
-      worldAny.strings = { values: strings }
-      worldAny.styles = {
-        subjectId: styleSubjectId,
-        display,
-        position,
-        zIndexKind,
-        zIndexValue,
-        overflowX,
-        overflowY,
-        opacity,
-        visibility,
-        containFlags,
-        pointerEvents,
-        lineHeight,
-        fontFamilyStringId,
-        fontSize,
-        fontWeight,
-        chWidth,
-      }
-    }
-
-    const selectorToIds = new Map<string, number[]>(extracted.selectorToIds)
-    const errors: ImhotepDiagnostic[] = []
-
-    for (const [selector, ids] of selectorToIds) {
-      // Skip zero-match check for bound variable references (FOL quantifiers)
-      // and variable domain selectors like descendants($var, '.title')
-      if (ids.length === 0 && !selector.startsWith('$')) {
-        errors.push({
-          code: 'IMH_SELECTOR_ZERO_MATCHES',
-          severity: 'error',
-          category: 'extraction-error',
-          message: `Selector "${selector}" resolved to 0 elements.`,
-          source: 'imhotep-playwright',
-          related: [],
-          fixHints: [
-            `Check that "${selector}" is a valid CSS selector or semantic reference.`,
-            `Use ui.extract('${selector}') to verify the selector resolves to at least one element.`,
-          ],
-          metrics: {},
-          sourceRef: { selector },
-        })
-      }
-    }
-
-    return { world, selectorToIds, errors }
-  } finally {
-    await playwrightPage.evaluate(() => {
-      const nodes = Array.from(document.querySelectorAll('[data-imhotep-runtime-id]'))
-      for (const el of nodes) {
-        el.removeAttribute('data-imhotep-runtime-id')
-      }
-    }).catch(() => {})
-  }
-}
-
-async function extractWorldCdp(
-  playwrightPage: Page,
-  selectors: string[],
-  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean },
-): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
-  const errors: ImhotepDiagnostic[] = []
-  const selectorToNodeIds = new Map<string, number[]>()
-
-  // Materialize all selectors in parallel (semantic selectors hit the
-  // browser via Playwright locators, CSS selectors are local).
-  const selectorPlans: SelectorPlan[] = await Promise.all(
-    selectors.map(async (key, i) => {
-      const queries = await materializeSemanticSelector(playwrightPage, key, i)
-      return { key, queries }
-    }),
-  )
-
-  const subjectQueries = selectorPlans.flatMap((p) => p.queries)
-  const sessionManager = createSessionManager(playwrightPage)
-  try {
-    await sessionManager.enableDomain('DOM')
-
-    // Push the full DOM tree to the CDP frontend before resolving selectors.
-    // DOM.querySelectorAll requires nodeIds to be in the frontend cache.
-    const session = sessionManager.getSession()
-    await session.send('DOM.getDocument', { depth: -1 })
-
-    // Resolve all selectors in parallel to minimize CDP round-trips.
-    const allQueries = selectorPlans.flatMap((plan) =>
-      plan.queries.map((query) => ({ key: plan.key, query })),
-    )
-    const allMatches = await Promise.all(
-      allQueries.map(({ query }) => resolveSelector(sessionManager, query)),
-    )
-    const resolvedSubjects: Array<{ id: string; selector: string; nodeId: number; backendNodeId: number }> = []
-    for (let i = 0; i < allQueries.length; i++) {
-      const { key, query } = allQueries[i]
-      const matches = allMatches[i]
-      const ids = selectorToNodeIds.get(key) ?? []
-      for (const m of matches) {
-        ids.push(m.backendNodeId)
-        resolvedSubjects.push({
-          id: `sel_${resolvedSubjects.length}`,
-          selector: query,
-          nodeId: m.nodeId,
-          backendNodeId: m.backendNodeId,
-        })
-      }
-      selectorToNodeIds.set(key, ids)
-    }
-    for (const plan of selectorPlans) {
-      const ids = selectorToNodeIds.get(plan.key) ?? []
-      if (ids.length === 0) {
-        errors.push({
-          code: 'IMH_SELECTOR_ZERO_MATCHES',
-          severity: 'error',
-          category: 'extraction-error',
-          message: `Selector "${plan.key}" resolved to 0 elements.`,
-          source: 'imhotep-cdp',
-          related: [],
-          fixHints: [
-            `Check that "${plan.key}" is a valid CSS selector or semantic reference.`,
-            `Use ui.extract('${plan.key}') to verify the selector resolves to at least one element.`,
-          ],
-          metrics: {},
-          sourceRef: { selector: plan.key },
-        })
-      }
-    }
-
-    const extractor = new CDPExtractor(sessionManager)
-    const cdpRequest = {
-      requestId: `req_${Date.now()}`,
-      sceneTarget: { pageRef: playwrightPage as unknown, url: playwrightPage.url?.() ?? '' },
-      env: {
-        viewportWidth: 0,
-        viewportHeight: 0,
-        colorScheme: 'light',
-        pointer: 'fine',
-      },
-      subjects: resolvedSubjects,
-      requiredFacts: requiredFacts ?? {
-        geometry: true,
-        fragments: true,
-        styles: true,
-        topology: true,
-      },
-    }
-    const cdpResponse = await extractor.extract(cdpRequest)
-    if (cdpResponse.status === 'error') {
-      throw new Error('CDP extraction failed for relational evaluation')
-    }
-
-    const snapshot = cdpResponse.snapshots[0]
-    const canonical = adaptSnapshotToCanonical(snapshot)
-    const world = adaptCanonicalWorldToSolver(canonical as any) as GeometryWorld
-    ;(world as any).styles = {
-      subjectId: Array.from(canonical.styles.subjectId),
-      lineHeight: Array.from(canonical.styles.lineHeight),
-      fontFamilyStringId: Array.from(canonical.styles.fontFamilyStringId),
-      fontSize: Array.from(canonical.styles.fontSize),
-      fontWeight: Array.from(canonical.styles.fontWeight),
-    }
-
-    const selectorToIds = new Map<string, number[]>()
-    for (const [selectorKey, nodeIds] of selectorToNodeIds) {
-      const idSet = new Set(nodeIds)
-      const matches: number[] = []
-      for (let i = 0; i < world.subjects.ids.length; i++) {
-        const domNodeId = world.subjects.domNodeId[i]
-        if (idSet.has(domNodeId)) {
-          matches.push(world.subjects.ids[i])
-        }
-      }
-      selectorToIds.set(selectorKey, matches)
-    }
-
-    return { world, selectorToIds, errors }
-  } finally {
-    await playwrightPage.evaluate(() => {
-      const nodes = Array.from(document.querySelectorAll('[data-imhotep-runtime-id]'))
-      for (const el of nodes) {
-        el.removeAttribute('data-imhotep-runtime-id')
-      }
-    }).catch(() => {})
-    await sessionManager.detach()
-  }
-}
-
-async function extractWorld(
-  playwrightPage: Page,
-  selectors: string[],
-  cacheDir?: string | null,
-  requiredFacts?: { geometry: boolean; topology: boolean; styles: boolean; fragments: boolean },
-  allowFastGeometry = false,
-): Promise<{ world: GeometryWorld; selectorToIds: Map<string, number[]>; errors: ImhotepDiagnostic[] }> {
-  async function resolveViewport(): Promise<{ width: number; height: number }> {
-    const direct = typeof playwrightPage.viewportSize === 'function' ? playwrightPage.viewportSize() : null
-    if (direct && direct.width > 0 && direct.height > 0) {
-      return { width: direct.width, height: direct.height }
-    }
-    try {
-      const measured = await playwrightPage.evaluate(() => ({
-        width: window.innerWidth || document.documentElement?.clientWidth || 0,
-        height: window.innerHeight || document.documentElement?.clientHeight || 0,
-      }))
-      return {
-        width: Number.isFinite(measured?.width) ? Number(measured.width) : 0,
-        height: Number.isFinite(measured?.height) ? Number(measured.height) : 0,
-      }
-    } catch {
-      return { width: 0, height: 0 }
-    }
-  }
-
-  maybeInstallExtractionStatsHook()
-  const filteredSelectors = selectors.filter((s) => typeof s === 'string' && s.length > 0)
-  const pageUrl = playwrightPage.url?.() ?? ''
-  const viewport = await resolveViewport()
-  const env = {
-    viewportWidth: viewport.width,
-    viewportHeight: viewport.height,
-    colorScheme: 'light',
-    pointer: 'fine',
-  }
-
-  const resolvedCacheDir = cacheDir === null ? null : (cacheDir ?? getDefaultCacheDir())
-  const cacheNamespace = getPageCacheNamespace(playwrightPage)
-  const cacheSelectors = requiredFacts
-    ? [...filteredSelectors, `__imhotep_facts:${requiredFacts.geometry ? 'g' : ''}${requiredFacts.topology ? 't' : ''}${requiredFacts.styles ? 's' : ''}${requiredFacts.fragments ? 'f' : ''}:${allowFastGeometry ? 'fast' : 'cdp'}`, `__imhotep_page_ns:${cacheNamespace}`]
-    : [...filteredSelectors, `__imhotep_page_ns:${cacheNamespace}`]
-
-  if (resolvedCacheDir !== null) {
-    const cacheKey = computeGeometryCacheKey(pageUrl, cacheSelectors, env)
-    const cached = await readCachedExtractionResult(resolvedCacheDir, cacheKey)
-    if (cached) {
-      return {
-        world: cached.world as unknown as GeometryWorld,
-        selectorToIds: cached.selectorToIds,
-        errors: cached.errors as unknown as ImhotepDiagnostic[],
-      }
-    }
-  }
-
-  const useFastGeometry = allowFastGeometry
-    && requiredFacts?.geometry === true
-    && requiredFacts.topology === false
-
-  const result = useFastGeometry
-    ? await extractWorldFastGeometry(playwrightPage, filteredSelectors, requiredFacts)
-    : await extractWorldCdp(playwrightPage, filteredSelectors, requiredFacts)
-
-  ;(result.world as any).env = {
-    ...(result.world as any).env,
-    viewportWidth: env.viewportWidth,
-    viewportHeight: env.viewportHeight,
-  }
-
-  if (requiredFacts?.styles) {
-    try {
-      const plans: SelectorPlan[] = await Promise.all(
-        filteredSelectors.map(async (key, i) => {
-          const queries = await materializeSemanticSelector(playwrightPage, key, i)
-          return { key, queries }
-        }),
-      )
-      const chWidthsBySelector = await measureChWidthsByPlan(playwrightPage, plans)
-      attachMeasuredChWidths(result.world, result.selectorToIds, chWidthsBySelector)
-    } catch {
-      // Best effort only; solver falls back to font-size heuristic.
-    }
-  }
-
-  if (useFastGeometry) {
-    extractionPathStats.fastPathHits += 1
-  } else {
-    extractionPathStats.cdpFallbacks += 1
-  }
-
-  if (resolvedCacheDir !== null) {
-    const cacheKey = computeGeometryCacheKey(pageUrl, cacheSelectors, env)
-    await writeCachedExtractionResult(
-      resolvedCacheDir,
-      cacheKey,
-      result.world as unknown as import('imhotep-core').GeometryWorld,
-      result.selectorToIds,
-      result.errors as any,
-    )
-  }
-
-  return result
-}
-
-// ---------------------------------------------------------------------------
-// Domain Resolver
-// ---------------------------------------------------------------------------
-
-class SelectorDomainResolver implements DomainResolver {
-  private domains = new Map<string, DomainValue>()
-
-  register(selector: string, subjectIds: number[]) {
-    this.domains.set(selector, {
-      domainId: `dom_${selector}`,
-      subjectIds: new Uint32Array(subjectIds),
-      provenance: `elements(${selector})`,
-      closed: true,
-    })
-  }
-
-  resolve(domain: DomainRef): DomainValue | undefined {
-    return this.domains.get(domain.selector ?? domain.domain)
-  }
-}
-
-function compileCanonicalClauseToFormula(clause: CanonicalClauseDescriptor): FormulaNode {
-  const extended = clause as CanonicalClauseDescriptor & {
-    space?: 'layout' | 'visual'
-    options?: Record<string, unknown>
-  }
-  const subjectVar = { type: 'VariableRef' as const, name: '$subject' }
-  const referenceVar = { type: 'VariableRef' as const, name: '$reference' }
-
-  const options: Record<string, unknown> = {}
-  if (clause.bounds?.minGap !== undefined) options.minGap = clause.bounds.minGap
-  if (clause.bounds?.maxGap !== undefined) options.maxGap = clause.bounds.maxGap
-  if (clause.tolerance?.value !== undefined) options.tolerance = clause.tolerance.value
-  if (extended.space) options.space = extended.space
-  if (extended.options) {
-    for (const [k, v] of Object.entries(extended.options)) {
-      options[k] = v
-    }
-  }
-
-  // ---------------------------------------------------------------------------
-  // Compile relation-specific body
-  // ---------------------------------------------------------------------------
-
-  let body: FormulaNode
-
-  // between size assertion → atLeast(min) AND atMost(max)
-  if (clause.relation === 'between') {
-    const minVal = extended.options?.min as number | undefined
-    const maxVal = extended.options?.max as number | undefined
-    const atLeastOpts: Record<string, unknown> = {}
-    const atMostOpts: Record<string, unknown> = {}
-    if (extended.options?.dimension !== undefined) {
-      atLeastOpts.dimension = extended.options.dimension
-      atMostOpts.dimension = extended.options.dimension
-    }
-    body = {
-      type: 'FormulaNode',
-      kind: 'and',
-      left: {
-        type: 'FormulaNode',
-        kind: 'predicate',
-        predicate: 'atLeast',
-        args: [subjectVar],
-        ...(minVal !== undefined ? { options: { ...atLeastOpts, value: minVal } } : { options: atLeastOpts }),
-      } as FormulaNode,
-      right: {
-        type: 'FormulaNode',
-        kind: 'predicate',
-        predicate: 'atMost',
-        args: [subjectVar],
-        ...(maxVal !== undefined ? { options: { ...atMostOpts, value: maxVal } } : { options: atMostOpts }),
-      } as FormulaNode,
-    }
-  }
-  // separatedFrom → not(overlaps) with margin from gap options
-  else if (clause.relation === 'separatedFrom') {
-    const overlapsOpts: Record<string, unknown> = { ...options }
-    body = {
-      type: 'FormulaNode',
-      kind: 'not',
-      operand: {
-        type: 'FormulaNode',
-        kind: 'predicate',
-        predicate: 'overlaps',
-        args: [subjectVar, referenceVar],
-        ...(Object.keys(overlapsOpts).length > 0 ? { options: overlapsOpts } : {}),
-      } as FormulaNode,
-    }
-  }
-  // Default: compile as direct predicate call
-  else {
-    const unaryPredicate = clause.relation === 'atLeast'
-      || clause.relation === 'atMost'
-      || clause.relation === 'aspectRatio'
-
-    body = {
-      type: 'FormulaNode',
-      kind: 'predicate',
-      predicate: clause.relation,
-      args: unaryPredicate ? [subjectVar] : [subjectVar, referenceVar],
-      ...(Object.keys(options).length > 0 ? { options } : {}),
-    } as FormulaNode
-
-    if ((clause.flags & 8) !== 0 && !unaryPredicate) {
-      body = {
-        type: 'FormulaNode',
-        kind: 'and',
-        left: body,
-        right: {
-          type: 'FormulaNode',
-          kind: 'predicate',
-          predicate: 'inStackingContext',
-          args: [subjectVar, referenceVar],
-        },
-      }
-    }
-  }
-
-  // Negation: wrap body in not() if clause is negated
-  if (clause.negated) {
-    body = {
-      type: 'FormulaNode',
-      kind: 'not',
-      operand: body,
-    }
-  }
-
-  const subjectBinding = {
-    type: 'TupleBinding' as const,
-    variables: ['$subject'],
-    domain: { type: 'DomainRef' as const, domain: 'elements', selector: clause.subject },
-  }
-  const referenceBinding = {
-    type: 'TupleBinding' as const,
-    variables: ['$reference'],
-    domain: { type: 'DomainRef' as const, domain: 'elements', selector: clause.reference },
-  }
-
-  // between and other unary predicates use single binding
-  const isUnary = clause.relation === 'atLeast'
-    || clause.relation === 'atMost'
-    || clause.relation === 'between'
-    || clause.relation === 'aspectRatio'
-
-  if (isUnary) {
-    return {
-      type: 'FormulaNode',
-      kind: 'forall',
-      bindings: [subjectBinding],
-      body,
-    }
-  }
-
-  if (clause.quantifier === 'any') {
-    return {
-      type: 'FormulaNode',
-      kind: 'exists',
-      bindings: [subjectBinding],
-      body: {
-        type: 'FormulaNode',
-        kind: 'forall',
-        bindings: [referenceBinding],
-        body,
-      },
-    }
-  }
-
-  if (clause.quantifier === 'none') {
-    return {
-      type: 'FormulaNode',
-      kind: 'forall',
-      bindings: [subjectBinding],
-      body: {
-        type: 'FormulaNode',
-        kind: 'not',
-        operand: {
-          type: 'FormulaNode',
-          kind: 'exists',
-          bindings: [referenceBinding],
-          body,
-        },
-      },
-    }
-  }
-
-  return {
-    type: 'FormulaNode',
-    kind: 'forall',
-    bindings: [subjectBinding, referenceBinding],
-    body,
-  }
-}
-
-function getSelectorsFromAssertion(assertion: FluentRelation | FluentAssertion | FluentQuantifier): string[] {
-  const selectors = new Set<string>()
-  const rel = assertion as any
-  if (rel.assertion?.getSubject) {
-    selectors.add(rel.assertion.getSubject())
-  }
-  if (rel.referenceSelector) {
-    selectors.add(rel.referenceSelector)
-  }
-  // Extract selectors from compound relation parts (.and / .or chaining)
-  if (Array.isArray(rel._compoundParts)) {
-    for (const part of rel._compoundParts) {
-      if (part.referenceSelector) {
-        selectors.add(part.referenceSelector)
-      }
-    }
-  }
-  if (Array.isArray(rel.bindings)) {
-    for (const b of rel.bindings) {
-      if (b?.selector) selectors.add(b.selector)
-      // Extract reference selectors from assertions inside FluentQuantifier bindings
-      if (typeof b?.getAssertions === 'function') {
-        for (const assertion of b.getAssertions()) {
-          if (assertion?.reference?.value) {
-            selectors.add(assertion.reference.value)
-          }
-        }
-      }
-    }
-  }
-  return Array.from(selectors)
-}
-
-function getSelectorsFromFormula(formula: FormulaNode): string[] {
-  const selectors = new Set<string>()
-  const visit = (node: FormulaNode) => {
-    if (node.kind === 'forall' || node.kind === 'exists') {
-      for (const b of node.bindings) {
-        if (b.domain.selector && !b.domain.selector.startsWith('$')) {
-          selectors.add(b.domain.selector)
-        }
-      }
-      visit(node.body)
-      return
-    }
-    if (node.kind === 'and' || node.kind === 'or') {
-      visit(node.left)
-      visit(node.right)
-      return
-    }
-    if (node.kind === 'not') {
-      visit(node.operand)
-      return
-    }
-    if (node.kind === 'implies') {
-      visit(node.antecedent)
-      visit(node.consequent)
-    }
-  }
-  visit(formula)
-  return Array.from(selectors)
-}
-
-// ---------------------------------------------------------------------------
-// Clause Label Builders
-// ---------------------------------------------------------------------------
-
-function buildFluentLabel(assertion: FluentRelation | FluentAssertion | FluentQuantifier): string {
-  const rel = assertion as any
-
-  // FluentQuantifier
-  if (rel.bindings && Array.isArray(rel.bindings)) {
-    const firstBinding = rel.bindings[0]
-    const selector = firstBinding?.selector || 'unknown'
-    return `quantified assertion over '${selector}'`
-  }
-
-  // FluentRelation
-  if (rel.relation && rel.assertion?.getSubject) {
-    const subject = rel.assertion.getSubject()
-    const ref = rel.referenceSelector || ''
-    const opts = rel.options || {}
-    const parts: string[] = [`'${subject}' ${rel.relation}`]
-    if (ref) parts.push(`'${ref}'`)
-    if (opts.minGap !== undefined) parts.push(`gap ${opts.minGap}px`)
-    if (opts.maxGap !== undefined) parts.push(`maxGap ${opts.maxGap}px`)
-    if (opts.tolerance !== undefined) parts.push(`tolerance ${opts.tolerance}px`)
-    if (opts.axis) parts.push(`axis ${opts.axis}`)
-    return parts.join(' ')
-  }
-
-  return 'fluent assertion'
-}
-
-function buildDenseLabel(clause: CanonicalClauseDescriptor): string {
-  const parts: string[] = [`'${clause.subject}' ${clause.relation}`]
-  if (clause.reference) parts.push(`'${clause.reference}'`)
-  if (clause.bounds?.minGap !== undefined) parts.push(`gap ${clause.bounds.minGap}px`)
-  if (clause.bounds?.maxGap !== undefined) parts.push(`maxGap ${clause.bounds.maxGap}px`)
-  if (clause.tolerance) parts.push(`tolerance ${clause.tolerance.value}${clause.tolerance.unit}`)
-  if (clause.quantifier && clause.quantifier !== 'all') parts.unshift(clause.quantifier)
-  return parts.join(' ')
-}
-
-function buildFOLLabel(folAst: any): string {
-  switch (folAst.type) {
-    case 'ForAll':
-      return `forall ${folAst.variable?.name} in ${folAst.domain?.kind}(${folAst.domain?.selector ?? ''})`
-    case 'Exists':
-      return `exists ${folAst.variable?.name} in ${folAst.domain?.kind}(${folAst.domain?.selector ?? ''})`
-    case 'And':
-      return `${buildFOLLabel(folAst.left)} and ${buildFOLLabel(folAst.right)}`
-    case 'Or':
-      return `${buildFOLLabel(folAst.left)} or ${buildFOLLabel(folAst.right)}`
-    case 'Not':
-      return `not ${buildFOLLabel(folAst.operand)}`
-    case 'Implies':
-      return `${buildFOLLabel(folAst.left)} implies ${buildFOLLabel(folAst.right)}`
-    case 'PredicateCall':
-      return `${folAst.name}(${folAst.args.map((a: any) => a.name ?? a).join(', ')})`
-    default:
-      return 'FOL formula'
-  }
-}
-
-// ---------------------------------------------------------------------------
-// Normalized Contract Builder
-// ---------------------------------------------------------------------------
-
-function extractCanonicalFromAssertion(
-  assertion: FluentRelation | FluentAssertion | FluentQuantifier,
-): CanonicalClauseDescriptor[] {
-  if (assertion instanceof FluentRelation) {
-    const ast = assertion.toAst()
-    return lowerToCanonical(ast)
-  }
-  if (assertion instanceof FluentQuantifier) {
-    const descriptors: CanonicalClauseDescriptor[] = []
-    for (const binding of assertion.bindings) {
-      for (const a of binding.getAssertions()) {
-        descriptors.push(...lowerToCanonical(a))
-      }
-    }
-    return descriptors
-  }
-  // FluentAssertion without a completed relation produces no descriptors.
-  return []
-}
-
-function buildNormalizedContracts(
-  assertions: (FluentRelation | FluentAssertion | FluentQuantifier)[],
-  specs: string[],
-): NormalizedContract[] {
-  const contracts: NormalizedContract[] = []
-  let index = 0
-
-  for (const assertion of assertions) {
-    const descriptors = extractCanonicalFromAssertion(assertion)
-    for (const desc of descriptors) {
-      contracts.push(descriptorToContract(desc, index++))
-    }
-  }
-
-  for (const source of specs) {
-    if (source.trim().length === 0) continue
-    const parsed = parseSpec(source)
-    if (parsed.diagnostics.some((d) => d.severity === 'error')) continue
-    const descriptors = lowerToCanonical(parsed.ast)
-    for (const desc of descriptors) {
-      contracts.push(descriptorToContract(desc, index++))
-    }
-  }
-
-  return contracts
-}
-
-function descriptorToContract(
-  desc: CanonicalClauseDescriptor,
-  index: number,
-): NormalizedContract {
-  const options: Record<string, unknown> = {}
-  if (desc.bounds) {
-    if (desc.bounds.minGap !== undefined) options.minGap = desc.bounds.minGap
-    if (desc.bounds.maxGap !== undefined) options.maxGap = desc.bounds.maxGap
-  }
-  if (desc.tolerance) {
-    options.tolerance = desc.tolerance.value
-    options.toleranceUnit = desc.tolerance.unit
-  }
-  if (desc.options) {
-    for (const [k, v] of Object.entries(desc.options)) {
-      if (options[k] === undefined) options[k] = v
-    }
-  }
-  if (desc.quantifier) {
-    options.quantifier = desc.quantifier
-  }
-  if (desc.space) {
-    options.space = desc.space
-  }
-
-  const labelParts: string[] = []
-  labelParts.push(`'${desc.subject}'`)
-  labelParts.push(desc.relation)
-  if (desc.reference) {
-    labelParts.push(`'${desc.reference}'`)
-  }
-
-  const optionEntries = Object.entries(options)
-  if (optionEntries.length > 0) {
-    const optionStr = optionEntries
-      .map(([k, v]) => `${k}: ${JSON.stringify(v)}`)
-      .join(', ')
-    labelParts.push(`with ${optionStr}`)
-  }
-
-  return {
-    clauseId: `contract_${index}`,
-    clauseLabel: labelParts.join(' '),
-    relation: desc.relation,
-    subject: desc.subject,
-    reference: desc.reference || '',
-    options,
-  }
-}
-
 // ---------------------------------------------------------------------------
 // LLM Format Output (P2.2)
 // ---------------------------------------------------------------------------
@@ -1415,598 +208,6 @@ import { formatAsLLM } from './llm-output.js'
 
 export { formatAsLLM }
 
-// ---------------------------------------------------------------------------
-// Cardinality Assertion Evaluation
-// ---------------------------------------------------------------------------
-
-interface CardinalityResult {
-  clauseId: string
-  status: ClauseResult['status']
-  truth: ClauseResult['truth']
-  diagnostics: ImhotepDiagnostic[]
-  selector: string
-  expectedCount: number
-  label: string
-}
-
-function buildCardinalityLabel(kind: 'exactlyOne' | 'atLeastN' | 'atMostN', selector: string, expectedCount: number): string {
-  if (kind === 'exactlyOne') return `'${selector}' exactlyOne`
-  if (kind === 'atLeastN') return `'${selector}' atLeastN ${expectedCount}`
-  return `'${selector}' atMostN ${expectedCount}`
-}
-
-function evaluateCardinalityAssertion(
-  assertion: any,
-  clauseId: string,
-  selectorToIds: Map<string, number[]>,
-): CardinalityResult {
-  const selector = assertion.assertion?.getSubject?.() ?? assertion.selector ?? ''
-  const kind = assertion.kind as 'exactlyOne' | 'atLeastN' | 'atMostN'
-  const expectedCount = assertion.expectedCount as number
-  const ids = selectorToIds.get(selector) ?? []
-  const observedCount = ids.length
-  const label = buildCardinalityLabel(kind, selector, expectedCount)
-
-  let pass = false
-  let expectedDescription = ''
-
-  switch (kind) {
-    case 'exactlyOne':
-      pass = observedCount === 1
-      expectedDescription = 'exactly 1'
-      break
-    case 'atLeastN':
-      pass = observedCount >= expectedCount
-      expectedDescription = `at least ${expectedCount}`
-      break
-    case 'atMostN':
-      pass = observedCount <= expectedCount
-      expectedDescription = `at most ${expectedCount}`
-      break
-  }
-
-  const diagnostics: ImhotepDiagnostic[] = []
-  if (!pass) {
-    diagnostics.push({
-      code: `IMH_CARDINALITY_${kind.toUpperCase()}_FAILED` as DiagnosticCode,
-      severity: 'error',
-      category: 'contract-failure',
-      message: `Selector "${selector}" resolved to ${observedCount} element(s), but expected ${expectedDescription}.`,
-      source: 'imhotep-playwright',
-      related: [],
-      fixHints: [
-        `Check that "${selector}" matches the intended number of elements.`,
-        `Use ui.extract('${selector}') to verify the selector resolves to the expected count.`,
-      ],
-      metrics: { observedCount, expectedCount },
-      sourceRef: { selector },
-      clauseLabel: label,
-    })
-  }
-
-  return {
-    clauseId,
-    status: pass ? 'pass' : 'fail',
-    truth: 'determinate',
-    diagnostics,
-    selector,
-    expectedCount,
-    label,
-  }
-}
-
-// ---------------------------------------------------------------------------
-// Result Adapter: FOL → Public API shape
-// ---------------------------------------------------------------------------
-
-const PREDICATE_TO_DIAGNOSTIC_CODE: Record<string, DiagnosticCode> = {
-  leftOf: 'IMH_RELATION_LEFT_OF_FAILED',
-  rightOf: 'IMH_RELATION_RIGHT_OF_FAILED',
-  above: 'IMH_RELATION_ABOVE_FAILED',
-  below: 'IMH_RELATION_BELOW_FAILED',
-  inside: 'IMH_RELATION_INSIDE_FAILED',
-  contains: 'IMH_RELATION_CONTAINS_FAILED',
-  alignedWith: 'IMH_ALIGNMENT_FAILED',
-  centeredWithin: 'IMH_RELATION_CENTERED_FAILED',
-  overlaps: 'IMH_RELATION_OVERLAPS_FAILED',
-  atLeast: 'IMH_SIZE_AT_LEAST_FAILED',
-  atMost: 'IMH_SIZE_AT_MOST_FAILED',
-  between: 'IMH_SIZE_BETWEEN_FAILED',
-}
-
-function mapFolDiagnostic(d: { code: string; severity: 'error' | 'warning' | 'info'; category?: string; message: string; clauseId?: string }): ImhotepDiagnostic {
-  let code = d.code as DiagnosticCode
-  let message = d.message
-  const fixHints: string[] = []
-
-  // Map missing predicate to the old unknown-clause code.
-  if ((code as string) === 'IMH_LOGIC_PREDICATE_MISSING') {
-    code = 'IMH_INTERNAL_UNKNOWN_CLAUSE_KIND'
-    fixHints.push('The assertion uses an unsupported relation or predicate.')
-    fixHints.push('Supported relations: leftOf, rightOf, above, below, alignedWith, centeredWithin, inside, contains, overlaps.')
-  }
-
-  // Map generic predicate failure to relation-specific code for backward compat.
-  if ((code as string) === 'IMH_PREDICATE_FAILED') {
-    const match = message.match(/Predicate "([^"]+)" failed/)
-    const predicateName = match?.[1]
-    if (predicateName && PREDICATE_TO_DIAGNOSTIC_CODE[predicateName]) {
-      code = PREDICATE_TO_DIAGNOSTIC_CODE[predicateName]
-      // Rebuild the message in the old format for spatial relations.
-      const gapMatch = message.match(/gap=([\d.-]+)/)
-      const observedGap = gapMatch ? parseFloat(gapMatch[1]) : undefined
-      const minGapMatch = message.match(/minGap=([\d.-]+)/)
-      const minGap = minGapMatch ? parseFloat(minGapMatch[1]) : undefined
-      const maxGapMatch = message.match(/maxGap=([\d.-]+)/)
-      const maxGap = maxGapMatch ? parseFloat(maxGapMatch[1]) : undefined
-      const gapKind = observedGap !== undefined && maxGap !== undefined && minGap !== undefined
-        ? (observedGap < minGap ? 'min' : observedGap > maxGap ? 'max' : 'min')
-        : 'min'
-      const expectedGap = gapKind === 'min' ? (minGap ?? 0) : (maxGap ?? 0)
-      const boundDescription = gapKind === 'min' ? 'minimum required gap' : 'maximum required gap'
-      if (predicateName === 'leftOf' && observedGap !== undefined) {
-        message = `leftOf assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
-        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
-      } else if (predicateName === 'above' && observedGap !== undefined) {
-        message = `above assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
-        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
-      } else if (predicateName === 'below' && observedGap !== undefined) {
-        message = `below assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
-        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
-      } else if (predicateName === 'rightOf' && observedGap !== undefined) {
-        message = `rightOf assertion failed: measured gap is ${observedGap.toFixed(0)}px, but ${boundDescription} is ${expectedGap}px.`
-        fixHints.push(`The measured gap is ${observedGap.toFixed(0)}px. Consider ${gapKind === 'min' ? 'lowering minGap' : 'increasing maxGap'} or checking element positions.`)
-      } else if (predicateName === 'atLeast' || predicateName === 'atMost' || predicateName === 'between') {
-        fixHints.push(`Check the expected size threshold and the actual element dimensions using ui.extract(selector).`)
-      } else {
-        fixHints.push(`Verify the expected layout and consider adjusting thresholds.`)
-      }
-    } else {
-      fixHints.push(`Verify the expected layout and consider adjusting thresholds.`)
-    }
-  }
-
-  // Add fixHints for specific known error codes.
-  if (code === 'IMH_SELECTOR_ZERO_MATCHES') {
-    fixHints.push('Check that the selector is valid and matches an element in the DOM.')
-    fixHints.push('Use ui.extract(selector) to verify the selector resolves to at least one element.')
-  }
-
-  if (code === 'IMH_EXTRACT_PROTOCOL_ERROR') {
-    fixHints.push('Verify the page is fully loaded before running assertions.')
-    fixHints.push('Check that selectors are valid CSS selectors or semantic references.')
-    fixHints.push('Use ui.extract(selector) to debug selector resolution.')
-  }
-
-  if ((code as string) === 'IMH_FEATURE_NOT_YET_IMPLEMENTED') {
-    fixHints.push('This assertion uses a relation that is documented but not yet implemented.')
-    fixHints.push('Use a supported relation such as leftOf, rightOf, above, below, inside, overlaps, alignedWith, or centeredWithin.')
-  }
-
-  const codeStr = code as string
-  if (codeStr === 'IMH_PARSE_ERROR' || codeStr === 'IMH_PARSE_INVALID_SYNTAX' || codeStr === 'IMH_PARSE_UNEXPECTED_TOKEN') {
-    fixHints.push('Selectors must be single-quoted strings, e.g. \'[data-testid="x"]\'.')
-    fixHints.push('Use relation keywords directly without "is": e.g. \'a\' leftOf \'b\'.')
-    fixHints.push('Gap values require units: e.g. gap 8px.')
-  }
-
-  // Fallback: if no specific fixHints were added, look them up in the registry.
-  if (fixHints.length === 0) {
-    const entry = lookupCode(code)
-    if (entry?.fixHints && entry.fixHints.length > 0) {
-      fixHints.push(...entry.fixHints)
-    }
-  }
-
-  return {
-    code,
-    severity: d.severity,
-    category: (d.category ?? 'internal-error') as ImhotepDiagnostic['category'],
-    message,
-    clauseId: d.clauseId,
-    source: 'imhotep-solver',
-    related: [],
-    fixHints,
-    metrics: {},
-    sourceRef: {},
-  }
-}
-
-interface TraceMetadata {
-  sourceRef?: SourceReference
-  clauseLabel?: string
-}
-
-function isDuckTypedFluentQuantifier(value: unknown): boolean {
-  return !!value
-    && typeof value === 'object'
-    && Array.isArray((value as any).bindings)
-    && typeof (value as any).toFormula === 'function'
-}
-
-function hasSubjectQuantifier(value: unknown): boolean {
-  if (!value || typeof value !== 'object') return false
-  const assertion = (value as any).assertion
-  return !!assertion && typeof assertion.getQuantifier === 'function' && assertion.getQuantifier() !== undefined
-}
-
-function findNearestPackageJson(startPath: string): string | null {
-  let current = path.dirname(startPath)
-  for (let i = 0; i < 16; i++) {
-    const candidate = path.join(current, 'package.json')
-    if (fs.existsSync(candidate)) return candidate
-    const parent = path.dirname(current)
-    if (parent === current) break
-    current = parent
-  }
-  return null
-}
-
-function resolvePackageFingerprint(name: string): { name: string; version: string; resolvedFrom: string } {
-  try {
-    const resolvedEntry = cjsRequire.resolve(name)
-    const pkgJson = findNearestPackageJson(resolvedEntry)
-    if (!pkgJson) {
-      return {
-        name,
-        version: 'unknown',
-        resolvedFrom: resolvedEntry,
-      }
-    }
-    const content = fs.readFileSync(pkgJson, 'utf8')
-    const parsed = JSON.parse(content) as { version?: string }
-    return {
-      name,
-      version: typeof parsed.version === 'string' ? parsed.version : 'unknown',
-      resolvedFrom: pkgJson,
-    }
-  } catch (err) {
-    return {
-      name,
-      version: 'unresolved',
-      resolvedFrom: err instanceof Error ? err.message : String(err),
-    }
-  }
-}
-
-function collectPackageFingerprints(): Array<{ name: string; version: string; resolvedFrom: string }> {
-  return [
-    resolvePackageFingerprint('imhotep-playwright'),
-    resolvePackageFingerprint('imhotep-dsl'),
-    resolvePackageFingerprint('imhotep-solver'),
-  ]
-}
-
-function buildCompatibilityReport(ui: ImhotepUi): CompatibilityReport {
-  const checks: CompatibilityCheck[] = []
-  const packageFingerprints = collectPackageFingerprints()
-
-  const packageResolutionOk = packageFingerprints.every((p) => p.version !== 'unresolved')
-  checks.push({
-    id: 'package-fingerprints-resolved',
-    ok: packageResolutionOk,
-    details: packageFingerprints.map((p) => `${p.name}@${p.version}`).join(', '),
-  })
-
-  const unitsSource = "in viewport:\n  '.probe' atMost 85vw wide\n  '.probe' atMost 60ch wide"
-  const parsedUnits = parseSpec(unitsSource)
-  const hasUnitsParseError = parsedUnits.diagnostics.some((d) => d.severity === 'error')
-  const unitsClauses = hasUnitsParseError ? 0 : lowerToCanonical(parsedUnits.ast).length
-  checks.push({
-    id: 'dsl-units-vw-ch',
-    ok: !hasUnitsParseError && unitsClauses === 2,
-    details: hasUnitsParseError
-      ? `parse errors: ${parsedUnits.diagnostics.map((d) => String(d.code)).join(', ')}`
-      : `parsed clauses=${unitsClauses}`,
-  })
-
-  const loweredUnits = hasUnitsParseError ? [] : lowerToCanonical(parsedUnits.ast)
-  const firstMax = loweredUnits[0]?.options?.max as any
-  const secondMax = loweredUnits[1]?.options?.max as any
-  const loweredUnitsOk =
-    !!firstMax
-    && typeof firstMax === 'object'
-    && firstMax.value === 85
-    && firstMax.unit === 'vw'
-    && !!secondMax
-    && typeof secondMax === 'object'
-    && secondMax.value === 60
-    && secondMax.unit === 'ch'
-  checks.push({
-    id: 'dsl-size-unit-lowering',
-    ok: loweredUnitsOk,
-    details: `first=${JSON.stringify(firstMax ?? null)}, second=${JSON.stringify(secondMax ?? null)}`,
-  })
-
-  const hasQuantifierHelpers = typeof ui.expect.all === 'function' && typeof ui.expect.any === 'function' && typeof ui.expect.none === 'function'
-  checks.push({
-    id: 'expect-quantifier-helpers',
-    ok: hasQuantifierHelpers,
-    details: `all=${typeof ui.expect.all}, any=${typeof ui.expect.any}, none=${typeof ui.expect.none}`,
-  })
-
-  const priorAssertions = [...(assertionStore.get(ui) || [])]
-  const priorSpecs = [...(specStore.get(ui) || [])]
-  let expectAllInvocationOk = false
-  let expectAllInvocationDetails = 'not executed'
-  try {
-    const chain = ui.expect.all('.__imhotep_compat_none__').to.be.atLeast(1, 'height') as any
-    expectAllInvocationOk = !!chain && typeof chain === 'object' && !!chain.assertion && chain.assertion.getQuantifier?.() === 'all'
-    expectAllInvocationDetails = `chain=${typeof chain}, quantifier=${chain?.assertion?.getQuantifier?.()}`
-  } catch (err) {
-    expectAllInvocationDetails = err instanceof Error ? err.message : String(err)
-  } finally {
-    assertionStore.set(ui, priorAssertions)
-    specStore.set(ui, priorSpecs)
-  }
-  checks.push({
-    id: 'expect-all-chain-invocation',
-    ok: expectAllInvocationOk,
-    details: expectAllInvocationDetails,
-  })
-
-  const emptyResolver: DomainResolver = {
-    resolve(domain) {
-      if (domain.selector === '.none') {
-        return {
-          domainId: 'dom_none',
-          subjectIds: new Uint32Array([]),
-          provenance: 'elements(.none)',
-          closed: true,
-        }
-      }
-      return undefined
-    },
-  }
-
-  const emptyWorld = buildGeometryWorld([]) as unknown as GeometryWorld
-  const forallEmpty = evaluateLogic({
-    formula: {
-      type: 'FormulaNode',
-      kind: 'forall',
-      bindings: [{
-        type: 'TupleBinding',
-        variables: ['$x'],
-        domain: { type: 'DomainRef', domain: 'elements', selector: '.none' },
-      }],
-      body: {
-        type: 'FormulaNode',
-        kind: 'predicate',
-        predicate: 'atLeast',
-        args: [{ type: 'VariableRef', name: '$x' }],
-        options: { value: 1, dimension: 'height' },
-      },
-    } as FormulaNode,
-    world: emptyWorld,
-    resolver: emptyResolver,
-    options: { trace: false },
-  })
-  const existsEmpty = evaluateLogic({
-    formula: {
-      type: 'FormulaNode',
-      kind: 'exists',
-      bindings: [{
-        type: 'TupleBinding',
-        variables: ['$x'],
-        domain: { type: 'DomainRef', domain: 'elements', selector: '.none' },
-      }],
-      body: {
-        type: 'FormulaNode',
-        kind: 'predicate',
-        predicate: 'atLeast',
-        args: [{ type: 'VariableRef', name: '$x' }],
-        options: { value: 1, dimension: 'height' },
-      },
-    } as FormulaNode,
-    world: emptyWorld,
-    resolver: emptyResolver,
-    options: { trace: false },
-  })
-  const quantifierEmptyDomainOk =
-    forallEmpty.passed
-    && existsEmpty.passed === false
-    && existsEmpty.diagnostics.some((d) => d.code === 'IMH_LOGIC_EMPTY_DOMAIN_EXISTS')
-  checks.push({
-    id: 'quantifier-empty-domain-semantics',
-    ok: quantifierEmptyDomainOk,
-    details: `forallPassed=${forallEmpty.passed}, existsPassed=${existsEmpty.passed}`,
-  })
-
-  const insideWorld = buildGeometryWorld([
-    { tagName: 'div', rect: { x: 47, y: 537, width: 231, height: 47 } },
-    { tagName: 'div', rect: { x: 47, y: 482, width: 619, height: 518 } },
-  ]) as unknown as GeometryWorld
-  registerDefaultPredicates()
-  const insideEvaluator = getPredicateEvaluator('inside')
-  const insideEval = insideEvaluator?.evaluateTuple(insideWorld, [1, 2], {})
-  const insideMetrics = ((insideEval?.metrics ?? {}) as Record<string, number>)
-  const hasOverflowMetrics =
-    typeof insideMetrics.overflowTop === 'number'
-    || typeof insideMetrics.overflowBottom === 'number'
-    || typeof insideMetrics.overflowLeft === 'number'
-    || typeof insideMetrics.overflowRight === 'number'
-  const insideMetricsOk =
-    insideEval?.truth === 'true'
-    && (
-      !hasOverflowMetrics
-      || (
-        (insideMetrics.overflowTop ?? 0) === 0
-        && (insideMetrics.overflowBottom ?? 0) === 0
-        && (insideMetrics.overflowLeft ?? 0) === 0
-        && (insideMetrics.overflowRight ?? 0) === 0
-      )
-    )
-  checks.push({
-    id: 'inside-overflow-orientation',
-    ok: insideMetricsOk,
-    details: hasOverflowMetrics
-      ? `top=${insideMetrics.overflowTop ?? 'na'}, bottom=${insideMetrics.overflowBottom ?? 'na'}, left=${insideMetrics.overflowLeft ?? 'na'}, right=${insideMetrics.overflowRight ?? 'na'}`
-      : 'overflow metrics unavailable in solver output',
-  })
-
-  const sizeWorld = buildGeometryWorld([
-    { tagName: 'div', rect: { x: 0, y: 0, width: 527, height: 100 } },
-  ]) as unknown as GeometryWorld
-  ;(sizeWorld as any).env = {
-    ...((sizeWorld as any).env || {}),
-    viewportWidth: 1280,
-    viewportHeight: 720,
-  }
-  ;(sizeWorld as any).styles = {
-    subjectId: [1],
-    fontSize: [16],
-    chWidth: [9],
-  }
-  registerDefaultPredicates()
-  const atMostEvaluator = getPredicateEvaluator('atMost')
-  const vwResult = atMostEvaluator?.evaluateTuple(sizeWorld, [1], { dimension: 'width', max: { value: 85, unit: 'vw' } })
-  const chResult = atMostEvaluator?.evaluateTuple(sizeWorld, [1], { dimension: 'width', max: { value: 60, unit: 'ch' } })
-  const solverUnitsOk =
-    vwResult?.truth === 'true'
-    && (vwResult.metrics?.max ?? 0) > 1000
-    && chResult?.truth === 'true'
-    && Math.abs((chResult.metrics?.max ?? 0) - 540) < 0.0001
-  checks.push({
-    id: 'solver-size-unit-conversion',
-    ok: !!solverUnitsOk,
-    details: `vwTruth=${vwResult?.truth ?? 'na'}, vwMax=${vwResult?.metrics?.max ?? 'na'}, chTruth=${chResult?.truth ?? 'na'}, chMax=${chResult?.metrics?.max ?? 'na'}`,
-  })
-
-  return {
-    ok: checks.every((c) => c.ok),
-    generatedAt: new Date().toISOString(),
-    checks,
-    packageFingerprints,
-  }
-}
-
-function maybeEmitCompatibilityWarning(ui: ImhotepUi): void {
-  if (compatibilityWarningEmitted) return
-  const report = buildCompatibilityReport(ui)
-  if (report.ok) return
-  compatibilityWarningEmitted = true
-  const failed = report.checks.filter((c) => !c.ok)
-  const detail = failed.map((c) => `${c.id}: ${c.details}`).join(' | ')
-  const fingerprints = report.packageFingerprints
-    .map((p) => `${p.name}@${p.version} (${p.resolvedFrom})`)
-    .join(' | ')
-  // eslint-disable-next-line no-console
-  console.warn(`[imhotep-playwright] compatibility warning: ${detail}; fingerprints=${fingerprints}`)
-}
-
-function buildCompatibilityDiagnostic(report: CompatibilityReport): ImhotepDiagnostic | null {
-  if (report.ok) return null
-  const failed = report.checks.filter((c) => !c.ok)
-  const detail = failed.map((c) => `${c.id}: ${c.details}`).join(' | ')
-  const fingerprints = report.packageFingerprints
-    .map((p) => `${p.name}@${p.version}`)
-    .join(', ')
-  return {
-    code: 'IMH_INTERNAL_COMPAT_WARNING' as DiagnosticCode,
-    severity: 'warning',
-    category: 'internal-error',
-    message: `Runtime compatibility checks reported issues: ${detail}`,
-    source: 'imhotep-playwright',
-    related: [],
-    fixHints: [
-      `Resolved packages: ${fingerprints}`,
-      'Reinstall imhotep-playwright, imhotep-dsl, and imhotep-solver together from the same build.',
-    ],
-    metrics: {},
-    sourceRef: { file: 'public.ts' },
-    clauseLabel: 'compatibility',
-  }
-}
-
-function adaptFOLResultToImhotepResult(
-  folResult: ReturnType<typeof evaluateLogic>,
-  assertionCount: number,
-  clauseId?: string,
-  traceMeta?: TraceMetadata,
-): ImhotepResult {
-  const diagnostics: ImhotepDiagnostic[] = folResult.diagnostics.map((d) => {
-    const mapped = mapFolDiagnostic(d)
-    if (traceMeta?.sourceRef) mapped.sourceRef = traceMeta.sourceRef
-    if (traceMeta?.clauseLabel) mapped.clauseLabel = traceMeta.clauseLabel
-    return mapped
-  })
-
-  const clauseResults: ClauseResult[] = folResult.formulaResults.map((fr, idx) => {
-    const status: ClauseResult['status'] =
-      fr.outcome === 'indeterminate' ? 'error' : fr.outcome
-
-    const normalizedMetrics = (() => {
-      const raw = (fr.metrics || {}) as Record<string, unknown>
-      const hasInsideGeometry =
-        typeof raw.subjectTop === 'number'
-        && typeof raw.subjectBottom === 'number'
-        && typeof raw.subjectLeft === 'number'
-        && typeof raw.subjectRight === 'number'
-        && typeof raw.refTop === 'number'
-        && typeof raw.refBottom === 'number'
-        && typeof raw.refLeft === 'number'
-        && typeof raw.refRight === 'number'
-      if (!hasInsideGeometry) {
-        const hasOverflowOnly =
-          typeof raw.overflowTop === 'number'
-          || typeof raw.overflowBottom === 'number'
-          || typeof raw.overflowLeft === 'number'
-          || typeof raw.overflowRight === 'number'
-        if (hasOverflowOnly && fr.outcome === 'pass') {
-          return {
-            ...raw,
-            overflowTop: 0,
-            overflowBottom: 0,
-            overflowLeft: 0,
-            overflowRight: 0,
-          }
-        }
-        return raw
-      }
-
-      const subjectTop = raw.subjectTop as number
-      const subjectBottom = raw.subjectBottom as number
-      const subjectLeft = raw.subjectLeft as number
-      const subjectRight = raw.subjectRight as number
-      const refTop = raw.refTop as number
-      const refBottom = raw.refBottom as number
-      const refLeft = raw.refLeft as number
-      const refRight = raw.refRight as number
-
-      return {
-        ...raw,
-        overflowTop: Math.max(0, refTop - subjectTop),
-        overflowBottom: Math.max(0, subjectBottom - refBottom),
-        overflowLeft: Math.max(0, refLeft - subjectLeft),
-        overflowRight: Math.max(0, subjectRight - refRight),
-      }
-    })()
-
-    return {
-      clauseId: clauseId ?? (fr.formulaId ?? `clause_${idx}`),
-      status,
-      truth: fr.truth,
-      metrics: normalizedMetrics as any,
-      witness: fr.witness
-        ? { subjectId: fr.witness[0] ?? 0, frameId: 0 }
-        : { subjectId: 0, frameId: 0 },
-      diagnostics: [fr.outcome === 'fail' ? 'IMH_PREDICATE_FAILED' : ''].filter(Boolean),
-      sourceRef: traceMeta?.sourceRef,
-      clauseLabel: traceMeta?.clauseLabel,
-    }
-  })
-
-  const passed = folResult.passed && clauseResults.every((r) => r.status === 'pass')
-
-  return {
-    schemaVersion: '1.0',
-    passed,
-    summary: `${assertionCount} assertion(s), ${diagnostics.length} diagnostic(s)`,
-    clauseResults,
-    diagnostics,
-  }
-}
-
 // ---------------------------------------------------------------------------
 // Main Public API
 // ---------------------------------------------------------------------------