feat(util): RFD R2+R4+R5 — surface precision marker + soundness check + live unsound detection

packages/mcp/src/handlers/context-handlers.ts

@@ -155,7 +155,12 @@ function formatCallsForDisplay(calls: CallInfo[]): string[] {
       ? ` -> ${c.target?.name} (${c.target?.file}:${c.target?.line})`
       : ' (unresolved)';
     const prefix = c.type === 'METHOD_CALL' ? `${c.object}.` : '';
-    lines.push(`  - ${prefix}${c.name}()${target}`);
+    // R2: annotate non-precise resolutions so the reader sees the sound-superset
+    // fan-out (the precise default stays silent to avoid noise).
+    const prec = c.precision && c.precision.precision !== 'precise'
+      ? ` [${c.precision.precision}: ${c.precision.candidateCount} candidates]`
+      : '';
+    lines.push(`  - ${prefix}${c.name}()${target}${prec}`);
   }
 
   // Transitive calls (grouped by depth)

packages/mcp/src/handlers/dataflow-handlers.ts

@@ -477,7 +477,31 @@ export async function handleTraceEffects(args: TraceEffectsArgs): Promise<ToolRe
     for (const leaf of result.leaf_sources) {
       const leafFile = leaf.file ? leaf.file.split('/').pop() : '';
       const loc = leafFile ? ` (${leafFile})` : '';
-      lines.push(`  depth ${leaf.depth}: ${leaf.node}${loc} → ${leaf.effects.join(', ')}`);
+      // R2: surface the resolution-precision class so a reader sees
+      // sound-superset / suspected-unsound resolutions, not just the effects.
+      let prec = '';
+      if (leaf.precision && leaf.precision.precision !== 'precise') {
+        const c = leaf.precision.candidateCount;
+        prec = leaf.precision.precision === 'suspected-unsound'
+          ? `  [⚠ suspected-unsound: ${leaf.precision.basis}]`
+          : `  [heuristic-superset: ${c} candidates]`;
+      }
+      lines.push(`  depth ${leaf.depth}: ${leaf.node}${loc} → ${leaf.effects.join(', ')}${prec}`);
+    }
+    lines.push('');
+  }
+
+  // R5: explicit suspected-unsound resolution block — the importedDefault
+  // .method() → ecma-GLOBAL defect (e.g. axios.get → GLOBAL::get). The effects
+  // are recovered elsewhere; this is the PRECISION mark on top so the reader
+  // knows the single resolved callee is WRONG.
+  if (result.suspected_unsound.length > 0) {
+    lines.push(`### ⚠ Suspected-unsound resolutions (${result.suspected_unsound.length})`);
+    for (const u of result.suspected_unsound) {
+      lines.push(
+        `  ${u.call_name} → ${u.resolved_to_name} (wrong: receiver '${u.receiver_module}' collapsed; ` +
+        `presents ${u.presented_effects.join(', ') || 'PURE'})`,
+      );
     }
     lines.push('');
   }

packages/util/src/index.ts

