Argon

Argon is a knowledge-representation language and graph database. You declare an ontology — concepts, the relations between them, and the rules that derive new facts — and Argon compiles it to a content-addressed artifact you can query, reason over, mutate, and serve.

This book is the surface specification: the syntax and meaning of an Argon program — the precise reference, chapter by chapter, in the technical specification and its appendices.

For a guided, motivated tour of the whole language, read The Argon Book, the teaching narrative (spec/book/). To watch real packages compile and run, see Argon by Example (examples/).

Two companion sources of truth sit beside this book:

• The Lean 4 mechanization (spec/lean/) is canonical for the substrate — the type system, reasoning semantics, and decidability results. Where the Lean and this book disagree on something the Lean covers, the Lean wins; the book is the bug.
• RFDs (Part II) record design decisions and their rationale. They are history, not normative spec.

Each chapter leads with a grammar fragment and a worked example before the prose. Cross-references are named links; each names the chapter or section it points to.

Toolchain: installation, channels, and versioning

How Argon is installed, versioned, and switched. oxup is the toolchain manager (rustup-style); ox/oxc/ox-lsp/oxfmt are the tools it dispatches.

Install

curl -fsSL https://argon.sharpe-dev.com/install.sh | sh

Installs oxup into ~/.argon/bin, links the tool shims, and installs the stable toolchain. Ensure ~/.argon/bin is on PATH.

Platforms: macos-arm64, linux-x86_64, linux-aarch64.

Channels

Version strings

X.Y.Z is the in-development line; dev/nightly are prereleases of it (they sort ahead of the last stable). oxup and the toolchain share one version.

Distribution layout

Served from https://argon.sharpe-dev.com (S3 origin behind CloudFront):

/install.sh                                                          installer
/toolchains/<version>/<platform>/argon-<version>-<platform>.tar.gz(.sha256)
/dist/channel-<channel>.toml                                         current version per channel
/dist/index-<channel>.json                                           all published versions
/oxup/latest/<platform>/oxup(.sha256)                                oxup self-update (stable)
/oxup/<channel>/latest/<platform>/oxup(.sha256)                      oxup self-update <channel>
/editors/vscode/<version>/argon-<version>.vsix(.sha256)              editor extension

• /toolchains/<version>/ is immutable. dev/nightly tarballs are pruned 30 days after publish; stable is kept indefinitely.
• index-<channel>.json is newest-first: an array of { version, released, platforms[], sha256, available }. A pruned build stays listed with "available": false.

Toolchain spec

A spec identifies a toolchain to install/use/+<spec>:

oxup commands

oxup use <spec>                            install if needed, then set as default
oxup default <spec>                        alias for `use`
oxup install <spec>                        install without changing the default
oxup uninstall <spec>                      remove an installed toolchain
oxup update [channel]                      re-fetch a channel's latest
oxup list                                  installed toolchains (default marked)
oxup list --available [--channel C] [--limit N]   published versions
oxup search <pattern>                      search published versions across channels
oxup show                                  active toolchain, default, installed
oxup which <tool> [--toolchain <spec>]     resolved binary path
oxup self-update [channel]                 update oxup itself (stable; or dev/nightly)
oxup extension install|uninstall|list      editor extension (matches the active toolchain)

--json is available on list, search, and show (for tooling).

Selecting a toolchain (per invocation)

First match wins:

1. OXUP_TOOLCHAIN=<spec>
2. +<spec> as the first argument — e.g. oxc +nightly build
3. ox-toolchain.toml in the working directory or a parent — [toolchain] channel = "<spec>"
4. ~/.argon/settings.toml — [default] channel
5. the built-in stable

A missing toolchain is fetched automatically on first use.

~/.argon/

~/.argon/
  bin/
    oxup                     the manager
    ox oxc ox-lsp oxfmt      symlinks → oxup
  toolchains/<spec>/
    bin/                     ox oxc ox-lsp oxfmt
    share/std/               bundled stdlib packages
    manifest.toml            version, platform, components
    provenance.toml          source (cdn|local), origin, sha256, install time
  settings.toml              [default] channel, [extension] state

ox/oxc/ox-lsp/oxfmt on PATH are symlinks to oxup; oxup reads argv[0], resolves the active toolchain, and execs ~/.argon/toolchains/<spec>/bin/<tool>.

Tools

Formatter notation policy

Argon’s dual notation (Unicode notation) lets source mix Unicode glyphs (∀ ⊑ → ⊞) with their ASCII spellings (forall <: -> box_plus); both lex to the same token. The formatter can normalize a file to one form, governed by [fmt] notation in ox.toml:

[fmt]
notation = "preserve"  # | "unicode" | "ascii"

• preserve (the default) never rewrites between the two forms — a file is formatted as typed, so mixed notation is left untouched.
• unicode rewrites every ASCII spelling to its glyph (forall → ∀); ascii does the reverse. The rewrite is lossless and round-trips, because both forms produce the identical token.

The policy resolves through a nearest-wins cascade (rustfmt/prettier-style): a package’s own [fmt] overrides a [workspace.fmt] at the workspace root, which overrides the global user config. The notation table itself is the single [[notation]] source shared with the lexer aliases and editor input methods. Notation is policy (a per-project taste call); spacing and layout are the Argon convention and are not configurable.

Editor support

Everything an editor knows about an Argon program comes from one place: the language server, ox lsp. The reason is the meta-calculus. Argon’s surface vocabulary is user-extensible — a package declares its own metatypes, concepts, relations, and constructs, so the set of meaningful words in a file is not fixed by the language. A static grammar can color and brace-match the punctuation, but it cannot know that Obligation is a concept or that owes is a relation; only the resolver that elaborated the package knows that. So all the language-aware behavior — diagnostics, hover, jump-to-definition, the right token colors — lives in the server, and editors are thin clients of it. One server, written once, drives every editor; an editor plugin is just an LSP client plus a syntax floor.

What ox lsp provides

ox lsp speaks LSP over stdio and advertises:

Inlay hints and code lenses are not built yet. Because the diagnostics are the server’s, they always match the toolchain that produced them — there is no second, drifting implementation of the checks.

Installing it

oxup installs and version-locks the editor integration, so the editor support matches the active toolchain:

oxup extension install                         # auto-detect every installed VS Code-family editor
oxup extension install --editor neovim         # or name one explicitly
oxup extension uninstall --editor emacs
oxup extension list                            # detected editors + the installed version

The two editor families install differently because they expose different contracts:

• VS Code family (VS Code, Cursor, VSCodium, VS Code Insiders, and the browser-hosted code-server) have an --install-extension CLI. oxup fetches the .vsix stamped with the active toolchain version from an immutable CDN path, sha256-verifies it (the same fail-closed discipline as the toolchain fetch), and installs it. A user on stable 0.2.2 gets the 0.2.2 extension, not “latest”.
• Neovim, Vim, and Emacs have no extension-CLI contract, so oxup installs them by file placement: it writes the embedded plugin files into the editor’s package directory and adds an idempotent, oxup-managed block to the init file (between >>> argon (oxup-managed) >>> sentinels) that points the client at the active toolchain’s ox lsp. Re-running updates the block in place and leaves everything outside the sentinels untouched; uninstall removes both.

oxup init and oxup update auto-install and refresh the integration after the toolchain is placed (oxup init --no-extension opts out). A failed editor install is a soft, one-line warning — the toolchain is what matters — never a hard error.

The VS Code extension ships the Argon “A” glyph as the .ar file icon. The Neovim and Emacs plugins cannot reuse that SVG (their file explorers draw a Nerd Font glyph, not an image); their READMEs give a suggested glyph-and-color registration keyed on the .ar extension.

Environment

Scope

Argon is a programming language for declaring and reasoning over a richly-typed knowledge graph at the data-system layer. The canonical specification of the language core lives in Lean 4 under spec/lean/; this document specifies the surface in prose. Where they disagree, the Lean wins.

The language is built from five atoms — meta-calculus, constructs, rule, trait, macro — and nothing else. Every surface form lowers to one of them. Argon has no surface for IO, threads, network, or filesystem; those live in the host runtime. Tenancy and multi-tenant orchestration are application concerns, not language concerns.

Lexical structure

Source

UTF-8. Source files have extension .ar. Non-ASCII text is admitted in identifiers (Identifiers, UAX #31), comments (Comments), and string/char literals (Literals). Operators and keywords have a canonical ASCII spelling and an equivalent Unicode form — Lean-style dual notation (Operators): ∀ is forall, ⊑ is <:, → is ->, ⊞ is box_plus. The two are interchangeable surface spellings of the same token, so a program may be written in either (or a mix), and editors enter the Unicode forms through a \abbrev input method (\forall → ∀). Delimiters and the remaining punctuation are ASCII.

Comments

• // — line comment, not extracted by ox doc.
• /// — outer doc comment, attaches to the next item.
• //! — inner doc comment, attaches to the enclosing module.
• /* … */ — block comment, may be nested. Not extracted by ox doc. Comments out arbitrary tokens including //-prefixed lines, useful when temporarily disabling sub-expressions.

Identifiers

Identifiers follow UAX #31: an identifier starts with a XID_Start character or _, and continues with XID_Continue characters. The ASCII subset [A-Za-z_][A-Za-z0-9_]* is the common case and the recommended style. An identifier’s text is its exact source bytes. NFC canonical equivalence (so that a precomposed é U+00E9 and the decomposed e + combining acute U+0065 U+0301 would denote the same name) and a mixed-script confusable warning (UAX #39, Latin A U+0041 vs Cyrillic А U+0410) are the RFD 0034 name-resolution design (Out of scope). Conventions: snake_case for value bindings, fields, and rules (fn, derive, query, mutate, check); CamelCase for types, metatype-introduced concepts, and metarel-introduced relations; lowercase (typically snake_case) for the metatype- and metarel-introducing keywords themselves (kind, role, rel, mediation, …); SCREAMING_SNAKE_CASE for stdlib constants. Conventions are not enforced.

Operators

Top / ⊤ and Bot / ⊥ are type-level constants.

Unicode notation

Each operator/keyword below has an equivalent Unicode glyph; the glyph and its ASCII spelling lex to the same token, so they are fully interchangeable and nothing past the lexer distinguishes them. Glyphs and the editor \abbrevs follow the Lean lean4-input conventions; the metric-modal glyphs (⊞/⊟) follow the DatalogMTL literature. The authoritative table is [[notation]] in compiler/crates/oxc-syntax/grammar.toml, the single source from which the lexer’s aliases and the editor input methods are generated.

=> is deliberately not given a Unicode form: it is match-arm / head syntax, not implication, so ⇒ would mislead. diamond_plus / diamond_minus have no single conventional glyph (the notation is ◇ with a directional marker) and stay ASCII-only for now.

Boolean operator placement. Argon distinguishes two syntactic positions:

• Rule-body position — after :- in derive/check, inside unsafe logic blocks, the from/where clauses of query bodies, subquery bodies (collect/set/one/count/exists), refinement where { … } / iff { … } clauses, and require { … } precondition blocks. Conjunction is ,; NAF is not atom. Disjunction is not inline — write multiple rules with the same head, or combine subquery variants via union / intersect / except.
• Expression position — inside fn bodies, if / match conditions, let initializers, the RHS of comparison atoms inside rule bodies, and atom arguments. Boolean operators are &&, ||, !.

The two are non-overlapping: && is not accepted between rule-body atoms; , is not a Boolean operator in expressions.

Literals

INT      ::= [0-9]+ ( '_' [0-9]+ )*
REAL     ::= INT '.' INT
STRING   ::= '"' chars '"'
DATE     ::= '#' YYYY '-' MM '-' DD '#'
DATETIME ::= '#' YYYY '-' MM '-' DD 'T' HH ':' MM ':' SS 'Z' '#'
BOOL     ::= 'true' | 'false'
LIST     ::= '[' (expr (',' expr)*)? ','? ']'
RECORD   ::= '{' (Ident ':' expr (',' …)*)? ','? '}'

Set/map literals are constructor calls (Set::new(a, b, c), Map::new((k, v), …)); there is no {1, 2, 3} form (Out of scope).

Modules and packages

Structure

Modules take three forms, all equivalent at the symbol table:

• A .ar file is implicitly a module named for its file stem.
• A directory containing mod.ar is a module; sibling .ar files (and subdirectories containing mod.ar) are submodules of it.
• An inline mod Name { … } declaration introduces a nested module in the current file.

A mod Name; declaration with no body has a single meaning — Rust’s child-module declaration: it asserts that a sibling Name.ar (or Name/mod.ar directory module) exists and attaches its contents under the current namespace as Name. A file does not rename itself: a content-carrying file whose mod Name; resolves to no sibling is refused with OE0715 (audit dc-06 retired the legacy “module-header” reading, where the first mod Name; of a file silently relabeled that file’s own declarations as module Name). To set a module’s name, use the file/directory layout — the project entry is module root, and any other .ar file is the module named for its stem; to declare a child, create the sibling Name.ar; to keep declarations where they are, omit the mod line. Explicit mod declarations are required; the compiler emits OW0710 when a sibling .ar file exists but no mod declaration references it.

Both project and package entry default to the root module file — preferring the Cargo-style src/root.ar, falling back to a flat root.ar at the package root. A prelude.ar is not an entry default: a package’s prelude is the manifest [package].prelude import model (the auto-imported use-tails of RFD 0038), and a prelude.ar file is an ordinary re-export module reached through the root — conventionally pub used at the root and imported by dependents via use pkg::prelude::*. The entry’s directory is the source root under which the package’s .ar files are indexed.

visibility ::= 'pub' | 'pub' '(' 'pkg' ')'
mod-decl   ::= 'mod' Ident ';'                                  // file-include
            |  'mod' Ident '{' mod-item* '}'                    // inline
            |  'mod' Ident '=' path '(' expr-list ')'           // functor alias (Functor modules)

Default visibility is module-private, following Rust: a default-visibility item is visible to the module that declares it and every descendant module. A private item declared at the package root is therefore visible package-wide (every module descends from the root); a private item in mod M is visible to M and M’s submodules, but not to the root or to sibling modules. This governs the privacy check only — name resolution is unchanged: a descendant still names an ancestor’s item through pkg::/super::/use (there is no bare-name inheritance from a parent module). pub exposes to dependents; pub(pkg) limits to the package.

Imports

use      ::= 'use' use-tree ';'
use-tree ::= path ('as' Ident)?
          |  path '::' '*'
          |  path '::' '{' use-tree (',' use-tree)* ','? '}'
path     ::= Ident ('::' Ident)*

Rust-style: single-symbol (use std::math::Nat;), brace-list (use std::math::{Nat, Int};), glob (use ufo_foundational::prelude::*; — a third-party vocabulary package), and aliased (use foo::bar::Sym as Other;) forms.

A plain use is a private import — visible only inside the importing module. A pub use re-exports: the imported items join this module’s public surface and are visible transitively to dependents, which is how a package prelude works (pub use pkg::prelude::*).

Import-resolution limits. Three forms parse but do not resolve: a single-item use M::X where X is re-exported by M rather than declared there (the glob re-export use M::* resolves it; the named form does not); pub use path as Alias (re-export with renaming); and a capitalized Self:: type path (lowercase self:: works). Import through the glob re-export or the original declaring path.

The prelude is a package feature, not a compiler default (RFD 0038). A package’s [package].prelude (an array of use-tails in ox.toml) is auto-prepended to every module of that package; it is empty by default and carries no vocabulary. type/rel are not in it unless the package opts them in (prelude = ["std::core::{type, rel}"], or prelude = ["pkg::prelude::*"] pointing at a prelude.ar of pub use re-exports). A module opts out with #![no_implicit_prelude]. There is no auto-imported std::prelude; what is always in scope is the language substrate (step 3 below), which is not a library prelude.

Manifest

ox.toml, Cargo-flavored:

[package]
name = "lease-story"
version = "0.1.0"
edition = 0
# Optional package entry override. Without this, the default search prefers the
# Cargo-style `src/root.ar` and falls back to the flat package root `root.ar`.
entry = "root.ar"

[dependencies]
# PATH dependencies (RFD 0030). The key is the path root the
# consumer uses (`use ufo::endurant::Object;`) and must equal the dependency
# package's `[package].name`.
ufo = { path = "../ufo" }

[lattice]
# Decidability-tier ceiling (Standpoints and modal operators). A declaration whose classified tier exceeds
# this ladder name is refused at `ox check` / `ox build` (OE1230, RFD 0030 D6).
max_tier = "recursive"

[standpoints]
# optional package-boundary declarations

[schema]
# Optional source root for generated or nested package layouts. Entry paths are
# resolved relative to this root when the nested entry exists.
root = "src"

Tooling resolves a package directory entry in this order: [project].entry, [project].main, [package].main, [package].entry, then the conventional defaults. With no explicit entry, the default search prefers the Cargo-style src/ layout and falls back to the flat package root (so existing packages keep resolving): both [project] and [package] try src/root.ar then root.ar. The first that exists wins, and its directory becomes the source root — a package laid out as src/root.ar roots all its .ar sources under src/ with no config (ox new/ox init scaffold exactly this). An explicit [schema].root overrides the source root. When no entry is found, the error names every path it searched.

Dependencies (RFD 0030). Only dep = { path = "…" } resolves: each path dependency’s package is loaded and its pub surface folded into the consumer’s workspace under the dependency name as a path root (see Name resolution). The registry/VCS surface — a bare version requirement (ufo = "1.0") or the version/git/branch/tag/rev/registry keys — is recognized and refused with OE1240 (Out of scope), never silently ignored. The dependency name must equal the dependency’s published [package].name (OE1241 otherwise); a dependency cycle is OE1242; the same name resolving to two different directories is OE1243. There is no ox.lock for a path-only graph (path deps are unlocked, Cargo precedent); ox.lock is reserved for the registry/git graph. Manifest honesty (RFD 0030 D6): an unrecognized section or key surfaces a Cargo-style OW1240 “unused manifest key” warning rather than being silently dropped, and [lattice].max_tier is enforced against the Standpoints and modal operators classifier (OE1230).

Name resolution

Resolution of a bare identifier proceeds in order:

1. Local scope. Definitions in the current module, including the lexical chain of enclosing mod bodies and impl blocks.
2. Imports + package prelude. Items brought into scope by use in the current module, and — unless #![no_implicit_prelude] is set — the package’s prelude ([package].prelude, auto-prepended uses; RFD 0038). The prelude is empty by default and carries no vocabulary.
3. Substrate. The fixed, always-in-scope language primitives — not a library, and not opt-outable: the primordial types (Nat, Int, Real, Decimal, Money, Date, Time, DateTime, Duration, Bool, String, Top, Bot) and the builtin type forms (Option, Result, Ordering, List, Set, Map, Range, Truth4, Truth4Of, Diagnostic, Severity, …).

A qualified identifier (containing ::) is resolved by walking the path. The leading segment selects a root:

• pkg — the current package’s root. This is the sole self-reference anchor: a package never refers to itself by its own name, so internal paths survive a package rename. pkg::a::b::X names item X in module a::b of this package. (Argon has packages, not crates — there is no crate keyword.)
• self — the current module; super — the parent module (repeatable: super::super::X).
• A dependency package name declared in [dependencies] — e.g. ufo::endurant::Object (a path-dependency vocabulary package, RFD 0030). The dependency’s pub surface is folded into this workspace under its name as a path root; ufo::X and use ufo::X; resolve into it. The stdlib root std is always available (std::math::Nat).
• Otherwise the leading segment resolves against the scope chain — a submodule of the current module, or a name brought in by use.

Subsequent segments resolve within the preceding module’s namespace. An item therefore has a single absolute name viewed from outside the package (mypkg::a::b::X); viewed from inside, the equivalent absolute form is pkg::a::b::X.

Contextual introducer identifiers (type, or vocabulary names like kind, role, phase, …) are ordinary identifiers — recognized by an IDENT IDENT shape at declaration position and resolved via the algorithm above against the pub metatype (concepts) / pub metarel (relations) declarations visible in scope: declared in this package, or imported from a vocabulary package (across a [dependencies] path-dependency boundary, RFD 0030). Nothing is ambient here — not even type/rel: a package brings the no-commitment baseline into scope explicitly, via use std::core::{type, rel} or its [package].prelude (RFD 0038), exactly as it brings any vocabulary (appendix A). The compiler emits OE0101 UnresolvedName for general failures, and OE0605 UnknownMetatype / OE0606 UnknownMetarel specifically when a leading identifier at declaration position fails to resolve — at ox check and ox build; no artifact is emitted. A use statement that does not resolve is itself refused with OE0103 UnresolvedUseImport (with a did-you-mean over the visible namespace, RFD 0030 D5) — a broken import is never silently accepted.

Module extraction (tree-shaking)

When a module imports another, the elaborator extracts a ⊥-locality module (Cuenca-Grau–Horrocks–Kazakov–Sattler 2008): the smallest subset of the imported module’s axioms that stays non-trivial once every concept outside the used signature is reinterpreted as ⊥. Extraction is a fixpoint, linear-time per iteration, terminating in at most |B| iterations.

The guarantee is Σ-scoped conservativity: every entailment about the used signature survives extraction. Argon strengthens the classical result for its own semantics — closed-world conclusions are preserved (CWA-conservativity), ghost individuals reachable only through non-Σ concepts are pulled in (domain-conservative extraction), defeasible rules drag in their defeaters (defeat-aware extraction — a classical extractor is unsound under non-monotonic semantics, Bonatti-Faella-Petrova-Sauro 2022), and extraction composes safely across an import chain. All are mechanized at spec/lean/Argon/Locality/.

Extraction is how the substrate composes decidability tiers across heterogeneous modules (Tier ladder): each extracted module is classified independently, and conservativity guarantees no entailment is lost. Failures emit OE0710 (conservativity cannot be proven under the importer’s world assumption) or OE0711 (defeat-aware extraction cannot close the defeat graph).

Meta-calculus atom

Three declarations: metaxis, metatype, metarel. They make the language ontology-neutral by letting packages declare the concept-introducing keywords.

metaxis

metaxis-decl ::= 'metaxis' Ident 'for' target metaxis-body? ';'
target       ::= 'metatype' | 'metarel' | 'individual' | 'macro' | '[' target (',' …)* ']'
metaxis-body ::= '{' enum-body '}' | '=' TypeExpr ('where' refinement)?
enum-body    ::= Ident (',' Ident)*          // unordered
              |  Ident ('<' Ident)+          // totally ordered (chain)

pub metaxis rigidity for metatype { anti_rigid < semi_rigid < rigid };
pub metaxis sortality for metatype { sortal, non_sortal };
pub metaxis identity_provision for metatype { provides, inherits };
pub metaxis dependency_kind for metarel { existential, contingent, none };
pub metaxis ordinality for metatype = Nat;
pub metaxis weight for metatype = Real where _ > 0.0;

A metaxis characterizes the meta level: its values are assigned to metatypes (for metatype) and metarels (for metarel), never to a concrete type directly. The targets name the meta-sort the axis applies to — metatype for the concept tier, metarel for the relation tier — not the type / rel concept introducers. (A future for <DeclaredType> target — a type-specific refinement axis bound to one declared type — is left open by the model but not yet specified.)

Cross-axis constraints are check rules at module level, never embedded in the body.

metatype

metatype-decl ::= 'abstract'? 'fixed'? 'metatype' Ident '=' '{' axis-assign (',' …)* ','? '}' ';'
axis-assign   ::= Ident ':' value
value         ::= Ident | literal

A metatype body is a record of axis values, so each binding reads like a struct field — a single : separates the axis from its value.

pub abstract fixed metatype category = { rigidity: rigid,      sortality: non_sortal };
pub fixed metatype kind     = { rigidity: rigid,      sortality: sortal,     identity_provision: provides };
pub fixed metatype subkind  = { rigidity: rigid,      sortality: sortal,     identity_provision: inherits };
pub metatype role           = { rigidity: anti_rigid, sortality: sortal };
pub metatype phase          = { rigidity: anti_rigid, sortality: sortal };

A metatype name in scope is contextually a concept-introducing keyword: pub kind Person { … }.

Axes are pure user vocabulary. The axis bindings in a metatype body are the declaring package’s own ontology — validated against the declared metaxis domains (RFD 0027 D2), persisted on the wire, and queryable — but the compiler never reads an axis name. No axis assignment changes elaboration, coverage, or mutation semantics; importing a vocabulary cannot alter substrate behavior because its author happened to name an axis rigidity. The metatypes shown above (kind, subkind, role, phase, category) are example declarations of the kind a third-party UFO vocabulary package would ship — they are not language atoms, and no UFO vocabulary ships with Argon or its stdlib. Other vocabularies (BFO, GFO, custom) define their own metatypes with their own axis assignments; the language treats all of them uniformly.

Substrate behavior comes from two ontology-neutral modifiers (RFD 0027 D6) — the operational shadows of the classic meta-property distinctions, with PL precedents rather than ontological commitments:

• abstract — no direct instances. Every type the metatype introduces refuses construction (insert T { … }), direct classification (insert iof(x, T)), and seeded assertion (positive pub fact T(x)) with OE0233; subtypes are unaffected, and pub not_fact T(x) (refuting membership) stays legal. Abstract types are exempt from trait impl-coverage obligations (Resolution) — they structure the hierarchy, and every individual is classified through some non-abstract subtype. abstract may also be declared per-type on a concept declaration (pub abstract type Vehicle { … }, the UML/PL convention); a type introduced by an abstract metatype is abstract with no override semantics.
• fixed — classification decided at construction. insert iof / delete iof against a type introduced by a fixed metatype refuses with OE0234 (mutate); construction itself is unaffected. Dynamic classification is the default — the restriction is the opt-in, the same posture as check. Fixed classification is what makes static modal discharge sound (Modal operators); the Kripke-semantics justification (rigid designation = fixed classification) is mechanized in Argon.Reasoning.StaticDischarge and the mutation-gate theorem in Argon.Runtime.ModifierGates.

A vocabulary author writes both layers together — pub abstract fixed metatype category = { sortality: non_sortal, rigidity: rigid }; — the modifiers carry the behavior, the bindings carry the package’s ontology. Misplaced modifiers (fixed on a concept declaration, either modifier on a struct/enum/relation, duplicates) are refused at parse with OE0008.

metarel

metarel-decl  ::= 'metarel' Ident '(' endpoint-list ')' metarel-body? ';'
endpoint-list ::= endpoint (',' endpoint)*
endpoint      ::= (Ident ':')? Ident          // optional name, then metatype name
metarel-body  ::= '{' axis-assign (',' …)* ','? '}'

pub metarel mediation(mediator: relator, mediated: kind) {
    dependency_kind: existential,
};

pub metarel material(kind, kind) { dependency_kind: contingent };
pub metarel three_way_dependence(kind, kind, kind);

The metarel name is itself a contextual relation-introducing keyword (Relations): pub mediation Involves(m: Marriage, p: Person) declares a relation classified by mediation. The elaborator verifies the relation’s endpoint metatypes match the metarel’s positions. (An alternative decorator-attachment spelling — #[mediation] on a generic relation declaration — was sketched in earlier drafts but is not built: user-declared metarel names are not compiler directives, so the attribute form refuses at the directive registry, OE0705. The introducer form above is the supported surface.)

The stdlib ships a generic metarel for ontology-uncommitted use:

// in std::core — the generic metarel (opt-in via `use std::core::rel`,
// RFD 0038), shown as it is declared inside the stdlib (not a user file).
pub metarel rel<E1: metatype, E2: metatype>(E1, E2);

rel accepts any endpoint metatypes (inferred from the relation’s parameter types). After use std::core::rel;, the modeler can write pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*] for relations without committing to a specific ontological vocabulary. Vocabulary packages may re-export std::core::rel in their prelude as a convenience.

Reflection

Reflective sorts: Entity, TypeRef, Metatype

The substrate exposes three reflective sorts and a fixed lattice over them:

Metatype  <:  TypeRef  <:  Entity

• Entity is the universal sort of all entities — individuals and type-references alike. A type is an entity (so it can itself be classified by a higher-order type; see Higher-order modeling). Entity <: Top.
• TypeRef is the sort whose values are references to declared types (concept / construct / relation / metatype) — a handle into the closed, nominal catalog of declarations, in the manner of OWL-2 punning, Java’s Class<?>, or Haskell’s TypeRep. TypeRef is unsealed, so Metatype remains the only sealed primitive. Because TypeRef denotes a closed catalog of already-declared types rather than an impredicative universe, there is no Type : Type: the reflective layer is a predicative, stratified universe of codes, not a self-membership hierarchy.
• Metatype is the sealed primitive that classifies all metatypes (kind, role, phase, …, and Metatype itself). Since Metatype <: TypeRef, every metatype name in scope is also a TypeRef value.

Type-as-value. A declared type’s name in value position is a TypeRef value — Person, kind, and Metatype are all TypeRef values, distinguished from the type Person by syntactic position. This is the substrate’s type-as-value facility: a field or parameter may be typed TypeRef (or the bounded TypeRef<C>; see Built-in type forms) and carry a reference to a declared type. The runtime carrier is the declared-symbol reference Value::Name; on the wire, a TypeRef/Entity argument is a qualified class-path ("pkg::mod::Type", or {"$typeRef": "pkg::mod::Type"}) resolved to the declared type’s identity — entity refs (#i…) are not accepted for these parameters. See RFD 0023.

Reflection intrinsics

The substrate provides five reflection intrinsics — meta, iof, specializes, extent, and implements (RFD 0026; signature implements(t: TypeRef, tr: TraitRef) -> Bool, materialized as the catalog-closed $implements relation with supertrait closure and <: upward target-coverage, Reflective conformance: TraitRef and implements) — admitted in any rule body without a use declaration. The first three have syntactic-sugar atom forms in Rule-atom grammar; extent and implements are called directly. For meta/iof/specializes/extent, each type-position argument is a TypeRef value — a literal type-reference or a bound variable of sort TypeRef — which is precisely what makes the intrinsics first-class, value-polymorphic predicates: library code can pass, count over, or quantify across type-values (see Higher-order modeling and the unprivileged mlt package, realizing the spec/research/RP-003-mlt-as-library.md GAP-1). implements differs in two deliberate ways: its second argument is TraitRef-sorted (traits are not types and stay off the <: lattice), and because $implements is a finite catalog-closed relation, both of its positions may be free — enumeration is the intended use (Reflective conformance: TraitRef and implements).

meta has the signature meta(x: Entity) -> TypeRef: it returns the immediate classifier of x — its <:-minimal declared type — as a TypeRef value. Under multiple classification (an entity instantiating incomparable types, e.g. a UFO individual that is both a Person and a Customer with neither <: the other), meta(x) is multi-valued: it yields one TypeRef per <:-minimal classifier. (It is a Metatype value only when x is itself a type — e.g. meta(kind) == Metatype — since Metatype <: TypeRef.) x :: T is syntactic sugar for meta(x) == T.

meta() applies only to ontologically-classified concepts (those declared under a vocabulary or stdlib metatype). Calling meta() on a struct/enum-declared value is a category error — language-level data carries no metatype — and emits a diagnostic at elaboration.

Worked examples (each right-hand side is a TypeRef value): meta(Person) == type when Person is pub type Person { … } under std::core::type; meta(Person) == kind when Person is pub kind Person { … } under an imported (or locally-declared) UFO vocabulary; meta(kind) == Metatype; meta(Metatype) == Metatype (sealed self-instantiation). Metatype is the sealed primitive that classifies all metatypes; it is special-cased by the compiler. The classifier kind and the primitive Metatype are TypeRef values because Metatype <: TypeRef.

iof has the signature iof(x: Entity, t: TypeRef) -> Bool. The rule-atom form x : T (Rule-atom grammar type test) is syntactic sugar for iof(x, T). Because the type-position argument t is a TypeRef value, iof is a first-class predicate: it can be passed as a relation argument, counted over, or quantified across — for example, library code building higher-order theories (the unprivileged mlt package, Higher-order modeling, Stdlib (selected)) treats iof as a first-class predicate.

iof is read at two tiers. The individual/ABox tier is membership of an order-0 entity in a type, asserted by a pub fact T(x) ground atom. The catalog/type tier is a declared type×type membership — a type X declared an instance of a higher-order type T via the : T instantiation clause (Vocabulary concepts and the generic type metatype, pub kind USD : Currency). The subject x is itself a TypeRef value (a type used as a higher-order individual), so the same iof relation carries both; which tier a read sits in is decided by whether the subject is an individual or a type, not by a separate relation. The catalog tier is declaration-derived (never an ABox event), so a #[static] check (Rule atom — fn, derive, query, mutate, check) may read it and extent projects it at the type level.

specializes has the signature specializes(t1: TypeRef, t2: TypeRef) -> Bool. The rule-atom form t1 <: t2 (Rule-atom grammar specialization) is syntactic sugar for specializes(t1, t2). Same first-class, value-polymorphic motivation as iof — both arguments are TypeRef values.

iof and specializes apply only to ontologically-classified concepts. Calling them on struct/enum-declared values is a category error and emits a diagnostic at elaboration, parallel to the meta() discipline.

extent has the signature extent(t: TypeRef) -> Set<Entity> (t is a TypeRef value naming the type whose extent is enumerated). Returns the set of entities x such that iof(x, t) holds at the current state. Both function-style (extent(EmperorPenguin)) and UFCS method-style (EmperorPenguin.extent()) are admitted; the method form lowers to the function form.

Worked examples: extent(Person) returns all order-0 entities classified as Person; extent(BirdSpecies) returns all order-1 kinds that are iof-instances of BirdSpecies (e.g., {EmperorPenguin, GoldenEagle, Grouse, Pheasant}); extent(Metatype) returns the set of all metatypes in scope. extent() on a struct/enum-declared value is a category error, parallel to the other reflection intrinsics.

Relation-signature reflection (rel / arm). Two further reflection predicates reflect over declared relations (the relation tier of the reflective catalog, RFD 0031 D2), so a vocabulary package can write relation-level compile-time constraints:

• rel(r: TypeRef, m: TypeRef) -> Bool — r is a declared relation and m its classifying metarel. One catalog row per declared relation.
• arm(r: TypeRef, pos: Int, t: TypeRef) -> Bool — for relation r, pos is a 0-based arm position and t the endpoint type declared there. One row per (relation, position).

Both are catalog-closed (one row per declared relation / arm, never the ABox), so — like $implements — every position may be free and enumeration is the intended use. rel/arm are abstract reflection primitives, never ontological vocabulary; the metarel/type names a check matches on are user vocabulary, compared by catalog identity. A package-shipped check quantifies over the catalog to enforce an endpoint discipline:

// "an endpoint of a `characterization` relation must be aspect-sorted"
pub check BadCharacterization(r: TypeRef, t: TypeRef) :-
    rel(r, characterization), arm(r, 1, t), meta(t) == kind
    => Diagnostic { severity: Severity::Warning, code: "UFO::W010", message: "..." };

(The metarel introducer itself also verifies its endpoint metatypes at elaboration — metarel, OE0631; $rel/$arm let a package extend or audit that discipline declaratively.)

Lowering. A declared type in value position lowers to the IR primitive Term::TypeRef. iof(x,t) (and x : t) lowers to the Core-IR typeTest atom and meta(x) == T (and x :: T) to the metaEq atom (spec/lean/Argon/CoreIR/RuleIR.lean); specializes(t1,t2)/t1 <: t2 has no dedicated atom and lowers to a reserved-head predicate, and extent(t) to an application of the extent builtin. Beneath Core IR, the reasoner evaluates these against catalog relations it materializes from the declarations — $iof (entity × type, closed under supertypes; this carries both tiers — the individual-tier rows from pub fact T(x) assertions and the catalog-tier type×type rows from each : T instantiation clause, the latter closed upward over the target type’s <: ancestors), $specializes (type × type: the reflexive-transitive specialization graph plus the built-in Metatype <: TypeRef <: Entity edges and the sibling TraitRef <: Entity edge), $meta (entity × its <:-minimal classifiers), $implements (type × trait, supertrait closure and <: upward target-coverage folded in — Reflective conformance: TraitRef and implements), and the relation-tier $rel (relation × metarel) / $arm (relation × position × endpoint type) — RFD 0031 D2. OE0212 MetaArgUnbound is the reserved refusal for an unbound argument of the four type-position intrinsics; implements is exempt by design — both of its positions enumerate over the catalog-closed $implements relation, which is the intended use.

Typical use: deriving cross-level properties of higher-order types from their instances.

#[categorizes(Bird)]
pub type BirdSpecies {
    numberOfLivingInstances: Int = extent(self).count(),
    averageHeight: Decimal = extent(self).map(|b| b.height).avg(),
}

The = expr field-default form shown above refuses with OE0237 FieldDefaultUnsupported (see struct and enum — language built-ins (data declarations) for the full disposition). Express cross-level derivations such as EmperorPenguin.numberOfLivingInstances with the from-navigation field form ([RFD 0005, struct and enum field navigation](constructs/struct-and-enum.md)) or an explicit derive/query rule (Rule atom — fn, derive, query, mutate, check).

Constructs atom

Concepts and relations are co-equal first-class entities. The construct atom is layered:

• Language built-ins (lexer-level, always available): struct and enum — pure data declarations with no ontological commitment, no metatype classification, structural equality.
• Stdlib ontological constructors (opt-in, not ambient — brought into scope via use std::core::{type, rel} or a [package].prelude entry, RFD 0038): the generic metatype type introduces ontologically-classified node-concepts (pub type Foo { … }); the generic metarel rel introduces ontologically-classified relations (pub rel R(...)). They are the no-commitment baseline, imported like any vocabulary — nothing is ambient.
• Vocabulary classifiers (require a pub metatype / pub metarel declaration in scope — declared in this package, or imported from an external vocabulary package): metatypes like UFO’s kind, role, phase, category and metarels like mediation, material for richer ontological commitment. No vocabulary ships with the language or the stdlib — a vocabulary is an ordinary external package (e.g. a UFO package authored by the UFO authors), and an introducer that resolves to no visible declaration is refused with OE0605 / OE0606.

All four layers compile to one substrate IR. The distinction lives in the metatype/metarel calculus (Meta-calculus atom); the language itself ships only the calculus, the data-declaration shorthands, and the meta-declaration keywords.

struct and enum — language built-ins (data declarations)

struct-decl ::= attribute* 'pub'? 'struct' Ident generic-params? where-clause? '{' field-list '}'
enum-decl   ::= attribute* 'pub'? 'enum'   Ident generic-params? where-clause?
                  '{' variant (',' …)* ','? '}'
field-list  ::= field-decl (',' …)* ','?
field-decl  ::= attribute* 'mut'? Ident ':' TypeExpr ('=' expr)? ('from' relation-ref)?
variant     ::= Ident ( '(' TypeExpr (',' …)* ')' | '{' field-list '}' )?

pub struct Diagnostic {
    severity: Severity,
    code:     String,
    message:  String,
    range:    Option<Range>,
}

pub enum Severity { Error, Warning, Info, Hint }
pub enum Option<T> { Some(T), None }
pub enum Result<T, E> { Ok(T), Err(E) }
pub enum Shape { Circle, Square, Triangle }

One enum spelling. enum has a single declaration form — the brace list above — matching Rust and the only form that carries payloads. An earlier enum Name = A | B | C pipe spelling is removed (OE0009). Concept cover declarations (Vocabulary concepts and the generic type metatype) take the matching brace form pub kind Name { A, B } (OE0012 on the old = A | B pipe), so no =-pipe surface survives.

struct/enum declarations carry no metatype classification. They are language-level data shapes — structural equality, no fact-store identity beyond storage, no participation in the metatype calculus. They cover stdlib data records (Diagnostic, Severity, Option, Result, Path, Range, Truth4) and user plumbing types. meta() reflection (Reflection) does not apply.

Struct and enum values

A struct value is constructed by naming the type and giving every field: Row { a: 1, b: 2 }. This is an ordinary expression — it can be a let binding, a field value, a function argument, a return value, a list element, or either side of a comparison. The full construction and projection grammar lives in the expression grammar (Expression grammar); this section states the data semantics.

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

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

Structural equality. Two struct values are equal when their fields are equal, field by field — there is no identity to compare. Field order in the literal does not matter: Row { a: 1, b: 2 } and Row { b: 2, a: 1 } are the same value. Equality is recursive: a struct whose field is itself a struct compares that field structurally too. This is what “pure data” means concretely — a struct is its fields, nothing more.

pub struct Row { a: Int, b: Int }

test "structural equality is field-wise and order-independent" {
    assert Row { a: 1, b: 2 } == Row { b: 2, a: 1 };
    assert Row { a: 1, b: 2 } != Row { a: 1, b: 3 };
}

Immutability. A struct value is immutable: its fields are fixed at construction and never change. There is no in-place update. To produce a struct that differs from an existing one in a few fields, use functional update — the ..base spread — which yields a new value and leaves the base untouched (Expression grammar):

pub struct Row { a: Int, b: Int }

test "spread is a functional update yielding a new value" {
    let base = Row { a: 1, b: 2 };
    assert Row { ..base, a: 9 } == Row { a: 9, b: 2 };   // a overridden, b carried
    assert base == Row { a: 1, b: 2 };                   // base is unchanged
}

Because a struct value is immutable, mut on a struct field is meaningless and is refused — mut field: Type on a struct raises OE0253 MutOnStructField. The mut modifier marks a concept field updatable by an update … set { … } statement inside a mutate body (mutate); that notion belongs to identity-bearing concept individuals, not to value-semantic data.

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

No identity — insert is refused. insert T { … } mints an identity and records an iof classification; it is how concept individuals are born. A struct has no metatype and no identity, so insert on a struct type is refused — OE0252 InsertOfStruct. Construct the struct as a plain value instead (drop the insert).

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

pub mutate make() {
    let p = insert Point { x: 1, y: 2 };
}

A struct literal must state every field exactly. A missing field is OE0249 StructFieldMissing, an undeclared field is OE0250 StructFieldExtra, and a field given the wrong type is OE0251 StructFieldTypeMismatch. These are build-time refusals, named to the field, not deferred to runtime.

Enum values. A payloadless variant is written as a path: Severity::Error, Shape::Circle. A payload variant carries one value and is constructed by applying the variant to that value: Msg::Text("hi"). Enum values compare structurally, the same as structs — Msg::Text("hi") == Msg::Text("hi"), and a payload variant never equals a different variant. A payload variant takes exactly one value; any other count is OE0256 EnumPayloadArity.

pub enum Msg { Text(String), Empty }
pub struct Mail { body: Msg }

pub fn greeting() -> Mail = Mail { body: Msg::Text("hi") };
pub fn blank()    -> Mail = Mail { body: Msg::Empty };

User-concept generics are decorative. A user-declared generic enum Opt<T> (or struct) parses, but its type parameters reach no storage slot, so applying it — Opt<Int> — is refused (OE0235). The optional and result shapes used in practice are the library generics Option<T> / Result<T, E> and the optional-field form T?, whose argument shapes the elaborator does interpret. Payload binding for the optional form is the rule-body is Some(a) / is None test (next paragraph) or a value-position match expression (let v = match opt { Some(x) => x, None => d };, below); a payload-binding arm in statement position refuses with OE1319.

Reading an enum payload — is Some(a). Inside a rule body, an optional field’s payload binds with the membership test path is Some(binder), and absence tests with path is None. A present field materializes one row binding the payload; an absent field materializes none, so the surrounding conjunction fails (RFD 0007 Rule-atom grammar):

pub type Person { mut age: Int? }

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

Reading an enum payload — value-position match. A match expression in value position — a let right-hand side, a comparison operand, a fn body, a return/require value — binds an enum payload and evaluates. let r = match opt { Some(x) => x, None => 0 }; reads the payload into x and yields the selected arm’s value; this is the idiomatic way to read or consume an enum value. The arm binds exactly one variable positionally; a zero-, multi-, or record-binder arm is OE0257 EnumPayloadPattern (Expression grammar).

pub enum Opt { Some(Int), None }

test "value-position match binds the payload and evaluates" {
    let some = Opt::Some(7);
    let none = Opt::None;
    assert (match some { Opt::Some(x) => x, Opt::None => 0 })  == 7;
    assert (match none { Opt::Some(x) => x, Opt::None => 99 }) == 99;
}

A payload-binding arm in statement position — an effectful arm body inside a mutate statement-match, e.g. match opt { Some(v) => { let _ = insert T { n: v }; }, None => {} } — refuses with OE1319 rather than silently mis-evaluating. Bind the payload in value position (let v = match opt { … };) first, then run the effect. The rule-body is Some(a) form above is the other supported reader; the constant-pattern subset of match (payloadless variants, literals, _) executes in both positions (Pattern matching).

Field defaults. The field-default form field: Type = expr refuses with OE0237 FieldDefaultUnsupported: the parser recognizes the = expr clause and rejects it loudly rather than silently dropping the default. Supply the value at the construction or kind-level binding site, or use the from-navigation form (next paragraph) for a derived value.

Field navigation views — from. Unaffected by the above: a field may carry a from Rel.endpoint navigation-view clause supplying a derived value (RFD 0005, relation subsumption). This form is parsed and elaborated normally; it is the supported way to compute a field’s value from related entities.

Field mutability — mut. A field declaration may carry the mut modifier between any leading attributes and the field name: mut field: Type. Without mut, the field is immutable post-construction — its value is fixed at the construction site (or by #[intrinsic] kind-level binding, or by from-clause derivation) and may not subsequently be re-assigned. With mut, the field admits update-stmt writes inside mutate bodies (mutate).

pub type Person {
    name: String,                          // set at construction; not updatable
    dob: Date,                             // set at construction; not updatable
    #[intrinsic] ssn: String,              // must be set at kind binding; not updatable
    mut current_address: String,           // updatable via `update`-stmt
    mut current_employer: Company?,
    #[intrinsic] mut current_role: Role,   // required at construction AND updatable later
}

mut is orthogonal to the other field-decl modifiers: #[intrinsic] governs construction-time required-ness, not updatability (both can apply); a mut on a from-derived field is contradictory and rejected with OE0822 MutOnDerivedField; a default = expr supplies a fallback at construction; the metatype’s fixed modifier (metatype, mutate) governs whether iof classification can change, not whether fields can, so a fixed kind admits mut fields. The modifier reads identically on struct, enum-variant, and vocabulary-concept fields. Mutations lower to append-only retract/assert event pairs on the axiom log (Storage layer); the proposition’s (entity_id, property_id) identity is stable across edits, so bitemporal queries reconstruct prior values (Temporal substrate).

Vocabulary concepts and the generic type metatype

When a vocabulary metatype is in scope, its name introduces a concept:

// A declaration is terminated by exactly ONE of: its `{ }` body, its `{ }`
// cover, or — when it has NEITHER — a REQUIRED ';' (the same item-termination
// rule as Rust: `struct Foo;` vs `struct Foo { … }`). A missing terminator on
// the bodyless form is `OE0011 MissingTerminator`.
concept-decl    ::= attribute* 'pub'? <metatype-name> Ident generic-params?
                     supertype? refinement-clause? ( cover | body | ';' )
supertype       ::= specialization? instantiation?
specialization  ::= '<:' TypeExpr (',' TypeExpr)*
instantiation   ::= ':' TypeExpr (',' TypeExpr)*
cover           ::= '{' variant (',' variant)* ','? '}' // bare-ident members; self-terminating
body            ::= '{' (field-decl | instance-value) (',' …)* ','? '}'   // self-terminating — no ';'
instance-value  ::= Ident '=' expr                     // see body modes below

A cover and a field/instance body share the { … } surface; the member shape distinguishes them. A cover’s members are bare concept names (a brace whose first entry is an Ident followed by , or }), matching enum’s { Circle, Square } and the complete Parent { A, B } group axiom; a body’s first entry carries a : (a field name: Type), :: (a per-target axis override), or = (an instance-value).

The leading identifier (type, or a vocabulary name like kind, subkind, role, phase, category, …) is contextually a concept-introducing keyword — resolved per Name resolution against the pub metatype declarations visible in scope: declared in this package, or imported from a vocabulary package. type is not ambient — it is the std::core baseline, brought into scope by use std::core::{type} or a [package].prelude entry (RFD 0038). An introducer that resolves to no visible pub metatype is refused with OE0605 UnknownMetatype at ox check and ox build.

use std::core::{type};   // the no-commitment baseline, brought into scope (RFD 0038)
pub type Document { title: String, body: String }

// Vocabulary-classified concepts: the vocabulary must be IN SCOPE.
// Here it is declared in-package (the external-vocabulary-package
// pattern — a real UFO package would ship these declarations and be
// imported instead; nothing UFO-related ships with Argon):
pub metatype kind = { };
pub metatype subkind = { };
pub metatype category = { };

pub kind Person { name: String, age: Nat }
pub subkind Adult <: Person iff { self.age >= 18 };   // defined class: auto-classified (Refinement)
pub category Animal;

// Concept with a cover — the fields attach to each variant via subkind hierarchy.
pub kind Vehicle { Car, Truck, Motorcycle }
pub subkind Car         <: Vehicle { license_plate: String }
pub subkind Truck       <: Vehicle { license_plate: String, cargo_kg: Nat }
pub subkind Motorcycle  <: Vehicle { license_plate: String, weight: Real }

Supertype clauses. <: T declares specialization (intra-classification subtyping): Adult <: Person says every adult is a person. : T declares iof-instantiation: pub kind USD : Currency says USD is an instance of the higher-order type Currency. Both clauses are general substrate features — neither commits to any specific higher-order theory. Higher-order theories like MLT (the unprivileged mlt package, Higher-order modeling, Stdlib (selected)) interpret the order arithmetic over :; the substrate itself only enforces that iof is well-founded and acyclic.

Multiple parents on either axis. Both clauses admit a comma-separated list, and both can co-occur on a single declaration:

pub subkind Penguin
    <: FlyingAnimal, AquaticAnimal              // specializes two kinds at order n
    :  Vertebrate_Species, Endangered_Species   // instance of two categories at order n+1
{
    name: String,
    body_plan   = "tetrapod",
    iucn_status = IucnStatus::Vulnerable,
}

When both clauses are present the canonical order is <: then :, mirroring the order arithmetic (specialization parents at the concept’s own order, instantiation parents one above). The order is a style convention, not a rule: both clauses are independent (parents are an unordered set on each axis), so either source order parses and means the same thing — writing : before <: is accepted with the OW0010 style warning (never an error), and oxfmt normalizes it to the canonical order. All parents in a single <: clause must be at the same order; all parents in a single : clause must be at one order above. Unprivileged theory packages (e.g. mlt) enforce additional cross-parent constraints over the iof DAG.

Diamond resolution. When multiple parents (on either axis) declare a field with the same name, the elaborator rejects the declaration with OE0208 AmbiguousFieldFromMultipleParents. The modeler resolves the ambiguity by qualifying the field with its parent:

pub category Vertebrate_Species { habitat: String }
pub category Endangered_Species { habitat: HabitatProtectionZone }

pub subkind Penguin : Vertebrate_Species, Endangered_Species {
    Vertebrate_Species::habitat = "Antarctic coast",
    Endangered_Species::habitat = HabitatProtectionZone::IUCN_II,
}

Field access from instances follows the same qualification when ambiguous: bar.habitat is rejected with OE0208; the modeler writes bar.Vertebrate_Species::habitat to disambiguate. The substrate offers no automatic merge, override-by-position, or last-wins behavior — every collision is resolved explicitly. (This is consistent with how Argon’s trait system handles method-name collisions; see Trait atom.)

Body modes when : T is present. When a concept is declared as an iof-instance of another (pub kind USD : Currency { … }), the body admits two statement kinds:

• field = value — sets the value of a field defined on the target T. This is the kind-as-instance facet: USD is filling in fields that Currency declared on its instances.
• field: Type — declares an instance-level field that the kind itself will carry forward to its own instances. This is the kind-as-kind facet: every USD bill will have its own serial_number.

pub category Currency {
    #[intrinsic] iso_code: String,
    #[intrinsic] decimal_places: Nat,
    symbol: String,
}

pub kind USD : Currency {
    iso_code       = "USD",        // value for the Currency-defined field
    decimal_places = 2,
    symbol         = "$",

    serial_number: String,         // instance-level field on bills
    denomination:  Nat,
}

let my_twenty = USD { serial_number: "L12345678A", denomination: 20 };

#[intrinsic] on a field declares it must be set at kind level by every iof-instance. Cross-level binding diagnostics: OE1901 InstantiationFieldNotInTarget (a = binding names a field absent from the target metatype), OE1902 InstantiationFieldShadows (a : field shadows an inherited one), OE1908 IntrinsicPropertyMissing (a required #[intrinsic] field is left unbound), and OE0208 AmbiguousFieldFromMultipleParents (a field declared by multiple parents, unqualified). Theory-specific cross-level constraints (e.g., MLT’s categorization / partition / subordination / powertype rules) are not compiler diagnostics: a higher-order theory ships as an unprivileged package (e.g. mlt, Higher-order modeling) and authors those constraints as its own rules/checks over the neutral substrate; see appendix C.

Field access through the iof chain. For an instance bar: SomeKind where SomeKind : SomeCat and SomeCat declares field x, the access bar.x is resolved by walking up the iof chain:

1. Instance fields first. If bar has x declared as an instance-level field (via x: Type in SomeKind’s body), return bar’s own value.
2. Kind-level values next. Otherwise, look at meta(bar) = SomeKind. If SomeKind set x = value at its kind level, return that value.
3. Walk further up. If SomeKind itself does not bind x, continue: meta(meta(bar)), etc., until either x is found or the chain bottoms out at an entity with no further : parent.
4. Not found. Error: OE0101 UnresolvedName (or a more specific field-not-found variant).

Three equivalent surface forms reach the same value when x lives at the kind level:

Shadowing across levels. If x is bound at both an instance level and a higher kind level — different types, or the same type with different values — the elaborator rejects the declaration with OE1902 InstantiationFieldShadows. Modelers either rename, or accept the shadow explicitly by writing meta(bar).x / SomeKind.x when they need the kind-level value. There is no implicit override.

Relations

Like concepts, relations are introduced by a vocabulary-defined metarel — there is no built-in rel keyword at lexer level. Stdlib ships a generic metarel std::core::rel<E1, E2>(E1, E2) for ontology-uncommitted relations; vocabulary packages can ship richer metarels (mediation, material, etc.) or re-export the generic.

// Same terminator rule as a concept (Vocabulary concepts and the generic `type` metatype): the `{ }` rel-body self-
// terminates; the bodyless form requires a ';' (`OE0011` if absent).
rel-decl         ::= attribute* 'pub'? <metarel-name> Ident '(' rel-param-list ')'
                      cardinality-list? rel-supertype? ( rel-body | ';' )
rel-supertype    ::= ('<:' | 'specializes') TypeExpr (',' TypeExpr)*
rel-param        ::= Ident ':' TypeExpr
cardinality-list ::= cardinality+                       // one slot per endpoint
cardinality      ::= '[' range ']'
range            ::= Nat '..' Nat | Nat '..' '*' | Nat '..=' Nat | Nat
                  // In cardinality position, `..` is INCLUSIVE on both ends
                  // (UML convention): `[1..1]` means exactly one, `[0..*]`
                  // means zero or more. Distinct from Rust range semantics.
rel-body         ::= '{' field-list '}'

The leading identifier (after pub) is contextually a metarel-introducing keyword, resolved per Name resolution against the pub metarel declarations visible in scope — declared in this package or imported from a vocabulary package; rel is not ambient — the std::core baseline is brought in by use std::core::{rel} or a [package].prelude entry (RFD 0038). An unresolved introducer is refused with OE0606 UnknownMetarel. The parser disambiguates concept-decl (no (...) after the new name) from relation-decl (has (...)).

Three surface forms (using the std::core baseline, brought into scope via use std::core::{type, rel};):

use std::core::{type, rel};
// Form A — anonymous binary field on a concept
pub type Person { children: [Person] }

// Form B — named relation with optional navigation views
pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];
pub type Person {
    parents:  [Person] from ParentOf.parent,
    children: [Person] from ParentOf.child,
}

// Form C — n-ary relation with intrinsic property body
pub rel Marriage(spouse_a: Person, spouse_b: Person) [0..1] [0..1] {
    since:  Date,
    status: MarriageStatus,
}
pub rel Transaction(seller: Person, buyer: Person, item: Asset) {
    amount: Money,
    at:     DateTime,
}

Cardinality (positional, UML association-end convention). For a relation with endpoints e₁, e₂, …, eₙ, the i-th cardinality slot bounds the number of distinct eᵢ for each fixed combination of all the other endpoints — the UML association-end multiplicity. (Equivalently: hold every endpoint but the i-th fixed, and the slot bounds how many distinct eᵢ may complete the tuple.) Omitted slots default to 0..*. For binary relations the slots read left-to-right; pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*] reads “each child has 1..1 parents (slot 1 bounds the parents per fixed child); each parent has 0..* children (slot 2 bounds the children per fixed parent).” For n-ary relations the same per-position rule holds against the fixed combination of the others; pub rel Transaction(seller, buyer, item) [0..*] [0..*] [0..1] reads “for each (buyer, item) pair, 0..* sellers; for each (seller, item) pair, 0..* buyers; and for each (seller, buyer) pair, 0..1 items.”

