/**
 * AEGIS SOAR (AS/SOAR/2026/001) — M3 CHUNK 1 STR SCHEMA/CONTROL SUBSTRATE BATTERY.
 *
 * SCOPE FENCE (central negative discipline): chunk 1 is SCHEMA + DB-ENFORCED
 * CONTROLS ONLY. There is NO finalizer, NO disposing route, NO goAML/FIA submission,
 * NO STR state-machine here. This battery therefore proves the SUBSTRATE — the two
 * NEW fincrime-spine tables (fincrime_str_reports, fincrime_str_approvals) and the
 * DB constraints that make a forged FIA acknowledgement / a cross-tenant reference /
 * an under-retained STR STRUCTURALLY UNSTORABLE — and STOPS. It deliberately does
 * NOT (and cannot) drive an STR route, because none exists at this gate.
 *
 * These are NEW tables — NOT the legacy suspicious_activity_reports (the old
 * regulator-gateway SAR with the fabricated-acknowledgement lineage), which is not
 * reused.
 *
 * Proof moves (kit-driven — scripts/lib/{schema-probe,proof-harness}.ts):
 *   L1  STRUCTURAL SNAPSHOT + GOLDEN: pg_catalog facts (ordered conkey/confkey via
 *       pg_get_constraintdef — catches a TRANSPOSED composite FK a naive 2-col count
 *       passes). Writes the dev golden artifact for a future prod read-back diff and
 *       proves the snapshot is canonical/deterministic (re-snapshot diff == []).
 *   L2  COMPOSITE-FK CROSS-TENANT ORACLE (reports → cases), Rule 18 paired: a
 *       same-tenant reference SUCCEEDS (green); a reference to a NONEXISTENT case AND
 *       a reference to a REAL case in ANOTHER tenant BOTH fail with the IDENTICAL
 *       SQLSTATE 23503 + constraint fsr_case_fk — so "exists in another tenant" is
 *       indistinguishable from "does not exist": the existence oracle is closed.
 *       Run on the OWNER (BYPASSRLS) connection so the refusal is proven to be the FK
 *       itself, not RLS.
 *   L3  COMPOSITE-FK CROSS-TENANT ORACLE (approvals → reports): same shape on
 *       fsa_report_fk.
 *   L4  RLS POS/NEG as aegis_app (NOT owner), Rule 18 paired: a real tenant-A row is
 *       visible under withTenantRls(A)=1 and invisible under withTenantRls(B)=0, while
 *       the owner ground-truth count=1 proves B's 0 is RLS isolation, not absence.
 *   L5  CHECK RED-THEN-GREEN, Rule 18 paired: every forbidden row (the HEADLINE
 *       fsr_no_fabricated_ack forged-ack states; bad status; under-retention; past
 *       retention_until; bad approver role) is refused with its EXACT 23514 +
 *       constraint name, and the corresponding legitimate row is accepted — so each
 *       refusal is provably the named control, not a generally-broken insert.
 *   HEAL (separate phases, agent-orchestrated reboot between): drop a representative
 *       spread (CHECK + FK + index on reports; CHECK + unique-index on approvals),
 *       reboot so boot DDL M13/M14 re-runs, and confirm every dropped object is
 *       restored (effect-idempotent self-heal, Rule 16).
 *
 * Phases (env BATTERY_PHASE): "main" (default) runs L1–L5 + teardown; "heal-drop"
 * snapshots-present then drops the spread; "heal-verify" snapshots-restored after a
 * reboot. Between heal-drop and heal-verify the operator/agent restarts the workflow.
 *
 * Side-effect discipline: imports ONLY the kit (which imports withTenantRls + pg +
 * bcryptjs + node:crypto). Does NOT import server/index.ts or server/routes.ts (no
 * second boot). Synthetic str/approval/case rows are cleaned up in the main phase's
 * finally; these are direct-DB rows with NO audit-chain side effects, so teardown is
 * complete (no immutable rows are created by this battery).
 *
 * Rule 1: never prints a secret/connection value. The DB name is a topology
 * discriminator, not a secret, and is logged.
 */

import {
  ownerPool,
  ownerQuery,
  endOwnerPool,
  rlsCountById,
  labelledSyntheticRef,
  randomUUID,
  createHash,
  ProofRun,
  verdict,
  type LegResult,
} from "./lib/proof-harness";
import { snapshotTable, diffStructures, canonical, type TableStructure } from "./lib/schema-probe";
import { mkdir, writeFile, readFile } from "node:fs/promises";

const TENANT_A = "aegis-sovereign"; // real seeded dev tenant
const TENANT_B = "stanbic-ug-001"; // a DIFFERENT real seeded dev tenant
const base = Date.now();
const PHASE = (process.env.BATTERY_PHASE ?? "main").trim();
const GOLDEN_PATH = "scripts/proofs/fincrime-str-m3c1-golden.json";

