IR V5: Predicates compile, and both engines agree

[afogel]

Fifth slice of the Normative IR (docs/shaping/normative-ir-slices.md §V5), stacked on #42. This is where the shaping doc's two open spikes, X1 (fact vocabulary) and X2 (predicate language and compiler), were executed as the slice.

Demo: bun run ir compile turns twenty-one IR predicates into ir/dist/rules.dl (published Soufflé program) and ir/.build/rules.json (the evaluator's rule set). bun run ir differential runs both engines over the same fixtures: identical violation sets, 0 on the conformant session and 24 on the violating one. A deliberately weakened rule turns the check red and prints the four tuples only one engine derived. Captured output and the design record are in ir/slices/v5/README.md.

What it delivers

• The fact vocabulary (S7). ir/vocabulary/relations.yaml: 44 relations over symbol and number, each tagged by source (wire, external, guardian-state, deployment, static). Static relations carry the spec's fixed tables (the §6 required-fields column, the DEFER reason enum, the trust ranking) and ship inside the program. The external-fact boundary (E7.1) is derived per provision from the relations a predicate touches, not authored.
• The predicate language. Datalog rules as strings in the record: atoms, not, the six comparators, Var = expr, cat/to_string, and count. A violation(subject..., witness...) head plus helpers. Nothing more, because every construct is emitted twice and held equivalent.
• The compiler (N31, N32, N36). Types every variable against the vocabulary, infers helper types to a fixpoint, rejects unsafe rules, stratifies by SCC and refuses negation inside a cycle, and enforces that the violation head is exactly subject then witness, both non-empty. A testable Requirement with neither a predicate nor a declared inexpressible reason does not compile (R3.1, R3.6).
• Two targets, one authority (R3.3). emitSouffleProgram() writes the .dl an auditor runs with stock Soufflé 2.5; rules.json feeds the semi-naive evaluator, which runs with no Soufflé install (R3.9). Both produce the unified violation(provision, subject, witness).
• The differential oracle (N63, R3.8). Both engines over ir/test/conformance/fixtures/{conformant,violating}, each held to the fixture's expected.tsv so two engines cannot agree on a wrong answer. CI installs the pinned 2.5 .deb (SHA-256 verified) in its own job; locally SOUFFLE=/path bun run ir differential.
• Results on the 28 provisions: 21 compiled, 1 alias (ACS-REQ-0024 through the provision it restates), 1 permission, 1 non-testable, 4 non-Requirements. Inexpressible: zero on these specimens. The test-coverage table (U14) is now populated: 24 of 28 provisions are cited by a fixture.

Decisions

• normalizeTrace() (N41) moves to V6 beside N42/N43, because wire relations are only useful once the external facts they join with exist; V5's fixtures are hand-authored .facts, which is what the differential needs regardless.
• The recursive lineage closure carries the path in its witness and assumes a DAG.
• invariants.tla (S15) is emitted and unread, per the shaping doc's non-goals.

Verification

• bun run typecheck passes; bun test ir: 161 tests pass, with Soufflé present (differential tests ran against the real binary here).
• bun run ir compile --check, render --check, lint, differential: all green.

🤖 Generated with Claude Code

https://claude.ai/code/session_01BX56nQPAsqYihopWfWy1xm

[github-actions]

Normative impact (ACS 0.1.2 at 6fce2a0)

No failures, nothing to review.

Changed provisions and their tests (U22)

None.

Added provisions with no conformance test (U23)

None.

Removed provisions missing a tombstone (U24)

None.

Unmarked normative statements (U25)

None.