AILang/design/models/0009-explicit-rc.md

# Explicit RC — refcounting as an opt-in, not the floor

**STATUS.** *Design exploration — NOT current state, NOT an approved
milestone.* Nothing here is shipped. The canonical memory model today is
universal reference counting with static uniqueness inference
(`../contracts/0008-memory-model.md`, `0004-rc-uniqueness.md`): every ADT
and closure is RC-heap-allocated, and a uniqueness pass elides inc/dec
where it can prove a reference unique. This whitepaper records a possible
direction — make RC an **authored opt-in** rather than the universal
floor — and isolates the genuinely-open questions in §8. The honesty
rule (`../contracts/0007-honesty-rule.md`) governs the contract ledger,
not this exploratory model; this file exists precisely to fix a future
shape before committing it. If adopted, it revises the floor recorded in
`0004-rc-uniqueness.md` and the codegen contract in
`../contracts/0008-memory-model.md`, and lands as one or more specs under
`../../docs/specs/`.

This is the **runtime-axis dual** of ownership totality
(`0008-ownership-totality.md`). That whitepaper makes the *annotation*
total — every position carries `own`/`borrow`, no `Implicit` — and its
core **shipped** via #55 (spec 0062, commit `76b21c0`, 2026-06-02), so
the precondition this proposal needs is now met, not hypothetical. This
one asks the question that totality, now in place, makes askable: once
ownership is authored on every position, does the *runtime discipline*
still have to be universal RC, or can it follow the annotation — affine
values drop deterministically with no refcount, and RC narrows to the
positions that actually declare sharing? The two compose: 0008 makes
ownership total in the type; 0009 makes the runtime mechanism track the
type. **Nothing in 0009 is built** — universal RC + uniqueness-elision
(§1) is still the floor; what changed is only that 0008 cleared its
runway. One coupling carried over intact: 0009's transitive `box`-drop
(§8 Q3) leans on 0008's return-side escape pass, which 0008 did *not*
ship (borrow-returns are rejected, not verified), so that dependency is
still entirely ahead.

---

## 1. The pain that motivates it

Memory management is the project's dominant maintenance cost. Across the
last ~200 commits, roughly a third touch the RC / ownership / drop
machinery. The notable fact about every leak and refcount bug in that
history is **where it was not**: not one was a defect in the RC runtime
itself (`ailang_rc_alloc`, `inc`, `dec`, free-on-zero — the header-at-`ptr
- 8` layout in `runtime/rc.c` is small and correct). Every bug lived in
the *static inference that decides where to place inc/dec/drop*:

- **#43 A2a** — cross-module ownership modes lost because the uniqueness
  pass ran per-module and missed a type-scoped signature
  (`RawBuf.get`), defaulting a `borrow` argument to `Consume` and
  suppressing a scope-close drop.