const REPORTS = "fincrime_str_reports";
const APPROVALS = "fincrime_str_approvals";

const run = new ProofRun(`AEGIS SOAR M3 chunk 1 — STR substrate battery [phase=${PHASE}]`, "DEV");

// track synthetic rows for teardown (main phase)
const createdReportIds = new Set<string>();
const createdApprovalIds = new Set<string>();
const createdCaseIds = new Set<string>();

// ── insert helpers with error capture (owner = BYPASSRLS; FK/CHECK still enforced) ─
interface InsertOutcome {
  ok: boolean;
  id?: string;
  code?: string;
  constraint?: string;
  message?: string;
}
async function tryInsert(text: string, params: unknown[]): Promise<InsertOutcome> {
  try {
    const r = await ownerPool().query<{ id: string }>(text, params as unknown[]);
    return { ok: true, id: r.rows[0]?.id };
  } catch (e) {
    const err = e as { code?: string; constraint?: string; message?: string };
    return { ok: false, code: err.code, constraint: err.constraint, message: err.message };
  }
}

async function seedOpenCase(tenantId: string, tag: string): Promise<string> {
  const id = randomUUID();
  await ownerPool().query(
    `INSERT INTO fincrime_cases (id, tenant_id, source_type, source_ref, source_signal_hash, subject_ref)
     VALUES ($1, $2, 'MANUAL_REFERRAL', $3, $4, $5)`,
    [
      id,
      tenantId,
      `ext-m3c1-${tag}-${base}`,
      createHash("sha256").update(`m3c1-${tag}-${base}-${randomUUID()}`).digest("hex"),
      labelledSyntheticRef(`m3c1-case-${tag}-${base}`),
    ],
  );
  createdCaseIds.add(id);
  return id;
}

/** Build/execute an STR-report INSERT with per-column control. Defaults are a VALID
 *  PREPARED report (all filing columns NULL, 10-year future retention). */
interface StrOpts {
  tenantId: string;
  caseId: string;
  status?: string;
  fiaReference?: string | null;
  filedAt?: string | null; // SQL expression fragment or null
  acknowledgedAt?: string | null;
  retentionYears?: number;
  retentionUntilExpr?: string; // SQL expr; default NOW() + 10y
}
async function insertStr(o: StrOpts): Promise<InsertOutcome> {
  const id = randomUUID();
  const cols: string[] = ["id", "tenant_id", "case_id", "status", "subject_ref", "prepared_by_user_id", "prepared_by_role", "retention_years"];
  const vals: string[] = ["$1", "$2", "$3", "$4", "$5", "$6", "$7", "$8"];
  const params: unknown[] = [
    id,
    o.tenantId,
    o.caseId,
    o.status ?? "PREPARED",
    labelledSyntheticRef(`m3c1-str-${base}`),
    `opaque-user-${base}`,
    "risk_manager",
    o.retentionYears ?? 10,
  ];
  let p = 9;
  if (o.fiaReference !== undefined) {
    cols.push("fia_reference");
    vals.push(o.fiaReference === null ? "NULL" : `$${p++}`);
    if (o.fiaReference !== null) params.push(o.fiaReference);
  }
  // retention_until: explicit expr (default 10y future), never a bound param (it is an interval expr)
  cols.push("retention_until");
  vals.push(o.retentionUntilExpr ?? "NOW() + INTERVAL '10 years'");
  // filed_at / acknowledged_at are SQL expressions (NOW()) or omitted
  if (o.filedAt !== undefined && o.filedAt !== null) {
    cols.push("filed_at");
    vals.push(o.filedAt);
  }
  if (o.acknowledgedAt !== undefined && o.acknowledgedAt !== null) {
    cols.push("acknowledged_at");
    vals.push(o.acknowledgedAt);
  }
  const text = `INSERT INTO ${REPORTS} (${cols.join(", ")}) VALUES (${vals.join(", ")}) RETURNING id`;
  const out = await tryInsert(text, params);
  if (out.ok && out.id) createdReportIds.add(out.id);
  return out;
}

async function insertApproval(tenantId: string, strReportId: string, caseId: string, approverRole: string): Promise<InsertOutcome> {
  const id = randomUUID();
  const out = await tryInsert(
    `INSERT INTO ${APPROVALS} (id, tenant_id, str_report_id, case_id, approver_user_id, approver_role, report_hash)
     VALUES ($1, $2, $3, $4, $5, $6, $7) RETURNING id`,
    [
      id,
      tenantId,
      strReportId,
      caseId,
      `opaque-approver-${base}`,
      approverRole,
      createHash("sha256").update(`report:${strReportId}:${base}`).digest("hex"),
    ],
  );
  if (out.ok && out.id) createdApprovalIds.add(out.id);
  return out;
}