@@ -223,6 +223,26 @@ export { findCallsInFunction, findContainingFunction, traceValues, aggregateValu
 export { traceDataflow, traceForwardBFS, traceBackwardBFS, makeDataflowIndexCache } from './queries/index.js';
 export { traceCallChain } from './queries/index.js';
 export { traceEffects } from './queries/index.js';
+// Resolution-precision marker (RFD R1) + consumers (R4 soundness check).
+export {
+  classifyResolution,
+  auditResolutionPrecision,
+  receiverExternalImport,
+  soundnessOf,
+  checkResolutionSoundness,
+} from './queries/index.js';
+export type {
+  ResolutionPrecision,
+  ResolutionMarker,
+  ResolutionBasis,
+  ClassifyContext,
+  MarkedResolution,
+  UnsoundCase,
+  ResolutionPrecisionAudit,
+  SoundnessVerdict,
+  ResolutionSoundnessViolation,
+  ResolutionSoundnessReport,
+} from './queries/index.js';
 export { getShape } from './queries/index.js';
 export type { ShapeResult, ShapeMember, ClassIndex } from './queries/index.js';
 export { buildNodeContext, getNodeDisplayName, formatEdgeMetadata, STRUCTURAL_EDGE_TYPES } from './queries/index.js';
@@ -252,6 +272,7 @@ export type {
   BoundaryCrossing,
   LeafSource,
   TraceEffectsOptions,
+  UnsoundResolutionLeaf,
 } from './queries/index.js';
 
 // Notation — DSL rendering engine

packages/util/src/queries/findCallsInFunction.ts

@@ -33,6 +33,8 @@
  */
 
 import type { CallInfo, FindCallsOptions } from './types.js';
+import { classifyResolution } from './resolutionPrecision.js';
+import type { DataflowNode, DataflowEdge } from './traceDataflow.js';
 
 /**
  * Graph backend interface (minimal surface)
@@ -50,7 +52,7 @@ interface GraphBackend {
   getOutgoingEdges(
     nodeId: string,
     edgeTypes: string[] | null
-  ): Promise<Array<{ src: string; dst: string; type: string }>>;
+  ): Promise<Array<{ src: string; dst: string; type: string; metadata?: Record<string, unknown> }>>;
 }
 
 /** Normalize node type field (RFDB uses nodeType, some backends use type) */
@@ -187,15 +189,29 @@ async function buildCallInfo(
   const isRemote = callsEdges.length > 0 && callsEdges[0].type === 'CALLS_REMOTE';
 
   let target = undefined;
+  let precision: CallInfo['precision'] = undefined;
   if (isResolved) {
-    const targetNode = await backend.getNode(callsEdges[0].dst);
+    const resolvedEdge = callsEdges[0];
+    const targetNode = await backend.getNode(resolvedEdge.dst);
     if (targetNode) {
       target = {
         id: targetNode.id,
         name: targetNode.name ?? '<anonymous>',
         file: targetNode.file,
         line: targetNode.line,
       };
+
+      // R2: precision marker. find_calls has no queryNodes surface, so the
+      // receiver-import walk is skipped (receiverIsExternalImport=false) — this
+      // path reports precise / heuristic-superset from fan-out + resolvedVia,
+      // never suspected-unsound (reserved for the full-walk audit/traceEffects).
+      precision = classifyResolution({
+        call: { id: callNode.id, type: getNodeType(callNode), name: callNode.name } as DataflowNode,
+        edge: { src: callNode.id, dst: resolvedEdge.dst, type: resolvedEdge.type, metadata: resolvedEdge.metadata } as DataflowEdge,
+        target: { id: targetNode.id, type: getNodeType(targetNode), name: targetNode.name } as DataflowNode,
+        candidateCount: callsEdges.length,
+        receiverIsExternalImport: false,
+      });
     }
   }
 
@@ -210,6 +226,7 @@ async function buildCallInfo(
     line: callNode.line,
     depth,
     remote: isRemote,
+    precision,
   };
 }
 

packages/util/src/queries/index.ts

@@ -47,8 +47,14 @@ export type {
   DataflowIndexCache,
 } from './traceDataflow.js';
 export { traceEffects } from './traceEffects.js';
-export type { TraceEffectsResult, BoundaryCrossing, LeafSource, TraceEffectsOptions } from './traceEffects.js';
-export { classifyResolution, auditResolutionPrecision } from './resolutionPrecision.js';
+export type { TraceEffectsResult, BoundaryCrossing, LeafSource, TraceEffectsOptions, UnsoundResolutionLeaf } from './traceEffects.js';
+export {
+  classifyResolution,
+  auditResolutionPrecision,
+  receiverExternalImport,
+  soundnessOf,
+  checkResolutionSoundness,
+} from './resolutionPrecision.js';
 export type {
   ResolutionPrecision,
   ResolutionMarker,
@@ -57,4 +63,7 @@ export type {
   MarkedResolution,
   UnsoundCase,
   ResolutionPrecisionAudit,
+  SoundnessVerdict,
+  ResolutionSoundnessViolation,
+  ResolutionSoundnessReport,
 } from './resolutionPrecision.js';

packages/util/src/queries/resolutionPrecision.ts

@@ -200,7 +200,7 @@ function isReceiverCollapsed(call: DataflowNode, target: DataflowNode): boolean
 // null. Kept here so the marker is self-contained for the spike; the production
 // merge would share the one copy in traceEffects.
 
-async function receiverExternalImport(
+export async function receiverExternalImport(
   backend: DataflowBackend,
   callId: string,
 ): Promise<string | null> {
@@ -343,3 +343,106 @@ function readEffects(node: DataflowNode | null): string[] {
   }
   return [];
 }
+
+// ── R4: soundness taxonomy + util-layer invariant check ───────
+//
+// The three precision classes carry a SOUNDNESS verdict the ≤1-target
+// "is-a-function" guarantee cannot express:
+//
+//   precise            → SOUND   (the resolution names the one real callee).
+//   heuristic-superset → SOUND   (acceptable-but-noisy: the real target IS in
+//                                 the candidate set; the resolver over-
+//                                 approximated but dropped nothing).
+//   suspected-unsound  → UNSOUND (a DEFECT: the real target was dropped and a
+//                                 single WRONG callee presented in its place —
+//                                 axios.get → ecma GLOBAL::get. This passes the
+//                                 ≤1-target guarantee while lying about the
+//                                 callee, so it needs an explicit hard flag).
+//
+// `checkResolutionSoundness` is the explicit hard-flag: given a backend it
+// returns every unsound resolution as a VIOLATION. It is a plain function
+// (NOT a guarantees.yaml rule — that surface is vm-owned), so the unsound
+// class is caught at the util layer even though it survives the structural
+// guarantee.
+
+/** Soundness verdict for a precision class (R4 taxonomy). */
+export type SoundnessVerdict = 'sound' | 'sound-superset' | 'unsound';
+
+/** Map a precision class to its soundness verdict. */
+export function soundnessOf(precision: ResolutionPrecision): SoundnessVerdict {
+  switch (precision) {
+    case 'precise':
+      return 'sound';
+    case 'heuristic-superset':
+      return 'sound-superset';
+    case 'suspected-unsound':
+      return 'unsound';
+  }
+}
+
+/** A single unsound resolution surfaced as a hard violation. */
+export interface ResolutionSoundnessViolation {
+  callId: string;
+  callName: string;
+  /** The (wrong) single resolved target. */
+  resolvedTo: string;
+  resolvedToName: string;
+  /** The collapsed-away receiver's module specifier (e.g. "axios"). */
+  receiverModule: string;
+  /** Effects the wrong target masks (e.g. ["PURE"]). */
+  presentedEffects: string[];
+  basis: ResolutionBasis;
+  /** Always 'unsound' here — kept explicit so callers can branch on verdict. */
+  verdict: SoundnessVerdict;
+}
+
+export interface ResolutionSoundnessReport {
+  /** True iff at least one unsound resolution was found. */
+  hasUnsound: boolean;
+  /** Every unsound resolution as a hard violation. */
+  violations: ResolutionSoundnessViolation[];
+  /** Tally by soundness verdict across all resolution edges. */
+  bySoundness: Record<SoundnessVerdict, number>;
+}
+
+/**
+ * R4 invariant check: flag every UNSOUND resolution (suspected-unsound class)
+ * as a hard violation. Sound and sound-superset resolutions are tallied but
+ * never reported as violations.
+ *
+ * This is the util-layer counterpart to the ≤1-target "is-a-function"
+ * guarantee: that guarantee passes on the axios.get→GLOBAL::get defect (it IS
+ * one function); THIS check fails it.
+ */
+export async function checkResolutionSoundness(
+  backend: DataflowBackend,
+): Promise<ResolutionSoundnessReport> {
+  const audit = await auditResolutionPrecision(backend);
+
+  const bySoundness: Record<SoundnessVerdict, number> = {
+    sound: 0,
+    'sound-superset': 0,
+    unsound: 0,
+  };
+  for (const r of audit.resolutions) {
+    bySoundness[soundnessOf(r.marker.precision)] += 1;
+  }
+
+  const violations: ResolutionSoundnessViolation[] = [];
+  for (const r of audit.resolutions) {
+    if (r.marker.precision !== 'suspected-unsound') continue;
+    const u = audit.suspectedUnsound.find(c => c.callId === r.callId && c.resolvedTo === r.targetId);
+    violations.push({
+      callId: r.callId,
+      callName: r.callName,
+      resolvedTo: r.targetId,
+      resolvedToName: r.targetName,
+      receiverModule: u?.receiverModule ?? '',
+      presentedEffects: u?.presentedEffects ?? [],
+      basis: r.marker.basis,
+      verdict: 'unsound',
+    });
+  }
+
+  return { hasUnsound: violations.length > 0, violations, bySoundness };
+}