/**
 * rigor/binary-mode-parity.test.js — js-rigor property tests for binary
 * (threshold) evaluation mode.
 *
 * Binary mode is a separate evaluation path (_checkBinary + binary rules
 * short-circuit) with dual thresholds: allow when strength >=
 * minAllowPossibility, deny when deny-strength >= maxDenyPossibility.
 *
 * Properties verified:
 *
 *   - BINARY-NORMAL AGREEMENT: for every config kind and threshold,
 *     binary.allow === (normal-mode possibility >= minAllowPossibility)
 *     and the reason string is consistent.
 *   - CONTINUOUS POSSIBILITY: binary.possibility reports the real
 *     continuous strength (=== normal-mode possibility), never a binarized
 *     0/1 — for direct, chain, and logical operator configs.
 *   - EXCLUSION DUAL THRESHOLD: top-level exclusion sets deny exactly when
 *     the negated child's strength >= maxDenyPossibility.
 *   - FASTPATH THRESHOLD PARITY: fastPath:true + minPossibility evaluates
 *     the same continuous possibility as normal mode.
 *   - MUTATION FRESHNESS: after every mutation, binary and normal checks
 *     agree, and binary reflects the new state even with caching enabled.
 */
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 POS = [0, 0.25, 0.5, 0.75, 1];
const THRESHOLDS = [0.2, 0.5, 0.8];
const DENY_THRESHOLDS = [0.3, 0.6, 0.9];

const KINDS = 10; // + defeasible (when+unless), (when+never), (always+when+unless)

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

function buildArbiter() {
  const arb = new Arbiter();
  arb.addNode('user:alice', 'user');
  arb.addNode('group:eng', 'group');
  arb.addNode('doc:1', 'doc');
  arb.setRelationConfig('r1', { type: 'direct' });
  arb.setRelationConfig('r2', { type: 'direct' });
  arb.setRelationConfig('r3', { type: 'direct' });
  arb.setRelationConfig('member_of', { type: 'direct' });
  arb.setRelationConfig('viewer', { type: 'direct' });
  arb.setRelationConfig('strict', { type: 'direct' });
  return arb;
}

function childRule(rel) {
  return { type: 'direct', relation: rel };
}

function makeConfig(kind) {
  switch (kind) {
    case 0: return childRule('r1');
    case 1: return {
      type: 'chain',
      steps: [
        { relation: 'member_of', direction: 'out' },
        { relation: 'viewer', direction: 'out' }
      ]
    };
    case 2: return { union: [childRule('r1'), childRule('r2')] };
    case 3: return { intersection: [childRule('r1'), childRule('r2')] };
    case 4: return { exclusion: [childRule('r1'), childRule('r2')] };
    case 5: return { union: [childRule('r1'), { exclusion: [childRule('r2'), childRule('r3')] }] };
    case 6: return { union: [makeConfig(1), childRule('r1')] };
    case 7: return { type: 'defeasible', when: childRule('r1'), unless: childRule('r2') };
    case 8: return { type: 'defeasible', when: childRule('r1'), never: childRule('r2') };
    case 9: return { type: 'defeasible', always: childRule('r3'), when: childRule('r1'), unless: childRule('r2') };
    default: throw new Error(`bad kind ${kind}`);
  }
}

function edgeMap(edges) {
  const m = new Map();
  for (const [rel, p] of edges) m.set(rel, p);
  return m;
}