// ── leg recorders ─────────────────────────────────────────────────────────────
function legPass(id: string, scenario: string, expectation: string, observed: string, how: string): LegResult {
  return run.leg({ id, scenario, expectation, observed, verdict: verdict.verified(how), pass: true, signals: {} });
}
function legFromBool(
  id: string,
  scenario: string,
  expectation: string,
  observed: string,
  how: string,
  ok: boolean,
  signals: Record<string, unknown> = {},
): LegResult {
  return run.leg({
    id,
    scenario,
    expectation,
    observed,
    verdict: ok ? verdict.verified(how) : verdict.fail(),
    pass: ok,
    signals,
  });
}

// ── structural assertions over a snapshot ──────────────────────────────────────
function constraintDef(s: TableStructure, name: string): string | null {
  return s.constraints.find((c) => c.name === name)?.definition ?? null;
}
function hasIndex(s: TableStructure, name: string): boolean {
  return s.indexes.some((i) => i.name === name);
}
function col(s: TableStructure, name: string) {
  return s.columns.find((c) => c.name === name);
}

async function structuralLegs(): Promise<void> {
  const dbName = (await ownerQuery<{ d: string }>("SELECT current_database() AS d"))[0].d;
  console.log(`[topology] current_database=${dbName}`);

  const rep = await snapshotTable(ownerPool(), REPORTS);
  const app = await snapshotTable(ownerPool(), APPROVALS);
  if (!rep || !app) {
    legFromBool("L1.0", "both STR tables exist", "fincrime_str_reports + fincrime_str_approvals present", `reports=${!!rep} approvals=${!!app}`, "to_regclass via snapshotTable", false);
    return;
  }

  // column shape
  const tId = col(rep, "tenant_id");
  legFromBool("L1.1", "reports.tenant_id text NOT NULL", "type=text notNull=true", `type=${tId?.type} notNull=${tId?.notNull}`, "pg_attribute", tId?.type === "text" && tId?.notNull === true, { type: tId?.type, notNull: tId?.notNull });
  const enc = col(rep, "encrypted_narrative");
  legFromBool("L1.2", "reports.encrypted_narrative nullable (ciphertext, applied at chunk-2)", "notNull=false", `notNull=${enc?.notNull}`, "pg_attribute", enc !== undefined && enc.notNull === false, { notNull: enc?.notNull });
  const ru = col(rep, "retention_until");
  legFromBool("L1.3", "reports.retention_until NOT NULL", "notNull=true", `notNull=${ru?.notNull}`, "pg_attribute", ru?.notNull === true, { notNull: ru?.notNull });

  // the 4 report CHECKs present
  for (const [id, name] of [["L1.4", "fsr_status_valid"], ["L1.5", "fsr_no_fabricated_ack"], ["L1.6", "fsr_retention_min_years"], ["L1.7", "fsr_retention_future"]] as const) {
    const def = constraintDef(rep, name);
    legFromBool(id, `reports CHECK ${name} present`, "constraint present (contype=c)", def ? `present: ${def.slice(0, 60)}…` : "ABSENT", "pg_get_constraintdef", def !== null, { def });
  }

  // composite FK — ORDERED columns (transposition discriminator)
  const fsrFk = constraintDef(rep, "fsr_case_fk");
  const fsrFkOk = fsrFk !== null && fsrFk.replace(/\s+/g, " ").includes("FOREIGN KEY (tenant_id, case_id) REFERENCES fincrime_cases(tenant_id, id)");
  legFromBool("L1.8", "reports composite FK fsr_case_fk ORDERED (tenant_id,case_id)→fincrime_cases(tenant_id,id)", "exact ordered-column FK def (not transposed)", fsrFk ?? "ABSENT", "pg_get_constraintdef (encodes ordered conkey/confkey)", fsrFkOk, { def: fsrFk });

  const fsrUniq = constraintDef(rep, "fsr_tenant_id_uniq");
  const fsrUniqOk = fsrUniq !== null && fsrUniq.replace(/\s+/g, " ").includes("UNIQUE (tenant_id, id)");
  legFromBool("L1.9", "reports UNIQUE(tenant_id,id) fsr_tenant_id_uniq (approval-FK target)", "UNIQUE (tenant_id, id)", fsrUniq ?? "ABSENT", "pg_get_constraintdef", fsrUniqOk, { def: fsrUniq });

  for (const [id, name] of [["L1.10", "fsr_tenant_case_idx"], ["L1.11", "fsr_tenant_status_updated_idx"], ["L1.12", "fsr_tenant_retention_idx"]] as const) {
    legFromBool(id, `reports index ${name} present`, "index present", hasIndex(rep, name) ? "present" : "ABSENT", "pg_indexes", hasIndex(rep, name));
  }

  // approvals: CHECK + composite FK + unique index
  const fsaChk = constraintDef(app, "fsa_approver_role_valid");
  legFromBool("L1.13", "approvals CHECK fsa_approver_role_valid present", "constraint present", fsaChk ? `present: ${fsaChk.slice(0, 50)}…` : "ABSENT", "pg_get_constraintdef", fsaChk !== null, { def: fsaChk });
  const fsaFk = constraintDef(app, "fsa_report_fk");
  const fsaFkOk = fsaFk !== null && fsaFk.replace(/\s+/g, " ").includes("FOREIGN KEY (tenant_id, str_report_id) REFERENCES fincrime_str_reports(tenant_id, id)");
  legFromBool("L1.14", "approvals composite FK fsa_report_fk ORDERED (tenant_id,str_report_id)→reports(tenant_id,id)", "exact ordered-column FK def", fsaFk ?? "ABSENT", "pg_get_constraintdef", fsaFkOk, { def: fsaFk });
  legFromBool("L1.15", "approvals UNIQUE index fsa_tenant_report_uniq present (one approval per report)", "unique index present", hasIndex(app, "fsa_tenant_report_uniq") ? "present" : "ABSENT", "pg_indexes", hasIndex(app, "fsa_tenant_report_uniq"));

  // golden write + deterministic re-snapshot diff
  const snapshot = { reports: rep, approvals: app };
  await mkdir("scripts/proofs", { recursive: true });
  await writeFile(GOLDEN_PATH, canonical(snapshot));
  const golden = JSON.parse(await readFile(GOLDEN_PATH, "utf8")) as { reports: TableStructure; approvals: TableStructure };
  const rep2 = await snapshotTable(ownerPool(), REPORTS);
  const app2 = await snapshotTable(ownerPool(), APPROVALS);
  const diffs = [...diffStructures(golden.reports, rep2!), ...diffStructures(golden.approvals, app2!)];
  legFromBool("L1.16", "snapshot is canonical/deterministic vs the written dev golden", "diff == [] (golden artifact written for prod read-back)", diffs.length === 0 ? `identical; golden=${GOLDEN_PATH}` : `DIFFS: ${diffs.join(" | ")}`, "schema-probe diffStructures", diffs.length === 0, { goldenPath: GOLDEN_PATH });
}

