AILang/design/contracts/0008-memory-model.md

# Memory model — schema, diagnostics, codegen contract

The four language-design constraints that make RC sound without a
cycle-collector backstop (strict evaluation, no recursive value
bindings, no shared mutable refs, acyclic ADTs) live in
[language constraints](0015-language-constraints.md); this file covers
the schema additions, advisory diagnostics, and codegen contract
that build on them.

## Schema additions

**Parameter modes on `Type::Fn`** (see [Data model](0002-data-model.md)
for the schema-level definition of `Type::Fn`).

The form-A surface (see [authoring surface](0001-authoring-surface.md))
for fn signatures gains mode wrappers:

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

Internally, this is *not* a new `Type` variant. Modes are
metadata on `Type::Fn` — `paramModes` and `retMode` fields run
parallel to `params` and `ret` (see [Data model](0002-data-model.md) for the JSON
schema). The substantive reasons for per-position metadata over a
`Type::Borrow` / `Type::Own` variant approach:

- **Semantic locality.** Modes are properties of fn-signature
  parameter positions, not of types in general. `Int` does not
  have a mode; a fn-parameter slot does. Embedding modes in
  `Type` would let the schema express forms like
  `(con List (borrow Int))` — syntactically possible, semantically
  meaningless (you cannot separately own/borrow a list element
  from the list it lives in). The
  [canonical-schema principle](0002-data-model.md) is "schema = data,
  schema permits exactly what is meaningful"; per-position
  metadata is the option that holds that line.
- **Compositional clarity.** A `Type` value's identity should
  depend only on the type. Two functions with the same param /
  ret types but different calling conventions share `Type::Fn.params`
  and differ only in `param_modes`. That is the right factoring:
  "what data does this carry" is one axis, "how is it transferred"
  is another. Mixing them under a single hierarchy conflates the
  two and makes both harder to reason about.
- **Future-proof against more position metadata.** If later iters
  add other per-position properties (streaming receiver, captured-
  by-closure, lifetime witness), they generalise as additional
  metadata fields on `Type::Fn` — one consistent hierarchy. The
  variant approach would force every new dimension into its own
  `Type::*` variant (`Type::Streamed`, `Type::Captured`, ...) and
  combinatorics blow up: `Type::Borrow(Type::Streamed(T))` versus
  `Type::Streamed(Type::Borrow(T))` raise questions of canonical
  ordering that don't exist when modes live in a flat metadata
  vector.

`Own` and `Borrow` are the two modes; every fn-type slot carries
one explicitly. Ownership has no default — there is no
bare/unannotated mode.

JSON canonical form: `param_modes` and `ret_mode` are always
present, one mode per slot, with no elision — the mode vectors
are never omitted from the canonical bytes.

**Type::Con name scoping (canonical form).** Within a
`.ail.json`, a `Type::Con.name` is interpreted relative to the
file's top-level `"name"` field (the owning module). Bare names
(no `.`) refer to a TypeDef in the owning module's own `defs`.
Cross-module references MUST be qualified `<owning_module>.<TypeName>`
where `<owning_module>` is a known module in the workspace.
Primitives (`Int`, `Bool`, `Str`, `Unit`, `Float`) are bare and
have no module qualifier. Bare cross-module references are a
schema violation (`WorkspaceLoadError::BareCrossModuleTypeRef`);
qualified references whose owner is unknown are also a violation
(`WorkspaceLoadError::BadCrossModuleTypeRef`). The same rule
applies to `Term::Ctor.type_name`.

Class names follow the same canonical-form rule: bare for
same-module references, `<module>.<Class>` for cross-module
references — symmetric to `Type::Con.name`'s rule above.
Three schema fields carry class references in this form:
`InstanceDef.class`, `Constraint.class`, and `SuperclassRef.class`.
`ClassDef.name` itself stays bare (defining-site context, like
`TypeDef.name`).

