/**
 * rigor/zanzibar-semantics.test.js — js-rigor property tests for
 * Zanzibar-style authorization graph semantics.
 *
 * Zanzibar's core model (Google's global authorization system):
 * relation tuples (object, relation, user), usersets, and rewrite rules
 * (direct, tuple-to-userset, union, intersection, exclusion).
 *
 * Properties verified:
 *
 *   - UNION: a grant from ANY child grants at the child's possibility
 *     (max over children); no child grants → deny.
 *   - INTERSECTION: ALL children must grant; result is the min.
 *   - EXCLUSION (A AND NOT B): the denied set blocks the allowed set;
 *     p = pA * (1 - pB).
 *   - EXPAND PARITY (flagship): a brute-force reference implementation of
 *     Zanzibar's Expand RPC (userset expansion) is compared against
 *     arbiter.check() over RANDOM graphs with random rewrite configs —
 *     direct, chain (transitive member_of), tuple-to-userset, union and
 *     exclusion — with random edge possibilities including 0.
 *   - NESTED CHAIN: membership transitivity through N nested groups honors
 *     the weakest link (min possibility along the full path).
 *   - CYCLE SAFETY: cyclic membership graphs terminate and never create
 *     spurious access.
 */
import { describe, it } from 'node:test';
import assert from 'node:assert/strict';
import { rigor } from '@rigor/core';
import { Arbiter } from '../../src/index.js';

const EPS = 1e-9;
const POSSIBILITIES = [0, 0.25, 0.5, 0.75, 1];

function fail(message) {
  throw new Error(message);
}

/**
 * Reference implementation of Zanzibar's Expand RPC over a graph of
 * users / groups / one object, for the rewrite configs the engine supports.
 * Returns the possibility that `user` is in the userset of (object, rel).
 *
 * Semantics mirrored from the engine (verified empirically):
 *   - direct: only edges whose subject is the user itself (no implicit
 *     group expansion on direct tuples); possibility = edge possibility.
 *   - chain: transitive `member_of` traversal (min along path, max over
 *     paths), then a final edge of the terminal relation into the object.
 *   - tuple_to_userset: object's tuplesetRelation edges (doc → group),
 *     joined with a DIRECT computedRelation edge from the user; min.
 *   - union: max over children.  intersection: min over children.
 *   - exclusion: pA * (1 - pB).
 */
