/**
 * AEGIS SOAR M3+M4 Verification-Machinery Kit (AS/PLATFORM/2026/002) — the BINDING
 * proven-equivalence gate (spec §2).
 *
 * Proves the harness-backed M2 battery reproduces the ORIGINAL 24-leg battery
 * 24/24 — and that each leg passes for its ORIGINAL REASON, not merely with a
 * matching pass boolean. Three independent assertions per leg:
 *
 *   (1) id-set identical          — same 24 leg ids in both runs (incl. the "10" quirk).
 *   (2) pass booleans identical   — orig.pass === harness.pass === true for every id.
 *   (3) signals satisfy manifest  — each harness leg's structured `signals` match the
 *                                   per-id MANIFEST below (the discriminating observables
 *                                   that make the pass attributable to its exact reason —
 *                                   Rule 18 anti-hollow-green / Rule 19 honesty).
 *
 * The ORIGINAL battery (scripts/fincrime-m2-investigation-route-battery.ts) is the
 * equivalence target and is NEVER edited — it is spawned read-only and its stdout
 * parsed for id+pass. The harness battery is spawned with PROOF_JSON_OUT and its JSON
 * read for id+pass+signals. Both batteries clean up their own synthetic rows; they use
 * distinct seed prefixes + rotated IPs and are run sequentially so they never collide.
 *
 * Exit 0 iff all three assertions hold for all 24 legs; otherwise exit 1 with the
 * specific divergences printed.
 */
import { spawn } from "node:child_process";
import { mkdirSync, readFileSync } from "node:fs";
import path from "node:path";

const ROOT = process.cwd();
const ORIGINAL = "scripts/fincrime-m2-investigation-route-battery.ts";
const HARNESS = "scripts/fincrime-m2-investigation-route-battery-harness.ts";
const HARNESS_JSON = "scripts/.artifacts/equiv-harness-results.json";

/** The 24 recorded leg ids — must reproduce verbatim, incl. the id="10" no-silent-close quirk. */
const CANONICAL_IDS = [
  "1a", "1b", "1c", "1d", "2a", "2b", "2d", "3", "4a", "4b", "5a", "5b",
  "6a", "6b", "6c", "7", "8", "9a", "9b", "9c", "11a", "11b", "12", "10",
] as const;

// ── per-id equivalence manifest — the "same reason" predicates ─────────────────
type Sig = Record<string, unknown>;
type Check = (s: Sig) => string[];

const eq = (s: Sig, k: string, v: unknown): string[] =>
  JSON.stringify(s[k]) === JSON.stringify(v) ? [] : [`${k}=${JSON.stringify(s[k])} expected ${JSON.stringify(v)}`];
const isTrue = (s: Sig, k: string): string[] =>
  s[k] === true ? [] : [`${k} expected true (got ${JSON.stringify(s[k])})`];
const ge = (s: Sig, k: string, n: number): string[] =>
  typeof s[k] === "number" && (s[k] as number) >= n ? [] : [`${k}=${JSON.stringify(s[k])} expected >=${n}`];
const all = (...cs: string[][]): string[] => cs.flat();

/**
 * Each entry lists the discriminating signals that make that leg's pass attributable
 * to its ORIGINAL reason. Values that are scheduling-dependent but still legal (e.g.
 * leg 12's win/loss split) are asserted via an invariant, not pinned to one outcome.
 */
