IR V6: The conformance report

.github/workflows/checks.yml

@@ -98,6 +98,14 @@ jobs:
       - name: Verify the published Soufflé program matches the predicates
         if: ${{ !cancelled() }}
         run: bun run ir compile --check
+      - name: Run the conformance report over the generated clean trace
+        # The clean envelope log must pass every compiled provision; a
+        # violation here is a regression in the normalizer, the external
+        # facts, or a predicate, not in the fixture.
+        if: ${{ !cancelled() }}
+        run: |
+          bun run ir/test/fixtures/trace/generate.ts .build-trace clean
+          bun run ir verify .build-trace/trace.jsonl --guardian .build-trace/guardian --deployment .build-trace/deployment --hmac-key .build-trace/hmac-key.hex --quiet > /dev/null
 
   # N62: the differential oracle (R3.8, X4). Soufflé is a CI-only dependency,
   # installed from the official ubuntu-24.04 .deb and never a local

.gitignore

@@ -39,3 +39,6 @@ packages/guardian/tmp-throwing-message-accessor-scratch/
 # S3, the marked copy of the pinned corpus that `acs-ir markers apply` writes
 # for the extractor to read. Regenerated from spec/acs plus ir/markers/overlay.yaml.
 ir/.build/
+
+# Scratch trace the checks workflow generates for `acs-ir verify`.
+.build-trace/

docs/shaping/normative-ir-slices.md

@@ -249,6 +249,8 @@ That is R2.6 demonstrated in one command: **a definition or invariant change inv
 | S10 | P1 | store | `ir/.build/external-facts/` — pre-computed crypto, hash, URI, timestamp facts | — | — | → N44 |
 | S13 | P1 | store | `spec/acs/specification/v0.1.0/**.json` — read-only, the 48 schemas cited not restated | — | — | → N43, N26 |
 
+🟡 **Shipped** ([`ir/slices/v6/`](../../ir/slices/v6/README.md)). `acs-ir verify <trace>` over the Guardian's envelope log (or a bare JSON-RPC log): the wire normalized to facts, Ajv over the 44 pinned schemas, JCS, §8.2 chain recomputation and HMAC verification in ordinary code, the evaluator, then profile scoping, modality, and evidence. Eleven verdict kinds, including one the plan did not name, `unevaluated`: a provision whose predicate reads Guardian records, deployment facts or a key the verifier was not given is reported as not evaluated with the missing relation named, never as a pass. On the generated traces: the clean one passes all 21 compiled provisions; the violating one fails the nine it breaches, with evidence. `ask_resolved` moved to guardian-state, since Guardian-to-Approver traffic is not in the Observed Agent's log.
+
 **The rosters are the point, not padding.** A conformance report that silently omits what it cannot check is a report that overstates its own coverage. U18 and U34 make the two kinds of silence distinguishable: *"required, but no trace can falsify it"* (§12.2's prompt rules) versus *"ACS deliberately requires nothing here"* (§14's multi-tenant isolation). R4.4 and R4.8 exist so neither becomes a dropped row.
 
 **The four-layer split is complete at this slice.** N43 carries JSON Schema, N44 (V5) carries Datalog, N42 carries ordinary code, N45/N46 carry the scoping layer the source's table did not name.

ir/README.md

@@ -18,6 +18,7 @@ bun run ir extract           # writes ir/manifest/provisions.json from the marke
 bun run ir render            # writes ir/dist/provision-index.md from manifest + records
 bun run ir lint              # spec-lint: failures by rule, records needing review, the migration worklist; exits 1 on either
 bun run ir compile           # predicates -> ir/dist/rules.dl (Soufflé), ir/.build/rules.json (evaluator), invariants.tla
+bun run ir verify t.jsonl    # conformance report over an envelope log; add --guardian, --deployment, --hmac-key for the external facts
 bun run ir verify --facts d  # in-process evaluator over a directory of .facts; prints unified violations
 bun run ir differential      # both engines over ir/test/conformance/fixtures; SOUFFLE=/path enables the oracle locally
 bun run ir ids next REQ      # allocates the next ACS-REQ-NNNN and bumps the counter
@@ -62,8 +63,10 @@ When the spec changes under a provision, `lint` names it and everything downstre
 | `src/catalog/staleness.ts` | code | N16 to N18: needs-review from a changed text, a changed dependency, or a changed canonical restatement; the migration worklist. |
 | `src/catalog/test-citations.ts` | code | Which conformance tests cite which IDs (empty until V5). |
 | `src/compile/` | code | N30 the vocabulary, the predicate parser, N31/N32/N36 the compiler, N34 the Soufflé emitter, N33 the TLA+ list. |
