AILang/docs/plans/0124-harden-ownership-part2-class2.md

Harden ownership part 2 — iteration 3: let-alias borrow propagation (class 2) — Implementation Plan

Parent spec: docs/specs/0064-harden-ownership-analysis-part-2.md

For agentic workers: REQUIRED SUB-SKILL: use the implement skill to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Stop a let-alias of a borrowed value from being treated as a consume, closing false-positive class 2, while keeping a real double-consume through an alias detectable.

Architecture: The Checker gains a scoped aliases: HashMap<String,String> map. (let a t body) whose value is a bare Term::Var resolving to a tracked binder records a → root(t) for the body scope and skips the Consume walk of the value. A new resolve_alias helper maps any name to its root, preferring a real binder at each chain step — so an inner binder named a (a nested let, a pattern binder, a lam param) automatically shadows the alias with no change to the binder-introduction sites. Every binder-state lookup keyed by name (use_var, the App borrow-count bump + decrement, callee_arg_modes, reuse-as source) resolves through the map first, so consume/borrow bookkeeping lands on the single root: a borrow-position use of the alias does not consume the root (the fix), and a consume of the alias marks the root consumed (so a later consume of either is still caught — no false negative). Diagnostic-only; no schema/type change.

Tech Stack: crates/ailang-check/src/linearity.rs (the whole fix), examples/ fixture, tests/workspace.rs assertion, design/contracts/0008-memory-model.md (the carve-out this closes).

Scope: THIRD iteration of spec 0064 — class 2 only. Out of scope (later iteration): class 4 (partition_eithers rewrite + c4_double_consume fixture). Classes 1/3 already shipped.

Resolution-site completeness note. Spec §"Fix 3" names use_var, the App borrow bump, and callee_arg_modes as the resolution points. The complete set of binder-state-reading sites in linearity.rs also includes the reuse-as source path (:663-685): a (reuse-as a …) whose a is an alias would otherwise mis-fire reuse-as-source-not-bare-var (it IS a Var). The plan resolves aliases there too — a faithful completion of Fix 3's "resolve a name to its root before touching binders", not a scope addition. The binder-introduction sites (with_binder, walk_arm, Lam) need NO change because resolve_alias prefers a real binder at each step.

---

Files this plan creates or modifies:

• Create: examples/c2_let_alias.ail — class-2 RED→GREEN fixture (let-alias of a borrow-mode param, matched).
• Modify: crates/ailang-check/src/linearity.rs — Checker.aliases field + init; resolve_alias helper; Term::Let alias case; alias-resolution in use_var, the App bump/decrement, callee_arg_modes, and reuse-as; an alias-soundness unit test.
• Modify: crates/ailang-check/tests/workspace.rs:728 — add c2_let_alias to harden_ownership_false_positives_are_clean.
• Modify: design/contracts/0008-memory-model.md:340-348 — the let-alias carve-out bullet rewritten to "ships"; the Ratified by: trailer extended to name linearity.rs.

---

Task 1: RED — class-2 fixture and its failing workspace assertion

Files:

• Create: examples/c2_let_alias.ail

• Test: crates/ailang-check/tests/workspace.rs:728

• Step 1: Create the fixture

Create examples/c2_let_alias.ail with exactly:

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

• Step 2: Add the fixture to the false-positive list

In crates/ailang-check/tests/workspace.rs, the test harden_ownership_false_positives_are_clean iterates a literal array at line 728. Change exactly:

    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof"] {

to:

    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias"] {

• Step 3: Run the test to verify it fails RED

Run: cargo test -p ailang-check --test workspace harden_ownership_false_positives_are_clean Expected: FAIL — panic c2_let_alias must be linearity-clean; got: [...] with a consume-while-borrowed diagnostic on t in count. The other five fixtures stay clean; only c2_let_alias fails.

---

Task 2: GREEN — the alias-redirect map

Files:

• Modify: crates/ailang-check/src/linearity.rs:460-481 (Checker struct), :398-405 (construction), :541-555 (Term::Let), :752-786 (use_var), :524-538 (App bump/decrement), :798-814 (callee_arg_modes), :663-685 (reuse-as), plus the in-source test module.

• Step 1: Add the aliases field to Checker

