From f9bd0a132997b7c4fb52c709a9e9a27b6fb9a153 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 14 Sep 2026 18:27:33 +0000 Subject: [PATCH 1/2] Represent RFC 2119 strength as facts and derive verdicts in Datalog MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The judgement moves from TypeScript into the rule program. Each compiled provision's keyword becomes facts (strength, polarity), with the profiles that activate it, the non-wire relations it reads, and whether it is conditional on a permission; the run supplies negotiated(session, profile) and available(relation); nine rules derive fail, deviates, pass, unevaluated, not_activated and not_exercised per session. The published Soufflé program outputs the verdicts and the differential oracle compares them between engines and against expected-verdicts.tsv. A breached SHOULD is now a deviation, counted apart from a failure; 13 of the 69 compiled rules are SHOULDs and were reported as failures before. The keyword is the marked span's first RFC 2119 word. A record states its own, with keyword_basis, where the span has none (nine table cells and list items) or a misleading one: hooks.md's "MAY NOT return DENY", which RFC 2119 does not define, and two tables whose first keyword is a RECOMMENDED beside the MUST the rule checks. The join refuses a permission judged by anything but MAY and an obligation judged by MAY. A conditional provision is exercised when the positive atoms of its rule matched in the session. The old check read the Guardian-state relations a provision uses and treated an empty list as never exercised, so ACS-REQ-0102, which reads wire relations only, could never fail. The rule checker is its own module, shared by the provision compiler and the verdict layer. Fixture envelope.facts now list every seq, which is how a violation keyed by seq is attributed to its session. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01BX56nQPAsqYihopWfWy1xm --- docs/shaping/normative-ir-slices.md | 3 + ir/README.md | 15 +- ir/dist/provision-index.md | 526 ++++++------- ir/dist/rules.dl | 711 +++++++++++++++++- ir/provisions/ACS-REQ-0001.yaml | 2 + ir/provisions/ACS-REQ-0003.yaml | 2 + ir/provisions/ACS-REQ-0005.yaml | 2 + ir/provisions/ACS-REQ-0007.yaml | 2 + ir/provisions/ACS-REQ-0008.yaml | 2 + ir/provisions/ACS-REQ-0009.yaml | 2 + ir/provisions/ACS-REQ-0014.yaml | 2 + ir/provisions/ACS-REQ-0015.yaml | 2 + ir/provisions/ACS-REQ-0061.yaml | 2 + ir/provisions/ACS-REQ-0082.yaml | 2 + ir/provisions/ACS-REQ-0113.yaml | 2 + ir/provisions/ACS-REQ-0135.yaml | 2 + ir/src/catalog/catalog.ts | 73 +- ir/src/compile/compile.ts | 220 +----- ir/src/compile/emit-souffle.ts | 19 +- ir/src/compile/typing.ts | 217 ++++++ ir/src/compile/verdict-layer.ts | 221 ++++++ ir/src/compile/vocabulary.ts | 3 +- ir/src/main.ts | 21 +- ir/src/render/compile.ts | 11 +- ir/src/render/provision-index.ts | 9 +- ir/src/render/report.ts | 21 +- ir/src/verify/differential.ts | 61 +- ir/src/verify/evaluate.ts | 32 +- ir/src/verify/external-facts.ts | 3 + ir/src/verify/normalize-trace.ts | 2 + ir/src/verify/verdicts.ts | 125 +-- ir/test/catalog.test.ts | 41 +- ir/test/compile.test.ts | 53 ++ .../conformance/fixtures/conformant/README.md | 4 + .../fixtures/conformant/expected-verdicts.tsv | 88 +++ .../fixtures/conformant/facts/available.facts | 15 + .../fixtures/conformant/facts/envelope.facts | 11 + .../conformant/facts/negotiated.facts | 4 + .../conformance/fixtures/violating/README.md | 4 + .../fixtures/violating/expected-verdicts.tsv | 88 +++ .../fixtures/violating/facts/available.facts | 22 + .../fixtures/violating/facts/envelope.facts | 13 +- .../fixtures/violating/facts/negotiated.facts | 4 + ir/test/differential.test.ts | 18 + ir/test/evaluate.test.ts | 83 +- ir/test/provision-index.test.ts | 2 +- ir/test/staleness.test.ts | 2 + ir/test/verify.test.ts | 22 +- ir/vocabulary/relations.yaml | 14 + 49 files changed, 2217 insertions(+), 588 deletions(-) create mode 100644 ir/src/compile/typing.ts create mode 100644 ir/src/compile/verdict-layer.ts create mode 100644 ir/test/conformance/fixtures/conformant/expected-verdicts.tsv create mode 100644 ir/test/conformance/fixtures/conformant/facts/available.facts create mode 100644 ir/test/conformance/fixtures/conformant/facts/envelope.facts create mode 100644 ir/test/conformance/fixtures/conformant/facts/negotiated.facts create mode 100644 ir/test/conformance/fixtures/violating/expected-verdicts.tsv create mode 100644 ir/test/conformance/fixtures/violating/facts/available.facts create mode 100644 ir/test/conformance/fixtures/violating/facts/negotiated.facts diff --git a/docs/shaping/normative-ir-slices.md b/docs/shaping/normative-ir-slices.md index ccbd896..02838fe 100644 --- a/docs/shaping/normative-ir-slices.md +++ b/docs/shaping/normative-ir-slices.md @@ -233,6 +233,8 @@ That is R2.6 demonstrated in one command: **a definition or invariant change inv **Demo:** `acs-ir verify .acs/envelopes.jsonl` emits a W3C-style conformance report. Per-provision verdicts with the facts that witness each violation. Scoped to the profiles the session actually negotiated, so a `["acs-core"]` session is never judged against ACS-Provenance obligations. An unexercised `MAY` produces no verdict. The non-testable roster and the exclusion roster are printed, not omitted. +🟡 **Revised after V8** ([#48](https://github.com/afogel/ACS_reference_implementation/pull/48), stacked on [#47](https://github.com/afogel/ACS_reference_implementation/pull/47)). The judgement moved from TypeScript into the rule program. Each compiled provision's RFC 2119 keyword is a fact (`strength`, `polarity`), so are the profiles that activate it (`requires_profile`), the non-wire relations it reads (`needs`) and whether it is conditional on a permission; the run supplies `negotiated(session, profile)` and `available(relation)`; nine rules derive `fail`, `deviates`, `pass`, `unevaluated`, `not_activated` and `not_exercised` per session, and the published `.dl` outputs them. A breached SHOULD is a `deviates`, which the report counts apart from `fail`: 13 of the 69 compiled rules are SHOULDs and were reported as failures before. The keyword comes from the marked span's first RFC 2119 word; a record states its own, with a `keyword_basis`, where the span has none (nine table cells and list items) or a misleading one (`MAY NOT`, and two tables whose first keyword is a RECOMMENDED beside the MUST the rule checks). The join refuses a permission judged by anything but MAY and an obligation judged by MAY. Verdicts are per session, folded for the report; a conditional provision is exercised when the positive atoms of its rule matched in the session, which also fixes ACS-REQ-0102, whose exercise the old code read off Guardian-state relations it does not use. The differential oracle compares the verdict relations too (findings row 9). + | # | Place | Component | Affordance | Control | Wires Out | Returns To | |---|-------|-----------|------------|---------|-----------|------------| | U6 | P1 | `ir/verify` | `acs-ir verify ` | invoke | → N40 | — | @@ -602,3 +604,4 @@ Not slice work, but discovered by it and worth reporting to the ACS maintainers | 6 | 🟡 `hooks.md` uses `MAY NOT`, which is not an RFC 2119 term (RFC 2119 defines MAY, and the prohibition is MUST NOT). Read as the prohibition the sentence means | V7, ACS-REQ-0113 | | 7 | 🟡 §10 does not say whether the handshake request is signed; the per-session key is derived from the `session_id` the handshake establishes, so signing it is circular unless a pre-session key exists. The catalog exempts it | V7, ACS-REQ-0081 | | 8 | 🟡 `hooks.md` says a postCompact summary's `derived_from` MUST equal the union of `provenance_id`s of every entry in `entries_compacted`, but `entries_compacted` lists `step_id`s and no wire message ties a `step_id` to a `provenance_id`. A verifier can check the union only from the Guardian's records; the payload could carry the ids it means | V8 follow-up, ACS-REQ-0111 | +| 9 | 🟡 `hooks.md:212` says a Guardian "MAY NOT return DENY" on postCompact. RFC 2119 defines no MAY NOT; the catalog reads it as MUST NOT, which is what the sentence means. Nine other provisions (the §3 response-shape and DEFER-reason cells, `previous_hash`, the deterministic-layer ordering, the version-mismatch outcome, the provenance uniqueness and lineage cells, the AgBOM serialization item) state an obligation with no RFC 2119 word at all; each record now says which keyword it is judged by and why | #48, ACS-REQ-0113 | diff --git a/ir/README.md b/ir/README.md index 0f6bd77..9bfe628 100644 --- a/ir/README.md +++ b/ir/README.md @@ -18,9 +18,9 @@ bun run ir markers patch # the overlay as a git patch against the spec repo: bun run ir extract # writes ir/manifest/provisions.json from the marked corpus 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 compile # predicates and the verdict layer -> 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 one line per violation: provision, subject values, witness values +bun run ir verify --facts d # in-process evaluator over a directory of .facts; prints one line per violation (provision, subject values, witness values), then one per verdict tuple (relation, provision, session) 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 ``` @@ -43,12 +43,12 @@ When the spec changes under a provision, `lint` lists it and everything downstre | `markers/overlay.yaml` | authored | The staging overlay: where each provision's anchor and terminator go, by verbatim quote against the pinned corpus. Retired once markers are merged upstream. | | `ids/counter.yaml`, `ids/tombstones.yaml` | authored via `acs-ir ids next` | Monotonic ID allocation and retired IDs. | | `manifest/provisions.json` | generated | The mechanical half of every provision: id, type, source, line, block type, section slug, level, text, text hash. Written only by `acs-ir extract`. | -| `provisions/.yaml` | authored | The semantic half: actor, profile, activation, modality, evidence class, schema refs, dependencies, restatement, status. One record per provision, joined to the manifest by ID. | +| `provisions/.yaml` | authored | The semantic half: actor, profile, activation, modality, keyword where the marked span has none or a misleading one (with its basis), evidence class, schema refs, dependencies, restatement, status. One record per provision, joined to the manifest by ID. | | `dist/provision-index.md` | generated | The human-readable catalog. | -| `vocabulary/relations.yaml` | authored | The fact vocabulary: every relation a predicate may name, typed, with its source (wire, external, guardian-state, deployment, static). | +| `vocabulary/relations.yaml` | authored | The fact vocabulary: every relation a predicate may name, typed, with its source (wire, external, guardian-state, deployment, static). Two of them, `negotiated` and `available`, describe the run and feed the verdict layer. | | `dist/markers.patch`, `dist/markers-poc.patch` | generated | The overlay as unified diffs against the spec repository: the bulk marker PR's payload and the five-provision proof of concept. Both apply to the pinned checkout; the test suite proves it. | -| `dist/rules.dl` | generated | The published Soufflé program: runnable by an auditor with stock Soufflé 2.5 and a directory of `.facts`. | -| `test/conformance/fixtures//` | authored | `.facts` per relation plus `expected.tsv`, the violations both engines must derive, one per line as provision, subject values, witness values. Cites provision IDs. | +| `dist/rules.dl` | generated | The published Soufflé program: runnable by an auditor with stock Soufflé 2.5 and a directory of `.facts`. It ends with the verdict layer: each compiled provision's RFC 2119 strength, profiles and needs as facts, and the rules that derive `fail`, `deviates`, `pass`, `unevaluated`, `not_activated` and `not_exercised` per session. | +| `test/conformance/fixtures//` | authored | `.facts` per relation plus `expected.tsv`, the violations both engines must derive, one per line as provision, subject values, witness values, and `expected-verdicts.tsv`, the verdict tuples. `negotiated.facts` and `available.facts` describe the run. Cites provision IDs. | | `.build/rules.json`, `.build/invariants.tla` | generated, ignored | The evaluator's rule set and the declared invariant list. | | `.build/marked/` | generated, ignored | The marked copy of the corpus the extractor reads. | | `.build/stale.json`, `.build/lint.json`, `.build/impact.md` | generated, ignored | Provisions needing review and the worklist, the full lint report, and the PR comment, written by `acs-ir lint`. | @@ -66,7 +66,7 @@ When the spec changes under a provision, `lint` lists it and everything downstre | `src/catalog/catalog.ts` | code | Record parsing and the manifest-to-record join. | | `src/catalog/staleness.ts` | code | 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 | The vocabulary, the predicate parser, the compiler, the Soufflé emitter, the TLA+ invariant list. | +| `src/compile/` | code | The vocabulary, the predicate parser, the rule checker, the compiler, the verdict layer, the Soufflé emitter, the TLA+ invariant list. | | `src/verify/` | code | The trace normalizer, the ordinary-code facts (JCS, chain hashes, HMAC), Ajv over the pinned schemas, the semi-naive evaluator, verdicts, fact files, 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 ` last produced. | @@ -86,3 +86,4 @@ When the spec changes under a provision, `lint` lists it and everything downstre | V6 | shipped | The conformance report over an envelope log: verdicts with evidence, scoped to negotiated profiles, rosters printed. | | V7 | shipped | The full conversion: 155 provisions, 34 authored exclusions, zero unbound occurrences; the inexpressible set enumerated. | | V8 | shipped (tooling and drafts) | `markers patch` writes the bulk and proof-of-concept patches; the Discussion and both PR texts are drafted under `slices/v8/`. Posting them upstream is the maintainer's step. | +| Keywords ([#48](https://github.com/afogel/ACS_reference_implementation/pull/48)) | shipped | RFC 2119 strength as facts and the verdicts as rules in both engines: a breached SHOULD is a deviation, not a failure; profile scoping, exercise and evaluability are Datalog; the published program outputs verdicts. | diff --git a/ir/dist/provision-index.md b/ir/dist/provision-index.md index 6cfc1a2..45387bf 100644 --- a/ir/dist/provision-index.md +++ b/ir/dist/provision-index.md @@ -6,7 +6,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. ## Index -| ID | Type | Level | Actor | Profile | Evidence | Modality | Status | Source | Title | +| ID | Type | Keyword | Actor | Profile | Evidence | Modality | Status | Source | Title | |---|---|---|---|---|---|---|---|---|---| | [ACS-DEF-0001](#acs-def-0001) | Definition | — | none | all | not-applicable | definition | active | spec/instrument/specification.md:295 | Signed input | | [ACS-DEF-0002](#acs-def-0002) | Definition | — | none | all | not-applicable | definition | active | concepts/provenance.md:19 | Lineage spans derivation | @@ -15,21 +15,21 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | [ACS-INV-0002](#acs-inv-0002) | Invariant | MUST NOT | none | all | guardian-state | invariant | active | concepts/intent.md:21 | The only conformant path to widen Intent | | [ACS-INV-0003](#acs-inv-0003) | Invariant | MUST NOT | none | all | not-applicable | invariant | active | concepts/identity.md:13 | Three identities are distinct | | [ACS-INV-0004](#acs-inv-0004) | Invariant | MUST NOT | none | all | guardian-state | invariant | active | concepts/trust.md:25 | The rungs do not collapse | -| [ACS-REQ-0001](#acs-req-0001) | Requirement | — | guardian | acs-core | schema | obligation | active | spec/instrument/specification.md:56 | Response shape is a discriminated union | +| [ACS-REQ-0001](#acs-req-0001) | Requirement | MUST | guardian | acs-core | schema | obligation | active | spec/instrument/specification.md:56 | Response shape is a discriminated union | | [ACS-REQ-0002](#acs-req-0002) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:59 | Non-batching Guardian rejects array input with -32600 | -| [ACS-REQ-0003](#acs-req-0003) | Requirement | RECOMMENDED | guardian | acs-core | schema | obligation | active | spec/instrument/specification.md:113 | Required fields per disposition | +| [ACS-REQ-0003](#acs-req-0003) | Requirement | MUST | guardian | acs-core | schema | obligation | active | spec/instrument/specification.md:113 | Required fields per disposition | | [ACS-REQ-0004](#acs-req-0004) | Requirement | MUST | guardian | acs-core | schema | obligation | active | spec/instrument/specification.md:119 | DEFER carries its resolution fields | -| [ACS-REQ-0005](#acs-req-0005) | Requirement | — | guardian | acs-core | schema | obligation | active | spec/instrument/specification.md:119 | DEFER reason vocabulary | +| [ACS-REQ-0005](#acs-req-0005) | Requirement | MUST | guardian | acs-core | schema | obligation | active | spec/instrument/specification.md:119 | DEFER reason vocabulary | | [ACS-REQ-0006](#acs-req-0006) | Requirement | MUST | guardian | acs-core | deployment-config | obligation | active | spec/instrument/specification.md:119 | Cascading deferrals are bounded per session | -| [ACS-REQ-0007](#acs-req-0007) | Requirement | — | observed-agent | acs-core | wire | obligation | active | spec/instrument/specification.md:65 | Handshake precedes any hook traffic | -| [ACS-REQ-0008](#acs-req-0008) | Requirement | — | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:22 | Deterministic layer evaluates before the agent layer | -| [ACS-REQ-0009](#acs-req-0009) | Requirement | — | framework | acs-provenance | wire | obligation | active | spec/instrument/specification.md:179 | derived_from is in-session lineage | +| [ACS-REQ-0007](#acs-req-0007) | Requirement | MUST | observed-agent | acs-core | wire | obligation | active | spec/instrument/specification.md:65 | Handshake precedes any hook traffic | +| [ACS-REQ-0008](#acs-req-0008) | Requirement | MUST | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:22 | Deterministic layer evaluates before the agent layer | +| [ACS-REQ-0009](#acs-req-0009) | Requirement | MUST | framework | acs-provenance | wire | obligation | active | spec/instrument/specification.md:179 | derived_from is in-session lineage | | [ACS-REQ-0010](#acs-req-0010) | Requirement | MUST | framework | acs-provenance | wire | obligation | active | spec/instrument/specification.md:188 | agent_generated trust is the minimum over its lineage | | [ACS-REQ-0011](#acs-req-0011) | Requirement | MUST | framework | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:244 | Framework enforces Intent immutability | | [ACS-REQ-0012](#acs-req-0012) | Requirement | SHOULD | framework | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:244 | Rejected Intent modification is recorded as an audit event | | [ACS-REQ-0013](#acs-req-0013) | Requirement | MUST | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:228 | entry_hash chain computation | -| [ACS-REQ-0014](#acs-req-0014) | Requirement | — | framework | acs-provenance | wire | obligation | active | spec/instrument/specification.md:176 | provenance_id is unique within a session | -| [ACS-REQ-0015](#acs-req-0015) | Requirement | — | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:71 | Version mismatch terminates with UNSUPPORTED_VERSION | +| [ACS-REQ-0014](#acs-req-0014) | Requirement | MUST | framework | acs-provenance | wire | obligation | active | spec/instrument/specification.md:176 | provenance_id is unique within a session | +| [ACS-REQ-0015](#acs-req-0015) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:71 | Version mismatch terminates with UNSUPPORTED_VERSION | | [ACS-REQ-0016](#acs-req-0016) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:254 | Chain head is published on every content-bearing response | | [ACS-REQ-0017](#acs-req-0017) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:254 | Published chain head is covered by the response signature | | [ACS-REQ-0018](#acs-req-0018) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:295 | Verifier recomputes the canonical signed input | @@ -37,10 +37,10 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | [ACS-REQ-0020](#acs-req-0020) | Requirement | SHOULD | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:248 | Chain hash mismatch triggers an audit event | | [ACS-REQ-0021](#acs-req-0021) | Requirement | MAY | guardian | acs-core | not-applicable | permission | active | spec/instrument/specification.md:248 | Guardian may archive above a byte threshold | | [ACS-REQ-0022](#acs-req-0022) | Requirement | MUST | guardian | acs-core | guardian-state | conditional-on-exercise | active | spec/instrument/specification.md:248 | Archival preserves chain_hash, provenance_summary and intent | -| [ACS-REQ-0023](#acs-req-0023) | Requirement | REQUIRED | guardian | acs-core | guardian-state | obligation | active | concepts/agents.md:21 | Approver authentication and identity verification | -| [ACS-REQ-0024](#acs-req-0024) | Requirement | REQUIRED | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:262 | Approver authentication and identity verification (pillar copy) | +| [ACS-REQ-0023](#acs-req-0023) | Requirement | MUST | guardian | acs-core | guardian-state | obligation | active | concepts/agents.md:21 | Approver authentication and identity verification | +| [ACS-REQ-0024](#acs-req-0024) | Requirement | MUST | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:262 | Approver authentication and identity verification (pillar copy) | | [ACS-REQ-0025](#acs-req-0025) | Requirement | MUST NOT | framework | all | non-testable | obligation | active | spec/instrument/specification.md:12 | The agent has no knowledge of hooks | -| [ACS-REQ-0026](#acs-req-0026) | Requirement | OPTIONAL | deployment | acs-provenance | not-applicable | permission | active | spec/instrument/specification.md:183 | The trust enum is optional on the wire | +| [ACS-REQ-0026](#acs-req-0026) | Requirement | MAY | deployment | acs-provenance | not-applicable | permission | active | spec/instrument/specification.md:183 | The trust enum is optional on the wire | | [ACS-REQ-0027](#acs-req-0027) | Requirement | SHOULD | guardian | acs-provenance | wire | obligation | active | spec/conformance.md:61 | Populated trust follows the default channel mapping | | [ACS-REQ-0028](#acs-req-0028) | Requirement | SHOULD | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:59 | Guardians accept batched requests | | [ACS-REQ-0029](#acs-req-0029) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:71 | Unknown fields are ignored | @@ -49,7 +49,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | [ACS-REQ-0032](#acs-req-0032) | Requirement | SHOULD | observed-agent | acs-trace | non-testable | obligation | active | spec/instrument/specification.md:77 | An unguarded session start surfaces on Trace events | | [ACS-REQ-0033](#acs-req-0033) | Requirement | SHOULD | observed-agent | acs-core | wire | obligation | active | spec/instrument/specification.md:77 | The Observed Agent retries the handshake for later sessions | | [ACS-REQ-0034](#acs-req-0034) | Requirement | SHOULD | deployment | acs-core | non-testable | obligation | active | spec/instrument/specification.md:130 | Audience-specific text is composed client-side | -| [ACS-REQ-0035](#acs-req-0035) | Requirement | OPTIONAL | guardian | acs-core | not-applicable | permission | active | spec/instrument/specification.md:131 | policy_version is optional | +| [ACS-REQ-0035](#acs-req-0035) | Requirement | MAY | guardian | acs-core | not-applicable | permission | active | spec/instrument/specification.md:131 | policy_version is optional | | [ACS-REQ-0036](#acs-req-0036) | Requirement | SHOULD | guardian | acs-core | deployment-config | obligation | active | spec/instrument/specification.md:131 | policy_version is populated when replay matters | | [ACS-REQ-0037](#acs-req-0037) | Requirement | MAY | guardian | acs-core | not-applicable | permission | active | spec/instrument/specification.md:131 | A decision may cite several policy references | | [ACS-REQ-0038](#acs-req-0038) | Requirement | SHOULD | deployment | acs-core | non-testable | obligation | active | spec/instrument/specification.md:132 | Consumers switch on reason codes, not prose | @@ -73,12 +73,12 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | [ACS-REQ-0058](#acs-req-0058) | Requirement | MAY | observed-agent | acs-core | not-applicable | permission | active | spec/instrument/specification.md:209 | The Observed Agent may cross-check the chain head | | [ACS-REQ-0059](#acs-req-0059) | Requirement | MAY | deployment | acs-core | not-applicable | permission | active | spec/instrument/specification.md:211 | The chain may initialize implicitly without sessionStart | | [ACS-REQ-0060](#acs-req-0060) | Requirement | SHOULD | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:222 | ContextEntry SHOULD carry request_hash, timestamp and provenance_summary | -| [ACS-REQ-0061](#acs-req-0061) | Requirement | — | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:222 | previous_hash is present on every entry but the first | +| [ACS-REQ-0061](#acs-req-0061) | Requirement | MUST | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:222 | previous_hash is present on every entry but the first | | [ACS-REQ-0062](#acs-req-0062) | Requirement | MUST | guardian | acs-audit | guardian-state | obligation | active | spec/instrument/specification.md:222 | ACS-Audit deployments populate request_hash | | [ACS-REQ-0063](#acs-req-0063) | Requirement | SHOULD | guardian | acs-audit | guardian-state | obligation | active | spec/conformance.md:75 | ACS-Audit entries carry timestamp and provenance_summary | -| [ACS-REQ-0064](#acs-req-0064) | Requirement | OPTIONAL | guardian | acs-core | not-applicable | permission | active | spec/instrument/specification.md:238 | ProvenanceSummary fields are all optional | -| [ACS-REQ-0065](#acs-req-0065) | Requirement | OPTIONAL | deployment | acs-core | not-applicable | permission | active | spec/instrument/specification.md:242 | Intent is optional | -| [ACS-REQ-0066](#acs-req-0066) | Requirement | REQUIRED | framework | acs-core | schema | obligation | active | spec/instrument/specification.md:242 | parser_provenance is required when parsed is present | +| [ACS-REQ-0064](#acs-req-0064) | Requirement | MAY | guardian | acs-core | not-applicable | permission | active | spec/instrument/specification.md:238 | ProvenanceSummary fields are all optional | +| [ACS-REQ-0065](#acs-req-0065) | Requirement | MAY | deployment | acs-core | not-applicable | permission | active | spec/instrument/specification.md:242 | Intent is optional | +| [ACS-REQ-0066](#acs-req-0066) | Requirement | MUST | framework | acs-core | schema | obligation | active | spec/instrument/specification.md:242 | parser_provenance is required when parsed is present | | [ACS-REQ-0067](#acs-req-0067) | Requirement | MUST | framework | acs-core | wire | obligation | active | spec/instrument/specification.md:242 | parser_provenance origin is user_input | | [ACS-REQ-0068](#acs-req-0068) | Requirement | MAY | guardian | acs-core | not-applicable | permission | active | spec/instrument/specification.md:256 | A Guardian may DENY or error on a chain mismatch | | [ACS-REQ-0069](#acs-req-0069) | Requirement | SHOULD | verifier | acs-core | non-testable | obligation | active | spec/instrument/specification.md:256 | A published chain head inconsistent with the chain is an integrity event | @@ -93,8 +93,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | [ACS-REQ-0078](#acs-req-0078) | Requirement | MUST NOT | guardian | acs-core | deployment-config | obligation | active | spec/instrument/specification.md:282 | No ASK to an approver-incapable client | | [ACS-REQ-0079](#acs-req-0079) | Requirement | MUST | guardian | acs-core | deployment-config | obligation | active | spec/instrument/specification.md:282 | ASK is substituted with a fail-closed DEFER or a DENY | | [ACS-REQ-0080](#acs-req-0080) | Requirement | SHOULD | deployment | acs-core | non-testable | obligation | active | spec/instrument/specification.md:287 | Substitution prefers DEFER when recoverable | -| [ACS-REQ-0081](#acs-req-0081) | Requirement | REQUIRED | deployment | acs-core | wire | obligation | active | spec/instrument/specification.md:293 | Every envelope carries a signature | -| [ACS-REQ-0082](#acs-req-0082) | Requirement | RECOMMENDED | deployment | acs-core | wire | obligation | active | spec/instrument/specification.md:303 | The signature algorithm registry | +| [ACS-REQ-0081](#acs-req-0081) | Requirement | MUST | deployment | acs-core | wire | obligation | active | spec/instrument/specification.md:293 | Every envelope carries a signature | +| [ACS-REQ-0082](#acs-req-0082) | Requirement | MUST | deployment | acs-core | wire | obligation | active | spec/instrument/specification.md:303 | The signature algorithm registry | | [ACS-REQ-0083](#acs-req-0083) | Requirement | MUST | guardian | acs-crypto | wire | obligation | active | spec/instrument/specification.md:318 | Hybrid signatures verify both components | | [ACS-REQ-0084](#acs-req-0084) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:322 | Requests outside the skew window are rejected | | [ACS-REQ-0086](#acs-req-0086) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:322 | Duplicate request_id within a session is rejected | @@ -105,7 +105,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | [ACS-REQ-0091](#acs-req-0091) | Requirement | MUST NOT | guardian | acs-core | non-testable | obligation | active | spec/instrument/specification.md:353 | The agent layer has no access to policy code | | [ACS-REQ-0092](#acs-req-0092) | Requirement | MUST | guardian | acs-core | guardian-state | obligation | active | concepts/agents.md:15 | Decisions are logged with reasoning, model identifier, and confidence | | [ACS-REQ-0093](#acs-req-0093) | Requirement | MUST | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:354 | Decisions are logged (pillar copy) | -| [ACS-REQ-0094](#acs-req-0094) | Requirement | OPTIONAL | deployment | acs-core | not-applicable | permission | active | spec/instrument/specification.md:357 | The agent layer is optional | +| [ACS-REQ-0094](#acs-req-0094) | Requirement | MAY | deployment | acs-core | not-applicable | permission | active | spec/instrument/specification.md:357 | The agent layer is optional | | [ACS-REQ-0095](#acs-req-0095) | Requirement | MUST | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:371 | system/ping is always allowed | | [ACS-REQ-0096](#acs-req-0096) | Requirement | MUST NOT | guardian | acs-core | guardian-state | obligation | active | spec/instrument/specification.md:372 | system/ping is not a ContextEntry | | [ACS-REQ-0097](#acs-req-0097) | Requirement | MUST NOT | guardian | acs-core | wire | obligation | active | spec/instrument/specification.md:373 | system/ping needs no signature | @@ -124,7 +124,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | [ACS-REQ-0110](#acs-req-0110) | Requirement | MAY | guardian | acs-core | not-applicable | permission | active | spec/instrument/hooks.md:200 | A Guardian may deny compaction | | [ACS-REQ-0111](#acs-req-0111) | Requirement | MUST | framework | acs-provenance | wire | obligation | active | spec/instrument/hooks.md:210 | A compaction summary carries the union of its inputs' lineage | | [ACS-REQ-0112](#acs-req-0112) | Requirement | MAY | guardian | acs-core | not-applicable | permission | active | spec/instrument/hooks.md:212 | A Guardian may rewrite a compaction summary | -| [ACS-REQ-0113](#acs-req-0113) | Requirement | MAY | guardian | acs-core | wire | obligation | active | spec/instrument/hooks.md:212 | A Guardian does not deny postCompact | +| [ACS-REQ-0113](#acs-req-0113) | Requirement | MUST NOT | guardian | acs-core | wire | obligation | active | spec/instrument/hooks.md:212 | A Guardian does not deny postCompact | | [ACS-REQ-0114](#acs-req-0114) | Requirement | MUST | guardian | acs-core | guardian-state | obligation | active | spec/instrument/hooks.md:212 | The audit chain records the post-compact state | | [ACS-REQ-0116](#acs-req-0116) | Requirement | MAY | guardian | acs-core | not-applicable | permission | active | spec/instrument/hooks.md:252 | A Guardian may deny a skill registration | | [ACS-REQ-0117](#acs-req-0117) | Requirement | MUST NOT | guardian | acs-core | wire | obligation | active | spec/instrument/hooks.md:252 | A denied skill cannot load | @@ -145,11 +145,11 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | [ACS-REQ-0132](#acs-req-0132) | Requirement | MUST NOT | guardian | acs-trace | non-testable | obligation | active | spec/trace/events.md:72 | Trace emission never blocks enforcement | | [ACS-REQ-0133](#acs-req-0133) | Requirement | SHOULD | deployment | acs-core | non-testable | obligation | active | spec/trace/events.md:72 | Trace events are emitted where feasible even without ACS-Trace | | [ACS-REQ-0134](#acs-req-0134) | Requirement | MUST | framework | acs-inspect | wire | obligation | active | spec/conformance.md:46 | ACS-Inspect emits agbom/snapshot before content-bearing hooks | -| [ACS-REQ-0135](#acs-req-0135) | Requirement | — | guardian | acs-inspect | non-testable | obligation | active | spec/conformance.md:49 | ACS-Inspect serializes the AgBOM on request | +| [ACS-REQ-0135](#acs-req-0135) | Requirement | MUST | guardian | acs-inspect | non-testable | obligation | active | spec/conformance.md:49 | ACS-Inspect serializes the AgBOM on request | | [ACS-REQ-0136](#acs-req-0136) | Requirement | MUST | framework | acs-inspect-dynamic | wire | obligation | active | spec/inspect/README.md:63 | ACS-Inspect-Dynamic emits agbom/changed on every mutation | | [ACS-REQ-0137](#acs-req-0137) | Requirement | MUST | guardian | acs-crypto | wire | obligation | active | spec/conformance.md:67 | ACS-Crypto supports ML-DSA-65 | | [ACS-REQ-0138](#acs-req-0138) | Requirement | SHOULD | guardian | acs-crypto | wire | obligation | active | spec/conformance.md:67 | ACS-Crypto supports SLH-DSA-128s | -| [ACS-REQ-0139](#acs-req-0139) | Requirement | OPTIONAL | deployment | acs-crypto | not-applicable | permission | active | spec/conformance.md:67 | Hybrid composites are optional | +| [ACS-REQ-0139](#acs-req-0139) | Requirement | MAY | deployment | acs-crypto | not-applicable | permission | active | spec/conformance.md:67 | Hybrid composites are optional | | [ACS-REQ-0140](#acs-req-0140) | Requirement | MUST | deployment | acs-core | non-testable | obligation | active | spec/inspect/README.md:10 | Inventory-dependent policy requires ACS-Inspect | | [ACS-REQ-0141](#acs-req-0141) | Requirement | SHOULD | framework | acs-inspect | wire | obligation | active | spec/inspect/README.md:42 | Components carry registration_provenance | | [ACS-REQ-0142](#acs-req-0142) | Requirement | MUST | framework | acs-provenance | wire | obligation | active | spec/inspect/README.md:42 | ACS-Provenance components carry registration_provenance | @@ -260,7 +260,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: schema +- Modality: obligation; evidence: schema; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): A schema-shaped table cell with no RFC 2119 word; the response shape is what the pinned schema enforces, and a schema constraint is a MUST. - Schema: `response-envelope.json#/properties/result/oneOf`, `response-envelope.json#/oneOf` - Status: active, since 0.1.0; reviewed against `42b94860cc35` - Note: The prose names the shape; v0.1.2's schema states the constraint a verifier checks: `result` is exactly one of AcsResult or ServerHello, and a response carries `result` or `error`, never both. @@ -273,7 +274,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the Guardian does not support JSON-RPC batching -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `f49085a4e1af` - Note: The other half of §3's batching sentence (Guardians SHOULD accept arrays) is a separate, unmarked SHOULD. @@ -289,7 +290,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: schema +- Modality: obligation; evidence: schema; keyword: MUST +- Keyword MUST stated by the record, not the span (RECOMMENDED): The span is the §6 table body, whose first keyword is RECOMMENDED, the status of `reasoning` on an ALLOW. The obligation the rule checks is the required field per disposition, which the table states without a keyword. - Schema: `response-envelope.json#/$defs/AcsResult/allOf` - Status: active, since 0.1.0; reviewed against `2eee6abd9102` - Note: One provision spanning the five body rows of the §6 table. The span rule handles a table body: the anchor sits in the first cell, the terminator in the last, and `block_type` is the anchor's cell. The text carries the table's pipe syntax; a reviewer reads it as the table. @@ -302,7 +304,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the decision is DEFER -- Modality: obligation; evidence: schema +- Modality: obligation; evidence: schema; keyword: MUST - Schema: `defer-details.json#/required` - Status: active, since 0.1.0; reviewed against `1f8ef3c0ba29` - Note: Finding for upstream: defer-details.json requires reason, resolution_method and resolution_timeout_ms but not timeout_decision, which this sentence says DEFER MUST include (with default deny). A verifier must treat an absent timeout_decision as deny rather than as a schema failure until the schema and the prose agree. @@ -315,7 +317,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the decision is DEFER -- Modality: obligation; evidence: schema +- Modality: obligation; evidence: schema; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): A table cell listing the reason vocabulary with no RFC 2119 word; a closed vocabulary is a MUST on the value. - Schema: `defer-details.json#/properties/reason/enum` - Status: active, since 0.1.0; reviewed against `874f308dd83c` - Note: Keyword-free; the enum is the obligation. @@ -328,7 +331,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `6e5372943ee9` - Note: The bound is deployment-defined, so the verifier needs it as an external fact (V5); what the wire shows is the DEFER count per session. §9.2's substituted DEFERs count toward this bound. @@ -340,7 +343,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): The cell says 'Required' in lowercase, which the keyword scan does not count; it is REQUIRED in RFC 2119's sense. - Status: active, since 0.1.0; reviewed against `2ad1827a2b1a` - Note: Keyword-free (the capital R in Required is prose, not RFC 2119). The V8 demo sentence. @@ -352,7 +356,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): The cell says 'always', which is not an RFC 2119 word; an unconditional ordering rule is a MUST. - Status: active, since 0.1.0; reviewed against `c086c0aaa3a3` - Note: Keyword-free nested list item. Observable only from the Guardian's own decision log (agents.md decision logging) or from metadata.evaluator, never from the request wire. @@ -364,7 +369,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-provenance; activation: provenance_producer: deterministic -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): A field-definition cell with no RFC 2119 word; the in-session lineage constraint is a MUST on the value. - Schema: `provenance.json#/properties/derived_from` - Depends on: [ACS-DEF-0002](#acs-def-0002) - Status: active, since 0.1.0; reviewed against `edaa44057b7f` @@ -378,7 +384,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-provenance; activation: the deployment populates the OPTIONAL trust field -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Depends on: [ACS-DEF-0002](#acs-def-0002), [ACS-REQ-0009](#acs-req-0009) - Status: active, since 0.1.0; reviewed against `41d62d77d341` - Note: Recursive: trust of an agent_generated object is min over the transitive derived_from closure, which is what ACS-DEF-0002 makes transitive. The closure is over (descendant, ancestor) pairs, so it terminates on a derived_from cycle; the witness names the offending ancestor and both levels, and the evidence lists the derived_from facts for the subject. No schema ref: provenance.json says trust is not a v0.1 schema field and implementations that carry it extend the schema, so there is no pointer to pin (there is nothing to cite here). @@ -391,7 +397,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core; activation: the session established an Intent (Intent is OPTIONAL, §8.4) -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Depends on: [ACS-INV-0001](#acs-inv-0001) - Status: active, since 0.1.0; reviewed against `8294e69b2c1a` - Note: Two MUSTs, one obligation: enforce, by ignoring or rejecting. The SHOULD in the same sentence is ACS-REQ-0012. @@ -404,7 +410,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core; activation: the session established an Intent, and a modification attempt was rejected -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: SHOULD - Depends on: [ACS-REQ-0011](#acs-req-0011) - Status: active, since 0.1.0; reviewed against `0e766c4dd46c` - Note: The SHOULD half of §8.4's enforcement sentence, addressed separately from the MUST. @@ -423,7 +429,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Schema: `context-entry.json#/properties/entry_hash`, `context-entry.json#/properties/previous_hash` - Status: active, since 0.1.0; reviewed against `dba9c6d83350` - Note: Spans a paragraph, a three-item list and a closing paragraph. SHA-256 and JCS enter as external facts; the verifier recomputes from the Guardian's entries and compares with the published chain_hash (ACS-REQ-0016). @@ -436,7 +442,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-provenance; activation: provenance_producer: deterministic -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): A field-definition cell with no RFC 2119 word; uniqueness is a MUST on the value. - Schema: `provenance.json#/properties/provenance_id` - Status: active, since 0.1.0; reviewed against `d87eacdf2d22` - Note: Keyword-free table cell. @@ -449,7 +456,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): A cell stating the outcome as fact with no RFC 2119 word; the termination is a MUST on the Guardian. - Status: active, since 0.1.0; reviewed against `98e8b785e760` - Note: Keyword-free. Negotiation: no common acs_version between ClientHello and the Guardian yields -32001. @@ -461,7 +469,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `5eb6235b1a30` - Note: First half of one §8.6 sentence; the second half is ACS-REQ-0017. @@ -473,7 +481,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Depends on: [ACS-DEF-0001](#acs-def-0001), [ACS-REQ-0016](#acs-req-0016) - Status: active, since 0.1.0; reviewed against `e1a36f5dffdd` - Note: Cross-message: the chain_hash the Guardian publishes must fall inside the signed input, which ACS-DEF-0001 fixes as the whole envelope minus signature. @@ -486,7 +494,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Depends on: [ACS-DEF-0001](#acs-def-0001) - Status: active, since 0.1.0; reviewed against `1f18a43a936e` - Note: Vocabulary gap found in V2: the spec's 'verifier' is whichever party checks a signature, so this binds the Observed Agent equally. The actor field holds one value; recorded as guardian with this note until the field can say 'either party'. @@ -499,7 +507,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-provenance; activation: provenance_producer: deterministic -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST - Status: active, since 0.1.0; reviewed against `51168a2c9d2a` - Note: Environmental: no trace can show which code path populated a field. Two sentences, one obligation; listed on the non-testable roster, never dropped. @@ -511,7 +519,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: an Observed Agent's cross-check chain_hash disagrees with the Guardian's computed head -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `ab2d4412fd1c` - Note: SHOULD-level. @@ -523,7 +531,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `a177e8226221` - Note: A permission: not archiving is conformant and yields no verdict. Exercising it activates ACS-REQ-0022. @@ -535,7 +543,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: archival (ACS-REQ-0021) occurred in the session -- Modality: conditional-on-exercise; evidence: guardian-state +- Modality: conditional-on-exercise; evidence: guardian-state; keyword: MUST - Depends on: [ACS-REQ-0021](#acs-req-0021) - Status: active, since 0.1.0; reviewed against `d42401486d28` - Note: The §8.5 type case: an obligation conditional on an implementation choice. @@ -548,7 +556,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the session uses ASK (a non-empty approver_types_supported) -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Status: active, since 0.1.0; reviewed against `b2043534abf5` - Note: The canonical copy, on the concept page (concepts/README.md:33). ACS-REQ-0024 restates it inline in §9. The taxonomy spike notes the callout is a Guardian obligation at concepts altitude. @@ -560,7 +568,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the session uses ASK (a non-empty approver_types_supported) -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Restates: [ACS-REQ-0023](#acs-req-0023) - Status: active, since 0.1.0; reviewed against `2afe3fa652ea` - Note: The pillar's inline restatement of ACS-REQ-0023; on the migration worklist until §9 references the concept page instead. @@ -573,7 +581,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: all -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `3957f333d277` - Note: §1.2 design principle; environmental, listed on the non-testable roster. @@ -585,7 +593,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-provenance -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `fc2d8aedb132` - Note: Populating it activates ACS-REQ-0010 and ACS-REQ-0054. @@ -597,7 +605,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-provenance; activation: the deployment populates the OPTIONAL trust field -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `c60df09f1e38` - Note: The §7.2 table is the static relation default_trust in the vocabulary. agent_generated is excluded: its default is the lineage minimum, ACS-REQ-0010. Overrides (ACS-REQ-0056) would need audit metadata this rule cannot see. @@ -609,7 +617,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `930840a8ade5` - Note: SHOULD-level; the observable breach is a batch answered with -32600. @@ -621,7 +629,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `9b230819cc76` - Note: Binds both parties; recorded as guardian, the same actor gap as ACS-REQ-0018. @@ -633,7 +641,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `1a1bb4354c71` ### ACS-REQ-0031 @@ -644,7 +652,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core; activation: the handshake failed and the startup posture was proceed -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `d4c58251de24` - Note: A handshake with no response and no audit event. @@ -656,7 +664,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-trace -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `98cda73c20d6` - Note: Non-testable: no Trace-event relations in the vocabulary; Trace emission is out of the envelope log. @@ -668,7 +676,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `2cce955a42ab` ### ACS-REQ-0034 @@ -679,7 +687,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `303ff2eb0162` ### ACS-REQ-0035 @@ -690,7 +698,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `064bbfeb73fb` ### ACS-REQ-0036 @@ -701,7 +709,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: replay or ledger-backed policy state matters to the deployment -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `918909651df9` ### ACS-REQ-0037 @@ -712,7 +720,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `9ce46540098e` ### ACS-REQ-0038 @@ -723,7 +731,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `805dc58c32a9` ### ACS-REQ-0039 @@ -734,7 +742,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST NOT - Schema: `modifications.json#/properties/modified_content` - Status: active, since 0.1.0; reviewed against `30ebd035ffdf` @@ -746,7 +754,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `6203ed391766` ### ACS-REQ-0041 @@ -757,7 +765,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Schema: `modifications.json#/properties/redactions` - Status: active, since 0.1.0; reviewed against `7ce33e1a588b` - Note: JSON Pointer ancestry is ordinary code: modification_targets_overlap is computed by the verifier. @@ -770,7 +778,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `646cf8618b1f` - Note: applied means the agent proceeded with the MODIFY; blocked is the conformant outcome. @@ -782,7 +790,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core; activation: a malformed modifications object arrived -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `c08ff72f1d4b` ### ACS-REQ-0045 @@ -793,7 +801,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `d845664065de` ### ACS-REQ-0046 @@ -804,7 +812,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `ac3cdce41840` - Note: Observable half: a non-ALLOW decision the agent recorded as proceeded. Applying MODIFY correctly is not checked. @@ -816,7 +824,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `9e2ddc2e6d29` ### ACS-REQ-0048 @@ -827,7 +835,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `9d4b0dc6e3c1` ### ACS-REQ-0050 @@ -838,7 +846,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `3a4c8fe64956` ### ACS-REQ-0051 @@ -849,7 +857,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `4d42af653d6d` - Note: Observable half: a DENY that arrived and was recorded as proceeded. @@ -861,7 +869,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-provenance; activation: provenance_producer: deterministic -- Modality: obligation; evidence: schema +- Modality: obligation; evidence: schema; keyword: MUST - Status: active, since 0.1.0; reviewed against `335f50c078e3` - Note: The verifier validates hook payloads against the strict *.acs-provenance.json variants when the session negotiated acs-provenance. @@ -873,7 +881,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core -- Modality: obligation; evidence: schema +- Modality: obligation; evidence: schema; keyword: MUST - Schema: `provenance.json#/required` - Status: active, since 0.1.0; reviewed against `70f11405491c` @@ -885,7 +893,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-provenance; activation: the deployment populates the OPTIONAL trust field -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST - Status: active, since 0.1.0; reviewed against `1ba6384f846a` ### ACS-REQ-0055 @@ -896,7 +904,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-provenance; activation: the deployment populates the OPTIONAL trust field -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST - Status: active, since 0.1.0; reviewed against `cd5af29f53be` ### ACS-REQ-0056 @@ -907,7 +915,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-provenance -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `b2fcfcd327b9` ### ACS-REQ-0057 @@ -918,7 +926,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-provenance; activation: the deployment overrides the default channel-to-trust mapping (ACS-REQ-0056) -- Modality: conditional-on-exercise; evidence: guardian-state +- Modality: conditional-on-exercise; evidence: guardian-state; keyword: SHOULD - Depends on: [ACS-REQ-0056](#acs-req-0056) - Status: active, since 0.1.0; reviewed against `2321adbd91b4` @@ -930,7 +938,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `ff368d786ee2` ### ACS-REQ-0059 @@ -941,7 +949,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `02813e67c977` ### ACS-REQ-0060 @@ -952,7 +960,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: SHOULD - Schema: `context-entry.json#/properties/request_hash` - Status: active, since 0.1.0; reviewed against `f66605809a92` - Note: Carries two keywords: the SHOULD, and the ACS-Audit MUST on request_hash, which is ACS-REQ-0062's own sentence inside this one; the span is the list item. @@ -965,7 +973,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): The cell says 'required' in lowercase, which the keyword scan does not count; it is REQUIRED in RFC 2119's sense. - Status: active, since 0.1.0; reviewed against `850d13a22d52` - Note: Keyword-free; the parenthetical requirement. @@ -977,7 +986,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-audit -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Status: active, since 0.1.0; reviewed against `e8311dbcf186` ### ACS-REQ-0063 @@ -988,7 +997,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-audit -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `a07b3a3994a7` ### ACS-REQ-0064 @@ -999,7 +1008,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Schema: `provenance-summary.json#/properties` - Status: active, since 0.1.0; reviewed against `f52a23c60bc3` @@ -1011,7 +1020,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Depends on: [ACS-INV-0001](#acs-inv-0001) - Status: active, since 0.1.0; reviewed against `f33cafc1c510` @@ -1023,7 +1032,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core; activation: an Intent with parsed capabilities is established -- Modality: obligation; evidence: schema +- Modality: obligation; evidence: schema; keyword: MUST - Schema: `hooks/session-start.json#/properties/intent` - Status: active, since 0.1.0; reviewed against `dc5386ddfe74` - Note: The hook schemas carry the conditional as if/then; a failure surfaces at path /intent. @@ -1036,7 +1045,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core; activation: an Intent with parsed capabilities is established -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `206c69b42c1e` ### ACS-REQ-0068 @@ -1047,7 +1056,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `b8b816055697` ### ACS-REQ-0069 @@ -1058,7 +1067,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: verifier; reported against: verifier - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `2a916723ff9a` ### ACS-REQ-0070 @@ -1069,7 +1078,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: approver; reported against: approver - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Schema: `ask-details.json#/properties/approver/properties/type` - Status: active, since 0.1.0; reviewed against `f330b880a32c` @@ -1081,7 +1090,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: approver; reported against: approver - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Restates: [ACS-REQ-0070](#acs-req-0070) - Status: active, since 0.1.0; reviewed against `caaab40fca50` @@ -1093,7 +1102,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: approver; reported against: approver - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `596e6efbbc42` ### ACS-REQ-0073 @@ -1104,7 +1113,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: approver; reported against: approver - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST NOT - Restates: [ACS-REQ-0072](#acs-req-0072) - Status: active, since 0.1.0; reviewed against `bb97ff1a9d0f` @@ -1116,7 +1125,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: approver; reported against: approver - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Depends on: [ACS-INV-0001](#acs-inv-0001) - Status: active, since 0.1.0; reviewed against `a322d44f2534` @@ -1128,7 +1137,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: approver; reported against: approver - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Restates: [ACS-REQ-0074](#acs-req-0074) - Status: active, since 0.1.0; reviewed against `aec341dd89c9` @@ -1144,7 +1153,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: an Approver granted an intent_extension with scope: session -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Status: active, since 0.1.0; reviewed against `809cc111ec9e` - Note: Checks item 2 (the intent_extension ContextEntry). Item 1 is ACS-REQ-0011's territory; item 3, the extension's separate provenance, is not observable in any relation and is a partial coverage flagged here. @@ -1156,7 +1165,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: scope_mode: strict -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST NOT - Restates: [ACS-INV-0002](#acs-inv-0002) - Status: active, since 0.1.0; reviewed against `0033f90eda4b` @@ -1168,7 +1177,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the Guardian determined the client cannot resolve ASK -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `6e4db93c668f` ### ACS-REQ-0079 @@ -1182,7 +1191,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the Guardian determined the client cannot resolve ASK -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `4d14901e605c` - Note: Observable half: a DEFER to an approver-incapable client whose timeout_decision is not deny. Which decisions would have been ASK is not observable. @@ -1194,7 +1203,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `0a70be5bf9c1` ### ACS-REQ-0081 @@ -1205,7 +1214,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `4b280ca6e17a` - Note: system/ping is exempt by §13. The handshake is exempted here because the per-session key is derived with the session_id it establishes; whether it is signed is a question for upstream. @@ -1226,7 +1235,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST +- Keyword MUST stated by the record, not the span (RECOMMENDED): The span is the §10.1 table body, whose first keyword is RECOMMENDED, the status of HMAC-SHA256. The obligation the rule checks is registry membership, which §10's prose states without a keyword ('the algorithm drawn from the registry below'). - Status: active, since 0.1.0; reviewed against `b6d956aea71c` - Note: One provision spanning the §10.1 table body, binding its eleven status keywords. The obligation it yields: an envelope's algorithm is a registered one. @@ -1238,7 +1248,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-crypto -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `5108e7f73d49` ### ACS-REQ-0084 @@ -1249,7 +1259,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `5bce9413e657` - Note: Binds the MUST and the RECOMMENDED default (300000 ms), which the verifier applies when a ServerHello names no window. The window is judged against the Guardian's recorded_at. @@ -1261,7 +1271,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `07a0d586fb4c` ### ACS-REQ-0087 @@ -1272,7 +1282,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `7517d30bb810` - Note: The sliding window is deployment-configured and not modelled; every repeat in the log is reported. @@ -1284,7 +1294,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: none; reported against: none - Profile: all -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST - Status: active, since 0.1.0; reviewed against `12ab230162bb` - Note: A design constraint on the specification itself. @@ -1296,7 +1306,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `270693d65410` ### ACS-REQ-0090 @@ -1307,7 +1317,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the deployment runs an agent evaluation layer -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST - Status: active, since 0.1.0; reviewed against `21410cd29f07` ### ACS-REQ-0091 @@ -1318,7 +1328,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the deployment runs an agent evaluation layer -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `aef6edc5e8ef` ### ACS-REQ-0092 @@ -1329,7 +1339,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Status: active, since 0.1.0; reviewed against `8bc76b31ea9b` - Note: A Guardian obligation at concepts altitude. Confidence is checked only when available, so only reasoning and model_identifier are required. @@ -1341,7 +1351,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the deployment runs an agent evaluation layer -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Restates: [ACS-REQ-0092](#acs-req-0092) - Status: active, since 0.1.0; reviewed against `c1a64dee4730` @@ -1353,7 +1363,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `95107eae27f5` ### ACS-REQ-0095 @@ -1364,7 +1374,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `661fbd40d3c0` ### ACS-REQ-0096 @@ -1375,7 +1385,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `28e65d616669` ### ACS-REQ-0097 @@ -1386,7 +1396,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `fe2e39e5c976` ### ACS-REQ-0098 @@ -1397,7 +1407,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `646597cda451` ### ACS-REQ-0099 @@ -1408,7 +1418,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `88f15dbbea0e` ### ACS-REQ-0100 @@ -1419,7 +1429,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-core -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `ec73112602cc` - Note: A ping that produced an enforcement audit event is the observable breach. @@ -1431,7 +1441,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `4a37e8b58adb` ### ACS-REQ-0102 @@ -1442,7 +1452,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core; activation: the error response carries a data object (ACS-REQ-0101) -- Modality: conditional-on-exercise; evidence: wire +- Modality: conditional-on-exercise; evidence: wire; keyword: SHOULD - Depends on: [ACS-REQ-0101](#acs-req-0101) - Status: active, since 0.1.0; reviewed against `08fc6084dacd` - Note: The per-code fields are not checked. @@ -1455,7 +1465,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `597265257e0d` ### ACS-REQ-0104 @@ -1466,7 +1476,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `7d06ec2f7f89` ### ACS-REQ-0105 @@ -1477,7 +1487,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `56cdac1aac6c` ### ACS-REQ-0106 @@ -1488,7 +1498,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `cb4a6c5a55e1` ### ACS-REQ-0107 @@ -1499,7 +1509,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `472d22d8d80b` ### ACS-REQ-0108 @@ -1510,7 +1520,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `53c10f4701c3` ### ACS-REQ-0109 @@ -1521,7 +1531,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core -- Modality: obligation; evidence: deployment-config +- Modality: obligation; evidence: deployment-config; keyword: MUST - Status: active, since 0.1.0; reviewed against `51de7945faac` ### ACS-REQ-0110 @@ -1532,7 +1542,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `849e3a92b4e3` ### ACS-REQ-0111 @@ -1543,7 +1553,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-provenance -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Depends on: [ACS-DEF-0002](#acs-def-0002) - Status: active, since 0.1.0; reviewed against `d79fbb903a78` - Note: entries_compacted lists step_ids and nothing on the wire ties a step_id to a provenance_id, so the union check reads step_provenance from the Guardian's records; a Guardian that does not supply it leaves this provision unevaluated rather than approximated. Extra derived_from entries are not reported. @@ -1556,7 +1566,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `bdbce7a11430` ### ACS-REQ-0113 @@ -1567,7 +1577,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST NOT +- Keyword MUST NOT stated by the record, not the span (MAY): The sentence says MAY NOT, which RFC 2119 does not define; read as MUST NOT, the prohibition the rule checks. Worth an upstream finding. - Status: active, since 0.1.0; reviewed against `415ba8b6ff4c` - Note: Finding for upstream: MAY NOT is not an RFC 2119 term; read here as the prohibition the sentence means. @@ -1579,7 +1590,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Status: active, since 0.1.0; reviewed against `38b5f512e0dd` ### ACS-REQ-0116 @@ -1590,7 +1601,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `4f444e38e0ef` ### ACS-REQ-0117 @@ -1601,7 +1612,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `0a1b0a62f271` ### ACS-REQ-0118 @@ -1612,7 +1623,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `3bca90127d17` ### ACS-REQ-0119 @@ -1623,7 +1634,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `bc27f422c346` ### ACS-REQ-0120 @@ -1634,7 +1645,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `a8721161dcf6` - Note: Registrations are correlated within the session; a Guardian persists the pair across sessions, which the verifier cannot see. @@ -1646,7 +1657,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `242488e96202` ### ACS-REQ-0122 @@ -1657,7 +1668,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `71c7ed9438a2` ### ACS-REQ-0123 @@ -1668,7 +1679,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `1d04053a843a` ### ACS-REQ-0124 @@ -1679,7 +1690,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-inspect -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `24d227c8494d` ### ACS-REQ-0125 @@ -1690,7 +1701,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `db09f6fa48cf` ### ACS-REQ-0126 @@ -1701,7 +1712,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `55d4831e632c` ### ACS-REQ-0127 @@ -1712,7 +1723,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `541d58f2f8bc` ### ACS-REQ-0128 @@ -1723,7 +1734,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: not-applicable +- Modality: obligation; evidence: not-applicable; keyword: MUST - Status: active, since 0.1.0; reviewed against `7424e248ba41` ### ACS-REQ-0129 @@ -1734,7 +1745,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `41c701804f08` ### ACS-REQ-0130 @@ -1745,7 +1756,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-inspect -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `2acab6478886` ### ACS-REQ-0131 @@ -1760,7 +1771,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-trace -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST - Status: active, since 0.1.0; reviewed against `3d2dff0ace85` - Note: Non-testable: no Trace-event relations in the vocabulary; Trace emission is out of the envelope log. @@ -1772,7 +1783,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-trace -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST NOT - Status: active, since 0.1.0; reviewed against `cf2b26045d5a` - Note: Non-testable: a Trace sink failure is not observable in the envelope log; the disposition it must not change is. @@ -1784,7 +1795,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `a97096ade935` ### ACS-REQ-0134 @@ -1797,7 +1808,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-inspect -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `3440c71e59da` - Note: The stem and its first item. The second item is ACS-REQ-0135. @@ -1809,7 +1820,8 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-inspect -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST +- Keyword MUST stated by the record, not the span (no keyword): An imperative list item with no RFC 2119 word; the conformance page lists it as what a claim of the profile requires, which is a MUST. - Status: active, since 0.1.0; reviewed against `209ec7826a83` - Note: Keyword-free list item under ACS-REQ-0134's stem Non-testable: serialization requests are Guardian-side and not on the wire in v0.1. @@ -1821,7 +1833,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-inspect-dynamic -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `9403b8b8fd95` ### ACS-REQ-0137 @@ -1832,7 +1844,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-crypto -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `cc783b3ba691` - Note: Binds the MUST and the parenthetical RECOMMENDED. Judged from ServerHello's signature_algorithms_supported; profile scoping activates it only for acs-crypto sessions. @@ -1844,7 +1856,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-crypto -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `062726c535ed` ### ACS-REQ-0139 @@ -1855,7 +1867,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-crypto -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `10bff837ec53` ### ACS-REQ-0140 @@ -1866,7 +1878,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-core -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST - Status: active, since 0.1.0; reviewed against `c9feed61920a` ### ACS-REQ-0141 @@ -1877,7 +1889,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-inspect -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: SHOULD - Schema: `agbom/component.json#/properties/registration_provenance` - Status: active, since 0.1.0; reviewed against `c6cadbe68b74` @@ -1889,7 +1901,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-provenance -- Modality: obligation; evidence: wire +- Modality: obligation; evidence: wire; keyword: MUST - Status: active, since 0.1.0; reviewed against `ce96d3240472` ### ACS-REQ-0143 @@ -1900,7 +1912,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-inspect -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `7e75dc82bee9` ### ACS-REQ-0144 @@ -1911,7 +1923,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: deployment; reported against: deployment - Profile: acs-inspect -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `54bda27f5991` ### ACS-REQ-0145 @@ -1922,7 +1934,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-trace -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: MUST - Status: active, since 0.1.0; reviewed against `6fb1cf6e4b10` - Note: Non-testable: no span relations in the vocabulary. @@ -1934,7 +1946,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-trace -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `0670a5350f65` - Note: Non-testable: no span relations in the vocabulary. @@ -1946,7 +1958,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-trace -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `7b1bb47704f2` ### ACS-REQ-0148 @@ -1957,7 +1969,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: framework; reported against: framework - Profile: acs-trace -- Modality: obligation; evidence: non-testable +- Modality: obligation; evidence: non-testable; keyword: SHOULD - Status: active, since 0.1.0; reviewed against `cbd4d4e69103` ### ACS-REQ-0149 @@ -1968,7 +1980,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-trace -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `114502b26f93` ### ACS-REQ-0150 @@ -1979,7 +1991,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: observed-agent; reported against: observed-agent - Profile: acs-trace; activation: the ServerHello advertised a collector endpoint (ACS-REQ-0149) -- Modality: conditional-on-exercise; evidence: non-testable +- Modality: conditional-on-exercise; evidence: non-testable; keyword: SHOULD - Depends on: [ACS-REQ-0149](#acs-req-0149) - Status: active, since 0.1.0; reviewed against `94c2e68548dc` - Note: Non-testable: trace routing is out of the envelope log. @@ -1992,7 +2004,7 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: obligation; evidence: guardian-state +- Modality: obligation; evidence: guardian-state; keyword: MUST - Status: active, since 0.1.0; reviewed against `2172d6bd1998` - Note: A Guardian obligation at concepts altitude, inside the Intent-derivation callout. @@ -2004,12 +2016,12 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. - Actor: guardian; reported against: guardian - Profile: acs-core -- Modality: permission; evidence: not-applicable +- Modality: permission; evidence: not-applicable; keyword: MAY - Status: active, since 0.1.0; reviewed against `c469c7c5a70a` ## Test coverage -27 of 155 provisions are cited by a conformance test or fixture under `ir/test/conformance/`. +85 of 155 provisions are cited by a conformance test or fixture under `ir/test/conformance/`. | ID | Conformance tests | |---|---| @@ -2020,106 +2032,106 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | ACS-INV-0002 | none | | ACS-INV-0003 | none | | ACS-INV-0004 | none | -| ACS-REQ-0001 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0002 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0003 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0004 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0005 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0006 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0007 | fixtures/conformant/README.md, fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0008 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0009 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0010 | fixtures/conformant/README.md, fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0011 | fixtures/conformant/README.md, fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0012 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0013 | fixtures/conformant/README.md, fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0014 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0015 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0016 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0017 | fixtures/conformant/README.md, fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0018 | fixtures/violating/README.md, fixtures/violating/expected.tsv | +| ACS-REQ-0001 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0002 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0003 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0004 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0005 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0006 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0007 | fixtures/conformant/README.md, fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0008 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0009 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0010 | fixtures/conformant/README.md, fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0011 | fixtures/conformant/README.md, fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0012 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0013 | fixtures/conformant/README.md, fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0014 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0015 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0016 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0017 | fixtures/conformant/README.md, fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0018 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | | ACS-REQ-0019 | none | -| ACS-REQ-0020 | fixtures/violating/README.md, fixtures/violating/expected.tsv | +| ACS-REQ-0020 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | | ACS-REQ-0021 | none | -| ACS-REQ-0022 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0023 | fixtures/violating/README.md, fixtures/violating/expected.tsv | +| ACS-REQ-0022 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0023 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | | ACS-REQ-0024 | none | | ACS-REQ-0025 | none | | ACS-REQ-0026 | none | -| ACS-REQ-0027 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0028 | none | +| ACS-REQ-0027 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0028 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0029 | none | -| ACS-REQ-0030 | none | -| ACS-REQ-0031 | none | -| ACS-REQ-0032 | none | +| ACS-REQ-0030 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0031 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0032 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0033 | none | | ACS-REQ-0034 | none | | ACS-REQ-0035 | none | | ACS-REQ-0036 | none | | ACS-REQ-0037 | none | | ACS-REQ-0038 | none | -| ACS-REQ-0039 | none | +| ACS-REQ-0039 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0040 | none | -| ACS-REQ-0041 | none | -| ACS-REQ-0043 | none | +| ACS-REQ-0041 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0043 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0044 | none | | ACS-REQ-0045 | none | -| ACS-REQ-0046 | none | +| ACS-REQ-0046 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0047 | none | | ACS-REQ-0048 | none | -| ACS-REQ-0050 | none | -| ACS-REQ-0051 | none | -| ACS-REQ-0052 | none | -| ACS-REQ-0053 | none | +| ACS-REQ-0050 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0051 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0052 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0053 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0054 | none | | ACS-REQ-0055 | none | | ACS-REQ-0056 | none | | ACS-REQ-0057 | none | | ACS-REQ-0058 | none | | ACS-REQ-0059 | none | -| ACS-REQ-0060 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0061 | none | -| ACS-REQ-0062 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0063 | none | +| ACS-REQ-0060 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0061 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0062 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0063 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0064 | none | | ACS-REQ-0065 | none | -| ACS-REQ-0066 | none | -| ACS-REQ-0067 | none | +| ACS-REQ-0066 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0067 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0068 | none | | ACS-REQ-0069 | none | | ACS-REQ-0070 | none | | ACS-REQ-0071 | none | -| ACS-REQ-0072 | none | +| ACS-REQ-0072 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0073 | none | | ACS-REQ-0074 | none | | ACS-REQ-0075 | none | -| ACS-REQ-0076 | none | -| ACS-REQ-0077 | none | -| ACS-REQ-0078 | none | -| ACS-REQ-0079 | none | +| ACS-REQ-0076 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0077 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0078 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0079 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0080 | none | -| ACS-REQ-0081 | none | -| ACS-REQ-0082 | none | -| ACS-REQ-0083 | none | -| ACS-REQ-0084 | none | -| ACS-REQ-0086 | none | -| ACS-REQ-0087 | none | +| ACS-REQ-0081 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0082 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0083 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0084 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0086 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0087 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0088 | none | | ACS-REQ-0089 | none | | ACS-REQ-0090 | none | | ACS-REQ-0091 | none | -| ACS-REQ-0092 | fixtures/violating/README.md, fixtures/violating/expected.tsv | +| ACS-REQ-0092 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | | ACS-REQ-0093 | none | | ACS-REQ-0094 | none | -| ACS-REQ-0095 | none | -| ACS-REQ-0096 | none | -| ACS-REQ-0097 | none | +| ACS-REQ-0095 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0096 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0097 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0098 | none | | ACS-REQ-0099 | none | -| ACS-REQ-0100 | none | +| ACS-REQ-0100 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0101 | none | -| ACS-REQ-0102 | none | -| ACS-REQ-0103 | none | +| ACS-REQ-0102 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0103 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0104 | none | | ACS-REQ-0105 | none | | ACS-REQ-0106 | none | @@ -2127,44 +2139,44 @@ ACS 0.1.2 at `6fce2a0`. 155 provisions. | ACS-REQ-0108 | none | | ACS-REQ-0109 | none | | ACS-REQ-0110 | none | -| ACS-REQ-0111 | none | +| ACS-REQ-0111 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0112 | none | -| ACS-REQ-0113 | none | -| ACS-REQ-0114 | none | +| ACS-REQ-0113 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0114 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0116 | none | -| ACS-REQ-0117 | none | +| ACS-REQ-0117 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0118 | none | | ACS-REQ-0119 | none | -| ACS-REQ-0120 | none | -| ACS-REQ-0121 | none | +| ACS-REQ-0120 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0121 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0122 | none | | ACS-REQ-0123 | none | -| ACS-REQ-0124 | none | +| ACS-REQ-0124 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0125 | none | | ACS-REQ-0126 | none | | ACS-REQ-0127 | none | | ACS-REQ-0128 | none | | ACS-REQ-0129 | none | -| ACS-REQ-0130 | none | -| ACS-REQ-0131 | none | -| ACS-REQ-0132 | none | +| ACS-REQ-0130 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0131 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0132 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0133 | none | -| ACS-REQ-0134 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0135 | none | -| ACS-REQ-0136 | none | -| ACS-REQ-0137 | none | -| ACS-REQ-0138 | fixtures/violating/README.md, fixtures/violating/expected.tsv | -| ACS-REQ-0139 | none | +| ACS-REQ-0134 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0135 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0136 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0137 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0138 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/README.md, fixtures/violating/expected-verdicts.tsv, fixtures/violating/expected.tsv | +| ACS-REQ-0139 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0140 | none | -| ACS-REQ-0141 | none | -| ACS-REQ-0142 | none | -| ACS-REQ-0143 | none | -| ACS-REQ-0144 | none | -| ACS-REQ-0145 | none | -| ACS-REQ-0146 | none | -| ACS-REQ-0147 | none | -| ACS-REQ-0148 | none | -| ACS-REQ-0149 | none | -| ACS-REQ-0150 | none | -| ACS-REQ-0151 | none | +| ACS-REQ-0141 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0142 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0143 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0144 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0145 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0146 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0147 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0148 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0149 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0150 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | +| ACS-REQ-0151 | fixtures/conformant/expected-verdicts.tsv, fixtures/violating/expected-verdicts.tsv | | ACS-REQ-0152 | none | diff --git a/ir/dist/rules.dl b/ir/dist/rules.dl index 5af0f65..d95ac1a 100644 --- a/ir/dist/rules.dl +++ b/ir/dist/rules.dl @@ -1,7 +1,11 @@ // GENERATED by `acs-ir compile` from ir/provisions/*.yaml over ir/vocabulary/relations.yaml. Do not edit. // ACS 0.1.2 at 6fce2a0. // Run: souffle -F -D rules.dl (Soufflé 2.5; facts are tab-separated, one file per relation; -// the out dir receives one tab-separated __violation.csv per compiled provision) +// the out dir receives one tab-separated __violation.csv per compiled provision, and one +// .csv per verdict relation: fail, deviates, pass, unevaluated, not_activated, not_exercised) +// Two facts files describe the run itself: negotiated.facts lists (session, profile) for every profile each session +// negotiated, and available.facts lists every guardian-state, deployment and external relation whose facts were +// supplied. A relation a provision needs that is not listed there makes the provision unevaluated, never passed. // ---- column domains: a value's kind, as a subtype, so a seq is never joined to a bound ---- .type Algorithm <: symbol @@ -32,10 +36,14 @@ .type Origin <: symbol .type Outcome <: symbol .type Pid <: symbol +.type Polarity <: symbol .type ProducerMode <: symbol +.type Profile <: symbol +.type Provision <: symbol .type Rank <: number .type Reason <: symbol .type ReasonCode <: symbol +.type Relation <: symbol .type RequestId <: symbol .type RpcId <: symbol .type Schema <: symbol @@ -46,6 +54,7 @@ .type Status <: symbol .type StepId <: symbol .type StepType <: symbol +.type Strength <: symbol .type Support <: symbol .type Timestamp <: symbol .type Version <: symbol @@ -67,6 +76,8 @@ .input array_input(IO=file, filename="array_input.facts", delimiter="\t") .decl handshake(seq:Seq, session:Session) .input handshake(IO=file, filename="handshake.facts", delimiter="\t") +.decl negotiated(session:Session, profile:Profile) +.input negotiated(IO=file, filename="negotiated.facts", delimiter="\t") .decl hook(seq:Seq, session:Session, method:Method) .input hook(IO=file, filename="hook.facts", delimiter="\t") .decl defer_field(seq:Seq, field:Field) @@ -95,6 +106,8 @@ .input signature_status(IO=file, filename="signature_status.facts", delimiter="\t") .decl schema_violation(seq:Seq, schema:Schema, path:JsonPath) .input schema_violation(IO=file, filename="schema_violation.facts", delimiter="\t") +.decl available(relation:Relation) +.input available(IO=file, filename="available.facts", delimiter="\t") .decl evaluator_ran(seq:Seq, layer:Layer, order:Order) .input evaluator_ran(IO=file, filename="evaluator_ran.facts", delimiter="\t") .decl context_entry(session:Session, entry_id:EntryId, seq:Seq, entry_hash:EntryHash) @@ -905,3 +918,699 @@ acs_req_0142__violation(Seq, ComponentId, "registration_provenance") :- agbom_co acs_req_0151__violation(Session, Seq, "steps/subagentStart") :- request(Seq, Session, "steps/subagentStart", _, _), !intent_derivation_recorded(Session, Seq, _). // ACS-REQ-0152: permission -- a MAY that was not exercised yields no verdict + +// ---- verdicts: RFC 2119 strength as facts, verdicts as rules ---- + +// what the catalog says about each compiled provision +// Every Requirement in the catalog, compiled or not. +.decl provision(provision:Provision) +provision("ACS-REQ-0001"). +provision("ACS-REQ-0002"). +provision("ACS-REQ-0003"). +provision("ACS-REQ-0004"). +provision("ACS-REQ-0005"). +provision("ACS-REQ-0006"). +provision("ACS-REQ-0007"). +provision("ACS-REQ-0008"). +provision("ACS-REQ-0009"). +provision("ACS-REQ-0010"). +provision("ACS-REQ-0011"). +provision("ACS-REQ-0012"). +provision("ACS-REQ-0013"). +provision("ACS-REQ-0014"). +provision("ACS-REQ-0015"). +provision("ACS-REQ-0016"). +provision("ACS-REQ-0017"). +provision("ACS-REQ-0018"). +provision("ACS-REQ-0019"). +provision("ACS-REQ-0020"). +provision("ACS-REQ-0021"). +provision("ACS-REQ-0022"). +provision("ACS-REQ-0023"). +provision("ACS-REQ-0024"). +provision("ACS-REQ-0025"). +provision("ACS-REQ-0026"). +provision("ACS-REQ-0027"). +provision("ACS-REQ-0028"). +provision("ACS-REQ-0029"). +provision("ACS-REQ-0030"). +provision("ACS-REQ-0031"). +provision("ACS-REQ-0032"). +provision("ACS-REQ-0033"). +provision("ACS-REQ-0034"). +provision("ACS-REQ-0035"). +provision("ACS-REQ-0036"). +provision("ACS-REQ-0037"). +provision("ACS-REQ-0038"). +provision("ACS-REQ-0039"). +provision("ACS-REQ-0040"). +provision("ACS-REQ-0041"). +provision("ACS-REQ-0043"). +provision("ACS-REQ-0044"). +provision("ACS-REQ-0045"). +provision("ACS-REQ-0046"). +provision("ACS-REQ-0047"). +provision("ACS-REQ-0048"). +provision("ACS-REQ-0050"). +provision("ACS-REQ-0051"). +provision("ACS-REQ-0052"). +provision("ACS-REQ-0053"). +provision("ACS-REQ-0054"). +provision("ACS-REQ-0055"). +provision("ACS-REQ-0056"). +provision("ACS-REQ-0057"). +provision("ACS-REQ-0058"). +provision("ACS-REQ-0059"). +provision("ACS-REQ-0060"). +provision("ACS-REQ-0061"). +provision("ACS-REQ-0062"). +provision("ACS-REQ-0063"). +provision("ACS-REQ-0064"). +provision("ACS-REQ-0065"). +provision("ACS-REQ-0066"). +provision("ACS-REQ-0067"). +provision("ACS-REQ-0068"). +provision("ACS-REQ-0069"). +provision("ACS-REQ-0070"). +provision("ACS-REQ-0071"). +provision("ACS-REQ-0072"). +provision("ACS-REQ-0073"). +provision("ACS-REQ-0074"). +provision("ACS-REQ-0075"). +provision("ACS-REQ-0076"). +provision("ACS-REQ-0077"). +provision("ACS-REQ-0078"). +provision("ACS-REQ-0079"). +provision("ACS-REQ-0080"). +provision("ACS-REQ-0081"). +provision("ACS-REQ-0082"). +provision("ACS-REQ-0083"). +provision("ACS-REQ-0084"). +provision("ACS-REQ-0086"). +provision("ACS-REQ-0087"). +provision("ACS-REQ-0088"). +provision("ACS-REQ-0089"). +provision("ACS-REQ-0090"). +provision("ACS-REQ-0091"). +provision("ACS-REQ-0092"). +provision("ACS-REQ-0093"). +provision("ACS-REQ-0094"). +provision("ACS-REQ-0095"). +provision("ACS-REQ-0096"). +provision("ACS-REQ-0097"). +provision("ACS-REQ-0098"). +provision("ACS-REQ-0099"). +provision("ACS-REQ-0100"). +provision("ACS-REQ-0101"). +provision("ACS-REQ-0102"). +provision("ACS-REQ-0103"). +provision("ACS-REQ-0104"). +provision("ACS-REQ-0105"). +provision("ACS-REQ-0106"). +provision("ACS-REQ-0107"). +provision("ACS-REQ-0108"). +provision("ACS-REQ-0109"). +provision("ACS-REQ-0110"). +provision("ACS-REQ-0111"). +provision("ACS-REQ-0112"). +provision("ACS-REQ-0113"). +provision("ACS-REQ-0114"). +provision("ACS-REQ-0116"). +provision("ACS-REQ-0117"). +provision("ACS-REQ-0118"). +provision("ACS-REQ-0119"). +provision("ACS-REQ-0120"). +provision("ACS-REQ-0121"). +provision("ACS-REQ-0122"). +provision("ACS-REQ-0123"). +provision("ACS-REQ-0124"). +provision("ACS-REQ-0125"). +provision("ACS-REQ-0126"). +provision("ACS-REQ-0127"). +provision("ACS-REQ-0128"). +provision("ACS-REQ-0129"). +provision("ACS-REQ-0130"). +provision("ACS-REQ-0131"). +provision("ACS-REQ-0132"). +provision("ACS-REQ-0133"). +provision("ACS-REQ-0134"). +provision("ACS-REQ-0135"). +provision("ACS-REQ-0136"). +provision("ACS-REQ-0137"). +provision("ACS-REQ-0138"). +provision("ACS-REQ-0139"). +provision("ACS-REQ-0140"). +provision("ACS-REQ-0141"). +provision("ACS-REQ-0142"). +provision("ACS-REQ-0143"). +provision("ACS-REQ-0144"). +provision("ACS-REQ-0145"). +provision("ACS-REQ-0146"). +provision("ACS-REQ-0147"). +provision("ACS-REQ-0148"). +provision("ACS-REQ-0149"). +provision("ACS-REQ-0150"). +provision("ACS-REQ-0151"). +provision("ACS-REQ-0152"). +// A provision with compiled rules. +.decl compiled(provision:Provision) +compiled("ACS-REQ-0001"). +compiled("ACS-REQ-0002"). +compiled("ACS-REQ-0003"). +compiled("ACS-REQ-0004"). +compiled("ACS-REQ-0005"). +compiled("ACS-REQ-0006"). +compiled("ACS-REQ-0007"). +compiled("ACS-REQ-0008"). +compiled("ACS-REQ-0009"). +compiled("ACS-REQ-0010"). +compiled("ACS-REQ-0011"). +compiled("ACS-REQ-0012"). +compiled("ACS-REQ-0013"). +compiled("ACS-REQ-0014"). +compiled("ACS-REQ-0015"). +compiled("ACS-REQ-0016"). +compiled("ACS-REQ-0017"). +compiled("ACS-REQ-0018"). +compiled("ACS-REQ-0020"). +compiled("ACS-REQ-0022"). +compiled("ACS-REQ-0023"). +compiled("ACS-REQ-0027"). +compiled("ACS-REQ-0028"). +compiled("ACS-REQ-0030"). +compiled("ACS-REQ-0031"). +compiled("ACS-REQ-0039"). +compiled("ACS-REQ-0041"). +compiled("ACS-REQ-0043"). +compiled("ACS-REQ-0046"). +compiled("ACS-REQ-0050"). +compiled("ACS-REQ-0051"). +compiled("ACS-REQ-0052"). +compiled("ACS-REQ-0053"). +compiled("ACS-REQ-0060"). +compiled("ACS-REQ-0061"). +compiled("ACS-REQ-0062"). +compiled("ACS-REQ-0063"). +compiled("ACS-REQ-0066"). +compiled("ACS-REQ-0067"). +compiled("ACS-REQ-0072"). +compiled("ACS-REQ-0076"). +compiled("ACS-REQ-0077"). +compiled("ACS-REQ-0078"). +compiled("ACS-REQ-0079"). +compiled("ACS-REQ-0081"). +compiled("ACS-REQ-0082"). +compiled("ACS-REQ-0084"). +compiled("ACS-REQ-0086"). +compiled("ACS-REQ-0087"). +compiled("ACS-REQ-0092"). +compiled("ACS-REQ-0095"). +compiled("ACS-REQ-0096"). +compiled("ACS-REQ-0097"). +compiled("ACS-REQ-0100"). +compiled("ACS-REQ-0102"). +compiled("ACS-REQ-0103"). +compiled("ACS-REQ-0111"). +compiled("ACS-REQ-0113"). +compiled("ACS-REQ-0114"). +compiled("ACS-REQ-0117"). +compiled("ACS-REQ-0120"). +compiled("ACS-REQ-0121"). +compiled("ACS-REQ-0130"). +compiled("ACS-REQ-0134"). +compiled("ACS-REQ-0137"). +compiled("ACS-REQ-0138"). +compiled("ACS-REQ-0141"). +compiled("ACS-REQ-0142"). +compiled("ACS-REQ-0151"). +// The provision's RFC 2119 strength: must, should, or may. +.decl strength(provision:Provision, strength:Strength) +strength("ACS-REQ-0001", "must"). +strength("ACS-REQ-0002", "must"). +strength("ACS-REQ-0003", "must"). +strength("ACS-REQ-0004", "must"). +strength("ACS-REQ-0005", "must"). +strength("ACS-REQ-0006", "must"). +strength("ACS-REQ-0007", "must"). +strength("ACS-REQ-0008", "must"). +strength("ACS-REQ-0009", "must"). +strength("ACS-REQ-0010", "must"). +strength("ACS-REQ-0011", "must"). +strength("ACS-REQ-0012", "should"). +strength("ACS-REQ-0013", "must"). +strength("ACS-REQ-0014", "must"). +strength("ACS-REQ-0015", "must"). +strength("ACS-REQ-0016", "must"). +strength("ACS-REQ-0017", "must"). +strength("ACS-REQ-0018", "must"). +strength("ACS-REQ-0020", "should"). +strength("ACS-REQ-0022", "must"). +strength("ACS-REQ-0023", "must"). +strength("ACS-REQ-0027", "should"). +strength("ACS-REQ-0028", "should"). +strength("ACS-REQ-0030", "must"). +strength("ACS-REQ-0031", "must"). +strength("ACS-REQ-0039", "must"). +strength("ACS-REQ-0041", "must"). +strength("ACS-REQ-0043", "must"). +strength("ACS-REQ-0046", "must"). +strength("ACS-REQ-0050", "must"). +strength("ACS-REQ-0051", "must"). +strength("ACS-REQ-0052", "must"). +strength("ACS-REQ-0053", "must"). +strength("ACS-REQ-0060", "should"). +strength("ACS-REQ-0061", "must"). +strength("ACS-REQ-0062", "must"). +strength("ACS-REQ-0063", "should"). +strength("ACS-REQ-0066", "must"). +strength("ACS-REQ-0067", "must"). +strength("ACS-REQ-0072", "must"). +strength("ACS-REQ-0076", "must"). +strength("ACS-REQ-0077", "must"). +strength("ACS-REQ-0078", "must"). +strength("ACS-REQ-0079", "must"). +strength("ACS-REQ-0081", "must"). +strength("ACS-REQ-0082", "must"). +strength("ACS-REQ-0084", "must"). +strength("ACS-REQ-0086", "must"). +strength("ACS-REQ-0087", "should"). +strength("ACS-REQ-0092", "must"). +strength("ACS-REQ-0095", "must"). +strength("ACS-REQ-0096", "must"). +strength("ACS-REQ-0097", "must"). +strength("ACS-REQ-0100", "must"). +strength("ACS-REQ-0102", "should"). +strength("ACS-REQ-0103", "must"). +strength("ACS-REQ-0111", "must"). +strength("ACS-REQ-0113", "must"). +strength("ACS-REQ-0114", "must"). +strength("ACS-REQ-0117", "must"). +strength("ACS-REQ-0120", "must"). +strength("ACS-REQ-0121", "should"). +strength("ACS-REQ-0130", "should"). +strength("ACS-REQ-0134", "must"). +strength("ACS-REQ-0137", "must"). +strength("ACS-REQ-0138", "should"). +strength("ACS-REQ-0141", "should"). +strength("ACS-REQ-0142", "must"). +strength("ACS-REQ-0151", "must"). +// Whether the sentence obliges (MUST, SHOULD) or prohibits (MUST NOT, SHOULD NOT). +.decl polarity(provision:Provision, polarity:Polarity) +polarity("ACS-REQ-0001", "obligation"). +polarity("ACS-REQ-0002", "obligation"). +polarity("ACS-REQ-0003", "obligation"). +polarity("ACS-REQ-0004", "obligation"). +polarity("ACS-REQ-0005", "obligation"). +polarity("ACS-REQ-0006", "obligation"). +polarity("ACS-REQ-0007", "obligation"). +polarity("ACS-REQ-0008", "obligation"). +polarity("ACS-REQ-0009", "obligation"). +polarity("ACS-REQ-0010", "obligation"). +polarity("ACS-REQ-0011", "obligation"). +polarity("ACS-REQ-0012", "obligation"). +polarity("ACS-REQ-0013", "obligation"). +polarity("ACS-REQ-0014", "obligation"). +polarity("ACS-REQ-0015", "obligation"). +polarity("ACS-REQ-0016", "obligation"). +polarity("ACS-REQ-0017", "obligation"). +polarity("ACS-REQ-0018", "obligation"). +polarity("ACS-REQ-0020", "obligation"). +polarity("ACS-REQ-0022", "obligation"). +polarity("ACS-REQ-0023", "obligation"). +polarity("ACS-REQ-0027", "obligation"). +polarity("ACS-REQ-0028", "obligation"). +polarity("ACS-REQ-0030", "obligation"). +polarity("ACS-REQ-0031", "obligation"). +polarity("ACS-REQ-0039", "prohibition"). +polarity("ACS-REQ-0041", "obligation"). +polarity("ACS-REQ-0043", "obligation"). +polarity("ACS-REQ-0046", "obligation"). +polarity("ACS-REQ-0050", "obligation"). +polarity("ACS-REQ-0051", "obligation"). +polarity("ACS-REQ-0052", "obligation"). +polarity("ACS-REQ-0053", "obligation"). +polarity("ACS-REQ-0060", "obligation"). +polarity("ACS-REQ-0061", "obligation"). +polarity("ACS-REQ-0062", "obligation"). +polarity("ACS-REQ-0063", "obligation"). +polarity("ACS-REQ-0066", "obligation"). +polarity("ACS-REQ-0067", "obligation"). +polarity("ACS-REQ-0072", "prohibition"). +polarity("ACS-REQ-0076", "obligation"). +polarity("ACS-REQ-0077", "prohibition"). +polarity("ACS-REQ-0078", "prohibition"). +polarity("ACS-REQ-0079", "obligation"). +polarity("ACS-REQ-0081", "obligation"). +polarity("ACS-REQ-0082", "obligation"). +polarity("ACS-REQ-0084", "obligation"). +polarity("ACS-REQ-0086", "obligation"). +polarity("ACS-REQ-0087", "obligation"). +polarity("ACS-REQ-0092", "obligation"). +polarity("ACS-REQ-0095", "obligation"). +polarity("ACS-REQ-0096", "prohibition"). +polarity("ACS-REQ-0097", "prohibition"). +polarity("ACS-REQ-0100", "prohibition"). +polarity("ACS-REQ-0102", "obligation"). +polarity("ACS-REQ-0103", "prohibition"). +polarity("ACS-REQ-0111", "obligation"). +polarity("ACS-REQ-0113", "prohibition"). +polarity("ACS-REQ-0114", "obligation"). +polarity("ACS-REQ-0117", "prohibition"). +polarity("ACS-REQ-0120", "obligation"). +polarity("ACS-REQ-0121", "obligation"). +polarity("ACS-REQ-0130", "obligation"). +polarity("ACS-REQ-0134", "obligation"). +polarity("ACS-REQ-0137", "obligation"). +polarity("ACS-REQ-0138", "obligation"). +polarity("ACS-REQ-0141", "obligation"). +polarity("ACS-REQ-0142", "obligation"). +polarity("ACS-REQ-0151", "obligation"). +// A profile that activates the provision; `all` is expanded to every profile. +.decl requires_profile(provision:Provision, profile:Profile) +requires_profile("ACS-REQ-0001", "acs-core"). +requires_profile("ACS-REQ-0002", "acs-core"). +requires_profile("ACS-REQ-0003", "acs-core"). +requires_profile("ACS-REQ-0004", "acs-core"). +requires_profile("ACS-REQ-0005", "acs-core"). +requires_profile("ACS-REQ-0006", "acs-core"). +requires_profile("ACS-REQ-0007", "acs-core"). +requires_profile("ACS-REQ-0008", "acs-core"). +requires_profile("ACS-REQ-0009", "acs-provenance"). +requires_profile("ACS-REQ-0010", "acs-provenance"). +requires_profile("ACS-REQ-0011", "acs-core"). +requires_profile("ACS-REQ-0012", "acs-core"). +requires_profile("ACS-REQ-0013", "acs-core"). +requires_profile("ACS-REQ-0014", "acs-provenance"). +requires_profile("ACS-REQ-0015", "acs-core"). +requires_profile("ACS-REQ-0016", "acs-core"). +requires_profile("ACS-REQ-0017", "acs-core"). +requires_profile("ACS-REQ-0018", "acs-core"). +requires_profile("ACS-REQ-0019", "acs-provenance"). +requires_profile("ACS-REQ-0020", "acs-core"). +requires_profile("ACS-REQ-0021", "acs-core"). +requires_profile("ACS-REQ-0022", "acs-core"). +requires_profile("ACS-REQ-0023", "acs-core"). +requires_profile("ACS-REQ-0024", "acs-core"). +requires_profile("ACS-REQ-0025", "acs-audit"). +requires_profile("ACS-REQ-0025", "acs-core"). +requires_profile("ACS-REQ-0025", "acs-crypto"). +requires_profile("ACS-REQ-0025", "acs-inspect"). +requires_profile("ACS-REQ-0025", "acs-inspect-dynamic"). +requires_profile("ACS-REQ-0025", "acs-provenance"). +requires_profile("ACS-REQ-0025", "acs-trace"). +requires_profile("ACS-REQ-0026", "acs-provenance"). +requires_profile("ACS-REQ-0027", "acs-provenance"). +requires_profile("ACS-REQ-0028", "acs-core"). +requires_profile("ACS-REQ-0029", "acs-core"). +requires_profile("ACS-REQ-0030", "acs-core"). +requires_profile("ACS-REQ-0031", "acs-core"). +requires_profile("ACS-REQ-0032", "acs-trace"). +requires_profile("ACS-REQ-0033", "acs-core"). +requires_profile("ACS-REQ-0034", "acs-core"). +requires_profile("ACS-REQ-0035", "acs-core"). +requires_profile("ACS-REQ-0036", "acs-core"). +requires_profile("ACS-REQ-0037", "acs-core"). +requires_profile("ACS-REQ-0038", "acs-core"). +requires_profile("ACS-REQ-0039", "acs-core"). +requires_profile("ACS-REQ-0040", "acs-core"). +requires_profile("ACS-REQ-0041", "acs-core"). +requires_profile("ACS-REQ-0043", "acs-core"). +requires_profile("ACS-REQ-0044", "acs-core"). +requires_profile("ACS-REQ-0045", "acs-core"). +requires_profile("ACS-REQ-0046", "acs-core"). +requires_profile("ACS-REQ-0047", "acs-core"). +requires_profile("ACS-REQ-0048", "acs-core"). +requires_profile("ACS-REQ-0050", "acs-core"). +requires_profile("ACS-REQ-0051", "acs-core"). +requires_profile("ACS-REQ-0052", "acs-provenance"). +requires_profile("ACS-REQ-0053", "acs-core"). +requires_profile("ACS-REQ-0054", "acs-provenance"). +requires_profile("ACS-REQ-0055", "acs-provenance"). +requires_profile("ACS-REQ-0056", "acs-provenance"). +requires_profile("ACS-REQ-0057", "acs-provenance"). +requires_profile("ACS-REQ-0058", "acs-core"). +requires_profile("ACS-REQ-0059", "acs-core"). +requires_profile("ACS-REQ-0060", "acs-core"). +requires_profile("ACS-REQ-0061", "acs-core"). +requires_profile("ACS-REQ-0062", "acs-audit"). +requires_profile("ACS-REQ-0063", "acs-audit"). +requires_profile("ACS-REQ-0064", "acs-core"). +requires_profile("ACS-REQ-0065", "acs-core"). +requires_profile("ACS-REQ-0066", "acs-core"). +requires_profile("ACS-REQ-0067", "acs-core"). +requires_profile("ACS-REQ-0068", "acs-core"). +requires_profile("ACS-REQ-0069", "acs-core"). +requires_profile("ACS-REQ-0070", "acs-core"). +requires_profile("ACS-REQ-0071", "acs-core"). +requires_profile("ACS-REQ-0072", "acs-core"). +requires_profile("ACS-REQ-0073", "acs-core"). +requires_profile("ACS-REQ-0074", "acs-core"). +requires_profile("ACS-REQ-0075", "acs-core"). +requires_profile("ACS-REQ-0076", "acs-core"). +requires_profile("ACS-REQ-0077", "acs-core"). +requires_profile("ACS-REQ-0078", "acs-core"). +requires_profile("ACS-REQ-0079", "acs-core"). +requires_profile("ACS-REQ-0080", "acs-core"). +requires_profile("ACS-REQ-0081", "acs-core"). +requires_profile("ACS-REQ-0082", "acs-core"). +requires_profile("ACS-REQ-0083", "acs-crypto"). +requires_profile("ACS-REQ-0084", "acs-core"). +requires_profile("ACS-REQ-0086", "acs-core"). +requires_profile("ACS-REQ-0087", "acs-core"). +requires_profile("ACS-REQ-0088", "acs-audit"). +requires_profile("ACS-REQ-0088", "acs-core"). +requires_profile("ACS-REQ-0088", "acs-crypto"). +requires_profile("ACS-REQ-0088", "acs-inspect"). +requires_profile("ACS-REQ-0088", "acs-inspect-dynamic"). +requires_profile("ACS-REQ-0088", "acs-provenance"). +requires_profile("ACS-REQ-0088", "acs-trace"). +requires_profile("ACS-REQ-0089", "acs-core"). +requires_profile("ACS-REQ-0090", "acs-core"). +requires_profile("ACS-REQ-0091", "acs-core"). +requires_profile("ACS-REQ-0092", "acs-core"). +requires_profile("ACS-REQ-0093", "acs-core"). +requires_profile("ACS-REQ-0094", "acs-core"). +requires_profile("ACS-REQ-0095", "acs-core"). +requires_profile("ACS-REQ-0096", "acs-core"). +requires_profile("ACS-REQ-0097", "acs-core"). +requires_profile("ACS-REQ-0098", "acs-core"). +requires_profile("ACS-REQ-0099", "acs-core"). +requires_profile("ACS-REQ-0100", "acs-core"). +requires_profile("ACS-REQ-0101", "acs-core"). +requires_profile("ACS-REQ-0102", "acs-core"). +requires_profile("ACS-REQ-0103", "acs-core"). +requires_profile("ACS-REQ-0104", "acs-core"). +requires_profile("ACS-REQ-0105", "acs-core"). +requires_profile("ACS-REQ-0106", "acs-core"). +requires_profile("ACS-REQ-0107", "acs-core"). +requires_profile("ACS-REQ-0108", "acs-core"). +requires_profile("ACS-REQ-0109", "acs-core"). +requires_profile("ACS-REQ-0110", "acs-core"). +requires_profile("ACS-REQ-0111", "acs-provenance"). +requires_profile("ACS-REQ-0112", "acs-core"). +requires_profile("ACS-REQ-0113", "acs-core"). +requires_profile("ACS-REQ-0114", "acs-core"). +requires_profile("ACS-REQ-0116", "acs-core"). +requires_profile("ACS-REQ-0117", "acs-core"). +requires_profile("ACS-REQ-0118", "acs-core"). +requires_profile("ACS-REQ-0119", "acs-core"). +requires_profile("ACS-REQ-0120", "acs-core"). +requires_profile("ACS-REQ-0121", "acs-core"). +requires_profile("ACS-REQ-0122", "acs-core"). +requires_profile("ACS-REQ-0123", "acs-core"). +requires_profile("ACS-REQ-0124", "acs-inspect"). +requires_profile("ACS-REQ-0125", "acs-core"). +requires_profile("ACS-REQ-0126", "acs-core"). +requires_profile("ACS-REQ-0127", "acs-core"). +requires_profile("ACS-REQ-0128", "acs-core"). +requires_profile("ACS-REQ-0129", "acs-core"). +requires_profile("ACS-REQ-0130", "acs-inspect"). +requires_profile("ACS-REQ-0131", "acs-trace"). +requires_profile("ACS-REQ-0132", "acs-trace"). +requires_profile("ACS-REQ-0133", "acs-core"). +requires_profile("ACS-REQ-0134", "acs-inspect"). +requires_profile("ACS-REQ-0135", "acs-inspect"). +requires_profile("ACS-REQ-0136", "acs-inspect-dynamic"). +requires_profile("ACS-REQ-0137", "acs-crypto"). +requires_profile("ACS-REQ-0138", "acs-crypto"). +requires_profile("ACS-REQ-0139", "acs-crypto"). +requires_profile("ACS-REQ-0140", "acs-core"). +requires_profile("ACS-REQ-0141", "acs-inspect"). +requires_profile("ACS-REQ-0142", "acs-provenance"). +requires_profile("ACS-REQ-0143", "acs-inspect"). +requires_profile("ACS-REQ-0144", "acs-inspect"). +requires_profile("ACS-REQ-0145", "acs-trace"). +requires_profile("ACS-REQ-0146", "acs-trace"). +requires_profile("ACS-REQ-0147", "acs-trace"). +requires_profile("ACS-REQ-0148", "acs-trace"). +requires_profile("ACS-REQ-0149", "acs-trace"). +requires_profile("ACS-REQ-0150", "acs-trace"). +requires_profile("ACS-REQ-0151", "acs-core"). +requires_profile("ACS-REQ-0152", "acs-core"). +// A relation the provision's rules read whose tuples are not derived from the wire. +.decl needs(provision:Provision, relation:Relation) +needs("ACS-REQ-0001", "schema_violation"). +needs("ACS-REQ-0002", "session_batching"). +needs("ACS-REQ-0006", "defer_bound"). +needs("ACS-REQ-0008", "evaluator_ran"). +needs("ACS-REQ-0011", "intent_established"). +needs("ACS-REQ-0011", "intent_extension"). +needs("ACS-REQ-0011", "intent_parsed"). +needs("ACS-REQ-0012", "audit_event"). +needs("ACS-REQ-0012", "intent_modification_rejected"). +needs("ACS-REQ-0013", "context_entry"). +needs("ACS-REQ-0013", "entry_hash_recomputed"). +needs("ACS-REQ-0015", "guardian_version"). +needs("ACS-REQ-0017", "signature_covers"). +needs("ACS-REQ-0018", "signature_status"). +needs("ACS-REQ-0020", "audit_event"). +needs("ACS-REQ-0022", "archive_preserved"). +needs("ACS-REQ-0022", "archived"). +needs("ACS-REQ-0023", "approver_verified"). +needs("ACS-REQ-0023", "ask_resolved"). +needs("ACS-REQ-0030", "policy_requires_provenance"). +needs("ACS-REQ-0031", "agent_audit_event"). +needs("ACS-REQ-0041", "modification_targets_overlap"). +needs("ACS-REQ-0043", "agent_step_outcome"). +needs("ACS-REQ-0043", "modification_targets_overlap"). +needs("ACS-REQ-0046", "agent_step_outcome"). +needs("ACS-REQ-0050", "agent_audit_event"). +needs("ACS-REQ-0050", "agent_step_outcome"). +needs("ACS-REQ-0051", "agent_step_outcome"). +needs("ACS-REQ-0052", "schema_violation"). +needs("ACS-REQ-0053", "schema_violation"). +needs("ACS-REQ-0060", "context_entry"). +needs("ACS-REQ-0060", "context_entry_field"). +needs("ACS-REQ-0061", "context_entry"). +needs("ACS-REQ-0061", "context_entry_field"). +needs("ACS-REQ-0062", "context_entry"). +needs("ACS-REQ-0062", "context_entry_field"). +needs("ACS-REQ-0063", "context_entry"). +needs("ACS-REQ-0063", "context_entry_field"). +needs("ACS-REQ-0066", "schema_violation"). +needs("ACS-REQ-0072", "ask_resolved"). +needs("ACS-REQ-0076", "context_entry"). +needs("ACS-REQ-0076", "context_entry_step"). +needs("ACS-REQ-0076", "intent_extension"). +needs("ACS-REQ-0077", "intent_extension"). +needs("ACS-REQ-0077", "strict_mode_forbidden"). +needs("ACS-REQ-0078", "client_ask_capable"). +needs("ACS-REQ-0079", "client_ask_capable"). +needs("ACS-REQ-0081", "signature_status"). +needs("ACS-REQ-0084", "timestamp_out_of_window"). +needs("ACS-REQ-0092", "decision_log_field"). +needs("ACS-REQ-0096", "context_entry"). +needs("ACS-REQ-0100", "agent_audit_event"). +needs("ACS-REQ-0111", "step_provenance"). +needs("ACS-REQ-0114", "context_entry"). +needs("ACS-REQ-0151", "intent_derivation_recorded"). +// An obligation conditional on a permission being exercised. +.decl conditional(provision:Provision) +conditional("ACS-REQ-0022"). +conditional("ACS-REQ-0102"). + +// what the rules derive; the verdicts are outputs +// The provision's violation relation, attributed to a session. +.decl violated(provision:Provision, session:Session) +// The situation a conditional provision's rules guard on arose in the session. +.decl exercised(provision:Provision, session:Session) +// The session negotiated a profile that activates the provision. +.decl active(provision:Provision, session:Session) +// A relation the provision needs was not supplied; no verdict. +.decl unevaluated(provision:Provision) +.output unevaluated +// No negotiated profile activates the provision in the session. +.decl not_activated(provision:Provision, session:Session) +.output not_activated +// The condition never arose in the session; the obligation had nothing to bind. +.decl not_exercised(provision:Provision, session:Session) +.output not_exercised +// A MUST or MUST NOT violated in a session that activated it. +.decl fail(provision:Provision, session:Session) +.output fail +// A SHOULD or SHOULD NOT violated in a session that activated it. +.decl deviates(provision:Provision, session:Session) +.output deviates +// Active, evaluated, exercised where conditional, and not violated. +.decl pass(provision:Provision, session:Session) +.output pass + +violated("ACS-REQ-0001", S) :- acs_req_0001__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0002", S) :- acs_req_0002__violation(_, S). +violated("ACS-REQ-0003", S) :- acs_req_0003__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0004", S) :- acs_req_0004__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0005", S) :- acs_req_0005__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0006", S) :- acs_req_0006__violation(S, _, _). +violated("ACS-REQ-0007", S) :- acs_req_0007__violation(_, S, _). +violated("ACS-REQ-0008", S) :- acs_req_0008__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0009", S) :- acs_req_0009__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0010", S) :- acs_req_0010__violation(Q, _, _, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0011", S) :- acs_req_0011__violation(S, _, _). +violated("ACS-REQ-0012", S) :- acs_req_0012__violation(S, _). +violated("ACS-REQ-0013", S) :- acs_req_0013__violation(S, _, _, _). +violated("ACS-REQ-0014", S) :- acs_req_0014__violation(S, _, _, _). +violated("ACS-REQ-0015", S) :- acs_req_0015__violation(_, S). +violated("ACS-REQ-0016", S) :- acs_req_0016__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0017", S) :- acs_req_0017__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0018", S) :- acs_req_0018__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0020", S) :- acs_req_0020__violation(S, _). +violated("ACS-REQ-0022", S) :- acs_req_0022__violation(S, _). +exercised("ACS-REQ-0022", Session) :- archived(Session). +violated("ACS-REQ-0023", S) :- acs_req_0023__violation(_, S, _). +violated("ACS-REQ-0027", S) :- acs_req_0027__violation(Q, _, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0028", S) :- acs_req_0028__violation(_, S). +violated("ACS-REQ-0030", S) :- acs_req_0030__violation(_, S). +violated("ACS-REQ-0031", S) :- acs_req_0031__violation(S, _). +violated("ACS-REQ-0039", S) :- acs_req_0039__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0041", S) :- acs_req_0041__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0043", S) :- acs_req_0043__violation(_, S). +violated("ACS-REQ-0046", S) :- acs_req_0046__violation(_, S, _). +violated("ACS-REQ-0050", S) :- acs_req_0050__violation(S, _). +violated("ACS-REQ-0051", S) :- acs_req_0051__violation(_, S). +violated("ACS-REQ-0052", S) :- acs_req_0052__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0053", S) :- acs_req_0053__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0060", S) :- acs_req_0060__violation(S, _, _). +violated("ACS-REQ-0061", S) :- acs_req_0061__violation(S, _, _). +violated("ACS-REQ-0062", S) :- acs_req_0062__violation(S, _, _). +violated("ACS-REQ-0063", S) :- acs_req_0063__violation(S, _, _). +violated("ACS-REQ-0066", S) :- acs_req_0066__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0067", S) :- acs_req_0067__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0072", S) :- acs_req_0072__violation(_, S, _). +violated("ACS-REQ-0076", S) :- acs_req_0076__violation(S, _, _). +violated("ACS-REQ-0077", S) :- acs_req_0077__violation(S, _, _). +violated("ACS-REQ-0078", S) :- acs_req_0078__violation(_, S). +violated("ACS-REQ-0079", S) :- acs_req_0079__violation(_, S, _). +violated("ACS-REQ-0081", S) :- acs_req_0081__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0082", S) :- acs_req_0082__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0084", S) :- acs_req_0084__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0086", S) :- acs_req_0086__violation(_, S, _). +violated("ACS-REQ-0087", S) :- acs_req_0087__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0092", S) :- acs_req_0092__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0095", S) :- acs_req_0095__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0096", S) :- acs_req_0096__violation(S, _, _). +violated("ACS-REQ-0097", S) :- acs_req_0097__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0100", S) :- acs_req_0100__violation(S, _, _). +violated("ACS-REQ-0102", S) :- acs_req_0102__violation(Q, _), envelope(Q, S, _, _, _). +exercised("ACS-REQ-0102", Session) :- error_data(Seq), envelope(Seq, Session, _, _, _). +violated("ACS-REQ-0103", S) :- acs_req_0103__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0111", S) :- acs_req_0111__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0113", S) :- acs_req_0113__violation(Q, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0114", S) :- acs_req_0114__violation(S, _, _). +violated("ACS-REQ-0117", S) :- acs_req_0117__violation(_, S, _). +violated("ACS-REQ-0120", S) :- acs_req_0120__violation(_, S, _, _). +violated("ACS-REQ-0121", S) :- acs_req_0121__violation(_, S, _). +violated("ACS-REQ-0130", S) :- acs_req_0130__violation(S, _). +violated("ACS-REQ-0134", S) :- acs_req_0134__violation(_, S, _). +violated("ACS-REQ-0137", S) :- acs_req_0137__violation(S, _). +violated("ACS-REQ-0138", S) :- acs_req_0138__violation(S, _). +violated("ACS-REQ-0141", S) :- acs_req_0141__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0142", S) :- acs_req_0142__violation(Q, _, _), envelope(Q, S, _, _, _). +violated("ACS-REQ-0151", S) :- acs_req_0151__violation(S, _, _). +active(P, S) :- requires_profile(P, Pr), negotiated(S, Pr). +not_activated(P, S) :- provision(P), negotiated(S, _), !active(P, S). +unevaluated(P) :- needs(P, R), !available(R). +not_exercised(P, S) :- conditional(P), active(P, S), !unevaluated(P), !exercised(P, S). +fail(P, S) :- violated(P, S), active(P, S), strength(P, "must"), !unevaluated(P). +deviates(P, S) :- violated(P, S), active(P, S), strength(P, "should"), !unevaluated(P). +pass(P, S) :- compiled(P), active(P, S), !conditional(P), !unevaluated(P), !violated(P, S). +pass(P, S) :- conditional(P), active(P, S), exercised(P, S), !unevaluated(P), !violated(P, S). diff --git a/ir/provisions/ACS-REQ-0001.yaml b/ir/provisions/ACS-REQ-0001.yaml index 7a5a55d..048216d 100644 --- a/ir/provisions/ACS-REQ-0001.yaml +++ b/ir/provisions/ACS-REQ-0001.yaml @@ -5,6 +5,8 @@ reported_against: guardian profile: [acs-core] activation: null modality_kind: obligation +keyword: MUST +keyword_basis: "A schema-shaped table cell with no RFC 2119 word; the response shape is what the pinned schema enforces, and a schema constraint is a MUST." evidence_class: schema schema_refs: - file: response-envelope.json diff --git a/ir/provisions/ACS-REQ-0003.yaml b/ir/provisions/ACS-REQ-0003.yaml index 9741a29..f287a56 100644 --- a/ir/provisions/ACS-REQ-0003.yaml +++ b/ir/provisions/ACS-REQ-0003.yaml @@ -5,6 +5,8 @@ reported_against: guardian profile: [acs-core] activation: null modality_kind: obligation +keyword: MUST +keyword_basis: "The span is the §6 table body, whose first keyword is RECOMMENDED, the status of `reasoning` on an ALLOW. The obligation the rule checks is the required field per disposition, which the table states without a keyword." evidence_class: schema schema_refs: - file: response-envelope.json diff --git a/ir/provisions/ACS-REQ-0005.yaml b/ir/provisions/ACS-REQ-0005.yaml index ee9f88a..5a18a96 100644 --- a/ir/provisions/ACS-REQ-0005.yaml +++ b/ir/provisions/ACS-REQ-0005.yaml @@ -5,6 +5,8 @@ reported_against: guardian profile: [acs-core] activation: "the decision is DEFER" modality_kind: obligation +keyword: MUST +keyword_basis: "A table cell listing the reason vocabulary with no RFC 2119 word; a closed vocabulary is a MUST on the value." evidence_class: schema schema_refs: - file: defer-details.json diff --git a/ir/provisions/ACS-REQ-0007.yaml b/ir/provisions/ACS-REQ-0007.yaml index a288de4..12a3348 100644 --- a/ir/provisions/ACS-REQ-0007.yaml +++ b/ir/provisions/ACS-REQ-0007.yaml @@ -5,6 +5,8 @@ reported_against: observed-agent profile: [acs-core] activation: null modality_kind: obligation +keyword: MUST +keyword_basis: "The cell says 'Required' in lowercase, which the keyword scan does not count; it is REQUIRED in RFC 2119's sense." evidence_class: wire schema_refs: [] depends_on: [] diff --git a/ir/provisions/ACS-REQ-0008.yaml b/ir/provisions/ACS-REQ-0008.yaml index 104ff76..aac57a5 100644 --- a/ir/provisions/ACS-REQ-0008.yaml +++ b/ir/provisions/ACS-REQ-0008.yaml @@ -5,6 +5,8 @@ reported_against: guardian profile: [acs-core] activation: null modality_kind: obligation +keyword: MUST +keyword_basis: "The cell says 'always', which is not an RFC 2119 word; an unconditional ordering rule is a MUST." evidence_class: guardian-state schema_refs: [] depends_on: [] diff --git a/ir/provisions/ACS-REQ-0009.yaml b/ir/provisions/ACS-REQ-0009.yaml index e22cae6..7265d09 100644 --- a/ir/provisions/ACS-REQ-0009.yaml +++ b/ir/provisions/ACS-REQ-0009.yaml @@ -5,6 +5,8 @@ reported_against: framework profile: [acs-provenance] activation: "provenance_producer: deterministic" modality_kind: obligation +keyword: MUST +keyword_basis: "A field-definition cell with no RFC 2119 word; the in-session lineage constraint is a MUST on the value." evidence_class: wire schema_refs: - file: provenance.json diff --git a/ir/provisions/ACS-REQ-0014.yaml b/ir/provisions/ACS-REQ-0014.yaml index 385254f..3149daa 100644 --- a/ir/provisions/ACS-REQ-0014.yaml +++ b/ir/provisions/ACS-REQ-0014.yaml @@ -5,6 +5,8 @@ reported_against: framework profile: [acs-provenance] activation: "provenance_producer: deterministic" modality_kind: obligation +keyword: MUST +keyword_basis: "A field-definition cell with no RFC 2119 word; uniqueness is a MUST on the value." evidence_class: wire schema_refs: - file: provenance.json diff --git a/ir/provisions/ACS-REQ-0015.yaml b/ir/provisions/ACS-REQ-0015.yaml index f19fcb4..78d706f 100644 --- a/ir/provisions/ACS-REQ-0015.yaml +++ b/ir/provisions/ACS-REQ-0015.yaml @@ -5,6 +5,8 @@ reported_against: guardian profile: [acs-core] activation: null modality_kind: obligation +keyword: MUST +keyword_basis: "A cell stating the outcome as fact with no RFC 2119 word; the termination is a MUST on the Guardian." evidence_class: wire schema_refs: [] depends_on: [] diff --git a/ir/provisions/ACS-REQ-0061.yaml b/ir/provisions/ACS-REQ-0061.yaml index 3f6fe6a..da004a6 100644 --- a/ir/provisions/ACS-REQ-0061.yaml +++ b/ir/provisions/ACS-REQ-0061.yaml @@ -5,6 +5,8 @@ reported_against: guardian profile: [acs-core] activation: null modality_kind: obligation +keyword: MUST +keyword_basis: "The cell says 'required' in lowercase, which the keyword scan does not count; it is REQUIRED in RFC 2119's sense." evidence_class: guardian-state schema_refs: [] depends_on: [] diff --git a/ir/provisions/ACS-REQ-0082.yaml b/ir/provisions/ACS-REQ-0082.yaml index a361504..ea5392d 100644 --- a/ir/provisions/ACS-REQ-0082.yaml +++ b/ir/provisions/ACS-REQ-0082.yaml @@ -5,6 +5,8 @@ reported_against: deployment profile: [acs-core] activation: null modality_kind: obligation +keyword: MUST +keyword_basis: "The span is the §10.1 table body, whose first keyword is RECOMMENDED, the status of HMAC-SHA256. The obligation the rule checks is registry membership, which §10's prose states without a keyword ('the algorithm drawn from the registry below')." evidence_class: wire schema_refs: [] depends_on: [] diff --git a/ir/provisions/ACS-REQ-0113.yaml b/ir/provisions/ACS-REQ-0113.yaml index ec336e7..2fcc1a4 100644 --- a/ir/provisions/ACS-REQ-0113.yaml +++ b/ir/provisions/ACS-REQ-0113.yaml @@ -5,6 +5,8 @@ reported_against: guardian profile: [acs-core] activation: null modality_kind: obligation +keyword: MUST NOT +keyword_basis: "The sentence says MAY NOT, which RFC 2119 does not define; read as MUST NOT, the prohibition the rule checks. Worth an upstream finding." evidence_class: wire schema_refs: [] depends_on: [] diff --git a/ir/provisions/ACS-REQ-0135.yaml b/ir/provisions/ACS-REQ-0135.yaml index 463ecbe..9afa717 100644 --- a/ir/provisions/ACS-REQ-0135.yaml +++ b/ir/provisions/ACS-REQ-0135.yaml @@ -5,6 +5,8 @@ reported_against: guardian profile: [acs-inspect] activation: null modality_kind: obligation +keyword: MUST +keyword_basis: "An imperative list item with no RFC 2119 word; the conformance page lists it as what a claim of the profile requires, which is a MUST." evidence_class: non-testable schema_refs: [] depends_on: [] diff --git a/ir/src/catalog/catalog.ts b/ir/src/catalog/catalog.ts index b5af56e..bfd54ff 100644 --- a/ir/src/catalog/catalog.ts +++ b/ir/src/catalog/catalog.ts @@ -26,6 +26,54 @@ export type Modality = (typeof MODALITIES)[number]; export const EVIDENCE_CLASSES = ["wire", "schema", "guardian-state", "deployment-config", "non-testable", "not-applicable"] as const; export type EvidenceClass = (typeof EVIDENCE_CLASSES)[number]; +/** + * The RFC 2119 keyword a provision binds, in its canonical form. RFC 2119 + * defines REQUIRED and SHALL as MUST, RECOMMENDED as SHOULD, OPTIONAL as + * MAY, and the negated forms likewise; the catalog keeps the five + * canonical words. The strength (must, should, may) and polarity + * (obligation, prohibition) the verdict rules read are derived from it. + */ +export const KEYWORDS = ["MUST", "MUST NOT", "SHOULD", "SHOULD NOT", "MAY"] as const; +export type CanonicalKeyword = (typeof KEYWORDS)[number]; +export type Strength = "must" | "should" | "may"; +export type Polarity = "obligation" | "prohibition"; + +const CANONICAL: Record = { + MUST: "MUST", + SHALL: "MUST", + REQUIRED: "MUST", + "MUST NOT": "MUST NOT", + "SHALL NOT": "MUST NOT", + SHOULD: "SHOULD", + RECOMMENDED: "SHOULD", + "SHOULD NOT": "SHOULD NOT", + "NOT RECOMMENDED": "SHOULD NOT", + MAY: "MAY", + OPTIONAL: "MAY", +}; + +/** The canonical keyword for any RFC 2119 word, or null for none. */ +export function canonicalKeyword(keyword: string | null | undefined): CanonicalKeyword | null { + return keyword ? (CANONICAL[keyword] ?? null) : null; +} + +export function strengthOf(keyword: CanonicalKeyword): Strength { + return keyword === "MAY" ? "may" : keyword.startsWith("SHOULD") ? "should" : "must"; +} + +export function polarityOf(keyword: CanonicalKeyword): Polarity { + return keyword.endsWith("NOT") ? "prohibition" : "obligation"; +} + +/** + * The keyword a provision is judged by: the record's own `keyword` when it + * states one, else the canonical form of the manifest's `level`, the first + * RFC 2119 word in the marked span. Null when neither says. + */ +export function effectiveKeyword(manifest: { level: string | null }, record: { keyword: CanonicalKeyword | null }): CanonicalKeyword | null { + return record.keyword ?? canonicalKeyword(manifest.level); +} + export interface SchemaRef { file: string; pointer: string; @@ -43,6 +91,16 @@ export interface ProvisionRecord { /** Session state that activates a conditional provision, in prose; null when unconditional (R4.5). */ activation: string | null; modality_kind: Modality; + /** + * The RFC 2119 keyword the provision is judged by, when the marked span's + * own keyword is absent or misleading: a schema cell with no keyword, a + * `MAY NOT` the RFC does not define, a table whose first keyword is not + * the obligation the rule checks. Null means the manifest's `level` + * stands. Stating one requires `keyword_basis`. + */ + keyword: CanonicalKeyword | null; + /** Why the record's keyword differs from the marked span's. */ + keyword_basis: string | null; evidence_class: EvidenceClass; schema_refs: SchemaRef[]; depends_on: string[]; @@ -94,6 +152,8 @@ export function parseProvisionRecord(yamlText: string, expectedId?: string): Pro profile: profile as Profile[] | "all", activation: optStr(r, "activation"), modality_kind: oneOf(r, "modality_kind", MODALITIES, id), + keyword: r.keyword === undefined || r.keyword === null ? null : oneOf(r, "keyword", KEYWORDS, id), + keyword_basis: optStr(r, "keyword_basis"), evidence_class: oneOf(r, "evidence_class", EVIDENCE_CLASSES, id), schema_refs: schemaRefs(r, id), depends_on: list(r, "depends_on"), @@ -108,6 +168,8 @@ export function parseProvisionRecord(yamlText: string, expectedId?: string): Pro for (const ref of [...record.depends_on, ...record.superseded_by, ...(record.restates ? [record.restates] : [])]) { if (!ID_PATTERN.test(ref)) throw new Error(`${id}: ${ref} is not a provision ID`); } + if (record.keyword && !record.keyword_basis) throw new Error(`${id}: keyword ${record.keyword} overrides the marked span's; say why in keyword_basis`); + if (!record.keyword && record.keyword_basis) throw new Error(`${id}: keyword_basis without a keyword`); return record; } @@ -143,7 +205,16 @@ export function loadCatalog(manifest: Manifest, records: ProvisionRecord[]): Cat if (!manifestIds.has(r.id) && r.status !== "withdrawn") problems.push(`${r.id}: has a record but is not marked in the corpus`); } const sourceOf = new Map(manifest.provisions.map((p) => [p.id, p.source_file])); - for (const { record } of entries) { + for (const { manifest: m, record } of entries) { + // The keyword and the modality say the same thing twice, so they must agree: a permission is a MAY, an obligation is not. + if (m.type === "Requirement") { + const keyword = effectiveKeyword(m, record); + if (!keyword) problems.push(`${record.id}: the marked span has no RFC 2119 keyword; state keyword: with keyword_basis`); + else if (record.modality_kind === "permission" && keyword !== "MAY") problems.push(`${record.id}: a permission is judged by MAY, not ${keyword}`); + else if ((record.modality_kind === "obligation" || record.modality_kind === "conditional-on-exercise") && keyword === "MAY") { + problems.push(`${record.id}: an ${record.modality_kind} is judged by MUST or SHOULD, not MAY; if the sentence says MAY NOT, state keyword: MUST NOT with keyword_basis`); + } + } for (const dep of record.depends_on) { if (!manifestIds.has(dep)) problems.push(`${record.id}: depends_on ${dep}, which is not in the catalog`); } diff --git a/ir/src/compile/compile.ts b/ir/src/compile/compile.ts index 6f690bf..45e7993 100644 --- a/ir/src/compile/compile.ts +++ b/ir/src/compile/compile.ts @@ -29,7 +29,9 @@ */ import type { ProvisionRecord, PredicateSpec } from "../catalog/catalog.ts"; import type { ManifestEntry } from "../extract/extract.ts"; -import { atomVars, parseRule, termVars, type Atom, type Literal, type Rule, type Term } from "./predicate.ts"; +import { parseRule, type Rule } from "./predicate.ts"; +import { headColumnType, literalAtoms, renameLiteral, sameTy, stratify, toTy, typeRule, type Env, type Ty } from "./typing.ts"; +import { buildVerdictLayer, type VerdictLayer } from "./verdict-layer.ts"; import type { Column, ColumnType, Relation, RelationSource, Vocabulary } from "./vocabulary.ts"; export type ProvisionStatus = "compiled" | "non-testable" | "permission" | "alias" | "no-predicate" | "inexpressible"; @@ -64,9 +66,11 @@ export interface RuleProgram { generated_by: string; corpus: { version: string | null; commit: string | null }; relations: Relation[]; - /** Every column domain the relations declare, with its base type; the Soufflé emitter declares each as a subtype. */ + /** Every column domain the relations declare, the verdict layer's included, with its base type; the Soufflé emitter declares each as a subtype. */ domains: { name: string; type: ColumnType }[]; provisions: CompiledProvision[]; + /** RFC 2119 strength as facts and the verdicts as rules, over the provisions' violation relations. */ + verdicts: VerdictLayer; problems: { id: string; message: string }[]; } @@ -89,12 +93,15 @@ export function compileProgram( problems.push({ id: manifest.id, message: error instanceof Error ? error.message : String(error) }); } } + const verdicts = buildVerdictLayer(vocabulary, entries, provisions); + problems.push(...verdicts.problems); return { generated_by: "acs-ir compile", corpus, relations: [...vocabulary.relations.values()], - domains: [...vocabulary.domains.entries()].sort(([a], [b]) => a.localeCompare(b)).map(([name, type]) => ({ name, type })), + domains: [...[...vocabulary.domains.entries()].map(([name, type]) => ({ name, type })), ...verdicts.layer.domains].sort((a, b) => a.name.localeCompare(b.name)), provisions, + verdicts: verdicts.layer, problems, }; } @@ -134,24 +141,6 @@ export function flagInexpressible(id: string, reason: string): CompiledProvision return skipped(id, "inexpressible", reason); } -/** A column type as the checker sees it: the base type, and the domain when the value is known to come from one. */ -interface Ty { - base: ColumnType; - domain: string | null; -} - -function describe(t: Ty): string { - return t.domain ?? t.base; -} - -function sameTy(a: Ty | null, b: Ty | null): boolean { - return a === null || b === null ? a === b : a.base === b.base && a.domain === b.domain; -} - -function toTy(c: Column): Ty { - return { base: c.type, domain: c.domain }; -} - /** N31: parse, type, check safety and stratification, and rename helpers so provisions never collide. */ export function compilePredicate(vocabulary: Vocabulary, id: string, spec: Extract): CompiledProvision { const prefix = slug(id); @@ -283,192 +272,3 @@ export function compilePredicate(vocabulary: Vocabulary, id: string, spec: Extra external_facts, }; } - -/** - * The type of a derived relation's column from every rule that produces it. - * Variables and functors decide it: two rules must agree on the base type, - * and on the domain when both name one; a rule that supplies a base-typed - * value (a `cat` result, say) makes the column base-typed, which every - * domain fits. A constant fits any domain, so it only has to agree on the - * base type, and decides the column alone only when no rule supplies a - * variable. - */ -function headColumnType(id: string, relation: string, i: number, producers: Rule[], envs: Env[]): Ty | null { - let acc: Ty | null = null; - let constant: ColumnType | null = null; - producers.forEach((rule, r) => { - const arg = rule.head.args[i] as Term; - if (arg.kind === "str" || arg.kind === "num") { - const base: ColumnType = arg.kind === "str" ? "symbol" : "number"; - if (constant && constant !== base) throw new Error(`${id}: ${relation} column ${i + 1} is ${constant} in one rule and ${base} in another`); - constant = base; - return; - } - const t = termType(arg, envs[r] as Env); - if (!t) return; - if (!acc) { - acc = t; - return; - } - if (acc.base !== t.base) throw new Error(`${id}: ${relation} column ${i + 1} is ${acc.base} in one rule and ${t.base} in another`); - if (acc.domain && t.domain && acc.domain !== t.domain) throw new Error(`${id}: ${relation} column ${i + 1} is ${acc.domain} in one rule and ${t.domain} in another`); - acc = { base: acc.base, domain: acc.domain && t.domain ? acc.domain : null }; - }); - const result: Ty | null = acc ?? (constant ? { base: constant, domain: null } : null); - if (result && constant && result.base !== constant) throw new Error(`${id}: ${relation} column ${i + 1} is ${result.base} in one rule and ${constant} in another`); - return result; -} - -type Env = Map; - -/** Type every variable in a rule from its positive atoms, then check the rest. Returns the environment. */ -function typeRule(id: string, rule: Rule, relationTypes: (name: string) => (Ty | null)[] | null, strict = false): Env { - const env: Env = new Map(); - // A variable's type is the meet of every column it fills: the base types - // must agree, and so must the domains when both are known. - const bindIn = (target: Env, name: string, type: Ty | null): void => { - if (!type) return; - const known = target.get(name); - if (!known) { - target.set(name, type); - return; - } - if (known.base !== type.base || (known.domain && type.domain && known.domain !== type.domain)) { - throw new Error(`${id}: variable ${name} is used as both ${describe(known)} and ${describe(type)} in: ${rule.source}`); - } - if (!known.domain && type.domain) target.set(name, type); - }; - const bindAtomIn = (target: Env, atom: Atom): void => { - const types = relationTypes(atom.relation); - if (!types) return; - if (types.length !== atom.args.length) throw new Error(`${id}: ${atom.relation} takes ${types.length} argument(s), got ${atom.args.length} in: ${rule.source}`); - atom.args.forEach((arg, i) => { - const t = types[i] ?? null; - if (arg.kind === "var") bindIn(target, arg.name, t); - else if (arg.kind === "str" && t?.base === "number") throw new Error(`${id}: ${atom.relation} argument ${i + 1} is a number, got a string in: ${rule.source}`); - else if (arg.kind === "num" && t?.base === "symbol") throw new Error(`${id}: ${atom.relation} argument ${i + 1} is a symbol, got a number in: ${rule.source}`); - else if (arg.kind === "func" && t?.base === "number") throw new Error(`${id}: ${atom.relation} argument ${i + 1} is a number, got ${arg.name}() in: ${rule.source}`); - }); - }; - const bind = (name: string, type: Ty | null): void => bindIn(env, name, type); - const bindAtom = (atom: Atom): void => bindAtomIn(env, atom); - // Positive atoms bind; then assignments; then everything is checked. - for (const lit of rule.body) if (lit.kind === "atom" && !lit.negated) bindAtom(lit.atom); - for (const lit of rule.body) if (lit.kind === "count") bind(lit.target, { base: "number", domain: null }); - let progressed = true; - while (progressed) { - progressed = false; - for (const lit of rule.body) { - if (lit.kind === "cmp" && lit.op === "=" && lit.left.kind === "var" && !env.has(lit.left.name)) { - const t = termType(lit.right, env); - if (t) { - bind(lit.left.name, t); - progressed = true; - } - } - } - } - if (!strict) return env; - - const bound = (t: Term): boolean => termVars(t).every((v) => env.has(v)); - for (const lit of rule.body) { - if (lit.kind === "atom" && lit.negated) { - for (const v of atomVars(lit.atom)) if (!env.has(v)) throw new Error(`${id}: variable ${v} in a negated atom is not bound by a positive atom (unsafe) in: ${rule.source}`); - bindAtom(lit.atom); // arity, constant types, and domains, now that every variable is known to be bound - } - if (lit.kind === "cmp") { - if (!bound(lit.left) || !bound(lit.right)) { - const missing = [...termVars(lit.left), ...termVars(lit.right)].filter((v) => !env.has(v)); - throw new Error(`${id}: variable ${missing[0]} in a comparison is not bound (unsafe) in: ${rule.source}`); - } - const l = termType(lit.left, env) as Ty; - const r = termType(lit.right, env) as Ty; - if (l.base !== r.base) throw new Error(`${id}: comparing ${l.base} with ${r.base} in: ${rule.source}`); - if (l.domain && r.domain && l.domain !== r.domain) throw new Error(`${id}: comparing a ${l.domain} with a ${r.domain} in: ${rule.source}`); - if (lit.op !== "=" && lit.op !== "!=" && l.base !== "number") throw new Error(`${id}: ordering comparisons need numbers, got ${l.base} in: ${rule.source}`); - } - if (lit.kind === "count") { - // The aggregate's own variables are local to it; they are typed in a copy so they never count as bound outside. - const inner: Env = new Map(env); - for (const atom of lit.atoms) bindAtomIn(inner, atom); - } - } - for (const v of atomVars(rule.head)) if (!env.has(v)) throw new Error(`${id}: head variable ${v} is not bound in the body (unsafe) in: ${rule.source}`); - for (const arg of rule.head.args) if (arg.kind === "wild") throw new Error(`${id}: a head cannot carry a wildcard in: ${rule.source}`); - return env; -} - -function termType(term: Term, env: Env): Ty | null { - switch (term.kind) { - case "var": - return env.get(term.name) ?? null; - case "str": - return { base: "symbol", domain: null }; - case "num": - return { base: "number", domain: null }; - case "func": - return { base: "symbol", domain: null }; - case "wild": - return null; - } -} - -function literalAtoms(lit: Literal): Atom[] { - if (lit.kind === "atom") return [lit.atom]; - if (lit.kind === "count") return lit.atoms; - return []; -} - -function renameLiteral(lit: Literal, rename: (name: string) => string): Literal { - if (lit.kind === "atom") return { ...lit, atom: { relation: rename(lit.atom.relation), args: lit.atom.args } }; - if (lit.kind === "count") return { ...lit, atoms: lit.atoms.map((a) => ({ relation: rename(a.relation), args: a.args })) }; - return lit; -} - -/** Strata by Tarjan SCC over positive+negative edges, refusing a negative edge inside a component. */ -function stratify(id: string, nodes: string[], positive: Map>, negative: Map>): string[][] { - const edges = (n: string): string[] => [...(positive.get(n) ?? []), ...(negative.get(n) ?? [])]; - let index = 0; - const stack: string[] = []; - const onStack = new Set(); - const idx = new Map(); - const low = new Map(); - const component = new Map(); - const components: string[][] = []; - const visit = (n: string): void => { - idx.set(n, index); - low.set(n, index); - index++; - stack.push(n); - onStack.add(n); - for (const m of edges(n)) { - if (!idx.has(m)) { - visit(m); - low.set(n, Math.min(low.get(n) as number, low.get(m) as number)); - } else if (onStack.has(m)) { - low.set(n, Math.min(low.get(n) as number, idx.get(m) as number)); - } - } - if (low.get(n) === idx.get(n)) { - const members: string[] = []; - let m: string | undefined; - do { - m = stack.pop(); - if (m !== undefined) { - onStack.delete(m); - component.set(m, components.length); - members.push(m); - } - } while (m !== n); - components.push(members); - } - }; - for (const n of nodes) if (!idx.has(n)) visit(n); - for (const [from, tos] of negative) { - for (const to of tos) { - if (component.get(from) === component.get(to)) throw new Error(`${id}: ${from} depends negatively on ${to} inside a recursive cycle; the predicate is not stratifiable`); - } - } - // Tarjan emits components in reverse topological order of dependencies: dependencies first. - return components; -} diff --git a/ir/src/compile/emit-souffle.ts b/ir/src/compile/emit-souffle.ts index 2638564..edb7826 100644 --- a/ir/src/compile/emit-souffle.ts +++ b/ir/src/compile/emit-souffle.ts @@ -21,7 +21,11 @@ export function emitSouffleProgram(program: RuleProgram): string { "// GENERATED by `acs-ir compile` from ir/provisions/*.yaml over ir/vocabulary/relations.yaml. Do not edit.", `// ACS ${program.corpus.version ?? "?"} at ${program.corpus.commit?.slice(0, 7) ?? "unknown"}.`, "// Run: souffle -F -D rules.dl (Soufflé 2.5; facts are tab-separated, one file per relation;", - "// the out dir receives one tab-separated __violation.csv per compiled provision)", + "// the out dir receives one tab-separated __violation.csv per compiled provision, and one", + "// .csv per verdict relation: fail, deviates, pass, unevaluated, not_activated, not_exercised)", + "// Two facts files describe the run itself: negotiated.facts lists (session, profile) for every profile each session", + "// negotiated, and available.facts lists every guardian-state, deployment and external relation whose facts were", + "// supplied. A relation a provision needs that is not listed there makes the provision unevaluated, never passed.", "", "// ---- column domains: a value's kind, as a subtype, so a seq is never joined to a bound ----", ]; @@ -41,6 +45,19 @@ export function emitSouffleProgram(program: RuleProgram): string { if (p.status !== "compiled" || !p.violation) continue; out.push(...emitProvision(p)); } + out.push("", "// ---- verdicts: RFC 2119 strength as facts, verdicts as rules ----", "", "// what the catalog says about each compiled provision"); + for (const rel of program.verdicts.catalog) { + out.push(`// ${rel.doc ?? rel.name}`, `.decl ${rel.name}(${columns(rel.columns)})`); + for (const tuple of rel.facts) out.push(`${rel.name}(${tuple.map((v) => (typeof v === "number" ? String(v) : JSON.stringify(v))).join(", ")}).`); + } + out.push("", "// what the rules derive; the verdicts are outputs"); + const outputs = new Set(program.verdicts.outputs); + for (const rel of program.verdicts.derived) { + out.push(`// ${rel.doc ?? rel.name}`, `.decl ${rel.name}(${columns(rel.columns)})`); + if (outputs.has(rel.name)) out.push(`.output ${rel.name}`); + } + out.push(""); + for (const rule of program.verdicts.rules) out.push(emitRule(rule)); return out.join("\n") + "\n"; } diff --git a/ir/src/compile/typing.ts b/ir/src/compile/typing.ts new file mode 100644 index 0000000..927fa31 --- /dev/null +++ b/ir/src/compile/typing.ts @@ -0,0 +1,217 @@ +/** + * The rule checker both the provision compiler and the verdict layer use: + * a variable's type is the meet of every column it fills (base type and + * domain), a head column's type comes from every rule that produces it, + * every variable in a head, a negated atom, or a comparison is bound by a + * positive atom, and the relations a rule set defines are stratified so no + * relation depends negatively on itself. + */ +import { atomVars, termVars, type Atom, type Literal, type Rule, type Term } from "./predicate.ts"; +import type { Column, ColumnType } from "./vocabulary.ts"; + +/** A column type as the checker sees it: the base type, and the domain when the value is known to come from one. */ +export interface Ty { + base: ColumnType; + domain: string | null; +} + +export function describe(t: Ty): string { + return t.domain ?? t.base; +} + +export function sameTy(a: Ty | null, b: Ty | null): boolean { + return a === null || b === null ? a === b : a.base === b.base && a.domain === b.domain; +} + +export function toTy(c: Column): Ty { + return { base: c.type, domain: c.domain }; +} + +/** + * The type of a derived relation's column from every rule that produces it. + * Variables and functors decide it: two rules must agree on the base type, + * and on the domain when both name one; a rule that supplies a base-typed + * value (a `cat` result, say) makes the column base-typed, which every + * domain fits. A constant fits any domain, so it only has to agree on the + * base type, and decides the column alone only when no rule supplies a + * variable. + */ +export function headColumnType(id: string, relation: string, i: number, producers: Rule[], envs: Env[]): Ty | null { + let acc: Ty | null = null; + let constant: ColumnType | null = null; + producers.forEach((rule, r) => { + const arg = rule.head.args[i] as Term; + if (arg.kind === "str" || arg.kind === "num") { + const base: ColumnType = arg.kind === "str" ? "symbol" : "number"; + if (constant && constant !== base) throw new Error(`${id}: ${relation} column ${i + 1} is ${constant} in one rule and ${base} in another`); + constant = base; + return; + } + const t = termType(arg, envs[r] as Env); + if (!t) return; + if (!acc) { + acc = t; + return; + } + if (acc.base !== t.base) throw new Error(`${id}: ${relation} column ${i + 1} is ${acc.base} in one rule and ${t.base} in another`); + if (acc.domain && t.domain && acc.domain !== t.domain) throw new Error(`${id}: ${relation} column ${i + 1} is ${acc.domain} in one rule and ${t.domain} in another`); + acc = { base: acc.base, domain: acc.domain && t.domain ? acc.domain : null }; + }); + const result: Ty | null = acc ?? (constant ? { base: constant, domain: null } : null); + if (result && constant && result.base !== constant) throw new Error(`${id}: ${relation} column ${i + 1} is ${result.base} in one rule and ${constant} in another`); + return result; +} + +export type Env = Map; + +/** Type every variable in a rule from its positive atoms, then check the rest. Returns the environment. */ +export function typeRule(id: string, rule: Rule, relationTypes: (name: string) => (Ty | null)[] | null, strict = false): Env { + const env: Env = new Map(); + // A variable's type is the meet of every column it fills: the base types + // must agree, and so must the domains when both are known. + const bindIn = (target: Env, name: string, type: Ty | null): void => { + if (!type) return; + const known = target.get(name); + if (!known) { + target.set(name, type); + return; + } + if (known.base !== type.base || (known.domain && type.domain && known.domain !== type.domain)) { + throw new Error(`${id}: variable ${name} is used as both ${describe(known)} and ${describe(type)} in: ${rule.source}`); + } + if (!known.domain && type.domain) target.set(name, type); + }; + const bindAtomIn = (target: Env, atom: Atom): void => { + const types = relationTypes(atom.relation); + if (!types) return; + if (types.length !== atom.args.length) throw new Error(`${id}: ${atom.relation} takes ${types.length} argument(s), got ${atom.args.length} in: ${rule.source}`); + atom.args.forEach((arg, i) => { + const t = types[i] ?? null; + if (arg.kind === "var") bindIn(target, arg.name, t); + else if (arg.kind === "str" && t?.base === "number") throw new Error(`${id}: ${atom.relation} argument ${i + 1} is a number, got a string in: ${rule.source}`); + else if (arg.kind === "num" && t?.base === "symbol") throw new Error(`${id}: ${atom.relation} argument ${i + 1} is a symbol, got a number in: ${rule.source}`); + else if (arg.kind === "func" && t?.base === "number") throw new Error(`${id}: ${atom.relation} argument ${i + 1} is a number, got ${arg.name}() in: ${rule.source}`); + }); + }; + const bind = (name: string, type: Ty | null): void => bindIn(env, name, type); + const bindAtom = (atom: Atom): void => bindAtomIn(env, atom); + // Positive atoms bind; then assignments; then everything is checked. + for (const lit of rule.body) if (lit.kind === "atom" && !lit.negated) bindAtom(lit.atom); + for (const lit of rule.body) if (lit.kind === "count") bind(lit.target, { base: "number", domain: null }); + let progressed = true; + while (progressed) { + progressed = false; + for (const lit of rule.body) { + if (lit.kind === "cmp" && lit.op === "=" && lit.left.kind === "var" && !env.has(lit.left.name)) { + const t = termType(lit.right, env); + if (t) { + bind(lit.left.name, t); + progressed = true; + } + } + } + } + if (!strict) return env; + + const bound = (t: Term): boolean => termVars(t).every((v) => env.has(v)); + for (const lit of rule.body) { + if (lit.kind === "atom" && lit.negated) { + for (const v of atomVars(lit.atom)) if (!env.has(v)) throw new Error(`${id}: variable ${v} in a negated atom is not bound by a positive atom (unsafe) in: ${rule.source}`); + bindAtom(lit.atom); // arity, constant types, and domains, now that every variable is known to be bound + } + if (lit.kind === "cmp") { + if (!bound(lit.left) || !bound(lit.right)) { + const missing = [...termVars(lit.left), ...termVars(lit.right)].filter((v) => !env.has(v)); + throw new Error(`${id}: variable ${missing[0]} in a comparison is not bound (unsafe) in: ${rule.source}`); + } + const l = termType(lit.left, env) as Ty; + const r = termType(lit.right, env) as Ty; + if (l.base !== r.base) throw new Error(`${id}: comparing ${l.base} with ${r.base} in: ${rule.source}`); + if (l.domain && r.domain && l.domain !== r.domain) throw new Error(`${id}: comparing a ${l.domain} with a ${r.domain} in: ${rule.source}`); + if (lit.op !== "=" && lit.op !== "!=" && l.base !== "number") throw new Error(`${id}: ordering comparisons need numbers, got ${l.base} in: ${rule.source}`); + } + if (lit.kind === "count") { + // The aggregate's own variables are local to it; they are typed in a copy so they never count as bound outside. + const inner: Env = new Map(env); + for (const atom of lit.atoms) bindAtomIn(inner, atom); + } + } + for (const v of atomVars(rule.head)) if (!env.has(v)) throw new Error(`${id}: head variable ${v} is not bound in the body (unsafe) in: ${rule.source}`); + for (const arg of rule.head.args) if (arg.kind === "wild") throw new Error(`${id}: a head cannot carry a wildcard in: ${rule.source}`); + return env; +} + +export function termType(term: Term, env: Env): Ty | null { + switch (term.kind) { + case "var": + return env.get(term.name) ?? null; + case "str": + return { base: "symbol", domain: null }; + case "num": + return { base: "number", domain: null }; + case "func": + return { base: "symbol", domain: null }; + case "wild": + return null; + } +} + +export function literalAtoms(lit: Literal): Atom[] { + if (lit.kind === "atom") return [lit.atom]; + if (lit.kind === "count") return lit.atoms; + return []; +} + +export function renameLiteral(lit: Literal, rename: (name: string) => string): Literal { + if (lit.kind === "atom") return { ...lit, atom: { relation: rename(lit.atom.relation), args: lit.atom.args } }; + if (lit.kind === "count") return { ...lit, atoms: lit.atoms.map((a) => ({ relation: rename(a.relation), args: a.args })) }; + return lit; +} + +/** Strata by Tarjan SCC over positive+negative edges, refusing a negative edge inside a component. */ +export function stratify(id: string, nodes: string[], positive: Map>, negative: Map>): string[][] { + const edges = (n: string): string[] => [...(positive.get(n) ?? []), ...(negative.get(n) ?? [])]; + let index = 0; + const stack: string[] = []; + const onStack = new Set(); + const idx = new Map(); + const low = new Map(); + const component = new Map(); + const components: string[][] = []; + const visit = (n: string): void => { + idx.set(n, index); + low.set(n, index); + index++; + stack.push(n); + onStack.add(n); + for (const m of edges(n)) { + if (!idx.has(m)) { + visit(m); + low.set(n, Math.min(low.get(n) as number, low.get(m) as number)); + } else if (onStack.has(m)) { + low.set(n, Math.min(low.get(n) as number, idx.get(m) as number)); + } + } + if (low.get(n) === idx.get(n)) { + const members: string[] = []; + let m: string | undefined; + do { + m = stack.pop(); + if (m !== undefined) { + onStack.delete(m); + component.set(m, components.length); + members.push(m); + } + } while (m !== n); + components.push(members); + } + }; + for (const n of nodes) if (!idx.has(n)) visit(n); + for (const [from, tos] of negative) { + for (const to of tos) { + if (component.get(from) === component.get(to)) throw new Error(`${id}: ${from} depends negatively on ${to} inside a recursive cycle; the predicate is not stratifiable`); + } + } + // Tarjan emits components in reverse topological order of dependencies: dependencies first. + return components; +} diff --git a/ir/src/compile/verdict-layer.ts b/ir/src/compile/verdict-layer.ts new file mode 100644 index 0000000..4cdf492 --- /dev/null +++ b/ir/src/compile/verdict-layer.ts @@ -0,0 +1,221 @@ +/** + * The verdict layer: RFC 2119 strength as facts, verdicts as rules. + * + * A provision's rules derive its violations. What a violation means is a + * question of the provision's keyword and of the session: a MUST breached + * in a session that activated the provision's profile is a failure, a + * SHOULD breached there is a deviation, a provision whose relations were + * not supplied is unevaluated, and a conditional obligation whose + * condition never arose is not exercised. Until this layer those decisions + * were TypeScript. Here they are facts generated from the catalog + * (`strength`, `polarity`, `requires_profile`, `needs`, `conditional`, + * `compiled`), two relations the run supplies (`negotiated`, `available`), + * and nine rules, so the published Soufflé program produces verdicts and + * the differential oracle checks them. + * + * Each compiled provision also gets a projection rule, `violated(P, S)`, + * attributing its violations to a session through a subject column that + * holds a session or a seq; a provision with neither does not compile. A + * conditional provision gets `exercised(P, S)`: the positive, non-static + * atoms of its violation rules, which is the situation the rule guards on. + */ +import { PROFILES, effectiveKeyword, polarityOf, strengthOf, type CatalogEntry } from "../catalog/catalog.ts"; +import type { CompiledProvision } from "./compile.ts"; +import { formatTerm, parseRule, type Atom, type Rule, type Term } from "./predicate.ts"; +import { stratify, toTy, typeRule, type Ty } from "./typing.ts"; +import type { Column, ColumnType, Relation, Vocabulary } from "./vocabulary.ts"; + +export interface VerdictLayer { + /** Facts from the catalog, one relation per thing the rules read about a provision, tuples inline. */ + catalog: Relation[]; + /** The relations the rules derive, declared with typed columns. */ + derived: Relation[]; + /** The derived relations that are verdicts, each an output of the published program. */ + outputs: string[]; + rules: Rule[]; + /** Strata over the derived relations, lowest first. */ + strata: string[][]; + /** The domains this layer's columns declare beyond the vocabulary's. */ + domains: { name: string; type: ColumnType }[]; +} + +export const VERDICT_OUTPUTS = ["fail", "deviates", "pass", "unevaluated", "not_activated", "not_exercised"] as const; +export type VerdictRelation = (typeof VERDICT_OUTPUTS)[number]; + +const col = (name: string, type: ColumnType = "symbol", domain: string = name): Column => ({ name, type, domain }); +const PROVISION = col("provision"); +const SESSION = col("session"); + +/** The rules, written once; the projection and exercise rules per provision are generated beside them. */ +const RULES = [ + "active(P, S) :- requires_profile(P, Pr), negotiated(S, Pr).", + "not_activated(P, S) :- provision(P), negotiated(S, _), not active(P, S).", + "unevaluated(P) :- needs(P, R), not available(R).", + "not_exercised(P, S) :- conditional(P), active(P, S), not unevaluated(P), not exercised(P, S).", + 'fail(P, S) :- violated(P, S), active(P, S), strength(P, "must"), not unevaluated(P).', + 'deviates(P, S) :- violated(P, S), active(P, S), strength(P, "should"), not unevaluated(P).', + "pass(P, S) :- compiled(P), active(P, S), not conditional(P), not unevaluated(P), not violated(P, S).", + "pass(P, S) :- conditional(P), active(P, S), exercised(P, S), not unevaluated(P), not violated(P, S).", +]; + +export function buildVerdictLayer(vocabulary: Vocabulary, entries: CatalogEntry[], provisions: CompiledProvision[]): { layer: VerdictLayer; problems: { id: string; message: string }[] } { + for (const name of ["envelope", "negotiated", "available"]) { + if (!vocabulary.relations.has(name)) throw new Error(`verdicts: the vocabulary has no ${name} relation; the verdict layer reads envelope, negotiated and available`); + } + const problems: { id: string; message: string }[] = []; + const records = new Map(entries.map((e) => [e.manifest.id, e])); + const compiled = provisions.filter((p) => p.status === "compiled" && p.violation); + + const facts = { + provision: [] as (string | number)[][], + compiled: [] as (string | number)[][], + strength: [] as (string | number)[][], + polarity: [] as (string | number)[][], + requires_profile: [] as (string | number)[][], + needs: [] as (string | number)[][], + conditional: [] as (string | number)[][], + }; + // Every Requirement is scoped to the profiles that activate it, compiled or not, so a permission or a non-testable provision in a profile the session never negotiated is reported as not activated. + for (const entry of entries) { + if (entry.manifest.type !== "Requirement") continue; + facts.provision.push([entry.manifest.id]); + for (const profile of entry.record.profile === "all" ? PROFILES : entry.record.profile) facts.requires_profile.push([entry.manifest.id, profile]); + } + const generated: string[] = []; + for (const p of compiled) { + const entry = records.get(p.id); + if (!entry) throw new Error(`${p.id}: compiled but not in the catalog`); + const keyword = effectiveKeyword(entry.manifest, entry.record); + if (!keyword) { + problems.push({ id: p.id, message: `${p.id}: no RFC 2119 keyword to judge it by` }); + continue; + } + try { + generated.push(projection(vocabulary, p)); + if (entry.record.modality_kind === "conditional-on-exercise") generated.push(...exercise(vocabulary, p)); + } catch (error) { + problems.push({ id: p.id, message: error instanceof Error ? error.message : String(error) }); + continue; + } + facts.compiled.push([p.id]); + facts.strength.push([p.id, strengthOf(keyword)]); + facts.polarity.push([p.id, polarityOf(keyword)]); + for (const e of p.external_facts) facts.needs.push([p.id, e.relation]); + if (entry.record.modality_kind === "conditional-on-exercise") facts.conditional.push([p.id]); + } + + const catalog: Relation[] = [ + { name: "provision", source: "catalog", columns: [PROVISION], doc: "Every Requirement in the catalog, compiled or not.", facts: facts.provision }, + { name: "compiled", source: "catalog", columns: [PROVISION], doc: "A provision with compiled rules.", facts: facts.compiled }, + { name: "strength", source: "catalog", columns: [PROVISION, col("strength")], doc: "The provision's RFC 2119 strength: must, should, or may.", facts: facts.strength }, + { name: "polarity", source: "catalog", columns: [PROVISION, col("polarity")], doc: "Whether the sentence obliges (MUST, SHOULD) or prohibits (MUST NOT, SHOULD NOT).", facts: facts.polarity }, + { name: "requires_profile", source: "catalog", columns: [PROVISION, col("profile")], doc: "A profile that activates the provision; `all` is expanded to every profile.", facts: facts.requires_profile.sort((a, b) => String(a[0]).localeCompare(String(b[0])) || String(a[1]).localeCompare(String(b[1]))) }, + { name: "needs", source: "catalog", columns: [PROVISION, col("relation")], doc: "A relation the provision's rules read whose tuples are not derived from the wire.", facts: facts.needs }, + { name: "conditional", source: "catalog", columns: [PROVISION], doc: "An obligation conditional on a permission being exercised.", facts: facts.conditional }, + ]; + const derived: Relation[] = [ + { name: "violated", source: "derived", columns: [PROVISION, SESSION], doc: "The provision's violation relation, attributed to a session.", facts: [] }, + { name: "exercised", source: "derived", columns: [PROVISION, SESSION], doc: "The situation a conditional provision's rules guard on arose in the session.", facts: [] }, + { name: "active", source: "derived", columns: [PROVISION, SESSION], doc: "The session negotiated a profile that activates the provision.", facts: [] }, + { name: "unevaluated", source: "derived", columns: [PROVISION], doc: "A relation the provision needs was not supplied; no verdict.", facts: [] }, + { name: "not_activated", source: "derived", columns: [PROVISION, SESSION], doc: "No negotiated profile activates the provision in the session.", facts: [] }, + { name: "not_exercised", source: "derived", columns: [PROVISION, SESSION], doc: "The condition never arose in the session; the obligation had nothing to bind.", facts: [] }, + { name: "fail", source: "derived", columns: [PROVISION, SESSION], doc: "A MUST or MUST NOT violated in a session that activated it.", facts: [] }, + { name: "deviates", source: "derived", columns: [PROVISION, SESSION], doc: "A SHOULD or SHOULD NOT violated in a session that activated it.", facts: [] }, + { name: "pass", source: "derived", columns: [PROVISION, SESSION], doc: "Active, evaluated, exercised where conditional, and not violated.", facts: [] }, + ]; + + const rules = [...new Set([...generated, ...RULES])].map((text) => parseRule(text)); + const declared = new Map(); + for (const r of [...catalog, ...derived]) declared.set(r.name, r.columns); + for (const p of compiled) if (p.violation) declared.set(p.violation.name, p.violation.columns); + const relationTypes = (name: string): (Ty | null)[] | null => vocabulary.relations.get(name)?.columns.map(toTy) ?? declared.get(name)?.map(toTy) ?? null; + for (const rule of rules) { + const env = typeRule("verdicts", rule, relationTypes, true); + const columns = declared.get(rule.head.relation); + if (!columns) throw new Error(`verdicts: ${rule.head.relation} is not a verdict-layer relation in: ${rule.source}`); + if (columns.length !== rule.head.args.length) throw new Error(`verdicts: ${rule.head.relation} has ${columns.length} column(s), the head ${rule.head.args.length} in: ${rule.source}`); + rule.head.args.forEach((arg, i) => { + const want = columns[i] as Column; + const got: Ty | null = arg.kind === "var" ? (env.get(arg.name) ?? null) : arg.kind === "str" ? { base: "symbol", domain: null } : arg.kind === "num" ? { base: "number", domain: null } : null; + if (!got) throw new Error(`verdicts: head argument ${i + 1} of ${rule.head.relation} is untyped in: ${rule.source}`); + if (got.base !== want.type || (got.domain && want.domain && got.domain !== want.domain)) { + throw new Error(`verdicts: ${rule.head.relation} column ${want.name} is ${want.domain ?? want.type}, got ${got.domain ?? got.base} in: ${rule.source}`); + } + }); + } + + const local = new Set(derived.map((r) => r.name)); + const positive = new Map>(); + const negative = new Map>(); + for (const rel of local) { + positive.set(rel, new Set()); + negative.set(rel, new Set()); + } + for (const rule of rules) { + for (const lit of rule.body) { + if (lit.kind === "atom" && local.has(lit.atom.relation)) (lit.negated ? negative : positive).get(rule.head.relation)?.add(lit.atom.relation); + } + } + const strata = stratify("verdicts", [...local], positive, negative); + const domains = new Map(); + for (const r of [...catalog, ...derived]) for (const c of r.columns) if (c.domain && !vocabulary.domains.has(c.domain)) domains.set(c.domain, c.type); + return { + layer: { catalog, derived, outputs: [...VERDICT_OUTPUTS], rules, strata, domains: [...domains.entries()].sort(([a], [b]) => a.localeCompare(b)).map(([name, type]) => ({ name, type })) }, + problems, + }; +} + +/** `violated(P, S)` from the provision's violation relation, through a subject column holding a session or a seq. */ +function projection(vocabulary: Vocabulary, p: CompiledProvision): string { + const v = p.violation as NonNullable; + const seqRelation = vocabulary.relations.get("envelope"); + if (!seqRelation) throw new Error(`${p.id}: the vocabulary has no envelope relation to attribute a seq to a session`); + const subject = v.columns.slice(0, p.subject.length); + const witness = v.columns.slice(p.subject.length); + const pick = (domain: string): number => { + const i = subject.findIndex((c) => c.domain === domain); + return i !== -1 ? i : witness.findIndex((c) => c.domain === domain) + (witness.some((c) => c.domain === domain) ? subject.length : -1 - subject.length); + }; + const session = pick("session"); + const seq = pick("seq"); + if (session >= 0) return `violated("${p.id}", S) :- ${v.name}(${v.columns.map((_, i) => (i === session ? "S" : "_")).join(", ")}).`; + if (seq >= 0) return `violated("${p.id}", S) :- ${v.name}(${v.columns.map((_, i) => (i === seq ? "Q" : "_")).join(", ")}), envelope(Q, S, _, _, _).`; + throw new Error(`${p.id}: no subject or witness column holds a session or a seq, so a violation cannot be attributed to a session`); +} + +/** `exercised(P, S)` per violation rule: its positive, non-static vocabulary atoms, attributed to a session. */ +function exercise(vocabulary: Vocabulary, p: CompiledProvision): string[] { + const v = p.violation as NonNullable; + const out: string[] = []; + for (const rule of p.rules) { + if (rule.head.relation !== v.name) continue; + const atoms: Atom[] = []; + for (const lit of rule.body) { + if (lit.kind !== "atom" || lit.negated) continue; + const rel = vocabulary.relations.get(lit.atom.relation); + if (rel && rel.source !== "static") atoms.push(lit.atom); + } + if (atoms.length === 0) throw new Error(`${p.id}: conditional on exercise, but a violation rule has no positive vocabulary atom to read the condition from: ${rule.source}`); + let session: string | null = null; + let seq: string | null = null; + const used = new Set(); + for (const atom of atoms) { + const columns = vocabulary.relations.get(atom.relation)?.columns ?? []; + atom.args.forEach((arg: Term, i) => { + if (arg.kind !== "var") return; + used.add(arg.name); + if (columns[i]?.domain === "session") session = session ?? arg.name; + if (columns[i]?.domain === "seq") seq = seq ?? arg.name; + }); + } + // The session variable joined in through envelope must not collide with the rule's own. + let fresh = "Session"; + for (let n = 2; used.has(fresh); n++) fresh = `Session${n}`; + const body = atoms.map((a) => `${a.relation}(${a.args.map(formatTerm).join(", ")})`); + if (session) out.push(`exercised("${p.id}", ${session}) :- ${body.join(", ")}.`); + else if (seq) out.push(`exercised("${p.id}", ${fresh}) :- ${body.join(", ")}, envelope(${seq}, ${fresh}, _, _, _).`); + else throw new Error(`${p.id}: conditional on exercise, but no positive atom binds a session or a seq in: ${rule.source}`); + } + return out; +} diff --git a/ir/src/compile/vocabulary.ts b/ir/src/compile/vocabulary.ts index 70899f4..e92a5da 100644 --- a/ir/src/compile/vocabulary.ts +++ b/ir/src/compile/vocabulary.ts @@ -20,7 +20,8 @@ import { readFileSync } from "node:fs"; import { resolve } from "node:path"; export type ColumnType = "symbol" | "number"; -export type RelationSource = "wire" | "external" | "guardian-state" | "deployment" | "static"; +/** Where a relation's tuples come from. `catalog` and `derived` are the verdict layer's: generated from the provision records, and computed by the verdict rules; neither is declared in relations.yaml. */ +export type RelationSource = "wire" | "external" | "guardian-state" | "deployment" | "static" | "catalog" | "derived"; export interface Column { name: string; diff --git a/ir/src/main.ts b/ir/src/main.ts index f9173a4..987d598 100644 --- a/ir/src/main.ts +++ b/ir/src/main.ts @@ -64,7 +64,8 @@ import { emitSouffleProgram } from "./compile/emit-souffle.ts"; import { emitTlaInvariants } from "./compile/emit-tla.ts"; import { defaultVocabularyPath, loadVocabulary } from "./compile/vocabulary.ts"; import { differentialCheck, findSouffle } from "./verify/differential.ts"; -import { evaluate, unified } from "./verify/evaluate.ts"; +import { evaluateProgram, unified } from "./verify/evaluate.ts"; +import { verdictRows } from "./verify/differential.ts"; import { readFacts } from "./verify/facts.ts"; import { renderCompile, renderDifferential } from "./render/compile.ts"; import { renderConformanceReport } from "./render/report.ts"; @@ -84,7 +85,7 @@ const USAGE = [ " acs-ir lint [--corpus ] [--build ] [--baseline ] [--provisions ] [--ids ] [--schemas ] [--conformance ] [--sources ] [--exclusions ]", " acs-ir compile [--check] [--manifest ] [--provisions ] [--vocabulary ] [--dist ] [--build ]", " acs-ir verify [--guardian ] [--deployment ] [--hmac-key ] [--out ] [--json ]", - " acs-ir verify --facts [--build ]", + " acs-ir verify --facts [--build ] (prints violations, then verdict rows: relation, provision, session)", " acs-ir differential [--fixtures ] [--build ] [--dist ] [--souffle ]", " acs-ir ids next [--ids ]", ].join("\n"); @@ -304,9 +305,10 @@ function verify(rest: string[]): number { const program = loadProgram(buildRoot); if (!program) return 1; if (factsDir) { - const violations = evaluate(program, readFacts(factsDir, program.relations)); - process.stdout.write(violations.length ? violations.map(unified).join("\n") + "\n" : ""); - console.error(`acs-ir verify: ${violations.length} violation(s) over ${factsDir}.`); + const evaluation = evaluateProgram(program, readFacts(factsDir, program.relations)); + const rows = [...evaluation.violations.map(unified), ...verdictRows(evaluation.verdicts)]; + process.stdout.write(rows.length ? rows.join("\n") + "\n" : ""); + console.error(`acs-ir verify: ${evaluation.violations.length} violation(s) over ${factsDir}; ${rows.length - evaluation.violations.length} verdict row(s).`); return 0; } const trace = rest.find((a) => !a.startsWith("--") && !flagValues(rest).has(a)); @@ -328,11 +330,11 @@ function verify(rest: string[]): number { const facts = new Map(normalized.facts); for (const rel of program.relations) if (rel.source === "static") facts.set(rel.name, rel.facts.map((t) => [...t])); for (const [relation, tuples] of external.facts) facts.set(relation, [...(facts.get(relation) ?? []), ...tuples]); - const violations = evaluate(program, facts); + const evaluation = evaluateProgram(program, facts); const negotiated = [...new Set(normalized.sessions.flatMap((s) => s.profiles))]; const stale = new Set(checkStaleness(catalog).stale.map((s) => s.id)); - const verdicts = judge(program, catalog, violations, facts, negotiated.length ? negotiated : ["acs-core"], external.available, stale); - const input = { corpus: program.corpus, trace, sessions: normalized.sessions, negotiated: negotiated.length ? negotiated : ["acs-core"], available: [...external.available].sort(), verdicts }; + const verdicts = judge(program, catalog, evaluation, facts, stale); + const input = { corpus: program.corpus, trace, sessions: normalized.sessions, negotiated: negotiated.length ? negotiated : ["acs-core"], available: [...external.available].filter((r) => r !== "available").sort(), verdicts }; const report = renderConformanceReport(input); process.stdout.write(report); mkdirSync(buildRoot, { recursive: true }); @@ -340,7 +342,8 @@ function verify(rest: string[]): number { writeFileSync(out, report); writeFileSync(flagValue(rest, "--json") ?? join(buildRoot, "conformance-report.json"), JSON.stringify(input, null, 2) + "\n"); const failed = verdicts.filter((v) => v.verdict === "fail").length; - console.error(`acs-ir verify: ${failed} provision(s) violated; wrote ${out}.`); + const deviating = verdicts.filter((v) => v.verdict === "deviates").length; + console.error(`acs-ir verify: ${failed} provision(s) violated, ${deviating} deviating from a SHOULD; wrote ${out}.`); return failed === 0 ? 0 : 1; } diff --git a/ir/src/render/compile.ts b/ir/src/render/compile.ts index 8a2a8eb..160ad1e 100644 --- a/ir/src/render/compile.ts +++ b/ir/src/render/compile.ts @@ -11,6 +11,9 @@ export function renderCompile(program: RuleProgram): string { const counts = new Map(); for (const p of program.provisions) counts.set(p.status, (counts.get(p.status) ?? 0) + 1); out.push(`${program.provisions.length} provisions: ${[...counts.entries()].map(([k, v]) => `${v} ${k}`).join(", ")}.`, ""); + const strength = new Map(); + for (const t of program.verdicts.catalog.find((r) => r.name === "strength")?.facts ?? []) strength.set(String(t[1]), (strength.get(String(t[1])) ?? 0) + 1); + out.push(`Verdict layer: ${program.verdicts.rules.length} rules over ${program.verdicts.catalog.length} catalog relations; compiled provisions by strength: ${[...strength.entries()].map(([k, v]) => `${v} ${k}`).join(", ")}.`, ""); out.push("| provision | status | subject | witness | external facts | detail |", "|---|---|---|---|---|---|"); for (const p of program.provisions) { out.push( @@ -27,12 +30,18 @@ export function renderCompile(program: RuleProgram): string { export function renderDifferential(report: DifferentialReport): string { const out = ["## Differential", "", report.souffle ? `Soufflé: ${report.souffle}` : "Soufflé: not available; evaluator checked against expectations only.", ""]; for (const f of report.fixtures) { - out.push(`### ${f.fixture}: ${f.ok ? "agree" : "DIVERGE"} (evaluator ${f.evaluator.length}, expected ${f.expected.length}${f.souffle ? `, souffle ${f.souffle.length}` : ""})`); + out.push( + `### ${f.fixture}: ${f.ok ? "agree" : "DIVERGE"} (evaluator ${f.evaluator.length}, expected ${f.expected.length}${f.souffle ? `, souffle ${f.souffle.length}` : ""}; verdicts: evaluator ${f.verdicts.length}${f.souffle_verdicts ? `, souffle ${f.souffle_verdicts.length}` : ""})`, + ); const rows: string[] = []; for (const t of f.evaluator_vs_expected.only_evaluator) rows.push(`- only the evaluator, not expected: ${t}`); for (const t of f.evaluator_vs_expected.only_expected) rows.push(`- expected, not derived by the evaluator: ${t}`); for (const t of f.evaluator_vs_souffle?.only_evaluator ?? []) rows.push(`- only the evaluator, not Soufflé: ${t}`); for (const t of f.evaluator_vs_souffle?.only_souffle ?? []) rows.push(`- only Soufflé, not the evaluator: ${t}`); + for (const t of f.verdicts_vs_expected?.only_evaluator ?? []) rows.push(`- verdict only the evaluator derived, not expected: ${t}`); + for (const t of f.verdicts_vs_expected?.only_expected ?? []) rows.push(`- verdict expected, not derived by the evaluator: ${t}`); + for (const t of f.verdicts_vs_souffle?.only_evaluator ?? []) rows.push(`- verdict only the evaluator derived, not Soufflé: ${t}`); + for (const t of f.verdicts_vs_souffle?.only_souffle ?? []) rows.push(`- verdict only Soufflé derived, not the evaluator: ${t}`); out.push(...rows, ""); } return out.join("\n") + "\n"; diff --git a/ir/src/render/provision-index.ts b/ir/src/render/provision-index.ts index 608bc27..baf86a4 100644 --- a/ir/src/render/provision-index.ts +++ b/ir/src/render/provision-index.ts @@ -5,7 +5,7 @@ * will publish (U26), and U14 the test-coverage table from the citation * index over `ir/test/conformance/` (R6.3). */ -import type { Catalog, CatalogEntry } from "../catalog/catalog.ts"; +import { effectiveKeyword, type Catalog, type CatalogEntry } from "../catalog/catalog.ts"; import { idToAnchor } from "../ids.ts"; export function renderProvisionIndex(catalog: Catalog, corpus: { version: string | null; commit: string | null }, citations: Map = new Map()): string { @@ -20,11 +20,11 @@ export function renderProvisionIndex(catalog: Catalog, corpus: { version: string "## Index", "", ...table( - ["ID", "Type", "Level", "Actor", "Profile", "Evidence", "Modality", "Status", "Source", "Title"], + ["ID", "Type", "Keyword", "Actor", "Profile", "Evidence", "Modality", "Status", "Source", "Title"], catalog.entries.map(({ manifest: m, record: r }) => [ `[${m.id}](#${m.id.toLowerCase()})`, m.type, - m.level ?? "—", + (m.type === "Requirement" ? effectiveKeyword(m, r) : m.level) ?? "—", r.actor, r.profile === "all" ? "all" : r.profile.join(", "), r.evidence_class, @@ -60,8 +60,9 @@ function renderDetail({ manifest: m, record: r }: CatalogEntry): string[] { "", `- Actor: ${r.actor}; reported against: ${r.reported_against}`, `- Profile: ${r.profile === "all" ? "all" : r.profile.join(", ")}${r.activation ? `; activation: ${r.activation}` : ""}`, - `- Modality: ${r.modality_kind}; evidence: ${r.evidence_class}`, + `- Modality: ${r.modality_kind}; evidence: ${r.evidence_class}${m.type === "Requirement" ? `; keyword: ${effectiveKeyword(m, r) ?? "none"}` : ""}`, ]; + if (r.keyword) lines.push(`- Keyword ${r.keyword} stated by the record, not the span (${m.level ?? "no keyword"}): ${r.keyword_basis}`); if (r.schema_refs.length) lines.push(`- Schema: ${r.schema_refs.map((s) => `\`${s.file}#${s.pointer}\``).join(", ")}`); if (r.depends_on.length) lines.push(`- Depends on: ${r.depends_on.map(link).join(", ")}`); if (r.restates) lines.push(`- Restates: ${link(r.restates)}`); diff --git a/ir/src/render/report.ts b/ir/src/render/report.ts index 382be3c..b1c6673 100644 --- a/ir/src/render/report.ts +++ b/ir/src/render/report.ts @@ -20,7 +20,7 @@ export interface ReportInput { verdicts: ProvisionVerdict[]; } -const ORDER: Verdict[] = ["fail", "pass", "unevaluated", "not-exercised", "not-activated", "permission", "non-testable", "inexpressible", "exclusion", "invariant", "definition"]; +const ORDER: Verdict[] = ["fail", "deviates", "pass", "unevaluated", "not-exercised", "not-activated", "permission", "non-testable", "inexpressible", "exclusion", "invariant", "definition"]; export function renderConformanceReport(input: ReportInput): string { const counts = new Map(); @@ -42,25 +42,28 @@ export function renderConformanceReport(input: ReportInput): string { "", "## Obligations per claimed profile", "", - "| profile | active obligations | met | unmet | unevaluated |", - "|---|---|---|---|---|", + "| profile | active obligations | met | unmet | deviating | unevaluated |", + "|---|---|---|---|---|---|", ]; for (const profile of input.negotiated) { - const active = input.verdicts.filter((v) => v.type === "Requirement" && (v.profile === "all" || v.profile.includes(profile)) && ["pass", "fail", "unevaluated", "not-exercised"].includes(v.verdict)); + const active = input.verdicts.filter((v) => v.type === "Requirement" && (v.profile === "all" || v.profile.includes(profile)) && ["pass", "fail", "deviates", "unevaluated", "not-exercised"].includes(v.verdict)); const met = active.filter((v) => v.verdict === "pass" || v.verdict === "not-exercised").length; const unmet = active.filter((v) => v.verdict === "fail").length; + const deviating = active.filter((v) => v.verdict === "deviates").length; const unevaluated = active.filter((v) => v.verdict === "unevaluated").length; - out.push(`| ${profile} | ${active.length} | ${met} | ${unmet} | ${unevaluated} |`); + out.push(`| ${profile} | ${active.length} | ${met} | ${unmet} | ${deviating} | ${unevaluated} |`); } - out.push("", "## Verdicts", "", "| provision | verdict | level | actor | profile | reason |", "|---|---|---|---|---|---|"); + const several = input.sessions.length > 1; + out.push("", "## Verdicts", "", "| provision | verdict | keyword | actor | profile | reason |", "|---|---|---|---|---|---|"); for (const v of [...input.verdicts].sort((a, b) => ORDER.indexOf(a.verdict) - ORDER.indexOf(b.verdict) || a.id.localeCompare(b.id))) { - out.push(`| ${v.id} ${v.title} | ${v.verdict}${v.needs_review ? " (needs-review)" : ""} | ${v.level ?? "—"} | ${v.actor} | ${v.profile === "all" ? "all" : v.profile.join(", ")} | ${(v.reason ?? "").replace(/\|/g, "\\|")} |`); + const perSession = several && v.sessions.length ? `${v.reason ? " " : ""}sessions: ${v.sessions.map((s) => `${s.session} ${s.verdict}`).join(", ")}` : ""; + out.push(`| ${v.id} ${v.title} | ${v.verdict}${v.needs_review ? " (needs-review)" : ""} | ${v.keyword ?? "—"} | ${v.actor} | ${v.profile === "all" ? "all" : v.profile.join(", ")} | ${((v.reason ?? "") + perSession).replace(/\|/g, "\\|")} |`); } - const failures = input.verdicts.filter((v) => v.verdict === "fail"); + const failures = input.verdicts.filter((v) => v.verdict === "fail" || v.verdict === "deviates"); out.push("", "## Evidence", ""); if (failures.length === 0) out.push("No violations."); for (const v of failures) { - out.push(`### ${v.id}: ${v.title}`, "", `${v.evidence.length} violation(s).`, ""); + out.push(`### ${v.id}: ${v.title}`, "", `${v.evidence.length} violation(s)${v.verdict === "deviates" ? ` of a ${v.keyword ?? "SHOULD"}: a deviation, not a failure` : ""}.`, ""); for (const e of v.evidence) { out.push(`- subject ${e.subject.map((s) => `${s.name}=${s.value}`).join(", ")}; witness ${e.witness.map((w) => `${w.name}=${w.value}`).join(", ")}`); for (const f of e.facts) out.push(` - ${f.relation}(${f.tuple.join(", ")})`); diff --git a/ir/src/verify/differential.ts b/ir/src/verify/differential.ts index 00f3e8f..557764a 100644 --- a/ir/src/verify/differential.ts +++ b/ir/src/verify/differential.ts @@ -5,7 +5,11 @@ * A fixture is a directory of `.facts` files plus `expected.tsv`, the * violations the fixture is meant to produce, one per line as provision, * subject values joined by "|", witness values joined by "|" (the unified - * form; Soufflé's per-provision CSVs are read back into it). The evaluator runs in-process; Soufflé runs as a subprocess when + * form; Soufflé's per-provision CSVs are read back into it), and + * optionally `expected-verdicts.tsv`, the verdict relations' tuples, one + * per line as relation then columns. The verdict relations are compared + * between the engines on every fixture, and against the expectation when + * the file exists. The evaluator runs in-process; Soufflé runs as a subprocess when * a binary is available (`SOUFFLE` env var or `souffle` on PATH), which in * CI it always is. Divergence in either direction is reported as the * tuples only one side derived (U31), and the evaluator is additionally @@ -17,8 +21,8 @@ import { existsSync, mkdirSync, mkdtempSync, readdirSync, readFileSync, statSync import { tmpdir } from "node:os"; import { join } from "node:path"; import type { RuleProgram } from "../compile/compile.ts"; -import { evaluate, unified } from "./evaluate.ts"; -import { readFacts, writeFacts } from "./facts.ts"; +import { evaluateProgram, unified } from "./evaluate.ts"; +import { readFacts, writeFacts, type FactSet } from "./facts.ts"; export interface FixtureResult { fixture: string; @@ -29,9 +33,22 @@ export interface FixtureResult { evaluator_vs_expected: { only_evaluator: string[]; only_expected: string[] }; /** Present only when Soufflé ran. */ evaluator_vs_souffle: { only_evaluator: string[]; only_souffle: string[] } | null; + /** The verdict relations' tuples, one per line as relation then columns. */ + verdicts: string[]; + souffle_verdicts: string[] | null; + /** Present when the fixture has `expected-verdicts.tsv`. */ + verdicts_vs_expected: { only_evaluator: string[]; only_expected: string[] } | null; + verdicts_vs_souffle: { only_evaluator: string[]; only_souffle: string[] } | null; ok: boolean; } +/** A verdict relation's tuples in the form the fixtures pin: relation, then each column, tab-separated. */ +export function verdictRows(verdicts: FactSet): string[] { + const rows: string[] = []; + for (const [relation, tuples] of verdicts) for (const t of tuples) rows.push([relation, ...t.map(String)].join("\t")); + return rows.sort(); +} + export interface DifferentialReport { souffle: string | null; fixtures: FixtureResult[]; @@ -60,8 +77,11 @@ export function differentialCheck(program: RuleProgram, dl: string, fixturesDir: export function runFixture(program: RuleProgram, dl: string, dir: string, name: string, souffle: string | null): FixtureResult { const facts = readFacts(join(dir, "facts"), program.relations); - const evaluator = evaluate(program, facts).map(unified); + const evaluation = evaluateProgram(program, facts); + const evaluator = evaluation.violations.map(unified); + const verdicts = verdictRows(evaluation.verdicts); const expected = readExpected(join(dir, "expected.tsv")); + const expectedVerdicts = existsSync(join(dir, "expected-verdicts.tsv")) ? readExpected(join(dir, "expected-verdicts.tsv")) : null; const result: FixtureResult = { fixture: name, evaluator, @@ -69,26 +89,33 @@ export function runFixture(program: RuleProgram, dl: string, dir: string, name: expected, evaluator_vs_expected: { only_evaluator: minus(evaluator, expected), only_expected: minus(expected, evaluator) }, evaluator_vs_souffle: null, + verdicts, + souffle_verdicts: null, + verdicts_vs_expected: expectedVerdicts ? { only_evaluator: minus(verdicts, expectedVerdicts), only_expected: minus(expectedVerdicts, verdicts) } : null, + verdicts_vs_souffle: null, ok: false, }; if (souffle) { - result.souffle = runSouffle(souffle, dl, program, facts); - result.evaluator_vs_souffle = { only_evaluator: minus(evaluator, result.souffle), only_souffle: minus(result.souffle, evaluator) }; + const ran = runSouffle(souffle, dl, program, facts); + result.souffle = ran.violations; + result.souffle_verdicts = ran.verdicts; + result.evaluator_vs_souffle = { only_evaluator: minus(evaluator, ran.violations), only_souffle: minus(ran.violations, evaluator) }; + result.verdicts_vs_souffle = { only_evaluator: minus(verdicts, ran.verdicts), only_souffle: minus(ran.verdicts, verdicts) }; } - result.ok = - result.evaluator_vs_expected.only_evaluator.length === 0 && - result.evaluator_vs_expected.only_expected.length === 0 && - (result.evaluator_vs_souffle === null || (result.evaluator_vs_souffle.only_evaluator.length === 0 && result.evaluator_vs_souffle.only_souffle.length === 0)); + const agree = (d: { only_evaluator: string[]; only_expected?: string[]; only_souffle?: string[] } | null): boolean => + d === null || (d.only_evaluator.length === 0 && (d.only_expected ?? d.only_souffle ?? []).length === 0); + result.ok = agree(result.evaluator_vs_expected) && agree(result.evaluator_vs_souffle) && agree(result.verdicts_vs_expected) && agree(result.verdicts_vs_souffle); return result; } /** * Run stock Soufflé on the published program over the fixture's facts and * read back every provision's violation CSV in the unified form the - * fixtures and the evaluator use: provision, subject values joined by - * "|", witness values joined by "|". + * fixtures and the evaluator use (provision, subject values joined by + * "|", witness values joined by "|"), and every verdict relation's CSV as + * relation then columns. */ -export function runSouffle(souffle: string, dl: string, program: RuleProgram, facts: ReturnType): string[] { +export function runSouffle(souffle: string, dl: string, program: RuleProgram, facts: ReturnType): { violations: string[]; verdicts: string[] } { const work = mkdtempSync(join(tmpdir(), "acs-ir-souffle-")); const factsDir = join(work, "facts"); const outDir = join(work, "out"); @@ -111,7 +138,13 @@ export function runSouffle(souffle: string, dl: string, program: RuleProgram, fa rows.push(`${p.id}\t${cells.slice(0, p.subject.length).join("|")}\t${cells.slice(p.subject.length).join("|")}`); } } - return rows.sort(); + const verdicts: string[] = []; + for (const relation of program.verdicts.outputs) { + const csv = join(outDir, `${relation}.csv`); + if (!existsSync(csv)) continue; + for (const line of readFileSync(csv, "utf8").split("\n")) if (line.trim() !== "") verdicts.push(`${relation}\t${line}`); + } + return { violations: rows.sort(), verdicts: verdicts.sort() }; } function readExpected(path: string): string[] { diff --git a/ir/src/verify/evaluate.ts b/ir/src/verify/evaluate.ts index 70e827e..0a80a0b 100644 --- a/ir/src/verify/evaluate.ts +++ b/ir/src/verify/evaluate.ts @@ -9,6 +9,10 @@ * construct nobody had checked. * * Running on a laptop needs only `bun install` and this file (R3.9). + * + * `evaluateProgram()` runs the provisions and then the verdict layer over + * their violation relations, returning both; `evaluate()` is the + * violations alone. */ import type { CompiledProvision, RuleProgram } from "../compile/compile.ts"; import type { Atom, Literal, Rule, Term } from "../compile/predicate.ts"; @@ -28,7 +32,17 @@ export function unified(v: Violation): string { type Store = Map>; type Bindings = Map; +export interface Evaluation { + violations: Violation[]; + /** The verdict layer's output relations: fail, deviates, pass, unevaluated, not_activated, not_exercised. */ + verdicts: FactSet; +} + export function evaluate(program: RuleProgram, facts: FactSet): Violation[] { + return evaluateProgram(program, facts).violations; +} + +export function evaluateProgram(program: RuleProgram, facts: FactSet): Evaluation { const store: Store = new Map(); for (const rel of program.relations) { const table = new Map(); @@ -43,15 +57,27 @@ export function evaluate(program: RuleProgram, facts: FactSet): Violation[] { violations.push({ provision: p.id, subject: t.slice(0, p.subject.length), witness: t.slice(p.subject.length) }); } } - return violations.sort((a, b) => unified(a).localeCompare(unified(b))); + // The verdict layer: catalog facts seeded, derived relations empty, then its strata. + const layer = program.verdicts; + for (const rel of layer.catalog) store.set(rel.name, new Map(rel.facts.map((t) => [key(t), [...t]]))); + for (const rel of layer.derived) store.set(rel.name, new Map()); + runStrata(layer.rules, layer.strata, store); + const verdicts: FactSet = new Map(); + for (const name of layer.outputs) verdicts.set(name, [...(store.get(name)?.values() ?? [])].sort((a, b) => key(a).localeCompare(key(b)))); + return { violations: violations.sort((a, b) => unified(a).localeCompare(unified(b))), verdicts }; } function evaluateProvision(p: CompiledProvision, store: Store): void { for (const h of p.helpers) store.set(h.name, new Map()); store.set((p.violation as NonNullable).name, new Map()); - for (const stratum of p.strata) { + runStrata(p.rules, p.strata, store); +} + +/** Semi-naive fixpoint per stratum, lowest first. */ +function runStrata(allRules: Rule[], strata: string[][], store: Store): void { + for (const stratum of strata) { const members = new Set(stratum); - const rules = p.rules.filter((r) => members.has(r.head.relation)); + const rules = allRules.filter((r) => members.has(r.head.relation)); // Semi-naive: after the first full round, only bindings that touch a delta tuple of a member relation can be new. let delta = new Map>(); for (const m of members) delta.set(m, new Map(store.get(m))); diff --git a/ir/src/verify/external-facts.ts b/ir/src/verify/external-facts.ts index fa93e51..4567456 100644 --- a/ir/src/verify/external-facts.ts +++ b/ir/src/verify/external-facts.ts @@ -126,6 +126,9 @@ export function computeExternalFacts(normalized: NormalizedTrace, relations: Rel if (options.deploymentDir && existsSync(options.deploymentDir)) { mergeFactFiles(options.deploymentDir, relations.filter((r) => r.source === "deployment"), facts, available); } + // What was supplied, as a relation, so the verdict rules can tell an empty relation from an absent one. + facts.set("available", [...available].sort().map((r) => [r])); + available.add("available"); return { facts, available }; } diff --git a/ir/src/verify/normalize-trace.ts b/ir/src/verify/normalize-trace.ts index 4307afe..265114e 100644 --- a/ir/src/verify/normalize-trace.ts +++ b/ir/src/verify/normalize-trace.ts @@ -206,6 +206,8 @@ export function normalizeTrace(lines: TraceLine[]): NormalizedTrace { } const sessionList = [...sessions.values()].map((s) => ({ ...s, profiles: s.profiles.length ? s.profiles : ["acs-core"] })); + // The verdict layer activates a provision in a session through `negotiated`. + for (const s of sessionList) for (const profile of s.profiles) add("negotiated", [s.session, profile]); return { lines, facts, sessions: sessionList, sessionOf }; } diff --git a/ir/src/verify/verdicts.ts b/ir/src/verify/verdicts.ts index 4102fe7..1c591c2 100644 --- a/ir/src/verify/verdicts.ts +++ b/ir/src/verify/verdicts.ts @@ -1,30 +1,32 @@ /** - * E12 and N45 to N47: from violation tuples to verdicts a report can carry. + * E12 and N45 to N47: from the verdict relations to verdicts a report can carry. * - * `scopeByProfile()` drops provisions the session never activated (R4.3): - * a provision's profile list must meet the profiles the trace negotiated, - * `all` always does. `applyModality()` gives permissions no verdict (R4.6) - * and marks a conditional-on-exercise obligation `not-exercised` when the - * Guardian-state relations it reads are empty. Exclusions never yield a - * violation and are reported as such (R4.8); non-testable and inexpressible - * provisions are listed, never dropped (R4.4, R3.6). A provision whose - * predicate needs a relation nobody supplied is `unevaluated`, never - * `pass`. `attachEvidence()` names each violation's subject and witness - * columns and gathers the facts that mention the subject (R3.4). + * The judgement itself is Datalog (`compile/verdict-layer.ts`): which + * sessions activated a provision, whether the relations it needs were + * supplied, whether a conditional obligation's condition arose, and + * whether a violation is a failure (MUST) or a deviation (SHOULD). This + * module reads those relations back and folds the per-session verdicts of + * a provision into the one the report shows: any failure is a failure, + * else any deviation, else any pass, else not exercised, else not + * activated. Provisions that did not compile get their verdict from the + * catalog as before: permissions yield none (R4.6), exclusions are listed + * (R4.8), non-testable and inexpressible ones are listed, never dropped + * (R4.4, R3.6). `attachEvidence()` names each violation's subject and + * witness columns and gathers the facts that mention the subject (R3.4). * * Activation conditions written in prose (R4.5) are carried into the * report as text; the ones this catalog needed mechanically are already * inside the predicates (`decision(Seq, "defer")`, `archived(Session)`). */ -import type { Catalog } from "../catalog/catalog.ts"; +import { effectiveKeyword, type CanonicalKeyword, type Catalog } from "../catalog/catalog.ts"; import type { CompiledProvision, RuleProgram } from "../compile/compile.ts"; -import type { Relation } from "../compile/vocabulary.ts"; -import type { Violation } from "./evaluate.ts"; +import type { Evaluation, Violation } from "./evaluate.ts"; import type { FactSet, Value } from "./facts.ts"; export type Verdict = | "pass" | "fail" + | "deviates" | "not-activated" | "not-exercised" | "permission" @@ -47,6 +49,8 @@ export interface ProvisionVerdict { title: string; type: string; level: string | null; + /** The RFC 2119 keyword the provision is judged by (the record's, else the marked span's). */ + keyword: CanonicalKeyword | null; actor: string; profile: string[] | "all"; activation: string | null; @@ -57,21 +61,22 @@ export interface ProvisionVerdict { /** Relations the predicate needed and nobody supplied. */ missing: string[]; evidence: Evidence[]; + /** For a compiled provision, the verdict in each session the trace holds; the report shows the fold. */ + sessions: { session: string; verdict: Verdict }[]; } -export function judge( - program: RuleProgram, - catalog: Catalog, - violations: Violation[], - facts: FactSet, - negotiated: string[], - available: Set, - stale: Set, -): ProvisionVerdict[] { +/** The fold over sessions: the first of these that any session reached. */ +const FOLD: Verdict[] = ["fail", "deviates", "pass", "not-exercised", "not-activated"]; + +export function judge(program: RuleProgram, catalog: Catalog, evaluation: Evaluation, facts: FactSet, stale: Set): ProvisionVerdict[] { const compiled = new Map(program.provisions.map((p) => [p.id, p])); - const relations = new Map(program.relations.map((r) => [r.name, r])); const byProvision = new Map(); - for (const v of violations) byProvision.set(v.provision, [...(byProvision.get(v.provision) ?? []), v]); + for (const v of evaluation.violations) byProvision.set(v.provision, [...(byProvision.get(v.provision) ?? []), v]); + const sessions = [...new Set((facts.get("negotiated") ?? []).map((t) => String(t[0])))].sort(); + const available = new Set((facts.get("available") ?? []).map((t) => String(t[0]))); + const needs = new Map(); + for (const t of program.verdicts.catalog.find((r) => r.name === "needs")?.facts ?? []) needs.set(String(t[0]), [...(needs.get(String(t[0])) ?? []), String(t[1])]); + const held = (relation: string, id: string, session: string): boolean => (evaluation.verdicts.get(relation) ?? []).some((t) => t[0] === id && (t.length < 2 || t[1] === session)); const verdicts = new Map(); for (const { manifest, record } of catalog.entries) { @@ -80,6 +85,7 @@ export function judge( title: record.title, type: manifest.type, level: manifest.level, + keyword: manifest.type === "Requirement" ? effectiveKeyword(manifest, record) : null, actor: record.actor, profile: record.profile, activation: record.activation, @@ -88,59 +94,68 @@ export function judge( reason: null, missing: [], evidence: [], + sessions: [], }; const c = compiled.get(manifest.id); + // Not activated in every session: the Datalog `not_activated` relation, over every Requirement (R4.3), checked before the catalog statuses as the report always has. + const inactive = sessions.length > 0 && sessions.every((session) => held("not_activated", manifest.id, session)); if (manifest.type === "Exclusion") verdicts.set(manifest.id, { ...base, verdict: "exclusion", reason: "ACS deliberately requires nothing here" }); else if (manifest.type === "Definition") verdicts.set(manifest.id, { ...base, verdict: "definition", reason: "a definition; verified through the Requirements that depend on it" }); else if (manifest.type === "Invariant") verdicts.set(manifest.id, { ...base, verdict: "invariant", reason: "an invariant; verified through the Requirements that enforce it" }); else if (!c) verdicts.set(manifest.id, { ...base, verdict: "unevaluated", reason: "not compiled" }); - else if (!scopeByProfile(record.profile, negotiated)) verdicts.set(manifest.id, { ...base, verdict: "not-activated", reason: `needs ${(record.profile as string[]).join(" or ")}; the session negotiated ${negotiated.join(", ")}` }); - else if (c.status === "permission") verdicts.set(manifest.id, { ...base, verdict: "permission", reason: c.reason }); + else if (inactive) { + const negotiated = [...new Set((facts.get("negotiated") ?? []).map((t) => String(t[1])))].sort(); + verdicts.set(manifest.id, { ...base, verdict: "not-activated", reason: `needs ${(record.profile as string[]).join(" or ")}; the session negotiated ${negotiated.join(", ")}`, sessions: sessions.map((session) => ({ session, verdict: "not-activated" as const })) }); + } else if (c.status === "permission") verdicts.set(manifest.id, { ...base, verdict: "permission", reason: c.reason }); else if (c.status === "non-testable") verdicts.set(manifest.id, { ...base, verdict: "non-testable", reason: c.reason }); else if (c.status === "inexpressible") verdicts.set(manifest.id, { ...base, verdict: "inexpressible", reason: c.reason }); else if (c.status === "alias") verdicts.set(manifest.id, base); // filled below once the target is known - else verdicts.set(manifest.id, applyModality(base, c, record.modality_kind, facts, relations, available, byProvision.get(manifest.id) ?? [])); + else if ((evaluation.verdicts.get("unevaluated") ?? []).some((t) => t[0] === manifest.id)) { + const missing = (needs.get(manifest.id) ?? []).filter((r) => !available.has(r)); + verdicts.set(manifest.id, { ...base, verdict: "unevaluated", missing, reason: `needs ${missing.join(", ")}, which the verifier was not given` }); + } else { + const perSession = sessions.map((session) => { + const verdict: Verdict = held("fail", manifest.id, session) + ? "fail" + : held("deviates", manifest.id, session) + ? "deviates" + : held("pass", manifest.id, session) + ? "pass" + : held("not_exercised", manifest.id, session) + ? "not-exercised" + : "not-activated"; + return { session, verdict }; + }); + const verdict = FOLD.find((v) => perSession.some((s) => s.verdict === v)) ?? "not-activated"; + const reason = + verdict === "not-activated" + ? sessions.length + ? `needs ${record.profile === "all" ? "any profile" : (record.profile as string[]).join(" or ")}; no session negotiated it` + : "no session negotiated a profile" + : verdict === "not-exercised" + ? "the permission it is conditional on was not exercised in this trace" + : verdict === "deviates" + ? `a ${base.keyword ?? "SHOULD"}: a deviation, not a failure` + : null; + const evidence = verdict === "fail" || verdict === "deviates" ? (byProvision.get(manifest.id) ?? []).map((v) => attachEvidence(c, v, facts)) : []; + verdicts.set(manifest.id, { ...base, verdict, reason, evidence, sessions: perSession }); + } } for (const c of program.provisions) { if (c.status !== "alias" || !c.alias_of) continue; const target = verdicts.get(c.alias_of); const own = verdicts.get(c.id); - if (target && own) verdicts.set(c.id, { ...own, verdict: target.verdict, reason: `${c.reason}: ${target.reason ?? target.verdict}`, missing: target.missing, evidence: target.evidence }); + if (target && own) verdicts.set(c.id, { ...own, verdict: target.verdict, reason: `${c.reason}: ${target.reason ?? target.verdict}`, missing: target.missing, evidence: target.evidence, sessions: target.sessions }); } return [...verdicts.values()].sort((a, b) => a.id.localeCompare(b.id)); } -/** N45 */ +/** N45: a provision's profile list meets the negotiated profiles; `all` always does. The verdict rules do this per session; the report uses it per claimed profile. */ export function scopeByProfile(profile: string[] | "all", negotiated: string[]): boolean { if (profile === "all") return true; return profile.some((p) => negotiated.includes(p)); } -/** N46, then N47 for a failing obligation. */ -function applyModality( - base: ProvisionVerdict, - c: CompiledProvision, - modality: string, - facts: FactSet, - relations: Map, - available: Set, - violations: Violation[], -): ProvisionVerdict { - const missing = c.relations_used.filter((r) => { - const source = relations.get(r)?.source; - return source !== "wire" && source !== "static" && !available.has(r); - }); - if (missing.length) return { ...base, verdict: "unevaluated", missing, reason: `needs ${missing.join(", ")}, which the verifier was not given` }; - if (modality === "conditional-on-exercise") { - const stateRelations = c.relations_used.filter((r) => relations.get(r)?.source === "guardian-state"); - if (stateRelations.every((r) => (facts.get(r) ?? []).length === 0)) { - return { ...base, verdict: "not-exercised", reason: "the permission it is conditional on was not exercised in this trace" }; - } - } - if (violations.length === 0) return base; - return { ...base, verdict: "fail", evidence: violations.map((v) => attachEvidence(c, v, facts)) }; -} - /** N47 */ export function attachEvidence(c: CompiledProvision, v: Violation, facts: FactSet): Evidence { const subject = c.subject.map((name, i) => ({ name, value: v.subject[i] as Value })); diff --git a/ir/test/catalog.test.ts b/ir/test/catalog.test.ts index f5250bd..9f256c3 100644 --- a/ir/test/catalog.test.ts +++ b/ir/test/catalog.test.ts @@ -1,5 +1,5 @@ import { describe, expect, it } from "bun:test"; -import { loadCatalog, parseProvisionRecord, type ProvisionRecord } from "../src/catalog/catalog.ts"; +import { canonicalKeyword, effectiveKeyword, loadCatalog, parseProvisionRecord, polarityOf, strengthOf, type ProvisionRecord } from "../src/catalog/catalog.ts"; import type { Manifest, ManifestEntry } from "../src/extract/extract.ts"; const entry = (id: string, source_file = "spec/x.md"): ManifestEntry => ({ @@ -22,6 +22,8 @@ const record = (id: string, extra: Partial = {}): ProvisionReco profile: ["acs-core"], activation: null, modality_kind: "obligation", + keyword: null, + keyword_basis: null, evidence_class: "wire", schema_refs: [], depends_on: [], @@ -95,3 +97,40 @@ describe("parseProvisionRecord -- the authored shape", () => { expect(() => parseProvisionRecord(base.concat("schema_refs:\n - file: a.json\n pointer: x").join("\n"))).toThrow("JSON Pointer starting with /"); }); }); + +describe("the RFC 2119 keyword a provision is judged by", () => { + it("canonicalizes the RFC's synonyms and derives strength and polarity", () => { + expect(["REQUIRED", "SHALL", "MUST NOT", "SHALL NOT", "RECOMMENDED", "NOT RECOMMENDED", "OPTIONAL"].map(canonicalKeyword)).toEqual(["MUST", "MUST", "MUST NOT", "MUST NOT", "SHOULD", "SHOULD NOT", "MAY"]); + expect(canonicalKeyword(null)).toBeNull(); + expect(["MUST", "MUST NOT", "SHOULD", "SHOULD NOT", "MAY"].map((k) => [strengthOf(k as "MUST"), polarityOf(k as "MUST")])).toEqual([["must", "obligation"], ["must", "prohibition"], ["should", "obligation"], ["should", "prohibition"], ["may", "obligation"]]); + }); + + it("is the marked span's first keyword unless the record states one", () => { + expect(effectiveKeyword({ level: "RECOMMENDED" }, { keyword: null })).toBe("SHOULD"); + expect(effectiveKeyword({ level: "RECOMMENDED" }, { keyword: "MUST" })).toBe("MUST"); + expect(effectiveKeyword({ level: null }, { keyword: null })).toBeNull(); + }); + + it("a record that states a keyword says why, and never a basis without a keyword", () => { + const base = ["id: ACS-REQ-0001", "title: T", "actor: guardian", "reported_against: guardian", "profile: [acs-core]", "modality_kind: obligation", "evidence_class: wire", "status: active", "since: 0.1.0", "reviewed_against: h"]; + expect(parseProvisionRecord([...base, "keyword: MUST NOT", "keyword_basis: the sentence says MAY NOT"].join("\n"))).toMatchObject({ keyword: "MUST NOT", keyword_basis: "the sentence says MAY NOT" }); + expect(() => parseProvisionRecord([...base, "keyword: MUST NOT"].join("\n"))).toThrow("say why in keyword_basis"); + expect(() => parseProvisionRecord([...base, "keyword_basis: why"].join("\n"))).toThrow("keyword_basis without a keyword"); + expect(() => parseProvisionRecord([...base, "keyword: REQUIRED", "keyword_basis: x"].join("\n"))).toThrow("keyword must be one of"); + }); + + it("the join refuses a keyword that disagrees with the modality, and a Requirement with no keyword at all", () => { + const catalog = loadCatalog(manifest({ ...entry("ACS-REQ-0001"), level: "MAY", keywords: ["MAY"] }, { ...entry("ACS-REQ-0002"), level: "MUST" }, { ...entry("ACS-REQ-0003"), level: null, keywords: [] }, { ...entry("ACS-REQ-0004"), level: "MAY", keywords: ["MAY"] }), [ + record("ACS-REQ-0001"), + record("ACS-REQ-0002", { modality_kind: "permission" }), + record("ACS-REQ-0003"), + record("ACS-REQ-0004", { keyword: "MUST NOT", keyword_basis: "the sentence says MAY NOT" }), + ]); + expect(catalog.problems).toEqual([ + "ACS-REQ-0001: an obligation is judged by MUST or SHOULD, not MAY; if the sentence says MAY NOT, state keyword: MUST NOT with keyword_basis", + "ACS-REQ-0002: a permission is judged by MAY, not MUST", + "ACS-REQ-0003: the marked span has no RFC 2119 keyword; state keyword: with keyword_basis", + ]); + }); +}); + diff --git a/ir/test/compile.test.ts b/ir/test/compile.test.ts index 94113eb..952856e 100644 --- a/ir/test/compile.test.ts +++ b/ir/test/compile.test.ts @@ -30,6 +30,8 @@ const record = (id: string, extra: Partial = {}): ProvisionReco profile: ["acs-core"], activation: null, modality_kind: "obligation", + keyword: null, + keyword_basis: null, evidence_class: "wire", schema_refs: [], depends_on: [], @@ -178,3 +180,54 @@ describe("parseVocabulary -- the vocabulary's own shape", () => { expect(() => parseVocabulary("relations:\n - name: a\n source: wire\n columns: [{ name: seq, type: number }, { name: x, type: symbol, domain: seq }]\n")).toThrow("domain seq is number elsewhere, symbol here"); }); }); + +describe("the verdict layer -- RFC 2119 strength as facts, verdicts as rules", () => { + const manifestEntry = (id: string, level: ManifestEntry["level"]): ManifestEntry => ({ ...entry(id), level, keywords: level ? [level] : [] }); + const program = compileProgram( + vocabulary, + [ + { manifest: manifestEntry("ACS-REQ-0007", "MUST"), record: record("ACS-REQ-0007", { predicate: rules(["Seq"], ["Session"], "violation(Seq, Session) :- hook(Seq, Session, _), not handshake(_, Session).") }) }, + { manifest: manifestEntry("ACS-REQ-0012", "SHOULD"), record: record("ACS-REQ-0012", { profile: ["acs-audit"], predicate: rules(["Session"], ["Seq"], 'violation(Session, Seq) :- intent_modification_rejected(Session, Seq), not audit_event(Session, Seq, "intent_modification_rejected").') }) }, + { manifest: manifestEntry("ACS-REQ-0022", "MUST"), record: record("ACS-REQ-0022", { modality_kind: "conditional-on-exercise", predicate: rules(["Session"], ["Field"], "violation(Session, Field) :- archived(Session), archive_required_field(Field), not archive_preserved(Session, Field).") }) }, + { manifest: manifestEntry("ACS-REQ-0021", "MAY"), record: record("ACS-REQ-0021", { modality_kind: "permission" }) }, + { manifest: manifestEntry("ACS-REQ-0003", "MUST"), record: record("ACS-REQ-0003", { predicate: rules(["Seq"], ["Field"], 'violation(Seq, "reasoning") :- decision(Seq, "deny"), not result_field(Seq, "reasoning").') }) }, + ], + { version: null, commit: null }, + ); + + it("states each compiled provision's strength, polarity, profiles and needs as facts, and every Requirement's profiles", () => { + const fact = (name: string) => program.verdicts.catalog.find((r) => r.name === name)?.facts; + expect(fact("strength")).toEqual([["ACS-REQ-0007", "must"], ["ACS-REQ-0012", "should"], ["ACS-REQ-0022", "must"], ["ACS-REQ-0003", "must"]]); + expect(fact("polarity")?.every((t) => t[1] === "obligation")).toBe(true); + expect(fact("provision")).toEqual([["ACS-REQ-0007"], ["ACS-REQ-0012"], ["ACS-REQ-0022"], ["ACS-REQ-0021"], ["ACS-REQ-0003"]]); + expect(fact("requires_profile")).toEqual([["ACS-REQ-0003", "acs-core"], ["ACS-REQ-0007", "acs-core"], ["ACS-REQ-0012", "acs-audit"], ["ACS-REQ-0021", "acs-core"], ["ACS-REQ-0022", "acs-core"]]); + expect(fact("needs")).toEqual([["ACS-REQ-0012", "audit_event"], ["ACS-REQ-0012", "intent_modification_rejected"], ["ACS-REQ-0022", "archive_preserved"], ["ACS-REQ-0022", "archived"]]); + expect(fact("conditional")).toEqual([["ACS-REQ-0022"]]); + }); + + it("attributes a violation to a session through a session column, or a seq column joined to envelope, and reads a conditional provision's exercise off its positive atoms", () => { + const sources = program.verdicts.rules.map((r) => r.source); + // A session column anywhere in the violation is used directly; a violation keyed by seq alone joins envelope. + expect(sources).toContain('violated("ACS-REQ-0007", S) :- acs_req_0007__violation(_, S).'); + expect(sources).toContain('violated("ACS-REQ-0012", S) :- acs_req_0012__violation(S, _).'); + expect(sources).toContain('violated("ACS-REQ-0003", S) :- acs_req_0003__violation(Q, _), envelope(Q, S, _, _, _).'); + expect(sources).toContain('exercised("ACS-REQ-0022", Session) :- archived(Session).'); + expect(program.verdicts.outputs).toEqual(["fail", "deviates", "pass", "unevaluated", "not_activated", "not_exercised"]); + expect(program.verdicts.strata.flat()).toEqual(["violated", "exercised", "active", "unevaluated", "not_activated", "not_exercised", "fail", "deviates", "pass"]); + expect(program.domains.map((d) => d.name)).toContain("provision"); + }); + + it("refuses a provision whose violation names neither a session nor a seq, since no session could be judged by it", () => { + const p = compileProgram(vocabulary, [{ manifest: manifestEntry("ACS-REQ-0014", "MUST"), record: record("ACS-REQ-0014", { predicate: rules(["Pid"], ["Other"], "violation(Pid, Other) :- provenance(_, _, Pid, _), provenance(_, _, Other, _), Pid != Other.") }) }], { version: null, commit: null }); + expect(p.problems.map((x) => x.message)).toEqual(["ACS-REQ-0014: no subject or witness column holds a session or a seq, so a violation cannot be attributed to a session"]); + }); + + it("emits the layer into the published program: catalog facts inline, the verdicts as outputs, the rules last", () => { + const dl = emitSouffleProgram(program); + expect(dl).toContain('.decl strength(provision:Provision, strength:Strength)\nstrength("ACS-REQ-0007", "must").'); + expect(dl).toContain(".decl deviates(provision:Provision, session:Session)\n.output deviates"); + expect(dl).toContain('deviates(P, S) :- violated(P, S), active(P, S), strength(P, "should"), !unevaluated(P).'); + expect(dl).toContain(".type Provision <: symbol"); + }); +}); + diff --git a/ir/test/conformance/fixtures/conformant/README.md b/ir/test/conformance/fixtures/conformant/README.md index d9246e2..5fb20c2 100644 --- a/ir/test/conformance/fixtures/conformant/README.md +++ b/ir/test/conformance/fixtures/conformant/README.md @@ -5,3 +5,7 @@ One session, `session-clean`, that breaches nothing: handshake first, a DENY wit ## Reading the facts files Each `facts/.facts` starts with `#` comment lines that name the relation's columns and its source, copied from `ir/vocabulary/relations.yaml`; the tuples follow, one per line, tab-separated. The evaluator skips comment lines and Soufflé is run on a copy without them. Values are named for what they are: `session-…` for a session id, `entry-N` for a ContextEntry id, `prov-…` for a provenance id (`prov-user-input` came in as `user_input`, `prov-agent` is `agent_generated`), `hash-…` for an `entry_hash`, `head-N` for the chain head published at response `N`, `req-N` for the request id of seq `N`, and `fingerprint-…` for a canonical-form fingerprint. Response lines use seq numbers ten times their request's (request 2 is answered at 20). + +## Verdicts + +`expected-verdicts.tsv` pins what the verdict layer derives over these facts, one line per tuple of `fail`, `deviates`, `pass`, `unevaluated`, `not_activated` and `not_exercised`, and both engines must agree on it. Two facts files describe the run rather than the wire: `negotiated.facts` lists the profiles the session negotiated, which is what activates a provision, and `available.facts` lists every guardian-state, deployment and external relation this fixture supplies. A provision that needs a relation not listed there is `unevaluated`, never passed, so a fixture that adds a `.facts` file for a non-wire relation lists it there too. `envelope.facts` has a row for every seq the other relations mention: that row is how a violation keyed by seq is attributed to its session. Violations are not scoped by profile, so `expected.tsv` holds every breach; the verdicts are, so a breach of an ACS-Crypto provision appears there as `not_activated`. diff --git a/ir/test/conformance/fixtures/conformant/expected-verdicts.tsv b/ir/test/conformance/fixtures/conformant/expected-verdicts.tsv new file mode 100644 index 0000000..c445880 --- /dev/null +++ b/ir/test/conformance/fixtures/conformant/expected-verdicts.tsv @@ -0,0 +1,88 @@ +# The verdict relations both engines must derive over facts/: relation, then its columns (provision, session). +# fail and deviates name the provisions this fixture breaches, by RFC 2119 strength; pass, not_exercised and not_activated +# cover the rest of the compiled catalog; unevaluated lists what needs a relation facts/available.facts does not list. +not_activated ACS-REQ-0032 session-clean +not_activated ACS-REQ-0062 session-clean +not_activated ACS-REQ-0063 session-clean +not_activated ACS-REQ-0083 session-clean +not_activated ACS-REQ-0124 session-clean +not_activated ACS-REQ-0130 session-clean +not_activated ACS-REQ-0131 session-clean +not_activated ACS-REQ-0132 session-clean +not_activated ACS-REQ-0134 session-clean +not_activated ACS-REQ-0135 session-clean +not_activated ACS-REQ-0136 session-clean +not_activated ACS-REQ-0137 session-clean +not_activated ACS-REQ-0138 session-clean +not_activated ACS-REQ-0139 session-clean +not_activated ACS-REQ-0141 session-clean +not_activated ACS-REQ-0143 session-clean +not_activated ACS-REQ-0144 session-clean +not_activated ACS-REQ-0145 session-clean +not_activated ACS-REQ-0146 session-clean +not_activated ACS-REQ-0147 session-clean +not_activated ACS-REQ-0148 session-clean +not_activated ACS-REQ-0149 session-clean +not_activated ACS-REQ-0150 session-clean +not_exercised ACS-REQ-0102 session-clean +pass ACS-REQ-0002 session-clean +pass ACS-REQ-0003 session-clean +pass ACS-REQ-0004 session-clean +pass ACS-REQ-0005 session-clean +pass ACS-REQ-0006 session-clean +pass ACS-REQ-0007 session-clean +pass ACS-REQ-0008 session-clean +pass ACS-REQ-0009 session-clean +pass ACS-REQ-0010 session-clean +pass ACS-REQ-0011 session-clean +pass ACS-REQ-0013 session-clean +pass ACS-REQ-0014 session-clean +pass ACS-REQ-0015 session-clean +pass ACS-REQ-0016 session-clean +pass ACS-REQ-0017 session-clean +pass ACS-REQ-0027 session-clean +pass ACS-REQ-0028 session-clean +pass ACS-REQ-0039 session-clean +pass ACS-REQ-0060 session-clean +pass ACS-REQ-0061 session-clean +pass ACS-REQ-0067 session-clean +pass ACS-REQ-0076 session-clean +pass ACS-REQ-0082 session-clean +pass ACS-REQ-0086 session-clean +pass ACS-REQ-0087 session-clean +pass ACS-REQ-0092 session-clean +pass ACS-REQ-0095 session-clean +pass ACS-REQ-0096 session-clean +pass ACS-REQ-0097 session-clean +pass ACS-REQ-0103 session-clean +pass ACS-REQ-0113 session-clean +pass ACS-REQ-0114 session-clean +pass ACS-REQ-0117 session-clean +pass ACS-REQ-0120 session-clean +pass ACS-REQ-0121 session-clean +pass ACS-REQ-0142 session-clean +unevaluated ACS-REQ-0001 +unevaluated ACS-REQ-0012 +unevaluated ACS-REQ-0018 +unevaluated ACS-REQ-0020 +unevaluated ACS-REQ-0022 +unevaluated ACS-REQ-0023 +unevaluated ACS-REQ-0030 +unevaluated ACS-REQ-0031 +unevaluated ACS-REQ-0041 +unevaluated ACS-REQ-0043 +unevaluated ACS-REQ-0046 +unevaluated ACS-REQ-0050 +unevaluated ACS-REQ-0051 +unevaluated ACS-REQ-0052 +unevaluated ACS-REQ-0053 +unevaluated ACS-REQ-0066 +unevaluated ACS-REQ-0072 +unevaluated ACS-REQ-0077 +unevaluated ACS-REQ-0078 +unevaluated ACS-REQ-0079 +unevaluated ACS-REQ-0081 +unevaluated ACS-REQ-0084 +unevaluated ACS-REQ-0100 +unevaluated ACS-REQ-0111 +unevaluated ACS-REQ-0151 diff --git a/ir/test/conformance/fixtures/conformant/facts/available.facts b/ir/test/conformance/fixtures/conformant/facts/available.facts new file mode 100644 index 0000000..b657fcd --- /dev/null +++ b/ir/test/conformance/fixtures/conformant/facts/available.facts @@ -0,0 +1,15 @@ +# available(relation) source: external +# Every non-wire relation this fixture supplies; a provision needing one not listed here is unevaluated. +context_entry +context_entry_field +context_entry_step +decision_log_field +defer_bound +entry_hash_recomputed +evaluator_ran +guardian_version +intent_established +intent_extension +intent_parsed +session_batching +signature_covers diff --git a/ir/test/conformance/fixtures/conformant/facts/envelope.facts b/ir/test/conformance/fixtures/conformant/facts/envelope.facts new file mode 100644 index 0000000..34790e1 --- /dev/null +++ b/ir/test/conformance/fixtures/conformant/facts/envelope.facts @@ -0,0 +1,11 @@ +# envelope(seq, session, direction, method, rpc_id) source: wire +# One tuple per envelope-log line. `direction` is request or response; `method` is the ACS method +# the Guardian dispatched. Every seq the other relations mention has a row here, which is how a +# violation is attributed to its session by the verdict layer. +1 session-clean request handshake/hello rpc-1 +2 session-clean request agbom/snapshot rpc-2 +3 session-clean request steps/toolCallRequest rpc-3 +4 session-clean request steps/agentResponse rpc-4 +10 session-clean response handshake/hello rpc-1 +20 session-clean response steps/toolCallRequest rpc-3 +30 session-clean response steps/agentResponse rpc-4 diff --git a/ir/test/conformance/fixtures/conformant/facts/negotiated.facts b/ir/test/conformance/fixtures/conformant/facts/negotiated.facts new file mode 100644 index 0000000..c38e7cf --- /dev/null +++ b/ir/test/conformance/fixtures/conformant/facts/negotiated.facts @@ -0,0 +1,4 @@ +# negotiated(session, profile) source: wire +# The profiles each session negotiated; the verdict rules activate a provision through this relation. +session-clean acs-core +session-clean acs-provenance diff --git a/ir/test/conformance/fixtures/violating/README.md b/ir/test/conformance/fixtures/violating/README.md index ac90882..20a6025 100644 --- a/ir/test/conformance/fixtures/violating/README.md +++ b/ir/test/conformance/fixtures/violating/README.md @@ -34,3 +34,7 @@ The breaches, by provision: ## Reading the facts files Each `facts/.facts` starts with `#` comment lines that name the relation's columns and its source, copied from `ir/vocabulary/relations.yaml`; the tuples follow, one per line, tab-separated. The evaluator skips comment lines and Soufflé is run on a copy without them. Values are named for what they are: `session-…` for a session id, `entry-N` for a ContextEntry id, `prov-…` for a provenance id (`prov-user-input` came in as `user_input`, `prov-agent` is `agent_generated`), `hash-…` for an `entry_hash`, `head-N` for the chain head published at response `N`, `req-N` for the request id of seq `N`, and `fingerprint-…` for a canonical-form fingerprint. Response lines use seq numbers ten times their request's (request 2 is answered at 20). + +## Verdicts + +`expected-verdicts.tsv` pins what the verdict layer derives over these facts, one line per tuple of `fail`, `deviates`, `pass`, `unevaluated`, `not_activated` and `not_exercised`, and both engines must agree on it. Two facts files describe the run rather than the wire: `negotiated.facts` lists the profiles the session negotiated, which is what activates a provision, and `available.facts` lists every guardian-state, deployment and external relation this fixture supplies. A provision that needs a relation not listed there is `unevaluated`, never passed, so a fixture that adds a `.facts` file for a non-wire relation lists it there too. `envelope.facts` has a row for every seq the other relations mention: that row is how a violation keyed by seq is attributed to its session. Violations are not scoped by profile, so `expected.tsv` holds every breach; the verdicts are, so a breach of an ACS-Crypto provision appears there as `not_activated`. diff --git a/ir/test/conformance/fixtures/violating/expected-verdicts.tsv b/ir/test/conformance/fixtures/violating/expected-verdicts.tsv new file mode 100644 index 0000000..ed15cce --- /dev/null +++ b/ir/test/conformance/fixtures/violating/expected-verdicts.tsv @@ -0,0 +1,88 @@ +# The verdict relations both engines must derive over facts/: relation, then its columns (provision, session). +# fail and deviates name the provisions this fixture breaches, by RFC 2119 strength; pass, not_exercised and not_activated +# cover the rest of the compiled catalog; unevaluated lists what needs a relation facts/available.facts does not list. +deviates ACS-REQ-0012 session-violating +deviates ACS-REQ-0020 session-violating +deviates ACS-REQ-0027 session-violating +deviates ACS-REQ-0060 session-violating +fail ACS-REQ-0001 session-violating +fail ACS-REQ-0002 session-violating +fail ACS-REQ-0003 session-violating +fail ACS-REQ-0004 session-violating +fail ACS-REQ-0005 session-violating +fail ACS-REQ-0006 session-violating +fail ACS-REQ-0007 session-violating +fail ACS-REQ-0008 session-violating +fail ACS-REQ-0009 session-violating +fail ACS-REQ-0010 session-violating +fail ACS-REQ-0011 session-violating +fail ACS-REQ-0013 session-violating +fail ACS-REQ-0014 session-violating +fail ACS-REQ-0015 session-violating +fail ACS-REQ-0016 session-violating +fail ACS-REQ-0017 session-violating +fail ACS-REQ-0018 session-violating +fail ACS-REQ-0022 session-violating +fail ACS-REQ-0023 session-violating +fail ACS-REQ-0092 session-violating +not_activated ACS-REQ-0032 session-violating +not_activated ACS-REQ-0062 session-violating +not_activated ACS-REQ-0063 session-violating +not_activated ACS-REQ-0083 session-violating +not_activated ACS-REQ-0124 session-violating +not_activated ACS-REQ-0130 session-violating +not_activated ACS-REQ-0131 session-violating +not_activated ACS-REQ-0132 session-violating +not_activated ACS-REQ-0134 session-violating +not_activated ACS-REQ-0135 session-violating +not_activated ACS-REQ-0136 session-violating +not_activated ACS-REQ-0137 session-violating +not_activated ACS-REQ-0138 session-violating +not_activated ACS-REQ-0139 session-violating +not_activated ACS-REQ-0141 session-violating +not_activated ACS-REQ-0143 session-violating +not_activated ACS-REQ-0144 session-violating +not_activated ACS-REQ-0145 session-violating +not_activated ACS-REQ-0146 session-violating +not_activated ACS-REQ-0147 session-violating +not_activated ACS-REQ-0148 session-violating +not_activated ACS-REQ-0149 session-violating +not_activated ACS-REQ-0150 session-violating +not_exercised ACS-REQ-0102 session-violating +pass ACS-REQ-0028 session-violating +pass ACS-REQ-0039 session-violating +pass ACS-REQ-0052 session-violating +pass ACS-REQ-0053 session-violating +pass ACS-REQ-0061 session-violating +pass ACS-REQ-0066 session-violating +pass ACS-REQ-0067 session-violating +pass ACS-REQ-0072 session-violating +pass ACS-REQ-0081 session-violating +pass ACS-REQ-0082 session-violating +pass ACS-REQ-0086 session-violating +pass ACS-REQ-0087 session-violating +pass ACS-REQ-0095 session-violating +pass ACS-REQ-0096 session-violating +pass ACS-REQ-0097 session-violating +pass ACS-REQ-0103 session-violating +pass ACS-REQ-0113 session-violating +pass ACS-REQ-0114 session-violating +pass ACS-REQ-0117 session-violating +pass ACS-REQ-0120 session-violating +pass ACS-REQ-0121 session-violating +pass ACS-REQ-0142 session-violating +unevaluated ACS-REQ-0030 +unevaluated ACS-REQ-0031 +unevaluated ACS-REQ-0041 +unevaluated ACS-REQ-0043 +unevaluated ACS-REQ-0046 +unevaluated ACS-REQ-0050 +unevaluated ACS-REQ-0051 +unevaluated ACS-REQ-0076 +unevaluated ACS-REQ-0077 +unevaluated ACS-REQ-0078 +unevaluated ACS-REQ-0079 +unevaluated ACS-REQ-0084 +unevaluated ACS-REQ-0100 +unevaluated ACS-REQ-0111 +unevaluated ACS-REQ-0151 diff --git a/ir/test/conformance/fixtures/violating/facts/available.facts b/ir/test/conformance/fixtures/violating/facts/available.facts new file mode 100644 index 0000000..200fb00 --- /dev/null +++ b/ir/test/conformance/fixtures/violating/facts/available.facts @@ -0,0 +1,22 @@ +# available(relation) source: external +# Every non-wire relation this fixture supplies; a provision needing one not listed here is unevaluated. +approver_verified +archive_preserved +archived +ask_resolved +audit_event +context_entry +context_entry_field +decision_log_field +defer_bound +entry_hash_recomputed +evaluator_ran +guardian_version +intent_established +intent_extension +intent_modification_rejected +intent_parsed +schema_violation +session_batching +signature_covers +signature_status diff --git a/ir/test/conformance/fixtures/violating/facts/envelope.facts b/ir/test/conformance/fixtures/violating/facts/envelope.facts index 1c09f7c..96f3020 100644 --- a/ir/test/conformance/fixtures/violating/facts/envelope.facts +++ b/ir/test/conformance/fixtures/violating/facts/envelope.facts @@ -1,3 +1,14 @@ # envelope(seq, session, direction, method, rpc_id) source: wire # One tuple per envelope-log line. `direction` is request or response; `method` is the ACS method -# the Guardian dispatched. +# the Guardian dispatched. Every seq the other relations mention has a row here, which is how a +# violation is attributed to its session by the verdict layer. +2 session-violating request steps/toolCallRequest rpc-2 +3 session-violating request handshake/hello rpc-3 +4 session-violating request steps/toolCallRequest rpc-4 +5 session-violating request steps/toolCallResult rpc-5 +6 session-violating request steps/agentResponse rpc-6 +20 session-violating response steps/toolCallRequest rpc-2 +30 session-violating response handshake/hello rpc-3 +40 session-violating response steps/toolCallRequest rpc-4 +50 session-violating response steps/toolCallResult rpc-5 +60 session-violating response steps/agentResponse rpc-6 diff --git a/ir/test/conformance/fixtures/violating/facts/negotiated.facts b/ir/test/conformance/fixtures/violating/facts/negotiated.facts new file mode 100644 index 0000000..cf6bcf5 --- /dev/null +++ b/ir/test/conformance/fixtures/violating/facts/negotiated.facts @@ -0,0 +1,4 @@ +# negotiated(session, profile) source: wire +# The profiles each session negotiated; the verdict rules activate a provision through this relation. +session-violating acs-core +session-violating acs-provenance diff --git a/ir/test/differential.test.ts b/ir/test/differential.test.ts index f0b75c3..2ef817a 100644 --- a/ir/test/differential.test.ts +++ b/ir/test/differential.test.ts @@ -40,6 +40,24 @@ describe("differentialCheck -- the evaluator against the fixtures' expectations" expect([...provisions].sort()).toEqual([...v5, ...v7]); }); + it("derives the verdicts beside the violations, and holds them to expected-verdicts.tsv", () => { + const violating = report.fixtures.find((f) => f.fixture === "violating"); + const rows = violating?.verdicts ?? []; + expect(violating?.verdicts_vs_expected).toEqual({ only_evaluator: [], only_expected: [] }); + expect(rows).toContain("fail\tACS-REQ-0007\tsession-violating"); + // ACS-REQ-0012 is a SHOULD: its breach is a deviation, not a failure. + expect(rows).toContain("deviates\tACS-REQ-0012\tsession-violating"); + expect(rows.filter((r) => r.startsWith("fail\tACS-REQ-0012"))).toEqual([]); + // ACS-REQ-0102 is conditional on an error carrying data, which this fixture never sends. + expect(rows).toContain("not_exercised\tACS-REQ-0102\tsession-violating"); + // ACS-REQ-0084 needs skew_window, which the fixture does not list as available: unevaluated, not passed. + expect(rows).toContain("unevaluated\tACS-REQ-0084"); + expect(rows.filter((r) => /^pass\tACS-REQ-0084/.test(r))).toEqual([]); + const conformant = report.fixtures.find((f) => f.fixture === "conformant"); + expect(conformant?.verdicts.filter((r) => /^(fail|deviates)\t/.test(r))).toEqual([]); + expect(conformant?.verdicts_vs_expected).toEqual({ only_evaluator: [], only_expected: [] }); + }); + it("reports a mismatch between the evaluator and expected.tsv as divergence", () => { const tampered: RuleProgram = JSON.parse(JSON.stringify(program)); const p = tampered.provisions.find((x) => x.id === "ACS-REQ-0007"); diff --git a/ir/test/evaluate.test.ts b/ir/test/evaluate.test.ts index b4b4a81..785015f 100644 --- a/ir/test/evaluate.test.ts +++ b/ir/test/evaluate.test.ts @@ -1,7 +1,8 @@ import { describe, expect, it } from "bun:test"; -import { compileProvision, type RuleProgram } from "../src/compile/compile.ts"; +import { compileProgram, type RuleProgram } from "../src/compile/compile.ts"; import { parseVocabulary } from "../src/compile/vocabulary.ts"; -import { evaluate, unified } from "../src/verify/evaluate.ts"; +import { evaluate, evaluateProgram, unified } from "../src/verify/evaluate.ts"; +import { verdictRows } from "../src/verify/differential.ts"; import type { FactSet } from "../src/verify/facts.ts"; import type { ProvisionRecord } from "../src/catalog/catalog.ts"; import type { ManifestEntry } from "../src/extract/extract.ts"; @@ -20,16 +21,38 @@ relations: - name: blocked source: wire columns: [{ name: node, type: symbol }] + - name: envelope + source: wire + columns: [{ name: seq, type: number }, { name: session, type: symbol }, { name: direction, type: symbol }, { name: method, type: symbol }, { name: rpc_id, type: symbol }] + - name: negotiated + source: wire + columns: [{ name: session, type: symbol }, { name: profile, type: symbol }] + - name: available + source: external + columns: [{ name: relation, type: symbol }] `); +type Spec = { id: string; subject: string[]; witness: string[]; rules: string[]; level?: ManifestEntry["level"]; modality?: ProvisionRecord["modality_kind"] }; + +function programOf(...specs: Spec[]): RuleProgram { + const entries = specs.map((s) => { + const manifest: ManifestEntry = { id: s.id, type: "Requirement", source_file: "x", line: 1, block_type: "paragraph", section_slug: null, level: s.level ?? "MUST", keywords: [], text: "", text_hash: "" }; + const record: ProvisionRecord = { + id: s.id, title: "T", actor: "guardian", reported_against: "guardian", profile: ["acs-core"], activation: null, modality_kind: s.modality ?? "obligation", keyword: null, keyword_basis: null, evidence_class: "wire", + schema_refs: [], depends_on: [], restates: null, status: "active", since: "0.1.0", superseded_by: [], reviewed_against: "", note: null, + predicate: { kind: "rules", subject: s.subject, witness: s.witness, rules: s.rules }, + }; + return { manifest, record }; + }); + const p = compileProgram(vocabulary, entries, { version: null, commit: null }); + // A provision whose subject is a node cannot be attributed to a session; these tests are about the violations, so that is not a failure here. + const attributable = new Set(p.verdicts.catalog.find((r) => r.name === "compiled")?.facts.map((t) => String(t[0]))); + for (const problem of p.problems) if (attributable.has(problem.id) || !/attributed to a session/.test(problem.message)) throw new Error(problem.message); + return p; +} + function program(id: string, subject: string[], witness: string[], ...rules: string[]): RuleProgram { - const manifest: ManifestEntry = { id, type: "Requirement", source_file: "x", line: 1, block_type: "paragraph", section_slug: null, level: "MUST", keywords: [], text: "", text_hash: "" }; - const record: ProvisionRecord = { - id, title: "T", actor: "guardian", reported_against: "guardian", profile: ["acs-core"], activation: null, modality_kind: "obligation", evidence_class: "wire", - schema_refs: [], depends_on: [], restates: null, status: "active", since: "0.1.0", superseded_by: [], reviewed_against: "", note: null, - predicate: { kind: "rules", subject, witness, rules }, - }; - return { generated_by: "t", corpus: { version: null, commit: null }, relations: [...vocabulary.relations.values()], domains: [...vocabulary.domains.entries()].map(([name, type]) => ({ name, type })), provisions: [compileProvision(vocabulary, manifest, record, new Set([id]))], problems: [] }; + return programOf({ id, subject, witness, rules }); } const facts = (init: Record): FactSet => new Map(Object.entries(init)); @@ -70,3 +93,45 @@ describe("evaluate -- the in-process engine's constructs", () => { expect(evaluate(p, facts({}))).toEqual([]); }); }); + +describe("evaluateProgram -- the verdict layer over the provisions' violations", () => { + const p = programOf( + { id: "ACS-REQ-0001", subject: ["S"], witness: ["N"], rules: ["violation(S, N) :- item(N, S), not blocked(N)."] }, + { id: "ACS-REQ-0002", subject: ["S"], witness: ["N"], rules: ["violation(S, N) :- item(N, S), not blocked(N)."], level: "SHOULD" }, + { id: "ACS-REQ-0003", subject: ["S"], witness: ["N"], rules: ["violation(S, N) :- item(N, S), bound(N, 0)."] }, + { id: "ACS-REQ-0004", subject: ["S"], witness: ["N"], rules: ["violation(S, N) :- item(N, S), blocked(N), bound(N, 0)."], modality: "conditional-on-exercise" }, + ); + const base = { + envelope: [[1, "s1", "request", "m", "r"], [2, "s2", "request", "m", "r"]], + item: [["a", 1], ["b", 2]], + blocked: [["b"]], + bound: [["a", 3]], + negotiated: [["s1", "acs-core"], ["s2", "acs-trace"]], + available: [["bound"]], + }; + + it("a MUST breached fails, a SHOULD breached deviates, a session that did not negotiate the profile is not activated", () => { + const rows = verdictRows(evaluateProgram(p, facts(base)).verdicts); + expect(rows.filter((r) => r.startsWith("fail"))).toEqual(["fail\tACS-REQ-0001\ts1"]); + expect(rows.filter((r) => r.startsWith("deviates"))).toEqual(["deviates\tACS-REQ-0002\ts1"]); + expect(rows.filter((r) => r.startsWith("not_activated"))).toEqual(["not_activated\tACS-REQ-0001\ts2", "not_activated\tACS-REQ-0002\ts2", "not_activated\tACS-REQ-0003\ts2", "not_activated\tACS-REQ-0004\ts2"]); + // ACS-REQ-0003 reads bound (a deployment relation), which was supplied, and derives nothing for s1's item, whose bound is 3: it passes there. + expect(rows.filter((r) => r.startsWith("pass"))).toEqual(["pass\tACS-REQ-0003\ts1"]); + // ACS-REQ-0004 is conditional; its condition (a blocked item with a bound of 0) never arose in s1. + expect(rows.filter((r) => r.startsWith("not_exercised"))).toEqual(["not_exercised\tACS-REQ-0004\ts1"]); + expect(rows.filter((r) => r.startsWith("unevaluated"))).toEqual([]); + }); + + it("a relation not listed as available makes the provisions that need it unevaluated, never passed", () => { + const rows = verdictRows(evaluateProgram(p, facts({ ...base, available: [] })).verdicts); + expect(rows.filter((r) => r.startsWith("unevaluated"))).toEqual(["unevaluated\tACS-REQ-0003", "unevaluated\tACS-REQ-0004"]); + expect(rows.filter((r) => /^(pass|not_exercised)\t/.test(r))).toEqual([]); + expect(rows.filter((r) => r.startsWith("fail"))).toEqual(["fail\tACS-REQ-0001\ts1"]); + }); + + it("a conditional provision whose condition arose is judged like any other, and stays not exercised where it did not", () => { + const rows = verdictRows(evaluateProgram(p, facts({ ...base, bound: [["a", 3], ["b", 0]], negotiated: [["s1", "acs-core"], ["s2", "acs-core"]] })).verdicts); + expect(rows.filter((r) => r.includes("ACS-REQ-0004"))).toEqual(["fail\tACS-REQ-0004\ts2", "not_exercised\tACS-REQ-0004\ts1"]); + }); +}); + diff --git a/ir/test/provision-index.test.ts b/ir/test/provision-index.test.ts index 0808bfb..60a82fe 100644 --- a/ir/test/provision-index.test.ts +++ b/ir/test/provision-index.test.ts @@ -10,7 +10,7 @@ describe("renderProvisionIndex -- P2 from the real catalog", () => { const index = renderProvisionIndex(catalog, manifest.corpus, new Map([["ACS-REQ-0007", ["fixtures/violating/expected.tsv"]]])); it("renders the index (U12), a detail per provision (U13), and the coverage table (U14)", () => { - expect(index).toContain("| [ACS-REQ-0007](#acs-req-0007) | Requirement | — | observed-agent | acs-core | wire | obligation | active | spec/instrument/specification.md:65 | Handshake precedes any hook traffic |"); + expect(index).toContain("| [ACS-REQ-0007](#acs-req-0007) | Requirement | MUST | observed-agent | acs-core | wire | obligation | active | spec/instrument/specification.md:65 | Handshake precedes any hook traffic |"); expect(index).toContain("### ACS-REQ-0007\n\n**Handshake precedes any hook traffic.** Requirement. `spec/instrument/specification.md:65` (paragraph, §`4-capability-negotiation-handshake`). Anchor: `#acs-req-0007`.\n\n> Required at session start, before any hook traffic."); expect(index).toContain("- Restates: [ACS-REQ-0023](#acs-req-0023)"); expect(index).toContain("| ACS-EXC-0001 | none |"); diff --git a/ir/test/staleness.test.ts b/ir/test/staleness.test.ts index 586517f..b8f2bc5 100644 --- a/ir/test/staleness.test.ts +++ b/ir/test/staleness.test.ts @@ -24,6 +24,8 @@ const record = (id: string, reviewed_against: string, extra: Partial [...t])); for (const [r, tuples] of external.facts) facts.set(r, [...(facts.get(r) ?? []), ...tuples]); const negotiated = options.negotiated ?? [...new Set(normalized.sessions.flatMap((s) => s.profiles))]; - const verdicts = judge(program, catalog, evaluate(program, facts), facts, negotiated, external.available, new Set()); + // An override of the negotiated profiles is an override of the `negotiated` facts the verdict rules read. + if (options.negotiated) facts.set("negotiated", normalized.sessions.flatMap((s) => (options.negotiated as string[]).map((p) => [s.session, p]))); + const verdicts = judge(program, catalog, evaluateProgram(program, facts), facts, new Set()); return { dir, trace, normalized, external, facts, verdicts, negotiated }; } @@ -116,6 +118,16 @@ describe("acs-ir verify -- the violating trace", () => { ]); }); + it("judges per session, and the report's verdict is the fold: this trace has one session, so it is that session's", () => { + const early = r.verdicts.find((v) => v.id === "ACS-REQ-0007"); + expect(early?.sessions).toEqual([{ session: SESSION, verdict: "fail" }]); + expect(early?.keyword).toBe("MUST"); + const archival = r.verdicts.find((v) => v.id === "ACS-REQ-0102"); + expect(archival?.sessions).toEqual([{ session: SESSION, verdict: "not-exercised" }]); + // No SHOULD is breached in this trace, so nothing deviates; the verdict exists for the trace that does. + expect(byVerdict(r.verdicts, "deviates")).toEqual([]); + }); + it("attaches evidence that names the subject, the witness, and the facts (R3.4)", () => { const trust = r.verdicts.find((v) => v.id === "ACS-REQ-0010"); expect(trust?.evidence).toHaveLength(1); @@ -134,7 +146,11 @@ describe("acs-ir verify -- the violating trace", () => { expect(report).toContain(h); } expect(report).toContain("fail 9, pass 54,"); - expect(report).toContain("| acs-core | 58 | 50 | 8 | 0 |"); + expect(report).toContain("| profile | active obligations | met | unmet | deviating | unevaluated |"); + expect(report).toContain("| acs-core | 58 | 50 | 8 | 0 | 0 |"); + // The verdict table shows the keyword each provision is judged by, the record's override included (ACS-REQ-0003's span starts with a RECOMMENDED). + expect(report).toContain("| ACS-REQ-0003 Required fields per disposition | fail | MUST | guardian | acs-core |"); + expect(report).toContain("| ACS-REQ-0113 A Guardian does not deny postCompact | pass | MUST NOT |"); expect(report).toContain("- ACS-EXC-0001 Multi-tenant isolation is unspecified in v0.1: ACS deliberately requires nothing here"); }); }); diff --git a/ir/vocabulary/relations.yaml b/ir/vocabulary/relations.yaml index b29c973..b047ed6 100644 --- a/ir/vocabulary/relations.yaml +++ b/ir/vocabulary/relations.yaml @@ -14,6 +14,12 @@ # static fixed by the spec; the tuples are listed here and shipped # inside the compiled program # +# The verdict layer's relations (a provision's RFC 2119 strength, the +# profiles that activate it, the relations it needs, and the verdicts the +# rules derive from them) are not declared here: the compiler generates +# them from the catalog. Two relations here feed that layer: `negotiated` +# and `available`. +# # Types are `symbol` (a string) and `number` (an integer), Soufflé's two # scalar kinds the evaluator also distinguishes. Every column also has a # domain, which names what it holds: `seq`, `session`, `pid`, `field`. The @@ -54,6 +60,10 @@ relations: source: wire columns: [{ name: seq, type: number }, { name: session, type: symbol }] doc: "A `handshake/hello` request." + - name: negotiated + source: wire + columns: [{ name: session, type: symbol }, { name: profile, type: symbol }] + doc: "A profile the session negotiated: the ServerHello's `profiles_accepted`, else the ClientHello's `profiles_supported`, else `acs-core`. The verdict rules activate a provision in a session through this relation." - name: hook source: wire columns: [{ name: seq, type: number }, { name: session, type: symbol }, { name: method, type: symbol }] @@ -109,6 +119,10 @@ relations: source: external columns: [{ name: seq, type: number }, { name: schema, type: symbol }, { name: path, type: symbol, domain: json_path }] doc: "An envelope that failed validation against a pinned schema, with the JSON path of the failure." + - name: available + source: external + columns: [{ name: relation, type: symbol }] + doc: "A relation whose tuples the verifier was given: every guardian-state, deployment and external relation it received a file or computed facts for. An empty relation and an absent one differ: a provision that needs a relation not listed here is unevaluated, never passed." # --- the Guardian's own records --- - name: evaluator_ran source: guardian-state From d40cf40b531b36e33e4f9c4d959cacd0fea3c4ae Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 14 Sep 2026 18:28:12 +0000 Subject: [PATCH 2/2] Point the keyword revision notes at PR #49 Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01BX56nQPAsqYihopWfWy1xm --- docs/shaping/normative-ir-slices.md | 4 ++-- ir/README.md | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/shaping/normative-ir-slices.md b/docs/shaping/normative-ir-slices.md index 02838fe..1d16531 100644 --- a/docs/shaping/normative-ir-slices.md +++ b/docs/shaping/normative-ir-slices.md @@ -233,7 +233,7 @@ That is R2.6 demonstrated in one command: **a definition or invariant change inv **Demo:** `acs-ir verify .acs/envelopes.jsonl` emits a W3C-style conformance report. Per-provision verdicts with the facts that witness each violation. Scoped to the profiles the session actually negotiated, so a `["acs-core"]` session is never judged against ACS-Provenance obligations. An unexercised `MAY` produces no verdict. The non-testable roster and the exclusion roster are printed, not omitted. -🟡 **Revised after V8** ([#48](https://github.com/afogel/ACS_reference_implementation/pull/48), stacked on [#47](https://github.com/afogel/ACS_reference_implementation/pull/47)). The judgement moved from TypeScript into the rule program. Each compiled provision's RFC 2119 keyword is a fact (`strength`, `polarity`), so are the profiles that activate it (`requires_profile`), the non-wire relations it reads (`needs`) and whether it is conditional on a permission; the run supplies `negotiated(session, profile)` and `available(relation)`; nine rules derive `fail`, `deviates`, `pass`, `unevaluated`, `not_activated` and `not_exercised` per session, and the published `.dl` outputs them. A breached SHOULD is a `deviates`, which the report counts apart from `fail`: 13 of the 69 compiled rules are SHOULDs and were reported as failures before. The keyword comes from the marked span's first RFC 2119 word; a record states its own, with a `keyword_basis`, where the span has none (nine table cells and list items) or a misleading one (`MAY NOT`, and two tables whose first keyword is a RECOMMENDED beside the MUST the rule checks). The join refuses a permission judged by anything but MAY and an obligation judged by MAY. Verdicts are per session, folded for the report; a conditional provision is exercised when the positive atoms of its rule matched in the session, which also fixes ACS-REQ-0102, whose exercise the old code read off Guardian-state relations it does not use. The differential oracle compares the verdict relations too (findings row 9). +🟡 **Revised after V8** ([#49](https://github.com/afogel/ACS_reference_implementation/pull/49), stacked on [#47](https://github.com/afogel/ACS_reference_implementation/pull/47)). The judgement moved from TypeScript into the rule program. Each compiled provision's RFC 2119 keyword is a fact (`strength`, `polarity`), so are the profiles that activate it (`requires_profile`), the non-wire relations it reads (`needs`) and whether it is conditional on a permission; the run supplies `negotiated(session, profile)` and `available(relation)`; nine rules derive `fail`, `deviates`, `pass`, `unevaluated`, `not_activated` and `not_exercised` per session, and the published `.dl` outputs them. A breached SHOULD is a `deviates`, which the report counts apart from `fail`: 13 of the 69 compiled rules are SHOULDs and were reported as failures before. The keyword comes from the marked span's first RFC 2119 word; a record states its own, with a `keyword_basis`, where the span has none (nine table cells and list items) or a misleading one (`MAY NOT`, and two tables whose first keyword is a RECOMMENDED beside the MUST the rule checks). The join refuses a permission judged by anything but MAY and an obligation judged by MAY. Verdicts are per session, folded for the report; a conditional provision is exercised when the positive atoms of its rule matched in the session, which also fixes ACS-REQ-0102, whose exercise the old code read off Guardian-state relations it does not use. The differential oracle compares the verdict relations too (findings row 9). | # | Place | Component | Affordance | Control | Wires Out | Returns To | |---|-------|-----------|------------|---------|-----------|------------| @@ -604,4 +604,4 @@ Not slice work, but discovered by it and worth reporting to the ACS maintainers | 6 | 🟡 `hooks.md` uses `MAY NOT`, which is not an RFC 2119 term (RFC 2119 defines MAY, and the prohibition is MUST NOT). Read as the prohibition the sentence means | V7, ACS-REQ-0113 | | 7 | 🟡 §10 does not say whether the handshake request is signed; the per-session key is derived from the `session_id` the handshake establishes, so signing it is circular unless a pre-session key exists. The catalog exempts it | V7, ACS-REQ-0081 | | 8 | 🟡 `hooks.md` says a postCompact summary's `derived_from` MUST equal the union of `provenance_id`s of every entry in `entries_compacted`, but `entries_compacted` lists `step_id`s and no wire message ties a `step_id` to a `provenance_id`. A verifier can check the union only from the Guardian's records; the payload could carry the ids it means | V8 follow-up, ACS-REQ-0111 | -| 9 | 🟡 `hooks.md:212` says a Guardian "MAY NOT return DENY" on postCompact. RFC 2119 defines no MAY NOT; the catalog reads it as MUST NOT, which is what the sentence means. Nine other provisions (the §3 response-shape and DEFER-reason cells, `previous_hash`, the deterministic-layer ordering, the version-mismatch outcome, the provenance uniqueness and lineage cells, the AgBOM serialization item) state an obligation with no RFC 2119 word at all; each record now says which keyword it is judged by and why | #48, ACS-REQ-0113 | +| 9 | 🟡 `hooks.md:212` says a Guardian "MAY NOT return DENY" on postCompact. RFC 2119 defines no MAY NOT; the catalog reads it as MUST NOT, which is what the sentence means. Nine other provisions (the §3 response-shape and DEFER-reason cells, `previous_hash`, the deterministic-layer ordering, the version-mismatch outcome, the provenance uniqueness and lineage cells, the AgBOM serialization item) state an obligation with no RFC 2119 word at all; each record now says which keyword it is judged by and why | #49, ACS-REQ-0113 | diff --git a/ir/README.md b/ir/README.md index 9bfe628..688a2d7 100644 --- a/ir/README.md +++ b/ir/README.md @@ -86,4 +86,4 @@ When the spec changes under a provision, `lint` lists it and everything downstre | V6 | shipped | The conformance report over an envelope log: verdicts with evidence, scoped to negotiated profiles, rosters printed. | | V7 | shipped | The full conversion: 155 provisions, 34 authored exclusions, zero unbound occurrences; the inexpressible set enumerated. | | V8 | shipped (tooling and drafts) | `markers patch` writes the bulk and proof-of-concept patches; the Discussion and both PR texts are drafted under `slices/v8/`. Posting them upstream is the maintainer's step. | -| Keywords ([#48](https://github.com/afogel/ACS_reference_implementation/pull/48)) | shipped | RFC 2119 strength as facts and the verdicts as rules in both engines: a breached SHOULD is a deviation, not a failure; profile scoping, exercise and evaluability are Datalog; the published program outputs verdicts. | +| Keywords ([#49](https://github.com/afogel/ACS_reference_implementation/pull/49)) | shipped | RFC 2119 strength as facts and the verdicts as rules in both engines: a breached SHOULD is a deviation, not a failure; profile scoping, exercise and evaluability are Datalog; the published program outputs verdicts. |