Argon RFDs

Design decision records for the Argon language, runtime, and toolchain.

An RFD records why a choice was made. It is not the specification. The Lean 4 mechanization at spec/lean/ is canonical for the substrate; the reference manual (Part I of this book) describes the surface in prose. RFDs explain how those landed where they did.

Format

• Filename: NNNN-kebab-case-name.md. Four-digit, no reuse. Numbers are not recycled even when an allocation is abandoned, so the sequence may carry gaps: 0012 was never authored — the number was skipped during a period of concurrent branch allocation (the same churn that renumbered the refinement RFD 0016 → 0017 once numeric-tower took 0016 on main) and the slot was left empty rather than reused.
• Structure: Question · Context · Decision · Rationale · Alternatives · Consequences · Open questions.
• States:
  • discussion — open; not committed.
  • committed — decided and binding. Implementation may or may not have landed; the decision is fixed.
  • accepted — partially implemented — decided and binding, with implementation landed in part; the State: line annotates what has shipped and what remains.
  • superseded — replaced by a later RFD. Cite the successor.
  • archived — the record outgrew this directory and moved intact (with history) to archive/ at the repository root. The number stays allocated; the index row points at the new location.

Authoring an RFD

RFDs live at spec/rfd/ in the repository. The published book reflects whatever is on main. To open a new RFD, allocate the next number, write the file, and submit it via PR — discussion happens on the PR or in linked threads, not by gating merge on consensus.

The format mirrors Oxide Computer Company’s RFD process (Yegge / Dijkstra-via-Bryan-Cantrill lineage) but lighter: no separate authoring tool, no review-state tracker, no required pre-commit lint. A repository PR is the discussion vehicle; the RFD’s State: field carries the decision status.

Index

RFD 0001 — ID architecture

• State: discussion
• Opened: 2026-05-27
• Decides: identifier types used across oxc-protocol, oxc-oxbin, oxc-instantiate, oxc-runtime, oxc-storage-mem, oxc-storage-pg, oxc-reasoning.

Question

Argon currently identifies every declared symbol, every event, every partition key, and every runtime tuple element with a 16-byte uuid::Uuid. Across ~286 call sites and ~21 distinct identifier roles, this is one type doing many jobs. The reasoner — which IS the data system — sees UUIDs in every Z-set tuple and every storage index entry. Is uuid::Uuid the right identifier type for Argon, and if not, what is?

Context

How identifiers flow through Argon

A modeler writes Argon source. The compiler lowers it to a sequence of typed axiom events stored in a .oxbin artifact. The runtime loads the artifact into a Module, opens a Store against a StorageBackend, executes mutations that emit more events, and answers queries by reasoning over the resulting fact set.

Identifiers appear at every stage:

Why the choice is load-bearing

In a system whose hot path involves billions of tuple comparisons in Z-set joins, the identifier IS the data structure. Concrete costs at scale:

• AxiomEvent header: 128 bytes of identifiers per event (7 mandatory UUIDs + 1 SHA-256). At a billion events: ~104 GB of just IDs in the header.
• Storage indexes: every (LiveKey, HistKey) entry carries two UUIDs (tenant + fork) plus a kind tag. ~40 bytes per index entry.
• Z-set tuples: every Value::Id is 17 CBOR-encoded bytes. A 3-arg relation tuple is ~55 bytes for IDs alone.

Survey: what comparable systems do

We studied three prior art systems carefully (Kora, Nous, the generic UUIDv8 graph-DB proposal). Each made specific design choices that don’t map cleanly to Argon:

• Kora (/Users/ivanleon/Code/wt/eidos/main/): Iri(NonZeroU32) backed by a process-wide LazyLock<ThreadedRodeo> interner. Per-engine ConceptIndex with TOP=0, BOTTOM=1 sentinels — owl:Thing / owl:Nothing baked in. Global static state. Tightly coupled to OWL semantics.
• Nous (/Users/ivanleon/Code/wt/orca-mvp/main/crates/nous/): define_id! macro generating newtyped u64 ids derived from FNV-1a 48-bit hashes of qualified IRIs. Sparse → dense IdBridge rebuilt per schema; DERIVED_ID_BIT = 1<<63 overload on IndividualId. 48-bit hash collides at ~2^24 entries.
• Generic graph-DB recommendation (UUIDv8 outer + 64-bit InternalId inner, with HLC timestamp inside the UUIDv8): the HLC timestamp inside the wire ID breaks byte-deterministic builds, which is a non-negotiable Argon property.

None of these are right for Argon directly. The substrate-neutrality requirement (no OWL Thing/Nothing), the per-build determinism requirement (no HLC inside wire IDs), and the multi-axis partition model (tenant × fork × standpoint × module — none of which are subordinate to the others) all push toward a custom design.

Decision

Argon defines ten identifier types, each tuned to its identity-source and role. No uuid::Uuid anywhere. The uuid crate is dropped from the workspace.

The types

