Represent RFC 2119 strength as facts and derive verdicts in Datalog

[afogel]

Stacked on #47. The RFC 2119 keyword a provision binds is now data the rule program reads, and the verdict a provision gets is derived by rules in both engines rather than decided in TypeScript.

What changed

• Strength and polarity as facts. Each compiled provision's keyword becomes strength(P, must|should|may) and polarity(P, obligation|prohibition), beside requires_profile, needs (the non-wire relations it reads), conditional, compiled and provision. The run supplies two new vocabulary relations: negotiated(session, profile) from the ServerHello, and available(relation), every guardian-state, deployment and external relation the verifier was given. An empty relation and an absent one differ, and only the latter makes a provision unevaluated.
• Verdicts as rules. Nine rules derive fail, deviates, pass, unevaluated, not_activated and not_exercised per session. Each compiled provision gets a projection rule attributing its violations to a session through a session column, or a seq column joined to envelope; a provision with neither does not compile. A conditional provision is exercised when the positive atoms of its rule matched in the session. The published .dl outputs the six verdict relations, and the differential oracle compares them between engines and against a new expected-verdicts.tsv per fixture. TypeScript only folds the per-session verdicts into the one the report shows.
• A breached SHOULD is a deviation. 13 of the 69 compiled rules are SHOULDs, and a breach of one rendered as fail before. The report now has a deviates verdict, a deviating column in the per-profile table, and shows the keyword each provision is judged by.
• The keyword on the record. The keyword comes from the marked span's first RFC 2119 word (the manifest's level). A record states its own, with a required keyword_basis, where the span has none or a misleading one. Eleven records do: nine table cells and list items with no keyword (schema constraints, lowercase "required", "always"), hooks.md's "MAY NOT return DENY", which RFC 2119 does not define, and two tables whose first keyword is a RECOMMENDED beside the MUST the rule checks. The join refuses a permission judged by anything but MAY, an obligation judged by MAY, and a Requirement with no keyword at all.
• Profile scoping for every Requirement. not_activated is derived over every Requirement, compiled or not, so the report's precedence is unchanged: a permission in a profile the session never negotiated is still reported as not activated.

What building it found

• ACS-REQ-0102 could never fail. The old exercise check read the Guardian-state relations a conditional provision uses and treated an empty list as "never exercised"; ACS-REQ-0102 reads wire relations only. The Datalog form reads exercise off the rule's own positive atoms.
• The conformance fixtures' envelope.facts were empty. Attribution by seq needs a row per seq, so both fixtures now list every seq the other relations mention.
• Findings row 9 in the slices doc: the MAY NOT and the nine keyword-free obligations, for upstream.

Checks

• tsc, bun test ir (189 pass), every --check (census, markers apply, extract, render, compile, both marker patches), lint: all clean.
• Differential with Soufflé 2.5 locally: violations conformant 0/0/0 and violating 33/33/33; verdict relations 85 tuples on each fixture, identical on both engines and equal to expected-verdicts.tsv.

Not in this PR: "never" and "always" as census candidates for unmarked normative statements. The normative sources carry 15 such lines; each would need a binding or an exclusion, which is census work of its own.

🤖 Generated with Claude Code

https://claude.ai/code/session_01BX56nQPAsqYihopWfWy1xm

---

Generated by Claude Code

[github-actions]

Normative impact (ACS 0.1.2 at 6fce2a0)

Nothing added, changed, removed, or unmarked.