function oraclePossibility(kind, em) {
  const p = (rel) => em.has(rel) ? em.get(rel) : 0;
  switch (kind) {
    case 0: return p('r1');
    case 1: {
      // min over path edges; 0 if either edge missing
      if (!em.has('member_of') || !em.has('viewer')) return 0;
      return Math.min(em.get('member_of'), em.get('viewer'));
    }
    case 2: return Math.max(p('r1'), p('r2'));
    case 3: return Math.min(p('r1'), p('r2'));
    case 4: return p('r1') * (1 - p('r2'));
    case 5: return Math.max(p('r1'), p('r2') * (1 - p('r3')));
    case 6: {
      const chain = (!em.has('member_of') || !em.has('viewer')) ? 0 : Math.min(em.get('member_of'), em.get('viewer'));
      return Math.max(chain, p('r1'));
    }
    case 7: return p('r1') * (1 - p('r2'));
    case 8: return p('r2') >= 0.5 ? 0 : p('r1');
    case 9: return Math.max(p('r3'), p('r1')) * (1 - p('r2'));
    default: throw new Error(`bad kind ${kind}`);
  }
}

function oracleDeniedPossibility(kind, em) {
  // The negated child strength for top-level exclusion (kind 4 only)
  if (kind !== 4) return 0;
  return em.has('r2') ? em.get('r2') : 0;
}

function randomEdges(seedState) {
  // Deterministic pseudo-random via mulberry32
  const edges = [];
  const rels = ['r1', 'r2', 'r3', 'member_of', 'viewer', 'banned', 'strict'];
  for (const rel of rels) {
    if (seedState.next() < 0.55) {
      edges.push([rel, POS[Math.floor(seedState.next() * POS.length)]]);
    }
  }
  return edges;
}

function mulberry32(seed) {
  let a = seed >>> 0;
  return {
    next() {
      a |= 0; a = (a + 0x6D2B79F5) | 0;
      let t = Math.imul(a ^ (a >>> 15), 1 | a);
      t = (t + Math.imul(t ^ (t >>> 7), 61 | t)) ^ t;
      return ((t ^ (t >>> 14)) >>> 0) / 4294967296;
    }
  };
}

function applyEdges(arb, edges, mode) {
  for (const [rel, p] of edges) {
    const dst = rel === 'member_of' ? 'group:eng' : 'doc:1';
    if (mode === 'add') {
      const src = rel === 'viewer' ? 'group:eng' : 'user:alice';
      arb.addRelation(src, rel, dst, { possibility: p });
    } else {
      const src = rel === 'viewer' ? 'group:eng' : 'user:alice';
      arb.removeRelation(src, rel, dst);
    }
  }
}

function verifyParity(arb, kind, { minAllow, maxDeny, edges }) {
  const config = arb.relationConfigs.get('target');
  const em = edgeMap(edges);
  const expectedP = oraclePossibility(kind, em);
  const expectedDenied = oracleDeniedPossibility(kind, em);

  const normal = arb.check('user:alice', 'target', 'doc:1');
  const binary = arb.check('user:alice', 'target', 'doc:1', { binary: true, minAllowPossibility: minAllow, maxDenyPossibility: maxDeny });

  // BINARY-NORMAL AGREEMENT (decision-level, always exact)
  const expectedAllow = expectedP >= minAllow;
  const expectedDeny = expectedDenied >= maxDeny;
  const expectedReason = expectedAllow ? 'allow' : (expectedDeny && kind === 4) ? 'deny' : 'insufficient_confidence';

  if (binary.allow !== expectedAllow) {
    fail(`allow mismatch kind=${kind} p=${expectedP} t=${minAllow}: expected allow=${expectedAllow}, got ${binary.allow} (normal=${normal.possibility})`);
  }
  if (binary.deny !== expectedDeny) {
    fail(`deny mismatch kind=${kind} denied=${expectedDenied} denyT=${maxDeny}: expected deny=${expectedDeny}, got ${binary.deny}`);
  }
  if (binary.reason !== expectedReason) {
    fail(`reason mismatch kind=${kind}: expected ${expectedReason}, got ${binary.reason}`);
  }

  // VALUE contract: binary mode evaluates via the rule path (chain children
  // collapse sub-threshold paths to 0) and must match exactly whenever no
  // operator early exit can have fired. fastPath normal mode evaluates via
  // the compiled path, which reports true continuous values (no collapse);
  // its early-exit gates are the same.
  const expectedValue = expectedBinaryValue(kind, em, minAllow);
  if (!earlyExitMayFire(kind, em, minAllow)) {
    if (Math.abs(binary.possibility - expectedValue) > EPS) {
      fail(`binary value mismatch kind=${kind}: expected ${expectedValue}, got ${binary.possibility} (normal=${normal.possibility}, p=${expectedP}, t=${minAllow})`);
    }
    const fp = arb.check('user:alice', 'target', 'doc:1', { fastPath: true, minAllowPossibility: minAllow });
    if (Math.abs(fp.possibility - expectedP) > EPS) {
      fail(`fastPath value mismatch kind=${kind}: expected ${expectedP}, got ${fp.possibility} (t=${minAllow})`);
    }
  } else {
    // Early exit may have fired: values are approximations, decisions exact.
    const fp = arb.check('user:alice', 'target', 'doc:1', { fastPath: true, minAllowPossibility: minAllow });
    if ((fp.possibility >= minAllow) !== (expectedP >= minAllow)) {
      fail(`fastPath decision mismatch kind=${kind}: p=${expectedP} t=${minAllow} fp=${fp.possibility}`);
    }
  }

  // NORMAL mode always reports the true continuous possibility.
  if (Math.abs(normal.possibility - expectedP) > EPS) {
    fail(`normal possibility mismatch kind=${kind}: expected ${expectedP}, got ${normal.possibility}`);
  }

  return { expectedP, binary, normal };
}

