Argon by Example

Runnable, CI-verified example packages. Each is a real Argon package — build it with ox build examples/<name> and run it (ox run-scenario, ox query, ox derive, or ox test, per its README) — and its README.md explains what it teaches and shows the actual output. This index is generated from those READMEs and grouped by learning area.

38 example packages:

Getting started

Vocabulary & packages

Relations

Refinement & types

Rules, aggregates & recursion

Constraints & checks

Defeasible reasoning

Standpoints & federation

Bitemporal time

Modal operators

Traits

Testing

Capstone

Other

Hello: the first program

Area: Getting started Teaches: the shape of an Argon source file — the std::core opt-in, a struct and an enum, a function, a derive rule, and the meta-calculus introducers (metaxis / metatype) that make the language vocabulary-neutral. Prerequisites: none — this is the entry point. Run: ox build examples/hello && ox check examples/hello

Argon ships zero built-in classifying vocabulary. Even type and rel — the keywords you declare a concept and a relation with — are not language keywords; they are the baseline introducers in std::core, brought in by an explicit use:

use std::core::{type, rel};

That single line is the whole story of the language’s neutrality: the words you classify your domain with are imported, never assumed. A foundational ontology like UFO is just another package you use — never something baked into the compiler.

What to read in root.ar

Ordinary data carriers — a struct and an enum. These are the value-level shapes, the parts of Argon that look like any modern typed language:

pub struct Diagnostic { severity: Severity, code: String, message: String }
pub enum Severity { Error, Warning, Info, Hint }

The meta-calculus introducers. A metaxis declares an axis of classification — a user-named dimension the compiler never reads the meaning of, only the lattice. A metatype is an introducer keyword built from positions on those axes:

pub metaxis rigidity for metatype { anti_rigid < semi_rigid < rigid };
pub metaxis sortality for metatype { sortal, non_sortal };

pub metatype kind = { rigidity: rigid, sortality: sortal };

After this, kind is usable as a declaration keyword for concepts — the same mechanism the vocabulary packages in this cluster (vocab_pkg_v0, metarel_vocab_v0) publish for other packages to import. hello declares the axes locally; the rest of the cluster shows them crossing a package boundary.

A function and a derive rule round out the file — the function is a pure value-level definition, the derive is a rule head over a body:

pub fn double(x: Int) -> Int = x * 2;
derive owes_tax(p) :- p.income > 0;

Running it

hello is the parser/elaboration smoke example — it declares forms but seeds no individuals, so there is nothing to query. Build it and check it:

$ ox build examples/hello
wrote examples/hello/target/root.oxbin (11 events, 6204 bytes)

$ ox check examples/hello --codes
ok

The artifact carries 11 events (one per declaration). ox check passes clean.

Honest caveats (what runs today)

• This package declares no pub query and no scenario, so ox query reports (module declares no \pub query` items). The owes_tax derive returns **0 tuples** (ox derive examples/hello owes_tax) — no Personindividuals are seeded andPersonhere has noincomefield, so the rule has nothing to fire on. The file is a *shape* demonstration, not a reasoning demonstration; for reasoning that produces rows, seeexamples/first_class_relationsandexamples/legal_norms_can_vote`.

This example is compiled and checked through the same ox pipeline the rest of the corpus uses; if a language change breaks its parse or elaboration, the build fails rather than the docs going stale.

Source

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

//! Walking example for the v0 parser smoke test.

// ANCHOR: opt_in
use std::core::{ type, rel };
// ANCHOR_END: opt_in
pub struct Diagnostic {
    severity: Severity,
    code: String,
    message: String,
}

pub enum Severity {
    Error,
    Warning,
    Info,
    Hint,
}

// ANCHOR: vocab
pub metaxis rigidity for metatype { anti_rigid < semi_rigid < rigid };
pub metaxis sortality for metatype { sortal, non_sortal };

pub metatype kind = { rigidity: rigid, sortality: sortal };
// ANCHOR_END: vocab
// ANCHOR: concept
pub type Person {
    name: String,
    age: Nat,
}

pub fn double(x: Int) -> Int = x * 2;

derive owes_tax(p) :- p.income > 0;
// ANCHOR_END: concept

Struct and enum values: data with no identity

Area: Getting started Teaches: the VALUE side of the value/ontology boundary — struct and enum as language built-ins (struct and enum). Pure data: structural equality, immutability, no metatype, no fact-store identity. How to construct a struct value, project a field, do a functional update with ..spread, build an enum payload value, read a payload back out with a value-position match, and read an optional field’s payload with the rule-body is Some(a) form. Prerequisites: hello (the shape of a source file). Run: ox check examples/struct_enum_values && ox test examples/struct_enum_values

Argon draws a line between ontology and data. A type (or any metatype-introduced concept) declares an entity with identity — an individual the fact store mints an id for, classifies, and reasons over. A struct or enum declares plain data: a value that is its contents, with no identity and no place in the metatype calculus. The two keywords are language built-ins, always available; the classifying vocabulary (type, rel) is imported.

This example is the data side. Everything here is a value.

A struct is its fields

pub struct Point { x: Int, y: Int }

pub fn origin() -> Point = Point { x: 0, y: 0 };
pub fn x_of(p: Point) -> Int = p.x;

A struct value is constructed by naming the type and giving every field. It is an ordinary expression — it can be a let binding, a field value, a function argument or return, a list element, or either side of a comparison. The postfix .x projects a field back out.

Equality is structural. Two struct values are equal when their fields are equal, field by field — there is no identity to tell them apart, and field order in the literal does not matter:

test "struct values are equal field-wise, order-independent" {
    assert Point { x: 1, y: 2 } == Point { y: 2, x: 1 };
    assert Point { x: 1, y: 2 } != Point { x: 1, y: 3 };
}

Immutability and ..spread

A struct value never changes. To get a value that differs in a few fields, copy an existing one and override those fields with the ..base spread — it yields a new value and leaves the base untouched:

test "spread overrides one field and leaves the base untouched" {
    let p = Point { x: 1, y: 2 };
    assert Point { ..p, x: 5 } == Point { x: 5, y: 2 };
    assert p == Point { x: 1, y: 2 };
}

Because the value is immutable, mut on a struct field is meaningless and refused (OE0253), and insert — which mints identity — is refused on a struct (OE0252). A struct is constructed as a value, never inserted.

Enum values, with and without a payload

pub enum Price { Cents(Int), Free }

A payloadless variant is a path: Price::Free. A payload variant carries one value and is built by applying the variant to it: Price::Cents(500). Enum values compare structurally too — same variant, same payload:

test "enum payload values compare structurally" {
    assert Price::Cents(500) == Price::Cents(500);
    assert Price::Cents(500) != Price::Cents(400);
    assert Price::Free != Price::Cents(0);
}

The struct-row table: a parameterized test

A struct value is the natural carrier for a parameterized test: one Case per scenario, looped with for. Each row is a value; the loop runs the same assertion over all of them.

pub struct Case { lhs: Int, rhs: Int, sum: Int }

test "addition over a table of struct cases" {
    for c in [
        Case { lhs: 0,  rhs: 0,  sum: 0 },
        Case { lhs: 2,  rhs: 3,  sum: 5 },
        Case { lhs: 20, rhs: 22, sum: 42 },
    ] {
        assert c.lhs + c.rhs == c.sum;
    }
}

Reading a payload back out

The idiomatic way to read or consume an enum value is a value-position match expression. Each arm names a variant; a payload arm binds the carried value into a fresh variable over the arm’s result. As an expression it sits anywhere a value can — a let right-hand side, a comparison operand, a fn body:

test "value-position match reads an enum payload" {
    let p = Price::Cents(500);
    assert (match p { Price::Cents(c) => c, Price::Free => 0 }) == 500;

    let free = Price::Free;
    assert (match free { Price::Cents(c) => c, Price::Free => 0 }) == 0;
}

For an optional field (age: Int?) inside a rule body, the reader is the membership test path is Some(binder): a present field binds the variable and contributes one row; an absent field contributes none, so the surrounding conjunction fails. is None is the absence test.

pub type Person { mut age: Int? }

pub derive Adult(p, a) :- p: Person, p.age is Some(a), a >= 18;
pub derive Ageless(p)  :- p: Person, p.age is None;

Running it

$ ox check examples/struct_enum_values --codes
ok

$ ox test examples/struct_enum_values
PASS  value-position match reads an enum payload
PASS  struct values are equal field-wise, order-independent
PASS  spread overrides one field and leaves the base untouched
PASS  projection reads a field off a struct value
PASS  enum payload values compare structurally
PASS  addition over a table of struct cases

6 passed, 0 failed, 0 errored, 0 inconclusive

Honest caveats (what runs today)

• A user-declared generic struct/enum (enum Opt<T> { … }) parses, but its type parameters reach no storage slot, so applying it (Opt<Int>) is refused (OE0235). The library generics Option<T> / Result<T, E> and the optional-field form T? are the supported parameterized shapes.
• A payload-binding match arm executes in value position (let r = match opt { Some(x) => x, None => 0 };, shown above) — but only there. The same arm in statement position (an effectful arm inside a mutate statement-match, e.g. match opt { Some(v) => { let _ = insert T { n: v }; }, None => {} }) is not yet executable — it is refused with OE1319 rather than mis-evaluated. Bind the payload in value position first, then run the effect. match over constant patterns (payloadless variants, literals, _) executes in both positions (pattern matching).
• A match over an enum declared in a different module (e.g. a test in tests/mod.ar matching an enum from root.ar) currently can’t resolve the scrutinee’s enum statically and is refused OE1319; keep the payload match in the same file as the enum (this example’s value-match test lives in root.ar).
• Calling a user fn inside a test assertion is not yet wired in the term evaluator, so the tests above construct and compare values directly rather than through the fn wrappers in root.ar. The functions still build and check; they are exercised by ox check / ox build.

This example is compiled, checked, and run through the same ox pipeline as the rest of the corpus; the whole-corpus gate (oxc-driver/tests/examples_corpus_gate.rs) ox checks it at source HEAD, so a language change that breaks its parse or elaboration fails CI rather than letting the docs go stale. The value-position payload-match semantics this example shows are independently gated end-to-end (construct, bind, select) by enum_payload_construct_equality_and_match_binding in oxc-driver/tests/cli_pipeline.rs.

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

//! Struct and enum VALUES: the data side of the value/ontology boundary.
//!
//! `struct` and `enum` are language built-ins (§5.1) — pure data, with no
//! metatype, no fact-store identity, and structural equality. A struct value
//! IS its fields; an enum value IS its variant (and its one payload, if any).
//! They are constructed in any value position — a `let`, a field, a function
//! argument or return, a list element, either side of a comparison.
//!
//! Demonstrates:
//!   * a struct value, constructed and projected
//!   * structural, field-wise, order-independent equality
//!   * `..spread` functional update — a NEW value, the base untouched
//!   * an enum payload variant as a value (`Money::Cents(n)`)
//!   * reading a payload back out with a value-position `match` expression
//!   * the `is Some(a)` rule-body form that reads an optional field's payload

// ANCHOR: struct
// A struct is a closed record of named fields. Equality is structural: two
// `Point` values are equal exactly when their `x` and `y` are equal — there
// is no identity to distinguish them.
pub struct Point {
    x: Int,
    y: Int,
}

pub fn origin() -> Point = Point { x: 0, y: 0 };

// Projection reads a field off a struct value.
pub fn x_of(p: Point) -> Int = p.x;
// ANCHOR_END: struct
// ANCHOR: case
// A struct value is the natural carrier for a parameterized-test row: one
// `Case` per scenario, looped with `for` (see `tests/mod.ar`).
pub struct Case {
    lhs: Int,
    rhs: Int,
    sum: Int,
}
// ANCHOR_END: case
// ANCHOR: spread
// Struct values are immutable. To get a value that differs in one field, use
// the `..base` spread: it copies `base`, overrides the restated fields, and
// yields a NEW value. `base` is never modified.
pub fn move_right(p: Point, dx: Int) -> Point = Point { ..p, x: p.x + dx };
// ANCHOR_END: spread
// ANCHOR: enum
// An enum names a closed set of variants; a variant may carry one payload
// value. `Cents(n)` is a payload variant; `Free` is payloadless. Enum values
// also compare structurally.
pub enum Price {
    Cents(Int),
    Free,
}

pub fn paid(amount: Int) -> Price = Price::Cents(amount);
pub fn comp() -> Price = Price::Free;
// ANCHOR_END: enum
// ANCHOR: value_match
// Reading a payload OUT of an enum value is a value-position `match`: each arm
// names a variant, and a payload arm binds the carried value into a fresh
// variable over the arm's result. `let amount = match p { … }` is the
// idiomatic way to read or consume an enum value.
pub fn amount(p: Price) -> Int = match p {
    Price::Cents(c) => c,
    Price::Free => 0
};

test "value-position match reads an enum payload" {
    let p = Price::Cents(500);
    assert (
        match p {
            Price::Cents(c) => c,
            Price::Free => 0
        }
    ) == 500;

    let free = Price::Free;
    assert (
        match free {
            Price::Cents(c) => c,
            Price::Free => 0
        }
    ) == 0;
}
// ANCHOR_END: value_match
// ANCHOR: payload_bind
// The rule-body `is Some(a)` test reads an optional FIELD's payload: a present
// `age` binds `a`; an absent one makes the conjunction fail. `is None` is the
// absence test. (Value-position `match` above is the expression form; only a
// payload arm in STATEMENT position — an effectful arm — is not yet executable,
// §6.6.)
pub type Person {
    mut age: Int?,
}

pub derive Adult(p, a) :- p: Person, p.age is Some(a), a >= 18;
pub derive Ageless(p) :- p: Person, p.age is None;
// ANCHOR_END: payload_bind

tests/mod.ar

//! In-language tests for the struct/enum value semantics in `root.ar`.
//! Run with `ox test examples/struct_enum_values`.
//!
//! Assertions construct and compare values directly: the `test` atom's term
//! evaluator runs struct/enum construction, projection, `..spread`, and
//! structural equality, so each value form is exercised end-to-end here.

test "struct values are equal field-wise, order-independent" {
    assert Point { x: 1, y: 2 } == Point { y: 2, x: 1 };
    assert Point { x: 1, y: 2 } != Point { x: 1, y: 3 };
}

test "spread overrides one field and leaves the base untouched" {
    let p = Point { x: 1, y: 2 };
    assert Point { ..p, x: 5 } == Point { x: 5, y: 2 };
    assert p == Point { x: 1, y: 2 };
}

test "projection reads a field off a struct value" {
    let p = Point { x: 9, y: 0 };
    assert p.x == 9;
    assert p.y == 0;
}

test "enum payload values compare structurally" {
    assert Price::Cents(500) == Price::Cents(500);
    assert Price::Cents(500) != Price::Cents(400);
    assert Price::Free != Price::Cents(0);
}

// The struct-row table: one `Case` value per scenario, looped with `for`. The
// idiomatic Argon parameterized test — a struct value carries each row's data.
test "addition over a table of struct cases" {
    for c in [
        Case { lhs: 0, rhs: 0, sum: 0 },
        Case { lhs: 2, rhs: 3, sum: 5 },
        Case { lhs: 20, rhs: 22, sum: 42 }
    ] { assert c.lhs + c.rhs == c.sum; }
}

A legal deontic vocabulary package

Area: Vocabulary & packages Teaches: how to publish a vocabulary — a package whose pub surface is upper-ontology concepts, introducer metatypes, an endpoint-constrained metarel, and catalog checks that a consumer gets for free when it imports the package. Prerequisites: machine parts (metarel endpoints, meta, specializes), and the meta-calculus. Run: ox build examples/legal_vocab_v0 && ox check examples/legal_vocab_v0 --codes

Ontological vocabulary is never built into Argon and never in std — a modeler ships it as an ordinary package and a consumer depends on it by path. This is the deontic counterpart of vocab_pkg_v0: a UFO-L modeler ships the deontic concepts, the directed-obligation relation, and the audits a legal modeler inherits. Its consumer is legal_catalog_v0.

What to read in root.ar

An axis orders the modalities. deontic_force is pure user vocabulary — the compiler never reads a force name — ordering the three modalities by the strength of the constraint each imposes:

pub metaxis deontic_force for metatype { permission < obligation < prohibition };

Introducer metatypes become the consumer’s declaration keywords. A consumer writes pub obligation PayRent <: … and the introducer gate resolves the keyword across the dependency boundary. Each binds its force on the axis:

pub metatype permission  = { deontic_force::permission,  legal_kind::norm };
pub metatype obligation  = { deontic_force::obligation,  legal_kind::norm };
pub metatype prohibition = { deontic_force::prohibition, legal_kind::norm };

The deontic relation constrains both endpoints. A directed obligation runs from a debtor to a creditor — both party-sorted, never a contract or a bare individual. The endpoint metatypes are verified at elaboration; a relation declared with this introducer whose endpoint is not party-sorted is refused (see legal_catalog_bad_v0):

pub metarel directed_obligation(debtor: party, creditor: party);

The vocabulary ships its own checks. Every variable is TypeRef-sorted, so each #[static] check discharges at the consumer’s ox check, reading meta(k) / specializes. OrphanObligationConcept flags a norm-tagged concept that anchors to nothing in the vocabulary:

#[static]
pub check OrphanObligationConcept(k: TypeRef) :-
    meta(k) == obligation,
    not specializes(k, TimedObligation)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "UFOL::W002",
        message:  "an `obligation` concept does not specialize `TimedObligation` — anchor it so its deadline discipline is inherited",
    };

Running it

The vocabulary itself checks clean — the checks fire on a consumer’s catalog, not on the vocabulary’s own declarations:

$ ox check examples/legal_vocab_v0 --codes
ok

The “free checks” property — that an imported check actually runs on the importing package — is demonstrated by the consumer legal_catalog_v0, where OrphanObligationConcept fires UFOL::W002 on the orphan norm concept.

This example is compiled in CI; the corpus auto-discovery parses and resolves it, and a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the package surface, so it can’t drift from the language.

Source

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

//! `legal_vocab_v0` — a small UFO-L-shaped legal deontic vocabulary package,
//! published for a SEPARATE consumer (`legal_obligations_v0`) to depend on by
//! path (RFD 0030; the two-package vocabulary-authoring journey). It is the
//! deontic counterpart of `vocab_pkg_v0`: a vocabulary author (the
//! ArgUFO/UFO-L modeler) ships the upper-ontology deontic concepts, the
//! deontic relation, and the catalog checks a legal modeler gets for free.
//!
//! The deontic plane it ships, all on `pub`, for a consumer to import:
//!
//!   * A `deontic_force` **metaxis** — the modal force of a norm
//!     (`permission < obligation < prohibition`, ordered by strength of the
//!     constraint a norm places on the bearer). Pure user vocabulary; the
//!     compiler never reads a force NAME (the no-ambient-ontology rule —
//!     deontic vocabulary is NEVER built-in and never `std`).
//!
//!   * Three introducer **metatypes** the consumer uses as declaration
//!     keywords for its own norm concepts, each binding its force on the axis:
//!     `permission`, `obligation`, `prohibition`. A consumer writes
//!     `pub obligation PayRent <: …` and the §3.4 introducer gate resolves the
//!     keyword across the dependency boundary (RFD 0030 D2).
//!
//!   * A `party` introducer metatype — the legal subjects (debtor / creditor)
//!     a directed obligation runs between — and a `legal_relator` metatype for
//!     the contract that bundles the obligations (UFO: a contract is a
//!     *relator* truthmaking the parties' obligations).
//!
//!   * A binary introducer **metarel** `directed_obligation<debtor, creditor>`
//!     whose BOTH endpoints are metatype-constrained to be `party`-sorted
//!     (#311, RFD 0031 D1): a directed obligation runs from one legal party to
//!     another, never to a contract or a bare individual. The sibling
//!     `legal_catalog_bad_v0` fixture supplies a wrong-sorted endpoint and is
//!     refused OE0631 at elaboration.
//!
//!   * Two package-shipped catalog **checks** — `ProhibitionIsNotAnObligation`
//!     and `OrphanObligationConcept` — that fire on the CONSUMER's catalog at
//!     the consumer's `ox check` (the thing that makes a vocabulary REAL:
//!     imported checks run). They mirror the working `OrphanKind` pattern in
//!     `examples/vocab_pkg_v0`.

// ── Axes (pure user vocabulary; the compiler never reads a force name) ──
//
// `deontic_force` orders the three modalities by the strength of the
// constraint the norm imposes: a permission leaves the bearer free, an
// obligation compels an act, a prohibition forbids one.
pub metaxis deontic_force for metatype { permission < obligation < prohibition };

// `legal_kind` separates the two structural roles a legal concept can play:
// a `norm` is a deontic statement; a `subject` is a party or a relator that
// norms range over. Used by the shipped checks to tell norms from subjects.
pub metaxis legal_kind for metatype { subject, norm };

// ── Introducer metatypes: the keywords this vocabulary ships ──
//
// The three deontic modalities — each binds its force on `deontic_force` and
// is tagged `norm` on `legal_kind`. A consumer declares its norm concepts
// with these as keywords (`pub obligation PayRent <: …`).
pub metatype permission = { deontic_force: permission, legal_kind: norm };
pub metatype obligation = { deontic_force: obligation, legal_kind: norm };
pub metatype prohibition = { deontic_force: prohibition, legal_kind: norm };

// The legal subjects. A `party` is a legal person (debtor / creditor); a
// `legal_relator` is the contract that bundles and truthmakes the obligations
// (UFO: contracts are relators). Both are `subject`s, not norms.
pub metatype party = { legal_kind: subject };
pub metatype legal_relator = { legal_kind: subject };

// ── The deontic relation ──
//
// A binary introducer metarel whose BOTH endpoints are `party`-sorted: a
// directed obligation runs FROM a debtor TO a creditor (UFO-L's directed
// obligation between two legal subjects). The endpoint metatypes are verified
// at elaboration (#311) — a relation declared with this introducer whose
// endpoint type is not `party`-sorted is refused OE0631.
pub metarel directed_obligation(debtor: party, creditor: party);

// ── Upper-ontology concepts the consumer specializes ──
//
// `LegalSubject` is the root `party` the consumer's `Person` / `Company`
// specialize; `Contract` is the root `legal_relator`. Shipping these lets the
// consumer's parties and contracts inherit the vocabulary's structural roles.
pub party LegalSubject;
pub legal_relator Contract;

// ── Vocabulary-shipped catalog checks ──
//
// Catalog-level: every variable is `TypeRef`-sorted, so each discharges at
// `ox check` / `ox build` (RFD 0025 §7.6). They run on the CONSUMING catalog's
// concept declarations.
// A prohibition is a force category error if it specializes the deadline-
// bearing obligation root: a prohibition FORBIDS ("you must never X") — it does
// not OBLIGE a timed act, so it has no business inheriting an obligation's
// deadline. This check FIRES (Warning) for any concept the consumer declares
// with the `prohibition` keyword that ALSO specializes `TimedObligation`. It
// demonstrates a force-aware catalog audit reading `meta(k)`.
#[static]
pub check ProhibitionIsNotAnObligation(k: TypeRef) :-
    meta(k) == prohibition,
    specializes(k, TimedObligation) => Diagnostic {
        severity: Severity::Warning,
        code: "UFOL::W001",
        message: "a `prohibition` specializes a `TimedObligation` — a prohibition forbids, it does not oblige; declare it as a top-level `prohibition`"
    };

// Every concept declared with a deontic NORM keyword (`legal_kind::norm`) is
// expected to specialize one of the vocabulary's norm roots so its force is
// anchored. An orphan norm concept — `norm`-tagged but specializing nothing in
// this vocabulary — is flagged. This is the legal counterpart of
// `vocab_pkg_v0`'s `OrphanKind`.
#[static]
pub check OrphanObligationConcept(k: TypeRef) :-
    meta(k) == obligation,
    not specializes(k, TimedObligation) => Diagnostic {
        severity: Severity::Warning,
        code: "UFOL::W002",
        message: "an `obligation` concept does not specialize `TimedObligation` — anchor it so its deadline discipline is inherited"
    };

// The deadline-bearing obligation root the consumer's timed obligations
// specialize. Declared with this vocabulary's own `obligation` keyword; it
// carries the deadline field every directed, time-bounded obligation needs.
pub obligation TimedObligation {
    mut due: Date,
}

Consuming a vocabulary: imported checks run on your catalog

Area: Vocabulary & packages Teaches: the property that makes a vocabulary package real — when you import a vocabulary and declare concepts with its keywords, the vocabulary’s catalog checks run on your declarations at your own ox check/ox build. Cross-package static checking, for free. Prerequisites: the legal vocabulary package it imports. Run: ox build examples/legal_catalog_v0

legal_vocab_v0 ships deontic concepts, an introducer metatype obligation, and an OrphanObligationConcept check. This package imports the vocabulary, declares two norm concepts with its keyword, and the vocabulary’s check fires across the package boundary on this catalog — one well-formed, one orphan.

What to read in root.ar

Import the vocabulary’s keywords and concepts:

use legal_vocab_v0::{ obligation, party };
use legal_vocab_v0::{ LegalSubject, TimedObligation };

A well-formed norm anchors to the vocabulary’s root, so it inherits the deadline discipline and the check stays silent:

pub obligation PayRent <: TimedObligation { mut amount: Decimal }

An orphan norm anchors to nothing in the vocabulary — declared with the obligation keyword but specializing no norm root. This is exactly what OrphanObligationConcept is built to catch:

pub obligation Indemnify { mut scope: String }

Running it

ox build elaborates the two modules together and the vocabulary-shipped check fires on Indemnify (the orphan) while leaving PayRent (anchored) silent:

workspace: elaborated 2 module(s) into one artifact
UFOL::W002

  ⚠ UFOL::W002: an `obligation` concept does not specialize `TimedObligation`
  │ — anchor it so its deadline discipline is inherited [Indemnify]
  help: fired by check `legal_vocab_v0::OrphanObligationConcept`

The help: line names the check’s originating package — the diagnostic comes from the dependency, not from this file. The decisive contrast is PayRent vs Indemnify: both are declared with the imported obligation keyword, but only the orphan trips the imported audit. UFOL::W002 is a Warning, so the build succeeds (ox check --codes reports ok).

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the cross-package check behaviour, so the “imported checks run” property can’t drift from the language.

Source

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

//! `legal_catalog_v0` — the cross-package catalog-check proof for the deontic
//! vocabulary `legal_vocab_v0` (RFD 0030; GO-journey (a)). It imports the
//! vocabulary and declares a WELL-FORMED norm concept and an ORPHAN one, so the
//! vocabulary-SHIPPED `OrphanObligationConcept` catalog check fires on THIS
//! consumer's catalog at the consumer's `ox check` — the property that makes a
//! vocabulary package real: imported checks run.
//!
//! This consumer carries NO defeasibility plane, so the check-discharge gate
//! (the wall documented in `legal_obligations_v0`) does not apply: the
//! vocabulary's checks and this catalog co-exist. The served flagship model
//! (`legal_obligations_v0`) carries the defeasible/temporal/derived/HTTP half
//! against the same vocabulary; the two halves are split by that gate.
//!
//! Mirrors the `vocab_consumer_v0` / `vocab_pkg_v0` pattern, lifted to the
//! legal-deontic vocabulary.

use legal_vocab_v0::{ obligation, party };
use legal_vocab_v0::{ LegalSubject, TimedObligation };

// A party declared with the imported `party` introducer.
pub party Tenant <: LegalSubject {
    name: String,
}

// WELL-FORMED: a norm concept declared with the imported `obligation` keyword
// that anchors to the vocabulary's `TimedObligation` root — so it inherits the
// deadline discipline and the `OrphanObligationConcept` check does NOT fire.
pub obligation PayRent <: TimedObligation {
    mut amount: Decimal,
}

// ORPHAN: a norm concept declared with the imported `obligation` keyword that
// does NOT specialize `TimedObligation`. The vocabulary-shipped
// `OrphanObligationConcept` catalog check FIRES on this declaration
// (Warning UFOL::W002) at THIS consumer's `ox check`.
pub obligation Indemnify {
    mut scope: String,
}

Legal catalog — cross-package refusal fixture

Area: Vocabulary & packages Teaches: the negative companion to legal_catalog_v0 — pointing an imported directed_obligation’s creditor endpoint at a norm concept instead of a party is refused with OE0631 across the package boundary. Run: ox check examples/legal_catalog_bad_v0 --codes (must print OE0631 and exit non-zero)

Conformance fixture, not a tutorial. This package is designed to be refused. It exists so CI can prove a metarel-endpoint violation is caught across a package boundary — the constraint lives in the imported vocabulary, not in this file. For the well-formed consumer, read legal_catalog_v0; for the vocabulary, legal_vocab_v0.

The imported directed_obligation metarel constrains both endpoints to be party-sorted. This fixture points the creditor endpoint at PayRent, a norm concept (an obligation) — a directed obligation cannot run to a norm:

pub directed_obligation owesBad(debtor: Tenant, creditor: PayRent);

ox check must refuse this with OE0631 and exit non-zero — the endpoint check fires on the dependency-declared metarel:

$ ox check examples/legal_catalog_bad_v0 --codes
OE0631
$ echo $?
1

The full diagnostic names the offending position and both metatypes:

× OE0631: in `root::owesBad`, position 1 of relation `owesBad` is `PayRent`
│ (a `obligation`), but its classifying metarel `directed_obligation`
│ declares that position as `party` — an endpoint must be (a sub-metatype
│ of) the metarel's position metatype.

A corpus test (oxc-runtime/tests/examples_corpus.rs) asserts this package is refused with OE0631 — proving the metarel endpoint constraint survives the package join. If it regressed, this fixture would start building and CI would fail.

Source

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

//! `legal_catalog_bad_v0` — the cross-package metarel-endpoint REFUSAL fixture
//! for the deontic vocabulary `legal_vocab_v0` (#311, RFD 0031 D1). It declares
//! a relation with the imported `directed_obligation` metarel keyword whose
//! creditor endpoint is a NORM concept (`PayRent`), not a `party`. The
//! vocabulary constrains both `directed_obligation` endpoints to be
//! `party`-sorted, and the endpoint-metatype check fires ACROSS the package
//! boundary: `ox check` refuses with OE0631. The sibling `legal_catalog_v0` is
//! the well-formed counterpart.

use legal_vocab_v0::{ obligation, party, directed_obligation };
use legal_vocab_v0::{ LegalSubject, TimedObligation };

pub party Tenant <: LegalSubject {
    name: String,
}
pub party Landlord <: LegalSubject {
    name: String,
}

pub obligation PayRent <: TimedObligation {
    mut amount: Decimal,
}

// WRONG: the creditor endpoint must be `party`-sorted, but `PayRent` is a
// `norm` (an obligation). Refused OE0631 across the dependency boundary.
pub directed_obligation owesBad(debtor: Tenant, creditor: PayRent);

Vocabulary package: publishing your own classifying vocabulary

Area: Vocabulary & packages Teaches: a package can publish its own introducer metatypes, an introducer metarel, upper categories, and a catalog check — the building blocks a foundational ontology like UFO is made of. None of this is built into the language; it is all ordinary pub surface. Prerequisites: the meta-calculus introducers (metatype / metarel), see hello. Run: ox build examples/vocab_pkg_v0 && ox check examples/vocab_pkg_v0

