// ============================================================================
// VF-RP02 — SOAR read-path cross-tenant isolation proof (F-RP-02, both tables)
// ----------------------------------------------------------------------------
// ref AS/AEGIS-CYBER/VERIFY/2026/001 | env: DEV | HOLD at publish gate
//
// WHAT THIS PROVES
//   F-RP-02 (HIGH): the SOAR read path served playbooks/executions from
//   process-global Maps, so the read path was NOT tenant-scoped. Operator
//   Option B made both tables per-tenant and DB-backed (mirror of the proven
//   PAM read-path fix), so the read path is now scoped by Postgres RLS (the
//   request-tx `app.current_tenant_id` GUC). This script proves that closure
//   end-to-end, ONE proof covering BOTH tables (soar_playbooks +
//   soar_executions), with paired POSITIVE/NEGATIVE legs, PLUS an execute-path
//   cross-tenant denial leg. The SOAR ACTION ENGINE itself is DEMO; only the
//   read-path tenant isolation is in scope here.
//
// WHY THIS SHAPE (non-hollow, per the standing rules)
//   • Driven as the least-privilege RLS-subject role `aegis_app` (NOT the owner,
//     which is BYPASSRLS → a hollow green). The owner pool is GROUND TRUTH ONLY
//     (proves the foreign-tenant 0 is RLS scoping, not row absence). [Rule 17/18]
//   • The seed and the POSITIVE read are driven through the REAL service methods
//     the HTTP routes call (soarPlaybook.createPlaybook / executePlaybook /
//     getPlaybooks / getPlaybook / getExecutions / getExecution), inside the
//     SAME request runtime the middleware builds: a pinned aegis_app client + a
//     real Drizzle tx + the LOCAL tenant GUC + the tenantContext ALS. So the
//     service's `db` proxy resolves to the aegis_app tx client exactly as in a
//     request. (The SOAR routes are role-gated; route auth gates WHO may call —
//     not WHICH tenant's rows are returned. The read-path leak is orthogonal to
//     auth and lives entirely in the service+RLS read path these calls exercise
//     verbatim.) [route-driven-proof-harness]
//   • Rule 18 (paired): every denial leg (foreign tenant sees 0 / cannot
//     execute) is paired with a positive-enforcement leg (owner tenant sees its
//     own row + a well-formed DTO / can execute), in the same run, so a green is
//     provably green for its EXACT reason.
//   • "0 is RLS, not a JS filter": getExecutions() applies NO tenant JS filter
//     (only playbookId/status/since/limit). The negative legs show the
//     service-method result and the raw aegis_app SELECT agree (both 0 under
//     GUC=B, both >=1 under GUC=A) — so the boundary is RLS, not app code.
//   • Non-colliding logical id: unlike the fixed seeded playbooks (PB-001..),
//     the seed here is a CUSTOM playbook with a unique logical id that tenant B
//     never seeds, so the foreign-tenant read AND execute legs are clean denials
//     (undefined / not-found), not a same-logical-id collision.
//
// CLEANUP: all rows for the two synthetic run-scoped tenants are deleted across
//   both tables + the child soar_action_results (owner pool, child-first). The
//   immutable audit-chain rows are left in place (synthetic, opaque, no PII) —
//   same precedent as vf-rp01.
// ============================================================================

import { sql } from "drizzle-orm";
import { appPool, tenantContext, makeClientRunner, type DrizzleDb } from "../server/db";
import {
  soarPlaybook,
  type Playbook,
  type PlaybookExecution,
} from "../server/lib/soar-playbook";
import {
  rlsPairedProbe,
  ownerCount,
  ownerQuery,
  endOwnerPool,
  verdict,
  ProofRun,
  type RlsPairedProbeResult,
} from "./lib/proof-harness";

const base = Date.now();
const TENANT_A = `rp02-a-${base}`; // owner tenant — seeds + reads its own rows
const TENANT_B = `rp02-b-${base}`; // foreign tenant — must see/execute NONE of A's

const captured = {
  logicalPbId: "",
  physPbId: "",
  execId: "",
};

/** FAITHFUL request runtime (the committing variant): a pinned aegis_app client
 *  + a real Drizzle tx + the LOCAL tenant GUC, with the PgTransaction stashed in
 *  the same AsyncLocalStorage the middleware uses, so the service's `db` proxy +
 *  any nested db.transaction() resolve to THIS connection under RLS — the exact
 *  production mechanism. */
