/**
 * Unit tests for the Imhotep deterministic FOL logic engine.
 *
 * Covers:
 *   - Universal quantification exhaustiveness and short-circuit
 *   - Existential quantification witness correctness and short-circuit
 *   - Boolean connectives (And, Or, Not, Implies)
 *   - Predicate calls against mock geometry worlds
 *   - Rich diagnostics, proofs, and trace events
 */

import { describe, it, beforeEach } from 'node:test';
import assert from 'node:assert';

import type {
  DomainValue,
} from 'imhotep-core';

import type {
  GeometryWorld,
} from './registry.js';

import type {
  FormulaNode,
  PredicateCall,
  ForAllFormula,
  ExistsFormula,
  AndFormula,
  OrFormula,
  NotFormula,
  ImpliesFormula,
  DomainRef,
  TermNode,
} from 'imhotep-core';

import {
  clearPredicateRegistry,
  registerDefaultPredicates,
  getPredicateEvaluator,
} from './predicates.js';

import {
  evaluateLogic,
  type LogicEngineInput,
  type DomainResolver,
} from './logic-engine.js';

// ---------------------------------------------------------------------------
// Mock World Helpers
// ---------------------------------------------------------------------------

function makeWorld(overrides?: Partial<GeometryWorld>): GeometryWorld {
  return {
    sceneId: 'scene_1',
    snapshotId: 'snap_1',
    env: {
      viewportWidth: 1280,
      viewportHeight: 800,
      deviceScaleFactor: 1,
      colorScheme: 'light',
      pointer: 'fine',
      hover: false,
      reducedMotion: false,
      locale: 'en',
      writingMode: 'horizontal-tb',
    },
    strings: { values: [] },
    subjects: {
      ids: [1, 2, 3],
      domNodeId: [10, 20, 30],
      subjectKind: [1, 1, 1],
      primaryBoxId: [100, 200, 300],
      firstFragmentId: [0, 0, 0],
      fragmentCount: [0, 0, 0],
    },
    dom: {
      nodeId: [10, 20, 30],
      parentNodeId: [0, 0, 0],
      childCount: [0, 0, 0],
      tagNameStringId: [0, 0, 0],
    },
    boxes: {
      boxId: [100, 200, 300],
      subjectId: [1, 2, 3],
      frameId: [1, 1, 1],
      borderLeft: [0, 110, 220],
      borderTop: [0, 50, 100],
      borderRight: [100, 210, 320],
      borderBottom: [40, 90, 140],
      paddingLeft: [0, 0, 0],
      paddingTop: [0, 0, 0],
      paddingRight: [0, 0, 0],
      paddingBottom: [0, 0, 0],
      contentLeft: [0, 0, 0],
      contentTop: [0, 0, 0],
      contentRight: [0, 0, 0],
      contentBottom: [0, 0, 0],
    },
    visualBoxes: {
      boxId: [], subjectId: [], frameId: [],
      borderLeft: [], borderTop: [], borderRight: [], borderBottom: [],
      paddingLeft: [], paddingTop: [], paddingRight: [], paddingBottom: [],
      contentLeft: [], contentTop: [], contentRight: [], contentBottom: [],
    },
    transforms: {
      transformId: [], subjectId: [], matrixStart: [], matrixLength: [],
      originX: [], originY: [],
    },
    matrices: { values: [] },
    rects: {
      rectId: [],
      left: [],
      top: [],
      right: [],
      bottom: [],
    },
    topology: {
      containingBlockOf: [0, 0, 0],
      nearestPositionedAncestorOf: [0, 0, 0],
      scrollContainerOf: [0, 0, 0],
      stackingContextOf: [0, 0, 0],
      formattingContextOf: [0, 0, 0],
      clippingRootOf: [0, 0, 0],
      paintOrderBucket: [0, 0, 0],
      paintOrderIndex: [0, 0, 0],
    },
    scroll: {
      containerId: [],
      scrollLeft: [],
      scrollTop: [],
      scrollWidth: [],
      scrollHeight: [],
      clientWidth: [],
      clientHeight: [],
    },
    clipping: {
      clipNodeId: [],
      subjectId: [],
      clipKind: [],
      clipLeft: [],
      clipTop: [],
      clipRight: [],
      clipBottom: [],
      parentClipNodeId: [],
    },
    visibility: {
      subjectId: [],
      isRendered: [],
      isVisible: [],
      visibleArea: [],
      clippedArea: [],
    },
    ...overrides,
  };
}