Method dispatch is type-driven (see
[Method dispatch](0016-method-dispatch.md)):
synth resolves a `Term::Var { name: "show" }` by consulting
the workspace's method-to-candidate-class index, filtering by
argument type (concrete) or by declared constraint (rigid-var), and
routing the residual through the registry at fn-body-end discharge.
Method-name collisions across classes are now structurally legal —
they resolve at the call site via type-driven dispatch with explicit
qualifier (`<module>.<Class>.<method>`) as the LLM-author's
disambiguation tool.

The legacy `(con T)` form is treated as `(own T)` semantically.

(An incidental observation, not a design reason: keeping `Type`
itself unchanged also avoids touching ~250 sites across the
typechecker / desugar / codegen that match on `Type` variants.
This is a tiebreaker, not a rationale — the substantive reasons
above are what justify the choice.)

**New `Term` variants.**

```
Term::Clone { value: Box<Term> }                     ; `(clone X)` — explicit RC inc
Term::ReuseAs { source: Box<Term>, body: Box<Term> } ; `(reuse-as SRC NEW-CTOR)`
```

`Term::ReuseAs` is structured as a *wrapper* around a `body`
term rather than as a `reuse_from: Option<String>` modifier on
`Term::Ctor`. Two substantive reasons:

1. **Compositional flexibility.** Reuse-as is conceptually a
   wrapper that says "this expression's allocation comes from
   `<source>`'s slot". The wrapper form generalises naturally
   if future iters introduce other allocating constructs
   (record literals, opaque box wrappers, capability cells) —
   they all become valid `body` positions. A modifier on
   `Term::Ctor` would have to be replicated on every
   constructible Term variant the language grows.
2. **Source-locality at the head.** `(reuse-as SRC NEW-CTOR)`
   reads as a single sentence with the source-binder named at
   the head. The modifier form would scatter the reuse intent
   across a child position of the constructor's argument
   syntax, separating the `source` from the rest of the
   reuse-as semantics.

The trade-off this accepts: the schema permits `Term::ReuseAs
{ body }` where `body` is not an allocating form (e.g. a
literal, a var). Such terms are caught at typecheck via a
`reuse-as-non-allocating-body` diagnostic — structural rejection
in the typechecker, not the schema. The principle: prefer
composability over schema-level rejection where the typecheck
rule is unambiguous.

**`TypeDef` attribute.**

```
TypeDef.drop_iterative: bool                         ; `(drop-iterative)`
```

All four are skipped during serialisation when absent / false /
None so canonical-JSON hashes of every fixture remain stable
until the fixture intentionally adopts the feature.

**`FnDef.suppress`.** The `suppress` field on `FnDef` carries a
list of advisory-diagnostic suppress entries; each entry has a
`code` (the diagnostic being suppressed) and a `because` (a
mandatory non-empty reason). See [Data model](0002-data-model.md) for
the canonical schema.

Form-A surface: `(suppress (code "...") (because "..."))` clause
between fn name and `(type ...)`. Multiple clauses allowed; one
per entry. Form-B (prose) renders one
`// @suppress <code>: <because>` line per entry above the doc
string — lossless, contract metadata.

Skipped from serialisation when empty so existing fixtures keep
bit-identical canonical-JSON hashes (regression-pinned by
`iter19b_empty_suppress_preserves_pre_19b_hashes` and
`iter19b_schema_extension_preserves_pre_19b_hashes`).
Two cross-module fixtures (`ordering_match.ail.json` and
`test_22b1_dup_a.ail.json`) carry canonical-form `Type::Con.name`
hashes, pinned by `ct4_migrated_fixtures_have_canonical_form_hashes`;
all intra-module fixtures, including `sum.ail.json` and
`list.ail.json`, are pinned bit-identical by
`ct4_unmigrated_fixtures_remain_bit_identical`.

## Advisory diagnostics