In crates/ailang-check/src/linearity.rs, the Checker<'a> struct (:460-481) ends with the binders field. Add after it:

    /// `let`-alias → root binder name. A `(let a t …)` whose value is
    /// a bare `Var t` resolving to a tracked binder records `a →
    /// root(t)` here for the body scope; every binder-state lookup
    /// resolves a name through this map first, so the alias shares the
    /// root's consume/borrow state. Scoped: removed when the `let`
    /// body ends.
    aliases: HashMap<String, String>,

• Step 2: Initialise aliases in the Checker construction

In crates/ailang-check/src/linearity.rs, the construction literal in check_fn (:398-405) names all fields. Add the init (after binders: HashMap::new(),):

        aliases: HashMap::new(),

• Step 3: Add the resolve_alias helper

In crates/ailang-check/src/linearity.rs, in the impl<'a> Checker<'a> block, immediately before fn use_var (:752), add:

    /// Resolve a name to the binder it ultimately denotes, following
    /// `let`-alias links. A real binder shadows an alias: at each step,
    /// if the current name is a tracked binder we stop there, so an
    /// inner `let`/pattern/`lam` binder of the same name takes
    /// precedence over an outer alias without any change to the
    /// binder-introduction sites. Returns an owned `String` so the
    /// immutable borrow of `self.aliases` ends before any
    /// `self.binders` mutation by the caller.
    fn resolve_alias(&self, name: &str) -> String {
        let mut cur = name.to_string();
        loop {
            if self.binders.contains_key(&cur) {
                return cur;
            }
            match self.aliases.get(&cur) {
                Some(next) => cur = next.clone(),
                None => return cur,
            }
        }
    }

• Step 4: Rewrite the Term::Let arm with the alias case

In crates/ailang-check/src/linearity.rs, the Term::Let arm (:541-555) is currently:

            Term::Let { name, value, body } => {
                self.walk(value, Position::Consume);
                let teed = self
                    .let_binder_types
                    .get(&(self.def_name.to_string(), name.clone()));
                let is_value = teed.map(type_is_value).unwrap_or(false);
                let fn_param_modes = teed.and_then(|t| fn_modes_of(t));
                self.with_binder(
                    name,
                    BinderState { is_value, fn_param_modes, ..BinderState::default() },
                    |this| {
                        this.walk(body, pos);
                    },
                );
            }