- **#43 A2b** — the uniqueness side table is keyed by `(def_name,
  binder_name)`; a shadow-rebind (`let buf … let buf …`) collapsed the
  keys, so codegen read a sibling binding's `consume_count`. The repair
  was a whole desugar alpha-rename pass (`docs/specs/0056`, plan 0111).
- **#47 / #49** — loop-carried owned values (a `RawBuf` accumulator, a
  `Str` threaded through `recur`) leaked because the codegen predicate
  `is_rc_heap_allocated` had no arm for that term shape.
- **`449df13`** — `Subst::apply` silently rebuilt every `Type::Fn` with
  `param_modes: vec![]`, dropping the modes; the typed-MIR drop path
  then could not see ownership and leaked.

The codegen-side complexity map quantifies it: roughly **22
independent conditions** — spread across `uniqueness.rs`,
`linearity.rs` (2149 lines), `escape.rs`, `drop.rs`, `match_lower.rs`,
`lower_to_mir.rs` and the substitution/monomorphisation passes — must
all agree for a single drop to be placed correctly.

The diagnosis is not "RC is slow" or "RC is wrong." It is that **three
memory disciplines run in parallel and the bugs live at their seams**:

1. **Affine ownership** via `own`/`borrow` modes (the Rust-shaped part);
2. **Universal reference counting** underneath *everything*;
3. **A uniqueness inference** that exists only to reconcile (1) with (2)
   — to prove references unique so it can *elide* the RC traffic that
   (2) would otherwise emit.

Discipline (3) is pure overhead in the literal sense: it is machinery
whose entire job is to remove the runtime mechanism of (2) wherever it
can. The corpus is overwhelmingly single-owner functional code — lists,
trees, `RawBuf` fills — so the inference is mostly *succeeding* at
proving uniqueness and stripping the RC. We pay enormous static-analysis
complexity to delete a mechanism we mostly never needed, and the bugs
are in the deletion logic.

## 2. The principle: RC is authored, never universal

0008's principle is "ownership is authored, never defaulted." The dual
on the runtime axis is: **the refcount is authored, never universal.**

A heap value is one of two things, and the author says which:

- **owned / `box`** — a *unique* heap allocation. Exactly one live owner
  at any program point. No refcount. Freed deterministically when the
  owner's lexical scope ends or the owner is moved-and-consumed. This is
  Rust's `Box<T>` — affine, single-owner, drop-at-scope.
- **shared / `rc`** — a *refcounted* heap allocation. Multiple owners
  may coexist; each is created by an explicit, source-visible `share`,
  each contributes one to the count, and the count is decremented at
  each owner's scope-end with free-on-zero. This is Rust's `Rc<T>`.

The default is `box`. `rc` appears only where an author declares genuine
sharing. Refcounting stops being the floor and becomes a *named,
visible, rare* construct — the dual of how 0008 makes `Implicit`
unrepresentable.

This admits no half-application, exactly as totality does not (0008 §2):
a value's heap discipline must be readable from its type, or the trust
break local reasoning forbids has merely moved from "which mode?" to
"counted or not?".

## 3. Why affine drop is sound here without a cycle collector

The move is only legal because AILang has already legislated the
preconditions. `../contracts/0015-language-constraints.md` binds four
constraints — strict evaluation, no recursive value bindings, no shared
mutable refs, ADTs acyclic by construction — whose stated purpose is to
make the reference graph a **DAG**. Today those constraints justify
"RC without a cycle collector." They justify something stronger that the
universal-RC framing leaves on the table:

> A DAG of single-owner values needs no refcount at all. Deterministic
> drop at end-of-owner-scope frees every node exactly once, in
> reverse-construction order, with no count to maintain.

Refcounting earns its keep on exactly one thing: **a node with more than
one owner** (so that no single scope-end may free it). The DAG
constraint plus AILang's *linear-by-default with explicit `clone`*
(`0004-rc-uniqueness.md` §2) already forces every act of sharing to be
written. So the set of values that genuinely need a count is precisely
the set the author already had to mark. Making that set the `rc` set is
not a new burden — it is naming a partition the language already draws.

The cycle question does not reappear: an `rc` value is still acyclic by
construction (constraints 1–4 are unchanged), so no `rc` graph can leak
via a cycle. `rc` buys *sharing*, not *cycles* — the cycle-collector
backstop stays unnecessary for the same reason it is unnecessary today.

## 4. Worked surface

The author-facing surface barely changes; the change is what the
compiler must do underneath. (Form-A keywords `box` / `rc` / `share`
below are illustrative; the real spelling is an open question, §8 Q4,
and should align with 0008 §3.4's adjectival argument — likely `owned`
heap vs `shared` heap.)

### 4.1 The linear majority — no RC at all

```lisp
(data List
  (ctor Nil)
  (ctor Cons (con Int) (box List)))     ; unique tail — affine, refcount-free

(fn map_inc
  (type (fn-type (params (own (box List))) (ret (box List))))
  (params xs)
  (body
    (match xs
      (case (pat-ctor Nil) (term-ctor List Nil))
      (case (pat-ctor Cons h t)
        (term-ctor List Cons (app + h 1) (app map_inc t))))))
