AILang/design/contracts/memory-model.md

# Memory model — language-design constraints and codegen contract

## Language-design constraints (binding)

The four constraints below are necessary preconditions for RC to
be sound and complete *without* a cycle-collector backstop. They
are not new — AILang already satisfies all four — but Decision 10
makes them load-bearing rather than incidental:

1. **Strict evaluation.** Every `Term::App` argument is fully
   evaluated before the call. No laziness, no thunks. (Already
   true.)
2. **No recursive value bindings.** `(let x EXPR ...)` evaluates
   `EXPR` in a scope where `x` is *not* bound. Recursion is
   exclusively via `Term::LetRec` (which binds a fn, not a value)
   and module-level fn defs. (Already true.)
3. **No shared mutable refs.** Values are immutable once
   constructed. There is no `ref`, `IORef`, `Mutex`, or any
   primitive that allows a value to be mutated from a position
   outside its allocation. (Already true.)
4. **ADTs are acyclic by construction.** Strict evaluation +
   no-recursive-value-bindings + no-shared-mutable-refs together
   guarantee that any value graph reachable from a binding is a
   DAG. The reference graph has no cycles. (Follows from 1–3.)

Laziness, recursive value bindings, shared mutable state, or any
feature that creates cycles is rejected at design time unless the
proposal proves the cycle is collectible by an extension (e.g.
linear ownership).

## Schema additions

**Parameter modes on `Type::Fn`.**

The form-A surface 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" 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). Decision 1 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.

`Implicit` is the legacy / back-compat state — semantically
equivalent to `Own` but printed bare (`(con T)`, no wrapper).
`Own` and `Borrow` are explicitly annotated.

JSON canonical hash for every existing fixture stays bit-
identical: `param_modes` is skipped when every entry is
`Implicit`, `ret_mode` is skipped when `Implicit`. Existing
modules emit the same bytes as before.

**Type::Con name scoping (canonical form, since ct.1).** 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 canonical-form rule (mq.1): bare for
same-module references, `<module>.<Class>` for cross-module
references — symmetric to `Type::Con.name`'s rule from ct.1.
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 post-mq.3 (see §"Method dispatch"
below): 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" 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 in ct.1 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
existing 13a/19b/22b.1 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. Decision 10's mandatory-annotation rule 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`.

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.

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)`. The initial RC plumbing
stops there — inc/dec instrumentation is added once the
inference is wired up. Until then, `--alloc=rc` deliberately
leaks like the pre-Boehm era; this is purely about plumbing.

## 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` and `Implicit` parameters are skipped:
  `Borrow` retains the caller's ownership by contract;
  `Implicit` carries no static caller-handed-off-ownership
  signal (it's the back-compat lane).

- **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 — `Borrow` and `Implicit` scrutinees 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]`.

**`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. `Borrow`-returning calls remain
  non-trackable (the callee retains ownership; the caller
  holds a view, not an own ref). `Implicit`-returning calls
  remain non-trackable (back-compat lane).

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).
- Does not cover let-aliases of borrowed values. A let-binder
  whose value is `Term::Var` referencing a `Borrow`-mode
  param is not yet propagated through; the param-mode gates
  treat such a binder as "owned" (its `current_param_modes`
  lookup misses, default = owned). This is a known carve-out
  shared by Iter A and the pre-tail-call shallow-dec arm; closing it is a propagation pass
  through let-bindings that has not shipped yet.

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