diff --git a/docs/shaping/normative-ir-slices.md b/docs/shaping/normative-ir-slices.md index ccbd896..1d16531 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** ([#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 | |---|-------|-----------|------------|---------|-----------|------------| | 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 | #49, ACS-REQ-0113 | diff --git a/ir/README.md b/ir/README.md index 0f6bd77..688a2d7 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 ([#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. | 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