# 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 `.` where `` 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, `.` 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 (`..`) 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 } ; `(clone X)` — explicit RC inc Term::ReuseAs { source: Box, body: Box } ; `(reuse-as SRC NEW-CTOR)` ``` `Term::ReuseAs` is structured as a *wrapper* around a `body` term rather than as a `reuse_from: Option` modifier on `Term::Ctor`. Two substantive reasons: 1. **Compositional flexibility.** Reuse-as is conceptually a wrapper that says "this expression's allocation comes from ``'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 : ` 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 `$` (`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__` (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__` / `partial_drop__` 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__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__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`.