fix(check): inherit borrow on heap sub-binders of a borrowed scrutinee (#58)

The strict linearity check accepted consuming a heap-typed pattern
sub-binder extracted from a `(borrow)`-mode match scrutinee. The
sub-binder aliases the caller-owned interior, so moving it into an
`(own)` slot double-frees at runtime (SIGSEGV) — `ail check` returned
exit 0, `ail build`+run crashed. A pre-existing hole the corpus never
exercised; the #55 cutover's universal activation of the strict check
exposed it (sibling to the #57 / spec 0064 class-2 let-alias-of-borrow
hardening — this is the pattern-sub-binder analog).

Root: `walk_arm` seeded every pattern sub-binder with
`borrow_count = 0` (freely consumable), bypassing the `Borrow`-param
seeding in `check_fn` that starts a borrowed param at `borrow_count = 1`.
The whole-param consume was caught (cut55_2d, correctly rejected); the
moved-out heap sub-binder was not.

Fix: in `Term::Match`, resolve the scrutinee through `resolve_alias`
and record whether it is a borrowed binder; thread that into `walk_arm`,
which now seeds a heap-typed (`!is_value`) sub-binder of a borrowed
scrutinee with `borrow_count = 1`. Value-typed sub-binders (e.g. the
`Int` head) stay at `0` — copied out, no heap alias. Nested matches fall
out for free: the inner match re-derives borrowed status from the
borrow-carrying sub-binder.

Rejected alternative: forcing fieldtest fixture cut55_2b to also reject.
2b is a clean borrow-traversal — `bump`'s recursive param is `(borrow)`,
so the tail `t` is only borrowed, never consumed into an `(own)` slot.
Distorting the fix to reject it would be unsound (false positive on
legitimate borrow-rebuild). The fixture's own comment misdescribed its
recursive param as `(own)`; the code says `(borrow)`.

Verification:
- RED test linearity::tests::consume_heap_sub_binder_of_borrow_scrutinee_is_rejected:
  was left:0 right:1 (check returned []), now green.
- Full workspace: 732 passed / 0 failed (was 731; +1 the new test). No
  committed corpus newly rejected by the sharper check.
- fieldtest repro cut55_2c: exit 0 (wrongly accepted) -> exit 1
  (consume-while-borrowed on `t`).

closes #58

crates/ailang-check/src/linearity.rs

@@ -629,11 +629,28 @@ impl<'a> Checker<'a> {
             Term::Match { scrutinee, arms } => {
                 // Scrutinee is read (Borrow), not moved.
                 self.walk(scrutinee, Position::Borrow);
+                // Determine whether the scrutinee is a borrowed binder:
+                // a bare `Var` resolving (through `let`-aliases) to a
+                // tracked binder whose `borrow_count > 0`. A heap-typed
+                // sub-binder extracted from a borrowed scrutinee aliases
+                // the caller-owned interior, so it must inherit the
+                // borrow (mirroring the `Borrow`-param seeding in
+                // `check_fn`). Any non-`Var` scrutinee is owned/fresh.
+                let scrutinee_borrowed = match scrutinee.as_ref() {
+                    Term::Var { name } => {
+                        let root = self.resolve_alias(name);
+                        self.binders
+                            .get(&root)
+                            .map(|s| s.borrow_count > 0)
+                            .unwrap_or(false)
+                    }
+                    _ => false,
+                };
                 let saved = self.binders.clone();
                 let mut acc: Option<HashMap<String, BinderState>> = None;
                 for arm in arms {
                     self.binders = saved.clone();
-                    self.walk_arm(arm, pos);
+                    self.walk_arm(arm, pos, scrutinee_borrowed);
                     match acc.as_mut() {
                         None => acc = Some(self.binders.clone()),
                         Some(m) => merge_states(m, &self.binders),
@@ -770,15 +787,23 @@ impl<'a> Checker<'a> {
     /// are linearity-fresh in 18c.2; we do not yet track ownership
     /// transfer from the scrutinee (that requires modelling pattern
     /// borrow vs. consume, which is 18c.3 work).
-    fn walk_arm(&mut self, arm: &Arm, pos: Position) {
+    fn walk_arm(&mut self, arm: &Arm, pos: Position, scrutinee_borrowed: bool) {
         let names = collect_pattern_binders(&arm.pat);
         let mut value_names: Vec<String> = Vec::new();
         collect_value_pattern_binders(&arm.pat, None, self.ctors, &mut value_names);
         let mut saved: HashMap<String, Option<BinderState>> = HashMap::new();
         for n in &names {
             saved.insert(n.clone(), self.binders.remove(n));
+            let is_value = value_names.contains(n);
             let st = BinderState {
-                is_value: value_names.contains(n),
+                is_value,
+                // A heap-typed sub-binder of a borrowed scrutinee aliases
+                // the caller-owned interior; seed `borrow_count = 1` so
+                // consuming it fires `consume-while-borrowed`, mirroring
+                // the `Borrow`-param seeding in `check_fn`. Value-typed
+                // sub-binders (e.g. `Int h`) are copied out — no heap
+                // alias — so they stay freely consumable at `0`.
+                borrow_count: if scrutinee_borrowed && !is_value { 1 } else { 0 },
                 ..BinderState::default()
             };
             self.binders.insert(n.clone(), st);
@@ -2239,6 +2264,152 @@ mod tests {
         );
     }
 
+    /// helper: a fn `sink : (own IntList) -> Int` whose only role is
+    /// to give an `(own)` arg slot for a consume. Its body matches and
+    /// moves out the heap-typed tail (`match ys { Cons(_, t) => sink(t),
+    /// Nil => 0 }`) so the sink genuinely consumes its `(own)` param —
+    /// no spurious `over-strict-mode` warning on `sink` itself to
+    /// confound the test.
+    fn fn_sink_own_intlist(name: &str) -> Def {
+        let body = Term::Match {
+            scrutinee: Box::new(Term::Var { name: "ys".into() }),
+            arms: vec![
+                Arm {
+                    pat: Pattern::Ctor { ctor: "Nil".into(), fields: vec![] },
+                    body: Term::Lit { lit: Literal::Int { value: 0 } },
+                },
+                Arm {
+                    pat: Pattern::Ctor {
+                        ctor: "Cons".into(),
+                        fields: vec![
+                            Pattern::Wild,
+                            Pattern::Var { name: "rest".into() },
+                        ],
+                    },
+                    body: Term::App {
+                        callee: Box::new(Term::Var { name: name.to_string() }),
+                        args: vec![Term::Var { name: "rest".into() }],
+                        tail: false,
+                    },
+                },
+            ],
+        };
+        Def::Fn(FnDef {
+            name: name.into(),
+            ty: Type::Fn {
+                params: vec![Type::Con { name: "IntList".into(), args: vec![] }],
+                param_modes: vec![ParamMode::Own],
+                ret: Box::new(Type::int()),
+                ret_mode: ParamMode::Own,
+                effects: vec![],
+            },
+            params: vec!["ys".into()],
+            body,
+            suppress: vec![],
+            doc: None,
+            export: None,
+        })
+    }
+
+    /// helper: a fn whose single param is `(borrow IntList)` and whose
+    /// body is `body`. The borrow param starts the walk with
+    /// `borrow_count = 1`, so any in-body consume of `xs` — or of a
+    /// heap sub-binder extracted from `xs` — must fire
+    /// `consume-while-borrowed`.
+    fn fn_borrow_intlist(name: &str, body: Term) -> Def {
+        Def::Fn(FnDef {
+            name: name.into(),
+            ty: Type::Fn {
+                params: vec![Type::Con { name: "IntList".into(), args: vec![] }],
+                param_modes: vec![ParamMode::Borrow],
+                ret: Box::new(Type::int()),
+                ret_mode: ParamMode::Own,
+                effects: vec![],
+            },
+            params: vec!["xs".into()],
+            body,
+            suppress: vec![],
+            doc: None,
+            export: None,
+        })
+    }
+
+    /// SOUNDNESS PROPERTY (#58): a heap-typed pattern sub-binder
+    /// extracted from a `(borrow)`-mode match scrutinee inherits the
+    /// scrutinee's borrowed status, so consuming it must fire
+    /// `consume-while-borrowed`.
+    ///
+    /// `leak : (borrow IntList)` matches `xs` and, in the `Cons(h, t)`
+    /// arm, passes the heap-typed tail `t` to `sink`, an
+    /// `(own IntList)` sink. `t` aliases the interior of the
+    /// caller-owned, only-borrowed `xs`; moving it into an `(own)`
+    /// param double-frees at runtime (SIGSEGV). The linearity pass
+    /// already rejects consuming the *whole* borrowed param (sibling
+    /// fixture `cut55_2d`), but here the sub-binder `t` is seeded as a
+    /// fresh `BinderState` with `borrow_count = 0`, so the consume goes
+    /// unflagged.
+    ///
+    /// RED today: `check_module` returns no `consume-while-borrowed`
+    /// diagnostic. The primitive sub-binder `h` (`Int`) is correctly
+    /// exempt (copied out, no heap alias); the bug is specific to the
+    /// heap-typed `t`.
+    #[test]
+    fn consume_heap_sub_binder_of_borrow_scrutinee_is_rejected() {
+        // leak body: (match xs
+        //   ((pat-ctor Nil) 0)
+        //   ((pat-ctor Cons (pat-var h) (pat-var t)) (app sink t)))
+        let body = Term::Match {
+            scrutinee: Box::new(Term::Var { name: "xs".into() }),
+            arms: vec![
+                Arm {
+                    pat: Pattern::Ctor { ctor: "Nil".into(), fields: vec![] },
+                    body: Term::Lit { lit: Literal::Int { value: 0 } },
+                },
+                Arm {
+                    pat: Pattern::Ctor {
+                        ctor: "Cons".into(),
+                        fields: vec![
+                            Pattern::Var { name: "h".into() },
+                            Pattern::Var { name: "t".into() },
+                        ],
+                    },
+                    body: Term::App {
+                        callee: Box::new(Term::Var { name: "sink".into() }),
+                        args: vec![Term::Var { name: "t".into() }],
+                        tail: false,
+                    },
+                },
+            ],
+        };
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            kernel: false,
+            imports: vec![],
+            defs: vec![
+                intlist_typedef(),
+                fn_sink_own_intlist("sink"),
+                fn_borrow_intlist("leak", body),
+            ],
+        };
+        let diags = check_module(&m);
+        let cwb: Vec<_> = diags
+            .iter()
+            .filter(|d| d.code == "consume-while-borrowed" && d.def.as_deref() == Some("leak"))
+            .collect();
+        assert_eq!(
+            cwb.len(),
+            1,
+            "consuming the heap-typed tail `t` of a borrowed scrutinee must fire \
+             consume-while-borrowed (it aliases caller-owned heap → double-free); got {diags:?}"
+        );
+        assert_eq!(
+            cwb[0].ctx,
+            serde_json::json!({ "binder": "t" }),
+            "the diagnostic must name the consumed sub-binder `t`; got {diags:?}"
+        );
+    }
+
     /// RED (over-strict-mode FP on ctor-rebuild): a `State(Float,
     /// Int)` ADT def. Both fields are primitive — the lint's
     /// `pattern_has_consumed_heap_binder` filters them out — yet a