AILang/docs/specs/0064-harden-ownership-analysis-part-2.md

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<Vec<ParamMode>>. 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<String, String>. 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:

(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:

(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:

(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:

(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:

(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):

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:

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<Vec<ParamMode>> }
        // Some(modes) for a function-typed binder; None otherwise.

linearity.rs — callee_arg_modes consults local binders first (:750):

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

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

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:

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