async function runRequestPhaseTx(
  tenantId: string,
  fn: (tx: DrizzleDb) => Promise<void>,
): Promise<"COMMIT" | "ROLLBACK"> {
  const client = await appPool.connect();
  try {
    const tdb = makeClientRunner(client);
    try {
      await tdb.transaction(async (tx) => {
        await tx.execute(
          sql`SELECT set_config('app.current_tenant_id', ${tenantId}, true)`,
        );
        await tenantContext.run(
          { runner: tx as unknown as DrizzleDb, tenantId },
          () => fn(tx as unknown as DrizzleDb),
        );
      });
      return "COMMIT";
    } catch (e) {
      console.error(`  [phase ${tenantId}] error:`, (e as Error)?.message ?? e);
      throw e;
    }
  } finally {
    client.release();
  }
}

const run = new ProofRun(
  "AS/CYBER/READPATH-FIX/SOAR — F-RP-02 read-path cross-tenant proof (playbooks + executions + execute-path)",
  "DEV",
);

/** Build the per-table paired-probe leg (POSITIVE owner-visible + NEGATIVE
 *  foreign-denied + ground-truth ownerExists), all as aegis_app under RLS. */
function probeLeg(id: string, label: string, p: RlsPairedProbeResult) {
  run.leg({
    id,
    scenario: `${label} — RLS paired probe as aegis_app (owner=${p.ownerTenant}, foreign=${p.foreignTenant})`,
    expectation:
      "row PHYSICALLY EXISTS (owner/BYPASSRLS) AND owner-tenant SEES it (count=1) AND foreign-tenant DENIED (count=0)",
    observed: `ownerExists=${p.ownerExists} ownerVisible=${p.ownerVisibleCount} foreignVisible=${p.foreignVisibleCount}`,
    verdict: p.pass
      ? verdict.verified(
          "aegis_app RLS-subject read: owner sees its own row, foreign tenant sees 0 of a row proven to exist",
        )
      : verdict.fail(),
    pass: p.pass,
    signals: {
      table: p.table,
      id: p.id,
      ownerExists: p.ownerExists,
      ownerVisibleCount: p.ownerVisibleCount,
      foreignVisibleCount: p.foreignVisibleCount,
    },
  });
}

async function cleanup() {
  // child first: soar_action_results has no tenant_id — delete by execution_id of
  // any A/B execution, then the tenant-scoped parents.
  const execRows = await ownerQuery<{ id: string }>(
    `SELECT id FROM soar_executions WHERE tenant_id = $1 OR tenant_id = $2`,
    [TENANT_A, TENANT_B],
  );
  const execIds = execRows.map((r) => r.id);
  if (execIds.length) {
    await ownerQuery(
      `DELETE FROM soar_action_results WHERE execution_id = ANY($1::varchar[])`,
      [execIds],
    );
  }
  await ownerQuery(
    `DELETE FROM soar_executions WHERE tenant_id = $1 OR tenant_id = $2`,
    [TENANT_A, TENANT_B],
  );
  await ownerQuery(
    `DELETE FROM soar_playbooks WHERE tenant_id = $1 OR tenant_id = $2`,
    [TENANT_A, TENANT_B],
  );
}