const MANIFEST: Record<string, Check> = {
  // assign OPEN→UNDER_INVESTIGATION (action-derived transition + event + audit)
  "1a": (s) => all(
    eq(s, "httpStatus", 200), eq(s, "durableState", "UNDER_INVESTIGATION"), isTrue(s, "assigneeMatches"),
    isTrue(s, "dispositionNull"), isTrue(s, "dispositionReasonNull"), isTrue(s, "dispositionedAtNull"),
    isTrue(s, "strFiledFalse"), eq(s, "caseAssignedEvents", 1), eq(s, "fromState", "OPEN"),
    eq(s, "toState", "UNDER_INVESTIGATION"), isTrue(s, "payloadHash64hex"), isTrue(s, "auditFkPresent"),
    isTrue(s, "attemptAuditsAtLeast1")),
  // RBAC deny — auditor cannot assign (403, no mutation)
  "1b": (s) => all(eq(s, "httpStatus", 403), eq(s, "durableState", "OPEN"), eq(s, "events", 0)),
  // unauthenticated deny (401, no mutation)
  "1c": (s) => all(eq(s, "httpStatus", 401), isTrue(s, "rejectedUnauth"), eq(s, "durableState", "OPEN")),
  // start + first encrypted INVESTIGATION_NOTE evidence; raw note never at-rest
  "1d": (s) => all(
    eq(s, "httpStatus", 200), eq(s, "respState", "UNDER_INVESTIGATION"), isTrue(s, "evidenceIdString"),
    eq(s, "durableState", "UNDER_INVESTIGATION"), eq(s, "startedEvents", 1), eq(s, "fromState", "OPEN"),
    eq(s, "toState", "UNDER_INVESTIGATION"), eq(s, "evidenceAddedEvents", 1), eq(s, "evidenceRows", 1),
    eq(s, "evidenceType", "INVESTIGATION_NOTE"), isTrue(s, "encryptedNoteSet"), isTrue(s, "rawNoteAbsentInEvidence"),
    isTrue(s, "payloadHash64hex"), isTrue(s, "auditFkPresent"), isTrue(s, "attemptAuditsAtLeast1"),
    eq(s, "leakAny", false)),
  // transition target derived from action — payload cannot smuggle state
  "2a": (s) => all(
    eq(s, "redStatus", 400), eq(s, "midState", "OPEN"), eq(s, "greenStatus", 200),
    eq(s, "durableState", "UNDER_INVESTIGATION"), isTrue(s, "dispositionNull")),
  // start strict-DTO fence + evidence strict-DTO fence; only clean bodies land
  "2b": (s) => all(
    isTrue(s, "startFencedAll400"), eq(s, "startFencedStatuses", [400, 400, 400, 400, 400]),
    isTrue(s, "midStateOpen"), eq(s, "cleanStartStatus", 200), eq(s, "durableStartState", "UNDER_INVESTIGATION"),
    eq(s, "evidenceRedStatus", 400), eq(s, "evidenceGreenStatus", 201), eq(s, "evidenceRows", 1)),
  // escalate cannot smuggle a disposition (400, disposition stays NULL)
  "2d": (s) => all(eq(s, "redStatus", 400), eq(s, "durableState", "UNDER_INVESTIGATION"), isTrue(s, "dispositionNull")),
  // M3-FENCE post-M3 refresh: 4 non-STR disposal verbs ABSENT (404); the shipped STR route is
  // reachable but (a) DTO-rejects a malformed body (400, AEGIS_ERR_100/fincrime_str_prepare) AND
  // (b) STATE-rejects a WELL-FORMED M2-context disposal (409, AEGIS_ERR_104/state_conflict — the
  // load-bearing two-eyes/state fence, not merely the schema); paired controls: zero STR rows +
  // rejected narrative not persisted; owner read-back proves no disposition (str_filed false);
  // real M2 route reaches handler (409)
  "3": (s) => all(
    isTrue(s, "nonStrDisposeStatuses404"), eq(s, "strStatus", 400), isTrue(s, "strRejectedByPrepareValidation"),
    eq(s, "strWellFormedStatus", 409), isTrue(s, "strWellFormedStateConflict"),
    isTrue(s, "zeroStrReports"), isTrue(s, "rejectedNarrativeNotPersisted"),
    isTrue(s, "noDispositionMutation"), isTrue(s, "strFiledFalse"), eq(s, "realRouteStatus", 409),
    isTrue(s, "realRouteNon404")),
  // escalate→PENDING_MLCO_REVIEW terminal; encrypted summary; no disposition; no leak
  "4a": (s) => all(
    eq(s, "httpStatus", 200), eq(s, "respState", "PENDING_MLCO_REVIEW"), isTrue(s, "evidenceIdString"),
    eq(s, "durableState", "PENDING_MLCO_REVIEW"), isTrue(s, "dispositionNull"), eq(s, "escalatedEvents", 1),
    eq(s, "fromState", "UNDER_INVESTIGATION"), eq(s, "toState", "PENDING_MLCO_REVIEW"), eq(s, "noteEvidence", 1),
    isTrue(s, "encryptedNoteSet"), isTrue(s, "rawSummaryAbsent"), isTrue(s, "attemptAuditsAtLeast1"),
    eq(s, "leakAny", false)),
  // M3-fence terminal — every onward M2 action 409, state/disposition unchanged
  "4b": (s) => all(
    eq(s, "assignStatus", 409), eq(s, "startStatus", 409), eq(s, "escalateStatus", 409),
    eq(s, "evidenceStatus", 409), eq(s, "durableState", "PENDING_MLCO_REVIEW"), isTrue(s, "dispositionNull"),
    isTrue(s, "evidenceUnchanged")),
  // opaque-only evidence add (201, no state change)
  "5a": (s) => all(
    eq(s, "httpStatus", 201), isTrue(s, "evidenceIdString"), eq(s, "durableState", "OPEN"),
    eq(s, "evidenceRows", 1), eq(s, "evidenceType", "TRANSACTION_REF"), isTrue(s, "opaqueRefMatches"),
    isTrue(s, "encryptedNoteNull"), isTrue(s, "auditFkPresent"), eq(s, "evidenceAddedEvents", 1),
    isTrue(s, "attemptAuditsAtLeast1")),
  // malformed evidence rejected (no content / bad type / raw-PII ref) — all 400
  "5b": (s) => all(eq(s, "noContentStatus", 400), eq(s, "badTypeStatus", 400), eq(s, "piiRefStatus", 400), eq(s, "evidenceRows", 1)),
  // tenant-from-session: cross-tenant assign 409; B untouched; RLS-isolated
  "6a": (s) => all(
    eq(s, "denyStatus", 409), eq(s, "bDurableState", "OPEN"), eq(s, "bEvents", 0), eq(s, "controlStatus", 200),
    eq(s, "controlDurableState", "UNDER_INVESTIGATION"), eq(s, "rlsVisibleA", 0), eq(s, "rlsVisibleB", 1)),
  // cross-tenant evidence add 404; zero rows on the B case
  "6b": (s) => all(eq(s, "httpStatus", 404), eq(s, "bEvidenceRows", 0)),
  // payload-asserted tenant rejected (camel + snake) 400; case unchanged
  "6c": (s) => all(eq(s, "camelStatus", 400), eq(s, "snakeStatus", 400), eq(s, "durableState", "OPEN")),
  // assignee no-oracle — valid 200; non-existent/wrong-role/cross-tenant ALL identical 400
  "7": (s) => all(
    eq(s, "validStatus", 200), eq(s, "validDurableState", "UNDER_INVESTIGATION"), isTrue(s, "validAssigneeMatches"),
    eq(s, "badStatuses", [400, 400, 400]), isTrue(s, "badAll400"), isTrue(s, "errorShapeIdentical")),
  // concurrent assign — exactly one wins (CAS): statuses [200,409], one event, two attempts
  "8": (s) => all(
    eq(s, "statusesSorted", [200, 409]), isTrue(s, "oneWonOne409"), eq(s, "durableState", "UNDER_INVESTIGATION"),
    eq(s, "caseAssignedEvents", 1), eq(s, "attemptAudits", 2)),
  // queue read — array, returns ours, disposition field omitted from DTO
  "9a": (s) => all(eq(s, "httpStatus", 200), isTrue(s, "casesIsArray"), isTrue(s, "returnedOursGt0"), isTrue(s, "dispositionOmitted")),
  // closed-enum queue selector — unknown 400, valid 200
  "9b": (s) => all(eq(s, "badStatus", 400), eq(s, "goodStatus", 200)),
  // queue segregation by state/assignee
  "9c": (s) => all(
    eq(s, "openStatus", 200), eq(s, "pendingStatus", 200), eq(s, "mineStatus", 200), isTrue(s, "openAllOpen"),
    isTrue(s, "pendingHasC4AndAllPending"), isTrue(s, "mineAllRmAndHasC1")),
  // TOCTOU race (denial) — test-valid, blocked on row lock, 409 on terminal, zero rows
  "11a": (s) => all(
    isTrue(s, "validTest"), isTrue(s, "blockedOnRowLock"), eq(s, "evidenceStatus", 409), eq(s, "docRefRows", 0),
    eq(s, "durableState", "PENDING_MLCO_REVIEW")),
  // TOCTOU race (positive) — test-valid, blocked then 201, exactly one row, non-terminal
  "11b": (s) => all(
    isTrue(s, "validTest"), isTrue(s, "blockedOnRowLock"), eq(s, "evidenceStatus", 201), eq(s, "docRefRows", 1),
    eq(s, "durableState", "UNDER_INVESTIGATION")),
  // real-route race ×8 — every iteration a legal shape; sum invariant (split is scheduling-legal)
  "12": (s) => {
    const reasons = all(ge(s, "iterations", 1), isTrue(s, "allLegalShapes"), ge(s, "serializedBefore201", 0), ge(s, "lostToEscalate409", 0));
    const it = s.iterations as number, a = s.serializedBefore201 as number, b = s.lostToEscalate409 as number;
    if (!(typeof it === "number" && a + b === it)) reasons.push(`serializedBefore201(${a})+lostToEscalate409(${b}) != iterations(${it})`);
    return reasons;
  },
  // M3-fence global — ZERO dispositioned cases / disposition fields across all touched
  "10": (s) => all(eq(s, "dispositionedCases", 0), eq(s, "casesWithAnyDispositionField", 0), ge(s, "totalTouched", 1)),
};

