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; 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 for the schema-level definition of Type::Fn).

The form-A surface (see authoring 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). The canonical-schema principle 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): 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). 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.