check

check-decl ::= attribute* 'pub'? 'check' Ident '(' param-list ')' ':-' atom-list '=>' diagnostic-expr ';'

pub check no_overlapping_leases(t: Person, p: Property) :-
    count { from l: Lease where l.tenant == t, l.property == p, is_active(l) } > 1
    => Diagnostic {
        severity: Severity::Error,
        code:     "Lease::E001",
        message:  format!("Tenant {} has overlapping active leases on {}", t.name, p.address),
    };

A check is a denial rule over the well-founded model: the body is the violation pattern, the => Diagnostic payload is the per-violation report. Checks never contribute facts (Cat3 — observers, not derivers). check is the only producer for the diagnostic stream from user code.

Discharge — the body’s vocabulary decides, not the author

You never declare a check “compile-time” or “runtime.” Discharge is staged by what the body reads (RFD 0025), the same staging discipline as refinement predicates (Refinement) and modal static discharge (Modal operators):

Catalog-level checks are the user-extensible compiler-diagnostic mechanism: a theory package ships its modeling constraints (OntoClean-style rigidity lints, MLT well-formedness, trait conformance) as check rules and they surface at ox check, ox build, and live in the editor — the LSP runs the same discharge — like any compiler diagnostic, under the package’s own codes.

The #[static] convention. Compile-time-intent checks carry #[static] by convention. The attribute does not change where discharge happens (the vocabulary does); it asserts the intent — if the body later drifts to instance vocabulary, the build fails with OE1322 instead of silently reclassifying the check to runtime discharge.

A firing Severity::Error check at build is a build failure: ox build writes no artifact, same discipline as every other loud gate. Warning/Info render and pass.

Runtime semantics — guard on the delta

At each mutation boundary the runtime evaluates the instance-level checks on the committed state (pre) and on the transaction’s overlay (post = committed + the body’s buffered events, mutate):

• Severity::Error guards: if the mutation creates violations — violations(post) ∖ violations(pre) is non-empty — the whole body is rejected atomically (nothing flushes, mutate’s atomicity) and the rendered diagnostics return to the caller. This generalizes the built-in write gates (OE0668 refinement invariants, OE0211 defined-concept inserts) to user-authored constraints.
• Pre-existing violations never block. A violation that predates the mutation (a stricter artifact over old data) is reported through the observe channel but does not reject writes — the guard is over the delta, not the absolute state.
• Warning/Info observe: collected and surfaced — on mutation results, in dispatch responses (the diagnostics section), and on demand. #[observe] on an Error check opts out of guarding (report-only, legitimate during migration).

The mechanized contract is spec/lean/Argon/Reasoning/Checks.lean: static_discharge_sound (a catalog-closed body evaluates identically at build and against any store extending the catalog) and guard_iff (the guard passes iff violations(post) ⊆ violations(pre)).

The Diagnostic payload

Diagnostic and Severity are check-surface syntax interpreted by the compiler (like the #[default] defeat-plane directive) — no import declares them. Exactly three fields, validated at ox check (OE1323); code: and message: are always required, and severity: is required unless the check implements a trait member whose signature pins it (check Member(Self) => Severity::…; — Trait atom, RFD 0026 amendment, issue #230), in which case omitting severity: inherits the pinned one (a divergent restatement is OE0676):

• severity: — Severity::Error | Severity::Warning | Severity::Info (closed set).
• code: — a string literal, namespaced: ::-qualified ("Lease::E001", "OntoClean::C1"), with the compiler’s OE/OW prefixes reserved (OE1324).
• message: — a string literal, or format!("…{}…", args) with positional {} placeholders only; each argument is evaluated per violation tuple and must resolve against the body’s bindings (OE1325). {{/}} escape literal braces.

at: is reserved for span attribution and refused.

Three-valued honesty

Check bodies evaluate over the well-founded model in K3 and fire on definite (is) violations only — undefined does not fire. Precisely: a violation requires the body to be well-founded true, so a negated body atom not p(x) contributes only when p(x) is well-founded false (definitely absent), not merely not-true — an undefined p(x) arising from recursion-through-negation does not satisfy the negation. A body that would have fired only because a NAF subject was undefined is surfaced on the observe channel marked [undefined], never as a violation and never to the delta guard, regardless of the check’s declared severity. Negation in a check body is negation-as-failure over the well-founded model (the CWA default, World assumptions (CWA / OWA)): not statute(c.cite) means “no derivably known statute,” not a claim about reality. Surfacing can-grade (possible) violations is out of scope.

Delivery contract: a fired check is semantically an emission to the reserved typed sink Diagnostics: Diagnostic (Sinks). Delivery is direct — the build diagnostic stream for static discharge, mutation results and the dispatch-response diagnostics section for runtime discharge.