-| `src/verify/` | code | N44 the semi-naive evaluator, S9 fact files, N63 the differential oracle. |
-| `src/render/` | code | N52 the census report, N50 the provision index, U9 the lint report, U10/U32 the stale list and worklist, N27 the impact comment, the compile summary and U31. |
+| `src/verify/` | code | N41 the trace normalizer, N42 the ordinary-code facts (JCS, chain hashes, HMAC), N43 Ajv over the pinned schemas, N44 the semi-naive evaluator, N45 to N47 verdicts, S9 fact files, N63 the differential oracle. |
+| `test/fixtures/trace/generate.ts` | code | Generates the clean and violating envelope logs, with a Guardian dump and deployment facts, that `verify` is tested against. |
+| `.build/conformance-report.md` | generated, ignored | The report `acs-ir verify <trace>` last produced (P3). |
+| `src/render/` | code | N52 the census report, N50 the provision index, U9 the lint report, U10/U32 the stale list and worklist, N27 the impact comment, the compile summary and U31, N51 the conformance report. |
 | `src/main.ts` | code | The `acs-ir` command line. |
 | `test/` | tests | Unit tests on a fixture corpus, plus the pinned corpus held to the survey's reference numbers. |
 
@@ -76,4 +79,5 @@ When the spec changes under a provision, `lint` names it and everything downstre
 | V3 | shipped | Staleness propagates: a changed concept page names the unchanged Requirements that depend on it. |
 | V4 | shipped | The spec PR polices itself: spec-lint against a baseline, and the normative-impact comment. |
 | V5 | shipped | Twenty-one predicates compiled to Soufflé and to the in-process evaluator; both engines agree over shared fixtures. |
-| V6 to V8 | planned | The conformance report over an envelope log, the full conversion, upstreaming. |
+| V6 | shipped | The conformance report over an envelope log: verdicts with evidence, scoped to negotiated profiles, rosters printed. |
+| V7, V8 | planned | The full conversion of all 197 unbound occurrences; upstreaming the markers. |

ir/dist/rules.dl

@@ -37,8 +37,6 @@
 .input chain_hash_published(IO=file, filename="chain_hash_published.facts", delimiter="\t")
 .decl client_version(session:symbol, version:symbol)
 .input client_version(IO=file, filename="client_version.facts", delimiter="\t")
-.decl ask_resolved(seq:number, session:symbol, approver:symbol)
-.input ask_resolved(IO=file, filename="ask_resolved.facts", delimiter="\t")
 .decl chain_mismatch_observed(session:symbol, seq:number)
 .input chain_mismatch_observed(IO=file, filename="chain_mismatch_observed.facts", delimiter="\t")
 .decl entry_hash_recomputed(entry_id:symbol, hash:symbol)
@@ -69,6 +67,8 @@
 .input archive_preserved(IO=file, filename="archive_preserved.facts", delimiter="\t")
 .decl approver_verified(session:symbol, approver:symbol)
 .input approver_verified(IO=file, filename="approver_verified.facts", delimiter="\t")
+.decl ask_resolved(seq:number, session:symbol, approver:symbol)
+.input ask_resolved(IO=file, filename="ask_resolved.facts", delimiter="\t")
 .decl session_batching(session:symbol, support:symbol)
 .input session_batching(IO=file, filename="session_batching.facts", delimiter="\t")
 .decl defer_bound(session:symbol, bound:number)

ir/package.json

@@ -15,5 +15,9 @@
   "devDependencies": {
     "bun-types": "^1.3.14",
     "typescript": "^7.0.2"
+  },
+  "dependencies": {
+    "ajv": "^8.20.0",
+    "ajv-formats": "^3.0.1"
   }
 }

ir/slices/v6/README.md

