Lean Rc Linearity

Lean 4 reference counting and linearity

Canonical source: https://lean-lang.org/doc/reference/latest/Run-Time-Code/Reference-Counting/. Runtime background distilled from Henrik Böving, Everything You Need To Know About The Lean Runtime (Lean FRO offsite, 2026-05-18). Project findings cite DESIGN.md sections and commits in this repo; toolchain evidence is lean.h at v4.33.0.

0. The one rule

An in-place update happens iff the object is at RC 1 at the moment of the mutation. Anything alive across that moment — a variable the compiler chose to keep live, a closure that captured it, a tuple the loop is threading — is a second reference, so the mutation copies the whole structure instead.

Corollary that costs the most time to learn: compiler liveness placement decides this, not source order. Every RC-2 holder found in this project was a compiler-liveness surprise, invisible in the source. Reason about it, then measure it (§4).

1. Rules first (apply these while writing)

1. Use-then-consume. Every use of a value must finish before the mutation that consumes it. If a rare branch needs the pre-mutation value, decide the branch before the expensive step, don't straddle it. (DESIGN.md "FEnv linearity", §3.4.)
2. No for/mut loops over threaded state on a hot path. Compiled forIn boxes the accumulator tuple and keeps the previous iteration live into the next step call. Use explicit tail recursion with the accumulators as plain arguments. (progressLoop/diagLoop/parseExportStream in Main.lean, ConLeche/Frontend/Export.lean.)
3. modify, not get/set. let s ← get; let s := f s; set s leaves the ref holding its own copy while you mutate; modify f hands ownership through. The VEIR parser went 22 s → 4.5 s on exactly this change (getContext/setContext → modifyContext).
4. One-shot container ops, not read-modify-write. HashMap.alter over getD + insert; Array.modify/set over read-then-write.
5. State reads that cross a call must be opaque. A read helper that inlines to a pure projection can be sunk past a later call, keeping the projected value alive across it. Mark it @[noinline] (§3.1).
6. Closure capture is an owned reference for the closure's whole lifetime. Building ops fe (a record of closures over fe) and passing it to a long call pins fe for the duration of that call, even though the source "just passes a parameter" (§3.4).
7. Borrow read-only parameters. @& (or inferred borrowing) elides RC on traversals entirely (§2.3).
8. Prefer a phase that returns only Bool. It provably cannot retain anything it built (§5.2).

2. Mechanics (enough to reason from)

2.1 Object model

Every heap object starts with an 8-byte header:

typedef struct { int m_rc; unsigned m_cs_sz:16; unsigned m_other:8; unsigned m_tag:8; } lean_object;