function chainPossibilityOf(em) {
  if (!em.has('member_of') || !em.has('viewer')) return 0;
  return Math.min(em.get('member_of'), em.get('viewer'));
}

function childPossibilitiesOf(kind, em) {
  const p = (rel) => em.has(rel) ? em.get(rel) : 0;
  switch (kind) {
    case 2: return [p('r1'), p('r2')];
    case 3: return [p('r1'), p('r2')];
    case 5: return [p('r1'), p('r2') * (1 - p('r3'))];
    default: return [];
  }
}

/**
 * Threshold-mode value oracle. Binary (and fastPath) evaluation runs in
 * threshold mode: chain children collapse to 0 when their possibility is
 * below the allow threshold (path pruning — decision-sound), while direct
 * children keep continuous values. Union/intersection/exclusion aggregate
 * the collapsed child values.
 */
function expectedBinaryValue(kind, em, t) {
  const p = (rel) => em.has(rel) ? em.get(rel) : 0;
  const chainV = (kind === 1 || kind === 6) ? chainPossibilityOf(em) : 0;
  const chainCollapsed = chainV >= t ? chainV : 0;
  switch (kind) {
    case 0: return p('r1');
    case 1: return chainCollapsed;
    case 2: return Math.max(p('r1'), p('r2'));
    case 3: return Math.min(p('r1'), p('r2'));
    case 4: return p('r1') * (1 - p('r2'));
    case 5: return Math.max(p('r1'), p('r2') * (1 - p('r3')));
    case 6: return Math.max(chainCollapsed, p('r1'));
    case 7: return p('r1') * (1 - p('r2'));
    case 8: return p('r2') >= 0.5 ? 0 : p('r1');
    case 9: return Math.max(p('r3'), p('r1')) * (1 - p('r2'));
    default: throw new Error(`bad kind ${kind}`);
  }
}

/**
 * True: an early-exit may have fired during evaluation, making the reported
 * value a first-crossing approximation (union: first child >= t; chain child
 * is first in kind 6). Decisions remain exact regardless.
 */
function earlyExitMayFire(kind, em, t) {
  const p = (rel) => em.has(rel) ? em.get(rel) : 0;
  switch (kind) {
    case 0:
    case 1:
    case 4: return false;
    case 2: return childPossibilitiesOf(kind, em).some(v => v >= t);
    case 3: return childPossibilitiesOf(kind, em).some(v => v < t);
    case 5: return childPossibilitiesOf(kind, em).some(v => v >= t);
    case 6: return chainPossibilityOf(em) >= t;
    case 7:
    case 8:
    case 9: return false;
    default: throw new Error(`bad kind ${kind}`);
  }
}