This is the author side of the two-package vocabulary journey. vocab_pkg_v0 ships a small UFO-shaped vocabulary; vocab_consumer_v0 (a separate package) depends on it. The point is that Argon has no privileged ontology: a vocabulary is a normal package, and everything that makes UFO “UFO” — the kinds, the categories, the well-formedness checks — lives on this package’s public surface.

What to read in root.ar

Introducer metatypes — declaration keywords for the consumer. A metatype published pub becomes a keyword a downstream package declares its concepts with:

pub metatype category = { };
pub metatype kind = { };

A binary introducer metarel. Same idea, for relations: a published metarel is a keyword for declaring relations downstream:

pub metarel characterization<A, B>(a: A, b: B);

Upper-ontology categories the consumer specializes. These are concepts declared with the package’s own category introducer, forming a small hierarchy the consumer hangs its domain off of:

pub category Endurant;
pub category Substantial <: Endurant;
pub category Detached    <: Endurant;

A catalog check the vocabulary ships — and that fires on the consumer’s catalog. This is what makes a vocabulary package real rather than decorative. The check is #[static] and every variable is TypeRef-sorted, so it discharges at ox check/ox build time over the catalog of declared types — not over runtime individuals:

#[static]
pub check OrphanKind(k: TypeRef) :-
    meta(k) == kind,
    specializes(k, Detached)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "UFO::W001",
        message:  "a `kind` specializes `Detached` — specialize `Substantial` instead",
    };

It reads the reflective intrinsics meta (the metatype a concept was introduced with) and specializes (the declared hierarchy). It flags any kind that specializes Detached. Crucially, the check is written here, in the vocabulary, but it runs against the consumer’s pub kind declarations — imported checks travel with the vocabulary.

Running it

The vocabulary checks clean on its own — it declares no offending kind itself:

$ ox build examples/vocab_pkg_v0
wrote examples/vocab_pkg_v0/target/root.oxbin (7 events, 4334 bytes)

$ ox check examples/vocab_pkg_v0 --codes
ok

To see OrphanKind actually fire, you need a consumer with a catalog that violates it — that is the next example, vocab_consumer_v0.

Honest caveats (what runs today)

• This package declares no pub query and no individuals; it is pure vocabulary. Its value is realized at a consumer’s ox check — vocab_pkg_v0 alone has nothing for the check to fire on.

This example and its consumer are driven through the real ox binary by a pipeline test (oxc-driver/tests/cli_pipeline.rs): the test pins that this package checks clean and that OrphanKind fires on the consumer’s catalog, so the cross-package check can’t drift from the language.

Source

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

//! `vocab_pkg_v0` — a small UFO-shaped vocabulary package, published for a
//! SEPARATE consumer package to depend on (RFD 0030; the two-package
//! vocabulary-authoring journey, GO-journey (a) of the v0.2.1 release gate).
//!
//! What this package ships, all on its `pub` surface, for a consumer to import
//! with `use vocab_pkg_v0::{ category, kind, characterization };`:
//!
//!   * Two introducer metatypes — `category` and `kind` — that a consumer uses
//!     as DECLARATION KEYWORDS for its own concepts (the §3.4 introducer gate
//!     resolves them across the dependency boundary, RFD 0030 D2).
//!   * A binary introducer metarel — `characterization`.
//!   * A handful of upper-ontology categories (`Endurant`, `Substantial`,
//!     `Detached`) the consumer specializes.
//!   * A catalog `check` rule — `OrphanKind` — over `meta`/`specializes`. This
//!     is the property that makes a vocabulary package REAL: the check is
//!     shipped by the vocabulary and FIRES on the CONSUMER's catalog at the
//!     consumer's `ox check` (a `kind` that specializes the vocabulary's
//!     `Detached` is flagged). It mirrors the working `NoDeprecatedVehicles`
//!     pattern in `examples/check_constraints`.

// ── Introducer metatypes (the consumer declares concepts with these) ──
// ANCHOR: introducers
pub metatype category = { };
pub metatype kind = { };

// ── A binary introducer metarel ──
pub metarel characterization<A, B>(a: A, b: B);
// ANCHOR_END: introducers
// ── Upper-ontology categories the consumer specializes ──
// ANCHOR: categories
pub category Endurant;
pub category Substantial <: Endurant;
// A `kind` specializing `Detached` is an ontological smell the vocabulary
// flags on every consumer catalog (see `OrphanKind`).
pub category Detached <: Endurant;
// ANCHOR_END: categories
// ── Vocabulary-shipped catalog check ──
//
// Catalog-level: every variable is `TypeRef`-sorted, so it discharges at
// `ox check`/`ox build` (RFD 0025 §7.6). It fires (Warning) for any `kind`
// in the consuming catalog that specializes `Detached`. The check is written
// HERE, in the vocabulary; it runs on the CONSUMER's `pub kind` declarations.
// ANCHOR: check
#[static]
pub check OrphanKind(k: TypeRef) :-
    meta(k) == kind,
    specializes(k, Detached) => Diagnostic {
        severity: Severity::Warning,
        code: "UFO::W001",
        message: "a `kind` specializes `Detached` — specialize `Substantial` instead"
    };
// ANCHOR_END: check

A metarel with metatype-constrained endpoints

Area: Vocabulary & packages Teaches: an introducer metarel can constrain the metatype of each endpoint position, and that constraint travels with the published metarel — a consumer’s relation endpoints are verified against it across the package boundary. Prerequisites: publishing a vocabulary (introducer metatypes and metarels). Run: ox build examples/metarel_vocab_v0 && ox check examples/metarel_vocab_v0

A relation is not just a tuple of types — in a vocabulary it often carries an ontological constraint on what kind of thing may sit in each slot. UFO’s characterization relates a bearer to an aspect: the bearer must be a substantial kind, the second slot must be an aspect. metarel_vocab_v0 publishes exactly that shape, so a separate consumer that fills a slot with the wrong sort of thing is refused at its own ox check. (The refusal itself is the companion fixture, metarel_consumer_bad_v0.)

What to read in root.ar

An axis, then two introducer metatypes positioned on it. The axis names are pure user vocabulary — the compiler reads the lattice, never the meaning of the words:

pub metaxis sortality for metatype { sortal, non_sortal };

pub metatype kind   = { sortality::sortal };
pub metatype aspect = { sortality::non_sortal };

A metarel whose endpoints are metatype-constrained. Position 0 (bearer) must be kind-sorted; position 1 (aspect_of) must be aspect-sorted. These position metatypes are part of the published metarel:

pub metarel characterization(bearer: kind, aspect_of: aspect);

When a consumer in another package declares a characterization relation, the endpoint metatypes of its relation are checked against these positions. An endpoint must be (a sub-metatype of) the position’s metatype, or ox check refuses it across the dependency boundary — the same refusal an in-package violation gets.

Running it

The vocabulary checks clean — it only publishes the constrained metarel, it doesn’t use it:

$ ox build examples/metarel_vocab_v0
wrote examples/metarel_vocab_v0/target/root.oxbin (4 events, 2393 bytes)

$ ox check examples/metarel_vocab_v0 --codes
ok

To see the constraint bite, point a consumer at this package and have it fill aspect_of with a kind — that is examples/metarel_consumer_bad_v0, which is refused OE0631.

Honest caveats (what runs today)

• This package declares no individuals and no pub query; it is pure vocabulary. The endpoint constraint is enforced statically, at a consumer’s ox check, not at runtime.

This vocabulary and its (deliberately failing) consumer are driven through the real ox binary by a pipeline test (oxc-driver/tests/cli_pipeline.rs): the test pins that this package checks clean and that a wrong-sorted endpoint in the consumer is refused OE0631, so the cross-package endpoint check can’t drift from the language.

Source

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

//! `metarel_vocab_v0` — a vocabulary package that PUBLISHES a metatype-
//! constrained introducer metarel, for a SEPARATE consumer package to depend
//! on (RFD 0031 D1, #311; the cross-package half of Gustavo's ArgUFO
//! publish→consume journey).
//!
//! The point of this fixture is the CROSS-PACKAGE endpoint-metatype check. The
//! `characterization` metarel below constrains its `aspect_of` position to be
//! `aspect`-sorted. A consumer in a SEPARATE package that declares a
//! `characterization` relation with a wrong-sorted endpoint (a `kind` in the
//! aspect slot) must be refused OE0631 at the consumer's `ox check` — the same
//! refusal an in-package violation gets (`examples/machine_parts_bad`).
//!
//! Published on the `pub` surface for `use metarel_vocab_v0::{ kind, aspect,
//! characterization };`.

// ── Axes (pure user vocabulary; the compiler never reads a name) ──
pub metaxis sortality for metatype { sortal, non_sortal };

// ── Introducer metatypes the consumer uses as declaration keywords ──
pub metatype kind = { sortality: sortal };
pub metatype aspect = { sortality: non_sortal };

// ── A binary introducer metarel whose endpoints are metatype-constrained.
// Position 0 (`bearer`) must be `kind`-sorted; position 1 (`aspect_of`) must
// be `aspect`-sorted. These constraints travel with the published metarel and
// are verified against a CONSUMER's relation endpoints across the dependency
// boundary (#311).
pub metarel characterization(bearer: kind, aspect_of: aspect);

metarel_consumer_bad_v0 — conformance fixture (must be refused)

Area: Vocabulary & packages Teaches: the negative companion to metarel_vocab_v0 — filling an imported metarel’s endpoint with the wrong metatype across a package boundary is refused with OE0631 at the consumer’s ox check. Run: ox check examples/metarel_consumer_bad_v0 --codes (must print OE0631 and exit non-zero)

This is a negative conformance fixture, not a tutorial. It depends on metarel_vocab_v0 and intentionally declares a relation with a wrong-sorted endpoint. It MUST fail ox check — that refusal is the whole point. For the teaching version, read metarel_vocab_v0.

What it does wrong

It imports the metatype-constrained characterization metarel from the separate metarel_vocab_v0 package — whose aspect_of position requires an aspect — and then fills that position with a kind:

use metarel_vocab_v0::{ kind, aspect, characterization };

pub kind Person;
pub kind Vehicle;

// WRONG: `aspect_of` requires an `aspect`, but `Vehicle` is a `kind`.
pub characterization inheresVia(bearer: Person, aspect_of: Vehicle);

The constraint lives in the dependency, not in this file — so this fixture proves the endpoint-metatype check survives the package join and is enforced at the consumer’s ox check.

Required behavior

ox check must refuse it with OE0631 and exit non-zero:

$ ox check examples/metarel_consumer_bad_v0 --codes
OE0631
$ echo $?
1

Full diagnostic:

Error: OE0631
  × OE0631: in `root::inheresVia`, position 1 of relation `inheresVia` is
  │ `Vehicle` (a `kind`), but its classifying metarel `characterization`
  │ declares that position as `aspect` — an endpoint must be (a sub-metatype
  │ of) the metarel's position metatype.

This package must never build clean. The pipeline test (oxc-driver/tests/cli_pipeline.rs) asserts the OE0631 refusal through the real ox binary; if a change lets it pass, the test fails.

Source

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

//! `metarel_consumer_bad_v0` — the REFUSAL half of the CROSS-PACKAGE metarel
//! endpoint-metatype proof (RFD 0031 D1, #311 F3). A modeler package that
//! DEPENDS ON the separate `metarel_vocab_v0` vocabulary, imports its
//! `characterization` metarel, and declares a relation whose `aspect_of`
//! position is filled by a `kind` (not an `aspect`).
//!
//! This is exactly Gustavo's publish→consume journey: the constraint lives in
//! a DEPENDENCY, not this file. Before #311 F3 the consumer checked CLEAN (the
//! dependency's `position_metatypes` were discarded at the package join); it
//! must now be refused the feature-named OE0631 — the same refusal the
//! in-package violation (`examples/machine_parts_bad`) gets.
//!
//! This package MUST NOT build; the corpus test asserts the OE0631 refusal.

use metarel_vocab_v0::{ kind, aspect, characterization };

// `Person` and `Vehicle` are both declared with the DEPENDENCY's `kind`
// introducer — both are `kind`-sorted.
pub kind Person;
pub kind Vehicle;

// WRONG: `characterization`'s `aspect_of` position (declared in the dependency)
// requires an `aspect`, but `Vehicle` is a `kind`. Refused OE0631 across the
// dependency boundary — the §4.3 endpoint-metatype verification.
pub characterization inheresVia(bearer: Person, aspect_of: Vehicle);

Consuming a vocabulary across a package boundary

Area: Vocabulary & packages Teaches: a modeler package depends on a separate vocabulary package, imports its introducer metatypes/metarel, and uses them as its own declaration keywords — and the vocabulary’s catalog check fires on this package’s catalog at ox check. Prerequisites: the vocabulary author side — read that first. Run: ox build examples/vocab_consumer_v0 && ox check examples/vocab_consumer_v0

This is the consumer side. vocab_consumer_v0 owns no vocabulary of its own; it declares a path dependency on vocab_pkg_v0 and models its domain entirely with imported keywords. This is the property that makes vocabulary packages real: the modeler classifies with words it doesn’t own, and the introducer gate resolves them across the dependency boundary.

What to read

ox.toml declares the dependency. The key is the path root the consumer imports under, and it must equal the dependency’s package name:

[dependencies]
vocab_pkg_v0 = { path = "../vocab_pkg_v0" }

root.ar imports the vocabulary and declares with it. The introducer metatypes (category, kind) and the metarel (characterization) come from the dependency — this package never declares them:

use vocab_pkg_v0::{ category, kind, characterization };
use vocab_pkg_v0::{ Endurant, Substantial, Detached };

pub kind Person <: Substantial { name: String }
pub category Dwelling <: Endurant;
pub characterization Inhabits(p: Person, d: Dwelling);

Person is declared with the dependency’s kind keyword and specializes the dependency’s Substantial — well-formed.

One declaration deliberately trips the vocabulary’s check. Ghost is a kind that specializes Detached, which is exactly what vocab_pkg_v0’s shipped OrphanKind check warns about:

pub kind Ghost <: Detached;

Running it

ox check resolves the dependency, declares Ghost with the imported kind, and the imported OrphanKind check fires on it — a non-fatal warning that names the offending type and the check that fired:

$ ox check examples/vocab_consumer_v0
UFO::W001

  ⚠ UFO::W001: a `kind` specializes `Detached` — specialize `Substantial`
  │ instead [Ghost]
  help: fired by check `vocab_pkg_v0::OrphanKind`

ok

The decisive detail is fired by check \vocab_pkg_v0::OrphanKind`: the check the modeler is being held to was authored in a package it merely depends on. The build still completes — UFO::W001is aWarning`, not an error:

$ ox build examples/vocab_consumer_v0
workspace: elaborated 2 module(s) into one artifact
UFO::W001
  ⚠ UFO::W001: a `kind` specializes `Detached` — specialize `Substantial` instead [Ghost]
  help: fired by check `vocab_pkg_v0::OrphanKind`
wrote examples/vocab_consumer_v0/target/root.oxbin (13 events, 7182 bytes)

Honest caveats (what runs today)

• UFO::W001 is a Warning, so ox check --codes prints ok (no error codes) even though the warning is emitted. Read the full ox check output (not --codes) to see the warning text.

This consumer and its vocabulary are driven through the real ox binary by a pipeline test (oxc-driver/tests/cli_pipeline.rs): the test pins that this package elaborates against the dependency and that the vocabulary-shipped OrphanKind check fires on Ghost, so the cross-package check can’t drift from the language.

Source

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

//! `vocab_consumer_v0` — a modeler package that DEPENDS ON the separate
//! `vocab_pkg_v0` vocabulary (RFD 0030; GO-journey (a)). It imports the
//! vocabulary's introducer metatypes and uses them as declaration keywords
//! for its own concepts, specializes the vocabulary's upper categories, and
//! the vocabulary-shipped catalog `check` fires on THIS catalog at `ox check`.
//!
//! This is the property that makes vocabulary packages real: the consumer
//! never declares `kind`/`category`/`characterization` — it imports them from
//! a package it doesn't own, and the §3.4 introducer gate resolves them across
//! the dependency boundary.

// ANCHOR: consume
use vocab_pkg_v0::{ category, kind, characterization };
use vocab_pkg_v0::{ Endurant, Substantial, Detached };

// `Person` is declared with the DEPENDENCY's `kind` introducer and specializes
// the dependency's `Substantial` — well-formed, the check does not fire.
pub kind Person <: Substantial {
    name: String,
}

// `Ghost` specializes the dependency's `Detached`. The vocabulary's shipped
// `OrphanKind` catalog check FIRES on this declaration (Warning UFO::W001) at
// the CONSUMER's `ox check` — imported checks run.
pub kind Ghost <: Detached;

// A concept declared with the dependency's `category` introducer.
pub category Dwelling <: Endurant;

// A relation declared with the dependency's `characterization` metarel
// introducer, across the boundary.
pub characterization Inhabits(p: Person, d: Dwelling);
// ANCHOR_END: consume

First-class relations

Area: Relations Teaches: relations are first-class constructs — n-ary, with their own properties, cardinality, specialization, and rule participation. Prerequisites: concepts and <: (see concepts and hierarchies). Run: ox build examples/first_class_relations && ox query examples/first_class_relations

In most data languages a relationship is a second-class thing: a foreign key with no identity and no data of its own, or something you reify by hand into a stand-in node. Argon makes a relation a construct, declared with a rel keyword exactly as a concept is declared with a type keyword. An edge has the same standing as a node.

What to read in root.ar

A relation carries its own data. An employment has a salary — the salary belongs to the relationship, not to the person or the org:

pub rel Employment(employee: Person, employer: Org) { mut salary: Int };

Cardinality is per endpoint (UML association-end multiplicity — the i-th bracket bounds the distinct position-i values for a fixed combination of the other endpoints): [0..1] on the owner slot means an asset has at most one owner, and [0..*] on the asset slot means a person may own any number.

pub rel Owns(owner: Person, asset: Asset) [0..1] [0..*];

Relations are n-ary, not just binary — a sale relates three participants without an intermediate node:

pub rel Sale(seller: Person, buyer: Person, item: Asset);

Relations specialize, like concepts — every internship is an employment:

pub rel Internship(employee: Person, employer: Org) <: Employment;

Relations participate in rules, read in a rule body exactly as a concept’s extent is:

pub derive colleagues(a: Person, b: Person) :- Employment(a, o), Employment(b, o);

Running it

With Alice and Bob both employed by Acme, colleague_pairs returns the four pairings the rule derives — including each person with themselves, since the rule as written does not exclude a = b (adding an inequality guard is a natural exercise).

Honest caveats (what runs today)

• Maximum cardinality is enforced at the write path; a minimum above zero (e.g. [1..1]) is recorded on the wire but not yet enforced in v0 — ox check emits OW1342 naming the relation and position. This example uses [0..1] / [0..*], so it has no unenforced minimum.

This example is compiled and run in CI — the corpus auto-discovery parses and resolves it, and a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the colleague_pairs behaviour to exactly the four pairings the rule derives. If the language changes underneath it, the build breaks rather than the docs going stale.

Source

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

//! First-class relations: an edge is a citizen, the same as a node.
//!
//! In most data languages a relationship is either a foreign key (no identity,
//! no data of its own) or something you reify by hand. In Argon a relation is a
//! first-class construct, declared with a `rel` keyword the way a concept is
//! declared with a `type` keyword. It can be n-ary, carry its own properties,
//! constrain its endpoints' cardinality, specialize another relation, and take
//! part in rules — every affordance a concept has.
//!
//! Demonstrates:
//!   * a relation that carries its OWN data (`Employment` has a salary)
//!   * per-endpoint cardinality (UML association-end multiplicity)
//!   * an n-ary (ternary) relation — relations are not limited to binary
//!   * relation specialization with `<:`
//!   * a relation participating in a `derive` rule, exactly as a concept does

pub type Person {
    name: String,
}
pub type Org {
    name: String,
}
pub type Asset {
    label: String,
}

// ANCHOR: carries_data
// A relationship that is the thing holding the data: an employment HAS a
// salary. The salary belongs to the relation, not to either endpoint.
pub rel Employment(employee: Person, employer: Org) {
    mut salary: Int,
}
// ANCHOR_END: carries_data
// ANCHOR: cardinality
// Cardinality is per endpoint, read as UML association-end multiplicity: the
// i-th bracket bounds the distinct position-i values for a fixed combination
// of the other endpoints. `[0..1]` on the owner slot means an asset has at
// most one owner; `[0..*]` on the asset slot means a person may own any
// number. The maximum is enforced at the write path; see the README on minimums.
pub rel Owns(owner: Person, asset: Asset) [0..1] [0..*];
// ANCHOR_END: cardinality
// ANCHOR: nary
// Relations are n-ary. A sale relates three participants at once — no
// intermediate "SaleRecord" node is needed to hold the third leg.
pub rel Sale(seller: Person, buyer: Person, item: Asset);
// ANCHOR_END: nary
// ANCHOR: specialize
// Relations specialize just like concepts: every Internship is an Employment.
pub rel Internship(employee: Person, employer: Org) <: Employment;
// ANCHOR_END: specialize
// ANCHOR: derive
// And relations take part in rules. `colleagues` reads the `Employment`
// relation in a rule body exactly as it would read a concept's extent.
pub derive colleagues(a: Person, b: Person) :- Employment(a, o), Employment(b, o);
// ANCHOR_END: derive
// Ground facts: two people employed by the same org.
pub fact Person(alice);
pub fact Person(bob);
pub fact Org(acme);
pub fact Employment(alice, acme);
pub fact Employment(bob, acme);

pub query colleague_pairs() -> colleagues;

Machine parts: metarel endpoints, signature reflection, per-type axis override

Area: Relations Teaches: the three relation/meta-property features a vocabulary author needs — a metarel that constrains its endpoints’ metatypes, a derive/check that reflects over relation signatures (rel/arm/meta) to audit them, and a per-type axis override that wins over the metatype default. Prerequisites: first-class relations, and the meta-calculus (metaxis / metatype / metarel, meta). Run: ox build examples/machine_parts_v0 && ox derive examples/machine_parts_v0/target/root.oxbin mountEndpointIsFitting

A vocabulary author building a classification vocabulary — here a small taxonomy of machine parts — does not just declare concepts: they declare the rules of well-formedness for the modelers who consume the vocabulary, and they want the compiler to enforce them. This example is the well-formed proof of three such features; its sibling machine_parts_bad is the refusal half.

What to read in root.ar

A metarel constrains its endpoints’ metatypes. attachment is a binary introducer metarel; its host position must be part-sorted and its mount position must be fitting-sorted. A component mounts via a fitting, not a bare part — and the compiler verifies it at elaboration:

pub metarel attachment(host: part, mount: fitting) {
    load_kind::load_bearing,
};

A relation declared with this introducer whose endpoints match is well-formed; mountedVia does, because Chassis is a part and Bracket is a fitting:

pub attachment mountedVia(host: Chassis, mount: Bracket) [1..1] [0..*];

A vocabulary audits relation signatures declaratively. rel(r, attachment) enumerates every relation classified by the metarel; arm(r, 1, t) reads its position-1 endpoint type; meta(t) reads that type’s metatype. Joined together, the vocabulary checks its own endpoint discipline — r and t are TypeRef-sorted, so this derives at the catalog tier:

pub derive mountEndpointIsFitting(r: TypeRef, t: TypeRef) :-
    rel(r, attachment), arm(r, 1, t), meta(t) == fitting;

pub derive mountEndpointIsPart(r: TypeRef, t: TypeRef) :-
    rel(r, attachment), arm(r, 1, t), meta(t) == part;

A type can override an axis its metatype binds. Gasket is introduced by part, whose metatype binds replaceability::permanent — but a gasket wears out and is consumable. The per-target override sets the type’s own effective replaceability, and the type-keyed t.replaceability projection reads the override, not the metatype default:

pub part Gasket { replaceability::consumable }

pub derive consumableTypes(t: TypeRef) :- t.replaceability == replaceability::consumable;

Running it

The vocabulary’s own audit confirms the discipline holds. The mount endpoint of every attachment relation is fitting-sorted (so the well-formed set is the whole set), and no attachment relation has a part in its mount slot:

derive(mountEndpointIsFitting): 1 tuple(s)
  (<anonymous>::mountedVia, <anonymous>::Bracket)
derive(mountEndpointIsPart): 0 tuple(s)

The override wins: consumableTypes returns three types — fitting and Bracket (consumable by their metatype) and Gasket, whose per-target override beats the permanent it inherits from part:

derive(consumableTypes): 3 tuple(s)
  (<anonymous>::fitting)
  (<anonymous>::Bracket)
  (<anonymous>::Gasket)

Honest caveats (what runs today)

• Maximum cardinality is enforced at the write path; a minimum above zero is recorded on the wire but not yet enforced in v0. mountedVia declares [1..1] at its host position, so ox build emits OW1342 naming the relation and position — a warning, not a refusal; the build succeeds.

This example is compiled and run in CI — the corpus auto-discovery parses and resolves it, and a driver test (oxc-driver/tests/cli/scenario.rs) pins that this package checks clean while its sibling refusal fixture is refused. If the language changes underneath it, the build breaks rather than the docs going stale.

Source

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

//! `machine_parts_v0` — the vocabulary-authoring proof for the v0.2.1
//! relation-constraint plane (RFD 0031). A small machine-parts classification
//! vocabulary that exercises, end-to-end and corpus-pinned, the three
//! relation/meta-property features a vocabulary author needs and could NOT
//! express before:
//!
//!   1. **Metarel endpoint-metatype verification** (#311, RFD 0031 D1). The
//!      `attachment` metarel requires its mount position to be
//!      `fitting`-sorted: a component must mount *via a fitting*, not a bare
//!      part. `mountedVia(host: Chassis, mount: Bracket)` is well-formed
//!      (`Bracket` is a `fitting`); the wrong-sorted variant in the sibling
//!      refusal fixture (`machine_parts_bad`) is refused OE0631.
//!
//!   2. **Relation-signature reflection** (#312, RFD 0031 D2). A
//!      vocabulary-shipped catalog `derive`/`check` quantifies over declared
//!      relations through `rel` / `arm`, joins their endpoint types' metatypes
//!      through `meta`, and audits the endpoint discipline declaratively.
//!
//!   3. **Per-type axis override** (R-M9, RFD 0031 D3). `Gasket` overrides the
//!      `replaceability` its `part` metatype binds — `Gasket`'s effective
//!      replaceability reads the per-target `consumable`, not the metatype
//!      default `permanent`.

// ── Axes (pure user vocabulary; the compiler never reads a name) ──
pub metaxis replaceability for metatype { consumable < serviceable < permanent };
pub metaxis granularity for metatype { atomic, composite };
pub metaxis load_kind for metarel { load_bearing, cosmetic };

// ── Metatypes: the introducer keywords this vocabulary ships ──
pub metatype part = { replaceability: permanent, granularity: atomic };
pub metatype fitting = { replaceability: consumable, granularity: composite };

// ── A binary introducer metarel whose endpoints are metatype-constrained.
// Position 0 must be `part`-sorted (the host), position 1 `fitting`-sorted
// (the fitting it mounts through) — verified at elaboration (#311).
pub metarel attachment(host: part, mount: fitting) { load_kind: load_bearing, };

// ── Concepts declared with this vocabulary's introducers ──
pub part Chassis;
pub fitting Bracket;

// R-M9 (RFD 0031 D3): `Gasket` is introduced by `part` (metatype
// replaceability `permanent`) but OVERRIDES replaceability to `consumable`
// per-target — a gasket wears out even though its metatype is permanent.
pub part Gasket {
    replaceability::consumable,
}

// ── An attachment relation with CORRECT endpoint metatypes ──
// `Chassis` is a `part`, `Bracket` is a `fitting` — matches the metarel
// positions, so this is well-formed (#311 passes).
pub attachment mountedVia(host: Chassis, mount: Bracket) [1..1] [0..*];

// ── #312: relation-signature reflection ──
//
// Enumerate every relation classified by `attachment` together with its
// mount-position endpoint type. Catalog-closed (`rel`/`arm`/`meta` over
// declarations), so `t` and `r` are TypeRef-sorted and this derives at the
// catalog tier.
pub derive attachmentMountEndpoint(r: TypeRef, t: TypeRef) :- rel(r, attachment), arm(r, 1, t);

// The vocabulary's own audit: the mount endpoint of every `attachment`
// relation IS fitting-sorted (so this WELL-FORMED-ENDPOINT set is the whole
// set, and the "part in the mount slot" set below is empty — the discipline
// holds across the consumer catalog).
pub derive mountEndpointIsFitting(r: TypeRef, t: TypeRef) :-
    rel(r, attachment),
    arm(r, 1, t),
    meta(t) == fitting;

pub derive mountEndpointIsPart(r: TypeRef, t: TypeRef) :-
    rel(r, attachment),
    arm(r, 1, t),
    meta(t) == part;

// ── R-M9: the per-target override is read by the TYPE-keyed
// `t.replaceability` projection (`t: TypeRef`). `Gasket` is introduced by the
// `permanent` metatype `part` but its per-target override makes ITS
// replaceability `consumable`. The metatype-tier `meta(t).replaceability`
// would still read the metatype default; `t.replaceability` reads the type's
// own effective value (override winning).
pub derive consumableTypes(t: TypeRef) :- t.replaceability == replaceability::consumable;

Machine parts — refusal fixture

Area: Relations Teaches: the negative companion to machine_parts_v0 — a metarel endpoint filled with the wrong metatype is refused with OE0631 at ox check, pinning the endpoint-constraint diagnostic. Run: ox check examples/machine_parts_bad --codes (must print OE0631 and exit non-zero)

Conformance fixture, not a tutorial. This package is designed to be refused. It exists so CI can prove ox check rejects a metarel-endpoint violation, and so the diagnostic stays pinned. For the feature it guards, read machine_parts_v0.

The attachment metarel requires its mount position (position 1) to be fitting-sorted. This fixture fills that position with Axle, a part — a component would have to mount via a bare part, not via a fitting:

pub attachment mountedVia(host: Chassis, mount: Axle);

ox check must refuse this with OE0631 and exit non-zero:

$ ox check examples/machine_parts_bad --codes
OE0631
$ echo $?
1

The full diagnostic names the offending position and both metatypes:

× OE0631: in `<anonymous>::mountedVia`, position 1 of relation `mountedVia`
│ is `Axle` (a `part`), but its classifying metarel `attachment` declares
│ that position as `fitting` — an endpoint must be (a sub-metatype of) the
│ metarel's position metatype.

The examples corpus gate (oxc-driver/tests/examples_corpus_gate.rs) asserts this package is refused with an OE code, and a driver test (oxc-driver/tests/cli/scenario.rs) pins the refusal — if the endpoint check regressed and this fixture started building, CI would fail.

Source

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

//! `machine_parts_bad` — the REFUSAL half of the relation-constraint proof
//! (RFD 0031 D1, #311). An `attachment` relation whose mount position is filled
//! by a `part` (not a `fitting`) is refused at `ox check`/`ox build` with the
//! feature-named OE0631 — a component must mount via a fitting, not a bare
//! part. This package MUST NOT build; the corpus gate asserts the OE0631
//! refusal. Mirrors the well-formed `machine_parts_v0`.