Amendment (2026-06-11, issue #270 / PR #285). The NonZeroU32 → INT4 mapping above carries an invariant the original RFD left implicit in the Postgres encoder. Recorded here so call-site comments can cite it: a NameRef’s Postgres wire mapping is INT4 with the high bit reserved — the valid band is [1, 2^31-1]. This is enforced by the sqlx::Encode impl (oxc-protocol/src/ids.rs), which signed-converts through i32::try_from and refuses any value with the high bit set rather than letting it wrap negative on the wire. The 0 slot stays the NonZero* niche sentinel; the top bit is held in reserve. Two consequences follow. First, any hash-derived NameRef (the property_id_for_field / reflective_sort_name_ref / individual_id_from_name stand-ins, which fold a BLAKE3 prefix into an id pending the symbol-table lift) must mask into the band — & 0x7FFF_FFFF, zero-folded to 1 — or a coin-flip of field names would set the high bit and abort the mutation (PR #285). Second, folding a hash into 31 bits is not injective; PR #285 adds the load-time collision gate (OE0231) so two distinct Type::field pairs that alias one id refuse loudly instead of silently sharing a storage column. The hash stand-ins are a bridge: the sequential interning table that derives NameRefs from canonical symbol-table position (Phase 3 below) is the production follow-up tracked at #270, and it retires both the mask and the gate.

Two ways identity is derived

The 10 types split cleanly on identity-source:

Content-addressed (deterministic from source content; same source → same byte):

• NameRef — derived from symbol-table position, which is derived from canonical-sorted qualified paths.
• AxiomKey — BLAKE3-128 of canonical body bytes.
• ContentId — BLAKE3-256 of body bytes.
• CompositionSignature — BLAKE3-256 of composition input.

Allocation-addressed (system-allocated counters, deterministic per-build):

• TenantId, ForkId — provisioning tables (counters under operator control).
• EventId — per-event counter (deterministic in build mode; Snowflake in runtime).
• IndividualId — per-mutation counter (deterministic within a build pass).

Iri is a surface artifact; InternalId is a runtime-only artifact. Neither participates in wire identity.

BLAKE3 unification

AxiomKey (128 bits) and ContentId (256 bits) come from a single BLAKE3-256 invocation of the canonical body bytes. AxiomKey is the first 16 bytes; ContentId is the full 32 bytes. One hash invocation per event.

BLAKE3 replaces SHA-256 throughout because: ~3× faster, parallel-friendly, same cryptographic strength, smaller code size. The replacement is a one-time wire-format change tied to this RFD.

Per-lattice sentinels (engine-local, never on wire)

Within a single Module load, the reasoner builds InternalId-space per lattice (per metatype’s subsumption lattice, per standpoint lattice, per refinement lattice). Within each lattice, the reasoner reserves:

• The lattice’s ⊤ (universal) at the lowest available InternalId for that lattice’s kind+partition.
• The lattice’s ⊥ (inconsistent) at the next one.

These are engine-local artifacts, recomputed at every Module::load, never written to the wire. The lattice’s actual top and bottom are declared concepts (e.g., the universal in a metatype’s subsumption lattice is a concept declared in stdlib like std::mlt::Class); the engine’s reservation is purely an evaluation-time optimization for short-circuit operations.

This differs from Kora/Nous, which reserve TOP=0 / BOTTOM=1 globally across all concept IDs — that’s an OWL-ism (a single owl:Thing for the whole ontology). Argon doesn’t have a single universal; each lattice has its own bounds, and they’re declared entities, not primitive IDs.

Type-distinct newtypes via the define_id! macro

Each ID type is a newtype with its own Display, Ord, Hash, Serialize, Deserialize, big-endian wire encoding, and NonZero* niche for Option<_>. Generated via a single define_id! macro (inspired by Nous’s pattern). Crossing roles requires explicit conversion — no accidental TenantId ↔ ForkId confusion at the type level.

Rationale

Why NameRef instead of UUIDv5(path)

The .oxbin format already mandates a symbol-table section (§D.5) with HDT-PFC-compressed canonical-sorted qualified paths. We’ve been routing around it by minting UUIDv5(path) instead of using the symbol-table position directly.

UUIDv5(path) gives:

• 16 bytes per reference
• Determinism (same path → same UUID)
• Cryptographic collision resistance

NameRef = symbol-table position gives:

• 4 bytes per reference
• Determinism (canonical sort order)
• Zero collision risk (by construction — positions are unique)
• Native: the dictionary the format already requires

The savings are 12 bytes per declarative reference. Across hundreds of bodies in a real workspace with hundreds of references each, this is substantial. And the property — same source → same NameRef — is preserved.

Why content-addressed AxiomKey at 128 bits, not 64

A 64-bit AxiomKey saves 8 bytes per event header — ~5% of the header. The cost: birthday-collision probability ~37% at 2^32 entries; necessitates collision-handling machinery (either deterministic re-salting or content_id fallback verification on every lookup).

128 bits is birthday-safe past 2^64 entries (effectively unbounded). Collision handling unnecessary. BLAKE3-128 is fast (free, given we compute BLAKE3-256 for ContentId anyway). The 8 bytes saved on the event header aren’t where the storage wins live — those are in declarative _id fields (16 → 4 = 12 bytes saved each, multiplied across every body) and Z-set tuples (17 → 9 bytes per ID, multiplied across millions of tuples).

The architectural rule: don’t compromise the wire format for bytes that aren’t on the hot path.

Why IndividualId is system-allocated, not caller-provided

Pattern: every database treats internal entity identity as surrogate, and external (caller-provided) identity as data. Postgres uses BIGSERIAL PRIMARY KEY + external_id TEXT UNIQUE. Datomic uses partition-encoded entids + :db/ident for natural keys.

Argon mutations like register(external_id: Text) should:

1. Allocate a fresh IndividualId(NonZeroU64) internally.
2. Emit iof_assertion(IndividualId, Person).
3. Emit hasExternalId(IndividualId, external_id) for the caller’s identifier.

The caller can query “find the Person where hasExternalId = ‘user_12345’” later. External identity is a property; internal identity is a surrogate. This is the pattern that scales and stays clean — and it lets IndividualId be 8 bytes (system-allocated) instead of 16 bytes (caller-provided UUID).

Why InternalId is runtime-only

InternalId layout [kind: 8 | partition: 16 | sequence: 40] is optimized for:

• Cache-friendly Vec<u64>-indexed bitmaps (per-kind, per-partition).
• Fibonacci-hashed U32-keyed sets in hot loops.
• Zero-cost type discrimination via the kind byte.

But this layout is engine-policy, not modeler-visible. We reserve the right to renumber on compaction, change partition functions, etc. Making InternalId part of the wire format would couple wire to engine — wrong direction. It stays runtime-only; Module::load builds a NameRef ↔ InternalId dictionary; the reasoner operates entirely in InternalId space.

Why no UUIDs

Five reasons:

1. We control allocation. UUIDs solve the “globally unique without coordination” problem. Argon’s identifiers are either declared (NameRef from canonical symbol position), system-allocated (EventId, IndividualId), or content-derived (AxiomKey, ContentId). No coordination problem exists.

2. Type safety. All 21 identifier roles collapsing into one Uuid type is a regression. Newtypes per role give compile-time discrimination.

3. Storage efficiency. Replacing UUIDs with the right-sized type per role saves 60-80% of identifier bytes across the system.

4. Wire format determinism. UUIDv4 is random; UUIDv7 has wall-clock time; UUIDv5 is one hash family. Custom types let us pick the determinism story per role (content-hash for AxiomKey, sort-position for NameRef, deterministic-counter for EventId in build mode).

5. No external compatibility need. Argon doesn’t need to interoperate with systems-that-mint-UUIDs at the identifier level. Federation happens at the Iri level (qualified paths), not at the binary-ID level.

Alternatives considered

Alt 1: Keep UUIDs everywhere

The status quo. Universal, well-understood. Costs: 145 bytes of identifiers per event header; 17-byte Z-set tuple elements; ~286 call sites with one type doing many jobs; full 16-byte width for partition keys with low-cardinality.

Rejected. The hot-path costs and lack of type discrimination outweigh the familiarity benefit.

Alt 2: UUIDv8 outer + 64-bit InternalId inner (the generic doc recommendation)

A two-tier system with UUIDv8 (RFC 9562, custom layout) as the durable external identifier and a packed 64-bit InternalId for hot paths.

Rejected. UUIDv8 in any recommended form embeds a timestamp (HLC), which breaks Argon’s byte-deterministic-build invariant. And the “external identifier” tier isn’t needed for Argon today — we don’t federate at the binary-ID level.

Alt 3: Snowflake-style 64-bit time-ordered IDs throughout

A single 64-bit ID type [time: 42 | shard: 10 | seq: 12] for everything.

Rejected. Conflates allocation-addressed (events) with content-addressed (declarative symbols). Concepts shouldn’t have time in their identity; events should. Single-type-for-everything is what we’re moving away from.

Alt 4: Nous’s FNV-1a 48-bit ConceptId

Hash the qualified path with FNV-1a, truncate to 48 bits, that’s the ID.

Rejected. Collides at 2^24 entries (~16M). Nous trusted IRIs not to collide; Argon shouldn’t. And it conflates declarative identity (paths) with run-of-the-mill IDs.

Alt 5: Kora’s per-engine ConceptIndex with HashMap<Iri, u32>

Each engine maintains its own Iri → u32 index, rebuilt per session.

Rejected as primary scheme (kept as inspiration for InternalId at Module::load time). Per-engine indexes don’t address the wire-format problem; they’re an in-memory representation.

Consequences

Wire format changes (major)

• Bump oxbin_format_version major (Phase 2 of rollout — see below).
• All _id: uuid::Uuid fields in oxc-protocol::storage::*Body types become typed: NameRef, EventId, AxiomKey, etc. per their role.
• AxiomEvent header shrinks from 145 bytes of identifiers to 81 bytes (44% reduction).
• .oxbin files produced under the old format are not readable under the new format. We have no externally-deployed .oxbin files; this is acceptable.

Code changes

• uuid crate removed from workspace dependencies.
• blake3 crate added (replaces sha2).
• New oxc-ids crate (or oxc-protocol::ids module) carries the 10 types + define_id! macro.
• oxc-instantiate::identity becomes the Iri ↔ NameRef ↔ symbol-table builder.
• oxc-runtime::Module::load builds the NameRef ↔ InternalId dictionary.
• oxc-reasoning::compile::Value becomes Value::Internal(InternalId) plus inline variants.
• oxc-storage-mem indexes re-keyed on (TenantId, ForkId, kind) instead of (Uuid, Uuid, &'static str).

Performance

Expected wins:

• Reasoner memory: ~30-50% reduction in Z-set tuple key storage (17 → 9 bytes per ID).
• Event headers: 44% smaller (145 → 81 bytes).
• Storage indexes: ~50% smaller (UUID → u32/u64 partition keys).
• Hash operations: BLAKE3 ~3× faster than SHA-256.

Costs:

• Module::load builds a dictionary (one pass over declared symbols; negligible).
• Dropping UUID crate removes a well-tested dependency; replaced with custom types that need testing.

Determinism preserved

Every wire-format identifier is content-derived (NameRef from sort position; AxiomKey from BLAKE3 of body; ContentId from BLAKE3 of body; EventId from build-deterministic counter in build mode). Same source → byte-identical .oxbin. Property preserved.

Phased rollout

The full design can be landed in four independently-shippable phases:

Phase 1 — runtime InternalId, no wire change (~3 days). oxc-reasoning::compile::Value::Internal(InternalId) replaces Value::Id(Uuid). Module::load builds a Uuid ↔ InternalId dictionary. Wire format unchanged. Win: ~30% reduction in reasoner Z-set memory.

Phase 2 — wire format break (~1 week). Add oxc-protocol::ids with all 10 types. Replace every _id: uuid::Uuid in body types. Drop uuid crate, add blake3. Bump oxbin_format_version major. Win: 44% reduction in event header size; type-safe identifiers throughout the wire.

Phase 3 — full Iri interner + symbol-table lift (~3 days). Iri(Arc<str>) with per-workspace arena. The .oxbin symbol-table section becomes the load-bearing dictionary it was designed to be. Win: cleanup of qualified_path: String duplication.

Phase 4 — dense engine structures (~1 week). Fibonacci-hashed U32Set, KindBitmap (Vec<u64> indexed by InternalId), RoleEdges-style packed adjacency. Per-lattice sentinel discipline. Win: foundation for future reasoner backends (SLG, DBSP, Kripke) sharing dense set primitives.

Open questions

• Cross-workspace federation: when two workspaces’ .oxbin artifacts need to interoperate, what’s the bridge? Open. Likely: an explicit GlobalRef type at the federation boundary only, derived from (workspace_uuid, NameRef) or from full Iri. Out of scope for this RFD.

• Distributed minting of EventId: the shard: 12 field is reserved but currently always 0. A future RFD addresses the distributed-minting protocol (Stateless Snowflake from container IP, range pre-allocation, or CRDT-style — see “Stateless Snowflake” Chinthareddy 2025).

• External identifier indexing: when IndividualId is system-allocated and the caller’s identifier is data (a hasExternalId property), querying by external identifier requires a property-indexed lookup. The storage layer’s per-relation indexes (book §20.3.1) cover this, but specific query ergonomics for “find by external id” want a small SDK helper.

• AxiomKey for non-data axioms: mutation_decl, query_decl, compute_decl are declarative axioms (have stable NameRef-based identity). Should their AxiomKey be BLAKE3(NameRef) or a special discriminator? Likely the former for uniformity; settle when wire format is finalized.

RFD 0002 — #[comptime] attribute

• State: discussion
• Opened: 2026-05-27
• Decides: surface syntax and semantics of compile-time evaluation in Argon. Affects oxc-parser (attribute recognition), oxc-instantiate (compile-time lifting), oxc-reasoning (the engine, run at build time on a subset of rules), oxc-oxbin (materialized fact storage), and diagnostic codes OE1307/OE1308.

Question

Argon’s reasoner can evaluate rules at runtime (the keystone path) or at compile time (when all inputs are statically known). The compile-time path is strictly faster: facts get materialized into the .oxbin at build time and shipped as data, eliminating runtime evaluation for that rule entirely. When and how should the modeler opt in to compile-time evaluation? What does it mean per rule mode? What’s the auto-vs-explicit story?

Context

Why compile-time evaluation matters

Argon’s central thesis is the reasoner IS the data system. The same engine that derives adult(p) at query time can derive adult(p) at build time — if its inputs (Person(p), hasAge(p, n)) are statically known. Materializing the derivation at build time gives:

1. Runtime queries see literal facts, not derivations. Faster, simpler query path.
2. The .oxbin ships the closed-world extent. Downstream consumers (other compilation units, runtime, federation peers) don’t re-derive.
3. Compile-time errors for impossible derivations. A check rule that fails at build time is a build error, not a runtime exception.
4. A natural staging surface. Modelers can mark which derivations are “decided at build” vs “decided at runtime” — explicit control over the deployment-time computational tier.

What “compile-time” means here

The reasoner has two distinct invocation points:

• Runtime mode — Engine instantiated inside oxc-runtime::Store; rules evaluate against live event state; result is queried via Store::query_derive.
• Compile-time mode — same Engine, instantiated inside oxc-instantiate during .oxbin lowering; rules evaluate against the source’s declarative facts (iof_assertion events from insert operations in mutations declared inside the workspace); result is emitted into the .oxbin’s events section as fresh axiom events (with derivation provenance pointing to the comptime rule).

The “engine is the engine” property holds: same code, same semantics, different invocation context.

What’s a “static input”?

A predicate is statically known at build time if its extent is fully determined by:

• Axioms declared in source code (pub kind, pub rel, pub mutate invocations baked into module initialization).
• Outputs of other comptime-eligible rules (the comptime fixpoint propagates).

A predicate is runtime-bound if any contributing fact comes from:

• Caller-invoked mutations (user runs register(...) against a running Store).
• External federation peers.
• Network/IO sources.

Today’s MVP only has declarative axioms — everything is statically known. But the distinction is structural, not implementation-momentary.

Decision

Attribute surface

#[comptime]
pub derive adult(p) :- Person(p), hasAge(p, n), n >= 18;

The #[comptime] attribute applies to a single declaration. Binary form in v1 — no arguments. Argument form is parser-reserved for v2 (see Open Questions).

Per-mode semantics

Auto-lifting

The compiler automatically lifts any rule (regardless of #[comptime]) whose body predicates are all statically known and whose result fits within the declared comptime budget. The lift is transparent — produces the same axiom events as if the rule had been declared #[comptime].

#[comptime] is therefore a promise (“this rule MUST be evaluable at build time”), not just an enable. If the modeler declares #[comptime] on a rule whose body references a runtime-only predicate, the build fails with OE1307 ComptimeNotStatic.

This makes #[comptime] checkable: it’s a verification that a property holds, not just a performance hint.

Diagnostic codes

• OE1307 ComptimeNotStatic — rule declared #[comptime] depends on runtime state (a mutation-bound predicate, a federation-bound predicate, or an indirect dependency through another runtime-only rule).
• OE1308 ComptimeForbiddenOnMutate — #[comptime] applied to a mutate declaration.
• OE0227 AttributeArgsNotYetImplemented (existing) — #[comptime(...)] with any arguments emits this; arg-form is parser-reserved for v2.

Materialization output

A #[comptime] derive p(x) :- A(x), B(x) rule produces, at build time:

1. The derivation: every tuple in p’s extent emitted as an iof_assertion or relation_tuple axiom event.
2. The provenance: each emitted event carries derivation set to the rule’s AxiomKey (per RFD 0001) so retraction propagates correctly.
3. A comptime_lifted: bool field in RuleDeclBody indicating “this rule’s facts are pre-materialized; runtime evaluators may skip it.” (Adds 1 byte to RuleDeclBody.)

Reasoning about freshness

If the source code changes such that a comptime-lifted rule’s inputs change, the .oxbin is rebuilt and the materialized facts are recomputed. The Salsa-style incremental compilation layer (book §18.2) treats comptime_lifted rules as memoization targets — their inputs are tracked, and only changed-input rules re-materialize.

Rationale

Why per-mode semantics, not uniform

The five rule modes (fn / derive / query / mutate / check) have genuinely different meanings, and “compile-time” means something different for each:

• derive produces facts → comptime means baking those facts into the artifact.
• query produces a result value → comptime means embedding that value.
• check produces a verdict → comptime means asserting at build time.
• fn is a function call → comptime means const-evaluation in the Rust/C++ tradition.
• mutate mutates state → comptime makes no sense; mutations are by definition runtime.

A single uniform “evaluate at build time” semantics would erase these distinctions. The mode-aware semantics match the modeler’s mental model.

Why auto-lift + explicit attribute (not just one)

Auto-lift alone risks silent performance cliffs: the modeler doesn’t know whether a rule is being materialized or runtime-evaluated. Adding a runtime-only predicate elsewhere could silently degrade performance.

Explicit-only would force the modeler to annotate every rule, even the obvious cases.

Auto-lift plus #[comptime] as a checked promise gives both: most rules auto-lift transparently; the modeler can opt-in to “this MUST be comptime” for ones where the property matters. Same pattern as Rust’s const fn — the compiler can evaluate any expression at compile time when possible, but const fn is the promise that this function is callable in const context.

Why argument-form is reserved, not implemented in v1

Four argument variants we expect to want:

• #[comptime(strict)] — fail build if auto-lift can’t reduce all inputs (stronger than the default OE1307 — even runtime-derivable-but-not-yet-evaluated counts as failure).
• #[comptime(profile)] — emit a build-time report of cost/cardinality for this rule.
• #[comptime(embed)] — for query mode: embed the result inline in source as a literal, not just in the .oxbin (useful for let X: extent = query foo inside a fn).
• #[comptime(lazy)] — comptime-eligible but defer materialization until first runtime access (useful for very-large extents).

None of these are necessary in v1. We commit the parser-level syntax (#[comptime(...)] parses without error) but emit OE0227 on any non-empty arg list. This lets us add the arg-form in v2 without changing parser surface.

Why OE1307 distinguishes “comptime-eligible but not yet evaluated” from “comptime-impossible”

A comptime rule depending on another rule that’s itself comptime-eligible but not yet processed should propagate up the comptime fixpoint, not fail. The build’s job is to find the comptime fixpoint over the rule graph; only rules that hit a runtime-only predicate or a cycle (that can’t be broken by other comptime rules) fail with OE1307.

Why mutate is forbidden, not silently no-op

Mutations modify state. State at compile time is the static fact base; “running” a mutation against it would change what’s baked into the artifact, which violates the closed-world property (the .oxbin’s facts are what the modeler wrote, plus what derivations they declared). Allowing #[comptime] mutate ... would either:

• Silently no-op (confusing — modeler thinks something happened).
• Modify the build’s fact base (dangerous — implicit data mutation hidden in code).

Better to forbid loudly via OE1308.

Alternatives considered

Alt 1: No comptime at all — everything is runtime

The status quo. All rules evaluate at runtime; the .oxbin carries only declared facts plus rule definitions.

Rejected: gives up the major performance win of build-time materialization. Loses the natural “compile-time assertion” surface for check rules. Forces every cross-cutting query to pay runtime evaluation cost.

Alt 2: Implicit only — no attribute, just auto-lift

Every rule the compiler can prove statically-decidable is auto-materialized. No modeler annotation.

Rejected: silent performance cliffs as discussed. Loses the “this MUST hold” checkable property. Loses the natural place to thread future args (strict/profile/lazy).

Alt 3: Explicit only — every comptime rule must be annotated

No auto-lift; only #[comptime] rules are materialized at build.

Rejected: forces annotation noise on the obvious cases. Modelers will either over-annotate (defensive #[comptime] everywhere) or under-annotate (missing perf wins). Loses the simplicity of “the compiler does the right thing by default.”

Alt 4: #[const] instead of #[comptime]

Borrow Rust’s terminology for symmetry.

Rejected: “const” connotes value-level immutability in Rust, which is a different concept from “evaluated at build time.” Argon’s facts are already immutable once asserted; the relevant axis is when they’re asserted (build vs runtime), not whether they’re mutable. comptime is clearer.

Alt 5: Zig-style comptime (full compile-time computation)

Zig’s comptime does general compile-time evaluation including type-level computation. Argon could expose the same generality.

Rejected as the v1 design. Zig’s comptime is a much larger surface — it includes generic instantiation, type erasure decisions, and runtime/compile-time polymorphism. Argon’s #[comptime] is scoped to the substrate’s reasoning capability: which rules get materialized. Generalizing to Zig-shape comptime is interesting future work, but it’s a different feature.

Consequences

Wire format

RuleDeclBody gains a comptime_lifted: bool field. 1 byte added per rule decl. Negligible.

Build performance

Comptime-eligible rules add to build time (the engine runs at build). Trade-off: build is slower; runtime is faster + simpler. For workloads where the .oxbin is built once and queried many times, this is strictly positive. For dev-loop scenarios (rebuild frequently), Salsa-style incremental compilation memoizes most of the work.

Diagnostic surface

Two new emission sites (OE1307, OE1308 — already reserved in grammar.toml from the earlier diagnostic landing). The parser keeps the existing OE0227 for non-empty arg form.

Code volume

Modest:

• Parser change: ~10 lines to recognize #[comptime] attribute on declarations.
• oxc-instantiate change: build-time engine invocation for comptime-eligible rules, comptime fixpoint analysis, OE1307 emission. ~200-300 LOC.
• oxc-oxbin change: emit derivation events from comptime rules into the events section. ~50 LOC.
• RuleDeclBody schema: comptime_lifted field. ~5 LOC.

Determinism preserved

Comptime evaluation produces the same axiom events from the same source — the engine is deterministic, and the inputs are entirely from source. Byte-identical .oxbin guaranteed (per RFD 0001).

Open questions

• The argument form in v2 — #[comptime(strict|profile|embed|lazy)]. Specific semantics deferred to a follow-up RFD when we have benchmarking to validate the tradeoffs. The parser-level syntax stays reserved.

• Comptime budget — should there be a soft limit on how much work a comptime rule can do (e.g., “evaluate up to N facts; if exceeded, emit a warning and fall back to runtime”)? Useful for guarding against accidentally exponential comptime work. Likely yes, with a default of 10M facts and a CLI/config override.

• Comptime + standpoint federation — when standpoint A imports from standpoint B and B has comptime-lifted rules, A sees B’s materialized facts. But if A re-evaluates a derived predicate against its own facts plus B’s, does the comptime materialization compose correctly under the FDE info-join? Likely yes (it’s just facts), but worth a separate verification when standpoint federation is mechanized in the Lean.

• Interaction with retraction — a comptime-materialized rule’s derived facts have a derivation lineage. If a contributing axiom is retracted at runtime (via delete operation), the derived facts must also be retracted. The retraction propagation needs to traverse the derivation graph. Architectural: yes; implementation: needs the Phase-4-style dense provenance index from RFD 0001 to be efficient.

• Comptime + temporal — for rules with explicit temporal qualifiers (at(t), during(...)), does comptime still make sense? The rule’s truth depends on t. Probably comptime should be allowed only when temporal qualifiers are themselves static (e.g., literal timestamps), and emit a diagnostic when they’re symbolic. Defer to the temporal-substrate work track.

RFD 0003 — Reasoner backend dispatch

• State: discussion
• Opened: 2026-05-27
• Decides: how multiple reasoning backends (semi-naive, SLG, DBSP, SMT, Kripke, Kora-extension) compose under one Engine interface; the dispatch policy for per-stratum routing; the registration discipline; the modeler-facing diagnostic surface for unsupported-tier rules.

Question

Argon’s tier ladder admits seven distinct reasoning tiers (§10.1: structural, closure, expressive, recursive, fol, modal, metaorder). No single algorithm handles all seven — semi-naive Datalog handles stratified recursive; SLG tabling handles expressive; DBSP handles recursive under IVM; SMT handles fol; Kripke tableau handles modal; Kora-EL handles a slice of OWL profile semantics. How do these backends compose under one engine interface? What does the dispatcher do? When does the modeler see backend choices vs not?

Context

What’s already in place

Phase 1 of the reasoner is shipped (oxc-reasoning crate, ~530 LOC of evaluator + classifier + scaffolding). The keystone test passes: derive adult(p) :- Person(p), hasAge(p, n), n >= 18 derives the right facts end-to-end.

The current shape:

Engine
  ├── executors: Vec<Box<dyn TierExecutor>>   (registration-ordered)
  └── run_rules(...) — dispatches each rule to the first executor
                       whose supported_tiers() contains the rule's
                       classified tier.

TierExecutor trait
  ├── name(&self) -> &'static str
  ├── supported_tiers(&self) -> TierSet
  └── execute(stratum, input) -> ReasoningResult<RelationCatalog>

The single MVP implementation SemiNaiveExecutor advertises {Structural, Closure, Recursive}. The dispatcher is one-deep: pick the first executor that supports the tier. Per-rule tier comes from RuleDeclBody.main_tier, populated by oxc-instantiate::tier_classify::classify_body.

Where this falls short

The “first executor that supports the tier” policy works for the trivial case (one executor) but doesn’t say what happens when:

1. Multiple executors claim the same tier (e.g., SemiNaive and DBSP both handle recursive). Which wins? Order-of-registration is the current answer; that’s an implicit policy with no surface.

2. A rule’s body spans multiple tiers (e.g., a recursive rule that joins against an expressive qualified-cardinality predicate). Today the rule’s main_tier is the max of its atoms’ tiers — so the whole rule goes to whatever handles the max. That’s correct semantically but ignores stratification: the lower-tier sub-rule could run on the cheaper engine, results then fed into the higher-tier engine.

3. Cross-backend data exchange — every backend produces RelationCatalog (Z-set BTreeMaps). Good for composition; the next stratum reads from the prior stratum’s output. But what if a backend uses internally-different data (DBSP’s arrangements vs SLG’s tabled tables)? The exchange happens at stratum boundaries via RelationCatalog; backend internals stay private.

4. The modeler’s diagnostic surface — OE1305 (TierNotYetImplemented) is reserved but emission sites aren’t wired. When does the modeler see it? At build time (the rule’s tier exceeds any registered backend) or at query time (the rule’s classified tier is unsupportable)?

5. Optional backends (Kora-extension) — std::owl is a stdlib package that brings in the Kora-EL / Kora-DL backend. How does that get registered? Is it an explicit Engine::with_executor call, or implicit on import std::owl?

Decision

The dispatch model: per-stratum, registration-ordered, with explicit OE1305 emission

1. Strata are the unit of dispatch. The physical plan (PhysicalPlan) carries a Vec<Stratum>. Each stratum has a tier (the max of its rules’ tiers). The dispatcher picks one executor per stratum and runs it.

2. Registration order = preference order. Executors are pushed onto Engine::executors in registration order. The dispatcher picks the first executor whose supported_tiers() contains the stratum’s tier. This makes the policy explicit and modeler-controllable via build configuration.

3. OE1305 emits at build time, not query time. When oxc-instantiate classifies a rule and the workspace’s configured backends don’t claim its tier, the build fails with OE1305. The modeler sees the error at compile time, before any runtime invocation.

4. Backend registration is workspace configuration. Backends are declared in ox.toml (or the equivalent), not in source code. Default workspaces register SemiNaiveExecutor only. Adding SLG, SMT, etc. is an explicit opt-in via:

   [reasoning]
   executors = ["semi-naive", "slg-tabled"]
   

   Kora-extension is enabled by import std::owl in source, which adds kora-el (and kora-dl) to the executor list automatically.

5. Cross-backend exchange is the shared RelationCatalog. All backends produce and consume RelationCatalog (Z-set BTreeMap). Internal representations (DBSP arrangements, SLG tabled solutions) are private. Composition happens at stratum boundaries: stratum N’s output catalog is stratum N+1’s input catalog.

The seven backends, mapped

Composition rules:

• DBSP wins over SemiNaive when both are registered: register DBSP first so the dispatcher picks it. DBSP is a strictly more powerful evaluator (handles IVM, deltas, retractions natively); SemiNaive becomes a fallback for environments where DBSP can’t be deployed.
• Kora-extension only handles its declared tier slice. It doesn’t claim recursive even though some EL rules look Datalog-shaped — Kora’s optimizations are OWL-specific and don’t generalize. The dispatcher uses Kora only for rules tagged as DL-shaped (a future RuleDeclBody field).

What the modeler sees

The modeler does not see backend names in source code. Rules are tier-classified by the compiler; backend selection is a deployment concern.

The modeler does see OE1305 when a rule’s tier exceeds the workspace’s configured backends. The diagnostic suggests which backend would handle it:

error[OE1305]: rule `complex_query` classified at tier `expressive` —
              no registered executor handles this tier
  --> demo.ar:42:1
  |
  | pub derive complex_query(p) :- ...
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = note: enable the `slg-tabled` executor in ox.toml:
        [reasoning]
        executors = ["semi-naive", "slg-tabled"]

The TierExecutor trait — refined

#![allow(unused)]
fn main() {
pub trait TierExecutor: Send + Sync {
    fn name(&self) -> &'static str;
    fn supported_tiers(&self) -> TierSet;

    /// Execute one stratum. Reads from `input` (current state +
    /// prior strata's outputs); returns the stratum's catalog delta.
    fn execute(
        &self,
        stratum: &Stratum,
        input: &RelationCatalog,
    ) -> ReasoningResult<RelationCatalog>;

    /// Optional: backend-specific cost estimate for a stratum.
    /// Returned values are comparable across backends (smaller = preferred).
    /// Default impl returns `f64::INFINITY` (never prefer).
    fn estimate_cost(&self, _stratum: &Stratum, _input: &RelationCatalog) -> f64 {
        f64::INFINITY
    }
}
}

The estimate_cost method is the hook for cost-based dispatch (v2). v1 uses pure registration-order dispatch; v2 may evolve to “pick the registered executor whose cost estimate is lowest.” Deferred to a follow-up RFD.

Stratum boundary policy

The optimizer is responsible for stratification: walk the rule dependency graph, partition into SCCs, topologically sort the SCCs into strata. Each stratum is single-tier (max of its rules). NAF is stratified across stratum boundaries (sound).

Inter-stratum NAF (a rule in stratum N+1 uses not p(...) where p is populated in stratum N) is the standard stratified-WFS case. Intra-stratum NAF is a cycle and either:

• Handled by the backend if the backend supports WFS (SLG does; SemiNaive doesn’t beyond stratification).
• Rejected with OE1309 (StratificationNafCycle) at build time.

Rationale

Why per-stratum, not per-rule

A real-world workload has many rules at different tiers. Dispatching per-rule means launching the backend’s per-call overhead for each. Per-stratum amortizes: the backend sees all its rules, can build its own internal arrangements once, run them all to fixpoint within its scope.

This matches DataFusion’s pattern (which inspired the architecture): each ExecutionPlan node runs to completion in one backend context; data flows between nodes via the shared columnar format. Argon’s analog: each stratum runs in one backend context; catalogs flow between strata via the shared Z-set format.

Why registration order, not declared priority

A priority: i32 field on TierExecutor would let backends declare their own preference order. Rejected because:

• It distributes the dispatch logic — each backend needs to know its place in the ordering vs other backends.
• It introduces a coordination problem when two backends claim the same priority.
• Registration order achieves the same expressivity (push backends in the desired order) without per-backend coordination.

Workspace configuration (ox.toml’s [reasoning].executors = [...]) makes the order explicit and modeler-visible. That’s the right surface for the policy decision.

Why OE1305 at build time, not query time

The alternative is lazy: register backends; at query time, if no backend handles the tier, fail. Rejected because:

• A modeler shouldn’t ship an .oxbin that they don’t know is unrunnable. Build-time emission catches it early.
• The set of registered backends is a deployment property; the modeler knows it at build configuration time.
• “Build it, ship it, then it fails when the user runs it” is a bad UX for a system whose virtue is “deterministic builds give you runtime guarantees.”

Why workspace-config, not in-source backend selection

Source code shouldn’t say “use SLG for this rule.” Two reasons:

• The modeler should describe what they want derived, not how to derive it. That’s the entire point of declarative semantics.
• Backend choice is deployment policy. A test workspace uses SemiNaive; a production workspace uses DBSP + SLG. Same source code, different deployment.

The exception: std::owl is a stdlib package that brings in OWL semantics. Importing it implicitly enables Kora-extension because the modeler is asking for OWL-shape reasoning. This isn’t “backend selection”; it’s “load this semantics extension.”

Why DBSP wins over SemiNaive when both registered

DBSP handles every workload SemiNaive handles, plus retractions and IVM. It’s strictly more powerful. Once DBSP is mature (Phase-4-of-RFD-0001 or later), the natural default is “use DBSP if available, fall back to SemiNaive otherwise.” Registration order encodes this: push DBSP first.

SemiNaive stays in the stack because:

• It has no external dependencies (DBSP needs the timely dataflow runtime).
• It’s simpler to reason about correctness in.
• It’s the reference implementation that other backends can be tested against.

Why Kora is “extension” not “default”

Argon’s substrate is OWL-neutral. Baking OWL-specific optimizations into the default executor stack would couple Argon to OWL semantics — which RFD 0001 and the broader architecture explicitly avoid.

Kora becomes available when a modeler imports std::owl. That import is a deliberate statement: “I want OWL semantics for this part of my model.” The Kora backend then handles those rules; non-OWL rules go through the default backends.

Alternatives considered

Alt 1: Single mega-engine

One backend handles all tiers via dispatched algorithms internally. Examples in prior art: SWRL-DL engines that switch between Datalog and tableau internally.

Rejected: kills modularity. Adding a new backend (SLG, DBSP) requires modifying the mega-engine. Cross-engine testing becomes impossible.

Alt 2: Runtime backend resolution

Backends register themselves via plugin discovery at runtime; the engine probes for capability.

Rejected: introduces dynamic-loading complexity Rust doesn’t natively support and Argon doesn’t need. All known backends are statically-known at build time.

Alt 3: Backend per rule mode

derive rules go to one backend, query rules to another, etc.

Rejected: backend choice is about tier (what features the rule uses), not mode (what kind of declaration it is). A derive rule and a query rule with the same body should run on the same backend.

Alt 4: First-class cost-based dispatch from v1

estimate_cost is mandatory; dispatcher picks the lowest-cost backend per stratum.

Rejected for v1: backends don’t yet have meaningful cost models. SemiNaive’s cost estimate is fact-count; DBSP’s would involve arrangement-sharing analysis. Without a calibrated cost surface, “lowest cost” is noise. Registration-order is honest about the v1 state. Cost-based dispatch becomes v2 once enough backends ship to make calibration meaningful.

Consequences

Code structure

The Engine and TierExecutor trait already exist (oxc-reasoning/src/executor/mod.rs). This RFD codifies the existing API; minor refinements needed:

• Add estimate_cost default method (deferred-use API).
• Add workspace configuration support (ox.toml parsing for [reasoning]).
• Wire OE1305 emission from oxc-instantiate::tier_classify when the configured backends don’t cover the classified tier.

Diagnostic surface

OE1305 emission gains a structured “suggest enabling X backend” hint. Requires the diagnostic system to know which backends could handle which tiers — a static table in oxc-diagnostics or oxc-reasoning::backend_registry.

Each future backend’s commit

Each new backend lands as:

1. A new module in oxc-reasoning::executor::{name}.rs implementing TierExecutor.
2. Registration plumbing in workspace config.
3. Backend-specific tests showing the keystone-equivalent for its tier (e.g., SLG’s keystone is a recursive-aggregate rule like count over a stratified-NAF derived predicate).
4. An interop test showing the backend composes cleanly with SemiNaive at stratum boundaries.

Kora vendoring decision

Per the earlier session decision: when we bring in Kora, we vendor the code into oxc-reasoning::executor::kora and own the implementation. We don’t depend on the upstream kora-* crates. This isolates Argon from Kora’s design choices and lets us evolve the embedded reasoner independently.

The vendoring is an explicit one-time copy; subsequent changes happen in Argon’s tree. If upstream Kora improves substantially, we re-vendor with a documented migration. This matches the pattern other projects use for embedded engines (e.g., rust-analyzer’s vendored libraries).

Open questions

• Stratum boundary policy with retractions: when a fact is retracted in stratum N, the retraction must propagate to stratum N+1’s derived facts. The current RelationCatalog exchange is a snapshot, not a delta stream. For DBSP this is solved natively (it IS the delta stream); for SemiNaive we recompute. Architecturally clean; performance-cost matters for large stores. Defer to the DBSP integration RFD.

• Workspace config schema: ox.toml’s [reasoning] section needs a concrete schema. Reserve the section now; nail down the schema when the second backend (DBSP or SLG, whichever lands first) makes it necessary.

• Per-rule backend override: should the modeler ever be able to say “use SemiNaive for this rule even though DBSP is registered”? Possible use cases: debugging (compare backends on the same rule), workload-specific tuning. Defer; revisit when a real use case emerges.

• Backend feature negotiation: a backend may support a tier but not a specific feature (e.g., SemiNaive supports recursive but not recursive with aggregates). How does the dispatcher know? Either (a) backends advertise feature support more granularly than tier, or (b) the classifier bumps tiers when specific features are used (e.g., aggregates always classify as expressive). The current classifier does (b); the trade-off is granularity vs simplicity. Probably keep (b) for v1.

• Dynamic backend selection by data characteristics: e.g., “use DBSP if the input cardinality is over 10M; use SemiNaive otherwise.” Cost-based dispatch (v2) addresses this. Out of scope for v1.

• Modal + temporal interaction: when temporal qualifiers nest inside modal operators (or vice versa), the relevant tier is modal per §10.1. Which backend handles? KripkeExecutor in the design; verify when the temporal-substrate work track lands the temporal evaluator.

RFD 0004 — pub fact declarations

• State: discussion
• Opened: 2026-05-28
• Decides: surface syntax for declaring ground-truth facts (axioms) in source code; per-mode semantics relative to pub mutate; the relationship between source-declared facts and runtime-asserted facts in storage; how compile-time materialization (#[comptime] per RFD 0002) feeds on these facts.

Question

Today, ground-truth facts in an Argon system can only arrive at runtime via mutation invocation. The keystone test demonstrates this: there’s no way to write Person(alice) in source code; the only path is to call register(alice). Should Argon admit a source-level fact declaration syntax? If so, what’s the right surface, what’s the relationship to mutations and storage, and how does compile-time materialization fit?

Context

What the gap looks like today

pub kind Person; declares a concept. pub rel hasAge(p: Person, n: Nat); declares a relation. pub derive adult(p) :- Person(p), hasAge(p, n), n >= 18; declares a rule. Nothing in the current surface lets a modeler write Person(alice) or hasAge(alice, 25) as a fact. The only way to get those tuples into the store is to invoke a mutation at runtime.

This creates several problems:

1. #[comptime] is starved. RFD 0002 specifies compile-time materialization for derive rules. But the build-time engine has no facts to materialize against — every fact requires a runtime mutation call. The #[comptime] flag stamps on the rule body but the lifter has nothing to evaluate.

2. Test fixtures are awkward. The keystone test had to inject hasAge(p, 25) via a test-only helper because the only fact path was through mutation execution (which until this session didn’t bind integer args). Even after Value-typed mutation args landed, declarative tests want to express “given these facts” without runtime invocation gymnastics.

3. Bootstrap data is awkward. Real ontologies have built-in facts: standard units, well-known individuals, vocabulary mappings (e.g., the OWL stdlib’s rdf:type predicate; the temporal stdlib’s Second, Minute instances). Today these would need runtime mutation calls at startup. Source-level facts let them ship as part of the .oxbin.

4. The substrate’s “five atoms” model is incomplete without it. The five atoms (meta-calculus, construct, rule, trait, macro) describe declarations. But declarations alone don’t carry data — they describe shape. Facts ARE data; they should have a declarative surface.

What “fact” means semantically

A fact in Argon is an axiom event of kind iof_assertion, relation_tuple, meta_property, subsumption_axiom, or partition_axiom. Each is a positive ground proposition. Modelers writing source today can declare structure (concepts, relations) and behavior (mutations, derive rules) but cannot declare contents (ground propositions).

The minimal addition: surface syntax that emits these axiom events at build time. The .oxbin carries them just like mutation-emitted events. The reasoner sees them as live state. Compile-time materialization can finally run with input.

Decision

Surface syntax

pub fact Person(alice);
pub fact Person(bob);
pub fact hasAge(alice, 25);
pub fact hasAge(bob, 12);

The pub fact keyword sequence introduces a single ground proposition. Its body is exactly the same syntactic shape as a mutation’s insert operations — a predicate name followed by a parenthesized argument list. Each argument is either an identifier (interpreted as an Individual reference) or a literal (Int, Bool, Text).

Multiple facts can share a single declaration via a brace-delimited block:

pub fact {
    Person(alice);
    Person(bob);
    hasAge(alice, 25);
    hasAge(bob, 12);
}

This is purely a syntactic convenience — semantically identical to N independent pub fact declarations.

Identity allocation for fact arguments

When a fact references an identifier (alice, bob), the elaborator allocates a fresh IndividualId for it (per RFD 0001’s “individuals are system-allocated” rule). The mapping identifier → IndividualId is interned per workspace build, so:

• The same identifier mentioned in two pub fact declarations resolves to the same IndividualId.
• Different builds of the same source produce the same IndividualId (deterministic).
• Different identifiers (alice vs bob) get distinct IndividualIds.

The identifier itself becomes available for runtime lookup via the workspace’s symbol table — callers can pass Value::Individual(alice_id) to mutations or queries. (Today the runtime hashes the variable name for unbound parameters; this convention extends naturally.)

Per-axiom-kind semantics

The fourth row’s surface (pub fact A <: B) is shorthand for declaring subsumption outside a concept declaration’s <: clause — useful for late-binding or library-extension idioms. Initial implementation focuses on the first two rows; meta-property and subsumption shapes land when the broader §13 / §11 substrate matures.

Relationship to mutations

A pub fact declaration is equivalent to a mutation that runs at module load with no parameters. The compile-time-equivalent expansion:

// User writes:
pub fact Person(alice);
pub fact hasAge(alice, 25);

// Semantically equivalent to (but the compiler does NOT actually
// emit this; it emits the axiom events directly):
pub mutate __bootstrap_module() {
    insert iof(alice, Person);
    insert hasAge(alice, 25);
}
// + invocation of __bootstrap_module at module-load time

The advantages of NOT going through a synthetic mutation:

1. Directly content-addressed. The fact’s AxiomKey is BLAKE3-128(canonical_body), deterministic per RFD 0001. Mutations get fresh EventIds at invocation; facts get content-stable identity.
2. No runtime invocation needed. The .oxbin carries the events directly; the runtime sees them in Store::seed_from(&Module).
3. Compile-time materialization works. RFD 0002’s #[comptime] lifter finally has inputs.

Interaction with #[comptime]

After pub fact lands, the comptime lifter has a non-trivial path:

pub fact Person(alice);
pub fact Person(bob);
pub fact hasAge(alice, 25);
pub fact hasAge(bob, 12);

#[comptime]
pub derive adult(p) :- Person(p), hasAge(p, n), n >= 18;

At build time, the lifter:

1. Collects facts from pub fact declarations → catalog seed.
2. Runs the comptime rule against the seed.
3. Emits the derived tuples (adult(alice) in this case) as fresh iof_assertion / relation_tuple events with derivation provenance.
4. The runtime sees the derived facts directly; no re-evaluation needed.

Mutability + lifecycle

pub fact declares an immutable ground fact. The fact exists from module-load onwards. Retraction must go through:

• A mutation: pub mutate forget_alice() { delete iof(alice, Person); }.
• A retraction event at runtime (when the storage layer supports it).

The fact’s AxiomKey is content-addressed, so even after retraction the event log records both the assertion and the retraction. Replaying the log reproduces the lineage.

Diagnostic surface

• OE0210 FactReferencesUnknownConcept — pub fact Person(alice) where Person is not a declared concept.
• OE0211 FactArgArityMismatch — pub fact hasAge(alice) for a binary relation.
• OE0212 FactArgTypeMismatch — pub fact hasAge(alice, "twenty-five") where the relation expects Nat.
• OE0213 FactInsideFn — pub fact is a module-level declaration; not admitted inside function bodies, traits, etc.

Rationale

Why a new keyword fact, not overloaded syntax

Alternatives we ruled out:

• pub Person(alice); — overloads the visibility keyword. Reads ambiguously next to pub kind Person.
• pub iof alice : Person; — too low-level; exposes the wire-format axiom kind to the surface.
• #[fact] Person(alice); — attribute-driven, but attributes describe modifiers, not the kind of declaration. Confusing.

pub fact reads cleanly, parallels pub kind / pub rel, and is unambiguous about meaning.

Why allow block form

The block form (pub fact { ... }) is shorthand for repeated declarations. Real modules have lots of bootstrap facts (a stdlib of units, well-known individuals); writing 50 pub fact declarations vs. one block of 50 is just keyboard noise.

The block form’s semantic is identical to N independent declarations. No grouping invariants implied.

Why content-addressed AxiomKey, not synthetic mutation EventId

Two reasons:

• Determinism: same source → same .oxbin bytes. The fact’s identity comes from its content, not from a mutation’s invocation order.
• Lineage clarity: a pub fact declaration is a statement about reality, not an operation that “happens.” Treating it as an event with content-derived identity matches the modeler’s mental model.

Why immutable

pub fact describes ground truth as the modeler authored it. Allowing inline mutation (pub fact Person(alice); pub fact !Person(alice); — withdraw the prior?) would conflate declaration with operation. Cleaner: declarations are immutable; runtime mutations are the path for state change.

The .oxbin-resident facts can still be retracted by a mutation at runtime; the assertion + retraction live in the event log together.

Why not full datalog-style “extensional database” syntax

Some Datalog systems allow large facts via a separate file format (e.g., .csv of relation tuples, loaded by relation name). Argon could borrow this.

Rejected for the v1 surface: introduces a second source format with different rules. The same module would split between .ar (rules) and .csv (facts) — a coordination burden. pub fact keeps everything in one file format.

For very large fact sets (e.g., million-row knowledge bases), a tooling layer can pre-process external data into pub fact declarations. The language surface stays uniform.

Alternatives considered

Alt 1: No pub fact; require synthetic mutations

The modeler writes pub mutate bootstrap() { insert iof(alice, Person); } and a runtime layer calls it on module load.

Rejected: confuses operations (mutations) with declarations (facts). Every fact-heavy module would have boilerplate. The #[comptime] lifter would still need to recognize “this mutation is actually fact bootstrapping” — same problem at one layer of indirection.

Alt 2: data keyword (a la SQL)

pub data hasAge { alice = 25; bob = 12; }

Rejected: “data” overemphasizes table-shaped thinking. Argon facts can be heterogeneous (subsumption axioms, meta-properties); data reads like “tabular data only.”

Alt 3: Module-level expression syntax

pub Person(alice); at module scope (no leading keyword).

Rejected: parser ambiguity with function calls. pub would have to mean two different things depending on what follows; messy.

Alt 4: Inline in concept declarations

pub kind Person {
    instances: alice, bob, carol;
}

Rejected: couples instance enumeration to concept declaration. The whole point of separating concept from instance is that instances can be added without modifying the concept. Argon’s metatype model assumes this separation.

Consequences

Wire format

No new axiom kinds — pub fact emits existing iof_assertion, relation_tuple, etc. events. The wire format is unchanged.

Parser changes

New keyword FACT_KW. New FactDecl AST node parallel to ConceptDecl / RelDecl. ~50 LOC in grammar.toml + argon.ungrammar + oxc-parser/src/grammar.rs.

Elaboration changes

oxc-instantiate gains a lower_fact_decl similar to lower_concept_decl. ~100-150 LOC. The fact’s args resolve through the same SymbolTableBuilder as other declarations.

Identity allocation for fact-mentioned individuals

The SymbolTableBuilder gains an intern_individual(name) -> IndividualId method. The first mention of alice allocates a fresh IndividualId; subsequent mentions return the same one. Per-build deterministic.

Comptime lifter

Per RFD 0002, the comptime lifter materializes derive rules into fresh axiom events at build time. After pub fact lands, the lifter has facts to evaluate against. The lifter implementation can finally land.

Test ergonomics

Tests like the keystone become much cleaner:

#![allow(unused)]
fn main() {
let source = r#"
mod demo;
pub kind Person;
pub rel hasAge(p: Person, n: Nat);

pub fact Person(alice);
pub fact hasAge(alice, 25);

pub derive adult(p) :- Person(p), hasAge(p, n), n >= 18;
"#;
// ...load, query, assert. No mutation calls. No test helpers.
}

Open questions

• How are pub fact declarations sorted in the events section? Per the canonical-event-key sort, events sort by (tenant, fork, standpoint, kind, vt_start, tx_from). Facts get tx_from = 0 (declared at the workspace’s origin time)? Or do they get a deterministic tx_from derived from source position? The latter preserves source order; defer to implementation.

• Can pub fact reference future-declared symbols? pub fact Person(alice); followed by pub kind Person; — does this work? Symmetric to how derive can reference forward-declared concepts. Default: yes; the elaborator does a single AST walk and resolves all references. Concrete error case: pub fact UnknownConcept(alice); → OE0210.

• pub fact inside mod blocks — pub mod sub { pub fact ... } admits per-submodule fact scoping. Symbol resolution follows module visibility rules (per §3.1). No special handling beyond what’s already established.

• Bulk-load tooling — for million-row fact sets, a CLI/tooling story is needed. Out of scope for the language surface; addressable post-MVP.

• Interaction with standpoint scoping — when standpoints are surfaced, a fact in standpoint X is only visible in X (and its supertypes per FDE info-join). Defer to the standpoint substrate work track.

• Negative facts / classical negation — pub not_fact Person(alice) to assert that alice is not a Person. Useful in OWA / classical contexts; relates to §12.2’s Truth4 bilattice. Defer; orthogonal to this RFD’s positive-only scope.

RFD 0005 — Relation subsumption

• State: committed
• Opened: 2026-05-28
• Decides: surface syntax for declaring that one relation subsumes another; the elaborator checks (endpoint covariance, cardinality refinement, metarel compatibility); the substrate impact; whether Argon adopts UML’s three-mechanism (subsetting / redefinition / specialization) story or collapses it into a single mechanism.

Question

Today, <: is a substrate-level subsumption operator admitted only on concept declarations (pub kind Adult <: Person). The substrate’s SubsumptionAxiomBody is generic over sub_id/super_id and would accept relation IDs without modification, but the surface grammar (§5.3 rel-decl) has no <: clause and the elaborator has no relation-side covariance machinery. Should Argon extend <: to relations? If so, what does the surface look like, what does the elaborator check, and how does this interact with UML’s three property-specialization mechanisms?

Context

Concrete modeler demand

The driving case (Luiz Almeida, 2026-05-28 design thread): a temporal-substrate model needs a sub-relation whose endpoints narrow and whose tuples flow into the parent.

pub type TimePoint <: TimeInterval;
pub type AbsoluteTimePoint <: TimePoint;

pub type TimeScale {
    timePoints: [TimePoint] from timeScaleHasTimePoint.range,
}

pub type IndefiniteTimeScale <: TimeScale {
    timePoints: [AbsoluteTimePoint]
        from indefiniteTimeScaleHasAbsoluteTimePoint.range,
}

pub rel timeScaleHasTimePoint(domain: TimeScale, range: TimePoint) [1] [1..*];
pub rel indefiniteTimeScaleHasAbsoluteTimePoint(
    domain: IndefiniteTimeScale,
    range:  AbsoluteTimePoint,
) [1] [1..*];

The intent: every tuple of indefiniteTimeScaleHasAbsoluteTimePoint is also a tuple of timeScaleHasTimePoint. Today there’s no way to express this; the modeler has to write a derive rule by hand, losing the structural property and the elaborator’s covariance check.

Substrate readiness

oxc-protocol::storage::SubsumptionAxiomBody:

#![allow(unused)]
fn main() {
pub struct SubsumptionAxiomBody {
    pub sub_id:   uuid::Uuid,    // generic — accepts concept or relation IDs
    pub super_id: uuid::Uuid,
}
}

The reasoner’s subsumption-closure logic (oxc-reasoning) parameterizes over symbol kind by construction. The substrate is ready; the surface and elaborator aren’t.

Parser asymmetry (the load-bearing gap)

oxc-parser/src/grammar.rs::concept_or_rel_decl already calls supertype_clause on the concept branch (lines 608–609), parsing <: via the existing LT_COLON / SPECIALIZES_KW machinery. The rel branch (lines 599–605) does not. The grammar’s SupertypeClause node is shared. Extending <: to relations reuses existing parser infrastructure; it does not introduce new syntax.

Argon’s existing position on shadowing and override

Three spec rules constrain the design space:

1. §3.4 name resolution does not walk <: chains. Resolution order is local → imports → auto-prelude → primordials. Verified in oxc-resolver/src/resolve.rs:207–255 — resolve_path walks module prefixes only.

2. §5.4 impl Type namespaces members as Type::name. Relations declared inside impl Person are reachable only as Person::ParentOf, not at module level. Verified in oxc-resolver/src/symbols.rs:57 — Item::ImplBlock(_) => return None. Impl-block contents don’t register top-level symbols.

3. §5.2 explicitly forbids implicit override. OE0206 InstantiationFieldShadows rejects iof-axis shadowing; OE0208 AmbiguousFieldFromMultipleParents rejects diamond ambiguity. Verbatim: “The substrate offers no automatic merge, override-by-position, or last-wins behavior — every collision is resolved explicitly.”

These three together eliminate the namespace problem UML’s {redefines} exists to solve: in Argon, Manager::subordinate and Employee::subordinate are already distinct qualified paths from the start.

UML’s three mechanisms and how they map

UML needs three mechanisms because UML conflates extent-level subsumption with namespace-level shadowing AND assumes properties propagate through the class hierarchy by name. Argon decouples all three concerns. One surface mechanism (<: on rel-decl) covers all three UML cases.

Decision

Surface

Extend rel-decl to admit a <: (or specializes) clause after the cardinality list:

rel-decl ::= attribute* 'pub'? <metarel-name> Ident generic-params?
              rel-param-list cardinality-list?
              supertype-clause?           // NEW
              rel-body? ';'?
supertype-clause ::= '<:' TypeExpr (',' TypeExpr)*
                  |  'specializes' TypeExpr (',' TypeExpr)*

The clause applies uniformly across every metarel-introducing keyword (rel, material, mediation, formal, …) — the production is shared with concept-decl’s supertype clause, identical to how SupertypeClause is currently defined in the ungrammar.

pub rel indefiniteTimeScaleHasAbsoluteTimePoint(
    domain: IndefiniteTimeScale,
    range:  AbsoluteTimePoint,
) [1] [1..*]
    <: timeScaleHasTimePoint;

Semantics

R1 <: R declares: every tuple of R1 is also a tuple of R. The reasoner’s subsumption-closure auto-derives

R(a₁, …, aₙ) :- R1(a₁, …, aₙ).

without an explicit derive rule. Queries against R see R1’s tuples; queries against R1 see only R1’s tuples.

Elaborator checks at the <: clause

1. Arity equality. R1 and R must have the same parameter count. Mismatch → OE0150 RelationSubsumptionArityMismatch.

2. Endpoint covariance. For each position i, R1.param[i].type <: R.param[i].type. Mismatch → OE0151 RelationSubsumptionEndpointVariance.

3. Cardinality refinement. For each slot i, R1.cardinality[i] must be no looser than R.cardinality[i]. Formal rule: [c..d] refines [a..b] iff c ≥ a and (d ≤ b or b = *). Mismatch → OE0152 RelationSubsumptionCardinalityViolation.

4. Metarel compatibility (MVP rule). meta(R1) == meta(R). Same metarel on both sides. Mismatch → OE0153 RelationSubsumptionMetarelMismatch. Cross-metarel subsumption (e.g., material <: formal if a vocabulary declares a metarel lattice) is deferred — see Open Questions.

5. Acyclicity. The relation subsumption graph must be acyclic. R1 <: R1 (direct or transitive) → OE0154 RelationSubsumptionCycle. Enforced by the same acyclic-DAG check used for concept subsumption.

Substrate impact

Zero new axiom kinds. The subsumption_axiom event with sub_id = R1’s NameRef and super_id = R’s NameRef carries the fact. The reasoner’s existing concept-subsumption closure generalizes by parameterizing over the symbol kind — relations are looked up via the same RelationCatalog machinery already used for storage.

Reasoner impact

oxc-reasoning::SemiNaiveExecutor extends its subsumption-closure pass to relation IDs. The existing concept-closure is parameterized on a SymbolKind enum; the implementation lifts the same Floyd-Warshall-style transitive closure over the subsumption DAG. Cost: O(|relations| · |subsumption_edges|) at module load.

Field-view propagation

A field declared via field: [T] from Rel.endpoint projects from Rel. When R1 <: R, a subtype concept may declare a field projecting from R1:

pub type TimeScale {
    timePoints: [TimePoint] from timeScaleHasTimePoint.range,
}
pub type IndefiniteTimeScale <: TimeScale {
    timePoints: [AbsoluteTimePoint]
        from indefiniteTimeScaleHasAbsoluteTimePoint.range,
}

The two fields are distinct projections per-concept; they share a name but live in different qualified namespaces (TimeScale::timePoints vs IndefiniteTimeScale::timePoints). Access from a TimeScale-typed binding projects the broader field; access from an IndefiniteTimeScale-typed binding projects the narrower one. Subsumption-closure ensures the narrower field’s tuples appear in the broader field’s view via the underlying relation <:.

Rationale

Why one mechanism, not three

UML’s {subsets} + {redefines} + implicit specialization is the right modeling vocabulary for a language whose properties propagate by name through the class hierarchy. Argon does not have that propagation:

• Name resolution doesn’t walk <:.
• impl Type namespacing creates distinct qualified paths from the start.
• §5.2 forbids implicit override.

Given these three, UML’s {redefines} solves a problem Argon doesn’t have. A subclass that wants to “redefine” a parent’s property declares its own relation in its own qualified namespace; the relation-level <: carries the extent containment; the modeler accesses through whichever qualified path is appropriate. No additional mechanism is required.

Why extend <: (not introduce a new operator)

The substrate’s subsumption relation is uniform across symbol kinds (concepts, relations, standpoints) — SubsumptionAxiomBody is already generic. Using <: consistently preserves that uniformity at the surface. Introducing a new operator (e.g., subsets, >:, #[subsets(...)]) would imply the substrate distinguishes mechanisms it does not in fact distinguish.

Why same-metarel for MVP

A vocabulary may eventually declare metarel-level subsumption (material <: formal); when that lands, the elaborator’s metarel-compatibility check follows the metarel lattice. For MVP, conservative same-metarel-required keeps the elaborator simple and matches the most common use cases. The conservative rule generalizes monotonically — relaxing it later does not break any existing models.

Alternatives considered

A. Three-mechanism mirror of UML

Add <: for subsetting AND a separate #[redefines(Parent::rel)] attribute (or redefines keyword) for namespace shadowing. Rejected. Argon’s name resolution + impl Type scoping eliminate the shadowing problem; a redefines mechanism would address a non-problem. Adds language surface for no semantic gain.

B. Implicit subsumption from endpoint typing

When a pub rel R1 has endpoints <: R’s endpoints, automatically infer R1 <: R. Rejected. Conflicts with Argon’s “no implicit override” policy (§5.2). Modeler intent must be explicit; covariant endpoint types alone do not signal a desire for tuple flow into the parent.

C. Derive-rule expansion

Tell modelers to write pub derive R(a, b) :- R1(a, b); by hand. Rejected. Loses the structural property (no covariance check), bloats the module with boilerplate, and gives the optimizer no opportunity to specialize storage layout for subsumption-closed relations.

D. Defer entirely to a follow-on

Don’t extend <: to relations now; revisit when more pressure builds. Rejected. The substrate already supports it. The grammar gap is forcing modelers (Luiz, OntoUML imports) to work around. The cost of landing is small (~1–2 days of focused work). Deferring accumulates technical debt and modeler confusion.

Consequences

What lands

What modelers gain

• Direct expression of UML {subsets} and OntoUML’s relation specialization patterns.
• Property narrowing in subtypes via paired relation+field declarations.
• Cleaner OntoUML import path (relation subsumption is a first-class OntoUML construct).
• Elaborator-verified endpoint covariance and cardinality refinement at declaration sites.

What modelers do NOT gain

• A separate redefines mechanism — Argon doesn’t need one (see Decision).
• Implicit override semantics — same name without <: remains unsupported; explicit qualification is the modeler’s tool.
• Cross-metarel subsumption (MVP) — initially restricted to same-metarel; lifted when metarel-lattice support lands.

Compatibility

Pure addition. No existing code changes behavior; the new clause is optional and absent in all today’s source. The subsumption_axiom wire format is unchanged.

Open questions

OQ1 — Field-level same-name across <:

When B <: A, both declaring a same-named field whose projection comes from <:-related relations (Luiz’s case), §5.2 has no explicit rule. Three readings:

• Permissive: allow whenever the underlying relations are in a subsumption relationship; the field views inherit the connection transitively.
• Strict: flag as shadowing per §5.2’s no-implicit-override policy; require explicit Parent::field qualification.
• Inherit the relation’s signal: treat the relation-level <: as the modeler’s explicit acknowledgment; no field-level signal required.

Recommend the third reading as the cleanest extension of §5.2 — the relation’s <: carries the intent through to the derived field views, no new field-level mechanism needed. Confirm before implementation.

OQ2 — Metarel lattice

Should metarels themselves admit <: (e.g., metarel material <: metarel formal in a vocabulary)? UFO’s relation taxonomy is layered; a vocabulary might want to express that material relations are a kind of formal relation. Deferring to a follow-on RFD; the conservative same-metarel rule in this RFD is forward-compatible.

OQ3 — N-ary relation subsumption

The covariance check (R1.param[i].type <: R.param[i].type for each i) generalizes to n-ary relations trivially. Verify the elaborator’s covariance pass handles ternary and higher relations without special-casing. Unlikely to be a problem — the per-position check is uniform — but the test suite should cover ternary cases explicitly.

OQ4 — Interaction with from Rel.endpoint field-view cardinality

When R1 <: R and a subtype declares a field f: [T] from R1.endpoint, what cardinality bound applies to f? The narrower relation’s slot bounds, or the broader’s? The narrower’s, almost certainly — the field is projecting from R1, not R — but verify the existing field-view elaboration respects this.

References

• §3.4 (name resolution), §5.2 (concept supertype clauses, OE0206/OE0208), §5.3 (relations), §5.4 (impl Type) — spec/reference/src/
• oxc-protocol/src/storage.rs:574–578 — SubsumptionAxiomBody
• oxc-resolver/src/{resolve.rs, symbols.rs} — name-resolution implementation
• oxc-parser/src/grammar.rs:599–672 — concept/rel decl parser and supertype_clause
• oxc-syntax/argon.ungrammar — typed AST shapes
• UML 2.5.1 §9.5 (Properties; subsetting and redefinition)
• Carvalho, V.A., Almeida, J.P.A., Guizzardi, G. (2017). Multi-level ontology-based conceptual modeling. Data & Knowledge Engineering 109, 3–24 — for the OntoUML relation-specialization patterns this RFD enables on import.

RFD 0006 — Field mutability via mut

• State: discussion
• Opened: 2026-05-28
• Decides: surface syntax for opting a field into post-construction updatability; the implicit default for non-annotated fields; the interaction with #[intrinsic], from-clauses, refinement, and metatype rigidity; how update-stmt becomes the only legal write path; the lowering to append-only event pairs; the elaborator checks and diagnostic codes.

Question

Argon’s spec today has no field-level mutability discipline. Every non-derived field is implicitly mutable via the update-stmt grammar (§7.5:306). This contradicts the rest of the architecture — the substrate is value-semantic with no borrows (§7:26), .oxbin is content-addressed and immutable (§19), the event log is append-only (§20.1), and the Lean State.lean + Fixpoint.lean prove information-monotonicity. Should Argon admit a field-level mutability marker (mut), what’s the default, and how does it interact with the existing modifiers?

Context

Today’s effective semantics

• field-decl ::= attribute* Ident ':' TypeExpr ('=' expr)? ('from' relation-ref)? (§5.1:18). No mutability slot.
• update-stmt ::= 'update' (Ident | pattern) 'set' '{' field-assign (',' …)* '}' ('where' expr)? ';' (§7.5:306). Any field may appear in field-assign.
• Worked example (§7.5:334): update c: Company set { name = new } — name is implicitly updatable.
• #[intrinsic] is an attribute (not a keyword) declaring that a field must be set at kind level by every iof-instance (§5.1:135, §10.2:57). It governs construction-time required-ness, not post-construction mutability. A field can be both #[intrinsic] and (today) implicitly updatable.

What’s opt-out from mutability today

• Refinement-determined classification (§7.5:357) — the substrate derives membership; explicit insert iof rejected with OE0211 IofInsertOnRefinedType.
• Rigid metatype classification (§7.5:356) — kind / subkind / category individuals can’t be re-classified; insert iof / delete iof rejected with OE0210 IofInsertOnRigidType.
• from-derived fields (§5.1:18) — value comes from a relation projection; not directly assignable.
• Architectural — .oxbin, Module, Engine (§19); axiom_events only grows via append (§20).

The genuine gap

There is no language for “field that is set at construction (or by #[intrinsic] binding, or from-derived) and may not be subsequently updated.” Modelers write pub kind Person { name: String, dob: Date, current_address: Text } with no way to say “name and dob are set-once; only current_address changes.” Today’s update-stmt admits writes to any of them.

The Argon vault’s open-questions doc (Efforts/On/Argon/scratch/open-questions response.md #18) names this verbatim: “Mutability annotations. No grep hit for mut/const/#[mut] on properties. Likely absent. Tied to #19 (change patterns). Genuine gap.”

mut is available

Per appendix-a:6-18, mut is not in the reserved keyword list. The mutation-related reserved words are mutate, insert, delete, update, upsert, detach, forget. Adding mut is a non-conflicting lexer change.

Decision

Surface

mut is a field-declaration modifier. Without it, fields are set at construction (or via #[intrinsic] kind-level binding, or by from-clause derivation) and immutable thereafter. With it, a field admits writes via update-stmt inside mutate bodies.

pub kind Person {
    name: String,                   // set at construction; not updatable
    dob: Date,                      // set at construction; not updatable
    #[intrinsic] ssn: Text,         // must be set at kind binding; not updatable
    mut current_address: Text,      // updatable post-construction
    mut current_employer: Company?, // updatable, optional
    #[intrinsic] mut current_role: EmploymentRole,  // both: required at construction, updatable later
}

pub mutate move(p: Person, addr: Text) {
    update p set { current_address = addr };       // OK
    // update p set { name = "Bob" };              // OE0820: name is not `mut`
}

Updated grammar

field-decl ::= attribute* 'mut'? Ident ':' TypeExpr ('=' expr)? ('from' relation-ref)?

Order: attribute* mut? Ident. Attributes precede mut; mut precedes the identifier. This places mut adjacent to the field name where its scope is most visible.

Defaults

• A non-mut field is immutable post-construction.
• A mut field is mutable post-construction.
• A from-derived field is always derived (not directly assignable); mut on a from-derived field is rejected with OE0822 MutOnDerivedField.
• A field with #[intrinsic] is required at construction; orthogonal to mut.

Lowering

Field mutations lower to append-only event pairs on the underlying axiom. A mutate body with update p set { current_address = "new" } emits:

1. A retract event (Polarity::Retract) on the prior property_assertion row whose body is { entity_id = p, property_id = NameRef(current_address), value = "old" }. The retract event’s asserts_axiom points to the prior assert’s EventId.
2. A new assert event (Polarity::Assert) on the new property_assertion row whose body is { entity_id = p, property_id = NameRef(current_address), value = "new" }.

Both share the same content-addressed AxiomKey for the proposition “p has current_address X” — the proposition’s identity is the property assertion’s logical content; the value is what changes. Per RFD 0001, AxiomKey is BLAKE3-128(canonical_body), so old and new have distinct AxiomKeys but the same (entity_id, property_id) pair identifies them as alternative assertions of the same property.

Elaborator checks

• OE0820 UpdateImmutableField — update e set { f = expr } where f is not mut. Caller is the update-stmt elaborator.
• OE0821 MutOnRefinementDerivedField — reserved; not yet emitted (refinements are concept-level today, not field-level; this exists in case refinement gains field-level derivation later).
• OE0822 MutOnDerivedField — mut f: T from rel.range. The from-clause already determines the value; mut is contradictory.
• OE0823 MutOnRelationTupleField — reserved for Form B/C relation tuple bodies whose intrinsic fields may want their own mutability discipline; nail down when relation-tuple updates land.

Interaction with the four orthogonal axes

The four existing constraint axes plus mut form a clean matrix:

Same commit ships update-stmt

The update-stmt grammar (§7.5:306) is reserved but unimplemented in the parser/lowerer/runtime today. mut is a no-op without update. The implementation of this RFD ships:

1. Parser: update statement parsing (§7.5:306 + 307).
2. Lowerer: update lowers to a new Operation::Update core_ir variant which expands to retract+assert event pairs at runtime.
3. Elaborator: rejects update p set { non_mut_field = ... } with OE0820.
4. Runtime: execute_mutation’s operation interpreter handles Operation::Update.

Local let mut is OUT OF SCOPE for this RFD

The §7.5:293 'let' Ident (':' TypeExpr)? '=' expr ';' grammar has no rebind form. A let mut x = ...; x = ... local-rebind story is meaningful but deferred to a follow-up RFD when the mutate-body language grows expression-level computation needs. The current RFD only addresses field mutability on declarations.

Rationale

Why immutable by default

Three reasons:

1. Aligns the surface with the substrate. Argon is content-addressed, append-only, value-semantic. Implicit field mutability is the one surface-level dissonance with the rest of the architecture. Making mutability opt-in restores coherence.

2. Forces modelers to identify stable attributes. Real ontologies have a sharp distinction between identity-bearing attributes (birth date, SSN, kind classification) and contingent attributes (current address, status, balance). Today’s syntax doesn’t make this visible. mut-by-default would have been a research-friendly default but explicit-opt-in matches the Mercury / Rust / Haskell tradition: types tell you what’s mutable.

3. Pairs with the rest of Argon’s modeling discipline. #[intrinsic] says “must be set”; from says “is derived”; <: says “is subsumed by”; refinement says “is constrained by.” Adding mut says “may change post-construction” — slots into the same pattern. No mut ⇒ no post-construction change.

Why keyword over attribute (mut vs #[mut])

Three considerations:

• Visual prominence. Mutability affects how the field participates in mutations; it’s a first-class semantic property, not metadata. Keyword form (pub mut current_address: Text) signals this; attribute form (#[mut] current_address: Text) reads as decoration.

• Consistency with rest of the surface. pub, from, where, :, = are all keyword-shaped in field declarations. #[intrinsic] is an attribute because it’s a kind-level constraint (governs the binding site), not a value-level property. mut is value-level. Keyword fits.

• Frequency of use. Field declarations are common; mut will appear often. Keyword form is shorter (3 chars + space vs 8 chars + space).

Why ship update-stmt with mut

The update keyword is reserved but the parser doesn’t recognize it; the lowerer doesn’t emit Operation::Update. Without it, mut is a marker that nothing reads. Two reasons to ship together:

• Coherent surface. Modelers learn mut and update together as a unit. Documentation lands as one chapter, not two halves separated by a release.
• End-to-end testable. A pub_fact_keystone analog with pub mutate move(p: Person, a: Text) { update p set { current_address = a }; } followed by a query_derive proves the full path.

Why orthogonal mut × #[intrinsic]

The two govern different lifecycle points:

• #[intrinsic] — “must be specified by every iof-instance at kind binding”
• mut — “may be re-assigned post-construction by update-stmt”

A real ontology pattern: #[intrinsic] mut employment_role: Role — every employee has a role from day one, and the role can change as they’re promoted. Forcing them to choose between “intrinsic” and “mutable” is a false dichotomy.

Why no let mut in this RFD

The mutate-body statement language (§7.5:293-313) is currently minimal: let, match, insert/update/delete/upsert/detach/emit, for, if, expr;. Local rebinding is interesting but isolated — it doesn’t interact with the field-mutability story. Treating it separately lets the field-mutability discussion stay focused.

Alternatives considered

Alt 1: mut as documentation only (β from the design discussion)

Keep current “any field is implicitly updatable” semantics. Use mut as a documentation marker driving tooling (audit, indexes, change-notification).

Rejected: doesn’t close the gap the vault names. Adds noise without changing semantics. The whole virtue of mut is forcing modelers to identify which attributes change.

Alt 2: mut for non-field axes only (γ)

Skip field-level mutability; use mut for pub mut concept (concept-level opt-in to state change) or pub mut rel (relation-level opt-in to tuple update).

Rejected: pub mut concept is redundant with metatype-driven rigidity (role is already anti-rigid). pub mut rel is interesting (insert/delete vs update) but is a smaller question than field mutability and can be addressed via a future RFD once relation-tuple intrinsic-field semantics solidify.

Alt 3: Attribute form #[mut]

Use #[mut] instead of mut. Composes with the existing attribute machinery; parallel to #[intrinsic].

Rejected as primary surface. Considered seriously; the keyword form wins on visual prominence + consistency with pub / from (other field-decl keywords). Attribute form might be admitted as an alias if grep-friendly attribute scanning becomes valuable, but the canonical surface is the keyword.

Alt 4: Tri-state: mut / default / const

Add both mut (mutable) and const (set-at-construction-then-frozen) with default being “construction-time once, kind-level once, no other constraint.” (const is already reserved per appendix-a:8.)

Rejected: the three-state design is more expressive but adds modeler load. The current architectural decision is “default to immutable; opt-in to mutability via mut.” const stays reserved for compile-time-known-value semantics if/when that landing strip becomes necessary.

Alt 5: Per-field via update rule mode

Instead of marking the field, mark the mutate body: declare which fields the body may touch via a frame clause. Closer to TLA+ / Reiter SSA semantics.

Rejected: heavier syntax. Real-world ontology workflows have many small mutations touching one field each; per-mutate-body declaration would multiply boilerplate. Field-level marker is more direct.

Consequences

Wire format

property_assertion events already carry an EventId and the body. Adding mut doesn’t change the wire format — the runtime emits retract+assert event pairs as it would for any other mutation. The field-decl’s mut marker is part of the concept/struct/etc. declaration’s wire body and rides along.

core_ir

Operation enum (today: InsertIof, DeleteIof, InsertTuple, DeleteTuple, Forget) gains:

#![allow(unused)]
fn main() {
Operation::Update {
    entity: Term,
    assigns: Vec<FieldAssign>,
    where_clause: Option<Term>,
},
}

Plus the FieldAssign shape: { field_name: String, op: AssignOp, expr: Term } where AssignOp is Set | AddSet | SubSet (for =, +=, -=).

Parser

• New mut keyword recognized at the lexer level (added to grammar.toml’s keyword list).
• field-decl parser admits optional mut token between attributes and the ident.
• update-stmt parser implements §7.5:306 including where clause.

Elaborator

• lower_concept_decl / lower_struct_decl walk field declarations; carry mut flag through to wire body (ConceptDeclBody.fields[i].mut_flag or similar — TBD when the field body wire shape solidifies).
• lower_mutate_body recognizes update-stmt, produces Operation::Update.
• Elaborator checks (OE0820, OE0822) emitted during update-stmt lowering.

Runtime

execute_mutation’s operation interpreter gains a Operation::Update arm:

1. For each FieldAssign, evaluate the expr against the current state.
2. Look up the prior property assertion event for (entity, field_name).
3. Emit a retract event for the prior + assert event for the new.

Diagnostics

Three new codes in grammar.toml, propagating to oxc-diagnostics::generated.rs + appendix-c-diagnostic-codes.md:

• OE0820 UpdateImmutableField — update e set { f = expr } where f lacks mut.
• OE0821 MutOnRefinementDerivedField — reserved; not yet emitted.
• OE0822 MutOnDerivedField — mut f: T from rel.range is contradictory.

Spec migration

The spec’s worked examples need updating. Specifically:

• §7.5:334 update c: Company set { name = new } — either annotate name as mut or rename the example to use a field that’s plausibly mut.
• §21 walking example: review for any field updates and add mut annotations.

Lean

Argon/Syntax/Decl.lean (field-decl) gains a mut: Bool field. Argon/Storage/AxiomBody.lean doesn’t change (property assertions are already individual axiom events; the retract+assert lineage is already in Polarity + asserts_axiom). Argon/TypeSystem/FlowTyping.lean may need refinement of the immutability assumption to “non-mut fields stay immutable across mutation”; the proof obligation is small (per-field discipline rather than blanket immutability).

CI drift gate

field-decl’s Lean inductive carries mut: Bool; the matching Rust struct in oxc-protocol::storage::FieldDecl (or wherever fields are wire-typed) must include it. CI drift check covers this.

Open questions

• Should mut admit += / -= only on numeric types? §7.5:307 field-assign allows =, +=, -=. For text fields current_address += "..." is ambiguous (string concatenation? error?). Lean toward: += / -= admitted only when the field’s type implements the arithmetic ops (Nat, Int, Real, Money, Duration). Resolve when the trait system covers numeric op overloading.

• mut on collection fields: pub mut friends: List<Person> — does mut admit both update p set { friends = [...] } (replace) and insert p.friends(other) (push)? Probably both, but the semantics need pinning down when collection-field mutation lands.

• mut on relation tuple bodies (Form B/C): a relation declared with intrinsic property body (§5.2 Form C) carries its own fields. Do those fields admit mut? Almost certainly yes, with the same defaults — but the syntactic surface (pub rel hasJob(p: Person, c: Company) [1] [1..*] { mut salary: Money }) needs validation. Reserved as OE0823.

• Interaction with #[brave] / stable models (§7.8): mut writes happen at runtime; brave-derived facts at build time. The two don’t collide today but if a #[brave] rule references a mut field’s prior value, the rule’s stratification needs to account for the temporal axis. Defer to when brave rules see real use.

• Update via partial assignment: update p set { current_address = ..., current_employer = ... } — atomic both-or-neither, or sequential? Today’s transactional semantics of mutate bodies suggests atomic; the elaborator emits the retract+assert event pairs in a single mutation transaction. Confirm when the runtime’s transaction semantics formalize.

• Identity-preserving field mutation: when a mut field changes, the entity’s IndividualId stays the same (RFD 0001). The AxiomKey for the property changes (content-addressed). Confirm the MutationReceipt shape adequately captures the lineage for downstream consumers (provenance witnesses, audit logs).

• Should pub fact (RFD 0004) be able to set a mut field at construction? pub fact Person(alice) { current_address: "..." } — yes, presumably, since this is construction-time assignment, not post-construction update. The fact-decl grammar in RFD 0004 doesn’t yet have a body form for setting fields; add when needed.

RFD 0007 — Missing-value semantics under OWA

• State: discussion
• Opened: 2026-05-28
• Decides: what field: T (required), field: T? (optional), and field: Truth4Of<T> (epistemic) each mean under CWA and OWA; what happens when the value isn’t asserted; how Option<T> lifts (or doesn’t) inside rule-body comparison atoms; the diagnostic surface that forces the modeler to pick an intent rather than guess one.

Question

Argon today lets a modeler write pub kind Person { age: Nat? }. What does the ? mean? Two readings, both defensible, both produce different rule-evaluation outcomes:

• Reference-ontology reading. Some persons genuinely have no age — the field’s absence is a positive fact about the world. None is on a par with Some(0) as a piece of information.
• Implementation reading. Every person has an age, but the KB may not yet record it — the field’s absence is epistemic uncertainty. None means unknown, not no age.

The OWL/SHACL ecosystem keeps these apart by treating cardinality (owl:FunctionalProperty, sh:minCount) as TBox/SHACL-shape declarations and treating ABox-incompleteness as a property of the knowledge graph, not of the property. Argon, today, conflates them: T? is the only surface, the spec doesn’t say which intent it expresses, and §5.1 line 42 — “yield Option::None if the field’s declared type is T?, else error” — forces modelers to reach for T? whenever the KB might be incomplete, even when the modeler means the implementation reading. That’s a real loss of expressivity, and it forces the rule-evaluation semantics to invent an ad-hoc lift rule for Option<T> >= T that the spec never actually specifies.

This RFD picks the semantics, picks the surface, and documents the elaborator’s lifting discipline.

Context

The motivating thread (Almeida + Almeida, 2026-05-28)

Gustavo Ladeira (Sharpe) asked:

pub kind Person { age: Nat? }

pub derive Adult(p: Person) :- p: Person, p.age >= 18;
pub derive Minor(p: Person) :- p: Person, not Adult(p);

“In OWA, can a derive resolve to CAN? Does p.age >= 18 lift to Can if age isn’t present? And then is not Adult(p) for a person with no age Is(true) (so Minor fires erroneously) or Can (so Minor stays unknown)?”

João Paulo Almeida (UFES) sharpened the framing:

“There is a key issue here to flesh out. Optionality in this form (in an implementation) is usually ambiguous. If we are building a reference ontology (about the world), an optional age would mean there [are] people without age (so, this would be a bad modeling choice). But when this is about an implementation, we’d also like to know whether within the knowledge base this information (about age) is optional. In the RDFS/OWL world, this is partially addressed with age being a functional data property (thus every person has an age even though we might not know it), and then might be SHACL constraints to clarify whether the knowledge graph must have information about age.”

JPA’s distinction is the question this RFD answers.

What the substrate already mechanizes (and what it doesn’t)

Foundation/Truth4.lean + Foundation/Projection.lean mechanize the bilattice Truth4 = {Is, Not, Can, Both} and the Pietz–Rivieccio Exactly-True projection. Reasoning/Fixpoint.lean is K3-aware: rule-body conjunction (§6.10.5 truth table) and Kleene negation (¬Is = Not, ¬Not = Is, ¬Can = Can) are the operators the stratified fixpoint already uses.

§6.9 verbatim: “The substrate enforces this by lifting the derive/query evaluation into Truth4 under OWA and projecting to Boolean only at refinement membership / if / match boundaries.” §12.2 verbatim: “Boolean projections: Can → false. Only Is(true) is designated.”

What the substrate does not specify:

1. How field: T under OWA behaves when no value is asserted. §5.1 line 42 says “error.” But the OWL functional-property pattern — every Person has an age; the KB may not know it — requires this to lift to Can, not error.

2. How Option<T> comp_op T evaluates in a rule-body atom. No rule. Today the elaborator type-errors, the parser accepts it, and the runtime would have to invent a coercion. The Gustavo trace above implicitly assumed None >= 18 lifts to Can; that assumption isn’t anywhere in the spec.

3. Whether structural-optional and epistemic-optional have separate surfaces. §6.6 says T? ≡ Option<T>. That’s the structural reading. The implementation reading currently has no surface — and §5.1’s “else error” forecloses it.

Three real gaps. JPA’s question lands on all three.

OWL / SHACL precedent

The reference systems handle JPA’s distinction with separation of concerns:

• TBox (OWL). Cardinality declarations (owl:FunctionalProperty, owl:minCardinality, owl:maxCardinality) state what is true of the world: every Person has an age. ABox-incompleteness does not contradict TBox cardinality under OWA — it means the missing fact is unknown.
• SHACL shapes. Constraints over the knowledge graph (sh:minCount, sh:maxCount, sh:datatype) state what must hold of the KB. A SHACL violation means the KB is incomplete, not that the world is malformed.

Argon’s existing machinery already has the analogous parts:

• TBox-cardinality analog. Field declarations on concepts. age: Nat says every Person has an age (OWL functional + min 1). age: Nat? says some Persons may genuinely lack an age.
• SHACL-shape analog. where { … } refinement clauses (§6.3) and #[intrinsic] (§5.2). These constrain the KB, not the world.

The pieces are in place. What’s missing is the lift discipline that connects them under OWA.

Decision

Decision pending ratification (2026-06-12, PR #289). This RFD is in discussion state, and its OE1014 story (Decision table row 1 / the lift rule below) places the required-field-completeness diagnostic at field-access / evaluation time — a query reading an unasserted required field under CWA is the schema violation. PR #289 needed a completeness gate for the insert iof(x, T) classification side-door (audit ufo-mut-06), and shipping the evaluation-time emitter is a larger build (it lifts every required-field read into a CWA cardinality check). So #289 decides and implements a narrower, complementary site: an in-body-vs-staged discriminator at commit time. A mutate body that classifies x into T and writes fields of x in the same body is constructing x in-body; completeness is judged at body end (read-your-writes, RFD 0019 RC2) and OE1014 refuses atomically if a required field is left unset. A body that only classifies — no in-body field writes to x — is staged construction and is permitted to defer (this RFD’s “ABox-incompleteness is fine”); it currently produces no diagnostic. Rationale: a blanket write-time / construction-time refusal would break staged construction across mutations (the legal_norms_can_vote::register and keystone add_sat → set_cap patterns), which this RFD explicitly blesses; keying on whether the same body populates the individual is the discriminator that lets both shapes stay green. This is a fresh design decision owned by #289, not a clause this RFD already settled — the RFD specifies the opposite site (field-access). The field-access-time / evaluation-channel emitter (Decision table row 1 CWA column, the lift rule’s state lacks ... CWA → OE1014 line) remains the open half of this RFD and is unbuilt; it is tracked at #292, and this RFD still needs ratification to lock both halves.

Three surfaces, three distinct intents

These three surfaces correspond exactly to JPA’s distinction (rows 1+3 are the implementation reading; row 2 is the reference-ontology reading), plus an escape hatch for modelers who want the bilattice shape directly. The default T row matches OWL functional-property + min-cardinality 1 under OWA; the T? row matches Rust-style structural Option.

The lift rule (the load-bearing piece)

In rule-body atom context, a field access p.field evaluates as follows:

For field: T (required, ontologically present):

state has hasField(p, v)        → Is(v) at the Truth4 level; surface value is v
state lacks hasField(p, _), OWA → Can at the Truth4 level
state lacks hasField(p, _), CWA → model-level error OE1014 (cardinality violation)

For field: T? (structurally optional):

state has hasField(p, v)         → Some(v)
state lacks hasField(p, _), any  → None  (a positive fact; no Truth4 lift)

For field: Truth4Of<T>:

state has hasField(p, v)         → Is(v)
state has not_hasField(p)        → Not        (explicit negative assertion)
state lacks both                 → Can

Surface comparison atoms use the resulting Truth4 / Option / value:

p.age >= 18          // T:    Is(true) | Not | Can per the trace above
                     // T?:   TYPE ERROR — see below
                     // T4Of: Is(true) | Not | Can — same as T, but explicit

Option<T> in comparison atoms is a type error

Option<T> comp_op T (and Option<T> comp_op Option<T>, and friends) is rejected by the elaborator: OE0612 OptionComparisonRequiresHandling with a diagnostic that suggests three explicit forms:

// 1. Pattern in the rule body — preferred when None should fail-closed
p.age is Some(a), a >= 18

// 2. Helper method on Option<T>
p.age.is_some_and(|a| a >= 18)

// 3. Match with explicit unknown handling
match p.age {
    Some(a)    => a >= 18,
    None       => false,           // pick: false / true / Truth4Of::Can
}

The first form (is Some(a)) compiles to a guarded match that fails the conjunction (binds nothing) on None — a positive fact about absence. The second is sugar for the same. The third lets the modeler explicitly say what None means in their model.

This is JPA’s point made structural: if you wrote T?, the language refuses to guess what None should mean in a comparison; you must say.

Required-field-under-OWA: the lifted access rule

§5.1 line 42 amends to:

No value present at field access — under OWA, lift to Can at the Truth4 level (the surface returns the field’s declared type via the K3 fail-closed projection: false for Bool, omitted for collections); under CWA, emit OE1014 RequiredFieldUnasserted (the schema declared this field present; the KB must record it). At construction time, the existing OE0207 IntrinsicPropertyMissing rule for #[intrinsic] fields is unchanged.

The asymmetry — construction strict, query OWA-lifted — is intentional and matches OWL: TBox cardinality requires presence, ABox completeness is a separate (SHACL) concern.

Diagnostic codes

Spec edits

Lean mechanization

The theorem statement is roughly:

theorem field_access_owa_lift
    {P : Program} {p : Individual} {f : RequiredField}
    (h_no_assertion : ¬ ∃ v, P.state.has (hasField p f v))
    (h_owa : P.worldAssumption f.declaringConcept = .open) :
    P.accessField p f = (Truth4.can, default)

with the CWA branch as a separate (sharper) statement: under CWA, h_no_assertion is provably false for any iof(p, concept) ∈ P.state (the schema mandates a value), so the case is unreachable and the elaborator’s OE1014 is sound.

The Gustavo trace, after this RFD lands

With Gustavo’s code as written (age: Nat?):

pub kind Person { age: Nat? }
pub derive Adult(p: Person) :- p: Person, p.age >= 18;
//                                         ^^^^^^^^^^^ OE0612

The elaborator rejects the comparison at OE0612, asking the modeler to pick. Gustavo then makes the modeling choice JPA was asking him to make — either:

// Reference-ontology reading: people with no age aren't adults; Minor fires
pub derive Adult(p: Person) :- p: Person, p.age is Some(a), a >= 18;
pub derive Minor(p: Person) :- p: Person, not Adult(p);
// carol (no age) → Adult = Not (the `is Some(a)` fails) → Minor = Is

or:

// Implementation reading: every person has an age; KB may not know it
pub kind Person { age: Nat }     // required, OWA-aware lift handles the gap
pub derive Adult(p: Person) :- p: Person, p.age >= 18;
pub derive Minor(p: Person) :- p: Person, not Adult(p);
// carol (no age asserted, OWA) → p.age lifts to Can
//   → Adult body = Is ⊓ Can = Can
//   → not Adult(carol) = ¬Can = Can
//   → Minor(carol) = Is ⊓ Can = Can
// Minor's extent at Bool projection: carol omitted. At Truth4Of<Person>: shown as Can.

JPA’s two intents are no longer conflated; the elaborator has forced the choice; the Truth4 lift handles whichever choice the modeler made; the diagnostic carries the explanation.

Rationale

Why three surfaces instead of two

A naive design would keep just T and T? and let OWA do all the work. That collapses JPA’s two intents into one surface (T?), reproducing today’s ambiguity. Truth4Of<T> adds a third surface for the specific case where the modeler wants the bilattice value exposed in storage — relatively rare, but exactly what one needs when modeling, e.g., a clinical-trial endpoint where “patient response = unknown” is a first-class data point separate from “patient response = no.”

Three surfaces is the minimum that lets every modeler intent be expressed cleanly:

• T: TBox cardinality 1 + OWA-tolerant ABox.
• T?: structural optionality (no TBox cardinality assertion).
• Truth4Of<T>: explicit four-valued storage.

Why type-error on Option<T> comp_op T

JPA’s “ambiguous” is the load-bearing observation. If the elaborator silently coerces None to false (Reading C, SQL-style), the modeler never confronts the ambiguity and the model’s semantics drifts from intent. If the elaborator silently lifts None to Can (Reading A, Truth4-style), the modeler is again not consulted. The type error is the modeler-respecting move: ask the modeler what they mean.

The cost is one extra ceremony at every Option<T> comparison site (is Some(a), a >= 18 instead of a >= 18). The benefit is no silent ambiguity, no quiet semantic drift, and a diagnostic that doubles as documentation.

Why required-field-under-OWA lifts to Can (not errors)

Without this lift, the spec is internally inconsistent. §6.9 promises OWA semantics (knowledge is open; absence is uncertainty); §5.1 promises construction-time strict checks (required fields must be set). Today these collide: under OWA, an iof(carol, Person) axiom can be asserted with no hasAge tuple, but accessing carol.age errors out — which contradicts §6.9’s premise that absence is uncertainty.

The fix preserves both intents by separating their layers. Construction (the axiom event being inserted) stays strict — you can’t write Person { name: "carol" } without age because the construction is a single axiom and missing required fields are malformed at the event level. Query (subsequent field access on a possibly-incomplete KB) lifts to Can under OWA, matching OWL functional-property semantics exactly: every Person has an age (TBox), but we may not know it (ABox-incompleteness is fine under OWA).

CWA does not tolerate this: under CWA, an iof(carol, Person) with no hasAge(carol, _) is a schema violation, and OE1014 is correct.

Why OW1015 OptionalFieldAmbiguousIntent

The warning catches the JPA case at declaration time: a modeler writes f: T? without saying which intent they mean. The warning links to the table in §5.1.x and suggests either #[doc] documentation, an explicit #[intent(structural)] attribute, or migration to T + OWA. It can be silenced per-field. The warning is off by default in the prelude (std::* legitimately uses T? for plumbing types like Option<Person> returned from one { ... } queries) and on by default in user code with #[intent(...)] available as the disambiguator.

Alternatives considered

A. Implicit lift of Option<T> to Truth4 in rule bodies (Reading A)

Auto-translate None → Can, Some(v) → standard comparison verdict. Rejected. Silently picks the implementation reading; loses the reference-ontology reading entirely. Modelers who wrote T? to mean “some persons have no age” would find their rules treating those persons as unknown instead of positively-not-an-adult — a semantic regression that’s invisible at the source. Fails JPA’s framing.

B. Option<T> comp_op T returns Option<Bool> via functor lift (Reading C)

Auto-translate None comp_op v → None, Some(a) comp_op v → Some(a comp_op v). Force the modeler to write match on the result. Rejected. Type system gets noisier without solving the underlying ambiguity; modelers will reflexively write match { Some(b) => b, None => false } and the SQL-NULL silent collapse returns. The type-error path (Decision) forces the choice earlier where the modeler still remembers the intent.

C. Only two surfaces: T + OWA and T?

Drop Truth4Of<T> as a field type. Rejected. Loses the explicit-epistemic case (clinical-trial endpoints, audit fields marking “unknown” as a first-class value). The marginal cost of admitting Truth4Of<T> as a field type is low — it’s an existing stdlib type — and the expressivity is meaningful for medical / legal / scientific modeling.

D. Defer the entire question; leave §5.1’s “else error” rule as-is

Wait for more modelers to hit the wall. Rejected. Two of the language’s core consultants (Gustavo, JPA) hit it on day one of working through a temporal model. The substrate is Truth4-aware; the spec gap is at the surface; the cost of resolving is small (~5 elaborator checks + the diagnostic codes). Deferring would let modelers internalize ad-hoc workarounds and would force oxc-instantiate to ship without crisp Option-handling semantics.

E. Adopt OWL/SHACL syntax wholesale (#[functional], #[min_count], #[max_count])

Map TBox-cardinality + SHACL-shape vocabulary to attributes on field declarations. Rejected as the primary surface. Argon’s T / T? distinction is more ergonomic than OWL’s flat-property + cardinality-restriction model; adopting OWL vocabulary as the primary surface would be a Rust-aesthetic regression (per the user-memory directive defaulting to Rust/Cargo aesthetic). The OWL/SHACL pattern is reachable as a target via the field-type decision matrix above, without forcing modelers to write #[functional, min_count = 1] at every field site.

Consequences

Source-level

• A pub kind Person { age: Nat } model becomes feasible under OWA where today the spec forces Nat?.
• Option<T> comp_op T rule-body atoms must be rewritten with is Some(a) / is_some_and / match. The Cargo-style ecosystem migration: one-shot cargo ox fix rewrite per repo.
• Truth4Of<T> becomes available as a field type. Modelers who want OWL-style four-valued storage have a first-class surface.

Substrate-level

• Two new variants on FieldDecl (intent kind: required / optional / epistemic).
• One new branch in accessField: returns (Truth4, Value) instead of Value. Hot-path impact: one extra tag byte in the tuple-encoding, negligible.
• relation_tuple axiom kind unchanged; the lift happens at the accessField level, not in storage.

Runtime-level

• The K3 truth tables (§6.10.5) are already mechanized and used; this RFD adds no new operators.
• Query results returning collections now omit Can-valued field rows under K3 fail-closed projection — already the spec, but newly exercised at scale.

Diagnostic-level

• Five new codes (OE0612, OE0613, OE1014, OW1015, OE1016).
• One existing code (OE0207 IntrinsicPropertyMissing) keeps its current semantics; the new OE1014 covers the disjoint case of required-non-intrinsic absence under CWA.

Compatibility

T? retains its current Option<T> semantics — modelers who already use it for structural optionality see no behavior change. The new OE0612 may flag existing rule bodies; the suggested fix is purely mechanical (is Some(a), insertion). T under OWA gains new expressivity that didn’t exist before. No silent semantic changes to any existing well-typed program.

Open questions

OQ1 — Truth4Of<T> as field type interactions with mutation

A field declared f: Truth4Of<T> can be set to Is(v), Not, Can, or Both(v1, v2) via insert. What is the storage representation? Likely two relations: hasField_pos(p, f, v) and hasField_neg(p, f). Both is encoded as both relations holding simultaneously. The mapping is mechanical but worth specifying before implementation.

OQ2 — Interaction with refinement clauses

A refinement pub subkind Adult <: Person where { self.age >= 18 } over a required age: Nat field, under OWA, evaluates to Is | Not | Can per §6.9. Does the refinement-classification machinery in TypeSystem/Soundness/FlowTyping.lean handle the Can case? Spot-check needed: I expect yes (the existing OWA branch already covers it), but the new lifting rule introduces a Can source the type system didn’t previously consider.

OQ3 — Aggregate semantics over Can-valued cells (resolved — see RFD 0011)

What does sum { p.age | p: Person } evaluate to when some p.age lift to Can? Resolved by RFD 0011: monotone aggregators (sum non-negative, count, set_collect) evaluate to Truth4Of<T> with interval bounds [lower, upper] where lower = aggregate over filter-Is-true cells and upper = aggregate over filter-Is-true-or-Can cells; non-monotone aggregators (min, max, avg, string_join, percentile) propagate Can (any Can-cell in the filter set → whole result is Can). The Truth4 result is projected at the typed boundary per §12.2’s K3 fail-closed rule; the projection is observable via diagnostic OW0613 (info in query/fn, warning in derive, error in check) and an always-present aggregation-metadata envelope on query results carrying the interval bounds and Can-cell counts. The motivating Gustavo Ladeira / J.P. Almeida thread (2026-05-28 → 2026-05-29) is the worked example; the full design and rationale lives in RFD 0011.

OQ4 — Path traversal under Can-valued intermediate steps

For alice.parent.spouse.age, if alice.parent lifts to Can, does the full chain short-circuit to Can or does it propagate through the K3 conjunction of step verdicts? Existing field-path semantics in Reasoning/Rule.lean treats path steps as conjunctions; this would give natural propagation. Confirm.

OQ5 — #[intent(structural)] / #[intent(epistemic)] as the disambiguator

The proposed attribute makes the modeler’s intent explicit at declaration time. Should it be required for T? declarations in non-prelude modules? Two readings: (a) required (zero-ambiguity policy; matches Argon’s “no implicit override” philosophy from §5.2); (b) optional with OW1015 warning (gentler migration). Default to (b); revisit if modelers report confusion.

OQ6 — Migration path for existing UFO vocabulary

The UFO stdlib package declares several optional fields in its concept catalog (Person, Organization, …). Are these structural-optional or epistemic-optional? A scan of ufo/src/*.ar is needed to assign intents per-field before this RFD lands; this is a UFO-package PR, not an argon PR.

References

• §5.1 (struct/concept field declarations, OE0207), §5.2 (concept supertype clauses), §6.3 (refinement, three-valued membership), §6.6 (T? ≡ Option<T>), §6.9 (CWA/OWA), §6.10.5 (strong-Kleene truth tables), §7.3.1 (rule-atom grammar, is unknown outcome-suffix), §12 (Truth4 + Pietz–Rivieccio projection) — spec/reference/src/
• Foundation/Truth4.lean, Foundation/Projection.lean, Reasoning/Fixpoint.lean, Reasoning/State.lean — substrate mechanization
• oxc-instantiate (elaborator), oxc-reasoning::compile::Value (runtime carrier) — implementation sites
• W3C OWL 2 Web Ontology Language Direct Semantics, §2.3.3 (functional property axioms)
• W3C SHACL §3 (Shape constraints)
• Pietz, A. & Rivieccio, U. (2013). Nothing but the truth. Journal of Philosophical Logic — the Exactly-True semantics underlying §12.2’s K3 fail-closed projection.
• Belnap, N. (1977). A useful four-valued logic. — the underlying bilattice.
• Almeida, J.P.A. (UFES) and Ladeira, G. (Sharpe), Slack thread, 2026-05-28 — the motivating discussion.

RFD 0008 — Standpoint-Sheaf Equivalence Proof Roadmap

• State: committed (Path A landed)
• Opened: 2026-05-28
• Path A landed: 2026-05-29 — Argon/Standpoint/AFTEquivalence.lean mechanizes the discrete T3 obstruction equivalence (aft_discharges_T3_obstruction proven).
• Decides: the proof obligation, viable proof paths, and arc structure for elevating standpoint-sheaf equivalence from “axiomatized / open research” to mechanically proven in Lean.

Question

Standpoint logic (Gómez Álvarez & Rudolph 2021) and sheaf cohomology (Abramsky & Brandenburger 2011) independently formalize multi-perspective knowledge. The conjectured equivalence between them — “a set of standpoint axioms has a consistent global merger iff the associated sheaf has trivial H¹” — is currently axiomatized in Argon’s Lean mechanization, with AGENTS.md noting it as “open research.”

Should Argon push to prove this equivalence, and what’s the right proof path?

Context

Why this matters strategically

The competitive audit identified federation across standpoints as Argon’s most distinctive feature — no other production language has it as a first-class primitive. The current Lean mechanization proves a Finset-based version (Argon/Locality/SheafEquivalence.lean: grounded MCS equilibrium = minimal global section over module DAGs). This is operationally useful but does not connect to the broader logical-topological equivalence the literature poses.

Without the broader proof, Argon’s federation claim is “the runtime computes equivalent results to a sheaf model under our axiomatic embedding.” With the proof, the claim becomes “the runtime computes a sheaf model — and we know precisely when and how the model breaks.”

The user has designated this a worldclass objective. The vault’s “Standpoint-Sheaf Dictionary” note carries the conjectured translation table. This RFD makes the proof obligation concrete.

What’s already proven

In Argon/Locality/SheafEquivalence.lean (~180 lines, lake-green):

• Theorem 1 (bottom-up computation → equilibrium): definitional.
• Theorem 2 (equilibrium → global section): from local_fp inclusion.
• Theorem 3 (equilibrium is minimal global section): from local_fp being a least fixpoint.

These cover a BeliefAssignment (function ModId → Finset Atom) with generic bridge and local_fp operators. The acyclicity of the module DAG is required.

Adjacent mechanization (Argon/Standpoint/Federation.lean) proves the FDE bilattice info-join (federate_eq_both_iff, strictFold_preserves_inK3) — the AFT-side analogue of “cross-source disagreement detection.”

What’s NOT proven

The three sub-theorems forming the conjecture:

Decision

Pursue the proof in three escalating proof paths, each independently shippable.

Path A — AFT-only restatement (lowest risk, ~600 LOC) — LANDED 2026-05-29

The existing Foundation/Federation.lean’s federate_eq_both_iff is already the bilattice-algebra-side analogue of “H¹ ≠ 0 detects contextuality.” T3 is restated in AFT terms:

federate contribs = .both ↔ no global K3-section exists

This makes T3 a corollary of existing mechanized work. T1 and T2 are not discharged in this path — we lose the cohomological diagnostics (cocycle witnesses, spectral solver) but keep the soundness story.

Cost (actual): 1 new file Argon/Standpoint/AFTEquivalence.lean (~225 LOC including docstrings). One iteration through Lean’s cases/split_ifs tactics.

What landed:

• SheafClassification inductive: consistentTrue / consistentFalse / undetermined / obstructed.
• sheafClassify : List Truth4 → SheafClassification — direct semantic over federate.
• aft_discharges_T3_obstruction (proven): sheaf-obstructed ↔ federate contribs = .both. The load-bearing theorem; the AFT-side analogue of “H¹(F) ≠ 0 detects contextuality.”
• sheafClassify_consistentTrue_iff, sheafClassify_consistentFalse_iff, sheafClassify_undetermined_iff — three companion characterizations.
• sheafObstructed_iff_disagreement_or_explicit_both — composes the above with federate_eq_both_iff for the diagnostic-surface-shaped form.
• sheafClassify_singleton, sheafClassify_empty — base cases.

What this ships: a named theorem in Lean asserting “Argon federation = AFT-bilattice-based cross-source consistency.” Bridges the existing operational federation runtime to a categorical-flavored claim.

Path B — Frame-theoretic (medium, ~1200 LOC)

Replace the Grothendieck topology with the simpler structure of a complete Heyting algebra (frame) of standpoint-downsets. Mathlib has Order.Heyting.Basic and Topology.Sheaves.Sheaf over locales. Bridge rules become frame homomorphisms.

This discharges T1 routinely (frames induce topologies; standpoint-downsets form a frame canonically) and T2 (frame homomorphisms preserve gluing). T3 still requires work but on more familiar ground than full Grothendieck descent.

Estimated cost: ~1200 LOC. ~6 weeks.

What it ships: a partial proof of the equivalence — the topology induction and the bridge-rule-as-restriction-map sides, with T3 stated as a theorem schema parameterized over the localic sheaf machinery.

Net gain over Path A: the equivalence is now bidirectional (Argon → sheaf AND sheaf → Argon round-trip), not just embedding.

Path C — Full Grothendieck (highest, ~2000 LOC)

Mathlib has CategoryTheory.Sites and Grothendieck topologies. Construct the topology directly; prove T1, T2, T3 via descent.

The genuinely novel obstacle: connecting Hansen-Ghrist’s sheaf Laplacian diffusion (proved for vector-space stalks) to Argon’s lattice-valued knowledge requires either a box-embedding (Garcez-Lamb) relaxation or a discrete cohomology theorem. This is open research; no published work bridges it.

For the equivalence itself, this gap is not blocking — the equivalence can be discrete on the lattice side. But the computational payoff (spectral solver, cohomological diagnostics) depends on it.

Estimated cost: ~2000 LOC. ~12 weeks for the equivalence; the spectral bridge is a separate research effort.

What it ships: a research paper. Independent value beyond Argon’s runtime needs.

Recommended sequencing

1. Arc N+1 (this RFD): Path A. ✅ Landed 2026-05-29. Discharges the immediate Argon claim (“federation is sound under AFT info-join, which is the bilattice-algebra-side analogue of the sheaf claim”). Closes the wire-clean version of the worldclass objective.

2. Arc N+2 (follow-on): Path B. Lifts to frame-theoretic, discharging T1 + T2 + a parameterized T3. The equivalence becomes bidirectional.

3. Arc N+3 (research-paper track): Path C. Full Grothendieck. Separately publishable; not on the Argon roadmap critical path. Bridge to continuous diffusion is a deferred research obligation.

Paths A and B compose: Path A’s theorems are corollaries of Path B’s. Path B’s theorems are corollaries of Path C’s. Each arc strictly strengthens the previous.

Rationale

Why three paths rather than one

Path C is what the literature poses. Path A is what we can ship next week. Path B is the sweet spot. Allowing all three to live in the roadmap acknowledges that:

• Argon’s runtime needs the operational claim (Path A) now.
• The mathematical claim worth defending publicly (Path C) is research-scale.
• The intermediate (Path B) delivers most of the value with mathlib4’s existing infrastructure.

Why not just ship Path C and skip the intermediates

Path C’s continuous-discrete bridge is a genuine open problem. If we commit to Path C exclusively, the roadmap is hostage to one unproven research result. Splitting into three paths means each is independently shippable; if Path C stalls on the continuous-discrete bridge, Paths A and B are unaffected.

Why the AFT-only path counts as discharging the worldclass objective

The vault’s “Standpoint-Sheaf Dictionary” note maps:

• federate contribs = .both ↔ “irreducible disagreement”
• K3-fragment containment ↔ “global section exists”

federate_eq_both_iff already proves this in Argon/Standpoint/Federation.lean. Restating it as the canonical sheaf-equivalence theorem under the AFT lens IS the worldclass deliverable for Argon’s runtime semantics, operationally. The Grothendieck topology proof is the categorical deliverable, with mathematical content beyond the runtime claim. Both are worth pursuing; Path A satisfies the worldclass objective for Argon-as-a-language; Path C satisfies the worldclass objective for Argon-as-a-publishable-research-contribution.

Alternatives considered

Alt 1: leave the equivalence axiomatized

Mark the three sub-theorems as axiom declarations with citations to Gómez Álvarez & Rudolph 2021 and Abramsky & Brandenburger 2011. AGENTS.md permits cited axioms. Cost: zero. Risk: the runtime claim depends on the citations being correct.

Rejected per user strategic clarification: “we should absolutely push for a proper proof and make sure that it’s world-class.”

Alt 2: ship only the AFT-only path

Land Path A; declare the categorical claim out of scope. Cost: ~600 LOC. Risk: ceiling-bound; the federation story remains “operational only,” with no path to spectral / cohomological diagnostics.

Rejected as too narrow. The user designated this worldclass; a worldclass deliverable includes the mathematical claim, not just the operational one.

Alt 3: ship Path C exclusively

Commit to the full Grothendieck construction; treat A and B as intermediate steps not worth landing independently.

Rejected: the continuous-discrete bridge is a research gap with no published solution. Risking the roadmap on it is unwise. Splitting into three paths lets each ship independently.

Consequences

Lean changes (per arc)

• Arc N+1 (Path A): ~600 LOC. New file Argon/Standpoint/AFTEquivalence.lean. Extends Federation.lean with the canonical theorem statement.

• Arc N+2 (Path B): ~1200 LOC. New file Argon/Standpoint/FrameEquivalence.lean. Depends on mathlib4 Order.Heyting.Basic + Topology.Sheaves.Sheaf.

• Arc N+3 (Path C): ~2000 LOC. New file Argon/Standpoint/SheafEquivalence.lean (NOT the existing Locality/SheafEquivalence.lean, which proves the discrete Finset form). Depends on mathlib4 CategoryTheory.Sites. Spectral bridge is a separate research effort.

Reference book changes

§11 (Standpoints and federation) gains a new subsection citing this RFD’s three theorems as the soundness foundation. Currently §11.x reads as informal motivation; after Path A lands, it can cite the mechanized theorem directly.

Runtime impact

Path A: none. Federation runtime continues to use AFT info-join; the equivalence theorem is a soundness claim about it.

Path B: enables across[] queries to use frame-homomorphism preservation as a static guarantee. Diagnostic surface gains an “irreducible disagreement: cocycle on edges {…}” message under H¹ obstruction.

Path C: enables sheaf Laplacian diffusion as an alternative federation evaluator (spectral solver for acyclic module DAGs). Spec gain λ₁-spectral-gap as a federation cost metric.

Citation registry

Each path adds named theorems whose proof obligations cite specific prior work. The citation list (book §22 references) gains:

• Gómez Álvarez, S. & Rudolph, S. (2021). Standpoint Logic: Multi-Perspective Knowledge Representation. (Path A, B, C)
• Abramsky, S. & Brandenburger, A. (2011). The Sheaf-Theoretic Structure of Non-locality and Contextuality. (Path B, C)
• Hansen, J. & Ghrist, R. (2020). Opinion Dynamics on Discourse Sheaves. (Path C, spectral bridge)
• Mac Lane, S. & Moerdijk, I. (1992). Sheaves in Geometry and Logic. (Path C foundations)
• Denecker, M., Marek, V., Truszczyński, M. (2000). Approximation Fixpoint Theory. (Path A AFT side)

Open questions

• Continuous-discrete bridge for stalks. Hansen-Ghrist’s diffusion convergence is proved for vector-space stalks. Argon’s modules use lattice-valued knowledge. No published work bridges them. Path C’s spectral payoff depends on resolution; the equivalence itself does not. Is the spectral-bridge worth a dedicated research effort, or accept the discrete cohomology theorem?

• Cocycle diagnostic surface. Under H¹ obstruction, what does the modeler see? “Irreducible disagreement on bridges {b1, b2, b3}” with a cycle witness? Diagnostic ergonomics design.

• Functorial canonicity of T1. Classical topology literature has Grothendieck constructions for modal Kripke frames, but no published canonical induction for standpoint orders. Path C may require an originality contribution here.

• MLT-style multi-level stalks. Standpoints can carry metatypes (a standpoint’s knowledge includes higher-order classifications). Whether sheafification respects MLT order arithmetic is unaddressed in the literature. Defer to MLT std library RFD.

• Defeasible bridges. Bridge rules can themselves be defeasible (per Argon’s defeasibility substrate). Does the sheaf framework absorb Governatori-Rotolo +Δ/-Δ proof tags as graded restriction maps? Open.

RFD 0009 — std::mlt library scope

• State: discussion
• Opened: 2026-05-28
• Last revised: 2026-05-29 (added #[order(N)] assertion decorator + completed decorator set per discussion with Tiago Sales; fixed @[…] → #[…] sigil throughout to align with §14.2)
• Decides: scope of the std::mlt library that provides Multi-Level Theory (Carvalho-Almeida 2018) as a parallel std::* package on Argon’s neutral substrate; surface syntax for decorators (relational AND assertion forms); the Datalog rules CL-1..CL-7 enforcing MLT well-formedness; per-rule diagnostic emission for OE1903–OE1907.

Question

Argon’s substrate is committed to MLT-as-library (RFD-relevant memory: “Higher-order theories as stdlib libraries”). The substrate provides the higher-order type primitives required (universe polymorphism via metaxis, level-indexed quantification via metatype) and now carries the five MLT primitive metarel kinds (MLTMetarelKind per the just-landed Argon/MetaCalculus/MLTKinds.lean). What’s needed is the library that operationalizes MLT — decorators, Datalog enforcement rules, diagnostic emission.

What should std::mlt v0.1 ship, and how should it be wired into the build pipeline?

Context

Why a library, not substrate

Per user strategic commitment: “MLT is a library, not substrate. The atoms of the language allow for MLT to be implemented, as we have higher-order type primitives, but MLT must be a library.” This preserves Argon’s neutrality. UFO, BFO, DOLCE, ML2 all ship as parallel std::* packages; the language doesn’t favor one foundational ontology over another. The substrate’s responsibility ends at exposing sufficient primitives.

This commitment is verified for MLT specifically by the just-landed substrate sufficiency scaffold:

• instanceOf, specializes admitted via the inheritance lattice + IsCanNot machinery.
• categorizes, partitions, subordinates admitted via MLTMetarelKind carriers.
• Order arithmetic semantics live in Argon/MetaCalculus/Wellformed.lean as parametric Props over an abstract T.

What’s missing: the library that instantiates these primitives against modeler-written declarations and emits enforcement rules.

What MLT requires from a library

Per Carvalho-Almeida 2018 (Theorem-based MLT axiomatic theory) and Vault’s “MLT as a Library, Not Substrate” deep-dive:

1. Decorators on metatype declarations that express MLT primitives at the surface. Two distinct kinds — relational (declare a cross-level relation between types) and assertion (declare a claim the compiler verifies against the derived fixpoint). Sigil is #[…] per Procedural macros; both kinds appear at declaration position.

   Relational decorators — desugar to canonical metarel-instance events; the relation participates in CL-1..CL-7 enforcement:

   • #[categorizes(T)] — the metatype’s instances are proper specializations of T; implies order(M) = order(T) + 1. (Carvalho-Almeida §3.2.)
   • #[partitions(T)] — #[categorizes(T)] + members of the metatype pairwise disjoint and jointly exhaustive of T’s extent. (Carvalho-Almeida §3.3.)
   • #[subordinate_to(M)] — same-order subordination per Carvalho-Almeida §3.4. (Spelled subordinate_to per Higher-order modeling, not subordinates — the §3.4 relation reads “A is subordinate to B”.)
   • #[power_type_of(T)] — the metatype is the powertype of T per Cardelli 1988; every instance of T is also an instance of M. (Carvalho-Almeida §3.5.)

   Assertion decorators — desugar to a check rule verifying a claim against the derived fixpoint; fail-loud at runtime if the assertion conflicts with the iof chain, vacuous when the chain is incomplete:

   • #[order(N)] — modeler asserts has_order(Self, N); the elaborator emits an implicit check rule that fires OE1905 OrderInconsistency if the derived order disagrees. See § Decorator kinds — assertion vs. relational below for the full design.

   Tier decorators — module-level annotations that narrow the decidability tier:

   • #[order_bound(N)] — module declaration; caps every concept’s order at N. Lowers the module from tier:metaorder to a polynomial tier under the bound. (See Higher-order modeling, Tier ladder.)

2. Datalog enforcement rules (kernel-native, fired automatically), per the Vault’s “Hybrid A+B” design pattern:

   • CL-1 Categorization: violation_categorization(X, T₂, T₁) :- categorizes(T₂, T₁), iof(X, T₂), ¬subclass(X, T₁). Emits OE1903.
   • CL-2 Partition disjointness: violation_partition_disjoint(Ind, T₃ₐ, T₃ᵦ) :- partitions(T₂, T₁), iof(T₃ₐ, T₂), iof(T₃ᵦ, T₂), T₃ₐ ≠ T₃ᵦ, iof(Ind, T₃ₐ), iof(Ind, T₃ᵦ). Emits OE1904.
   • CL-3 Order consistency: violation_order(X, T) :- concept_order(T, N), iof(X, T), concept_order(X, M), M ≥ N. Emits OE1905.
   • CL-4 Categorization inference: subclass(X, T₁) :- categorizes(T₂, T₁), iof(X, T₂). (Positive rule, no diagnostic.)
   • CL-5 Subordination requirement: violation_subordination(A, B) :- subordinates(A, B), (order(A) ≠ order(B) ∨ order(A) < 2). Emits OE1906.
   • CL-6 Powertype completeness: violation_powertype(T) :- power_type_of(M, T), iof(X, T), ¬iof(X, M). Emits OE1907.
   • CL-7 MLT compositional consistency (Carvalho-Almeida Theorem 5): a closure rule that propagates categorizes/partitions/subordinates interactions per the §3.4 composition table.

3. Diagnostic codes OE1903–OE1907 wired into oxc-diagnostics and emitted from oxc-instantiate (or a follow-on pass) when CL-1..CL-7 detect violations.

4. Library API surface modelers reach for:

   • use std::mlt::* brings the decorator set #[categorizes] / #[partitions] / #[subordinate_to] / #[power_type_of] / #[order] / #[order_bound] into scope.
   • std::mlt::well_formed!() build-time check macro that runs CL-1..CL-7 (plus the user’s #[order] assertions, if any) and fails the build on violation. Modelers serious about MLT correctness add this to their root module.
   • std::mlt::order(e: Entity) -> Option<Nat> library function — query a concept’s derived order at runtime; None when the iof chain is incomplete enough that order isn’t yet determined. (Operationally lowered to a one-shot query over the has_order/2 predicate per RP-003 §4.3.)

What std::mlt does NOT do

Per the strategic commitment, MLT-as-library means:

• The library does NOT extend the substrate. No new atoms.
• The library does NOT enforce MLT globally — only modules that use std::mlt opt in. Other modules see iof/specializes as usual without categorization arithmetic.
• The library does NOT subsume UFO, BFO, DOLCE — those are parallel std::* libraries with independent enforcement.

Decision

Scope of v0.1

Three landings, each independent:

Phase 1 — Decorator parser + lowering (~1-2 weeks)

• New oxc-parser recognition for the v0.1 MLT decorator set on type/metatype declarations:
  • Relational (lower to metarel_decl axiom events): #[categorizes(T)], #[partitions(T)], #[subordinate_to(M)], #[power_type_of(T)].
  • Assertion (lower to implicit check rules): #[order(N)].
  • Tier (module-level, narrows decidability tier): #[order_bound(N)].
• oxc-instantiate lowers each decorator according to its kind:
  • Relational → canonical metarel_decl axiom event via Argon.MetaCalculus.MLT.declOfKind.
  • Assertion → synthesized check declaration; for #[order(N)] on concept X, the check is check OrderMatches { has_order(X, N) } keyed to OE1905 OrderInconsistency.
  • Tier → module-attribute on the elaborated program; the classifier reads it and narrows the tier.
• Diagnostic emission for surface mis-use (decorator on a non-applicable position, bad argument shape, conflicting decorators on the same declaration). Reuses OE0708 ReservedAttributeName only when collision is genuine; the MLT-specific positional checks ride on a new fingerprint.
• Sigil is fixed at #[…] (Procedural macros); the prior draft of this RFD used @[…] which was a typo against the rest of the spec.

Phase 2 — CL-1..CL-7 Datalog rules + OE1903–OE1907 (~3-4 weeks)

• oxc-reasoning admits the seven CL-* rules as built-in rules (compiled at runtime, not modeler-written).
• evaluate_to_fixpoint (or its semi-naive successor — depends on RFD 0003 backend dispatch) computes the violation predicates.
• oxc-runtime lifts violation tuples to OE1903–OE1907 diagnostics at query-time-of-affected-rule.
• Lean-side: extend Argon.MetaCalculus.Wellformed’s parametric predicates to a runtime-evaluable form; prove correctness against Carvalho-Almeida 2018’s axioms.

Phase 3 — std::mlt package + integration tests (~1-2 weeks)

• Ship std::mlt as a workspace package with use std::mlt::* bringing in decorators.
• Integration test exercising the Vault’s “biological taxonomy” canonical example (Animal → AnimalSpecies → DogBreed, order 0/1/2).
• Documentation: short tutorial showing modeler-facing usage.

Total v0.1 effort: ~5-8 weeks across Phase 1+2+3.

Implementation pattern — “Hybrid A+B”

Per Vault’s MLT design synthesis: enforcement is two-layered.

• A — Compile-time decorator expansion: #[categorizes(T)] on metatype M desugars to a canonical metarel categorizes(M, T) declaration that lands in the events list. Pure source transformation; no runtime cost. Assertion decorators (#[order(N)]) similarly desugar at compile time, but to a synthesized check rule rather than a metarel-instance event.

• B — Runtime Datalog evaluation: CL-1..CL-7 rules fire continuously during query evaluation, detecting violations as they arise. Lazy by construction (a violation only matters when a query touches the affected predicate). Diagnostics emit at query time, not at build time.

This hybrid lets the build complete even if MLT violations exist (graceful degradation for in-progress modeling), while ensuring runtime queries fail loud if a violation is reachable.

Decorator kinds — assertion vs. relational

The two decorator kinds carry different semantic weight and warrant different mechanical treatment.

Relational decorators (#[categorizes], #[partitions], #[subordinate_to], #[power_type_of]) introduce a fact into the model: “this metatype is in this cross-level relation with that type.” They desugar to canonical metarel_decl events that participate in the CL-1..CL-7 enforcement closures. The diagnostic surface for these is the closure rules — a violation is detected when the modeler’s facts are mutually inconsistent under MLT’s axioms (Carvalho-Almeida §3.2–§3.5).

Assertion decorators (#[order(N)]) introduce a claim into the model: “this concept has this property.” They desugar to implicit check rules that fire at runtime against the derived fixpoint. The diagnostic surface is the check rule itself — a violation is detected when the modeler’s claim conflicts with what the iof chain actually derives.

#[order(N)] — design

use std::mlt::*;

#[order(2)]
pub type AnimalSpecies : TaxonomicRank <: Species  // claimed 2; derived order(AnimalSpecies) = 2 ✓

#[order(1)]
pub kind Dog : AnimalSpecies <: Animal             // claimed 1; derived order(Dog) = 1 ✓

let Lassie : Dog                                    // individuals don't need #[order]; order = 0 always

Semantics. On a concept declaration X with #[order(N)], the elaborator synthesizes a check rule equivalent to:

check OrderMatches { has_order(X, N) }   // mlt::E0007 in the library namespace; routed to OE1905 in v0.1

The has_order(_, _) predicate is std::mlt’s stratified-aggregate derivation over the iof DAG (RP-003 §4.3, lines 226–240):

• has_order(x, 0) for any individual x;
• has_order(t, n) for type t when n = 1 + max{m | iof(t’, t) ∧ has_order(t’, m)} (well-founded by iof acyclicity).

Three possible outcomes at check time:

The vacuous-pass case is the load-bearing one for incomplete-model checking — a modeler partway through wiring up the iof chain can assert #[order(2)] and the build won’t fail just because the chain isn’t done; it only fails when the chain explicitly contradicts the assertion. As the model grows toward completeness, more #[order] assertions become checkable, and any divergence shows up immediately.

Why this matters (ergonomics). Three concrete wins motivate the assertion decorator over inference-only:

1. Incomplete-model verification. Modelers iterate. A partial iof chain doesn’t yet derive order, but the modeler has a belief about what the final order should be. #[order(N)] records that belief and turns it into a checkable invariant the moment the chain reaches completeness.
2. Self-documenting models. A reader can see a concept’s intended tower position at a glance without traversing iof predecessors. This compounds in large models where the iof chain crosses module boundaries.
3. Agent guidance. LLM-driven modeling is a primary v0 use case (per Argon’s stdlib-libraries design memo and design notes). Explicit assertions give the agent something to be checked against; pure inference gives the agent nothing to falsify. Agents reason better when their claims are observably refutable.

Why this design, not a procmacro. RP-003 GAP-3 calls for eventually re-homing all MLT decorators as pub macro declarations in std::mlt once the procmacro system is implemented (§14.2). For v0.1, parser-recognized attributes are simpler and ship sooner; the surface (#[order(N)]) is identical either way. Migration is internal.

Applicability. #[order(N)] is valid on:

• Concept declarations (pub type, pub kind, and any user metatype-introduced declaration). Asserts the concept’s tower position.
• Individual declarations (let X : T). Trivially asserts N == 0; mostly redundant since individuals always have order 0, but admitted for symmetry.

It is not valid on:

• struct/enum declarations (no metatype, category error parallel to meta()).
• Relation declarations (relations don’t carry order in MLT; the relation’s metarel does).

Mis-application emits OE1908 OrderAssertionMisplaced (a new code reserved by Phase 1).

Order ceiling at 2 for v1

Per Vault’s “Orca domain census” finding: real-world MLT patterns max out at order 2 (Animal → AnimalSpecies → DogBreed; no order-3 patterns required). v0.1 caps support at order 2:

• concept_order predicate ranges over {0, 1, 2}.
• OE1905 emits for order ≥ 3 declarations.
• MLT* orderless types (universe polymorphism per Sozeau-Tabareau 2014) defer to v2.

This bound makes polynomial decidability concrete: D1Pred over a bounded type graph is polynomial; OE1905 enforcement is O(n²) in the type graph’s edge count.

Rationale

Why ship std::mlt rather than fold it into the language

Three reasons:

1. Neutrality preservation. UFO and BFO have ontological commitments MLT doesn’t (UFO commits to a rigidity/sortality taxonomy; BFO commits to continuant/occurrent). If MLT were substrate, every Argon program would inherit MLT’s claims even when modeling a non-MLT ontology. Library-form means opt-in.

2. Substrate parsimony. Adding MLT to the substrate would grow the five atoms to six. The substrate’s clean five-atom architecture (memory: “Argon substrate atoms fixed: five atoms; mutate not mutation; no event atom; standpoints first-class”) is load-bearing for the meta-calculus story; growing it for one foundational ontology breaks the symmetry.

3. Future foundations. ML2, MLT*, DeepTelos all extend MLT in different directions. Library form lets each ship as a parallel package (std::ml2, std::mlt_star, std::deeptelos); substrate form would force one to be canonical.

Why decorators rather than a new keyword

Carvalho-Almeida’s notation uses categorizes as a relation name. The decorator form #[categorizes(T)] mirrors this exactly: “the metatype is categorized by T.” A keyword form (pub categorization Foo of T) would invent surface syntax that doesn’t appear in the literature.

Decorators also compose naturally with other attributes (#[categorizes(T)] #[disjoint] pub metatype M). A keyword form forces a single grammar position.

Why Datalog enforcement rather than compile-time

Several MLT constraints (CL-1, CL-3 in particular) require closing over the full extent of iof — instances asserted across the module. Compile-time evaluation can’t see runtime-asserted facts (added via mutations). Datalog evaluation fires lazily at query time, catching violations including runtime-added ones.

The downside: violations don’t surface until queried. A modeler can build a broken MLT module that passes the build. The catch is the build-time std::mlt::well_formed!() macro: it pre-runs CL-1..CL-7 against the build-time fact catalog and fails the build if violations exist. Modelers serious about MLT enforcement add this macro to their root module.

Why the OE1903–OE1907 codes are reserved but not yet emitted

The codes were reserved in grammar.toml when RFD 0006 landed (field mutability). The reservation predates this RFD because the diagnostic codes are part of the broader Argon diagnostic registry, not specific to std::mlt. Their EMIT SITES land with Phase 2; reservation is already in place.

Alternatives considered

Alt 1: ship MLT as part of substrate

Add categorizes/partitions/subordinates as substrate atoms; bake CL-1..CL-7 into the elaborator.

Rejected per user strategic commitment. See “Why ship std::mlt rather than fold it into the language” above.

Alt 2: ship std::mlt v0.1 with only the surface (decorators), defer Datalog

A “syntax-only” v0.1: parser admits decorators, but enforcement is documentation-only (“violations are the modeler’s responsibility”).

Rejected as too weak. Decorator-only would let broken MLT modules pass the build silently — the worst-of-both world (visible syntax claiming MLT compliance with no actual checking). Phase 2’s Datalog enforcement is what makes the library credible.

Alt 3: ship Phase 1 + 2, defer the std::mlt package wrapper (Phase 3)

Decorators + Datalog rules + diagnostics ship as part of the language; the std::mlt package is a thin re-export layer added later.

Rejected because it leaks MLT-specific names (categorizes, subordinates, etc.) into the language’s prelude. Keeping them library-prefixed (std::mlt::categorizes) maintains the neutrality claim.

Alt 4: full Carvalho-Almeida axiomatization (Theorems 1-8) in Lean before shipping

Mechanize every Carvalho-Almeida theorem in Argon/Locality/MLTAxioms.lean before allowing the Rust library to claim MLT compliance.

Rejected as too ambitious for v0.1. The substrate-sufficiency scaffold (MLTMetarelKind + classify_declOfKind theorem) discharges the expressibility claim; full axiomatization is a separate research effort (~24-38 person-months per Vault’s D-132 estimate). Defer to v0.2 or beyond.

Consequences

Wire format

No new axiom kinds. #[categorizes(T)] and its relational siblings desugar to canonical metarel_decl events; #[order(N)] desugars to a synthesized check declaration that emits a CheckDecl event keyed to OE1905. No new body types.

Lean changes

Phase 2 lands a Argon/Locality/MLTRules.lean (~400-600 LOC) that:

• Defines the seven CL-* rule shapes against Argon.MetaCalculus.MLTKinds.
• States the soundness theorem (CL-rules detect exactly the violations of Carvalho-Almeida’s axioms).
• Proof handle: parametric predicates in Wellformed.lean already capture the violation semantics; this module instantiates them against runtime tuples.

Rust changes

Phase 1: oxc-parser decorator recognition + oxc-instantiate decorator-to-metarel lowering. ~300-500 LOC.

Phase 2: oxc-reasoning admits built-in rules; oxc-runtime lifts violation tuples to diagnostics. ~800-1200 LOC.

Phase 3: std::mlt package declaration in packages/std-mlt/ with re-exports. ~100-200 LOC.

Diagnostic surface

The #[order(N)] assertion is the first MLT diagnostic emitted from Phase 1 (the synthesized check rule fires under runtime evaluation but the check declaration itself lands in Phase 1’s parser/elaborator output). All other MLT diagnostics land with Phase 2’s CL-rule evaluator.

Per RP-003 GAP-4, the OE19xx codes are scheduled to migrate to the library namespace (mlt::E0001–mlt::E0008); v0.1 retains OE19xx for continuity with the rest of the diagnostic registry and tracks the migration as an open question below.

Documentation

Reference book §13 (or §5.x — placement TBD) gains a subsection on MLT-as-library, citing Carvalho-Almeida 2018. The §17 ARS substrate description references MLT as one of the foundational ontologies the substrate admits via library composition.

Open questions

• Phase 2 evaluation dispatch: CL-1..CL-7 are Datalog rules. They should run on the same executor as user-written derives. But CL-1..CL-7 are built-in, not modeler-written — should they be loaded as part of the runtime’s bootstrap, or shipped in a special “kernel” rule set? Affects how RFD 0003 (per-stratum backend dispatch) handles them.

• Cross-library MLT consistency: if a module uses both std::mlt and std::ufo, do their iof/specializes semantics align? UFO inherits MLT semantics by reference (per Vault’s “UFO Design Limitations”); BFO does not. The interaction needs RFD-level treatment.

• Order arithmetic via Lean universe inference vs explicit predicate: Vault’s Phase B1 + B2 work proposes mechanizing T2 substrate (Tarski-cumulative universes) so Lean’s elaborator infers order(T) automatically. v0.1 sticks with the explicit concept_order predicate; T2 mechanization is a separate research effort.

• MLT orderless types*: universe-polymorphic types per Sozeau-Tabareau 2014. v0.1 caps at order 2; MLT* unlocks unbounded order. Defer to v0.2.

• Powertype keyword deprecation: per Vault, pub powertype Name (categorizes|partitions) Target { instances } is currently hard-reserved in kind.rs:657 but marked for removal. The pattern system + decorator approach in this RFD obsoletes that surface. Removal unblocks pub metatype powertype = { ... } from user code. Coordinated removal with this RFD’s Phase 1.

• MLT decidability under unbounded order: at order ≥ 3, decidability becomes uncertain (Carvalho-Almeida 2018 is silent past order 2). If v0.2 admits MLT*, the decidability classifier needs an MLT-specific tier or a refinement to the existing metaorder tier.

• Backward compatibility of iof semantics: in MLT, iof(x, T) includes order arithmetic. In other foundational ontologies (UFO continuant, BFO universals), iof is order-agnostic. Module-local use std::mlt::* should NOT retroactively change iof semantics for non-std::mlt-using modules — but the runtime evaluator runs CL-1..CL-7 globally. Resolution: scope CL-1..CL-7 to predicates declared with MLT decorators (a metarel_decl.is_mlt_primitive flag added by Phase 1 decorator lowering).

• OE19xx → mlt::E* namespace migration (RP-003 GAP-4): the diagnostic codes in this RFD use the language-level OE19xx range, inherited from when MLT was substrate-embedded. Per the MLT-as-library commitment, library-namespaced codes (mlt::E0001–mlt::E0008, with the mlt:: prefix matching 09-higher-order.md:20) are the consistent endpoint. v0.1 keeps OE19xx for continuity with the existing registry; the migration is a coordinated rename across oxc-diagnostics, the Lean wellformedness module, and appendix-c-diagnostic-codes.md. Open question: do we migrate before or after Phase 2 emit sites land?

• Assertion-decorator pattern as a reusable mechanism: #[order(N)] is the first assertion-style decorator. The same pattern is the natural shape for forthcoming ontological libraries — #[potency(N)] in std::potency (deep-instantiation level), #[stratum(N)] in std::ml2, etc. Should std::core expose a generic assertion-decorator builder (a procmacro helper) so each library doesn’t re-implement the lowering? Or do we accept boilerplate per library and re-evaluate when a third library wants this pattern? v0.1 hard-codes #[order]’s lowering; revisit after std::potency is sketched.

• Vacuous-pass behavior under incomplete iof chains: #[order(N)] passes vacuously when has_order(X, _) is undefined at check time. This is the right default for incomplete-model development — but it means a modeler can ship a build with unverified assertions. Mitigation: the well_formed!() macro could escalate vacuous passes to warnings (OE1909 OrderAssertionUnverified) so modelers see what’s not yet covered. Decide whether to land that escalation in Phase 1 or defer.

• #[order(N)] on individuals: let Lassie : Dog #[order(0)] is admitted but redundant (individuals always have order 0). Should the elaborator reject as a useless annotation (W0001-style warning) or silently accept? Argument for accepting: agent-generated models may always emit it for symmetry; the redundancy is harmless. Argument for warning: signals to the modeler that they may be confused about what #[order] means. Lean toward silent accept for v0.1; revisit if it becomes a source of confusion.

Discussion log

2026-05-29 — #[order(N)] added, decorator set completed

Tiago Sales asked in chat whether the syntax for declaring a type’s MLT order should be a refinement on the meta-calculus (pub type Species <: Taxon where { meta(self).order == 2 }) or an attribute (@[order(2)]). Neither matched the substrate’s actual design — meta(x) returns a Metatype value, not an arithmetic carrier, and @[…] is the wrong sigil. The substrate’s design is that order is computed, not declared: it falls out of the iof chain as a fixpoint over the well-founded has_order/2 predicate.

The follow-up question was the load-bearing one: “is implicit ordering sufficient for the modeler?” Tiago’s argument — that explicit assertions help with incomplete-model checking, documentation, and agent guidance — settled the question. #[order(N)] becomes a std::mlt assertion decorator that verifies the modeler’s belief against the derived fixpoint, fail-loud on conflict, vacuous-pass on incomplete chain.

Changes made to this RFD in the 2026-05-29 revision:

1. Added #[order(N)] to the v0.1 decorator set as the canonical example of an assertion decorator (a new decorator kind alongside the existing relational decorators).
2. Completed the relational decorator set — added #[power_type_of(T)] (was missing) and renamed #[subordinates(M)] → #[subordinate_to(M)] (the §9 spelling, matching Carvalho-Almeida §3.4’s “A is subordinate to B” reading).
3. Added #[order_bound(N)] as the module-level tier decorator (was referenced in §9 / RP-003 but not enumerated in this RFD).
4. Fixed @[…] → #[…] throughout. The @[…] form was a typo against Procedural macros and every example in the reference book.
5. New diagnostic code OE1908 OrderAssertionMisplaced for #[order(N)] on inapplicable declarations (struct/enum/relation).
6. New subsection “Decorator kinds — assertion vs. relational” with the #[order(N)] design in full, including the three-state check outcome table (pass / fail / vacuous) and the ergonomic rationale.
7. New open questions: OE19xx → mlt::E* migration, assertion-decorator pattern as a reusable mechanism for std::potency / std::ml2, vacuous-pass behavior under incomplete chains, and the individual-redundancy question.

RFD 0010 — Negative facts / strong negation

• State: discussion
• Opened: 2026-05-29
• Decides: surface syntax for asserting a fact’s negation as ground truth (distinct from absence-as-unknown under OWA, and distinct from default negation-as-failure in rule bodies); the wire-format mirror; how this composes with the standpoint federation runtime to make Truth4::Both operationally reachable.

Question

Today a pub standpoint X { pub fact Person(alice); } lets standpoint X assert alice ∈ Person as positive ground truth. The federation runtime’s query_dispatch then evaluates this row as Truth4::Is from X and Truth4::Can (implicit absence) from any other contributing standpoint. The AFT info-join Is ⊕ Can = Is, so the row surfaces tagged Is.

There is no current way for a standpoint to assert alice ∉ Person as positive ground truth. This means:

• The bilattice value Truth4::Not (Belnap-Dunn’s F, AFT’s (F, F) pair) is never produced from a fact-derived per-source classification.
• The bilattice value Truth4::Both (Belnap’s B, AFT’s inconsistent (T, F)) is consequently never produced by federate, because Is ⊕ Can ⊕ Can ⊕ ... = Is regardless of contributor count.
• The federation runtime is operationally category-(b) bilattice-traced in the vault’s Bilattice-Native Query Evaluation taxonomy, not the category-(c) bilattice-native outcome the substrate’s proven theorems (federate_eq_both_iff, aft_discharges_T3_obstruction) advertise.

The decision: introduce a surface form for strong negation of facts, lower it to a new wire-format IofRefutation axiom kind, and have the per-standpoint materializer compute Truth4 values per (tuple, source) pair so that the runtime is operationally bilattice-native.

Context

What’s deferred from RFD 0004

RFD 0004 §Future Work explicitly anticipated this work:

Negative facts / classical negation — pub not_fact Person(alice) to assert that alice is not a Person. Useful in OWA / classical contexts; relates to §12.2’s Truth4 bilattice. Defer; orthogonal to this RFD’s positive-only scope.

That deferral is now load-bearing: it gates the operational reachability of the bilattice’s most distinctive value.

The two negations distinction (Gelfond-Lifschitz 1991)

Gelfond and Lifschitz (1991) draw the canonical line between two negations every paraconsistent logic-programming surface must distinguish:

Argon already uses not in rule bodies (NAF, stratified). What it lacks is the declaration-level strong negation. The two are independent: NAF is a reasoning-time operator inferring absence from the current extent; strong negation is a build-time ground-truth assertion of refutation.

What the substrate already supplies

The Lean substrate is fully ready for this:

• Argon.Foundation.Truth4 has the four-valued carrier with all algebraic laws.
• Argon.Foundation.Bilattice.infoJoin is proven associative, commutative, idempotent.
• Argon.Standpoint.Federation.federate is the AFT info-join over List Truth4.
• federate_eq_classify characterizes federate outputs structurally.
• federate_eq_both_iff: federate xs = .both ↔ hasBoth xs ∨ (hasIs xs ∧ hasNot xs) — the precise theorem stating when Both arises.
• aft_discharges_T3_obstruction: sheafClassify contribs = .obstructed ↔ federate contribs = .both.

None of this is reachable by the runtime today because no source ever contributes .not. The Lean theorems are sound but the runtime cannot exhibit the case they characterize.

What the wire format already supplies

AxiomEvent.standpoint_id (set by the standpoint-block elaborator in commit 2776be9) tags each event with its asserting source. The materializer in commit 9aa8c73 (materialize_predicates_for_standpoint) filters per source. The dispatcher in the same commit feeds per-source classifications to query_derive_federated. The shape is right; only the negative half is missing.

The Polarity field is not a negation field

AxiomEvent.op: Polarity ∈ {Assert, Retract} is the time-evolution polarity (asserting vs withdrawing a previous claim under bitemporal extent). It is not the ontological polarity (P(x) vs ¬P(x)). Conflating them would break RP-004’s bitemporal contract. The right move is a new axiom kind for ontological refutation, orthogonal to op.

Decision

Surface (1) — declaration-level strong negation

pub not_fact Person(alice);
pub not_fact Adult(bob);
pub not_fact employed_by(alice, AcmeCorp);

Symmetric to pub fact P(x); syntactically. Lowers to a new wire event variant. Permitted at file level and inside pub standpoint X { ... } blocks; in the latter case the refutation is stamped with X.standpoint_id like positive facts (commit 2776be9’s mechanism applies uniformly).

Wire format (2) — new axiom kind IofRefutation

#![allow(unused)]
fn main() {
pub enum AxiomKind {
    ...,
    IofAssertion,
    IofRefutation,  // NEW
    ...
}
}

Body shape mirrors IofAssertionBody exactly (concept_id + individual_id). The semantic difference is carried in the variant tag, not in body fields. Encoding/decoding follow the same pattern as IofAssertion.

Symmetrically, a relation-tuple refutation lands as RelationTupleRefutation parallel to RelationTuple for the N-ary case. Same body shape; same variant-tag carries the polarity.

Lean drift (3)

Argon.Storage.AxiomKind gains iofRefutation and relationTupleRefutation constructors with @[language_interface] carried. The Lean side reads only the algebraic content; the bilattice/federation machinery is unchanged because it already handles Truth4.not symmetrically.

Materializer (4)

Store::materialize_predicates_for_standpoint is extended:

• Maintain TWO per-source extents: positive: RelationCatalog and negative: RelationCatalog.
• IofAssertion events stamp positive; IofRefutation events stamp negative.
• Symmetric handling for RelationTuple / RelationTupleRefutation.

The output is PerSourceExtents { positive, negative } rather than a single RelationCatalog.

Dispatcher (5)

Store::query_dispatch for federated queries classifies each (relation, tuple) pair via the cross-product of per-source extents:

for each source S:
    in_pos = tuple ∈ positive[S].entry(rel)
    in_neg = tuple ∈ negative[S].entry(rel)
    truth4_S(tuple) =
        match (in_pos, in_neg) {
            (true,  false) => Is,
            (false, true ) => Not,
            (true,  true ) => Both,   // S already contradicts itself
            (false, false) => Can,    // S has no evidence
        }

The full row classification feeds query_derive_federated exactly as before; the AFT info-join over per-source Truth4 values yields the final row tag.

For derived (rule-output) relations, rule evaluation runs against the positive catalog per source as before; Truth4::Not contribution only arises when the rule’s head is one a refutation event positively names — which is unusual for rule heads but legal. Per-source Truth4::Both from a single source is the contradiction-with-self case (pub fact P(a); pub not_fact P(a); inside the same standpoint block) — useful as an internal consistency check; federation then surfaces it as Both.

Soundness

The implementation is the operational discharge of federate_eq_both_iff:

• A federated row surfaces Truth4::Both ⟺ some source’s per-tuple Truth4 is Both, OR some source contributes Is and another contributes Not.
• This is exactly the Lean theorem.

aft_discharges_T3_obstruction then lifts: sheafClassify of the federated row’s contribution list is obstructed ⟺ row tag is Both. The runtime now exhibits the contextuality-detection case the proven theorem characterizes.

Diagnostics

• OE0640 NegativeFactArityMismatch — pub not_fact P(x, y) where P has arity 1 (parallels positive-side checks in RFD 0004).
• OE0641 NegativeFactUndeclaredPredicate — pub not_fact P(x) where P is not a declared concept or relation.
• Stratified-NAF / strong-negation interaction inside rule bodies is out of scope for this RFD: rule bodies admit only not (NAF). A future RFD may add ~ (strong negation) as a body atom, but that work composes cleanly only after IofRefutation exists at the wire level.

Rationale

Why this and not just NAF

NAF is reasoning-time and absent from the wire format. It already exists. The bilattice value Truth4::Not represents positive evidence of refutation — distinct from NAF’s “no positive evidence”. Without strong negation, a standpoint cannot DISTINGUISH “I don’t know whether P(alice) holds” from “I know P(alice) does NOT hold”. These are different epistemic states and the bilattice is designed to track exactly that distinction.

Why a new AxiomKind, not an extension of IofAssertion

Three reasons:

1. Clean Lean drift. @[language_interface] checks variant alignment. Adding a body field forces every existing consumer to handle a new field; adding a sibling variant only forces consumers of the new variant to handle it. RP-004 chose the second pattern (IofAssertion, RelationTuple, PropertyAssertion are all sibling variants), maintaining symmetry.
2. Storage efficiency. A standpoint with mostly positive facts wastes a byte per event encoding polarity: false. A separate kind allows the encoder to omit the discriminator in the common case.
3. Diagnostic and tool surface. axiom-events queries that want all refutations for a standpoint scan by kind == IofRefutation directly. A polarity-field design forces every consumer to decode-and-test.

Why declaration-level, not rule-body

The conflation of strong negation and NAF in rule bodies is a known source of confusion in logic-programming languages (Gelfond-Lifschitz 1991 §1: “the two negations are often conflated in practice, leading to subtle bugs”). Argon’s design discipline is to surface them as distinct categories: NAF as a rule-body operator on the extent at evaluation time, strong negation as a declaration form that ships through the wire format. This RFD keeps to that discipline.

Why now, not as part of RFD 0004

RFD 0004 was scoped to positive ground-truth facts. The federation runtime didn’t exist then; the gap was theoretical. With federation operationally complete (commits 14–16 + standpoint scoping + dispatcher), the gap is now load-bearing: it gates the headline competitive claim (vault: bilattice-native runtime, category C, “production-scale systems do not”). RFD 0004’s deferral was correct then; closing it is correct now.

Why the standpoint federation is the right host for this

The bilattice’s most distinctive value (Both) is a cross-source notion: it requires two sources contributing opposite verdicts on the same proposition. Single-source Both arises only from a source contradicting itself (legal but unusual). Federation is the natural host because federation is where cross-source disagreement is computed. Implementing strong negation as a fact-declaration form makes it composable with the federation runtime already wired.

Alternatives

A1: pub fact !Person(alice);

Reuse pub fact with a ! prefix on the head atom. Closer to logic-programming notation. Rejected: harder to grep, conflates positive/negative in the same surface form, makes the elaborator’s per-form dispatch fuzzier, and reads worse in error messages.

A2: pub fact not Person(alice);

not keyword inline. Rejected: collides with the existing rule-body NAF not, the exact conflation Gelfond-Lifschitz warned against. Different surfaces for different semantics is a feature.

A3: Extend IofAssertion with a polarity: bool body field

Single AxiomKind, body carries polarity. Rejected per §Rationale above (Lean drift symmetry, storage efficiency, tool surface).

A4: Defer until rule-body strong negation is also designed

Bundle both surfaces into a single RFD. Rejected: declaration-level refutation is a complete, independently-useful feature — every modeler can write pub not_fact P(x); and benefit immediately; rule-body strong negation requires non-trivial stratification work (~ P(x) interacts with NAF and defeasible rules in subtle ways and probably needs an answer-set-style semantics). Shipping declaration-level first lets us learn from usage before designing the rule-body half.

Consequences

What modelers gain

pub standpoint internal_audit {
    pub fact employed_by(alice, AcmeCorp);
}

pub standpoint public_record {
    pub not_fact employed_by(alice, AcmeCorp);
}

pub query employment() -> employed_by
    across [internal_audit, public_record];

The query returns (alice, AcmeCorp) tagged Truth4::Both — explicit, runtime-visible, modeler-actionable evidence of cross-source disagreement. Under #[federate(strict)] this surfaces as OE1302 FederationDisagreement (other agent’s renumbering); under default paraconsistent the row surfaces with the Both tag intact.

This is the operational moat Argon claims and nobody else delivers (per the vault note).

What changes for existing code

Nothing breaks. Every existing source compiles unchanged because pub not_fact is a new declaration form parsed by a new branch; existing pub fact lowering is untouched; existing federation queries return identical results when no source uses not_fact (because no Truth4::Not enters the contribution list, so the info-join behaves identically).

What this opens up

• Rule-body strong negation (future RFD): ~ P(x) in rule bodies, with answer-set-style or AFT-stable-pair semantics.
• Refutation rules (future RFD): derive ~ Adult(p) :- Adolescent(p) — deriving negative extents from rules, not just facts.
• Per-relation closure declarations (future RFD): a relation explicitly marked CWA could auto-emit IofRefutation for every tuple not asserted, making CWA reasoning composable with federation.

Open questions

1. Wire-format symmetry with Retract. Should Retract of an IofAssertion event subsequently restate the proposition’s status as Can (no positive evidence; no negative evidence) or as Not (positively refuted)? Retract clearly leans toward Can; the semantic gap with IofRefutation is then preserved. The implementation should treat them distinctly.

2. What happens when a single standpoint asserts both pub fact P(a); and pub not_fact P(a);? Per the dispatcher design above, the per-source Truth4 becomes Both directly; federation then surfaces Both. Should this also be a build-time error (single-source consistency check), or only a runtime tag? RFD position: lower without error; the bilattice tag IS the diagnostic. A separate #[strict_internal] per-standpoint attribute could opt into build-time rejection in a future RFD.

3. Diagnostic emission scope. Should OE0640/OE0641 ALSO be emitted at federation-query time when sources disagree even under #[federate(strict)]? No — the strict-policy case is already covered by OE1302 FederationDisagreement (other agent’s renumbering). OE0640/OE0641 are build-time arity/declared-predicate checks; they don’t need a runtime counterpart.

References

• RFD 0004 §Future Work — “Negative facts / classical negation”
• RFD 0007 — Missing-value semantics (the related distinction between three field intents)
• RFD 0008 — Standpoint-Sheaf Equivalence Proof Roadmap (Path A discharge)
• Argon.Foundation.Truth4 — bilattice carrier with .not constructor
• Argon.Standpoint.Federation.federate_eq_both_iff — proven theorem this RFD makes runtime-observable
• Argon.Standpoint.AFTEquivalence.aft_discharges_T3_obstruction — sheaf-equivalence discharge
• Gelfond, M. & Lifschitz, V. (1991). Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing.
• Belnap, N. D. (1977). A useful four-valued logic.
• Vault: Bilattice-Native Query Evaluation — operationality levels (a/b/c)
• Vault: AFT-Grounded Truth Value Semantics for Argon — the AFT pair correspondence

RFD 0011 — Aggregate semantics under OWA

• State: discussion
• Opened: 2026-05-29
• Decides: how aggregate atoms (sum, count, min, max, avg, set_collect, …) evaluate under OWA when filter or input cells carry Can verdicts; the per-mode default semantics (query / derive / check / fn); the diagnostic surface that makes the projection observable rather than silent; the aggregation-metadata envelope that surfaces interval bounds and excluded-cell counts at every data-system boundary; resolves RFD 0007 OQ3.

Question

Argon admits aggregate atoms in rule bodies and query bodies (§6.6, §7.3.1, §7.4): sum(i.value for i in income where i.taxable) > threshold and friends. Under OWA, the filter predicate i.taxable can evaluate to Can (per RFD 0007’s required-field-under-OWA lift). The substrate has not specified what aggregates do with Can-valued cells.

The spec at §12.2 has only one nearby sentence: “Set / list / record projections: Can-valued cells are omitted from the result set.” Applied literally to aggregates this is silent fail-closed at the filter — Can-cells get dropped, the sum is a definite number, the comparison yields a definite verdict, and the modeler never learns that the answer depended on uncertain data they did not see. This is the SQL-NULL bug at scale. For a language whose primary contract is “OWA semantics done right,” it is an unacceptable default.

But the formal-correctness response (the elaborator forces the modeler to declare an aggregate-Can handling at every site) is hostile to the 90% case: writing reports, dashboards, and analytics queries should feel like SQL, not like coursework on three-valued logic.

This RFD picks the semantics that gives Argon both: SQL-like ergonomics in the default case, OWA-sound interval semantics in the substrate, and a never-silent projection at the surface.

Context

The motivating Slack thread (Almeida + Almeida, 2026-05-28 → 2026-05-29)

Gustavo Ladeira (Sharpe) extended the discussion of RFD 0007 with a concrete query:

pub kind Income {
    taxable: Bool?,
    value:   Money,
}

pub query AllIncome() -> [Income] :- i: Income, select i

pub derive TotalTaxableIncomeExceedsThreshold(threshold: Money) :-
    sum(i.value for i in AllIncome() where i.taxable) > threshold

He asked: “does the derive resolve to Can if both lines below hold simultaneously?

sum(i.value for i in AllIncome() where i.taxable == true) <= threshold
sum(i.value for i in AllIncome() where (i.taxable == true) || (not exists i.taxable)) > threshold

He had derived the interval-bound semantics for monotone aggregates in his own message: lower bound = sum over confirmed-true filter; upper bound = sum over confirmed-true OR Can filter; verdict is Can exactly when the threshold falls in the open interval. The spec did not have a rule giving him that semantics.

João Paulo Almeida (UFES) had separately raised the structural-vs-epistemic ambiguity of Bool? (RFD 0007’s motivating point), which compounds: under structural-optional Bool?, Gustavo’s None-cells are not taxable (a positive fact of absence) and the aggregate is definite by structural exclusion; under epistemic Bool + OWA, missing taxable lifts to Can and the interval semantics is what he wants. RFD 0007 resolved the surface ambiguity. This RFD resolves what happens once the Can-cells reach an aggregator.

Substrate readiness

• Aggregate grammar is in §6.6 / §7.3.1 (atom shape: aggregate (comp-op expr)?; expression shape: aggregate ::= ('sum'|'count'|'min'|'max'|'avg') '(' expr ('for' Ident 'in' expr ('where' expr)?)? ')').
• Aggregate runtime is not yet implemented. oxc-reasoning/src/compile/rule.rs:78 returns RuleCompileError::AggregateNotYet. The semi-naive executor classifies aggregates at the expressive tier (§10.1) and rejects them; no execution path exists. This RFD is greenfield design, not a behavior change.
• Lean mechanization has no Reasoning/Aggregate.lean. The Truth4 substrate (Foundation/Truth4.lean) + the K3 conjunction in Reasoning/Fixpoint.lean give the operators an aggregate semantics can build on; the aggregate-specific theorems do not yet exist.
• Truth4 projection is documented at §12.2: K3 fail-closed projection (Pietz–Rivieccio Exactly-True) folds Can → false for Bool, omits Can-cells from set/list/record results. This RFD threads the aggregate question through that projection rule without contradicting it.

Why the obvious answers fail

Three semantics, evaluated independently:

No single option covers all aggregator kinds. The decision is to combine them with type-driven projection, so the modeler picks the level of sophistication via the result type while the substrate always evaluates soundly.

Decision

Three rules, applied in order. Each rule is one click away from the next; the modeler picks the level at which they want to engage with Can.

Rule 1 — The substrate evaluates aggregates in Truth4

Under OWA, an aggregate agg(expr for x in S where φ(x)) evaluates over a Truth4-tagged set:

{ x ∈ S : φ(x) ∈ {Is, Can} }

— with each element marked by its filter verdict. The aggregator’s behavior on this tagged set depends on its monotonicity class:

Monotone aggregators (interval bounds)

For sum over non-negative values, count, set_collect:

lower = agg over { x : φ(x) is Is(true) }
upper = agg over { x : φ(x) is Is(true) or Can }

For sum over signed values, the bounds are sign-partitioned: lower = sum(Is) + sum(negative-valued Can cells); upper = sum(Is) + sum(positive-valued Can cells). This is monotone in each sign-class independently and computable in a single pass.

The aggregator returns the Truth4-lifted interval — internally a pair (lower, upper) carried as Truth4Of<T> with bounds metadata.

Non-monotone aggregators (propagating)

For min, max, avg, percentile, string_join, count distinct:

if { x : φ(x) is Can } is empty:
    result = agg over { x : φ(x) is Is(true) }    // definite verdict
else:
    result = Can                                   // any Can in filter set
                                                    // propagates to whole result

These aggregators have non-monotone bounds (min(A ∪ B) ≤ min(A) and the upper bound depends on Can-cell values that aren’t known), so interval semantics gives vacuous bounds in the worst case. Propagating is the only sound default that doesn’t over-claim; modelers who want sharper semantics narrow the filter explicitly to Is-only.

Aggregator-kind taxonomy

The classification is fixed at the aggregator-kind level, not per-call.

Rule 2 — The surface projection is type-driven

The Truth4-tagged aggregate result propagates until it hits a typed boundary (the declared return type of the enclosing query/derive/fn, the head of a derive, the predicate of an if/match, the membership-witness of a refinement clause). At the boundary, the §12.2 K3 fail-closed projection fires, governed by the boundary’s declared type:

A modeler switches between ergonomic and sound semantics by changing one type annotation:

// Ergonomic: SQL-like; projects Can → false at Bool boundary.
pub query QuarterlyOK() -> Bool {
    sum(i.value for i in income where i.taxable) > threshold
}

// Sound: preserves three-way verdict for caller.
pub query QuarterlyOK() -> Truth4Of<Bool> {
    sum(i.value for i in income where i.taxable) > threshold
}

For derive rule heads, the same dial applies via the head type. A pub derive Foo(p: Person) is Truth4Of<Bool> rule populates a Truth4-aware IDB relation; consumers reading Foo(p) get Is | Not | Can directly.

Rule 3 — The projection is never silent

Two pieces ensure the modeler always sees the soundness picture, no matter which projection they chose.

3a. Per-projection diagnostic

Every fail-closed projection at an aggregate boundary emits a diagnostic with the interval bounds and excluded-cell count. The diagnostic level depends on the mode:

The diagnostic carries:

14:5: info[OW0613]: aggregate filter projection fail-closed
  |
14 |   sum(i.value for i in income where i.taxable) > threshold
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  | filter `i.taxable` may evaluate to Can; verdict projects to Bool with
  | Can → false (Pietz–Rivieccio Exactly-True, §12.2). Interval bounds for
  | this materialization: [$1,234,567.00, $1,256,789.00]; 5 Can-cells.
  |
help: change return type to Truth4Of<Bool> to preserve Can verdict:
  pub query QuarterlyOK() -> Truth4Of<Bool> { … }
help: or filter explicitly to suppress this diagnostic:
  ... where i.taxable is Is(true)              // fail-closed, explicit
  ... where i.taxable is Is(true) or Can       // include unknowns
help: silence per-rule with #[allow(aggregate_fail_closed)]

The diagnostic is suppressible per-site with #[allow(aggregate_fail_closed)]; in check mode, the diagnostic is OE0614 (error) and the only opt-out is #[check(fail_closed)] on the check declaration, which makes the soundness loss explicit at the check site.

3b. Per-result metadata envelope

Every aggregate query result, regardless of projection target, carries an aggregation_metadata envelope alongside the projected value. The envelope is always present when the aggregate’s filter set could have been Can-valued; it is absent when the aggregate is provably Can-free.

JSON shape (REST / wire format):

{
    "value": true,
    "aggregation_metadata": {
        "result_type": "Bool",
        "projected_from": "Truth4Of<Bool>",
        "projected_verdict": "Is(true)",
        "interval": { "lower": 1234567.00, "upper": 1256789.00 },
        "excluded_can_cells": 5,
        "excluded_can_value_bounds": { "lower": 22222.00, "upper": 22222.00 },
        "verdict_robust": true
    }
}

verdict_robust = true iff the projected verdict would be the same across every completion of the Can-cells. When false, the modeler / auditor / dashboard sees that the answer depended on the projection — exactly the SQL-NULL bug made visible.

CLI presentation (ox query):

$ ox query QuarterlyOK
true

(aggregate: 5 of 100 income rows had Can-valued `taxable`;
            bounds [$1,234,567, $1,256,789];
            verdict robust to all completions)

ox query --explain prints the full envelope; standard text mode prints a one-line summary when excluded_can_cells > 0. The envelope is computed during the substrate’s Truth4 evaluation (the bounds are already needed for monotone aggregators), so the runtime cost is one allocation per aggregate, not an extra pass.

Per-mode default summary

Worked example — Gustavo’s case

After this RFD lands, Gustavo’s pattern, with the epistemic-Bool surface (per RFD 0007) and the sound-three-verdict return type:

pub kind Income {
    taxable: Bool,                // required + OWA — epistemic reading
    value:   Money,
}

pub query AllIncome() -> [Income] :- i: Income, select i

pub derive TotalTaxableIncomeExceedsThreshold(threshold: Money)
        is Truth4Of<Bool> :-
    sum(i.value for i in AllIncome() where i.taxable) > threshold

The substrate’s monotone-sum evaluates to Truth4Of<Money> with bounds [lower, upper] per Rule 1. The comparison > threshold lifts pointwise:

threshold <  lower            → Is(true)    // every completion exceeds
threshold >= upper            → Is(false)   // no completion exceeds
lower <= threshold < upper    → Can         // depends on which Can-cells are taxable

The head type Truth4Of<Bool> preserves the verdict (Rule 2). Consumers read TotalTaxableIncomeExceedsThreshold(threshold) and pattern-match on the three outcomes. No diagnostic fires (Rule 3) — the modeler chose the sound path explicitly.

If Gustavo had written is Bool on the head, the verdict projects fail-closed (Can → false), the diagnostic fires at warning level (derive mode), and the materialized IDB record carries false for the Can-case threshold. The metadata envelope on the query result still shows the bounds and Can-cell count.

Rationale

Why “substrate sound, surface projected” rather than “force the modeler”

The earlier draft of this design (A1+B1 from the Slack discussion) made the elaborator hard-error at every where-clause that could be Can, requiring the modeler to declare an aggregate-Can handling explicitly. This was formally correct but practically hostile: every aggregate over OWA data in a routine query would error until the modeler annotated. Argon’s contract as a practical data systems language requires that day-to-day analytics queries — reports, dashboards, ad-hoc SQL-like exploration — feel like SQL with one knob upgraded, not like a three-valued-logic seminar.

The substrate-Truth4 + surface-projected design separates the two concerns. The substrate always evaluates with Truth4 fidelity (the OWA-soundness contract is preserved regardless of what the modeler writes). The surface projection is type-driven: the modeler picks ergonomic Bool or sound Truth4Of via the return type, with the type-system change costing one character. The “never silent” rule ensures the modeler is informed about the projection at every fail-closed site without being blocked. This is the design SQL should have had.

Why the per-mode default split

query is the analytics surface — ergonomics-first. derive populates the IDB and propagates downstream; an unsound derive contaminates many subsequent rules. check is compliance — a check that silently fails-closed and misses a violation is the worst possible failure mode for the system. The diagnostic level escalates monotonically with the cost of silent-wrong: info → warning → error.

This is symmetric with how Rust handles Result<T, E>: ignoring the error is allowed but loud (#[must_use] warning by default), and the language never forces you to handle every case at every call site. The “you must handle this” boundary is at the typed-result boundary, not at every intermediate computation.

Why the metadata envelope is always-present (not opt-in)

The bounds and Can-cell counts are computed by the substrate regardless (they’re load-bearing for the monotone interval evaluation). Surfacing them at the result boundary is near-free. Making them opt-in (?metadata=true) would mean most data-system consumers — dashboards, CSV exports, REST clients — never see them, and the SQL-NULL bug returns silently. Always-present means the auditor / debugger / pipeline-engineer always has the evidence; the cost is a few extra bytes per result.

The CLI’s one-line summary (only printed when excluded_can_cells > 0) keeps the common-case output clean while still being honest. ox query --explain shows the full envelope.

Why interval semantics, not propagation, for monotone aggregators

Propagation (any Can → whole result Can) is sound but loses real conclusions. When sum-over-Is alone already exceeds threshold, the verdict is definitively Is(true) regardless of the Can-cells; propagation would still say Can and the modeler / system / auditor would get a less informative answer than the data supports. Interval semantics extracts the maximum signal from the partial data without over-claiming.

For non-monotone aggregators, interval semantics gives vacuous bounds (e.g., min with Can-cells could be anything in the Can-cells’ value range); propagation is the right default there because the alternative is bounds that don’t constrain. The taxonomy fixes the classification per-aggregator-kind so modelers don’t have to reason about which gets which.

Alternatives considered

A. Silent fail-closed (the SQL-NULL default, what §12.2 implies today)

Can-cells dropped from filter set; aggregate produces a definite verdict; modeler never told. Rejected. Reproduces the SQL-NULL bug at the OWA scale. Argon’s substrate guarantees OWA-soundness; a surface that silently violates the guarantee defeats the language’s central pitch.

B. Hard-error at every aggregate over Can-potential filter (the original A1+B1)

Elaborator refuses to compile until the modeler annotates the aggregate with one of is Is(true) / is Can / propagating. Rejected. Hostile to practical analytics — every query against OWA-required field must annotate; the migration cost from existing codebases is enormous; the friction undermines the data-system-as-product story.

C. Always-Truth4Of return type

Aggregators always return Truth4Of<T>; modelers must pattern-match to extract a value. Rejected. Most aggregator results are immediately compared or summed downstream where the ergonomic fail-closed projection is what the modeler wants; forcing Truth4Of<T> everywhere is the same hostile-friction problem as B.

D. Per-call annotation in the aggregate body

sum(i.value for i where i.taxable mode=interval) > threshold. Rejected. Annotation is at the wrong site — the modeler’s intent is about the projection, not the aggregator. The return type is the natural place to declare it.

E. Two-pass query model (run with one semantics, switch interactively)

ox query defaults to fail-closed; modeler runs ox query --reanalyze sound if they want to see the Can-case. Rejected. Doesn’t work for batch / programmatic consumers, and the modeler doesn’t know to ask the second time unless something cues them. The always-present metadata envelope (Rule 3b) gives the same effect without the second invocation.

F. Defer entirely

Wait until the aggregate executor lands (oxc-reasoning::AggregateNotYet) and decide then. Rejected. The executor needs this decision before it can be implemented; the design space has been actively explored; settling now means the implementation doesn’t ship with an ad-hoc choice. RFD 0007 OQ3 already promised follow-on; this is it.

Consequences

What lands

Substrate impact

• One new theorem in Reasoning/Aggregate.lean: for any monotone aggregator A over a filter predicate φ, the interval [A(Is), A(Is ∪ Can)] is a sound over-approximation of every completion of the KB. Proven by induction on the K3 fixpoint already established in Reasoning/Fixpoint.lean.
• No change to subsumption_axiom, iof_assertion, relation_tuple wire formats. The metadata envelope is computed at query time, not stored.
• No change to the Z-set Storage model. Aggregates are evaluated over materialized relation extents, which already carry the Truth4 tags from the underlying fixpoint.

Modeler impact

• Routine analytics queries compile unchanged; behavior is SQL-NULL fail-closed but with bounded transparency via the metadata envelope and the info-level diagnostic.
• Soundness opt-in is a one-character type change (Bool → Truth4Of<Bool>).
• check rules get stricter default — modelers writing compliance checks must engage with Can or explicitly opt out, which is the right default for compliance.
• Existing rules that compiled under the unimplemented-aggregate path will compile under this RFD with the same surface; behavior change vs the unimplemented baseline is the addition of the diagnostic and the metadata envelope.

Tooling impact

• ox query shows aggregate summaries by default when Can-cells were excluded.
• ox query --explain shows full metadata envelopes.
• LSP can surface the diagnostic inline; debuggers can read the envelope.
• REST adapters return the envelope alongside results; clients can ignore it or render it.

Compatibility

The aggregate executor is a new implementation; there is no prior behavior to preserve. The grammar surface is unchanged. The metadata envelope is additive; consumers that don’t read it see the same JSON shape they would have seen.

Open questions

OQ1 — Aggregator-kind monotonicity classification under user-defined aggregators

When modelers register custom aggregators via pub aggregate (a future grammar surface for plugin aggregators), how do they declare the monotonicity class? Likely via attribute (#[monotone] / #[propagating]) on the aggregator declaration. Out of scope for this RFD; document when the custom-aggregator surface lands.

OQ2 — Aggregate-of-aggregate composition

What does sum(count(j.value for j in i.children) for i in roots()) look like under partial Can data? The inner aggregator produces a Truth4Of<Nat> interval per row; the outer aggregator over a sequence of intervals needs an interval composition rule. For monotone outer aggregators over interval-valued inputs, the composition is sum-of-bounds — pointwise interval arithmetic. Specify in the Reasoning/Aggregate.lean mechanization; document examples in §7.4.

OQ3 — Interaction with temporal aggregates (§6.10.5 + §7.3.2)

DatalogMTL operators since/until combined with aggregates. Under OWA + temporal Can, the interval bounds need to factor in the temporal extent. The temporal substrate’s three-valued evaluation (§6.10.5) composes pointwise; the aggregate’s interval semantics composes monotonically; the combined semantics needs verification. Likely lands in a follow-on RFD on temporal-aggregate semantics.

OQ4 — #[brave] mode interaction

§7.3 admits #[brave] for stable-model semantics. Under brave + OWA, aggregates need to evaluate across stable models. Each stable model produces a definite verdict; the aggregate result is the join across models. Out of scope; document when the brave-semantics RFD is written.

OQ5 — Metadata envelope schema versioning

The envelope is a wire-format addition; future fields (additional bounds, multiple Can-cell categorizations) require a schema version. Adopt the oxc-protocol versioning policy from RFD 0001; envelope carries a version: 1 field.

OQ6 — Persistent aggregate caching under metadata

Salsa-cached aggregate results need to track the metadata envelope; cache invalidation when Can-cells are resolved (via subsequent insert facts) must re-fire dependent aggregates. Likely a small extension to the Salsa cache key but worth verifying with the oxc-runtime Salsa wiring.

References

• RFD 0007 — Missing-value semantics under OWA §OQ3 — the open question this RFD resolves
• §6.6 (aggregate expression grammar), §6.9 (CWA/OWA), §6.10.5 (Kleene truth tables), §7.3.1 (rule-atom aggregates), §7.3 line 72 (“stratified aggregates”), §7.4 (query mode), §12.2 (K3 fail-closed projection)
• oxc-reasoning/src/compile/rule.rs:78 — AggregateNotYet (the implementation site)
• Foundation/Truth4.lean, Foundation/Projection.lean, Reasoning/Fixpoint.lean — substrate mechanization this RFD builds on
• Faber, W., Pfeifer, G., Leone, N. (2011). Semantics and complexity of recursive aggregates in answer set programming. Artificial Intelligence — the stratification rule §7 cites
• Pietz, A. & Rivieccio, U. (2013). Nothing but the truth. Journal of Philosophical Logic — the K3 fail-closed projection
• Belnap, N. (1977). A useful four-valued logic — the underlying bilattice
• Almeida, J.P.A. (UFES) & Ladeira, G. (Sharpe), Slack thread, 2026-05-28 → 2026-05-29 — the motivating discussion

RFD 0013 — Toolchain distribution + oxup toolchain manager

• State: accepted — partially implemented (Stage 0 deployed, Stage 4 merged)
• Opened: 2026-06-01
• Last revised: 2026-06-02
• Decides: how Argon ships to engineer laptops (Mac arm64) + ODE sandbox AMIs (Linux arm64 + x86_64); whether to adopt a rustup-style toolchain manager; the AWS-hosted distribution architecture; the ~/.argon/ legacy-install cleanup story.
• Status: Implemented — the v0.2 toolchain shipped; this RFD is the design record.

Question

v0.1.0 ships a single ox binary from a homemade install.sh against git clone. For Sharpe-internal v0.2, what’s the install + distribution + toolchain-management story?

Decision

Adopt the rustup-style architecture with an oxup manager binary + argv[0] dispatch, splitting the compiler into four logical tools (oxc / ox / ox-lsp / oxfmt), distributed via AWS S3 + CloudFront at argon.sharpe-dev.com (managed via Pulumi in the shared infra account 285688017134). The user-facing reference is the book Toolchain chapter; the dist mechanics live in infra/ + the release pipeline.

Sharpe-internal scope means: no LICENSE / no Marketplace publish / no public installer; private bucket via Cloudflare-proxied CloudFront; CI’s ArgonReleaseRole is narrow-scoped (S3 PutObject + CloudFront invalidate only). Okta-gated downloads deferred to v0.3 (separate RFD).

Account note: the distribution lives in AWS account 285688017134, which is the default SSO profile (~/.aws/config) — the shared infra account where the ODE/orca-mvp Pulumi stacks, the s3://sharpe-pulumi-state backend, and the *.sharpe-dev.com wildcard ACM cert already live. It is not the shared-admin profile (account 548277374575, which is empty). Maintainers authenticate with assume default / AWS_PROFILE=default.

Implementation status (2026-06-02)

• Stage 0 deployed to account 285688017134: S3 argon-dist-sharpe + CloudFront E16VOSAVQFX5Y8 (argon.sharpe-dev.com, proxied) + ArgonReleaseRole (OIDC). Edge verified (HTTP 403 = healthy empty bucket).
• Stage 4 merged (PR #6): release.yml publish-dist (OIDC → S3 → CloudFront) + nightly cron, wired via repo secret AWS_ROLE_ARGON_RELEASE + var ARGON_CLOUDFRONT_DIST_ID. Graduated to the §5 toolchain (Stages 1–3 having landed): builds all four binaries, assembles argon-<v>-<plat>.tar.gz via scripts/assemble-toolchain.sh, and publishes the [artifacts.*] channel-<channel>.toml via scripts/make-channel-manifest.sh — the schema oxup install consumes (round-trip tested in oxup/src/fetch.rs; the format is pinned by scripts/make-channel-manifest.sh). Fixed two latent contract bugs (bare-ox tarball; [platforms.*] vs [artifacts.*] manifest).
• Stays in the mgmt account (285). A move to a workload account (prod/623) was investigated and rejected: the workload-account org SCP p-pif76ezm denies s3:PutBucketPolicy / PutBucketPublicAccessBlock to interactive SSO admins, so the CloudFront-OAC bucket policy can only be set by an SCP-exempt CI role. For an internal static CDN that’s not worth a full CI-driven deploy apparatus; 285 (where SSO admins can set bucket policies) is the right home for maintainer-operated tooling. Maintainer-local pulumi up runs from nix develop .#infra.
• Adjacent: Argon-aware PR review bots (claude-review.yml + claude.yml, PR #7) landed alongside this work.
• Remaining: Stages 1–3, 5–7 (binary split → share/std/ → oxup → oxfmt → hosted install.sh → smoke) → tag v0.2.0.

Scope of infra/

This RFD authorizes the new top-level infra/ directory holding the Pulumi project (TypeScript + Bun, matches the ODE pattern at ontology-tooling/infra/) that creates the distribution stack:

• argon-dist-sharpe S3 bucket (us-east-2, private, OAC-only read)
• CloudFront distribution (PriceClass_100, TLS 1.2+, two cache policies)
• Reuse of the existing *.sharpe-dev.com wildcard ACM cert (us-east-1)
• Cloudflare CNAME argon.sharpe-dev.com → CloudFront (proxied / orange cloud)
• ArgonReleaseRole IAM role with GitHub OIDC trust for sharpe-dev/argon tag pushes

Maintainers run pulumi up locally with the default profile (assume default). CI never touches the infra stack — only the ArgonReleaseRole it outputs.

Scope of oxup/

This RFD also authorizes the new top-level oxup/ directory (Stage 3) — a standalone Rust crate (its own Cargo.toml/Cargo.lock, not a member of compiler/’s workspace) so it stays cheap to build for bootstrap. It is a single binary with argv[0] dispatch:

• Invoked as ox/oxc/ox-lsp/oxfmt (via symlinks), it resolves the active toolchain (§4) and execs the real tool from ~/.argon/toolchains/<spec>/bin/<tool>.
• Invoked as oxup, it’s the manager CLI (init/install/update/default/list/which/uninstall/self-update).

Decomposition (decided during Stage 2/3): Stage 3 lands in two PRs.

• 3a — network-free foundation: the crate, argv[0] dispatch, toolchain resolution (§4 precedence), the ~/.argon layout, and the local manager commands (which/list/default/uninstall). Its own CI job in check.yml.
• 3b — the network layer: install/update/self-update + auto-fetch-on-miss from argon.sharpe-dev.com, plus the release.yml §5 tarball (bin/ + share/std + manifest.toml) the fetch consumes. 3b also drops the Stage 2 stdlib embed once the tarball ships share/std. Gated on the release pipeline producing real toolchains.

Three-platform build matrix (v0.2)

• macos-arm64 — all Sharpe dev machines (Apple Silicon)
• linux-aarch64 — ODE sandbox AMIs + arm Linux CI runners
• linux-x86_64 — generic Linux + non-arm CI runners

Intel Mac (macos-x86_64) deferred; Windows deferred.

Build order (eight stages, ~8 focused days)

Out of scope for this RFD

• Okta-gated downloads (Google Workspace SSO) — v0.3 RFD
• Package registry + lockfile — v0.3+ when external deps land
• Apple Developer signing / notarization — internal binaries
• Telemetry payloads — opt-out reserved in settings.toml; no payload sent

See

• The book Toolchain chapter (spec/reference/src/toolchain.md) — the user-facing install/channel/version reference
• /infra/README.md — operator’s guide for running pulumi up
• /infra/index.ts — top-level Pulumi wiring
• ontology-tooling/infra/ — the ODE pattern this design adapts

RFD 0014 — Runtime Serving Surface

State: discussion

Question

Should Argon expose a first-party serving surface for executing a loaded .oxbin against tenant/fork scoped runtime state?

Context

The §19 runtime contract defines the in-process Engine / Module / Store semantics, but Ode and Tide workflows need an executable boundary: load the workspace .oxbin, keep Store state warm, dispatch generated SDK descriptors, and expose forks, snapshots, derive output, and debug traces.

The old kernel and devbox-kernel path mixed this runtime work with live source loading, generated SDK transport concerns, tenant hardcoding, workflow state, and Tide-specific globals. New Argon has a compiled .oxbin, so the runtime serving layer can be Argon-native and narrower.

Decision

Add ox runtime serve backed by an oxc-serve crate. The command serves a versioned /v1 API around a loaded .oxbin:

• GET /v1/health
• GET /v1/module
• GET /v1/schema
• POST /v1/dispatch/query
• POST /v1/dispatch/mutation
• POST /v1/dispatch/compute
• fork-scoped dispatch aliases under /v1/forks/{fork}/dispatch/*
• GET /v1/forks, POST /v1/forks, GET /v1/forks/{fork}
• DELETE /v1/forks/{fork}, POST /v1/forks/{fork}/promote
• GET /v1/forks/{fork}/diff/{other}
• POST /v1/forks/{fork}/derive
• POST /v1/forks/{fork}/derive/trace
• GET /v1/snapshot
• GET /v1/derived/individuals/{id}
• GET /v1/derived/individuals/{id}/explain
• GET /v1/derived/facts/{fact_id}/explain

The serving layer supports mem and pg storage. Both backends preserve the append-only ABox event-log model; derived state and snapshots are projections over .oxbin plus visible events. Postgres additionally owns durable fork records, generation counters, scoped/as-of scans, and projection-cache invalidation.

The generated SDK remains dependency-free and transport-agnostic. It emits types, validators, metadata, descriptors, and wire parse/serialize helpers. It does not import or generate a runtime client.

Rationale

This keeps the core runtime responsibilities inside Argon, where the .oxbin, storage, rule evaluation, and fork semantics live. It also keeps environment concerns outside Argon:

• tenant/principal selection belongs to the caller or proxy,
• Tide workflow state and run journals belong to Tide,
• Ode UI state and visualization layout belong to Ode,
• SDK transport adapters belong to the host application.

The /v1 API is descriptor-based so generated SDKs can call it through a small host transport without coupling generated code to HTTP, Tide, fetch, or a specific deployment.

Alternatives

One alternative was a separate ontology-tooling service that wrapped Argon. That would have duplicated runtime semantics and left forks, storage, and derive behavior outside the implementation that owns them.

Another alternative was generating a full SDK runtime client. That is more ergonomic for simple workflows, but it couples generated output to transport and deployment concerns. The chosen design leaves that as a hand-written host adapter.

Consequences

ox runtime serve is a long-running process and therefore introduces async HTTP dependencies in the compiler workspace. The serving layer must keep a strict boundary: no generic entity writes, no ad-hoc raw query/mutation execution, no Tide or Ode state, no tenant hardcoding, and no SDK transport generation.

Hot reload is allowed only after compatibility checks. Additive schema changes may load; declaration removal or field/relation type changes are rejected when live ABox data exists.

unsafe_logic and forget remain capability-gated. Where the underlying language/runtime substrate is not enabled, the serving API refuses the request instead of pretending the capability exists.

Open Questions

• Whether the full PosBool DNF provenance witness tree should be exposed by the current explain endpoints or by a later provenance-specific API.
• Whether projection caches should become durable response caches for selected read endpoints or stay as backend-maintained invalidation state until DBSP arrangements land.
• The final production IAM mapping for fork, forget, and future unsafe_logic execution budgets.

RFD 0015 — mutate body surface: EdgeQL-shaped, set-semantic

• State: committed
• Opened: 2026-06-03
• Decides: the surface and semantics of the imperative mutate body that §7.5 promises but the v0.1 implementation never shipped (issue #15) — require guards, let bindings, insert-as-expression with named-field entity construction, update … set { = / += / -= }, insert … into …, for iteration, and return; the collection model these operate over (first-class, stored, generic) and its determinism contract (adopts RP-006 Track A / D-133); the subset that ships first to unblock the overlay vs. the full surface; and the commitment to mechanize mutation execution semantics in Lean. Rejects the legacy orca do { } / retract { } / emit { } clause structure. Relates to RFD 0001 (identity), RFD 0006 (field mutability), RFD 0011 (aggregates in guards).

Question

§7.5 documents a full imperative mutate body — preconditions, local bindings, typed-literal entity construction, collection inserts, control flow, and return. §7.5.1 admits the v0.1 implementation ships only a datalog-style subset (insert iof, relation-tuple insert, simple-target update … set, delete, forget) and that everything else “is designed but not yet implemented in the parser, elaborator, or runtime.” Two production mutations in packages/overlay (Ayush & Aryan’s materializeExpectedSatisfaction / recognizeSatisfaction) cannot be expressed without the missing forms; the parser reports OE0001 unexpected token … at module level the moment it meets let/for/return after a require block.

What is the mutate body’s surface and semantics, what does it operate over, and what ships first?

Context

The blocker. The overlay needs, per mutation: a precondition (one with an aggregate — occurrence.value == sum(r.value for r in records)), construction of fresh entities with named fields whose handles are reused downstream (let record = insert ExpectedSatisfactionRecord { … } then timeInterval: period), appending to a collection at a nested path, per-element posting under a for, and a returned result.

Why it doesn’t parse. mutation_stmt (compiler/crates/oxc-parser/src/grammar.rs) recognizes only insert/delete/forget/update; any other leading token falls through recovery, the require { } block’s } is mistaken for the body’s, and the remaining statements are re-parsed at module level.

Three layers, only one of them easy.

1. AST — the Lean already mechanizes the whole imperative body (MutateDecl { require, body : List Stmt }; Stmt = letStmt | insertStmt | updateStmt | forLoop | ifStmt | returnStmt | exprStmt | …; InsertForm = typedLiteral | namedTyped | intoCollection | relation), all @[language_interface]-tagged, so the Rust AST is generated. The grammar exists; the parser just doesn’t build it.
2. Execution — today a body lowers to a flat Vec<Operation> (a datalog DML batch: InsertIof/InsertTuple/Update{set}/Delete/Forget). There are no bindings, no data-flow between statements, no entity minting, no control flow, no return. Individuals arrive as parameters and get classified/updated; nothing is created. This is the real gap.
3. Substrate (Lean) — mutate is deliberately not a substrate rule (lowerRule returns none; it is a “host-runtime entry point”), and its execution semantics are unspecified.

The legacy precedent we reject. The orca-era vault design (D-064) gave mutations a five-clause COBOL-like structure: require { } / do { } / retract { } / emit { } / return. The new Argon already dropped the divisions (the Lean has a flat body : List Stmt, not separate do/retract clauses). This RFD finishes that move in the opposite stylistic direction from imperative paragraphs: SQL/EdgeQL-shaped statements, not COBOL divisions.

The settled direction (this RFD’s design discussion, 2026-06-02/03). The mutate body is imperative-looking but set-semantic, rhyming with EdgeQL: named-field insert as a value, update … set with collection ops, for as set-mapped iteration, guards as preconditions. Collections are first-class and stored (not derived-from-edges) — Set/Map/List are already declared generics in §6 — and governed by a determinism contract (below). Rust-like return types and error handling (Option/Result/?) are explicitly out of scope here.

Decision

1. The body is a sequence of statements; insert is an expression

mutate-decl   ::= attribute* 'pub'? 'mutate' Ident generic-params? '(' param-list ')'
                  ('->' TypeExpr)? mutate-body
mutate-body   ::= '{' stmt* tail-expr? '}'
stmt          ::= require-stmt | let-stmt | update-stmt | insert-stmt
                | delete-stmt | for-stmt | expr-stmt | return-stmt
require-stmt  ::= 'require' (expr | '{' expr (',' expr)* ','? '}') ';'
let-stmt      ::= 'let' Ident (':' TypeExpr)? '=' expr ';'
update-stmt   ::= 'update' expr (':' TypeExpr)? 'set' '{' field-assign (',' …)* '}' ('where' expr)? ';'
insert-stmt   ::= 'insert' insert-form ('since'|'during'|'at' expr)? ';'
insert-form   ::= TypeExpr '{' field-init (',' …)* '}'        // typed-literal: construct + return entity
                | Ident ':' TypeExpr '{' field-init (',' …)* '}'
                | Ident 'into' expr                            // collection add (sugar — see §4)
                | Path '(' arg-list ')'                        // relation tuple / iof — existing
delete-stmt   ::= 'delete' delete-form ('at' expr)? ';'
for-stmt      ::= 'for' Ident 'in' expr '{' stmt* '}'
return-stmt   ::= 'return' expr ';'
field-assign  ::= Ident ('=' | '+=' | '-=') expr               // set / collection-add / collection-remove

insert TypeExpr { … } is an expression that evaluates to the freshly-constructed entity (EdgeQL / SQL RETURNING). This is forced by the binding case (let record = insert … { … } then referencing record), and it makes entity construction compose. Constructing a fresh entity mints a fresh identity per RFD 0001.

2. Return: tail expression, or explicit return (which stays first-class)

• A mutate with -> T must produce a T. The body’s tail expression (Rust’s rule — no trailing ;) is that value; since insert is an expression, ending the body with an insert T { … } returns the new entity with no keyword.
• A value bound with let is returned by a bare tail (sr) or by explicit return sr;.
• return expr; is first-class, not merely an early-exit affordance — it is what makes returning collections, tuples, and (later) Option/Result readable.
• No -> T ⇒ the mutate returns unit; the body is pure effects.
• “Return everything inserted” is rejected as a default (fragile under reordering, ambiguous for multiple inserts). To return several things, the tail is an explicit tuple or collection.

3. Collections are first-class, stored, and governed by determinism-by-observability

Adopts RP-006 Track A / D-133:

• The invariant: no language-observable result (return values, serialization, the mutation event-log order) may depend on hash-derived order. This is stronger than “the implementation is internally deterministic” and is the correct knob — a randomly-seeded hash table is admissible iff order never leaks; a fixed-seed one still couples program meaning to the hasher the moment order is observed, breaking reproducibility across Argon’s in-process / Postgres / DBSP backends.
• Order-sensitivity is a type property. Vec/List are ordered (order is the contract). Set/Map are unordered: the contract forbids observing order; where an observable sequence is unavoidable the language yields a canonical key-sorted order, never hash order.
• Default backing: BTreeSet/BTreeMap (canonical iteration for free; no rehash spikes). A SwissTable/hashbrown Map is the opt-in fast path for lookup-heavy, order-insensitive use. Elastic/funnel hashing (#[dense]) is deferred pending a measured high-density win (RP-006 §5, benchmark harness pending).

4. insert … into … is kept as sugar

insert x into <coll-path> is retained (users coming from SQL INSERT INTO expect it) and desugars to a collection add: insert x into a.b.records ≡ update a.b set { records += x }. The canonical/primitive form is update … set { coll += / -= … }; insert into is surface sugar over it. (Reverses this RFD’s draft decision to drop it.)

5. for is set-mapped, and the event-order leak is closed

for x in coll { … } applies its body per element. To keep the mutation event-log order deterministic (replay, provenance), iteration over an unordered collection proceeds in canonical key-sorted order by default (RP-006 §A.3). When the analyzer can prove the body’s per-iteration effects are commutative (independent updates to disjoint targets — e.g. the overlay’s for r in records { update r.account … } when the r.account targets are distinct), the canonical sort may be elided. DBSP’s Z-set deltas may discharge this automatically for IVM-backed mutations (open question).

6. Atomicity

A mutate body commits as one transaction: all of its effects, or none. A failed require aborts with no events emitted. (Consistent with the append-only event-log substrate.)

7. What ships first

The immediate subset — exactly what compiles residential_lease.ar:

Ayush & Aryan’s mutations in the shipped form:

pub mutate materializeExpectedSatisfaction(
    pair: CorrelativePositionPair, perPeriodValue: Real,
) -> MaterializedExpectedSatisfaction {
    require perPeriodValue > 0;
    let period = insert TimeInterval {
        start: pair.propositionalContent.recurrence.startsOn,
        end:   pair.propositionalContent.recurrence.endsOn,
    };
    let record = insert ExpectedSatisfactionRecord {
        account: pair.book.expectedSatisfactionAccount, value: perPeriodValue,
        timeInterval: period, allenRelator: AllenRelationType::Before,
    };
    insert record into pair.book.expectedSatisfactionAccount.records;   // sugar → update … set { records += record }
    insert MaterializedExpectedSatisfaction {                           // tail = return value
        records: [record], expectedAccount: pair.book.expectedSatisfactionAccount, postedCount: 1,
    }
}

pub mutate recognizeSatisfaction(
    occurrence: OccurrenceEvent, records: [SatisfactionRecord],
) -> SatisfactionRecognition {
    require occurrence.value == sum(r.value for r in records);
    for r in records { insert r into r.account.records; }              // per-element, canonical-ordered
    insert SatisfactionRecognition {
        recordedValue: occurrence.value, satisfactionAccount: records[0].account,
    }
}

8. Lean is a committed deliverable, not a vague “later”

To unblock the overlay we ship the parser + elaborator + runtime for the immediate subset ahead of the mechanized semantics. But the substrate work is a firm obligation, tracked, not optional: (a) refine the Lean AST (insert as expression; +=/-= field-assign ops; for set-semantics); (b) mechanize mutation execution semantics (entity construction & identity, statement sequencing with bindings, collection ops, atomic event emission); (c) the soundness obligation flow-typing already assumes (FlowTyping.lean states, without proof, that mutate writes respect the monotone fixpoint discipline). Per AGENTS.md this is Lean-first substrate work; the only concession is that code may land first to unblock, with the Lean following.

Rationale

• EdgeQL/set-semantic over imperative-procedural. Argon’s working substrate is already relational (relation-tuple and iof edges); a set-at-a-time, expression-valued mutation surface is continuous with it and with the language’s declarative core, where a COBOL-style statement machine would not be. Crucially, the choice keeps ~90% of the syntax §7.5 already documents while changing its meaning — far less throwaway work than a ground-up redesign, and the Lean AST is already close.
• insert as expression is not a stylistic preference; it is forced by let x = insert … + downstream reuse. Once forced, the return design (tail expression) falls out, and “what if multiple inserts” stops being ambiguous because only the tail is returned.
• Determinism-by-observability (RP-006 Track A) lets the language be deterministic and free to use any map backend, by legislating observability rather than implementation. B-tree default because canonical iteration — on the hot path for a KR language — is free, while a hash table pays an O(n log n) sort to honor the same contract.
• Keep insert into because the cost is one desugaring rule and the benefit is meeting SQL-trained expectations; the canonical += keeps the core small.

Alternatives

• Build §7.5 imperative as literally documented (document/OOP model). Rejected: it bakes “entities own arrays you imperatively append to” into the language, away from the relational/EdgeQL direction, and still requires the entire new execution model — so it is not actually cheaper.
• Pure-graph: make collections derived from edges (no stored collections). Rejected by decision: collections are first-class and stored (Set/Map/List), and the stdlib provides them. insert into/for are legitimate operations on stored collection fields, not smells.
• Drop insert into, canonicalize only on +=. Considered and reversed — kept as sugar for ergonomics.
• Auto-return the last/all inserts. Rejected: fragile and ambiguous.
• EdgeQL with … select with no return keyword. Rejected: return must stay first-class for Option/collection/tuple returns and future error handling.
• Elastic/funnel hashing as default backing. Deferred: real result (arXiv:2501.02305) but the win is at high load factors and no hardened implementation exists; gated on a measured Argon-workload win (RP-006).

Consequences

• Parser: mutation_stmt grows from four verbs to the full statement set; insert becomes expression-valued; require/let/for/return/tail-expression parsing; struct-literal-in-tail disambiguation (the Rust if x { S {} } wrinkle).
• AST/elaborator: consume the (already-generated) Stmt/InsertForm nodes; thread an environment for let bindings and insert handles; lower the new forms — the flat Vec<Operation> model grows into a statement/expression evaluation with data-flow.
• Runtime: entity construction with identity minting (RFD 0001); collection field +=/-=; for evaluation with canonical ordering; atomic multi-effect commit; tail/return value.
• Types: the ordered/unordered collection contract (§3) governs all collection use, not just mutations; it should also be reflected in §6 and the type-system Lean. sum/count in guards interacts with RFD 0011 under OWA.
• Stdlib: Set/Map/List implementations + a Rust-like API (parallel workstream; the first push needs only += and list literals).
• Reference: §7.5 / §7.5.1 rewritten from “designed, not implemented” to the shipped surface + the explicit later-list.
• Lean: the obligations in §8 are now tracked work, including closing the flow-typing assumption.
• Research: RP-006 (collection-backend benchmark; Bayesian; topology) proceeds in parallel; none gates this.

Open questions

1. Identity minting details for insert Type { … } — resolved by RFD 0001; confirm the runtime hook and how a minted id appears in the event log / provenance.
2. Are relation/extent tables insert-only-then-read-mostly? (The #[dense]/elastic precondition — RP-006 Q1.)
3. Does iteration dominate the reasoning workload? Validate with a real op-trace before finalizing the B-tree-vs-hashbrown default (RP-006 Q2).
4. Do DBSP Z-set commutative-monoid deltas discharge the for event-order mitigation automatically for IVM-backed mutations? (RP-006 Q3.)
5. Postgres bridge order — can canonical iteration order be pushed into SQL ORDER BY? (RP-006 Q4 — the riskiest leak surface.)
6. if/match in bodies and for-as-returning-comprehension — surface + value semantics, deferred past the first push. Resolved by Amendment 1.
7. Error handling — Option/Result/? and Rust-like return types; their own RFD.

Amendment 1 (2026-06-05) — control flow is expression-valued; bodies and branches are blocks (resolves OQ #6)

OQ #6 left the surface and value semantics of if/match in mutate bodies open. While that gap stood, the two representations drifted: the Lean surface AST split the construct into a value form (Expr.ifExpr / Expr.matchExpr, with bare-Expr branches) and an effect form (Stmt.ifStmt / Stmt.matchStmt, with List Stmt branches), whereas the Rust grammar modelled a single IF_EXPR / MATCH_EXPR over BLOCK_EXPR branches. This amendment settles it.

Decision. if and match are expressions, and their branches/arms are blocks. A block { s₁; … ; sₙ tail? } is itself an expression: it executes its statements for effect and evaluates to its optional trailing expression, or to unit () when there is none (Rust’s block rule, continuous with §1–§2’s tail-expression return and insert-as-expression). The mutate body is a block. There is exactly one if and one match form — a value use (let x = if c { a } else { b }) and an effect use (if c { insert X } else { insert Y }) are the same construct, distinguished only by whether the branch blocks have a non-unit tail.

Why (not the split).

• Rust/Cargo aesthetic — Rust has one if, an expression; Argon defaults to that idiom.
• Consistency — §1/§2 already chose expression-orientation (tail-expression return, insert as an expression). A statement-only if contradicts it.
• Expressiveness — the split cannot express let x = if c { let y = f(); g(y) } else { h() }: a bare-Expr branch admits no statements, and a statement-if yields no value. Block branches give both. The split is a strict expressiveness loss, for no gain.
• No redundancy — one construct, not a value/effect pair that must be kept in sync.

AST / Lean consequence. Add Expr.block (stmts : List Stmt) (tail : Option Expr). Expr.ifExpr / Expr.matchExpr keep Expr-typed branches/arm-bodies (which now admit block), so their signatures are unchanged. Remove Stmt.ifStmt and Stmt.matchStmt — an effectful if/match is Stmt.exprStmt (ifExpr …) over block branches. (for remains a unit-valued effect statement for now; promoting it to an expression is uniform but not required, since it never produces a value — tracked, not blocking.) Because a block-expression runs statements, expression- and statement-evaluation become a single mutual clique; Argon.Runtime.MutationSemantics and its theorems (runMutation_error_noop atomicity, the fresh-monotonicity family) are re-mechanized against the merged induction. The @[language_interface] surface mirror and CoreIR lowering update accordingly.

Code consequence. The parser already yields IF_EXPR / MATCH_EXPR / BLOCK_EXPR. The elaborator routes a block to its body-op sequence and an effectful if/match to control-flow IR (Operation::If / Operation::Match over the branch blocks’ operations), while a pure-value if lowers to Term::IfExpr (evaluated by resolve_term_to_value). The _ => {} catch-all in mutate_lower::lower_body_stmt, which silently dropped unrecognized statements, is replaced by a loud diagnostic. Tracked in #74.

Amendment 2 (2026-06-09) — value-position match realized by the IfExpr desugar; constant-pattern subset; OE0203

Amendment 1 prescribed an Operation::Match control-flow IR alongside Operation::If. The implementation that landed realizes the value half of match differently — and the prescription is amended to match it.

Decision. A value-position match over constant patterns desugars at elaboration to the existing right-nested Term::IfExpr chain — match s { P1 => v1, P2 => v2, _ => v3 } ⇒ if s == P1 { v1 } else if s == P2 { v2 } else { v3 } — with no new IR (no protocol/drift change). For constant patterns the two semantics are identical: ordered first-match, the final arm’s value as the else-branch. The executable pattern subset is payloadless enum constant paths, Int/String/Bool/Date literals, or-patterns of those (consecutive conditions sharing a body), and the wildcard _; the richer §14 forms (binders, payload/record patterns, guards, type tests, is-outcomes) are refused loudly (OE1319) until they land. Exhaustiveness is required (OE0203 at ox check): a final _ arm, or full coverage of the scrutinee’s enum variants when statically known. The same desugar serves every value position — fn bodies, rule-body comparison operands (compiled to CompiledExpr::If in the reasoner), and mutate let RHS / update values / return values / require guards (evaluated by the existing Term::IfExpr arm of resolve_term_to_value); the Lean evalExpr gains the matching .matchExpr arm (evalMatchArms / patternMatchesConst).

Statement-position match (arms running effects) is now realized the same way — no Operation::Match: it lowers to a right-nested Operation::If chain over the arm blocks’ operation sequences (match s { P1 => { ops₁ }, P2 => { ops₂ }, _ => { ops₃ } } ⇒ If(s == P1) { ops₁ } else { If(s == P2) { ops₂ } else { ops₃ } }), reusing the value desugar’s pattern classification and exhaustiveness (same constant subset, same OE0203 / OE1319 sinks; or-patterns expand to consecutive conditions sharing the arm’s operations; a wildcard-only match splices its arm unconditionally behind a hidden Operation::Let of the scrutinee, so an aborting scrutinee — a missing-field projection, say — aborts exactly as in the chained case, matching Lean’s evaluate-scrutinee-first order). Scrutinee Terms are pure, so per-link re-evaluation is effect-free. One scoping caveat: the Lean matchStmt/ifStmt semantics scope arm/branch-local bindings, while the Rust runtime threads one flat environment and currently leaks them past the match/if (pre-existing, recorded drift — #196). The enabling parser change threads an in-mutate-body flag so blocks at any nesting depth (match arms, if branches, for bodies) admit the full mutate statement set — which also fixed update not parsing inside if branches; blocks in value position (a let RHS block, a value-if branch, a value-match arm) refuse effectful statements loudly (OE1321) since value lowering reduces a block to its tail expression. On the Lean side, Stmt.matchStmt gains direct execution semantics (evalMatchStmtArms: ordered first-match, the selected arm’s block runs for effect, return propagates), intended-equivalent to the If-chain by construction. Stmt.matchStmt / Stmt.ifStmt are NOT yet removed as Amendment 1 ordered: the A1 encoding (exprStmt over Expr.block arms) needs block evaluation inside evalExpr, which merges the expression/statement interpreter cliques and requires evalExpr to carry control flow for return propagation — exactly the merged-clique re-mechanization A1 itself anticipated; doing it halfway would regress return-in-branch. The removal stays tied to that re-mechanization; the drift is documented at both constructors and in Argon.Runtime.MutationSemantics. OE1318 (Module::unsupported_mutation_forms) remains the gate for the genuinely unexecutable statement forms — emit now parses (EMIT_STMT) and lowers to Operation::Unsupported so it is refused there rather than as a generic parse error.

RFD 0016 — Numeric tower: exact by default

• State: committed
• Opened: 2026-06-05
• Decides: the runtime representation and arithmetic semantics of the numeric tower — specifically that Real is exact (arbitrary-precision rational), Decimal/Money are exact, and machine floats (f32/f64) are the explicit opt-in inexact types; how the reasoner’s value domain represents numbers; and that aggregate folds (sum/avg/min/max) are exact. Resolves the “finer breakdown of the tower … deferred to a follow-up RFD” note in §17.1.

Question

§17.1 lists Real as “real number; runtime-chosen representation (defaults to IEEE 754 f64)” and defers the finer tower (rationals, fixed-point) to a follow-up RFD. But the substrate is already ahead of the book: the slice-4 mutation semantics (Argon/Runtime/MutationSemantics.lean:85) models Value.real : Rat — an exact rational — with exact parseDecimal, toRat, and evalRatBinary. Meanwhile the reasoner’s catalog value domain has no numeric beyond Int (a Real/Decimal/Money literal round-trips as opaque CBOR), so an aggregate like sum(r.value for r in …) where value: Real cannot fold at all.

What is Real’s representation, what does the reasoner store, and is avg exact? And which wins — the book’s “f64” or the Lean’s exact rational?

Context

• Domain. Argon’s flagship workloads are finance and legal (the residential-lease / accounting overlay). For that domain IEEE-754 f64 is a bug generator: 0.1 + 0.2 ≠ 0.3, summed payments drift, and cumulative-satisfaction checks (e.value <= sum(r.value …)) become subtly wrong at the boundary. Exactness is a correctness requirement, not a nicety.
• The Lean already chose exact. MutationSemantics.lean models Real as Rat deliberately (“the spec’s arithmetic is exact”). Per the project’s own rule — where the book disagrees with the Lean on something the Lean covers, the Lean wins; the book is a bug — §17.1’s “f64 default” is the bug.
• avg wants a field. avg over a Real collection is Σ / n. Over rationals this stays exact (rationals are closed under division); over fixed-precision decimals or floats it rounds. Exact Real is what makes avg mathematically clean.
• The reasoner gap. oxc-reasoning’s Value has Int(i64) but no exact Real/Decimal; the fold is Int-only. This blocks the overlay’s Met rule (the motivating case) and any Real/Money aggregate.

Decision

1. Real = exact, arbitrary-precision rational. Numerator/denominator big integers; no precision ceiling; no implicit rounding. This is the canonical Real for the data/ontology substrate.
2. Decimal and Money are exact. Decimal is arbitrary-precision base-10; Money is a currency-tagged Decimal. Both share the exact-rational carrier in the reasoner (a Decimal is a rational whose denominator is a power of ten); the currency tag and display scale are metadata on top. Money arithmetic (§17.1, D-069) is unchanged in typing; only its representation becomes exact.
3. Floats are the explicit opt-in inexact tier. f32/f64 live in std::math::primitive (already the case) and are the only inexact numerics. Real never silently becomes a float. The implicit-widening chain keeps Int → Real (exact ⊆ exact) but the f32 → f64 → Real step is removed — a float reaches Real only via an explicit, lossy to_real-style conversion (a float is not exact, so widening it into the exact tier must be a visible choice).
4. The reasoner value domain carries exact numerics. oxc-reasoning’s Value gains an exact-rational variant; Real/Decimal/Money literals materialize to it (replacing the opaque-CBOR/f64 path). Mirrors MutationSemantics.Value.real : Rat.
5. Aggregate folds are exact. sum/min/max/avg fold over the exact domain: integer-exact when all operands are Int, else promoted to exact rational; avg stays exact (Σ/n as a rational). This mirrors MutationSemantics.foldAggregate.
6. §17.1 is corrected to describe Real as exact arbitrary-precision rational (not f64), and the deferral note is resolved by this RFD.

Rationale

• Correctness-first for the domain. A financial/legal substrate that silently rounds is unfit for purpose; exact-by-default makes “the numbers are right” the default, with floats available when a modeler explicitly wants approximate/scientific compute.
• The Lean is the source of truth. Adopting exact rationals aligns the reference and the implementation to the already-mechanized MutationSemantics; it is reconciliation, not invention.
• avg exactness is a concrete, checkable win unavailable under float or fixed decimal.
• Implementation. The Rust reasoner uses num-rational::BigRational over num-bigint (MIT/Apache-2.0, on the workspace allow-list) — arbitrary precision, exact division, deterministic Ord/Hash over normalized components. Not rust_decimal (96-bit fixed; would diverge from the Lean Rat carrier and cap precision).

Alternatives considered

• Real = f64 default (status quo §17.1). Rejected: float drift is a correctness bug for the domain; contradicts the Lean.
• Real = fixed-precision Decimal (e.g. rust_decimal, 96-bit). Rejected: caps precision, rounds division (so avg is inexact), and diverges from the Lean’s Rat carrier.
• Defer (keep folding Int-only). Rejected: blocks the motivating Met rule and every Real/Money aggregate; the deferral was already taken once in §17.1 and this RFD is its resolution.

Follow-ups

• L5 — exact avg + a Reasoning/Aggregate.lean fold theorem (the interval/fold characterization; closes the Lean item of issue #52).
• R4 — oxc-reasoning exact Value variant + exact encode_tuple + exact sum/min/max/avg fold mirroring MutationSemantics.foldAggregate; oxc-runtime literals → exact value (replace the opaque-CBOR path).
• A future RFD may add custom-precision fixed-point / refinement-driven width selection (the remaining tail of §17.1’s deferral); not needed for exact-by-default.

RFD 0017 — Refinement classification: where (primitive) vs iff (defined)

• State: committed
• Opened: 2026-06-05
• Decides: whether a concept’s refinement predicate (<: Parent where { P }, Refinement) is a necessary condition only (membership asserted; the predicate is an invariant) or a necessary-and-sufficient condition (membership derived; the substrate auto-classifies). Today every refinement is implicitly the latter. This RFD splits the surface so the modeler chooses explicitly: where { P } is primitive (description-logic ⊑; necessary-only; membership asserted), iff { P } is defined (DL ≡; necessary-and-sufficient; membership derived). Confirms dyn remains reserved exclusively for runtime trait objects (Built-in type forms, Out of scope (v0)). Relates to RFD 0006 (refinement-determined classification was cited there as canonical), RFD 0007 (three-valued refinement membership under OWA), RP-007 (spec/research/RP-007-narrowing-under-mutation.md; value-dependent narrowing soundness).

Question

concept Adult <: Person where { self.age >= 18 } — is an arbitrary Person with age >= 18 automatically an Adult, or must Adult-membership be asserted, with the predicate merely constraining who may be one?

Today the answer is “automatically.” The runtime computes extent(Adult) = { x : iof(x, Person) ∧ predicate(x) } (compiler/crates/oxc-runtime/src/lib.rs:1986-2008, the “refinement-honesty pass”); the book states it outright — “the refinement is the substrate’s source of truth for membership… the substrate derives the iof classification automatically” (mutate, constraint 2 on insert iof) — and rejects explicit insert iof(x, Adult) with OE0211. That is the DL defined-class (≡) reading, and it is the only reading the surface can express. There is no way to say “validate this predicate on every Adult, but membership is conferred, not inferred” — the DL primitive-class (⊑) reading, which is the common case in real ontologies.

Auto-classification by default, with no opt-out, is the wrong default for three reasons (Rationale). The question: what surface distinguishes the two, and what does each mean across the extent query, insert iof, construction, and mutation?

Context

The DL distinction. A primitive class C ⊑ D ⊓ P states necessary conditions: every C is a D satisfying P, but a D satisfying P is not thereby a C — membership is asserted (SubClassOf in OWL). A defined class C ≡ D ⊓ P states necessary and sufficient conditions: a D satisfies P iff it is a C — membership is inferred by the reasoner (EquivalentClasses; classification/realization). In real ontology engineering the overwhelming majority of named classes are primitive; defined classes are the deliberate minority written specifically to drive inference. Defaulting every where to defined inverts that.

What the substrate mechanizes vs. specifies. The Lean models the refinement predicate as a decidable fragment (spec/lean/Argon/Decidability/Fragment.lean) but leaves the instance-level value predicate D2Pred opaque (Fragment.lean:80-103: “we do not formalize the internal structure of QF-LIA formulas”). mutate emits only explicit assertIof/retractIof effects (spec/lean/Argon/Runtime/MutationSemantics.lean:104-115). The defined-class realization (iof(x,C) ↔ iof(x,parent) ∧ P(x)) exists as book prose + Rust runtime, not as a Lean theorem. So this is a clean point to fix the surface: the substrate has not committed to “all refinements are defined” — only the prose and one runtime pass have.

The corpus is entirely defined classes. Every where in a runnable example declares the refinement, never asserts iof to the refined type, and queries the derived extent: FullTime/Manager (examples/refinement_employment), ActiveAdult (examples/multi_field_refinement), Adult/Felon/SpecialClass feeding defeasible can_vote (examples/legal_norms_can_vote), FullTime over time (examples/temporal_promotion), Adult as-of (examples/temporal_as_of_surface). These are defined classes; migrating them where→iff is correctness, not churn. The sole where test that does not auto-classify hand-asserts alice iof Adult (compiler/crates/oxc-oxbin/tests/end_to_end_program.rs) — the natural primitive case.

No write-time enforcement exists today. The predicate is purely a query-time filter; construction, insert iof, and update perform no validation (oxc-runtime/src/lib.rs: Operation::Construct, Operation::InsertIof, Operation::Update). OE0210/OE0211 are declared in grammar.toml but never emitted. So a primitive where needs new enforcement machinery (its predicate must do something), and a defined iff needs OE0211 finally wired.

Decision

1. Two clause keywords; identical syntax, opposite membership semantics

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

The predicate grammar (refinement-pred ::= D1Pred | D2Pred, Refinement) is unchanged. The keyword alone selects the membership semantics:

• where { P } — primitive (DL ⊑). P is a necessary condition. Membership is asserted (by construction or insert iof). extent(C) is the set of entities asserted iof C (or iof a subtype) — identical to an unrefined subtype’s extent. P is enforced as an invariant at every membership-write point; it never widens the extent.
• iff { P } — defined (DL ≡). P is a necessary-and-sufficient condition. Membership is derived: extent(C) = { x : iof(x, parentᵢ) ∧ P(x) } over C’s <:-ancestors-including-self — the current runtime behavior, unchanged. Manual assertion is forbidden.

2. insert iof / construction / mutation, per kind

OE0211 (declared, previously unemitted) is narrowed to iff concepts — you cannot assert membership of a defined class because its membership is the predicate. For where, asserting membership is exactly how you become a member, so insert iof is permitted and the predicate gates it.

3. New diagnostic: OE0668 RefinementInvariantViolated

A membership-write that would place an entity in a primitive where-concept whose predicate it does not satisfy is rejected at runtime, surfaced as Result<_, Diagnostic> (the mutate-rejection channel mutate already promises). Three-valued, OWA-aligned (World assumptions (CWA / OWA), RFD 0007): reject only on positive evidence of violation (P evaluates to definite false); unknown — information absence, i.e. a referenced field with no recorded value — permits the write. A primitive invariant blocks the demonstrably-bad, not the merely-unproven — symmetric with iff’s rule that unknown does not grant membership.

Amendment (2026-06-11, audit ts-01 / PR #272). The original clause folded unevaluable (a v0.1-unsupported form or a type-mismatched operation) into unknown-permits. That fold was the ts-01 critical: predicates over Real/Decimal/Money/Date were “unevaluable” to the v0.1 evaluator and therefore silently never enforced. The ratified semantics split the bucket: unknown = missing field only (OWA information-absence; permits where, withholds iff membership). A predicate that cannot be evaluated — unsupported form, malformed wire data, type-mismatched comparison — is a loud error (RefinementUnevaluable at runtime; OE0660 refuses unsupported forms at build time), never a silent permit or a silently-empty extent. Three-valuedness is for the world’s incompleteness, not the evaluator’s.

4. dyn is reserved exclusively for trait objects

Confirmed (your call (c)). dyn is and stays the keyword for deferred runtime trait objects (&dyn Trait / Box<dyn Trait>, Built-in type forms, Out of scope (v0)) — dynamic dispatch + type erasure, orthogonal to whether membership is derived. The classification axis uses where/iff; the dispatch axis uses dyn. They may co-occur on a future concept and must not share a keyword.

5. Substrate scope

The Lean surface AST (ConceptDecl) and storage body (Storage.AxiomBody.ConceptDeclBody) carry the primitive/defined discriminator now — a shared @[language_interface] inductive RefinementKind, drift-gated against the Rust RefinementKind mirror — and the two membership semantics are documented in the substrate docstrings. The realization theorem for iff — iof(x,C) ↔ iof(x,parent) ∧ P(x), requiring the instance population + value-environment that State C A does not yet model — is not mechanized here; it is the value-dependent-membership case that RP-007 §1.2 hazard 2 / §4.5 scopes as open. It is left as a follow-up (RP-007-adjacent, #40), not claimed as done. This is honest staging, not a stub: the surface, elaboration, storage, and runtime are complete and proven-to-run (parser, elaborator, and five end-to-end runtime tests); the deep substrate theorem is research, exactly as RP-007 is.

Rationale

Why split at all (against auto-by-default). (1) Practice: most real classes are primitive; the common case should be the plain keyword. (2) No spooky inference: silent derivation of facts is un-Rust-like (the house aesthetic default); a modeler should opt into the reasoner minting memberships. (3) Soundness blast radius: value-dependent auto-classification is the source of RP-007’s hardest open hazard (a narrowing if x: VerifiedAdult invalidated by update x set { age = 10 }). Making it opt-in (iff) makes that hazard opt-in — the obligation narrows to exactly the concepts that asked for derivation.

Why iff. It is the membership biconditional: iof(x, Adult) ↔ iof(x, Person) ∧ age ≥ 18 reads directly as “Adult iff Person and age ≥ 18.” Necessary-and-sufficient is the literal meaning of “if and only if.” No other candidate (defined, :=, ≡) is as self-documenting at the use site, and it touches neither dyn nor = (taken by metaxis typed domains, Meta-calculus atom).

Why where for primitive. Rust’s where is a bound — a necessary constraint on a type, never a definition (fn f<T>() where T: Clone). Reusing it for “necessary condition on members” aligns with the Rust/Cargo aesthetic default and with DL ⊑. A where-refined concept reads as “a Person, further constrained to age ≥ 18” — a constraint, not a definition.

Why three independent principles agree (practice, no-spooky-inference, soundness-containment) plus two surface alignments (Rust where-bound, iff-as-biconditional) is why (a) — which keyword is primitive — has a correct answer rather than a coin-flip: where = primitive, iff = defined is over-determined.

Alternatives

• Keep auto-by-default; add a keyword for primitive. Rejected: inverts ontology practice, keeps the spooky default, and leaves the RP-007 hazard pervasive. Also incompatible with choosing iff (which must be the defined form — it claims sufficiency).
• Operator distinction <:+where vs =. (Adult = Person where {…}.) Mirrors DL ⊑/≡ exactly but a one-character carrier of enormous semantic weight is dangerous, and = already introduces metaxis typed domains.
• defined modifier on the concept. (pub defined kind Adult ….) Familiar to Protégé users but detached from the clause and heavier; loses the at-the-predicate self-documentation iff gives.
• Reuse dyn (dyn where). Rejected per call (c): collides with trait objects, and “dynamic dispatch” ≠ “derived membership.”
• Enforce primitive where purely via a separate check rule (status quo workaround: drop the predicate, add a constraint rule). Rejected as the only mechanism: it detaches the invariant from the concept’s identity and gives no surface to the necessary/sufficient choice. where-as-invariant and check-rules coexist; the former is a membership invariant local to the concept, the latter a global constraint.

Consequences

• Migration. All 8 example where sites → iff; the corpus tests, CLI pipeline tests, and runtime unit test that assert derived extents update accordingly. Primitive-where behavior (no auto-classify, asserted membership, OE0668 on insert-iof / construct / update, OE0211 on iff insert-iof, atomic rejection) is covered by five new end-to-end runtime tests. The oxbin round-trip fixture stays where-compatible.
• Wire format. ConceptDeclBody gains a classification discriminator; canonical-CBOR field order updated; decode_concept_decl back-compat: absent discriminator ⇒ iff is not assumed — pre-split artifacts are rebuilt (Argon is pre-1.0, in-process; no stored-artifact compatibility burden).
• OE0211 semantics change. Previously declared-but-unemitted “refined type”; now emitted, and only for iff. Any future code keying on “has refinement predicate ⇒ reject insert iof” must key on “is iff.”
• New runtime enforcement path (OE0668 RefinementInvariantViolated) for primitive where at construction / insert iof / dependent update.
• Rigidity (OE0210) remains out of scope here: it gates insert iof on anti-rigidity (a UFO meta-property carried as meta_property events, not in the ontology-neutral ConceptDeclBody). Still declared-but-unenforced after this RFD; a separate rigidity-enforcement effort owns it. Noted so the two insert iof gates (rigidity, classification) are not conflated.

Open questions

• iff realization soundness (follow-up, RP-007-adjacent #40): mechanize iof(x,C) ↔ iof(x,parent) ∧ P(x) in Lean, which requires extending the state model to carry the value environment — the RP-007 §4.5 sub-problem. Until then iff derivation is runtime-correct but not substrate-proven (parity with the pre-RFD status quo).
• update-time invariant scope. v0.1 re-checks a primitive where predicate only against the directly mutated entity/fields. Transitive invalidation (a mutation to entity y that changes an aggregate a where-predicate on x reads) is not chased; the predicate fragment (OE0660) forbids the aggregate/subquery forms that could create such coupling, so this is currently vacuous — revisit if the fragment widens.
• Should iff construction (insert C { … }) be sugar or an error? Decided: sugar (construct + set fields; classification derived). Revisit if it proves confusing that a constructed iff-C with predicate-violating fields silently is not in extent(C).

RFD 0018 — Production reasoner: the incremental DBSP engine

• State: accepted — implemented with revisions; per-decision status below (2026-07-03)
• Opened: 2026-06-05

Per-decision status (2026-07-03):

• D3 — abandoned. No Feldera fork; the engine adopts the DBSP model on its own operators (RFD 0021 D6).
• D11 WFS-over-cycles — shipped, without the SLG kernel. Batch Van Gelder alternating fixpoint atop semi-naive (executor/wfs.rs); supersedes the BUILD-SOON row (note under D11).
• Persisted-IVM (D4/D6 arc) — shipped, with a ceiling. DRedc two-counter retraction (#642) + delta-seeded monotone insertion + the checkpoint-seeded read-model (RFD 0053 D6). Incremental insert remains monotone-only; WFS-cycle / rule-augmenting reads still full-recompute.
• D1 — the unbuilt keystone in Rust. The substrate is a 2-valued signed-multiplicity Z-set; WFS is a hardcoded strategy, not a selectable fixpoint. The #640 AFT Phase-0/1 track is building the pair-encoding, differential-oracle-gated (note under D1).
• D5 — still unformalized. The ℕ[X]→PosBool[X] retraction homomorphism (commuting with deletion) remains the open obligation gating incremental-retract-under-pair.
• D8 — as-shipped oracle stack. FullRecomputeMaintainer + the Lean evalProgram executed oracle + the RFD-0055 conformance corpus; see the D8 note for a floor-scope correction.
• Decides: the concrete realization of RFD 0003’s DBSPExecutor — the data model, evaluation engine, storage model, provenance, and invalidation that take Argon’s reasoner from a correct demo (cold, non-incremental, nested-loop semi-naive) to production-grade (“working and usable” at scale). Resolves RFD 0003’s deferred open question (“Stratum boundary policy with retractions → defer to the DBSP integration RFD”). Fixes the scope cut (RP-009 §4) and answers RP-009’s open questions (§9). Scopes the ARS substrate research record (vault ars-substrate R-3.1–R-3.8) down to what we build now vs design-for vs defer.

This RFD is the architecture decision record for the production reasoner. It is Lean-first where it touches semantics (the engine conforms to spec/lean/Argon/Reasoning/; divergence is a bug). It commits a plan, not code; its Phase 0 is a de-risking spike that gates the central engineering bet before any irreversible code lands.

Question

RP-009 mandates: bring the rule engine from correct MVP to production-grade, because it is the foundation the entire language sits on. RFD 0003 settled how multiple backends compose under one Engine/TierExecutor interface, named DBSPExecutor as the incremental recursive-tier backend, and explicitly deferred the engine itself — its data model, its IVM/retraction semantics, its storage and invalidation — to “the DBSP integration RFD.” This is that RFD.

Concretely: What is the production engine? — (1) the value/data model that lets a bilattice (Truth4) truth domain ride an incremental dataflow substrate that needs an abelian group; (2) the evaluation substrate (build vs fork vs wrap, and which); (3) how facts are stored and read at scale (the event log is the source of truth, but a cold per-query re-materialization is O(database) and dies at scale); (4) how derived state is incrementally maintained, persisted, and invalidated; (5) how provenance composes with incrementality; (6) how it conforms to the Lean; and (7) the scope cut + build order that gets us there correctly the first time, designed so the features we’ll need soon (defeasibility, metric-temporal, well-founded semantics over cycles) integrate neatly without a rewrite.

Context

Current state (verified against origin/main @ b7a24bc)

The engine is a sound, well-tested, semi-naive stratified-Datalog evaluator — correct on the Datalog + stratified-NAF + exact-rational-aggregate fragment, at small scale. It is not production-grade. The load-bearing gaps:

• Cold + non-incremental. oxc-runtime::query_derive calls materialize_predicates(module) (a full scan of all IofAssertion/RelationTuple/IndividualPropertyAssertion events into a fresh RelationCatalog) then evaluate_to_fixpoint from scratch — every query. No derived state persists across queries; no incremental update on mutation. Every query is O(all events) + O(rules × facts × iterations), cold. This is the headline scaling failure.
• Nested-loop joins, decode-per-tuple. extend_bindings/unify iterate every tuple of a relation and decode_tuple (CBOR) it inside the innermost join loop; Relation<Vec<u8>> = BTreeMap<CBOR-full-tuple, weight>. No join-key index, no arrangement (arrangement_body is reserved + inert). The dominant cost is O(iterations · rules · |prior| · |rel|) CBOR decodes.
• Executor split. The live path is the free fn executor::eval::evaluate_to_fixpoint; SemiNaiveExecutor::execute is a stub returning an empty catalog; the RFD-0003 TierExecutor trait and the DataFusion-shaped logical/physical/optimizer layers are orphaned scaffolding.
• Generation counter wired to the wrong cache. oxc-storage-pg has runtime_generations (bumped atomically with appends, invalidating a projection cache), and oxc-serve reads it — but only to memoize the hydrated Store (raw replayed events), not derived reasoning state. The §19.6 runtime-Salsa db (OxcRuntimeDatabase/EventLogInput) does not exist (oxc-runtime doesn’t depend on salsa). So there is no derived-state invalidation today.
• Correctness items. Modal box/diamond erase to the inner atom — unsound for anti-rigid types (the Lean proves box(anti_rigid) → false in StaticDischarge.lean). The 1000-iteration cap is a hard Err (not silent), but is a literal at every call site, not a configured convergence policy.

What already works and must stay green: stratified Datalog + NAF; exact-rational sum/count/min/max/avg/count_distinct folds (RFD 0011/0016); the keystone end-to-end tests (oxc-runtime/tests/keystone.rs); Apt-Blair-Walker stratification (compile/stratify.rs, Tarjan SCC); and — partially — a Governatori three-stratum defeasible evaluator and per-standpoint federated Truth4 evaluation.

What the substrate requires (Lean-first conformance bar)

The only fully-mechanized reasoning semantics is strict-stratified perfect-model evaluation (Reasoning/Fixpoint.lean: Cat1-monotone to fixpoint, then Cat2-NAF once, per axis in topological order; Theorems terminate/unique/stable, zero sorry). Consequences for the engine:

• Order-independence (stratified_fixpoint_unique): within-stratum rule/axis order is semantically irrelevant ⇒ any strategy converging to the same perfect model is conformant — DBSP, semi-naive, indexed, all sound. Engine choice is a performance decision, not a correctness one.
• NAF order-sensitivity (cat2Apply_sublist): Cat2 extension is monotone only under List.Sublist; the engine must preserve relative Cat2 rule order across deltas.
• Acyclicity is necessary (Necessity.lean): cyclic axis-dependency ⇒ non-unique. Cycle rejection (OE1309) is correct, not conservative.
• Modal: box(anti_rigid) → false is proven and must be honored (or the case honestly refused).
• WFS-by-default, #[brave] stable models, the defeasibility proof-tag engine, DatalogMTL operators, and aggregate OWA-intervals are book-promised but not Lean-backed — they are the “design-for / defer” set, not the conformance floor.

What the north-star application needs (RP-009 §4, the residential-lease + accounting overlay)

A shallow, narrow rule program (≈28 derive rules, one true positive recursion — BreachedAt over the propositional-content tree, with stratified not Met — one NAF pipeline). Its load-bearing needs: recursive stratified Datalog with field-navigation joins; aggregates in derive bodies incl. aggregate-comprehension where with rule-atom/predicate filters; stratified NAF; function application + projected-field terms as rule-atom arguments; an Allen-interval + date-arithmetic builtin; forall; denial constraints. It does not today exercise WFS-over-cycles, standpoints, or modal operators, and it models legal exceptions monotonically (conditional propositional content), not via rule defeat. But defeasibility and metric-temporal reasoning are confirmed near-term needs — design for them now, build them next.

Prior research: input, re-derived (not authority)

Per AGENTS.md the vault is research, not authority — the decision below stands on this RFD’s own rationale; the prior record is reconciled and re-derived, not deferred to. The vault ars-substrate program produced a decision record (R-3.1–R-3.8): a two-strategy architecture — DBSP for the bottom-up recursive tier (R-3.3, Feldera dbsp / differential-dataflow), SLG (chalk-engine-shaped) for top-down WFS/upper tiers (R-3.1), bilattice answers via the AFT pair construction (R-3.2), Salsa above both (R-3.4), provenance as a side-track (R-3.6). Four validation passes against that record surfaced the decisive fact:

The single most load-bearing unproven claim — recursive WFS riding DBSP via coupled alternating-fixpoint circuits, which the research itself says has no published precedent — is co-extensive with the WFS-over-cycles feature we are deferring. Everything our scoped target needs (positive recursion, stratified NAF, stratified aggregates, defeasibility’s Maher three-stratum compilation, stratified-NAF DatalogMTL) sits in DBSP’s proven, standard fragment.

So “build it correctly once” is more achievable than RP-009 implies: the scary part is the part we defer, and the AFT pair-encoding keeps the door open to add it (via SLG) without a data-model rewrite.

Decision

A new module realizing RFD 0003’s DBSPExecutor, plus the storage/invalidation/provenance substrate around it. Twelve decisions:

D1 — Value model: AFT pair-encoded Z-sets (the keystone)

Each Truth4 atom is a pair of ℤ-weighted Z-sets: tt (told-true / evidence-for support) and tf (told-false / evidence-against support), in the Belnap evidence-pair encoding (is = (1,0), not = (0,1), CAN/U = (0,0), BOTH = (1,1); a coordinate is present iff its support weight is non-zero). Each stream is a standard Z-set over an abelian group, so DBSP’s incremental machinery (chain rule, distinct, recursion via δ₀/∫) applies per-stream unmodified. Bilattice operations are per-coordinate: info-meet ⊗ = pointwise AND/min; info-join ⊕ (federation → BOTH) = pointwise OR/max; truth meet/join = the Belnap 4×4 table per atom; negation swaps the two streams (the sole cross-stream coupling). This gives, for free: K3 per-standpoint (⊕ statically unreachable within a standpoint; a clash is a diagnostic), FDE BOTH only at the federation boundary — matching the mechanized K3-per-standpoint / FDE-at-federation split (Foundation/Bilattice.lean, Standpoint/Federation.lean; per-standpoint state in Reasoning/State.lean) exactly. Cost ≈ 2× monotone Datalog (3× with symmetric T/F provenance).

Lean gate (D1), discharged. The value-level correspondence is mechanized in Standpoint/PairEncoding.lean (zero sorry/sorryAx; audited): encode/readoff form a bijection, and neg = stream-swap, ⊕ = pointwise-OR, ⊗ = pointwise-AND, plus federate evaluated in the pair representation reads back to the canonical Truth4 fold (readoff_pfederate). Mechanizing this corrected the encoding: the operations above (swap / pointwise OR-AND) hold under the evidence-for/against labels here, not the Fitting consistent-pair labels (T = (1,1), …) an earlier draft printed — under which neg is not a pure swap and ⊕ is not pointwise-max. (This is the for/against form the Phase-0 spike already used.) The ℤ-multiplicity→support bridge for the assert-only fragment, and the retraction case, are the separate D5 obligation.

This is the keystone because it is also the shared substrate for the deferred SLG kernel (R-3.1): SLG’s answer-subsumption over a 2-D lattice is literally this pair. Adding WFS later is a new fixpoint strategy over the same state — not a rewrite.

Status (2026-07-03): unbuilt in Rust — the keystone is still open. The shipped substrate is a 2-valued signed-multiplicity Z-set (maintainer/mod.rs), and WFS is realized as a hardcoded batch strategy (executor/wfs.rs rewrites in-SCC not R against a frozen shadow EDB and reuses semi-naive), not a selectable fixpoint over a pair-encoded state. The Lean value-level correspondence (the blockquote above) is the only discharged half. The #640 AFT Phase-0/1 track is lifting the pair-encoding into Rust — assert-only first (D1), differential-oracle-gated tuple-for-tuple on both the true and $undefined:: fragments; the K3-vs-native-Both invariant (a Both leaking into the reasoner corrupts the fixpoint — spec/lean/Argon/Reasoning/AGENTS.md) is held as a loud I ⊆ J check pending its Lean non-corruption obligation.

D2 — Three time axes, kept strictly separate

• Transaction/circuit time = the IVM stream index (each kernel commit is a Z-set delta: +1 assert / −1 retract, paired by axiom_id).
• Valid time (VT) = a payload column on the Z-set key, never the circuit clock. Derived VT = intersection of body-atom VTs; derived TT = materialization tx-time.
• Transaction time (TT) = the durable audit axis (tx_from/tx_to) for “AS OF” reads.

The tuple representation is interval-aware from day one even though metric-temporal ships later (D11), because retrofitting intervals is a rewrite. Metric-temporal reasoning is a separate DRedMTL maintainer over interval-set deltas (no engine implements interval-Z-sets), not a modified DBSP circuit.

D3 — Engine: fork Feldera dbsp (own it; do not wrap, do not fork differential-dataflow)

Revised by RFD 0021 D6. The in-memory reasoner adopts the DBSP model (every operator a pure Z-set→Z-set function, so incrementality is an additive outer loop) but does not fork Feldera’s dbsp crate: its flat binary-join Z-sets are the wrong substrate for the WCOJ / factorization / BYODS representations 0021 builds on. The Phase-0 spike below still stands as evidence that the model decouples latency from DB size; what changed is the substrate it runs on.

We fork Feldera dbsp (Apache-2.0) — the Lean-verified Z-set algebra itself — and own it under oxc-reasoning::executor::dbsp. We do not fork differential-dataflow/timely: DD’s value is its distributed/multi-worker machinery, which we would immediately strip on a single-node per-tenant engine. (This refines RFD 0003’s DBSPExecutor row, which said “differential dataflow / timely” — that was the stale default.) Strip: timely exchange/workers/progress-tracking, distributed coordination, any SQL frontend. Keep: the sorted Z-set traces/arrangements and the operator set (map, filter, join, antijoin = stratified NAF via distinct(I₁ − I₁⋈I₂), distinct, consolidate, iterate). Build on top: the D1 pair-encoding, the D2 interval payload, the D5 provenance side-track.

From kora-reason-rl (MIT/Apache, Argon-family — kora-reason-rl is itself “forked from the Orca kernel”) we borrow (lift into our tree, BTreeMap-convert, attribute), not depend on: its bit-parallel Warshall transitive-closure fast path (tc.rs/bitmatrix.rs) as a tier-dispatched operator; its forward/recursive derivation-tree provenance; its stratification (as a cross-check of ours); and its DatalogMTL→time-guarded-Datalog compilation approach (for D11). We skip its incremental.rs (DRed — over-delete+rederive, strictly inferior to DBSP exact deltas, falls back to full re-materialize on additions) and its hand-rolled datafrog_eval.rs (except as a differential-test oracle). This realizes RFD 0003’s “vendor Kora, own it” decision, scoped to the genuinely-reusable pieces.

D4 — Storage: CQRS — event-log write model + persisted, graph-optimized read model

Adopt the event-sourcing / CQRS split explicitly:

• Write model = the append-only event log (axiom_events) — the single source of truth (audit, time-travel, bitemporal). It is the Z-set delta stream the engine consumes. Append scales; scanning to re-materialize is what dies — and that is exactly what D6/D7 eliminate.
• Read model = a persisted, indexed, graph-optimized materialized representation — the durable form of the DBSP arrangements (D7). In Phase 1 it is in-memory; Phase 4 persists it so cold-start does not replay the whole log. Its layout borrows graph-database storage techniques (CSR / index-free adjacency, native edge stores) for traversal-heavy relations — Argon’s data is a graph (individuals + relation-edges).

This commits the scaling contract: no O(database) operation on any hot path, at any scale — mutation→query is O(Δ) (D6); cold-start is O(read the persisted read model), not O(replay log) (Phase 4). It aligns with the spec §20 reserved CQRS catalog tables and the StorageBackend “per-tenant LSM, XTDB-inspired, recency-sharded” slot. The StorageBackend trait is a clean seam now (Phase 1) so the persisted read model slots in without a reasoner rewrite, even though its implementation is Phase 4.

D5 — Provenance: dual-track (mandatory)

Provenance cannot ride the IVM Z-set stream (PosBool is an idempotent semiring with no additive inverse — Amsterdamer 2011 — so it breaks DBSP’s chain rule; answer-subsumption and variant dedup also erase per-derivation identity). So: the Z-set stream carries counting-multiplicity (ℕ) for IVM; why-provenance lives in the separate append-only derivation log (the existing D-097 PosBool-DNF column on axiom_events), joined by the erasing homomorphism ℕ[X] → PosBool[X]. Cheap (O(1)/conjunct: append-on-assert, remove-by-witness-on-retract, empty-DNF ⇒ retracted); bilattice = per-coordinate (separate T-witness and F-witness DNFs); each conjunct carries its own VT interval. Commit dual-track from day one — it is nearly free given the event log exists, but retrofitting onto a single-track answer table is expensive.

D6 — Incrementality + invalidation: Salsa above, generation-driven, one coherent path

Salsa sits above the engine (session granularity, per-(tenant, fork); the engine owns its internal incrementality). Build the §19.6 runtime OxcRuntimeDatabase with EventLogInput + the u64 generation counter as Salsa inputs, route query_derive through it, and unify it with oxc-serve’s hand-rolled runtime_cache so there is exactly one invalidation path: event-log delta → DBSP circuit (warm arrangements) → Salsa session cache, with the generation bump (already atomic with appends in oxc-storage-pg) as the single invalidation signal. “Warm derived state across queries” (Phase 1) is the prerequisite milestone; “warm across restarts” (Phase 4, via D4’s persisted read model) follows.

D7 — Tuple/index layout: typed, sorted arrangements on InternalId

Replace BTreeMap<CBOR-Vec<u8>, weight> + decode-per-tuple with typed, decode-once, partial-key-indexable arrangements (Materialize-style immutable sorted batches + trace) keyed on the existing InternalId (8-byte NonZeroU64, [kind:8 | partition:16 | sequence:40], range-scannable). All layouts are sorted (B-tree / arrangements / interval-trees), honoring the determinism-by-observability rule (RP-006) and the BTreeMap-not-HashMap convention. Automatic index selection (Subotić-style bipartite matching, ~500 LoC) is a compile-time pass portable from the Souffle literature (“steal the ideas, don’t port the C++”).

D8 — Conformance harness: Lean-first + dual-oracle differential testing

The correctness target is the strict-stratified perfect model. The DBSP engine is differential-tested against (a) the retained semi-naive evaluator as an independent oracle and (b) the Lean semantics on generated stratified programs, in addition to keeping the ~600 workspace tests + keystone.rs green throughout. Implement the proven modal discharge (box(anti_rigid) → false) statically; refuse the rest.

As shipped (2026-07-03). No second engine materialized (D6 of RFD 0021 kept ONE evaluator), so “dual-oracle” resolved to a different, stronger stack: FullRecomputeMaintainer (from-scratch Engine::evaluate as the standing IVM equality oracle, maintainer/mod.rs), the Lean evalProgram executed oracle (conformance_replay/conformance_fuzz diff the engine against lake exe eval-batch directly — no Rust port), and the RFD-0055 conformance corpus (hand-pinned goldens through the real ox CLI, covering the front half no self-differential can reach). Floor-scope correction: until 2026-07-03 the path-independent oracles pinned only the definitely-true fragment — the corpus goldens’ not derivable conflates FALSE with UNDEFINED, and the Lean oracle emitted only wfTrue — so a false↔undefined misclassification was visible only to the path-dependent maintainer diff. Corrected by vector schema v3: the Lean oracle now also emits the undefined fragment (wfPossible \ wfTrue) and the harnesses diff the engine’s $undefined::R companions against it.

D9 — Semi-naive is retained as oracle + cold/one-shot fallback (not retired)

DBSP subsumes semi-naive (its recursive operator is semi-naive internally; a circuit fed the database as one delta-from-empty computes the same bottom-up fixpoint), so the algorithm is never lost. The standalone semi-naive evaluator is kept as: (a) the independent differential oracle (D8) — validating the new engine against an independent implementation is the correct practice; and (b) a registered cold/one-shot fallback executor in the RFD-0003 dispatch (it wins only for query-once-tear-down workloads where arrangement maintenance is pure overhead). It is not grown — all expressivity (D11) lands once, in DBSP. One rule-IR + one Z-set semantics + one RelationCatalog exchange, two backends — not “build twice.” This realizes RFD 0003’s “DBSP preferred; SemiNaive stays as fallback + reference implementation.”

D10 — Executor unification

Collapse the live-eval / TierExecutor-stub split: DBSPExecutor becomes the real recursive-tier path through the RFD-0003 dispatch (registered first, ahead of SemiNaiveExecutor); fold compile/stratify’s stratification into the PhysicalPlan strata so the physical plan is the real execution unit; either move evaluate_to_fixpoint’s body into SemiNaiveExecutor::execute or delete the trait method’s stub. Fix the stale eval.rs “naive” header and replace the literal 1000 caps with a configured convergence/divergence policy (divergence stays a first-class, explained Err).

D11 — Scope cut (RP-009 §4)

Legend: BUILD-NEXT = ships on the stratified bottom-up core in this effort’s own later phases (no new kernel); BUILD-SOON = the next major arc after this effort (the SLG kernel), reached through the RFD-0003 dispatch seam; DEFER = not foreclosed, no current design work.

• IN (this effort): recursive stratified Datalog (joins, field-navigation, collection iterators, comparisons); full in-body aggregates incl. aggregate-comprehension where with rule-atom/predicate filters; stratified NAF; function application + projected-field terms as rule-atom arguments; Allen-interval + date-arithmetic builtins; forall; denial constraints (assert ⇒ error); occurrence-typing type-tests; modal discharge soundness; indexing; incrementality; durable+warm derived state; observability; the scaling contract to 10M facts.

• DESIGN-FOR-NOW, BUILD-NEXT (ride the stratified bottom-up core; no SLG kernel): defeasibility (Maher three-stratum at the closure tier; proof tags +Δ/−Δ/+∂/−∂ as derived-predicate labellings; defeater chains in the provenance side-track); metric-temporal (DatalogMTL compiled to time-guarded interval-Datalog; a separate DRedMTL maintainer over interval deltas).

• DESIGN-FOR-NOW, BUILD-SOON (the next major arc, via the RFD-0003 seam): WFS-over-cycles — the SLG kernel (R-3.1). OE1309 stays reject-with-a-good-error now, architected as the future dispatch-to-SLG trigger. Coupling: ambiguity-propagating defeasibility = WFS-of-translation (Maier–Nute; +∂‖ = well-founded-true), so the SLG arc serves both WFS and the richer defeasibility.

  Superseded by events (2026-07-03): WFS-over-cycles shipped without the SLG kernel — executor/wfs.rs runs the Van Gelder alternating fixpoint (T = lfp(S_P∘S_P)) as a batch atop the semi-naive evaluator, materializing the definitely-true extent into R and the undefined extent into the $undefined::R companion. A NAF-cyclic SCC therefore evaluates (the old OE1309 acceptance behavior for that shape is gone); the honest boundary refusals are OE1365 (a higher-stratum not R(..) over a WFS relation would read undefined-as-false — refused pending three-valued propagation into derive heads, i.e. the D1 pair-encoding arc) and OE1317 (recursion through an aggregate). The SLG-tabled kernel remains reserved for the Expressive tier (classifier/mod.rs); it is no longer the WFS delivery vehicle.

• DEFER, don’t foreclose: full Kripke modal; FOL/SMT (unsafe logic); KoraExtensionExecutor (DL via std::owl); standpoint-translation hardening; per-tenant eviction (a 10⁹ / ~2 TB-provenance concern); #[brave] stable models.

D12 — Phased plan, with a gating spike (no phase rebuilds a prior phase)

• Phase 0 — de-risking spike (GATE before committing the fork). On a forked/wrapped dbsp: a bilattice-pair-encoded recursive rule (the overlay’s Met-style rule, or reachability) with stratified NAF, over bitemporal-interval-keyed tuples. Acceptance: a post-mutation query does not re-materialize — incremental mutation→query latency decouples from total DB size (latency ∝ |Δ|, not |DB|); cross-stream pair-encoding throughput is acceptable on a real rule mix. If the public dbsp API proves too lossy for the pair-encoding or the interval payload, that is the signal to fork internals (which we do anyway).
  • RESULT — PASSED (2026-06-05). Ran on stock dbsp 0.277 (rustc-1.92-compatible), release, 1 worker. (A) recursive transitive closure swept 1K→1M components (10K→10M derived facts): full re-eval grew ≈linearly (9.4 ms→5.78 s) while the steady-state incremental step stayed flat at ~400–850 µs — at 10M facts a mutation propagates in <1 ms vs 5.78 s full (~6,800×), ratio growing with DB size. The decoupling holds. (C) a valid-time [lo,hi) interval carried as a payload column (interval-intersection join) preserved the same flat incremental step (~390–863 µs) — VT rides as data, not the clock (§D2 validated; MTL can compile to interval-Datalog on this base). (B) the AFT pair-encoding (two ℤ-streams) + stratified NAF (antijoin) computed correctly at 1M (active = 500K, T/F disjoint within source, BOTH only at federation) with pair-encoding overhead 1.46× — under the ~2× the construction predicts (§D1 validated). Three Path-A frictions surfaced and reinforce D3 (fork & own): (i) upstream MSRV churn (latest dbsp needs rustc 1.93; we used 0.277); (ii) relations >65,535 records silently read empty without a storage backend configured; (iii) .output() (delta mailbox) reads empty at scale — must use .accumulate_output() (materialized snapshot). A vendored fork eliminates all three by giving us the spine/storage/read-model directly. (Harness + full results live at .local/spikes/dbsp-phase0/ — local-only / gitignored: a throwaway Path-A measurement harness, not shipped and not independently checkable from this tree. The tables and method above are the auditable record; reproduction is three cargo run --release -- {A,C,B} … lines against dbsp = "=0.277.0".)
• Phase 1 — the build-once engine core. Forked dbsp IVM + D1 pair-encoding + D7 arrangements (on InternalId) + D10 executor unification + D5 dual-track provenance carriers + D6 runtime-Salsa/generation wiring (unified with serve’s cache) + the D4 StorageBackend seam. Conformance: D8 differential testing. Lean gate (Lean-first): the D5 retraction homomorphism (commutes-with-deletion) and the D1 pair-encoding↔bilattice correspondence are mechanized before the incremental-retract and cross-stream-negation paths they underwrite are trusted (see Consequences/Lean). Bench: mutation→query vs DB size (the headline).
• Phase 2 — expressivity on the real engine (unblocks the overlay end-to-end; closes RP-008’s operational-evaluator debt as a by-product): aggregate-comprehension rule-atom/predicate filters, function application in rule bodies, projected-field rule-atom args, Allen/date builtins, modal discharge soundness.
• Phase 3 — design-for features: defeasibility (proof-tag propagation) and metric-temporal (interval-Datalog + DRedMTL), each Lean-first + reject/accept tests.
• Phase 4 — scale + ops: persisted graph read model (D4) + restart-warmth (checkpoint vs snapshot-replay), observability (structured logging/metrics/slow-query), resource limits, concurrency model, the benchmark suite to the 10M-fact target, IAM in oxc-serve. (Per-tenant eviction enters here only if the scale target rises.)

Each phase is a CI-gated PR sequence, complete + tested + benchmarked — no hollow features; a thing is done only when it runs and is proven.

Rationale

Why DBSP at all (vs indexed-semi-naive-with-caching). The product thesis is “the data system IS the reasoner”: a mutation must make a subsequent query cheap. That is incremental view maintenance, and DBSP is the provably-incremental, Lean-verified Z-set IVM substrate the codebase already committed to (runtime/relation.rs is “the day-one commitment to DBSP-shaped data”; arrangement_body is reserved). Indexed-semi-naive-with-caching gets indexing but not principled incrementality; it would be a stepping-stone we’d replace — i.e., build twice.

Why fork dbsp, not differential-dataflow, and not wrap. Single-node per-tenant means DD’s distributed/timely machinery is surface we’d strip, not value we’d keep; dbsp is the algebra itself with no distribution layer and a verified core (matching the Lean-first bar). Owning the fork (vs wrapping) is required to thread the pair-encoding, interval payloads, and provenance through the operators — and to honor the house constraints by fencing unsafe/HashMap behind a deny.toml-reviewed boundary rather than inheriting them opaquely.

Why the scope is safe to build correctly once. The only unproven piece in the ARS record (recursive-WFS-on-DBSP) is exactly the WFS feature we defer to the SLG kernel; everything in D11-IN is DBSP’s proven fragment. The AFT pair-encoding (D1) is what makes the deferral non-binding: WFS/SLG and the richer defeasibility slot in over the same state, via the same RFD-0003 dispatch seam, with no data-model rewrite. So designing-for-soon costs us a clean trait seam (D6/D10) and a value model (D1) we want regardless — not speculative engine work.

Why CQRS / dual representation. A single append-only log is a fine write model but a terrible read path at scale (re-materialization is O(DB)). Separating a persisted, indexed, graph-optimized read model (the durable DBSP arrangements) from the event-log write model is the standard event-sourcing answer, it is what the spec §20 already reserves, and it is what makes the no-O(DB)-on-any-hot-path contract achievable at all scales.

Why dual-track provenance, from day one. It is forced by three independent facts (group-vs-semiring impossibility, answer subsumption, variant dedup); it is nearly free given the event log already carries the PosBool-DNF column; and retrofitting it onto a single-track answer table later would be a rewrite of the hot path.

Why keep semi-naive. Validating the new engine against an independent implementation — not against itself — is the correct way to earn “completely correct.” Retiring the reference implementation to save tidiness is the wrong trade for a foundation. DBSP subsumes it, so this costs nothing in duplicated expressivity.

Alternatives considered

• Indexed semi-naive + cross-query caching (no IVM). Smaller, stays in the BTreeMap world, gets indexing — but delivers caching, not principled incrementality, and would be replaced by DBSP. Rejected as a stepping-stone we’d build twice. (Its good ideas — arrangements, auto index selection — are absorbed by D7.)
• Fork differential-dataflow (the ARS-record default Path B). Rejected: its distinguishing value is distributed/timely scale-out we don’t need; we’d fork-then-amputate. dbsp is the cleaner thing to own single-node.
• Wrap Feldera dbsp as a black-box dependency (ARS Path A). Rejected as the product path (kept only as a throwaway Phase-0 measurement harness): wrapping can’t thread the pair-encoding/interval/provenance through operator internals, and drags in unsafe/HashMap behind an API we don’t control. “Build correctly once” + the fork-and-strip preference favor owning it.
• DRedc as the shipping recursive substrate, DBSP as a v0.3 migration (ARS W5.S2/D-103). This existed as the safe fallback precisely because recursive-WFS-on-DBSP was unproven. Since we stay strict-stratified (where DBSP is proven), DRedc would be a stepping-stone we’d replace — rejected. (This reconciles the R-3.3-vs-D-103 internal inconsistency in the ARS record for our scope.)
• Single-track provenance (on the answer row / on-stream). Structurally impossible under the bilattice + group structure (D5 rationale). Rejected.
• Build recursive-WFS-on-DBSP now (the novel coupled-fixpoint construction). Unproven, no published precedent; the ARS record itself names it the gating risk. Rejected for this effort — WFS goes to the SLG kernel via the seam.
• Event-log only (no persisted read model). The status quo; O(DB) re-materialization; dies at scale. Rejected (D4).
• Retire semi-naive. Loses the independent oracle and the cold/one-shot fallback. Rejected (D9).

Consequences

• Code structure. New oxc-reasoning::executor::dbsp (the forked, owned engine) registered first in the RFD-0003 dispatch; SemiNaiveExecutor implemented for real and retained as oracle/fallback; the orphaned logical/physical/optimizer scaffolding either wired into the real path or removed; oxc-runtime gains a salsa dependency and the OxcRuntimeDatabase; a StorageBackend trait seam for the future persisted read model; tc.rs/provenance/MTL-compile borrowed from kora-reason-rl under attribution.
• Dependencies. The vendored dbsp fork enters via compiler/deny.toml allow-list + an explicit constraint review; unsafe is minimized and fenced (our new code stays #![forbid(unsafe_code)]); HashMap is permitted only in the vendored fork where it cannot affect observable order, justified in this RFD. num-rational/num-bigint already present (RFD 0016).
• Lean (Lean-first for new semantics; evaluation-strategy obligations trail). AGENTS.md puts substrate semantics in the Lean-first lane, so the new obligations split by kind:
  • Gates the code it underwrites (Lean-first — these are new semantics not covered by the forward perfect-model theorems): (a) the ℕ[X]→PosBool[X] homomorphism commuting with deletion under DBSP’s chain rule (D5) — incremental retract is genuinely new semantics (stratified_fixpoint_unique is the forward model only), so it is mechanized before Phase 1’s incremental-retract path is trusted; (b) the D1 pair-encoding ↔ mechanized bilattice correspondence (representation adequacy for cross-stream negation = stream-swap, and ⊕-only-at-federation = Foundation/Bilattice.lean/Standpoint/Federation.lean) — mechanized before Phase 1 relies on the cross-stream coupling.
  • Trails implementation (evaluation strategy — reduces to the already-proven perfect model, sound for any converging strategy by stratified_fixpoint_unique): the operational RuleIR→extent evaluator (closes RP-008).
  • All anchored on porting Bogaerts–Cruz-Filipe 2024 (AFT-in-Coq) to Lean 4.
• Conformance. The ~600 tests + keystone.rs stay green throughout; new differential + per-feature tests per phase.
• Workflow. Branch off origin/main (this RFD is on rfd/0018-production-reasoner); per-PR CI-gated; commit at checkpoints; no “done” without a running/benchmarked proof.
• Spec. Resolves RFD 0003’s deferred retraction/IVM open question; refines its DBSPExecutor row (Feldera dbsp fork, not DD/timely). The reference (spec/reference/src/{17,19,20}) follows once the design lands.
• Relationship to RFD 0017 (refinement classification). RFD 0017’s two refinement kinds map cleanly onto this engine, with no scope expansion: a defined (iff) refinement is a derived-membership rule — iof(x, C) :- iof(x, parentᵢ), P(x) — i.e. an incrementally-maintained view (a mutation touching P(x) updates C-membership as a Z-set delta; this is the IVM win applied to classification), and is already covered by D11-IN’s recursive stratified Datalog. A primitive (where) refinement is a write-time invariant (OE0668 RefinementInvariantViolated) — a constraint check at the mutation boundary (Cat3-shaped), not a derived relation. RFD 0017 explicitly defers the iff realization theorem (iof(x,C) ↔ iof(x,parent) ∧ P(x)) to RP-007-adjacent work; this engine is its operational home, and that theorem is part of the D8 / RP-008 Lean conformance debt.

Open questions / tracked-future

• The Phase-0 spike — PASSED (2026-06-05). Decoupling (∝|Δ| not |DB|) confirmed to 10M facts; AFT pair-encoding + stratified NAF correct at 1M with 1.46× overhead; VT-as-payload preserves incrementality. The three Path-A frictions found (MSRV churn; >65k-record relations need a storage backend; .output() reads empty at scale, must use .accumulate_output()) all reinforce D3 — fork & own. See the Phase-0 RESULT block in §Decision/D12.
• AS OF tx-time = X × Salsa backdating — prototype with the Phase-1 Salsa layer; fallback = disable backdating for AS OF queries (ARS R-W5S2-04).
• ℕ[X]→PosBool[X] commutes with deletion under DBSP’s chain rule (ARS R-W5.S3-4) — new semantics; gates Phase 1’s incremental-retract code (Lean-first; see Consequences/Lean). Not “tracked-future” — a Phase-1 prerequisite, listed here for visibility.
• Persisted-read-model layout — a research item: graph-DB storage internals (CSR / index-free adjacency, native edge stores, triple-store indexing) → the Phase-4 read-model design.
• PG schema canonicalization — spec §20.3 (TSTZRANGE+GIST, generated columns, JSONB derivation) vs the shipped migrations (INT8 ns columns, projection-index tables, TEXT derivation). Decide canonical before Phase 4 scaling.
• The SLG kernel arc (WFS + ambiguity-propagating defeasibility) — the next major effort after Phase 2; its own RFD, building on D1’s pair-encoding and the D10 dispatch seam.
• Per-tenant eviction — tracked, not built; enters when a tenant exceeds ~100 GB (provenance ≈ 2 TB/tenant at 10⁹ is the binding constraint); recommended composition = snapshot-at-τ₀ + continuous provenance compaction + tenant archival.
• Cross-stream operator throughput for the pair-encoding — RESOLVED by the Phase-0 spike: measured at 1.46× at 1M facts, under the ~2× the construction predicts.

RFD 0019 — Mutation write-path correctness: construction, identity, read-your-writes, and exact values

• State: accepted — partially implemented (RC1/RC2/RC4 landed; required-fields and within-body read-your-writes remain)
• Opened: 2026-06-06
• Decides: the surface and runtime semantics that take Argon’s write path — insert/construct → mint identity → persist fields and relations as ABox events → read them back within the same body and on reload — from silently incorrect to correct, durable, and Lean-conformant. Records the decisions taken on the design questions in RP-010 §6/§11. Refines RFD 0015 (the mutate body surface — insert disambiguation), and connects to RFD 0001 (identity), RFD 0006 (IndividualPropertyAssertion), RFD 0007 (required/missing fields under OWA), and RFD 0016 (exact Real). Its read/execution-path counterpart is RFD 0018 (RP-009); this RFD owns the write side and coordinates at the seams (§Consequences).

This RFD is the architecture decision record for the mutation write path. It is Lean-first where it touches semantics — the engine conforms to spec/lean/Argon/Runtime/MutationSemantics.lean (+ MutationFreshness.lean, AggregateExact.lean); divergence is a bug. It commits a plan and a set of surface-semantics decisions, not code. The full verified evidence lives in RP-010; this RFD states the decisions and why.

Question

Argon can parse and type a rich ontology and can reason over facts at small scale, but the write path is silently incorrect: real ontologies produce no usable instance data. Concretely (verified against origin/main @ 967cc03; see RP-010 §1 for the file:line evidence):

• RC1 — positional insert Concept(...) does not construct. The parser dispatches purely syntactically (L_PAREN ⇒ relation-tuple op, L_BRACE ⇒ struct/construct op), never consulting whether the head resolves to a concept or a relation. So insert Person(name) lowers to a relation-tuple assertion that mints no individual, persists no fields, and lands under NameRef::DEFAULT (a garbage relation id). In let position it is totally silent: lower_let_stmt (mutate_lower.rs:271) only binds an INSERT_STRUCT_OP, so let p = insert Person(name) emits zero ops and binds nothing — and a later unbound p then collapses to a blake3("individual:{name}") content-hash id (oxc-runtime/src/lib.rs:3874), identical across runs. The brace form insert Type { f = v } is correct.
• RC2 — no read-your-writes; navigation fields invisible. A Term::Proj reader in a mutate body reads committed (pre-mutation) state, not this body’s own buffered writes, so coll = coll + [x] clobbers. And from <rel>.endpoint navigation-view fields — which do resolve in the derive/query read path — are invisible inside mutate bodies.
• RC4 — exact Real mishandled. The rule-body aggregate fold is exact BigRational (RFD 0016), but the mutate/term value path is f64-based: as_f64 has no Value::Real arm, so mutate-expression arithmetic/aggregates error on exact-Real operands.
• §1.5 — required fields unchecked. No construction-time field-coverage check exists; insert Type { … } with missing required (incl. inherited) fields silently creates an incomplete individual. The relevant diagnostics (OE1908, OE1014) are defined-but-never-emitted.