Replace it with (alias case first; non-alias case is today's body unchanged):

            Term::Let { name, value, body } => {
                // Class 2: a bare-Var value aliasing a tracked binder is
                // a borrow-preserving rename, not a consume. Record
                // `name → root` and skip the consume walk of the value;
                // all binder-state lookups resolve through `aliases`.
                let alias_root = match value.as_ref() {
                    Term::Var { name: vname } => {
                        let root = self.resolve_alias(vname);
                        if self.binders.contains_key(&root) { Some(root) } else { None }
                    }
                    _ => None,
                };
                if let Some(root) = alias_root {
                    // Shadow any outer binder / alias of `name` for the
                    // body, install the alias, walk, then restore both.
                    let prev_binder = self.binders.remove(name);
                    let prev_alias = self.aliases.insert(name.clone(), root);
                    self.walk(body, pos);
                    self.aliases.remove(name);
                    if let Some(a) = prev_alias {
                        self.aliases.insert(name.clone(), a);
                    }
                    if let Some(b) = prev_binder {
                        self.binders.insert(name.clone(), b);
                    }
                } else {
                    self.walk(value, Position::Consume);
                    let teed = self
                        .let_binder_types
                        .get(&(self.def_name.to_string(), name.clone()));
                    let is_value = teed.map(type_is_value).unwrap_or(false);
                    let fn_param_modes = teed.and_then(|t| fn_modes_of(t));
                    self.with_binder(
                        name,
                        BinderState { is_value, fn_param_modes, ..BinderState::default() },
                        |this| {
                            this.walk(body, pos);
                        },
                    );
                }
            }

• Step 5: Resolve aliases in use_var

In crates/ailang-check/src/linearity.rs, use_var (:752-786) starts with let state = match self.binders.get_mut(name) {. Replace its first lines:

    fn use_var(&mut self, name: &str, pos: Position) {
        let state = match self.binders.get_mut(name) {
            Some(s) => s,
            None => return,
        };
        if state.consumed {
            self.diags
                .push(make_use_after_consume(self.def_name, name));
            return;
        }

with (resolve to the root first; report the root in the diagnostic):

    fn use_var(&mut self, name: &str, pos: Position) {
        let root = self.resolve_alias(name);
        let state = match self.binders.get_mut(&root) {
            Some(s) => s,
            None => return,
        };
        if state.consumed {
            self.diags
                .push(make_use_after_consume(self.def_name, &root));
            return;
        }

The make_consume_while_borrowed(self.def_name, name) call later in the same fn must also report the root — change that one argument from name to &root:

                if state.borrow_count > 0 {
                    self.diags
                        .push(make_consume_while_borrowed(self.def_name, &root));
                    return;
                }

• Step 6: Resolve aliases in the App borrow bump and decrement

In crates/ailang-check/src/linearity.rs, the App borrow-bump block (:524-528) is:

                    if matches!(arg_pos, Position::Borrow) {
                        if let Term::Var { name } = arg {
                            if let Some(s) = self.binders.get_mut(name) {
                                s.borrow_count = s.borrow_count.saturating_add(1);
                                lent.push(name.clone());
                            }
                        }
                    }

Replace with (resolve the arg name to its root; push the root so the decrement targets the same key):

                    if matches!(arg_pos, Position::Borrow) {
                        if let Term::Var { name } = arg {
                            let root = self.resolve_alias(name);
                            if let Some(s) = self.binders.get_mut(&root) {
                                s.borrow_count = s.borrow_count.saturating_add(1);
                                lent.push(root);
                            }
                        }
                    }

(The decrement loop for name in lent { … self.binders.get_mut(&name) … } at :535-538 is unchanged — lent now holds resolved roots.)

• Step 7: Resolve the callee alias in callee_arg_modes

In crates/ailang-check/src/linearity.rs, callee_arg_modes (:798-814) binds name then reads the local binder. Replace:

        let name = match callee {
            Term::Var { name } => name,
            _ => return vec![],
        };
        if let Some(s) = self.binders.get(name) {
            if let Some(modes) = &s.fn_param_modes {
                return modes.clone();
            }
        }

with (resolve to root before the local-binder read; the global lookup below is unchanged — root == name whenever the callee is a global):

        let name = match callee {
            Term::Var { name } => name,
            _ => return vec![],
        };
        let root = self.resolve_alias(name);
        if let Some(s) = self.binders.get(&root) {
            if let Some(modes) = &s.fn_param_modes {
                return modes.clone();
            }
        }

• Step 8: Resolve the reuse-as source through aliases

In crates/ailang-check/src/linearity.rs, the reuse-as source match (:663-685) is:

                match source.as_ref() {
                    Term::Var { name } if self.binders.contains_key(name) => {
                        let already_consumed = self
                            .binders
                            .get(name)
                            .map(|s| s.consumed)
                            .unwrap_or(false);
                        if already_consumed {
                            self.diags
                                .push(make_use_after_consume_at_reuse_as(self.def_name, name, body));
                        } else if let Some(s) = self.binders.get_mut(name) {
                            // Mark the source consumed at the reuse-as site.
                            s.consumed = true;
                        }
                    }
                    other => {
                        self.diags.push(make_reuse_as_source_not_bare_var(
                            self.def_name,
                            other,
                            body,
                        ));
                    }
                }

Replace with (resolve a Var source to its root; a Var aliasing a tracked binder is a valid bare-Var source, not "not bare var"):

                let resolved = match source.as_ref() {
                    Term::Var { name } => Some(self.resolve_alias(name)),
                    _ => None,
                };
                match resolved {
                    Some(root) if self.binders.contains_key(&root) => {
                        let already_consumed = self
                            .binders
                            .get(&root)
                            .map(|s| s.consumed)
                            .unwrap_or(false);
                        if already_consumed {
                            self.diags
                                .push(make_use_after_consume_at_reuse_as(self.def_name, &root, body));
                        } else if let Some(s) = self.binders.get_mut(&root) {
                            // Mark the source consumed at the reuse-as site.
                            s.consumed = true;
                        }
                    }
                    _ => {
                        self.diags.push(make_reuse_as_source_not_bare_var(
                            self.def_name,
                            source.as_ref(),
                            body,
                        ));
                    }
                }

• Step 9: Build the crate (compile gate)

Run: cargo build -p ailang-check Expected: 0 errors. (Adding the aliases field broke only the Checker construction literal, fixed in Step 2; resolve_alias is used in Steps 4-8.)

• Step 10: Run the RED test from Task 1 — now GREEN

Run: cargo test -p ailang-check --test workspace harden_ownership_false_positives_are_clean Expected: PASS — c2_let_alias is now linearity-clean (a aliases the borrowed t; the match a scrutinee is a borrow use of the root, not a consume), and the other five fixtures stay clean.

• Step 11: Add the alias-soundness unit test

In crates/ailang-check/src/linearity.rs, in the #[cfg(test)] mod tests block (alongside heap_let_binder_multi_read_still_errors), add:

    /// Alias soundness: `(let a p0 (seq a p0))` over an OWN heap binder
    /// `p0` — consuming the alias `a` then the root `p0` is a real
    /// double-consume and MUST still fire use-after-consume. The
    /// redirect shares one root state; it does not mask the second
    /// consume (the clone alternative would). Empty table → the alias
    /// path triggers structurally on the bare-Var value.
    #[test]
    fn let_alias_of_owned_double_consume_still_errors() {
        let body = Term::Let {
            name: "a".into(),
            value: Box::new(Term::Var { name: "p0".into() }),
            body: Box::new(Term::Seq {
                lhs: Box::new(Term::Var { name: "a".into() }),
                rhs: Box::new(Term::Var { name: "p0".into() }),
            }),
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            kernel: false,
            imports: vec![],
            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
        };
        let diags = check_module(&m);
        assert!(
            diags.iter().any(|d| d.code == "use-after-consume"),
            "consuming an alias then its root is a real double-consume; got {diags:?}"
        );
    }

• Step 12: Run the in-source linearity unit tests

Run: cargo test -p ailang-check --lib linearity::tests Expected: PASS — the new let_alias_of_owned_double_consume_still_errors plus every pre-existing linearity unit test (the class-1/class-3 tests from iters 1-2, heap_param_multi_consume_still_errors, the implicit_fn_is_exempt family, …) stay green.

• Step 13: Full crate regression

Run: cargo test -p ailang-check Expected: PASS — the whole ailang-check suite green. Alias resolution is a no-op for every name that is not a recorded alias (resolve_alias returns the name unchanged), so no non-alias outcome changes except c2_let_alias flipping RED→GREEN.

• Step 14: Workspace suite + regression scripts

Run: cargo test --workspace Expected: PASS (per the typed-MIR re-synth strictness memory, run the whole workspace, not just e2e).

Run: python3 bench/check.py then python3 bench/compile_check.py Expected: both green — diagnostic-only change; no compile-baseline shift.

---

Task 3: Close the contract carve-out

Files:

• Modify: design/contracts/0008-memory-model.md:340-348

• Step 1: Rewrite the let-alias carve-out bullet

In design/contracts/0008-memory-model.md, the bullet under "What this widening does NOT do" (:340-346) currently reads:

- Does not cover let-aliases of borrowed values. A let-binder
  whose value is `Term::Var` referencing a `Borrow`-mode
  param is not yet propagated through; the param-mode gates
  treat such a binder as "owned" (its `current_param_modes`
  lookup misses, default = owned). This is a known carve-out
  shared by Iter A and the pre-tail-call shallow-dec arm; closing it is a propagation pass
  through let-bindings that has not shipped yet.

Replace that bullet with:

- Covers let-aliases of borrowed values (spec 0064, class 2). A
  let-binder whose value is a bare `Term::Var` resolving to a
  tracked binder is recorded as an alias to that root in the
  linearity walk (`crates/ailang-check/src/linearity.rs`,
  `Checker.aliases` + `resolve_alias`); the binding does not
  consume the source, and every binder-state lookup resolves
  the alias to its root, so a borrow-position use of the alias
  does not consume the root while a real double-consume through
  the alias is still caught.

• Step 2: Extend the Ratified by: trailer

In design/contracts/0008-memory-model.md, the section trailer (:348) currently reads:

Ratified by: `crates/ailang-check/src/uniqueness.rs`.

Change it to name the linearity walk, which now hosts the let-alias propagation:

Ratified by: `crates/ailang-check/src/uniqueness.rs`,
`crates/ailang-check/src/linearity.rs`.

• Step 3: Verify the contract file is internally consistent

Run: grep -n "let-alias\|Ratified by" design/contracts/0008-memory-model.md Expected: the carve-out bullet now states the propagation ships, and the trailer names both uniqueness.rs and linearity.rs. No remaining "has not shipped yet" / "Does not cover let-aliases" text.