// ── L2/L3: composite-FK cross-tenant existence-oracle (paired, Rule 18) ─────────
async function fkOracleLegs(caseA: string, caseB: string): Promise<{ strA: string | null; strB: string | null }> {
  // L2 reports → cases
  const pos = await insertStr({ tenantId: TENANT_A, caseId: caseA });
  legFromBool("L2.1", "reports FK POSITIVE: same-tenant case reference", "INSERT succeeds (FK satisfied)", pos.ok ? `ok id=${pos.id}` : `FAIL ${pos.code}/${pos.constraint}`, "owner INSERT (BYPASSRLS; FK enforced regardless)", pos.ok, { id: pos.id });
  const strA = pos.ok ? pos.id! : null;

  const neNon = await insertStr({ tenantId: TENANT_A, caseId: randomUUID() });
  const neCross = await insertStr({ tenantId: TENANT_A, caseId: caseB }); // real case, WRONG tenant
  const nonOk = !neNon.ok && neNon.code === "23503" && neNon.constraint === "fsr_case_fk";
  const crossOk = !neCross.ok && neCross.code === "23503" && neCross.constraint === "fsr_case_fk";
  const identical = nonOk && crossOk && neNon.code === neCross.code && neNon.constraint === neCross.constraint;
  legFromBool(
    "L2.2",
    "reports FK ORACLE: cross-tenant ref is INDISTINGUISHABLE from nonexistent",
    "both fail IDENTICAL 23503/fsr_case_fk (existence oracle closed)",
    `nonexistent=${neNon.code}/${neNon.constraint} cross-tenant=${neCross.code}/${neCross.constraint} identical=${identical}`,
    "owner INSERT — refusal is the composite FK, not RLS (owner BYPASSRLS)",
    identical,
    { nonexistent: { code: neNon.code, constraint: neNon.constraint }, crossTenant: { code: neCross.code, constraint: neCross.constraint } },
  );

  // L3 approvals → reports (needs a real report in each tenant)
  const posB = await insertStr({ tenantId: TENANT_B, caseId: caseB });
  const strB = posB.ok ? posB.id! : null;
  legFromBool("L3.0", "fixture: a real STR report in tenant B", "INSERT succeeds", posB.ok ? `ok id=${posB.id}` : `FAIL ${posB.code}`, "owner INSERT", posB.ok, { id: posB.id });

  if (strA && strB) {
    const aPos = await insertApproval(TENANT_A, strA, caseA, "risk_manager");
    legFromBool("L3.1", "approvals FK POSITIVE: same-tenant report reference", "INSERT succeeds", aPos.ok ? `ok id=${aPos.id}` : `FAIL ${aPos.code}/${aPos.constraint}`, "owner INSERT", aPos.ok, { id: aPos.id });
    const aNon = await insertApproval(TENANT_A, randomUUID(), caseA, "risk_manager");
    const aCross = await insertApproval(TENANT_A, strB, caseA, "risk_manager"); // real report, WRONG tenant
    const aNonOk = !aNon.ok && aNon.code === "23503" && aNon.constraint === "fsa_report_fk";
    const aCrossOk = !aCross.ok && aCross.code === "23503" && aCross.constraint === "fsa_report_fk";
    const aIdentical = aNonOk && aCrossOk && aNon.code === aCross.code && aNon.constraint === aCross.constraint;
    legFromBool(
      "L3.2",
      "approvals FK ORACLE: cross-tenant report ref INDISTINGUISHABLE from nonexistent",
      "both fail IDENTICAL 23503/fsa_report_fk",
      `nonexistent=${aNon.code}/${aNon.constraint} cross-tenant=${aCross.code}/${aCross.constraint} identical=${aIdentical}`,
      "owner INSERT — refusal is the composite FK, not RLS",
      aIdentical,
      { nonexistent: { code: aNon.code, constraint: aNon.constraint }, crossTenant: { code: aCross.code, constraint: aCross.constraint } },
    );
  }
  return { strA, strB };
}