export function buildExpandOracle(graph, config) {
  const { memberOf, edgesByRelation } = graph;
  const edges = (rel) => edgesByRelation.get(rel) || [];

  function directUserset(rel) {
    return (userId) => {
      let best = 0;
      // direct edges point FROM the subject TO the object (src=subject, dst=object)
      for (const e of edges(rel)) {
        if (e.from === userId && e.subject === graph.objectId) {
          if (e.p > best) best = e.p;
        }
      }
      return best;
    };
  }

  function transitiveMembers(userId) {
    // BFS over member_of edges; min possibility along each path; max over paths.
    const best = new Map([[userId, 1]]);
    const queue = [userId];
    while (queue.length) {
      const node = queue.shift();
      const nodeP = best.get(node);
      for (const e of edges('member_of')) {
        if (e.from !== node) continue;
        const nextP = Math.min(nodeP, e.p);
        const prev = best.get(e.subject);
        if (prev === undefined || nextP > prev) {
          best.set(e.subject, nextP);
          queue.push(e.subject);
        }
      }
    }
    return best;
  }

  function reachAtExactHops(userId, hops) {
    // Nodes reachable in EXACTLY `hops` member_of traversals, with the
    // best (max) possibility per node. Mirrors the engine's per-step
    // path extension (paths always traverse every step).
    let frontier = new Map([[userId, 1]]);
    for (let h = 0; h < hops; h++) {
      const next = new Map();
      for (const [node, nodeP] of frontier) {
        for (const e of edges('member_of')) {
          if (e.from !== node) continue;
          const nextP = Math.min(nodeP, e.p);
          const prev = next.get(e.subject);
          if (prev === undefined || nextP > prev) {
            next.set(e.subject, nextP);
          }
        }
      }
      frontier = next;
      if (frontier.size === 0) break;
    }
    return frontier;
  }

  function evalRule(rule, userId) {
    if (rule.type === 'direct') {
      return directUserset(rule.relation)(userId);
    }
    if (rule.type === 'chain') {
      // steps: N member_of hops then a terminal relation into the object.
      // The engine extends paths through EVERY step, so the terminal edge
      // may only originate from nodes reachable in exactly N member_of hops
      // (the starting user alone never satisfies the chain).
      const steps = rule.steps;
      const terminal = steps[steps.length - 1].relation;
      const memberHops = steps.length - 1;
      let best = 0;
      if (memberHops > 0) {
        for (const [node, p] of reachAtExactHops(userId, memberHops)) {
          for (const e of edges(terminal)) {
            if (e.from === node && e.subject === graph.objectId) {
              const pathP = Math.min(p, e.p);
              if (pathP > best) best = pathP;
            }
          }
        }
      }
      return best;
    }
    if (rule.type === 'tuple_to_userset') {
      let best = 0;
      for (const t of edges(rule.tuplesetRelation)) {
        if (t.from !== graph.objectId) continue;
        // computed side is a DIRECT relation lookup (verified semantics)
        let memberP = 0;
        for (const m of edges(rule.computedRelation)) {
          if (m.from === userId && m.subject === t.subject) {
            if (m.p > memberP) memberP = m.p;
          }
        }
        const combined = Math.min(t.p, memberP);
        if (combined > best) best = combined;
      }
      return best;
    }
    if (rule.union) {
      return Math.max(0, ...rule.union.map((r) => evalRule(r, userId)));
    }
    if (rule.intersection) {
      return Math.min(...rule.intersection.map((r) => evalRule(r, userId)));
    }
    if (rule.exclusion) {
      const [a, b] = rule.exclusion;
      return evalRule(a, userId) * (1 - evalRule(b, userId));
    }
    return 0;
  }

  return { evalRule };
}

/**
 * Build a random Zanzibar-style graph + rewrite config, and the matching
 * Arbiter instance. Config shapes are chosen from a fixed family so the
 * oracle and the engine stay in sync by construction.
 */