The advisory-diagnostics arc introduces the language's first
**advisory** typechecker diagnostic and the suppression mechanism
that goes with it. The mandatory-annotation rule of this memory
model is unchanged: `param_modes` and `ret_mode` remain
author-required; the typechecker does not infer them. What's new
is feedback when an authored annotation is *stricter than necessary*.

**The lint: `over-strict-mode`.** Fires on a
fn-param `p` annotated `(own T)` when:

  1. `p`'s `consume_count == 0` (uniqueness pass: the body
     never consumes `p` as a whole).
  2. For every match arm whose scrutinee is `p`, no
     **heap-typed** pattern-binder has `consume_count > 0`.
  3. `p`'s type `T` is **not** a value type
     (`Int`/`Bool`/`Float`/`Unit`).
  4. The enclosing fn's body is **not** `(intrinsic)`.

The heap-type filter is load-bearing for soundness:
`match xs { Cons(h, t) => h }` records `consume_count(h) == 1`,
but `h: Int` is read by-value — no RC traffic, no heap data
moved out of `xs`'s allocation. Filtering primitive-typed
binders is what lets the lint correctly identify `head_or_zero`
as over-strict (could be `borrow`) while staying silent on
`sum_list` where `t: List` *is* moved out.

Conditions 3 and 4 keep the lint coherent under universal mode
activation:

- **Value-typed params never fire.** `(borrow V)` for a value
  type `V` is itself rejected by the `borrow-over-value` check,
  so `(own V)` is the only legal mode for a value-typed param.
  A suggestion to relax `(own Int)` to `(borrow Int)` would point
  at an illegal rewrite, so the lint stays silent on value-typed
  params regardless of whether they are consumed.
- **`(intrinsic)`-bodied fns never fire.** The linearity walk
  does nothing for a `Term::Intrinsic` body, so every param of an
  intrinsic has `consume_count == 0` — a guaranteed false positive.
  An intrinsic's param modes are hand-authored contracts
  (`new`/`get`/`set`/`float_*`), not lint-derivable from a walkable
  body, so the whole fn is skipped.

Severity: `Warning`. `ail check`, `ail build`, `ail emit-ir` exit 1
only on at least one `Error`; warnings print but do not abort.

**The suppression: `mode-strict-because`.** Authors
who want to keep an over-strict annotation deliberately (e.g.
RC codegen-test fixtures, fns reserved for planned in-place
mutation) attach a `Suppress` entry naming the diagnostic code
and a non-empty reason. The typechecker drops matching
diagnostics from the output. Empty `because` is a hard error
(`empty-suppress-reason`); wrong-code suppresses are silent
no-ops (open-set diagnostic registry — a suppress for a code
that doesn't fire today may exist defensively for a code that
might fire after a future edit).

## Codegen contract

Memory layout:

- Every heap allocation has an 8-byte refcount header, followed
  by the payload. `ailang_rc_alloc(size)` returns a pointer to
  the *payload*; the header is at `ptr - 8`.
- `ailang_rc_inc(ptr)`: load `ptr - 8`, +1, store. Non-atomic
  (single-threaded).
- `ailang_rc_dec(ptr)`: load, -1, store; if zero, recurse-dec
  child references and `free(ptr - 8)`. For `(drop-iterative)`
  types, the recursion is replaced by a worklist loop (via `drop-iterative`).

Codegen for `Term::Ctor` / `Term::Lam` env / closure pair under
`--alloc=rc` calls `ailang_rc_alloc(SIZE)`; inc/dec instrumentation
is emitted per the uniqueness inference. `--alloc=bump` selects the
bench-floor allocator, which leaks by design (no inc/dec, no free);
it is bench-only and never a production target.

## Mode metadata is load-bearing for codegen

`param_modes` and `ret_mode` on `Type::Fn` are not merely
typechecker metadata — codegen consults both to decide where to
emit drop calls:

**`param_modes` — drop-emission gates.**

