v1.1.0: pooled runtime, 959 tests, production hardening (0 squash)

2025-08-15 10:00:00 -07:00
commit 92deb689cd
321 changed files with 79170 additions and 0 deletions
@@ -0,0 +1,922 @@
+/**
+ * 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): 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('returns not-yet-implemented for aligned-with variants', () => {
+    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);
+      assert.strictEqual(result.passed, false, `Expected ${variant} to fail`);
+      assert.ok(
+        result.diagnostics.some((d) => d.code === 'IMH_FEATURE_NOT_YET_IMPLEMENTED'),
+        `Expected ${variant} to produce IMH_FEATURE_NOT_YET_IMPLEMENTED`
+      );
+    }
+  });
+});
+
+// ---------------------------------------------------------------------------
+// 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);
+  });
+});