AILang/design/models/rc-uniqueness.md

# RC + Uniqueness — memory model whitepaper

## Per-fn arena via stack `alloca`

This optimisation is layered on top of the canonical RC runtime.
`ailang-codegen` runs an escape-analysis pre-pass over every fn
body (and every lifted lambda thunk body); allocations the pass
proves do not outlive the fn frame are lowered to LLVM `alloca`
instead of the runtime allocator. Allocations that may escape
continue to use the runtime allocator. The runtime is unaffected;
escape analysis is purely an optimisation above the floor.

**Allocation mechanism: LLVM `alloca`** (not a heap arena). Stack
allocation matches the "freed at fn return" lifetime exactly,
needs no malloc/free pair, and integrates with LLVM's existing
optimiser (mem2reg / SROA may further promote the alloca'd box
to registers if the box is small and its uses are simple). No
new runtime is introduced; no language-level change; no AST or
schema change.

**Escape rule (conservative).** A `Term::Ctor` or `Term::Lam`
allocation is non-escaping iff (1) it is the value of a
`Term::Let { name = X, value = ALLOC, body = B }`, and (2) the
body `B` does not let any value derived from `X` flow past the
fn frame. "Derived from" follows two propagation rules:
- A `Term::Match` whose scrutinee is a `Var` referring to a
  tainted name propagates taint to every pattern-bound name in
  every arm. (Pattern bindings hold field projections of the
  scrutinee, which live inside the same allocation.)
- A `Term::Let { name = Y, value = Var(t), ... }` where `t` is
  tainted makes `Y` tainted in the let's body.

A tainted name "escapes" if it appears in any of: the tail
position of `B`, the arg list of any `Term::App` / `Term::Do`,
the field list of a `Term::Ctor`, or the free-var capture set of
a `Term::Lam`. The closure-pair-callee position of `Term::App`
where the callee is a bare `Var` to the tainted name is NOT an
escape (calling locally is fine).

**What this is not.** Not a region-inference system. Not
flow-sensitive within an arm. Not field-sensitive (pattern
bindings are tainted wholesale). Precision can be improved later;
correctness is the priority for this iter. A pessimistic answer
(claiming an allocation escapes when it does not) only loses
optimisation, never correctness.

**Codegen integration.** Three sites in
`ailang-codegen/src/lib.rs`:
- `lower_ctor` — ADT box.
- `lower_lambda` env block (when there are captures).
- `lower_lambda` closure pair (always 16 bytes).

Each site queries the per-fn `non_escape: BTreeSet<usize>` (raw
pointer addresses of `Term::Ctor` / `Term::Lam` AST nodes flagged
as non-escaping). On a hit the emitter writes
`alloca i8, i64 <size>, align 8`; on a miss it writes
`call ptr @ailang_rc_alloc(i64 <size>)` (or the bump-mode
equivalent). The rest of the lowering (tag store, field stores,
closure-pair packing) is identical.

The closure-pair and its env share an escape verdict — they have
parallel lifetimes. If the closure pair is non-escaping, the env
is too.

## Memory model — RC + Uniqueness with LLM-author annotations

**AILang commits to reference counting with static uniqueness
inference as the canonical memory model, extended with mandatory
LLM-author mode annotations (`borrow` / `own`), explicit `clone`,
first-class `reuse-as`, and `drop-iterative` data attrs.**

RC's costs are bounded and analysable per program point; the
canonical position is "RC + inference" sharpened with the five
LLM-author mechanisms below. A corpus committed to one memory
model is expensive to switch — the commitment lives in the
contracts ([memory-model](../contracts/memory-model.md),
[language-constraints](../contracts/language-constraints.md)).

**Choice.** AILang's canonical [memory model](../contracts/memory-model.md)
is reference counting with static uniqueness inference **and
explicit LLM-author annotations on fn signatures**, in the lineage
of Lean 4 / Roc / Koka. The RC pipeline tracks the bump-allocator
raw-alloc floor: a bench-health regression gate requires RC overhead
≤ 1.3× bump on the linear/tree corpus, with a wider ±15% band on
the closure-chain corpus (representational cost of the closure-pair
layout). See `bench/run.sh` for the active check.

**Workload scope of the 1.3× target.** The 1.3× target was
calibrated on the original `bench/run.sh` corpus: linear list
sum (`bench_list_sum`) and tree walk (`bench_tree_walk`) — uniform
single-allocation-per-step workloads where one inc/dec pair
amortises against one allocation. The corpus was later extended
with `bench_closure_chain` (closure-pair allocation: each step
allocates *two* heap objects, the closure cell and its captured
env struct) and `bench_hof_pipeline` (poly-ADT + indirect
dispatch). The closure-chain fixture measures wider than the 1.3×
linear/tree target: each step pays two allocs and two decs against
one bump-pointer bump, doubling the allocation tax on closure
construction (current ratio recorded in
`bench/orchestrator-stats/` and the bench iter commit bodies).
This is a representational cost of the closure-pair layout,
not a defect in the RC implementation; a future closure-pair
slab/pool optimisation for fixed-shape pair cells would compress
this ratio without changing semantics.