- **Own-param dec at fn return.** When a fn body
  fall-throughs to a `ret` (no tail-call), every parameter with
  `param_modes[i] == Own` is dec'd before the `ret` iff its
  uniqueness `consume_count == 0` and the ret value is not the
  param itself. `Borrow` parameters are skipped: `Borrow` retains
  the caller's ownership by contract. (There is no `Implicit`
  parameter any longer — every param is `Own` or `Borrow`.)

- **Arm-close pattern-binder dec.** When a match-arm's
  body terminates without a tail-call, every ptr-typed
  pattern-bound binder pushed by the arm is dec'd at arm close
  iff its `consume_count == 0` and it is not the arm's tail
  value, **gated on the scrutinee's static ownership**. If the
  scrutinee is a fn-param, only `Own`-mode scrutinees enable
  the dec — a `Borrow` scrutinee would let the arm dec memory
  the caller still references.

- **Pre-tail-call shallow-dec.** When a match-arm's
  body IS a tail call, both the own-param dec and the arm-close
  pattern-binder dec are skipped (the block is terminated). A separate seam in `lower_match` emits
  a shallow `ailang_rc_dec` on the scrutinee outer cell BEFORE
  the tail call, gated identically on the scrutinee mode plus
  the requirement that every ptr-typed slot in the active
  ctor's pattern is in `moved_slots[scrutinee]`.

- **Leak-class branch-param drop.** When a `match`-arm or
  `if`-branch falls through (no tail-call) and an `Own`, ptr-typed
  parameter is LIVE on that branch (its per-branch consume is `0`)
  but CONSUMED on a sibling branch (per-fn aggregate
  `consume_count >= 1`), it is dec'd at that branch's close, before
  the `br` to the join — never at the join, which is a merge point
  that cannot tell the consumed path from the live one. Three guards
  make this sound:
  - *Disjointness from the fn-return dec.* The fn-return Own-param
    dec above owns the `aggregate == 0` class (live on every path);
    this gate owns the `aggregate >= 1` class. The predicates are
    mutually exclusive, so no param is dropped twice — the fn-return
    dec is left unchanged and no tail-position analysis is required.
  - *No use-after-free.* An `aggregate >= 1` param is provably dead
    past the branch construct: the checker rejects use-after-consume
    (`use-after-consume`), so a param consumed on any branch cannot
    be used afterwards. The per-branch drop is therefore
    path-terminal regardless of whether the construct sits in tail
    position.
  - *Heap-RC-ADT type precondition.* The drop fires only for a param
    whose static type resolves to a real per-type heap drop fn
    (`field_drop_call != "ailang_rc_dec"`). Closure (`Type::Fn`),
    static-`Str`, and `Type::Var` params route to the bare
    `ailang_rc_dec`, which would underflow on a static closure-pair /
    static-`Str` constant (`.rodata`, no rc-header); they are
    skipped. A heap-capturing closure in this exact position leaks
    rather than double-frees — soundness is preferred over
    completeness (tracked in the backlog).

  The pre-tail-call Own-param dec (the drop of an `Own` param a
  tail-call arm neither forwards nor consumes) shares this
  per-branch model: its gate-source is the per-arm `consume_count`
  (`MArm.consume`), which for an `aggregate == 0` param is identical
  to the old aggregate gate.

**Per-fn binder-name injectivity (a precondition of every gate
above).** Every drop gate reads `consume_count` from the uniqueness
side-table keyed by `(def_name, binder_name)`; the two per-branch
gates (leak-class drop, pre-tail-call Own-param dec) additionally read
the per-branch consume map carried on `MArm.consume` /
`MTerm::If.{then,else}_consume`, correlated to the MIR branch nodes by
a traversal-order lock-step cursor in `lower_to_mir` (the AST carries
no node id). Codegen looks up by the binder's source name and must
resolve the binding it means — so within one `def_name`, every
`binder_name` must denote exactly one binding. The desugar pass guarantees this: it
alpha-renames any binder whose name shadows an enclosing binding to a
fresh `<name>$<n>` (`ailang-core::desugar`), so a shadow-rebind idiom
like `(let buf (new…) (let buf (set buf…) … (get buf)))` becomes
`buf, buf$1, buf$2, buf$3`. Without this, shadowed binders collapse
onto one key and a gate reads a sibling binding's `consume_count`,
suppressing or doubling a drop. Ratified by
`raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats` and
`flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed` in
`crates/ail/tests/e2e.rs`, and the desugar unit test
`shadowing_let_is_alpha_renamed`.

