Merge remote-tracking branch 'upstream/main' into fix/release-exposure-audit

scripts/ci/plan.mjs

@@ -229,6 +229,7 @@ if (tier === "reused") {
           file,
         ) ||
         file.startsWith("docs/") ||
+        file === "scripts/verify-documentation-routes.mjs" ||
         file.startsWith(".github/ISSUE_TEMPLATE/")
       ) {
         selected.docs = true;

scripts/ci/scopes.mjs

@@ -102,6 +102,7 @@ const PATH_SCOPES = {
     "tests/boundary/providers/RizinTimeoutEvidence.test.ts",
     "tests/boundary/providers/RizinDebugSession*.test.ts",
     "tests/boundary/providers/RizinInferiorTty.test.ts",
+    "tests/boundary/providers/RizinDecoderInputs.test.ts",
     "tests/boundary/providers/RizinTestInferiorTty.ts",
     "tests/boundary/process/ownedDebuggerSession.test.ts",
     "tests/boundary/cli/debuggerOneShotExit.test.ts",

scripts/lib/artifact-e2e.mjs

@@ -1,15 +1,26 @@
 import assert from "node:assert/strict";
-import { execFile } from "node:child_process";
-import { promisify } from "node:util";
 import { fileURLToPath } from "node:url";
 import { Client } from "@modelcontextprotocol/client";
-import { StdioClientTransport } from "@modelcontextprotocol/client/stdio";
+import { createVerifierCommands } from "./verify-commands.mjs";
+import { createOwnedMcpStdioTransport } from "./owned-mcp-stdio.mjs";
 import { withVerifierCleanup } from "./verifier-cleanup.mjs";
 import { INLINE_EVIDENCE_MCP_ENVIRONMENT } from "./mcp-verification-environment.mjs";
 
-// REA registers process-static tool contracts. Bind their parsed definitions to
-// the SDK's negotiated connection identity, including when a Client reconnects.
+// Bind parsed definitions to this connection. Hot/cold catalogs may add tools;
+// refresh a missing name once without throwing away already validated bindings.
 const toolBindings = new WeakMap();
+const readDefinitions = (client) =>
+  client.listTools().then(({ tools }) => {
+    const definitions = new Map();
+    for (const tool of tools) {
+      assert.ok(
+        !definitions.has(tool.name),
+        `Duplicate MCP tool: ${tool.name}`,
+      );
+      definitions.set(tool.name, tool);
+    }
+    return definitions;
+  });
 
 const advertisedTool = async (client, name) => {
   const connection = client.getServerVersion();
@@ -18,23 +29,19 @@ const advertisedTool = async (client, name) => {
   if (binding?.connection !== connection) {
     binding = {
       connection,
-      definitions: client.listTools().then(({ tools }) => {
-        const definitions = new Map();
-        for (const tool of tools) {
-          assert.ok(
-            !definitions.has(tool.name),
-            `Duplicate MCP tool: ${tool.name}`,
-          );
-          definitions.set(tool.name, tool);
-        }
-        return definitions;
-      }),
+      definitions: readDefinitions(client),
     };
     toolBindings.set(client, binding);
   }
   let definitions;
+  const snapshot = binding.definitions;
   try {
-    definitions = await binding.definitions;
+    definitions = await snapshot;
+    if (!definitions.has(name)) {
+      if (binding.definitions === snapshot)
+        binding.definitions = readDefinitions(client);
+      definitions = await binding.definitions;
+    }
     assert.equal(
       client.getServerVersion(),
       connection,
@@ -67,6 +74,23 @@ export async function artifactMcpCall(client, parameters, options = {}) {
   return client.callTool(parameters, { ...options, toolDefinition });
 }
 
+/** Retain the exact command owner when a verifier cannot finish cleanup. */
+class ArtifactVerifierCleanupError extends Error {
+  constructor(cause, cleanupOwner) {
+    super("Artifact verifier cleanup is incomplete", { cause });
+    this.name = "ArtifactVerifierCleanupError";
+    this.cleanupOwner = cleanupOwner;
+  }
+}
+
+const closeOwnedCommands = async (owner) => {
+  try {
+    await owner.close();
+  } catch (cause) {
+    throw new ArtifactVerifierCleanupError(cause, owner);
+  }
+};
+
 const environment = () => {
   const compileCache =
     process.env.NODE_COMPILE_CACHE ??
@@ -101,68 +125,130 @@ export async function artifactCliEvidence(
   command,
   target,
   arguments_ = [],
-  { timeoutMs = 60000 } = {},
+  { timeoutMs = 60000, signal, commands } = {},
 ) {
-  const { stdout } = await promisify(execFile)(
-    process.execPath,
-    [
-      fileURLToPath(new URL("../rea.mjs", import.meta.url)),
-      command,
-      target,
-      ...arguments_,
-      "--json",
-    ],
-    { env: environment(), timeout: timeoutMs, maxBuffer: 16 * 1024 * 1024 },
-  );
+  signal?.throwIfAborted();
+  const owner = commands ?? (await createVerifierCommands());
+  const execute = () =>
+    owner.exec(
+      process.execPath,
+      [
+        fileURLToPath(new URL("../rea.mjs", import.meta.url)),
+        command,
+        target,
+        ...arguments_,
+        "--json",
+      ],
+      {
+        env: environment(),
+        timeout: timeoutMs,
+        maxBuffer: 16 * 1024 * 1024,
+        signal,
+      },
+    );
+  const { stdout } =
+    commands === undefined
+      ? await withVerifierCleanup(execute, [() => closeOwnedCommands(owner)])
+      : await execute();
+  signal?.throwIfAborted();
   const evidence = JSON.parse(stdout);
   assert.equal(evidence.error, undefined, stdout);
   assert.ok(evidence.normalized_result, "CLI omitted normalized result");
   return evidence;
 }
 
-const withOpenedArtifactMcp = async (target, openTool, verify) => {
-  const transport = new StdioClientTransport({
+const withOpenedArtifactMcp = async (
+  target,
+  openTool,
+  verify,
+  options = {},
+) => {
+  options.signal?.throwIfAborted();
+  const owner = options.commands ?? (await createVerifierCommands());
+  const transport = await createOwnedMcpStdioTransport({
     command: process.execPath,
-    args: [fileURLToPath(new URL("../rea.mjs", import.meta.url)), "mcp"],
-    env: { ...environment(), ...INLINE_EVIDENCE_MCP_ENVIRONMENT },
-    stderr: "pipe",
+    arguments: [fileURLToPath(new URL("../rea.mjs", import.meta.url)), "mcp"],
+    hostEnvironment: { ...environment(), ...INLINE_EVIDENCE_MCP_ENVIRONMENT },
+    cwd: process.cwd(),
+    expectedCommand: null,
+    sweepTokenOwnedProcesses: true,
+    signal: options.signal,
   });
+  owner.adopt(transport, "artifact MCP process");
   const client = new Client({ name: "artifact-real-e2e", version: "1" });
-  return withVerifierCleanup(async () => {
-    await client.connect(transport);
-    const opened = await artifactMcpCall(client, {
-      name: openTool,
-      arguments: { path: target },
-    });
-    assert.notEqual(opened.isError, true, JSON.stringify(opened));
-    if (openTool === "open_bundle_resources")
-      assert.equal(opened.structuredContent?.result?.caller_path, target);
-    await verify(client);
-  }, [
-    () => {
-      toolBindings.delete(client);
-    },
-    () => client.close(),
-    () => transport.close(),
-  ]);
+  let clientClose;
+  const closeClient = () =>
+    (clientClose ??= Promise.resolve().then(() => client.close()));
+  const abortTransport = () => {
+    // Keep the same promise for finalization; concurrent SDK closes can return
+    // before the first close has observed the child exit.
+    void closeClient().catch(() => undefined);
+  };
+  options.signal?.addEventListener("abort", abortTransport, { once: true });
+  try {
+    const result = await withVerifierCleanup(async () => {
+      options.signal?.throwIfAborted();
+      await client.connect(transport);
+      options.signal?.throwIfAborted();
+      const opened = await artifactMcpCall(
+        client,
+        {
+          name: openTool,
+          arguments: { path: target },
+        },
+        { signal: options.signal },
+      );
+      assert.notEqual(opened.isError, true, JSON.stringify(opened));
+      if (openTool === "open_bundle_resources")
+        assert.equal(opened.structuredContent?.result?.caller_path, target);
+      await verify(client);
+    }, [
+      () => {
+        toolBindings.delete(client);
+      },
+      () => closeClient(),
+      () => transport.close(),
+      ...(options.commands === undefined
+        ? [() => closeOwnedCommands(owner)]
+        : []),
+    ]);
+    options.signal?.throwIfAborted();
+    return result;
+  } finally {
+    options.signal?.removeEventListener("abort", abortTransport);
+  }
 };
 
 /** Run a real stdio MCP subprocess with an explicitly opened binary target. */
-export async function withArtifactMcp(target, verify) {
-  return withOpenedArtifactMcp(target, "open_binary", verify);
+export async function withArtifactMcp(target, verify, options = {}) {
+  return withOpenedArtifactMcp(target, "open_binary", verify, options);
 }
 
 /** Run a real stdio MCP subprocess with an explicitly opened bundle resource root. */
-export async function withBundleResourcesMcp(target, verify) {
-  return withOpenedArtifactMcp(target, "open_bundle_resources", verify);
+export async function withBundleResourcesMcp(target, verify, options = {}) {
+  return withOpenedArtifactMcp(
+    target,
+    "open_bundle_resources",
+    verify,
+    options,
+  );
 }
 
 /** Require a successful structured MCP tool result rather than its text rendering. */
-export async function artifactMcpResult(client, name, arguments_ = {}) {
-  const result = await artifactMcpCall(client, {
-    name,
-    arguments: arguments_,
-  });
+export async function artifactMcpResult(
+  client,
+  name,
+  arguments_ = {},
+  options = {},
+) {
+  const result = await artifactMcpCall(
+    client,
+    {
+      name,
+      arguments: arguments_,
+    },
+    options,
+  );
   assert.notEqual(result.isError, true, JSON.stringify(result));
   assert.ok(
     result.structuredContent?.normalized_result,

scripts/lib/canonical-temporary-directory.d.mts

@@ -0,0 +1,5 @@
+/** Allocate under a caller-selected parent and return the host's canonical spelling. */
+export declare const createCanonicalTemporaryDirectory: (
+  prefix: string,
+  parent?: string,
+) => Promise<{ readonly path: string; readonly allocatedPath: string }>;

scripts/lib/canonical-temporary-directory.mjs

@@ -0,0 +1,17 @@
+import { mkdtemp, realpath, rm } from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+
+/** Allocate under a caller-selected parent and return the host's canonical spelling. */
+export const createCanonicalTemporaryDirectory = async (
+  prefix,
+  parent = tmpdir(),
+) => {
+  const allocatedPath = await mkdtemp(join(parent, prefix));
+  try {
+    return { path: await realpath(allocatedPath), allocatedPath };
+  } catch (cause) {
+    await rm(allocatedPath, { recursive: true, force: true });
+    throw cause;
+  }
+};

scripts/lib/docs-facts.mjs

@@ -121,14 +121,19 @@ export const documentationFactIssues = async (root, catalog) => {
         issues,
         path,
         content,
-        "(docs/installation.md#supported-agents)",
+        "(docs/getting-started/installation.md#supported-agents)",
       );
-      requireText(issues, path, content, "(docs/installation.md#mcp-registry)");
       requireText(
         issues,
         path,
         content,
-        "(docs/mcp-contracts.md#generated-catalog)",
+        "(docs/getting-started/installation.md#mcp-registry)",
+      );
+      requireText(
+        issues,
+        path,
+        content,
+        "(docs/reference/mcp-contracts.md#generated-catalog)",
       );
     }
   }
@@ -156,7 +161,7 @@ export const documentationFactIssues = async (root, catalog) => {
     )
       issues.push(`${path}: documentation links differ from README.md`);
 
-  const installationPath = "docs/installation.md";
+  const installationPath = "docs/getting-started/installation.md";
   const installation = await readFile(join(root, installationPath), "utf8");
   for (const client of catalog.setup_clients)
     requireText(issues, installationPath, installation, client.display_name);

scripts/lib/native-value-e2e.mjs

@@ -18,6 +18,7 @@ import {
 } from "./mcp-verifier-results.mjs";
 import { verifyGhidraBoundaries } from "./real-ghidra-boundaries.mjs";
 import { verifyGhidraProjectIdentity } from "./real-ghidra-project-identity.mjs";
+import { verifyGhidraSocketBoundary } from "./real-ghidra-socket-boundary.mjs";
 
 const defaultEntrypoint = fileURLToPath(new URL("../rea.mjs", import.meta.url));
 const environment = () => ({
@@ -355,6 +356,12 @@ async function verifyNativeValueAdapters(
     entrypoint,
     env,
   });
+  const socketBoundary = await verifyGhidraSocketBoundary({
+    target,
+    procedure,
+    entrypoint,
+    env,
+  });
   return {
     mocked: false,
     cli: true,
@@ -363,6 +370,7 @@ async function verifyNativeValueAdapters(
     direct_function_comparison: true,
     boundaries,
     project_identity: projectIdentity,
+    socket_boundary: socketBoundary,
     nodes: cliGraph.total_nodes,
     edges: cliGraph.total_edges,
     decompilations: cliGraph.decompilations,

scripts/lib/owned-mcp-stdio.mjs

@@ -0,0 +1,24 @@
+import { importVerifierSource } from "./verifier-source-loader.mjs";
+
+let implementation;
+
+/** Create an SDK-compatible transport which retains the exact process owner. */
+export async function createOwnedMcpStdioTransport(options) {
+  implementation ??= importVerifierSource(
+    new URL("../../src/process/OwnedMcpStdioTransport.ts", import.meta.url)
+      .href,
+    import.meta.url,
+  );
+  const { OwnedMcpStdioTransport } = await implementation;
+  return new OwnedMcpStdioTransport(options, {
+    provider: "artifact-verifier",
+    label: "Artifact verifier",
+    // Match the SDK's default maximum buffered stdio message size.
+    maxFrameBytes: 10 * 1024 * 1024,
+    // Unlike the JADX adapter, artifact verifiers do not impose a cumulative
+    // per-connection output limit; the SDK bounds each buffered message.
+    maxOperationBytes: Infinity,
+    gracefulInputCloseMs: 2000,
+    maxDiagnosticBytes: 64 * 1024,
+  });
+}

scripts/lib/real-ghidra-address-boundaries.d.mts

@@ -1,8 +1,12 @@
 import type { Client } from "@modelcontextprotocol/client";
 
-/** Verify segmented aliases and restore the entry's observed public name. */
+/**
+ * Verify segmented aliases and restore the entry's observed public name.
+ * With `mutable: false` (Windows P0), annotation and naming edits must be refused.
+ */
 export function verifyGhidraAddressBoundaries(
   client: Pick<Client, "callTool">,
   entry: string,
   cli: (command: string, address: string, flags: string[]) => Promise<unknown>,
+  options?: { readonly mutable?: boolean },
 ): Promise<void>;

scripts/lib/real-ghidra-address-boundaries.mjs

@@ -1,8 +1,16 @@
 import { requireMcpToolError } from "./mcp-verifier-results.mjs";
 import assert from "node:assert/strict";
 
-/** Exercise segmented-address truncation through real CLI/MCP reads and edits. */
-export async function verifyGhidraAddressBoundaries(client, entry, cli) {
+/**
+ * Exercise segmented-address truncation through real CLI/MCP reads and edits.
+ * A read-only provider (Windows P0) must refuse edits before parsing them.
+ */
+export async function verifyGhidraAddressBoundaries(
+  client,
+  entry,
+  cli,
+  { mutable = true } = {},
+) {
   const query = async (name, args) => {
     const reply = await client.callTool(
       { name, arguments: args },
@@ -45,6 +53,14 @@ export async function verifyGhidraAddressBoundaries(client, entry, cli) {
       );
       assert.equal(reply.isError, true, `${name} accepted ${address}`);
       const error = requireMcpToolError(reply);
+      if (!mutable && name === "annotate_native_function") {
+        assert.equal(
+          error?.code,
+          "capability_unavailable",
+          JSON.stringify(reply),
+        );
+        continue;
+      }
       assert.equal(error?.code, "invalid_request", JSON.stringify(reply));
       assert.equal(error.details.operation, name);
       const issues = JSON.stringify(error.details.issues);
@@ -65,6 +81,63 @@ export async function verifyGhidraAddressBoundaries(client, entry, cli) {
     await query("read_bytes", { address: padded, length: 1 }),
     await query("read_bytes", { address: entry, length: 1 }),
   );
+  if (mutable) await verifyAliasNaming(query, entry, padded);
+  else await verifyNamingRefused(client, query, entry, padded);
+  for (const [command, flags, operation] of [
+    ["read-bytes", ["--length", "1"], "read_bytes"],
+    [
+      "annotate-native-function",
+      ["--name", "MUST_NOT_ALIAS"],
+      "annotate_native_function",
+    ],
+  ]) {
+    let failure;
+    try {
+      await cli(command, representations[0], flags);
+    } catch (error) {
+      assert.equal(error.code, 1);
+      failure = JSON.parse(error.stdout);
+    }
+    if (!mutable && operation === "annotate_native_function") {
+      assert.equal(failure?.code, "capability_unavailable");
+      continue;
+    }
+    assert.equal(failure?.code, "invalid_request");
+    assert.equal(failure.details.operation, operation);
+    assert.match(
+      JSON.stringify(failure.details.issues),
+      /cannot be represented without truncation/u,
+    );
+  }
+}
+
+/** A read-only provider refuses both naming operations and keeps the entry name. */
+async function verifyNamingRefused(client, query, entry, padded) {
+  const originalName = await query("address_name", { address: entry });
+  for (const [name, args] of [
+    ["set_address_name", { address: entry, name: "MUST_NOT_RENAME" }],
+    [
+      "set_addresses_names",
+      { names: { [entry]: "MUST_NOT_RENAME", [padded]: "MUST_NOT_RENAME" } },
+    ],
+  ]) {
+    const reply = await client.callTool(
+      { name, arguments: args },
+      { timeout: 240000 },
+    );
+    assert.equal(reply.isError, true, `${name} was not refused`);
+    const error = requireMcpToolError(reply);
+    assert.equal(error?.code, "capability_unavailable", JSON.stringify(reply));
+  }
+  assert.equal(
+    await query("address_name", { address: entry }),
+    originalName,
+    "A refused naming edit changed the entry name",
+  );
+}
+
+/** Equivalent spellings of one address share or reject one naming edit together. */
+async function verifyAliasNaming(query, entry, padded) {
   const originalName = await query("address_name", { address: entry });
   assert.equal(
     typeof originalName,
@@ -127,26 +200,4 @@ export async function verifyGhidraAddressBoundaries(client, entry, cli) {
       throw cleanupCause;
     }
   }
-  for (const [command, flags, operation] of [
-    ["read-bytes", ["--length", "1"], "read_bytes"],
-    [
-      "annotate-native-function",
-      ["--name", "MUST_NOT_ALIAS"],
-      "annotate_native_function",
-    ],
-  ]) {
-    let failure;
-    try {
-      await cli(command, representations[0], flags);
-    } catch (error) {
-      assert.equal(error.code, 1);
-      failure = JSON.parse(error.stdout);
-    }
-    assert.equal(failure?.code, "invalid_request");
-    assert.equal(failure.details.operation, operation);
-    assert.match(
-      JSON.stringify(failure.details.issues),
-      /cannot be represented without truncation/u,
-    );
-  }
 }

scripts/lib/real-ghidra-boundaries.mjs

@@ -13,6 +13,7 @@ import { promisify } from "node:util";
 import { GHIDRA_ANNOTATIONS_RETAINED } from "../../dist/ghidra/GhidraProviderClient.js";
 import Ajv from "ajv/dist/2020.js";
 import addFormats from "ajv-formats";
+import { OFFICIAL_TOOL_CONTRACTS } from "../../dist/contracts/officialToolContracts.js";
 
 import { verifyLegacyGhidraReferenceSnapshot } from "./ghidra-reference-snapshot-e2e.mjs";
 import { verifyGhidraSnapshotLifecycle } from "./real-ghidra-snapshot-lifecycle.mjs";
@@ -22,6 +23,7 @@ import { verifyGhidraEntryAliases } from "./real-ghidra-entry-aliases.mjs";
 import { verifyGhidraNamespaceAnnotations } from "./real-ghidra-namespace-annotations.mjs";
 import { verifyGhidraBatchIdentity } from "./real-ghidra-batch-identity.mjs";
 import { verifyGhidraInstructionFlow } from "./real-ghidra-instruction-flow.mjs";
+import { verifyGhidraSearchFacts } from "./real-ghidra-search-facts.mjs";
 
 /** Probe real Ghidra location, annotation and error contracts through public adapters. */
 export async function verifyGhidraBoundaries(
@@ -30,6 +32,14 @@ export async function verifyGhidraBoundaries(
 ) {
   const options = { timeout: 180000 };
   const catalog = await client.listTools();
+  const annotation = catalog.tools.find(
+    (tool) => tool.name === "annotate_native_function",
+  );
+  const annotationContract = OFFICIAL_TOOL_CONTRACTS.find(
+    (tool) => tool.name === "annotate_native_function",
+  );
+  assert.ok(annotationContract, "Annotation contract is missing");
+  assert.equal(annotation?.description, annotationContract.description);
   const ajv = new Ajv({ strict: false });
   addFormats(ajv);
   const validators = new Map();
@@ -401,6 +411,11 @@ export async function verifyGhidraBoundaries(
     (item) => item.value === "REA_GHIDRA_INVENTORY_ENTRY",
   );
   assert.ok(marker);
+  await verifyGhidraSearchFacts(call, {
+    strings,
+    procedures,
+    entryAddress: address,
+  });
   assert.ok(
     (
       await call("search_strings", { pattern: marker.value.toLowerCase() })
@@ -589,9 +604,7 @@ export async function verifyGhidraBoundaries(
   const longString = strings.find((item) => item.value === longLiteral);
   assert.ok(longString, "The provider must retain the full regression literal");
   const literalMatches = await call("search_strings", { pattern: longLiteral });
-  assert.deepEqual(literalMatches, [
-    { address: longString.address, value: longLiteral },
-  ]);
+  assert.deepEqual(literalMatches, [longString]);
   assert.deepEqual(await cli("search", longLiteral), literalMatches);
   await assert.rejects(
     cli("search", regexPattern, ["--mode", "regex"]),

scripts/lib/real-ghidra-entry-aliases.mjs

@@ -156,6 +156,15 @@ export async function verifyGhidraEntryAliases({
       alias.address,
       "Explicit interior addresses keep their existing containment semantics",
     );
+    const interiorEdit = await call("annotate_native_function", {
+      procedure: interior.address,
+      comment: "Selected by interior address",
+    });
+    assert.equal(interiorEdit.annotations.address, alias.address);
+    assert.equal(
+      interiorEdit.annotations.comment,
+      "Selected by interior address",
+    );
     const edited = await call("annotate_native_function", {
       procedure: alias.value,
       comment: "Selected by imported entry alias",

scripts/lib/real-ghidra-search-facts.mjs

@@ -0,0 +1,58 @@
+import assert from "node:assert/strict";
+
+/** Compare public searches and composed traces with their provider inventory rows. */
+export async function verifyGhidraSearchFacts(
+  call,
+  { strings, procedures, entryAddress },
+) {
+  const marker = strings.find(
+    (row) => row.value === "REA_GHIDRA_INVENTORY_ENTRY",
+  );
+  const entry = procedures.find((row) => row.address === entryAddress);
+  const external = procedures.find((row) => row.procedure.external);
+  const thunk = procedures.find((row) => row.procedure.thunk);
+  assert.ok(marker, "Missing source string fixture");
+  assert.ok(entry, "Missing selected entry procedure");
+  assert.ok(external, "Missing external procedure fixture");
+  const cases = [
+    { type: "string", operation: "search_strings", row: marker },
+    ...[entry, external, ...(thunk === undefined ? [] : [thunk])].map(
+      (row) => ({
+        type: "procedure",
+        operation: "search_procedures",
+        row,
+      }),
+    ),
+  ];
+  for (const { type, operation, row } of cases) {
+    const search = await call(operation, {
+      pattern: row.value,
+      mode: "literal",
+      case_sensitive: true,
+    });
+    const match = search.find(
+      (item) => item.address === row.address && item.value === row.value,
+    );
+    assert.deepEqual(
+      match,
+      row,
+      `${operation} must preserve inventory facts for ${row.value}`,
+    );
+    const trace = await call("trace_feature", {
+      query: row.value,
+      case_sensitive: true,
+    });
+    const traced = trace.matches.find(
+      (item) =>
+        item.type === type &&
+        item.address === row.address &&
+        item.value === row.value,
+    );
+    assert.deepEqual(
+      traced,
+      { ...row, type },
+      `trace_feature must preserve ${operation} facts for ${row.value}`,
+    );
+  }
+  return { compared: cases.length, thunk_observed: thunk !== undefined };
+}

scripts/lib/real-ghidra-socket-boundary.mjs

@@ -0,0 +1,200 @@
+import assert from "node:assert/strict";
+import { execFile } from "node:child_process";
+import { createHash } from "node:crypto";
+import {
+  access,
+  mkdir,
+  mkdtemp,
+  readFile,
+  readdir,
+  realpath,
+  rm,
+  stat,
+} from "node:fs/promises";
+import { basename, dirname, join } from "node:path";
+import { promisify } from "node:util";
+import { Client } from "@modelcontextprotocol/client";
+import { StdioClientTransport } from "@modelcontextprotocol/client/stdio";
+import { withVerifierCleanup } from "./verifier-cleanup.mjs";
+
+const exec = promisify(execFile);
+
+/** Exercise the OpenJDK Unix-socket boundary through real Ghidra and REA. */
+export async function verifyGhidraSocketBoundary({
+  target,
+  procedure,
+  entrypoint,
+  env,
+}) {
+  if (process.platform !== "darwin" && process.platform !== "linux")
+    return {
+      status: "not-applicable",
+      reason: "The Ghidra Unix-socket lane is not used on this host.",
+    };
+  const limit = process.platform === "darwin" ? 102 : 106;
+  const before = createHash("sha256")
+    .update(await readFile(target.path))
+    .digest("hex");
+  const root = await realpath(await mkdtemp("/tmp/rea-gsock-"));
+  const suffixBytes = Buffer.byteLength("/rea-ghidra-XXXXXX/bridge.sock");
+  let cleanupIncomplete = false;
+  const samples = [];
+  try {
+    for (const { proposedBytes, unicode } of [
+      { proposedBytes: limit, unicode: false },
+      { proposedBytes: limit + 1, unicode: false },
+      { proposedBytes: limit + 2, unicode: false },
+      { proposedBytes: limit + 1, unicode: true },
+    ]) {
+      const character = unicode ? "雪" : "";
+      const padding =
+        proposedBytes -
+        suffixBytes -
+        Buffer.byteLength(root) -
+        1 -
+        Buffer.byteLength(character);
+      assert.ok(
+        padding > 0,
+        "Verifier workspace leaves no room for the boundary fixture",
+      );
+      const parent = join(root, "x".repeat(padding) + character);
+      await mkdir(parent);
+      assert.equal(Buffer.byteLength(parent) + suffixBytes, proposedBytes);
+      if (unicode) assert.ok(Buffer.byteLength(parent) > parent.length);
+      const sessionEnv = { ...env, TMPDIR: parent };
+      const client = new Client({
+        name: "rea-ghidra-socket-boundary",
+        version: "1",
+      });
+      const transport = new StdioClientTransport({
+        command: process.execPath,
+        args: [entrypoint, "mcp"],
+        env: sessionEnv,
+        stderr: "pipe",
+      });
+      let connected = false;
+      let opened = false;
+      let runtimeRoot;
+      let socketRoot;
+      let endpoint;
+      const cleanup = async (task) => {
+        try {
+          await task();
+        } catch (cause) {
+          cleanupIncomplete = true;
+          throw cause;
+        }
+      };
+      await withVerifierCleanup(async () => {
+        await client.connect(transport);
+        connected = true;
+        const tools = new Map(
+          (await client.listTools()).tools.map((tool) => [tool.name, tool]),
+        );
+        const call = async (name, arguments_ = {}) => {
+          const reply = await client.callTool(
+            { name, arguments: arguments_ },
+            { timeout: 180000, toolDefinition: tools.get(name) },
+          );
+          assert.notEqual(
+            reply.isError,
+            true,
+            `${name}: ${JSON.stringify(reply)}`,
+          );
+          return reply.structuredContent ?? JSON.parse(reply.content[0].text);
+        };
+        await call("open_binary", { path: target.path, provider_id: "ghidra" });
+        opened = true;
+        await call("list_documents");
+        const roots = (await readdir(parent)).filter((name) =>
+          name.startsWith("rea-ghidra-"),
+        );
+        assert.equal(roots.length, 1);
+        runtimeRoot = join(parent, roots[0]);
+        endpoint = JSON.parse(
+          await readFile(join(runtimeRoot, "ownership.json"), "utf8"),
+        ).endpoint_path;
+        assert.equal(
+          Buffer.byteLength(join(runtimeRoot, "bridge.sock")),
+          proposedBytes,
+        );
+        const fallback = dirname(endpoint) !== runtimeRoot;
+        assert.equal(fallback, proposedBytes > limit);
+        if (fallback) {
+          socketRoot = dirname(endpoint);
+          assert.match(basename(socketRoot), /^rea-ghidra-socket-/u);
+          assert.equal((await stat(socketRoot)).mode & 0o777, 0o700);
+        }
+        samples.push({
+          proposed_bytes: proposedBytes,
+          unicode,
+          endpoint_bytes: Buffer.byteLength(endpoint),
+          fallback,
+        });
+      }, [
+        () =>
+          cleanup(async () => {
+            if (!connected || !opened) return;
+            const reply = await client.callTool(
+              { name: "close_binary", arguments: {} },
+              { timeout: 180000 },
+            );
+            assert.notEqual(
+              reply.isError,
+              true,
+              `close_binary: ${JSON.stringify(reply)}`,
+            );
+          }),
+        () =>
+          cleanup(async () => {
+            await client.close();
+          }),
+        () =>
+          cleanup(async () => {
+            await transport.close();
+          }),
+      ]);
+      await assert.rejects(access(runtimeRoot), { code: "ENOENT" });
+      if (socketRoot !== undefined)
+        await assert.rejects(access(socketRoot), { code: "ENOENT" });
+      if (proposedBytes === limit + 1 && !unicode) {
+        const { stdout } = await exec(
+          process.execPath,
+          [
+            entrypoint,
+            "function",
+            target.path,
+            procedure,
+            "--provider",
+            "ghidra",
+            "--json",
+          ],
+          { env: sessionEnv, timeout: 240000, maxBuffer: 72 * 1024 * 1024 },
+        );
+        assert.ok(JSON.parse(stdout).normalized_result.procedure);
+        assert.deepEqual(
+          (await readdir(parent)).filter((name) =>
+            name.startsWith("rea-ghidra-"),
+          ),
+          [],
+          "CLI left a Ghidra runtime directory",
+        );
+      }
+    }
+    assert.equal(
+      createHash("sha256")
+        .update(await readFile(target.path))
+        .digest("hex"),
+      before,
+    );
+    return {
+      status: "verified",
+      samples,
+      cli_boundary: true,
+      target_unchanged: true,
+    };
+  } finally {
+    // A failed cleanup retains its exact workspace for investigation and retry.
+    if (!cleanupIncomplete) await rm(root, { recursive: true, force: true });
+  }
+}

scripts/lib/release-notes.mjs

@@ -476,7 +476,8 @@ export async function verifyInventoryHistory(run, raw, source) {
       "package-lock.json",
       "server.json",
       "src/generatedPackageMetadata.ts",
-      "docs/installation.md",
+      "docs/installation.md", // Historical releases before documentation organization.
+      "docs/getting-started/installation.md",
       `docs/releases/${inventory.version}.contributions.json`,
     ]);
     const paths = (

scripts/pack-build-computer-runtime.mjs

@@ -0,0 +1,54 @@
+#!/usr/bin/env node
+// Pack this checkout as the REA a build computer runs, the archive REA_BUILD_COMPUTER_REA_ARCHIVE names:
+// `npm pack`, its package folder as rea-prod with the lockfile, production dependencies installed with
+// `npm ci --omit=dev --omit=optional`, then rea-prod as a .tar.xz.
+// Usage: node scripts/pack-build-computer-runtime.mjs <archive.tar.xz>
+import { spawnSync } from "node:child_process";
+import { copyFile, mkdtemp, readdir, rename, rm, stat } from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { dirname, join, resolve } from "node:path";
+import { fileURLToPath } from "node:url";
+
+const root = join(dirname(fileURLToPath(import.meta.url)), "..");
+const npm = process.platform === "win32" ? "npm.cmd" : "npm";
+
+const run = (command, args, cwd) => {
+  const result = spawnSync(command, args, { cwd, stdio: "inherit" });
+  if (result.error !== undefined) throw result.error;
+  if (result.status !== 0)
+    throw new Error(
+      `${command} ${args.join(" ")} failed with status ${String(result.status)}`,
+    );
+};
+
+const [destination] = process.argv.slice(2);
+if (destination === undefined || !destination.endsWith(".tar.xz")) {
+  process.stderr.write(
+    "Usage: node scripts/pack-build-computer-runtime.mjs <archive.tar.xz>\n",
+  );
+  process.exit(2);
+}
+const archive = resolve(destination);
+const work = await mkdtemp(join(tmpdir(), "rea-build-runtime-"));
+try {
+  run(npm, ["pack", "--pack-destination", work], root);
+  const [packed] = (await readdir(work)).filter((name) =>
+    name.endsWith(".tgz"),
+  );
+  if (packed === undefined) throw new Error("npm pack wrote no .tgz");
+  run("tar", ["-xzf", packed], work);
+  const runtime = join(work, "rea-prod");
+  await rename(join(work, "package"), runtime);
+  await copyFile(
+    join(root, "package-lock.json"),
+    join(runtime, "package-lock.json"),
+  );
+  run(npm, ["ci", "--omit=dev", "--omit=optional"], runtime);
+  run("tar", ["-cJf", archive, "-C", work, "rea-prod"], work);
+  const { size } = await stat(archive);
+  process.stdout.write(
+    `${archive} (${(size / 1024 / 1024).toFixed(1)} MiB): set REA_BUILD_COMPUTER_REA_ARCHIVE to it.\n`,
+  );
+} finally {
+  await rm(work, { recursive: true, force: true });
+}

scripts/verify-agentenv-environment.mjs

@@ -27,7 +27,7 @@ const MIN_RETRY_MS = 5 * 60_000;
 for (const key of ["REA_AGENT_ENV_COMMAND", "REA_DOCKER_COMMAND"])
   if (!isAbsolute(process.env[key] ?? ""))
     throw new Error(
-      `verify:agentenv:environment requires absolute ${key}; see docs/testing.md. No dependencies are installed by this verifier.`,
+      `verify:agentenv:environment requires absolute ${key}; see docs/development/testing.md. No dependencies are installed by this verifier.`,
     );
 const agentEnv = process.env.REA_AGENT_ENV_COMMAND;
 const docker = process.env.REA_DOCKER_COMMAND;

scripts/verify-documentation-routes.mjs

@@ -0,0 +1,130 @@
+import assert from "node:assert/strict";
+import { readFile, readdir, stat } from "node:fs/promises";
+import { basename, resolve, sep } from "node:path";
+import { fileURLToPath } from "node:url";
+
+// Public route baseline before categorization, including upstream signal recordings.
+// This fixture is independent of the navigation/rewrite implementation.
+const routes = `
+adb-device-analysis android-analysis apktool-resource-analysis apple-application-analysis
+binary-diagnostics browser-observation browser-scenario-contract cli client-configuration
+client-verification electron-observation evm-bytecode firmware-analysis flutter-analysis
+frida-instrumentation ghidra-dos ghidra-mips ghidra-nativeaot ghidra-provider ghidra-psp
+ghidra-riscv go-binaries harmony-analysis http3-capture-lab ida-provider installation
+javascript-application-graph javascript-application-workflows javascript-artifact-reconstruction
+javascript-recovery javascript-runtime-observation javascript-runtime-reconciliation
+jeb-analysis managed-code-analysis mcp-contracts mcp-prompts migration-6.2
+native-investigation packet-captures pcap-analysis process-capture raw-binary reconstruction-obligation-ledgers
+reconstruction-readiness recorded-crashes releasing roadmap signal-recordings sqlite-databases
+testing tool-design wasm-artifacts web-network-captures web-runtime web-source-location
+website-module-trace website-script-export windows-ghidra-p0
+binary-hardening desktop-application-capture desktop-application-export desktop-application-state
+desktop-application-tasks desktop-build-computer desktop-build-witness ines-containers
+design/limits-and-recovery
+`
+  .trim()
+  .split(/\s+/u);
+assert.equal(routes.length, 67);
+assert.equal(new Set(routes).size, routes.length);
+
+const documentation = resolve(
+  fileURLToPath(new URL("../docs/", import.meta.url)),
+);
+const output = resolve(documentation, ".vitepress/dist");
+const origin = "https://documentation.invalid";
+const checked = new Set();
+let internalTargets = 0;
+let sourceLinks = 0;
+// Legacy public routes remain an independent baseline; all generated pages also
+// participate so newly authored directories/specifications cannot escape checks.
+for (const route of routes) {
+  const html = await readFile(resolve(output, route + ".html"), "utf8");
+  const edit = physicalEditSource(html, route);
+  assert.equal(basename(edit), basename(route) + ".md");
+}
+const htmlPages = [];
+const directories = [output];
+while (directories.length > 0) {
+  const directory = directories.pop();
+  for (const entry of await readdir(directory, { withFileTypes: true })) {
+    const path = resolve(directory, entry.name);
+    if (entry.isDirectory()) directories.push(path);
+    else if (entry.isFile() && entry.name.endsWith(".html"))
+      htmlPages.push(path);
+  }
+}
+for (const page of htmlPages.sort()) {
+  const route = page
+    .slice(output.length + 1)
+    .split(sep)
+    .join("/");
+  const html = await readFile(page, "utf8");
+  // The configured home layout and generated 404 render no edit action.
+  // Their outgoing links still participate in the same all-page scan.
+  if (route !== "404.html" && route !== "index.html") {
+    const source = physicalEditSource(html, route);
+    assert.ok(
+      (await stat(source)).isFile(),
+      route + ": edit link source is missing",
+    );
+    sourceLinks++;
+  }
+  for (const match of html.matchAll(
+    /<(?:a|img)\b[^>]*\b(?:href|src)="([^"]+)"/gu,
+  )) {
+    const destination = match[1].replaceAll("&amp;", "&");
+    const url = new URL(destination, origin + "/rea/" + route);
+    if (url.origin !== origin) continue;
+    assert.ok(
+      url.pathname.startsWith("/rea/"),
+      route + ": local link escaped site base " + destination,
+    );
+    const key = url.pathname + url.hash;
+    if (checked.has(key)) continue;
+    checked.add(key);
+    let target = decodeURIComponent(url.pathname.slice("/rea/".length));
+    if (!target || target.endsWith("/")) target += "index.html";
+    else if (!basename(target).includes(".")) target += ".html";
+    const physical = resolve(output, target);
+    assert.ok(
+      physical.startsWith(output + sep),
+      destination + ": published path escaped site output",
+    );
+    assert.ok(
+      (await stat(physical)).isFile(),
+      route + ": broken rendered target " + destination,
+    );
+    if (url.hash && target.endsWith(".html")) {
+      const fragment = decodeURIComponent(url.hash.slice(1));
+      const page = await readFile(physical, "utf8");
+      assert.ok(
+        page.includes('id="' + fragment + '"'),
+        route + ": missing rendered anchor " + destination,
+      );
+    }
+    internalTargets++;
+  }
+}
+function physicalEditSource(html, route) {
+  const edit = html.match(
+    /href="https:\/\/github\.com\/morluto\/rea\/edit\/main\/docs\/([^"]+)"/u,
+  );
+  assert.ok(edit, route + ": missing physical-source edit link");
+  const source = resolve(documentation, decodeURIComponent(edit[1]));
+  assert.ok(
+    source.startsWith(documentation + sep),
+    route + ": source escaped documentation root",
+  );
+  return source;
+}
+console.log(
+  JSON.stringify({
+    ok: true,
+    published_routes: routes.length,
+    html_pages: htmlPages.length,
+    physical_edit_links: sourceLinks,
+    distinct_internal_targets_and_anchors: internalTargets,
+    scope:
+      "actual generated HTML, local guide routes/edit sources/images and anchors; external network links are not fetched",
+  }),
+);

scripts/verify-native-calls.mjs

@@ -61,6 +61,10 @@ const stable = (result) =>
     file_address: event.file_address,
     selector: event.selector,
     receiver_class: event.receiver_class,
+    source_location: event.source_location,
+    caller_source_locations: event.backtrace.map(
+      (frame) => frame.source_location,
+    ),
     counter:
       event.symbol === GREET
         ? event.registers[3].value
@@ -96,6 +100,18 @@ const checkScenario = async (binary) => {
   });
   const greet = result.events.filter(({ symbol }) => symbol === GREET);
   const add = result.events.filter(({ symbol }) => symbol === "rea_call_add");
+  for (const location of [
+    ...result.events,
+    ...result.events.flatMap((event) => event.backtrace),
+    ...result.breakpoints.flatMap((breakpoint) => breakpoint.locations),
+  ]) {
+    assert.equal(location.source_location?.file_path, SOURCE);
+    assert.ok(location.source_location.line > 0);
+    assert.ok(
+      location.source_location.column === null ||
+        location.source_location.column > 0,
+    );
+  }
   assert.equal(greet.length, 3, JSON.stringify(result));
   assert.equal(add.length, 3, JSON.stringify(result));
   for (const [index, event] of greet.entries()) {
@@ -269,6 +285,8 @@ try {
   const binary = join(directory, "ReaCalls");
   await exec("/usr/bin/xcrun", [
     "clang",
+    "-g",
+    "-O0",
     "-fobjc-arc",
     "-framework",
     "Foundation",

scripts/verify-native-pascal-calls.mjs

@@ -0,0 +1,186 @@
+import assert from "node:assert/strict";
+import { readFile, rm } from "node:fs/promises";
+import { isAbsolute, join } from "node:path";
+import { fileURLToPath } from "node:url";
+import { createPackageVerifierCommands } from "./lib/verify-package-commands.mjs";
+import { withVerifierCleanup } from "./lib/verifier-cleanup.mjs";
+
+import {
+  artifactCli,
+  artifactMcpResult,
+  withArtifactMcp,
+} from "./lib/artifact-e2e.mjs";
+import { createCanonicalTemporaryDirectory } from "./lib/canonical-temporary-directory.mjs";
+
+const cancellation = new AbortController();
+let shutdownSignal;
+const signalExitCodes = { SIGINT: 130, SIGTERM: 143 };
+const forwardCancellation = (signal) => {
+  if (shutdownSignal !== undefined) return;
+  shutdownSignal = signal;
+  cancellation.abort(new Error(`Verification cancelled by ${signal}`));
+};
+const signalHandlers = Object.fromEntries(
+  Object.keys(signalExitCodes).map((signal) => [
+    signal,
+    () => forwardCancellation(signal),
+  ]),
+);
+for (const [signal, handler] of Object.entries(signalHandlers))
+  process.on(signal, handler);
+
+const compiler = process.env.REA_VERIFY_FPC_COMMAND;
+if (process.platform !== "darwin" || !isAbsolute(compiler ?? ""))
+  throw new Error(
+    "Requires macOS and an absolute caller-selected REA_VERIFY_FPC_COMMAND; build the runtime first.",
+  );
+const source = fileURLToPath(
+  new URL("../tests/conformance/native/calls.pas", import.meta.url),
+);
+const fixtureLines = (await readFile(source, "utf8")).split(/\r?\n/u);
+const callerLines = new Set(
+  ["REA_VERIFY_CALLER_LOOP", "REA_VERIFY_CALLER_CALL"].map((marker) => {
+    const matches = fixtureLines.flatMap((line, index) =>
+      line.includes(marker) ? [index + 1] : [],
+    );
+    assert.equal(matches.length, 1, `fixture has one ${marker} marker`);
+    return matches[0];
+  }),
+);
+const allocatedDirectory =
+  await createCanonicalTemporaryDirectory("rea-pascal-calls-");
+let directory = allocatedDirectory.path;
+const commands = await createPackageVerifierCommands({
+  workspace: {
+    path: allocatedDirectory.allocatedPath,
+    close: () =>
+      rm(allocatedDirectory.allocatedPath, { recursive: true, force: true }),
+  },
+});
+const execute = (command, arguments_, { timeout }) =>
+  commands.exec(command, arguments_, {
+    timeout,
+    diagnosticBytes: 1024 * 1024,
+    signal: cancellation.signal,
+  });
+const input = {
+  breakpoints: [{ kind: "function", name: "rea_pascal_call" }],
+  argument_registers: 1,
+  backtrace_frames: 1,
+  duration_ms: 30_000,
+};
+const inspect = (result) => {
+  assert.equal(result.process.outcome, "exited");
+  assert.equal(result.process.exit_status, 0);
+  assert.equal(result.process.terminated, true);
+  assert.equal(result.process.stdout.text, "pascal 0\npascal 1\npascal 2\n");
+  assert.equal(result.events.length, 3);
+  assert.deepEqual(
+    result.events.map((event) => event.registers[0].value),
+    ["0x0", "0x1", "0x2"],
+  );
+  assert.equal(result.breakpoints[0].location_count, 1);
+  for (const event of result.events) {
+    assert.equal(event.backtrace.length, 1);
+    assert.equal(event.backtrace[0].source_location?.file_path, source);
+    assert.equal(event.backtrace[0].module_path, join(directory, "calls"));
+    assert.ok(
+      callerLines.has(event.backtrace[0].source_location.line),
+      "caller is the Pascal loop/call site",
+    );
+  }
+  for (const location of [
+    ...result.events,
+    ...result.breakpoints[0].locations,
+  ]) {
+    assert.equal(location.source_location?.file_path, source);
+    assert.ok(location.source_location.line > 0);
+  }
+};
+const stable = (result) =>
+  result.events.map((event) => ({
+    file_address: event.file_address,
+    source_location: event.source_location,
+    registers: event.registers,
+    callers: event.backtrace.map((frame) => ({
+      file_address: frame.file_address,
+      symbol: frame.symbol,
+      source_location: frame.source_location,
+    })),
+  }));
+try {
+  const result = await withVerifierCleanup(async () => {
+    const version = (
+      await execute(compiler, ["-iV"], { timeout: 30_000 })
+    ).stdout.trim();
+    const architecture = (
+      await execute(compiler, ["-iTP"], {
+        timeout: 30_000,
+      })
+    ).stdout.trim();
+    await execute(
+      compiler,
+      [
+        "-dDEBUG",
+        "-gw3",
+        "-O-",
+        "-Xs-",
+        `-FE${directory}`,
+        `-FU${directory}`,
+        source,
+      ],
+      { timeout: 120_000 },
+    );
+    const binary = join(directory, "calls");
+    const cli = await artifactCli(
+      "observe-native-calls",
+      binary,
+      [JSON.stringify(input)],
+      { timeoutMs: 180_000, signal: cancellation.signal, commands },
+    );
+    cancellation.signal.throwIfAborted();
+    inspect(cli);
+    await withArtifactMcp(
+      binary,
+      async (client) => {
+        const mcp = await artifactMcpResult(
+          client,
+          "observe_native_calls",
+          input,
+          { signal: cancellation.signal },
+        );
+        cancellation.signal.throwIfAborted();
+        inspect(mcp);
+        assert.deepEqual(stable(mcp), stable(cli));
+      },
+      { signal: cancellation.signal, commands },
+    );
+    cancellation.signal.throwIfAborted();
+    return {
+      ok: true,
+      mocked: false,
+      compiler,
+      version,
+      architecture,
+      debugger: cli.debugger,
+      cli: true,
+      stdio_mcp: true,
+      scope:
+        "bounded native call entries and compiler-provided source coordinates; no typed Pascal locals or interactive stepping",
+    };
+  }, [() => commands.close()]);
+  cancellation.signal.throwIfAborted();
+  console.log(JSON.stringify(result));
+} catch (cause) {
+  const cancelled =
+    cause === cancellation.signal.reason ||
+    (cause?.reason === "cancelled" &&
+      cause.cancellation?.reason === cancellation.signal.reason &&
+      cause.cleanupFailure === null);
+  if (shutdownSignal === undefined || !cancelled) throw cause;
+  console.error(`Verification cancelled by ${shutdownSignal}.`);
+  process.exitCode = signalExitCodes[shutdownSignal];
+} finally {
+  for (const signal of Object.keys(signalExitCodes))
+    process.off(signal, signalHandlers[signal]);
+}

scripts/verify-real-ghidra-checkpoints.mjs

@@ -0,0 +1,489 @@
+#!/usr/bin/env node
+
+import assert from "node:assert/strict";
+import { execFile } from "node:child_process";
+import { createHash } from "node:crypto";
+import {
+  copyFile,
+  mkdtemp,
+  mkdir,
+  readFile,
+  readdir,
+  rm,
+  writeFile,
+} from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+import { fileURLToPath } from "node:url";
+import { promisify } from "node:util";
+import { Client } from "@modelcontextprotocol/client";
+import { StdioClientTransport } from "@modelcontextprotocol/client/stdio";
+import {
+  requireMcpOperationResult,
+  requireMcpToolError,
+} from "./lib/mcp-verifier-results.mjs";
+import {
+  createVerifierRun,
+  completeVerifierRun,
+  assertVerifierCleanupComplete,
+} from "./lib/verifier-run.mjs";
+
+if (process.platform === "win32")
+  throw new Error(
+    "Owned Ghidra checkpoints currently support Linux/macOS only.",
+  );
+const run = createVerifierRun(),
+  exec = promisify(execFile);
+const root = await mkdtemp(join(tmpdir(), "rea-ghidra-checkpoints-"));
+const runtime = join(root, "runtime"),
+  checkpointDirectory = join(root, "checkpoints");
+const entrypoint = fileURLToPath(new URL("./rea.mjs", import.meta.url));
+const sourcePath = join(root, "fixture.c"),
+  target = join(root, "checkpoint-fixture");
+const env = {
+  ...process.env,
+  HOME: root,
+  XDG_CONFIG_HOME: join(root, "config"),
+  XDG_CACHE_HOME: join(root, "cache"),
+  XDG_DATA_HOME: join(root, "data"),
+  TMPDIR: runtime,
+  JDK_JAVA_OPTIONS: `-Duser.home=${root}`,
+  REA_ANALYSIS_PROVIDER: "ghidra",
+  REA_GHIDRA_CHECKPOINT_DIR: checkpointDirectory,
+};
+for (const name of [
+  "REA_GHIDRA_PROJECT_PATH",
+  "REA_GHIDRA_PROGRAM_NAME",
+  "REA_GHIDRA_SEED_FILE",
+  "REA_GHIDRA_NATIVEAOT_JAR",
+  "REA_GHIDRA_LANGUAGE_ID",
+  "REA_GHIDRA_COMPILER_SPEC_ID",
+  "REA_GHIDRA_DISABLED_ANALYZERS",
+])
+  delete env[name];
+const report = {
+  verifier: "ghidra-owned-checkpoints",
+  phases: [],
+  target: null,
+};
+const sha = async (path) =>
+  createHash("sha256")
+    .update(await readFile(path))
+    .digest("hex");
+async function phase(name, operation) {
+  const start = performance.now();
+  try {
+    const facts = await operation();
+    report.phases.push({
+      name,
+      status: "verified",
+      elapsed_ms: Math.round(performance.now() - start),
+      ...facts,
+    });
+  } catch (cause) {
+    report.phases.push({
+      name,
+      status: "failed",
+      elapsed_ms: Math.round(performance.now() - start),
+    });
+    throw cause;
+  }
+}
+async function cli(procedure, flags = [], path = target) {
+  const { stdout } = await exec(
+    process.execPath,
+    [
+      entrypoint,
+      "decompile",
+      path,
+      procedure,
+      "--provider",
+      "ghidra",
+      "--json",
+      ...flags,
+    ],
+    { env, timeout: 240000, maxBuffer: 16 * 1024 * 1024 },
+  );
+  return JSON.parse(stdout);
+}
+async function refuseCli(procedure, flags, expected) {
+  let refusal;
+  try {
+    await cli(procedure, flags);
+  } catch (cause) {
+    assert.equal(cause.code, 1, cause.stderr);
+    refusal = JSON.parse(cause.stdout);
+  }
+  assert.ok(refusal, "CLI unexpectedly accepted unavailable checkpoint state");
+  assert.equal(refusal.code, expected, JSON.stringify(refusal));
+  return refusal;
+}
+async function connect(environment = {}) {
+  const client = new Client({
+    name: "rea-ghidra-checkpoint-verifier",
+    version: "1",
+  });
+  const transport = new StdioClientTransport({
+    command: process.execPath,
+    args: [entrypoint, "mcp"],
+    env: { ...env, ...environment },
+    stderr: "pipe",
+  });
+  transport.stderr?.on("data", () => {});
+  try {
+    await client.connect(transport);
+  } catch (cause) {
+    await client.close();
+    await transport.close();
+    throw cause;
+  }
+  const raw = (name, args = {}) =>
+    client.callTool({ name, arguments: args }, { timeout: 240000 });
+  return {
+    raw,
+    call: async (name, args = {}) =>
+      requireMcpOperationResult(await raw(name, args), name),
+    close: async () => {
+      await client.close();
+      await transport.close();
+    },
+  };
+}
+let manifestPath;
+const manifest = async () => JSON.parse(await readFile(manifestPath, "utf8"));
+try {
+  await mkdir(runtime);
+  await writeFile(
+    sourcePath,
+    `typedef struct CheckpointRecord { int value; int flag; } CheckpointRecord;
+__attribute__((noinline)) int rea_checkpoint_leaf(CheckpointRecord *record) { return record->value * 7 + record->flag; }
+int main(void) { CheckpointRecord record = { 3, 11 }; return rea_checkpoint_leaf(&record); }
+`,
+  );
+  await exec("cc", [
+    "-O0",
+    "-g",
+    "-gdwarf-4",
+    "-fno-inline",
+    sourcePath,
+    "-o",
+    target,
+  ]);
+  const targetDigest = await sha(target);
+  report.target = {
+    sha256: targetDigest,
+    source: "self-built C struct/function fixture; never executed",
+    host: process.platform,
+    architecture: process.arch,
+  };
+  let original, initialManifest;
+  const snapshotPath = join(root, "analysis-snapshot.json");
+  await phase(
+    "a cold MCP session keeps its live Program across initial save and repeated open",
+    async () => {
+      const cold = await connect({
+        REA_GHIDRA_CHECKPOINT_DIR: join(root, "cold-session-checkpoints"),
+      });
+      try {
+        await cold.call("open_binary", { path: target, provider_id: "ghidra" });
+        await cold.call("procedure_pseudo_code", {
+          procedure: "rea_checkpoint_leaf",
+        });
+        const id = (await cold.call("binary_session")).analysis_run.run_id;
+        await cold.call("annotate_native_function", {
+          procedure: "rea_checkpoint_leaf",
+          comment: "cold-session unsaved comment",
+        });
+        await cold.call("open_binary", { path: target, provider_id: "ghidra" });
+        assert.equal(
+          (await cold.call("binary_session")).analysis_run.run_id,
+          id,
+        );
+        const current = await cold.call("procedure_pseudo_code", {
+          procedure: "rea_checkpoint_leaf",
+        });
+        assert.match(JSON.stringify(current), /cold-session unsaved comment/);
+        await cold.call("close_binary");
+        return { same_live_run: true, unsaved_metadata_retained: true };
+      } finally {
+        await cold.close();
+      }
+    },
+  );
+  await phase("first analysis creates a checkpoint", async () => {
+    original = await cli("rea_checkpoint_leaf", ["--snapshot", snapshotPath]);
+    assert.match(JSON.stringify(original.normalized_result), /value/);
+    const keys = await readdir(checkpointDirectory);
+    assert.equal(keys.length, 1);
+    manifestPath = join(checkpointDirectory, keys[0], "current.json");
+    initialManifest = await manifest();
+    assert.equal(initialManifest.target_sha256, targetDigest);
+    assert.deepEqual(
+      original.analysis_profile.parameters.owned_checkpoint.state,
+      { kind: "initial-analysis" },
+    );
+    return {
+      provider_version: original.provider.version,
+      response_bytes: Buffer.byteLength(JSON.stringify(original)),
+    };
+  });
+  await phase(
+    "the first checkpoint publication preserves initial immutable snapshot identity",
+    async () => {
+      const cached = await cli("rea_checkpoint_leaf", [
+        "--snapshot",
+        snapshotPath,
+      ]);
+      assert.deepEqual(cached, original);
+      assert.deepEqual(await manifest(), initialManifest);
+      return {};
+    },
+  );
+  await phase(
+    "fresh CLI restores the Program and does not rewrite it",
+    async () => {
+      const restored = await cli("rea_checkpoint_leaf");
+      assert.deepEqual(restored.normalized_result, original.normalized_result);
+      assert.equal(
+        restored.analysis_profile.digest,
+        original.analysis_profile.digest,
+      );
+      assert.ok(
+        restored.limitations.some((value) =>
+          value.includes(initialManifest.source.sha256),
+        ),
+      );
+      assert.deepEqual(await manifest(), initialManifest);
+      return {
+        checkpoint_sha256: initialManifest.source.sha256,
+        response_bytes: Buffer.byteLength(JSON.stringify(restored)),
+      };
+    },
+  );
+  await phase(
+    "another path with identical target bytes reuses the same Program",
+    async () => {
+      const alias = join(root, "renamed-target");
+      await copyFile(target, alias);
+      const restored = await cli("rea_checkpoint_leaf", [], alias);
+      assert.deepEqual(restored.normalized_result, original.normalized_result);
+      assert.equal(restored.caller_input_path, alias);
+      assert.deepEqual(await manifest(), initialManifest);
+      return {};
+    },
+  );
+  await phase(
+    "MCP preserves a live run, refuses a concurrent writer, and saves edits",
+    async () => {
+      const active = await connect();
+      try {
+        await active.call("open_binary", {
+          path: target,
+          provider_id: "ghidra",
+        });
+        await active.call("procedure_pseudo_code", {
+          procedure: "rea_checkpoint_leaf",
+        });
+        const id = (await active.call("binary_session")).analysis_run.run_id;
+        const other = await connect();
+        try {
+          await other.call("open_binary", {
+            path: target,
+            provider_id: "ghidra",
+          });
+          const error = requireMcpToolError(await other.raw("list_documents"));
+          assert.equal(error.code, "configuration_invalid");
+          assert.match(error.message, /another REA session/);
+          await other.call("close_binary");
+        } finally {
+          await other.close();
+        }
+        await active.call("open_binary", {
+          path: target,
+          provider_id: "ghidra",
+        });
+        assert.equal(
+          (await active.call("binary_session")).analysis_run.run_id,
+          id,
+        );
+        await active.call("annotate_native_function", {
+          procedure: "rea_checkpoint_leaf",
+          name: "rea_checkpoint_retained",
+          comment: "REA checkpoint first comment",
+        });
+        await active.call("close_binary");
+        assert.notDeepEqual(await manifest(), initialManifest);
+        return { same_live_run: true, concurrent_owner_refused: true };
+      } finally {
+        await active.close();
+      }
+    },
+  );
+  await phase("new MCP restores edits and remains editable", async () => {
+    const resumed = await connect();
+    try {
+      await resumed.call("open_binary", {
+        path: target,
+        provider_id: "ghidra",
+      });
+      const analysis = await resumed.call("analyze_function", {
+        procedure: "rea_checkpoint_retained",
+        detail: "complete",
+      });
+      assert.equal(analysis.procedure.name, "rea_checkpoint_retained");
+      assert.match(JSON.stringify(analysis), /REA checkpoint first comment/);
+      assert.match(analysis.pseudocode, /value/);
+      await resumed.call("annotate_native_function", {
+        procedure: "rea_checkpoint_retained",
+        comment: "REA checkpoint second comment",
+      });
+      await resumed.call("close_binary");
+      return { structure_field_preserved: true };
+    } finally {
+      await resumed.close();
+    }
+  });
+  await phase("CLI sees the second MCP edit", async () => {
+    const result = await cli("rea_checkpoint_retained");
+    assert.match(
+      JSON.stringify(result.normalized_result),
+      /REA checkpoint second comment/,
+    );
+    return {};
+  });
+  await phase(
+    "an older immutable REA snapshot refuses the changed checkpoint",
+    async () => {
+      const refusal = await refuseCli(
+        "rea_checkpoint_leaf",
+        ["--snapshot", snapshotPath],
+        "evidence_integrity_mismatch",
+      );
+      assert.ok(refusal.details.binding_mismatch.profile_digest);
+      return {};
+    },
+  );
+  await phase(
+    "an edited live Program switches to identical bytes at another path",
+    async () => {
+      const active = await connect();
+      const alias = join(root, "live-alias");
+      await copyFile(target, alias);
+      try {
+        await active.call("open_binary", {
+          path: target,
+          provider_id: "ghidra",
+        });
+        await active.call("annotate_native_function", {
+          procedure: "rea_checkpoint_retained",
+          comment: "REA checkpoint second comment; saved during alias switch",
+        });
+        await active.call("open_binary", {
+          path: alias,
+          provider_id: "ghidra",
+        });
+        const result = await active.call("procedure_pseudo_code", {
+          procedure: "rea_checkpoint_retained",
+        });
+        assert.match(JSON.stringify(result), /saved during alias switch/);
+        await active.call("close_binary");
+        return { alias_switch_preserved_edits: true };
+      } finally {
+        await active.close();
+      }
+    },
+  );
+  const current = await manifest(),
+    bytes = await readFile(manifestPath);
+  await phase(
+    "target/profile mismatch is refused without replacing the saved state",
+    async () => {
+      try {
+        await writeFile(
+          manifestPath,
+          JSON.stringify({ ...current, target_sha256: "0".repeat(64) }),
+        );
+        await refuseCli("rea_checkpoint_retained", [], "configuration_invalid");
+      } finally {
+        await writeFile(manifestPath, bytes);
+      }
+      return {};
+    },
+  );
+  await phase(
+    "malformed manifest is refused without a fresh import",
+    async () => {
+      try {
+        await writeFile(manifestPath, "{");
+        await refuseCli("rea_checkpoint_retained", [], "configuration_invalid");
+      } finally {
+        await writeFile(manifestPath, bytes);
+      }
+      return {};
+    },
+  );
+  await phase(
+    "corrupt packed data is refused and explicit restoration recovers",
+    async () => {
+      const packed = join(
+          checkpointDirectory,
+          (await readdir(checkpointDirectory))[0],
+          current.source.file,
+        ),
+        backup = join(root, "good.gzf");
+      await copyFile(packed, backup);
+      try {
+        await writeFile(packed, "corrupted packed data");
+        await refuseCli("rea_checkpoint_retained", [], "configuration_invalid");
+      } finally {
+        await copyFile(backup, packed);
+      }
+      const result = await cli("rea_checkpoint_retained");
+      assert.match(
+        JSON.stringify(result.normalized_result),
+        /REA checkpoint second comment/,
+      );
+      return {};
+    },
+  );
+  assert.equal(await sha(target), targetDigest);
+  assert.deepEqual(await readdir(runtime), []);
+  const checkpointFiles = await readdir(
+    join(checkpointDirectory, (await readdir(checkpointDirectory))[0]),
+  );
+  assert.equal(
+    checkpointFiles.length,
+    2,
+    "Only the current manifest and packed Program should remain",
+  );
+  report.status = "verified";
+} catch (cause) {
+  report.status = "failed";
+  report.error = cause instanceof Error ? cause.stack : String(cause);
+  if (typeof cause?.stdout === "string")
+    report.failure_stdout = cause.stdout.slice(-12000);
+  if (typeof cause?.stderr === "string")
+    report.failure_stderr = cause.stderr.slice(-4000);
+  process.exitCode = 1;
+} finally {
+  report.run = await completeVerifierRun(run);
+  let cleanupVerified = false;
+  try {
+    assertVerifierCleanupComplete(report.run.process_lineage);
+    cleanupVerified = true;
+  } catch (cause) {
+    report.cleanup_error = String(cause);
+    report.retained_workspace = root;
+    process.exitCode = 1;
+  }
+  if (cleanupVerified) {
+    try {
+      await rm(root, { recursive: true, force: true });
+    } catch (cause) {
+      report.cleanup_error = String(cause);
+      report.retained_workspace = root;
+      process.exitCode = 1;
+    }
+  }
+  process.stdout.write(JSON.stringify(report, null, 2) + "\n");
+}

scripts/verify-real-ghidra-dos.mjs

@@ -35,10 +35,10 @@ import { verifyGhidraAddressBoundaries } from "./lib/real-ghidra-address-boundar
 // This lane intentionally has no game paths, binary seeds or compiler dependency.
 if (process.argv.length !== 2)
   throw new Error("Usage: node scripts/verify-real-ghidra-dos.mjs");
-if (!["linux", "darwin"].includes(process.platform))
-  throw new Error(
-    "verify:ghidra:dos supports Linux/macOS hosts only; Windows P0 is PE x86-64 only.",
-  );
+if (!["linux", "darwin", "win32"].includes(process.platform))
+  throw new Error("verify:ghidra:dos supports Linux, macOS and Windows hosts.");
+// Windows P0 is read-only: annotation and naming edits must be refused.
+const windows = process.platform === "win32";
 if (process.env.GHIDRA_INSTALL_DIR === undefined)
   throw new Error(
     "verify:ghidra:dos prerequisite missing: GHIDRA_INSTALL_DIR (bring your own Ghidra).",
@@ -72,6 +72,8 @@ await writeFile(targetPath, fixture.bytes, { mode: 0o600 });
 const sha256 = digest(fixture.bytes);
 const entrypoint = fileURLToPath(new URL("./rea.mjs", import.meta.url));
 const env = {
+  // Windows children need the system environment (SystemRoot, profile paths).
+  ...(windows ? { ...process.env, TMP: runtime, TEMP: runtime } : {}),
   PATH: process.env.PATH ?? "/usr/bin:/bin",
   TMPDIR: runtime,
   REA_LOG_LEVEL: "silent",
@@ -396,21 +398,25 @@ try {
     client,
     identities.entry.address,
     cliEvidence,
+    { mutable: !windows },
   );
   const entrySymbol = entryWindow.procedure.symbol;
   assert.ok(entrySymbol != null, "The DOS entry needs observed symbol facts");
   // Restoring the name is itself a user edit, so Ghidra records user provenance.
+  // Windows P0 refuses edits and never renames, so its entry stays unchanged.
   assert.deepEqual(
     await call("read_function_instructions", {
       procedure: identities.entry.address,
     }),
-    {
-      ...entryWindow,
-      procedure: {
-        ...entryWindow.procedure,
-        symbol: { ...entrySymbol, source: "user_defined" },
-      },
-    },
+    windows
+      ? entryWindow
+      : {
+          ...entryWindow,
+          procedure: {
+            ...entryWindow.procedure,
+            symbol: { ...entrySymbol, source: "user_defined" },
+          },
+        },
     "Restoring the entry name changed more than its symbol provenance",
   );
   assert.equal(
@@ -474,7 +480,11 @@ try {
       "The complete body is Ghidra's observed AddressSet, not independently proven historical compiler ownership.",
       "Language/compiler identity is bound by the production authenticated bridge handshake; profile loader is the declared import policy.",
       "Native high-pcode flow is excluded from cross-runtime parity: LOAD/STORE address-space selector constants are process-specific in current Ghidra output. Both dossiers are still strictly parsed.",
-      "Windows P0 remains unsupported for DOS MZ.",
+      ...(windows
+        ? [
+            "Windows P0 is read-only: annotation and naming edits were checked as refused, not exercised.",
+          ]
+        : []),
     ],
   };
 } catch (error) {
@@ -510,7 +520,8 @@ try {
 }
 assert.ok(report, "No DOS proof report was produced");
 const verifierRun = await completeVerifierRun(run);
-assertVerifierCleanupComplete(verifierRun.process_lineage);
+// Windows provider jobs are verified by their native owners, as in the 6502 lane.
+if (!windows) assertVerifierCleanupComplete(verifierRun.process_lineage);
 process.stdout.write(
   `${JSON.stringify({ verifier_run: verifierRun, ...report, cleanup: "complete" })}\n`,
 );

scripts/verify-real-ghidra-function-bundle.mjs

@@ -0,0 +1,187 @@
+#!/usr/bin/env node
+
+// Exercise the public one-shot CLI on a caller-owned saved project. The report
+// is intentionally synthetic; it is not a claim about Ghidra's analysis history.
+import assert from "node:assert/strict";
+import { createHash } from "node:crypto";
+import {
+  mkdtemp,
+  mkdir,
+  readFile,
+  readdir,
+  rm,
+  writeFile,
+} from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join, resolve } from "node:path";
+import { createVerifierCommands } from "./lib/verify-commands.mjs";
+import { withVerifierCleanup } from "./lib/verifier-cleanup.mjs";
+const installation = process.env.GHIDRA_INSTALL_DIR;
+if (!installation || !process.env.JAVA_HOME)
+  throw new Error(
+    "Set GHIDRA_INSTALL_DIR and JAVA_HOME to caller-installed Ghidra and JDK 21.",
+  );
+const commands = await createVerifierCommands();
+let root;
+let commandsClosed = false;
+const targetHash = await withVerifierCleanup(async () => {
+  root = await mkdtemp(join(tmpdir(), "rea-function-bundle-"));
+  const target = join(root, "fixture");
+  const projectDir = join(root, "project");
+  const scriptDir = join(root, "scripts");
+  const source = join(root, "fixture.c");
+  const project = join(projectDir, "SourceControl.gpr");
+  const repo = resolve(process.cwd());
+  const hash = (data) => createHash("sha256").update(data).digest("hex");
+  const tree = async (directory, prefix = "") => {
+    const result = [];
+    for (const entry of (
+      await readdir(directory, { withFileTypes: true })
+    ).sort((a, b) => a.name.localeCompare(b.name))) {
+      const path = join(directory, entry.name);
+      const relative = join(prefix, entry.name);
+      if (entry.isDirectory()) result.push(...(await tree(path, relative)));
+      else if (entry.isFile())
+        result.push([relative, hash(await readFile(path))]);
+      else throw new Error(`Unexpected project entry: ${relative}`);
+    }
+    return result;
+  };
+  const run = async (command, args, options = {}) =>
+    commands.exec(command, args, {
+      timeout: 120_000,
+      maxBuffer: 16 * 1024 * 1024,
+      ...options,
+    });
+  await mkdir(projectDir);
+  await mkdir(scriptDir);
+  await writeFile(
+    source,
+    "__attribute__((noinline)) int leaf(int x) { return x + 1; }\nint main(void) { return leaf(2); }\n",
+  );
+  await writeFile(
+    join(scriptDir, "SetHistory.java"),
+    `import ghidra.app.script.GhidraScript;
+import ghidra.program.model.listing.Program;
+public class SetHistory extends GhidraScript {
+  public void run() throws Exception {
+    currentProgram.getOptions(Program.PROGRAM_INFO).setString("REA disabled analyzers", "{\\"format\\":\\"rea-ghidra-disabled-analyzers-v1\\",\\"analyzers\\":[{\\"name\\":\\"Synthetic historical control\\",\\"status\\":\\"disabled\\"}]}");
+  }
+}
+`,
+  );
+  await run(process.env.REA_CC ?? "cc", ["-O0", "-g", source, "-o", target]);
+  await run(join(installation, "support", "analyzeHeadless"), [
+    projectDir,
+    "SourceControl",
+    "-import",
+    target,
+    "-scriptPath",
+    scriptDir,
+    "-postScript",
+    "SetHistory.java",
+  ]);
+  const before = await tree(projectDir);
+  const targetHash = hash(await readFile(target));
+  const env = {
+    ...process.env,
+    REA_GHIDRA_PROJECT_PATH: project,
+    REA_GHIDRA_PROGRAM_NAME: "fixture",
+  };
+  const cli = join(repo, "scripts", "rea.mjs");
+  for (const detail of ["complete", "summary"]) {
+    const output = join(root, `${detail}.json`);
+    const { stdout } = await run(
+      process.execPath,
+      [
+        cli,
+        "function",
+        target,
+        "main",
+        "--provider",
+        "ghidra",
+        "--detail",
+        detail,
+        "--evidence_output",
+        output,
+        "--format",
+        "json",
+        "--full-output",
+      ],
+      { env },
+    );
+    assert.equal(JSON.parse(stdout).ok, true);
+    const bundle = JSON.parse(await readFile(output, "utf8"));
+    const parent = bundle.records.find(
+      (record) => record.operation === "analyze_function",
+    );
+    assert.ok(parent, "function observation missing from bundle");
+    assert.ok(
+      parent.evidence_links.length,
+      "fixture did not produce a linked historical source",
+    );
+    const records = new Map(
+      bundle.records.map((record) => [record.evidence_id, record]),
+    );
+    for (const record of bundle.records)
+      for (const link of record.evidence_links)
+        assert.ok(records.has(link), `bundle omits linked Evidence ${link}`);
+    assert.ok(
+      parent.evidence_links.some(
+        (id) => records.get(id)?.operation === "health",
+      ),
+      "historical health source missing",
+    );
+  }
+  const existing = join(root, "existing.json");
+  await writeFile(existing, "caller-owned\n");
+  let failure;
+  try {
+    await run(
+      process.execPath,
+      [
+        cli,
+        "function",
+        target,
+        "main",
+        "--provider",
+        "ghidra",
+        "--detail",
+        "summary",
+        "--evidence_output",
+        existing,
+        "--format",
+        "json",
+        "--full-output",
+      ],
+      { env },
+    );
+    assert.fail("existing output unexpectedly overwritten");
+  } catch (error) {
+    if (error.code !== 1) throw error;
+    failure = JSON.parse(error.snapshot.stdout.text);
+  }
+  assert.equal(await readFile(existing, "utf8"), "caller-owned\n");
+  assert.equal(failure.ok, false);
+  assert.equal(failure.error.details.source_closure.complete, true);
+  assert.ok(
+    failure.error.details.source_closure.records.some(
+      (record) => record.operation === "health",
+    ),
+  );
+  assert.equal(hash(await readFile(target)), targetHash);
+  assert.deepEqual(await tree(projectDir), before);
+  return targetHash;
+}, [
+  async () => {
+    await commands.close();
+    commandsClosed = true;
+  },
+  async () => {
+    if (commandsClosed && root !== undefined)
+      await rm(root, { recursive: true, force: true });
+  },
+]);
+process.stdout.write(
+  `PASS Ghidra function bundles: complete, summary, no-overwrite; target and project unchanged (${targetHash})\n`,
+);

scripts/verify-real-ghidra-mips.mjs

@@ -38,6 +38,8 @@ import {
   buildPspFixture,
   assertPspLoadedImage,
   assertPspProbe,
+  PSP_VFPU_DECODE_CASES,
+  assertPspVfpuProbe,
 } from "../tests/conformance/ghidra/psp-fixture.mjs";
 import {
   requireMcpToolError,
@@ -541,6 +543,47 @@ try {
       });
       if (psp) assertPspProbe(move, branch);
       else assertMipsProbe(move, branch, byteOrder, probe);
+      let vfpuCoverage;
+      if (psp) {
+        const vfpuAddress = BigInt(independent.symbols.rea_psp_vfpu_probe);
+        const vfpuInstructions = [];
+        for (const { index } of PSP_VFPU_DECODE_CASES) {
+          vfpuInstructions.push(
+            await call("inspect_native_instruction", {
+              address: `0x${(vfpuAddress + 4n * BigInt(index)).toString(16)}`,
+            }),
+          );
+        }
+        assertPspVfpuProbe(vfpuInstructions);
+        const vfpuDossier = functionDossierSchema.parse(
+          await call("analyze_function", {
+            procedure: independent.symbols.rea_psp_vfpu_probe,
+            detail: "complete",
+          }),
+        );
+        assert.equal(BigInt(vfpuDossier.procedure.address), vfpuAddress);
+        const flow = vfpuDossier.native_value_flow;
+        const hasHighPcode = flow?.available === true;
+        vfpuCoverage = {
+          decoded_instructions: vfpuInstructions.length,
+          prefix_sites: 4,
+          vadd_sites: 3,
+          high_pcode: hasHighPcode ? "observed" : "unavailable",
+          opaque_high_pcode_operations: hasHighPcode
+            ? flow.operations.filter(({ opcode }) => opcode === "CALLOTHER")
+                .length
+            : null,
+          truncated: hasHighPcode ? flow.truncated : null,
+          unavailable_reason:
+            flow?.available === false
+              ? flow.reason
+              : hasHighPcode
+                ? null
+                : "Ghidra did not report a HighFunction value flow",
+          pseudocode_nonempty: vfpuDossier.pseudocode.trim().length > 0,
+          numeric_vector_semantics: "not_verified",
+        };
+      }
       const global = await call("read_bytes", {
         address: independent.symbols[`${prefix}_global`],
         length: 4,
@@ -807,6 +850,9 @@ try {
           "independent ELF/ABI and symbols",
           "loaded Ghidra identity",
           "fixed instruction bytes and immediate",
+          ...(psp
+            ? ["VFPU prefix/vadd opcode decoding (not arithmetic equivalence)"]
+            : []),
           psp
             ? "Allegrex BITREV decoding and A-B-A target identity"
             : "conditional branch destination",
@@ -816,6 +862,7 @@ try {
             ? ["soft-float o32 parameter/return storage and caller constants"]
             : []),
         ],
+        ...(vfpuCoverage === undefined ? {} : { vfpu_decode: vfpuCoverage }),
         ...(softFloat === undefined ? {} : { soft_float: softFloat }),
         procedures: procedures.length,
         carved: carved ?? {

scripts/verify-real-ida.mjs

@@ -31,7 +31,7 @@ const { values } = parseArgs({
 });
 if (values.target === undefined || process.env.REA_IDA_MCP_CONFIG === undefined)
   throw new Error(
-    "IDA verification requires --target and REA_IDA_MCP_CONFIG; see docs/ida-provider.md. No toolchain is installed by this lane.",
+    "IDA verification requires --target and REA_IDA_MCP_CONFIG; see docs/providers/ida-provider.md. No toolchain is installed by this lane.",
   );
 if (
   (values["second-procedure"] === undefined) !==
@@ -79,7 +79,7 @@ if (
     values["second-marker"] === undefined)
 )
   throw new Error(
-    "Native IDA verification requires --second-procedure and --second-marker to verify distinct-function switching; see docs/ida-provider.md.",
+    "Native IDA verification requires --second-procedure and --second-marker to verify distinct-function switching; see docs/providers/ida-provider.md.",
   );
 const environment = Object.fromEntries(
   Object.entries({

scripts/verify-real-kuna.mjs

@@ -26,8 +26,17 @@ import { parseArgs, promisify } from "node:util";
 import { Client } from "@modelcontextprotocol/client";
 import { StdioClientTransport } from "@modelcontextprotocol/client/stdio";
 import { inspectKunaInstallation } from "../dist/kuna/KunaInstallation.js";
+import {
+  KUNA_RELEASE_VERIFICATION_EXPLANATION,
+  KUNA_UNVERIFIED_VERSION_REMEDIATION,
+  KUNA_VERIFIED_VERSION,
+} from "../dist/kuna/KunaRelease.js";
 import { ArtifactResourceScope } from "../dist/artifacts/ArtifactResourceScope.js";
 import { AnalysisCleanupLease } from "../dist/artifacts/AnalysisCleanupLease.js";
+import {
+  KUNA_XREF_MISSING_NAME_REMEDIATION,
+  missingKunaXrefNameMessage,
+} from "../dist/kuna/KunaSelectorGuidance.js";
 import {
   requireMcpOperationResult,
   requireMcpToolError,
@@ -233,13 +242,13 @@ const openServer = async (provider, kunaSettings = {}) => {
       structured: result.structuredContent,
     };
   };
-  const callError = async (name, arguments_ = {}) => {
-    const result = await client.callTool(
-      { name, arguments: arguments_ },
-      { timeout: 3_600_000 },
+  const callError = async (name, arguments_ = {}) =>
+    requireMcpToolError(
+      await client.callTool(
+        { name, arguments: arguments_ },
+        { timeout: 3_600_000 },
+      ),
     );
-    return requireMcpToolError(result);
-  };
   const close = async (priorFailure) => {
     clearInterval(timer);
     await sample();
@@ -277,6 +286,34 @@ const openServer = async (provider, kunaSettings = {}) => {
       path: provider.path,
       provider_id: provider.id,
     });
+    if (provider.id === "kuna") {
+      const status = (await call("binary_session")).value;
+      const binding = status.analysis_provider_binding;
+      const verification = binding.release_verification;
+      assert.equal(verification.basis, "reported_version");
+      assert.equal(verification.verified_version, KUNA_VERIFIED_VERSION);
+      assert.equal(
+        verification.reported_version,
+        binding.analysis_profile.parameters.kuna_version,
+      );
+      assert.equal(
+        verification.status,
+        binding.analysis_profile.parameters.kuna_version ===
+          KUNA_VERIFIED_VERSION
+          ? "verified"
+          : "unverified",
+      );
+      assert.equal(
+        verification.explanation,
+        KUNA_RELEASE_VERIFICATION_EXPLANATION,
+      );
+      if (verification.status === "unverified")
+        assert.equal(
+          verification.remediation,
+          KUNA_UNVERIFIED_VERSION_REMEDIATION,
+        );
+      else assert.equal(verification.remediation, null);
+    }
   } catch (cause) {
     // A rejected connection/target still owns its transport and workspace.
     await close(cause);
@@ -409,6 +446,44 @@ const verifyKuna = async (
       }),
     });
     const listed = await cold.call("list_procedures");
+    if (verifyNamedTrace) {
+      const missing = await cold.callError("xrefs", {
+        address: "rea_missing_xref_inventory_name",
+      });
+      assert.equal(missing.code, "invalid_request");
+      assert.equal(
+        missing.message,
+        missingKunaXrefNameMessage("rea_missing_xref_inventory_name"),
+      );
+      assert.equal(
+        missing.remediation.action,
+        KUNA_XREF_MISSING_NAME_REMEDIATION,
+      );
+      assert.ok(missing.message.includes("rea_missing_xref_inventory_name"));
+      assert.equal(missing.recovery, undefined);
+      const procedure = await cold.callError("procedure_address", {
+        procedure: "rea_missing_procedure_name",
+      });
+      assert.equal(procedure.code, "invalid_request");
+      assert.equal(procedure.recovery, undefined);
+      assert.match(procedure.remediation.action, /search_procedures/u);
+      assert.ok(
+        procedure.details.issues.some(
+          (issue) => issue.observed?.procedure === "rea_missing_procedure_name",
+        ),
+      );
+      const missingAddress = await cold.callError("procedure_address", {
+        procedure: "0x00000001",
+      });
+      assert.equal(missingAddress.code, "invalid_request");
+      assert.equal(missingAddress.recovery, undefined);
+      assert.match(missingAddress.remediation.action, /list_procedures/u);
+      assert.ok(
+        missingAddress.details.issues.some(
+          (issue) => issue.observed?.procedure === "0x00000001",
+        ),
+      );
+    }
     for (const [name, address] of functions) {
       assert.ok(
         listed.value.some((entry) => entry.address === address),
@@ -595,15 +670,37 @@ const measureGhidra = async (path, functions) => {
   return answers;
 };
 
-/** Symbol-bearing caller binaries with the requested functions, beside their stripped copies. */
-const targetPairs = async (root, names) => {
+const describeFailure = (cause) => ({
+  message: cause instanceof Error ? cause.message : String(cause),
+  ...(cause instanceof AggregateError
+    ? { causes: cause.errors.map(describeFailure) }
+    : {}),
+});
+
+/** Inspect symbol-bearing caller binaries, retaining both selected and unmatched inputs. */
+const targetPairs = async (root, names, selection) => {
   const pairs = [];
   for (const flavor of (await readdir(root)).sort()) {
     const directory = join(root, flavor);
     if (!(await stat(directory)).isDirectory()) continue;
     for (const file of (await readdir(directory)).sort()) {
       if (file.endsWith(".stripped")) continue;
-      const symbols = await symbolAddresses(join(directory, file), names);
+      let symbols;
+      try {
+        symbols = await symbolAddresses(join(directory, file), names);
+      } catch (cause) {
+        selection.examined.push({
+          binary: `${flavor}/${file}`,
+          status: "inspection_failed",
+          error: describeFailure(cause),
+        });
+        throw cause;
+      }
+      selection.examined.push({
+        binary: `${flavor}/${file}`,
+        status: symbols.size > 0 ? "selected" : "no_matching_text_symbols",
+        matched_functions: [...symbols.keys()],
+      });
       if (symbols.size > 0) pairs.push({ flavor, directory, file, symbols });
     }
   }
@@ -624,6 +721,18 @@ const verifyVariant = async ({ flavor, directory, symbols }, variant) => {
 const results = [];
 let timeoutRecovery;
 const failures = [];
+const callerTargetSelection =
+  values.targets === undefined
+    ? undefined
+    : {
+        directory: values.targets,
+        functions_argument: values.functions ?? null,
+        requested_functions: (values.functions ?? "")
+          .split(",")
+          .filter(Boolean),
+        symbol_scan_complete: false,
+        examined: [],
+      };
 let inspectionResourcesClean = true;
 try {
   const installation = await inspectKunaInstallation(
@@ -636,13 +745,18 @@ try {
   );
   kunaVersion = `kuna ${installation.value.version}`;
   let callerPairs = [];
-  if (values.targets !== undefined) {
-    const names = (values.functions ?? "").split(",").filter(Boolean);
+  if (callerTargetSelection !== undefined) {
+    const names = callerTargetSelection.requested_functions;
     assert.ok(names.length > 0, "--targets requires --functions");
-    callerPairs = await targetPairs(values.targets, names);
+    callerPairs = await targetPairs(
+      callerTargetSelection.directory,
+      names,
+      callerTargetSelection,
+    );
+    callerTargetSelection.symbol_scan_complete = true;
     assert.ok(
       callerPairs.length > 0,
-      `No caller-built targets contain the requested functions in ${values.targets}`,
+      `No caller-built targets contain the requested functions in ${callerTargetSelection.directory}`,
     );
     const found = new Set(
       callerPairs.flatMap(({ symbols }) => [...symbols.keys()]),
@@ -730,18 +844,15 @@ if (cleanupComplete)
     cleanupComplete = false;
     failures.push(cause);
   }
-const describeFailure = (cause) => ({
-  message: cause instanceof Error ? cause.message : String(cause),
-  ...(cause instanceof AggregateError
-    ? { causes: cause.errors.map(describeFailure) }
-    : {}),
-});
 const report = {
   lane: "kuna",
   status: failures.length === 0 ? "passed" : "failed",
   kuna_version: kunaVersion,
   platform: `${process.platform}/${process.arch}`,
   verifier_run: lifecycle,
+  ...(callerTargetSelection === undefined
+    ? {}
+    : { caller_target_selection: callerTargetSelection }),
   results,
   ...(timeoutRecovery === undefined
     ? {}

scripts/verify-recorded-crash.mjs

@@ -28,7 +28,7 @@ for (const key of [
 ])
   if (!isAbsolute(environment[key] ?? ""))
     throw new Error(
-      `verify:recorded:crash requires absolute ${key}; see docs/recorded-crashes.md. No dependencies are installed by this verifier.`,
+      `verify:recorded:crash requires absolute ${key}; see docs/guides/native/recorded-crashes.md. No dependencies are installed by this verifier.`,
     );
 if (process.platform !== "linux" || process.arch !== "x64")
   throw new Error("verify:recorded:crash requires Linux x64.");

scripts/verify/android/analysis.mjs

@@ -24,7 +24,7 @@ const apk = process.env.REA_ANDROID_TEST_APK;
 const jar = process.env.REA_JADX_MCP_JAR;
 if (apk === undefined || jar === undefined)
   throw new Error(
-    "verify:android requires REA_ANDROID_TEST_APK and REA_JADX_MCP_JAR. Run npm run fixtures:android and select the downloaded files; see docs/android-analysis.md.",
+    "verify:android requires REA_ANDROID_TEST_APK and REA_JADX_MCP_JAR. Run npm run fixtures:android and select the downloaded files; see docs/guides/android/android-analysis.md.",
   );
 await access(apk);
 await access(jar);

scripts/verify/firmware/analysis.mjs

@@ -49,7 +49,7 @@ async function checkPrerequisites() {
     const value = process.env[name];
     if (value === undefined) {
       throw new Error(
-        `verify:firmware requires ${name}; see docs/firmware-analysis.md`,
+        `verify:firmware requires ${name}; see docs/guides/firmware/firmware-analysis.md`,
       );
     }
     await fs.access(value);
@@ -341,7 +341,7 @@ async function stageExt4() {
 async function stageGhidra(mcpFiles) {
   if (process.env.GHIDRA_INSTALL_DIR === undefined) {
     throw new Error(
-      "Firmware Ghidra handoff requires GHIDRA_INSTALL_DIR and Java; see docs/ghidra.md",
+      "Firmware Ghidra handoff requires GHIDRA_INSTALL_DIR and Java; see docs/providers/ghidra-provider.md",
     );
   }
 

scripts/verify/harmony/analysis.mjs

@@ -20,7 +20,7 @@ const repository = resolve(dirname(fileURLToPath(import.meta.url)), "../../..");
 const hap = process.env.REA_HARMONY_TEST_HAP;
 if (hap === undefined)
   throw new Error(
-    "verify:harmony requires REA_HARMONY_TEST_HAP. Run npm run fixtures:harmony and set it to the downloaded file; see docs/harmony-analysis.md.",
+    "verify:harmony requires REA_HARMONY_TEST_HAP. Run npm run fixtures:harmony and set it to the downloaded file; see docs/guides/harmony/harmony-analysis.md.",
   );
 await access(hap);
 const hashFile = async (path) => {