export function buildRandomZanzibarCase(seedCase) {
  const { userCount, groupCount, configKind } = seedCase;
  const users = Array.from({ length: userCount }, (_, i) => `user:${i}`);
  const groups = Array.from({ length: groupCount }, (_, i) => `group:${i}`);
  const allSubjects = [...users, ...groups];
  const doc = 'doc:1';

  const arbiter = new Arbiter();
  for (const u of users) arbiter.addNode(u, 'user');
  for (const g of groups) arbiter.addNode(g, 'group');
  arbiter.addNode(doc, 'doc');
  arbiter.setRelationConfig('member_of', { type: 'direct' });

  const edgesByRelation = new Map();
  const addEdge = (rel, from, subject, p) => {
    let list = edgesByRelation.get(rel);
    if (!list) {
      list = [];
      edgesByRelation.set(rel, list);
    }
    // The engine dedups relations per (src, rel, dst) with last-write-wins
    // (addRelation updates an existing tuple). Mirror that so the oracle
    // and the engine observe identical edge data.
    const existing = list.find((e) => e.from === from && e.subject === subject);
    if (existing) {
      existing.p = p;
      arbiter.removeRelation(from, rel, subject);
    }
    list.push(existing || { from, subject, p });
    arbiter.addRelation(from, rel, subject, { possibility: p });
  };

  const pick = (arr) => arr[Math.floor(Math.random() * arr.length)];

  // member_of edges: users AND groups can be members (nesting), subjects can be groups
  const memberEdges = Math.max(1, Math.floor((userCount + groupCount) / 2));
  for (let i = 0; i < memberEdges; i++) {
    const from = pick(allSubjects);
    const subject = pick(groups);
    addEdge('member_of', from, subject, pick(POSSIBILITIES));
  }

  // Two direct relations (for union / exclusion / direct configs)
  const d1 = 'viewer_allowed';
  const d2 = 'viewer_staff';
  const denied = 'viewer_denied';
  for (const rel of [d1, d2, denied]) {
    arbiter.setRelationConfig(rel, { type: 'direct' });
  }
  const directEdgeCount = Math.max(1, Math.floor(userCount / 2) + 1);
  for (let i = 0; i < directEdgeCount; i++) {
    // direct edges point FROM the subject TO the object (src=subject, dst=doc)
    addEdge(pick([d1, d2]), pick(allSubjects), doc, pick(POSSIBILITIES));
    addEdge(denied, pick(allSubjects), doc, pick(POSSIBILITIES));
  }

  // Tupleset relation: doc → group (for tuple_to_userset)
  const t1 = 'owner';
  arbiter.setRelationConfig(t1, { type: 'direct' });
  if (groupCount > 0) {
    for (let i = 0; i < groupCount; i++) {
      addEdge(t1, doc, pick(groups), pick(POSSIBILITIES));
    }
  }

  const directRule = () => ({ type: 'direct', relation: pick([d1, d2]) });
  const chainRule = () => ({
    type: 'chain',
    steps: [
      { relation: 'member_of', direction: 'out' },
      { relation: 'member_of', direction: 'out' },
      { relation: pick([d1, d2]), direction: 'out' }
    ]
  });
  const ttuRule = () => ({
    type: 'tuple_to_userset',
    tuplesetRelation: t1,
    computedRelation: 'member_of',
    reverse: false
  });
  const allowRule = () => pick([directRule(), chainRule(), ttuRule()]);

  let config;
  if (configKind === 0) config = allowRule();
  else if (configKind === 1) config = { union: [allowRule(), allowRule()] };
  else if (configKind === 2) config = { intersection: [allowRule(), allowRule()] };
  else if (configKind === 3) config = { exclusion: [allowRule(), { type: 'direct', relation: denied }] };
  else config = { union: [allowRule(), { exclusion: [allowRule(), { type: 'direct', relation: denied }] }] };

  arbiter.setRelationConfig('viewer', config);
  return {
    arbiter,
    graph: {
      objectId: doc,
      memberOf: edgesByRelation.get('member_of') || [],
      edgesByRelation
    },
    config,
    users
  };
}