```

Count the occurrences of `rc`: zero. For the entire list / tree /
`RawBuf` corpus the author writes `box`, and `box` carries no count. The
inc/dec inference, the `reuse-as` hint, the `over-strict-mode` lint, and
the escape-analysis-to-reclaim-stack all have nothing to do here, because
"this allocation is not shared" is a *type fact*, not an inference
result.

### 4.2 Genuine sharing — the one place `rc` and `share` appear

```lisp
(fn two_views
  (type (fn-type (params (own (rc List))) (ret (con Pair))))
  (params shared_tail)
  (body
    (let a (term-ctor List Cons 1 (share shared_tail))   ; +1 owner, visible
      (let b (term-ctor List Cons 2 (share shared_tail)) ; +1 owner, visible
        (term-ctor Pair MkPair a b)))))                  ; a, b, shared_tail
                                                         ; drop at scope-end → dec
```

Forget a `share` and use `shared_tail` twice and it is a **use-after-move
error on that line** — the affine/linearity check (`linearity.rs`, which
already exists) catches it locally — not a silent leak surfacing three
passes later in codegen. The failure class moves from "the compiler
placed a drop wrong" to "the author did not declare sharing," and the
latter is local and checkable.

### 4.3 In-place mutation: unique-by-type replaces unique-by-inference

`RawBuf` is the language's only mutation, and the case where explicit
ownership pays the most. Its `set` is `own RawBuf → own RawBuf` and its
doc states the current semantics exactly:

> *Under uniqueness in-place; under shared copy-on-write (Issue #22).*

i.e. whether a write reuses the slab or copies is decided by the
uniqueness *inference* — the fragile part (A2a, A2b, the loop arm). With
`box`:

```lisp
(fn set                                                  ; HYPOTHETICAL
  (type (forall (vars a)
    (fn-type (params (box (con RawBuf a)) (own (con Int)) (own a))
             (ret (box (con RawBuf a))))))
  (params b i v) (intrinsic))
