/**
 * rigor/check-explain-agreement.test.js — js-rigor property tests for the
 * agreement between arbiter.check() and arbiter.explain().
 *
 * Properties verified:
 *
 *   - AGREEMENT: check().possibility equals explain().decision.possibility
 *     on the same graph (the explain path must never diverge from the
 *     check path).
 *   - GRANT ⟺ USED FACTS: a grant (possibility > 0) is always accompanied
 *     by provenance used_facts; a deny with no path produces none.
 *   - INJECTABLE REMEDIATION: when the checked relation depends on an
 *     injectable source that is absent, both check() and explain() surface
 *     unified remediation naming the missing relation.
 *   - CONFIG OVERRIDE: these invariants hold with relation-override configs
 *     (can_read → viewer), where the provenance must report the effective
 *     relation.
 */
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];

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

function buildArbiter(seedCase) {
  const { hasRelation, p, injectable, override } = seedCase;
  const arbiter = new Arbiter();
  arbiter.addNode('user:1', 'user');
  arbiter.addNode('doc:1', 'doc');

  if (injectable) {
    arbiter.setRelationConfig('mfa', {
      type: 'source',
      relation: 'mfa',
      injectable: true,
      provides: 'Proof'
    });
  }
  arbiter.setRelationConfig('viewer', { type: 'direct' });
  arbiter.setRelationConfig('can_read', override
    ? { type: 'direct', relation: 'viewer' }
    : { type: 'direct' });

  if (hasRelation) {
    arbiter.addRelation('user:1', override ? 'viewer' : 'can_read', 'doc:1', { possibility: p });
  }
  return arbiter;
}

describe('check/explain agreement (rigor)', () => {
  it('AGREEMENT: check and explain always decide the same possibility', async () => {
    async function check(seedCase) {
      const arbiter = buildArbiter(seedCase);
      const checked = arbiter.check('user:1', 'can_read', 'doc:1');
      const explained = arbiter.explain('user:1', 'can_read', 'doc:1');

      if (Math.abs(checked.possibility - explained.decision.possibility) > EPS) {
        fail(`agreement: check=${checked.possibility} vs explain=${explained.decision.possibility}`);
      }
      return explained.decision;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            hasRelation: rigor.gen.boolean(),
            p: rigor.gen.oneOf(POS),
            injectable: rigor.gen.boolean(),
            override: rigor.gen.boolean()
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('check-explain-agree', ({ error, errorMessage }) => !error && !errorMessage)
      ])
    ).run({ effort: 500, seed: 'explain-agreement' , artifacts: { dir: '', persist: 'never' }});

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

  it('GRANT ⟺ USED FACTS: provenance marks used facts exactly when granting', async () => {
    async function check(seedCase) {
      const arbiter = buildArbiter(seedCase);
      const checked = arbiter.check('user:1', 'can_read', 'doc:1');

      if (seedCase.withPartial) {
        // Partial-graph mode: the fact arrives via the request's partial
        // graph, and provenance must mark it used iff the check grants.
        const partialGraph = {
          relations: [
            {
              src: 'user:1',
              relation: seedCase.override ? 'viewer' : 'can_read',
              dst: 'doc:1',
              possibility: 0.9
            }
          ]
        };
        const checked = arbiter.check('user:1', 'can_read', 'doc:1', { partialGraph });
        const explained = arbiter.explain('user:1', 'can_read', 'doc:1', { partialGraph });
        const used = explained.audit?.provenance?.used_facts || [];
        // A grant must always be explainable by a used fact. (A deny may
        // also have used facts — a 0-possibility persistent fact that beat
        // a partial fact by trust precedence.)
        if (checked.possibility > 0 && !used.some(u => u.used === true)) {
          fail(`partial grant (${checked.possibility}) without a used fact`);
        }
        // Every used fact must correspond to a real edge in the effective source
        for (const u of used) {
          if (u.used === true && u.source !== 'persistent' && u.source !== 'partial') {
            fail(`used fact with unknown source: ${u.source}`);
          }
        }
      } else {
        // Plain-graph mode: provenance is not emitted; the trace must
        // contain a true decision node exactly when granting.
        const explained = arbiter.explain('user:1', 'can_read', 'doc:1');
        const traceTrue = (explained.trace?.path || []).filter(n => n.result === true).length;
        if (checked.possibility > 0 && traceTrue === 0) {
          fail(`grant (${checked.possibility}) without a true trace node`);
        }
        if (checked.possibility === 0 && traceTrue > 0) {
          fail(`deny with spurious true trace nodes`);
        }
      }
      return checked.possibility;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            hasRelation: rigor.gen.boolean(),
            p: rigor.gen.oneOf(POS),
            injectable: rigor.gen.boolean(),
            override: rigor.gen.boolean(),
            withPartial: rigor.gen.boolean()
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('used-facts-consistent', ({ error, errorMessage }) => !error && !errorMessage)
      ])
    ).run({ effort: 600, seed: 'explain-used-facts' , artifacts: { dir: '', persist: 'never' }});

    const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'used-facts-consistent');
    assert.ok(inv);
    assert.equal(inv.passed, true, `USED FACTS violated in ${inv.failureCount} cases`);
  });

  it('INJECTABLE REMEDIATION: missing witness surfaces remediation in both check and explain', async () => {
    async function check(seedCase) {
      const arbiter = buildArbiter({ ...seedCase, injectable: true, override: true });
      // can_delete depends on the injectable mfa source
      arbiter.setRelationConfig('can_delete', { type: 'direct', relation: 'mfa' });
      if (seedCase.hasRelation) {
        arbiter.addRelation('user:1', 'mfa', 'doc:1', { possibility: seedCase.p });
      }

      const checked = arbiter.check('user:1', 'can_delete', 'doc:1');
      if (seedCase.hasRelation) {
        // Edge present: grants at its possibility when > 0; a 0-possibility
        // edge is present-but-no-confidence — deny, no remediation.
        if (checked.possibility !== seedCase.p) {
          fail(`witness present: expected ${seedCase.p}, got ${checked.possibility}`);
        }
        if (checked.remediation) {
          fail(`witness present must not carry remediation`);
        }
      } else {
        const options = checked.remediation?.options || [];
        const mfaOption = options.find(o => o.relation === 'mfa' && o.object === 'doc:1');
        if (!mfaOption) {
          fail(`missing witness must remediate mfa on doc:1, got ${JSON.stringify(options)}`);
        }
      }
      return checked;
    }

    const report = await rigor.campaign(
      [
        rigor.fn('check', check, rigor.args(
          rigor.gen.object({
            hasRelation: rigor.gen.boolean(),
            p: rigor.gen.oneOf([0, 0.25, 0.5, 1])
          })
        ))
      ],
      rigor.crucible([
        rigor.invariant('remediation-consistent', ({ error, errorMessage }) => !error && !errorMessage)
      ])
    ).run({ effort: 400, seed: 'explain-remediation' , artifacts: { dir: '', persist: 'never' }});

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