pub metaxis granularity for metatype { atomic, composite };

pub metatype part = { granularity: atomic };
pub metatype fitting = { granularity: composite };

pub metarel attachment(host: part, mount: fitting);

pub part Chassis;
pub part Axle;

// WRONG: position 1 (mount) requires a `fitting`, but `Axle` is a `part`.
// Refused OE0631 — the §4.3 endpoint-metatype verification.
pub attachment mountedVia(host: Chassis, mount: Axle);

Refinement: iff (defined) vs where (primitive)

Area: Refinement & types Teaches: the two ways a refined concept gets its members — iff derives membership from a predicate, where asserts membership and treats the predicate as an enforced invariant. This is the most consequential distinction in Argon’s type layer. Prerequisites: concepts and <: specialization. Run: ox build examples/primitive_refinement && ox run-scenario examples/primitive_refinement

Two refined concepts sit over one Person population, and the keyword decides who is a member:

// Defined: anyone satisfying the predicate is automatically a member.
pub type Adult   <: Person iff   { self.age >= 18 };

// Primitive: membership is granted by an authority; the predicate is a
// necessary invariant on members, checked at the grant — never a classifier.
pub type Cleared <: Person where { self.clearance_score >= 50 };

• iff (Adult) — membership is derived. You never assert it; the reasoner classifies every Person whose age >= 18. Asserting it directly (insert iof(p, Adult)) is refused with OE0211.
• where (Cleared) — membership is asserted. A clearance is conferred by an act (grant_clearance → insert iof(p, Cleared)); the predicate only guards that act. A qualifying score is necessary, not sufficient.

The teaching contrast

Run it and compare the two extents. After the scenario seeds four people:

query clearance::adults:  4 row(s)   — Adult (iff):   everyone 18+, auto-classified
query clearance::cleared: 2 row(s)   — Cleared (where): only the two who were granted

The decisive case is dave: he has clearance_score = 70 (≥ 50) but was never granted, so he is not Cleared. Under iff he’d be classified automatically; under where membership is conferred, never inferred.

Honest caveats (what runs today)

• Granting clearance below the invariant is rejected with OE0668 (the where predicate is enforced at the grant). Inserting an iff membership directly is refused with OE0211.
• Refinement membership is evaluated by the reasoner at query time against each individual’s fields, so the extents above reflect the seeded age/score values.

This example is compiled and run in CI; its iff/where runtime behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so it 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

//! Primitive (`where`) vs defined (`iff`) refinement — RFD 0017.

mod clearance;

clearance.ar

//! Primitive (`where`) vs defined (`iff`) refinement — the description-logic
//! split between *asserted* and *derived* membership (RFD 0017).
//!
//! Two refined concepts sit over one `Person` population:
//!
//!   * `Adult` is **defined** (`iff`): any `Person` with `age >= 18` is
//!     *automatically* classified — the substrate derives membership. You
//!     cannot `insert iof(p, Adult)` (it would emit `OE0211`); you change the
//!     underlying `age` and the classification follows.
//!
//!   * `Cleared` is **primitive** (`where`): clearance is *granted* by an
//!     authority (asserted via `grant_clearance`). `clearance_score >= 50` is
//!     a **necessary invariant** on members — necessary, not sufficient.
//!     Having a qualifying score does NOT make you `Cleared`; someone must
//!     grant it. Granting below the threshold is rejected with `OE0668`.
//!
//! Expected runtime behavior (after demo.toml):
//!   * `Adult`   (iff):   {alice, bob, carol, dave}  — all are 18+, derived
//!   * `Cleared` (where): {alice, carol}             — only those *granted*
//!
//! The teaching contrast: `dave` has `clearance_score` 70 (>= 50) but was
//! never granted, so he is NOT `Cleared`. Under `iff` he would be classified
//! automatically; under `where` membership is conferred, never inferred.

pub type Person {
    mut age: Int,
    mut clearance_score: Int,
}

// ANCHOR: defined
// Defined: membership is derived from the predicate (auto-classified).
pub type Adult <: Person iff { self.age >= 18 };
// ANCHOR_END: defined
// ANCHOR: primitive
// Primitive: membership is asserted (granted); the predicate is a necessary
// invariant checked at the grant, never a query-time extent filter.
pub type Cleared <: Person where { self.clearance_score >= 50 };
// ANCHOR_END: primitive
pub mutate register(p: Person, age: Int, score: Int) {
    insert iof(p, Person);
    update p: Person set { age = age, clearance_score = score }
}

// ANCHOR: grant
pub mutate grant_clearance(p: Person) {
    insert iof(p, Cleared);
}
// ANCHOR_END: grant
pub query adults() -> Adult;
pub query cleared() -> Cleared;

Refinement with multi-field predicates

Area: Refinement & types Teaches: a refinement predicate is an ordinary boolean expression — it can read several fields and combine them with &&/||, comparisons, and string equality. Prerequisites: refinement (iff/where). Run: ox build examples/multi_field_refinement && ox run-scenario examples/multi_field_refinement

A single iff refinement classifies a Person by two fields at once:

pub type ActiveAdult <: Person iff {
    self.age >= 18 && self.status == "active"
};

ActiveAdult is the subset of people who are both adults and active. The predicate is evaluated per individual at query time against that individual’s declared fields — no membership is stored.

Running it

The scenario registers four people; only those satisfying both conjuncts are classified:

alice  age=25  status="active"    → ActiveAdult
bob    age=12  status="active"    → not (fails age >= 18)
carol  age=30  status="inactive"  → not (fails status == "active")
dave   age=45  status="active"    → ActiveAdult

so active_adults returns 2 rows (alice, dave) out of the 4 in all_people.

This example is compiled and run in CI; its runtime behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

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

//! Refinement with multi-field predicates and logical operators.

mod people;

people.ar

//! Refinement with multi-field predicates and logical operators.
//!
//! Demonstrates:
//!   * Refinement using `&&` and `||`
//!   * Multiple fields in a single predicate
//!   * Comparison operators (`>=`, `<`, `==`)
//!
//! Expected runtime behavior — the refinement predicate is evaluated
//! per individual against the individual's declared field values:
//!
//!   alice  age=25  status="active"   →  ✓ ActiveAdult
//!   bob    age=12  status="active"   →  ✗ (too young)
//!   carol  age=30  status="inactive" →  ✗ (wrong status)
//!   dave   age=45  status="active"   →  ✓ ActiveAdult

pub type Person {
    mut age: Int,
    mut status: String,
}

pub type ActiveAdult <: Person iff { self.age >= 18 && self.status == "active" };

pub mutate register(p: Person, age: Int, status: String) {
    insert iof(p, Person);
    update p: Person set { age = age, status = status }
}

pub query all_people() -> Person;
pub query active_adults() -> ActiveAdult;

A small employment ontology: refinement + a concept hierarchy

Area: Refinement & types Teaches: how iff refinements layer over a concept hierarchy (<:), with mutable fields populated by a mutate and read back through queries — a realistic, end-to-end shape. Prerequisites: refinement (iff/where). Run: ox build examples/refinement_employment && ox run-scenario examples/refinement_employment

pub type Person   { mut weekly_hours: Int, mut direct_reports: Int }
pub type Employee <: Person;
pub type FullTime <: Employee iff { self.weekly_hours  >= 35 };
pub type Manager  <: Employee iff { self.direct_reports >= 1 };

Employee specializes Person; FullTime and Manager are defined subsets of Employee — a person is classified into them automatically by their fields, and is reclassified when those fields change. A single hire mutation establishes a person and populates the fields:

pub mutate hire(p: Person, hours: Int, reports: Int) {
    insert iof(p, Person);
    insert iof(p, Employee);
    update p: Person set { weekly_hours = hours, direct_reports = reports }
}

Running it

The scenario hires several people; full_timers and managers come back as the filtered subsets of the all_persons extent — the iff predicates evaluated per individual at query time. Change someone’s weekly_hours below 35 and they leave FullTime on the next read; classification follows the data.

This example is compiled and run in CI; its refinement behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

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

//! Refinement types: a typical employment ontology.

mod employment;

employment.ar

//! Refinement types: a typical employment ontology.
//!
//! Demonstrates:
//!   * Concept hierarchy with `<:` subsumption
//!   * Refinement predicates on subtypes (`where { ... }`)
//!   * Mutable fields (`mut`)
//!   * Mutations that establish individuals + populate fields
//!   * Queries that read refined extents
//!
//! Expected runtime behavior:
//!   * `Person` extent: every individual created via `hire`
//!   * `Employee` extent: same (everyone hired is an Employee
//!     iof-asserted by the mutation)
//!   * `FullTime` extent: only employees with `weekly_hours >= 35`,
//!     computed by the refinement at query time
//!   * `Manager` extent: employees with `direct_reports >= 1`

// ANCHOR: hierarchy
pub type Person {
    mut weekly_hours: Int,
    mut direct_reports: Int,
}

pub type Employee <: Person;
// ANCHOR_END: hierarchy
// ANCHOR: fulltime
pub type FullTime <: Employee iff { self.weekly_hours >= 35 };
// ANCHOR_END: fulltime
pub type Manager <: Employee iff { self.direct_reports >= 1 };

pub mutate hire(p: Person, hours: Int, reports: Int) {
    insert iof(p, Person);
    insert iof(p, Employee);
    update p: Person set { weekly_hours = hours, direct_reports = reports }
}

pub query all_persons() -> Person;
pub query all_employees() -> Employee;
pub query full_timers() -> FullTime;
pub query managers() -> Manager;

Aggregates: count and exists in rule bodies

Area: Rules, aggregates & recursion Teaches: the aggregate forms exists { B } and count { B } cmp N inside a derive body — a subquery whose cardinality (or mere non-emptiness) drives the head. Aggregation is part of the rule language, not a separate report step. Prerequisites: concepts and <: specialization, and derive rule bodies (see first-class relations). Run: ox build examples/aggregate_count_v0 && ox derive examples/aggregate_count_v0 <predicate>

A data language that cannot count inside a rule pushes every cardinality question out to application code. Argon admits an aggregate atom as a subquery in the body: exists { B } is true when B has any solution, and count { B } yields the number of solutions so a comparison atom can filter on it.

What to read in company.ar

The corpus is three people, one of them a manager:

pub fact Person(alice);
pub fact Person(bob);
pub fact Person(carol);
pub fact Manager(alice);

exists { B } is a bare Boolean — the head fires iff the body has at least one solution:

pub derive any_person()  :- exists { Person(p) };
pub derive any_manager() :- exists { Manager(p) };

count { B } cmp N compares the cardinality. The aggregate binds the count to a synthesized variable; the comparison atom is the filter:

pub derive at_least_three_persons() :- count { Person(p) } >= 3;
pub derive thin_management()        :- count { Manager(p) } < 2;
pub derive huge_company()           :- count { Person(p) } >= 100;

These heads are 0-ary: each is a propositional flag that either fires or does not.

Running it

ox derive <predicate> prints the derived tuples. A 0-ary head that fires returns exactly one tuple — the empty tuple (); one that does not fire returns none:

derive(any_person):              1 tuple(s)   ()   — three Persons exist
derive(any_manager):             1 tuple(s)   ()   — alice is a Manager
derive(at_least_three_persons):  1 tuple(s)   ()   — count{Person} = 3, so >= 3 holds
derive(thin_management):         1 tuple(s)   ()   — count{Manager} = 1, so < 2 holds
derive(huge_company):            0 tuple(s)        — count{Person} = 3, so >= 100 fails

The decisive contrast is at_least_three_persons vs huge_company: the same count { Person(p) } subquery (which evaluates to 3) yields opposite verdicts because the threshold differs. The count is computed inside the rule, not handed to the rule.

Honest caveats (what runs today)

• v0 admits count (and bare exists) with the comparison operators ==, !=, <, <=, >, >=. The comprehension form (sum(expr for x in S where φ)), aggregators beyond count / count_distinct, and nested aggregates are γ follow-ons of RFD 0011.
• A 0-ary head models a proposition: one tuple means true, zero tuples means false. The single tuple is the empty tuple ().
• This package builds and runs under ox; unlike its sibling aggregate_membership_join it is not yet pinned by a corpus test, so it documents the surface rather than a regression.

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

//! Aggregates v0.1 — `count { atoms }` / `exists { atoms }`
//! demo. Phase γ closes one of the last open substrate audit
//! walls (RFD 0011); this example exercises the end-to-end
//! pipeline: surface syntax → SUBQUERY_EXPR CST → AtomIR::
//! Aggregate → CompiledAtom::Aggregate → executor.
//!
//! v0.1 scope:
//!
//!   * `count { B }` — cardinality of solutions to B (binds
//!     to a result var when followed by a comparison).
//!   * `exists { B }` — bare-form Boolean (truthy iff B has
//!     any solution).
//!   * Comparison forms: `count { B } cmp N` for `==`, `!=`,
//!     `<`, `<=`, `>`, `>=`.
//!
//! Deferred (RFD 0011 / γ follow-ons):
//!
//!   * Comprehension form `sum(expr for x in S where φ)`.
//!   * Truth4 interval semantics under OWA.
//!   * Aggregators other than `count` / `count_distinct`.
//!   * Nested aggregates (OE1311).

mod company;

company.ar

//! `company` — a small employment ontology with aggregate
//! queries over the workforce.

pub type Person;
pub type Manager <: Person;

pub fact Person(alice);
pub fact Person(bob);
pub fact Person(carol);
pub fact Manager(alice);

// ANCHOR: aggregates
/// Truthy iff there is at least one Person in the catalog.
/// Uses bare-`exists` form; the result is a Boolean atom.
pub derive any_person() :- exists { Person(p) };

/// Truthy iff there are at least three Persons.
/// Comparison form: the aggregate binds the cardinality to a
/// synthesized variable; the paired comparison atom filters.
pub derive at_least_three_persons() :- count { Person(p) } >= 3;
// ANCHOR_END: aggregates
/// Truthy iff there is at least one Manager.
pub derive any_manager() :- exists { Manager(p) };

/// Truthy iff the workforce has fewer than two Managers.
pub derive thin_management() :- count { Manager(p) } < 2;

/// Negative case: 100+ persons; should NOT fire on this corpus.
pub derive huge_company() :- count { Person(p) } >= 100;

Aggregates: counting inside a join

Area: Rules, aggregates & recursion Teaches: a count { B } whose body B is a join — a relation atom together with a type-membership atom (p in Person) — so the count ranges only over partners that satisfy both. The membership filter and the relation join are the same body; reordering them must not change the count. Prerequisites: aggregates (count / exists), and first-class relations. Run: ox build examples/aggregate_membership_join && ox derive examples/aggregate_membership_join <predicate>

count { Person(p) } counts a population; count { R(a, p) } counts edges. The interesting case is the conjunction — count the R-partners of a that are also Persons — because the membership atom and the relation atom must be solved together, and a bug that drops the membership test silently under-joins to zero.

What to read in root.ar

a0 relates via R to three things, but only two of them (p1, p2) are Persons — p3 is a plain Thing:

pub fact R(a0, p1);   // p1 in Person
pub fact R(a0, p2);   // p2 in Person
pub fact R(a0, p3);   // p3 in Thing, NOT Person

Relation-only count ranges over all three R-partners:

pub derive rel_count_is_three(a) :- Thing(a), count { R(a, p) } >= 3;

Count inside a join intersects the relation with type membership, so only the Person-typed partners count — two, not three:

pub derive member_count_at_least_two(a)   :- Thing(a), count { p in Person, R(a, p) } >= 2;
pub derive member_count_at_least_three(a) :- Thing(a), count { p in Person, R(a, p) } >= 3;

Order-independence — swapping the two body atoms is the same join, so the same count of 2:

pub derive member_count_reordered_two(a) :- Thing(a), count { R(a, p), p in Person } >= 2;

Running it

ox derive <predicate> prints the head’s tuples; each firing head returns the bound a (here the individual a0):

derive(rel_count_is_three):           1 tuple(s)   (a0)   — count{R(a,p)} = 3, so >= 3 holds
derive(member_count_at_least_two):    1 tuple(s)   (a0)   — count{p in Person, R(a,p)} = 2, so >= 2 holds
derive(member_count_at_least_three):  0 tuple(s)          — that count is 2, so >= 3 fails
derive(member_count_reordered_two):   1 tuple(s)   (a0)   — reordered body, same count of 2

The decisive contrast is rel_count_is_three vs member_count_at_least_three: both ask >= 3 of a count over a0’s R-partners, but the membership atom drops p3 (a non-Person), so the count falls from 3 to 2 and the second head does not fire. The member_count_reordered_two head proves the count is independent of atom order — both arrangements solve the same join.

Honest caveats (what runs today)

• The join inside the aggregate is the ordinary conjunctive body: p in Person is a type-membership atom and R(a, p) is a relation atom, solved together over the shared variable p.
• The count ranges over distinct solution bindings of the body, evaluated against the current state.

This example is compiled and run in CI; its join-count behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs::corpus_aggregate_membership_join_count), so the membership-inside-aggregate semantics can’t regress to the silent under-count it was written to guard against.

Source

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

//! #308 regression — aggregate body that mixes a TYPE-MEMBERSHIP atom
//! (`p in Person`) with a relation atom (`R(a, p)`).
//!
//! Found while writing the relation guide (executed on v0.2.0): the
//! membership-atom form inside an aggregate body silently evaluated to 0
//! for every binding, while the relation-only body was correct. Both
//! shapes must count the same pairs.
//!
//! Corpus seed: a0 relates (via R) to p1, p2, p3; only p1 and p2 are
//! Persons. So:
//!
//!   * `count { R(a, p) }`            over a0 = 3 (all R-partners).
//!   * `count { p in Person, R(a,p) }` over a0 = 2 (the Person-typed).
//!
//! Pinned as three boolean derives whose thresholds straddle 2 vs 3.

pub type Person;
pub type Thing;

pub fact Thing(a0);
pub fact Person(p1);
pub fact Person(p2);
pub fact Thing(p3);

pub rel R(a: Thing, p: Thing);

pub fact R(a0, p1);
pub fact R(a0, p2);
pub fact R(a0, p3);

/// Relation-only baseline: count is 3, so `>= 3` fires.
pub derive rel_count_is_three(a) :- Thing(a), count { R(a, p) } >= 3;

/// Membership+relation: count is 2 (only Person-typed partners), so
/// `>= 2` fires but `>= 3` must NOT (the #308 silent-0 bug made BOTH
/// fail — the derive would be empty).
pub derive member_count_at_least_two(a) :- Thing(a), count { p in Person, R(a, p) } >= 2;
pub derive member_count_at_least_three(a) :- Thing(a), count { p in Person, R(a, p) } >= 3;

/// Order-independence: relation atom first, membership second — same 2.
pub derive member_count_reordered_two(a) :- Thing(a), count { R(a, p), p in Person } >= 2;

Double-entry accounting: aggregates, balance, and an invariant

Area: Rules, aggregates & recursion Teaches: quantitative modeling that was inexpressible declaratively before RFD 0029 — a rule head that carries a computed value, two aggregates compared (the double-entry invariant as a single check), exact Decimal money end to end, and banker’s rounding. Plus in-language test blocks that assert against the derived plane. Prerequisites: first-class relations (the postings join through relations); check constraints. Run: ox build examples/double_entry_v0 && ox run-scenario examples/double_entry_v0 — and ox test examples/double_entry_v0

Double-entry is the canonical small accounting model: every transaction posts a debit and a matching credit, and the books balance when, within every journal entry, total debits equal total credits. It is also the exact wall RFD 0029 broke through — a rule head could not carry a computed value, and two aggregates could not be compared, so neither a per-account balance nor the balancing invariant could be written.

What to read in ledger.ar

A head carries a computed value. The per-account balance is Σ debits − Σ credits, grouped by the outer-bound acct; both aggregates bind to a variable, then bal is a derived value:

pub derive accountBalance(acct, bal) :- acct: Account,
    debits  = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    credits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "C"),
    bal     = debits - credits;

The invariant compares two aggregates — a balanced entry derives nothing, an unbalanced one fires the check:

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", /* … */ };

Money is exact, with banker’s rounding. A Decimal stays a Decimal — never via f64 — and round_half_even ties to even (the money default, avoiding the upward bias of half-away-from-zero):

pub derive accountTax(acct, tax) :- acct: Account,
    debits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    raw    = debits * 0.075,
    tax    = round_half_even(raw, 2);

Running it

ox run-scenario posts two balanced entries (Cash 100.50 / Revenue 100.50 and Cash 50.25 / Revenue 50.25), each leg pair committing atomically so the EntryNotBalanced Error guard is satisfied at every committed state:

scenario: applied 6 mutation(s) from examples/double_entry_v0/demo.toml

The interesting outputs are the derived values themselves, and the package asserts them directly with in-language test blocks. ox test runs each test "name" { … } against a fresh store and reports pass/fail:

PASS  a constructed account carries its name
PASS  postings carry exact decimal amounts and sides
PASS  an entry carries its memo and a second posting still reads back
PASS  accountBalance derives the posted amount per account
PASS  accountDebits derives the debit total per account
PASS  a balanced entry is derivable
PASS  an unbalanced entry is not derivable as balanced
PASS  an auto-discovered tests/ file runs its tests

8 passed, 0 failed, 0 errored, 0 inconclusive

The accountBalance test asserts accountBalance(cash) == 100.50 against the reasoner’s materialized extent — a deductive-plane assert, the point of testing a reasoning system. After the full demo harness the books read: accountBalance = {(cash, 150.75), (revenue, -150.75)}, and accountTax(cash) = round_half_even(11.30625, 2) = 11.31 (rounded to cents under round-half-even — here .30625 is past the half-cent, so it rounds up; the tie-to-even rule only changes the result on an exact x.xx5 boundary).

Honest caveats (what runs today)

• The ledger’s interesting predicates are pub derive, not pub query, so ox run-scenario --extent <name> (a concept extent lookup) does not enumerate them — the derived values are read through ox test asserts and the corpus pin instead.
• assert [not] derivable F(args) reads with world-honest three-valued semantics keyed on F’s world assumption. These concepts are closed-world (the package default), so absence is definite non-derivability — both derivable and not derivable are assertable here.
• The second tests/derived.ar file is auto-discovered by ox test but is not mod-wired into root.ar, so ox build never sees it (test-mode only).

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the exact decimal balances (150.75 / −150.75), the per-account totals, and the banker’s-rounded tax (11.31), so the aggregate semantics 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

//! Double-entry accounting — the quantitative-modeling wall, made a running
//! proof (RFD 0029).
//!
//! Before RFD 0029 this domain was *inexpressible declaratively*: a rule head
//! could not carry a computed value, and two aggregates could not be compared,
//! so neither the per-account balance `debits − credits` nor the ledger
//! invariant `sum(debits) == sum(credits)` could be written. This example is
//! the journey's exact wall — it exercises, end to end:
//!
//!   * **body-level binding** `x = expr` (derived values) — RFD 0029 §2.1;
//!   * **aggregates as bindable terms** with relation-atom sources and the
//!     outer-variable grouping (per-account `sum`) — §2.2–§2.4;
//!   * **comparing two aggregates** — the double-entry invariant — §2.3;
//!   * **exact decimal arithmetic** end to end — money never via f64;
//!   * **banker's rounding** (`round_half_even`) — §2.7;
//!   * **decimal demo-harness arguments** — RFD 0029 R-B10.
//!
//! All concepts use the neutral `pub type` introducer (`std::core`'s
//! no-commitment baseline) — no ontological commitment lives in the language.

mod ledger;
mod tests;

ledger.ar

//! The ledger model.
//!
//! An `Account` holds postings. A journal `Entry` groups the postings of one
//! transaction. Each `Posting` records an exact `Decimal` `amount`, a `side`
//! (`"D"` debit / `"C"` credit), the `Account` it hits, and the `Entry` it
//! belongs to (carried as relations so the aggregates can join them).
//!
//! Double-entry's one invariant: within every entry, total debits equal total
//! credits. With RFD 0029 that is a single `check` comparing two aggregates.

pub type Account {
    mut name: String,
}

pub type Entry {
    mut memo: String,
}

pub type Posting {
    mut amount: Decimal,
    mut side: String,
}

/// `postedTo(p, a)` — posting `p` hits account `a`.
pub rel postedTo(mut posting: Posting, mut account: Account);

/// `inEntry(p, e)` — posting `p` belongs to journal entry `e`.
pub rel inEntry(mut posting: Posting, mut entry: Entry);

// ── Derived values ────────────────────────────────────────────────
//
// Per-account balance = Σ debits − Σ credits, grouped by account (the
// grouping is the outer bound variable `acct`, the standard Datalog reading).
// Both aggregates are BOUND to variables, then the balance is a derived value
// — exactly the head-carries-a-computed-value shape RFD 0029 R-B2 unblocks.
pub derive accountDebits(acct, total) :-
    acct: Account,
    total = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D");

pub derive accountCredits(acct, total) :-
    acct: Account,
    total = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "C");

pub derive accountBalance(acct, bal) :-
    acct: Account,
    debits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    credits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "C"),
    bal = debits - credits;

// ── The double-entry invariant ────────────────────────────────────
//
// Within every entry, total debits == total credits. Two aggregates compared
// (RFD 0029 R-B3): a binding for each side, then `!=` flags the imbalance.
// A balanced entry derives nothing; an unbalanced one fires the check.
// ANCHOR: check
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 — total debits must equal total credits"
    };
// ANCHOR_END: check
// A balanced entry: the positive twin of the check, so the corpus test can
// read the *balanced* set directly (a `check` populates no IDB).
pub derive balancedEntry(e) :-
    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;

// ── Rounding ──────────────────────────────────────────────────────
//
// A 7.5%% sales-tax line on each account's debit total, rounded to cents with
// banker's rounding (the money default — round-half-even avoids the upward
// bias of half-away-from-zero). `round_half_even(x, 2)` is exact: a `Decimal`
// stays a `Decimal`, never via f64.
pub derive accountTax(acct, tax) :-
    acct: Account,
    debits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    raw = debits * 0.075,
    tax = round_half_even(raw, 2);

// ── Seeding ───────────────────────────────────────────────────────
//
// One mutation per posting keeps the demo harness a flat script. Amounts
// arrive as decimal harness arguments (RFD 0029 R-B10).
// ANCHOR: mutate
pub mutate openAccount(a: Account, name: String) {
    insert iof(a, Account);
    update a: Account set { name = name };
}
// ANCHOR_END: mutate
pub mutate openEntry(e: Entry, memo: String) {
    insert iof(e, Entry);
    update e: Entry set { memo = memo };
}

/// Post a SINGLE leg. Useful for the negative case: posting one leg without
/// its matching opposite leaves the entry unbalanced, which the
/// `EntryNotBalanced` Error guard rejects (double-entry is enforced, not
/// merely reported). The balanced demo uses `postPair` instead.
pub mutate post1(p: Posting, account: Account, entry: Entry, amount: Decimal, side: String) {
    insert iof(p, Posting);
    update p: Posting set { amount = amount };
    update p: Posting set { side = side };
    insert postedTo(p, account);
    insert inEntry(p, entry);
}

/// Post one balanced journal entry in a single atomic transaction: a debit
/// leg and a matching credit leg. Posting both legs together keeps the
/// `EntryNotBalanced` delta guard satisfied at every committed state — a
/// half-posted entry (debit without its credit) would gain a violation and
/// be rejected, so the two legs must commit together (double-entry IS atomic).
pub mutate postPair(
    debit: Posting,
    credit: Posting,
    debitAccount: Account,
    creditAccount: Account,
    entry: Entry,
    amount: Decimal
) {
    insert iof(debit, Posting);
    update debit: Posting set { amount = amount };
    update debit: Posting set { side = "D" };
    insert postedTo(debit, debitAccount);
    insert inEntry(debit, entry);

    insert iof(credit, Posting);
    update credit: Posting set { amount = amount };
    update credit: Posting set { side = "C" };
    insert postedTo(credit, creditAccount);
    insert inEntry(credit, entry);
}

tests/derived.ar

//! A second `tests/` file that is NOT `mod`-wired (no `mod derived;` in root).
//! `ox test` auto-discovers it; `ox build` never sees it (test-mode-only).
//!
//! A discovered top-level `tests/*.ar` references package items by their
//! package-absolute path (`pkg::`), since `super` from a plain `tests/` file
//! anchors at the `tests/` directory (no `ledger.ar` sibling there).

use pkg::ledger::{ Account };

test "an auto-discovered tests/ file runs its tests" {
    let a = insert Account { name: "Auto" };
    assert a.name == "Auto";
}

tests/mod.ar

//! In-language tests for the double-entry ledger (§16, the `test` atom).
//!
//! Each `test "name" { ... }` is a named imperative block run top-to-bottom
//! against a FRESH store by `ox test`. The body is the mutate-body statement
//! set (`let` / `insert` / mutation calls) plus the new `assert <bool-expr>;`
//! statement: true is a PASS, false a FAIL, an eval-error an ERROR, and
//! execution continues past a failed assert (unlike `require`, which aborts).
//!
//! An assert reads the DEDUCTIVE plane: a condition that names a derived
//! predicate / `pub query` (`accountBalance(cash)`) is evaluated against the
//! reasoner's materialized extent at the fixpoint of the current committed
//! state, after the body's writes (read-your-writes over committed+derived).

use super::ledger::{ Account, Entry, Posting };

// A constructed entity's scalar fields read back through field access — the
// simplest setup-then-assert flow (construct, then assert on `.field`).
test "a constructed account carries its name" {
    let cash = insert Account { name: "Cash" };
    assert cash.name == "Cash";
}

// Multiple asserts in one body; every one is recorded. Decimal amounts stay
// exact (never via f64), so the equality is precise.
test "postings carry exact decimal amounts and sides" {
    let debit = insert Posting { amount: 100.50, side: "D" };
    let credit = insert Posting { amount: 100.50, side: "C" };
    assert debit.amount == 100.50;
    assert credit.amount == 100.50;
    assert debit.side == "D";
    assert credit.side == "C";
}

// Setup interleaves with assertions: construct an entry, then assert on its
// field, then construct more — no separate fixture block needed.
test "an entry carries its memo and a second posting still reads back" {
    let e = insert Entry { memo: "sale 1" };
    assert e.memo == "sale 1";
    let p = insert Posting { amount: 50.25, side: "D" };
    assert p.amount == 50.25;
}

// The deductive-plane assert (the point of testing a reasoning system): after
// posting one balanced entry through the `postPair` mutation, the per-account
// balance derive `accountBalance(acct, bal)` is materialized and the keyed
// read `accountBalance(cash)` yields the computed value. The debit side nets
// +amount, the credit side -amount — exactly the §19 `x.method() == v` shape,
// evaluated against the reasoner's output, not a stored scalar.
test "accountBalance derives the posted amount per account" {
    let cash = insert Account { name: "Cash" };
    let rev = insert Account { name: "Revenue" };
    let e = insert Entry { memo: "sale 1" };
    postPair(cash, rev, cash, rev, e, 100.50);
    assert accountBalance(cash) == 100.50;
    assert accountBalance(rev) == - 100.50;
}