describe('Binary (threshold) mode parity (rigor)', () => {
  it('BINARY-NORMAL AGREEMENT across all config kinds and thresholds', async () => {
    async function check({ kind, seed, minAllow, maxDeny }) {
      const rng = mulberry32(seed);
      const edges = randomEdges(rng);
      const arb = buildArbiter();
      arb.setRelationConfig('target', makeConfig(kind));
      applyEdges(arb, edges, 'add');
      return verifyParity(arb, kind, { minAllow, maxDeny, edges });
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            kind: rigor.gen.int(0, KINDS - 1),
            seed: rigor.gen.int(1, 100000),
            minAllow: rigor.gen.oneOf(THRESHOLDS),
            maxDeny: rigor.gen.oneOf(DENY_THRESHOLDS)
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('binary-normal-agreement', ({ error, errorMessage }) => !error && !errorMessage)
      ])
    ).run({ effort: 1200, seed: 'binary-mode-config-matrix' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'binary-normal-agreement');
    assert.ok(inv, 'invariant missing');
    assert.equal(inv.passed, true, `binary parity violated in ${inv.failureCount} cases: ` +
      JSON.stringify((report.failures || []).slice(0, 2).map(f => ({ name: f.name, msg: f.message, seq: (f.sequence || []).map(s => s.args) }))));
  });

  it('MUTATION FRESHNESS: binary and normal agree after every mutation with caching enabled', async () => {
    async function check({ kind, seed, minAllow, maxDeny, mutations }) {
      const rng = mulberry32(seed);
      const edges = randomEdges(rng);
      const arb = buildArbiter();
      arb.setRelationConfig('target', makeConfig(kind));
      applyEdges(arb, edges, 'add');

      // Warm the cache with an initial binary check
      arb.check('user:alice', 'target', 'doc:1', { binary: true, minAllowPossibility: minAllow, maxDenyPossibility: maxDeny });

      for (let i = 0; i < mutations; i++) {
        // Mutate: toggle a random edge's presence
        const rels = ['r1', 'r2', 'r3', 'member_of', 'viewer', 'banned', 'strict'];
        const rel = rels[Math.floor(rng.next() * rels.length)];
        const dst = rel === 'member_of' ? 'group:eng' : 'doc:1';
        const src = rel === 'viewer' ? 'group:eng' : 'user:alice';
        const existing = arb.indices.getDirectRelation(
          arb.resolveNodeId(src), rel, arb.resolveNodeId(dst)
        );
        const idx = edges.findIndex(e => e[0] === rel);
        if (existing) {
          arb.removeRelation(src, rel, dst);
          if (idx !== -1) edges.splice(idx, 1);
        } else {
          const p = POS[Math.floor(rng.next() * POS.length)];
          arb.addRelation(src, rel, dst, { possibility: p });
          if (idx !== -1) edges[idx][1] = p;
          else edges.push([rel, p]);
        }

        verifyParity(arb, kind, { minAllow, maxDeny, edges });
      }
      return { mutations };
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            kind: rigor.gen.int(0, KINDS - 1),
            seed: rigor.gen.int(1, 50000),
            minAllow: rigor.gen.oneOf(THRESHOLDS),
            maxDeny: rigor.gen.oneOf(DENY_THRESHOLDS),
            mutations: rigor.gen.int(2, 6)
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('mutation-freshness', ({ error, errorMessage }) => !error && !errorMessage)
      ])
    ).run({ effort: 800, seed: 'binary-mode-mutation-parity' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'mutation-freshness');
    assert.ok(inv, 'invariant missing');
    assert.equal(inv.passed, true, `mutation freshness violated in ${inv.failureCount} cases`);
  });
});