RFD 0025 — check discharge: vocabulary-staged compile-time and runtime constraint checking

• State: accepted — implementation in flight
• Opened: 2026-06-10
• Decides: the complete semantics of the check rule mode — when and where a check discharges, what the => Diagnostic { … } payload is, what severity means at runtime, and how violations surface. Settles the question Gustavo Guizzardi and Tiago raised (“is a check compile-time or runtime?”) and Ivan’s original conception (checks as user-authored compiler diagnostics) into one model. Design discussion: .local/research/checks/DESIGN-2026-06-10.md.

Prior state (verified at 8deb583): checks parse and lower to RuleMode::Check Cat3 rules, the => Diagnostic expression is discarded at lowering, the payload shape is unvalidated, and no discharge path exists — RuleMode::Check has zero evaluation consumers. The body is evaluable (ox derive <oxbin> <CheckName> returns the violation set), so this RFD is the harness, payload, and contract around an engine that already computes the hard part.

D1 — One construct; the body’s vocabulary determines the discharge site

A check is a denial rule over the well-founded model: the body is the violation pattern, the payload is the per-violation report. The author never chooses a mode; discharge is staged by what the body reads — the third instance of an established pattern (refinement where staging D1Pred/D2Pred; modal static discharge):

The classification rule is crisp and checkable: a check is catalog-level iff every variable in head and body is reflective-sorted (TypeRef, TraitRef, or Metatype). Mixed bodies are instance-level. (Amended by RFD 0026 D6, which introduces TraitRef; the original rule read “TypeRef-sorted”.)

#[static] (convention, Ivan 2026-06-10): compile-time-intent checks carry #[static] by convention. Discharge is still computed from the vocabulary; the attribute (a) makes intent legible at the declaration and (b) turns accidental instance-vocabulary drift into a hard error (new OE: static check reads instance vocabulary) instead of a silent reclassification to runtime. There is no #[runtime] twin — a catalog-level check evaluated at build is simply done.

D2 — Runtime Error semantics: guard on the delta

An Error-severity instance check rejects any mutation that creates new violations: violations(post) ∖ violations(pre) ≠ ∅ ⇒ abort, atomically (RFD 0015 whole-body atomicity — nothing flushes), with the rendered diagnostics returned to the caller. Precedent: OE0668 (where-invariant) and OE0211 already reject writes this way; user checks generalize that gate.

• Delta, not absolute state. Pre-existing violations (e.g. a new artifact’s stricter rules over old data) are reported through the observe channel but never block writes — absolute semantics would brick every subsequent mutation on a store with one legacy violation.
• Post-state realization: committed state + the transaction’s buffered events, read through an overlay view — the runtime realization of exactly the overlay semantics Runtime/MutationSemantics.lean already models for mutate bodies. No speculative store clone, no compensating events; the guard runs before flush.
• v1 computes violations(pre)/violations(post) by evaluating the check predicates on both views and set-differencing; incremental maintenance of violation relations is explicitly the RFD 0018 persisted-IVM follow-on (the delta is what semi-naive computes natively).

D3 — Severity drives blocking

Error guards (D2); Warning/Info observe only. #[observe] on an Error check opts out of guarding (report-only errors are legitimate during migration). Severities are the closed set Severity::{Error, Warning, Info}.

D4 — K3: fire on is only

Check bodies evaluate over the WFM in K3. A violation fires iff definitely derived (is); undefined (can) does not fire. Surfacing can-grade violations (e.g. at Info) is deferred. Documentation must state the OWA reading plainly: not statute(c.cite) is NAF — “no derivably known statute” — not a claim about reality.

D5 — The Diagnostic { … } payload is check-surface syntax, not a user value

Diagnostic, Severity, and the field set are interpreted by the compiler (like #[strict] strengths) — no user-space Diagnostic type exists or is needed. Validated at ox check:

• severity: — exactly Severity::Error | Severity::Warning | Severity::Info (nominal).
• code: — string literal, namespaced: must contain :: (e.g. "Lease::E001"), and the OE/OW prefixes are reserved for the compiler (extends #150’s hygiene rule to user space).
• message: — string literal, or format!("…{}…", args) with positional {} only; each argument must resolve against the body’s bindings (variables / field chains), checked like any body term. Named/spec’d interpolations ({name}, {:?}) are refused loudly.
• Unknown fields are errors; at: is reserved (refused with a “reserved for span attribution” note) until the LSP consumes it.
• All three fields are required. (Amended by RFD 0026’s 2026-06-11 amendment (check members may pin their severity), issue #230: when the check implements a trait member whose signature pins a severity — check Member(Self) => Severity::…; — severity: may be omitted and inherits the pin; a divergent restatement is OE0676. code: and message: stay unconditionally required.)

format! becomes a real (dedicated) expression form in the parser — the §13 macro system is not implied; format! is recognized structurally, the way count { … } is.

D6 — Delivery: the diagnostic stream now, the Diagnostics sink contract forward

Semantically a fired check is an emission to a reserved typed sink Diagnostics: Diagnostic (§7.7.1) — that contract is recorded here so the sink machinery subsumes delivery when it lands, and checks become its first real producer. Until then, delivery is direct:

• Static discharge → the build/LSP diagnostic stream: violations render exactly like compiler diagnostics, under the check’s own user code, at ox check and ox build (build does not fail on user Error checks over declared EDB? — it does: a firing Severity::Error check at build is a build failure, same as any other error diagnostic; Warning renders and passes).
• Runtime discharge → mutation results carry rejected-guard diagnostics; dispatch responses (oxc-serve) gain a diagnostics section for observe-channel violations (amended 2026-06-11: the shipped wire key is diagnostics, not the originally drafted $diagnostics — the $ sigil is the reserved internal-relation namespace, the wrong register for a JSON response key); ox query renders them; the violation set is queryable on demand.

D7 — Wire and drift

RuleDeclBody gains additive fields: the lowered diagnostic template (severity, code, message parts as literal/argument segments) and the #[static]/#[observe] markers. Lean @[language_interface] carriers align; the drift gate covers the new shapes. Existing .oxbin artifacts predate any consumer of these fields; no migration concern.

Non-decisions (tracked, out of scope here)

• Artifact-upgrade pre-existing-violation reporting moment (load-time observe pass) — open.
• can-grade violation surfacing (D4 deferral).
• Per-standpoint checks; check members in traits (companion trait design — their discharge follows this RFD unchanged once monomorphized).
• Incremental violation maintenance (RFD 0018 phase 2).
• ox check --runtime <store> verb cosmetics; ox derive <CheckName> stays the debug surface.