describe('Zanzibar rewrite-rule semantics (rigor)', () => {
  it('UNION: max over children — any grant grants, none denies', async () => {
    async function check({ pa, pb, hasA, hasB }) {
      const arbiter = new Arbiter();
      ['user:u', 'doc:1'].forEach((k) => arbiter.addNode(k, k.startsWith('user') ? 'user' : 'doc'));
      arbiter.setRelationConfig('rel_a', { type: 'direct' });
      arbiter.setRelationConfig('rel_b', { type: 'direct' });
      arbiter.setRelationConfig('viewer', {
        union: [
          { type: 'direct', relation: 'rel_a' },
          { type: 'direct', relation: 'rel_b' }
        ]
      });
      if (hasA) arbiter.addRelation('user:u', 'rel_a', 'doc:1', { possibility: pa });
      if (hasB) arbiter.addRelation('user:u', 'rel_b', 'doc:1', { possibility: pb });

      const result = arbiter.check('user:u', 'viewer', 'doc:1');
      const expected = Math.max(hasA ? pa : 0, hasB ? pb : 0);
      if (Math.abs(result.possibility - expected) > EPS) {
        fail(`union: expected ${expected}, got ${result.possibility}`);
      }
      return result;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            pa: rigor.gen.oneOf(POSSIBILITIES),
            pb: rigor.gen.oneOf(POSSIBILITIES),
            hasA: rigor.gen.boolean(),
            hasB: rigor.gen.boolean()
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('union-max', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 400, seed: 'zanzibar-union' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'union-max');
    assert.ok(inv);
    assert.equal(inv.passed, true, `UNION contract violated in ${inv.failureCount} cases`);
  });

  it('INTERSECTION: min over children — all must grant', async () => {
    async function check({ pa, pb, hasA, hasB }) {
      const arbiter = new Arbiter();
      ['user:u', 'doc:1'].forEach((k) => arbiter.addNode(k, k.startsWith('user') ? 'user' : 'doc'));
      arbiter.setRelationConfig('rel_a', { type: 'direct' });
      arbiter.setRelationConfig('rel_b', { type: 'direct' });
      arbiter.setRelationConfig('viewer', {
        intersection: [
          { type: 'direct', relation: 'rel_a' },
          { type: 'direct', relation: 'rel_b' }
        ]
      });
      if (hasA) arbiter.addRelation('user:u', 'rel_a', 'doc:1', { possibility: pa });
      if (hasB) arbiter.addRelation('user:u', 'rel_b', 'doc:1', { possibility: pb });

      const result = arbiter.check('user:u', 'viewer', 'doc:1');
      const expected = Math.min(hasA ? pa : 0, hasB ? pb : 0);
      if (Math.abs(result.possibility - expected) > EPS) {
        fail(`intersection: expected ${expected}, got ${result.possibility}`);
      }
      return result;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            pa: rigor.gen.oneOf(POSSIBILITIES),
            pb: rigor.gen.oneOf(POSSIBILITIES),
            hasA: rigor.gen.boolean(),
            hasB: rigor.gen.boolean()
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('intersection-min', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 400, seed: 'zanzibar-intersection' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'intersection-min');
    assert.ok(inv);
    assert.equal(inv.passed, true, `INTERSECTION contract violated in ${inv.failureCount} cases`);
  });

  it('EXCLUSION (A AND NOT B): denied set blocks the allowed set', async () => {
    async function check({ pa, pb, denied }) {
      const arbiter = new Arbiter();
      ['user:u', 'doc:1'].forEach((k) => arbiter.addNode(k, k.startsWith('user') ? 'user' : 'doc'));
      arbiter.setRelationConfig('rel_a', { type: 'direct' });
      arbiter.setRelationConfig('rel_b', { type: 'direct' });
      arbiter.setRelationConfig('viewer', {
        exclusion: [
          { type: 'direct', relation: 'rel_a' },
          { type: 'direct', relation: 'rel_b' }
        ]
      });
      arbiter.addRelation('user:u', 'rel_a', 'doc:1', { possibility: pa });
      if (denied) arbiter.addRelation('user:u', 'rel_b', 'doc:1', { possibility: pb });

      const result = arbiter.check('user:u', 'viewer', 'doc:1');
      const expected = pa * (1 - (denied ? pb : 0));
      if (Math.abs(result.possibility - expected) > EPS) {
        fail(`exclusion: expected ${expected}, got ${result.possibility}`);
      }
      return result;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            pa: rigor.gen.oneOf(POSSIBILITIES),
            pb: rigor.gen.oneOf(POSSIBILITIES),
            denied: rigor.gen.boolean()
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('exclusion-blocks', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 400, seed: 'zanzibar-exclusion' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'exclusion-blocks');
    assert.ok(inv);
    assert.equal(inv.passed, true, `EXCLUSION contract violated in ${inv.failureCount} cases`);
  });

  it('EXPAND PARITY: check() agrees with the Expand-RPC oracle on random graphs', async () => {
    async function check(caseParams) {
      const { arbiter, graph, config, users } = buildRandomZanzibarCase(caseParams);
      const oracle = buildExpandOracle(graph, config);

      for (const user of users) {
        const expected = oracle.evalRule(config, user);
        const actual = arbiter.check(user, 'viewer', graph.objectId);
        if (Math.abs(actual.possibility - expected) > EPS) {
          fail(`expand parity for ${user}: oracle=${expected}, engine=${actual.possibility}`);
        }
      }
      return { checked: users.length };
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            userCount: rigor.gen.int(1, 4),
            groupCount: rigor.gen.int(0, 4),
            configKind: rigor.gen.int(0, 4)
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('expand-parity', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 800, seed: 'zanzibar-expand-parity' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'expand-parity');
    assert.ok(inv);
    assert.equal(inv.passed, true, `EXPAND PARITY violated in ${inv.failureCount} cases`);
  });

  it('NESTED CHAIN: transitivity through N groups honors the weakest link', async () => {
    async function check({ depth, ps }) {
      const arbiter = new Arbiter();
      arbiter.addNode('user:alice', 'user');
      arbiter.addNode('doc:1', 'doc');
      const groupKeys = [];
      for (let i = 0; i < depth; i++) {
        const key = `group:${i}`;
        groupKeys.push(key);
        arbiter.addNode(key, 'group');
      }
      arbiter.setRelationConfig('member_of', { type: 'direct' });
      arbiter.setRelationConfig('viewer', { type: 'direct' });
      const steps = [];
      for (let i = 0; i < depth; i++) {
        steps.push({ relation: 'member_of', direction: 'out' });
      }
      steps.push({ relation: 'viewer', direction: 'out' });
      arbiter.setRelationConfig('can_access', { type: 'chain', steps });

      let from = 'user:alice';
      let expected = 1;
      for (let i = 0; i < depth; i++) {
        arbiter.addRelation(from, 'member_of', groupKeys[i], { possibility: ps[i] });
        expected = Math.min(expected, ps[i]);
        from = groupKeys[i];
      }
      arbiter.addRelation(from, 'viewer', 'doc:1', { possibility: ps[depth] });
      expected = Math.min(expected, ps[depth]);

      const result = arbiter.check('user:alice', 'can_access', 'doc:1');
      if (Math.abs(result.possibility - expected) > EPS) {
        fail(`nested chain depth ${depth}: expected ${expected}, got ${result.possibility}`);
      }
      return result;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            depth: rigor.gen.int(1, 5),
            ps: rigor.gen.array(rigor.gen.oneOf(POSSIBILITIES), 2, 6)
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('nested-weakest-link', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 500, seed: 'zanzibar-nested-chain' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'nested-weakest-link');
    assert.ok(inv);
    assert.equal(inv.passed, true, `NESTED CHAIN contract violated in ${inv.failureCount} cases`);
  });

  it('CYCLE SAFETY: cyclic memberships terminate and never fabricate access', async () => {
    async function check({ cycleSize, memberP }) {
      const arbiter = new Arbiter();
      arbiter.addNode('user:alice', 'user');
      arbiter.addNode('doc:1', 'doc');
      const groups = [];
      for (let i = 0; i < cycleSize; i++) {
        const key = `group:${i}`;
        groups.push(key);
        arbiter.addNode(key, 'group');
      }
      arbiter.setRelationConfig('member_of', { type: 'direct' });
      arbiter.setRelationConfig('viewer', { type: 'direct' });
      arbiter.setRelationConfig('can_access', {
        type: 'chain',
        steps: [
          { relation: 'member_of', direction: 'out' },
          { relation: 'member_of', direction: 'out' },
          { relation: 'viewer', direction: 'out' }
        ]
      });

      // Closed cycle: g0 → g1 → ... → g0 (no user attached, no doc access)
      for (let i = 0; i < cycleSize; i++) {
        const next = groups[(i + 1) % cycleSize];
        arbiter.addRelation(groups[i], 'member_of', next, { possibility: memberP });
      }
      // A user attached to the cycle must not gain access to the doc
      arbiter.addRelation('user:alice', 'member_of', groups[0], { possibility: memberP });

      const result = arbiter.check('user:alice', 'can_access', 'doc:1');
      if (result.possibility !== 0) {
        fail(`cycle fabricated access: ${result.possibility}`);
      }
      return result;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            cycleSize: rigor.gen.int(2, 6),
            memberP: rigor.gen.oneOf([0.25, 0.5, 1])
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('cycle-safe', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 400, seed: 'zanzibar-cycle-safety' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'cycle-safe');
    assert.ok(inv);
    assert.equal(inv.passed, true, `CYCLE SAFETY violated in ${inv.failureCount} cases`);
  });
});