Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD 0060 — The Lean substrate mechanization architecture

  • State: accepted
  • Depends on: RFD 0059 (the typed-interface manifest drift gate — the seam this RFD reorganizes around), the @[language_interface] contract (spec/lean/Argon/Interface.lean ↔ compiler/crates/oxc-protocol/)
  • Tracks: issue #1038 (the _root_ shadowing footgun), #1062 (dedup), #1063 (lowering preservation)
  • Prior art: the convergent structural conventions of mature mechanizations — CompCert (lib/ foundation never depends upward; deep-embedded source+IR), CakeML (functional big-step, in-logic bootstrap), Iris / iris-lean (directory = namespace, import hygiene via linters), Mathlib (namespace = path, one-concept-one-definition, @[deprecated] rename aliases, import-graph linters), seL4 (refinement reserved for a thin hand-written slice). Design-research evidence base: deep-vs-shallow embedding (Gibbons & Wu 2014), the intrinsic-typing cost scaling law (Reynolds 2000; Allais et al. 2018; Rouvoet et al. 2021), the spec↔impl trust-tier menu (Pnueli et al. 1998; Klein et al. 2009), lowering preservation as least-model agreement vs step-simulation (Leroy 2009), and the calibrated finding that naming→maintainability is convergent best practice but not a measured causal lever (Ringer et al. 2019; Baanen et al. 2025).

Question

The Lean 4 / Mathlib development under spec/lean/Argon/ is canonical for Argon’s substrate semantics. It was grown incrementally by agents without Lean tooling, and it is mathematically sound but architecturally unplanned. Two questions, settled here:

  1. What is the right internal architecture — module structure, namespacing, embedding choices, dedup — for a world-class substrate mechanization, and how do we migrate to it without re-proving anything?
  2. How should the CI / drift contract be coupled to the Lean during and after that re-architecture, given the contract was itself partly responsible for the mess?

Context