// ── L4: RLS pos/neg as aegis_app (NOT owner), paired ────────────────────────────
async function rlsLegs(strA: string, apprA: string | null): Promise<void> {
  const aSee = await rlsCountById(TENANT_A, REPORTS, strA);
  const bSee = await rlsCountById(TENANT_B, REPORTS, strA);
  const ground = (await ownerQuery<{ n: number }>(`SELECT count(*)::int AS n FROM ${REPORTS} WHERE id=$1`, [strA]))[0].n;
  legFromBool(
    "L4.1",
    "reports RLS isolation (read as aegis_app): A sees its row, B does not",
    "withTenantRls(A)=1 AND withTenantRls(B)=0 AND owner ground-truth=1 (B's 0 is RLS, not absence)",
    `A=${aSee} B=${bSee} owner=${ground}`,
    "withTenantRls = aegis_app (non-superuser, non-BYPASSRLS) + tenant GUC",
    aSee === 1 && bSee === 0 && ground === 1,
    { a: aSee, b: bSee, owner: ground },
  );
  if (apprA) {
    const aSee2 = await rlsCountById(TENANT_A, APPROVALS, apprA);
    const bSee2 = await rlsCountById(TENANT_B, APPROVALS, apprA);
    const ground2 = (await ownerQuery<{ n: number }>(`SELECT count(*)::int AS n FROM ${APPROVALS} WHERE id=$1`, [apprA]))[0].n;
    legFromBool(
      "L4.2",
      "approvals RLS isolation (read as aegis_app): A sees its row, B does not",
      "withTenantRls(A)=1 AND withTenantRls(B)=0 AND owner=1",
      `A=${aSee2} B=${bSee2} owner=${ground2}`,
      "withTenantRls = aegis_app + tenant GUC",
      aSee2 === 1 && bSee2 === 0 && ground2 === 1,
      { a: aSee2, b: bSee2, owner: ground2 },
    );
  }
}