// ---------------------------------------------------------------------------
// Domain Resolver
// ---------------------------------------------------------------------------

function makeResolver(domains: Map<string, DomainValue>): DomainResolver {
  return {
    resolve(domain: DomainRef, _env?): DomainValue | undefined {
      const key = domain.selector ?? domain.domain;
      return domains.get(key);
    },
  };
}

// ---------------------------------------------------------------------------
// Formula Helpers
// ---------------------------------------------------------------------------

function predicate(name: string, args: TermNode[]): PredicateCall {
  return {
    type: 'FormulaNode',
    kind: 'predicate',
    predicate: name,
    args,
  };
}

function varRef(name: string): TermNode {
  return { type: 'VariableRef', name };
}

function domainRef(domain: string, selector?: string, parentVar?: string): DomainRef {
  return { type: 'DomainRef', domain, selector, parentVar };
}

function forall(bindings: { vars: string[]; domain: DomainRef }[], body: FormulaNode): ForAllFormula {
  return {
    type: 'FormulaNode',
    kind: 'forall',
    bindings: bindings.map((b) => ({
      type: 'TupleBinding',
      variables: b.vars,
      domain: b.domain,
    })),
    body,
  };
}

function exists(bindings: { vars: string[]; domain: DomainRef }[], body: FormulaNode): ExistsFormula {
  return {
    type: 'FormulaNode',
    kind: 'exists',
    bindings: bindings.map((b) => ({
      type: 'TupleBinding',
      variables: b.vars,
      domain: b.domain,
    })),
    body,
  };
}

function and(left: FormulaNode, right: FormulaNode): AndFormula {
  return { type: 'FormulaNode', kind: 'and', left, right };
}

function or(left: FormulaNode, right: FormulaNode): OrFormula {
  return { type: 'FormulaNode', kind: 'or', left, right };
}

function not(operand: FormulaNode): NotFormula {
  return { type: 'FormulaNode', kind: 'not', operand };
}

function implies(antecedent: FormulaNode, consequent: FormulaNode): ImpliesFormula {
  return { type: 'FormulaNode', kind: 'implies', antecedent, consequent };
}

// ---------------------------------------------------------------------------
// Setup
// ---------------------------------------------------------------------------

beforeEach(() => {
  clearPredicateRegistry();
  registerDefaultPredicates();
});

// ---------------------------------------------------------------------------
// Predicate Call Tests
// ---------------------------------------------------------------------------