Anonymous-field cardinality default. A field declared with the inline anonymous-relation form field: [T] (Form A) synthesizes a binary relation with default cardinality 0..* and Set semantics. To bound: field: [T; n..m]. To opt into ordered list semantics: field: [T; n..m, ordered] (lowers to List<T>). [T; <=1] emits OW2402 suggesting T? (Option<T>) instead.

Anonymous fields are structural shorthand: they do not engage the metarel calculus. No metarel name is attached; the synthesized relation is accessed only via dot-traversal. This is symmetric with struct/enum, which are likewise language-level structural and carry no metatype. Named relations (Forms B and C) require a metarel-introducing keyword in scope.

[T] on struct vs concept. On a struct or enum field, [T] is plain List<T> — no synthesized relation, no closure traversal, no metarel. On an ontologically-classified concept (declared under a metatype), [T] is Form A — a synthesized binary relation supporting closure traversal (alice.children+(b)). The difference is whether the enclosing declaration is data (struct/enum) or ontology (declared under a metatype — type or a vocabulary introducer).

When to upgrade Form A to Form B or C. Promote an anonymous field to a named relation when any of: (a) the relation needs to be classified under a metarel (mediation, material, …) so the substrate can reason over its properties; (b) the relation carries intrinsic data of its own (since: Date, amount: Money); or (c) the relation must be referenced as a first-class predicate from rule bodies (derive ancestor(d, a) :- ParentOf(d, a), …). When none of those apply, Form A is the right choice.

Generic relation-property characteristics. A named relation (rel or metarel) may carry the standard relation-algebra property characteristics (the OWL object-property characteristics) — PL/DB-neutral, describing the shape of the relation’s extent with enforcement, not an ontological commitment. All four are shipped by the std::rel standard-library package and must be brought into scope — use std::rel::{transitive, irreflexive, asymmetric, functional} (nothing is ambient — Name resolution / RFD 0038). #[transitive] is a genuine declarative macro (it expands to the closure derive). #[irreflexive] and #[asymmetric] are genuine procedural macros (RFD 0040): they re-emit the relation and paste the guarding check’s internal __{rel}_{prop} head via concat_idents. They read the relation’s name, so they apply to a rel; on a metarel they decline (the invocation is refused, OE0723). #[functional] is a builtin-backed macro (the #[rustc_builtin_macro] analogue, RFD 0037 D8) — the library owns the surface while a privileged compiler path implements it (a [0..1] cardinality cap on a rel’s target, or a guarding check on a metarel); re-emitting a rel with a modified cardinality bracket needs structural reflection. A characteristic applied without its import is refused — OE0705 for the macros #[transitive]/#[irreflexive]/#[asymmetric], OE1362 for the builtin #[functional]. Multiple characteristics compose on one declaration.

use std::rel::{transitive, irreflexive, asymmetric, functional};

#[transitive]
#[irreflexive]
#[asymmetric]
pub rel is_proper_part_of(part: Top, whole: Top);

#[functional]
pub rel inheres_in(burden: Aspect, bearer: ConcreteIndividual);  // each aspect inheres in one bearer

Enforcement applies to the declared relation’s own extent. Propagation of a property borne by a metarel to the relations it classifies is out of scope (Out of scope). A characteristic applied without importing it from std::rel is refused — OE0705 for the macros #[transitive]/#[irreflexive]/#[asymmetric] (genuine macros, not directives), OE1362 for the builtin #[functional]. On a non-relation declaration (a concept, a rule), the still-directive #[functional] is refused with OE0707 (invalid position); the procedural #[irreflexive]/#[asymmetric] instead decline (the invocation is refused, OE0723), as they do on a metarel. (The ontology-specific relation properties — MLT’s #[partitions], #[categorizes], etc. — are vocabulary decorators and live in their packages, distinct from this generic family.)

impl Type { … } — grouping

impl-block ::= 'impl' generic-params? TypeExpr  '{' impl-item* '}'      // grouping
            |  'impl' generic-params? TypeExpr 'for' TypeExpr '{' trait-impl-item* '}'   // trait impl

The grouping form admits any declaration kind (impl-item); the trait-impl form is restricted to the contract member forms (trait-impl-item: fn / mutate / derive / check / query) and is governed by the conformance obligations of the trait surface and conformance (RFD 0026).

impl Person {
    pub fn greeting(self) -> String = "Hello, " + self.name;       // instance method
    pub fn adult(p: Person) -> Bool = p.age >= 18;                  // associated function
    pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];  // lexically grouped
    pub query oldest() -> Option<Person> {
        select p from p: Person order by p.age desc limit 1
    }
}

An impl Type block accepts any declaration kind: methods, associated functions, relations, queries, mutations, checks, associated type / const. All declarations inside the block are namespaced under Type::. Methods (items with self first parameter) are additionally accessible via UFCS dot-notation (alice.greeting()); associated functions and relations are reachable only as Type::name(args).

impl Person {
    /// Instance method (has `self`): both `alice.greeting()` and `Person::greeting(alice)` work.
    pub fn greeting(self) -> String = "Hello, " + self.name;

    /// Associated function (no `self`): reached as `Person::adult(p)`.
    pub fn adult(p: Person) -> Bool = p.age >= 18;

    /// Type-associated relation: reached as `Person::ParentOf(a, b)`.
    pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];

    /// Method-shaped query: `alice.oldest()` and `Person::oldest(alice)` both work.
    pub query oldest() -> Option<Person> {
        select p from p: Person order by p.age desc limit 1
    }
}

A relation declared inside impl Type is not exposed at module level. Choose the placement (module level, inside a topic mod, or inside impl Type) according to the semantic association the modeler intends — see Connecting concepts and relations.

Connecting concepts and relations

A relation is first-class, but where it is declared expresses its semantic association with the participating concepts. Three placements coexist; the modeler picks by intent:

• Module level — a free predicate owned by no single endpoint: pub rel ConnectedTo(a: Node, b: Node) [0..*] [0..*];, accessed as ConnectedTo(x, y) anywhere in the module.
• Topic mod — grouped with related concepts; accessed as family::ParentOf(a, b) after use family::*;.
• impl Type (impl Type { … } — grouping) — conceptually “about” the type, alongside its methods; accessed as Person::ParentOf(a, b) only, not at module level.

Navigation from a concept value to its participations. Three mechanisms link an instance to the relations it participates in.

1. Field-form navigation view (cheapest, declarative):

pub type Person {
    parents:  [Person] from ParentOf.parent,    // alice.parents
    children: [Person] from ParentOf.child,     // alice.children
}

Each field is a derived view over the relation. The compiler verifies the field type matches the role’s endpoint type and that cardinality is consistent with the relation’s per-endpoint cardinality. The view materializes against the relation’s closed extent: because relation subsumption (Relations) makes a subsumed relation’s tuples tuples of its supersuming relation, a view over Rel.endpoint includes the endpoints contributed by every <:-subsumed relation — so a subtype that refines an inherited collection by projecting from a subsumed relation (SatisfactionAccount.records from satisfactionAccountRecords <: recordAccountRecords) sees exactly its narrower elements.

2. UFCS method via impl (richer navigation):

impl Person {
    pub query siblings(self) -> [Person] {
        select s from ParentOf(p, self), ParentOf(p, s) where s != self
    }
}

Methods are appropriate when navigation requires filtering, joining, ordering, or aggregation beyond a simple projection. Accessed as alice.siblings().

3. Direct rule-body invocation (always available):

pub derive grandparent(g: Person, c: Person) :- ParentOf(g, p), ParentOf(p, c);

Inside any rule body, the relation is a predicate addressable by name (or by qualified path: family::ParentOf(...), Person::ParentOf(...)).

Inverse declaration (when both sides are field-form):

pub type Country { citizens: [Citizen] }
pub type Citizen {
    #[inverse(Country.citizens)]
    countries: [Country],
}

The compiler verifies cardinality consistency and exposes both navigation directions over a single synthesized relation.

Naming convention. Relation names are CamelCase (per Identifiers) — ParentOf, Marriage, IsCitizenOf — symmetric with the CamelCase of metatype-introduced concepts. The name plus argument order encodes semantic direction; ParentOf(p, c) reads “p is the parent of c.” The convention is the modeler’s responsibility — the language does not enforce it. Use field-form views or methods to expose semantically-named navigation in the opposite direction.

Three import postures

A modeler picks an ontological posture per module by choosing what to use. Three cover almost all code:

// Posture 1 — pure data, no ontology. `struct`/`enum` are lexer built-ins.
use std::math::Nat;
pub struct Receipt { lease_id: Nat, paid: Money, at: Date }
pub enum Severity { Error, Warning, Info, Hint }

// Posture 2 — generic ontological commitment via the std::core
// baseline, brought into scope explicitly (RFD 0038).
use std::core::{type, rel};
pub type Document { title: String, body: String }
pub rel Cites(citer: Document, cited: Document) [0..*] [0..*];

// Posture 3 — vocabulary-classified. The vocabulary is an ordinary
// EXTERNAL package — here a hypothetical third-party UFO package;
// nothing UFO-related ships with Argon or its stdlib — or the module
// declares its own `pub metatype` / `pub metarel` vocabulary locally.
use ufo_foundational::prelude::*;   // a third-party vocabulary package
pub kind Person { name: String, age: Nat }
pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];
pub mediation Involves(m: Marriage, p: Person);