// ── L5: CHECK red-then-green (paired, Rule 18) ──────────────────────────────────
async function checkLegs(caseA: string, strA: string): Promise<void> {
  // fsr_no_fabricated_ack — HEADLINE forged-ack guard
  const redAck = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "PREPARED", acknowledgedAt: "NOW()" });
  legFromBool("L5.1", "HEADLINE: PREPARED + acknowledged_at REFUSED (no forged FIA ack)", "23514/fsr_no_fabricated_ack", `${redAck.code}/${redAck.constraint}`, "owner INSERT (CHECK always enforced)", !redAck.ok && redAck.code === "23514" && redAck.constraint === "fsr_no_fabricated_ack", { code: redAck.code, constraint: redAck.constraint });
  const redFia = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "PREPARED", fiaReference: "FIA-FORGED" });
  legFromBool("L5.2", "PREPARED + fia_reference REFUSED", "23514/fsr_no_fabricated_ack", `${redFia.code}/${redFia.constraint}`, "owner INSERT", !redFia.ok && redFia.code === "23514" && redFia.constraint === "fsr_no_fabricated_ack", { code: redFia.code, constraint: redFia.constraint });
  const redFiledNoRef = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "FILED", filedAt: "NOW()", fiaReference: null });
  legFromBool("L5.3", "FILED without fia_reference REFUSED", "23514/fsr_no_fabricated_ack", `${redFiledNoRef.code}/${redFiledNoRef.constraint}`, "owner INSERT", !redFiledNoRef.ok && redFiledNoRef.code === "23514" && redFiledNoRef.constraint === "fsr_no_fabricated_ack", { code: redFiledNoRef.code, constraint: redFiledNoRef.constraint });
  const redFiledAck = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "FILED", fiaReference: "FIA-1", filedAt: "NOW()", acknowledgedAt: "NOW()" });
  legFromBool("L5.4", "FILED + acknowledged_at REFUSED (ack requires ACKNOWLEDGED status)", "23514/fsr_no_fabricated_ack", `${redFiledAck.code}/${redFiledAck.constraint}`, "owner INSERT", !redFiledAck.ok && redFiledAck.code === "23514" && redFiledAck.constraint === "fsr_no_fabricated_ack", { code: redFiledAck.code, constraint: redFiledAck.constraint });

  const grnPrepared = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "PREPARED" });
  legFromBool("L5.5", "GREEN: PREPARED with all filing columns NULL ACCEPTED", "INSERT succeeds", grnPrepared.ok ? `ok id=${grnPrepared.id}` : `FAIL ${grnPrepared.code}/${grnPrepared.constraint}`, "owner INSERT", grnPrepared.ok, { id: grnPrepared.id });
  const grnFiled = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "FILED", fiaReference: "FIA-REAL-1", filedAt: "NOW()" });
  legFromBool("L5.6", "GREEN: FILED + fia_reference + filed_at (no ack) ACCEPTED", "INSERT succeeds", grnFiled.ok ? `ok id=${grnFiled.id}` : `FAIL ${grnFiled.code}/${grnFiled.constraint}`, "owner INSERT", grnFiled.ok, { id: grnFiled.id });
  const grnAck = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "ACKNOWLEDGED", fiaReference: "FIA-REAL-2", filedAt: "NOW()", acknowledgedAt: "NOW()" });
  legFromBool("L5.7", "GREEN: ACKNOWLEDGED + fia_reference + filed_at + acknowledged_at ACCEPTED", "INSERT succeeds", grnAck.ok ? `ok id=${grnAck.id}` : `FAIL ${grnAck.code}/${grnAck.constraint}`, "owner INSERT", grnAck.ok, { id: grnAck.id });

  // fsr_status_valid. NOTE: an unknown status violates BOTH status-domain guards —
  // fsr_status_valid (status IN ...) AND fsr_no_fabricated_ack (disjunctive form,
  // every branch enumerates a known status), so their valid-status sets are IDENTICAL
  // and a bogus status cannot be isolated to one constraint behaviorally. Postgres
  // reports whichever it evaluates first. This overlap is INTENTIONAL fail-closed
  // redundancy (Rule 16: existence ≠ correctness — if status_valid were ever dropped,
  // no_fabricated_ack still rejects an unknown status). fsr_status_valid's EXACT
  // predicate is pinned independently and structurally by L1.4.
  const redStatus = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "BOGUS" });
  const statusDomainGuards = ["fsr_status_valid", "fsr_no_fabricated_ack"];
  legFromBool("L5.8", "bad status REFUSED by a status-domain CHECK (status_valid/no_fabricated_ack overlap on unknown status — intentional fail-closed redundancy)", "23514 by fsr_status_valid OR fsr_no_fabricated_ack", `${redStatus.code}/${redStatus.constraint}`, "owner INSERT; exact status_valid predicate pinned structurally by L1.4", !redStatus.ok && redStatus.code === "23514" && statusDomainGuards.includes(redStatus.constraint ?? ""), { code: redStatus.code, constraint: redStatus.constraint, overlappingGuards: statusDomainGuards });
  const grnStatus = await insertStr({ tenantId: TENANT_A, caseId: caseA, status: "NOT_FILED" });
  legFromBool("L5.9", "GREEN: status NOT_FILED ACCEPTED", "INSERT succeeds", grnStatus.ok ? `ok id=${grnStatus.id}` : `FAIL ${grnStatus.code}/${grnStatus.constraint}`, "owner INSERT", grnStatus.ok, { id: grnStatus.id });

  // fsr_retention_min_years
  const redRet = await insertStr({ tenantId: TENANT_A, caseId: caseA, retentionYears: 9 });
  legFromBool("L5.10", "retention_years < 10 REFUSED", "23514/fsr_retention_min_years", `${redRet.code}/${redRet.constraint}`, "owner INSERT", !redRet.ok && redRet.code === "23514" && redRet.constraint === "fsr_retention_min_years", { code: redRet.code, constraint: redRet.constraint });
  const grnRet = await insertStr({ tenantId: TENANT_A, caseId: caseA, retentionYears: 10 });
  legFromBool("L5.11", "GREEN: retention_years = 10 ACCEPTED", "INSERT succeeds", grnRet.ok ? `ok id=${grnRet.id}` : `FAIL ${grnRet.code}/${grnRet.constraint}`, "owner INSERT", grnRet.ok, { id: grnRet.id });

  // fsr_retention_future (retention_until < created_at)
  const redFut = await insertStr({ tenantId: TENANT_A, caseId: caseA, retentionUntilExpr: "NOW() - INTERVAL '1 day'" });
  legFromBool("L5.12", "retention_until in the PAST REFUSED", "23514/fsr_retention_future", `${redFut.code}/${redFut.constraint}`, "owner INSERT", !redFut.ok && redFut.code === "23514" && redFut.constraint === "fsr_retention_future", { code: redFut.code, constraint: redFut.constraint });
  // green for retention_future already covered by every other accepted row (10y future).

  // fsa_approver_role_valid
  const redRole = await insertApproval(TENANT_A, strA, caseA, "auditor");
  legFromBool("L5.13", "approver_role 'auditor' REFUSED (risk_manager|admin only)", "23514/fsa_approver_role_valid", `${redRole.code}/${redRole.constraint}`, "owner INSERT", !redRole.ok && redRole.code === "23514" && redRole.constraint === "fsa_approver_role_valid", { code: redRole.code, constraint: redRole.constraint });
  // green approver-role accepted is covered by L3.1 (risk_manager). Add an admin positive too.
  const grnAdmin = await insertStr({ tenantId: TENANT_A, caseId: caseA });
  if (grnAdmin.ok && grnAdmin.id) {
    const grnRole = await insertApproval(TENANT_A, grnAdmin.id, caseA, "admin");
    legFromBool("L5.14", "GREEN: approver_role 'admin' ACCEPTED", "INSERT succeeds", grnRole.ok ? `ok id=${grnRole.id}` : `FAIL ${grnRole.code}/${grnRole.constraint}`, "owner INSERT", grnRole.ok, { id: grnRole.id });
  }
}

