Checks

A check observes and reports; it never changes state. When its body holds, it emits the diagnostic on the right of =>. This is how an integrity rule flags a violation instead of silently repairing it. Double-entry accounting has one invariant — within every journal entry, total debits equal total credits — and it is a single check comparing two aggregates:

pub check EntryNotBalanced(e: Entry) :-
    e: Entry,
    debits  = sum(p.amount for p in Posting, inEntry(p, e), p.side == "D"),
    credits = sum(p.amount for p in Posting, inEntry(p, e), p.side == "C"),
    debits != credits
    => Diagnostic {
        severity: Severity::Error,
        code:     "Ledger::E001",
        message:  "journal entry is not balanced",
    };

Each sum totals one side of the entry; debits != credits fires the diagnostic. A balanced entry derives nothing.

Where a check discharges is decided by what its body reads, not by an annotation the author writes. A catalog-level check — every variable reflective-sorted, reading declaration structure like specializes or implements — discharges at ox check and ox build, because the declared catalog is closed at build and evaluation there is final. This is the user-extensible compiler-diagnostic mechanism: a vocabulary package ships its modeling constraints as check rules, and they surface under the package’s own codes like any built-in diagnostic. An instance-level check — any variable ranging over individuals — discharges at runtime, on every mutation boundary, as a delta guard: it rejects a mutation that creates a violation while leaving a pre-existing one to be reported, not blocked. The guard is over the change, not the absolute state.

Severity decides the consequence. Because EntryNotBalanced carries Severity::Error, an unbalanced posting is rejected, not merely reported — at build a firing error writes no artifact, and at runtime it aborts the offending mutation atomically. Double-entry is enforced at the rule layer, not left to a downstream report. The mechanization proves the two halves that make this trustworthy: a catalog-closed check evaluates identically at build and against any extending store, and the runtime guard passes exactly when the mutation introduces no new violation. Argon by Example carries the worked check packages — double_entry_v0 and check_constraints.