```

A `box` is unique *by type*, so the write is in-place **unconditionally**
— no proof, no copy-on-write branch, no refcount check at the write site.
There is no shared case for a `box`; an author who wanted sharing wrote
`rc`, and `set` on an `rc` is a type error ("cannot mutate a shared
buffer") rather than a silent COW branch.

**This is consume-and-return, not mutable aliasing.** `set` *consumes*
its buffer (a move); the old binding is dead afterward and never
observable, so semantically a new value is produced and "immutable once
constructed" (constraint 3) holds for every individual value — the
in-place slab reuse is an optimisation under the hood, never a
language-visible write through a live alias. A `&mut`-style mutable-borrow
mode is therefore **out of scope by principle, not preference**: a mutable
borrow *is* a mutable alias, which constraint 3 forbids, and it is the one
genuinely hard part of Rust's borrow checker (aliased-mutation policing)
that AILang's identity removes the pressure for. In-place update rides
*uniqueness/linearity* (now: *type*), exactly as 0008 §8 records, not
exclusive borrows.

The shadow-rebind idiom (`let buf … let buf …`) may stay verbatim, and
A2b still cannot recur — not because the rebind is gone, but because there
is **no uniqueness side table to collapse**. Codegen reads no per-name
`consume_count` to decide in-place vs. drop; drop is placed at the
lexical scope of the move-checked binding. The alpha-rename pass `C′`
(spec 0056) was load-bearing only for disambiguating side-table keys;
absent the side table it is at most optional scoping hygiene.

## 5. What this removes from the compiler, and what stays

**Removed** — from author code *and* from the compiler:

- The **uniqueness-elision inference** (`uniqueness.rs`'s `consume_count`
  dataflow) — its entire job was to strip universal RC; with no universal
  RC there is nothing to strip. A `box` is non-shared by type; an `rc` is
  counted by type.
- The **`is_rc_heap_allocated` term-shape predicate** with its
  Ctor/Lam/Own-App/Loop arms — the thing that kept missing cases (#47).
  "Does this need a drop?" becomes a *type* question (`box`/`rc`), total
  and arm-free, not a term-shape guess.
- The **`over-strict-mode` lint** and its `suppress` mechanism — there is
  no over-strict `own` to warn about once `box` carries no count.
- **`reuse-as`** as a distinct hint — a unique `box` is reusable in place
  because it is the sole owner; reuse is a property of the owner, not an
  author annotation the inference must verify.
- The **escape-analysis-to-reclaim-stack** pass (`escape.rs`) — an owned
  `box` already *is* "not shared," so stack-promotion of non-escaping
  allocations is a plain liveness question, not a clawback from a
  universal-RC default.

**Kept** (and made more prominent):

- The **affine / linearity check** (`linearity.rs`) — use-after-move,
  consume-while-borrowed. This is the load-bearing safety pass and it
  already exists; it becomes *the* mechanism rather than a diagnostic
  layered over an inference.
- **`own` / `borrow`** — unchanged, call-scoped, no lifetime variables
  (0008 §8).
- **`clone` / `share`** — but now type-distinguished: `share` on an `rc`
  is a cheap inc; "clone" of a `box` is a genuine copy. The two meanings
  the single `Term::Clone` conflates today are split by the type.

The net is **fewer moving parts than today**, not more: the borrow check
stays (we pay it already), and the universal-RC + elision-inference +
escape-clawback triad collapses into one type-directed rule.

## 6. Relation to ownership totality (0008) and to Rust

0008 and this whitepaper are two cuts of the same object and are most
coherent adopted together:

| Axis | 0008 (totality) | 0009 (explicit RC) |
|---|---|---|
| What it totalises | the *annotation* (`own`/`borrow` everywhere) | the *runtime discipline* (counted vs. affine) |
| Removes | `Implicit` default | universal-RC default |
| Default | `own` (trivially true on value types) | `box` (affine, no count) |
| The opt-in | `borrow` (a lent view) | `rc` (a shared, counted value) |
| Soundness pass | return-provenance / escape (0008 §5.2) | the same affine check, now load-bearing |

0008 §5.1 already takes **regime A** — borrows may not escape into an
escaping heap structure; a field of a returned box is necessarily owned.
That decision is exactly what makes `box` drop transitively sound here:
under regime A, dropping an owned box recursively frees owned children
with no borrowed member to mis-free. The two designs share one
substrate.

This is **not** a rebuild of Rust, for the reasons 0008 §8 already lays
out and this proposal sharpens: no lifetime variables (point-free is
cut, §4.4 there), no `&mut` / shared-XOR-mutable (§4.3 here, constraint
3), no elision (totality is the opposite of Rust's lifetime elision).
What this adds to 0008 is the one further Rust correspondence 0008 left
implicit: `box` ≈ `Box`, `rc` ≈ `Rc`, and **the default is `Box`, not
`Rc`** — which is the entire point. Today AILang's default is
effectively `Rc` everywhere with a pass trying to downgrade it to `Box`;
the proposal flips the default to `Box` and makes `Rc` the marked case,
which is both what Rust does and what the corpus's actual sharing
profile wants.

## 7. Feature-acceptance check

`../contracts/0004-feature-acceptance.md`: a feature ships only if an LLM
author reaches for it unprompted *and* it measurably improves
correctness or removes redundancy.

- **Reached for unprompted.** The `Box`/`Rc` distinction is core Rust
  vocabulary; an LLM author trained on Rust produces `Box` for unique
  ownership and `Rc` only for sharing without prompting. The construct is
  LLM-native in the strongest sense — it is what the model already
  expects, and the *current* implicit-universal-RC model is the surprise.
- **Correctness.** It deletes the inference layer that produced ~⅓ of
  recent commits and the three named leak clusters; "is this shared?"
  becomes a checked type fact rather than a dataflow result codegen
  re-reads out of band.
- **Redundancy.** It removes universal refcount traffic (inc/dec the
  uniqueness pass mostly elides anyway) and the `reuse-as` /
  `over-strict` / escape-clawback machinery that exists to claw back what
  universal RC over-charges.

Both clauses are met. The cost (below) is real but is implementation
effort and one irreversible hash reset, not a design objection — and per
the design-rationale rule effort is at most a tiebreaker.

## 8. Costs, consequences, open questions

Named honestly:

- **Memory-model swap + hash reset.** This revises the canonical floor
  (`0004-rc-uniqueness.md`) and the codegen contract
  (`../contracts/0008-memory-model.md`). As in 0008 §6, removing a
  serialisation default (here: the RC-everywhere assumption baked into
  layout and drop emission) shifts module hashes once across the corpus
  and resets every hash-pin test. This is the one genuinely irreversible
  step and the one to sign off on deliberately. The hash-pin blast radius
  spans every `crates/*/tests/` hash-pin file, not only the AST-home
  crate.

- **Closures are the hard case.** A closure captures an environment;
  capture-by-move (`box`) vs. capture-by-share (`rc`) is a real authored
  decision, and the capture set is where single-ownership is least
  obvious. Today captures are conservatively `Consume`
  (`uniqueness.rs`, "Lam captures are conservatively Consume" —
  unsound-but-safe). The explicit model must make `move`/`share` on
  captures authored and checked. This is the closure-chain benchmark
  that already measures widest against the RC target
  (`0004-rc-uniqueness.md`). **Open (Q1):** what does the capture surface
  look like, and does the affine check cover capture-by-move without new
  machinery?

- **`clone` semantics split.** `Term::Clone` today is "RC inc." Under the
  split, `share` on an `rc` is the inc; cloning a `box` is a genuine
  (structural) copy. **Open (Q2):** is a structural deep-copy of a `box`
  a primitive, or is it only ever "promote to `rc` then `share`"? The
  latter keeps one sharing mechanism; the former allows owned duplication
  without ever introducing a count.

- **Coupling to 0008's return-side pass.** 0008 §5.2 shows that for a
  *compound* `box` return, the flat ownership claim is sound only if a
  reachability pass proves nothing borrowed is reachable. That pass is
  the same one this proposal relies on for transitive `box` drop. **Open
  (Q3):** does `box`-drop soundness require 0008's escape analysis to
  land first, making 0009 strictly downstream of 0008's verification
  axis? (Working hypothesis: yes for compound returns; scalar `box`
  drop is independent.)

- **Keyword spelling.** **Open (Q4):** `box`/`rc`/`share` vs. the
  adjectival `owned`/`shared` that 0008 §3.4 argues for on
  position-neutrality grounds. The choice should land *before* the hash
  reset, since renaming a keyword post-cutover is a second irreversible
  step (0008 §7 Q3 makes the identical argument for `own`/`borrow`).

- **Sharing-heavy workloads.** The proposal bets the corpus is
  overwhelmingly single-owner. **Open (Q5):** is there a real workload
  class (memoised DAGs, hash-consed terms, shared dictionaries) where
  `rc` would be pervasive rather than rare? If so, the ergonomics of
  pervasive `share` need a second look — though even then the
  *correctness* argument (sharing is checked, not inferred) stands.

**Resolved by the shape above** (not open): the default is `box`, not
`rc` (§2); affine drop is sound under the existing DAG constraints (§3);
no `&mut` / mutable-borrow mode, in-place rides consume-and-return (§4.3);
the uniqueness-elision inference, `is_rc_heap_allocated`, `over-strict`,
`reuse-as`, and escape-clawback are removed, the affine check stays (§5).

---

*Cross-references:* ownership totality (the annotation-axis dual)
`0008-ownership-totality.md`; current memory model
`../contracts/0008-memory-model.md`; RC + uniqueness floor this revises
`0004-rc-uniqueness.md`; the language constraints that make affine drop
sound `../contracts/0015-language-constraints.md`; feature-acceptance
gate `../contracts/0004-feature-acceptance.md`.