// ── teardown (main phase) — child→parent; no audit rows are created here ─────────
async function teardown(): Promise<void> {
  if (createdApprovalIds.size) await ownerPool().query(`DELETE FROM ${APPROVALS} WHERE id = ANY($1::varchar[])`, [Array.from(createdApprovalIds)]);
  if (createdReportIds.size) await ownerPool().query(`DELETE FROM ${REPORTS} WHERE id = ANY($1::varchar[])`, [Array.from(createdReportIds)]);
  if (createdCaseIds.size) await ownerPool().query(`DELETE FROM fincrime_cases WHERE id = ANY($1::varchar[])`, [Array.from(createdCaseIds)]);
}

// ── HEAL phases ─────────────────────────────────────────────────────────────────
const HEAL_TARGETS = {
  reportsConstraints: ["fsr_no_fabricated_ack", "fsr_case_fk"],
  reportsIndexes: ["fsr_tenant_case_idx"],
  approvalsConstraints: ["fsa_approver_role_valid"],
  approvalsIndexes: ["fsa_tenant_report_uniq"],
} as const;

async function healDrop(): Promise<void> {
  // confirm present FIRST (so the absence after-drop is meaningful)
  const repBefore = await snapshotTable(ownerPool(), REPORTS);
  const appBefore = await snapshotTable(ownerPool(), APPROVALS);
  const presentBefore =
    !!repBefore && !!appBefore &&
    HEAL_TARGETS.reportsConstraints.every((c) => constraintDef(repBefore, c) !== null) &&
    HEAL_TARGETS.reportsIndexes.every((i) => hasIndex(repBefore, i)) &&
    HEAL_TARGETS.approvalsConstraints.every((c) => constraintDef(appBefore, c) !== null) &&
    HEAL_TARGETS.approvalsIndexes.every((i) => hasIndex(appBefore, i));
  legFromBool("HEAL.1", "spread present BEFORE drop", "all heal targets present", presentBefore ? "present" : "NOT all present", "pg_catalog snapshot", presentBefore);

  for (const c of HEAL_TARGETS.reportsConstraints) await ownerPool().query(`ALTER TABLE ${REPORTS} DROP CONSTRAINT IF EXISTS ${c}`);
  for (const i of HEAL_TARGETS.reportsIndexes) await ownerPool().query(`DROP INDEX IF EXISTS ${i}`);
  for (const c of HEAL_TARGETS.approvalsConstraints) await ownerPool().query(`ALTER TABLE ${APPROVALS} DROP CONSTRAINT IF EXISTS ${c}`);
  for (const i of HEAL_TARGETS.approvalsIndexes) await ownerPool().query(`DROP INDEX IF EXISTS ${i}`);

  const repAfter = await snapshotTable(ownerPool(), REPORTS);
  const appAfter = await snapshotTable(ownerPool(), APPROVALS);
  const absentAfter =
    !!repAfter && !!appAfter &&
    HEAL_TARGETS.reportsConstraints.every((c) => constraintDef(repAfter, c) === null) &&
    HEAL_TARGETS.reportsIndexes.every((i) => !hasIndex(repAfter, i)) &&
    HEAL_TARGETS.approvalsConstraints.every((c) => constraintDef(appAfter, c) === null) &&
    HEAL_TARGETS.approvalsIndexes.every((i) => !hasIndex(appAfter, i));
  legFromBool("HEAL.2", "spread ABSENT after drop (RED — substrate intentionally broken)", "all heal targets dropped", absentAfter ? "absent" : "still present", "pg_catalog snapshot", absentAfter);
  console.log("\n>>> HEAL-DROP complete. RESTART the workflow now, then run BATTERY_PHASE=heal-verify.\n");
}