The verified current state (three independent firsthand audits + the design-research synthesis converge):

  • Sound where it matters, tangled where agents touched it. ~1,500 source declarations (kernel-elaborated ≈8,000) across 146 files, ~25.6k lines. Zero sorry and zero axiom in the build target; the strict proof-discipline gate (mech verify) passes; the development is faithful (mech check flags are structural false-positives — ¬-lemmas, empty/nil base cases).
  • Crown jewels to preserve verbatim: the Foundation/ bilattices (the K3 “no CompleteLattice on MetaValue” landmine is mechanized as a theorem, infoJoin_escapes_K3, not merely a comment) and the Reasoning/Datalog/ AFT proof spine. Mathlib reuse is already disciplined (fine-grained imports, no blanket import Mathlib).
  • The dominant defect is namespacing incoherence: 101 of 167 @[language_interface] types are at _root_; of 146 files, 57 use namespace Argon.*, 48 use none, 41 use a bare-generic namespace (Modal, State, Closure). Core types Atom, Term, Expr, Literal, Tier, Truth4 shadow Lean.*/Mathlib — the footgun that broke the mech probe (#1038).
  • The coupling caused the mess, and RFD 0059 already cut the cause. The original drift gate text-scanned .lean files keyed on the bare inductive name, so the convention grew up to declare contract types at _root_. RFD 0059’s manifest keys on qualified names emitted by the elaborator, so root-level placement is now load-bearing for nothing — vestigial.
  • The coupling is already loose. The lean CI job (full lib build + manifest/vector freshness) is push-only and non-blocking — it does not gate PRs or the merge queue. Only the committed-manifest-vs-Rust-table check (drift.rs, no lake needed) gates the queue, and the drift key is shortName = the last namespace component, so moving a type from _root_ into Argon.Syntax.* keeps its key stable; the gate survives namespacing. A reorg’s failure mode is therefore post-merge red on main (a stale committed manifest), not a queue block.
  • Two content holes, not just structural debt: CoreIR/Lowering.lean is a placeholder (lowerRule emits empty heads/bodies, deriveCategory hardwires .cat1) — the content of the preservation theorem is absent; and ARS/Spec.lean’s ars_contracts_hold reduces to ⟨trivial, trivial, trivial⟩ — a vacuous theorem, a faithfulness liability.

Decision

Re-architect the substrate in place, proof-preservingly to the target below. The skeleton (directory layering) is kept; the skin (namespacing) is normalized; the fused organ (the ABI contract) is separated from the proof body. No rewrite; no intrinsic-typing or refinement rebuild.

  1. Namespace = directory path under Argon.*. Every declaration lives under Argon.<Layer>[.<Sub>]; no domain type at _root_; no bare-generic namespace (namespace Modal → namespace Argon.Decidability.Modal). One concept gets exactly one definition. Stated honestly as convergent best practice + footgun removal (the _root_/Lean.* shadowing is a real correctness hazard), not as a proven maintainability cause.
  2. The import graph is guarded against growing entanglement, and the foundation stays pure — but the target is bounded entanglement, NOT a strict DAG. The directory graph is not a linear DAG, and for a reflective core it should not be (see “The layering” and “Delimited reflection is forced”): the meta-calculus’s upward edges are essential reflection, permanent by design. The enforceable invariant (the evidence-backed “keep the import graph minimal” lever, plus our KNOWN_UNMIRRORED-style baseline idiom) is: a committed baseline of the cross-directory edge set that distinguishes INTENTIONAL reflective edges from ACCIDENTAL ones, a lake-free CI guard (spec/lean/scripts/check_layering.py, runs on PRs + enforces in the merge queue) that fails on any new edge (no new entanglement) or any stale edge (an accidental cycle shrank — lock the win), and hard foundation-layer purity (Foundation/Interface rest only on Mathlib). The resting state is bounded entanglement; only the accidental edges are debt.
  3. The ABI is separated from the proofs by a data-from-proofs discipline (the seam). Contract-bearing @[language_interface] types live in thin data-only modules (declarations + deriving, no substantive theorems); their proofs and semantics live in importing modules. The in-Lean elaborator manifest (RFD 0059) stays the single source of truth; no non-Lean IDL (it would reopen the two-sources-of-truth hole 0059 closed). Restructuring the proof body then never touches the contract surface.
  4. Embedding: deep + extrinsic, everywhere. Surface AST and IR stay deep-embedded (lowering is the canonical non-compositional traversal). Typing stays extrinsic. Reject well-typed-by-construction / intrinsic IR typing (Argon’s subtyping + refinement + occurrence/flow typing + RuleIR’s global stratification is exactly the rich-equational-index regime where intrinsic typing’s transport + coherence tax dominates, with no Lean port of the Allais lineage even existing) and reject wholesale Rust↔Lean refinement (≈20py, does not amortize; seL4’s own reason for keeping hand-written code).
  5. Gate posture: migration-tolerant during the window, re-armed hard after. During the migration: keep the cheap silent-accept guards hard (manifest freshness, ambiguity/shape-twin detection); demote mirror-alignment to advisory; rely on the behavioral oracle (the conformance vectors / engine_agrees_with_batched_lean_oracle, the tier that actually carries spec↔impl correctness). After the seam is stable: re-arm all of drift.rs hard and pull the freshness re-emission into the merge-queue gate (it is currently only post-merge). Operational discipline meanwhile: because the Lean is under-gated, reorg PRs regenerate the committed manifest locally before merge.
  6. Close the two content holes (separately scoped, after the structural work). Implement CoreIR/Lowering as a real translation with an explicit match-relation, and prove preservation as least-model / denotational agreement (not CompCert step-simulation — Argon’s semantics is a fixpoint). Replace the vacuous ars_contracts_hold with the real contract, or, if Rust wiring genuinely blocks it, an honest tracked open obligation rather than a True-laundered theorem.

Design

The layering: foundation purity + bounded entanglement (NOT a strict DAG)

The coarse intended order:

L0  Foundation / Interface / Schema   bilattices, the tag attribute, ontology+signature data  → Mathlib only
L1  Syntax                            the surface AST (deep, extrinsic)
L2  Core (data)                       Substrate (atoms), MetaCalculus *data* (Axis), CoreIR (incl. Lowering)
L3  Semantics                         TypeSystem, Reasoning (Datalog/AFT), Standpoint, Locality, Decidability,
                                      and the meta-calculus's *reflective semantics* (see below)
L4  Contracts                         Storage, Runtime, BuildArtifact, Pipeline, ARS
    Oracle/  Scratch/                 globbed out of the lib — not in the layering

(Schema is foundational data, not a contract — Mathlib-only, depended on by Locality/TypeSystem — so it sits at L0.)

The enforced invariant is NOT a strict linear DAG. It is acyclicity-as-achievable + hard foundation purity + a frozen, minimal entanglement baseline — what check_layering.py enforces. This is deliberate, on two grounds: it is the invariant the maintainability evidence actually supports (the strict stratification is convergent convention, not measured cause), and — decisively — a strict per-directory DAG is the wrong ideal for Argon, because its core is a reflective meta-calculus.

The meta-calculus is an intentional two-tier reflective subsystem. Its data (Axis — the axis / metatype / metarel shapes) is low (depended on downward by Storage, Decidability, …). Its reflective semantics is high by necessity: IS/CAN/NOT classification is the reasoning fixpoint (IsCanNot builds on Reasoning.Fixpoint); TypeRef reflection is decided by TypeSystem.Subtyping (Reflect); the meta-property model is the storage catalog (AxisRelation). The meta-level is expressed in object-level vocabulary — that is what reflection means (Bowen–Kowalski amalgamation; 2LTT; Lean’s own cyclic-and-operationally-broken bootstrap). So the upward edges MetaCalculus → {Reasoning, TypeSystem, CoreIR, Storage} are essential and permanent, not debt — re-homing them to satisfy a DAG would scatter a defining atom across four directories and is forbidden (the baseline marks them INTENTIONAL).

The genuinely accidental cycles — the only ones to dissolve over time — are {CoreIR, Substrate} and the filing-neutral TypeSystem → Runtime (the MutationWrites bridge). The within-L3 mutual edges (Reasoning ↔ Standpoint ↔ Locality ↔ TypeSystem) are legal within-stratum, not cycles. So “cycle-breaking” is a small, optional tidy — not a phase the architecture is waiting on.

Delimited reflection is forced (the reflective tier)

Argon’s reflection is delimited: TypeRef is a handle into a closed, predicative catalog (no Type:Type); iof/specializes/extent are decidable predicates over reasoner-materialized catalog relations; runtime metaprogramming is a separate macro atom (re-checked), not open reflection. This is forced, not stylistic, by the two commitments that define Argon — characterized decidability and a sound Lean mechanization — confirmed from four independent directions:

  • Argon’s own decidability ladder: the metaorder tier (reflection / higher-order instantiation) is “bounded decidable; otherwise not.” Decidable ⟺ bounded is the ladder’s organizing principle.
  • Soundness: impredicative Type:Type is Girard-inconsistent (Hurkens) — it could not be modeled in the predicative Lean substrate at all.
  • Static reasoning: open, syntax-observing reflection is Wand-trivial (contextual equivalence collapses to α-congruence), destroying the equational theory the static-check plane and the content-addressed build depend on — hence the macro-atom separation.
  • Argon’s own domain (DL/KR): unbounded/expressive metamodeling (OWL-Full) is undecidable; the decidable path is a controlled base + stratification. The undecidability is not from the cross-level identity tie — Motik (2007) proves tied metamodeling decidable over a controlled base — so Argon does genuine contextual-tie, catalog-tier reasoning, strictly richer than OWL-punning / Java Class<?>.

So Argon sits at the richest uniformly-decidable point: closed predicative codes for the handle, first-class bounded multi-level iof/specializes for the reasoning, with higher-order orders pushed to stratified library theories (std::mlt, std::potency at tier:metaorder) that opt back into PTIME via a declared order bound. The only construct forfeited is unbounded orderless metamodeling (Type-of-itself) — which ontological modeling does not need and which is not even proven decidable. The bounded reflective edge set in the baseline is the formal expression of this delimitation.

Two obligations this carries (tracked separately, not in this RFD’s slices): the order bound must be a checked contract the tier classifier honors (with a cross-level-equality guard), not an inferred bound; and the order_bound(N) ⇒ N-stratified ⇒ decidable demotion is currently a sound argument, not a Lean proof.

Enforcement. The baseline guard (check_layering.py, lake-free, runs on PRs + enforces in the merge queue) freezes the cross-directory edge set and holds foundation purity, failing on new entanglement. The baseline distinguishes INTENTIONAL reflective edges (permanent) from ACCIDENTAL ones (may be shrunk). There is no “phase 2 converge-to-DAG” — bounded entanglement is the resting state.

The seam (data-from-proofs)

A module that declares @[language_interface] types is a data module: type declarations + deriving, no substantive theorems. Proofs about those types live in sibling semantics modules that import them. The @[language_interface] tag stays on the real inductive/structure (the emitter reads constructor data from .inductInfo/.ctorInfo, so it must tag the actual type, not an abbrev alias). Argon/Interface.lean remains the attribute definition and becomes the documented ABI index. Consequence: a proof-side re-architecture (renaming internal namespaces, splitting proof files, reordering) cannot move a contract type by accident, because contract types are quarantined in data modules.

Dedup targets (surgical — the raw count of “6 duplicates” overstates it)

  • RuleMode — genuinely identical (Syntax/Rule.lean + Storage/AxiomBody.lean, same 5 ctors). Unify to one canonical definition (Argon.Syntax.RuleMode), Storage imports it. (Conflict note: Storage/AxiomBody.lean is modified by feat/0.3-surface-operators-630-631; sequence after it lands.)
  • WorldAssumption ×3 — untagged, but divergent constructor order across Schema/ and the two TypeSystem/Soundness/ copies (a latent bug). Unify to one Argon.Schema.WorldAssumption.
  • FieldDecl, Path — intentional same-name different-layer twins, already drift-waived (KNOWN_DUPLICATE_SHORTNAMES). Keep distinct; namespacing makes the divergence legible. No merge.
  • Term, AtomIR — the second copy is the out-of-target oracle (Reasoning/EvalProgram.lean); namespace the oracle as Argon.Reasoning.Oracle.* so the divergence is named, not accidental. No merge.

Migration plan (proof-safe slices, in order)

  1. Layering guard (done in this RFD’s PR) — check_layering.py + the committed 52-edge baseline, wired as a lake-free lean-layering CI job (runs on PRs, enforces in the merge queue). Freezes entanglement and foundation purity now; no code moved.
  2. Namespace normalization — move every declaration under Argon.<Layer>; kill _root_ and bare-generic namespaces; ensure no open Lean in the spine. Proof terms are untouched (rename + import churn only); the drift shortName key survives; regenerate the committed manifest in the same PR. This does not change cross-directory edges, so the layering baseline is unaffected. Sequence the MetaCalculus/* and Storage/AxiomBody.lean files around feat/0.3-surface-operators (do them last or after it merges).
  3. Optional tidy (NOT cycle-breaking the reflective tier) — the meta-calculus’s upward edges are intentional reflection and stay. The only accidental edges worth dissolving are {CoreIR, Substrate} and the filing-neutral TypeSystem → Runtime (MutationWrites, which could move to Runtime). Small and optional; the guard’s stale-edge check locks any win. Do not re-home MetaCalculus/{IsCanNot,Reflect,AxisRelation}.
  4. Dedup — RuleMode, WorldAssumption; namespace the oracle twins (Argon.Reasoning.Oracle.*). Coordinate on Storage/AxiomBody.lean.
  5. Re-arm the gate — pull freshness into the queue gate; restore mirror-alignment to hard.
  6. Content holes (Option C, separate effort) — lowering match-relation (#1063); de-vacuify ARS.

Each slice: own worktree off origin/main; lake build + mech verify + the drift tests + manifest freshness green before merge; commit as you go.

Alternatives considered

  • Intrinsic / well-typed-by-construction IR, or seL4-style refinement against the Rust engine. Rejected on documented cost-scaling grounds (transport + coherence tax for rich indices; refinement does not amortize). Argon’s extrinsic-deep choice already matches CompCert/CakeML.
  • A non-Lean IDL for the contract. Rejected — reintroduces the two-sources-of-truth hazard RFD 0059 eliminated; the contract belongs in the prover, since the Lean leads on substrate semantics.
  • Formally decouple / rip the gate to fully advisory during the redesign. Rejected as unnecessary: the gate is already PR-/queue-non-blocking and survives namespacing, so migration-tolerant posture suffices while keeping the cheap silent-accept guards.
  • Do nothing (keep the organic structure). Rejected: the _root_ shadowing is an active footgun, and “architected” means the layering is a checked invariant, not prose that drifts.

Non-goals

  • The reasoner-semantics catch-up (the Rust-leads-the-Lean reasoner gap, issue #134) is out of scope; this RFD is about structure and the contract, not closing semantic gaps beyond the two named content holes.
  • Naming/namespacing is adopted as cheap anticipatory hygiene + footgun removal; this RFD makes no claim that it causes lower maintenance cost (the evidence does not support that claim). The evidence-backed maintainability levers — acyclic/minimal import graph, one-concept-one-definition, interface-hiding, proof-robustness (structural tactics, no auto-generated-name dependence), a deprecation path before foundation-type changes — are folded into the slices above and the layering DAG.