feat(check): let-alias borrow propagation via alias-redirect (#57, 0064 iter 3)

Third iteration of spec 0064 (the #55-cutover hardening, #57). Closes
false-positive class 2: Term::Let walked its value in Position::Consume,
so (let a t (match a …)) over a borrow-mode t consumed t at the binding
and tripped consume-while-borrowed -- a let-alias of a borrowed value
read in a borrow position is not a consume.

Fix: the Checker gains a scoped aliases: HashMap<String,String>. A
(let a t body) whose value is a bare 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 a name to its root,
preferring a real binder at each chain step -- so an inner binder named
`a` (nested let, pattern binder, lam param) automatically shadows the
alias with NO change to with_binder/walk_arm/Lam (the shadowing is
resolved centrally in the resolver, not at three scattered introduction
sites). Every binder-state lookup keyed by name resolves through the
map first: use_var, the App borrow bump + decrement (pushing the
resolved root to `lent` so the decrement matches), callee_arg_modes,
and the reuse-as source.

Design calls (orchestrator):
- Alias REDIRECT, not state clone (spec scope decision 3): consuming
  the alias marks the single root consumed, so a real double-consume
  through an alias is still caught. A clone would track two independent
  binders and miss it (unsound). Pinned by the new
  let_alias_of_owned_double_consume_still_errors unit test:
  (let a p0 (seq a p0)) over an own heap p0 still fires
  use-after-consume.
- resolve_alias prefers binders -> shadowing needs no edits to the
  binder-introduction sites. Lower-risk than clearing aliases at each.
- reuse-as source (linearity.rs:663) is resolved through aliases too:
  it is the 4th binder-state-reading site; the spec's Fix 3 named three
  illustratively. Without it, (reuse-as <alias> …) would mis-fire
  reuse-as-source-not-bare-var on what IS a Var. Faithful completion of
  Fix 3.

The diagnostic now reports the resolved root name (the actual consumed
resource), not the surface alias.

Closes the design/contracts/0008-memory-model.md let-alias carve-out
(was "has not shipped yet") and extends its Ratified-by trailer to name
linearity.rs, where the propagation now lives -- a contract change
riding with the feature that forces it.

RED-first: examples/c2_let_alias.ail added to
harden_ownership_false_positives_are_clean (RED: consume-while-borrowed
on count's t); GREEN after. Verified: c2 RED->GREEN; 120 linearity unit
tests green; the soundness test fires; harden false-positive + heap
double-consume guards green; cargo test --workspace green;
bench/check.py 34/34, compile_check.py 24/24 stable. Diagnostic-only;
no schema/type/codegen change.

Class 4 (partition_eithers body rewrite) remains for the final
iteration of spec 0064.

refs #57

crates/ailang-check/src/linearity.rs

@@ -402,6 +402,7 @@ fn check_fn(
         ctors,
         let_binder_types,
         binders: HashMap::new(),
+        aliases: HashMap::new(),
     };
 
     // Install fn parameters as binders, with initial `borrow_count = 1`
@@ -478,6 +479,13 @@ struct Checker<'a> {
     /// Live binder state, keyed by name. Modified in place; lexical
     /// scoping is restored by [`Checker::with_binder`].
     binders: HashMap<String, BinderState>,
+    /// `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>,
 }
 
 impl<'a> Checker<'a> {
@@ -523,9 +531,10 @@ impl<'a> Checker<'a> {
                     // triggers `consume-while-borrowed`.
                     if matches!(arg_pos, Position::Borrow) {
                         if let Term::Var { name } = arg {
-                            if let Some(s) = self.binders.get_mut(name) {
+                            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(name.clone());
+                                lent.push(root);
                             }
                         }
                     }
@@ -539,19 +548,45 @@ impl<'a> Checker<'a> {
                 }
             }
             Term::Let { name, value, body } => {
-                self.walk(value, Position::Consume);
+                // Class 2: a bare-Var value aliasing a tracked binder is
-                let teed = self
+                // a borrow-preserving rename, not a consume. Record
-                    .let_binder_types
+                // `name → root` and skip the consume walk of the value;
-                    .get(&(self.def_name.to_string(), name.clone()));
+                // all binder-state lookups resolve through `aliases`.
-                let is_value = teed.map(type_is_value).unwrap_or(false);
+                let alias_root = match value.as_ref() {
-                let fn_param_modes = teed.and_then(|t| fn_modes_of(t));
+                    Term::Var { name: vname } => {
-                self.with_binder(
+                        let root = self.resolve_alias(vname);
-                    name,
+                        if self.binders.contains_key(&root) { Some(root) } else { None }
-                    BinderState { is_value, fn_param_modes, ..BinderState::default() },
+                    }
-                    |this| {
+                    _ => None,
-                        this.walk(body, pos);
+                };
-                    },
+                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);
+                        },
+                    );
+                }
             }
             Term::LetRec { name, body, in_term, .. } => {
                 // The body is the recursive fn's own body; treating it as
@@ -660,25 +695,29 @@ impl<'a> Checker<'a> {
                 //     to the usual position rules; e.g. a Consume of
                 //     the same binder inside `BODY` will fire
                 //     use-after-consume because reuse-as already ate it.
-                match source.as_ref() {
+                let resolved = match source.as_ref() {
-                    Term::Var { name } if self.binders.contains_key(name) => {
+                    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(name)
+                            .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, name, body));
+                                .push(make_use_after_consume_at_reuse_as(self.def_name, &root, body));
-                        } else if let Some(s) = self.binders.get_mut(name) {
+                        } else if let Some(s) = self.binders.get_mut(&root) {
                             // 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,
+                            source.as_ref(),
                             body,
                         ));
                     }