The 1.3× bench-health regression gate therefore applies to the
linear / tree / poly-ADT subset of the corpus. Closure-heavy
workloads are tracked under a wider band (the closure-chain
baseline records its rc/bump ratio as the `rc_over_bump`
reference value with ±15% tolerance) and are excluded from the
linear/tree 1.3× regression gate; the closure-chain corpus has
its own ±15% band until a slab/pool optimisation ships. The
[memory model](../contracts/memory-model.md)'s RC commitment is
unchanged; what is scoped is the *quantitative* regression band,
not the choice of memory model.

The architecture has two layers:

1. **Inference.** A post-typecheck pass produces a per-node
   uniqueness side table. Codegen uses it to elide inc/dec
   wherever provably redundant.
2. **LLM-author annotations.** Fn signatures carry mandatory
   `(borrow T)` / `(own T)` mode markers. Authors mark
   sharing-vs-consumption explicitly. The compiler verifies
   rather than guesses.

The combination plays to what LLMs are good at (writing slightly
more annotation per definition) and avoids what compilers are
bad at (proving sharing absent in the face of recursion +
closures + match).

## The LLM-aware sharpening

A mainstream RC implementation (think Lean 4 in default mode)
infers everything from naked AST plus a few optional hints. The
inference is conservative; whatever it can't prove unique becomes
shared and pays runtime inc/dec. AILang exploits its target
audience to push that conservative ceiling higher.

Five mechanisms.

**(1) Mandatory `(borrow T)` / `(own T)` on fn signatures.**

```
(fn list_length
  (type (fn-type (params (borrow (List Int))) (ret (con Int))))
  ...)

(fn sum_list_consume
  (type (fn-type (params (own (List Int))) (ret (con Int))))
  ...)
```

`(borrow T)` declares the parameter is read-only and lives at
most until the call returns; the caller still owns it; the
callee performs no inc/dec on it. `(own T)` declares ownership
transfer; the callee consumes the value and is responsible for
its end-of-life. The declaration is structural (visible in JSON)
and binding (the typechecker rejects bodies that contradict it).

For a Lean 4 / Roc author this is all *optional* and inferred
when omitted. AILang makes it mandatory because the LLM author
can carry the cognitive cost trivially, and the compiler gains a
precise contract at every call site instead of a probabilistic
guess.

**(2) Linear-by-default consumption with explicit `(clone X)`**
(the `Term::Clone` schema entry lives in
[Data model](../contracts/data-model.md)).

In bodies, every binder is consumed by exactly one `own`-mode
use. If the LLM writes:

```
(let p (expensive_fn x)
  (let r1 (consume_a p)        ; consume_a takes (own); consumes p
    (let r2 (consume_b p)      ; ERROR: p already consumed
      ...)))
```

the compiler emits a structured non-linear-use diagnostic with
concrete `suggested_rewrites`:

- "make consume_a borrow": refactor consume_a's signature, no
  body change at the call site;
- "explicit clone": insert `(clone p)` at the first use;
- "fuse traversal": replace the two separate calls with a fused fn.

The LLM picks one. There is no implicit clone — sharing always
costs visible source.

**(3) Reuse hints as first-class.**

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

`(reuse-as SRC NEW-CTOR)` asks the codegen to allocate `NEW-CTOR`
in `SRC`'s memory slot. Compiler verifies: `SRC` is owned, this
is its last use, sizes match. On a hit: no malloc, no free — the
box is overwritten in place. On a miss: structured diagnostic
explains which precondition failed; the LLM either adjusts the
surrounding code or removes the hint.

This matches Lean 4 / Roc reuse analysis but lifts it from
"compiler-inferred when possible" to "author-asserted, compiler-
verified". The LLM applies it everywhere it expects to fire and
lets the compiler bounce the request when it can't.

**(4) `(drop-iterative)` annotation on data declarations.**

```
(data Tree (vars a)
  (ctor Leaf)
  (ctor Node a (Tree a) (Tree a))
  (drop-iterative))
```

When the refcount of a `Tree` value reaches zero, the synthesised
dec-on-zero traversal is iterative (worklist + heap-allocated
stack) instead of recursive. Avoids stack overflow on deep
structures. The LLM adds the annotation where appropriate; the
compiler refuses to emit recursive dec-cascade on annotated types.

**(5) Structured compiler diagnostics with `suggested_rewrites`.**

Every RC-mode error (use-after-consume, mode-mismatch,
reuse-as-fail, drop-cascade-too-deep) emits a JSON object
containing the failure kind, the source span, and a list of
concrete rewrite suggestions in form-A AILang. The LLM consumes
these without prose-parsing. This is the missing half of the
LLM-as-author story: the language spec defines not only what
compiles, but what the compiler tells the author when it doesn't.

## Inference algorithm

Post-typecheck, post-`lift_letrecs` (see [pipeline](pipeline.md)),
pre-codegen pass over the elaborated module. For each `Term` node that produces or binds a
boxed value, the pass computes a uniqueness flag:

- **Unique:** at this program point, the reference is the only
  outstanding reference to its referent.
- **Shared:** there may be multiple outstanding references.

A reference is *unique* if every path from its allocation to the
current program point passes through exactly one binding. The
inference is a forward dataflow over the AST. The annotations
(`borrow` / `own`) provide the inter-fn contract; the
inference fills in intra-fn detail.