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 onmain) 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; theState: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) toarchive/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
| # | Title | State |
|---|---|---|
| 0001 | ID architecture | discussion |
| 0002 | #[comptime] attribute | discussion |
| 0003 | Reasoner backend dispatch | discussion |
| 0004 | pub fact declarations | discussion |
| 0005 | Relation subsumption | committed |
| 0006 | Field mutability via mut | discussion |
| 0007 | Missing-value semantics under OWA | discussion |
| 0008 | Standpoint-sheaf equivalence proof roadmap | committed (Path A landed) |
| 0009 | std::mlt library scope | discussion |
| 0010 | Negative facts / strong negation | discussion |
| 0011 | Aggregate semantics under OWA | discussion |
| 0013 | Toolchain distribution | accepted — partially implemented |
| 0014 | Runtime serving surface | discussion |
| 0015 | mutate body surface: EdgeQL-shaped, set-semantic | committed |
| 0016 | Numeric tower: exact by default | committed |
| 0017 | Refinement classification: where (primitive) vs iff (defined) | committed |
| 0018 | Production reasoner: the incremental DBSP engine | accepted — partially implemented |
| 0019 | Mutation write-path correctness: construction, identity, read-your-writes, exact values | accepted — partially implemented |
| 0020 | The runtime data engine: a composable query + reasoning pipeline | accepted — partially implemented |
| 0021 | The reasoner execution engine (as built): joins, optimizer, factorization, BYODS, incrementality discipline | committed |
| 0022 | Package-path addressing (pkg, not crate) and the build evaluability gate | committed |
| 0023 | Reflective TypeRef: type-as-value in the meta-calculus (RP-003 GAP-1) | committed |
| 0024 | Allen interval algebra as a library (std::allen), not substrate operators | committed |
| 0025 | check discharge: vocabulary-staged compile-time and runtime constraint checking | accepted |
| 0026 | Trait rule members: clause-union dispatch, conformance, and the implements intrinsic | accepted — implementation planned |
| 0027 | The meta-property plane: axis bindings, catalog tiers, value-position resolution, and substrate-neutral modifiers | accepted — implementation planned |
| 0028 | Defeasibility redesign: honest heads, the defeat-directive plane, and strategy as a compilation scheme | accepted — implementation planned |
| 0029 | Derived values and aggregate terms: body-level binding, aggregate sources, rounding | committed |
| 0030 | Package dependencies ([dependencies], path deps v1) | committed |
| 0031 | The relation-constraint plane + meta-property completion | committed |
| 0032 | oxup manages editor-extension installation | committed |
| 0033 | The ad-hoc query and mutation surface | accepted — implemented |
| 0034 | Source text encoding and the Unicode lexical policy (UAX #31 identifiers, NFC, module reachability) | committed |
| 0035 | The composable operator-tree execution pipeline: shared LogicalPlan lowering, tree optimizer, physical mapper, generalized executor, table operators | discussion |
| 0036 | Heterogeneous and specialized data stores: foreign federation, external-valued attributes, persistence swap; the connector SPI, placement, world-assumption tiering | discussion |
| 0037 | The macro atom: a phase-separated, hygienic, declarative-first expander over surface syntax | discussion |
| 0038 | The prelude, ambient scope, and symbol-precise stdlib loading | discussion |
| 0039 | Composable mutations: nested invocation and derived reads | accepted — implemented |
| 0040 | The procedural macro layer: a total, structurally-recursive meta-language over reflected syntax | discussion |
| 0042 | The re-checkable emission boundary: a self-validating .oxbin and sound direct artifact emission | discussion |
| 0043 | Theory packages and the neutrality boundary: where ontologies and higher-order theories live | discussion |
| 0044 | Package registry, workspaces, and distribution: a static content-addressed registry over the CDN | discussion |
| 0045 | The world-assumption write-side: refuse-on-K3-not and the #[world] per-concept opt-in | discussion |
| 0046 | Derivation serving surfaces: query, delta, explain, trace (kill the per-rule derive loop) | discussion |
| 0047 | The temporal value library (TC39-Temporal-modeled std) and the value/ontology boundary | discussion |
| 0048 | The test atom: in-language unit tests, and why a test is substrate | accepted — partially implemented |
| 0049 | Error-tolerant diagnostics: recovery, source-faithful expansion, What/Where/Why/Fix | discussion |
| 0050 | Documentation architecture: three books, correctness by construction, and a verified authoring pipeline | discussion |
| 0051 | oxfmt: a canonical, idempotent source formatter over the shared CST | discussion |
| 0052 | Deployment topologies, the connection abstraction, and host-language parity: embedded vs. standalone, Rust/TS parity, access-vs-durability | discussion |
| 0053 | The standalone concurrent engine: transactor, MVCC reads, and IVM-in-lockstep | discussion |
| 0054 | Set-valued, characterization-relative composition over standpoints | discussion |
| 0055 | The conformance corpus: a standing golden differential-correctness gate | accepted |
| 0056 | Enactment-time-bitemporal rules: the law as it stood | accepted |
| 0057 | Argon as a served platform: the operational host (loopback engine + auth gateway, OTel, lifecycle, config, packaging) | discussion |
| 0058 | The Tableau Model Engine (modal escape hatch) | proposed |
| 0059 | The drift gate as a typed interface manifest | accepted |
| 0060 | The Lean substrate mechanization architecture | accepted |
| 0061 | A single VERSION file is the source of truth for the toolchain version (git-independent, read at build time; the tag is cut from it, the atomic advance is the only bump) | accepted |
| 0062 | CI tiers + affected-scoping: main green by construction — explicit PR/queue/post-merge tiers (named setup outputs), cargo xtask affected scoping, a curated merge-critical release-gate, and a documented post-merge accepted-risk set | accepted |
| 0063 | The bitemporal read-point: the snapshot at now for derived reads (valid-time + transaction-time; clock frozen at the boundary; cache validity-epoch guard) | accepted |
| 0064 | Compiler source decomposition: add-only hotspots, a ~3,000-LOC per-file ceiling (with the irreducible runtime-spine exception), grammar.d//lower//commands//per-concern impl Store siblings, and content-free merge=regenerate codegen merges | accepted — implemented |
| 0065 | The runtime⟷engine seam: oxc-value (the shared value vocabulary as a leaf crate) + the QueryEngine facade trait, making engine and runtime disjointly ownable without splitting the unified RFD 0020 design; records the FORK-2 resolution (the LogicalPlan operator tree is live on the production query path) | accepted |
| 0066 | Agent integration: the Argon MCP server (oxc-mcp / ox mcp) — a runtime-provenance-led third frontend over the transport-agnostic dispatch core (sibling to oxc-serve), backed by RuntimeService for coherence (build → reload → query → explain), with a coherence invariant, ephemeral/promotable forks, and an honest why-not boundary | discussion |
| 0067 | The temporal literal surface, carrier reach, and the four-valued comparison frontier: one #…# delimiter with inner-shape kind determination (resolving #1285 — #…Z# is the Instant literal), nanosecond valid-time reach (agents/robots + legal on one substrate), out-of-range valid-time must refuse not saturate, astronomical time as a modeled domain not a civil-carrier stretch, and the native-four-valued-comparison decidability obligation | discussion |
| 0068 | Native four-valued temporal comparison: decidability of a paraconsistent metric reasoner over ℤ — funds RFD 0067’s sole open research obligation and records the mechanized result (kernel-clean, #print axioms-verified) that the designated non-explosive Both does not break the ultimate-periodicity that buys decidability (the twist coordinate-wise reduction), the binding constraint that metric operators must propagate the full Belnap pair, and the shift-invariance restriction the decidable fragment requires | discussion |
| 0069 | The shared-live-KB write model: concurrent authoring, coexistence, and resolution — many writers on one durable store with durable disagreement. Reasoning-native coexistence (append-Both fold, never the retraction group-wall); two operators not one (monotone LUB merge + a read-time defeasible resolver — a coexistence/resolution split corroborated across six independent fields; the composition soundness is deferred to Lean); per-source-extent Single-Writer write unit; the KB as a verb (lazy cross-standpoint fold); a new tertiary cross-standpoint-designation layer (legal-pluralism forum-priority); the CALM monotone/non-monotone coordination boundary; external decorrelated verification for cross-writer trust; and the retirement of promote()-as-last-writer-wins | discussion |
| 0070 | Derive-backed classification: the shape clause — a shape-defined concept is an ordinary IDB atom of the reasoner’s WFS/AFT fixpoint, with a stated + mechanized realization biconditional; the guardrail floor; the construct count; the Can-membership dispatch policy | committed |
| 0071 | Agent-tooling distribution: the top-level agents/ tree (per-host peers, single-source discipline), the ~/.argon/.agents/ oxup-owned home, and oxup agents register/unregister/list registration | committed |
| 0072 | Persisted derived read-model: populate .oxbin section 6 (projection-cache) with the build-time serialized RelationCatalog — deterministic CBOR (amending the never-implemented Cap’n Proto sketch; a named artifact-tier deviation from 0035 D7’s persisted-columnar, reconciled via payload_version), validity keyed on a length-framed derivation-input commitment (artifact_hash ∥ enumerated GlobalControl semantics incl. tzdb ∥ mapping ∥ axes ∥ DERIVATION_SEMANTIC_EPOCH) + an unforgeable pristine-seed marker (generation tuple as cross-check only), consumed fail-closed by the strict read path (world/metric restamped; v1 fragment = undated + clock-free + non-temporal, re-derived consumer-side; registries-empty + tzdb-pin + preflight-bounded-decode preconditions; provenance-scoped defaults enforcing the trust boundary), gated by a cache-seeded ≡ recomputed differential arm driven by the production routing predicate (doc-hidden audit API) + golden conformance entries (incl. poisoned-cache + epoch-mismatch fixture); section 7 stays reserved and its OE1205 refusal gets wired | discussion |
| 0076 | Mutability of relation ends: apply the field-mutability rule (mut? Ident : TypeExpr, immutable default) to relation endpoints — mut opts an end into value variation through tuple retract/assert history, the immutable default binds the end for its dependent context’s lifetime; effective mutability is conjunctive over relation subsumption; the write path gains retraction, assertion-freeze, dependent-context cascade, and subsumed/derived-extent gates plus a RetractIndividuals kernel effect, and the reflection plane exposes the effective per-end is_mut bit as armMutability; rides a MAJOR core-IR bump | discussion |
| 0079 | Main rewind and contract-driven reimplementation: rewind main to 59a49045 (old tip preserved as dev), re-land the 512-commit performance-and-features range through a phased, contract-reviewed PR sequence; companions in archive/rfd/0079/ carry the per-subsystem architecture record, the behavioral-contract catalog, the test triage, and the baseline-latent bug-fix inventory. Numbers 0073–0078 are allocated on dev and appear here when their content re-lands | archived |
| 0081 | Check-pass rule registry: one auditable rule table per enumeration axis (BODY, ITEM), each entry data (codes, mask, fn, driver-vs-inline wiring); adopts pull request #1727’s body-walk driver as the BODY axis, adds a for_each_item + ItemKind-mask driver for the ITEM axis, and inventories inference-interleaved and cross-layer gates as inline rows rather than migrating them; exactly-once-per-axis and byte-identical-per-wave invariants; motivated by the pull request #1701 / #1727 seam-hole history | discussion |
| 0082 | Cross-module defeat: import-scoped #[defeats] resolution over the importing module’s visible names (defeat edges stay in-package), the combined-artifact defeat pass at workspace assembly, connected-component strategy identity, cross-package refusal (in-workspace only), and #[default] as the cross-module override-consent token — successor amendment to RFD 0028, discharging the deferred workspace-scoped-resolution work | discussion |
| 0083 | Defeat-plane compilation: realize RFD 0028’s Governatori strategy by compiling the mechanized transform (Transform.lean) at elaboration into ordinary strict WFS rules in the .oxbin — support / blocking / team-defeat-fold / F2-reinstatement as $-qualified internal relations — deleting the interpretive runtime resolver (oxc-runtime/src/defeasible.rs) whose per-head memo + reentrancy guard + fail-open fallback produced the order-dependent memo-poisoning / under-suppression / recursive-default-fail-open / short-name-collision bug family; recursive #[default] dependencies admitted (WFS-native), defeat-graph cycles still refused (OE0718); executable defeat metadata stripped and re-homed to an inert DefeatCompilationProvenance carrier so no old runtime double-applies; artifact grows (format minor, no Core-IR bump); elaboration-time switch (OXC_DEFEAT_ELABORATE selects a compiled vs a legacy artifact — the artifact hash is the cache discriminator, so no epoch bump); oracle-clean acceptance (PR #1793) + Lean golden transformed-program vectors via EmitVectors; the recursive-fixpoint theorems are the scoped Lean prerequisite | committed |
| 0084 | Mapped relation subsumption: the explicit argument-mapped subsumption form, keyed by parent end name, becomes the ONLY surface — a child names, for each parent end, what fills it (Home(p, c) <: Loc(p = p, c = c)), may pin a parent end to a constant (WagesUSA(p, amount) <: IncomeItem(p = p, amount = amount, c = USD)), and may cast a child end to a parent supersort; both the bare form (RFD 0005) and the positional filler list are removed and refused (positional fillers re-pair silently under a same-sort parent-end reorder — verified empirically — so only parent-name keying is mechanically reorder-safe); no same-name abbreviation (p = p, never bare p); a breaking source change with a mechanical in-repo rewrite (identity filler lists read off each child/parent declaration; semantics-preservation proved by mappedChecks_identity_eq_bareChecks, which survives as the internal migration-soundness witness); subsumption generalizes from tuple-inclusion to mapped-tuple-inclusion (the image of the child under the declared mapping φ); the canonical family-query surface is the trailing Parent(args) via k (own-extent witness — each row once under its declaring relation), whose meaning is the generalized specializes(k(memberArgs), Parent(parentArgs)) atom (its one-desugar-point target and spec-level semantics; correspondence is the declared mapping, never visual position) — the parent frame is information-complete because D1 forbids dropped child ends; threads the mapping through end-mutability inheritance (RFD 0076 OE0267/OE0268), the retract/amend cascade, relation-value application dispatch (pull requests #1805/#1806, merged), reflection ($specializes carries the mapping — the wire/reflection field is additive optional-on-decode), coverage/OE1404, and the incremental circuits (project/map/union); maintainability by construction — one canonical resolved-mapping structure read by every plane, one surface spelling (no sugar to drift), exhaustive wildcard-free matches over the mapping-entry enum, refusals over silent adaptation, and dispatch/cascade as the same φ with the shared-translation-function obligation on the dispatch slice | discussion |
| 0085 | Incremental rule circuit compiler: compile accepted rules into signed persistent delta circuits with exact Z-set arithmetic, operator-local state, atomic frontiers, recursion, checkpoint recovery, and full-evaluation differential gates | accepted — partially implemented |
| 0086 | Admission-point checks: an undecided membership stops a blocking check’s write, and only reports under a reporting one — a check whose violation body reads membership in a computed (iff/shape-defined) concept gets a first-class inconclusive verdict, disposed of per check from the severity the modeler already wrote, and is judged at the admission point of the data it governs (the write’s valid-time instant, or the all-times view) rather than over the whole store at commit time. Mechanism: membership the well-founded fixpoint leaves undetermined (three-valued Can — a negation/defeat standoff or open-world absence) is neither collapsed to a pass nor fired as a false accusation, replacing the measured status-quo silent-pass (probed on the default branch: a Severity::Error check over undetermined membership fires only an [undefined]-grade observe note and the write commits); disposition of a new inconclusive tuple requires no new surface — blocking (Severity::Error) refuses the write (OE1430), reporting severities and #[observe] report at undefined grade, and an => emit check simply does not emit; a per-check firing closure means a write outside every closure runs no discharge; a point-free judgment of point-variable membership is refused (unimplemented, no diagnostic code allocated; three variability sources: dated evidence, dated rule window, clock-reading classifier) on the write / ox derive / on-demand surfaces; an aggregated standoff re-registers OE1332 as OE1430; the check-rule registry (RFD 0081) stays the dispatch substrate, taking the runtime gate as a single inline inventory row and no driver-wired row; a hard resolution-pass boundary reads resolved identities and never rewrites resolution or introduces a second scope-identity carrier; the Lean obligation extends Reasoning/Checks.lean with the inconclusive set as wfPossible ∖ wfTrue over membership atoms and a no-collapse partition theorem | committed |
| 0087 | Fixpoint typed views: a typed navigation view (f: [T] from Rel.endpoint) whose element type T is standoff-capable (a shape-clause concept whose membership is a rule head the well-founded fixpoint can leave undefined; a braced iff { P } refinement cannot stand off and is out of scope in both directions) is evaluated IN that fixpoint rather than materialized store-locally — a single pin-resolution ladder keys every concept-pinned field read, a raw (extent-blind EDB) + gate (fixpoint rule) split keeps a fixpoint-decided extent live and delta-maintainable, and the K3 standoff at the view boundary is surface-honest (definite extent served, undefined region rides $undefined:: and surfaces loudly — never silently included or dropped, the consumer adjudicates); the ladder CONSUMES the per-scope resolution pass (no rewrite, one scope model), a view over a subsumed-parent relation walks the φ-images of RFD 0084, filtered views over a standoff-capable element type refuse fail-closed, and it shares ONE principle with the admission-point-checks RFD (undetermined never silently coerces; each construct declares its own policy) with independent policies and no shared dispatch structure; rides a derivation-semantic epoch bump. The standoff policy’s aggregate arm is the one piece still undecided | discussion |
| 0090 | In-body determinedness tests — the ADOPTED surface for per-check disposition of an undetermined membership verdict (owner decision 2026-07-24), chosen over a declaration-level #[undetermined(...)] disposition attribute that this record carries as its rejected alternative (the two surfaces are mutually exclusive): a check-body atom undetermined(A) / determined(A) reading the converged three-valued model (holds iff the membership atom’s verdict is Can), so cascading policies inexpressible under the single-disposition attribute — statutory tie-breaker ladders, definite-blocks-while-undetermined-reports in one check — become body branching; check-plane-only by a stated soundness argument (a determinedness read in a derive body is truth-value reflection into the fixpoint, circular under WFS, refused OE1431; anchored to wfPossible ∖ wfTrue in Checks.lean); a conservative three-valued exhaustiveness warning (OW0744) over unhandled undetermined paths, falling through to RFD 0086 slice 1’s severity-derived default; shared base is the slice-1 honesty gate (pull request #1826); comparison table (expressiveness vs. near-zero compiler cost + grep-able governance) and an honest maintainability account (new expression form, the standing plane boundary, the rot-prone coverage pass); implementation open in pull request #1848, stacked on the slice-1 honesty-gate base (pull request #1826); the rejected attribute’s own implementation was drafted in pull request #1840 and closed unmerged | committed |
| 0093 | iof denotes membership, whole: iof(x, C) means an individual’s FULL membership — asserted, <:-closed, predicate-refinement-derived, and rule-derived alike — with extent and meta following it, so that C(x), x : C, and iof(x, C) are three exact spellings of one question, equal under substitution of a bound type variable; the seed-time $iof materialization, which answers empty for a shape-defined concept (RFD 0070) whose members the reasoner computes, is an incomplete implementation of an already-ratified meaning (RFD 0017, RFD 0023, RFD 0070 L5, Realization.lean) rather than a narrower definition, and the same seed scan breaks meta(x) == C as a third silently-empty spelling; the remedy makes the reflection relation carry derived membership — the semantic decision asked for; the implementation mechanism stays open between generated bridge rules ($iof(x, C) :- C(x) plus <: closure over the catalog-closed $specializes), the form the record is written against, and rewriting constant type positions with a single materialization above every read, which is semantically indistinguishable — deleting the individual-tier seed scan while the declaration-derived catalog tier stays extensional, turning extent(t) into a projection and $meta’s individual tier into an antichain over $iof (measured equivalent row-for-row, and deliberately NOT extended to the catalog tier, whose meta is the exact declared introducer); the bridge is positive so concept↔relation recursion is monotone, in-component negation is evaluated by the well-founded semantics exactly as a shape classifier in a negation cycle already is, undefined membership stays the third truth value and must not collapse to false, and recursion through aggregation stays refused (OE1317); requires NO change to the Lean mechanization, where membership is an opaque catalog field and extentOf is defined from it; REJECTS this record’s own first remedy (rewriting only the statically-known iof(x, C) and refusing meta(x) == C) because rewriting only the constant form makes iof(x, Voter) and iof(x, t), t == Voter extensionally unequal, breaking substitution for a first-class type-value-polymorphic predicate; DECLINES a second asserted-plane intrinsic as not load-bearing, unmotivated by any use case, already covered on the write path by OE0211, and — being identifier-lexed unlike the keyword-lexed iof — a needless expansion of the reserved-name gates; records that the qualified type test x : pkg::C is already fail-closed (OE0223) and needs a better message rather than a new diagnostic, and that x is T is not a membership spelling at all; six slices from an executable oracle pinning today’s wrong answers through derived $iof (the first behaviour-changing slice, epoch 12 or later) to optimization last; RFD 0092 remains the alternative on the whole surface | discussion |
| 0094 | Rule-body reads of a completed undefined companion | committed |