plan: harden ownership analysis — is_value_type + value exemption + app-borrow (0120)

Executable projection of spec 0063 into four tasks: (1) is_value_type predicate in ailang-core::primitives; (2) application-is-a-borrow (Term::App callee walked Position::Borrow); (3) value-type exemption (BinderState.is_value seeded at param/pattern/lam sites, use_var short-circuit); (4) on-disk RED->GREEN fixtures + workspace assertions. Placeholder-free with exact code for every edit site. refs #56
2026-06-01 15:29:12 +02:00
parent 8cdac7ecef
commit 47fb328aca
1 changed files with 752 additions and 0 deletions
@@ -0,0 +1,752 @@
+# Harden the ownership analysis for universal activation — Implementation Plan
+
+> **Parent spec:** `docs/specs/0063-harden-ownership-analysis.md`
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use the
+> `implement` skill to run this plan. Steps use `- [ ]`
+> checkboxes for tracking.
+
+**Goal:** Make the linearity analysis (`crates/ailang-check/src/linearity.rs`) correct under universal activation by exempting value-type binders from consume-tracking and treating function application as a borrow, plus a new `is_value_type` predicate.
+
+**Architecture:** Two orthogonal additive changes inside `linearity.rs` (a value-type exemption gated on a per-binder `is_value` flag, and switching the `Term::App` callee walk from `Consume` to `Borrow`), plus one new shared predicate in `ailang-core::primitives`. No schema change, no hash reset, no codegen change. The analysis stays a pure diagnostic pass; the two existing diagnostic codes simply fire on a smaller, more correct set.
+
+**Tech Stack:** `ailang-core` (primitives predicate), `ailang-check` (linearity pass + in-source unit tests + on-disk fixture tests), `examples/` (`.ail` fixtures).
+
+---
+
+**Files this plan creates or modifies:**
+
+- Modify: `crates/ailang-core/src/primitives.rs` — add `is_value_type`; extend the `#[cfg(test)] mod tests` block.
+- Modify: `crates/ailang-check/src/linearity.rs` — `BinderState.is_value`; `Checker.ctors`; `type_is_value` + `collect_value_pattern_binders` helpers; param/pattern/lam seeding; `use_var` short-circuit; `Term::App` callee borrow; `merge_states` carry; in-source tests.
+- Create: `examples/fp_value.ail` — Class-1 value-type RED→GREEN fixture.
+- Create: `examples/fp_hof.ail` — Class-2a own-fn-param RED→GREEN fixture.
+- Create: `examples/fp_map.ail` — Class-2b borrow-fn-param RED→GREEN fixture.
+- Create: `examples/real_consume.ail` — must-stay-RED heap double-consume fixture.
+- Modify: `crates/ailang-check/tests/workspace.rs` — on-disk linearity assertions for the four fixtures.
+
+---
+
+## Task 1: `is_value_type` predicate
+
+**Files:**
+- Modify: `crates/ailang-core/src/primitives.rs`
+
+- [ ] **Step 1: Write the failing test**
+
+In `crates/ailang-core/src/primitives.rs`, inside the existing `#[cfg(test)] mod tests` block, add this test after `predicate_and_surface_name_agree`:
+
+```rust
+    /// `is_value_type` is the unboxed/no-RC subset of the primitives:
+    /// it agrees with `is_primitive_name` on every name EXCEPT `Str`,
+    /// which is a primitive zero-arity ctor but is heap-allocated
+    /// (`ptr`, RC'd) — see drop.rs:490-492.
+    #[test]
+    fn value_type_is_primitive_minus_str() {
+        for name in ["Int", "Bool", "Float", "Unit"] {
+            assert!(is_value_type(name), "{name} must be a value type");
+            assert!(is_primitive_name(name), "{name} must be a primitive");
+        }
+        // The sole divergence: Str is a primitive but NOT a value type.
+        assert!(!is_value_type("Str"), "Str is heap-allocated, not a value type");
+        assert!(is_primitive_name("Str"), "Str is still a primitive zero-arity ctor");
+        // Non-primitives are neither.
+        for name in ["List", "Foo", ""] {
+            assert!(!is_value_type(name));
+            assert!(!is_primitive_name(name));
+        }
+    }
+```
+
+- [ ] **Step 2: Run test to verify it fails**
+
+Run: `cargo test -p ailang-core value_type_is_primitive_minus_str`
+Expected: FAIL to compile — `cannot find function `is_value_type` in this scope`.
+
+- [ ] **Step 3: Write minimal implementation**
+
+In `crates/ailang-core/src/primitives.rs`, immediately after the closing `}` of `pub fn is_primitive_name`, insert:
+
+```rust
+/// Returns `true` iff `name` is an **unboxed value type** — no RC, no
+/// heap slab, copied by value. This is the `Str`-excluding subset of
+/// [`is_primitive_name`]: `Str` is a primitive zero-arity ctor but is
+/// heap-allocated (`ptr`, RC-`dec`'d — codegen `drop.rs:490-492` lowers
+/// only `Int`/`Bool`/`Float`/`Unit` to non-`ptr`). Used by the
+/// linearity analysis to exempt value-type binders from
+/// consume-tracking: a value type is never consumed, so multi-use is
+/// always legal.
+pub fn is_value_type(name: &str) -> bool {
+    matches!(name, "Int" | "Bool" | "Float" | "Unit")
+}
+```
+
+- [ ] **Step 4: Run test to verify it passes**
+
+Run: `cargo test -p ailang-core value_type_is_primitive_minus_str`
+Expected: PASS.
+
+---
+
+## Task 2: Application is a borrow
+
+**Files:**
+- Modify: `crates/ailang-check/src/linearity.rs` (`Term::App` arm at `:430-433`; in-source tests)
+
+- [ ] **Step 1: Write the failing test**
+
+In `crates/ailang-check/src/linearity.rs`, inside `#[cfg(test)] mod tests`, add a helper (after `fn_with_modes`, near `:1315`) and a test. The helper builds a fn with a single function-typed param `p0 : (mode (Int -> Int))` returning Int:
+
+```rust
+    /// A fn with one function-typed param `p0 : (mode (Int -> Int))`,
+    /// returning Int. Used to exercise HOF application linearity.
+    fn fn_with_fn_param(name: &str, mode: ParamMode, body: Term) -> Def {
+        Def::Fn(FnDef {
+            name: name.into(),
+            ty: Type::Fn {
+                params: vec![Type::Fn {
+                    params: vec![Type::int()],
+                    param_modes: vec![ParamMode::Own],
+                    ret: Box::new(Type::int()),
+                    ret_mode: ParamMode::Own,
+                    effects: vec![],
+                }],
+                param_modes: vec![mode],
+                ret: Box::new(Type::int()),
+                ret_mode: ParamMode::Implicit,
+                effects: vec![],
+            },
+            params: vec!["p0".into()],
+            body,
+            suppress: vec![],
+            doc: None,
+            export: None,
+        })
+    }
+
+    /// Applying a function param more than once is a borrow each time,
+    /// not a consume: `(app p0 (app p0 0))` must NOT fire
+    /// use-after-consume. (Today the App callee is walked Consume, so
+    /// the first application consumes `p0` and the second fires
+    /// use-after-consume — this test is RED until Fix 2.)
+    #[test]
+    fn own_fn_param_applied_twice_is_clean() {
+        let body = Term::App {
+            callee: Box::new(Term::Var { name: "p0".into() }),
+            args: vec![Term::App {
+                callee: Box::new(Term::Var { name: "p0".into() }),
+                args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
+                tail: false,
+            }],
+            tail: false,
+        };
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            kernel: false,
+            imports: vec![],
+            defs: vec![fn_with_fn_param("f", ParamMode::Own, body)],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| d.code == "use-after-consume"),
+            "applying a function param is a borrow, not a consume; got {diags:?}"
+        );
+    }
+```
+
+- [ ] **Step 2: Run test to verify it fails**
+
+Run: `cargo test -p ailang-check own_fn_param_applied_twice_is_clean`
+Expected: FAIL — assertion fires; a `use-after-consume` diagnostic is present (the App callee is walked in `Position::Consume` today).
+
+- [ ] **Step 3: Write minimal implementation**
+
+In `crates/ailang-check/src/linearity.rs`, in the `Term::App { callee, args, .. }` arm (`:430-433`), change the callee walk. Replace:
+
+```rust
+            Term::App { callee, args, .. } => {
+                // The callee itself is consumed (it's "the function value");
+                // for var-callees this is typically a global fn ref.
+                self.walk(callee, Position::Consume);
+```
+
+with:
+
+```rust
+            Term::App { callee, args, .. } => {
+                // Applying a function value READS it (a borrow): the value
+                // stays live for further applications and is dropped at
+                // scope close like any other binder. For a global fn-ref
+                // callee this is a no-op (globals are untracked, so
+                // `use_var` returns early either way); for a tracked
+                // function-typed binder (a HOF param) it stops application
+                // from consuming the binder. The `consumed` check still
+                // runs in Borrow position, so applying an already-consumed
+                // function value still fires use-after-consume.
+                self.walk(callee, Position::Borrow);
+```
+
+- [ ] **Step 4: Run test to verify it passes**
+
+Run: `cargo test -p ailang-check own_fn_param_applied_twice_is_clean`
+Expected: PASS.
+
+---
+
+## Task 3: Value-type exemption
+
+**Files:**
+- Modify: `crates/ailang-check/src/linearity.rs` (`BinderState` `:181-192`; `Checker` `:408-420`; `Checker` literal `:351-356`; param install `:361-370`; `walk_arm` `:638-652`; `Term::Lam` `:541-560`; `use_var` `:683-690`; `merge_states` `:781-787`; new helpers; in-source tests)
+
+- [ ] **Step 1: Write the failing tests**
+
+In `crates/ailang-check/src/linearity.rs`, inside `#[cfg(test)] mod tests`, add a helper and three tests:
+
+```rust
+    /// A fn with one `(own (con Int))` value-type param `p0`, returning
+    /// Int. Used to exercise the value-type exemption.
+    fn fn_with_int_own(name: &str, body: Term) -> Def {
+        Def::Fn(FnDef {
+            name: name.into(),
+            ty: Type::Fn {
+                params: vec![Type::Con { name: "Int".into(), args: vec![] }],
+                param_modes: vec![ParamMode::Own],
+                ret: Box::new(Type::int()),
+                ret_mode: ParamMode::Implicit,
+                effects: vec![],
+            },
+            params: vec!["p0".into()],
+            body,
+            suppress: vec![],
+            doc: None,
+            export: None,
+        })
+    }
+
+    /// A value-type param read in two consume positions
+    /// (`(seq p0 p0)`) must NOT fire use-after-consume: an `Int` has no
+    /// refcount and is never consumed. RED until Fix 1.
+    #[test]
+    fn value_param_multi_read_is_clean() {
+        let body = Term::Seq {
+            lhs: Box::new(Term::Var { name: "p0".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_int_own("f", body)],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| d.code == "use-after-consume"),
+            "a value-type param is never consumed; multi-read is legal; 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.
+    /// (Green today and after the fix; a regression guard, not RED-first.)
+    #[test]
+    fn heap_param_multi_consume_still_errors() {
+        let body = Term::Ctor {
+            type_name: "Pair".into(),
+            ctor: "Pair".into(),
+            args: vec![
+                Term::Var { name: "p0".into() },
+                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"),
+            "a heap param consumed twice must still error; got {diags:?}"
+        );
+    }
+
+    /// A borrow function param applied AND passed (the recursive-HOF
+    /// shape `map_int`) must be clean: application is a borrow, and the
+    /// param starts borrowed, so neither use-after-consume nor
+    /// consume-while-borrowed should fire. Covered by Fix 2 (App
+    /// borrow); this asserts the borrow-param variant. RED until Fix 2.
+    #[test]
+    fn borrow_fn_param_applied_is_clean() {
+        let body = Term::App {
+            callee: Box::new(Term::Var { name: "p0".into() }),
+            args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
+            tail: false,
+        };
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            kernel: false,
+            imports: vec![],
+            defs: vec![fn_with_fn_param("f", ParamMode::Borrow, body)],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| {
+                d.code == "use-after-consume" || d.code == "consume-while-borrowed"
+            }),
+            "applying a borrow function param is a clean read; got {diags:?}"
+        );
+    }
+```
+
+- [ ] **Step 2: Run tests to verify they fail (the RED ones) / pass (the guard)**
+
+Run: `cargo test -p ailang-check value_param_multi_read_is_clean heap_param_multi_consume_still_errors borrow_fn_param_applied_is_clean`
+Expected: `value_param_multi_read_is_clean` FAILS (use-after-consume fires today); `borrow_fn_param_applied_is_clean` PASSES (already fixed by Task 2's App-borrow change); `heap_param_multi_consume_still_errors` PASSES (regression guard, green today).
+
+- [ ] **Step 3a: Add the `is_value` field to `BinderState`**
+
+Replace the `BinderState` struct (`:181-192`):
+
+```rust
+#[derive(Debug, Default, Clone)]
+struct BinderState {
+    /// `true` once the binder has been used in a Consume position.
+    /// Subsequent uses (in any position) trigger `use-after-consume`.
+    consumed: bool,
+    /// Number of currently-live borrows of this binder. ...
+    borrow_count: u32,
+}
+```
+
+with (keep the existing doc comments on `consumed`/`borrow_count` verbatim; only the field is added):
+
+```rust
+#[derive(Debug, Default, Clone)]
+struct BinderState {
+    /// `true` once the binder has been used in a Consume position.
+    /// Subsequent uses (in any position) trigger `use-after-consume`.
+    consumed: bool,
+    /// Number of currently-live borrows of this binder. Incremented
+    /// when a Borrow-position use starts (in a fn-call arg slot or as
+    /// the initial state of a `Borrow` parameter); decremented when
+    /// the borrow ends. Consume while `> 0` triggers
+    /// `consume-while-borrowed`.
+    borrow_count: u32,
+    /// `true` if this binder has an unboxed value type
+    /// (`Int`/`Bool`/`Float`/`Unit`). A value type has no refcount and
+    /// is never consumed, so `use_var` skips all consume bookkeeping
+    /// for it. Invariant per binder; set at the introduction site
+    /// (param / pattern / lam) where the type is locally available.
+    is_value: bool,
+}
+```
+
+- [ ] **Step 3b: Add the type-is-value helper**
+
+In `crates/ailang-check/src/linearity.rs`, immediately after the `is_heap_type` function (`:164`), add:
+
+```rust
+/// `true` iff `t` is an unboxed value type (`Int`/`Bool`/`Float`/`Unit`).
+/// The `Str`-excluding counterpart of `is_heap_type`'s primitive check —
+/// see `ailang_core::primitives::is_value_type`.
+fn type_is_value(t: &Type) -> bool {
+    matches!(t, Type::Con { name, .. } if ailang_core::primitives::is_value_type(name))
+}
+```
+
+- [ ] **Step 3c: Add the `ctors` field to `Checker` and the value-binder pattern helper**
+
+Replace the `Checker` struct field list (`:408-420`) — add the `ctors` field after `def_name`:
+
+```rust
+struct Checker<'a> {
+    /// Top-level symbol → type. Used to look up the param_modes of an
+    /// `App` callee that resolves to a global fn def.
+    globals: &'a HashMap<String, Type>,
+    /// Diagnostic accumulator (shared with the module-level walk).
+    diags: &'a mut Vec<Diagnostic>,
+    /// Name of the fn currently being checked (becomes
+    /// [`Diagnostic::def`]).
+    def_name: &'a str,
+    /// ctor name → field types. Used to type pattern binders so a
+    /// value-typed sub-binder (`Cons(h, t)` with `h: Int`) is exempted
+    /// from consume-tracking. Mirrors the `ctors` map built in
+    /// `check_module_with_visible`.
+    ctors: &'a HashMap<String, Vec<Type>>,
+    /// Live binder state, keyed by name. Modified in place; lexical
+    /// scoping is restored by [`Checker::with_binder`].
+    binders: HashMap<String, BinderState>,
+}
+```
+
+Then add this free function after `collect_pattern_binders` (`:775`):
+
+```rust
+/// Collect the names of pattern binders that have an unboxed value
+/// type, by walking the pattern alongside the ctor field types.
+/// Mirrors `pattern_has_consumed_heap_binder_at`'s descent: a
+/// `Pattern::Var` directly under a ctor field of value type is added;
+/// a top-level `Pattern::Var` (whole-scrutinee binder, `declared_ty ==
+/// None`) is conservatively treated as heap and never added.
+fn collect_value_pattern_binders(
+    pat: &Pattern,
+    declared_ty: Option<&Type>,
+    ctors: &HashMap<String, Vec<Type>>,
+    out: &mut Vec<String>,
+) {
+    match pat {
+        Pattern::Wild | Pattern::Lit { .. } => {}
+        Pattern::Var { name } => {
+            if let Some(t) = declared_ty {
+                if type_is_value(t) {
+                    out.push(name.clone());
+                }
+            }
+        }
+        Pattern::Ctor { ctor, fields } => {
+            let field_tys: &[Type] = ctors.get(ctor).map(|v| v.as_slice()).unwrap_or(&[]);
+            for (i, f) in fields.iter().enumerate() {
+                collect_value_pattern_binders(f, field_tys.get(i), ctors, out);
+            }
+        }
+    }
+}
+```
+
+- [ ] **Step 3d: Wire `ctors` into the `Checker` literal and seed param `is_value`**
+
+Replace the `Checker` construction + param install loop in `check_fn` (`:351-370`):
+
+```rust
+    let mut checker = Checker {
+        globals,
+        diags,
+        def_name: &f.name,
+        binders: HashMap::new(),
+    };
+
+    // Install fn parameters as binders, with initial `borrow_count = 1`
+    // for `Borrow` params (the caller's outer borrow stays live for the
+    // body's whole duration) and `0` for `Own` params.
+    for (name, mode) in f.params.iter().zip(param_modes.iter()) {
+        let initial = BinderState {
+            consumed: false,
+            borrow_count: match mode {
+                ParamMode::Borrow => 1,
+                ParamMode::Own | ParamMode::Implicit => 0,
+            },
+        };
+        checker.binders.insert(name.clone(), initial);
+    }
+```
+
+with:
+
+```rust
+    let mut checker = Checker {
+        globals,
+        diags,
+        def_name: &f.name,
+        ctors,
+        binders: HashMap::new(),
+    };
+
+    // Install fn parameters as binders, with initial `borrow_count = 1`
+    // for `Borrow` params (the caller's outer borrow stays live for the
+    // body's whole duration) and `0` for `Own` params. A value-type
+    // param starts `is_value = true` and is exempt from consume-tracking.
+    for (i, (name, mode)) in f.params.iter().zip(param_modes.iter()).enumerate() {
+        let initial = BinderState {
+            consumed: false,
+            borrow_count: match mode {
+                ParamMode::Borrow => 1,
+                ParamMode::Own | ParamMode::Implicit => 0,
+            },
+            is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
+        };
+        checker.binders.insert(name.clone(), initial);
+    }
+```
+
+- [ ] **Step 3e: Seed `is_value` for pattern binders in `walk_arm`**
+
+Replace the binder-install loop in `walk_arm` (`:638-644`):
+
+```rust
+    fn walk_arm(&mut self, arm: &Arm, pos: Position) {
+        let names = collect_pattern_binders(&arm.pat);
+        let mut saved: HashMap<String, Option<BinderState>> = HashMap::new();
+        for n in &names {
+            saved.insert(n.clone(), self.binders.remove(n));
+            self.binders.insert(n.clone(), BinderState::default());
+        }
+```
+
+with:
+
+```rust
+    fn walk_arm(&mut self, arm: &Arm, pos: Position) {
+        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 st = BinderState {
+                is_value: value_names.contains(n),
+                ..BinderState::default()
+            };
+            self.binders.insert(n.clone(), st);
+        }
+```
+
+- [ ] **Step 3f: Seed `is_value` for lam params in `Term::Lam`**
+
+Replace the `Term::Lam` arm's destructure and param-install loop (`:541-552`):
+
+```rust
+            Term::Lam { params, body, .. } => {
+                // Lam captures cross the linearity boundary: any free
+                // var of the body is implicitly consumed by closure
+                // construction (we don't yet model captured-borrow
+                // discipline; that is 18c.3 territory). For 18c.2 we
+                // walk the body with the lam's own params as fresh
+                // binders.
+                let mut saved_for_params: HashMap<String, Option<BinderState>> = HashMap::new();
+                for p in params {
+                    saved_for_params.insert(p.clone(), self.binders.remove(p));
+                    self.binders.insert(p.clone(), BinderState::default());
+                }
+```
+
+with:
+
+```rust
+            Term::Lam { params, param_tys, body, .. } => {
+                // Lam captures cross the linearity boundary: any free
+                // var of the body is implicitly consumed by closure
+                // construction (we don't yet model captured-borrow
+                // discipline; that is 18c.3 territory). For 18c.2 we
+                // walk the body with the lam's own params as fresh
+                // binders; a value-typed lam param is exempt from
+                // consume-tracking.
+                let mut saved_for_params: HashMap<String, Option<BinderState>> = HashMap::new();
+                for (i, p) in params.iter().enumerate() {
+                    saved_for_params.insert(p.clone(), self.binders.remove(p));
+                    let st = BinderState {
+                        is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
+                        ..BinderState::default()
+                    };
+                    self.binders.insert(p.clone(), st);
+                }
+```
+
+- [ ] **Step 3g: Short-circuit the consume arm in `use_var`**
+
+Replace the `Position::Consume` arm in `use_var` (`:683-690`):
+
+```rust
+            Position::Consume => {
+                if state.borrow_count > 0 {
+                    self.diags
+                        .push(make_consume_while_borrowed(self.def_name, name));
+                    return;
+                }
+                state.consumed = true;
+            }
+```
+
+with:
+
+```rust
+            Position::Consume => {
+                // A value type has no refcount and is never consumed;
+                // multi-use in any position is legal.
+                if state.is_value {
+                    return;
+                }
+                if state.borrow_count > 0 {
+                    self.diags
+                        .push(make_consume_while_borrowed(self.def_name, name));
+                    return;
+                }
+                state.consumed = true;
+            }
+```
+
+- [ ] **Step 3h: Carry `is_value` through `merge_states`**
+
+Replace `merge_states` (`:781-787`):
+
+```rust
+fn merge_states(into: &mut HashMap<String, BinderState>, other: &HashMap<String, BinderState>) {
+    for (name, s) in other {
+        let entry = into.entry(name.clone()).or_default();
+        entry.consumed = entry.consumed || s.consumed;
+        entry.borrow_count = entry.borrow_count.max(s.borrow_count);
+    }
+}
+```
+
+with (add the `is_value` carry — invariant per binder, but `or_default()` would otherwise reset a value binder present only in `other` to `false`):
+
+```rust
+fn merge_states(into: &mut HashMap<String, BinderState>, other: &HashMap<String, BinderState>) {
+    for (name, s) in other {
+        let entry = into.entry(name.clone()).or_default();
+        entry.consumed = entry.consumed || s.consumed;
+        entry.borrow_count = entry.borrow_count.max(s.borrow_count);
+        // is_value is invariant per binder; the OR recovers it when the
+        // binder reached `into` via a fresh `or_default()`.
+        entry.is_value = entry.is_value || s.is_value;
+    }
+}
+```
+
+- [ ] **Step 4: Build and run the linearity tests**
+
+Run: `cargo build -p ailang-check`
+Expected: 0 errors (every `BinderState` / `Checker` literal compiles; the `..Default::default()` tail and the explicit `is_value` field cover all sites).
+
+Run: `cargo test -p ailang-check value_param_multi_read_is_clean heap_param_multi_consume_still_errors borrow_fn_param_applied_is_clean own_fn_param_applied_twice_is_clean`
+Expected: all PASS.
+
+---
+
+## Task 4: On-disk fixtures and assertions
+
+**Files:**
+- Create: `examples/fp_value.ail`, `examples/fp_hof.ail`, `examples/fp_map.ail`, `examples/real_consume.ail`
+- Modify: `crates/ailang-check/tests/workspace.rs`
+
+- [ ] **Step 1: Create the four fixtures**
+
+Create `examples/fp_value.ail`:
+
+```ail
+(module fp_value
+  (fn sum_explicit
+    (doc "value-type param read multiple times")
+    (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
+    (params n)
+    (body (if (app eq n 0) 0 (app + n (app sum_explicit (app - n 1))))))
+  (fn main
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
+    (params)
+    (body (app print (app sum_explicit 10)))))
+```
+
+Create `examples/fp_hof.ail`:
+
+```ail
+(module fp_hof
+  (fn apply_thrice
+    (doc "apply a function param three times")
+    (type (fn-type
+            (params (own (fn-type (params (own (con Int))) (ret (own (con Int))))) (own (con Int)))
+            (ret (own (con Int)))))
+    (params f x)
+    (body (app f (app f (app f x)))))
+  (fn main
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
+    (params)
+    (body (app print (app apply_thrice (lam (params (typed y (con Int))) (ret (con Int)) (body (app + y 1))) 0)))))
+```
+
+Create `examples/fp_map.ail`:
+
+```ail
+(module fp_map
+  (data IntList
+    (doc "boxed list")
+    (ctor Nil)
+    (ctor Cons (con Int) (con IntList)))
+  (fn map_int
+    (doc "recursive HOF: f applied AND passed to the recursive call")
+    (type (fn-type
+            (params (borrow (fn-type (params (own (con Int))) (ret (own (con Int))))) (own (con IntList)))
+            (ret (own (con IntList)))))
+    (params f xs)
+    (body (match xs
+      (case (pat-ctor Nil) (term-ctor IntList Nil))
+      (case (pat-ctor Cons h t) (term-ctor IntList Cons (app f h) (app map_int f t)))))))
+```
+
+Create `examples/real_consume.ail`:
+
+```ail
+(module real_consume
+  (data Box
+    (doc "heap cell")
+    (ctor Box (con Int)))
+  (data Pair
+    (doc "two boxes")
+    (ctor Pair (con Box) (con Box)))
+  (fn dup
+    (doc "MUST STAY an error: a heap param consumed twice without clone")
+    (type (fn-type (params (own (con Box))) (ret (own (con Pair)))))
+    (params b)
+    (body (term-ctor Pair Pair b b))))
+```
+
+- [ ] **Step 2: Verify the fixtures check clean / error as designed**
+
+Run: `cargo build -p ail && for f in fp_value fp_hof fp_map real_consume; do echo "== $f =="; ./target/debug/ail check examples/$f.ail; echo "exit=$?"; done`
+Expected: `fp_value`, `fp_hof`, `fp_map` each exit 0 (clean, post-fix); `real_consume` exits 1 with `[use-after-consume] dup: \`b\` is used after it was already consumed`.
+
+- [ ] **Step 3: Add the on-disk assertions**
+
+In `crates/ailang-check/tests/workspace.rs`, append after `borrow_own_demo_is_linearity_clean` (`:720`):
+
+```rust
+/// #56 Fix 1+2: under universal activation the linearity analysis must
+/// not false-fire on value-type params or on applied function params.
+/// These three fixtures use explicit-mode signatures (so the analysis
+/// 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"] {
+        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);
+        let lin: Vec<&ailang_check::Diagnostic> = diags
+            .iter()
+            .filter(|d| d.code == "use-after-consume" || d.code == "consume-while-borrowed")
+            .collect();
+        assert!(lin.is_empty(), "{name} must be linearity-clean; got: {lin:#?}");
+    }
+}
+
+/// #56 type-gating: the exemption is value-type-only. A heap param
+/// consumed twice (`real_consume.dup`, `(term-ctor Pair Pair b b)`) MUST
+/// still fire use-after-consume — proving the fix did not blanket-silence
+/// genuine multi-consume.
+#[test]
+fn harden_ownership_heap_double_consume_still_errors() {
+    let entry = examples_dir().join("real_consume.ail");
+    let ws = load_workspace(&entry).expect("load real_consume");
+    let diags = check_workspace(&ws);
+    assert!(
+        diags.iter().any(|d| d.code == "use-after-consume"),
+        "real_consume.dup must still fire use-after-consume; got: {diags:#?}"
+    );
+}
+```
+
+- [ ] **Step 4: Run the on-disk assertions**
+
+Run: `cargo test -p ailang-check --test workspace harden_ownership`
+Expected: both `harden_ownership_false_positives_are_clean` and `harden_ownership_heap_double_consume_still_errors` PASS.
+
+- [ ] **Step 5: Full workspace regression**
+
+Run: `cargo test --workspace`
+Expected: PASS (no regressions; per the typed-MIR re-synth strictness memory, the whole suite is the net, not just e2e).
+
+Run: `python3 bench/check.py && python3 bench/compile_check.py`
+Expected: both report clean (the analysis is diagnostic-only; no compile-baseline shift expected).