// A second derived aggregate read: the per-account debit total.
test "accountDebits derives the debit total per account" {
    let cash = insert Account { name: "Cash" };
    let rev = insert Account { name: "Revenue" };
    let e = insert Entry { memo: "sale 1" };
    postPair(cash, rev, cash, rev, e, 50.25);
    assert accountDebits(cash) == 50.25;
    assert accountCredits(rev) == 50.25;
}

// ── Derivability assertions (§17.14 / §7.9) ────────────────────────
//
// The membership / non-derivability half of the test atom's vocabulary.
// `assert [not] derivable F(args)` tests whether a matching row is in F's
// materialized extent, with world-honest three-valued semantics keyed on F's
// world assumption (§6.9). The ledger concepts are closed-world (the package
// default), so absence reads as definite non-derivability — both directions
// are assertable here.
// A balanced entry: posting a matching debit/credit pair makes
// `balancedEntry(e)` derivable (a value-less membership derive — the clean
// case the v1 value-read assert could not express). PRESENT ⇒ `derivable`
// passes.
test "a balanced entry is derivable" {
    let cash = insert Account { name: "Cash" };
    let rev = insert Account { name: "Revenue" };
    let e = insert Entry { memo: "balanced sale" };
    postPair(cash, rev, cash, rev, e, 100.00);
    assert derivable balancedEntry(e);
}

// An entry with a single un-matched leg is NOT balanced, so `balancedEntry`
// does not derive it. Under the closed-world default, absence is definite
// non-derivability ⇒ `not derivable` passes (the non-derivability assertion
// the v1 assert could not make — a missing row errored).
test "an unbalanced entry is not derivable as balanced" {
    let cash = insert Account { name: "Cash" };
    let p = insert Posting { amount: 0.00, side: "D" };
    let e = insert Entry { memo: "half-posted" };
    post1(p, cash, e, 75.00, "D");
    assert not derivable balancedEntry(e);
}

Robot plan execution: three reasoning regimes on one model

Area: Rules, aggregates & recursion Teaches: a planning/robotics domain over a self-defined upper ontology, exercising three workhorse reasoning regimes on one package — a true bounded forall, a mutually-recursive least fixpoint, and arbitration by recursion through negation under well-founded semantics — plus a fourth regime: federating a precondition across two disagreeing sensor standpoints, where the conflict surfaces as the four-valued both. Also: an upper ontology is an ordinary module, not a language built-in. Prerequisites: first-class relations; derive rule bodies; negation-as-failure. For the sensor federation: federation disagreement. Run: ox build examples/robot_plan_execution && ox query examples/robot_plan_execution

A mobile robot executes a plan: charge, navigate, scan, pick up. Two modules split the model deliberately — upper is a minimal upper ontology defined in this package (Object, Event, Capability, a derived involves), and robot specializes it (Agent <: Object, Action <: Event, Skill <: Capability) and builds the planner. Argon is ontology-neutral: a published foundational ontology could be imported in upper’s place without touching the domain.

What to read in robot.ar

A true universal — the bounded forall. An action is ready-at-start when every one of its preconditions holds initially. This lowers to a count-equality, not the existential “some precondition holds” (an action with no preconditions is vacuously ready):

pub derive readyAtStart(a: Action) :-
    Action(a),
    forall f: Fluent where pre(a, f), holds(f);

A mutually-recursive least fixpoint — forward reachability. A fluent is reachable if it holds initially or is added by an applicable action; an action is applicable when none of its preconditions is unreachable. The universal “all preconditions reachable” is the standard double-negation encoding, because a forall may not sit inside a recursive cycle on this engine — the alternating fixpoint converges it:

pub derive unreached(a: Action) :- pre(a, f), not reachable(f);
pub derive applicable(a: Action) :- Action(a), not unreached(a);
pub derive reachable(f: Fluent) :- adds(a, f), applicable(a);

Arbitration — recursion through negation. Two conflicting actions cannot both run. scheduled recurses through its own negation via challenged, so {scheduled, challenged} form one NAF-cyclic SCC the engine evaluates by well-founded semantics directly (strict stratification would reject this):

pub derive challenged(a: Action) :- conflicts(a, b), scheduled(b);
pub derive scheduled(a: Action)  :- applicable(a), not challenged(a);

Federating a precondition across disagreeing sensors — the four-valued both. The planner reads the initial state from a single trusted holds(f) extent. Real robots read the world from sensors, and sensors disagree. sensors.ar models two — lidar and camera — as standpoints over the planner’s own holds relation. A federated query joins them by the four-valued information-join (is/not/can/both); a pub fact asserts a fluent in that sensor’s view, a pub not_fact positively refutes it (RFD 0010 strong negation, not silence):

use robot::{ Fluent, holds };

pub standpoint lidar;
pub standpoint camera;

pub standpoint lidar  { pub fact holds(clearPath); pub not_fact holds(objectVisible); }
pub standpoint camera { pub not_fact holds(clearPath); pub fact holds(nearObject); }

pub query sensedState() -> holds across [lidar, camera];

The decisive row is clearPath → Both: lidar asserts the path is clear, camera refutes it, and the information-join carries both polarities rather than picking a winner or crashing. clearPath is the precondition for navigate, so the federation tells the planner — as a value — that its sensors are in conflict about whether it may proceed.

Running it

ox query enumerates every declared pub query. The plan chain closes over all seven fluents and all seven actions are applicable; the arbitration is the payoff:

query robot::reachableFluents:   7 row(s)
query robot::applicableActions:  7 row(s)
query robot::readyActions:       1 row(s)    — only `charge` (pre {atHome}, true at start)
query robot::scheduledActions:   4 row(s)    — {charge, navigate, scan, pickup}
query robot::challengedActions:  1 row(s)    — {pushObject}
query sensors::sensedState:      4 row(s)    — clearPath → Both, nearObject → Is, objectVisible → Not
query upper::involvement:        1 row(s)    — (pickup, rob): pickup exercises a capability rob bears

Two conflicts drive the arbitration. The asymmetric one resolves to a definite winner: pushObject is challenged by the higher-priority pickup, pickup has no rival so it is never challenged, so pickup is scheduled and pushObject is not. The symmetric one (wipeLeft ↔ wipeRight, no tiebreak) is well-founded-undefined: the engine materializes only definitely-true atoms, so neither appears in scheduled and neither appears in challenged — that absence-of-both is the deadlock’s observable signature.

Honest caveats (what runs today)

• ox query renders rows as opaque individual ids; the row counts and the named membership above are what the corpus test pins (it resolves the ids back to names).
• Arbitration is kept as a single SCC on purpose. Splitting it into a lower blocked stratum and a higher scheduled :- not blocked would ask the engine to read a well-founded relation under a higher negation — it materializes the WFS stratum two-valued at that boundary, so a genuinely-undefined atom would read as false downstream and over-assert. The single-SCC form is the sound one.

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins scheduled = {charge, navigate, scan, pickup}, challenged = {pushObject}, the absence of both symmetric-deadlock actions, and the sensor federation’s per-fluent Truth4 verdicts (clearPath → Both, nearObject → Is, objectVisible → Not), so the well-founded arbitration and the four-valued information-join 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

//! # Robot plan execution — WFS arbitration over a self-defined upper ontology
//!
//! A two-module package modeling a mobile robot that executes a plan. The split
//! is deliberate and load-bearing:
//!
//!   * `upper` — a minimal upper ontology defined *in this package* (`Object`,
//!     `Event`, `Capability`, `bears`, `exercises`, derived `involves`). Argon
//!     is ontology-neutral; the foundational categories are an ordinary module,
//!     not a language built-in — a published foundational ontology could be
//!     imported in its place without touching the domain.
//!
//!   * `robot` — the domain. It `use`s `upper`, specialises its categories
//!     (`Agent <: Object`, `Action <: Event`, `Skill <: Capability`), and
//!     builds a plan executor with three reasoning regimes: a bounded universal
//!     (`applicable`), a positive least fixpoint (`reachable`), and arbitration
//!     by **recursion through negation** (`scheduled` recurses through its own
//!     negation via `challenged` — one well-founded SCC, queried directly).
//!
//! See `robot.ar` for the scenario and the precise modeling of the asymmetric
//! (resolving) and symmetric (deadlock) conflicts.

mod upper;
mod robot;
mod sensors;

robot.ar

//! # `robot` — plan execution for a mobile robot, over the `upper` vocabulary
//!
//! This module `use`s the package's own upper ontology and *specialises* it for
//! a robotics domain: an `Agent` is an `Object`, an `Action` is an `Event`, a
//! `Skill` is a `Capability`. The cross-module dependency is real — these
//! subkind declarations resolve their supertypes in the sibling `upper` module,
//! and the two files elaborate into one artifact.
//!
//! On top of the imported vocabulary it builds a small **plan executor** that
//! exhibits three reasoning regimes, each a workhorse of knowledge
//! representation:
//!
//!   1. **The bounded universal `forall`** (`readyAtStart`). An action is
//!      ready-at-start when **every** one of its preconditions holds in the
//!      initial state. This is the *true* universal — lowered to a
//!      count-equality, never the existential "some precondition holds".
//!
//!   2. **A least fixpoint** (`reachable` / `applicable`). A fluent is reachable
//!      if it holds initially, or if some applicable action adds it; an action
//!      is applicable when none of its preconditions is unreachable. The two
//!      relations are mutually recursive — the executor walks the plan forward
//!      to its closure (charge → navigate → scan → pick up). The universal
//!      "all preconditions reachable" is expressed by *double negation*
//!      (`applicable` = not (`unreached`)), the standard Datalog encoding of a
//!      universal that recurses; the alternating-fixpoint engine converges it.
//!
//!   3. **Recursion through negation** (`scheduled` / `challenged`). Two actions
//!      that conflict cannot both run. `scheduled(a)` holds when `a` is
//!      applicable and **not** challenged; `challenged(a)` holds when a
//!      conflicting `b` is itself scheduled. So `scheduled` recurses through its
//!      own negation *via* `challenged` — exactly the win–move game on the
//!      conflict graph — and `{scheduled, challenged}` form ONE NAF-cyclic SCC
//!      the engine evaluates by **well-founded semantics** (strict
//!      stratification rejects a rule that recurs through its own negation).
//!      An asymmetric (prioritised) conflict resolves to a definite winner; a
//!      symmetric conflict is a genuine standoff whose well-founded value is
//!      *undefined* — observable as the **absence of both** actions from the
//!      `scheduled` extent (and from `challenged`).

use upper::{ kind, Object, Event, Capability };

// ── Domain specialisation of the upper-ontology categories ──────────────────
/// A robot — an object that bears skills and performs actions.
pub kind Agent <: Object;

/// A plan step — an event the agent can perform.
pub kind Action <: Event;

/// A capability the agent bears (grasping, locomotion, …).
pub kind Skill <: Capability;

/// A propositional state of the world the planner tracks (battery charged,
/// path clear, object visible, …). Fluents are the planner's currency.
pub kind Fluent {}

// ── Planner relations (asserted as the scenario ABox below) ─────────────────
/// `pre(a, f)` — action `a` requires fluent `f` to hold before it can run.
pub rel pre(a: Action, f: Fluent);

/// `adds(a, f)` — running action `a` makes fluent `f` hold (its effect).
pub rel adds(a: Action, f: Fluent);

/// `holds(f)` — fluent `f` is true in the initial state (a base fact).
pub rel holds(mut f: Fluent);

/// `conflicts(a, b)` — action `a` is challenged by action `b`: they cannot both
/// be scheduled. Read directionally for the arbitration game below.
pub rel conflicts(a: Action, b: Action);

// ── 1. The true universal: readiness in the initial state ───────────────────
/// `readyAtStart(a)` — **every** precondition of `a` holds in the initial
/// state. The `forall` ranges over the action's preconditions; an action with
/// a precondition that does not initially hold is excluded. This is a genuine
/// universal — lowered to `#{f : pre(a,f), holds(f)} == #{f : pre(a,f)}` — not
/// the existential "some precondition holds". (An action with no preconditions
/// is vacuously ready.)
pub derive readyAtStart(a: Action) :- Action(a), forall f: Fluent where pre(a, f), holds(f);

// ── 2. The least fixpoint: forward reachability ─────────────────────────────
//
// `applicable` quantifies universally over preconditions ("none unreachable"),
// `reachable` feeds back into `applicable` — a mutually recursive fixpoint.
// The universal is written as double negation because a `forall`/aggregate may
// not appear *inside* a recursive cycle on this engine (it is evaluated as a
// strict, lower-stratum dependency); the `not unreached` form is the standard
// Datalog encoding of the recursive universal, and the alternating fixpoint
// converges it.
/// `unreached(a)` — `a` has at least one precondition that is not (yet)
/// reachable. The existential witness of a *failed* universal.
pub derive unreached(a: Action) :- pre(a, f), not reachable(f);

/// `applicable(a)` — `a` is applicable when none of its preconditions is
/// unreachable, i.e. *all* are reachable (the universal, by double negation).
pub derive applicable(a: Action) :- Action(a), not unreached(a);

/// A fluent that holds initially is reachable (base case).
pub derive reachable(f: Fluent) :- holds(f);

/// A fluent added by an applicable action is reachable (recursive case). Mutual
/// recursion with `applicable` drives the plan forward to its closure.
pub derive reachable(f: Fluent) :- adds(a, f), applicable(a);

// ── 3. Arbitration: recursion through negation (well-founded semantics) ─────
//
// Arbitration is ONE recursion-through-negation SCC, queried directly. We do
// NOT split it into a lower `blocked` stratum and a higher `scheduled :- not
// blocked` stratum: that split asks the engine to read a well-founded relation
// under a *higher* negation, and the engine materializes the WFS stratum
// 2-valued at the boundary, so a genuinely-undefined atom would read as false
// downstream and over-assert. Instead `scheduled` recurses through its own
// negation **via** `challenged`, so `{scheduled, challenged}` form a single
// NAF-cyclic SCC the engine evaluates by well-founded semantics directly.
/// `challenged(a)` — `a` is challenged when some action `b` that conflicts with
/// it is itself `scheduled`. This is one half of the win–move game on the
/// conflict graph; the other half is `scheduled`, which negates `challenged`.
// ANCHOR: wfs
pub derive challenged(a: Action) :- conflicts(a, b), scheduled(b);

/// `scheduled(a)` — `a` runs if it is applicable and **not** challenged.
///
/// `scheduled` recurses through its own negation via `challenged`
/// (`scheduled` → `not challenged` → `scheduled`), so `{scheduled, challenged}`
/// is a single SCC the engine evaluates by well-founded semantics — no higher
/// stratum negates a WFS relation, so the model is sound:
///
///   * An ASYMMETRIC (prioritised) conflict resolves to a **definite winner**:
///     the uncontested action is scheduled, and its rival is challenged and so
///     absent from `scheduled`.
///   * A SYMMETRIC conflict is well-founded-**undefined**: the engine
///     materializes only definitely-true atoms, so neither side is scheduled
///     and neither side is challenged. The deadlock's observable signature is
///     the **absence of both actions from `scheduled`** (and from `challenged`).
pub derive scheduled(a: Action) :- applicable(a), not challenged(a);
// ANCHOR_END: wfs
// ── Scenario ABox ───────────────────────────────────────────────────────────
//
// The fluents:
//   atHome, clearPath        — true initially (holds)
//   haveBattery              — added by `charge`
//   nearObject               — added by `navigate`
//   objectVisible            — added by `scan`
//   holding                  — added by `pickup` / `pushObject`
//   wiped                    — added by either wipe action
//
// The plan chain (each action's preconditions are the previous effects):
//   charge   : pre {atHome}                     adds {haveBattery}
//   navigate : pre {haveBattery, clearPath}     adds {nearObject}
//   scan     : pre {nearObject}                 adds {objectVisible}
//   pickup   : pre {objectVisible, haveBattery} adds {holding}
//
// So reachability closes over all seven fluents (atHome, clearPath,
// haveBattery, nearObject, objectVisible, holding, wiped) and all seven
// actions are applicable.
//
// Two conflicts exercise the well-founded arbitration:
//
//   ASYMMETRIC (resolves): `pickup` and `pushObject` contend for the manipulator.
//   `pushObject` is the lower-priority fallback, so it is *challenged by*
//   `pickup`:  conflicts(pushObject, pickup).  `pickup` has no conflicting
//   rival, so it is never challenged ⇒ pickup is scheduled; hence pushObject is
//   challenged (its rival pickup is scheduled) ⇒ pushObject is NOT scheduled.
//   (pushObject is itself applicable — pre {nearObject} — so arbitration, not
//   inapplicability, is what stops it.) A definite winner: pickup.
//
//   SYMMETRIC (deadlock): `wipeLeft` and `wipeRight` mutually conflict with no
//   tiebreak:  conflicts(wipeLeft, wipeRight)  and  conflicts(wipeRight, wipeLeft).
//   Each is applicable (pre {haveBattery}). Their scheduled/challenged-values
//   form a 2-cycle through negation, so both are well-founded-*undefined*:
//   neither appears in `scheduled`, and neither appears in `challenged`.
pub fact Fluent(atHome)
pub fact Fluent(clearPath)
pub fact Fluent(haveBattery)
pub fact Fluent(nearObject)
pub fact Fluent(objectVisible)
pub fact Fluent(holding)
pub fact Fluent(wiped)

pub fact Action(charge)
pub fact Action(navigate)
pub fact Action(scan)
pub fact Action(pickup)
pub fact Action(pushObject)
pub fact Action(wipeLeft)
pub fact Action(wipeRight)

// Initial state.
pub fact holds(atHome)
pub fact holds(clearPath)

// Preconditions.
pub fact pre(charge, atHome)
pub fact pre(navigate, haveBattery)
pub fact pre(navigate, clearPath)
pub fact pre(scan, nearObject)
pub fact pre(pickup, objectVisible)
pub fact pre(pickup, haveBattery)
pub fact pre(pushObject, nearObject)
pub fact pre(wipeLeft, haveBattery)
pub fact pre(wipeRight, haveBattery)

// Effects.
pub fact adds(charge, haveBattery)
pub fact adds(navigate, nearObject)
pub fact adds(scan, objectVisible)
pub fact adds(pickup, holding)
pub fact adds(pushObject, holding)
pub fact adds(wipeLeft, wiped)
pub fact adds(wipeRight, wiped)

// Asymmetric conflict: pushObject is challenged by the higher-priority pickup.
pub fact conflicts(pushObject, pickup)

// Symmetric conflict: wipeLeft and wipeRight deadlock.
pub fact conflicts(wipeLeft, wipeRight)
pub fact conflicts(wipeRight, wipeLeft)

// ── Queries ─────────────────────────────────────────────────────────────────
/// Actions all of whose preconditions hold in the initial state (true forall).
pub query readyActions() -> readyAtStart;

/// Fluents reachable from the initial state by the applicable plan.
pub query reachableFluents() -> reachable;

/// Actions all of whose preconditions are reachable.
pub query applicableActions() -> applicable;

/// Actions challenged by a scheduled rival (well-founded; the win–move dual of
/// `scheduled`).
pub query challengedActions() -> challenged;

/// Actions that actually run: applicable and unchallenged.
pub query scheduledActions() -> scheduled;

upper.ar

//! # `upper` — a small upper ontology, defined in this package
//!
//! Argon is ontology-neutral: the foundational categories a domain reasons
//! over come from an ordinary module, not from the language. This package
//! defines its own minimal upper ontology — three categories and two
//! relations are enough for the planner. A published foundational ontology
//! (UFO, BFO) could be imported in its place and the domain module would not
//! change.
//!
//! The one derived relation is the point of the module: an event *involves*
//! an object exactly when the event exercises a capability the object bears.
//! Involvement is never asserted directly; it is derived.

// Vocabulary (§3.4, §5.2): a concept introducer must resolve to a visible
// `pub metatype` that is IN SCOPE — declared locally or imported (RFD 0038
// D4; the baseline `type`/`rel` come from this package's
// `[package].prelude = ["std::core::{type, rel}"]`). This upper ontology
// declares the one classifier it commits to — `kind`, a rigid sortal — and
// the domain module (`robot`) imports it (`use upper::{kind, …}`) to
// classify its own `pub kind` declarations.

/// Kind: a rigid sortal classifier supplying an identity principle.
pub metatype kind = { };

/// A thing that persists through time and bears capabilities.
pub kind Object {}

/// An occurrence.
pub kind Event {}

/// A power an object bears, exercised by events.
pub kind Capability {}

/// `bears(o, c)` — object `o` bears capability `c`.
pub rel bears(o: Object, c: Capability);

/// `exercises(v, c)` — event `v` exercises capability `c`.
pub rel exercises(v: Event, c: Capability);

/// `involves(v, o)` — event `v` involves object `o`: it exercises a
/// capability `o` bears. Derived, never asserted.
pub derive involves(v: Event, o: Object) :- bears(o, c), exercises(v, c);

// A minimal self-contained instance so the derived relation is observable
// on its own: `rob` bears `grasping`; the `pickup` event exercises it.
pub fact Object(rob)
pub fact Capability(grasping)
pub fact Event(pickup)
pub fact bears(rob, grasping)
pub fact exercises(pickup, grasping)

/// The involvement extent — `(event, object)` pairs.
pub query involvement() -> involves;

sensors.ar

//! # `sensors` — federating a precondition across two disagreeing sensors
//!
//! The planner in `robot.ar` reads the initial state from a single, trusted
//! `holds(f)` extent. Real robots don't have one: the world is reported by
//! *sensors*, and sensors disagree. A LiDAR sweep may report the path clear
//! while the camera, seeing glare, reports it blocked. A planner that picks one
//! sensor and ignores the other is silently unsound; one that crashes on the
//! conflict is useless. Argon does neither — it federates the two readings and
//! reports the disagreement **as a value**.
//!
//! Each sensor is a `standpoint`: its own source of ground truth over the SAME
//! `holds` relation the planner reads. A sensor `pub fact holds(f)` asserts the
//! fluent; a `pub not_fact holds(f)` is a positive refutation (RFD 0010 strong
//! negation), not mere silence. A federated query joins the sensors by the
//! four-valued information-join over the Belnap-Dunn bilattice (`Truth4`):
//!
//!   * `is`   — asserted by some sensor, refuted by none
//!   * `not`  — refuted by some sensor, asserted by none
//!   * `can`  — neither (a fluent no sensor mentions)
//!   * `both` — asserted by one sensor AND refuted by another: the conflict,
//!              carried rather than discarded
//!
//! The scenario, over the planner's own fluents:
//!
//!   clearPath  — lidar asserts `holds`, camera refutes it      → Both
//!   nearObject — only the camera reports it (lidar silent)      → Is
//!   objectVisible — only the lidar refutes it (camera silent)   → Not
//!   atHome     — asserted only in the base both sensors inherit → Is
//!
//! `both` is the load-bearing row: `clearPath` is the precondition for
//! `navigate`, and the federation tells the planner — without crashing and
//! without silently picking a winner — that its sensors are in conflict about
//! whether the path is clear.
//!
//! Soundness: `Argon.Standpoint.Federation.federate_eq_both_iff` (Lean, proven)
//! — the per-row `Truth4` the federated dispatcher computes is exactly the AFT
//! info-join across the contributing standpoints.

use robot::{ Fluent, holds };

// Each sensor is a source of ground truth — a standpoint over `holds`.
pub standpoint lidar;
pub standpoint camera;

pub standpoint lidar {
    // LiDAR sweeps the floor: it reads the path as clear.
    pub fact holds(clearPath);
    // It cannot see the object yet (occlusion) — a positive refutation.
    pub not_fact holds(objectVisible);
}

pub standpoint camera {
    // The camera, against glare, reads the path as blocked — refuting `clearPath`.
    pub not_fact holds(clearPath);
    // It does see the object in frame.
    pub fact holds(nearObject);
}

// Federate the two sensors' readings of `holds`. Each standpoint also inherits
// the base `holds` extent (robot.ar asserts `holds(clearPath)` and
// `holds(atHome)`) as a global section, so the query returns one row per fluent
// any source speaks to, each tagged with the joined four-valued status.
// `clearPath` is asserted by the base and by `lidar` and refuted by `camera`, so
// the information-join carries both polarities: `Both` — the camera's refutation
// surfaces even against the base assertion. `atHome`, asserted only in the base
// that both sensors inherit, comes back `Is`.
pub query sensedState() -> holds across [lidar, camera];

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 };
}

Legal norms: strict vs default vs defeater

Area: Defeasible reasoning Teaches: the three rule strengths of defeasible reasoning on one head — a strict (unattackable) clause, an overridable #[default] clause, and a #[defeats] directive that attacks the default per-tuple. RFD 0028’s “honest heads”: no rule spells the conclusion it denies. Prerequisites: refinement (iff/where), and derive rule bodies (see first-class relations). Run: ox build examples/legal_norms_can_vote && ox run-scenario examples/legal_norms_can_vote

Who can vote? Three norms speak to can_vote, and they conflict. A pre-defeasibility data language forces you to fold the exceptions into the rule body by hand (Adult(p), not Felon(p), not …), which becomes unmaintainable as exceptions accumulate. Argon keeps each norm a separate honest rule and resolves the conflict with directives.

What to read in norms.ar

The strict clause is unmarked — it is unattackable. Special-class members vote regardless of any disenfranchisement edge:

pub derive can_vote(p) :- SpecialClass(p);

The default clause is overridable. Adults vote by default — #[default] marks the clause as defeasible, and #[label(adult)] gives it an identity an attacker can name:

#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

The exception is its own honest rule, and the attack is a directive. disenfranchised reads true on its own terms — it does not spell not can_vote. The attack lives in #[defeats(can_vote(p))], a meta-level statement about rules that resolves per-tuple against the bound p:

#[defeats(can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);

So for a given person, disenfranchised defeats the default can_vote clause — but the strict clause is not a default, so the attack cannot touch it.

Running it

The scenario registers four people, one per case:

alice  age=25  felon=false  special=false  → can_vote   (default holds, unattacked)
bob    age=12  felon=false  special=false  → not        (not an Adult — no clause fires)
carol  age=30  felon=true   special=false  → not        (default defeated by disenfranchised)
dave   age=45  felon=true   special=true   → can_vote   (strict clause; the attack can't reach it)

so voters returns 2 rows — alice (default survives) and dave (strict overrides the very defeat that blocks carol). The decisive contrast is carol vs dave: both are felons, both are disenfranchised, but dave’s vote comes from the strict clause that #[defeats] cannot attack.

This example is compiled and run in CI; its can_vote extent under the strict/default/defeater interplay is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the resolution 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

//! Defeasibility (Governatori-style strict / defeasible / defeater).

mod norms;

norms.ar

//! Defeasibility, RFD 0028 honest-head form.
//!
//! The legal-norms use case: special-class members can vote (strict);
//! adults can vote by default; felons are disenfranchised, and that
//! disenfranchisement defeats the adult default.
//!
//! Every rule reads true (RFD 0028 D1 — "honest heads"): no rule
//! spells the head it denies. The exception (`disenfranchised`) lives
//! under its own name, and the attack is a directive (`#[defeats]`),
//! never the rule's syntax.
//!
//! Demonstrates:
//!   * `#[default]` — an overridable clause (the adult default)
//!   * `#[label(adult)]` — the clause's identity
//!   * `#[defeats(can_vote(p))]` — the attack, a meta-level statement
//!     about rules, resolving per-tuple against the bound `p`
//!   * the strict clause (unmarked) is unattackable — special-class
//!     members vote regardless of the disenfranchisement edge
//!
//! Expected runtime behavior:
//!   alice  age=25, felon=false, special=false  → can_vote (default holds)
//!   bob    age=12, felon=false, special=false  → not can_vote (not adult)
//!   carol  age=30, felon=true,  special=false  → not can_vote (defeated)
//!   dave   age=45, felon=true,  special=true   → can_vote (strict; unattackable)

pub type Person {
    mut age: Int,
    mut felon: Bool,
    mut special: Bool,
}

pub type Adult <: Person iff { self.age >= 18 };

pub type Felon <: Person iff { self.felon == true };

pub type SpecialClass <: Person iff { self.special == true };

// strict = unmarked: special-class members vote, period (unattackable)
pub derive can_vote(p) :- SpecialClass(p);

// the overridable default
#[default]
#[label (adult)]
pub derive can_vote(p) :- Adult(p);

// the exception: an honest head, and the attack as a directive
#[defeats (can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);

pub mutate register(p: Person, age: Int, felon: Bool, special: Bool) {
    insert iof(p, Person);
    update p: Person set { age = age, felon = felon, special = special }
}

pub query voters() -> can_vote;

Lex specialis: the specific rule defeats the general

Area: Defeasible reasoning Teaches: resolving a same-strength norm conflict with #[defeats] — lex specialis, where a specific rule beats the general one it names, per-tuple, by an explicit checked edge rather than a pair of magic priority integers. Prerequisites: strict vs default vs defeater. Run: ox build examples/legal_priority_v0 && ox run-scenario examples/legal_priority_v0

Two norms conclude about the same head at the same strength: imported goods owe import duty (general); medical imports are exempt (specific). Without a superiority mechanism this conflict is unresolvable — both fire on a medical import and you get a contradiction. Lex specialis is the legal rule that the specific norm wins; Argon expresses it as one rule defeating another’s labeled clause.

What to read in statute.ar

The general norm is an overridable, labeled default. #[label(general)] is the handle a more specific rule will name:

#[default]
#[label(general)]
pub derive must_pay_duty(g) :- Imported(g);

The specific norm names the general clause and defeats it. The #[defeats] target is qualified by the label — must_pay_duty.general(g) — and resolves per-tuple against the bound g. It defeats the general duty clause for exactly the goods exempt derives, and no others:

#[defeats(must_pay_duty.general(g))]
pub derive exempt(g) :- MedicalGood(g);

This is the whole lex-specialis idea in two lines: the more specific rule (medical imports) defeats the more general one (imported goods), tuple by tuple. A non-medical import is untouched by the defeat and keeps owing duty.

Running it

The scenario declares four goods:

steel    imported=true   medical=false  → owes duty   (general default, unattacked)
insulin  imported=true   medical=true   → exempt      (specific defeats general)
gauze    imported=true   medical=true   → exempt      (specific defeats general)
widget   imported=false  medical=false  → no clause fires

so dutiable (the warranted must_pay_duty) returns 1 row — steel — while exemptions returns 2 rows, insulin and gauze. The two medical imports are dutiable under the general norm and exempt under the specific one; lex specialis subtracts them from the duty extent, leaving the single non-medical import.

This example is compiled and run in CI; the post-defeat must_pay_duty and exempt extents are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the lex-specialis resolution can’t drift.

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

//! Lex specialis via `#[defeats]` (RFD 0028, register R-B8).
//!
//! The legal-domain unblock: same-strength norm conflicts
//! (lex specialis / lex posterior) were unresolvable without a
//! superiority mechanism. RFD 0028 makes the specific rule defeating
//! the general clause's label an explicit, resolution-checked edge —
//! not a pair of magic priority integers.

mod statute;

statute.ar

//! A customs statute with a lex-specialis exception.
//!
//! General norm:  imported goods owe import duty (the default).
//! Specific norm: medical imports are exempt — and *lex specialis*
//!                says the specific rule wins.
//!
//! Pre-RFD-0028 this conflict was unresolvable: both rules concluded
//! about the same head at the same strength, and there was no
//! superiority mechanism (`#[priority]` was silently dropped;
//! `#[defeats]` did not exist) — register blocker R-B8. Now the
//! exemption rule names the general clause's label and defeats it,
//! per-tuple, with an explicit edge:
//!
//!   #[defeats(must_pay_duty.general(g))]
//!
//! Reads true at every line: imported goods owe duty by default;
//! medical goods are exempt; the exemption defeats the general duty
//! clause for exactly the exempt goods.
//!
//! Expected `must_pay_duty` extent over the four goods below:
//!   steel    (imported, not medical)  → owes duty   (default, unattacked)
//!   insulin  (imported, MEDICAL)       → exempt      (lex specialis defeats)
//!   gauze    (imported, MEDICAL)       → exempt      (lex specialis defeats)
//!   widget   (NOT imported)            → no clause fires
//!
//!   ⇒ must_pay_duty = { steel }

pub type Good {
    mut imported: Bool,
    mut medical: Bool,
}

pub type Imported <: Good iff { self.imported == true };

pub type MedicalGood <: Good iff { self.medical == true };

// General norm: imported goods owe import duty — but overridable, and
// labeled so a more specific rule can name it.
#[default]
#[label (general)]
pub derive must_pay_duty(g) :- Imported(g);

// Specific norm: medical imports are exempt. Lex specialis — the
// specific rule defeats the general clause for exactly the medical
// goods it derives.
#[defeats (must_pay_duty.general(g))]
pub derive exempt(g) :- MedicalGood(g);

pub mutate declare(g: Good, imported: Bool, medical: Bool) {
    insert iof(g, Good);
    update g: Good set { imported = imported, medical = medical }
}

pub query dutiable() -> must_pay_duty;
pub query exemptions() -> exempt;

Cross-module defeat: each provision in its own file

Area: Defeasible reasoning Teaches: the defeat plane across files (RFD 0082) — one provision per file: the exemption defeats the duty clause it names in another module over an ordinary use import, and an emergency tariff defeats the exemption from a third file, reinstating the duty for exactly the listed goods. Prerequisites: lex specialis in one file. Run: ox build examples/cross_module_defeat_v0 && ox run-scenario examples/cross_module_defeat_v0

The lex-specialis customs story (legal_priority_v0) laid out the way a statute corpus wants it — one file per provision, every #[defeats] edge crossing a module boundary (RFD 0082):

• duty.ar — the general norm: imported goods owe duty (#[default], labeled general).
• exemption.ar — medical imports are exempt; carries #[defeats(must_pay_duty.general(g))], naming the clause it overrides in another file, resolved over an ordinary use import. Itself #[default].
• emergency.ar — an emergency tariff suspends the exemption for listed goods; carries #[defeats(exempt.medical(g))] from a third file. Where it fires, the exemption stops blocking and the general duty reinstates — the defeated-defeater property over the merged, cross-module graph.

Over the three goods in demo.toml: steel (imported) owes duty by the unattacked default; insulin (medical) is exempt by the cross-file defeat; serum (medical, emergency-listed) owes duty again by the cross-file reinstatement. must_pay_duty = { steel, serum }, exempt = { insulin }, emergency_tariff = { serum }.

Defeated defeaters: a pardon restores the vote

Area: Defeasible reasoning Teaches: a defeater that is itself a #[default] and is itself defeated. The attacker stops blocking its target on exactly the tuples where the attacker was defeated — RFD 0028 D4, “defeated defeaters are legal.” Prerequisites: strict vs default vs defeater, lex specialis. Run: ox build examples/defeasible_defeated_defeater_v0 then ox run-scenario examples/defeasible_defeated_defeater_v0 --scenario <scenario.toml> (see Running it for a four-person scenario).

The previous examples have a two-level defeat: a default, and an attacker that blocks it. Here there are three levels — an exception, and an exception to the exception:

adult(p)         →  can_vote(p)              the overridable default
disenfranchised  ⇒  defeats can_vote          felons lose the vote
restored         ⇒  defeats disenfranchised   a pardon restores it

The legal question: a felon is disenfranchised, but a pardon overturns the disenfranchisement. Does the pardoned felon vote? The answer requires the middle rule to be both an attacker (of can_vote) and a target (of restored).

What to read in franchise.ar

The default and its attacker — but the attacker is itself a #[default], so it can be defeated in turn:

#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

#[default]
#[label(felon)]
#[defeats(can_vote.adult(p))]
pub derive disenfranchised(p) :- Felon(p);

The exception to the exception. restored defeats disenfranchised’s labeled clause for the pardoned felons:

#[defeats(disenfranchised.felon(p))]
pub derive restored(p) :- Pardoned(p);

The subtle part is what disenfranchised is allowed to block. It blocks can_vote only on the felons it itself still survives for — i.e. the unpardoned ones. On a pardoned felon, disenfranchised is defeated, so it no longer blocks can_vote, and the adult default underneath survives. Resolving this correctly means resolving attacker survival in defeat-graph order, not from each attacker’s raw support.

Running it

This package ships no data (no demo.toml, no facts) — its behavior is exercised by registering people, so supply a four-person scenario. Save this as scenario.toml:

[[mutate]]
path = "franchise::register"
args = { p = "adam", age = 40, felon = false, pardoned = false }
[[mutate]]
path = "franchise::register"
args = { p = "ben", age = 30, felon = true, pardoned = false }
[[mutate]]
path = "franchise::register"
args = { p = "cleo", age = 50, felon = true, pardoned = true }
[[mutate]]
path = "franchise::register"
args = { p = "dot", age = 12, felon = false, pardoned = false }

Then ox run-scenario examples/defeasible_defeated_defeater_v0 --scenario scenario.toml:

adam   adult, not felon            → can_vote   (default, unattacked)
ben    adult, felon, NOT pardoned  → blocked    (disenfranchised survives)
cleo   adult, felon, PARDONED      → can_vote   (defeater itself defeated)
dot    minor                       → absent     (not an Adult)

so voters returns 2 rows — adam and cleo. The decisive contrast is ben vs cleo: both are felons, both are disenfranchised, but cleo’s disenfranchisement is itself defeated by the pardon, so the adult default underneath survives for her and not for ben.

This example is compiled and run in CI; the {adam, cleo} voter set — proving the pardoned felon votes and the unpardoned one stays blocked — is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), which registers the four people directly, so the defeated-defeater resolution can’t drift.

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

//! Defeated defeaters are legal (RFD 0028 D4 — the F2 regression).
//!
//! The exception-to-the-exception: an attacker that is itself
//! `#[default]` and itself defeated stops blocking its target on the
//! tuples where it was defeated.

mod franchise;

franchise.ar

//! Pardoned felons regain the vote: a three-level defeat chain.
//!
//!     adult(p)          →  can_vote(p)         (the overridable default)
//!     disenfranchised   ⇒  defeats can_vote     (felons lose the vote)
//!     restored          ⇒  defeats disenfranchised  (a pardon restores it)
//!
//! `disenfranchised` is itself `#[default]` and is itself the target of
//! `restored`'s `#[defeats]`. RFD 0028 D4: "defeated defeaters are
//! legal." So on a PARDONED felon, `disenfranchised` is defeated and
//! therefore no longer blocks `can_vote` — the adult default survives
//! and the pardoned felon can vote. An UNpardoned felon stays blocked.
//!
//! The F2 bug projected the blocking set from `disenfranchised`'s RAW
//! support extent rather than its post-defeat SURVIVING extent, so a
//! pardoned felon was still (wrongly) blocked. The fix resolves attacker
//! survival in defeat-graph topological order: `disenfranchised` blocks
//! `can_vote` only on the felons it itself still survives for — i.e. the
//! UNpardoned ones.
//!
//! Expected `can_vote` extent:
//!   adam   adult, not felon                  → can_vote   (default, unattacked)
//!   ben    adult, felon, NOT pardoned        → blocked    (disenfranchised survives)
//!   cleo   adult, felon, PARDONED            → can_vote   (defeater defeated)
//!   dot    minor                             → absent     (not adult)

pub type Person {
    mut age: Int,
    mut felon: Bool,
    mut pardoned: Bool,
}

pub type Adult <: Person iff { self.age >= 18 };

pub type Felon <: Person iff { self.felon == true };

pub type Pardoned <: Person iff { self.pardoned == true };

// The overridable default: adults can vote.
#[default]
#[label (adult)]
pub derive can_vote(p) :- Adult(p);

// The exception: felons are disenfranchised, which defeats the vote.
// Itself a default — so it can be defeated in turn.
#[default]
#[label (felon)]
#[defeats (can_vote.adult(p))]
pub derive disenfranchised(p) :- Felon(p);

// The exception-to-the-exception: a pardon defeats the disenfranchisement.
#[defeats (disenfranchised.felon(p))]
pub derive restored(p) :- Pardoned(p);

pub mutate register(p: Person, age: Int, felon: Bool, pardoned: Bool) {
    insert iof(p, Person);
    update p: Person set { age = age, felon = felon, pardoned = pardoned }
}

pub query voters() -> can_vote;

Recursion under a live defeat plane

Area: Defeasible reasoning Teaches: a recursive rule (transitive closure) still computes its full fixpoint when the module also carries a defeat plane — the defeasibility transform attributes each clause’s contribution over the converged support, so a recursive clause sees its own prior tuples. Prerequisites: lex specialis, and recursive derive rules (transitive closure). Run: ox build examples/defeasible_recursion_v0 && ox derive examples/defeasible_recursion_v0 reach

The presence of a single #[default]/#[defeats] pair anywhere in a module switches its entire evaluation onto the Governatori defeasibility transform rather than the classical Datalog fast path. A recursive rule must keep working under that transform. This example pins that property: a transitive closure, evaluated next to an unrelated defeat plane, must still be whole.

What to read in graph.ar

A standard recursive transitive closure over a 3-edge chain a → b → c → d:

pub derive reach(x: Node, y: Node) :- edge(x, y);
pub derive reach(x: Node, z: Node) :- reach(x, y), edge(y, z);

The recursive clause feeds on its own prior output — (a,c) needs (a,b) and (b,c) to already be in reach.

An unrelated defeat plane — a #[default] head attacked by a #[defeats] edge — on a different predicate entirely. Its only job here is to make has_defeat_plane() true so the whole module evaluates through the defeasibility transform:

#[default]
#[label(presumed)]
pub derive flagged(n: Node) :- Node(n);

#[defeats(flagged(n))]
pub derive cleared(n) :- edge(n, n);

cleared requires a self-loop edge(n, n); the chain has none, so the defeat never actually fires. It exists purely to activate the transform that the recursive closure must survive.

Running it

The graph is shipped as pub fact data (no mutations), so the runner is ox derive … reach rather than a scenario. Over a → b → c → d the closure is the six reachable pairs:

derive(reach): 6 tuple(s)
  (a,b) (a,c) (a,d)
  (b,c) (b,d)
  (c,d)

The transitive pairs (a,c), (b,d), (a,d) are exactly the ones the recursive clause derives from reach’s own prior tuples — the contributions a naive per-clause defeat attribution would drop if it cleared the head before attributing support. Six tuples, not three: the closure is whole under the live defeat plane.

This example is compiled and run in CI; the full six-pair closure under the defeat plane is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so a regression in the defeasibility transform breaks the build rather than silently under-deriving.

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

//! Recursion under a live defeat plane (RFD 0028 — the F1 regression).
//!
//! A self-recursive `#[default]`-bearing module must still compute the
//! full transitive closure. The defeasibility transform attributes each
//! clause's contribution over the CONVERGED support catalog — never a
//! cleared head — so a recursive clause sees its own prior tuples and
//! transitive closure does not silently under-derive.

mod graph;

graph.ar

//! Transitive closure of a 3-edge chain (a→b→c→d), evaluated inside a
//! module that carries a live defeat plane.
//!
//! The chain: edge(a,b), edge(b,c), edge(c,d).
//!
//! `reach` is the standard recursive transitive closure:
//!     reach(x, y) :- edge(x, y);                       // base
//!     reach(x, z) :- reach(x, y), edge(y, z);          // recursive step
//!
//! Over a→b→c→d the closure is the six pairs
//!     {(a,b),(b,c),(c,d),(a,c),(b,d),(a,d)}.
//!
//! The defeat plane below (a `#[default]` clause attacked by a
//! `#[defeats]` edge, on an unrelated head) makes `has_defeat_plane()`
//! true, so `reach` is evaluated through the Governatori compilation
//! transform rather than the classical fast path. The F1 bug cleared
//! the head before per-clause attribution, dropping every transitive
//! pair the recursive clause needed its own prior tuples to derive
//! (it returned only {(a,b),(b,c),(c,d)} with no diagnostic). The fix
//! attributes per clause over the converged support catalog, so the
//! recursive clause derives (a,c),(b,d),(a,d) and the closure is whole.

pub type Node {}

pub rel edge(x: Node, y: Node);

// The graph: a → b → c → d.
pub fact Node(a)
pub fact Node(b)
pub fact Node(c)
pub fact Node(d)

pub fact edge(a, b)
pub fact edge(b, c)
pub fact edge(c, d)

// Transitive closure — the recursive head under test.
// ANCHOR: reach
pub derive reach(x: Node, y: Node) :- edge(x, y);
pub derive reach(x: Node, z: Node) :- reach(x, y), edge(y, z);
// ANCHOR_END: reach
// ── The live defeat plane (unrelated to `reach`) ──────────────────
// A standalone `#[default]` head attacked by a `#[defeats]` edge. This
// activates the defeasibility transform for the whole module so `reach`
// is evaluated through it — the path the F1 bug corrupted.
// ANCHOR: defeat
#[default]
#[label (presumed)]
pub derive flagged(n: Node) :- Node(n);

#[defeats (flagged(n))]
pub derive cleared(n) :- edge(n, n);
// ANCHOR_END: defeat
pub query closure() -> reach;

Defeat plane + check, in one module

Area: Defeasible reasoning Teaches: a #[defeats] lex-specialis priority plane and a check compliance invariant composing in the same build — a check evaluates over the warranted (post-defeat) extent, so a defeated conclusion never trips it. Prerequisites: lex specialis, and check invariants (see check constraints). Run: ox build examples/legal_obligations_compose_v0 && ox run-scenario examples/legal_obligations_compose_v0

A realistic legal consumer wants both: a vocabulary’s free compliance checks and defeasible norm priority. These were once mutually exclusive — ox build refused any module carrying both a check and a #[defeats]/#[default] plane, because the static-discharge evaluator ran the strict path only and would over-fire checks on conclusions the defeat plane removes. The fix composes them on a single principle: a check is a constraint over what the program concludes, and under a defeat plane the conclusions are the warranted, post-defeat extent.

What to read in statute.ar

A lex-specialis defeat plane — the general breach norm, defeated by a force-majeure exemption per-tuple:

#[default]
#[label(general)]
pub derive obligated(o) :- Outstanding(o);

#[defeats(obligated.general(o))]
pub derive exempt(o) :- ForceMajeure(o);

A check that reads the defeasible head. UnreviewedBreach fires on an obligation that is in breach but not reviewed. It reads the warranted obligated, so it must not fire on an exempted obligation — even though that obligation is still Outstanding (the general clause’s body):

pub check UnreviewedBreach(o: Obligation) :-
    obligated(o),
    o.reviewed == false
    => Diagnostic { severity: Severity::Error, code: "Compliance::E001", … };

A transitive downstream rule joins the defeasible head. seriousBreach is a non-defeasible rule that joins obligated — it must see the warranted extent, so it does not classify a defeated (exempted) obligation as serious even when that obligation is high-value. A second check, UnescalatedSeriousBreach, reads seriousBreach, so the defeated tuple must not leak through the downstream join into a check either:

pub derive seriousBreach(o) :- obligated(o), o.highValue == true;

This is the retraction-safe path: the warranted obligated is what every downstream consumer — checks and joins alike — observes.

Running it

The scenario opens three obligations:

ob1  outstanding, not force-majeure, reviewed     → breach, no violation
ob2  outstanding, FORCE MAJEURE (exempt), UNreviewed, high-value → defeated out of obligated
ob3  outstanding, not force-majeure, reviewed     → breach, no violation

The queries report:

query statute::breaches:        2 row(s)   — warranted obligated = { ob1, ob3 }
query statute::exemptions:      1 row(s)   — { ob2 }
query statute::seriousBreaches: 0 row(s)   — no high-value warranted breach

ob2 is both force-majeure and high-value, yet it appears in neither breaches nor seriousBreaches: the defeat removes it from obligated, and that removal propagates through the downstream join. ob2 is also the one unreviewed obligation — and yet UnreviewedBreach never fires on it, precisely because the check reads the warranted obligated and the defeat already removed ob2 from it (ob1 and ob3 are reviewed, so they trip nothing either). So the scenario commits cleanly — and the reason is the lesson: a module carrying both a defeat plane and a check now builds, and the check sees only the post-defeat extent.

Honest caveats (what runs today)

• The check’s firing behavior over the warranted extent — that UnreviewedBreach fires on an unreviewed warranted breach and does not fire on the exempted (defeated-away) obligation, and likewise for the transitive seriousBreach/UnescalatedSeriousBreach chain — is exercised by separate corpus tests with unreviewed obligations, not by this clean scenario. The scenario shows the module building and running; the corpus tests show the check discriminating.

This example is compiled and run in CI; the warranted breach extent and the check-firing behavior over it (including the transitive downstream relation) are pinned by corpus tests (oxc-runtime/tests/examples_corpus.rs), so the defeat↔check composition can’t drift.

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

//! `#[defeats]` priority + a `check` compliance invariant in one build
//! (issue #373). See `statute.ar` for the model and the expected breach
//! calculus. This package proves that the lex-specialis defeat plane and
//! catalog `check`s COMPOSE — the check evaluates over the warranted
//! (post-defeat) extent, so a defeated obligation does not trip it.

mod statute;

statute.ar

//! Lex-specialis `#[defeats]` priority AND a `check` compliance
//! invariant, in ONE module (issue #373).
//!
//! Before #373 these two features were mutually exclusive: `ox build`
//! refused any module carrying BOTH a `check` and a
//! `#[defeats]`/`#[default]` defeat plane (the static-discharge
//! evaluator ran the strict path only and would over-fire checks on
//! defeated conclusions). That blocked the realistic legal consumer —
//! one that wants the vocabulary's free `check`s AND defeasible norm
//! priority. The fix composes them: a `check` is a constraint over what
//! the program *concludes*, and under a defeat plane the conclusions are
//! the WARRANTED (post-defeat) extent. So a check evaluates over the
//! warranted set — a tuple defeated away does not trip a check that
//! would have fired on it; a surviving tuple does.
//!
//! The model — a rent-obligation breach calculus with a force-majeure
//! exemption (lex specialis) and a compliance invariant:
//!
//!   * `obligated(o)` — every outstanding obligation is in breach by
//!     default (`#[default]`, `#[label(general)]`).
//!   * `exempt(o)` — a force-majeure obligation is excused, and that
//!     exemption `#[defeats(obligated.general(o))]` the general clause
//!     for exactly the exempt obligations (per-tuple lex specialis).
//!   * `UnreviewedBreach` — a `check` compliance invariant: an
//!     obligation that is IN BREACH (warranted) but not flagged for
//!     review is a violation. It reads the WARRANTED `obligated` head,
//!     so it must NOT fire on an exempted obligation.
//!
//! Expected breach (warranted `obligated`) over the obligations below:
//!   ob1  outstanding, not exempt, reviewed     → breach, NO violation
//!   ob2  outstanding, FORCE MAJEURE (exempt)    → defeated away
//!   ob3  outstanding, not exempt, NOT reviewed  → breach + violation
//!
//!   ⇒ obligated = { ob1, ob3 };  UnreviewedBreach fires on { ob3 }

pub type Obligation {
    mut outstanding: Bool,
    mut forceMajeure: Bool,
    mut reviewed: Bool,
    mut highValue: Bool,
}

pub type Outstanding <: Obligation iff { self.outstanding == true };
pub type ForceMajeure <: Obligation iff { self.forceMajeure == true };

// General norm (overridable): an outstanding obligation is in breach by
// default — labeled so the specific exemption can name it.
#[default]
#[label (general)]
pub derive obligated(o) :- Outstanding(o);

// Lex specialis: a force-majeure obligation is exempt, and the exemption
// defeats the general breach clause for exactly the exempt obligations.
#[defeats (obligated.general(o))]
pub derive exempt(o) :- ForceMajeure(o);

// Compliance invariant (a `check`): an obligation in breach (warranted)
// that has not been flagged for review is a violation. Reads the
// post-defeat `obligated` head — an exempted obligation is NOT in
// warranted breach, so this never fires on the force-majeure case even
// though it is `Outstanding` (the general clause's body).
pub check UnreviewedBreach(o: Obligation) :-
    obligated(o),
    o.reviewed == false => Diagnostic {
        severity: Severity::Error,
        code: "Compliance::E001",
        message: "obligation in breach has not been reviewed"
    };

// A TRANSITIVE downstream relation: a high-value obligation in breach is
// a "serious" breach. This is a NON-defeasible rule that JOINS the
// defeasible `obligated` head — it must see the WARRANTED extent, so it
// does NOT classify the exempted (defeated-away) obligation as serious
// even when that obligation is high-value. This pins the retraction-safe
// recompute: the warranted `obligated` is seeded as EDB and this rule
// recomputes over it (a monotone fixpoint over the raw extent would have
// leaked the defeated tuple in).
pub derive seriousBreach(o) :- obligated(o), o.highValue == true;

// A compliance invariant over the TRANSITIVE downstream relation: a
// serious breach must be escalated. This `check` reads `seriousBreach`,
// which itself joins the defeasible `obligated` head — so the check sees
// the warranted recompute. An exempted high-value obligation is NOT a
// warranted serious breach, so this never fires on it (the retraction-
// safe path: the defeated `obligated` tuple does not leak through the
// downstream join into the check).
pub type Escalated;
pub check UnescalatedSeriousBreach(o: Obligation) :-
    seriousBreach(o),
    not Escalated(o) => Diagnostic {
        severity: Severity::Error,
        code: "Compliance::E002",
        message: "serious breach has not been escalated"
    };
pub fact Escalated(ghost);

pub mutate openObligation(
    o: Obligation,
    outstanding: Bool,
    forceMajeure: Bool,
    reviewed: Bool,
    highValue: Bool
) {
    insert iof(o, Obligation);
    update o: Obligation set {
        outstanding = outstanding,
        forceMajeure = forceMajeure,
        reviewed = reviewed,
        highValue = highValue
    }
}

pub query breaches() -> obligated;
pub query exemptions() -> exempt;
pub query seriousBreaches() -> seriousBreach;

Lease obligations: lex specialis as stratified negation

Area: Defeasible reasoning Teaches: expressing lex specialis (a specific exemption overriding a general breach norm) with stratified negation rather than the #[defeats] directive plane — the form you reach for when a module also imports a check-bearing vocabulary. Plus a real breach calculus over an imported deontic vocabulary. Prerequisites: lex specialis via #[defeats], defeat plane + check, and cross-package vocabulary (use legal_vocab_v0::…). Run: ox build examples/legal_obligations_v0 && ox run-scenario examples/legal_obligations_v0

This is the flagship legal-obligations model: a lease creates a rent obligation running from a tenant (debtor) to a landlord (creditor), declared against the separate legal_vocab_v0 deontic vocabulary. An obligation past its due date and unperformed is in breach — unless a force-majeure exemption applies. That “unless” is lex specialis again, but written a different way than the previous two examples, and the why is the lesson.

What to read in lease.ar

Lex specialis as stratified negation. The general breach norm fires unless the specific exemption holds; the exemption lives in a strictly-lower stratum, so not exempt(o) is well-defined:

pub derive outstanding(o) :- o: RentObligation, o.performed == false, o.due < today();
pub derive exempt(o)      :- o: ExemptObligation, outstanding(o);
pub derive breach(o)      :- outstanding(o), not exempt(o);

The resolution is identical to the #[defeats] lex-specialis in legal_priority_v0 — the specific rule wins for exactly the exempt obligations — but expressed with negation instead of a defeat directive.

Why not #[defeats] here? This package imports the check-bearing legal_vocab_v0, and ox build refuses any module that has both a check and a #[defeats]/#[default] plane in scope (check-discharge runs the strict path only). So when a defeat plane and an imported check can’t coexist in one build, stratified negation gives the same lex-specialis resolution and composes with the vocabulary’s catalog checks. (The composing case — defeat plane and check in one module, post-fix — is legal_obligations_compose_v0.)

A second, additive breach path for a long-stale obligation, still subtracting the exemption:

pub derive breach(o) :-
    o: RentObligation, o.performed == false, not exempt(o),
    o.due + 365.days < today();

The force-majeure exemption protects the obligor on this path too — it is not unconditionally overridden by staleness.

A derived penalty value bound in the rule head, rate × days-late, staying in the exact numeric tower:

pub derive penaltyOwed(o, amount) :- breach(o), amount = o.rate * o.daysLate;

Running it

The scenario opens four obligations against an evaluation clock of “today”:

ob1  due 2020-01-01, unperformed, NOT exempt   → breach (long-overdue path keeps it in at every clock)
ob2  due 2026-05-01, unperformed, EXEMPT        → not in breach (lex specialis subtracts it)
ob3  due 2026-05-01, unperformed, NOT exempt    → breach (outstanding, not exempt)
ob4  due 2026-05-01, PERFORMED                   → not in breach (discharged)

The queries report:

query lease::outstanding_obligations: 3 row(s)   — { ob1, ob2, ob3 }   (ob4 performed)
query lease::exempt_obligations:      1 row(s)   — { ob2 }
query lease::breached_obligations:    2 row(s)   — { ob1, ob3 }        (ob2 exempt; ob4 performed)
query lease::penalties:               2 row(s)   — (ob1, 1500) and (ob3, 250)

ob2 is outstanding but exempt, so the exemption subtracts it from breach on both paths — the lex-specialis point. The penalties are rate × daysLate: ob1 is 50.00 × 30 = 1500, ob3 is 25.00 × 10 = 250, both exact Decimal × Int.

Honest caveats (what runs today)

• #[defeats] and check are mutually exclusive in one build (the wall this model documents). The canonical RFD 0028 spelling of lex specialis is the #[defeats] directive plane, proven standalone in legal_priority_v0; it cannot be used here because this package imports a check-bearing vocabulary. Stratified negation is the composing form.
• Days-late is recorded, not computed from the dates. A penalty cannot be derived from elapsed time inside a rule: there is no Duration → Int day-count extractor, and today()/now() as a rule-body operand is refused with OE1316. So daysLate is stamped as an Int at breach time (recordBreach) rather than computed from today() - due.

This example is compiled and run in CI; the breach calculus over the cross-package vocabulary — the {ob1, ob3} breach extent and the 1500/250 penalties — is pinned by a CLI-pipeline test (oxc-driver/tests/cli_pipeline.rs), so the lex-specialis-via-negation behavior can’t drift.

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

//! `legal_obligations_v0` — a real, Sharpe-style legal-obligations model
//! authored IN Argon against the SEPARATE `legal_vocab_v0` deontic vocabulary
//! (RFD 0030). This is the v0.2.1 legal-demo forcing function: it exercises the
//! whole stack in one served package — cross-package vocabulary dependency
//! (#350), deontic metatypes + the `directed_obligation` metarel as imported
//! keywords (#311/#350), temporal `#date#` deadlines and `today()` / `+ N.days`
//! date arithmetic (#366), lex-specialis norm priority (a specific exemption
//! overriding the general breach norm), and a derived penalty value (#351) —
//! and is then SERVED over HTTP and driven through the obligation lifecycle
//! (#353; see `demo.toml` for the in-process harness and the PR transcript for
//! the served `/v1` run).
//!
//! ## The legal scenario
//!
//! A lease contract creates a rent obligation running FROM a tenant (debtor) TO
//! a landlord (creditor) — a `directed_obligation`, the deontic relation the
//! vocabulary ships. The obligation carries a `due` date (its VALID time: it
//! does not hold before the rent period begins) and a daily late penalty rate.
//! A rent obligation past its due date and unperformed is in BREACH — UNLESS a
//! force-majeure exemption applies, which OVERRIDES the general breach norm
//! (lex specialis: the specific exemption beats the general norm). An
//! obligation more than one year (365 days) past due is in breach via a
//! SECOND, independent breach path (the long-overdue path) — an additive
//! derivation that catches a long-stale obligation even when some other excuse
//! would otherwise apply, but which STILL subtracts the lex-specialis
//! exemption (`not exempt`): a force-majeure-exempt obligation is excluded from
//! breach on either path. The penalty owed on a breached obligation is a
//! DERIVED value: `rate × days-late`.
//!
//! ## What each construct proves (the canary trail)
//!
//!   * `use legal_vocab_v0::{ obligation, party, directed_obligation };` — the
//!     consumer never declares these introducers; it imports them from a
//!     package it does not own and uses them as keywords. Cross-package vocab
//!     dependency (#350) + deontic metatypes as introducers (#311/RFD 0031).
//!
//!   * `RentObligation <: TimedObligation` declared with the imported
//!     `obligation` keyword; `Tenant`/`Landlord <: LegalSubject` with the
//!     imported `party` keyword; `owes(...)` declared with the imported
//!     `directed_obligation` metarel, whose BOTH endpoints the vocabulary
//!     constrains to be `party`-sorted (#311 — a directed obligation between
//!     two legal subjects, verified across the boundary; the wrong-sorted
//!     refusal is in `examples/legal_catalog_bad_v0`).
//!
//!   * `insert iof(o, RentObligation) at due` — the obligation's membership
//!     takes the VALID time of the rent period (#366 valid-time at-writes): the
//!     obligation did not hold before `due`.
//!
//!   * `o.due < today()` and `o.due + 365.days < today()` — breach is
//!     `today()` past the due date, plus a second additive clause for a stale
//!     (> 1 year / 365 days overdue) obligation. That second clause is an
//!     independent breach path but still carries `not exempt(o)`, so the
//!     lex-specialis exemption subtracts on it too (it does not unconditionally
//!     override the exemption). `today()` reads the evaluation clock, fixed for
//!     the fixpoint, and `+ N.days` is exact day-granular date arithmetic
//!     (#366).
//!
//!   * `breach(o) :- outstanding(o), not exempt(o)` — lex specialis as
//!     stratified negation: the general breach norm fires unless the specific
//!     exemption holds. See the WALL note below on why this served model does
//!     NOT use the `#[defeats]` directive plane.
//!
//!   * `amount = o.rate * o.daysLate` — a DERIVED computed value in a rule head
//!     (#351/RFD 0029 body-level binding `=`): the late penalty owed,
//!     `Decimal × Int`, staying in the exact numeric tower.
//!
//! ## Walls this package documents (see the PR wall list)
//!
//!   * `#[defeats]` + `check` are mutually exclusive in one build. The
//!     canonical RFD 0028 lex-specialis spelling is the `#[defeats]` directive
//!     plane (proven standalone in `examples/legal_priority_v0`). This served
//!     model imports the CHECK-BEARING `legal_vocab_v0`, and `ox build` refuses
//!     any module that has BOTH a `check` and a `#[defeats]`/`#[default]` plane
//!     in scope (check-discharge runs the strict path only and would over-fire
//!     checks on defeated conclusions — `oxc-runtime/src/checks.rs`). So lex
//!     specialis is expressed here with stratified negation, which composes
//!     with the vocabulary's catalog checks. Filed as a FINAL-gate wall.
//!
//!   * A penalty cannot be computed from elapsed time INSIDE a rule. Two
//!     mechanisms block it, and neither is a `Decimal × Duration` type refusal
//!     (a bare `Decimal * Duration` over a `Duration` field type-checks clean):
//!     (1) there is no `Duration → Int` day-count extractor, so an elapsed
//!     `Duration` cannot be turned into the `Int` multiplier the penalty needs;
//!     and (2) date subtraction against the evaluation clock is not available in
//!     a rule body — `today()` / `now()` inside a rule is refused with OE1316,
//!     so `today() - due` cannot be formed to produce the elapsed span in the
//!     first place. So `daysLate` is recorded as an `Int` at breach time
//!     (`recordBreach`) rather than computed from the dates in the rule. Filed
//!     as a wall (#374).

mod lease;

lease.ar

//! The lease-obligations model. See `root.ar` for the scenario and the
//! construct-by-construct canary trail.

// The deontic vocabulary's introducer keywords + upper concepts, imported
// across the package boundary (RFD 0030). The consumer declares its concepts
// WITH these keywords; it never declares the keywords themselves.
use legal_vocab_v0::{ obligation, party, directed_obligation };
use legal_vocab_v0::{ LegalSubject, Contract, TimedObligation };

// ── Parties (the legal subjects) ──
//
// `Tenant` and `Landlord` are declared with the vocabulary's `party`
// introducer and specialize its `LegalSubject` root — so both are `party`-
// sorted, which is what the `directed_obligation` metarel requires of its
// endpoints (#311). `name` is a plain ABox field.
pub party Tenant <: LegalSubject {
    name: String,
}
pub party Landlord <: LegalSubject {
    name: String,
}

// ── The contract (a UFO relator) ──
//
// A `Lease` is declared with the vocabulary's `legal_relator` root `Contract`:
// the relator that bundles and truthmakes the rent obligations.
pub type Lease <: Contract {
    mut address: String,
}

// ── The rent obligation ──
//
// `RentObligation` is declared with the imported `obligation` keyword and
// specializes the vocabulary's `TimedObligation` root — so it inherits the
// `due: Date` deadline field and is anchored (the vocabulary's
// `OrphanObligationConcept` check, were it in scope, would NOT fire on it).
// `rate` is the daily late penalty; `daysLate` is recorded when the breach is
// observed (see the Wall note in root.ar — elapsed time cannot be computed
// inside a rule: there is no `Duration → Int` day-count extractor and `today()`
// inside a rule is refused with OE1316, so days-late is recorded as an `Int` at
// breach time rather than derived from the dates).
pub obligation RentObligation <: TimedObligation {
    mut rate: Decimal,
    mut daysLate: Int,
    mut performed: Bool,
}

// A force-majeure exemption is a SPECIFIC kind of rent obligation: one the
// modeler has flagged as excused (a flood, a declared emergency). The
// lex-specialis exemption defeats the general breach claim.
pub type ExemptObligation <: RentObligation;

// ── The deontic relation (imported metarel) ──
//
// `owes` is declared with the imported `directed_obligation` metarel
// introducer. Its endpoints are `party`-sorted (Tenant debtor → Landlord
// creditor), satisfying the metarel's cross-package endpoint constraint (#311).
pub directed_obligation owes(mut debtor: Tenant, creditor: Landlord);

// `binds` ties an obligation to its contract (the relator's truthmaking edge).
pub rel binds(contract: Lease, ob: RentObligation);

// ════════════════════════════════════════════════════════════════════
// Breach calculus — lex specialis (a specific exemption overrides the
// general breach norm)
// ════════════════════════════════════════════════════════════════════
//
// NOTE on the priority mechanism (a documented wall — see root.ar). The
// canonical RFD 0028 spelling of lex specialis is the `#[defeats]` directive
// plane: `#[default] breach :- outstanding` defeated by
// `#[defeats(breach(o))] exempt :- ExemptObligation(o)`. That spelling is
// proven standalone in `examples/legal_priority_v0`. It CANNOT be used here:
// this package imports the check-bearing `legal_vocab_v0`, and `ox build`
// refuses any module that has BOTH a `check` and a `#[defeats]`/`#[default]`
// plane in scope (check-discharge runs the strict path only). So this served
// model expresses the SAME lex-specialis resolution with stratified negation —
// the general norm fires unless the specific exemption holds — which composes
// with the vocabulary's catalog checks. Filed as a FINAL-gate wall.
// An obligation is OUTSTANDING if it is past its due date and not yet
// performed. (`today()` parses as a comparison operand in either position —
// `o.due < today()` and `today() > o.due` are equivalent since #375.)
pub derive outstanding(o) :- o: RentObligation, o.performed == false, o.due < today();

// The EXCEPTION (lex specialis): a force-majeure exemption excuses an
// outstanding obligation. The more specific norm.
pub derive exempt(o) :- o: ExemptObligation, outstanding(o);

// The GENERAL norm, overridden by the specific exemption: an outstanding
// obligation is in breach UNLESS it is exempt (stratified negation — the
// exemption lives in a strictly-lower stratum). Lex specialis: the specific
// rule wins for exactly the exempt obligations; a non-exempt outstanding
// obligation stays in breach.
pub derive breach(o) :- outstanding(o), not exempt(o);

// The STALE-OBLIGATION clause: an obligation more than a year past due is in
// breach. This is a SECOND, independent breach path (a disjunctive head): it
// fires on a long-stale obligation even if some other excuse would otherwise
// apply, EXCEPT the lex-specialis exemption, which it still subtracts (`not
// exempt`) — a force-majeure exemption protects the obligor here. Demonstrates
// `+ N.days` exact day-granular date arithmetic (#366) as a second, additive
// derivation of the same `breach` head.
//
// Determinism over time: ob1 (due 2020-01-01) is always past `due + 365.days`,
// so this clause fires on ob1 for every evaluation clock (it is the rule that
// keeps ob1 in breach independent of the general path). The recent 2026
// obligations are protected by `not exempt` (ob2) or are already in breach via
// the general path (ob3) — so the breach extent is the same {ob1, ob3} at every
// clock past their due dates, which is the property the corpus test pins.
pub derive breach(o) :-
    o: RentObligation,
    o.performed == false,
    not exempt(o),
    o.due + 365.days < today();

// ── Derived penalty value (#351 / RFD 0029) ──
//
// The late penalty owed on a breached obligation: `rate × days-late`, a
// computed value bound in the rule head via the body-level binding `=`
// (single `=`, assignment; distinct from the `==` filter). `Decimal × Int`
// stays in the exact numeric tower.
pub derive penaltyOwed(o, amount) :- breach(o), amount = o.rate * o.daysLate;

// ════════════════════════════════════════════════════════════════════
// Obligation lifecycle — the mutations served over HTTP (#353)
// ════════════════════════════════════════════════════════════════════
//
// `openObligation` mints the obligation, the parties, and the contract over
// HTTP (entity-typed params take a symbolic name and mint a fresh individual —
// R-B5), stamps the obligation's VALID time at its `due` date (#366), and wires
// the deontic + relator edges. `recordPerformance` discharges it (no breach).
// `recordBreach` records the observed days-late (the penalty input).
pub mutate openObligation(
    o: RentObligation,
    contract: Lease,
    tenant: Tenant,
    landlord: Landlord,
    address: String,
    due: Date,
    rate: Decimal
) {
    insert iof(tenant, Tenant);
    insert iof(landlord, Landlord);
    insert iof(contract, Lease);
    update contract: Lease set { address = address };
    insert iof(o, RentObligation) at due;
    update o: RentObligation set { due = due, rate = rate, daysLate = 0, performed = false };
    insert owes(tenant, landlord);
    insert binds(contract, o);
}

// Mark the obligation performed — it leaves the outstanding/breach set.
pub mutate recordPerformance(o: RentObligation) {
    update o: RentObligation set { performed = true }
}

// Record an observed breach: stamp the days-late (the penalty multiplier).
pub mutate recordBreach(o: RentObligation, daysLate: Int) {
    update o: RentObligation set { daysLate = daysLate }
}

// Flag an obligation as force-majeure exempt (reclassify into the specific
// `ExemptObligation` subtype — the lex-specialis exception).
pub mutate grantExemption(o: ExemptObligation) {
    insert iof(o, ExemptObligation)
}

// ── Queries (the served read surface) ──
pub query outstanding_obligations() -> outstanding;
pub query breached_obligations() -> breach;
pub query exempt_obligations() -> exempt;
pub query penalties() -> penaltyOwed;

Standpoint visibility: the DEFAULT layer vs scoped facts

Area: Standpoints & federation Teaches: how a fact’s scope decides which views can see it. A DEFAULT-layer (unscoped, module-level) fact restricts into every view; a standpoint-scoped fact is local to its standpoint. This is the sheaf reading of visibility — a global section restricts to every open set; a local section does not. Prerequisites: concepts, and pub query (see first-class relations). Run: ox build examples/standpoint_visibility && ox query examples/standpoint_visibility --with-truth4

A standpoint is a named viewpoint — a place from which facts are asserted and read. Standpoints sit in a <: lattice, and the unscoped DEFAULT layer is the shared base every standpoint extends. The question this example answers: when you assert a fact, who can see it? The answer turns entirely on whether the fact is scoped.

What to read in visibility.ar

Two standpoints and one concept:

pub type Widget;

pub standpoint s1;
pub standpoint s2;

A DEFAULT-layer fact is unscoped — declared at module level, outside any standpoint block. It restricts into every view:

// DEFAULT-layer (unscoped) fact — visible in every view.
pub fact Widget(dfl);

A scoped fact lives inside a standpoint block and is local to it:

pub standpoint s1 {
    pub fact Widget(only_s1);
}

pub standpoint s2 {
    pub fact Widget(only_s2);
}

Four queries read from four vantage points. The base query is unfederated (DEFAULT only); across [...] selects which standpoints join the view:

pub query base() -> Widget;                       // DEFAULT only
pub query in_s1() -> Widget across [s1];           // DEFAULT ∪ s1
pub query in_s2() -> Widget across [s2];           // DEFAULT ∪ s2
pub query fed() -> Widget across [s1, s2];         // DEFAULT ∪ s1 ∪ s2

Running it

The four views form a visibility matrix — dfl is the DEFAULT-layer individual, only_s1/only_s2 are scoped:

base   (unfederated):   { dfl }                    — DEFAULT only
in_s1  (across [s1]):    { dfl, only_s1 }           — DEFAULT ∪ s1
in_s2  (across [s2]):    { dfl, only_s2 }           — DEFAULT ∪ s2
fed    (across [s1, s2]): { dfl, only_s1, only_s2 } — DEFAULT ∪ s1 ∪ s2

The decisive cell is only_s1 against base and in_s2: it is invisible to both. A standpoint-scoped fact does not leak into the unfederated base view, and it does not leak into a different standpoint’s view. Seeing it requires explicitly selecting s1 (or federating over a list that includes it). Meanwhile dfl appears in all four rows — the DEFAULT layer is the floor every view stands on.

Every row reads [Is] here: there is no disagreement in this example, so the four-valued status is uniform. (For where [Both] arises, see federation: standpoints disagree and federation: the DEFAULT layer joins as a constituent.)

Honest caveats (what runs today)

• The query output identifies rows by individual id; the named mapping above (dfl, only_s1, only_s2) is how the package declares them.
• --with-truth4 surfaces the per-row four-valued tag. Unfederated queries always read Is; the federated views here also read Is because nothing refutes a Widget.

This example is compiled and run in CI; the four-quadrant visibility matrix is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so a leak across standpoints breaks the build rather than the docs.

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

//! Standpoint visibility composition (rsn-05).

mod visibility;

visibility.ar

//! Standpoint visibility composition (audit rsn-05).
//!
//! Demonstrates the sheaf reading of standpoint visibility (§10.4):
//!
//!   * A DEFAULT-layer (unscoped, file/module-level) `pub fact`
//!     restricts into EVERY view — the base/unfederated query AND
//!     every standpoint's federated view (a global section restricts
//!     to every open set).
//!   * A standpoint-scoped `pub fact` is LOCAL to its standpoint: it
//!     is invisible to the base/unfederated query and to a query
//!     scoped to a DIFFERENT standpoint. Cross-standpoint reads
//!     require explicit federation (`across [...]`), `box`/`diamond`,
//!     or selecting that standpoint.
//!
//! Expected runtime behavior (four-quadrant matrix):
//!
//!   base()   (unfederated):       { dfl }                    — DEFAULT only
//!   in_s1()  (across [s1]):       { dfl, only_s1 }           — DEFAULT ∪ s1
//!   in_s2()  (across [s2]):       { dfl, only_s2 }           — DEFAULT ∪ s2
//!   fed()    (across [s1, s2]):   { dfl, only_s1, only_s2 }  — DEFAULT ∪ s1 ∪ s2
//!
//! In particular `only_s1` is invisible to `base()` and to `in_s2()`;
//! `dfl` is visible everywhere.
//!
//! Soundness: `Argon.Visibility.view_of_base_eq_default_layer`
//! (base = DEFAULT layer), `Argon.Visibility.scoped_view_eq_default_union_own`
//! (scoped = DEFAULT ∪ own standpoint), `default_visible_everywhere`,
//! `scoped_invisible_to_base`, `scoped_invisible_to_other`.

// ANCHOR: visibility
pub type Widget;

pub standpoint s1;
pub standpoint s2;

// DEFAULT-layer (unscoped) fact — visible in every view.
pub fact Widget(dfl);

pub standpoint s1 {
    pub fact Widget(only_s1);
}

pub standpoint s2 {
    pub fact Widget(only_s2);
}

// Unfederated / base view: sees the DEFAULT layer only.
pub query base() -> Widget;
// Scoped views: DEFAULT layer ∪ own standpoint.
pub query in_s1() -> Widget across [s1];
pub query in_s2() -> Widget across [s2];
// Federated across both: DEFAULT layer ∪ s1 ∪ s2.
pub query fed() -> Widget across [s1, s2];
// ANCHOR_END: visibility

Federation: when standpoints disagree

Area: Standpoints & federation Teaches: across [...] joins standpoints by the four-valued information-join (FDE / Truth4). When two sources speak to the same individual, the join surfaces all four values — is, not, can, and crucially both, which arises only from one source asserting while another refutes. Prerequisites: standpoint visibility (DEFAULT vs scoped facts). Run: ox build examples/federation_disagreement && ox query examples/federation_disagreement --with-truth4

Two data sources rarely agree on everything. Most systems force you to pick a winner or crash on the conflict. Argon does neither: it federates them and reports the disagreement as a value. The four-valued truth space — is (asserted), not (refuted), can (neither), both (asserted and refuted) — is a bilattice, and across [...] combines standpoints by the information-join over it. A conflict does not corrupt the answer; it becomes both.

What to read in federation.ar

Two standpoints, each its own source of truth:

pub type Person;

pub standpoint historical;
pub standpoint public_record;

One source asserts with fact; the other refutes with not_fact (strong negation):

pub standpoint historical {
    pub fact Person(alice);
    pub fact Person(bob);
}

pub standpoint public_record {
    pub not_fact Person(alice);
    pub not_fact Person(carol);
    pub fact Person(dave);
}

not_fact is not absence — it is a positive refutation. historical says alice is a Person; public_record says alice is not. They overlap on alice and clash.

The federated query joins both sources:

pub query everyone() -> Person across [historical, public_record];

Running it

The query returns one row per individual, each tagged with the joined four-valued status:

alice  → Both   (historical asserts Person, public_record refutes)
bob    → Is     (only historical asserts)
carol  → Not    (only public_record refutes)
dave   → Is     (only public_record asserts)

All four Truth4 values appear in a single query. The decisive row is alice → Both: she is the only individual both asserted (by historical) and refuted (by public_record), and the information-join carries both polarities rather than discarding either. bob and dave are Is because exactly one source asserts and nothing refutes; carol is Not because she is refuted with no countervailing assertion. The can value is the join’s bottom — neither asserted nor refuted — and is what an individual no source mentions would read.

Honest caveats (what runs today)

• This is the default paraconsistent federation policy: a conflict is preserved as Both rather than resolved or rejected. A source declaring a contradiction does not poison the whole query.
• Rows are reported by individual id; the name mapping above is how the package declares its facts.

This example is compiled and run in CI; the per-row Truth4 verdicts under federation are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the information-join 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

//! Federation: two standpoints disagree on a fact.

mod federation;

federation.ar

//! Federation: two standpoints disagree on a fact.
//!
//! Demonstrates:
//!   * Standpoint declarations
//!   * Standpoint-scoped `pub fact` (RFD: standpoint-block scoping)
//!   * `pub not_fact` strong negation (RFD 0010)
//!   * Federated query with `across [...]` (RFD: federation runtime)
//!   * The Truth4::Both bilattice value exhibited at runtime
//!     (operational discharge of `federate_eq_both_iff`)
//!
//! Expected runtime behavior:
//!   * `everyone` query under default (paraconsistent) policy:
//!     - alice: Truth4::Both  (historical says Person, public_record refutes)
//!     - bob:   Truth4::Is    (only historical asserts)
//!     - carol: Truth4::Not   (only public_record refutes)
//!     - dave:  Truth4::Is    (only public_record asserts)
//!
//! Soundness: `Argon.Standpoint.AFTEquivalence.aft_discharges_T3_obstruction`

// ANCHOR: federation
pub type Person;

pub standpoint historical;
pub standpoint public_record;

pub standpoint historical {
    pub fact Person(alice);
    pub fact Person(bob);
}

pub standpoint public_record {
    pub not_fact Person(alice);
    pub not_fact Person(carol);
    pub fact Person(dave);
}

pub query everyone() -> Person across [historical, public_record];
// ANCHOR_END: federation

Federation: the DEFAULT layer joins as a constituent

Area: Standpoints & federation Teaches: the DEFAULT (unscoped) layer is not a privileged outer frame that overrides standpoints — it is a join constituent on equal footing. Because the DEFAULT layer restricts into every scoped view, a DEFAULT-asserted fact and a scoped refutation of the same individual collide inside one standpoint’s view, and the four-valued join yields both. Prerequisites: standpoint visibility and federation: when standpoints disagree. Run: ox build examples/federation_default_conflict && ox query examples/federation_default_conflict --with-truth4

The visibility example showed that a DEFAULT-layer fact restricts into every view — its agreement case. This example pins the disagreement case, and it is the subtle one. A single standpoint’s view is DEFAULT ∪ own. So when DEFAULT asserts a fact and the standpoint refutes it, both polarities live in the same view, and the information-join produces both — even though only one standpoint is federated. DEFAULT does not win by virtue of being the base; it participates in the join like any other source.

What to read in conflict.ar

One standpoint, with DEFAULT-layer facts above it:

pub type Person;

pub standpoint s;

// DEFAULT-layer (unscoped) facts — restrict into the scoped view `s`.
pub fact Person(eve);
pub fact Person(frank);

The standpoint refutes one of the DEFAULT facts, and refutes a third individual DEFAULT is silent on:

pub standpoint s {
    // `s` refutes the DEFAULT-layer `eve` — a same-view collision → Both.
    pub not_fact Person(eve);
    // `s` refutes `gwen`, on whom DEFAULT is silent → Not.
    pub not_fact Person(gwen);
}

Federating over the single standpoint still meets the DEFAULT layer — s’s view is DEFAULT ∪ s:

pub query conflicting() -> Person across [s];

Running it

Even across a single standpoint, the DEFAULT layer is a constituent, so the join surfaces three different verdicts:

eve    → Both   (DEFAULT asserts Person, s refutes — both meet in s's view)
frank  → Is     (DEFAULT asserts, s silent)
gwen   → Not    (s refutes, DEFAULT silent)

The decisive row is eve → Both. There is only one standpoint in across [s], so it is tempting to read DEFAULT as an outer context that s overrides — it is not. The DEFAULT assertion of eve and s’s refutation of eve are two constituents of one join, and the join holds both. Contrast frank (Is — DEFAULT alone) and gwen (Not — s alone): the verdict is exactly the information-join of whatever each layer contributes, with DEFAULT counted, never privileged.

Honest caveats (what runs today)

• This is the same paraconsistent federation policy as the two-source case: collisions are preserved as Both, not resolved in DEFAULT’s favor.
• Rows are reported by individual id; the name mapping above is how the package declares its facts.

This example is compiled and run in CI; the DEFAULT-disagreement verdicts (eve = Both in particular) are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the equal-footing join rule can’t drift.

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

//! Federation: the DEFAULT layer and a scoped layer disagree.

mod conflict;

conflict.ar

//! Federation: the DEFAULT layer participates as a join constituent
//! (rsn-05). Pins the newly-introduced behavior the review's probe
//! surfaced: under the sheaf reading (§10.4) the DEFAULT (unscoped,
//! file/module-level) layer restricts into EVERY scoped view, so a
//! DEFAULT-layer `pub fact` and a scoped `pub not_fact` over the same
//! individual COLLIDE inside the single scoped view — the FDE
//! info-join yields `Truth4::Both`. DEFAULT is not a privileged outer
//! frame that overrides standpoints; it is a constituent that joins on
//! equal footing.
//!
//! This is deliberate and consistent with
//! `Argon.Visibility.scoped_view_eq_default_union_own` (the scoped view
//! is `DEFAULT ∪ own standpoint`): when DEFAULT asserts and `own`
//! refutes, the view holds both polarities. The four-quadrant matrix
//! (`standpoint_visibility`) pins DEFAULT *agreement* (a DEFAULT fact is
//! visible everywhere); this example pins DEFAULT *disagreement*.
//!
//! Expected runtime behavior (`across [s]`):
//!
//!   eve   — Truth4::Both  (DEFAULT asserts Person, s refutes)
//!   frank — Truth4::Is     (DEFAULT asserts, s silent)
//!   gwen  — Truth4::Not     (s refutes, DEFAULT silent)
//!
//! Soundness: `Argon.Standpoint.AFTEquivalence.aft_discharges_T3_obstruction`
//! (the per-tuple Truth4 classification the federated dispatcher computes)
//! and `Argon.Visibility.scoped_view_eq_default_union_own` (DEFAULT ∪ own).

pub type Person;

pub standpoint s;

// DEFAULT-layer (unscoped) facts — restrict into the scoped view `s`.
pub fact Person(eve);
pub fact Person(frank);

pub standpoint s {
    // `s` refutes the DEFAULT-layer `eve` — a same-view collision → Both.
    pub not_fact Person(eve);
    // `s` refutes `gwen`, on whom DEFAULT is silent → Not.
    pub not_fact Person(gwen);
}

// Federated over the single standpoint `s`: its view is DEFAULT ∪ s, so
// the DEFAULT assertion and s's refutation of `eve` meet here.
pub query conflicting() -> Person across [s];

Time-travel: as_of reads the past

Area: Bitemporal time Teaches: the surface as_of clause on a pub query — the same query, snapshotted at different transaction-times, returns different answers. Every mutation stamps a monotonic transaction-time, and as_of <tx> reads the state visible at that instant. Prerequisites: refinement (iff), and mutate bodies. Run: ox build examples/temporal_as_of_surface && ox run-scenario examples/temporal_as_of_surface

A database that only knows “now” cannot answer “what did we believe last Tuesday”. Argon’s substrate is bitemporal: each mutation emits events with a monotonically-increasing transaction-time stamp, and a query can read as of any past stamp. The history is queryable, not overwritten.

What to read in chronicle.ar

A Person carries a mutable age, and Adult is the iff-refinement that classifies anyone 18 or older:

pub type Person { mut age: Int }
pub type Adult <: Person iff { self.age >= 18 };

Two declared queries pin the same Adult extent to two past transaction-times — the surface as_of <int> clause is the whole point:

pub query current_adults() -> Adult;          // latest snapshot
pub query adults_at_2()    -> Adult as_of 2;   // right after the hire
pub query adults_at_4()    -> Adult as_of 4;   // right after set_age

The driver routes a query carrying as_of through the time-travel read path automatically; the modeler never touches the runtime API.

Running it

The demo.toml scenario hires alice as a minor (age 12), then later sets her age to 25. Each mutation advances transaction-time, so the same Adult query gives different answers at different stamps:

query chronicle::adults_at_2:   0 row(s)        — alice is 12 here, not an Adult
query chronicle::adults_at_4:   1 row(s)  alice — alice is 25 here, now an Adult
query chronicle::current_adults: 1 row(s) alice — latest state agrees with tx=4

The decisive contrast is adults_at_2 vs adults_at_4: it is one query against one individual, but the answer flips from empty to {alice} purely because the read snapshot moved past the set_age event. The refinement is re-evaluated against the field value as of each instant.

Honest caveats (what runs today)

• v0 admits only integer literals as the as_of argument (a raw transaction-time stamp). Forms like as_of now() - 1 day or a parameterized argument are reserved for a later RFD.
• This is the transaction-time axis (when the system learned a fact). The valid-time axis — when a fact is true in the modelled world — is shown in effective_dated_tax_v0, which reads as_of <#date#>.

This example is compiled and run in CI; its as_of snapshot behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the time-travel surface 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

//! Bitemporal time-travel via SURFACE syntax (`as_of <int>`).

mod chronicle;

chronicle.ar

//! Bitemporal time-travel via SURFACE syntax (`as_of <int>`).
//!
//! Demonstrates the surface-level half of the temporal wall. The
//! runtime API (`Store::query_extent_as_of`) was opened in a prior
//! commit; this example uses the modeler-facing `as_of` clause:
//!
//!   pub query at_t1() -> Adult as_of 2;
//!   pub query at_t3() -> Adult as_of 3;
//!
//! Driver dispatch routes through `query_extent_as_of` automatically
//! based on the `as_of_tx_nanos` field stamped on the QueryDecl.
//!
//! V0.1 admits only integer literals as `as_of` arguments. Future
//! RFDs may add `as_of now() - 1 day` or parameterized form.

pub type Person {
    mut age: Int,
}

pub type Adult <: Person iff { self.age >= 18 };

pub mutate hire(p: Person, age: Int) {
    insert iof(p, Person);
    update p: Person set { age = age }
}

pub mutate set_age(p: Person, age: Int) {
    update p: Person set { age = age }
}

// ANCHOR: as_of_queries
// Latest snapshot — the current Adult extent.
pub query current_adults() -> Adult;

// Snapshot at tx=2 (right after the hire).
pub query adults_at_2() -> Adult as_of 2;

// Snapshot at tx=4 (right after set_age).
pub query adults_at_4() -> Adult as_of 4;
// ANCHOR_END: as_of_queries

Effective dating: which rate is in force on a date

Area: Bitemporal time Teaches: the valid-time axis — insert iof(…) at #date# writes a fact whose effectivity begins on a civil date, and as_of <#date#> reads which facts were in force on a given day. This is distinct from (and composable with) the transaction-time as_of <int> of temporal_as_of_surface. Prerequisites: as_of time-travel, and first-class relations. Run: ox build examples/effective_dated_tax_v0 && ox run-scenario examples/effective_dated_tax_v0

“What was the standard tax rate on 2024-04-15?” is a valid-time question: it asks what was true in the world on that day, not what the system happened to know at some processing instant. Hand-rolling an effectiveFrom: Date field forces every query to re-implement interval logic. Argon puts effectivity on the substrate: an enactment is written at its effective date, and a date-stamped as_of read projects the rates in force.

What to read in tax.ar

StandardRate is “the standard rate in force”; each enactment is one individual, and its value rides on a rate relation tuple. The enactment writes both at the effective date, so before that date neither holds:

pub type StandardRate;
pub rel rate(r: StandardRate, pct: Decimal);

pub mutate enact(r: StandardRate, pct: Decimal, effective: Date) {
    insert iof(r, StandardRate) at effective;
    insert rate(r, pct) at effective;
}

The queries read the valid-time axis with a date-literal as_of:

pub query rate_on_2023_06_01() -> StandardRate as_of #2023-06-01#;
pub query rate_on_2024_04_15() -> StandardRate as_of #2024-04-15#;
pub query rate_on_2025_06_01() -> StandardRate as_of #2025-06-01#;
pub query rate_now()           -> StandardRate;

Running it

The demo.toml enacts three rates — 20% effective 2020-01-01, 22% effective 2024-01-01, 19% effective 2025-01-01 — passing the Date and Decimal arguments in their exact table forms ({ date = "…" }, { decimal = "…" }). Each date-stamped query then projects the rates whose valid-time has begun by that day:

query tax::rate_on_2023_06_01:  1 row(s)   — only the 2020 rate has begun
query tax::rate_on_2024_04_15:  2 row(s)   — 2020 + 2024 are both in force by a 2024 filing
query tax::rate_on_2025_06_01:  3 row(s)   — 2020 + 2024 + 2025
query tax::rate_now:            3 row(s)   — every begun rate (valid = now)

The decisive contrast is rate_on_2023_06_01 vs rate_on_2024_04_15: the same query shape, two civil dates, and the row count rises from 1 to 2 because the 2024 enactment’s valid-time interval opens between them. A rate enacted at #2024-01-01# is invisible to a 2023 read and visible to a 2024 read — the effectivity is enforced by the substrate, not by a where clause in the query.

Honest caveats (what runs today)

• The rate table is append-only in this v0: each enactment opens a valid-time interval but does not close the prior one, so a later date sees all begun rates accumulated (hence 3 rows in 2025), not only the single rate that superseded. Closing the prior interval (so a date sees exactly one rate) is the during / bitemporal-retraction follow-on.
• Date arguments use the { date = "…" } table form (a bare string parses as an individual); Decimal arguments use { decimal = "…" }, parsed exactly rather than through a float.
• This is the valid-time axis (true-in-the-world). It composes with — and is distinct from — the transaction-time axis of temporal_as_of_surface (when the system learned a fact).

This example is compiled and run in CI; its valid-time as_of <#date#> round-trip is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the effective-dating surface 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

//! Effective-dated tax rates — the temporal substrate end-to-end (arc5).
//!
//! A tax model cannot ask "what rate was in effect on 2024-04-15" without
//! valid-time. This package is the living proof that it now can:
//!
//!   * each rate is enacted `at #date#` — a bitemporal VALID-time assertion
//!     (RP-004 §7.5), not a hand-rolled `effectiveFrom: Date` field;
//!   * `as_of <#date#>` queries read the VALID-time axis — "what was valid
//!     at VT = t" — distinct from and composable with the transaction-time
//!     `as_of <int>` axis (RP-004 §6/§15).
//!
//! The `mod` indirection (rather than a flat `root.ar`) keeps the qualified
//! mutation/query paths stable (`tax::…`) instead of the `<anonymous>::…`
//! single-file trap.

mod tax;

tax.ar

//! The effective-dated rate table.
//!
//! `StandardRate` is the concept of "the standard income-tax rate in force".
//! Each enactment introduces a fresh `StandardRate` individual whose VALID
//! time begins on the day the statute took effect — `insert iof(r, StandardRate)
//! at #date#`. The runtime threads that `at <date>` onto the event's bitemporal
//! valid-time extent (RP-004 §7.5), so an `as_of <#date#>` query projects the
//! rate(s) in force on that civil day.
//!
//! The rate's numeric value rides on a `rate(StandardRate, Decimal)` relation
//! tuple set in the same mutation, so each enactment is one atomic step.

pub type StandardRate;

pub rel rate(mut r: StandardRate, pct: Decimal);

// ANCHOR: enact
/// Enact a new standard rate, effective from `effective` (a `#date#`).
/// The membership AND the rate value both take the valid-time of the
/// enactment: before `effective` the rate did not hold.
pub mutate enact(r: StandardRate, pct: Decimal, effective: Date) {
    insert iof(r, StandardRate) at effective;
    insert rate(r, pct) at effective;
}
// ANCHOR_END: enact
// ── Valid-time time-travel queries (the effective-dating wall) ──
//
// "Which standard rate(s) were in force on <date>?" Each reads the VALID-time
// axis via `as_of <#date#>`. A rate enacted `at #2024-01-01#` is invisible to
// an `as_of #2023-…#` read and visible to an `as_of #2024-…#` read.
// ANCHOR: valid_time_queries
/// The rate(s) in force in mid-2023 — before the 2024 enactment.
pub query rate_on_2023_06_01() -> StandardRate as_of #2023-06-01#;

/// The rate(s) in force on a 2024 filing day — after the 2024 enactment.
pub query rate_on_2024_04_15() -> StandardRate as_of #2024-04-15#;
// ANCHOR_END: valid_time_queries
/// The rate(s) in force in 2025 — after the 2025 enactment supersedes.
pub query rate_on_2025_06_01() -> StandardRate as_of #2025-06-01#;

/// The latest believed snapshot (VALID = now): every enacted rate whose
/// valid-time has begun is visible (the table is append-only here).
pub query rate_now() -> StandardRate;

Time-travel: a refinement’s verdict changes over time

Area: Bitemporal time Teaches: how an iff-refinement composes with bitemporal time-travel — as a field rises across transaction-time, the individual’s membership in the refinement changes per snapshot. The classifier is re-run against the field value as of each instant. Prerequisites: as_of time-travel, and refinement (iff). Run: ox build examples/temporal_promotion && ox run-scenario examples/temporal_promotion

In temporal_as_of_surface the query moved through time. Here the classification moves: an employee crosses a threshold, and the refinement that depends on that field flips from non-member to member — but only for snapshots taken after the crossing.

What to read in hr.ar

FullTime is the iff-refinement over an employee’s weekly hours:

pub type Employee { mut weekly_hours: Int }
pub type FullTime <: Employee iff { self.weekly_hours >= 35 };

pub query all_employees() -> Employee;
pub query full_timers()   -> FullTime;

There is no as_of on these declared queries; the time-travel here is driven by the --as-of flag on ox query, which reads the FullTime extent visible at a chosen transaction-time.

Running it

The demo.toml scenario hires alice at 20 hours/week (below the threshold), then promotes her to 40. The latest snapshot has her full-time:

$ ox run-scenario examples/temporal_promotion
query hr::all_employees: 1 row(s)  alice
query hr::full_timers:   1 row(s)  alice      — 40 >= 35 in the latest state

Travel back, and the verdict flips. The same FullTime extent, read at different transaction-times:

$ ox query examples/temporal_promotion --extent hr::FullTime --as-of 1
extent(hr::FullTime as_of 1): 0 individual(s)             — alice still at 20h, not FullTime

$ ox query examples/temporal_promotion --extent hr::FullTime --as-of 100
extent(hr::FullTime as_of 100): 1 individual(s)  alice    — past the promotion, 40 >= 35

The decisive contrast is --as-of 1 vs --as-of 100: one individual, one refinement, two snapshots — empty before the promotion, {alice} after. The field value is read as of the same instant the membership is evaluated (the latest property assertion with tx_from <= tx wins per field), so the iff classifier sees 20 in the past and 40 in the present.

Honest caveats (what runs today)

• --as-of takes a transaction-time stamp as an integer. A stamp before any event (--as-of 1) reads the pre-promotion state; a large stamp (--as-of 100) reads the latest.
• The --as-of flag lives on ox query; ox run-scenario prints the latest snapshot for the declared queries.

This example is compiled and run in CI; the corpus test (oxc-runtime/tests/examples_corpus.rs::corpus_temporal_promotion_full_time_eligibility_changes_over_time) pins exactly this — the FullTime extent differing across transaction-time as the hours rise — so the refinement-over-time composition can’t drift.

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

//! Bitemporal time-travel queries.

mod hr;

hr.ar

//! Bitemporal time-travel queries.
//!
//! An employee's eligible status changes as their hours go up over
//! time. The refinement `FullTime <: Employee iff { hours >= 35 }`
//! evaluates per-snapshot.
//!
//! Demonstrates:
//!   * Bitemporal substrate: every mutation-emitted event gets a
//!     monotonic transaction-time stamp
//!   * Time-travel queries: `Store::query_extent_as_of(tx)` returns
//!     the extent visible at a given transaction-time
//!   * Refinement composition with bitemporal: field values are
//!     read AS OF the same instant (latest property assertion
//!     with `tx_from <= tx_nanos` wins per field)
//!
//! Expected runtime behavior:
//!   * After hire(alice, 20): `FullTime` extent = {}     (alice at 20h)
//!   * After update(alice, 40): `FullTime` extent = {alice}
//!   * Time-travel: `query_extent_as_of(t_before_update)` returns {}
//!   * Time-travel: `query_extent_as_of(t_after_update)` returns {alice}

pub type Employee {
    mut weekly_hours: Int,
}

pub type FullTime <: Employee iff { self.weekly_hours >= 35 };

pub mutate hire(p: Employee, hours: Int) {
    insert iof(p, Employee);
    update p: Employee set { weekly_hours = hours }
}

pub mutate promote(p: Employee, hours: Int) {
    update p: Employee set { weekly_hours = hours }
}

pub query all_employees() -> Employee;
pub query full_timers() -> FullTime;

Modal operators: box

Area: Modal operators Teaches: the necessity (box) operator in a rule body, and the fixed-introduction discharge — over a type whose introducing metatype is fixed, box(P) reduces to P at the current world (box_fixed_discharge). The classifier promotes a rule carrying a modal operator to tier:modal. Prerequisites: concepts, metatypes (the fixed modifier), and derive rule bodies (see first-class relations). Run: ox build examples/modal_box_diamond && ox derive examples/modal_box_diamond necessarily_eligible — this reads the empty store (0 tuple(s)); construct a citizen first to see the discharge (see Running it).

Modal logic distinguishes what must hold from what may hold. box(P) reads “necessarily P” — P at every accessible world; diamond(P) reads “possibly P” — P at some accessible world. Argon exposes both as operators usable inside a rule body.

The engine performs exactly one sound reduction: the forward-rigidity discharge box(x : T) → x : T when T is introduced by a fixed metatype. Fixed classification is decided at construction and never changes, so a fixed-member is a member at every accessible world — necessity and plain membership coincide. Everything else is refused (OE1104) rather than silently stripped to the inner atom (which would be a wrong answer for anti-rigid or dynamic classification):

• diamond is not discharged, even over a fixed type. Under the open-world assumption a current non-member could be constructed into the fixed type in a reachable world, so diamond(x:T) can hold where x:T is currently false — reducing it to x:T would under-derive. There is no diamond_fixed_discharge theorem, so diamond is refused.
• A box over a non-fixed type (whose membership can change across worlds), a box(not (x:T)) (a fixed type discharges necessary membership, never necessary non-membership — the polarity is asymmetric), and any standpoint-frame modal are all refused too.

The standpoint-frame translation and the tableau model engine over a Kripke carrier are future work; until they land the refusal holds the place soundly. This example therefore demonstrates the one case that runs today: box over a fixed type.

What to read in governance.ar

One fixed-introduced (frame-rigid) type, wrapped in box:

pub fixed metatype status = { };

pub status Citizen;

pub derive necessarily_eligible(p) :- box(Citizen(p));

box(Citizen(p)) discharges to p: Citizen because Citizen is introduced by the fixed metatype status. The classifier promotes the rule to tier:modal, and the build admits it. (A diamond(Citizen(p)) rule would be refused with OE1104.)

A mutation mints the citizens, and a query reads the modal derive:

pub mutate register() -> Citizen {
    let c = insert Citizen { };
    c
}

pub query who_necessarily_eligible() -> necessarily_eligible;

Because Citizen is fixed-introduced, membership is decided at construction — register constructs a citizen (an insert iof(p, Citizen) re-classification would be refused, OE0234). That is exactly what makes the discharge sound: a citizen is a citizen at every accessible world.

Running it

The package ships no seed facts, so against the empty store the derive is empty:

$ ox derive examples/modal_box_diamond necessarily_eligible
derive(necessarily_eligible): 0 tuple(s)

Citizens come from register. Constructing two citizens and reading the query shows the discharge:

query who_necessarily_eligible: 2 row(s)

The query returns exactly the constructed citizens — and nothing else. That is the whole point of the fixed-introduction discharge: over a frame-rigid type, box agrees with plain membership. An individual that was never constructed as a citizen does not match, since there is no iof(_, Citizen) for the modal body to discharge against.

Honest caveats (what runs today)

• Only box over a fixed-introduced type discharges. A diamond (any frame), a box over a non-fixed type, a box(not (x:T)), or a standpoint-frame modal is refused (OE1104) rather than stripped — the full Kripke / standpoint-frame evaluator, where the operators genuinely diverge, is future work.
• The package ships no demo.toml, so a bare ox derive reads the empty store. To reproduce the rows above, construct a citizen first (the corpus test drives governance::register programmatically; from the CLI, a one-line scenario file with a [[mutate]] entry for governance::register does the same via ox run-scenario).

This example is compiled and run in CI; the fixed-introduction box discharge — matching the constructed citizens and nothing else — is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

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

//! Modal operators (`box` / `diamond`, spec §11.2).

mod governance;

governance.ar

//! Modal operators (`box`, spec §11.2).
//!
//! The necessity operator `box` over a Kripke frame. The engine
//! performs the sound forward-rigidity discharge `box(x : T) → x : T`
//! ONLY when `T` is introduced by a `fixed` metatype (§10.2: a
//! fixed-member is a member at every accessible world, so `box φ` and
//! `φ` coincide) — this is `box_fixed_discharge`, the only proven
//! reduction.
//!
//! `diamond` is NOT discharged, even over a `fixed` type: under OWA a
//! current non-member could be constructed into the fixed type in a
//! reachable world, so `diamond(x:T)` can hold where `x:T` is false —
//! reducing it to `x:T` would under-derive. So `diamond`, a `box`
//! over a non-`fixed` type, a `box(not (x:T))`, and any
//! standpoint-frame modal are all refused with OE1104 rather than
//! silently stripped to the inner atom (stripping would be a wrong
//! answer for anti-rigid / dynamic classification).
//!
//! `Citizen` is introduced by the `fixed` metatype `status`, so a
//! citizen's membership is decided at construction and never changes
//! — that is exactly what makes the `box` discharge sound.
//!
//! Demonstrates:
//!   * `box(Citizen(p))` in a rule body — necessity over a
//!     fixed-introduced (frame-rigid) type. Discharges to
//!     `p: Citizen` (always-true at every accessible world).
//!   * The classifier promotes the rule to `tier:modal`;
//!     the build admits it after the frame-aware dispatch.
//!
//! Expected runtime behavior:
//!   a constructed citizen → necessarily_eligible
//!   any other individual  → not (no matching iof)

pub fixed metatype status = { };

pub status Citizen;

// ANCHOR: modal
pub derive necessarily_eligible(p) :- box(Citizen(p));
// ANCHOR_END: modal
// `Citizen` is `fixed`-introduced: membership is decided AT
// CONSTRUCTION and never re-classified (`insert iof(p, Citizen)`
// would be the refused re-classification, OE0234). A citizen is
// minted by constructing one; the constructed individual is returned
// so a caller can read it back.
pub mutate register() -> Citizen {
    let c = insert Citizen { };
    c
}

pub query who_necessarily_eligible() -> necessarily_eligible;

Trait contracts: clause union, supertraits, and reflective dispatch

Area: Traits Teaches: the trait atom — a rule-plane trait whose per-type impl clauses union under one head (dispatch is derivation), a supertrait acting as a requires-constraint, the partial-coverage guard that excludes uncovered individuals explicitly rather than by silence, enumeration/NAF over the catalog-closed $implements relation, and a #[static] conformance check. Prerequisites: concepts and <:; derive rule bodies; the reflective meta-plane (meta, implements, specializes). Run: ox build examples/trait_contracts && ox check --codes examples/trait_contracts — and ox derive examples/trait_contracts/target/root.oxbin ServiceableKinds

A trait names a contract a type can implement. Inspectable requires a Due rule; each impl Inspectable for T supplies one clause, and the clauses union under the single Inspectable::Due head. Dispatch is not a vtable lookup — it is derivation: the reasoner fires whichever clauses match.

What to read in fleet.ar

Clause union — one head, three type-guarded clauses with per-kind thresholds:

pub trait Inspectable { derive Due(Self); }
impl Inspectable for Truck { derive Due(t: Self) :- t.hours >= 100; }
impl Inspectable for Crane { derive Due(c: Self) :- c.hours >= 50; }
impl Inspectable for Drone { derive Due(d: Self) :- d.hours >= 10; }

A supertrait is a requires-constraint (Rust’s :): impl Serviceable for T demands impl Inspectable for T, and the reflective surface closes over it — implements(t, Serviceable) entails implements(t, Inspectable). Serviceable covers only Truck and Crane; Drone is field-maintained.

The partial-coverage guard (D3.2). A bare NeedsService(a) over Asset would be OE1327 because Serviceable does not cover every kind. ShopQueue writes the dispatch-can-fail branch explicitly — uncovered drone individuals are excluded by the guard’s $implements join, never by silence:

pub derive ShopQueue(a: Asset) :-
    implements(meta(a), Serviceable),
    NeedsService(a);

Enumeration and NAF over the catalog-closed $implements — these read type names directly, with no instances:

pub derive ServiceableKinds(t) :- implements(t, Serviceable);
pub derive SelfMaintained(t)  :- specializes(t, Asset), t != Asset, not implements(t, Serviceable);

A #[static] catalog-level conformance check discharges totally at ox check. It PASSES — the three Inspectable impls cover every declared asset kind:

#[static]
pub check EveryAssetKindIsInspectable(t: TypeRef) :-
    specializes(t, Asset), t != Asset, not implements(t, Inspectable)
    => Diagnostic { severity: Severity::Error, code: "Fleet::E010", /* … */ };

Running it

ox check discharges the catalog-level conformance check and passes — every asset kind is inspectable:

$ ox check --codes examples/trait_contracts
ok

The catalog-closed reflective derives need no instances, so ox derive reads them straight off the type catalog:

$ ox derive examples/trait_contracts/target/root.oxbin ServiceableKinds
derive(ServiceableKinds): 2 tuple(s)
  (fleet::Truck)
  (fleet::Crane)

$ ox derive examples/trait_contracts/target/root.oxbin SelfMaintained
derive(SelfMaintained): 1 tuple(s)
  (fleet::Drone)

ServiceableKinds = {Truck, Crane} (the free-t enumeration over implements(t, Serviceable)); SelfMaintained = {Drone} (the NAF complement). Once individuals are registered, InspectionQueue collects every asset past its kind’s threshold (truck 100h / crane 50h / drone 10h — the Inspectable cover is total), while ShopQueue admits only the guard-covered and clause-satisfying ones (the worn truck, the flagged crane) — never a drone, even a worn one: its dispatch fails visibly through the guard.

Honest caveats (what runs today)

• The package has no demo.toml, and the instance-driven derives (Due, InspectionQueue, ShopQueue) need registered individuals — ox derive over the bare artifact shows them empty. The catalog-closed reflective derives (ServiceableKinds, SelfMaintained) are the part demonstrable straight from the CLI; the instance-driven extents are pinned by the corpus test, which seeds via the register_* mutations.
• To see the failing conformance variant, retarget the check at Serviceable (commented in fleet.ar): Drone implements no Serviceable, so ox check fails with Fleet::E010 before any artifact is written.

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the clause-union InspectionQueue, the D3.2-guarded ShopQueue (truck + crane, never a drone), ServiceableKinds = {Truck, Crane}, SelfMaintained = {Drone}, and the check’s catalog-level classification, so the trait surface 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

//! # Trait contracts — clause union, `implements`, and static conformance
//!
//! A single-module fleet-maintenance package exercising the full RFD 0026
//! trait surface as of slice 2:
//!
//!   * a **multi-impl rule-plane trait** (`Inspectable::Due`) whose per-type
//!     clauses union under one head — dispatch is derivation;
//!   * a **supertrait** (`Serviceable: Inspectable`) acting as a
//!     requires-constraint, and its logical consequence in the reflective
//!     surface (`implements(t, Serviceable) → implements(t, Inspectable)`);
//!   * the **D3.2 partial-coverage guard**: `ShopQueue` calls a member of a
//!     trait that does NOT cover every Asset kind, made legal by the visible
//!     `implements(meta(a), Serviceable)` conjunct — uncovered individuals
//!     are excluded by the guard, never by silence;
//!   * **enumeration** over the catalog-closed `$implements` relation (free
//!     type position) and **NAF** over it;
//!   * a **`#[static]` catalog-level conformance check** that discharges at
//!     `ox check` (RFD 0025 D1 as amended: `TypeRef`/`TraitRef` vocabulary).
//!
//! The metatypes are declared in-package (`category`/`kind` are ordinary
//! `pub metatype` declarations, not language surface). `category` is
//! declared `abstract` (RFD 0027 D6) — the substrate-neutral modifier is
//! what exempts `Asset` from needing a covering impl of its own (no direct
//! instances ⇒ no coverage obligation); the package's sortality axis is
//! its own ontological vocabulary, inert to the compiler.

mod fleet;

fleet.ar

//! Fleet maintenance under trait contracts.
//!
//! ## The contracts
//!
//! `Inspectable` covers EVERY asset kind (three impls — clause union with
//! per-kind thresholds), so the bare member atom in `InspectionQueue` passes
//! the coverage gate outright. `Serviceable` covers only `Truck` and `Crane`
//! — `Drone` is field-maintained — so a bare `NeedsService(a)` over `Asset`
//! would be OE1327; `ShopQueue` writes the dispatch-can-fail branch
//! explicitly with the `implements(meta(a), Serviceable)` guard (RFD 0026
//! D3.2): drone individuals are excluded by the guard's `$implements` join,
//! never by silence.
//!
//! ## Expected behavior (pinned by the corpus test)
//!
//!   * `Due` / `InspectionQueue` — every registered asset past its kind's
//!     inspection threshold (truck 100h, crane 50h, drone 10h);
//!   * `ShopQueue` — only covered+satisfying individuals: the worn truck
//!     (mileage ≥ 10000) and the flagged crane; never a drone;
//!   * `ServiceableKinds` — free-variable enumeration of the catalog-closed
//!     `$implements` relation: exactly {Truck, Crane};
//!   * `SelfMaintained` — NAF over `$implements`: exactly {Drone};
//!   * `EveryAssetKindIsInspectable` — a `#[static]` conformance check whose
//!     vocabulary is all reflective-sorted (`TypeRef` variable, `specializes`
//!     + `implements` atoms), so it discharges totally at `ox check` — and
//!     PASSES (the three Inspectable impls cover every kind).
//!
//! To see the failing variant, retarget the check at `Serviceable` (comment
//! below): `Drone` implements no `Serviceable`, so `ox check` fails with
//! `Fleet::E010` before any artifact is written.

// The sortality axis is the package's own ONTOLOGICAL vocabulary — the
// compiler never reads it (RFD 0027 D6). The substrate behavior comes
// from the `abstract` modifier on `category`: abstract types admit no
// direct instances, so the OE1327 coverage gate exempts `Asset` itself
// and quantifies over its non-abstract kinds.
pub metaxis sortality for metatype { sortal, non_sortal };

pub abstract metatype category = { sortality: non_sortal };
pub metatype kind = { sortality: sortal };

pub category Asset {
    mut hours: Int,
    mut flagged: Bool,
}

pub kind Truck <: Asset {
    mut mileage: Int,
}
pub kind Crane <: Asset;
pub kind Drone <: Asset;

// ANCHOR: trait_union
/// Every asset kind must be inspectable — the package-wide obligation.
pub trait Inspectable {
    derive Due(Self);
}

/// Shop-serviceable kinds. A supertrait (requires-constraint, Rust's `:`):
/// an `impl Serviceable for T` demands `impl Inspectable for T` — and the
/// reflective surface closes over it: `implements(t, Serviceable)` entails
/// `implements(t, Inspectable)`.
pub trait Serviceable : Inspectable {
    derive NeedsService(Self);
}

// Clause union: one head (`Inspectable::Due`), three type-guarded clauses
// with per-kind thresholds. Dispatch is derivation.
impl Inspectable for Truck {
    derive Due(t: Self) :- t.hours >= 100;
}
impl Inspectable for Crane {
    derive Due(c: Self) :- c.hours >= 50;
}
impl Inspectable for Drone {
    derive Due(d: Self) :- d.hours >= 10;
}
// ANCHOR_END: trait_union
// Partial coverage BY DESIGN: drones are field-maintained.
impl Serviceable for Truck {
    derive NeedsService(t: Self) :- Due(t), t.mileage >= 10000;
}
impl Serviceable for Crane {
    derive NeedsService(c: Self) :- Due(c), c.flagged == true;
}

/// Fully covered bare member atom — no guard needed (D3.1).
pub derive InspectionQueue(a: Asset) :- Due(a);

/// Partially covered member atom under the explicit D3.2 conformance
/// guard: fires only for individuals SOME classifier of which is covered
/// (existential over the multi-valued `meta`, §12.4) AND whose clause
/// body holds.
pub derive ShopQueue(a: Asset) :- implements(meta(a), Serviceable), NeedsService(a);

/// Free-variable enumeration over `$implements` (the OE0212 exemption):
/// which declared types carry the Serviceable contract?
pub derive ServiceableKinds(t) :- implements(t, Serviceable);

/// NAF over the catalog-closed `$implements` — stratification-safe:
/// asset kinds that do NOT carry the Serviceable contract.
pub derive SelfMaintained(t) :- specializes(t, Asset), t != Asset, not implements(t, Serviceable);

/// Catalog-level conformance check (RFD 0025 D1 as amended by RFD 0026
/// D6: every variable reflective-sorted — `TypeRef` here; `specializes` /
/// `implements` vocabulary). Discharges totally and finally at
/// `ox check` / `ox build`; `#[static]` makes instance-vocabulary drift a
/// hard error (OE1322) instead of a silent reclassification. PASSES: the
/// three Inspectable impls cover every declared asset kind.
// ANCHOR: static_conformance
#[static]
pub check EveryAssetKindIsInspectable(t: TypeRef) :-
    specializes(t, Asset),
    t != Asset,
    not implements(t, Inspectable) => Diagnostic {
        severity: Severity::Error,
        code: "Fleet::E010",
        message: format!("{} must implement Inspectable", t)
    };
// ANCHOR_END: static_conformance
// The FAILING variant — retarget the obligation at Serviceable and the
// check fires on Drone at `ox check` (Fleet::E010, build refused):
//
// #[static]
// pub check EveryAssetKindIsServiceable(t: TypeRef) :-
//     specializes(t, Asset), t != Asset,
//     not implements(t, Serviceable)
//     => Diagnostic {
//         severity: Severity::Error,
//         code: "Fleet::E010",
//         message: format!("{} must implement Serviceable", t),
//     };
pub mutate register_truck(x: Truck, hours: Int, mileage: Int) {
    insert iof(x, Truck);
    update x: Truck set { hours = hours, mileage = mileage, flagged = false }
}

pub mutate register_crane(x: Crane, hours: Int, flagged: Bool) {
    insert iof(x, Crane);
    update x: Crane set { hours = hours, flagged = flagged }
}

pub mutate register_drone(x: Drone, hours: Int) {
    insert iof(x, Drone);
    update x: Drone set { hours = hours, flagged = false }
}

assert rejects: unit-testing that a constraint refuses bad data

Area: Testing Teaches: the negative-enforcement half of the test atom. Argon is a constraint language, so a model’s most important property is which writes its invariants turn away — assert rejects { … } runs a write block against an isolated world and PASSes when the write is refused. An optional (Pkg::Code) pins the exact rejecting code. Prerequisites: refinement (where invariants); check constraints (delta guards). Run: ox test examples/assert_rejects_v0

The positive test forms — assert <expr> and assert [not] derivable — say what a model accepts or derives. They cannot say what it refuses. assert rejects { <writes> } is the missing half: it runs its block against an isolated copy of the test world, and a write-path guard rejection is a PASS (the rejected transaction commits nothing). An accepted write FAILs; a non-guard error — a typo, an unbound name — ERRORs loudly and never masquerades as a passing rejection.

What to read

The constraints under test in model.ar: a where-invariant concept (membership asserted, balance >= 0 enforced at the write with OE0668) and a check delta-guard (a new over-100t truck refused with Fleet::E001):

pub type Solvent <: Account where { self.balance >= 0 };

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

The tests in tests/mod.ar exercise each rejection mode. A where-invariant violation, a code-pinned check rejection, the same rejection without a pin, and a legal write that must NOT satisfy a rejection assertion:

test "a negative balance is rejected by the where-invariant" {
    let a = insert Solvent { balance: 100 };
    assert rejects { update a: Account set { balance = -50 } };
}

test "an overweight truck is rejected by its check, by code" {
    assert rejects(Fleet::E001) { let t = insert Truck { weight: 200 }; };
}

test "a within-limit balance is accepted" {
    let a = insert Solvent { balance: 100 };
    update a: Account set { balance = 50 };
    assert a.balance == 50;        // the positive form tests an accepted write
}

Running it

ox test discovers every test "name" { … } block, runs each against a fresh store, and reports pass/fail/error (it exits non-zero if any fails or errors — CI-usable):

$ ox test examples/assert_rejects_v0
PASS  a negative balance is rejected by the where-invariant
PASS  an overweight truck is rejected by its check, by code
PASS  an overweight truck is rejected by its check
PASS  a within-limit balance is accepted

4 passed, 0 failed, 0 errored, 0 inconclusive

The decisive contrast is the last test against the first three: setting a Solvent account to -50 is refused by the where-invariant (so assert rejects passes), but setting it to 50 is accepted — and an accepted write is tested with the positive assert a.balance == 50, never with assert rejects. The code-pinned variant passes only on its exact code: assert rejects(Fleet::E001) would FAIL, not pass, if the write were turned away by some other guard.

Honest caveats (what runs today)

• assert rejects is satisfied by a write-path guard rejection (a where-invariant OE0668 or a check delta-guard). A non-guard error inside the block (an unbound name, a type error) is an ERROR, not a PASS — the form does not let a broken test launder itself into a green rejection.
• Each block runs against an isolated copy of the test world, so a rejected transaction leaves no residue for the next test.

This example is compiled and run in CI; a CLI test (oxc-driver/tests/cli_pipeline.rs) runs ox test examples/assert_rejects_v0 and asserts it stays green, and a companion test pins that the test runner classifies every outcome (pass / fail / error), so the negative-enforcement surface 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

//! `assert rejects { … }` — unit-testing that a constraint REFUSES bad data
//! (§17.14). Argon is a constraint language: a model's most important property
//! is which writes its `where`-invariants and `check` delta-guards turn away.
//! The positive assertion forms (`assert <expr>`, `assert [not] derivable`)
//! cannot express that; `assert rejects` is the negative-enforcement half.
//!
//! Each `assert rejects { <writes> }` runs its block against an ISOLATED copy
//! of the test world. A write-path guard rejection PASSes (the rejected
//! transaction commits nothing); an optional `(Pkg::Code)` pin PASSes only on
//! that exact code; an accepted write FAILs; and a non-guard error (a typo, an
//! unbound name) ERRORs loudly — it never masquerades as a passing rejection.
//!
//! All concepts use the neutral `pub type` introducer — no ontological
//! commitment lives in the language.

mod model;
mod tests;

model.ar

//! The constraints under test.

// A primitive (`where`) concept: membership is asserted, and `balance >= 0` is
// a necessary invariant checked at the write — a violating write is refused
// with OE0668.
pub type Account {
    mut balance: Int,
}

pub type Solvent <: Account where { self.balance >= 0 };

// A `pub check` delta-guard: a write that creates a new `Truck` over the 100t
// limit is refused atomically with the coded `Fleet::E001`.
pub type Truck {
    mut weight: Int,
}

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)
    };