Postures compose and are per-module, not per-package: a module may use the imported std::core baseline (use std::core::{type, rel}, or via the package prelude) alongside another imported (or locally-declared) vocabulary, and a package may ship modules in different postures behind one prelude. The metatype calculus (Meta-calculus atom) distinguishes the declarations by the keyword in declaration position.

Group axioms — disjoint, complete, partition

A group axiom constrains a set of sibling concepts collectively: that they never overlap, that they jointly exhaust a parent, or both. The three forms share one declaration shape — a contextual keyword, an optional parent, and a brace list of member concept paths:

disjoint  { Cat, Dog, Fish }            // pairwise non-overlapping
complete  Animal { Cat, Dog, Fish }     // jointly exhaustive over Animal
partition Animal { Cat, Dog, Fish }     // disjoint AND complete

The keywords (disjoint / complete / partition) are contextual — they lex as ordinary identifiers and bind as group-axiom keywords only in declaration position followed by the group-axiom shape, so they remain available as concept and field names elsewhere. A group axiom introduces no name of its own; it names existing concepts.

disjoint { A, B, C } asserts the members are pairwise non-overlapping: no individual is an instance of two of them at once. Disjointness is instance-level. A write that would classify one individual into two declared-disjoint members is refused (OE0240), so the contradictory state never enters the store. disjoint takes no parent — the members need not share a supertype.

complete Parent { A, B, C } asserts the members jointly cover Parent: every Parent instance is an instance of at least one member. Under the closed-world default (Type system), a Parent instance derivable into none of the members is an uncovered instance, and the write that creates it is refused (OE0241). Each member must be a subtype (<:, transitively) of Parent, checked at elaboration (OE0243 otherwise). Completeness has a second, static half: if the schema declares an instantiable (non-abstract) concept S <: Parent that specializes none of the members, the cover is provably incomplete and the build is refused (OE0242) — an abstract subtype, having no direct instances, is exempt. This static gate ranges only over the concepts declared in the same file as the group axiom; a subtype introduced in another module is not seen at this point, so its covering is left to the runtime OE0241 guard rather than refused statically.

partition Parent { A, B, C } is the conjunction: the members are both disjoint and complete over Parent. It imposes the OE0240 overlap guard, the OE0241 covering guard, and the OE0242 / OE0243 static gates together.

Disjointness and covering are enforced as ordinary substrate checks (Rule atom — fn, derive, query, mutate, check) the compiler synthesizes from the declaration — one overlap check per unordered member pair, one negation-as-failure covering check per cover — so a violating write is refused by the same delta-guard that enforces a hand-written check, with no separate axiom machinery. The covering check is closed-world: it fires when no member membership is derivable. Its interaction with a concept’s #[world(open)] assumption is specified in World assumptions (CWA / OWA) (RFD 0045).

A degenerate group axiom synthesizes no runtime check, because it has nothing to guard. An empty disjoint { } and a one-member disjoint { A } have no unordered pair to overlap, so no overlap check is produced and the declaration is accepted in silence. An empty complete Parent { } likewise produces no covering check — but it still meets the static cover gate above, so any instantiable subtype of Parent (including Parent itself, if non-abstract) is then provably uncovered and the build is refused (OE0242).

Types and refinement

Generics

Angle brackets, Rust-aligned:

generic-params ::= '<' generic-param (',' …)* '>'
generic-param  ::= Ident ('<:' TypeExpr ('+' TypeExpr)*)?

Type arguments at call site use turbofish for disambiguation: sort::<Money>(prices).

Subtyping

A <: B declares A is a subtype of B. Two universal bounds frame the lattice: A <: Top and Bot <: A hold for every A.

Beyond the declared <: graph, the substrate has three built-in subtyping sources (oxc-check/src/infer.rs::types_compatible):

• Numeric tower: Nat <: Int <: Real and Nat <: Int <: Decimal. Money is not in the tower — there is no implicit Int → Money; Money only arises through the result-side widening of monetary arithmetic (Numeric tower and coercion), Money ▷ Decimal ▷ Real ▷ Int.
• Covariant collections: List<A> <: List<B> and Option<A> <: Option<B> iff A <: B (written [A]/A?).
• Invariant elsewhere: tuples, fn(…) -> _, and generic applications subtype only by equality.

Real, Decimal, and Money are exact arbitrary-precision rationals (BigRational); source numeric literals parse to exact rationals with no f64 round-trip, so 0.1 + 0.2 == 0.3 (RFD 0016, oxc-reasoning/src/compile/value.rs).

Refinement

refinement-clause ::= ('where' | 'iff') '{' refinement-pred (',' …)* '}'
refinement-pred   ::= D1Pred | D2Pred

A refinement attaches a predicate to a concept. The keyword chooses how the predicate relates to membership — the description-logic split between a primitive class (⊑, necessary conditions only) and a defined class (≡, necessary and sufficient conditions). See RFD 0017.

• where { P } — primitive. P is a necessary condition: every member satisfies it, but a supertype instance that merely satisfies P is not thereby a member. Membership is asserted (by construction or insert iof, mutate); P is enforced as an invariant at each membership write and never widens the extent. This is Rust’s where bound lifted to a concept’s members — a constraint, not a definition.
• iff { P } — defined. P is necessary and sufficient: an instance of the supertype is a member if and only if it satisfies P. Membership is derived — the substrate auto-classifies and rejects manual insert iof (mutate, OE0211). Reads as the membership biconditional: “an Adult is a Person iff age >= 18.”

pub type Adult          <: Person  iff   { self.age >= 18 && self.has_id };   // defined: any qualifying Person is automatically an Adult
pub type ExtinctSpecies <: Species iff   { self.living_count == 0 };          // defined: classification derived from state
pub type VettedVendor   <: Vendor  where { self.risk_score <= 30 };           // primitive: vetting is conferred; the score is a necessary invariant on members

D1Pred (substrate-locked): metaEq, isDet, hasAnc, hasDesc, countGeq, forallC, existsC, plus Booleans. D2Pred: QF-LIA, GNFO, enum equality. The elaborator stages D1 ahead of D2 residual.

Mechanically: D1Pred / D2Pred / MixedPred are inductives at spec/lean/Argon/Decidability/Fragment.lean; the staging theorem stage_correct lives at CrossDomain/Staging.lean; the polynomial bound on D1 evaluation (d1EvalCost n φ ≤ d1Size φ · (n+1)^(d1QuantifierDepth φ)) is proven in Complexity/Bounds.lean. The bound grounds the polytime claim Tier ladder makes for tier:structural and tier:closure.

Three-valued membership under OWA. When the governing world assumption is open (World assumptions (CWA / OWA)), iff-derived membership is three-valued: success requires positive evidence that the predicate holds. A value whose predicate evaluates to unknown does not satisfy the refinement — matching SHACL’s sh:Violation discipline and SQL’s three-valued NULL semantics. Under CWA, unknown collapses to false. The mechanization at TypeSystem/Soundness/CwaOwa.lean proves that CWA-true refinement results survive transition to OWA (monotonic knowledge transfer). The symmetric rule for a primitive where invariant: a membership write is rejected only on positive evidence of violation (P evaluates to a definite false); unknown permits the write (mutate, OE0668). unknown means information absence — a referenced field with no recorded value. A predicate that cannot be evaluated at all (an unsupported form, malformed stored data, or a type-mismatched comparison such as ordering a Date against an Int) is not unknown: unsupported forms are refused at build time (OE0660), and anything that slips past the gate fails the operation loudly at runtime — never a silent permit (where) or a silently-empty derived extent (iff). Refinement predicates evaluate on the same exact value tower as every other value position (RFD 0016): exact rationals for Real/Decimal/Money, chronological Date comparison, with no value-dependent enforcement.

Built-in type forms

First-class function values include references to declared fns and closures (Expression grammar); both share the fn(T1, T2) -> U type. Higher-kinded types and runtime trait objects (dyn Trait) are out of scope (Out of scope).

Reflective sorts. Entity, TypeRef, and Metatype are the reflective sorts of the meta-calculus (Reflection), ordered Metatype <: TypeRef <: Entity (and Entity <: Top). These are distinct from Top (Subtyping): Top is the <:-greatest type, whereas TypeRef is the sort whose values are references to declared types. The bounded form TypeRef<C> is sugar for the Refinement refinement { t: TypeRef where specializes(t, C) } (RFD 0017, where = primitive/asserted), with TypeRef == TypeRef<Top>. It is covariant — TypeRef<A> <: TypeRef<B> iff A <: B — which follows directly from the refinement ({t | t <: A} ⊆ {t | t <: B}), adding no new structural subtyping rule. Membership is three-valued under OWA (World assumptions (CWA / OWA), RFD 0007): specializes(t, C) unknown ⇒ not a member. Powertype / order / categorization semantics stay in the unprivileged mlt package (Higher-order modeling); TypeRef<C> carries none of them. See RFD 0023.

? propagation

expr? on a Result<T, E>-typed expression unwraps to T on Ok or returns the Err from the enclosing rule. Admitted in fn and mutate bodies, where the enclosing rule’s return type is Result<U, E> for some U. Not admitted in derive (which has no return type — predicates do not fail) or query (whose return type is the projection type, not a Result); check rules emit diagnostics rather than returning Results. Calling ? outside an admitted context is a parse-time error.

Expression grammar

expr            ::= primary-postfix
                      ((arith-op | comp-op) primary-postfix)*
                      (('not')? 'in' primary-postfix)?
                      ('&&' expr | '||' expr)*

primary-postfix ::= unary-op* primary postfix*
unary-op        ::= '!' | '-'
postfix         ::= '.' Ident '(' expr-list ')'                  // n-arg method call
                  | '.' Ident                                     // field access OR zero-arg method call
                  | '[' expr ']'                                  // index
                  | '[' expr? '..' expr? ']'                      // slice
                  | '?'                                            // try (Result propagation)

primary         ::= literal
                  | '_'                                            // wildcard / anonymous binding (rule-atom arg positions only)
                  | '(' expr ')'
                  | list-or-comprehension
                  | if-expr
                  | match-expr
                  | block-expr
                  | meta-call
                  | aggregate
                  | subquery                                       // `query` (count/set/one/collect/exists braces)
                  | call-expr
                  | path
                  | struct-literal
                  | closure

literal         ::= INT | REAL | STRING | DATE | DATETIME | BOOL

list-or-comprehension
                ::= '[' ']'
                  | '[' expr (',' expr)* ','? ']'
                  | '[' expr 'for' Ident 'in' expr ('where' expr)? ']'

if-expr         ::= 'if' expr block ('else' (block | if-expr))?
match-expr      ::= 'match' expr '{' arm (',' arm)* ','? '}'
block-expr      ::= '{' stmt* expr? '}'
block           ::= '{' stmt* expr? '}'

call-expr       ::= path '(' expr-list ')'
meta-call       ::= 'meta' '(' expr ')'

aggregate       ::= ('sum'|'count'|'min'|'max'|'avg')
                    '(' expr ('for' Ident 'in' expr
                              ('where' expr)? (',' rule-atom)*)? ')'   // RFD 0029: trailing atoms refine the fold

struct-literal  ::= path '{' (struct-init-list)? '}'
struct-init-list ::= field-init (',' field-init)* ','?
                   | '..' expr (',' field-init)* ','?            // struct-update spread
field-init      ::= Ident (':' expr)?                            // `name` shorthand or `name: expr`

closure         ::= '|' closure-params? '|' ('->' TypeExpr)? closure-body
closure-params  ::= closure-param (',' closure-param)* ','?
closure-param   ::= Ident (':' TypeExpr)?
closure-body    ::= expr | block

path            ::= Ident ('::' Ident)*
expr-list       ::= (expr (',' expr)*)?

arith-op        ::= '+' | '-' | '*' | '/' | '%'
comp-op         ::= '==' | '!=' | '<' | '<=' | '>' | '>='        // non-chainable

Precedence (tightest to loosest):

1. Postfix (.f(), [i], [a..b], .field, ?)
2. Unary prefix (!, -)
3. Multiplicative (*, /, %) — left-associative
4. Additive (+, -) — left-associative
5. Comparison (==, !=, <, <=, >, >=) — non-associative (a < b < c is rejected; use a < b && b < c)
6. Membership (in, not in) — non-associative
7. Logical AND (&&) — left-associative, short-circuit
8. Logical OR (||) — left-associative, short-circuit

Turbofish disambiguates generic call sites at expression position: sort::<Money>(prices).

Rounding builtins (RFD 0029). A small family of rounding functions is available in expression position — both in rule-body bindings and in the fn/compute plane — operating exactly over the numeric tower (Decimal stays Decimal, never via f64):

round_half_even is the money default: financial rounding rounds half to even to avoid the systematic upward bias of half-away-from-zero. All four return an exact value (integral results collapse to Int). A wrong argument count is refused at compile with OE1333 RoundingBuiltinArity.

Closures capture environment by value (Argon is value-semantic; no references). A closure’s type is fn(T1, T2) -> U — interchangeable with declared fn references at any function-typed argument or binding.

Property-style accessors. The paren-less postfix .Ident resolves to a stored field if the receiver type declares one with that name; otherwise to a call of a zero-argument method with that name. This unifies the .field and .zero_arg_method() forms — both read obj.name. The 30.days, 5.minutes, 60.seconds shorthand in Numeric tower and coercion is exactly this affordance over zero-arg methods on numeric types. Methods with one or more arguments always require explicit parens.

Struct-literal evaluation. A struct-literal T { … } evaluates each field initializer and assembles a struct value of type T (the data semantics — structural equality, immutability, no identity — are stated in struct and enum — language built-ins (data declarations)). The literal must state every field: a missing field is OE0249, an undeclared one is OE0250, and a field given the wrong type is OE0251. The field shorthand in field-init (a bare Ident with no : expr) takes the field’s value from a same-named binding in scope.

Functional update — the ..base spread. The ..expr form in a struct-init-list constructs a new struct value from an existing one: it evaluates base, copies every field, then overrides the fields the literal restates. Row { ..base, a: 9 } is base with a replaced by 9 and every other field carried over. The result is a fresh value; base is never modified (struct values are immutable, struct and enum — language built-ins (data declarations)). The spread supplies the fields the literal omits, so the every-field rule is satisfied by the base — a spread literal need only name the fields it changes.

pub struct Row { a: Int, b: Int }

test "spread overrides one field and carries the rest" {
    let base = Row { a: 1, b: 2 };
    assert Row { ..base, a: 9 } == Row { a: 9, b: 2 };
    assert base == Row { a: 1, b: 2 };          // base unchanged
}

Field projection. The postfix .f reads field f off a struct value, by structure. Projection nests — outer.inner.v reads v off the inner struct off outer. A field the struct’s type does not declare is OE0254 StructFieldAccessUnknown.

pub struct Inner { v: Int }
pub struct Outer { inner: Inner, tag: String }

test "projection reads through nested struct values" {
    let o = Outer { inner: Inner { v: 7 }, tag: "x" };
    assert o.inner.v == 7;
    assert o.inner == Inner { v: 7 };
}

Enum payload binding in match. The constant-pattern subset of match — payloadless enum constants, literals, or-patterns of those, and _ — executes (Pattern matching). A payload-binding arm (match opt { Some(x) => …x… }) destructures one payload value into one fresh variable, bound over the arm body. In value position — a let right-hand side, a comparison operand, a fn body, a return/require value — this binds and evaluates: let r = match opt { Some(x) => x, None => 0 }; is the idiomatic way to read an enum payload. The arm binds exactly one variable positionally; a zero-, multi-, or record-binder arm is OE0257 EnumPayloadPattern. A payload-binding arm in statement position (an effectful arm inside a mutate statement-match) refuses with OE1319 rather than mis-evaluating; bind the payload in value position first. The rule-body membership test path is Some(binder) / path is None is the other supported reader (struct and enum — language built-ins (data declarations), RFD 0007 Rule-atom grammar).

Functor modules

A module declaration may take type or value parameters, producing a functor module — a module-valued function:

functor-mod  ::= 'mod' Ident generic-params '{' mod-item* '}'
                                                              // generic functor
              |  'mod' Ident '(' param-list ')' '{' mod-item* '}'
                                                              // value-parameter functor
mod-alias    ::= 'mod' Ident '=' path '(' expr-list ')' ';'  // instantiation

Functor modules are instantiated via the mod Name = path(args); alias form introduced in Structure; the body is re-elaborated per instantiation site with the parameters bound. The substrate guarantees monomorphization at elaboration — there is no runtime module dispatch.

mod TaxJurisdiction<J: Jurisdiction> {
    pub type TaxableIncome <: Money;
    pub derive owes_tax(p: Person) :- p.income: TaxableIncome, p.income > 0;
}

mod us_federal = TaxJurisdiction<USFederal>;
mod california = TaxJurisdiction<California>;

Parametric modules, not parametric concepts. Argon admits parameterization only at the module level. There is no parametric pub type Container<T> { … } form — a metatype-classified concept is always a closed, monomorphic classifier. When a modeler wants Container<Apple> vs Container<Orange>, the answer is either (a) a specialization hierarchy (pub type AppleBox <: Container) when the variation is ontological, or (b) a functor module whose body declares the per-instantiation concepts when the variation is parametric. This restriction keeps the metatype calculus first-order and the inference tier classifier decidable; lifting it would require admitting kind-polymorphism into refinement and standpoint federation, both of which are unsound at present without further machinery.

A functor body admits any module-level item: concepts, relations, rules, traits, macros, sub-mods, and other functor modules. Each instantiation produces a fully elaborated namespace; symbols from one instantiation do not unify with symbols from another (us_federal::TaxableIncome and california::TaxableIncome are distinct types, both <: Money).

Functor modules are the canonical mechanism for vocabulary-parameterized libraries (per D-007).

The Path type

Path<NodeT, EdgeT> is the first-class type produced by path-projecting query forms (query). It appears in the built-in type forms (Built-in type forms) because the compiler synthesizes path values from query results; the value-level API lives in the stdlib (std::path).

A path is an ordered, alternating sequence n₀, e₁, n₁, e₂, n₂, …, eₘ, nₘ where m = length(path) is the number of edges. A path of length zero is a single node. NodeT and EdgeT are the least common supertypes of the node and edge values respectively.

Edge values by relation form. Edge values vary with which relation form (Relations) the path traverses:

• Forms B and C — named relations. Each edge value is the relation tuple-entity itself, carrying any intrinsic properties: path.nth_edge(0)?.distance retrieves the distance field of the first edge when the underlying relation declares it.
• Form A — anonymous fields. Each edge value is the structural placeholder Edge<From, To> { from: From, to: To }. Form A carries no metarel classification and no intrinsic data, so the placeholder exposes only endpoint identities.

Heterogeneous chains. When a path traverses relations with differing endpoint types (e.g., user.knows(friend).works_at(company) where knows: User → Person and works_at: Person → Company), NodeT is the join (least common supertype) of User, Person, and Company, and EdgeT the join of the involved relation types. When no common supertype is in scope, both fall back to Top. Modelers needing precise heterogeneous typing decompose into single-relation queries and join at the modeler level.

Hyperedges. Paths are over binary relations only. n-ary relations (pub rel Transaction(seller, buyer, item)) are queryable but not path-traversable; hypergraph traversal semantics is out of scope (Out of scope).

API. The shape/projection/fold operators (length, nodes, edges, nth_edge, reverse, concat, map_*, …) are stdlib API on impl<N, E> Path<N, E> in std::path — see Stdlib (selected). The type-system-relevant facts: cost(self) -> Real lives in a conditional impl gated on E <: Weighted (the Rust-aligned conditional-impl pattern), so a uniform Path<N, E> admits cost() only when the edge type implements the std::path trait Weighted { fn weight(self) -> Real; }; without it, shortest-path queries rank by edge count. The Form-A edge value is the placeholder pub struct Edge<A, B> { from: A, to: B } — no metarel classification, just a first-class edge for uniform iteration.

Equality. Path<N, E> has structural equality: two paths are equal iff their node and edge sequences match position-by-position. Paths are value-semantic and immutable; all transformations produce new path values.

Temporal substrate

Why bitemporal

The substrate before this section operates on a single state mapping concepts to extents. The mutation grammar (mutate) advances the state from snapshot to snapshot; prior snapshots are not addressable. This section introduces the bitemporal substrate: every fact carries a valid time and a transaction time. Bare queries default to the current snapshot; explicit temporal operators address the past, the future, and the historical record of the system’s beliefs.

The formalism is DatalogMTL (Wałęga et al., IJCAI 2019) with stratified negation (Tena Cucala et al., AAAI 2021) over the integer timeline; the reference reasoner is MeTeoR (Wałęga et al., AAAI 2022).

Valid time and transaction time

Two interval annotations on every fact (and every relation tuple):

• Valid time (VT) — when the fact holds in the world. [VT_start, VT_end], with open-ended [VT_start, ∞] for ongoing.
• Transaction time (TT) — when the system recorded the fact. [TT_start, TT_end], with open-ended [TT_start, ∞] for current belief.

The snapshot view is the projection ${,\mathsf{iof}(x, T),\mid,VT_{\text{start}} \le \mathit{now} \le VT_{\text{end}} ;\wedge; TT_{\text{start}} \le \mathit{now} \le TT_{\text{end}},}$. Bare rule atoms and bare queries default to this view.

The bitemporal extension applies uniformly to all relations, not just iof. A pub rel Enrolment(s: Person, u: University) tuple carries VT and TT just like an iof fact.

Mechanized at spec/lean/Argon/Reasoning/Temporal.lean (BiState as the bitemporal State; TTHistory and TTMonotone for the transaction-time invariant). The bitemporal extension is additive — the termination machinery of Argon.Reasoning.State lifts pointwise without modification.

Retroactive correction and audit

Mutations that close a VT interval retroactively (delete iof(x, T) at #PAST-DATE#) do not erase the prior record. They close its TT interval at now and append a new record with the corrected VT. Audit queries as of TT = #PAST-DATE# reconstruct what the system believed at any past point. The substrate is append-only by default; explicit erasure (forget), crypto-shredding (#[shred_on_forget]), and #[retention(…)] bounds are storage-layer concerns specified in mutate and Storage layer.

Three-valued evaluation under OWA

Under open-world assumption, temporal atoms evaluate to Is | Not | Can. The since and until operators (see Temporal rule atoms) lift to three-valued via the strong-Kleene meet/join tables that truth values defines, composed pointwise across the interval. Unknown temporal extent projects to Can, never to Both — there are no conflicting witnesses, just single-source uncertainty.

Temporal sub-tier

Temporal expressiveness is an orthogonal sub-tier on top of the main tier ladder. Every program has a tier pair (main, temporal) — see Tier ladder.

Rule atom — fn, derive, query, mutate, check

Argon distinguishes the definition of derived predicates (derive) from inference tasks over the resulting theory (query). derive populates IDB predicates that other rule modes can join against, contributing to the inductive closure. query consumes them and returns a typed value with no IDB side-effect. The split mirrors IDP’s { … } inductive-definition block vs. propagate/expand inference tasks. fn is pure value computation over its arguments; mutate is the only side-effecting verb; check emits diagnostics observer-only (lowers to Cat3 — never populates the IDB).

Purity ladder

fn and query are cacheable on (args, state_version). derive is stratified fixpoint. mutate is transactional.

fn

fn-decl ::= attribute* 'pub'? 'fn' Ident generic-params? '(' param-list ')' '->' TypeExpr fn-body
fn-body ::= '=' expr ';'                          // single-expression
         |  '{' stmt* expr? '}'                    // block, implicit return
param   ::= 'self' | Ident ':' TypeExpr

self and Self. Argon is value-semantic; there is no reference or borrow form. self is always owned-by-value (no &self / &mut self) and is admitted only as the first parameter of a method inside an impl block or a trait declaration; its type is the enclosing impl’s target. Self resolves to the implementing type in trait declarations, to Type inside impl Trait for Type, and to Type inside bare impl Type { … }.

pub fn rent_per_day(l: Lease) -> Money = l.monthly_rent / 30;

pub fn classify(area: Decimal) -> Size {
    if area < 50.0 { Size::Small }
    else if area < 200.0 { Size::Medium }
    else { Size::Large }
}

pub fn safe_div(a: Money, b: Money) -> Result<Money, Diagnostic> {
    if b == 0 {
        Err(Diagnostic { severity: Severity::Error, code: "Math::DivZero", message: "..." })
    } else {
        Ok(a / b)
    }
}

derive

derive-decl ::= attribute* 'pub'? 'derive' Ident '(' param-list ')'
                  ( ':-' atom-list )? ';'
atom-list   ::= atom (',' atom)*
atom        ::= predicate-call | comparison | type-test | 'not' atom | path-pattern

pub derive ancestor(d: Person, a: Person) :- ParentOf(d, a);
pub derive ancestor(d: Person, a: Person) :- ParentOf(d, p), ancestor(p, a);
pub derive senior(p: Person) :- p: Person, p.age >= 65;

// Ground-fact form (no body, concrete args): the head holds for the named terms.
pub derive iof(Type, Type);                                    // MLT* OL3
pub derive Within(usc26, usc);                                 // seed a derived predicate

Multiple derives with matching head name and arity compose as Datalog union (modulo the stratification check below). not atom is NAF, evaluated under well-founded semantics. A derive with no :- clause is bodiless, and its head arguments decide its reading:

• Concrete arguments → a ground fact. When every head argument is a concrete term — a declared individual (Within(usc26, usc)), an enum constant, an axis value, or a type reference (iof(Type, Type)) — the bodiless derive declares that tuple as a ground fact, equivalent to :- true. This is the sanctioned way to seed ground tuples directly on a derived predicate: the seed tuples union with the head’s other derive clauses and rules over the same relation node (same name, same arity), so a recursive rule reads them and computes their closure (seeds ∪ derived-closure). A non-concrete (free-variable) argument is the error — a bodiless derive has no body to range-restrict it — and is refused with OE1342, the bodiless analogue of OE1303 (below), naming the offending argument and directing you to declare the individual or add a :- … body.
• Type-annotated parameters → an empty predicate. A bodiless head whose arguments are typed parameters (pub derive adult(p: Person);) introduces the predicate with that signature and an initially empty extent — the introduce-empty idiom (Rule-atom grammar). Its rows arrive from later same-head derive clauses.

Every body-carrying rule must be range-restricted (safe): each variable in the head, in a negated (NAF) atom, or in a comparison/compute operand is bound by some positive body atom; an unsafe rule is refused at compile (OE1303), since an unbound variable would silently project Null or mis-evaluate.

Evaluation model. A derive program denotes the tuples its rules derive, under the semantics fixed in Reasoning: the least fixpoint of the positive program, stratified negation layered along the axis dependency graph, and — for a negation cycle no stratification can layer — the well-founded model computed by the alternating fixpoint. The surface consequences a rule author relies on:

• Recursion through negation is accepted. A negation cycle (p :- not q, q :- not p) that strict stratification cannot layer is evaluated under well-founded semantics rather than refused. Cross-stratum, acyclic NAF is ordinary stratified negation. (OE1309 no longer fires from stratification; it survives only as the dispatch seam.)
• Two-valued query surface. WFS is three-valued (true / false / undefined), but the engine materializes only the definitely-true extent — a paradoxical atom resolves to undefined and does not fire. A rule whose conclusion is genuinely undecided neither fires nor is denied.
• #[brave] / stable-model semantics is out of scope (Out of scope).

Parametric (axis-generic) rules. A derive rule may be generic over a set of axes; the elaborator monomorphizes it to a finite set of concrete rules at elaboration, with no change to fixpoint semantics.

Stratified aggregates. Aggregate atoms (count, sum, max, min, avg, set_collect, …; see query) are admitted inside derive bodies when the aggregated predicate sits at a strictly lower stratum than the rule head, where the stratification dimension is a well-founded relation (typically the iof DAG, the specialization lattice, or an explicit user-declared ordering). The classic library use case is computing a derived level function over iof:

pub derive has_order(t: Entity, n: Nat) :-
    n == 1 + max { select m from t': Entity, m: Nat
                   where iof(t', t), has_order(t', m) };

The stratifier accepts this because the inner max aggregates has_order over iof-predecessors of t, and iof is well-founded. Stratified aggregates that would loop through an aggregation step on the same stratum are rejected with OE0510 NonStratifiedAggregate.

Universals over recursive predicates. A common composite pattern — a conjunction is fulfilled iff all of its children are — is a universal over the very predicate being defined:

pub derive Fulfilled(p: Conjunction, t: Instant) :-
    Instant(t), forall c: PC where childOf(p, c), Fulfilled(c, t);

This form is refused (OE1317 RecursionThroughAggregation): the forall lowers to the count-equality aggregate (Rule-atom grammar), and stratified-aggregate semantics (Faber–Pfeifer–Leone) require the aggregated predicate in a strictly-lower stratum — here Fulfilled aggregates over itself, so its SCC crosses an aggregate boundary and has no stratification. No intermediate derive helps: recursion depth follows the data (the part-whole tree), so any helper joins the same cycle. The supported phrasing is negation-as-failure double negation — ∀c.F(c) rewritten as ¬∃c.¬F(c):

pub derive HasUnfulfilledChild(p: Conjunction, t: Instant) :-
    childOf(p, c), Instant(t), not Fulfilled(c, t);
pub derive Fulfilled(p: Conjunction, t: Instant) :-
    Conjunction(p), Instant(t), not HasUnfulfilledChild(p, t);

This converts recursion-through-aggregation into recursion-through-negation, which the well-founded executor evaluates. On two-valued-total data — every child’s Fulfilled status resolves to true or false, as it does over a finite acyclic part-whole tree of leaves with definite status — the double negation derives exactly the universal’s extent, bottom-up through the tree. The honest caveat: where a child’s status is genuinely undefined under WFS, the double-negation form propagates undefined to the parent rather than guessing either way — and the two-valued surface omits undefined atoms, per the projection rule under well-founded semantics. Admitting the forall form directly (structural stratification over a provably well-founded relation) is tracked in issue #185.

Worked example — double-entry accounting (RFD 0029). Derived values and aggregate-as-term together make quantitative domains authorable. The double-entry invariant — within every journal entry, total debits equal total credits — is a check comparing two aggregates; the per-account balance is a derived value, grouped per account (the outer bound variable). The running package is examples/double_entry_v0.

pub type Account { mut name: String, }
pub type Entry   { mut memo: String, }
pub type Posting { mut amount: Decimal, mut side: String, }   // side = "D" | "C"
pub rel postedTo(posting: Posting, account: Account);
pub rel inEntry(posting: Posting, entry: Entry);

// Per-account balance = Σ debits − Σ credits, grouped per `acct`.
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 — two aggregates compared, per entry.
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",
    };

// A sales-tax line, rounded to cents with banker's rounding (the money default).
pub derive accountTax(acct, tax) :- acct: Account,
    debits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    tax    = round_half_even(debits * 0.075, 2);

Every amount is an exact Decimal: sum folds rationals (no rounding), the balance subtraction is exact, and round_half_even rounds to cents exactly — 150.75 * 0.075 = 11.30625 rounds to 11.31, never an f64 artifact. The EntryNotBalanced check is an instance-level Error, so at runtime it is a delta guard: a mutation that would leave an entry unbalanced is rejected atomically (double-entry is enforced, not merely reported).

Rule-atom grammar

Bodies of derive, query from clauses, check, and unsafe logic blocks are conjunctive sequences of rule atoms. The atom shapes:

rule-body ::= rule-atom (',' rule-atom)*
rule-atom ::=
    // Negation as failure
      'not' rule-atom
    | 'not' '(' rule-atom (',' rule-atom)* ')'
    // Modal (tier:modal)
    | 'box' '(' rule-atom ')'
    | 'diamond' '(' rule-atom ')'
    // Restriction quantifiers — DL ∀R.C / ∃R.C  (tier:expressive)
    | 'forall' '(' field-path ',' type-expr ')'
    | 'exists' '(' field-path ',' type-expr ')'
    // FOL binding quantifiers — admitted at tier:fol (inside unsafe logic)
    | 'forall' Ident ':' type-expr 'where' rule-body
    | 'exists' Ident ':' type-expr 'where' rule-body
    // Aggregate as atom, optionally compared (paren form, Expression grammar)
    | aggregate (comp-op expr)?
    // Subquery as atom, optionally compared (brace form, `query`)
    | subquery (comp-op expr)?
    // Reflection
    | meta-call (comp-op expr)?
    | path '::' Ident                                // sugar for meta(path) == Ident
    // Predicate call with optional outcome / comparison suffix
    | path '(' rule-arg (',' rule-arg)* ')'
        ('is' outcome-suffix | comp-op expr)?
    // Role invocation with closure (+ = transitive, * = reflexive-transitive)
    | field-path ('+'|'*') '(' Ident (':' type-expr)? ')'
    | field-path '(' Ident (':' type-expr)? ')'
    // Type test and `is` sugar
    | field-path ':' type-expr
    | field-path 'is' ('not'? 'unknown' | type-expr | Ident)
    // Specialization
    | field-path '<:' field-path
    // Binding — single `=`, distinct from the comparison `==` (RFD 0029)
    | Ident '=' expr
    // Comparison — RHS is a full expression (Expression grammar)
    | field-path comp-op expr
    // Membership — RHS is a full expression (set, list, or range)
    | field-path 'not'? 'in' expr
    // Bare-path Boolean test
    | field-path