@@ -749,8 +788,30 @@ impl<'a> Checker<'a> {
     /// (incrementing before the next sibling, decrementing when the
     /// call returns). A scrutinee or `Term::Clone` borrow does not
     /// span siblings, so it just checks `consumed` and returns.
+    /// 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,
+            }
+        }
+    }
+
     fn use_var(&mut self, name: &str, pos: Position) {
-        let state = match self.binders.get_mut(name) {
+        let root = self.resolve_alias(name);
+        let state = match self.binders.get_mut(&root) {
             Some(s) => s,
             None => return,
         };
@@ -759,7 +820,7 @@ impl<'a> Checker<'a> {
         // regardless of position.
         if state.consumed {
             self.diags
-                .push(make_use_after_consume(self.def_name, name));
+                .push(make_use_after_consume(self.def_name, &root));
             return;
         }
 
@@ -777,7 +838,7 @@ impl<'a> Checker<'a> {
                 }
                 if state.borrow_count > 0 {
                     self.diags
-                        .push(make_consume_while_borrowed(self.def_name, name));
+                        .push(make_consume_while_borrowed(self.def_name, &root));
                     return;
                 }
                 state.consumed = true;
@@ -800,13 +861,14 @@ impl<'a> Checker<'a> {
             Term::Var { name } => name,
             _ => return vec![],
         };
+        let root = self.resolve_alias(name);
         // A local function-typed binder (HOF predicate param, or a
         // `let`/`lam`-bound function value) carries its declared arg
         // modes on its `BinderState`. Prefer those over the global
         // table so `(app p h)` with `p` a local `(borrow …)` predicate
         // borrows `h` instead of consuming it. A local binder shadows a
         // global of the same name, which is the correct lexical scope.
-        if let Some(s) = self.binders.get(name) {
+        if let Some(s) = self.binders.get(&root) {
             if let Some(modes) = &s.fn_param_modes {
                 return modes.clone();
             }
@@ -1715,6 +1777,36 @@ mod tests {
         );
     }
 
+    /// 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:?}"
+        );
+    }
+
     /// Type-gating guard: a HEAP param (`List`) consumed twice in a ctor
     /// (`(term-ctor Pair Pair p0 p0)`) MUST still fire use-after-consume
     /// after the fix — the exemption is value-type-only, not blanket.

crates/ailang-check/tests/workspace.rs

@@ -725,7 +725,7 @@ fn borrow_own_demo_is_linearity_clean() {
 /// is active today) and were RED before the hardening (docs/specs/0063).
 #[test]
 fn harden_ownership_false_positives_are_clean() {
-    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof"] {
+    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias"] {
         let entry = examples_dir().join(format!("{name}.ail"));
         let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}"));
         let diags = check_workspace(&ws);

design/contracts/0008-memory-model.md

@@ -337,12 +337,15 @@ twice (double-free under a hypothetical Consume + scope-close).
   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).
-- Does not cover let-aliases of borrowed values. A let-binder
+- Covers let-aliases of borrowed values (spec 0064, class 2). A
-  whose value is `Term::Var` referencing a `Borrow`-mode
+  let-binder whose value is a bare `Term::Var` resolving to a
-  param is not yet propagated through; the param-mode gates
+  tracked binder is recorded as an alias to that root in the
-  treat such a binder as "owned" (its `current_param_modes`
+  linearity walk (`crates/ailang-check/src/linearity.rs`,
-  lookup misses, default = owned). This is a known carve-out
+  `Checker.aliases` + `resolve_alias`); the binding does not
-  shared by Iter A and the pre-tail-call shallow-dec arm; closing it is a propagation pass
+  consume the source, and every binder-state lookup resolves
-  through let-bindings that has not shipped yet.
+  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.
 
-Ratified by: `crates/ailang-check/src/uniqueness.rs`.
+Ratified by: `crates/ailang-check/src/uniqueness.rs`,
+`crates/ailang-check/src/linearity.rs`.

examples/c2_let_alias.ail

@@ -0,0 +1,14 @@
+(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))))))