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.

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). 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). 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.

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); 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 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].

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. 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). 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.