tests/mod.ar

use super::model::{ Account, Solvent, Truck };

// ANCHOR: rejects_tests
// A `where`-invariant rejection: setting a Solvent account below zero violates
// the necessary invariant `balance >= 0`, so the write is refused (OE0668).
test "a negative balance is rejected by the where-invariant" {
    let a = insert Solvent { balance: 100 };
    assert rejects {
        update a: Account set { balance = - 50 }
    };
}

// A `check` delta-guard rejection, with the rejecting code pinned: a 200t
// truck creates an OverweightTruck violation, refused with `Fleet::E001`.
test "an overweight truck is rejected by its check, by code" {
    assert rejects(Fleet::E001) {
        let t = insert Truck { weight: 200 };
    };
}
// ANCHOR_END: rejects_tests
// The same rejection without a code pin — any guard rejection satisfies it.
test "an overweight truck is rejected by its check" {
    assert rejects {
        let t = insert Truck { weight: 200 };
    };
}

// A legal write within the invariant is ACCEPTED, so it does not satisfy a
// rejection assertion. The positive form (`assert a.balance == 50` after the
// update) is how you test an accepted write — not `assert rejects`.
test "a within-limit balance is accepted" {
    let a = insert Solvent { balance: 100 };
    update a: Account set { balance = 50 };
    assert a.balance == 50;
}