@@ -0,0 +1,80 @@
+# V6: The conformance report
+
+**Demo:** `bun run ir verify <trace.jsonl> --guardian <dir> --deployment <dir> --hmac-key <hex>` emits a W3C-style conformance report over an envelope log: per-provision verdicts with the facts that witness each violation, scoped to the profiles the session negotiated, with the non-testable roster and the exclusion roster printed rather than omitted, and an unexercised `MAY` producing no verdict.
+
+**Master doc:** [`docs/shaping/normative-ir-slices.md`](../../../docs/shaping/normative-ir-slices.md) §V6, authoritative for this slice's scope.
+
+**Affordances:** U6, U11, U15, U16, U17, U18, U34, N40, N41 (from V5), N42, N43, N45, N46, N47, N51, S10, S13. Defined in [Detail E](../../../docs/shaping/normative-ir-shaping.md#detail-e-affordances).
+
+**Stacked on V5.**
+
+## The demo, captured
+
+Two envelope logs generated by `ir/test/fixtures/trace/generate.ts` (generated, not committed, so their chain hashes and HMAC signatures are always the ones the code computes). The clean one:
+
+```
+## Summary (U11)
+
+pass 21, not-exercised 1, permission 1, non-testable 1, exclusion 1, invariant 1, definition 2.
+
+| profile | active obligations | met | unmet | unevaluated |
+|---|---|---|---|---|
+| acs-core | 19 | 19 | 0 | 0 |
+| acs-provenance | 3 | 3 | 0 | 0 |
+```
+
+The violating one, which breaches nine provisions on purpose:
+
+```
+## Summary (U11)
+
+fail 9, pass 12, not-exercised 1, permission 1, non-testable 1, exclusion 1, invariant 1, definition 2.
+
+| profile | active obligations | met | unmet | unevaluated |
+|---|---|---|---|---|
+| acs-core | 19 | 11 | 8 | 0 |
+| acs-provenance | 3 | 2 | 1 | 0 |
+
+### ACS-REQ-0010: agent_generated trust is the minimum over its lineage
+
+1 violation(s).
+
+- subject Seq=11, Pid=p3; witness Ancestor=p2, Path=p3<-p2, Level=trusted, AncestorLevel=untrusted
+  - provenance(11, 0f8fad5b-..., p3, agent_generated)
+  - derived_from(11, p3, p2)
+  - trust(11, p3, trusted)
+```
+
+The same violating log with no key, no Guardian dump and no deployment facts:
+
+```
+fail 7, pass 2, unevaluated 13, permission 1, non-testable 1, exclusion 1, invariant 1, definition 2.
+
+## Not evaluated: facts the verifier was not given
+
+- ACS-REQ-0017 Published chain head is covered by the response signature: needs signature_covers
+- ACS-REQ-0013 entry_hash chain computation: needs context_entry, entry_hash_recomputed
+...
+```
+
+## What this slice delivers
+
+**The four-layer split, complete.** `normalizeTrace()` (N41) restates the wire as facts. `validateSchemas()` (N43) runs Ajv over the 44 pinned schemas, every envelope against its envelope schema and every hook payload against its hook schema, and emits `schema_violation` facts: the JSON-Schema layer, cited by the structural provision (ACS-REQ-0001) and never restated in Datalog (R5). `computeExternalFacts()` (N42) does the work Datalog cannot: RFC 8785 canonicalization, §8.2's `entry_hash` recomputation over `content || raw(previous_hash)`, and HMAC-SHA256 verification over §10's signed input with `signature` removed. The evaluator (N44, V5) derives the violations. Then the scoping layer the source's table did not name: `scopeByProfile()` (N45), `applyModality()` (N46), `attachEvidence()` (N47).
+
+**Every provision gets one of eleven verdicts**, and no verdict is a dropped row: `pass`, `fail`, `not-activated` (the session never negotiated the profile, R4.3), `not-exercised` (the permission the obligation is conditional on was not taken, R4.6), `permission`, `non-testable` and `inexpressible` (listed on the U18 roster, R4.4 and R3.6), `exclusion` (the U34 roster, R4.8), `definition`, `invariant`, and `unevaluated`.
+
+**`unevaluated` is the verdict the slices doc did not have.** Predicates read relations whose source is the Guardian's own records, the deployment's configuration, or a key the verifier holds. When those were not supplied, the provisions that need them are reported as not evaluated, naming the missing relation, rather than passing on an empty relation. The compiler's per-provision external-fact list (E7.1, V5) is what makes this mechanical.
+
+**Evidence (U17, R3.4).** Each violation carries its subject and witness columns by name and the facts from the predicate's relations that mention the subject, so the failure is readable without re-running the verifier.
+
+## Decisions made here
+
+- **The trace format is the Guardian's envelope log**, `{seq, recorded_at, direction, method, rpc_id, envelope}` per line, and also a bare JSON-RPC log (direction from shape, `seq` from line number), so a log from any conformant deployment works. Nothing in `ir/` imports from `packages/`: the format is described here, not shared (R8.2).
+- **The Guardian's records arrive as a dump directory:** `context-entries.jsonl` with full ContextEntry objects (so the §8.2 recomputation has something to recompute) and `facts/<relation>.facts` for the other guardian-state relations. Deployment facts are a directory of `.facts`. A Guardian that wants to be verified against the guardian-state provisions exports this; one that does not is reported as unevaluated on exactly those.
+- **Two vocabulary corrections from building the normalizer.** `ask_resolved` moved from `wire` to `guardian-state`: Guardian-to-Approver traffic is not in the Observed Agent's log. `chain_mismatch_observed` is derived on the wire from `metadata.session_state.chain_hash` against the head the Guardian last published for the session, which the request schema names as the cross-check's location.
+- **Activation conditions stay prose (R4.5).** The ones this catalog needed mechanically are already inside the predicates (`decision(Seq, "defer")`, `archived(Session)`); the prose is carried into the report as text.
+- **A permission that was not exercised is not a pass.** ACS-REQ-0022 reports `not-exercised` when the guardian-state relations it reads are empty, and ACS-REQ-0021 always reports `permission`. Neither counts toward met or unmet.
+
+## Not in this slice
+
+No timestamp-window or URI facts (E7.1 names them; no V2 provision needs them yet). No signature algorithms beyond HMAC-SHA256: an asymmetric signature is reported `unverifiable`, which yields no `signature_status` fact and therefore an honest `unevaluated`. Both arrive with the provisions that need them in V7.