/**
 * rigor/zanzibar-defeasible-dsl-comparator.test.js — js-rigor property tests
 * for defeasible logic, DSL→runtime parity, and value aggregation.
 *
 * Properties verified:
 *
 *   - NEVER: an absolute denial overrides every positive rule (binary).
 *   - UNLESS (defeater): a triggered defeater blocks the defeasible grant.
 *   - ALWAYS (strict): strict grants survive unless NEVER fires.
 *   - WHEN: a defeasible rule grants iff its conditions hold and no
 *     defeater fires.
 *   - DSL→RUNTIME PARITY: evidence compiled from DSL behaves identically
 *     to the equivalent hand-written relation configs on identical graphs,
 *     across generated edge possibilities.
 *   - AGGREGATION: a relational-comparator sum over N parallel chain paths
 *     totals ALL path values (regression — the dedup-before-collect bug
 *     dropped weaker paths' contributions).
 */
import { describe, it } from 'node:test';
import assert from 'node:assert/strict';
import { rigor } from '@rigor/core';
import { Arbiter } from '../../src/index.js';
import { DSLCompiler } from '@arbiter/evidence-dsl/DSLCompiler';

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

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

describe('Defeasible logic, DSL parity, aggregation (rigor)', () => {
  it('DEFEASIBLE: NEVER denies, UNLESS defeats, ALWAYS survives, WHEN grants', async () => {
    async function check({ shape, pAllow, pBlock }) {
      const arbiter = new Arbiter();
      ['user:u', 'doc:1'].forEach((k) =>
        arbiter.addNode(k, k.startsWith('user') ? 'user' : 'doc'));
      arbiter.setRelationConfig('can_access', { type: 'direct' });
      arbiter.setRelationConfig('is_blocked', { type: 'direct' });
      arbiter.setRelationConfig('is_emergency', { type: 'direct' });

      const configs = {
        when: {
          when: { intersection: [{ type: 'direct', relation: 'can_access' }] }
        },
        unless: {
          when: { intersection: [{ type: 'direct', relation: 'can_access' }] },
          unless: { union: [{ type: 'direct', relation: 'is_blocked' }] }
        },
        never: {
          never: { union: [{ type: 'direct', relation: 'is_blocked' }] },
          when: { intersection: [{ type: 'direct', relation: 'can_access' }] }
        },
        always: {
          always: { type: 'direct', relation: 'is_emergency' },
          when: { intersection: [{ type: 'direct', relation: 'can_access' }] }
        }
      };
      arbiter.setRelationConfig('viewer', configs[shape]);

      arbiter.addRelation('user:u', 'can_access', 'doc:1', { possibility: pAllow });
      if (shape !== 'always') {
        arbiter.addRelation('user:u', 'is_blocked', 'doc:1', { possibility: pBlock });
      } else {
        arbiter.addRelation('user:u', 'is_emergency', 'doc:1', { possibility: pBlock });
      }

      const result = arbiter.check('user:u', 'viewer', 'doc:1');
      // Normal-mode defeasible semantics (continuous possibility):
      //   - when:    base = when-part possibility
      //   - unless:  result *= (1 - defeater possibility)
      //   - never:   result = 0 when never possibility >= 0.5
      //   - always:  result = max(base, strict possibility)
      let expected;
      if (shape === 'when') {
        expected = pAllow;
      } else if (shape === 'unless') {
        expected = pAllow * (1 - pBlock);
      } else if (shape === 'never') {
        expected = pBlock >= 0.5 ? 0 : pAllow;
      } else {
        expected = Math.max(pAllow, pBlock);
      }
      if (Math.abs(result.possibility - expected) > EPS) {
        fail(`${shape}: expected ${expected}, got ${result.possibility} (pAllow=${pAllow}, pBlock=${pBlock})`);
      }
      return result;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            shape: rigor.gen.oneOf(['when', 'unless', 'never', 'always']),
            pAllow: rigor.gen.oneOf(POSSIBILITIES),
            pBlock: rigor.gen.oneOf(POSSIBILITIES)
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('defeasible-semantics', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 600, seed: 'defeasible-semantics' , artifacts: { dir: '', persist: 'never' }});

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

  it('DSL→RUNTIME PARITY: compiled evidence matches hand-written configs on identical graphs', async () => {
    const DSL = `
      definition Doc { id: string }
      definition Dept { id: string }
      fact owns(user: User, doc: Doc)
      fact works_in(user: User, dept: Dept)
      fact has_access(dept: Dept, doc: Doc)
      evidence can_read(user: User, doc: Doc) { owns(user, doc) }
      evidence can_access(user: User, doc: Doc) { works_in(user, *d) { has_access(d, doc) } }
    `;

    async function check({ pOwn, pMember, pReads }) {
      // Compiled arbiter: DSL -> generated configs
      const compiled = new Arbiter();
      compiled.addNode('user:alice', 'user');
      compiled.addNode('group:eng', 'group');
      compiled.addNode('doc:1', 'doc');
      const compiler = new DSLCompiler(compiled);
      const result = compiler.compile(DSL, 'parity');
      if (!result.success) {
        fail(`DSL compile failed: ${result.errors.join('; ')}`);
      }

      // Hand-written arbiter: equivalent configs by hand
      const manual = new Arbiter();
      manual.addNode('user:alice', 'user');
      manual.addNode('group:eng', 'group');
      manual.addNode('doc:1', 'doc');
      manual.setRelationConfig('can_read', { type: 'direct', relation: 'owns' });
      manual.setRelationConfig('can_access', {
        type: 'chain',
        steps: [
          { relation: 'works_in', direction: 'out' },
          { relation: 'has_access', direction: 'out' }
        ]
      });

      // Identical graph on both
      for (const arb of [compiled, manual]) {
        arb.addRelation('user:alice', 'owns', 'doc:1', { possibility: pOwn });
        arb.addRelation('user:alice', 'works_in', 'group:eng', { possibility: pMember });
        arb.addRelation('group:eng', 'has_access', 'doc:1', { possibility: pReads });
      }

      for (const rel of ['can_read', 'can_access']) {
        const compiledResult = compiled.check('user:alice', rel, 'doc:1');
        const manualResult = manual.check('user:alice', rel, 'doc:1');
        if (Math.abs(compiledResult.possibility - manualResult.possibility) > EPS) {
          fail(`${rel}: compiled=${compiledResult.possibility} vs manual=${manualResult.possibility}`);
        }
      }
      return { canRead: compiled.check('user:alice', 'can_read', 'doc:1').possibility };
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            pOwn: rigor.gen.oneOf(POSSIBILITIES),
            pMember: rigor.gen.oneOf(POSSIBILITIES),
            pReads: rigor.gen.oneOf(POSSIBILITIES)
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('dsl-parity', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 400, seed: 'dsl-runtime-parity' , artifacts: { dir: '', persist: 'never' }});

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

  it('AGGREGATION: relational-comparator sum totals ALL parallel path values', async () => {
    async function check({ paths, value, price }) {
      const arbiter = new Arbiter();
      arbiter.addNode('user:alice', 'user');
      arbiter.addNode('feature:premium', 'feature');
      const mids = [];
      for (let i = 0; i < paths; i++) {
        const key = `mid:${i}`;
        mids.push(key);
        arbiter.addNode(key, 'account');
      }
      arbiter.setRelationConfig('can_debit', { type: 'direct' });
      arbiter.setRelationConfig('has_balance', { type: 'direct' });
      arbiter.setRelationConfig('has_price', { type: 'direct' });
      arbiter.setRelationConfig('authorized_balance_check', {
        type: 'relational_comparator',
        left: {
          rule: {
            type: 'chain',
            steps: [
              { relation: 'can_debit', direction: 'out' },
              { relation: 'has_balance', direction: 'out' }
            ],
            extractValues: true,
            extractFrom: 1,
            extractRelation: 'has_balance',
            valueAggregation: 'sum',
            evaluateFrom: 'user'
          },
          extractValue: true,
          aggregator: 'sum',
          evaluateFrom: 'user',
          decayRate: 0,
          decayFunction: 'rational'
        },
        right: {
          rule: { type: 'direct', relation: 'has_price', evaluateFrom: 'object' },
          extractValue: true,
          evaluateFrom: 'object',
          decayRate: 0,
          decayFunction: 'rational'
        },
        comparator: '>=',
        fallbackBehavior: 'deny'
      });

      // N parallel paths, weakening possibilities (the old dedup bug dropped
      // the weaker paths' values, under-reporting the authorized total).
      for (let i = 0; i < paths; i++) {
        const p = 1 - i * 0.15;
        arbiter.addRelation('user:alice', 'can_debit', mids[i], { possibility: p });
        arbiter.addRelation(mids[i], 'has_balance', 'feature:premium', { possibility: p, value });
      }
      arbiter.addRelation('feature:premium', 'has_price', 'feature:premium', { value: price });

      const result = arbiter.check('user:alice', 'authorized_balance_check', 'feature:premium', {
        includeMeta: true
      });

      const expectedTotal = paths * value;
      const leftValue = result.meta?.allow?.leftValue ?? result.meta?.deny?.leftValue;
      if (Math.abs(leftValue - expectedTotal) > EPS) {
        fail(`sum: expected ${expectedTotal}, got ${leftValue} (${paths} paths × ${value})`);
      }
      const expectedGrant = expectedTotal >= price;
      if ((result.possibility > 0) !== expectedGrant) {
        fail(`decision: expected grant=${expectedGrant} (${expectedTotal} >= ${price}), got ${result.possibility}`);
      }
      return { leftValue, granted: result.possibility > 0 };
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            paths: rigor.gen.int(2, 5),
            value: rigor.gen.int(50, 300),
            price: rigor.gen.int(100, 1000)
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('aggregation-complete', ({ actual }) => actual !== undefined)
      ])
    ).run({ effort: 500, seed: 'aggregation-completeness' , artifacts: { dir: '', persist: 'never' }});

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