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`).
The canonical-form tightening for `Type::Con.name` shifted the
hashes of two cross-module fixtures (`ordering_match.ail.json` and
`test_22b1_dup_a.ail.json`); all intra-module fixtures, including
the regression-pinned `sum.ail.json` and `list.ail.json`, remain
bit-identical. The new pins are
`ct4_migrated_fixtures_have_canonical_form_hashes` (locks the
post-migration hashes) and
`ct4_unmigrated_fixtures_remain_bit_identical` (re-asserts the
pre-tightening hashes still hold).

## 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. They were promoted from
"annotation that the typechecker enforces" to "annotation that
codegen reads to keep RC correct". Recorded here so the schema
metadata's role is explicit:

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

- **Iter B: 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`.)

- **Iter A: 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 Iter A and Iter B 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]`.

**Per-fn binder-name injectivity (a precondition of every gate
above).** All three drop gates read `consume_count` from the
uniqueness side-table keyed by `(def_name, binder_name)`. 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).

#### 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** (no longer a
carve-out). 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`.