RFD 0059 — The drift gate as a typed interface manifest

State: accepted
Depends on: RFD 0055 (the conformance corpus — the “Lean emits → Rust replays → CI freshness-gates” loop this reuses), the @[language_interface] contract (spec/lean/Argon/Interface.lean ↔ compiler/crates/oxc-protocol/)
Tracks: issue #1038
Prior art: the project’s own conformance-vector loop (EmitVectors.lean → compiler/tests/lean-vectors/*.json → conformance_replay.rs, CI-freshness-gated in check.yml); schema-from-source generation (protobuf descriptors, cargo-public-api); the general principle that a contract checker should read the elaborated artifact, not re-parse the surface text.

Question

@[language_interface] is the load-bearing Lean↔Rust contract: inductives tagged with it carry the language’s data shapes, and the Rust mirror enums in oxc-protocol must align by name and arity. CI enforces this through compiler/crates/oxc-protocol/tests/drift.rs. Is that enforcement sound, or is it fragile in a way that can let real drift through silently?

Context

drift.rs establishes the Lean side of the contract by textually scanning every .lean file under spec/lean/Argon/: it greps for @[language_interface], then for the next inductive line, then parses constructor lines for names and counts → arrows for arity. Three properties of that scanner are load-bearing and, on inspection, fragile:

It keys on the unqualified inductive name (the token after inductive) and resolves duplicates with .or_insert — first-in-filesystem-walk-order wins. read_dir order is not deterministic across machines.
There is more than one tagged inductive with the same short name. RuleMode is @[language_interface]-tagged in both Syntax/Rule.lean and Storage/AxiomBody.lean. They currently have identical variants, so the mirror binds correctly by luck, not by construction — the moment the two diverge, the gate binds to whichever the walk reaches first and can report green on a drifted type. (Term and AtomIR also have same-named twins in Reasoning/EvalProgram.lean; those are saved today only because the twins are untagged.)
Coverage is partial and silent. ~88 inductives carry the tag; only ~40 appear in declared_mirrors(). A tagged type with no mirror entry drifts entirely undetected — only a coarse “≥ 25 discovered” sanity floor and the Decl→grammar.toml check guard the remainder.

On top of these, the scanner is regex-grade parsing of a real grammar (one-line | a | b | c, :-detection, breaks on def/theorem/@[), so it can mis-read multi-line constructor signatures or attribute-then-comment-then-inductive sequences.

None of this is hypothetical drift today — the gate is green. But it is one rename away from a silent false-pass on a CI-enforced correctness contract, which is the exact “silent-accept at an un-RFD’d seam” failure class the 2026-06 system audit found to dominate.

Decision

Stop deriving the Lean side of the contract by re-parsing surface text. Have the Lean elaborator emit a typed interface manifest — every @[language_interface] declaration with its fully-qualified name, kind, and constructor names + arities — and have the Rust gate diff its mirror table against that manifest. The manifest is the same shape of artifact as the conformance vectors: Lean computes it, it is committed, and CI freshness-gates it against a fresh emission.

This makes three things true by construction that the scanner only approximated:

Names are qualified, so same-short-name twins are distinguishable and the binding is never ambiguous.
The elaborator is the source of truth for constructors and arity, so there is no grammar to re-parse and no parsing bug to hide drift.
Coverage is enumerable: the gate sees every tagged declaration and can require each to be either mirrored or explicitly waived, turning “silently unchecked” into “explicitly listed.”

Design

Emitter. spec/lean/EmitInterface.lean + an emit-interface lean_exe. It folds over the environment, selects declarations tagged @[language_interface], and emits, sorted by qualified name for stable diffs:
```
{
  "_comment": "GENERATED by `lake exe emit-interface` — do not edit by hand.",
  "schema": "argon.interface.v1",
  "decls": [
    { "name": "Argon.Substrate.Atom", "shortName": "Atom", "kind": "inductive",
      "ctors": [ { "name": "metaCalculus", "arity": 1 }, … ] },
    …
  ]
}
```
arity is the constructor’s field count (parameters excluded) — the same convention the Rust mirror table already uses (metaCalculus : MetaCalculusAtom → Atom ⇒ arity 1). Structures carry kind: "structure" and their single mk (waived from mirroring; included for completeness).
Committed artifact. compiler/tests/lean-vectors/interface-manifest.json, alongside the conformance vectors, never edited by hand.
Gate. drift.rs parses the manifest with serde instead of scanning .lean files. It then:
1. Detects ambiguity: if two manifest decls share a shortName with different ctors, hard-error (the divergence hole). Identical twins (today’s RuleMode) are tolerated and bind unambiguously.
2. Checks each mirror (declared_mirrors()) against the manifest decl of that name by constructor PascalCase-name and arity — the existing alignment logic, now over typed data.
3. Enforces coverage: every inductive manifest decl is either mirrored or in an explicit UNMIRRORED_WAIVERS list with a one-line reason. A newly-tagged-but-unmirrored type fails the gate instead of passing unseen.
4. Keeps the Decl→grammar.toml variant check and a sanity floor, now exact against the manifest.
Freshness. CI re-emits and diffs, exactly as the conformance vectors are gated (check.yml): lake exe emit-interface piped to diff against the committed manifest, with a clear regen instruction on mismatch. The cargo test only consumes the committed file (it does not require lake), matching the established split.

Non-goals (sequenced separately)

Namespacing the root-level surface AST types (_root_.Expr/Pattern/Literal/RuleAtom/RuleMode/…). These shadow Lean.* under open Lean and are a latent footgun for any metaprogram in the tree (it is what broke the mech probes before the tool-side fix). The typed manifest emits qualified names regardless, so it composes with a later move into Argon.Syntax.* — but that move is a large mechanical rename across the canonical substrate, a merge-conflict hazard against the many in-flight branches, and no longer load-bearing for any tool. It is tracked as its own change, to be done in a quiet window after this manifest lands.
Rust-side introspection. The mirror table stays hand-maintained; Rust enums are not reflected at test time. The manifest secures the Lean side (where the parsing fragility lived); the Rust side remains a small, reviewed table.

Alternatives considered

Harden the text scanner in place (B1): make .or_insert a hard duplicate-name error and assert mirror-or-waiver, keeping textual parsing. Smaller, and it closes the two worst holes (ambiguous binding, silent coverage gap). Rejected as the primary because it leaves the grammar-reparsing brittleness and keeps two encodings of “what is tagged” (the scanner’s view and the elaborator’s truth) that can disagree. It is the acceptable fallback if the emitter proves disproportionate.
Do nothing — the gate is green. Rejected: green-by-luck on a contractual gate is the failure mode this RFD exists to remove.

Keyboard shortcuts