async function healVerify(): Promise<void> {
  const rep = await snapshotTable(ownerPool(), REPORTS);
  const app = await snapshotTable(ownerPool(), APPROVALS);
  const restored =
    !!rep && !!app &&
    HEAL_TARGETS.reportsConstraints.every((c) => constraintDef(rep, c) !== null) &&
    HEAL_TARGETS.reportsIndexes.every((i) => hasIndex(rep, i)) &&
    HEAL_TARGETS.approvalsConstraints.every((c) => constraintDef(app, c) !== null) &&
    HEAL_TARGETS.approvalsIndexes.every((i) => hasIndex(app, i));
  legFromBool("HEAL.3", "spread RESTORED after reboot (GREEN — effect-idempotent self-heal)", "all heal targets present again", restored ? "restored" : "NOT restored", "pg_catalog snapshot after boot DDL re-run", restored);
  // and the restored FK is the correct ORDERED composite, not a transposed re-create
  const fk = rep ? constraintDef(rep, "fsr_case_fk") : null;
  const ordered = fk !== null && fk.replace(/\s+/g, " ").includes("FOREIGN KEY (tenant_id, case_id) REFERENCES fincrime_cases(tenant_id, id)");
  legFromBool("HEAL.4", "restored fsr_case_fk is the ORDERED composite (not transposed on re-create)", "exact ordered-column FK def", fk ?? "ABSENT", "pg_get_constraintdef", ordered, { def: fk });

  // diff full snapshot against the golden from the main phase, if present
  try {
    const golden = JSON.parse(await readFile(GOLDEN_PATH, "utf8")) as { reports: TableStructure; approvals: TableStructure };
    const diffs = [...diffStructures(golden.reports, rep!), ...diffStructures(golden.approvals, app!)];
    legFromBool("HEAL.5", "post-reboot snapshot matches the dev golden byte-for-byte", "diff == []", diffs.length === 0 ? "identical to golden" : `DIFFS: ${diffs.join(" | ")}`, "schema-probe diffStructures vs golden", diffs.length === 0);
  } catch {
    console.log("[heal-verify] golden not found — run BATTERY_PHASE=main first to write it; skipping HEAL.5 diff.");
  }
}

async function main(): Promise<void> {
  if (PHASE === "heal-drop") {
    await healDrop();
  } else if (PHASE === "heal-verify") {
    await healVerify();
  } else {
    // main phase
    try {
      await structuralLegs();
      const caseA = await seedOpenCase(TENANT_A, "a");
      const caseB = await seedOpenCase(TENANT_B, "b");
      const { strA } = await fkOracleLegs(caseA, caseB);
      if (strA) {
        // a fresh approval in A for the RLS leg
        const apprA = await insertApproval(TENANT_A, strA, caseA, "risk_manager");
        await rlsLegs(strA, apprA.ok ? apprA.id! : null);
        await checkLegs(caseA, strA);
      } else {
        legFromBool("L2.1.guard", "no STR row created → cannot run RLS/CHECK legs", "strA present", "strA=null", "fixture", false);
      }
    } finally {
      await teardown();
    }
  }

  run.report();
  await run.writeJson(process.env.PROOF_JSON_OUT);
  const { allPass } = run.acceptance();
  await endOwnerPool();
  process.exit(allPass ? 0 : 1);
}

main().catch((e) => {
  console.error("BATTERY ERROR:", e);
  process.exit(1);
});