**`ret_mode` — let-binder trackability.**

- **`Term::App` drop at let-scope close.** A
  let-binder whose value is `Term::App { callee, .. }` is
  trackable for scope-close drop iff the callee's
  `ret_mode == Own`. The signal is the callee's static
  contract that ownership of the freshly heap-allocated cell
  flows to the caller. Every `Term::App` callee now carries an
  explicit `Own`/`Borrow` `ret_mode`; an `Own`-returning call is
  trackable for scope-close drop, a `Borrow`-returning call is
  not (the callee retains ownership; the caller holds a view,
  not an own ref — and a borrow-return is in any case rejected
  at the signature, spec 0062).

The drop fn's symbol resolution for an Own-returning App:
synthesise the call's return type, resolve `Type::Con { name }`
to `drop_<owner>_<T>` (with cross-module qualification through
the import map). Falls back to shallow `ailang_rc_dec` for
returns that are not `Type::Con` (e.g. unresolved type vars on
a polymorphic call's pre-monomorphisation site; the
monomorphised copies resolve to concrete drop fns).

#### Per-monomorph drop fns for polymorphic ADTs

A polymorphic ADT (`Box a`, `Pair a b`) has no single correct
drop fn: a ctor field typed at a type-var lowers to `ptr` and is
`rc_dec`'d, but at a value-type instantiation (`Box Int`) that
field is an inline `i64`, so dec'ing it dereferences a scalar.
Codegen therefore emits **one drop fn per (polymorphic-ADT,
concrete instantiation)** and makes the dec-vs-skip decision on
the *substituted* field type: a value-type field
(`Int`/`Bool`/`Float`/`Unit`) is skipped (inline scalar, no RC);
a heap field is dec'd through its own per-monomorph drop symbol
so the cascade composes.

The workspace-global collection lives in
`crates/ailang-codegen/src/dropmono.rs` (`collect_drop_monos`,
`DropAdtMeta`), built once before the per-module codegen loop and
shared by reference with every `Emitter`. Symbol naming:

- A concrete-monomorphic ADT (declared `vars` empty: `IntList`,
  `Ordering`) keeps its un-suffixed `drop_<m>_<T>` /
  `partial_drop_<m>_<T>` symbol byte-for-byte (the `ir_snapshot`
  goldens pin these).
- A polymorphic ADT instantiation gets a mono suffix mangled
  exactly as `ailang_check::mono::mono_symbol_n` mangles fn
  symbols (`drop_<m>_Pair__Int_Int`; compound args hash-route to
  stay bounded).
- Intrinsic-storage types (`RawBuf`) are polymorphic but use the
  flat intrinsic drop path and are NOT suffixed (their drop is
  element-type independent; the golden pins `drop_<m>_RawBuf`).

A drop fn and its call sites consult the same `DropAdtMeta`
(emission + manglers in `drop.rs`, call-site manglers in
`match_lower.rs`), so they always agree on the symbol — a
mismatch would be a link error. Ratified by
`alloc_rc_value_type_field_is_not_rc_dec_dropped` in
`crates/ail/tests/drop_value_field_no_segfault_pin.rs`.

#### String-literal rep promotion at owned drop sites