describe('predicate calls', () => {
  it('evaluates width predicate against a subject', () => {
    const world = makeWorld();
    const formula = predicate('width', [varRef('btn')]);
    const domains = new Map<string, DomainValue>([
      ['.button', {
        domainId: 'dom_1',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.button)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([{ vars: ['btn'], domain: domainRef('elements', '.button') }], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.mode, 'scene-determinate');
    assert.strictEqual(result.passed, true);
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
  });

  it('evaluates leftOf predicate with two subjects', () => {
    const world = makeWorld();
    // Subject 1 [0,0,100,40] is left of subject 2 [110,50,210,90] with gap 10.
    const formula = predicate('leftOf', [varRef('a'), varRef('b')]);
    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['a'], domain: domainRef('elements', '.a') },
        { vars: ['b'], domain: domainRef('elements', '.b') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true);
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
  });

  it('returns indeterminate for unregistered predicate', () => {
    const world = makeWorld();
    clearPredicateRegistry(); // Remove all predicates

    const formula = predicate('unknownPredicate', [varRef('x')]);
    const domains = new Map<string, DomainValue>([
      ['.x', {
        domainId: 'dom_x',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.x)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([{ vars: ['x'], domain: domainRef('elements', '.x') }], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.mode, 'scene-indeterminate');
    assert.strictEqual(result.passed, false);
    assert.ok(result.diagnostics.some((d) => d.code === 'IMH_LOGIC_PREDICATE_MISSING'));
  });

  it('evaluates separatedFrom as inverse of overlaps', () => {
    const world = makeWorld();
    const formula = predicate('separatedFrom', [varRef('a'), varRef('b')]);
    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['a'], domain: domainRef('elements', '.a') },
        { vars: ['b'], domain: domainRef('elements', '.b') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    // Subjects 1 (0,0,100,40) and 2 (110,50,210,90) do not overlap,
    // so separatedFrom should return true and forall should pass.
    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true);
    assert.ok(!result.diagnostics.some((d) => d.code === 'IMH_FEATURE_NOT_YET_IMPLEMENTED'));
  });

  it('evaluates aligned-with directional variants correctly', () => {
    const world = makeWorld();
    const variants = ['leftAlignedWith', 'rightAlignedWith', 'topAlignedWith', 'bottomAlignedWith'];
    for (const variant of variants) {
      const formula = predicate(variant, [varRef('a'), varRef('b')]);
      const domains = new Map<string, DomainValue>([
        ['.a', {
          domainId: 'dom_a',
          subjectIds: new Uint32Array([1]),
          provenance: 'elements(.a)',
          closed: true,
        }],
        ['.b', {
          domainId: 'dom_b',
          subjectIds: new Uint32Array([2]),
          provenance: 'elements(.b)',
          closed: true,
        }],
      ]);

      const input: LogicEngineInput = {
        formula: forall([
          { vars: ['a'], domain: domainRef('elements', '.a') },
          { vars: ['b'], domain: domainRef('elements', '.b') },
        ], formula),
        world,
        resolver: makeResolver(domains),
      };

      const result = evaluateLogic(input);
      // Elements 1 (0,0,100,40) and 2 (110,50,210,90) are not aligned
      // on any side, so all directional alignments should produce determinate
      // false results (not IMH_FEATURE_NOT_YET_IMPLEMENTED).
      assert.strictEqual(result.passed, false, `Expected ${variant} to evaluate, not return NYI`);
      assert.strictEqual(result.formulaResults.length, 1);
      assert.strictEqual(result.formulaResults[0].outcome, 'fail');
    }
  });
});

// ---------------------------------------------------------------------------
// Universal Quantification Tests
// ---------------------------------------------------------------------------

describe('universal quantification', () => {
  it('passes when all elements satisfy predicate', () => {
    const world = makeWorld();
    // All three subjects have width >= 50 (100, 100, 100).
    const formula = predicate('atLeast', [varRef('btn')]);
    const domains = new Map<string, DomainValue>([
      ['.button', {
        domainId: 'dom_1',
        subjectIds: new Uint32Array([1, 2, 3]),
        provenance: 'elements(.button)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([{ vars: ['btn'], domain: domainRef('elements', '.button') }], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true);
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
  });

  it('fails on first violating element and short-circuits', () => {
    const world = makeWorld();
    // We need a predicate that will fail for some subjects.
    // Use inside: subject 1 [0,0,100,40] is NOT inside subject 2 [110,50,210,90].
    const formula = predicate('inside', [varRef('btn'), varRef('container')]);
    const domains = new Map<string, DomainValue>([
      ['.button', {
        domainId: 'dom_btn',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.button)',
        closed: true,
      }],
      ['.container', {
        domainId: 'dom_container',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.container)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['btn'], domain: domainRef('elements', '.button') },
        { vars: ['container'], domain: domainRef('elements', '.container') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, false);
    assert.strictEqual(result.formulaResults[0].outcome, 'fail');
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-forall-failure'));
  });

  it('is vacuously true over empty domain', () => {
    const world = makeWorld();
    const formula = predicate('width', [varRef('btn')]);
    const domains = new Map<string, DomainValue>([
      ['.button', {
        domainId: 'dom_1',
        subjectIds: new Uint32Array([]),
        provenance: 'elements(.button)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([{ vars: ['btn'], domain: domainRef('elements', '.button') }], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true);
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-forall-vacuous'));
    assert.ok(
      result.diagnostics.some((d) => d.code === 'IMH_LOGIC_VACUOUS_FORALL'),
      'Should emit vacuous forall diagnostic',
    );
    assert.ok(
      result.diagnostics.some((d) => d.message.includes('vacuously true')),
      'Diagnostic message should mention vacuous truth',
    );
  });
});

// ---------------------------------------------------------------------------
// Existential Quantification Tests
// ---------------------------------------------------------------------------

describe('existential quantification', () => {
  it('finds a witness when one exists', () => {
    const world = makeWorld();
    // Subject 1 is inside subject 3 [220,100,320,140]? No.
    // But subject 2 [110,50,210,90] is inside subject 3 [220,100,320,140]? No.
    // Let's make subject 1 inside a larger container.
    const customWorld = makeWorld({
      boxes: {
        ...makeWorld().boxes,
        borderLeft: [10, 110, 0],
        borderTop: [10, 50, 0],
        borderRight: [50, 150, 200],
        borderBottom: [30, 80, 150],
      },
    });

    // Subject 1 [10,10,50,30] is inside subject 3 [0,0,200,150].
    const formula = predicate('inside', [varRef('item'), varRef('container')]);
    const domains = new Map<string, DomainValue>([
      ['.item', {
        domainId: 'dom_item',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.item)',
        closed: true,
      }],
      ['.container', {
        domainId: 'dom_container',
        subjectIds: new Uint32Array([3]),
        provenance: 'elements(.container)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: exists([
        { vars: ['item'], domain: domainRef('elements', '.item') },
        { vars: ['container'], domain: domainRef('elements', '.container') },
      ], formula),
      world: customWorld,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true);
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-exists-witness'));
  });

  it('fails when no witness exists', () => {
    const world = makeWorld();
    // Subject 1 [0,0,100,40] is NOT inside subject 2 [110,50,210,90].
    const formula = predicate('inside', [varRef('item'), varRef('container')]);
    const domains = new Map<string, DomainValue>([
      ['.item', {
        domainId: 'dom_item',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.item)',
        closed: true,
      }],
      ['.container', {
        domainId: 'dom_container',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.container)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: exists([
        { vars: ['item'], domain: domainRef('elements', '.item') },
        { vars: ['container'], domain: domainRef('elements', '.container') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, false);
    assert.strictEqual(result.formulaResults[0].outcome, 'fail');
  });

  it('is false over empty domain', () => {
    const world = makeWorld();
    const formula = predicate('width', [varRef('btn')]);
    const domains = new Map<string, DomainValue>([
      ['.button', {
        domainId: 'dom_1',
        subjectIds: new Uint32Array([]),
        provenance: 'elements(.button)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: exists([{ vars: ['btn'], domain: domainRef('elements', '.button') }], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, false);
    assert.strictEqual(result.formulaResults[0].outcome, 'fail');
    assert.ok(
      result.diagnostics.some((d) => d.code === 'IMH_LOGIC_EMPTY_DOMAIN_EXISTS'),
      'Should emit empty domain exists diagnostic',
    );
    assert.ok(
      result.diagnostics.some((d) => d.message.includes('empty domain')),
      'Diagnostic message should mention empty domain',
    );
  });
});

// ---------------------------------------------------------------------------
// Boolean Connective Tests
// ---------------------------------------------------------------------------

describe('boolean connectives', () => {
  it('And passes when both sides pass', () => {
    const world = makeWorld();
    const p = predicate('leftOf', [varRef('a'), varRef('b')]);
    const q = predicate('above', [varRef('a'), varRef('b')]);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const formula = forall([
      { vars: ['a'], domain: domainRef('elements', '.a') },
      { vars: ['b'], domain: domainRef('elements', '.b') },
    ], and(p, q));

    const result = evaluateLogic({ formula, world, resolver: makeResolver(domains) });
    assert.strictEqual(result.passed, true);
  });

  it('And fails when left side fails', () => {
    const world = makeWorld();
    // Subject 1 is NOT inside subject 2.
    const p = predicate('inside', [varRef('a'), varRef('b')]);
    const q = predicate('leftOf', [varRef('a'), varRef('b')]);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const formula = forall([
      { vars: ['a'], domain: domainRef('elements', '.a') },
      { vars: ['b'], domain: domainRef('elements', '.b') },
    ], and(p, q));

    const result = evaluateLogic({ formula, world, resolver: makeResolver(domains) });
    assert.strictEqual(result.passed, false);
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-and-short-circuit'));
  });

  it('Or passes when left side passes', () => {
    const world = makeWorld();
    // Subject 1 is leftOf subject 2 (true) OR inside subject 2 (false).
    const p = predicate('leftOf', [varRef('a'), varRef('b')]);
    const q = predicate('inside', [varRef('a'), varRef('b')]);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const formula = forall([
      { vars: ['a'], domain: domainRef('elements', '.a') },
      { vars: ['b'], domain: domainRef('elements', '.b') },
    ], or(p, q));

    const result = evaluateLogic({ formula, world, resolver: makeResolver(domains) });
    assert.strictEqual(result.passed, true);
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-or-short-circuit'));
  });

  it('Or fails when both sides fail', () => {
    const world = makeWorld();
    const p = predicate('inside', [varRef('a'), varRef('b')]);
    const q = predicate('inside', [varRef('b'), varRef('a')]);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const formula = forall([
      { vars: ['a'], domain: domainRef('elements', '.a') },
      { vars: ['b'], domain: domainRef('elements', '.b') },
    ], or(p, q));

    const result = evaluateLogic({ formula, world, resolver: makeResolver(domains) });
    assert.strictEqual(result.passed, false);
  });

  it('Not inverts the outcome', () => {
    const world = makeWorld();
    const p = predicate('inside', [varRef('a'), varRef('b')]);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    // NOT inside(a, b) should pass because inside(a, b) is false.
    const formula = forall([
      { vars: ['a'], domain: domainRef('elements', '.a') },
      { vars: ['b'], domain: domainRef('elements', '.b') },
    ], not(p));

    const result = evaluateLogic({ formula, world, resolver: makeResolver(domains) });
    assert.strictEqual(result.passed, true);
  });

  it('Implies is vacuously true when antecedent is false', () => {
    const world = makeWorld();
    // inside(a, b) is false, so implies(false, anything) is true.
    const antecedent = predicate('inside', [varRef('a'), varRef('b')]);
    const consequent = predicate('leftOf', [varRef('a'), varRef('b')]);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const formula = forall([
      { vars: ['a'], domain: domainRef('elements', '.a') },
      { vars: ['b'], domain: domainRef('elements', '.b') },
    ], implies(antecedent, consequent));

    const result = evaluateLogic({ formula, world, resolver: makeResolver(domains) });
    assert.strictEqual(result.passed, true);
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-implies-vacuous'));
  });

  it('Implies fails when antecedent is true and consequent is false', () => {
    const world = makeWorld();
    // leftOf(a, b) is true, but inside(a, b) is false.
    const antecedent = predicate('leftOf', [varRef('a'), varRef('b')]);
    const consequent = predicate('inside', [varRef('a'), varRef('b')]);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const formula = forall([
      { vars: ['a'], domain: domainRef('elements', '.a') },
      { vars: ['b'], domain: domainRef('elements', '.b') },
    ], implies(antecedent, consequent));

    const result = evaluateLogic({ formula, world, resolver: makeResolver(domains) });
    assert.strictEqual(result.passed, false);
  });
});

// ---------------------------------------------------------------------------
// Diagnostic and Proof Tests
// ---------------------------------------------------------------------------

describe('diagnostics and proofs', () => {
  it('produces proofs for every evaluated formula', () => {
    const world = makeWorld();
    const formula = predicate('width', [varRef('btn')]);
    const domains = new Map<string, DomainValue>([
      ['.button', {
        domainId: 'dom_1',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.button)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([{ vars: ['btn'], domain: domainRef('elements', '.button') }], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.ok(result.proofs.length > 0);
    assert.ok(result.proofs[0].proofId.startsWith('proof_'));
    assert.strictEqual(result.proofs[0].clauseId.startsWith('formula_'), true);
  });

  it('produces trace events for evaluation phases', () => {
    const world = makeWorld();
    const formula = predicate('width', [varRef('btn')]);
    const domains = new Map<string, DomainValue>([
      ['.button', {
        domainId: 'dom_1',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.button)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([{ vars: ['btn'], domain: domainRef('elements', '.button') }], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.ok(result.trace.length > 0);
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-logic-start'));
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-logic-end'));
    assert.ok(result.trace.some((t) => t.phase === 'evaluate-forall-start'));
  });

  it('reports failing assignments for forall failures', () => {
    const world = makeWorld();
    const formula = predicate('inside', [varRef('btn'), varRef('container')]);
    const domains = new Map<string, DomainValue>([
      ['.button', {
        domainId: 'dom_btn',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.button)',
        closed: true,
      }],
      ['.container', {
        domainId: 'dom_container',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.container)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['btn'], domain: domainRef('elements', '.button') },
        { vars: ['container'], domain: domainRef('elements', '.container') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, false);
    assert.ok(result.failingAssignments);
    assert.ok(result.failingAssignments!.length > 0);
    // The failing assignment should include the bound variables.
    const firstFailure = result.failingAssignments![0];
    assert.ok('btn' in firstFailure || 'container' in firstFailure);
  });
});