Residential lease: a breach / fulfillment calculus

Area: Capstone Teaches: the worked, end-to-end legal model — a UFO-L deontic theory of a residential lease where concepts, first-class relations, refined collections, mod structure, cumulative aggregation, and recursion-through-negation rules combine to decide, per obligation, whether it is breached or fulfilled as of a date. The capstone of the corpus. Prerequisites: first-class relations, refined collections and from-fields (see refined collections), derive rule bodies with aggregates and negation, and the in-package vocabulary pattern (pub metatype, see legal vocabulary). Run: ox build examples/residential_lease_breach && ox run-scenario examples/residential_lease_breach

This is the example the rest of the corpus builds toward. The others isolate one idea — a relation carries data, a #[defeats] plane resolves a conflict, a check reads a warranted extent. Here those ideas carry a single working legal model: a residential lease, transcribed faithfully from a propositional-content theory in the UFO-L tradition of Griffo/Guizzardi. The question the model answers is the one a lease actually poses — given what was owed, what was paid, and what day it is, which obligations are in breach? — and it answers it by running, not by hand-waving.

The package is two modules: root.ar (mod lease;) and lease.ar, which holds the whole hierarchy, the calculus, the seeding mutations, and the queries.

The UFO vocabulary is declared in-package, not built in

UFO’s classifiers are not Argon language surface. Even the std::core baseline type/rel is opt-in — this package’s ox.toml lists them in its prelude (RFD 0038 D4; the baseline is no longer ambient). A category/kind/relator introducer then resolves against pub metatype declarations visible in scope — an introducer with no visible declaration is refused (OE0605). The example declares the three UFO metatypes it uses locally — the external-vocabulary-package pattern, where a real UFO package authored with the UFO authors would ship these and be imported instead:

pub metatype category = { };   // a rigid non-sortal classifier
pub metatype kind     = { };   // a rigid sortal supplying an identity principle
pub metatype relator  = { };   // the truth-maker of material relations

Everything downstream is vocabulary, not keyword: pub category Endurant;, pub kind Person <: LegalAgent { name: String }, pub relator CorrelativePositionPair <: LegalRelator { … }. The compiler never reads the word “category” as special — it reads a metatype declared one screen up.

What to read in lease.ar

Cumulative tracking is built from records, accounts, and a book. A Record carries a value and a closed day-window [startsOn, endsOn]. An expected record says what is owed in a period; a satisfaction record says what was performed. An account holds records as a refined collection navigated through a relation — the from recordInAccount.range field is the collection of records reachable across that relation:

pub category Record { mut value: Real, mut startsOn: Int, mut endsOn: Int }
pub category RecordAccount { records: [Record] from recordInAccount.range }
pub rel recordInAccount(account: RecordAccount, record: Record);

A CorrelativePositionBook separates the two sides through bookExpectedAccount and bookSatisfactionAccount, so the calculus can compare what is owed against what was realized.

Legal positions are Hohfeldian relators. A right–duty pair is the truth-maker that links an advantaged holder, a burdened holder, the tracking book, and the propositional content that supplies its legal meaning. For rent the landlord is advantaged, the tenant burdened:

pub relator CorrelativePositionPair <: LegalRelator {
    advantageHolder: LegalAgent,
    burdenHolder: LegalAgent,
}
pub relator RightDutyPair <: CorrelativePositionPair;

The propositional content hierarchy is a named cover. The = A | B | … transcribes the source theory’s partition blocks — the alternatives are disjoint and exhaustive. A content is either an occurrence-referring content (positive or negative), a conditional, a conjunction, or a disjunction:

pub category PropositionalContent =
    OccurrenceReferringPropositionalContent |
    ConditionalPropositionalContent |
    Conjunction |
    Disjunction

Positive content is fulfilled by matching satisfaction (rent paid); negative content by the absence of a forbidden occurrence (no subletting). Conjuncts and disjuncts are collection slots filled by navigation over the pairing relations:

pub category Conjunction <: PropositionalContent {
    conjunct: [PropositionalContent] from conjunctOf.range
}

The calculus is the set of derive rules. An expected record is Met when the cumulative realized value in its satisfaction account covers the expected value — a sum aggregate over the navigated collection:

pub derive Met(e: ExpectedSatisfactionRecord) :-
    recordInAccount(expectedAccount, e),
    bookExpectedAccount(book, expectedAccount),
    bookSatisfactionAccount(book, satisfactionAccount),
    e.value <= sum(r.value for r in satisfactionAccount.records);

Breach is as of an instant. PastCurrent(e, t) holds when e’s window has closed on or before t (the obligation is due, so non-satisfaction now counts). Positive content is breached as of t when a past-due expected record is not Met — negation over the aggregate-defined Met:

pub derive BreachedAt(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
    contentBook(pc, book),
    bookExpectedAccount(book, expectedAccount),
    recordInAccount(expectedAccount, e),
    PastCurrent(e, t),
    not Met(e);

Fulfillment is the negation of breach, and composition is per the deontic logic. Positive content is fulfilled as of t when it is not BreachedAt; a conjunction is breached when any conjunct is breached (existential), and a disjunction is fulfilled when at least one disjunct is fulfilled:

pub derive Fulfilled(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
    PositiveOccurrencePropositionalContent(pc), Instant(t), not BreachedAt(pc, t);

pub derive BreachedAt(conj: Conjunction, t: Instant) :- conjunctOf(conj, c), BreachedAt(c, t);
pub derive Fulfilled(disj: Disjunction, t: Instant) :- disjunctOf(disj, d), Fulfilled(d, t);

Each a.b.c navigation in the source theory becomes one join per hop over the relation that is that navigation (contentBook, bookExpectedAccount, …) — semantically identical, and how the relations materialize anyway.

Running it

The harness sets the clock to day 45 and opens three rent obligations, each €1000 due on day 31 (so all are past-due as of day 45). They differ only in what was paid, plus two composites over { rentPaid, rentUnpaid }:

rentUnpaid   paid 0           → not met → BREACHED   as of day 45
rentPaid     paid 600 + 400   → met     → FULFILLED  as of day 45
rentPartial  paid 600         → not met → BREACHED   as of day 45
bothRents    (rentPaid AND rentUnpaid)  → BREACHED   (one conjunct breached)
eitherRent   (rentPaid OR  rentUnpaid)  → FULFILLED  (one disjunct fulfilled)

ox run-scenario applies the nine mutations and reports the three query extents (individual ids elided; the subjects are named here for reading):

scenario: applied 9 mutation(s) from examples/residential_lease_breach/demo.toml
query lease::breached: 3 row(s)   — { rentUnpaid, rentPartial, bothRents } each as of `today`
query lease::fulfilled: 2 row(s)  — { rentPaid, eitherRent } each as of `today`
query lease::met: 1 row(s)        — { expPaid }  (the only fully-covered expected record)

The decisive reads: rentPartial is breached even though €600 was paid, because cumulative satisfaction (600) does not cover the expected 1000 — the sum-defined Met fails and not Met fires. rentPaid is met because 600 + 400 = 1000 covers it, so BreachedAt finds no unmet past-due record and Fulfilled (its negation) holds. And composition runs through: bothRents is breached because one conjunct (rentUnpaid) is, while eitherRent is fulfilled because one disjunct (rentPaid) is.

Honest caveats (what runs today)

The model declares more of the calculus than the v0.1 executor evaluates, and the source surfaces each residual loudly rather than approximating it silently:

• The universal halves of composition are commented out. “A conjunction is fulfilled when all conjuncts are” and its disjunction dual recurse through a forall/aggregate over the very predicate they define (Fulfilled of a conjunction counts over Fulfilled of its conjuncts). Argon evaluates a genuine restricted forall, but stratified-aggregate semantics require the aggregated predicate in a strictly-lower stratum, so ox build refuses this cycle as OE1317 (recursion through aggregation) rather than evaluating something ill-founded. The supported rephrasing is NAF double-negation (a counter-example helper, then negate it), evaluated under well-founded semantics; adopting it reshapes the rule surface and is deliberate follow-up. The existential halves — conjunction-breached, disjunction-fulfilled — are what evaluate, and the demo exercises exactly those.
• Conditional vesting is declared and admitted but not exercised by the pinned demo. A conditional’s breach depends on its guard being fulfilled, and fulfillment is not breached — a genuine recursion-through-negation cycle, inherent to the deontic logic. The stratifier now flags such SCCs and evaluates them under well-founded semantics (the Van Gelder alternating fixpoint), so the rules pass ox check verbatim; they are left commented only to keep the pinned demo extents stable. The ConditionalPropositionalContent type and its guardOf / consequentOf relations remain in the hierarchy.
• Dates are Int day-numbers. Ordering and interval comparison — all the calculus needs — are exact; day-numbers keep the example runnable because the demo harness cannot yet seed the Date primordial.
• One book per obligation period. A satisfaction account’s records all count toward its period, so Met is the cumulative sum over the account. The intra-account Allen-relation window filter (for accounts spanning many periods) needs multi-condition comprehension where, a documented residual.

This example is compiled and run in CI; its Met / BreachedAt / Fulfilled extents under cumulative aggregation, negation, and existential composition are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs) to exactly {expPaid} / {rentUnpaid, rentPartial, bothRents} / {rentPaid, eitherRent}. If the language changes underneath it, the build breaks rather than the docs going stale.

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

//! Residential-lease deontic **breach / fulfillment calculus** (UFO-L).
//!
//! When is a lease obligation *breached*? When is it *fulfilled*? This
//! example models the propositional-content calculus a residential lease
//! runs on: cumulative payment tracking, past-due detection, and the
//! logical composition of obligations (and / or / if-then).
//!
//! It is a faithful, self-contained transcription of a working legal model
//! (a residential-lease propositional-content theory in the UFO-L tradition
//! of Griffo/Guizzardi). The full hierarchy and calculus build and admit;
//! a seeded scenario (`demo.toml`) makes the core *run* — see `lease.ar`
//! for the precise modeling choices and the documented residuals.

mod lease;

lease.ar

//! # Residential-lease breach / fulfillment calculus
//!
//! A UFO-L deontic model of a residential lease, centered on the
//! *propositional-content* theory that decides, for each obligation,
//! whether it is **breached** or **fulfilled** as of a given date.
//!
//! ## What the calculus says
//!
//! An obligation is carried by a *propositional content* (`PropositionalContent`).
//! A positive occurrence content (e.g. "pay €1000 rent by the 31st") tracks an
//! **expected-satisfaction account** (what is owed, by period) and a
//! **satisfaction account** (what was actually performed). The content is:
//!
//!   * **Met** for an expected record when the cumulative realized value in its
//!     period satisfaction account covers the expected value.
//!   * **Breached** as of an instant when some past-due expected record is *not*
//!     Met (positive content), or — for prohibitions — when a forbidden record
//!     *is* Met.
//!   * **Fulfilled** as of an instant when it is not Breached.
//!
//! Obligations compose: a **Conjunction** ("A and B") is breached if *any*
//! conjunct is, fulfilled if *all* are; a **Disjunction** ("A or B") flips both;
//! a **Conditional** ("if guard then consequent") *vests* once its guard is
//! fulfilled, after which a breached consequent breaches the conditional.
//!
//! ## Modeling choices (faithful, and noted for honesty)
//!
//!   * **Dates are `Int` day-numbers.** Ordering and interval comparison — all
//!     the calculus needs — are preserved exactly; the demo harness cannot seed
//!     the `Date` primordial, so day-numbers keep the example runnable.
//!   * **Evaluation is parameterized by an `Instant`** individual carrying a
//!     `day`, rather than a free `date` variable. A derived `BreachedAt(pc, t)`
//!     binds `t` over the seeded instants — the faithful "breach *as of* a date"
//!     reading, made evaluable.
//!   * **Navigation is by relation.** Each `a.b.c` chain in the source theory is
//!     expressed as a join over the relations that *are* that navigation
//!     (`contentBook`, `bookExpectedAccount`, …) — one hop per atom. Semantically
//!     identical; it is also how the relations would be materialized anyway.
//!   * **One book per obligation period.** A satisfaction account's records all
//!     count toward that period, so `Met` is the cumulative sum over the account.
//!     The intra-account Allen-relation window filter (for accounts spanning many
//!     periods) needs multi-condition comprehension `where` — a documented
//!     residual (see "Residuals" below).
//!
//! ## Residuals (admit but do not yet *evaluate* on the v0.1 executor)
//!
//!   * **Conditional vesting** (`Vested` / conditional `BreachedAt`) closes a
//!     negation cycle `BreachedAt → Vested → Fulfilled → ¬BreachedAt`. It is
//!     declared and admitted, but requires well-founded / SLG evaluation of
//!     recursion-through-negation (RFD 0018) rather than strict stratification.
//!   * **Multi-condition / Allen-relation comprehension filters** in `Met`
//!     (issue #56). Both are surfaced *loudly* by `ox build` rather than
//!     silently approximated.

// ─────────────────────────────────────────────────────────────────────────
// UFO vocabulary (declared in-package)
//
// UFO's classifiers are NOT Argon language surface — they are package
// vocabulary (§3.4, §5.2): a concept introducer resolves against `pub
// metatype` declarations visible in scope, and only `type`/`rel` are
// ambient (from `std::core`). This example declares the three UFO
// metatypes it uses locally — the external-vocabulary-package pattern;
// a real UFO package, authored with the UFO authors, would ship these
// declarations and be imported here instead.
// ─────────────────────────────────────────────────────────────────────────

/// UFO category: a rigid non-sortal classifier.
pub metatype category = { };
/// UFO kind: a rigid sortal supplying an identity principle.
pub metatype kind = { };
/// UFO relator: the truth-maker of material relations.
pub metatype relator = { };

// ─────────────────────────────────────────────────────────────────────────
// UFO foundation (minimal)
//
// The handful of upper-ontology concepts the lease layer specializes.
// ─────────────────────────────────────────────────────────────────────────
pub category Endurant;
pub category Object <: Endurant;
pub category Agent <: Object;
pub category Aspect <: Endurant;
pub category Relator <: Aspect;

// ─────────────────────────────────────────────────────────────────────────
// Lease parties
// ─────────────────────────────────────────────────────────────────────────
/// A legally relevant agent that can hold lease positions.
pub category LegalAgent <: Agent;

/// A natural person; lease participants (landlord, tenant) are persons.
pub kind Person <: LegalAgent {
    name: String,
}

// ─────────────────────────────────────────────────────────────────────────
// Cumulative tracking: records, accounts, book
//
// A record carries a value and a closed window `[startsOn, endsOn]` (day
// numbers). Expected records say what is owed in a period; satisfaction records
// say what was performed.
// ─────────────────────────────────────────────────────────────────────────
pub category Record {
    mut value: Real,
    mut startsOn: Int,
    mut endsOn: Int,
}

/// A period-specific expected value — the owed side of cumulative fulfillment.
pub category ExpectedSatisfactionRecord <: Record;

/// A period-specific realized value — appended when a payment is performed.
pub category SatisfactionRecord <: Record;

/// A tracking account holding records, navigable as a collection through the
/// `recordInAccount` relation.
pub category RecordAccount {
    records: [Record] from recordInAccount.range,
}
// `account` is immutable: a record belongs to one account for the life of both
// individuals — it is never moved between accounts. `record` is `mut` because an
// account holds MANY records (one-to-many): each `recordPayment` adds a fresh
// record to the same satisfaction account, so this end is genuinely not
// lifetime-fixed per account (an immutable `record` end would refuse the second
// payment with OE1403).
pub rel recordInAccount(account: RecordAccount, mut record: Record);

/// Account for what is owed by period.
pub category ExpectedSatisfactionAccount <: RecordAccount;

/// Account for what has actually been performed.
pub category SatisfactionAccount <: RecordAccount;

/// The book of a correlative position pair: separates expected from realized.
pub category CorrelativePositionBook;
// Both ends immutable: the book/account binding is functional one-to-one,
// established once at `openRentObligation` and never rebound.
pub rel bookExpectedAccount(book: CorrelativePositionBook, account: ExpectedSatisfactionAccount);
pub rel bookSatisfactionAccount(book: CorrelativePositionBook, account: SatisfactionAccount);

// ─────────────────────────────────────────────────────────────────────────
// Correlative legal positions (Hohfeld)
//
// A right–duty pair links an advantaged holder, a burdened holder, a tracking
// book, and the propositional content that supplies its legal meaning.
// ─────────────────────────────────────────────────────────────────────────
pub relator LegalRelator <: Relator;
pub relator CorrelativePositionPair <: LegalRelator {
    advantageHolder: LegalAgent,
    burdenHolder: LegalAgent,
}
// Both ends immutable: a pair has one book and vice versa, bound once at
// `openRentObligation` and never rebound.
pub rel pairBook(pair: CorrelativePositionPair, book: CorrelativePositionBook);

/// A right–duty pair: for rent, the landlord is advantaged, the tenant burdened.
pub relator RightDutyPair <: CorrelativePositionPair;

// ─────────────────────────────────────────────────────────────────────────
// Propositional content hierarchy
//
// `partition` group axioms transcribe the source theory's `partition` blocks:
// the alternatives are disjoint and exhaustive (OE0242/OE0243-checked). The
// cover-body spelling (`{ A, B }` on the declaration itself) is refused
// (OE0214) until the elaborator threads it into the subkind hierarchy.
// ─────────────────────────────────────────────────────────────────────────
pub category PropositionalContent;
partition PropositionalContent {
    OccurrenceReferringPropositionalContent,
    ConditionalPropositionalContent,
    Conjunction,
    Disjunction
}

/// Content that constrains the occurrence of an event or situation. Carries the
/// tracking book whose accounts decide whether it is met.
pub category OccurrenceReferringPropositionalContent <: PropositionalContent;
partition OccurrenceReferringPropositionalContent {
    PositiveOccurrencePropositionalContent,
    NegativeOccurrencePropositionalContent
}
// Both ends immutable: the content/book binding is functional one-to-one,
// established once at `openRentObligation` and never rebound.
pub rel contentBook(
    content: OccurrenceReferringPropositionalContent,
    book: CorrelativePositionBook
);

/// Fulfilled by the presence of matching satisfaction (e.g. rent *paid*).
pub category PositiveOccurrencePropositionalContent <: OccurrenceReferringPropositionalContent;

/// Fulfilled by the *absence* of a forbidden occurrence (e.g. *no* subletting).
pub category NegativeOccurrencePropositionalContent <: OccurrenceReferringPropositionalContent;

/// "A and B": every conjunct must hold.
pub category Conjunction <: PropositionalContent {
    conjunct: [PropositionalContent] from conjunctOf.range,
}
pub rel conjunctOf(mut conjunction: Conjunction, mut conjunct: PropositionalContent);

/// "A or B": at least one disjunct must hold.
pub category Disjunction <: PropositionalContent {
    disjunct: [PropositionalContent] from disjunctOf.range,
}
pub rel disjunctOf(mut disjunction: Disjunction, mut disjunct: PropositionalContent);

/// "If guard then consequent": the consequent is owed once the guard is met.
pub category ConditionalPropositionalContent <: PropositionalContent;
pub rel guardOf(mut conditional: ConditionalPropositionalContent, mut guard: PropositionalContent);
pub rel consequentOf(
    mut conditional: ConditionalPropositionalContent,
    mut consequent: PropositionalContent
);

// ─────────────────────────────────────────────────────────────────────────
// Evaluation clock
// ─────────────────────────────────────────────────────────────────────────
/// An evaluation instant. Breach / fulfillment are computed *as of* an instant.
pub kind Instant {
    mut day: Int,
}

// ─────────────────────────────────────────────────────────────────────────
// The calculus
// ─────────────────────────────────────────────────────────────────────────
/// `e`'s expected window has closed on or before instant `t` (Allen *after* the
/// check date): the obligation is due, so non-satisfaction now counts.
pub derive PastCurrent(e: ExpectedSatisfactionRecord, t: Instant) :-
    ExpectedSatisfactionRecord(e),
    Instant(t),
    e.endsOn <= t.day;

/// `e`'s window has not closed strictly before `t` (not Allen *before* the check
/// date): for prohibitions, a forbidden satisfaction in this window still counts.
pub derive CurrentOrPastCurrent(e: ExpectedSatisfactionRecord, t: Instant) :-
    ExpectedSatisfactionRecord(e),
    Instant(t),
    e.endsOn >= t.day;

/// An expected record is **met** when the cumulative realized value in its
/// period satisfaction account covers the expected value.
pub derive Met(e: ExpectedSatisfactionRecord) :-
    recordInAccount(expectedAccount, e),
    bookExpectedAccount(book, expectedAccount),
    bookSatisfactionAccount(book, satisfactionAccount),
    e.value <= sum(r.value for r in satisfactionAccount.records);

/// Positive content is **breached** as of `t` when a past-due expected record is
/// not met.
pub derive BreachedAt(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
    contentBook(pc, book),
    bookExpectedAccount(book, expectedAccount),
    recordInAccount(expectedAccount, e),
    PastCurrent(e, t),
    not Met(e);

/// Negative (prohibition) content is **breached** as of `t` when a forbidden
/// expected record in a current-or-past window *is* met.
pub derive BreachedAt(pc: NegativeOccurrencePropositionalContent, t: Instant) :-
    contentBook(pc, book),
    bookExpectedAccount(book, expectedAccount),
    recordInAccount(expectedAccount, e),
    CurrentOrPastCurrent(e, t),
    Met(e);

/// Positive content is **fulfilled** as of `t` when it is not breached.
pub derive Fulfilled(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
    PositiveOccurrencePropositionalContent(pc),
    Instant(t),
    not BreachedAt(pc, t);

/// Negative content is **fulfilled** as of `t` when it is not breached.
pub derive Fulfilled(pc: NegativeOccurrencePropositionalContent, t: Instant) :-
    NegativeOccurrencePropositionalContent(pc),
    Instant(t),
    not BreachedAt(pc, t);

/// A conjunction is breached when *any* conjunct is breached (existential).
pub derive BreachedAt(conj: Conjunction, t: Instant) :- conjunctOf(conj, c), BreachedAt(c, t);

/// A disjunction is fulfilled when *at least one* disjunct is fulfilled (existential).
pub derive Fulfilled(disj: Disjunction, t: Instant) :- disjunctOf(disj, d), Fulfilled(d, t);

// ── Frontier: the universal halves of composition (OE1317 aggregate cycle) ──
//
// The other two composition rules are the universal duals:
//
//     pub derive Fulfilled(conj: Conjunction, t: Instant) :-
//         Conjunction(conj), Instant(t),
//         forall c: PropositionalContent where conjunctOf(conj, c), Fulfilled(c, t);
//
//     pub derive BreachedAt(disj: Disjunction, t: Instant) :-
//         Disjunction(disj), Instant(t),
//         forall d: PropositionalContent where disjunctOf(disj, d), BreachedAt(d, t);
//
// The executor DOES evaluate the restricted universal now: `forall v: T where
// Body, Head` lowers to the count-equality `count { v: Body, Head } ==
// count { v: Body }` (#129, #133), so a genuine ∀ — not an existential
// approximation — is available. What blocks THESE two rules is that they
// recurse *through* that aggregate: `Fulfilled` of a conjunction counts over
// `Fulfilled` of its conjuncts, and a conjunct may itself be a conjunction,
// so `Fulfilled` (dually `BreachedAt`) appears inside its own aggregate body.
// Stratified-aggregate semantics require the aggregated predicate in a
// strictly-lower stratum, so `ox check`/`ox build` refuse the cycle as OE1317
// RecursionThroughAggregation (#175) rather than evaluating something
// ill-founded. The supported rephrasing is NAF double negation — derive a
// counter-example helper (`HasUnfulfilledConjunct(conj, t) :-
// conjunctOf(conj, c), Instant(t), not Fulfilled(c, t);`), then
// `Fulfilled(conj, t) :- Conjunction(conj), Instant(t),
// not HasUnfulfilledConjunct(conj, t);` — recursion through negation,
// evaluated under well-founded semantics (§7.3 "Universals over recursive
// predicates", #185). Adopting it here is deliberate follow-up work (it
// reshapes the example's rule surface); admitting the forall form directly
// (structural stratification) is also tracked in #185. Until then the
// existential halves above (conjunction-breached, disjunction-fulfilled)
// evaluate and the demo exercises those.
// ── Conditional vesting (evaluable under well-founded semantics) ────────────
//
// The conditional's calculus is faithfully:
//
//     pub derive Vested(cpc: ConditionalPropositionalContent, t: Instant) :-
//         guardOf(cpc, guard), Fulfilled(guard, t);
//
//     pub derive BreachedAt(cpc: ConditionalPropositionalContent, t: Instant) :-
//         Vested(cpc, t), consequentOf(cpc, consequent), BreachedAt(consequent, t);
//
//     pub derive Fulfilled(cpc: ConditionalPropositionalContent, t: Instant) :-
//         consequentOf(cpc, consequent), Fulfilled(consequent, t);
//
// These rules close a recursion-through-negation cycle: a conditional's breach
// depends on its guard being *fulfilled*, and fulfillment is defined as *not
// breached* —
//
//     BreachedAt(cpc) → Vested(cpc) → Fulfilled(guard) → ¬BreachedAt(guard)
//
// This is inherent to the deontic logic, not an artifact of the encoding. The
// strict-stratified v0.1 evaluator used to refuse such cycles (OE1309); since
// #136 the stratifier instead flags NAF-cyclic SCCs and evaluates them under
// well-founded semantics (the Van Gelder alternating fixpoint), so these rules
// now pass `ox check` verbatim. They remain commented out only to keep this
// example's pinned demo corpus stable — enabling them is uncommenting plus
// re-pinning the expected query results in the demo harness, not reasoner
// work. (Note the cycle runs through negation, not aggregation, so OE1317 —
// recursion *through aggregation*, #175 — does not apply here.) The
// `ConditionalPropositionalContent` type and its `guardOf` / `consequentOf`
// relations remain in the hierarchy above.
// ─────────────────────────────────────────────────────────────────────────
// Seeding (the demo harness drives these — see demo.toml)
// ─────────────────────────────────────────────────────────────────────────
/// Seed the evaluation instant.
pub mutate setClock(t: Instant, day: Int) {
    insert iof(t, Instant);
    update t: Instant set { day = day }
}

/// Set up a positive occurrence obligation with its book, accounts, and a single
/// expected record (value `owed`, due on `dueDay`). `landlord`/`tenant` populate
/// the right–duty pair that carries it.
pub mutate openRentObligation(
    pair: RightDutyPair,
    landlord: Person,
    tenant: Person,
    pc: PositiveOccurrencePropositionalContent,
    book: CorrelativePositionBook,
    expectedAccount: ExpectedSatisfactionAccount,
    satisfactionAccount: SatisfactionAccount,
    e: ExpectedSatisfactionRecord,
    owed: Real,
    dueDay: Int
) {
    insert iof(landlord, Person);
    insert iof(tenant, Person);
    insert iof(pair, RightDutyPair);
    insert iof(pc, PositiveOccurrencePropositionalContent);
    insert iof(book, CorrelativePositionBook);
    insert iof(expectedAccount, ExpectedSatisfactionAccount);
    insert iof(satisfactionAccount, SatisfactionAccount);
    insert iof(e, ExpectedSatisfactionRecord);
    insert pairBook(pair, book);
    insert contentBook(pc, book);
    insert bookExpectedAccount(book, expectedAccount);
    insert bookSatisfactionAccount(book, satisfactionAccount);
    insert recordInAccount(expectedAccount, e);
    update pair: RightDutyPair set { advantageHolder = landlord, burdenHolder = tenant }
    update e: ExpectedSatisfactionRecord set { value = owed, startsOn = 1, endsOn = dueDay }
}

/// Record a rent payment of `amount` into a satisfaction account.
pub mutate recordPayment(
    satisfactionAccount: SatisfactionAccount,
    payment: SatisfactionRecord,
    amount: Real,
    paidOn: Int
) {
    insert iof(satisfactionAccount, SatisfactionAccount);
    insert iof(payment, SatisfactionRecord);
    insert recordInAccount(satisfactionAccount, payment);
    update payment: SatisfactionRecord set { value = amount, startsOn = paidOn, endsOn = paidOn }
}

/// Compose two contents into a conjunction ("both must hold").
pub mutate makeConjunction(
    conj: Conjunction,
    left: PropositionalContent,
    right: PropositionalContent
) {
    insert iof(conj, Conjunction);
    insert conjunctOf(conj, left);
    insert conjunctOf(conj, right);
}

/// Compose two contents into a disjunction ("either may hold").
pub mutate makeDisjunction(
    disj: Disjunction,
    left: PropositionalContent,
    right: PropositionalContent
) {
    insert iof(disj, Disjunction);
    insert disjunctOf(disj, left);
    insert disjunctOf(disj, right);
}

// ─────────────────────────────────────────────────────────────────────────
// Queries
// ─────────────────────────────────────────────────────────────────────────
/// Expected records whose obligation is cumulatively met.
pub query met() -> Met;

/// `(content, instant)` pairs where the content is breached as of the instant.
pub query breached() -> BreachedAt;

/// `(content, instant)` pairs where the content is fulfilled as of the instant.
pub query fulfilled() -> Fulfilled;

plan_bench — a write-heavy-then-derive-read benchmark corpus

Area: Benchmarks Teaches: the two-phase benchmark profile — a large scripted series of mutations followed by a derived measurement that traverses all of it. A self-contained investment ledger whose mutation count is the scaling knob, sized so the headline configuration runs in the dozens of seconds (real benchmark signal) while a small configuration stays fast for CI. Prerequisites: double-entry accounting (mutate flows and aggregates); robot plan execution (rule-driven derivation). Run: ox run-scenario examples/plan_bench --scenario scenarios/plan.toml && ox test examples/plan_bench — and examples/plan_bench/bench.sh to time it at scale. (The --scenario pin matters after a bench.sh run: a bare run-scenario also picks up the locally generated scenarios/generated.toml.)

A repository-owned benchmark corpus with the two-phase profile a plan-search benchmark measures: do a large scripted series of mutations, then measure a derived quantity whose computation traverses everything the mutations built.

The domain is a self-contained, simplified investment ledger — lots are acquired and sold, and each disposition’s realized gain (proceeds - costBasis) is classified by holding period and asset class, then rolled up. Nothing here is tax law or an external model; it is entirely owned by this repository and formatter-canonical.

Shape

1. Mutation phase (planner.ar) — recordBuy + recordSale, one Lot/Sale/sold edge per pair. The number of pairs is the scaling knob.
2. Measurement phase (rules.ar) — the derived rollups totalRealizedGain, longTermGain, shortTermGain, and the grouped netByAssetClass. Reading them forces the derivation plane to traverse every accumulated disposition.

The OrphanDisposition check re-evaluates on every commit, so under ox run-scenario (one transaction per step) the write phase is deliberately super-linear in the pair count — that is what gives the benchmark real signal (dozens of seconds at the headline scale, versus the millisecond-scale rest of the repository).

Construct coverage

• mutate/apply flows with insert / update (planner);
• deductive reads feeding inserts through nested for loops over parameterized queries (planner::classifyRound);
• rule-driven derivation — joins, comparisons, global and grouped aggregates, and an integrity check (rules);
• a relation with constrained endpoints (catalog::heldIn);
• a concept (kind) hierarchy and a standpoint scope (catalog, seed).

Running it

Correctness golden (tiny, hand-checkable — 2 securities, 3 lots, 3 sales):

ox run-scenario examples/plan_bench      # runs scenarios/plan.toml, asserts the rollups
ox test examples/plan_bench              # the in-language goldens (tests/mod.ar)

Benchmark at a chosen scale:

cd examples/plan_bench
./bench.sh 25       # smoke scale (~0.1s)
./bench.sh 500      # headline scale (~67s), dozens of seconds of real signal

bench.sh calls gen.py <N> to emit scenarios/generated.toml (git-ignored), builds the package, and reports the ox check and ox run-scenario wall-clocks. Measured on an Apple-silicon dev reference machine with release ox (the timings below are Apple-silicon reference numbers):

ox check is ~0.01 s at every scale (the schema is fixed-size; only the scenario grows), so the corpus build gate stays fast.

Note: ox run-scenario examples/plan_bench with no --scenario discovers and runs every scenarios/*.toml. After a bench.sh run the git-ignored scenarios/generated.toml sits alongside plan.toml, so a bare run-scenario will also execute the generated scale scenario. Pass --scenario scenarios/plan.toml to run only the correctness golden.