A `Str` literal carries a `StrRep`: `Static` (header-less rodata
constant) or `Heap` (rc-headered owned slab). An `Own`-mode drop
path emits `ailang_rc_dec` on the value; dec'ing a
`StrRep::Static` reads `payload - 8` (the length field) as a fake
refcount and `free()`s a static address — a segfault. Codegen
therefore promotes a `Str` literal that flows into an `Own` slot
the callee will drop from `Static` to `Heap` (codegen then emits
`ailang_str_clone` → refcount 1, and the single dec is sound).
The promotion is gated **strictly on `Own`**: a `Borrow` slot
fires no `rc_dec`, so a borrow-position literal stays
`StrRep::Static` (no spurious clone).
`crates/ailang-check/src/lower_to_mir.rs` applies this at four
sites — the `Term::App` owned-arg site (`is_str_ty` + `Own`) and
the loop-carried seed/tail/recur sites of a `Str`-returning loop
body. Ratified by `own_str_literal_arg_is_dropped_exactly_once`
in `crates/ail/tests/e2e.rs`.

#### Same-constructor arm grouping in match desugar

`crates/ailang-core/src/desugar.rs` groups consecutive match
arms that share a head constructor (`build_chain` /
`build_ctor_group`) into a single match over that constructor's
fields, binding the fields once. This keeps a literal sub-pattern
(`(Cons (pat-lit K) _)`) from re-matching — and re-dropping — the
same owned scrutinee tail across the literal-discriminating arms.
Ratified by `lit_pat_ctor_tail_drop_single_drop` and
`lit_pat_nil_scrutinee_single_drop` in `crates/ail/tests/e2e.rs`.

#### Arg-position policy for compound AST nodes

The uniqueness and linearity passes walk arguments of compound
nodes with a fixed `Position` policy. For ownership-bearing nodes:

| Node                 | Arg position | Reason                                                                                |
|----------------------|--------------|---------------------------------------------------------------------------------------|
| `Term::Ctor.args[*]` | Consume      | constructor packs values into the cell; the cell owns them afterwards                 |
| `Term::Do.args[*]`   | Borrow       | effect-op observes its arguments; the caller still owns whatever pointer it passed in |

The two policies are language rules, not per-op annotations. They
do not appear as fields on `EffectOpSig` or `Ctor`; the AST node
kind itself carries the default. The walkers that read this policy
live at `crates/ailang-check/src/uniqueness.rs` and
`crates/ailang-check/src/linearity.rs` (matched arms in both).

The Do = Borrow rule pairs with the `ret_mode == Own` letbinder-
trackability rule above: when a built-in such as `int_to_str` is
declared `ret_mode: Own` and its result is fed into an effect-op
(`io/print_str s`), the let-binder is RC-tracked for scope-close
drop *and* the effect-op does not consume it — the slab is freed
exactly once at scope close, never zero-times (RC leak under the
old Consume rule, which silenced the scope-close drop) and never
twice (double-free under a hypothetical Consume + scope-close).

**What this widening does NOT do.**

- Does not change the canonical hash. `param_modes` /
  `ret_mode` were already hash-load-bearing when introduced;
  subsequent work added codegen consumers, not new schema fields.
- Does not introduce a new `Type` variant. Mode metadata stays
  flat on `Type::Fn` (see "Schema additions" above on why).
**Let-aliases of borrowed values are propagated.** A let-binder
whose value is a bare `Term::Var`
resolving to a tracked binder is treated as an alias of that
source on both axes of the ownership analysis:

- the linearity diagnostic (spec 0064, class 2) records `a →
  root` in the walk (`crates/ailang-check/src/linearity.rs`,
  `Checker.aliases` + `resolve_alias`) and resolves every
  binder-state lookup to the root, so a borrow-position use of
  the alias does not consume the source while a real
  double-consume through the alias is still caught;
- the codegen drop gates (`crates/ailang-codegen/src/lib.rs`,
  the `MTerm::Let` lowering's `current_param_modes` mode
  inheritance) give the let-binder its source's mode, so the
  scope-close drop gate treats an alias of a borrow as borrowed
  and emits no spurious `dec`.

Ratified by: `crates/ailang-check/src/uniqueness.rs`,
`crates/ailang-check/src/linearity.rs`.