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

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

- [ ] **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:

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

to:

```rust
    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:

```rust
    /// `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(),`):

```rust
        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:

```rust
    /// 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:

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

```rust
            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:

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

```rust
    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`:

```rust
                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:

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

```rust
                    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:

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

```rust
        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:

```rust
                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"):

```rust
                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:

```rust
    /// 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.