// ── battery runners + parsers ─────────────────────────────────────────────────
interface OrigLeg { id: string; pass: boolean; }

function runBattery(script: string, extraEnv: Record<string, string> = {}): Promise<{ code: number; stdout: string }> {
  return new Promise((resolve) => {
    const child = spawn("npx", ["tsx", script], { cwd: ROOT, env: { ...process.env, ...extraEnv } });
    let out = "";
    child.stdout.on("data", (d: Buffer) => { const s = d.toString(); out += s; process.stdout.write(s); });
    child.stderr.on("data", (d: Buffer) => process.stderr.write(d));
    child.on("close", (code) => resolve({ code: code ?? -1, stdout: out }));
  });
}

/** Parse the original battery's stdout: [id] scenario … then VERDICT : PASS …/FAIL. */
function parseOriginal(stdout: string): OrigLeg[] {
  const legs: OrigLeg[] = [];
  let curId: string | null = null;
  for (const ln of stdout.split(/\r?\n/)) {
    const m = ln.match(/^\[(\d{1,2}[a-z]?)\]\s/);
    if (m) { curId = m[1]; continue; }
    const v = ln.match(/^\s*VERDICT\s*:\s*(.*)$/);
    if (v && curId) { legs.push({ id: curId, pass: /^PASS\b/.test(v[1].trim()) }); curId = null; }
  }
  return legs;
}

