2026-07-31 13:44:06 -07:00
|
|
|
|
/**
|
|
|
|
|
|
* 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 '../../src/ast/DSLCompiler.js';
|
|
|
|
|
|
|
|
|
|
|
|
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', ({ error, errorMessage }) => !error && !errorMessage)
|
|
|
|
|
|
])
|
2026-08-01 09:52:31 -07:00
|
|
|
|
).run({ effort: 600, seed: 'defeasible-semantics' , artifacts: { dir: '', persist: 'never' }});
|
2026-07-31 13:44:06 -07:00
|
|
|
|
|
|
|
|
|
|
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', ({ error, errorMessage }) => !error && !errorMessage)
|
|
|
|
|
|
])
|
2026-08-01 09:52:31 -07:00
|
|
|
|
).run({ effort: 400, seed: 'dsl-runtime-parity' , artifacts: { dir: '', persist: 'never' }});
|
2026-07-31 13:44:06 -07:00
|
|
|
|
|
|
|
|
|
|
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', ({ error, errorMessage }) => !error && !errorMessage)
|
|
|
|
|
|
])
|
2026-08-01 09:52:31 -07:00
|
|
|
|
).run({ effort: 500, seed: 'aggregation-completeness' , artifacts: { dir: '', persist: 'never' }});
|
2026-07-31 13:44:06 -07:00
|
|
|
|
|
|
|
|
|
|
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`);
|
|
|
|
|
|
});
|
|
|
|
|
|
});
|