# Harden the ownership analysis for universal activation, part 2 — Design Spec **Date:** 2026-06-01 **Status:** Draft — awaiting user spec review **Authors:** orchestrator + Claude ## Goal Close the remaining precision gaps in the strict linearity analysis (`use-after-consume` / `consume-while-borrowed`, `crates/ailang-check/src/linearity.rs`) so that deleting `ParamMode::Implicit` (#55, spec 0062) does not turn part of the migrated corpus red. This is the **second hardening pass** — `#56` (spec 0063, plan 0120) closed two false-positive classes (value-type *params*; application-is-a-borrow). Executing the #55 cutover (plan 0121, Task 4) surfaced **three more** false-positive classes plus **one genuine corpus over-consume** that no mode annotation can fix: 1. **Local function-typed binder modes (false positive).** `callee_arg_modes` (`linearity.rs:750`) resolves the param-modes of a call's callee only for **global** fns; a local function-typed binder (a HOF predicate param such as `std_list.filter`'s `p`) returns an empty mode vector, so every arg of `(app p h)` defaults to `Consume`. `filter` then reuses `h` in the kept `Cons` after `(app p h)` "consumed" it → false `use-after-consume`. Blocks `std_list.filter` and its importers. 2. **`let`-alias of a borrowed value (false positive).** `Term::Let` walks its value in `Position::Consume` (`linearity.rs:506`). `(let a t (match a …))` over a `borrow`-mode `t` therefore *consumes* `t` at the binding, tripping `consume-while-borrowed`. `design/contracts/0008-memory-model.md:340` documents this propagation as explicitly **not shipped**. 3. **Inferred value-typed `let`-binders (false positive).** A `let`-binder of an unboxed value type (`Float` etc.) is installed as a default `BinderState` with `is_value = false` (`linearity.rs:507`), so a value-typed `let`-binder used more than once trips `use-after-consume`. Spec 0063 deferred exactly this class ("value-typed `let`-binders … deferred until a corpus shape demands it"); `eqord_3_newton_sqrt.iterate`'s `(let xnew (app / …) …)` is that shape. No mode annotation applies — the binder's type is inferred, not annotated. 4. **Genuine double-consume (real corpus bug, NOT a false positive).** `std_either_list.partition_eithers` projects both `(app Pair.fst rest)` and `(app Pair.snd rest)` from one owned `rest`. `Pair.fst` / `Pair.snd` are `own`-param projections that move a field out, so each consumes `rest` → `rest` is genuinely consumed twice without a `clone`. The fix is a body rewrite (destructure `rest` once), out of the migration's mechanical scope; the check correctly stays RED on the unrewritten shape. Classes 1–3 are precision gaps the gated-off `Implicit` activation was hiding; class 4 is a real fixture over-consume. This is the **precondition for #55**: spec 0062 §8 asserts the migrated corpus "contains none" of the rejected shapes, which only holds once classes 1–3 are closed and class 4 is rewritten. The rationale anchors are `design/models/0008-ownership-totality.md` §4 (HOF mode slots — a function param is applied, which is a read) and §3.2 (value types are trivial-`own`), plus the RC/uniqueness contract `design/contracts/0008-memory-model.md` (whose `:340` let-alias carve-out this cycle closes). The model is `status: Design exploration`; its claims are validated against the live tool below (Testing strategy), not assumed. ### Scope decisions ratified here 1. **The let-binder type is teed out of the type-checker, not re-inferred.** The inferred type of every `Term::Let` binder is *already computed* at `synth`'s `Let` arm (`lib.rs:3808`, `let v = synth(value, …)`) and then **discarded**. The fix records it into a `(def, binder) → Type` table returned alongside the typecheck diagnostics; linearity reads the table. This is the "stop discarding known information" fix, not the "re-run inference in the linearity walk" anti-pattern that aaa70d4 / spec 0063 ruled out. The table is the chosen mechanism for classes 1 (function-typed `let`/`lam` binders) and 3 (value-typed `let` binders) uniformly. *(User decision, 2026-06-01.)* 2. **Parameter and `lam`-param modes/types stay signature-local.** A parameter's fn-type (with `param_modes`) and a `lam`-param's type are already on the signature where the linearity walk installs the binder (`check_fn` has `param_tys`; `Term::Lam` carries `param_tys`). These continue to be read from the signature — the type table is only needed for `let`-binders, whose type is not locally annotated. The corpus driver for class 1 (`filter`'s `p`) is a **param**, so its mode resolution is signature-local; the table generalises class 1 to `let`/`lam`-bound function values for free. 3. **The `let`-alias fix is an alias *redirect*, not a state clone.** `(let a t body)` where `t` is a bare `Term::Var` resolving to a tracked binder records `a → root(t)` in an alias map for the body scope and does **not** walk `t` in `Consume`; `use_var`, the `App` borrow-count bump, and `callee_arg_modes` resolve a name through the map first. A clone of `t`'s state would be **unsound** — `(let a t (seq (consume a) (consume t)))` would mark two independent binders and miss the double-consume. The redirect keeps consume/borrow bookkeeping on the single root, so a real double-consume through an alias is still caught. ### Out of scope - **#55 itself** — deleting `ParamMode::Implicit`, the schema/hash reset, the parser/return changes (spec 0062). This spec only hardens the analysis; it changes no schema, resets no hash, and is testable **today** against explicit-mode fns (Testing strategy). - **Re-running inference in the linearity walk.** Ruled out by aaa70d4 and reaffirmed here; the type is teed, never recomputed. - **`Str` consume semantics.** Unchanged — `Str` stays heap (`is_value_type` excludes it, spec 0063 scope decision 1). - **The `over-strict-mode` lint.** Untouched. (It emits a benign Warning on the `fst`/`snd` projection helpers; that is pre-existing and orthogonal.) ## Architecture Four additive changes, no schema change, no new `Type` variant, no hash shift, no codegen change. The analysis stays a pure diagnostic pass. **New type-checker output (`crates/ailang-check/src/lib.rs`):** A `LetBinderTypes` table, `HashMap<(String, String), Type>` keyed `(def_name, binder_name)`, populated at the `synth` `Term::Let` arm (`lib.rs:3808`) with the binder's resolved inferred type, and threaded out of `check_in_workspace` / `check_workspace` to the linearity dispatch. One insert, the value already in hand; the cost is plumbing the table through the two pass functions and into the `Checker`. **Fix 1 — local function-typed binder modes (`linearity.rs`):** `BinderState` gains `fn_param_modes: Option>`. It is seeded at every binder-introduction site whose binder is function-typed: params and `lam`-params from the locally-available signature type; `let`-binders from the `LetBinderTypes` table. `callee_arg_modes`, for a local `Var` callee, reads the callee binder's `fn_param_modes` before falling back to the global symbol table. A local HOF predicate's declared arg modes then resolve, so its borrow-arg slot is walked `Borrow`, not `Consume`. **Fix 2 — value-typed `let`-binder exemption (`linearity.rs`):** `Term::Let` looks the binder's type up in the `LetBinderTypes` table and sets `is_value` from `type_is_value` — the same per-binder flag spec 0063 already seeds at param / pattern / `lam` sites, now extended to the `let` site. The walk reads the table where the source's type is otherwise unavailable; it never re-infers. **Fix 3 — `let`-alias borrow propagation (`linearity.rs`):** The `Checker` gains `aliases: HashMap`. `Term::Let` with a bare `Term::Var` value resolving (through the alias map) to a tracked binder records the alias and skips the `Consume` walk of the value; `use_var` / the `App` borrow bump / `callee_arg_modes` resolve a name to its root before touching `binders`. Scoped by the existing save/restore discipline. **Fix 4 — class-4 corpus body rewrite (`examples/std_either_list.ail`):** `partition_eithers` is rewritten to destructure `rest` once via `(match rest (case (pat-ctor MkPair ls rs) …))` and reuse `ls` / `rs`, instead of the double `Pair.fst` / `Pair.snd` projection. No check change; the check correctly rejects the old shape (a genuine double-consume) and accepts the new one. Any other corpus fn the universal activation reveals to have the same genuine-consume shape is rewritten the same way (enumerated during the migration, not here). **Contract update (`design/contracts/0008-memory-model.md`):** The `:340` "Does not cover let-aliases of borrowed values" carve-out is rewritten to record that the propagation now ships (Fix 3). A contract change rides with the feature that forces it. ## Concrete code shapes Every `ail` block below was run through `ail check` (`target/debug/ail`, 2026-06-01); the exit-code traces are in the Testing section. All are **explicit-mode** fns, so the linearity check is active **today** without #55 — each is RED now and GREEN after the named fix. ### RED→GREEN class 1: local function-typed predicate param An LLM author writes the canonical `filter` HOF; the borrow-mode predicate `p` is applied to the heap element `h`, which is then reused in the kept `Cons`. False `use-after-consume` today: ```ail (module c1_local_hof (data Box (doc "heap cell") (ctor Box (con Int))) (data List (doc "boxed list of boxes") (ctor Nil) (ctor Cons (con Box) (con List))) (fn filter_box (doc "borrow-mode predicate p applied to h; h reused in the kept Cons") (type (fn-type (params (borrow (fn-type (params (borrow (con Box))) (ret (own (con Bool))))) (own (con List))) (ret (own (con List))))) (params p xs) (body (match xs (case (pat-ctor Nil) (term-ctor List Nil)) (case (pat-ctor Cons h t) (if (app p h) (term-ctor List Cons h (app filter_box p t)) (app filter_box p t))))))) ``` ### RED→GREEN class 2: `let`-alias of a borrowed param `(let a t …)` over a `borrow`-mode `t`; false `consume-while-borrowed` today: ```ail (module c2_let_alias (data Tree (doc "boxed tree") (ctor TLeaf) (ctor TNode (con Int) (con Tree) (con Tree))) (fn count (doc "alias a := borrowed t, then match a") (type (fn-type (params (borrow (con Tree))) (ret (own (con Int))))) (params t) (body (let a t (match a (case (pat-ctor TLeaf) 0) (case (pat-ctor TNode v l r) 1)))))) ``` ### RED→GREEN class 3: value-typed `let`-binder used multiple times `xnew` is a `Float` `let`-binder used in the cond and both branches; false `use-after-consume` (×2) today: ```ail (module c3_value_let (fn iterate (doc "xnew is a Float let-binder used in cond and both branches") (type (fn-type (params (own (con Float)) (own (con Float))) (ret (own (con Float))))) (params x tol) (body (let xnew (app / x 2.0) (if (app float_lt (app - xnew x) tol) xnew xnew))))) ``` ### Must-stay-RED class 4: genuine double-consume `rest` is projected by both `fst` and `snd` (`own`-param projections) → genuinely consumed twice. This is a **real** `use-after-consume` and **stays an error** after every fix (the exemptions are type-/alias-gated, not blanket). The migration rewrites the body; the check is unchanged: ```ail (module c4_double_consume (data Pair (doc "boxed pair of ints") (ctor MkPair (con Int) (con Int))) (fn fst (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p) (body (match p (case (pat-ctor MkPair a b) a)))) (fn snd (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p) (body (match p (case (pat-ctor MkPair a b) b)))) (fn both (doc "MUST STAY RED: rest projected by fst AND snd = consumed twice") (type (fn-type (params (own (con Pair))) (ret (own (con Pair))))) (params rest) (body (term-ctor Pair MkPair (app fst rest) (app snd rest))))) ``` ### Class-4 fix: destructure once (clean today) The body rewrite — the same shape applied to the real `partition_eithers`. Clean today, clean after: ```ail (module c4_rewrite (data Pair (doc "boxed pair of ints") (ctor MkPair (con Int) (con Int))) (fn both (doc "rewrite: destructure rest once via match") (type (fn-type (params (own (con Pair))) (ret (own (con Pair))))) (params rest) (body (match rest (case (pat-ctor MkPair a b) (term-ctor Pair MkPair a b)))))) ``` ### Secondary: implementation shapes (before → after) *Supporting detail, not the headline.* **`crates/ailang-check/src/lib.rs` — tee the let-binder type at `synth`'s `Let` arm (`:3808`):** ```text before: Term::Let { name, value, body } => { let v = synth(value, env, locals, …, subst, …)?; let prev = locals.insert(name.clone(), v); let r = synth(body, …)?; …restore prev… Ok(r) } after: Term::Let { name, value, body } => { let v = synth(value, env, locals, …, subst, …)?; let_binder_types.insert((in_def.clone(), name.clone()), subst.apply(&v)); // tee the known type let prev = locals.insert(name.clone(), v); …unchanged… } // let_binder_types is a new &mut out-param on synth, threaded out of // check_fn → check_in_workspace → check_workspace to the linearity dispatch. ``` **`crates/ailang-check/src/linearity.rs` — `BinderState`:** ```text before: struct BinderState { consumed: bool, borrow_count: u32, is_value: bool } after: struct BinderState { consumed: bool, borrow_count: u32, is_value: bool, fn_param_modes: Option> } // Some(modes) for a function-typed binder; None otherwise. ``` **`linearity.rs` — `callee_arg_modes` consults local binders first (`:750`):** ```text before: only Term::Var resolving to self.globals; locals → vec![] after: for a Term::Var callee, resolve through self.aliases, then: 1. if the binder carries fn_param_modes, return them; 2. else fall back to self.globals (today's path). ``` **`linearity.rs` — `Term::Let` (`:505`):** ```text before: Term::Let { name, value, body } => { self.walk(value, Position::Consume); self.with_binder(name, BinderState::default(), |this| { this.walk(body, pos); }); } after: Term::Let { name, value, body } => { // (a) bare-Var alias of a tracked binder → record alias, skip the consume walk; // (b) otherwise walk value in Consume as today; // seed the let-binder's is_value / fn_param_modes from LetBinderTypes // (keyed (def, name)) for the body scope. } ``` **`examples/std_either_list.ail` — `partition_eithers` Cons arm (`:61`):** ```text before: (case (pat-ctor Cons h t) (let rest (app partition_eithers t) (match h (case (pat-ctor Left l) (term-ctor Pair MkPair (term-ctor List Cons l (app Pair.fst rest)) (app Pair.snd rest))) (case (pat-ctor Right r) (term-ctor Pair MkPair (app Pair.fst rest) (term-ctor List Cons r (app Pair.snd rest))))))) after: (case (pat-ctor Cons h t) (let rest (app partition_eithers t) (match rest (case (pat-ctor MkPair ls rs) (match h (case (pat-ctor Left l) (term-ctor Pair MkPair (term-ctor List Cons l ls) rs)) (case (pat-ctor Right r) (term-ctor Pair MkPair ls (term-ctor List Cons r rs)))))))) // rest destructured once; ls/rs each consumed once per independent match-arm. ``` ## Components - **`ailang-check::lib` (typecheck pass)** — `synth` gains the `let_binder_types` out-param and one insert at the `Let` arm; `check_fn` / `check_in_workspace` / `check_workspace` thread the table out to the linearity dispatch (`lib.rs:1276`). - **`ailang-check::linearity`** — `BinderState.fn_param_modes`; the `Checker` gains an immutable `let_binder_types` reference and a scoped `aliases` map; `callee_arg_modes` resolves locals + aliases; `Term::Let` seeds `is_value` / `fn_param_modes` from the table and records bare-Var aliases. - **`.ail` fixtures** — the three RED→GREEN fixtures (classes 1–3), the must-stay-RED double-consume, and the rewrite, under `examples/`. - **`examples/std_either_list.ail`** — the `partition_eithers` rewrite (plus any sibling corpus fn the migration reveals with the same genuine-consume shape). - **`design/contracts/0008-memory-model.md`** — the `:340` let-alias carve-out updated to "ships". No change to: the schema (`ParamMode`, `Type::Fn`), the parser, the printer, codegen, the runtime, `is_heap_type`, or the `over-strict-mode` lint. ## Data flow **The type table.** The typecheck pass already synthesises every `let`-binder's type (`lib.rs:3808`); today it is dropped when `check_fn` returns `Result<()>`. The fix records `subst.apply(&v)` — the resolved type — into `(def, binder) → Type` and threads it to linearity, which runs strictly **after** a clean typecheck (`lib.rs:1254` gate), so the table is fully populated before the walk starts. Linearity reads the table only at the `Term::Let` introduction site; params and `lam`-params keep reading their signature types. A binder whose teed type is not a value `Type::Con` and not a `Type::Fn` defaults exactly as today (`is_value = false`, `fn_param_modes = None`). **Mode resolution.** For `(app callee args)`, `callee_arg_modes` resolves the callee `Var` through the alias map, then prefers a tracked binder's `fn_param_modes` over the global table. A global fn-ref callee is untracked, so it still falls through to `self.globals` — no behaviour change for the common case. A local function-typed binder now resolves its declared arg modes, so a borrow-arg slot is walked `Borrow`. **Alias soundness.** `(let a t body)` with `t` a tracked binder makes `a` a redirect to `root(t)`. Every binder op on `a` (consume, borrow, mode lookup) acts on the single root state, so: a borrow-position use of `a` does not consume `t` (fixes the false positive), and a consume of `a` marks `t` consumed (so a later consume of either is a real `use-after-consume` — no false negative). Aliases are installed for the body scope and removed on exit, like any binder. ## Error handling No new diagnostic codes. The two existing codes (`use-after-consume`, `consume-while-borrowed`) fire on a strictly smaller, more correct set: they no longer fire on local HOF-param applications (class 1), borrowed-value `let`-aliases (class 2), or value-typed `let`-binders (class 3). They continue to fire on the genuine double-consume (class 4, must-stay-RED) and on any real use-after-consume reached through an alias. The change is a precision improvement to existing diagnostics, not a new check surface. ## Testing strategy Live `ail check` traces (run 2026-06-01, `target/debug/ail`) — the state **today**, before the fixes: ```text c1_local_hof.ail : exit 1 error: [use-after-consume] filter_box: `h` ... c2_let_alias.ail : exit 1 error: [consume-while-borrowed] count: `t` ... c3_value_let.ail : exit 1 error: [use-after-consume] iterate: `xnew` ... (x2) c4_double_consume.ail : exit 1 error: [use-after-consume] both: `rest` ... (+ benign over-strict-mode warnings on fst/snd) c4_rewrite.ail : exit 0 ok ``` - **RED→GREEN fixtures.** `c1_local_hof`, `c2_let_alias`, `c3_value_let` land under `examples/`; each asserts its named diagnostic fires **today** and is **clean** (exit 0) after the matching fix. These are the RED side of fixes 1–3. - **Must-stay-RED fixture.** `c4_double_consume` asserts the genuine double-consume still fires after all fixes — the exemptions are type-/alias-gated, not blanket. It is the analogue of spec 0063's `real_consume`. - **Class-4 corpus rewrite.** `examples/std_either_list.ail` checks and runs clean after the `partition_eithers` rewrite; its existing E2E/demo (`std_either_list_demo.ail`) output is unchanged. - **Alias soundness unit test.** An in-source `#[cfg(test)]` case in `linearity.rs`: a `(let a t (seq …consume a… …consume t…))` over an `own` `t` still produces `use-after-consume` (the redirect does not mask a real double-consume). - **`std_list.filter` + importers.** `std_list.ail` and the seven modules that import it (`kem_1_list_running_sum`, `nested_pat`, `std_either_list`, `std_either_list_demo`, `std_list_demo`, `std_list_more_demo`, `std_list_stress`) check clean once `filter`'s signature is migrated to explicit modes (validated against the migrated corpus; the analysis only activates with explicit modes). - **Full corpus regression.** `cargo test --workspace` stays green, and the `examples/` typecheck/codegen suite is the net for "no exemption silenced a real consume". Per the typed-MIR re-synth strictness memory, run the whole workspace suite, not just e2e. - **Regression scripts.** `bench/check.py` and `bench/compile_check.py` stay green (diagnostic-only change; no compile-baseline shift expected). ## Acceptance criteria 1. A `(def, binder) → Type` table is teed from the typecheck pass and threaded to linearity; `synth`'s `Let` arm records the resolved binder type, and linearity reads it (no inference re-run in the walk). 2. `c1_local_hof`, `c2_let_alias`, `c3_value_let` check **clean** (exit 0) after their fixes; each shipped as an `examples/` fixture asserting its today→post transition. 3. `c4_double_consume` still fails with `use-after-consume` after all fixes (exemptions are type-/alias-gated). 4. `callee_arg_modes` resolves a local function-typed binder's `param_modes`; a borrow-mode HOF predicate param applied to a heap element does not consume it. 5. A `let`-alias of a `borrow`-mode binder does not trip `consume-while-borrowed`, and a `let`-alias of an `own` binder still catches a real double-consume (alias soundness unit test). 6. `examples/std_either_list.ail` checks and runs clean after the `partition_eithers` rewrite; output unchanged. 7. `cargo test --workspace` green; `bench/check.py` and `bench/compile_check.py` green. 8. `design/contracts/0008-memory-model.md:340` is updated to record the let-alias propagation as shipped. 9. No change to `ParamMode`, `Type::Fn`, the parser/printer, codegen, the runtime, `is_heap_type`, or the `over-strict-mode` lint (grep / diff clean).