interface HarnessLeg { id: string; pass: boolean; signals: Sig; }
function readHarness(jsonPath: string): HarnessLeg[] {
  const j = JSON.parse(readFileSync(path.resolve(ROOT, jsonPath), "utf8")) as { results: HarnessLeg[] };
  return j.results;
}

const setEq = (a: string[], b: string[]): boolean => {
  const sa = new Set(a), sb = new Set(b);
  return sa.size === sb.size && [...sa].every((x) => sb.has(x));
};

async function main(): Promise<void> {
  mkdirSync(path.resolve(ROOT, "scripts/.artifacts"), { recursive: true });

  console.log("=".repeat(82));
  console.log("AEGIS SOAR — M2 harness proven-equivalence gate (AS/PLATFORM/2026/002 §2)");
  console.log("=".repeat(82));

  console.log("\n>>> [1/2] spawning ORIGINAL battery (equivalence target, read-only) …\n");
  const orig = await runBattery(ORIGINAL);
  const origLegs = parseOriginal(orig.stdout);

  console.log("\n>>> [2/2] spawning HARNESS battery (PROOF_JSON_OUT) …\n");
  const harn = await runBattery(HARNESS, { PROOF_JSON_OUT: HARNESS_JSON });
  const harnLegs = readHarness(HARNESS_JSON);

  const origIds = origLegs.map((l) => l.id);
  const harnIds = harnLegs.map((l) => l.id);
  const origById = new Map(origLegs.map((l) => [l.id, l]));
  const harnById = new Map(harnLegs.map((l) => [l.id, l]));

  const failures: string[] = [];

  // (1) id-set identical (both runs) and equal to the canonical 24
  if (!setEq(origIds, [...CANONICAL_IDS])) failures.push(`original id-set != canonical: got [${origIds.join(" ")}]`);
  if (!setEq(harnIds, [...CANONICAL_IDS])) failures.push(`harness id-set != canonical: got [${harnIds.join(" ")}]`);
  if (origIds.length !== 24) failures.push(`original leg count ${origIds.length} != 24`);
  if (harnIds.length !== 24) failures.push(`harness leg count ${harnIds.length} != 24`);

  console.log("\n" + "=".repeat(82));
  console.log("PER-LEG EQUIVALENCE  (id  orig  harness  reason-match)");
  console.log("-".repeat(82));
  for (const id of CANONICAL_IDS) {
    const o = origById.get(id);
    const h = harnById.get(id);
    const legFail: string[] = [];
    if (!o) legFail.push("absent in original");
    if (!h) legFail.push("absent in harness");
    // (2) pass booleans identical AND both true
    if (o && h && o.pass !== h.pass) legFail.push(`pass mismatch orig=${o.pass} harness=${h.pass}`);
    if (o && !o.pass) legFail.push("original FAILED");
    if (h && !h.pass) legFail.push("harness FAILED");
    // (3) harness signals satisfy the manifest (same-reason proof)
    let reasonMatch = "—";
    if (h) {
      const check = MANIFEST[id];
      if (!check) legFail.push("no manifest entry");
      else {
        const r = check(h.signals);
        reasonMatch = r.length === 0 ? "MATCH" : "MISMATCH";
        if (r.length) legFail.push(`signal manifest: ${r.join("; ")}`);
      }
    }
    const ok = legFail.length === 0;
    console.log(
      `${ok ? "PASS" : "FAIL"}  ${id.padEnd(4)} orig=${String(o?.pass ?? "—").padEnd(5)} harness=${String(h?.pass ?? "—").padEnd(5)} reason=${reasonMatch}`
      + (ok ? "" : `\n        ↳ ${legFail.join("\n        ↳ ")}`),
    );
    if (!ok) failures.push(`[${id}] ${legFail.join("; ")}`);
  }

  console.log("=".repeat(82));
  if (failures.length === 0) {
    console.log("EQUIVALENCE GATE: PASS — 24/24 legs reproduce id + pass + manifest-encoded ORIGINAL REASON.");
    console.log("(id-set + pass booleans are the original battery's independent contribution, parsed from its");
    console.log(" stdout; the 'same reason' proof is the per-id manifest of discriminating signals, not separate");
    console.log(" original-battery signal telemetry.) The harness battery is a proven-equivalent re-host of M2.");
    process.exit(0);
  }
  console.log(`EQUIVALENCE GATE: FAIL — ${failures.length} divergence(s):`);
  for (const f of failures) console.log(`  - ${f}`);
  process.exit(1);
}

main().catch((e) => {
  console.error("equivalence gate crashed:", e);
  process.exit(1);
});