m_rc: > 0 single-threaded, = 1 unique, = 0 persistent, < 0 multi-threaded (atomic RC). m_tag is 8 bits → at most 256 constructors. Every indirection costs ≥ 8 bytes, which is why flattening nested structs into scalar fields is a real memory win (leanprover/lean4#11162: ~1 GB off Mathlib's language server by inlining Lsp.Range/Position into Nat fields).

Representations: enum inductives → unboxed integers; single-ctor single-field inductives → that field; everything else lean_ctor_object; Array → lean_array_object; ByteArray/FloatArray → lean_sarray_object; UIntN/USize → native ints; Float32/Float → float/double; Nat/Int → tagged scalar or boxed MPZ.

Boxing when an unboxed value is passed where a lean_object* is expected: UInt8/16/32 → tagged ((n << 1) | 1); UInt64/USize/floats → a single-field ctor allocation; Nat/Int → tagged while small, MPZ otherwise. Chains like n.toNat.toUInt64 pay this repeatedly; a struct of UInt64 fields beats a polymorphic Prod'.

2.2 In-place update and reuse

Array/ByteArray always update in place at RC 1; lean_ctor_object when the compiler decides to. Reuse: when the optimizer sees x will be dec-ed and then an object of the same layout allocated, it emits a runtime uniqueness check and reuses x's memory instead of hitting the allocator.

2.3 The RC ABI

Three argument kinds:

• scalar (uint8, tagged) — never RC-ed;
• owned (x : obj) — the callee must dec it;
• borrowed (x : @& obj) — the caller stays responsible.

Insertion is then forced: inc x when passing x as owned while still using it later; dec x once x is dead, owned and not transferred. A parameter is inferred borrowed if it is only read from, only passed on as borrowed, and never used in reuse — and modern Lean lets you write @& on ordinary functions, not just @[extern]. Marking a recursive read-only traversal @&Node α β → … removes the RC traffic from the whole walk.

Avoiding RC matters beyond the counter bump: it adds code size, adds "is it mt?" branches, and LLVM refuses to optimize across atomics (it will not prove *x still reads 42 after an atomic_fetch_add on an unrelated pointer).

2.4 Compiler knobs you will actually reach for

• Inlining is annotation-driven (auto-inline only below compiler.small, default 1): @[inline]/@[always_inline], @[macro_inline] (parameters treated lazily — fixes control-flow helpers like a custom ite), @[noinline], and inline (f x) at a call site.
• Specialization: type classes specialize by default; @[specialize], @[specialize f], @[nospecialize], @[weak_specialize] (for Inhabited-style classes that should ride along only). Inner let rec go loops usually need an explicit @[specialize] to escape closure/vtable passing.
• Tracing: trace.Compiler (everything), trace.Compiler.saveBase / saveImpure (end-of-phase IR), trace.Compiler.simp, trace.Compiler.result, plus pp.funBinderTypes / pp.letVarTypes. (trace.compiler.ir.result is gone.)

2.5 Concurrency notes (rarely relevant here, but sharp)

Putting a value into Std.Mutex, IO.Ref or Std.Channel marks it multi-threaded → atomic RC forever after. IO.Ref is a TAS spinlock: for real multi-threading use Std.Mutex. Blocking inside IO.asTask does not context-switch and stalls the pool — use Async/Async.sleep. Prefer bounded channels.

3. The three-and-a-half RC-2 holder incidents in this repo

All four have the same shape: a value stayed live across a mutation site because of where the compiler placed liveness, not because the source shared it. Retention across a mutation = inc = copy at that site.

3.1 Sunk pure store reads → @[noinline] withStore

withStore f inlined to the pure application f s.store. When the result was not consumed before the next call, the compiler sank the application past that call (profitable when the call can throw) — e.g. inferBodyI computed getAppArgsI only after r.infer returned, keeping the projected EStore at RC 2 across the entire nested inference. ~6100 whole-table copies per run; ~35 % of the init-prelude probe. Fix: withStore is @[noinline] — an opaque state-threading call cannot be reordered, so the projection lives and dies inside the callee. (ConLeche/Kernel/CoreI.lean:279-291; DESIGN.md "The whole-arena copy-on-write strikes".) Note viewI stays @[inline]: its result is always immediately matched, and branch selection forces it before any later state op.

3.2 progressLoop: the boxed forIn accumulator

The progress heartbeat's (--progress) for/mut loop compiled to forIn, whose state tuple (fe, s) stays live into the next step call — so the interned state entered every declaration at RC 2 and the first mutation struck (+110 G instructions in both modes). Fix: explicit tail recursion, accumulators as plain arguments (Main.lean:86).

3.3 diagLoop: the diagnostic second pass

"Non-progress is >20× slower" on Mathlib prefixes was not the verified fold — checkDeclsPure's List.foldlM compiles to a specialized tail-recursive loop threading state uniquely (confirmed in the generated C). It was checkMain's diagnostic second pass (error branch only, and every big Mathlib stream ends in a decline): its for d in decls2 loop's boxed state tuple kept the re-parsed arena at RC 2 into every step, so each declaration's first arena mutation copied the whole node/hash tables. Copy cost grows with the arena, which is why small streams never showed it. Fix: diagLoop, same explicit-recursion pattern (Main.lean:124; DESIGN.md "Mathlib-scoping driver fixes" item 2).

3.4 The FEnv cert branch (#99): closure capture across the value check

Every defnDecl cost a full copy of the FEnv.idx bucket array — a hidden O(n²) in the number of definitions. The driver branches kept fe live across checkDefnValP for the conditional Nat-op certification (certifyNatEqs (sharedOps fe) fe.env, checkDivModPinF … fe fe2, intentionally pre-insertion), so fe was pinned at RC 2 and the final fe.push copied the map. sharedOps fe (ConLeche/Kernel/CheckerS.lean:329) is a record of five closures each capturing fe — capture is an owned reference held for the callee's whole lifetime.

Fix (the use-then-consume shape): the rare branch is a pure name test over 16 pinned names, so it is decided before the value check; the common path tail-calls with fe consumed (CheckerS.lean:1252, :1504). Measured: copies 2532 → 297, init-prelude 27.98 G → 27.82 G, and the many scale shape's doubling exponent 1.16/1.27/1.43 → 1.00/1.00/1.01 (at n = 16000, 8.91 G → 4.54 G).