async function main() {
  console.log("=".repeat(82));
  console.log(
    "VF-RP02 — SOAR read-path cross-tenant isolation proof (F-RP-02, both tables)",
  );
  console.log(
    "ref AS/AEGIS-CYBER/VERIFY/2026/001 | env: DEV |",
    new Date().toISOString(),
  );
  console.log(`tenant A (owner)=${TENANT_A}  tenant B (foreign)=${TENANT_B}`);
  console.log("=".repeat(82));

  await cleanup(); // idempotent pre-clean

  // ── PHASE 1 — SEED tenant-A via the REAL service path ────────────────────────
  // Tx1: createPlaybook(A) writes a CUSTOM playbook (unique logical id B never
  // seeds) to A's per-tenant soar_playbooks (commits).
  let seedPb: Playbook | undefined;
  await runRequestPhaseTx(TENANT_A, async () => {
    seedPb = await soarPlaybook.createPlaybook(
      {
        name: "RP02 Custom Playbook",
        description: "F-RP-02 read+execute-path cross-tenant proof seed",
        trigger: "manual",
        enabled: true,
        priority: 5,
        actions: [
          {
            id: "rp02-act-1",
            type: "send_alert",
            name: "RP02 Notify",
            params: { channel: "test", severity: "low" },
            order: 1,
          },
        ],
      },
      { tenantId: TENANT_A },
    );
  });
  if (!seedPb) {
    console.error("FATAL: createPlaybook(A) returned no playbook — cannot proceed");
    await cleanup();
    await endOwnerPool();
    await appPool.end();
    process.exit(1);
  }
  captured.logicalPbId = seedPb.id;
  captured.physPbId = `${TENANT_A}::${seedPb.id}`;

  // Tx2: executePlaybook(A) persists a 'running' soar_executions row for A
  // (commits). Same real path the routes drive; the detached completion then
  // re-enters via withTenantRls(captured) — proven separately by the architect.
  await runRequestPhaseTx(TENANT_A, async () => {
    const exec = await soarPlaybook.executePlaybook(
      captured.logicalPbId,
      "rp02-trigger",
      { trigger: "manual", proof: "F-RP-02" },
      { tenantId: TENANT_A },
    );
    captured.execId = exec.id;
  });

  if (!captured.execId) {
    console.error("FATAL: executePlaybook(A) produced no execution id");
    await cleanup();
    await endOwnerPool();
    await appPool.end();
    process.exit(1);
  }

  // Let the detached runPlaybookAsync(A) completion settle (single quick action)
  // so cleanup later does not race a late onConflict re-insert.
  await new Promise((r) => setTimeout(r, 3000));

  console.log("");
  console.log(
    `seeded: playbook(phys)=${captured.physPbId}  execution=${captured.execId}`,
  );

  // ── PHASE 2 — SUBSTRATE: per-table paired RLS probe (both tables) ────────────
  const pPb = await rlsPairedProbe(
    "soar_playbooks",
    captured.physPbId,
    TENANT_A,
    TENANT_B,
  );
  const pExec = await rlsPairedProbe(
    "soar_executions",
    captured.execId,
    TENANT_A,
    TENANT_B,
  );
  probeLeg("RP-PB", "soar_playbooks", pPb);
  probeLeg("RP-EXEC", "soar_executions", pExec);

  // ── PHASE 3 — PROVE-THROUGH-ROUTE: real service read methods, paired A vs B ──
  // POSITIVE (tenant A, as aegis_app): the exact methods the routes call return
  // A's rows with WELL-FORMED DTOs (mapper ran; logical id, not physical).
  let svcAPb: Playbook | undefined;
  let svcAPbList: Playbook[] = [];
  let svcAPhysLeak = false;
  let svcAExec: PlaybookExecution | undefined;
  let svcAExecIds: string[] = [];
  await runRequestPhaseTx(TENANT_A, async () => {
    svcAPbList = await soarPlaybook.getPlaybooks({ tenantId: TENANT_A });
    svcAPb = await soarPlaybook.getPlaybook(captured.logicalPbId, {
      tenantId: TENANT_A,
    });
    svcAPhysLeak = svcAPbList.some((p) => p.id === captured.physPbId); // DTO must use LOGICAL id
    svcAExec = await soarPlaybook.getExecution(captured.execId, {
      tenantId: TENANT_A,
    });
    svcAExecIds = (await soarPlaybook.getExecutions(undefined, { tenantId: TENANT_A })).map(
      (e) => e.id,
    );
  });

  // NEGATIVE (tenant B, as aegis_app): the same methods must return NONE of A's
  // rows. B's getPlaybooks seeds B's OWN default catalog (must not surface A's
  // custom playbook or execution).
  let svcBPbSeesA = false;
  let svcBPbById: Playbook | undefined;
  let svcBExecById: PlaybookExecution | undefined;
  let svcBExecSeesA = false;
  await runRequestPhaseTx(TENANT_B, async () => {
    const bList = await soarPlaybook.getPlaybooks({ tenantId: TENANT_B });
    svcBPbSeesA = bList.some((p) => p.id === captured.logicalPbId); // B never seeds this custom id
    svcBPbById = await soarPlaybook.getPlaybook(captured.logicalPbId, {
      tenantId: TENANT_B,
    });
    svcBExecById = await soarPlaybook.getExecution(captured.execId, {
      tenantId: TENANT_B,
    });
    svcBExecSeesA = (await soarPlaybook.getExecutions(undefined, { tenantId: TENANT_B })).some(
      (e) => e.id === captured.execId,
    );
  });

  // ground truth: A's rows physically still exist while B's service read sees 0.
  const aRowsPb = await ownerCount("soar_playbooks", "id = $1", [captured.physPbId]);
  const aRowsExec = await ownerCount("soar_executions", "tenant_id = $1", [TENANT_A]);

  // SVC-POS — A's service read returns A's rows with well-formed DTOs.
  const pbWellFormed =
    !!svcAPb &&
    svcAPb.id === captured.logicalPbId && // logical id (prefix stripped)
    typeof svcAPb.name === "string" &&
    svcAPb.name.length > 0 &&
    Array.isArray(svcAPb.actions) &&
    svcAPb.actions.length === 1 &&
    !svcAPhysLeak;
  const posPass =
    pbWellFormed &&
    svcAPbList.some((p) => p.id === captured.logicalPbId) &&
    !!svcAExec &&
    svcAExec.id === captured.execId &&
    svcAExecIds.includes(captured.execId);
  run.leg({
    id: "SVC-POS",
    scenario:
      "POSITIVE — tenant A drives getPlaybooks/getPlaybook/getExecution/getExecutions (real service path, aegis_app)",
    expectation:
      "A sees its own playbook (LOGICAL id, well-formed DTO, no physical-id leak) and its execution",
    observed:
      `pbWellFormed=${pbWellFormed} physIdLeak=${svcAPhysLeak} ` +
      `pbInList=${svcAPbList.some((p) => p.id === captured.logicalPbId)} ` +
      `execSeen=${!!svcAExec && svcAExec.id === captured.execId} execInList=${svcAExecIds.includes(captured.execId)}`,
    verdict: posPass
      ? verdict.verified(
          "the real route-backing read methods return A's own rows with correctly-mapped DTOs",
        )
      : verdict.fail(),
    pass: posPass,
    signals: {
      pbId: svcAPb?.id,
      pbName: svcAPb?.name,
      pbActions: svcAPb?.actions?.length,
      physIdLeak: svcAPhysLeak,
      execId: svcAExec?.id,
      execInList: svcAExecIds.includes(captured.execId),
    },
  });

  // SVC-NEG — B's service read returns NONE of A's rows, while A's rows are proven
  // to physically exist (so the 0 is RLS scoping, not absence) and the service
  // applies no tenant JS filter (so the 0 is RLS, not app code).
  const negPass =
    !svcBPbSeesA &&
    svcBPbById === undefined &&
    svcBExecById === undefined &&
    !svcBExecSeesA &&
    pPb.foreignVisibleCount === 0 &&
    pExec.foreignVisibleCount === 0 &&
    aRowsPb >= 1 &&
    aRowsExec >= 1;
  run.leg({
    id: "SVC-NEG",
    scenario:
      "NEGATIVE — tenant B drives the SAME service read methods (aegis_app, GUC=B)",
    expectation:
      "B sees 0 of A's playbook/execution via the real methods; A's rows still physically exist; raw aegis_app SELECT agrees (0) → RLS-caused, not a JS filter",
    observed:
      `B.pbSeesA=${svcBPbSeesA} B.pbById=${svcBPbById === undefined ? "undefined" : "FOUND"} ` +
      `B.execById=${svcBExecById === undefined ? "undefined" : "FOUND"} B.execSeesA=${svcBExecSeesA} ` +
      `rawForeignPb=${pPb.foreignVisibleCount} rawForeignExec=${pExec.foreignVisibleCount} ` +
      `A.physRows(pb/exec)=${aRowsPb}/${aRowsExec}`,
    verdict: negPass
      ? verdict.verified(
          "cross-tenant read CLOSED: foreign tenant's real service read returns none of A's rows; service result and raw aegis_app SELECT agree → boundary is RLS",
        )
      : verdict.fail(),
    pass: negPass,
    signals: {
      svcBPbSeesA,
      svcBPbByIdFound: svcBPbById !== undefined,
      svcBExecByIdFound: svcBExecById !== undefined,
      svcBExecSeesA,
      rawForeignPb: pPb.foreignVisibleCount,
      rawForeignExec: pExec.foreignVisibleCount,
      aPhysRowsPb: aRowsPb,
      aPhysRowsExec: aRowsExec,
    },
  });

  // ── PHASE 4 — EXECUTE-PATH cross-tenant denial (architect action #2) ─────────
  // POSITIVE: A executing its own custom logical id succeeded above (execId).
  // NEGATIVE: B executing A's custom logical id must THROW not-found — B's
  // gate-before-write getPlaybookByPhysicalId(`${B}::${logicalId}`) is undefined
  // (B never owns A's custom playbook), and NO soar_executions row is created for
  // B against this playbook.
  let bExecuteThrew = false;
  let bExecuteErr = "";
  try {
    await runRequestPhaseTx(TENANT_B, async () => {
      await soarPlaybook.executePlaybook(
        captured.logicalPbId,
        "rp02-foreign-trigger",
        { trigger: "manual", proof: "F-RP-02-xtenant-execute" },
        { tenantId: TENANT_B },
      );
    });
  } catch (e) {
    bExecuteThrew = true;
    bExecuteErr = (e as Error)?.message ?? String(e);
  }
  // ground truth: B created ZERO executions for A's custom logical playbook id.
  const bExecRowsForPb = await ownerCount(
    "soar_executions",
    "tenant_id = $1 AND playbook_id = $2",
    [TENANT_B, captured.logicalPbId],
  );
  const execNegPass = bExecuteThrew && bExecRowsForPb === 0;
  run.leg({
    id: "EXEC-NEG",
    scenario:
      "NEGATIVE — tenant B attempts executePlaybook on A's custom logical id (real service path, aegis_app)",
    expectation:
      "execute is REFUSED (throws not-found at the gate-before-write) AND no soar_executions row is created for B against A's playbook",
    observed: `threw=${bExecuteThrew} err="${bExecuteErr.slice(0, 80)}" bExecRowsForPb=${bExecRowsForPb}`,
    verdict: execNegPass
      ? verdict.verified(
          "execute-path cross-tenant CLOSED: foreign tenant cannot execute another tenant's playbook (gate-before-write refuses, no row written)",
        )
      : verdict.fail(),
    pass: execNegPass,
    signals: { bExecuteThrew, bExecuteErr, bExecRowsForPb },
  });

  // EXEC-POS (pair for Rule 18) — A's own execute produced exactly its own row.
  const aExecOwn = await ownerCount(
    "soar_executions",
    "id = $1 AND tenant_id = $2 AND playbook_id = $3",
    [captured.execId, TENANT_A, captured.logicalPbId],
  );
  const execPosPass = aExecOwn === 1;
  run.leg({
    id: "EXEC-POS",
    scenario:
      "POSITIVE — tenant A executed its own custom playbook (real service path, aegis_app)",
    expectation:
      "exactly one soar_executions row exists for (execId, tenant=A, playbook=A's custom logical id)",
    observed: `aExecOwnRows=${aExecOwn}`,
    verdict: execPosPass
      ? verdict.verified(
          "owner tenant's execute persisted exactly its own tenant-stamped execution row",
        )
      : verdict.fail(),
    pass: execPosPass,
    signals: { aExecOwn, execId: captured.execId },
  });

  // ── REPORT ───────────────────────────────────────────────────────────────────
  run.report();
  await run.writeJson();

  await cleanup();
  console.log(
    `\ncleanup: deleted all soar_playbooks/soar_executions/soar_action_results rows for ${TENANT_A} + ${TENANT_B} ` +
      `(audit-chain rows immutable by design — left in place).`,
  );

  const { allPass } = run.acceptance();
  await endOwnerPool();
  await appPool.end();
  if (!allPass) {
    console.error("\n❌ READ-PATH PROOF FAILED — see failing legs above.");
    process.exit(1);
  }
  console.log(
    "\n✅ F-RP-02 read-path + execute-path cross-tenant CLOSED for both SOAR tables (DEV, as aegis_app). HOLD at publish gate.",
  );
}

main().catch(async (err) => {
  console.error("FATAL:", err);
  try {
    await cleanup();
  } catch {}
  try {
    await endOwnerPool();
  } catch {}
  try {
    await appPool.end();
  } catch {}
  process.exit(1);
});