Check constraints: diagnostics on two moments

Area: Constraints & checks Teaches: check rules — constraint/integrity rules that emit a Diagnostic instead of populating an IDB. Where a check discharges is decided by its vocabulary: a catalog-level (TypeRef-sorted) check fires at build, an instance-level check is a runtime delta guard, and one whose EDB is partly declared in source fires at both moments. Prerequisites: concepts and <: specialization; refinement (iff/where) helps. Run: ox build examples/check_constraints && ox run-scenario examples/check_constraints

A check is not a derive. It has no head extent; it computes a condition and, when the condition holds, raises a coded Diagnostic. Argon is a constraint language, and a check is the unit of constraint. The decisive idea here is that the sort of a check’s variables tells the compiler when it can be discharged.

What to read in fleet.ar

A catalog-level check discharges at build. Every variable is TypeRef-sorted, so the condition is decidable over the declared types alone — no instances needed. #[static] makes that a contract: if the body ever drifts to instance vocabulary, the build fails with OE1322 rather than silently reclassifying to a runtime guard.

#[static]
pub check NoDeprecatedVehicles(t: TypeRef) :-
    specializes(t, Deprecated),
    t != Deprecated
    => Diagnostic {
        severity: Severity::Warning,
        code:     "Fleet::W001",
        message:  "type still specializes Deprecated — migrate it before v2",
    };

An instance-level Error check is a runtime delta guard. At runtime a mutation that creates a new violation is rejected atomically; mutations that don’t make things worse pass, and pre-existing violations never block:

pub check OverweightTruck(v: Truck) :-
    v.weight > 100
    => Diagnostic { severity: Severity::Error, code: "Fleet::E001", /* … */ };

A check whose EDB is partly declared in source fires at both moments. Truck(ghost) is a declared fact, so UnweighedTruck fires once at build over the declared facts, and again at runtime on the observe channel for any truck registered without a weighing:

pub check UnweighedTruck(v: Truck) :- v: Truck, not Weighed(v) => Diagnostic { /* W002 */ };
pub fact Truck(ghost);

Running it

ox build discharges the build-moment checks and prints two warnings, then writes the artifact (warnings pass — a firing Error check would refuse the build):

Fleet::W001  type still specializes Deprecated — migrate it before v2   [OldTruck]
Fleet::W002  truck has never been weighed   [#i3356…]
wrote examples/check_constraints/target/root.oxbin

(W002’s subject is the declared ghost truck, rendered as its opaque individual id.)

ox run-scenario registers hauler at weight 50. The OverweightTruck Error guard passes (no new violation), and the observe channel still reports the pre-existing Fleet::W002 on the never-weighed ghost:

Fleet::W002  truck has never been weighed   [#i3356…]
scenario: applied 1 mutation(s) from examples/check_constraints/demo.toml

Registering a truck with weight > 100 would instead be refused atomically with Fleet::E001.

Honest caveats (what runs today)

• ox check --codes prints only error-severity codes (it is the machine-readable feed for the coverage gates). Both checks here that fire at build are Warnings, so --codes reports ok and exits 0 — the warnings surface on plain ox build (rendered) and on the run-scenario observe channel, not in the --codes stream.
• Catalog-level discharge happens at ox check / ox build, and live in the editor — the LSP runs the same discharge and publishes firings as you type.

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the runtime delta-guard behaviour — the under-limit registration commits and an over-limit one is refused — so the both-moments discharge can’t drift from the language.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! `check` discharge across both moments — RFD 0025.

mod fleet;

fleet.ar

//! `check` rules discharge where their *vocabulary* says (RFD 0025, §7.6):
//!
//!   * `NoDeprecatedVehicles` is **catalog-level** — every variable is
//!     `TypeRef`-sorted — so it discharges finally at `ox check` / `ox build`
//!     (and live in the editor via the LSP, which runs the same discharge). It carries
//!     `#[static]` by convention: if its body ever drifts to instance
//!     vocabulary, the build fails with OE1322 instead of silently
//!     reclassifying to runtime. Here it FIRES at build (Warning):
//!     `OldTruck` still specializes `Deprecated`.
//!
//!   * `OverweightTruck` is **instance-level** with `Severity::Error`, so at
//!     runtime it is a *delta guard*: a mutation that creates a violation
//!     (weight > 100) is rejected atomically with `Fleet::E001`; mutations
//!     that don't make things worse pass. Pre-existing violations never block.
//!
//!   * `UnweighedTruck` is instance-level too, and shows the **both moments**
//!     rule: part of its EDB is declared in source (`pub fact Truck(ghost)`),
//!     so it fires once at build over the declared facts (Warning) — and again
//!     at runtime, on the observe channel, for any truck registered without a
//!     weighing.
//!
//! Expected: `ox check`/`ox build` render `Fleet::W001` (OldTruck) and
//! `Fleet::W002` (ghost) and succeed (warnings pass; a firing `Error` check
//! would fail the build and write no artifact). After demo.toml registers
//! `hauler` at weight 50, the Truck extent is {ghost, hauler} and `hauler` is
//! weighed; registering a 200-weight truck is refused by the guard.
//!
//! All concepts use the neutral `pub type` introducer (`std::core`'s
//! no-commitment baseline metatype) — this example carries no ontological
//! commitment; vocabulary packages (UFO et al.) are external libraries.

pub type Vehicle;

pub type Deprecated;

pub type OldTruck <: Deprecated;

// ANCHOR: catalog_check
#[static]
pub check NoDeprecatedVehicles(t: TypeRef) :-
    specializes(t, Deprecated),
    t != Deprecated => Diagnostic {
        severity: Severity::Warning,
        code: "Fleet::W001",
        message: "type still specializes Deprecated — migrate it before v2"
    };
// ANCHOR_END: catalog_check
pub type Truck {
    mut weight: Int,
}

pub type Weighed;

// ANCHOR: instance_check
pub check OverweightTruck(v: Truck) :-
    v.weight > 100 => Diagnostic {
        severity: Severity::Error,
        code: "Fleet::E001",
        message: format!("truck exceeds the 100t road limit: {}", v.weight)
    };
// ANCHOR_END: instance_check
pub check UnweighedTruck(v: Truck) :-
    v: Truck,
    not Weighed(v) => Diagnostic {
        severity: Severity::Warning,
        code: "Fleet::W002",
        message: "truck has never been weighed"
    };

// Declared EDB — the build-visible half of UnweighedTruck's "both moments".
pub fact Truck(ghost);

pub mutate register_truck(v: Truck, weight: Int) {
    insert iof(v, Truck);
    insert iof(v, Weighed);
    update v: Truck set { weight = weight };
}