field-path     ::= Ident ('.' name)*
rule-arg       ::= expr | expr comp-op expr
outcome-suffix ::= 'not'? ('ambiguous'|'unknown'|'timeout') ('(' Ident ')')?

Binding atoms (x = expr, RFD 0029). A rule body may bind a fresh variable to the value of an expression: x = expr (single =) is assignment, distinct from the comparison x == e (double =, a filter). expr ranges over bound variables, literals, field projections (t.income), exact arithmetic over the numeric tower, the rounding builtins (Expression grammar), and aggregate expressions. This is the established Datalog/Soufflé assignment concept and is what lets a rule head carry a derived value:

pub derive Tax(t, owed) :- appliesTo(b, t), owed = t.income * b.rate;

The binding introduces a fresh variable, and is range-restricted. Two distinct refusal paths, never a silent Null:

• Freshness (OE1335 BindingLhsAlreadyBound). The left-hand side x must be a new name. If x is already bound — by a prior positive predicate atom, a head parameter bound elsewhere, a projection, an aggregate result, or an earlier binding — the = would silently degrade into an equality filter (x joined against the computed value) rather than a binding. It is refused, naming x, with the directed hint: use == to compare, or pick a fresh name. This is the path a rebind x = x + 1 takes when x is otherwise bound (e.g. by a body predicate) — the LHS is not fresh.
• Range restriction (OE1303 RuleNotRangeRestricted). x = expr binds x positively iff every variable in expr is itself positively bound. An unbound right-hand-side variable, or a pure self-reference / cycle among binding atoms where the result variable is bound by nothing else (x = x + 1 as the only binder of x; x = y, y = x), leaves x unbound under the binding fixpoint and is refused as unsafe.

So x = x + 1 refuses either way — via OE1335 when x is already bound elsewhere (freshness), or via OE1303 when x has no other binder (range restriction) — and the two codes name the two genuinely different errors.

Aggregates as bindable terms (RFD 0029). Because an aggregate is a bindable expression, comparing two aggregates — the double-entry sum(debits) == sum(credits) invariant — is simply binding each and comparing the bound variables:

pub derive balanced(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;

The aggregate source extends the comprehension form: after for x in Source, a comma-separated list of additional body atoms (relation atoms, comparisons, type tests) refines the fold’s domain, and variables from the outer rule body are visible inside. That visibility is the grouping — the group key is the set of outer bound variables free in the aggregate, the standard Datalog reading. pub derive balance(acct, s) :- acct: Account, s = sum(p.amount for p in Posting, postedTo(p, acct)); groups per acct. A binding is not a comprehension trailing-atom form — sum(w for u in T, …, w = u.v) is refused with OE1336 BindingInComprehension, which directs you to project the value into the fold directly (sum(u.v for u in T, …)) or to bind in the outer rule body and aggregate the bound variable. The brace form (sum { … }) stays count/exists-only; a value aggregate in brace form is refused with OE1331 ValueAggregateBraceForm, which directs to the comprehension form. The SQL-ish group by … having is not built; it refuses with OE0007 carrying the binding-form rewrite. (Aggregates evaluate over the definitely-true extent: an aggregate folding over a relation with well-founded-undefined atoms is refused at runtime with OE1332 AggregateOverUndefined rather than silently treating undefined as false. The refusal is whole-relation, not per-group; three-valued aggregate intervals are tracked under issue #250.)

Empty-group semantics — a deliberate split. When a group is empty (the fold sees no rows), the aggregators divide by role:

• sum, count, count_distinct emit a value for the empty group — 0. An additive/cardinality fold has a well-defined identity (the empty sum is zero, the empty count is zero), so the grouped row is produced with that identity value.
• min, max, avg drop the row — they have no value over an empty set (there is no least/greatest element, and the mean is 0/0), so no grouped row is produced for an empty group rather than fabricating one.

This split is load-bearing for the double-entry invariant. sum(debits) == sum(credits) must catch an entry that has credits but no debits: because sum emits 0 for the empty debit side, the comparison is 0 == credits, which fails and flags the entry as unbalanced. Were sum to drop the empty group, the row would vanish and the imbalance would pass silently. The examples/double_entry_v0 package relies on exactly this behavior.

Conjunction between atoms uses ,. NAF uses the not keyword. Disjunction is not inline — write separate derive rules with the same head and arity; the union composes structurally. The same-head idiom is derive-only: a check head carries payload identity (its => Diagnostic { severity, code, message } report, its guard classification, its violation relation), so two checks sharing one head would cross-talk and are refused at elaboration (OE1328 DuplicateCheckHead) — rename one check, or express the disjunction through a shared derive predicate whose same-head clauses union, read by a single check. (Trait check members are unaffected: each impl’s monomorphized member rule is qualified by its impl target and keeps a distinct head, Trait atom.) The RHS of comparison atoms is a full expression (Expression grammar); inside that expression context, && / || / ! apply normally.

Payloadless enum constants. In value position, a path of the form EnumName::VariantName denotes the canonical enum value when the variant has no payload. This is distinct from the standalone rule atom sugar path :: Ident above, which means meta(path) == Ident. Payload-carrying variants require constructor semantics and are not constants by themselves.

Predicate resolution. The head of every predicate-call atom (path '(' … ')') must resolve to a declared predicate in scope — a rel, a concept used as a classification predicate, a derive / query head, a trait rule member (qualified Trait::member(...), or bare when exactly one provider is in lexical scope; subject to the coverage gate, Resolution), a pub fact / pub not_fact predicate, a fn, or a reflection intrinsic (iof, specializes, meta, extent, implements). check heads are not consumable: checks are observers only (Purity ladder) — their violation sets never populate the IDB — so a body atom resolving to a check head (module-level or trait check member) is refused with OE1329 CheckHeadConsumed; derive from the underlying body predicates instead (factor the violation pattern into a pub derive head read by both the check and the consuming rule). This applies to the predicate atoms of derive and check bodies and to both the body and head atoms of bridge rules (Bridge rules). An unresolved head is OE0223 RuleReferencesUnknownPredicate, the rule-body analogue of the pub fact obligation OE0220 (RFD 0004). A resolved atom is further checked for arity (OE0225) and — where both the argument’s type and the declared parameter type are concretely known — argument type (OE0226, sound under multiple classification: it fires only on provable disjointness). This is independent of the world assumption: the world assumption governs the truth value of instances of a declared predicate (under the CWA default an unasserted instance is false; under an #[world(open)] concept it is unknown/Can, World assumptions (CWA / OWA)) — it never admits an undeclared predicate name. To introduce a predicate that is intentionally empty until populated, declare it (pub rel P(...), or a bodiless pub derive P(...); head). ox check enforces this, and ox build refuses to emit an artifact for a program containing an unresolved predicate.

pub fact targets a base predicate, never a derived one. A derive / query head is a valid rule-body atom (it is in the resolution set above), but it is not a valid pub fact target. pub fact asserts into an extensional relation (a concept-as-classification or a pub rel); a derived predicate’s extent is intensional — computed by rule derivation. A pub fact P(...) whose P is a pub derive / pub query head is refused with OE0239 FactReferencesDerivedPredicate: the asserted seed tuple would key a different relation node than the rule head reads, so it would silently drop out of the rule’s fixpoint — the derive would evaluate to a result that omits the asserted tuples (no error, wrong answer). To give a derived predicate ground tuples that participate in its derivation, use one of two sanctioned forms, and OE0239’s help names both:

• A bodiless pub derive P(args); clause over concrete arguments (derive). The seed tuple is itself a derive clause on P, so it shares P’s relation node and participates directly in P’s fixpoint — the simplest way to seed P itself.
• A base relation the rule reads — declare pub rel Base(...), seed it with pub fact Base(...), and add a clause pub derive P(...) :- Base(...). Use this when the seed tuples are themselves a reusable extensional predicate.

Either keeps P a single-origin intensional head (the same rule Build pipeline and .oxbin enforces for a foreign-placed-vs-derived relation, OE1246). (A pub fact over a check head is the ordinary OE0220 — a check head is observer-only, not a predicate at all.)

Build loud-gate. More broadly, ox build refuses (writing no .oxbin) any derive / query rule the engine does not evaluate — an unsupported quantifier shape, a nested or non-count-class aggregate, not <aggregate>, an unsupported type-test or meta-eq (OE1311–OE1315). Argon refuses rather than emit an artifact that would silently mis-derive; see Build pipeline and .oxbin.

Modal atoms (box(...), diamond(...)) carry Kripke-frame semantics over the standpoint and classification frames described in Modal operators. The elaborator statically discharges the common case (type-classification atoms whose target is introduced by a fixed metatype — membership constant, RFD 0027 D6) and routes the remainder to a modal reasoner over std::kripke. Modal atoms are admitted only at tier:modal; lower tiers reject them.

Restricted universals (forall v: T where Body, Head). In the where body the last atom is the consequent (Head) and all preceding atoms are the domain restriction (Body). The quantifier holds iff every domain element also satisfies the consequent — it lowers to the count-equality count{ v : Body, Head } == count{ v : Body } (the domain-and-consequent count equals the domain count). The type annotation T is the static sort of v; the runtime domain comes from the where Body, so the Body must restrict v with a membership or predicate atom (e.g. member(g, v) or v in g.items) — Body, not T, bounds the count. An empty domain (count{ v : Body } == 0) makes the universal vacuously true (0 == 0), deriving the head — classical restricted-∀ semantics. The encoding needs at least a domain atom and a consequent (≥2 where atoms); the paren restriction form forall(path, T), the exists-binder form, and a single-atom where refuse with OE1315 (App. C).

Allen interval relations (before, meets, overlaps, during, starts, finishes, and their reciprocals) are not substrate operators. They are provided by the std::allen library (RFD 0024), defined over the Date / Duration value layer (Temporal substrate) — ordinary predicates over interval endpoints, not parser-level syntax.

Three atom shapes in the grammar above parse-refuse rather than silently mis-derive:

• Role closure field-path ('+'|'*') '(' … ')' (e.g. p.knows+(q: Person)). The base role-invocation form field-path '(' Ident (':' type-expr)? ')' is accepted; the transitive (+) / reflexive-transitive (*) closure suffix refuses with OE0001. Express transitive reachability through a recursive derive head.
• Axis sugar path '::' Ident (x :: T, i.e. meta(x) == T). Write the meta(x) == T comparison atom directly; the :: rule-atom shorthand refuses. (In value position EnumName::Variant is unaffected — see the payloadless-enum-constant note above.)
• Range membership field-path 'not'? 'in' <range> (p.v in 1..10). The set/list RHS of in is accepted; a lo..hi range RHS refuses (OE0001 on ..). Write the two-sided comparison p.v >= 1, p.v <= 10 instead.

Temporal rule atoms

Argon’s bitemporal substrate (Temporal substrate) admits metric temporal operators in rule bodies — the DatalogMTL fragment with stratified negation over the integer timeline.

Any atom may be qualified by a valid-time point or interval: atom at t (a single VT point), atom during [t1, t2] (a closed VT interval), atom since t (the open interval [t, ∞]).

Six prefix metric operators address past and future. Their interval bounds are durations (0, N with a unit ns…y, or inf/∞):

box_minus     [a, b] (φ)         // φ held at every past point in [a, b]
diamond_minus [a, b] (φ)         // φ held at some past point in [a, b]
box_plus      [a, b] (φ)         // φ holds at every future point in [a, b]
diamond_plus  [a, b] (φ)         // φ holds at some future point in [a, b]
since         [a, b] (φ, ψ)      // φ has held since ψ within [a, b]
until         [a, b] (φ, ψ)      // φ holds until ψ within [a, b]

Two shortcuts expand to [0, ∞] intervals: ever atom (some past or future point; needs tier: expressive for the disjunction) and always atom (every point; tier: recursive).

Side-by-side modal (box/diamond) and metric temporal atoms in one body compose additively. Nesting one family inside the other is refused at tier: recursive and routed to tier: fol — see Tier ladder for the decidability rule (OE0712).

query

query-decl ::= attribute* 'pub'? 'query' Ident '(' param-list ')' '->' TypeExpr
               ('across' '[' standpoint (',' …)* ']')?
               '{' query-body '}'
query-body ::= ('with' Ident '=' query-body ';')*
               'select' projection
               'from' rule-body                                    // Rule-atom grammar
               ('optional' 'from' rule-body)*
               ('where' rule-body)?                                // additional atoms
               ('group' 'by' expr ('having' expr)?)?
               ('order' 'by' expr ('asc' | 'desc')?)?
               ('limit' Nat ('offset' Nat)?)?
projection ::= expr | '{' struct-init-list '}' | 'path' Ident | aggregate
role-step  ::= Ident quantifier? ('(' role-binders ')')? ('as' Ident)? mode-spec?
quantifier ::= '+' | '*' | '{' expr (',' expr)? '}'                // expr of type Nat
mode-spec  ::= 'mode' ('walk' | 'trail' | 'acyclic' | 'simple')
            |  'shortest' | 'all-shortest' | 'any' | 'k-shortest' Nat

Role-step path-traversal chains (a.role+(b), c.ParentOf{1, n}(p: Person)) are admitted as predicate-call atoms in the rule-atom grammar (Rule-atom grammar) and are not separately defined here.

The evaluated query-body is select … from … (where …)?. Every other form parse-refuses loudly with a feature-named code — never a generic OE0001, never silently ignored: the result-shaping clauses (group by … having, order by … asc|desc, limit … offset) with OE0007; the with CTE clause with OE1344; the graph-/path-traversal projections (select shortest path …, select path …, … as <name> mode …) with OE1345; optional from with OE1346; and the result-table set operators (union / union all / intersect / except) with OE1347.

pub query active_leases_for(t: Person) -> [Lease] {
    select l from l: Lease, l.tenant == t where is_active(l)
}

pub query ancestors_within(p: Person, n: Nat) -> Set<Person> {
    select a from p.ParentOf{1, n}(a: Person)
}

pub query shortest_route(a: City, b: City) -> Path<City, Road> {
    select shortest path r from a.road+(b) as r
}

pub query avg_age_by_dept() -> Map<Department, Real> {
    select { dept: avg(p.age) }
    from p: Person, p.works_in(dept: Department)
    group by dept
}

pub query rich_friends_of(p: Person) -> Set<Person> {
    with rich = select x from x: Person where x.net_worth > 1_000_000;
    select f from p.knows(f: Person) where f in rich
}

pub query agreed_across(p: Person) -> Truth4Of<Bool>
    across [LegalGround, MedicalGround]
{
    select consents(p)
}

Subquery forms. Brace-bracketed inner queries used as expressions:

subquery      ::= subquery-kind '{' rule-body '}'                   // Rule-atom grammar; no `from` keyword
subquery-kind ::= 'collect' | 'set' | 'one' | 'count' | 'exists'

The subquery body is a bare rule-atom list — there is no from keyword inside the braces (that prefix belongs to the top-level query-body only; an inner from parse-refuses with OE0001).

The cardinality-fold kinds count and exists evaluate over the bare atom list above (count { p: Person }, exists { p: Person }). The projection-carrying kinds collect / set / one parse but refuse at ox check / ox build (OE1312); they never silently lower to a cardinality fold. Use a derive head plus a top-level query projection.

Set operations on result tables: union, union all, intersect, except.

Subquery aggregates (admitted as aggregate projections inside subquery bodies and as the subquery-form <aggregate> { atoms }): count, count distinct, sum, avg, min, max, collect, set_collect, string_join, percentile. The expression-level comprehension form sum(expr for x in coll where pred) (Expression grammar) admits a subset (sum, count, min, max, avg) for non-subquery contexts.

Default lattice context: K3. With across [...]: FDE.

mutate

mutate-decl ::= attribute* 'pub'? 'mutate' Ident '(' param-list ')' ('->' TypeExpr)?
                '{' mutate-body '}'
mutate-body ::= ('require' '{' expr (',' …)* '}')?
                stmt*
                ('return' expr ';')?
stmt        ::= 'let' Ident (':' TypeExpr)? '=' expr ';'
             |  'match' expr '{' arm (',' …)* '}'
             |  insert-stmt | update-stmt | delete-stmt | upsert-stmt
             |  'detach' 'delete' expr ';'                                  // ‡ refused, OE1353
             |  emit-stmt
             |  'for' Ident 'in' expr '{' stmt* '}'
             |  'if' expr '{' stmt* '}' ('else' '{' stmt* '}')?
             |  expr ';'
insert-stmt ::= 'insert' TypeExpr '{' field-init-list '}' ';'              // typed-literal insert
             |  'insert' Ident ':' TypeExpr '{' field-init-list '}' ';'   // ‡ named typed-literal — OE0001
             |  'insert' Ident 'into' expr ';'                             // insert binding into collection
             |  'insert' predicate-call '{' field-init-list '}' ';'        // relation insert with body
             |  'insert' predicate-call ';'                                // relation insert, no body
update-stmt ::= 'update' (Ident | pattern) 'set' '{' field-assign (',' …)* '}' ('where' expr)? ';'
field-assign ::= Ident ('=' | '+=' | '-=') expr
delete-stmt ::= 'delete' predicate-call ';'                                // delete iof(…) / delete Rel(…)
             |  'delete' (Ident | pattern) ('where' expr)? ';'             // ‡ entity / bulk delete — OE0001
upsert-stmt ::= 'upsert' pattern ('as' Ident)? upsert-clause+ ';'          // ‡ refused, OE1352
upsert-clause ::= 'on' 'insert' '{' field-assign (',' …)* '}'
               |  'on' 'update' '{' field-assign (',' …)* '}'
emit-stmt   ::= 'emit' Ident '{' expr '}' ';'

pub mutate sign_lease(t: Person, p: Property, rent: Money, term_days: Nat) -> Lease {
    require { rent > 0, term_days > 0 }
    let l = insert Lease(t, p) {
        monthly_rent: rent,
        start:        today(),
        end:          today() + term_days.days,
        status:       Pending,
    };
    emit AuditLog { LeaseSigned { lease: l, at: now() } };
    return l;
}

pub mutate hire_or_raise(p: Person, o: Organization, salary: Money) {
    upsert p.works_at(o) as emp
        on insert { emp.start_date = now(), emp.salary = salary }
        on update { emp.salary = salary };
}

pub mutate rebrand(old: String, new: String) {
    update c: Company set { name = new } where c.name == old;
}

An update of a bound target writes its mut fields directly. The ('where' expr)? filter (and the bulk/pattern target forms it implies, as in rebrand above) is refused at ox check / ox build (OE1318), never silently dropped.

The grammar shapes marked ‡ are loud refusals, not silent no-ops. Named typed-literal insert (insert l: Lease { … }; use let l = insert Lease { … } instead) and entity/bulk delete of a bound target or pattern with an optional where refuse with OE0001 — only delete predicate-call (delete iof(…) / delete Rel(…)) is admitted. detach delete refuses with OE1353 and upsert with OE1352.

The rebrand example assumes name is declared mut on Company. Per struct and enum — language built-ins (data declarations), fields are immutable post-construction unless explicitly marked mut:

pub type Company {
    #[intrinsic] founded: Date,    // construction-required; not updatable
    mut name: String,              // updatable via `update`-stmt
}

update-stmt admits writes only to mut fields. A field-assign targeting a non-mut field is rejected with OE0820 UpdateImmutableField. The elaborator validates each field-assign against the entity’s field-decl mut flag; rejection surfaces at build time, not at mutation invocation.

Field updates lower to append-only event pairs on the underlying property axiom (Storage layer): a retract event for the prior value and an assert event for the new. The proposition’s logical identity is the (entity_id, property_id) pair; the value is what changes. Bitemporal queries reconstruct prior values per Temporal substrate.

Mutations are transactional within the body; the kernel may reject mutations that violate refinement, consistency policy, or stratification — rejection surfaces to the caller as Result<T, Diagnostic> from the host runtime.

Dynamic reclassification — insert iof / delete iof. Because iof is a first-class predicate (Reflection), mutate bodies can dynamically classify and declassify entities by inserting or deleting iof tuples through the existing insert predicate-call / delete predicate-call forms:

pub mutate enrol(p: Person) {
    insert iof(p, Student);                  // p is now a Student
}

pub mutate expel(s: Student) {
    delete iof(s, Student);                  // s is no longer a Student
}

The single-type insert iof(x, T) / delete iof(x, T) forms above classify and declassify an entity, subject to the gates below. Inserting an iof tuple over a relation concept — insert iof((p, into), EnrolledAt) for a named relation EnrolledAt — refuses: the tuple-argument form parse-refuses with OE0001 rather than silently doing nothing.

The substrate enforces two constraints on insert iof(x, T):

1. Refinement gate (enforced). If T carries a defined refinement iff { … } (Refinement) — for example, pub type ExtinctSpecies <: BirdSpecies iff { self.numberOfLivingInstances == 0 } — the predicate is the substrate’s source of truth for membership: the modeler updates the underlying state (here, numberOfLivingInstances) and the substrate derives the iof classification automatically, so explicit insert iof(x, ExtinctSpecies) emits OE0211 IofInsertOnDefined and the mutation is rejected. If instead T carries a primitive refinement where { … }, membership is conferred by assertion, so insert iof(x, T) is permitted — but the predicate is a necessary invariant: an x that positively violates it (definite false, World assumptions (CWA / OWA)) is rejected with OE0668 RefinementInvariantViolated. The same invariant is checked when a primitive-where member is created by construction (insert T { … }) or when an update writes a field the predicate reads.
2. Modifier gates (enforced — RFD 0027 D6). Re-classification is governed by the ontology-neutral fixed modifier on the target’s introducing metatype (metatype), never by any axis name: insert iof(x, T) / delete iof(x, T) where T is fixed-introduced is refused with OE0234 FixedReclassification — classification under such types is decided at construction (insert <T> { … } remains legal; construction is not re-classification). Admission is the absence of fixed: dynamic classification is the default, and a vocabulary opts its rigid metatypes into the restriction explicitly (pub fixed metatype kind = { … };) — an axis assignment like rigidity::anti_rigid is inert user vocabulary and grants nothing by itself. Likewise insert iof(x, T) against an abstract type — a direct instance — is refused with OE0233 AbstractTypeConstruct; non-abstract subtypes are unaffected. Both gates fire at ox check / ox build where the target is statically known and at the runtime write path otherwise, rejecting the whole mutation atomically. The membership-constancy theorem (Argon.Runtime.ModifierGates.runMutation_fixed_iof_constant) is what grounds static modal discharge over fixed-introduced types (Modal operators).
3. Compatibility gate. x’s existing classification chain must include some supertype that T specializes (e.g. Student <: Person requires x: Person).

After insert iof(x, T), the entity x is classified under both its prior types and T. After delete iof(x, T), x is no longer classified under T but retains all other classifications. The substrate maintains a single global iof relation; insert/delete operate transactionally.

Bitemporal mutation forms. Per the temporal substrate (Temporal substrate, Effective-dating: valid time and the two as_of axes), an insert may carry an explicit valid-time at <date> qualifier — the assertion’s valid time begins on that civil day (RP-004 mutate). This form executes: the write threads the date onto the event’s bitemporal extent, and an as_of <#date#> query reads it back.

pub type T;
pub mutate enact(x: T, effective: Date) {
    insert iof(x, T);              // [VT: now → ∞]  [TT: now → ∞]  — atemporal default
    insert iof(x, T) at effective; // [VT: effective → ∞]            — effective-dated
}

The window form during [t1, t2], the since open-interval form, and a valid-time-qualified delete (bitemporal retraction — closing a valid-time interval rather than opening one) refuse loudly (OE1330) rather than silently applying at all valid times:

pub type T;
pub mutate retro(x: T) {
    insert iof(x, T) during #2020-09-01#;   // window VT
}

Explicit erasure — forget. For compliance scenarios (GDPR right-to-erasure, sensitive-data redaction), forget removes the underlying tuple including its bitemporal history:

forget x;                                               // bound individual; capability-gated

Only the bound-individual form forget <expr> is admitted; the forget iof(x, T) and bulk forget … where … shapes refuse with OE0001.

forget is capability-gated at the source level: a mutate body containing forget refuses to build (OE0730 ForgetWithoutCapability) unless the enclosing mutate declaration grants #[allow_forget]. Cascading derived facts are revised via DRed overdelete.

Reasserting a tuple after retraction produces distinct VT intervals on the underlying store — the substrate does not coalesce on adjacent boundaries. Historical retract/reassert is queryable via audit projections.

Body semantics

A mutate body lowers to the Operation IR and runs with all-or-nothing atomic commit: a failed require guard, or any error, emits nothing (RFD 0015). require preconditions, let bindings, typed-literal entity construction with system-minted identity, projection navigation (a.b.c) over committed state, collection inserts (insert … into …) with for iteration, sum / count aggregate guards over comprehensions, index projection (coll[i]), and effectful if/else (control flow is expression-valued; branches are blocks) all execute, returning the body’s tail value.

match in bodies. A value-position match (a let RHS, an update … set value, a tail / return value, or a require guard) matches over constant patterns (payloadless enum constants, literals, or-patterns, _; Pattern matching) and desugars to the same IfExpr chain a value if uses, with exhaustiveness enforced at ox check (OE0203). A statement-position match (arms running effects — the BPMN-gateway dispatch match d { Disposition::Clean => { update … }, Disposition::BreaksFound => { insert … }, _ => {} }) lowers to a right-nested Operation::If chain over the arm blocks’ operations (RFD 0015 Amendment 2): the same ordered first-match semantics, constant-pattern subset, and OE0203 exhaustiveness as the value desugar; arm blocks and if branches admit the full mutate statement set at any nesting depth. upsert, emit, and detach delete in a body refuse by name rather than dying generic or doing nothing silently: emit with OE1318, upsert with OE1352, and detach delete with OE1353.

Mutate-body arithmetic is exact (RFD 0016 / RFD 0029): require guards and let / field expressions route through one canonical evaluation core — pure-Int operands stay checked integers (overflow is a loud error, never a wrap), and any Real / Decimal / Money operand promotes to an exact rational (/ is the field operation, no truncation), so 0.1 + 0.2 == 0.3 holds exactly in a mutate body where it would fail in f64.

Reads see committed state. A body’s projections (a.b.c) read the store as committed before the mutation; a body does not observe its own not-yet-committed constructions. One consequence: constructing a collection-valued field and then insert … into that same field in a single body does not compose (the append seeds from committed state).

check

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

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

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

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

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

Catalog-level checks are the user-extensible compiler-diagnostic mechanism: a theory package ships its modeling constraints (OntoClean-style rigidity lints, MLT well-formedness, trait conformance) as check rules and they surface at ox check / ox build like any compiler diagnostic, under the package’s own codes (editor surfacing via the LSP is tracked follow-on work).

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

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

Runtime semantics — guard on the delta

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

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

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

The Diagnostic payload

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

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

at: is reserved for span attribution and refused.

Three-valued honesty

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

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

emit from any rule mode

emit Name { value } publishes value to sink Name. Allowed in any rule body whose required sinks are in scope. In fn and query, emit fires once per fresh evaluation; cache hits do not re-emit. Sinks are observation channels and never affect the queryable extent.

Sinks

A sink is the typed publication channel emit targets:

sink-decl ::= attribute* 'pub'? 'sink' Ident ':' TypeExpr ';'

pub sink AuditLog: LeaseEvent;
pub sink HitlQueue: ReviewTask;
pub sink Notify:    Notification;

Delivery (log file, webhook, message queue, HITL ticket) is a runtime concern; the language guarantees only that emitted values match the sink’s declared type. An emit statement in a mutate body refuses with OE1318 (mutate) rather than silently dropping the emission.

Pattern matching

match-expr ::= 'match' expr '{' arm (',' …)* ','? '}'
arm        ::= pattern ('if' expr)? '=>' expr
pattern    ::= '_'
            |  literal
            |  Ident                                    // binder
            |  TypeExpr '(' pattern (',' …)* ')'        // variant
            |  TypeExpr '{' field-pattern-list '}'      // record
            |  Ident ':' TypeExpr                       // type test
            |  'is' reasoning-outcome
            |  pattern '|' pattern                      // OR
reasoning-outcome ::= 'unknown'
                  |  'ambiguous' '(' Ident ')'
                  |  'timeout'   '(' Ident ')'
                  |  'both'      '(' Ident ',' Ident ')'

pub fn classify(l: Lease) -> Status =
    match l {
        ResidentialLease(r) if r.bedrooms > 4 => Status::Large,
        ResidentialLease(_)                   => Status::Standard,
        CommercialLease(_)                    => Status::Commercial,
        _: TerminatedLease                    => Status::Closed,
        is unknown                            => Status::Pending,
        is ambiguous(x)                       => Status::Ambiguous(x),
        _                                     => Status::Unknown,
    };

Exhaustiveness checked; non-exhaustive matches require _ or fail with OE0203.

Match semantics

match evaluates — in value position and statement position — as ordered first-match over constant patterns:

A value-position match (a fn body, a rule-body comparison operand, a mutate let RHS / update … set value / return value / require guard) desugars at elaboration to a right-nested conditional chain over scrutinee == constant tests — if s == P1 { v1 } else if s == P2 { v2 } else { v_last } — so it executes on the existing IfExpr paths in the reasoner and the mutate runtime; semantics are first-match in arm order, and the final arm’s value is the else-branch. Exhaustiveness is required: a final _ arm, or full coverage of the scrutinee’s enum variants when statically known — otherwise OE0203 at ox check. Statement-position match (arms running effects inside a mutate body) executes with the same semantics (RFD 0015 Amendment 2): the arms are blocks running mutate statements (update / insert / delete / forget / require / nested for / if / match), the match lowers to a right-nested Operation::If chain over the arm blocks’ operations — ordered first-match, exactly one selected arm’s effects run, the arm value is discarded — and the same exhaustiveness rule applies (_ => {} with an empty block is the idiomatic catch-all; OE0203 otherwise). Or-patterns expand to consecutive conditions sharing the arm’s operations.

A single-binder payload destructuring (Some(v) => …) executes in value position — let r = match opt { Some(v) => v, None => 0 }; and every value-position site above: the arm’s condition tests the variant tag and its body sees the binder substituted by the decoded payload. A payload-binding arm in statement position (an effectful arm inside a mutate statement-match) refuses with OE1319: bind the payload in value position first (let v = match opt { … };), then run the effect. A bare binder Ident, a type test, an is-outcome arm, and an arm guard refuse with OE1319 in both positions.

Rule-body arm projections must be total. In a rule body (derive / check / query / bridge), the relational lowering hoists every field projection inside the conditional chain — including arms the scrutinee never selects — into an eager, unconditional $field:: join, because the relational plan has no lazy join. $field::<f> has no row when an individual lacks f, so an arm projecting an optional (T?) field would silently filter out every row missing that field, even rows whose matching arm never touches it. Rather than mis-evaluate, ox check / ox build refuse such a rule with OE1320: every field projected inside a conditional arm (a value-if branch or match arm — both lower identically) must be total, i.e. declared required on every visible type that declares it. Workarounds: split the conditional into one rule per arm (each joining only the fields that arm needs), or declare the field required. Projections in always-evaluated positions (the rule body proper, the outermost condition / scrutinee test) and fn / mutate bodies (which evaluate branches lazily) are unaffected.

Trait atom

A trait is a behavioral contract: a named bundle of obligations over a Self type, discharged by impl Trait for Type blocks. The boundary with the concept lattice is doctrinal: concepts say what something is (ontologically); traits say what something can do — trait hierarchies never enter the <: concept lattice, traits cannot be specialized or inherited, and classification never belongs in a trait (Modeling guidance: traits versus phases and categories). The full design is RFD 0026; the trait surface lands in stages, and what runs end-to-end is exercised by the packages in examples/.

Surface

trait-decl  ::= attribute* 'pub'? 'trait' Ident generic-params?
                   (':' TypeExpr ('+' TypeExpr)*)?            -- supertraits (requires-constraints)
                   ('{' trait-item* '}')? | ';'               -- empty body = marker trait
trait-item  ::= fn-signature ';'                              -- invocation-plane member ('self' leads)
             |  'mutate' Ident '(' 'self' (',' member-params)? ')' ';'   -- invocation-plane member
             |  'derive' Ident '(' member-params ')' ';'                    -- rule-plane member
             |  'check' Ident '(' member-params ')'
                   ('=>' 'Severity' '::' Ident)? ';'          -- rule-plane member; optional
                                                              -- severity pin (issue #230)
             |  'query' Ident '(' member-params ')' '->' TypeExpr ';'       -- rule-plane member
             -- 'type' Ident ';' / 'const' Ident ':' TypeExpr ';' remain reserved

impl-block      ::= 'impl' generic-params? TypeExpr ('for' TypeExpr)? ('{' … '}')? | ';'
trait-impl-item ::= fn-decl | mutate-decl                     -- full bodies
                 |  derive-decl | check-decl | query-decl     -- full bodies (rule body; select
                                                              -- body for query), Self admitted

When 'for' TypeExpr is present the construct is a trait impl (impl Renewable for Lease) and its items are trait-impl-items; when absent it is a bare impl (impl Lease { … }), whose items parse per impl Type { … } — grouping but are gated at elaboration (OE1326) until inherent members execute. Conformance (Conformance) governs trait impls only. Impls of either form are standpoint-global: declaring one inside a standpoint { … } block is refused at elaboration (per-standpoint impls are an open design question RFD 0026 deliberately does not decide).

• Self resolves only inside trait and impl bodies: in a trait item it is the obligation’s type parameter; in an impl item it denotes the impl’s target type. Misuse is OE0675. A trait member signature must mention Self in at least one parameter position (a member that is not about the implementing type belongs at module level — OE0675 says so). Multiple Self positions are legal.
• Supertraits use : (pub trait Repaintable: Drawable), Rust’s spelling, because they are Rust’s semantics — requires-constraints, not subsumption (Resolution). <: is reserved for the concept lattice.
• Generic parameters remain unbounded-only (Generic parameters); generic members, bounded generics, and trait-side default bodies refuse loudly, never dropped.

Member semantics: two planes

Members split by how they are consumed; both planes elaborate by monomorphization — each impl member lowers to an ordinary rule (Self ↦ target type) flowing through the standard pipeline (classifier, stratifier, evaluability gate, reasoner) with no new evaluation machinery.

Rule plane (derive, check, query) — clause union

The trait declares the predicate; each impl contributes a type-guarded clause:

pub trait Adulthood {
    derive Adult(Self)
}
impl Adulthood for USPerson     { derive Adult(p: Self) :- p.age >= 18 }
impl Adulthood for GermanPerson { derive Adult(p: Self) :- p.age >= 18, p.has_residence }

elaborates to two ordinary rules with one head, Adulthood::Adult — Datalog unions same-head rules natively, and the head-parameter guards close over <: (World assumptions (CWA / OWA)). Dispatch is derivation: an atom Adult(p) in

pub derive CanVote(p: Person) :- Adult(p), p.registered

holds per-individual under whichever impl covers the individual’s actual type — the relational transposition of dyn dispatch, with the no-overlap rule (Conformance) keeping the selection single-valued per declared type (per-individual multiple classification is defined in Conformance). A query member carries the full query signature — Self in parameter positions, a Self-free return type (return-position Self is OE0675: it would need union types or bounded generics) — and each impl provides a full select … from … body; the trait signature fixes the projection shape. Query members are declared, conformance-checked, and lowered per impl, and they surface through the same per-impl query dispatch top-level queries use — each impl’s clause is queryable under its per-impl identity Trait::member@Target. They are not rule-body atoms: a query-member atom in a derive/check body is refused loudly at ox check, the same envelope discipline fn members get (Resolution) — top-level queries are not rule-body predicates either, and the member form inherits exactly that. A single dispatch endpoint returning the union of per-impl results is reserved. A check member monomorphizes to ordinary RuleMode::Check rules; discharge, payload, and delivery follow RFD 0025 unchanged. A check member’s signature may pin its severity with the payload-arrow suffix (check OverLimit(Self) => Severity::Error; — RFD 0026 amendment 2026-06-11, issue #230): the pin makes blocking behavior part of the trait contract. Under a pin, an impl’s Diagnostic { … } payload may omit severity: (it inherits the pinned one), may restate the same severity (harmless), and is refused with OE0676 when it states a different one — a contract whose blocking behavior varies by implementor is a weak contract. Only the severity is pinnable: code: and message: stay per-impl, and a full Diagnostic { … } payload on the trait-side signature is refused (OE1323). An unpinned member keeps per-impl severity freedom. #[observe] on an impl member whose pinned severity is Error remains legal (a discharge-mode opt-out, not a severity change).

Invocation plane (fn, mutate) — receiver resolution

A body is a single value or a single transaction; resolution is to exactly one impl. An invocation-plane member leads with the self receiver — its first parameter must be self (OE0675 otherwise; further Self-typed parameters are admitted after it) — because the receiver is what dispatch selects on. A mutate member —

pub trait Closable {
    mutate close(self, reason: String);
}
impl Closable for SavingsAccount {
    mutate close(self, reason: String) {
        update self: SavingsAccount set { status = "closed" }
    }
}

— monomorphizes per impl (full RFD 0015 imperative bodies; self is the receiver variable inside the body, Self splices to the target type) into the mutation catalog under the per-impl identity Closable::close@SavingsAccount, callable as Closable::close: invocation dispatches on the receiver individual’s actual committed type to the unique covering impl (<:-aware — an impl for Account covers a SavingsAccount receiver). An ambiguous receiver — classified under two <:-incomparable covered targets — and a receiver with no covering impl are both loud runtime refusals naming the impls / the receiver’s types (Conformance), never an arbitrary pick. Invocation flows through the standard mutation-dispatch surface (CLI harness / serve / SDK); the receiver is passed as the self argument (an individual reference), exactly like any RFD 0019 entity-ref parameter. fn members elaborate and dispatch the same way through the compute surface (Resolution has the precise execution envelope). Mutations do not call mutations; member mutates do not change that.

Generic parameters

Unbounded generics parse and travel the wire; bounded generics are rejected (OE0667). The conditional-impl coherence theorem (Argon.TypeSystem.Conditional) is mechanized.

Resolution

Calling convention (rule plane). Trait::member(args) qualified is always legal. Bare member(args) is legal when exactly one provider of that name and arity is in lexical scope; ambiguity is an error naming the candidates. There is no postfix p.member() sugar in rule bodies — p.x is field-access space (Rule-atom grammar).

The coverage gate. A bare member atom requires the argument’s static type to be fully covered — you cannot call what isn’t implemented, statically. Coverage is computed over the workspace-closed catalog via the abstract modifier (metatype, RFD 0027 D6): a static type T is fully covered iff every instantiable (non-abstract) declared S ⊑ T (including T itself when non-abstract) is ⊑ some impl target. Abstract types admit no direct instances (OE0233 refuses construction) — every individual is classified through some non-abstract subtype — so they need no covering themselves; their non-abstract descendants do. The instantiability oracle is a pure wire-flag read (Argon.TypeSystem.Conformance. instantiableOfAbstract); no axis vocabulary is consulted — a sortality::non_sortal binding is the package’s own ontology and exempts nothing by itself. The default is instantiable: an unmodified declaration (the neutral std::core::type baseline, any pub metatype m = { };) obligates coverage — the gate can only over-refuse, never silently admit a vacuous member call, and the exemption is the explicit abstract opt-in. Partial coverage is legal only under an explicit conformance guard:

pub derive CanVote(p: Person) :-
    implements(meta(p), Adulthood),     -- the visible branch
    Adult(p), p.registered

Uncovered or unguarded-partial atoms are OE1327, whose help names the uncovered types and offers both fixes (add the impl, or write the guard). Dispatch that can fail is always visible in the source. Under multiple classification meta(p) is multi-valued (Reflection); the guard is existential by construction — meta is a relation and the conjunction is a join, so the guard holds iff some <:-minimal classifier of p is covered, and the clause that fires is the one whose target that classifier satisfies.

Invocation-plane dispatch. Invocation-plane members are end to end through the execution surfaces Argon has — the dispatch surfaces, where the only type information is the receiver individual’s committed classification:

• A member is invoked by its callable name Trait::member (qualified path, or any unambiguous ::-suffix — the same resolution rules as mutations and rule heads; ambiguity is an error naming the candidates), or pinned to one impl by its per-impl identity Trait::member@Target. The pinned form is an explicit escape hatch: it bypasses receiver dispatch and does not re-verify that the receiver is covered by that impl’s target (parity with ordinary mutations, which do not re-verify update x: T against x’s classification).
• The self argument carries the receiver individual; dispatch selects the unique impl whose target covers the receiver’s actual committed type (<:-aware). No covering impl, and a receiver under two <:-incomparable covered targets (the Conformance residual), are loud refusals naming the types / the impls — never an arbitrary pick.
• mutate members run through every mutation surface (the CLI demo harness, serve’s /v1/dispatch/mutation, the generated SDK’s member endpoint); fn members run through the compute surface (/v1/dispatch/compute, SDK) — exactly the surfaces where top-level fn declarations execute.

Source-level call sites are not an execution surface — for any fn. Top-level fn declarations cannot be called from rule bodies or from fn/mutate bodies (term-position user-function application does not resolve); method-call syntax x.foo() parses but has no semantics — the call expression builds, resolves to nothing, and derives nothing (the same silent-vacuity bucket as term-position application; tracked for a loud gate). fn members inherit exactly that envelope — they are declared, conformance-checked, lowered, and dispatchable wherever top-level fns are, and nowhere else. Source-level calls bind to the rules this section reserves: build-time resolution (first x’s inherent impls, then trait impls; one concrete body, no vtables), Trait1::foo(x) (UFCS) on collision, bare calls legal where exactly one trait in scope provides the member, and the receiver’s static type subject to the same coverage gate.

Supertraits are requires-constraints. pub trait Renewable: Resource makes impl Renewable for Lease well-formed only if impl Resource for Lease exists (OE0674). Nothing is inherited — no member bodies, no identity, no lattice position.

Orphan rule. An impl Trait for Type must live in the package declaring Trait or the one declaring Type (OE0672), so every workspace’s impl set is unambiguous.

Conformance

Enforced at ox check and ox build over the closed catalog (elaboration-time diagnostics, not check rules):

No-overlap (OE0673) instantiates the mechanized coherence contract by construction — a nominal target is a TraitBound with satisfied T := T ⊑ target — so at most one impl covers any declared instantiable type and there is never a specificity question. Both arms matter: impl Adulthood for Person + impl Adulthood for USPerson is OE0673 (the “default + override” pattern is rejected by design — write disjoint targets, or one impl whose body branches), and impl T for Person + impl T for Customer is OE0673 when some pub type Employee <: Person, Customer is declared (the common descendant would sit under two clauses). One residual cannot be closed statically — the set of an individual’s runtime classifications is not known at compile time: an individual dynamically classified under two <:-incomparable covered targets with no declared common descendant. Its semantics is defined, not accidental — in the rule plane the clauses are independent sufficient conditions (both may fire; the union is their disjunction); in the invocation plane an ambiguous receiver is a loud runtime refusal.

Reflective conformance: TraitRef and implements

• TraitRef is a reflective sort parallel to TypeRef (RFD 0023): values are handles to declared traits (carrier Value::Name). It is a sibling sort under Entity — deliberately not on the Metatype <: TypeRef chain, because traits are not types.
• implements(t: TypeRef, tr: TraitRef) -> Bool is the fifth reflection intrinsic (Reflection), materialized as the RT-closed reserved-head relation $implements from impl declarations, with supertrait closure and <: upward target-coverage folded in (an impl for Person covers USPerson, World assumptions (CWA / OWA)-coherent).
• $implements is catalog-closed, so not implements(…) is stratification-safe, and — unlike the type-position arguments of the other four intrinsics — both positions of implements are exempt from OE0212 and may be free: enumeration is relational (implements(t, Adulthood) with free t yields the implementing types; implements(meta(p), tr) with free tr yields the traits of p’s type). The expression plane gets the boolean form (if/match scrutinees) and implementors(Trait) -> Set<TypeRef>.
• Conformance checks are catalog-level vocabulary under RFD 0025 D1 as amended by RFD 0026 (catalog-level iff every variable is reflective-sorted: TypeRef, TraitRef, or Metatype), so they discharge statically at ox check:

#[static]
pub check EveryPersonKindHasAdulthood(t: TypeRef) :-
    specializes(t, Person),
    not implements(t, Adulthood)
    => Diagnostic {
        severity: Severity::Error,
        code:     "Onto::E001",
        message:  format!("{} must implement Adulthood", t),
    }

Wire and Lean correspondence

Member rules are emitted as ordinary RuleDecl/QueryDecl events; invocation-plane members as ordinary MutationDecl/ComputeDecl events keyed Trait::member@Target — no new AxiomKind. TraitDeclBody.methods carries member signatures (all five planes); ImplDeclBody.items carries member provenance (both fields carry it — the wire is built for this). spec/lean/Argon/Substrate/Trait.lean carries the @[language_interface] shapes; Argon.TypeSystem.Conditional states the coherence contract that OE0673 enforces. The Lean obligations for this design (monomorphization conservativity on the Reasoning/Datalog/ spine; coherence instantiation; structural-tier conformance) are listed in RFD 0026.

Modeling guidance: traits versus phases and categories

If it classifies, it is a concept; if it obligates behavior, it is a trait. “Adult” as a classification is an anti-rigid phase of Person — model it as pub type Adult <: Person iff { age >= 18 } and the substrate derives membership. Reach for a trait when otherwise-unrelated types must satisfy a common contract of derivations or operations (Closable, Auditable, per-jurisdiction rule families) — the contract is about what the types provide, not what their instances are. A trait carrying a single unary Self-member named like a classification is usually a phase in disguise.

Examples

-- Marker trait.
pub trait Renewable;

-- Rule-plane contract; per-jurisdiction clauses.
pub trait Adulthood {
    derive Adult(Self)
}
impl Adulthood for USPerson     { derive Adult(p: Self) :- p.age >= 18 }
impl Adulthood for GermanPerson { derive Adult(p: Self) :- p.age >= 18, p.has_residence }

pub derive CanVote(p: Person) :-
    implements(meta(p), Adulthood), Adult(p), p.registered

-- Invocation-plane contract. The receiver leads; invocation passes
-- `self` (an individual ref) and dispatches on its actual type.
pub trait Closable {
    mutate close(self, reason: String);
}

-- Supertrait as requires-constraint (Rust's `:`). Return-position
-- `Self` is OE0675 (it would need union types / bounded generics);
-- return a concrete type.
pub trait Repaintable: Drawable {
    fn repaint_cost(self, color: Color) -> Int;
}

-- Bare impl (inherent grouping): parses per `impl Type { … }` — grouping, but its members are
-- OE1326-gated at elaboration — inherent members do not execute yet
-- (the RFD 0026 invocation plane covers trait members only).
impl Lease {
    fn extend(self, days: Nat) -> Lease;
}

Macro atom

The macro atom is the fifth substrate atom (meta-calculus, constructs, rule, trait, macro) and the extensibility layer the ontology-neutral doctrine depends on: it is how a vocabulary library grows the surface without a compiler change. Its design is settled by RFD 0037; this chapter is the surface specification.

The declarative expansion engine — pub macro declarations expand at EXPAND (hygiene, repetition, attribute/decl-position invocation, cross-module imports), and their output re-elaborates through the ordinary path to events. The procedural layer (#[procmacro] pub fn, Procedural macros) provides concat_idents, quote/${} antiquotation, decl-reflection, and a total non-recursive body — the mechanism that re-homes #[irreflexive]/#[asymmetric] from compiler builtins to library procedural macros. #[functional] is a builtin-backed macro (Migration: re-homing the hard-coded surface).

The shape of the design. A macro expands to surface syntax, which is re-parsed and re-elaborated through the one existing path to events — never to events directly. Expansion is a phase between parse and resolve, run to a fixed point; the resolver, type checker, Name resolution ontology-neutrality gate, and decidability-tier classifier all run on the post-expansion program, so a macro is invisible to none of them. The declarative layer (pub macro, pattern→template) is the foundation; the procedural layer (#[procmacro], computation over reflected syntax) is layered on top (Procedural macros).

Declarative macros

macro-decl    ::= attribute* 'pub'? 'macro' Ident '{' macro-rule (';' macro-rule)* ';'? '}'
macro-rule    ::= '(' macro-pattern ')' '=>' '{' template '}'
macro-pattern ::= /* token tree with $name:SPEC metavariables and $(...)* / $(...)+ / $(...)? repetitions */

A declarative macro is a sequence of (pattern) => { template } rules. A pattern matches a token tree; metavariables are tagged with a fragment specifier that fixes the syntactic category matched and the binding space the bound name lives in. The template is surface syntax, with metavariable substitution and $( … )*/+/? repetitions (optional separator: $( … ),*).

pub macro vec {
    () => { Vec::empty() };
    ($head:expr $(, $tail:expr)*) => { /* … */ };
}

let xs = vec!(1, 2, 3);

Fragment specifiers. The syntactic categories $x:expr, $t:ty, $i:ident, pat, stmt, block, item, literal, path, tt; plus four Argon-specific specifiers, each a binding-space-targeted parse — $c:concept parses a concept-introducing declaration and binds in the concept space, $r:rel a relation declaration (rel space), $m:metatype a metatype introducer, and $u:rule a rule-body atom (carrying its own rule-variable sub-bindings). The set is closed; a standpoint specifier and a user-extensible registry are out of scope (Out of scope). Because a concept/metatype specifier only binds — the Name resolution gate runs later, at resolution (Hygiene) — and no specifier carries a tier, ontology-neutrality and tier-honesty hold by construction.

The expansion model

Expansion is a distinct compilation phase:

lex → parse → expand* → resolve → check → instantiate (lower to events) → tier-classify → discharge

• Expand to surface, re-elaborate. A macro produces surface syntax that is spliced into the module and re-parsed; it then flows through the same resolve → check → lower path as hand-written source. The content-addressed AxiomKind event wire is produced only by the unchanged lowering, so a macro inherits the substrate’s identity and drift guarantees for free. A macro never emits events directly.
• Fixed point. A macro whose output contains further invocations re-expands until none remain, bounded by a fuel cap that errors on exhaustion.
• Emit into the invocation module. A macro expands at its use site and its output lands in the invoking module, where rules it emits compose with the user’s by the same-module same-head union (derive). It cannot contribute to another module’s heads.
• Classifier-last gives tier-honesty. The decidability-tier classifier runs after expansion on the lowered events, so the program lands on its true tier — a macro that emits a recursive rule is classified exactly as if the rule were hand-written, and cannot smuggle the program across a tier boundary.
• Determinism. The declarative layer is strongly normalizing by construction, has no I/O, and emits collections in a canonical order. Rule variables are alpha-canonicalized at lowering (Hygiene), so a macro’s choice of fresh variable names never affects the .oxbin content hash. Expansion is therefore a deterministic function of its input, and reproducible builds need no author discipline.

Hygiene

Macro-introduced binders neither capture nor are captured by names at the use site, across all of Argon’s binder namespaces (rule variables, concept/type, rel/metarel, metatype/metaxis + axis values, individuals, trait members). The model is scope-sets with binding spaces (Flatt 2016 + Racket binding spaces): each namespace is an interned scope inside one scope-set, resolved by the unchanged maximal-subset rule. Hygiene is white-box — the quotation applies a fresh macro scope to the identifiers a macro introduces.

The Name resolution ontology-neutrality gate composes as a commuting pass: scope-set resolution (syntactic) produces a candidate binding, then the gate (semantic) checks that a macro-introduced concept resolves to a visible pub metatype — it may reject, but never re-points a reference. Macro-introduced vocabulary is not exempt from the gate.

Two regimes follow from what reaches event identity:

• Rule variables are clause-local and alpha-canonicalized at lowering, so hygiene need only guarantee non-capture; their names are irrelevant to identity.
• Introduced vocabulary (a concept/relation a macro declares) has a semantic, referenceable name, so hygiene gives it a content-derived, stable identity.

Macros are hygienic-only: there is no unhygienic!. A $crate-style self-reference plus syntax-parameter keywords cover the real needs; any future raw escape must name the binding space it breaks into.

Imports and the shared #[…] namespace

A pub macro foo { … } declaration occupies a single symbol in the module namespace. use mod::foo; brings it into scope; foo!(args) invokes it at expression position and #[foo(args)] at declaration position. The ! and #[…] sigils are invocation markers, not separate-namespace tags — there is no distinct macro namespace, and no #[macro_use] form; macro imports follow ordinary item-import rules (Imports).

User macros and compiler-known directives share the #[…] namespace. Resolution is by uniqueness at registration: a name resolves to exactly one implementation, and a user macro colliding with a built-in directive is an OE0705-class error, never a silent shadow (matching the loud-refusal discipline of the directive registry, Directive surface and the MLT decorator path). Identity is keyed to a stable handle, not the spelling, so re-homing a directive (Migration: re-homing the hard-coded surface) does not change how a #[name] resolves.

Procedural macros

A procedural macro computes its expansion by running code, rather than rewriting a pattern into a template. It is not a fn over a TokenStream: the procedural layer is a total, structurally-recursive meta-language over reflected syntax, not general-purpose computation. Totality is what the substrate’s own doctrine requires — it is strongly normalizing and deterministic by construction, and (being a total function over an inductive syntax type) mechanizable in Lean (Lean correspondence).

A procedural macro is a #[procmacro] pub fn in the one macro namespace:

#[procmacro]
pub fn irreflexive(item: Decl) -> Syntax {
    let head = concat_idents("__", item.name, "_irreflexive");
    quote {
        $item;
        pub check $head(x: $item.params[0].ty) :- $item.name(x, x)
          => Diagnostic { severity: Severity::Error, code: "Argon::OE1359",
               message: "relation `${item.name}` is #[irreflexive] but relates an element to itself" };
    }
}

The body is a total, non-recursive fragment: let bindings over the construction builtins and reflection projections, then a trailing quote. The surface is:

• quote { … } — a QUOTE_EXPR; its body is re-parsed through the ordinary elaboration path (never emitted as events directly). Splices: $name (a let-bound value), $item (the whole reflected declaration, re-emitted verbatim), $item.name (the relation’s name), $item.params[i].ty (a parameter’s type).
• ${expr} antiquotation — an in-string splice (e.g. inside a diagnostic message:), resolved by the macro renderer at EXPAND. It is render-time, not runtime string concatenation (the runtime has no Text + Text — that is a separate arc).
• concat_idents(a, b, …) (paste) — builds a raw definition-site identifier from pieces; the single capability the splice-only declarative layer lacks. The result is not freshened — the macro intends it as the stable public head (__{rel}_{prop}); splices are substitution barriers carrying their own use-site identity.

Bodies are non-recursive (trivially total). #[procmacro] resolves as a macro (DefKind::Macro), runs at EXPAND by a dedicated evaluator, and its #[procmacro] directive executes at fn-decl position. #[irreflexive] and #[asymmetric] (Migration: re-homing the hard-coded surface) are genuine procedural macros written exactly this way.

Full structural recursion over reflected Syntax — a totality checker, a derive-class macro inspecting a concept’s fields, #[functional]’s rel-cardinality-cap arm (which re-emits a rel with a modified cardinality bracket), and the classify ∘ expand tier-honesty theorem — is out of scope (Out of scope).

Directive surface and the MLT decorator path

Every #[…] attribute must resolve to a registered compiler directive or an in-scope pub macro (e.g. #[transitive], re-homed to std::rel, Migration: re-homing the hard-coded surface / RFD 0037 D8 — brought in by use). The directive registry (oxc-instantiate’s DIRECTIVE_REGISTRY) is the single declarative table of every directive the toolchain reads or reserves, with its argument shape, valid positions, and status. There are no silently-ignored attributes: an attribute that is neither a registered directive nor an in-scope macro refuses with OE0705 UnknownDirective (nearest-known suggestion), documented-but-unbuilt directives with OE0706 DirectiveReservedUnimplemented, misplaced directives with OE0707 DirectiveInvalidPosition, argument forms on bare-form directives with OE0709 AttributeArgsNotYetImplemented, and conflicting families with OE0714 DirectiveConflict.

The relation-property directives are library macros, split by mechanism (Migration: re-homing the hard-coded surface):

• Relation-property directives (RFD 0031) — #[transitive] is a declarative pub macro in std::rel (closure derive R(x, z) :- R(x, y), R(y, z) into the relation’s own head); #[irreflexive]/#[asymmetric] are genuine procedural macros (#[procmacro], RFD 0040) that re-emit the decorated declaration and paste a __{rel}_{prop} check head via concat_idents (Procedural macros); #[functional] is a builtin-backed macro (#[builtin] pub macro, the #[rustc_builtin_macro] analogue, OE1362 if unimported), since its rel-cardinality-cap [0..1] arm requires structural re-emission. The declarative and procedural forms format Argon source and re-parse it through the ordinary derive/check pipeline; #[functional]’s privileged path synthesizes the guard (and the cap) directly.
• MLT decorators — #[categorizes(T)], #[partitions(T)], #[subordinate_to(M)], #[power_type_of(T)], and #[order(N)] are no longer compiler directives at all. They are genuine library #[procmacro]s in the unprivileged mlt package (not std): each re-emits the decorated declaration and emits a MetaProperty on the metarel (or, for #[order], the metaxis) it shares its name with — reading the argument’s name (or, for #[order], an integer), not its structure. Nothing is ambient: a consumer lists mlt in ox.toml and imports the vocabulary (use mlt::*; / use mlt::{categorizes};), and an unimported decorator is an unknown attribute macro, refused by the no-silent-attribute gate (OE0705). The emitted MetaProperty is re-checked at the emission boundary and again at load — #[order]’s value is validated against the mlt::order metaxis’s declared Nat where { _ <= 16 } domain by the self-validating .oxbin load re-check (OE0623), so the bound holds without any compiler privilege. The reasoner-side enforcement of the MLT closure rules over the emitted metaproperties is authored as the mlt package’s own rules/checks over the neutral substrate (Phase 2).

Directives as library macros

The hard-coded directive surface is library macros, with the user-facing syntax byte-identical to a privileged-path synthesis (RFD 0009 RP-003 GAP-3). The mechanism is decided by the directive’s emit target:

• Relation-property emits ordinary rules (which have surface), so it lives in std::rel, split by what each member needs:
  • #[transitive] is a declarative pub macro: the macro template produces lowered events byte-identical to a direct synthesis (verified differentially).
  • #[irreflexive] / #[asymmetric] are genuine procedural macros (#[procmacro] pub fn … -> Syntax, RFD 0040): each re-emits the decorated declaration ($item) and pastes a pub check whose head is concat_idents("__", item.name, "_{prop}") — the unique ident the splice-only declarative layer cannot build. Their import gate is OE0705 (a bare unimported #[irreflexive] is an unknown attribute macro, like transitive).
  • #[functional] is a #[builtin] macro (importable from std::rel, OE1362 if not), with privileged synthesis as the implementation. It is one attribute covering both a metarel-check (paste-able) and a rel-cardinality-cap [0..1] on the target endpoint — and the cap arm re-emits a rel with a modified cardinality bracket, i.e. structural re-emission. An attribute name is builtin or procmacro, not split across both halves, so functional is entirely builtin.
• MLT emits MetaProperty events. Its surface is the unprivileged mlt package (RFD 0043): every decorator — the relational #[categorizes]/#[partitions]/#[subordinate_to]/#[power_type_of] and the metaxis-valued #[order(N)] — is a genuine #[procmacro] emitting a re-checked MetaProperty through the emission boundary (Procedural macros). There is no compiler builtin, no std::mlt, and no reserved MLT diagnostic code; the expander is the package’s own procmacro, not a privileged compiler path. MLT is one higher-order type theory among several (potency, ML2, powertype), so the substrate stays neutral about which one a model commits to.
• std::temporal / std::lifecycle become declarative library macros; whether each operator ships native or library is a scoping choice once the engine exists.

// std/temporal.ar — a declarative desugaring to rule-body atoms (no computation)
pub macro since {
    ( $lhs:rule since [ $lo:literal , $hi:literal ] $rhs:rule ) => {
        @meta_window($t, $lo, $hi), $rhs at $t, holds_throughout($lhs, $t, now)
    };
}

Lean correspondence

The substrate at spec/lean/Argon/Substrate/Macro.lean mechanizes the shape of macro declarations — MacroAtom = declarative MacroDecl | procedural ProcMacroDecl as @[language_interface] carriers policed by the drift gate. Per RFD 0037 D7, the substrate boundary is held at the typed AST: macro expansion is untrusted and Rust-side, and assurance comes from re-checking its output — the tier classifier runs last, the content hash is re-derivable, and the drift gate covers the MacroAtom shape. Mechanize the re-checker, not the producer.

The tier-honesty theorem — that classify ∘ expand lands a program on the same decidability class as its expansion — is statable only once expand is a total Lean object over an inductive Syntax type (RFD 0040 D7). The scope-set hygiene algebra and a full expansion-preservation theorem are out of scope.

The MLT-relational kinds — instanceOf, specializes, categorizes, partitions, subordinates — live in spec/lean/Argon/MetaCalculus/MLTKinds.lean, with the round-trip theorem classify_declOfKind; the elaborator emits canonical metarel_decl events via declOfKind.

Testing

A test declares an in-language unit test: a named imperative block run against a fresh world by ox test. Its name is a string literal; its body is the mutate-body statement set (mutate) plus the assert statement. An assert mirrors require, except a failed assert records a pass/fail outcome and execution continues (rather than aborting). Three assertion forms exist: the value/boolean form assert <expr>;; the derivability form assert [not] derivable F(args);, which tests membership / non-derivability of a fact against the materialized extent with world-honest three-valued outcomes — present ⇒ PASS/FAIL, absent under closed-world ⇒ FAIL/PASS, absent under open-world ⇒ a loud INCONCLUSIVE (absence is unknown, not false, World assumptions (CWA / OWA)); and the rejection form assert rejects [( Pkg::Code )] { … }, which asserts that a write block is refused by a write-path guard (a where-invariant, a check delta-guard, a group axiom, …) — a genuine guard rejection PASSes (matching a pinned code if given), an accepted write FAILs, and a non-guard error ERRORs loudly so a broken test never masquerades as a passing rejection. derivable and rejects are contextual keywords (leading position only). The runner, the full assertion semantics — including reads over the deductive plane, the three-valued tables, and the guard-vs-non-guard classification — isolation, and the scope are specified in Runtime contract.

test-decl ::= attribute* 'test' String '{' test-stmt* '}'
test-stmt ::= mutate-stmt            // `mutate`: let / insert / update / delete / for / require / calls
           |  'assert' expr ';'
           |  'assert' 'not'? 'derivable' IDENT '(' (expr (',' expr)*)? ')' ';'
           |  'assert' 'rejects' ('(' path ')')? '{' mutate-stmt* '}' ';'

(The fixture / expect block forms are reserved and do not parse.)

pub type Account { name: String }

// A test constructs a world top-to-bottom and asserts over it; `ox test`
// runs each test against its own fresh store and reports PASS / FAIL / ERROR.
test "a constructed account carries its name" {
    let cash = insert Account { name: "Cash" };
    assert cash.name == "Cash";
}

Discovery. ox test runs test declarations from mod-reachable modules and auto-discovers every *.ar anywhere under the package’s tests/ directory (recursive, any depth — so no test under tests/ silently fails to run), elaborating them as part of the package — so a test placed in the reserved tests/ directory runs without mod-wiring, symmetric with scenarios/*.toml. This is test-mode only: tests/*.ar never enters ox build’s artifact. See Runtime contract.

Isolation. Each test runs against its own fresh store seeded with the package’s declared facts; no test sees another’s writes, so test ordering is unspecified and irrelevant. Within a test, the body’s writes are visible to later assertions, including the facts they derive (read-your-writes over the committed + deductive state). See Runtime contract for the ox test runner and the assertion semantics in full.

Scenario harness — ox run-scenario

An .ar package declares the ontology; it does not carry data. So a built .oxbin queried with no fixtures answers against an empty store. A scenario is a small .toml script that seeds the store and then reads it back, so a model ships with realistic, reproducible state — and, with assertions, with executable checks.

A scenario file lists an ordered sequence of steps. Each [[step]] is tagged by do:

[[step]]
do   = "mutate"                  # invoke a declared mutation
path = "norms::register"
args = { p = "alice", age = 25 }

[[step]]
do     = "query"                 # run a declared query, print its rows
path   = "norms::findEmployeeNamesOfCompany"
args   = { c = "acme" }
label  = "employees of acme"     # optional, echoed in the output

[[step]]
do      = "derive"               # dump a derived predicate's extent
name    = "spouses"              # the rule head's short name
explain = true                   # optional: annotate each tuple with its proof tag

[[step]]
do    = "compute"                # invoke a declared `fn`, print its single result
path  = "norms::getSpouse"
args  = { p = "alice" }

Document order is execution order. A scenario interleaves writes and reads: populate, look, mutate again, look again — each read sees the state at that point. The four kinds map to the same operations as the standalone commands: a mutate step runs a declared mutation (with the same check-guard handling as a write over HTTP); a query step runs a declared pub query and prints its rows; a derive step dumps a derivation’s extent by its rule-head short name, the read ox derive <oxbin> <rule> performs (with explain = true adding the Rule atom — fn, derive, query, mutate, check proof tag per tuple); a compute step evaluates a declared pub fn and prints the single value it returns.

A query step’s args is what makes a parameterized declared query do a keyed lookup. A pub query findEmployeeNamesOfCompany(c: Company) -> … whose body binds c looks c up only when c is supplied; with no args, the parameter degrades to a free join variable and the query enumerates the whole extent. A derive step takes no args — a derivation has no parameters, so it always dumps the full extent.

Argument typing

Each args table maps a parameter name to a TOML value, typed into the runtime’s value space by one shared rule (the same path expect tuples use, below):

A bare string defaulting to an individual is the load-bearing convention: the same name in the source and in the scenario refers to the same entity. Array values and a non-finite float are rejected with a clear diagnostic.

Assertions — expect

Add an expect table to a step and it stops being a printer and becomes a test: its result is diffed against the expectation and a PASS/FAIL verdict is reported. Which sub-keys apply depends on the step kind:

[[step]]
do     = "query"
path   = "norms::findEmployeeNamesOfCompany"
args   = { c = "acme" }
expect = { equals = [ [{ text = "Dave" }], [{ text = "Alice" }] ] }

[[step]]
do     = "derive"
name   = "isDisenfranchised"
expect = { empty = true }

[[step]]
do     = "compute"
path   = "norms::getSpouse"
args   = { p = "alice" }
expect = { value = "dave" }      # a single expected value

[[step]]
do       = "mutate"
path     = "norms::register"
args     = { p = "bob", age = 12 }
expect   = { rejected = "Norms::E001" }   # assert a check guard rejects it

• A query or derive step takes the row-set sub-keys: rows = N (exact count), contains = [tuple, …] (every listed tuple is present, count-sensitive), equals = [tuple, …] (the result set matches exactly, order-insensitive multiset equality), empty = true (no rows).
• A compute step takes value = <toml value>: a single expected value.
• A mutate step takes rejected = "<CODE>": assert the mutation is rejected by a check guard carrying that user code. A rejection by that code is a PASS and the run continues (the rejected transaction committed nothing); a success or a rejection by a different code is a FAIL. Without rejected, a guard rejection halts the scenario.

The correctness crux is that an expected value is typed through the same rule as the step args, and the diff is by value identity — never by rendered string. So an entity-valued result column matches a bare-string or { individual = "…" } expectation, but never a { text = "…" } one; a Text "dave" is never equal to the individual dave. A sub-key applied to the wrong kind (value on a query, rows on a compute, an unknown key) is a loud scenario error, not a silent no-op.

Files, discovery, and running

A package carries scenarios as a sibling demo.toml and/or any number of files under a scenarios/ subdirectory:

ox run-scenario <pkg>                       # run every discovered scenario
ox run-scenario <pkg> --scenario voting     # run scenarios/voting.toml (or a sibling voting.toml)
ox run-scenario <pkg> --scenario path/to.toml
ox run-scenario <pkg> --extent norms::Voter  # also print a concept extent after the run

With no --scenario, run-scenario discovers every scenario — the sibling demo.toml plus every scenarios/*.toml, filename-sorted for determinism — and runs them all. Each scenario runs against its own freshly-loaded, freshly-seeded store re-derived from the artifact bytes, so a mutation in one scenario cannot leak into another’s reads and the order across files is irrelevant. --scenario runs exactly one: a path verbatim, or a bare name resolving to scenarios/<name>.toml then a sibling <name>.toml. --extent <concept> prints that concept’s extent once the scenario has run.

run-scenario collects every failed assertion (it does not stop at the first) and exits non-zero if any assertion — or any scenario — failed, naming the offending file. A scenario therefore doubles as a CI-usable check.

A single file uses either [[step]] or the older flat [[mutate]] list (a pure population script, applied in order), never both — the whole point of [[step]] is interleaving, which a split across two arrays cannot express. The flat [[mutate]] form is also what ox query and ox derive apply when they find a sibling demo.toml: they seed from [[mutate]] fixtures, then run their own read. A [[step]] scenario beside one of those commands is not run by them (they have nowhere to surface the interleaved reads); they print a warning pointing at ox run-scenario.

The scenarios/ directory is the integration-.toml surface, distinct from tests/, which holds the in-language test atom (The test atom — ox test). The two are complementary: scenarios/ scripts the runtime from outside the language with a .toml harness; the test atom expresses checks inside the language.

The test atom — ox test

A test is a named imperative block, run top-to-bottom against a fresh store. Its name is a string literal; its body is the mutate-body statement set (let / insert / update / delete / for / require and declared mutation/fn calls — mutate, RFD 0015) plus the assert statement:

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;   // reads the derived value
    assert accountBalance(rev) == -100.50;
}

An assert mirrors require exactly, with one difference: a failed require aborts the body; a failed assert records a pass/fail outcome and execution continues. true is a PASS, false a FAIL, and an evaluation error (an unbound reference, a non-boolean result, a missing field, a value not derivable in the current state) is an ERROR (the test errors; it never panics). Setup and assertions interleave naturally, so there is no separate fixture block.

Asserting over the deductive plane. A condition that names a derived predicate or a declared pub query — accountBalance(cash), or the nav-method form x.active_leases() — is evaluated against the reasoner’s materialized extent at the fixpoint of the current committed state, the same read path ox query / ox derive and the for x in <derive> snapshot use. A keyed call (accountBalance(cash)) selects the row whose leading columns match the argument and returns its head-carried value; with no matching row the assert ERRORs (the value is not derivable), and an ambiguous match is a loud error too. Scalar comparisons, field access, arithmetic, and aggregates evaluate as in a require guard. This is the point of testing a reasoning system: an assert checks what the rules derive, not just what was stored.

Asserting derivability — assert [not] derivable F(args). The value-read assert above answers what value a keyed derive carries; the derivability form answers whether a fact holds at all — membership and, crucially, non-derivability. assert derivable F(a, …) passes when a row whose leading columns equal the resolved args is in F’s materialized extent; assert not derivable F(a, …) is its negation. The predicate F resolves the same way the value-read assert and for x in <derive> do — a derive head, a declared pub query, or a base rel. The predicate slot accepts a qualified path (assert derivable students::adult(p), assert not derivable pkg::accounts::adult(p)), resolved by the same ::-suffix matching the rest of the runtime uses: a bare leaf resolves when it is unambiguous, and qualifying disambiguates a name carried by two heads in different modules — that case stays a loud ERROR for the bare form, naming every candidate, so qualification is the way to pick one. Partial args test prefix membership (derivable amtOf(acme) over amtOf(account, money) = “some row has account == acme”); zero args test extent non-emptiness (derivable F()). A predicate that names nothing is a loud ERROR, not a silent outcome. derivable is a contextual keyword — recognized only in leading position after assert / assert not, so it stays usable as an ordinary identifier everywhere else.

The outcome is world-honest and three-valued, keyed on the predicate’s world assumption (World assumptions (CWA / OWA)):

The open-world row is the load-bearing soundness case. Under the open-world assumption absence of evidence is not evidence of absence (World assumptions (CWA / OWA)): a missing row is unknown, not false, so closed-world non-derivability is not assertable and must never silently pass. The runner reports a distinct, loud INCONCLUSIVE outcome — neither PASS nor FAIL — carrying a teaching detail that names the open-world cause and the two ways forward (assert a positive outcome instead, or mark the concept #[world(closed)] if it should be closed). This composes with the world-honest negation-as-failure of the rule engine: a derivability assert reads the same world each negated atom does.

Asserting rejection — assert rejects [( Pkg::Code )] { … }. Argon is a constraint language; a model’s most important property is which writes its where-invariants and check delta-guards turn away. The two forms above assert positive outcomes — the negative-enforcement half is assert rejects { <mutate-body-stmts> }, which asserts that the block’s write is refused by a write-path guard. The block admits the full mutate-body statement set (insert / insert iof / update / delete / mutation calls); it runs against an isolated copy of the test world, so it commits nothing back regardless of outcome. An optional code pin assert rejects(Pkg::Code) { … } requires the rejection to carry that exact diagnostic code. Like derivable, rejects is a contextual keyword — recognized only in leading position after assert — so it stays usable as an ordinary identifier elsewhere.

The outcome is three-valued, and the guard-vs-non-guard distinction is load-bearing:

A guard rejection is a genuine constraint refusal on the write path — a where-invariant violation (OE0668), a check delta-guard refusal (which is also how a group axiom — disjoint / complete / partition — surfaces, carrying the check’s own Pkg::Code), an insert iof onto a defined (iff) concept (OE0211), a write onto an abstract or fixed-introduced type (OE0233 / OE0234), a construction-completeness refusal (OE0207 / OE1014), a property write to an unclassified individual (OE0238), or a relation write over a non-existent endpoint or past a declared cardinality (OE0232 / OE1341). Only these satisfy rejects. A non-guard error — a typo, an unbound reference, a type error, an unevaluable term, a stray require failure — is reported as a loud ERROR, never counted as a rejection: a broken test must never masquerade as a passing rejection test. An accepted write is a FAIL (and is rolled back, like any other block outcome, so it does not pollute the rest of the test). Use the positive forms to test that a legal write is accepted.

Isolation. Each test runs against its own fresh store seeded with the package’s declared facts (the same fresh-store-per-run discipline as the scenario harness, Scenario harness — ox run-scenario). No test sees another’s writes, so tests are order-independent. Within one test, the body’s writes are flushed and the read-model maintained before each assert, so an assert observes every earlier write — including the derived facts they entail (read-your-writes over the committed + deductive state).

Discovery + running. ox test runs every test from two sources, unioned: (1) any test declaration in a mod-reachable module (e.g. tests/mod.ar reached by mod tests;), and (2) every *.ar anywhere under <pkg>/tests/, which ox test auto-discovers (recursive, any depth — a nested tests/sub/foo.ar is discovered too, so no test under tests/ silently fails to run — filename-sorted) and elaborates as part of the package, so each sees the package’s full vocabulary. This mirrors how ox run-scenario auto-discovers scenarios/*.toml: a test placed in the reserved tests/ directory runs without mod-wiring. A tests/ file that is also mod-reachable is folded exactly once (its tests never double-run). A discovered tests/foo.ar references package items by their package-absolute path (pkg::…). This discovery is test-mode only: ox build / ox check and the shipped .oxbin never include tests/*.ar — tests do not ship. Tests are inert at query / serve time; only ox test enumerates and runs them:

ox test <pkg>                 # build the package (+ tests/), run every test, report
ox test <pkg> --filter NAME   # run only tests whose name/path contains NAME

A tests/*.ar with a parse or resolve error fails loudly (ox test aborts with the diagnostic), never a silent skip; a package with genuinely no tests anywhere prints “no tests found” and exits 0.

ox test builds the package (so the run reflects current source), runs every discovered test, and prints a PASS / FAIL / ERROR / INCONCLUSIVE line per test — a failed or inconclusive assertion shows its rendered source text and why it could not pass — followed by an N passed, M failed, K errored, I inconclusive summary. A test’s rollup status takes the strongest of its assertions in the precedence Error > Fail > Inconclusive > Pass. It exits non-zero if any test fails, errors, or is inconclusive (a test you cannot decide is not green), so ox test doubles as a CI-usable gate (like ox run-scenario).

Assertion forms. Three forms are admitted. The value/boolean form is assert <bool-expr>; — scalar comparisons (==, !=, <, <=, >, >=), field access on bound entities (x.field, chained x.a.b), arithmetic on those, the aggregate/comprehension forms, and the deductive-plane reads above (a derived-predicate / pub query keyed call, and the nav-method x.method() form). The derivability form is assert [not] derivable F(args); with the world-honest three-valued semantics above. The rejection form is assert rejects [( Pkg::Code )] { <mutate-body-stmts> } — the negative-enforcement half above. All three are test-only: a stray assert (any form) in a mutate / fn body lowers to an unsupported form and ox check / ox build refuse it up front with OE1318 (the runtime also rejects it, as defense-in-depth) — it is never a silent no-op.

Only the three assert forms above are admitted; anything else is a loud refusal, never a silent pass.

Truth values

Types

Two related types, exported from std::core and in the prelude:

pub enum Truth4 { Is, Not, Can, Both }                              // substrate, no payload
pub enum Truth4Of<T> { Is(T), Not, Can, Both(T, T) }                  // parameterized lift

The unparameterized Truth4 is the substrate bilattice carrier — what the Lean spec mechanizes and what Federation.infoJoin, Consistency.append, and Projection.project operate over. The parameterized Truth4Of<T> is the stdlib presentation type used at query-result boundaries that have already produced typed projections — Is(T) carries the witness for the is verdict; Both(T, T) carries the two disagreeing witnesses.

Locked-substrate semantics (per Foundation/Truth4.lean, Standpoint/Consistency.lean, Standpoint/Federation.lean):

• K3 single-standpoint queries return projections containing only Is, Not, Can.
• FDE across [...] queries may return Both(a, b) when standpoints disagree.
• #[consistency(paraconsistent)] standpoints admit Both internally.

Default visibility and K3 projection

Default query return type is the projection type (e.g., Bool, [Lease]); Truth4Of<T> is introduced only when:

• The query has across [...].
• The return type is explicitly Truth4Of<…>.
• A paraconsistent standpoint admits internal Both.

K3 fail-closed projection. When a single-standpoint K3-context query projects to a non-Truth4 type, Can is folded into the projection per Pietz–Rivieccio Exactly-True semantics:

• Boolean projections: Can → false. Only Is(true) is designated.
• Set / list / record projections: Can-valued cells are omitted from the result set.
• Scalar projections: Can collapses fail-closed (omitted for collection-shaped results, false for Boolean predicates).

To preserve the distinction between Not and Can at the surface, declare the return type as Truth4Of<T> explicitly.

The compiler emits Info-level diagnostics on every across query reminding the modeler that Both may arise.

World assumptions (CWA / OWA)

A world assumption governs how the absence of evidence is interpreted:

• Closed (CWA) — if a fact isn’t derivable, it’s false. Negation-as-failure is total.
• Open (OWA) — if a fact isn’t derivable, it’s unknown. Negation requires positive disproof.

The blessed default is CWA; OWA is a live per-concept opt-in. Every concept Argon evaluates is closed-world unless it carries a #[world(open)] mark: negation-as-failure over the stratified / well-founded fixpoint (Rule atom — fn, derive, query, mutate, check, truth values) treats an unmarked concept’s absent membership as definite-false. The package-level default_world (CWA unless a manifest sets it otherwise) governs every concept without an explicit mark. This default is a deliberate choice: an Argon program is a data system whose extents are the authority for what is true, and CWA is the regime that makes “not in the extent” mean “false”. A modeler who wants the OWL/DL open-world reading for a specific concept opts that concept in with #[world(open)], described below (RFD 0045, #787/#796).

CWA is the operative default because Argon’s primary use is application data — counts, payments, schedules, classifications — where the stored extent is the closed world. Concepts that model genuinely-incomplete knowledge (where “absent” means “unknown”, not “false”) opt into the open-world reading per the surface below.

Per-concept OWA opt-in (#[world(open|closed)]) — live. The surface is a #[world(...)] attribute on an ontologically-classified concept:

#[world(open)]
pub type LegalAgent { mut name: String }   // OWA — `unknown` is distinct from `false`

The world directive is executed (RFD 0045 D2): the elaborator reads the policy word — open or closed, any other word is a loud refusal — records the concept’s world assumption on the per-concept world map (keyed by qualified concept path), and the reasoner stamps that map onto every evaluation catalog so each negated concept-membership atom is read under its own concept’s world. The attribute is concept-only (OE0707 on other placements). Concepts without the attribute inherit the package default_world (CWA by default).

The OWA semantics. The world a concept declares changes how the substrate reads its absence:

Interaction with negation-as-failure (Rule atom — fn, derive, query, mutate, check). Under CWA, not P succeeds whenever P is not derivable. Under OWA, an absent P(x) is unknown, not a definite not — so a closed-world not H whose derivation depends on an open-world negation does not get to read that unknown as false. Rather than silently over-asserting the head, the substrate refuses that genuinely-unsound shape at ox check / ox build (OE1367 NegatedOpenWorldDerived): mark H’s concept open-world too (so not H tolerates the unknown), or restructure so the open-world negation does not flow into a closed-world-negated head. This is world-honest negation-as-failure: the engine honors default_world and each concept’s mark instead of evaluating closed-world unconditionally. The is unknown rule atom (Rule-atom grammar) is reachable under OWA — an open-world concept’s absent membership flows through it as unknown.

Interaction with the write side. A concept’s world governs its compiler-synthesized structural checks. Under the closed-world default a complete/partition covering check fires when no member membership is derivable (OE0241) and a disjoint overlap check refuses a double-classification (OE0240). Under an open-world concept the covering check softens to refuse-on-K3-not — refuse only on a definite violation, tolerating the merely-unknown case — while disjointness stays world-invariant (a positive overlap is definite under any world). This is the RFD 0045 D1/D2 design.

Interaction with the test atom. assert [not] derivable F(x) (Runtime contract) reads F’s world directly: a present row is PASS/FAIL; an absent row under CWA is definite non-derivability (FAIL for derivable, PASS for not derivable); an absent row under OWA is unknown, so closed-world non-derivability is not assertable — the runner reports a distinct, loud INCONCLUSIVE, never a silent pass.

Interaction with refinement (Refinement). The world a concept declares makes iff-derived membership three-valued — unknown does not grant membership, and a primitive where invariant is the dual where only a definite false denies a write — whereas under CWA unknown collapses to false in both directions. The three-valued refinement field-access discipline is a separate mechanism: a refinement predicate reading a field with no recorded value evaluates to unknown rather than failing — the K3 fail-closed boundary of Refinement, orthogonal to the concept-level world assumption. A missing field makes a predicate unknown; the world assumption then decides whether that unknown collapses to false (CWA) or is preserved (OWA).

Required-field completeness under CWA. Under the closed-world default a required field that is unasserted is a schema violation, not an unknown. OE1014 RequiredFieldUnasserted fires for the in-body construction case — a mutate body that classifies an individual with insert iof and populates its fields in the same body — at body end / commit time (see mutate). The construction-time gate for brace construction (insert T { … } missing a required field, OE0207) is unconditional. Under an #[world(open)] concept an unasserted required field is unknown rather than a violation.

Cross-world conservativity (mechanized). A CWA-true result lifts safely into an OWA consumer — positive evidence stays positive when more information may yet arrive. The base transfer theorem is mechanized at TypeSystem/Soundness/CwaOwa.lean (cwa_owa_transfer): a refinement membership established under CWA remains valid when re-evaluated under OWA, and cwa_isCwa_preserved_under_info_increase extends this to a more-informative consistent (K3) state. The reverse is provably not sound (owa_to_cwa_not_sound): a CWA conclusion that holds only via the closed-world collapse of an unknown to false does not transfer. The module is deliberately parameterized over the WorldAssumption — the CWA default is a surface/engine policy, not a substrate theorem, so the mechanization arbitrates the relationship between the two regimes without privileging either. The bitemporal lift of the transfer is in Locality/Temporal.lean.

Module-extraction interaction. Cross-module imports preserve CWA conclusions about the imported signature via ⊥-local module extraction; the Σ-scoped conservativity theorems are in Module extraction (tree-shaking) (Locality/ScopedConservativity.lean, Locality/DomainConservative.lean).

Per-(standpoint, concept), not per-(concept, time). A world assumption is declared per-(standpoint, concept), never per-(concept, time). A modeler needing different closure disciplines across valid-time would declare two or more standpoints with VT-scoped activation conditions and compose them via standpoint federation (Standpoints and modal operators); the substrate WA-map signature has no time argument. Attempting a per-concept closure with an explicit VT scope without standpoint decomposition is refused with OE0810 WorldAssumptionTemporalIndex.

Reasoning

A derive program is a set of rules (derive); its meaning is the set of tuples those rules derive. This chapter fixes that meaning: the least-fixpoint model of the positive program, the stratification that orders negation, the well-founded semantics that handles recursion through negation, and the defeasibility layer that compiles overrides onto all of it. The surface — what a derive rule looks like and what each clause is allowed to say — is in derive; this chapter is what the engine computes from it.

Least-fixpoint model

A positive derive program (no negation, no aggregation) denotes a single model: the least fixpoint of its immediate-consequence operator. Start from the ground facts, apply every rule once to derive new tuples, repeat until nothing new appears. Over a finite domain this terminates, and the result is unique — independent of the order rules fire. Multiple derive clauses with matching head name and arity union into one relation node, so a seed tuple and a recursive clause over the same head share a fixpoint (seeds ∪ derived-closure).

Aggregation extends the operator without breaking uniqueness, provided each aggregate reads a strictly lower stratum than its head writes (the stratification below). The aggregate fold then sees a converged input relation before it runs, so the fixpoint over the layered program is still unique.

Stratified negation

Negation breaks the monotonicity the least fixpoint relies on: a tuple that adds to a positive relation can remove a tuple that a not atom guarded. Stratification restores order. The rules are partitioned along their axis dependency graph — which axes a rule’s body reads against which axis its head writes — and each layer is evaluated to fixpoint before the layer above it reads its negation. A rule’s body negation must read a relation already converged in a lower stratum.

The graph must be acyclic for this layering to exist. The Lean substrate proves (Theorem 2) that a cycle in the axis dependency graph admits a Cat1/Cat2 rule pair whose stratified fixpoint is order-dependent — there is no canonical layer assignment, so the program has no single stratified model. Cross-stratum, acyclic negation is ordinary stratified negation and is evaluated by this layering.

A negation cycle that no stratification can layer — p :- not q, q :- not p — is not rejected. It is dispatched to the well-founded semantics below. (The diagnostic that once rejected such a cycle, OE1309, no longer fires from stratification; it survives only as the dispatch seam.)

Well-founded semantics

Negation reads against the well-founded model, computed by the Van Gelder–Ross–Schlipf 1991 alternating fixpoint. WFS is the default because the well-founded model always exists and is unique — every program has exactly one, with no choice for the engine to make. The headline consequence: recursion through negation is accepted. A negation cycle that strict stratification cannot layer is evaluated by the alternating fixpoint rather than refused.

The alternating fixpoint is three-valued: every atom is true, false, or undefined. The query surface is two-valued. The engine materializes only the definitely-true extent — a paradoxical atom (one the alternating fixpoint cannot pin to true or false) resolves to undefined and simply does not fire. For conditional obligations this is the sound projection: an obligation whose trigger is genuinely undecided neither fires nor is denied; it is omitted.

#[brave] / stable-model semantics — multiple two-valued models, with credulous and skeptical readings — is out of scope (Out of scope). WFS is the single evaluation discipline.

Defeasible reasoning

Real ontologies have exceptions and overrides; classical Datalog does not. Argon’s defeasibility (RFD 0028) makes them first-class without letting any rule lie about what it derives. The design has three commitments:

1. Honest heads. A rule derives exactly what its head says. An unmarked derive rule is strict — classical Datalog, exactly as derive; its conclusions cannot be overridden.
2. The attack is a directive, not grammar. Whether one rule displaces another is a statement about rules, carried in the directive plane above the rule, never a clause inside its body.
3. Strategy is a compilation scheme. The meaning of a defeasible program is the meaning of its compilation onto the core stratified/WFS semantics. No separate reasoner runs; the engine stays strategy-blind.

The directive vocabulary

The canonical example — adults can vote by default, felons are disenfranchised, special-class members vote regardless — reads true at every line:

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

No rule spells the head it denies. The exception lives under its own name (disenfranchised); the attack rides the directive plane. The pure “block without asserting” defeater (Governatori’s ⇝) is the degenerate case — a #[defeats(…)] rule whose head no one reads.

Targeting

A #[defeats] target is resolution-checked at elaboration (goto-def-able); an unresolvable target refuses loudly. Three targeting forms ship:

• Head-level — #[defeats(can_vote(p))]: attacks every #[default] clause of that head.
• Clause-level — #[defeats(can_vote.adult(p))]: attacks exactly the clause labeled adult. This is lex specialis — the specific rule defeating the general clause’s label, an explicit cross-package-stable edge rather than a pair of magic priority integers.
• Trait-qualified — #[defeats(Vote::can_vote(p) @ A)]: attacks a trait member’s clause at a given impl target, using the qualified catalog naming (Rule-atom grammar). Exceptions compose across modules: a regulation package can defeat a clause it does not own.

Arguments resolve against the decorated rule’s variables. #[defeats(can_vote(p))] on disenfranchised(p) blocks can_vote exactly for the p the attacker derives — per-tuple blocking, not head-wide suppression. A #[defeats] argument that binds in neither the head nor the body of the rule is a loud error (OE0721), never a fresh variable.

Discipline

• Strict conclusions are unattackable (OE0717). A #[defeats] target resolving to a head or clause not marked #[default] refuses: adding rules to a classical program can only add conclusions.
• Defeat-graph cycles are refused (OE0718). The graph over resolved rule identities is acyclic by build-time check; cyclic attack structures are where the well-behaved compilation stories diverge, and Argon refuses rather than picking one silently.
• Defeated defeaters are legal — a #[defeats] rule may itself be #[default] and be attacked in turn (the exception to the exception), as long as the chain bottoms out.
• Team defeat, ambiguity blocking. A tuple is in the head’s extent iff some clause not attacked on that tuple derives it — an unbeaten teammate keeps the conclusion. A blocked tuple is simply absent from the extent; it does not propagate a third truth value downstream.
• Duplicate labels per head refuse (OE0719); labels are per-head identities.

Strategy #1: Governatori with explicit superiority

The strategy is Governatori-style defeasible logic with explicit superiority and ambiguity blocking, specified as its Maher-2021 three-stratum compilation onto the core stratified/WFS semantics:

1. Support — run every clause (strict + default, plus the attacker rules’ own honest heads) to fixpoint over the materialized base, and attribute each clause’s contribution over that converged catalog — a recursive clause sees its own prior tuples, so transitive closure does not under-derive.
2. Blocking, from surviving attackers — project each attacker’s surviving extent (resolved in defeat-graph topological order, which exists because the graph is acyclic) through its edge argument binding to the blocked target tuples (per-tuple). A defeated defeater contributes nothing — it no longer blocks on the tuples where it was itself defeated.
3. Team-defeat fold — strict clauses contribute unconditionally; a default clause contributes the tuples no surviving edge blocks.

The strategy id is recorded in the .oxbin so an artifact is honest about which compilation gave it its meaning. Future strategies (default logic, courteous LP, argumentation, ASP preferences) arrive as use-imported macro-vocabulary packages selected per module; the engine never changes.

Proof tags

Every derived fact carries one of four tags (Rule-atom grammar), surfaced through the provenance channel (ox derive --explain):

• +Δ definitely provable — supported by a strict (unattackable) clause.
• −Δ definitely refuted.
• +∂ defeasibly provable — a surviving #[default] clause supports it after defeat resolution.
• −∂ defeasibly refuted — every supporting clause was attacked.

$ ox derive examples/legal_norms_can_vote can_vote --explain
  +Δ (dave)     // strict special-class clause
  +∂ (alice)    // surviving adult default

The Lean substrate proves the defeat algebra over each clause’s converged contribution: the team-defeat fold realizes the declarative per-tuple warranted set (Argon.Reasoning.Defeasibility.Transform.compiled_extent_eq_warranted), strict conclusions are unattackable (strict_clause_unattackable), ambiguity blocking holds (all_supporting_clauses_attacked_absent), and — modelling the blocking sets as derived from the attackers’ surviving extents rather than as opaque inputs — a defeated defeater no longer blocks (defeated_defeater_does_not_block, block_mono_in_survivors, pardoned_target_survives). The safe interaction with occurrence typing carries over — only narrowings established by strict (non-#[default]) rules are preserved under defeasible attack (Argon.TypeSystem.Soundness.Defeasibility).

Migration from the strength triple

The pre-RFD-0028 surface — #[strict] / #[defeasible] / #[defeater], #[priority(N)], and pub priority blocks — is removed, and refuses loudly (OE0722) with no silent aliasing. The map:

• #[defeasible] → #[default].
• #[defeater] (which spelled the head it denied) → an ordinary rule under its own honest head carrying #[defeats(target(args))]; the targeted clause must be #[default].
• #[strict] → delete it; unmarked rules are already strict.
• #[priority(N)] / pub priority → an explicit #[defeats] edge. Lex specialis is the specific rule defeating the general clause’s #[label]. Derived superiority (lex posterior over enactment dates) belongs to a future strategy vocabulary that derives edges.

Standpoints and modal operators

Standpoint declaration and federation

standpoint-decl ::= attribute* 'pub'? 'standpoint' Ident ('<:' TypeExpr (',' …)*)?
                     '{' mod-item* '}'

pub standpoint USFederalTax {
    pub type TaxableIncome <: Money;
    pub derive owes_tax(p: Person) :- p.income: TaxableIncome, p.income > 0;
}

pub standpoint California <: USFederalTax {
    pub derive state_owes_tax(p: Person) :- /* … */;
}

pub standpoint ContestedClaims { /* … */ }

A standpoint is a namespace-bearing module: items declared inside are accessible as StandpointName::ItemName (e.g., USFederalTax::owes_tax). The <: relation between standpoints declares lattice membership (federation ancestor for across [...] queries), not namespace inheritance — a child standpoint does not automatically see the parent’s items; explicit use is required to bring items into scope. Cross-standpoint federation via the across [...] annotation on queries; results may carry Truth4 values.

Nested standpoint declarations are not admitted — lattice edges come from <:, not from textual containment. Submodules (mod) and impl blocks inside a standpoint are permitted.

Federation conflict policy is chosen per query, not per standpoint: a federated across [...] query is paraconsistent by default — disagreement surfaces as Both (see truth values) — and may request strict projection. Conflict policy is a per-query projection, not a standpoint-level declaration.

Visibility composition. Facts are scoped by where they are asserted. A fact/not_fact declared inside a standpoint s { … } block is local to s; one declared at file/module scope, outside any standpoint block, sits in the DEFAULT (unscoped) layer. The two compose by the sheaf reading (Sheaf-theoretic semantics for standpoint federation):

• The DEFAULT layer restricts into every view. An unscoped assertion is visible to an unfederated query, to every standpoint-scoped query, and to every standpoint in an across [...] federation — it is the broadest perspective, and the sheaf restriction maps carry it into every stalk.
• A standpoint-scoped fact is invisible outside its standpoint. It does not appear in an unfederated (unscoped) query, nor in a query scoped to a different standpoint. Reading a scoped fact requires explicitly selecting its standpoint — via across [...], box/diamond (Modal operators), or a bridge rule (Bridge rules).

So an unfederated query (pub query q() -> P;) reads exactly the DEFAULT layer; a single-standpoint federation (across [s]) reads the DEFAULT layer unioned with s’s own facts; a multi-standpoint federation info-joins those per-standpoint views (Sheaf-theoretic semantics for standpoint federation). Derive rules, checks, and the mutation delta-guard all evaluate over the DEFAULT-layer (base) view — a scoped fact never silently becomes global truth. A federated query that names a standpoint with no declaration is refused (OE1103 UndeclaredStandpointInAcross) rather than contributing an empty extent that would mask the typo. Mechanized at spec/lean/Argon/Standpoint/Visibility.lean: view_of_base_eq_default_layer (base = DEFAULT layer), scoped_view_eq_default_union_own (scoped = DEFAULT ∪ own standpoint), default_visible_everywhere, scoped_invisible_to_base, and scoped_invisible_to_other.

Modal operators

box(P) and diamond(P) are rule atoms (Rule-atom grammar) admitted at tier:modal. They are interpreted over a Kripke frame; the frame is determined by the surrounding context.

Frames. Argon recognizes two intrinsic frames:

• Standpoint frame. Worlds are standpoints; the accessibility relation is the reflexive-transitive closure of <: over the standpoints in scope (extended by the explicit set of any enclosing across [...] clause). box(P) at standpoint s holds iff P holds at every s' reachable from s along the frame.
• Classification frame. Worlds are configurations in which an individual exists (store states reachable by mutations). A type introduced by a fixed metatype (metatype, RFD 0027 D6) carries forward rigidity: once an individual is a member, the mutate mutation gate preserves that membership forward along accessibility (Argon.Runtime.ModifierGates.runMutation_fixed_iof_constant). This is one-directional, not two-way constancy — a current non-member can still later be constructed into a fixed type, so fixed pins membership going forward but says nothing about future gains. A type introduced by an unmodified (dynamic) metatype carries no such guarantee. This is the standard Guizzardi/UFO modal characterization of rigidity, realized operationally by the ontology-neutral fixed bit rather than by reading any vocabulary’s rigidity axis.

diamond(P) is dual: it holds when P holds in at least one accessible world.

Static discharge. When P is a positive type-classification atom over a target introduced by a fixed metatype, forward rigidity preserves membership across accessible worlds and the elaborator can discharge the modal at compile time without consulting a reasoner (Argon.Reasoning.StaticDischarge.box_fixed_discharge). The discharge is polarity-asymmetric: forward rigidity grips box(x : T) but gives no grip on the negation box(¬(x : T)), since a current non-member may still be constructed into the type later (Argon.Reasoning.StaticDischarge.isRigidIn_does_not_discharge_box_neg).

Atoms that survive static discharge are routed to a modal reasoner over the std::kripke carrier; the choice of backend (tableau, resolution, bounded model-checking) is implementation-defined.

std::kripke. Exported from the stdlib for explicit modal modeling — e.g., writing forall w: World where accessible(current, w), P@w inside unsafe logic { }. The carrier is minimal:

// in std::kripke
pub struct World;
pub struct Entity;
pub fn iof(e: Entity, t: Top, w: World) -> Bool;            // instance-of-in-world
pub fn accessible(w1: World, w2: World) -> Bool;            // frame accessibility
pub fn current() -> World;                                   // the current world

The surface operators box(P) and diamond(P) are syntactic forms — not function calls — and desugar to FOL over World:

Where P@w denotes the rule atom P evaluated at world w (i.e., relativized to w’s extension). Modelers using only the surface operators need not import std::kripke directly; the desugaring threads through the elaborator. There are no Box / Diamond runtime functions — modal operators reduce to quantification over worlds.

Federation interaction. Inside a query annotated across [s₁, s₂, …], the standpoint frame is extended to the named set; box(P) reads “P holds in every listed standpoint” and may return Both, Can, or Not per truth values when the standpoints disagree. Classification-frame box/diamond atoms compose with federation by being evaluated independently at each listed standpoint, then info-joined via the FDE lattice.

Lowering. box(P) and diamond(P) lower to AtomIR::Modal and classify at tier:modal. Cross-nesting a modal with a temporal operator is refused by the tier classifier. examples/modal_box_diamond.ar exercises both operators end-to-end.

Bridge rules

Bridge rules thread information explicitly between standpoints. Where across [...] composes standpoints lattice-wise (FDE info-join over <:), a bridge rule is a directional, named, typed inference that moves a conclusion from one standpoint to another, optionally applying a domain mapping.

Status. pub bridge is refused at ox check / ox build with OE1102 (audit doc-04 / issue #151). Bridge rules parse, lower to wire events, resolve, and pass well-formedness checks — but the federation fixpoint never fires them, so a built artifact’s bridge bodies would silently never contribute to their target standpoint. Rather than ship that inert surface, a bridge declaration is refused loudly; model the cross-standpoint inference with an explicit derive / pub fact for now. Bridge evaluation is the post-stable flagship standpoint deliverable: the parse / lower / wire / decode surface is retained intact (Module::bridges_targeting, the BridgeDecl codec) so the work resumes without a grammar or wire-format change. The semantics below is the committed design.

bridge-decl ::= attribute* 'pub'? 'bridge' Ident
                  '(' standpoint-ref '->' standpoint-ref ')'
                  '{' bridge-rule (';' bridge-rule)* ';'? '}'
bridge-rule ::= rule-body '=>' bridge-head
bridge-head ::= predicate-call                           // direct assertion into target
             |  predicate-call 'mapping' mapping-clause  // with domain map
mapping-clause ::= '{' (Ident '=' expr (',' …)*)? '}'    // src-var ↦ dst-expr
standpoint-ref ::= path                                  // resolves to a standpoint

pub bridge USCitizens(US::Tax -> International::Legal) {
    Person(p), p.citizenship == "US"
        => LegalEntity(q) mapping { q.jurisdiction = "US", q.person_ref = p };
    Person(p), p.passport != null
        => Verified(p);
}

The -> between standpoint references in the bridge head encodes the direction; existing -> operator (function return arrow) is reused with no new lexer token.

Directionality (key property). A bridge from s₁ to s₂ does not imply a bridge from s₂ to s₁. The asymmetry is what makes bridges different from equality / equivalence axioms; without it, bridge composition would collapse standpoints and destroy their contextual scoping. This is the standard discipline across DFOL (Ghidini-Serafini), DDL / C-OWL (Borgida-Serafini-Bouquet), and MCS (Brewka-Eiter) — see the vault notes on bridge-rule semantics for the comparative landscape.

Body and head. The rule body uses the standard rule-atom grammar (Rule-atom grammar) evaluated at the source standpoint. The head is a predicate call evaluated at the target standpoint. If source and target have different domains (e.g., a tax-jurisdiction Person vs. an international-law LegalEntity), an explicit mapping { … } clause specifies how source variables map to target-domain values; without a mapping clause, the bridge is identity (source variable = target argument).

Negation-as-failure in bridge bodies. Bridge bodies admit NAF (not atom) over the source standpoint’s predicates — matching the MCS form. The bridge graph (nodes = standpoints; edges = bridges) must be stratified for the federation fixpoint to be unique; cycles in the bridge graph emit OE1101 BridgeCycle.

Composition with across [...]. A query annotated across [s₁, s₂] composes lattice federation (via <:) and any bridges between s₁ and s₂ in scope. Both contributions are info-joined via the FDE lattice; conflicts surface as Both per truth values.

Mechanization. The standpoint-frame sheaf semantics (Sheaf-theoretic semantics for standpoint federation) treats bridges as restriction maps on the perspectival sheaf — see that section. Diagnostic codes for malformed bridges live in the OE11xx range (Standpoints / perspectival config).

Bridges under temporal extent (Temporal substrate). When bridges cross modules with bitemporal extent, the substrate admits only temporal-uniform bridges at tier: recursive: a bridge rule consults facts only at the same valid-time at which it fires. Bridges that consult facts at different times (bridge m s t reading s _ t' with $t’ \ne t$) require tier: fol and an explicit temporal-bridge-monotonicity axiom in the module’s prelude. The sheaf-equivalence theorems of Sheaf-theoretic semantics for standpoint federation lift pointwise under temporal-uniform bridges with no new axioms; non-uniform bridges require a new axiom and are out of the conservativity envelope. Diagnostic: OE0720 NonUniformBridgeRefused. Mechanized at spec/lean/Argon/Locality/Temporal.lean (sheaf_equivalence_bitemporal_uniform).

Sheaf-theoretic semantics for standpoint federation

The standpoint lattice carries a sheaf-theoretic semantics — the formal grounding of why across [...] federation, bridge rules (Bridge rules), and box/diamond modal operators all compose coherently.

The sheaf. Treat the standpoint lattice as a base for a Grothendieck topology: open sets are downward-closed subsets of the <: lattice. The perspectival sheaf 𝓕 assigns to each open set U a stalk 𝓕(U) — the local knowledge (set of derivable facts, three-valued atoms, evidence accumulations) available to the standpoints in U. Restriction maps 𝓕(U) → 𝓕(V) for V ⊆ U encode how broader perspectives specialize to narrower ones; explicit bridge rules (Bridge rules) lift to additional restriction maps wherever the bridge graph reaches.

Substrate theorems. The correspondence is proved over a finite model at spec/lean/Argon/Locality/SheafEquivalence.lean — no axioms, no sorry: bottom_up_is_equilibrium, equilibrium_is_global_section, and equilibrium_is_minimal_section. Stated informally: the bottom-up evaluation of the federated standpoint system produces an MCS-style equilibrium, and that equilibrium is a minimal global section of the perspectival sheaf. The full categorical construction — a genuine Grothendieck topology with general restriction maps — is open research (it would unify two independent formalizations of perspectival reasoning; see the vault note “Topology of Understanding”). The finite-model theorems are the substrate commitment.

Consequence (H¹ interpretation). When across [s₁, s₂] yields Both(a, b) (the FDE conflict outcome), the first cohomology H¹(𝓕) carries a non-trivial generator. The two witnesses a, b are cohomologically distinct — they witness an irreducible perspectival disagreement that no global section can unify. This is the formal content behind the #[consistency(paraconsistent)] policy: the substrate makes the disagreement explicit rather than collapsing it.

Consequence (sheaf cohomology as diagnostics). Future tooling may surface H¹(𝓕) generators as a diagnostic class — “your federation disagreement is reducible (cohomologous to zero, fixable by a bridge rule) or irreducible (a non-trivial cohomology generator, requiring paraconsistent acceptance).” This is research-grade; the substrate axioms are the commitment.

Lift under bitemporal extent. When the standpoint federation runs over modules with bitemporal extent (Temporal substrate), the three sheaf-equivalence theorems lift pointwise without new axioms — provided bridges are temporal-uniform (Bridge rules). The bitemporal BeliefAssignment, BridgeEval, and LocalFixpoint become time-indexed functions; at each time slice, the canonical theorem applies. Mechanized at spec/lean/Argon/Locality/Temporal.lean (bottom_up_is_equilibrium_bitemporal, equilibrium_is_global_section_bitemporal, equilibrium_is_minimal_section_bitemporal, bundled as sheaf_equivalence_bitemporal_uniform). Non-uniform bridges (consulting facts at different VTs) require a new temporal-bridge-monotonicity axiom and are out of the conservativity envelope.

Decidability

Tier ladder

Default module tier: structural.

Temporal sub-tier (orthogonal axis). Every program has a tier pair (main, temporal). The temporal sub-tier ladder:

The classifier accepts a program if both axes are tractable and the program respects additive composition between modal (box/diamond) and metric temporal operators — no nesting of one family inside the other. Cross-mixed nesting box(box_minus[a,b](C)) is refused at tier: recursive (OE0712 ModalTemporalCrossNestRefused) and routed to tier: fol. The grounding is Demri-Wałęga 2024 (Standpoint LTL): satisfiability is EXPSPACE-complete unrestricted, with a PSPACE fragment under interplay restriction that Argon’s rigidity-of-standpoints commitment satisfies.

Annotation:

#[dec(tier: recursive, temporal: stratified)]
mod my_module { … }

If only one axis is annotated, the other is inferred from the module’s content.

Mechanized at spec/lean/Argon/Decidability/Temporal.lean (TemporalSubTier lattice + additiveComposition predicate + admitsAt_admits soundness lemma).

Annotations

#[dec(tier:<name>)]
#[budget(heartbeats: Nat)]
#[scope(max: Nat)]
#[brave]                  // stable models (reserved)
#[coinductive]            // greatest fixpoint
#[constructive]           // required at tier 5+ for non-ground NAF
#[shape(<recognized-shape>)]
#[lattice(K3 | FDE | Boolean)]
#[consistency(strict | paraconsistent)]    // on standpoint
#[world(open | closed)]                     // on concept (World assumptions (CWA / OWA); live — marks the concept's world, default CWA)
#[default]                                  // on derive — overridable clause (Defeasibility, RFD 0028)
#[defeats(target(args))]                    // on derive — declares an attack (Defeasibility, RFD 0028)
#[label(name)]                              // on derive — clause identity, head.label (Defeasibility)
#[intrinsic]                                // on iof-body field
#[unproven] / #[assumed]                    // on test
#[language_interface]                       // on Lean-spec-bound items

Theory-specific annotations (e.g., #[order(N)] from the mlt package, #[potency(N)] from a potency package) are library macros in unprivileged theory packages, not language-level attributes — see Higher-order modeling and Stdlib (selected).

Reserved attribute names. The compiler-known attribute names listed above are reserved. A user pub macro <name> { … } or #[procmacro] pub fn <name>(…) declaration whose name collides with the reserved set is rejected at the declaration site with OE0708 ReservedAttributeName. The full reserved set:

brave, budget, coinductive, consistency, constructive, dec, default,
defeasible, defeater, defeats, derive, intrinsic, inverse, label,
language_interface, lattice, managed, no_implicit_prelude, priority,
procmacro, scope, shape, unproven, assumed, world

(defeasible, defeater, priority are removed surfaces — they stay reserved so a typo refuses with a migration hint, RFD 0028 D9 — and default, defeats, label are the replacements.)

This list is fixed; adding to it requires an edition bump (the edition = N field in ox.toml). Theory-specific attribute names (categorizes, partitions, subordinate_to, power_type_of, order, complete, potency, @n, …) live in their own unprivileged theory package (mlt, potency, …) as #[procmacro] / pub macro declarations, not as language-reserved attributes — see Higher-order modeling and Stdlib (selected).

unsafe logic

The only escape to full FOL:

unsafe logic {
    #[scope(max: 10)]
    forall p: Person where exists q: Person where ParentOf(p, q)
}

The body admits the rule-atom grammar of Rule-atom grammar; FOL binding quantifiers (forall x: T where … and exists x: T where …) are accepted without tier-cap rejection. No new connectives or syntax are introduced — only the elaborator’s tier classifier differs. The tier classifier statically routes the block to a backend (native / SMT / ASP / FOL prover) and emits a per-block verdict: TERMINATES, TERMINATES UNDER BOUND (requires #[scope] / #[budget]), or REJECTED.

Higher-order modeling

Multi-level / higher-order theories live in ordinary first-party packages with zero compiler privilege — never in the language core and never in std. The substrate provides the primitives — iof (Reflection), <: (Vocabulary concepts and the generic type metatype), the meta-calculus (Meta-calculus atom), well-founded instantiation, stratified aggregates over the iof DAG (derive) — and theories layer on top. The substrate is deliberately neutral about which higher-order theory a model commits to, so none of them belongs in std (RFD 0043).

The mlt package’s ability to treat iof and specializes as first-class predicates — passing, counting over, and quantifying across type-values — rests on the substrate reflective sort TypeRef (Reflection), whose values are references to declared types; this realizes RP-003 GAP-1. The substrate TypeRef sort is the neutral handle layer and is distinct from any library construct built atop it: it is not an MLT* orderless Type term (whose powertype/order semantics live in that package) nor a vocabulary’s own Type_ concept (an ordinary declared type). TypeRef carries no order, potency, or categorization — those remain the theory packages’ concern.

Higher-order theories ship as unprivileged packages at tier:metaorder (Tier ladder), e.g.:

Each package provides:

• its metaxes (e.g., the mlt package declares pub metaxis order for metatype = Nat where { _ <= 16 }),
• its metarels (e.g., the mlt package declares pub metarel categorizes(higher: type, base: type)),
• the decorator forms as library #[procmacro]s (e.g., #[categorizes(Animal)] re-emits the decorated declaration and emits a re-checked MetaProperty on the categorizes metarel; #[order(2)] does the same on the order metaxis),
• derived level functions over the iof graph,
• check rules enforcing the theory’s axioms (e.g., the mlt package enforces Carvalho-Almeida S1–S5),
• the theory’s constraints as its own rules/checks over the neutral substrate — never compiler-reserved diagnostic codes; the substrate ships no theory-namespaced codes.

Intrinsic-by-default for higher-order types. When the mlt package’s cross-level decorators (#[categorizes], #[partitions], #[subordinate_to], #[power_type_of]) are applied to a type declaration, the type’s fields default to #[intrinsic] — every iof-instance must supply a value (field = value at kind level) or carry a from-navigation source (struct and enum — language built-ins (data declarations)). A field with neither emits OE1908 IntrinsicPropertyMissing against every iof-instance. Modelers opt a field out by declaring it T? (optional, yields None when absent). The field-default opt-out (field: Type = expr) refuses with OE0237 FieldDefaultUnsupported (see struct and enum — language built-ins (data declarations)). Parallel decorators in a potency, ml2, or user theory package may declare their own intrinsic-default rules.

A modeler picks a theory by listing its package in ox.toml and importing it: use mlt::*; brings MLT’s vocabulary into scope; a third-party vocabulary package (e.g. an externally-authored UFO package) may re-export mlt::* plus its own metatypes (kind, role, phase, …) on top.

The std::level::Stratified trait gives consumers a theory-agnostic level handle:

// in std::level
pub trait Stratified {
    type Level;
    fn level(self) -> Self::Level;
}

Each theory implements Stratified for its entities; consumers depend on the trait, not the theory.

See the stdlib reference (Stdlib (selected)) for full package documentation. Decidability tier metaorder (Tier ladder) admits unbounded multi-level / higher-order instantiation; theory packages may surface their own bounded variants (e.g., a package may cap MLT order to lower the module to a polynomial tier).

Prior versions of this specification embedded MLT directly in Higher-order modeling with built-in decorators and OE19xx diagnostic codes. That commitment is superseded; see spec/research/RP-003-mlt-as-library.md for the feasibility study and migration rationale.

Build pipeline and .oxbin

An Argon workspace compiles to one content-addressed file: .oxbin. This chapter is the build contract: what ox build accepts and rejects (ox build is fail-closed), the pipeline that produces the artifact (Pipeline), how a composition gets its cryptographic identity (Composition signature), the artifact’s section model (Section model), versioning (Versioning — four orthogonal axes), content-addressing (Content-addressing), and load-time validation (Load-time validation — two layers). The byte-level wire format is documented in the oxc-oxbin crate (compiler/crates/oxc-oxbin/FORMAT.md); the axiom-ADT body variants the events section carries are catalogued in Axiom-ADT variant catalog.

ox build is fail-closed

A built artifact evaluates every rule it contains, or it does not exist. ox build runs three gates in order; any gate that fails aborts the build and writes no .oxbin. A wrong artifact is worse than no artifact.

1. Parse gate. Elaboration is error-tolerant — it recovers from malformed input by dropping the broken construct. Left unchecked, a parse error would silently produce an .oxbin missing whatever the parser choked on. So ox build first collects every error-severity parse diagnostic; if any exist, it prints them and exits 1 before resolution runs (oxc-driver/src/lib.rs:759).

2. Resolution and type gate. It then runs the full resolve/typecheck pass (collect_check_diagnostics). Any error-severity diagnostic — an unresolved predicate, a type error — aborts the build with no artifact.

3. Un-evaluable-rule oracle gate. The lowering pipeline admits some rule shapes the runtime’s rule compiler then refuses. Such a rule is silently dropped from evaluation, so an artifact containing one returns wrong (under-derived) query answers with no runtime error. To prevent that, ox build loads the elaborated artifact and re-runs the runtime’s own compile_rule as an oracle over every rule (Module::uncompilable_rules). If any rule will not evaluate, the build fails loudly and writes nothing. ox check enforces the same oracle through the driver’s internal validate_runtime_evaluable_rules path, so editor/CI validation cannot green-light a package that ox build later rejects. This intentionally makes ox check do the extra work needed for artifact-parity validation: package elaboration, stdlib loading, comptime lifting, event encoding, and Module::load. Refused shapes:

   Shape	Diagnostic
   Unsafe rule — a head / negated / comparison / compute variable not bound by a positive body atom (range-restriction)	OE1303
   Nested aggregate (count { count { … } > N })	OE1311
   Collection/string aggregate kind (collect/set_collect/string_join/percentile); the folding kinds count/sum/min/max/avg/count_distinct evaluate	OE1312
   not wrapping an aggregate subquery	OE1313
   Empty aggregate body (count { })	OE1314
   Unsupported quantifier shape (exists binder, forall(path, T), under-specified forall)	OE1315

   Rule bodies the semi-naive executor does not compile — a type-test atom or a meta-equality (== on meta(x)) — are recorded the same way and surface as the same load-time refusal (oxc-runtime/src/lib.rs:299).

   The oracle reports executor-capability failures. A hard Module::load failure surfaces through normal artifact load/build diagnostics.

   The fix is always to rephrase the rule into a supported shape — typically by exposing the offending subterm through an intermediate pub derive rule. The supported universal forall v: T where Body, Head (the last where atom is the consequent, the rest the domain) does evaluate; it lowers to a count-equality.

Pipeline

ox build <dir> searches upward from <dir> for the nearest ox.toml and treats that directory as the package (oxc-workspace::find_nearest_package_dir), the same cargo-style discovery ox check and ox lsp use. Module resolution then handles real nested package layouts — pkg::, super::, self:: path roots and pub use re-exports (see Modules and packages; not repeated here).

Output location. Build products never sit next to sources — cargo-style, the artifact is written under a target/ directory: <root>/target/<name>.oxbin, where <root> is the package directory (the one holding ox.toml) and <name> is the resolved entry’s file stem (so a package whose entry is root.ar yields target/root.oxbin). For a standalone .ar file with no enclosing manifest, target/ is created beside the file. target/ is created on demand and is git-ignored. -o/--out overrides the path entirely. The artifact-loading commands (ox query, ox derive, ox run, ox run-scenario, and ox runtime serve --oxbin) accept a package directory or source .ar and resolve the same default target/ location, or an explicit .oxbin path.

The pipeline has a sharp boundary: oxc is the per-package compiler; ox is the workspace orchestrator. Every cross-package concern lives in ox.

per-package source
      ↓ oxc elaborate              ← oxc owns (sync; salsa-cached)
per-package CoreIR
      ↓ oxc instantiate            ← oxc owns; consumes wiring
per-package .oxc cache
      ↓                            ─┐
(workspace metadata + lockfile)     │  ox owns:
      ↓ ox build                    │  • compute wiring diagram
      ↓                             │  • compose standpoint lattice
      ↓                             │  • check tier cap
      ↓                            ─┘  • merge .oxc → .oxbin
workspace .oxbin
      ↓ runtime backend (Runtime contract)
answers / docs / mutations / …

Three artifacts, three typed transitions:

• Source — the .ar surface text plus the per-package manifest.
• .oxc cache — one file per package: the elaborated, instantiated serialization of that package’s contribution relative to this composition. Same section model as Section model, smaller scope.
• .oxbin — the workspace artifact: one file per ox build, content-addressed, consumed by a runtime backend (Runtime contract).

oxc never sees the workspace. It elaborates a single package against a wiring diagram ox supplies; it cannot resolve cross-package references, merge standpoint lattices, check tier consistency across packages, or emit the workspace .oxbin. ox is the only command modelers invoke directly (ox build, ox run, ox query, ox check, ox test, ox doc, ox inspect, ox runtime serve, per reserved keywords); oxc instantiate / oxc emit core-ir / oxc dump are tooling-internal.

Build scope (RFD 0030). ox build produces a single, monolithic .oxbin per invocation covering the entry’s dependency closure: each [dependencies] path dependency’s modules are loaded and folded into the consumer’s workspace (exactly as the embedded stdlib is folded), elaborated into the same event stream, and embedded in the one artifact — so a dependency’s content participates in the artifact’s content hashes (Content-addressing). Cross-package references across a path dependency resolve at build time. The registry/git dependency surface (a bare version requirement, the version/git/branch/tag/rev/registry keys, ox.lock) is out of scope (Out of scope) and refuses with OE1240. The separate per-package .oxc cache and workspace-merge orchestrator below (Composition signature) describe the composition model the registry story realizes.

Composition signature

The wiring diagram is the workspace-level resolution of every cross-package symbol reference — the closed-world view of how packages compose. ox computes it from the package graph and the lockfile.

WiringDiagram :=
    map from (consumer_package, ref_site)
            to (target_package, target_qualified_path, target_stable_id)

The composition signature is the cryptographic identity of one composition:

composition_signature  :=  BLAKE3-256(
    wiring_diagram_hash       ∥   // BLAKE3-256 over the canonical resolved symbol table
    standpoint_lattice_hash   ∥   // BLAKE3-256 over canonical-form composed lattice
    tier_ladder_version       ∥   // u32 LE (preamble, Versioning — four orthogonal axes)
    runtime_contract_version      // u32 LE (preamble, Versioning — four orthogonal axes)
)

The hash is BLAKE3-256 throughout the content-addressing story (RFD 0001 Phase 2 replaced SHA-256). ox build computes wiring_diagram_hash as a BLAKE3 over the canonically-sorted (axiom-kind, content-id) of the structural axiom events — the schema-defining declarations, axioms, and rule-modes — so it is sensitive to a relation/concept rename or a rule change but stable under instance-data churn (asserted facts carry no structural weight); standpoint_lattice_hash is the same construction over the standpoint and bridge declarations.

The wiring diagram source is not preserved in .oxbin — it is a transient build-time input. Only the four sub-hashes survive (wiring_diagram_hash and standpoint_lattice_hash in global-control; the two version u32s in the preamble). ox build checks that the wiring is correct; the runtime re-verifies at load that the stored sub-hashes have not been tampered with. Two semantically equivalent compositions produce byte-equivalent .oxbin files — the central content-addressing invariant (Content-addressing).

Section model

A .oxbin is a preamble followed by a sequence of typed sections. Ten section types are defined — five mandatory, five optional:

Optional and LAZY are independent: optional governs presence in the artifact; LAZY governs whether the runtime mmaps the section on first access rather than reading it in the synchronous load prefix. Section type-ids live in one uint8 namespace — 0..99 standard, 100..199 Argon-future, 200..255 user-custom (unknown custom sections are ignored on load unless MANDATORY-flagged). The section directory in global-control indexes every section; its order is canonical load order. The runtime tolerates a mandatory section that is present but empty. Byte layout of the preamble, per-section sub-headers, and per-section encodings is documented in the oxc-oxbin crate.

Versioning — four orthogonal axes

The preamble carries four independent uint32 version axes, each bumped on its own:

Robustness: producers strict, consumers liberal, per axis.

• A consumer accepts a future minor bump on any axis: load proceeds and unknown additive things degrade gracefully (an unrecognized non-MANDATORY section is skipped).
• A consumer refuses a future major bump on any axis: load fails with OE1202 IncompatibleVersionAxis(axis, want, got).
• A consumer refuses any MANDATORY-flagged section it does not recognize, regardless of axis: OE1203 UnknownMandatorySection(section_type).

Within one oxbin_format_version major, an artifact MAY carry two representations of the same logical content side by side (e.g. a DRedc-shaped projection-cache and a DBSP-shaped arrangement-section); each runtime picks the section it understands.

There is no kernel_api_version axis — the runtime contract is the OxbinRuntime trait (Runtime contract), versioned by runtime_contract_version. A backend’s internal schema version (e.g. the Postgres backend’s migrations, Storage layer) is not carried in the preamble; backends version their own schemas.

Content-addressing

The artifact-level hash is a Merkle root over the composition and the section directory:

artifact_hash  :=  SHA-256(
    composition_signature                ∥   // Composition signature
    section_directory_canonical_form         // deterministic-CBOR section directory
)

Each section additionally carries a content_hash (SHA-256 over its encoded body) when CONTENT_HASHED-flagged. Two semantically equivalent compositions produce byte-equivalent .oxbin files, hence an identical artifact_hash. This holds because every section uses deterministic encoding (RFC 8949 deterministic CBOR for structural sections) plus per-section canonical-form rules (canonicalization is part of the oxc-oxbin format contract). The payoff:

• Distributed caching — re-running ox build on the same inputs is a cache hit on artifact_hash.
• Selective invalidation — a TBox change touches only the events content hash; downstream caches invalidate at section granularity.
• Content-addressed distribution — an .oxbin can be named by its artifact_hash in a CAS/Nix/IPFS-style registry.
• Tamper detection — any byte changed after ox build is caught at load.

Load-time validation — two layers

The runtime contract requires two validation layers.

Layer 1 — closed boolean. Computed once global-control is parsed, before any other section body is read; constant-time per artifact:

tier_valid(.oxbin, runtime)
  := global_control.max_tier_claimed       ≤ runtime.max_tier_supported
   ∧ global_control.max_temporal_claimed   ≤ runtime.max_temporal_supported

max_tier_claimed and max_temporal_claimed reflect the highest tier pair (per Decidability and RP-004) of any rule in the artifact. Failure refuses the artifact with OE1204 TierMismatch(want, got).

Layer 2 — per-section verifier. Run after Layer 1 passes:

Policy is per runtime kind, made explicit at OxbinRuntime::load (Runtime contract):

• Sandboxed runtimes (untrusted content) default strict — any Layer 2 failure refuses the load.
• Trusted runtimes (in-process from a trusted ox build) default lenient — non-load-bearing failures (e.g. OE1215) warn and proceed; symbol-resolution and lattice failures are always fatal.

RP-004 hooks

The bitemporal substrate of RP-004 (Types and refinement, Rule atom — fn, derive, query, mutate, check, Decidability, Standpoints and modal operators) flows through .oxbin natively:

• The events sort key is (tenant_id, fork_id, standpoint_id, predicate, valid_time, tx_time) — bitemporal-native ordering, no Layer-2 rewrite for temporal queries.
• global-control carries both max_tier_claimed and max_temporal_claimed; Layer 1 checks both.
• tier-table rows carry a (main_tier, temporal_tier) pair per rule, mirroring Decidability/Temporal.lean’s classifyPair. Cross-nest violations (OE0712 ModalTemporalCrossNestRefused) are rejected at compose time, before the artifact is emitted.
• pathology-flags includes an “additive-composition violation detected at compose time” flag, distinguishing provably-correct artifacts from trusted-by-compiler ones.

Runtime serving command

ox runtime serve exposes the Runtime contract serving surface around one compiled artifact. It does not compile source — a caller runs ox build first and passes the resulting .oxbin.

ox runtime serve \
  --project . \
  --oxbin target/main.oxbin \
  --host 127.0.0.1 --port 7780 \
  --storage mem

Postgres-backed serving uses the same .oxbin plus a durable ABox event log (--storage pg --database-url "$DATABASE_URL"). Watch-mode compilation, if tooling enables it, is a separate process that rewrites the artifact; the serving process hot-reloads only after the Runtime contract compatibility checks pass.

Mechanization

The wire shape, validation predicates, composition_signature, and four-axis versioning are mechanized in spec/lean/Argon/BuildArtifact/: Section.lean (section type + flags, @[language_interface]), Header.lean (preamble + version axes), Oxbin.lean (the Oxbin record + section invariants), ContentHash.lean (Merkle-of-sections), Validation.lean (Layer 1 + Layer 2 predicates), CompositionSignature.lean, and Versioning.lean (four-axis robustness). The Rust crate oxc-protocol::oxbin mirrors the @[language_interface]-tagged inductives; CI fails on drift.

Editor extensions — oxup extension

The Argon editor integration is installed and kept in sync by the toolchain manager (oxup), not by hand. oxup extension (alias ext) manages it, abstracted over editors (RFD 0032).

oxup extension install   [--editor <vscode|cursor|codium|code-insiders|code-server|neovim|vim|emacs>] [--archive <path.vsix>]
oxup extension uninstall [--editor <name>]
oxup extension list

install (no --editor) auto-detects every installed VS Code-family editor (by its CLI on PATH) and installs the extension matching the active toolchain version into each. The version coupling is real: the published .vsix is stamped with the toolchain version and addressed at an immutable CDN path, https://argon.sharpe-dev.com/editors/vscode/<version>/argon-<version>.vsix. oxup resolves the active toolchain’s concrete version (from its manifest.toml), fetches that .vsix, sha256-verifies it against the published sidecar (the same fail-closed discipline as the toolchain fetch), and hands it to the editor CLI’s --install-extension. --archive <path.vsix> installs a local .vsix offline instead of fetching.

oxup init (non-minimal) and oxup update auto-install / refresh the extension after the toolchain is placed; oxup init --no-extension skips it, and update re-installs only when the toolchain version changed (the installed version is recorded in settings.toml). A failed extension install is a soft failure — the toolchain is what matters — and “no editor detected” is a quiet one-line note, not an error.

Editor support matrix

Two install mechanisms, by the contract the editor exposes. The user-facing detail — the language-server capability set, and the file-placement managed-config block — is in Toolchain → Editor support.

Neovim, Vim, and Emacs are recognized — naming one with --editor produces a specific, loud refusal pointing at manual setup and the tracking issue, never a silent no-op.

Runtime contract

A .oxbin is consumed by a runtime backend. The runtime contract defines what a backend promises: how to load an artifact, how to bind it to per-tenant state, how to answer queries against bitemporal data, how to apply mutations, and how to enforce the capability surface that gates compliance-sensitive operations.

The contract specifies a three-role factoring (Engine / Module / Store factoring), a trait surface (The OxbinRuntime trait surface), a lifecycle (Lifecycle), bitemporal AsOf semantics (AsOf semantics — bitemporal point), a capability surface (Capability surface), and the ox runtime serve HTTP surface (Serving surface).

Engine / Module / Store factoring

The runtime decomposes into three roles:

• Engine is the shared, immutable base — the shared schema (std + any base packages the workspace declared — including any vocabulary packages — plus the meta-axes those packages declared). The Engine is Arc<SchemaStore>, mmap-friendly, and shareable across processes and threads.
• Module is a typed, loaded .oxbin. It owns the artifact’s structural content (symbol table, standpoint lattice, tier table, rules, queries, mutations) and is immutable for its lifetime. Many Stores may use one Module concurrently.
• Store is the isolated execution context where facts live. One Store is one (tenant, fork) pair: it accumulates events through mutate and answers query.

A Store sees facts according to two filters: (1) tenant + fork scope — only events tagged with this Store’s tenant_id and fork_id, under the fork’s copy-on-write lineage rules (AsOf semantics — bitemporal point); (2) standpoint perspective — when a query names a standpoint, only events visible from that standpoint by the lattice ancestor relation.

The OxbinRuntime trait surface

A backend implements:

#![allow(unused)]
fn main() {
pub trait OxbinRuntime: Send + Sync {
    type Module: 'static + Send + Sync;
    type Store: 'static + Send + Sync;
    type Error: std::error::Error + Send + Sync;

    /// Load an .oxbin into a Module. Layer 1 validation runs synchronously
    /// here (RP-004 hooks); Layer 2 runs in the prefix before this returns Ok.
    fn load(
        &self,
        oxbin: &Oxbin,
        validation: ValidationPolicy,
    ) -> Result<Self::Module, Self::Error>;

    /// Open a Store for one (tenant, fork). May create the fork if it
    /// doesn't exist (subject to capability checks per the backend's IAM).
    fn open_store(
        &self,
        module: &Self::Module,
        tenant_id: TenantId,
        fork_id: ForkId,
    ) -> Result<Self::Store, Self::Error>;

    /// Run a query at a bitemporal point (default `AsOf::Now`). Standpoint
    /// scope is part of the query, not this argument.
    fn query(
        &self,
        module: &Self::Module,
        store: &Self::Store,
        query: &CoreIRQuery,
        as_of: AsOf,
    ) -> Result<Answer, Self::Error>;

    /// Apply a mutation; returns the TT at which it became effective.
    /// Mutations are transactional; partial mutations are not observable.
    fn mutate(
        &self,
        module: &Self::Module,
        store: &mut Self::Store,
        mutation: &CoreIRMutation,
    ) -> Result<TxTime, Self::Error>;

    /// Fork an existing (tenant, fork) at a given TT. The new fork inherits
    /// parent state up to fork_point_tt; later mutations diverge (CoW, `AsOf` semantics — bitemporal point).
    fn fork(
        &self,
        module: &Self::Module,
        parent: &Self::Store,
        new_fork_name: &str,
        fork_point_tt: TxTime,
    ) -> Result<Self::Store, Self::Error>;

    /// Capability-gated physical erasure (Capability surface). Requires both
    /// `#[allow_forget]` on the target concept and the runtime principal
    /// to hold the `forget` capability.
    fn forget(
        &self,
        module: &Self::Module,
        store: &mut Self::Store,
        targets: &[AxiomId],
        actor: PrincipalId,
        reason: &str,
    ) -> Result<ForgetReceipt, Self::Error>;
}
}

The trait is Send + Sync; a backend’s concurrency discipline is its own concern. The ValidationPolicy argument to load distinguishes sandboxed Strict (any Layer-2 failure refuses the load) from trusted Lenient (Layer-2 failures emit warnings; non-load-bearing issues are tolerated).

AsOf, Capability, and ValidationPolicy are @[language_interface] types mirrored by oxc-protocol::runtime; CI fails on drift.

Lifecycle

A normal lifecycle: at startup, runtime.load(oxbin, policy) returns a Module (Layer 1 tier check synchronously, Layer 2 per-section invariants in the prefix); per request, open_store then query / mutate; at shutdown, Stores drop, then the Module, then the Engine.

A second load returns a new Module. The runtime MAY share the first Module’s Engine if the base schemas are byte-identical (Arc identity), otherwise the new Module gets a fresh Engine. Hot replacement of a live Module is not required by the in-process trait; the serving helper (Serving surface) implements a guarded form that loads the next Module, checks compatibility against live ABox state, and swaps atomically only if compatible. The Engine/Module split is what makes this possible without redesigning Store semantics.

AsOf semantics — bitemporal point

Every query reads facts at a specific bitemporal point. The AsOf type carries both axes:

#![allow(unused)]
fn main() {
pub enum AsOf {
    /// Default: VT = now, TT = now — "what is currently true, as currently believed."
    Now,
    /// "What was valid at VT = t, as currently believed?" Historical-fact view.
    AtVt(DateTime),
    /// "What was believed at TT = t about VT = now?" Audit view.
    AtTt(DateTime),
    /// Full bitemporal: "what was believed at TT = tt about VT = vt?"
    At { vt: DateTime, tt: DateTime },
}
}

The default AsOf::Now answers about current state; historical and audit queries are opt-in.

Forks interact with AsOf through the copy-on-write invariant. A child fork inherits parent state up to fork_point_tt. A query against the child at AsOf::AtTt(tt): if tt < fork_point_tt it reads the parent’s events at tt; if tt ≥ fork_point_tt it reads the parent’s pre-fork events plus the child’s own events up to tt. The parent’s pre-fork state is shared with all children; each child sees its own divergence. A backend MAY materialize the inheritance at fork-creation or compute it lazily on read; both satisfy the contract.

Capability surface

Three capabilities gate dangerous operations:

• forget — physical erasure of axiom events for compliance (RP-004 Temporal substrate). The source-level gate: a mutate body containing forget refuses to build (OE0730) unless the enclosing mutate declaration grants #[allow_forget]. The serving layer refuses forget outright (Runtime contract limits below).
• unsafe_logic — execution of tier:fol rules under unsafe logic { }. Granted to the workspace at ox build time. A query whose dependency closure touches an unsafe_logic rule may run unbounded; runtimes MAY apply a per-query wall-clock timeout and return OE1301 UnsafeLogicTimeout.
• fork — creating new forks, per-(tenant, parent_fork). A principal without it can open_store against existing forks but cannot create new ones. The trunk fork’s owner holds fork automatically.

Capabilities flow through the runtime as part of the PrincipalId argument to forget and the principal context of open_store. How a runtime authenticates a principal is backend-specific (the Postgres backend uses Postgres roles; the in-memory backend trusts the calling process).

Incremental evaluation

The runtime commits to incremental (Salsa-style) computation at two layers. A compile-time layer, keyed on the immutable .oxbin, memoizes Module-only work (parse / resolve / type-check / classify-tier / compile-rule) once per loaded Module and shares it across Stores. A runtime layer, one per (tenant, fork), memoizes every query whose dependency set touches the event log (extent, iof closure, rule fixpoint); a mutate bumps a per-Store generation counter and the engine invalidates exactly the downstream queries.

The load-bearing invariant: for any tracked query, the same (module, store generation, query args) yields the same result. The backend MUST guarantee the generation bump after a successful mutate is atomic and monotonic — no thread observes the increment before the mutation is durable (for Postgres, the bump is in the same transaction as the event insert; for in-memory, a write-lock spans the index update and the increment). Per-(tenant, fork) keying — not per-tenant — is what keeps a mutation on fork A from invalidating warm queries on fork B.

Serving surface

The in-process trait is the semantic contract. ox runtime serve is the first-party helper around it for tools that need a process boundary, specified by RFD-0014. It exposes a versioned HTTP surface:

Dispatch routes take a runtime context from trusted headers (X-Tenant-Id, X-Fork-Id, X-Principal-Id, X-Request-Id, X-Standpoint) or the request body; headers win when both are present. Missing tenant defaults are a CLI/helper concern; missing fork defaults to main.

Storage modes. mem keeps Store state in process memory — useful for local experiments, tests, and short-lived sandboxes; durability ends with the process. It is the default runtime backend. pg is an append-only axiom event log in Postgres (oxc-storage-pg): scoped tenant/fork/standpoint/module scans, AsOf::Now/AtVt/AtTt/full-bitemporal reads, durable fork records and lineage, generation counters bumped atomically with appends, projection-cache invalidation in the same transaction, and decoded body-field lookups for iof assertions and relation tuples. ox runtime serve --storage pg selects it. The source of truth in either mode is the event log; snapshots, derived facts, and projection caches are recomputable views over .oxbin plus visible events.

Ad-hoc query/mutation submission (RFD 0033). Beyond declared-descriptor dispatch, the API accepts arbitrary query/mutation bodies as source text — POST /v1/query/adhoc and POST /v1/mutation/adhoc (plus the per-fork analogs). A submitted body is parsed, fully type-checked against the loaded module (the same checker the build runs, via the runtime Schema backend — an ill-typed body is refused with ARGON_RUNTIME_ADHOC_TYPE_ERROR and never executes), lowered, and run through the same path declared pub query/pub mutate use; the declared forms are a named convenience layer over this generic path. Ad-hoc invocation carries the same context/tenant/fork/standpoint scoping as declared dispatch — there is no ad-hoc-specific restriction on what it may read or write, with one capability exception: forget (physical erasure) requires the build-time #[allow_forget] grant, which a runtime-submitted body cannot self-confer, so an ad-hoc forget is refused (OE0730). Ad-hoc submission is on by default; a deployment may lock down to declared invocables only (--no-adhoc / --no-adhoc-mutation), in which case the endpoint returns ARGON_RUNTIME_ADHOC_DISABLED.

Generic entity writes remain declaration-typed. There is no untyped entity-write surface (no POST /v1/entities): every write — declared or ad-hoc — routes through the typed pub mutate / Operation mechanism, never a raw entity blob. Compute dispatch supports the pure CoreIR subset evaluable without Store effects (literals, parameters, tuples, lists, boolean/int/text operators, membership, conditionals, ascription); calls, projections, and Store-dependent terms are refused until their runtime substrate is specified.

Entity-reference arguments — new vs existing. A pub mutate parameter typed as a declared concept/struct is an entity reference. Over HTTP such an argument takes a JSON string in one of two forms, and the form the client chooses decides the meaning:

• An #i<N> string (e.g. "#i7") names an existing individual — one already minted in this scope (typically returned by an earlier dispatch). It is validated against the store’s next-fresh floor: a reference at or above the floor cannot name an existing individual and is refused (ARGON_RUNTIME_VALIDATION_FAILED).
• Any other string (e.g. "alice") is a client-supplied symbolic name for a NEW individual. The server mints a fresh #i<N> identity for it inside the per-scope critical section, runs the mutation with that identity substituted, and returns the mapping on the receipt under mintedEntities: an array of { "name", "id", "concept" } records. The client uses the returned id to refer to that individual on subsequent dispatches.

This is what makes the flagship models writable over HTTP: a mutation such as openRentObligation(landlord: Person, tenant: Person, …) whose body classifies its parameters via insert iof(landlord, Person) is dispatched by supplying symbolic names ("alice", "bob"), and a later recordPayment(satisfactionAccount: SatisfactionAccount, payment: SatisfactionRecord, …) supplies the minted #i<N> for the existing account and a fresh symbolic name for the new payment. The in-process / demo.toml path mints symbolic names deterministically from the name (so the same name is the same individual); the HTTP path mints fresh per request with no idempotency-by-name — the same name in two requests is two individuals.

Atomic batches. POST /v1/batch executes an ordered array of mutation dispatches as one unit: { "context": …, "mutations": [ { "qualifiedPath", "args" }, … ] }. Every step runs in one per-scope critical section against a single hydrated store, so step N sees the effects of steps 0..N and the check delta-guard evaluates each step against the accumulating state. On success the union of emitted events is persisted in one transaction; the response carries committed: true, a per-step steps array (each with its result / mintedEntities / diagnostics), and eventsCommitted. Any step failure rolls the whole batch back — nothing is persisted — and the error envelope reports the failing step under error.details.batchStep. The request body cap and the result-row cap apply to the batch as a whole. New-entity symbolic-name minting is per step: a symbolic name repeated across two steps mints two individuals (each step is a distinct mutation). To thread one new individual through several steps, mint it in the first step and reference the returned #i<N> in the later ones.

Named individuals in outputs. Individuals declared by pub fact carry their source name into the artifact’s name-index, and every entity rendered by a query / extent / snapshot / dispatch result includes that name under $name alongside the opaque $id (so a served scope reads with its modeler-chosen names). HTTP-minted individuals (above) carry their client label out on the dispatch receipt’s mintedEntities; the durable identity is always the #i<N> id.

Runtime error codes. Failures on the /v1 surface use a stable error.code string in the ARGON_RUNTIME_* family (distinct from the compile-time OE#### catalog of Appendix C). Every 4xx/5xx response uses the same structured envelope — {error:{code,message,details},requestId,moduleHash} — including routing, method, and request-body parse failures (a malformed JSON body is ARGON_RUNTIME_VALIDATION_FAILED, an unknown route is ARGON_RUNTIME_UNKNOWN_ROUTE, a wrong method is ARGON_RUNTIME_METHOD_NOT_ALLOWED), so a client keys on error.code uniformly for every failure class. The full set of codes, their HTTP statuses, and their meanings is the published failure reference in Appendix E, checked against the runtime’s canonical registry. A batch-step failure rides the same envelope with the failing step index under error.details.batchStep.

Pagination. A list-shaped read (pub query, /v1/snapshot) larger than the result-row cap is read page by page rather than refused. A query takes an optional page: { limit, cursor } in its request body; /v1/snapshot takes ?limit=&cursor=. The response carries a page object — { total, returned, nextCursor } (the snapshot’s under abox.page) — and a nextCursor of null marks the last page. The cursor is an opaque server-issued token: pass back the previous page’s nextCursor verbatim, do not parse or construct it (a foreign cursor is refused with ARGON_RUNTIME_INVALID_CURSOR). Page size is min(limit, cap), so one page never exceeds the cap; an un-paged read still refuses (ARGON_RUNTIME_RESULT_TOO_LARGE) when the whole result is over the cap — a truncated answer is indistinguishable from a complete one.

The cursor pins a read point, so a multi-page walk is consistent against one fixed view rather than re-evaluated against live state each page. Page 1 reads at the request’s asOf (or Now); the server resolves Now to the transaction time of the store that served the page and embeds it in the nextCursor. Every later page inherits that pinned point from the cursor (it overrides the request’s asOf), so the offset is always taken against the same bitemporal snapshot. A concurrent insert lands past the pinned point and stays invisible to the walk; a concurrent retraction before the cursor stays visible (it existed at the pinned point) — so the walk neither skips nor duplicates a row, and total is stable across pages. To page over a historical point, pass asOf (the bitemporal read point of AsOf semantics — bitemporal point) on the first request; the whole walk then follows it.

/v1/snapshot carries the same pin in its cursor. On the durable pg backend the pinned page re-hydrates the ABox at the pinned transaction time, so the snapshot walk is consistent under concurrent writes. The in-process mem backend keeps only current-state events (it has no historical scan), so a mem snapshot walk is a live positional read; production serving is pg-backed.

Checks surface. GET /v1/checks enumerates the checks currently violated in a scope, evaluated against live state — the compliance/violations view, complementing the per-mutation observe channel (which only fires on a write). The response carries violated (any blocking Error firing), violationCount, diagnosticCount, and a diagnostics array of {code,message,severity,check,args} (the same shape a mutation response’s observe-channel diagnostics use). ?check=<name> filters to one check (an unknown name is ARGON_RUNTIME_UNKNOWN_CHECK). The generated SDK exposes this as client.checks(), and the mutation receipt now carries the observe-channel diagnostics (previously dropped for typed-SDK consumers).

Liveness and readiness. GET /healthz is liveness — 200 while the process is up and serving; it deliberately does not probe storage, so a transient storage outage does not trigger a process restart. GET /readyz is readiness — it probes the storage backend (SELECT 1 on pg; always ready on mem) and returns 503 ARGON_RUNTIME_STORAGE_UNREACHABLE when storage is down, so a load balancer stops routing to a dead-storage instance. GET /v1/health folds both into one human/debug body and is honest about storage: ok:false + 503 when the backend is unreachable. See the deployment runbook for how an orchestrator should wire these.

Hot reload. The serving layer may watch the active .oxbin path. On a changed artifact it loads the new bytes into a fresh Module, validates, computes the new module hash and declaration signatures, probes live ABox state, accepts additive schema changes, and rejects declaration removal or changed signatures when live ABox state exists — keeping the previous Module active and recording diagnostics on failure. Failed reloads never discard ABox state.

Capability and provenance limits. The serving layer enforces fork on nested forks. forget mutations are refused at the serving layer; unsafe_logic queries are refused (lowering emits unsafe_logic = false for supported rules). The derive/explain endpoints expose buffered rule/tuple provenance only; full PosBool DNF witness trees are reserved for the formal provenance substrate and must not be implied by the response shape.

Defaults

Runtimes default several axes — these live in the ox CLI driver and library helpers, not in the runtime trait: tenant → a singleton UUID (multi-tenant configs override); fork → trunk at tenant creation; standpoint → tenant-wide :root; AsOf → Now; ValidationPolicy → Lenient for ox run, Strict for sandboxed contexts.

SDK generation

ox gen emits a typed client SDK from a built .oxbin so application code calls declared pub query / pub mutate / pub fn descriptors with checked argument and result types instead of hand-writing HTTP requests against the /v1 surface.

Mechanization

The runtime contract is mechanized in Lean as abstract signatures (parallel to std::kripke’s interface-only mechanization): Engine/Module/Store types, the OxbinRuntime trait surface, the bitemporal AsOf type, the three-capability surface, and the generation-monotonicity / cache-correctness invariant, under Argon/Runtime/. oxc-protocol::runtime mirrors the @[language_interface]-tagged types; CI fails on drift.

Deployment and trust model

The server has no authentication. ox runtime serve consumes X-Tenant-Id / X-Principal-Id (and the other context headers) at face value — it does not verify who the caller is or whether they may act as the named tenant or principal. Tenant data is isolated at the storage layer (one tenant cannot read another’s individuals, verified), but the gate deciding who may claim a tenant is absent by design. A caller that sets X-Tenant-Id: acme reads and writes acme’s data regardless of any Authorization header.

This is an honest internal-service posture, not a bug — but it has a hard deployment consequence: the server MUST be fronted by a gateway and MUST NOT be directly reachable by untrusted clients. The default loopback-only bind (serve refuses a non-loopback host) enforces “behind a proxy on the same host or network namespace”; do not relax it without a fronting gateway.

The deployment contract:

1. Front it with an authenticating gateway. A reverse proxy / API gateway terminates client auth (mTLS, OIDC, an API-key service — backend-specific), and only after authenticating injects the trusted X-Tenant-Id / X-Principal-Id headers. The runtime trusts these because the gateway is the only thing that can reach it.
2. Strip inbound trust headers at the edge. The gateway MUST overwrite (not pass through) X-Tenant-Id / X-Principal-Id / X-Standpoint from the client request, so a client cannot forge a tenant. Treat these as gateway-internal headers.
3. Network-isolate the runtime. Bind loopback (the default) or a private interface, and use network policy / security groups so only the gateway can open a connection. The runtime has no rate limiting or load-shedding beyond the per-request timeout, body-size cap, and result-row cap (Serving surface) — the gateway owns rate limiting and client back-pressure.
4. Wire liveness/readiness to the orchestrator. Point the orchestrator’s liveness probe at GET /healthz (restart on failure) and its readiness probe at GET /readyz (remove from the load-balancer pool on failure — e.g. when Postgres is unreachable). Do not gate liveness on storage: a storage outage should drain traffic (readiness), not restart pods (liveness).
5. Schema-change gate. Cross-version artifact loads over live data refuse by default (ARGON_RUNTIME_SCHEMA_MISMATCH, R-B7); an operator opts into serving a changed schema over an existing scope with ARGON_ACCEPT_SCHEMA_CHANGE=1. Treat that as a deliberate migration step, not a default.

forget (physical erasure) is refused outright over HTTP and there is no per-principal authorization inside the runtime (Capability surface, Serving surface) — all authorization is the gateway’s responsibility.

Embedding contract (in-process)

oxc-runtime and oxc-serve are publish = false: there is no crates.io artifact, no semver guarantee, and no docs.rs. Embedding the runtime in-process from Rust means a git dependency on the workspace against APIs that are documented at intent level (the crates’ AGENTS.md nodes) but are not a stable, versioned contract. The semantic contract is the OxbinRuntime trait (The OxbinRuntime trait surface); the serving surface (Serving surface) is the supported boundary for everyone else. Prefer the HTTP surface unless you specifically need in-process embedding.

The in-process Store is the mem backend: durable Postgres serving is reached through the served async adapter (PgOxbinRuntime), via ox runtime serve --storage pg, not by constructing a Store and selecting pg. The HTTP serving surface (Serving surface) sits above the in-process surface — it uses the served pg adapter rather than in-process Store pg — so an integration over HTTP is the lower-risk path.

Storage layer

Argon’s storage layer is a trait abstraction (The storage trait) with two backends behind it: an in-memory backend for tests and REPL, and a Postgres backend. Both implement the same trait so the rest of the runtime is backend-agnostic.

The architectural decision that frames every other choice is the rejection of triple-decomposition: storage is a single append-only log of axiom-ADT events, not entity-attribute-value triples (The single-event-log architecture). The single log carries every cross-cutting concern — discriminator axes, bitemporality, defeasibility, provenance, capability gates — once, instead of per-relation.

The contract is ontology-neutral. No UFO axis is a column. Rigidity, sortality, identity-provision, and any vocabulary-specific axis live as meta_property events whose body declares (axis, target, value). A UFO vocabulary package ships its axes as data, not as type-system primitives.

The single-event-log architecture

Storage is one canonical relation: axiom_events. Every kernel write — concept declaration, subsumption axiom, relation declaration, rule declaration, type assertion, relation tuple, property assertion, meta-property, standpoint declaration, module declaration, retraction — inserts exactly one row. Rows are never updated in place except for the transaction-time-end field on supersession. Rows are deleted only via the capability-gated forget operation (Capability surface).

Each row carries:

1. Identity — a UUIDv7 event identifier (time-orderable, monotonic) and a stable axiom_id UUID identifying the logical axiom across edits.
2. The axiom-ADT body — a variant tag (one of the 26 axiom kinds catalogued in Axiom-ADT variant catalog) plus a canonical-CBOR payload mirroring Argon’s CoreIR 1:1. The content_id is SHA-256(body), so identical bodies deduplicate.
3. Discriminator axes — tenant, fork, standpoint, module. Always present; default singletons in single-tenant deployments.
4. Bitemporality — a valid-time range and transaction-time begin/end (Temporal substrate, RP-004).
5. Polarity — assert (+) or retract (-); retractions point at the assert they supersede.
6. Decidability classification — the tier-pair (main_tier, temporal_tier) per Tier ladder and RP-004.
7. Defeasibility proof tags — Governatori-Rotolo 4-slot tags per defeasible reasoning.
8. Provenance — PosBool(M) DNF for derived events (absent for axioms).

The four discriminator axes plus the bitemporal pair give the 4-axis versioning contract: any event is located by (tenant, fork, standpoint, module) in space and by (valid-time, transaction-time) in time. A query at an AsOf point (AsOf semantics — bitemporal point) reads the events live in scope at that bitemporal coordinate.

Why one log, not many tables. A split design (mutable normalized TBox tables plus an append-only ABox log) cannot answer “what was the TBox as of TT₀” without rebuilding state from a separate ledger, and forces every discriminator axis to be added redundantly to every TBox table. A unified log factors these axes once. Event sourcing is the correct foundation for bitemporal retraction, copy-on-write forking, and PosBool(M) derivation provenance; any of these over a mutable schema introduces impedance mismatches that surface as edge-case correctness bugs.

Why ADT-shaped bodies, not RDF-style decomposition. Reifying an axiom into triples loses the ADT pattern-matching benefit, inflates row count 5–50×, and adds a join layer on every read. The empirical case is clear: horned-owl (Phillip Lord, Newcastle) achieves 1–2 orders of magnitude faster parsing and ~20× less memory than the OWL API’s triple store by using Rust enums for OWL axioms; Konclude and Tawny-OWL converge on the same shape. Pattern matching on the ADT is reasoning in the matching-logic sense (Roșu 2017, LMCS).

The body encoding is canonical CBOR (deterministic per RFC 8949 §4.2.1). The body schema is the variant’s body shape from the axiom-ADT variant catalog.

The storage trait

Backends implement:

pub trait StorageBackend: Send + Sync {
    type Error: std::error::Error + Send + Sync;

    /// Open or create storage for a (tenant, fork). Includes any
    /// per-backend schema migrations.
    fn open(
        &mut self,
        tenant_id: TenantId,
        fork_id: ForkId,
    ) -> Result<(), Self::Error>;

    /// Append one axiom event (assert or retract).
    fn append(&mut self, event: &AxiomEvent) -> Result<TxTime, Self::Error>;

    /// Append a batch of axiom events as one transaction.
    fn append_batch(
        &mut self,
        events: &[AxiomEvent],
    ) -> Result<TxTime, Self::Error>;

    /// Physically erase axiom events for compliance. Capability checked
    /// by the caller; the backend logs to its forget log.
    fn forget(
        &mut self,
        targets: &[AxiomId],
        actor: PrincipalId,
        reason: &str,
    ) -> Result<ForgetReceipt, Self::Error>;

    /// Scan live events of a kind in scope at a bitemporal point.
    /// Returns events with op='+' and (tx_to absent OR tx_to > as_of.tt).
    fn scan_live(
        &self,
        scope: Scope,
        kind: AxiomKind,
        as_of: AsOf,
    ) -> Result<EventCursor<'_>, Self::Error>;

    /// Lookup events by extracted body field. Backends with the right
    /// index serve this in O(log n); others fall back to scan.
    fn lookup_by_field(
        &self,
        scope: Scope,
        kind: AxiomKind,
        field: BodyField,
        value: BodyValue,
        as_of: AsOf,
    ) -> Result<EventCursor<'_>, Self::Error>;

    /// Per-axiom-id history (across retractions / reasserts).
    fn axiom_history(
        &self,
        scope: Scope,
        axiom_id: AxiomId,
    ) -> Result<EventCursor<'_>, Self::Error>;

    /// Apply CQRS projection maintenance after a batch of appends.
    fn maintain_projections(
        &mut self,
        delta: &EventDelta,
    ) -> Result<(), Self::Error>;
}

Scope carries (tenant_id, fork_id, standpoint_id_set, module_id_set). The standpoint_id_set is typically a single standpoint plus its lattice ancestors (pre-computed at compose time, cached in global-control).

Backends manage their own schema versioning. The schema version is not carried in the .oxbin preamble.

The Postgres backend

The Postgres backend (oxc-storage-pg) materializes the event log as a single canonical axiom_events table plus a set of CQRS projection tables (modules, concepts, relations, meta-axes, standpoints and their ancestry, per-(standpoint, concept) world assumption, forks, and a forget-audit log). The event log is the source of truth; projections are recomputable views maintained incrementally by the Argon runtime calling maintain_projections after each batch (so projection logic stays in Rust and is shared with the in-memory backend) rather than by DB triggers.

Body fields are extracted into DB-enforced generated columns (STORED GENERATED ALWAYS AS) via an oxc-pgx pgrx extension that reads canonical CBOR; because deterministic CBOR is byte-deterministic, these extractions cannot drift from the body. Hot-path access patterns — live-in-scope-by-kind, axiom-id history, valid-time and transaction-time ranges, and per-variant / per-relation hot fields — are served by partial, GiST, and BRIN indexes that ox build auto-generates from the declared schema; modelers never write storage indexes by hand.

The concrete Postgres DDL — table definitions, index definitions, the cbor_extract_* extension signatures, and the projection catalog — is an operational artifact of this one backend, not part of the language surface. It is not mechanized (see Mechanization) and lives in the oxc-storage-pg crate. ox kernel init installs the extension and runs migrations.

The Postgres backend crate exists but is not the default runtime path; the in-memory backend is what the runtime exercises by default (see Serving surface).

The in-memory backend

The in-memory backend (oxc-storage-mem) is the live backend — for tests, REPL, and ephemeral runtimes. It implements StorageBackend with BTreeMap-backed indexes plus an interval tree for O(log n) bitemporal range queries, sharing all query and mutation code with the Postgres backend. It is the default for cargo nextest run -j 4 (tests need no Postgres). It has no durability (drops on shutdown), no IAM (trusts the calling process; capability checks pass unconditionally), and no partitioning.

Mechanization

The storage layer is mechanized in Lean at the contract level — abstract over backend, ontology-neutral, axiom-ADT-shaped:

• Argon/Storage/Trait.lean — abstract StorageBackend signature (no DDL)
• Argon/Storage/AxiomEvent.lean — the canonical event row shape (@[language_interface])
• Argon/Storage/AxiomKind.lean — the 26 variants as a Lean inductive (@[language_interface])
• Argon/Storage/AxiomBody.lean — per-variant body payloads (@[language_interface])
• Argon/Storage/CatalogProjections.lean — projection shapes

oxc-protocol::storage mirrors the @[language_interface]-tagged inductives; CI fails on drift. The Postgres DDL is not mechanized — it is an operational artifact of the Postgres backend. The trait admits future backends (analytical / RDF-bridge / property-graph / object-store) without changing the canonical axiom_events abstraction; none are standard backends, and none would change the event-log contract above.

Stdlib (selected)

Standard packages

The standard library is five packages. The compiler embeds each one’s root.ar via include_str! (oxc-instantiate/src/lower.rs) and elaborates it before every user build, so use std::… resolves to real declarations.

Higher-order type theories are not in std. MLT ships as the unprivileged first-party package mlt (packages/mlt, RFD 0043): its own metarels (categorizes, partitions, is_subordinate_to, power_type_of), the order metaxis, and the decorator #[procmacro]s, with zero compiler privilege — a consumer lists it in ox.toml and imports the vocabulary. Parallel theories (potency, ML2, …) ship the same way; the substrate stays neutral about which one a model commits to.

Per-package worked programs live in examples/, compiled and run in CI.

Note std::math is not a package. The numeric and temporal types (Nat, Int, Real, Decimal, Money, Date, …) are compiler-injected primordials resolved directly by the resolver, not imported from .ar source. The fixed-width primitives (i8–i128, u8–u128, f32, f64) are likewise compiler-provided under the std::math::primitive name, requiring explicit use.

Primordial types (lexically always in scope, no use required):

Nat, Int, Real, Decimal, Money, Date, Time, DateTime, Duration,
Bool, String, Top, Bot

These match how ontologists think — counts, measurements, monetary amounts — rather than machine-level widths. Fixed-width variants (i8–i128, u8–u128, f32, f64) ship in std::math::primitive for FFI, performance-critical paths, and binary-protocol interop; explicit use required.

The prelude is a package feature, not a compiler default (RFD 0038). There is no auto-imported std::prelude; a package’s [package].prelude (ox.toml, an array of use-tails) auto-prepends uses to its own modules, empty by default, opt-out per-module with #![no_implicit_prelude]. What is always in scope without any use is the substrate — the language primitives, not a library:

• Primordial types (above) and builtin type forms: Option<T> (Some/None), Result<T, E> (Ok/Err), Ordering (Less/Equal/Greater), Truth4, Truth4Of<T>, List<T>, Set<T>, Map<K, V>, Range<T>, plus the check surface Diagnostic / Severity. These are compiler-provided (is_builtin_type_form) and resolve directly — in scope everywhere, no import, no prelude.

type/rel are not ambient. Opt into the no-commitment baseline with use std::core::{type, rel} or a [package].prelude entry (RFD 0038) — exactly as you bring in any vocabulary. Every ontological commitment is visible in the source: vocabulary classifiers (UFO’s kind, BFO’s class, …) and the baseline type/rel alike resolve only against pub metatype / pub metarel declarations in scope — declared in the package or imported from an external vocabulary package (Name resolution, Vocabulary concepts and the generic type metatype); an unresolved introducer is OE0605 / OE0606. No vocabulary — not even the baseline — ships ambient. A vocabulary package may re-export std::core::rel (and/or type) in its own prelude.ar as a convenience.

Numeric tower and coercion

Modeling-surface numeric types (primordial, always in scope):

All numeric primitives are signed where signedness is meaningful. The runtime chooses an implementation width based on refinement bounds: Int where _ < 256 may compile to i16; unbounded Int defaults to arbitrary-precision.

Fixed-width primitives (std::math::primitive, requires explicit use):

i8, i16, i32, i64, i128, u8, u16, u32, u64, u128, f32, f64

For FFI, performance-critical paths, and binary-protocol interop.

Money arithmetic (per D-069):

Scalar multiplication and division accept any numeric type as the non-Money operand (the scalar widens implicitly to Decimal for the arithmetic). Money-to-Money addition and subtraction are currency-checked at elaboration when the operands have refined currency annotations. No implicit conversion Nat → Money or Decimal → Money; construct via Money::from_cents(n) or Money::from_decimal(d, currency).

Temporal arithmetic:

Date literals. A calendar date is written hash-delimited: #YYYY-MM-DD#. The hashes are load-bearing — they distinguish a date from arithmetic. A bare 2024-01-01 is integer subtraction (2024 − 1 − 1 = 2022), not a date; written against a Date-typed position it is refused with OE1340 and a directed hint toward the #…# form (the #date# silent-Int landmine, fixed in arc5). The inner text is an ISO YYYY-MM-DD civil date validated at compile time (month 01–12, day in range, leap years exact); a DateTime literal #YYYY-MM-DDTHH:MM:SSZ# carries a trailing T time.

pub type Invoice { mut issued: Date, mut paid: Date }

// `<int>.days` / `<int>.weeks` are duration sugar: a fixed whole-day count
// (`30.days` ⤳ 30, `2.weeks` ⤳ 14). `Date ± Duration` evaluates exactly.
pub derive overdue(i: Invoice) :- Invoice(i), i.paid > i.issued + 30.days;

// `today()` reads the evaluation's current valid-time (a `Date`).
pub derive past_due(i: Invoice) :- Invoice(i), i.paid < today();

Duration construction. A duration is a count of whole days in this increment. The fixed-length units <int>.days and <int>.weeks lower at rule-term resolution to a Duration literal — no impl is needed, and they work in rule bodies today. The calendar-relative units .months / .years have no fixed day count (a month is 28–31 days depending on the anchor), so they are loud-refused with OE1337 rather than silently approximated; compute the target date explicitly instead. Sub-day units (.seconds / .minutes / .hours) await the sub-day Time value layer.

today() — the current valid-time of the evaluation, as a Date — is the one nullary date intrinsic that evaluates today (now() awaits the sub-day layer). It is fixed for the whole evaluation, so a rule stays a pure function of its snapshot; a served model’s deadline arithmetic advances with the wall clock across requests rather than baking a build-time date.

Operator semantics — division. / is exact field division on the numeric tower, on every plane (checker, runtime, reasoner). Statically, Int / Int : Real — the quotient of two integers is a rational, and the type says so; 7 / 2 evaluates to the exact rational 7/2, never a truncated 3. The inference is uniform: 20 / 5 : Real statically even though the value collapses at the carrier (next sentence) — soundly, since Int <: Real. At the value carrier, integral results collapse to Int per the tower-wide convention (20 / 5 is Int(4); integral Real values are Int at the carrier). All other arithmetic operators on Int × Int stay Int. Truncating integer division does not exist; if it is ever wanted, it will be an explicit operator, never /.

Coercion rules:

• Implicit widening: i32 → i64 → Int, Nat → Int, and Int → Real. Since Real is exact (RFD 0016), Int → Real is exact-into-exact (Int ⊆ Real mathematically): require perPeriodValue > 0 compares the Real against the Int literal 0 without an explicit 0.0, and Int + Real yields a Real; a pure-Int expression stays Int — except /, which is Real (operator semantics above). The inexact floats f32/f64 do not implicitly widen into Real — a float reaches the exact tier only via an explicit, lossy conversion (widening an approximate value into the exact tier must be a visible choice).
• Explicit narrowing: i64::try_into::<i32>() returning Result<i32, OverflowError>.
• No implicit truncation, ever.