RFD 0040 — The procedural macro layer

• Status: P2 built — all builtin stubs retired. Reflection-types-as-real-types (#850) and the Lean line (D7) remain.
• Depends on: RFD 0037 (the macro atom — declarative layer, D7 Lean line, D9 deferred analytic layer), RFD 0038 (nothing-ambient / import discipline)
• Blocks: the genuine re-home of the relation-property checks and the MLT decorators (today shipped as builtin-backed P0 stubs, RFD 0037 D8); the classify ∘ expand tier-honesty theorem (RFD 0037 D7)
• Implements: RFD 0037 D9 — “the procedural / analytic layer is deferred, with its end-state shape committed.”

Amendment (P2 built) — bounded structural iteration

D4 below commits to general structural recursion checked at declaration. Building P2 ruled the meta-language’s traversal to be bounded structural iteration instead, and this amendment records that decision (it supersedes the recursion framing in D4 / D6 stage 3 / Acceptance test 2):

• The one iteration form is $( for x in item.fields ) { … } (and item.params) inside quote — a bounded loop over a finite reflected child-list, total by construction, nestable for depth. There is no user-writable recursion or call form (only the concat_idents paste builtin). So totality needs no decreasing-argument analysis: the body is a closed fragment {let-paste, quote + $(for) + ${…}/if, match on a reflected scalar, list-lit of quote/artifacts}, and anything outside it is refused at the declaration (OE0729 — Acceptance test 2, reframed from “non-structural recursion refused” to “out-of-fragment construct refused”).
• Rationale (not effort): strong normalization without a checker that could itself be wrong; alignment with Argon’s determinism + decidability + cheap-Lean doctrine; the warning in this RFD’s own Background that compile-time-Argon must not grow “more powerful and less correct.” Every real client needs ≤2 levels of named children, which nested bounded iteration covers.

Landed: P2 structural field reflection + the derive-class capability (proven by #[reflect_fields], Acceptance test 3); the OE0729 totality guard (Acceptance test 2); #[functional] retired — the last #[builtin] (it is now a std::rel procmacro that dispatches on item.kind: a rel re-emits with a [0..1] target cardinality cap via structural re-emission, a metarel pastes the __{rel}_functional check — Acceptance test 1’s third). The MLT re-home (Acceptance test 4) had already landed under RFD 0043. OE1362 (the #[functional] import gate) is retired — an unimported one is now OE0705, like its siblings.

Remaining: the reflection vocabulary as real resolvable types (#850; the hover symptom is already fixed) and the Lean Syntax carrier + tier-honesty theorem (D7). Reference §13.5/§13.8 + §05 prose lift from “deferred”/“builtin” to “built” — coordinated with the docs work, not in the compiler branch.

Summary

RFD 0037 shipped the macro atom’s declarative layer (pub macro, pattern→template, hygiene, expand-to-surface) and committed — but did not design — the procedural layer: “a total, structurally-recursive meta-language over reflected syntax — not general-purpose Argon.” This RFD designs that layer.

The motivation is honesty, not novelty. Two macro clients ship today as P0 stubs — a library surface whose implementation is still a privileged compiler builtin, because the declarative layer cannot express them:

• the relation-property checks (#[irreflexive]/#[asymmetric]) need to construct an identifier (__{rel}_irreflexive) — paste — which a splice-only language has no operator for. (#[functional] is the family’s third member but is not paste-shaped: one of its two arms re-emits a rel with a modified cardinality bracket, which is structural re-emission — P2 — so it stays a builtin stub past P1; see D6 / Acceptance test 1.)
• the MLT decorators (#[categorizes(T)] …) need to read the decorated declaration’s name and emit a metaproperty — which has no user-writable surface.

A stub is a deferral, not a re-home: the library owns the surface, the compiler still owns the implementation. The procedural layer is what turns these into genuine macros and lets the library migrate its implementations. It is deliberately smaller than “compile-time Argon”: a total fragment, strongly-normalizing by construction, so it preserves Argon’s determinism (content-addressed builds), decidability-tier honesty, and Lean-mechanizability.

This RFD is design-first: it crystallizes the surface, the reflection model, the totality discipline, the staged delivery, and the Lean line. The committed first implementation step — P1, identifier construction (paste) — is now built (#567): it retires the #[irreflexive] + #[asymmetric] stubs (genuine #[procmacro]s, byte-identical events). #[functional] stays a builtin stub until P2 (its cardinality-cap arm is structural re-emission, not paste).

Background — what’s a stub today, and why

The declarative layer is Syntax → Syntax by splice: it matches a token pattern and substitutes captured fragments into a template. It has no operation that (a) builds a new identifier from pieces, or (b) inspects a declaration’s structure and computes output from it. Both current stubs need exactly one of these:

The research campaign (research/macro-system, D4) recommended C-then-B: declarative now, then a bootstrapped-in-Argon procedural layer on a zero-capability Wasm substrate, fuel-bounded. RFD 0037 D9 narrowed that to a total meta-language — strongly-normalizing by construction rather than fuel-bounded-and-Turing-complete — because totality is what Argon’s own doctrine demands (deterministic builds, the decidability ladder, Lean-canonical substrate) and “a Turing-complete compile-time Argon would be more powerful and less correct.” This RFD designs the committed total meta-language; Wasm is then an implementation option for its sandboxed substrate, never the user-facing surface.

Decision

D1 — Surface: #[procmacro] pub fn, body in a total fragment

A procedural macro is a function marked #[procmacro], in the one macro namespace (RFD 0037 D9; the !/#[…] sigils are invocation markers, not namespace tags). This is the shape already carried by the Lean substrate (Macro.lean: MacroAtom.procedural : ProcMacroDecl → MacroAtom, p.fn.name/p.fn.isPub).

#[procmacro]
pub fn transitive(item: Decl) -> Syntax = …      // a derive-style decorator

The body is not general-purpose Argon. It is a total fragment: structural recursion over reflected Syntax, the construction/quotation builtins (D3), and pure expressions — no I/O, no clock/RNG/filesystem, no unbounded recursion. The body’s totality is checked at declaration (D4), so a #[procmacro] either is strongly-normalizing-by-construction or is refused — never “trusted to terminate.” #[procmacro] is currently reserved (OE0706); this RFD lifts the reservation in stages (D6).

Rationale: reusing pub fn (not a bespoke DSL keyword) keeps the surface familiar and the namespace single; restricting the body to the total fragment is what buys determinism + decidability + mechanizability. This mirrors Argon’s own tier ladder — the meta-language is, in effect, a low-tier total sublanguage applied to syntax.

D2 — Reflection model: an inductive Syntax, read-only, finite

The macro receives its input as a value of an inductive Syntax type — the reflected post-parse AST (a deep embedding mirroring the typed AST that @[language_interface] already governs). Inputs by invocation position:

• function-like name!(tokens) → Syntax of the argument fragment;
• attribute / derive #[name(args)] <item> → the decorated Decl (a Syntax subtype) plus the attribute args fragment.

Reflection is read-only and finite: a Decl exposes its name, kind, generics, parameters, fields, and attributes as Syntax children; a macro pattern-matches and recurses on those children, which are structurally smaller. There is no reflection of resolved identity (DefIds), types post-elaboration, or tiers — expansion runs before resolve/check (RFD 0037 D1), and reflecting post-resolution facts would break the phase ordering and S4 (tier-honesty). The Syntax shape is itself an @[language_interface] carrier, so the drift gate covers it (D7).

D3 — The construction builtins: paste, quote, splice

The meta-language’s output side is three primitives, each total:

• quote { … } / splice — build Syntax from a literal template with $-holes (the declarative transcriber, now first-class and nestable). Output is surface text re-parsed by the ordinary path (RFD 0037 D2) — never events directly.
• concat_idents(a, b, …) (paste) — construct a new identifier from identifier/literal pieces. This is the single capability the three checks need (concat_idents("__", rel_name, "_irreflexive")). It is total (string-level), non-recursive, and deterministic.
• structural match over Syntax — case-split a reflected node and recurse on its children (D4).

A pasted identifier is raw (definition-site, not freshened): the macro intends it as the actual program name — like the check head __{rel}_irreflexive, which must be a stable, collision-resistant identity the classifier and the .oxbin see. Paste therefore composes with hygiene (RFD 0037 D3) as a definition-site name in the reserved-marker namespace where collision-resistance is needed, and as a plain raw name where the macro author wants a predictable public name. (The exact hygiene interaction of paste is the one sub-decision flagged in Open Questions.)

As shipped in P1: concat_idents emits the pasted head as a raw definition-site name with no freshening — exactly the former synthesis’s __{rel}_{prop}. Splices ($item, $item.name, $item.params[i].ty) are substitution barriers: the reflected text is dropped in verbatim, carrying its own use-site identity, not re-scoped by the macro. So P1 does no hygienic renaming at all — which is correct for these checks (they want the stable public head), and is the conservative floor the Open-Questions paste×hygiene decision will build on.

D4 — Totality: structural recursion, checked at declaration

Termination is by construction, not by fuel. The only recursion the meta-language admits is structural: a recursive #[procmacro] (or meta-helper) may recurse only on a Syntax value that is a proper child of its argument. The compiler checks this at declaration (a decreasing-argument check over the finite Syntax tree — the same well-founded-recursion discipline Lean uses for structural recursion). A body that cannot be shown structurally decreasing is refused (a new OE07xx), not accepted-and-fuel-capped.

A fuel cap (RFD 0037’s OE0727 runaway diagnostic) remains as a backstop against implementation bugs, but it is not the termination argument: the argument is strong normalization of the total fragment. This is what makes expand a total function over an inductive type — the precondition for the D7 theorem — and what distinguishes this layer from the research’s fuel-bounded Option B.

Determinism: no non-determinism sources are in scope (no clock/RNG/FS/hash-seed); emitted collections are emitted in canonical (content-sorted) order; fresh names are content-derived (RFD 0037 D3). The drift contract (S2) and tier-honesty (S4) hold because the classifier still runs last on lowered events (RFD 0037 D6) — expansion is upstream of, and invisible to, the trusted re-check.

D5 — The MLT path: an axis-assertion surface

The MLT decorators are not paste and not field-reflection — they read the decorated concept’s name and emit a MetaProperty(subject = the concept, axis = the metarel, value = T). Today that event has no user-writable surface, which is why the expander stays native. The procedural layer’s MLT deliverable is therefore a surface for asserting a metaproperty, e.g.

#[procmacro]
pub fn categorizes(item: Decl, target: Ident) -> Syntax =
    quote { assert std::mlt::categorizes($item.name, $target) }

where assert <metarel>(a, b) is a surface form that lowers to a MetaProperty event. With (a) light decl-reflection ($item.name) and (b) this axis-assertion surface, the four MLT decorators become genuine procedural macros emitting through the ordinary path — and the native lower_relational_mlt_decorators emitter retires. The metaproperty surface is partly independent of the meta-language (it is an event surface question), so it is its own decision here and could land separately.

D6 — Staging: the full layer, built in sequence

The procedural layer ships in full, in three stages built in order — each stage retires real debt, and stage 3 follows stages 1 and 2; no stage is gated on a hypothetical future client. (“Built when a derive-class client forces it” — the framing RFD 0037 D9 and the research used — is a hollow deferral that lets the capability never get built; this RFD rejects it. The capability is the deliverable.)

1. P1 — paste (concat_idents) + the #[procmacro] surface for non-recursive bodies. Total trivially (no recursion). SHIPPED: retires the #[irreflexive] + #[asymmetric] P0 stub — they become genuine std::rel procedural macros emitting byte-identical events (their arms in synthesize_relation_property_rules are deleted; OE0706 reservation for #[procmacro] is lifted; the new evaluator is oxc-workspace/src/procmacro.rs). #[functional] does NOT migrate in P1: its rel-cardinality-cap arm needs to re-emit a rel with a modified cardinality bracket = structural re-emission = P2, and a single attribute name cannot be half-builtin/half-procmacro — so functional stays a #[builtin] stub (OE1362-gated) until P2. This was the committed first implementation step; it is now built.
2. The axis-assertion surface (D5). Retires the MLT P0 stub — the four std::mlt decorators become genuine procedural macros.
3. P2 — full structural recursion over reflected Syntax (D2+D4) — the committed end-state meta-language. Built once stages 1 and 2 are done. It is exercised + proven by writing a real derive-class macro (one that inspects a concept’s fields and synthesizes per-field output — e.g. a #[derive(Reflect)]-style macro) as part of the deliverable, not by waiting for one to “arrive.” This stage also makes expand a total Lean object, unlocking the D7 theorem.

Each stage is surface-stable: a stub-backed #[name] and its procedural-macro implementation have byte-identical lowered events, so migration never changes a program’s meaning (RFD 0037 D8 / S3). RFD 0037 D9 deferred this layer “until a forcing client”; this RFD supersedes that — the full layer is built in sequence.

D7 — The Lean line: hold the AST boundary; pursue tier-honesty when expand is a Lean object

Per RFD 0037 D7 and the research (track-F: Lean 4, CompCert, translation-validation all mechanize the re-checker, not the producer), the expander is untrusted by design. Assurance is the downstream re-check: the tier classifier runs last, the .oxbin content hash is re-derivable, and the drift gate covers the MacroAtom = declarative MacroDecl | procedural ProcMacroDecl shape plus the Syntax carrier (D2).

What changes with this RFD: the total meta-language makes expand a total function over an inductive Syntax type — the precondition for stating the tier-honesty commutation theorem (classify ∘ expand lands a program on the same decidability class as its expansion). RFD 0037 named this “the one worth pursuing.” This RFD commits: when P2 lands, expand becomes a Lean object and the tier-honesty theorem is the rung-(c) deliverable — not a full MacroExpansion.lean expansion-preservation proof (rung d, CakeML-scale, out), not hygiene-algebra mechanization (rung b, POPLmark-scale, out). The totality discipline (D4) is precisely what keeps that theorem statable and the substrate honest.

D8 — Conservative monotonicity: a macro may only raise the tier

A macro’s expansion may land its program at a higher decidability tier than the source spelled, never silently lower it (the program is classified last, on the truth). Sound tier-lowering desugarings — where a macro provably produces a lower-tier equivalent — are a later, proof-carrying escape hatch, out of this RFD. This keeps S4 a structural guarantee during expansion, not a per-macro audit.

Migration

• P1 landed → std::rel’s #[irreflexive] and #[asymmetric] are now genuine #[procmacro] pub fn … -> Syntaxs: each re-emits the decorated declaration ($item), projects the relation’s name and endpoint types ($item.name, $item.params[i].ty), and pastes a guarding pub check whose head is concat_idents("__", item.name, "_{prop}"). Their arms in the native synthesize_relation_property_rules are deleted, and their import gate shifted from OE1362 to OE0705 (a bare unimported #[irreflexive] is now an unknown attribute macro, exactly like transitive). The byte-identical differential test (relation_property_rehome.rs) now asserts the procedural macro’s events equal the hand-written expansion. #[functional] is deferred to P2 and stays the #[builtin] stub (OE1362-gated): its rel-cardinality-cap arm needs structural re-emission, and an attribute is builtin or procmacro, not both.
• Axis-surface lands → rewrite the four std::mlt decorators as #[procmacro]s; delete lower_relational_mlt_decorators. Closes #483 genuinely (not as a surface stub).
• No source migration for users: #[transitive], #[irreflexive], #[categorizes(T)] are spelled identically before and after; only the import (use std::{rel,mlt}::{…}, already required post-RFD-0038) and the byte-identical events are observable. S3 holds at every step.

Acceptance tests

1. P1 retires the checks’ stub (byte-identical): #[irreflexive] and #[asymmetric] are re-expressed as #[procmacro]s — each re-emits the decorated declaration ($item) and pastes a guarding pub check whose head is built by concat_idents("__", item.name, "_{prop}") — and produce events byte-identical to the former synthesis (relation_property_rehome.rs); their arms in synthesize_relation_property_rules are deleted. #[functional] stays a #[builtin] stub, not a procmacro: it is one attribute that covers BOTH a metarel-check (paste-able) AND a rel-cardinality-cap [0..1] on the target endpoint (lower.rs, the cap arm) — and re-emitting a rel with a modified cardinality bracket is structural reflection, which is P2. Because an attribute name is either a builtin or a procmacro (not both halves split across the two), functional stays entirely a #[builtin] stub (both the rel-cap and the metarel-check synthesized natively, OE1362 import-gate retained) until P2 builds structural re-emission. So P1 retires two of the three checks byte-identically; the third is deferred because the capability (structural re-emission) is unbuilt — not for want of a client.
2. Totality is enforced, not trusted: a #[procmacro] whose body recurses non-structurally is refused at declaration (the new totality OE07xx), with no fuel-cap fallback masking it.
3. A genuine derive-class macro (P2): a real procedural macro that inspects a concept’s fields and synthesizes per-field output — written as part of the P2 deliverable — expands end-to-end (parse → EXPAND → resolve → check → instantiate → classify), clears the §3.4 gate, and lands on its true tier.
4. MLT genuinely re-homed: the four MLT decorators are #[procmacro]s emitting via the axis-assertion surface; lower_relational_mlt_decorators is deleted; events byte-identical.

Lean obligations

• Extend the @[language_interface] drift coverage to the reflected Syntax carrier (D2), so the Rust Syntax reflection type and the Lean Syntax inductive stay aligned by the existing gate.
• No MacroExpansion.lean in P1/P2-surface. When P2’s expand becomes a total Lean function, schedule the tier-honesty commutation theorem (rung c) — the distinctive Argon invariant — as the macro layer’s first mechanized theorem (D7).

Spec reconciliation (reference edits)

• §13.5 (“Procedural macros (deferred)”) → describe this design: the #[procmacro] pub fn surface, the total meta-language, reflection, paste, the axis-surface, and the full staged build (P1 → axis-surface → P2, in sequence). Lift “deferred” to “built (P1 first)” — drop the “first derive-class client” trigger.
• §13.8 (Lean correspondence) → add the Syntax carrier + the tier-honesty theorem schedule.

Resolved (this RFD)

• The procedural model is the total meta-language (RFD 0037 D9), not the research’s fuel-bounded bootstrapped-Argon (D4 R1) — committed and now designed.
• Totality is by construction (structural recursion, checked at declaration), not fuel-bounded (D4).
• No client-gating: the full layer is built in sequence (P1 → axis-surface → P2); P2 is built once 1 and 2 are done, not “when a derive-class client forces it.” This supersedes RFD 0037 D9’s forcing-client trigger (a hollow deferral) (D6).
• P1 (paste) is built — it retires the #[irreflexive] + #[asymmetric] stubs byte-identically; #[functional] stays a #[builtin] stub pending P2 structural re-emission (D6, Acceptance test 1).
• quote’s ${expr} antiquotation is expansion-time. The in-string ${…} form inside a quote { … } body (e.g. the diagnostic message "relation ${item.name} is #[irreflexive] …") is resolved by the macro renderer at EXPAND, substituting the reflected/let-bound value into the rendered surface text before re-parse. It needs no runtime string concatenation — it is a render-time splice, total and deterministic.

Open questions

1. Paste × hygiene: the precise hygiene treatment of a concat_idents result — raw definition-site name vs reserved-marker freshening — per use (D3). The three checks want a stable public-ish __{rel}_{prop}; a general paste in user code may want freshening.
2. The axis-assertion surface shape (D5): assert categorizes(a, b) vs a metaproperty-bearing declaration form — an event-surface question that may warrant its own short RFD.
3. Reflection accessor API for P2: the precise Decl/Syntax accessor set — settled when building P2 as a complete reflection of a declaration’s structure (name, kind, generics, parameters, fields, attributes), not a minimal subset and not deferred to a client.
4. ${} spelling-overlap with runtime string interpolation. P1’s quote antiquotation ${expr} is an expansion-time render splice (resolved above, Resolved). It is spelled the same as a hypothetical runtime string-interpolation form "…${x}…" that would lower to string concatenation and const-fold — but that is a separate, unbuilt foundational arc (tracked as issue #575): the runtime today has no Text + Text operator and no const-fold pass, so general runtime interpolation does not exist. Do not assume the two ${…} spellings unify — whether the render-time antiquotation and a future runtime interpolation should share a surface (or must be kept distinct, since one is total-by-construction at EXPAND and the other is value-level) is an open question for the #575 arc, not settled here.
5. elab-class (type-directed) expansion — firing a macro over the expected metatype/sort — is a distinct mechanism (type-direction), not part of the procedural layer (computing an expansion). It stays out of this RFD’s scope; the real ergonomic need it was floated for (legal scoping) is already served by binding-space resolution. If type-direction is wanted, it is its own design, not a deferred piece of this one.