AILang/docs/plans/0123-harden-ownership-part2-class1.md

# Harden ownership part 2 — iteration 2: local function-typed binder modes (class 1) — 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:** Resolve the parameter modes of a *local* function-typed
binder so applying a borrow-mode HOF predicate (`std_list.filter`'s
`p`) borrows its argument instead of consuming it, closing
false-positive class 1.

**Architecture:** `BinderState` gains `fn_param_modes:
Option<Vec<ParamMode>>`, seeded at every function-typed binder
introduction site — params and `lam`-params from their
locally-available signature type, `let`-binders from the
`LetBinderTypes` table built in iteration 1 (now on the `Checker`).
`callee_arg_modes`, for a local `Var` callee, returns the binder's
`fn_param_modes` before falling back to the global symbol table. The
existing `Term::App` arg-walk already maps a `Borrow` mode to a borrow
walk, so no App-arm change is needed. Diagnostic-only; no schema/type
change.

**Tech Stack:** `crates/ailang-check/src/linearity.rs` (the whole
fix), `examples/` fixture, `tests/workspace.rs` assertion.

**Scope:** SECOND iteration of spec 0064 — class 1 only. Out of scope
(later iterations): class 2 (alias-redirect map + contract 0008:340
update — `callee_arg_modes` resolves through aliases there, NOT here),
class 4 (`partition_eithers` rewrite). Iteration 1 already shipped the
table infrastructure + class 3. Do NOT add `Checker.aliases` or touch
`design/contracts/0008-memory-model.md` / `examples/std_either_list.ail`
here.

---

**Files this plan creates or modifies:**

- Create: `examples/c1_local_hof.ail` — class-1 RED→GREEN fixture
  (borrow-mode predicate param applied to a heap element reused in the
  kept `Cons`).
- Modify: `crates/ailang-check/src/linearity.rs` — `fn_modes_of`
  helper; `BinderState.fn_param_modes` field; seeding at the param loop
  (`:394`), `let` arm (`:531`), `lam` arm (`:610`); `callee_arg_modes`
  local-binder read (`:776`); a borrow-predicate test helper + two
  in-source unit tests.
- Test: `crates/ailang-check/tests/workspace.rs:728` — add
  `c1_local_hof` to `harden_ownership_false_positives_are_clean`.

---

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

**Files:**
- Create: `examples/c1_local_hof.ail`
- Test: `crates/ailang-check/tests/workspace.rs:728`

- [ ] **Step 1: Create the fixture**

Create `examples/c1_local_hof.ail` with exactly:

```ail
(module c1_local_hof
  (data Box
    (doc "heap cell")
    (ctor Box (con Int)))
  (data List
    (doc "boxed list of boxes")
    (ctor Nil)
    (ctor Cons (con Box) (con List)))
  (fn filter_box
    (doc "borrow-mode predicate p applied to h; h reused in the kept Cons")
    (type
      (fn-type
        (params (borrow (fn-type (params (borrow (con Box))) (ret (own (con Bool)))))
                (own (con List)))
        (ret (own (con List)))))
    (params p xs)
    (body
      (match xs
        (case (pat-ctor Nil) (term-ctor List Nil))
        (case (pat-ctor Cons h t)
          (if (app p h)
            (term-ctor List Cons h (app filter_box p t))
            (app filter_box p t)))))))
```

- [ ] **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"] {
```

to:

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

- [ ] **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 `c1_local_hof must be linearity-clean; got: [...]`
with a `use-after-consume` diagnostic on `h` in `filter_box`. The other
four fixtures stay clean; only `c1_local_hof` fails.

---

### Task 2: GREEN — `fn_param_modes` on `BinderState`, seeded at every introduction site, read by `callee_arg_modes`

**Files:**
- Modify: `crates/ailang-check/src/linearity.rs:342-348` (add
  `fn_modes_of` after `strip_forall`), `:199-216` (`BinderState`),
  `:393-403` (param loop), `:522-536` (`Term::Let`), `:599-623`
  (`Term::Lam`), `:776-820` (`callee_arg_modes`), plus the in-source
  test module.

- [ ] **Step 1: Add the `fn_modes_of` helper**

In `crates/ailang-check/src/linearity.rs`, immediately after the
`strip_forall` fn (which ends at `:348`), add:

```rust
/// Pull a function-typed value's declared parameter modes out of its
/// type, unwrapping a leading `forall`. Returns `None` for any
/// non-function type and for a fn-type with no explicit modes (legacy
/// all-implicit), so a caller that gets `None` falls back to the
/// global symbol table exactly as before.
fn fn_modes_of(t: &Type) -> Option<Vec<ParamMode>> {
    match strip_forall(t) {
        Type::Fn { param_modes, .. } if !param_modes.is_empty() => Some(param_modes.clone()),
        _ => None,
    }
}
```

- [ ] **Step 2: Add the `fn_param_modes` field to `BinderState`**

In `crates/ailang-check/src/linearity.rs`, the `struct BinderState`
(`:200-216`) ends with the `is_value: bool` field. Add after it:

```rust
    /// For a function-typed binder (a HOF predicate param, or a
    /// `let`/`lam`-bound function value), its declared parameter modes
    /// — so `callee_arg_modes` can resolve `(app p h)` where `p` is a
    /// local `(borrow …)` predicate and walk `h` as a borrow, not a
    /// consume. `None` for a non-function binder.
    fn_param_modes: Option<Vec<ParamMode>>,
```

(`BinderState` derives `Default` at `:199`; `Option<…>` defaults to
`None`, so every `..BinderState::default()` / `BinderState::default()`
construction site auto-fills it. Only the explicit literal in the param
loop, Step 3, must name the new field.)

- [ ] **Step 3: Seed `fn_param_modes` at the param loop**

In `crates/ailang-check/src/linearity.rs`, the param-seeding loop
(`:393-403`) builds an explicit `BinderState` literal. Replace:

```rust
        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),
        };
```

with (add the final field; the others are unchanged):

```rust
        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),
            fn_param_modes: param_tys.get(i).and_then(|t| fn_modes_of(t)),
        };
```

- [ ] **Step 4: Seed `fn_param_modes` at the `Term::Let` arm**

In `crates/ailang-check/src/linearity.rs`, the `Term::Let` arm
(`:522-536`) currently reads the table only for `is_value`. Replace:

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

with (read the teed type once, derive both flags from it):

```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);
                    },
                );
            }
```

- [ ] **Step 5: Seed `fn_param_modes` at the `Term::Lam` arm**

In `crates/ailang-check/src/linearity.rs`, the `Term::Lam` arm builds a
per-param `BinderState` at `:610-613`. Replace:

```rust
                    let st = BinderState {
                        is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
                        ..BinderState::default()
                    };
```

with:

```rust
                    let st = BinderState {
                        is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
                        fn_param_modes: param_tys.get(i).and_then(|t| fn_modes_of(t)),
                        ..BinderState::default()
                    };
```

- [ ] **Step 6: Read the local binder's modes in `callee_arg_modes`**

In `crates/ailang-check/src/linearity.rs`, `callee_arg_modes`
(`:776-820`) binds `name` from a `Term::Var` callee at `:777-780`, then
goes straight to `self.globals.get(name)` at `:783`. Insert, between the
`name` binding and the globals lookup (after the `let name = match …`
block closes, before `let ty = match self.globals.get(name)`):

```rust
        // 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(modes) = &s.fn_param_modes {
                return modes.clone();
            }
        }
```

- [ ] **Step 7: Build the crate (compile gate)**

Run: `cargo build -p ailang-check`
Expected: 0 errors. (Adding the `Option` field broke only the explicit
param-loop literal, fixed in Step 3; all other construction sites use
`..BinderState::default()`. The new field is read in Step 6, so no
dead-code warning.)

- [ ] **Step 8: Run the RED test from Task 1 — now GREEN**

First rebuild the CLI is not needed for the test (the test calls
`check_workspace` directly).
Run: `cargo test -p ailang-check --test workspace harden_ownership_false_positives_are_clean`
Expected: PASS — `c1_local_hof` is now linearity-clean (`(app p h)`
borrows `h` via `p`'s declared `(borrow …)` arg mode, so `h` is
reusable in the kept `Cons`), and the other four fixtures stay clean.

- [ ] **Step 9: Add the borrow-predicate test helper and two unit tests**

In `crates/ailang-check/src/linearity.rs`, in the `#[cfg(test)] mod
tests` block (alongside `fn_with_fn_param` at `:1426` and
`own_fn_param_applied_twice_is_clean` at `:1455`), add the helper and
two tests. The first test exercises the **param** seeding path (modes
from the signature, empty table); the second exercises the **`let`**
seeding path (modes from a hand-built `LetBinderTypes` table):

```rust
    /// fn f(p0: (borrow (List -> Bool, inner arg Borrow)), h: (own List)).
    /// The inner predicate's arg is `Borrow`, so applying `p0` to `h`
    /// borrows `h` (it stays reusable). Used by the class-1 tests.
    fn fn_with_borrow_pred_and_heap(name: &str, body: Term) -> Def {
        let list = Type::Con { name: "List".into(), args: vec![] };
        Def::Fn(FnDef {
            name: name.into(),
            ty: Type::Fn {
                params: vec![
                    Type::Fn {
                        params: vec![list.clone()],
                        param_modes: vec![ParamMode::Borrow],
                        ret: Box::new(Type::bool_()),
                        ret_mode: ParamMode::Own,
                        effects: vec![],
                    },
                    list.clone(),
                ],
                param_modes: vec![ParamMode::Borrow, ParamMode::Own],
                ret: Box::new(Type::int()),
                ret_mode: ParamMode::Own,
                effects: vec![],
            },
            params: vec!["p0".into(), "h".into()],
            body,
            suppress: vec![],
            doc: None,
            export: None,
        })
    }

    /// Class 1 (param path): a local borrow-mode predicate param `p0`
    /// applied to a heap binder `h` (`(seq (app p0 h) h)`) does NOT
    /// consume `h` — `p0`'s declared `(borrow …)` arg mode makes the
    /// application a borrow, so `h` is reusable. RED until the
    /// local-fn-param-mode resolution lands.
    #[test]
    fn borrow_fn_param_applied_does_not_consume_heap_arg() {
        let body = Term::Seq {
            lhs: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "p0".into() }),
                args: vec![Term::Var { name: "h".into() }],
                tail: false,
            }),
            rhs: Box::new(Term::Var { name: "h".into() }),
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            kernel: false,
            imports: vec![],
            defs: vec![fn_with_borrow_pred_and_heap("f", body)],
        };
        let diags = check_module(&m);
        assert!(
            !diags.iter().any(|d| d.code == "use-after-consume"),
            "applying a borrow-mode predicate param borrows its arg; got {diags:?}"
        );
    }

    /// Class 1 (let path): a `let`-bound function value whose type is
    /// teed as a `(borrow …)` predicate resolves its modes from the
    /// LetBinderTypes table — applying it to heap binder `h` borrows
    /// `h`. The let-value term is a trivial literal; the hand-built
    /// table is the unit under test.
    #[test]
    fn borrow_fn_let_binder_applied_does_not_consume_heap_arg() {
        let body = Term::Let {
            name: "g".into(),
            value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
            body: Box::new(Term::Seq {
                lhs: Box::new(Term::App {
                    callee: Box::new(Term::Var { name: "g".into() }),
                    args: vec![Term::Var { name: "p0".into() }],
                    tail: false,
                }),
                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 list = Type::Con { name: "List".into(), args: vec![] };
        let mut lbt = LetBinderTypes::new();
        lbt.insert(
            ("f".into(), "g".into()),
            Type::Fn {
                params: vec![list.clone()],
                param_modes: vec![ParamMode::Borrow],
                ret: Box::new(Type::bool_()),
                ret_mode: ParamMode::Own,
                effects: vec![],
            },
        );
        let diags = check_module_with_visible(&m, &[], &lbt);
        assert!(
            !diags.iter().any(|d| d.code == "use-after-consume"),
            "a let-bound borrow predicate borrows its arg via the teed modes; got {diags:?}"
        );
    }
```

(`fn_with_modes` at `:1403` builds a fn with `List`-typed params — here
`p0` is the `(own List)` heap binder applied to `g`. `Type::bool_()` /
`Type::int()` are the existing convenience constructors used elsewhere
in this test module.)

- [ ] **Step 10: Run the in-source linearity unit tests**

Run: `cargo test -p ailang-check --lib linearity::tests`
Expected: PASS — both new tests
(`borrow_fn_param_applied_does_not_consume_heap_arg`,
`borrow_fn_let_binder_applied_does_not_consume_heap_arg`) plus every
pre-existing linearity unit test (`own_fn_param_applied_twice_is_clean`,
`value_let_binder_multi_read_is_clean`,
`heap_let_binder_multi_read_still_errors`,
`heap_param_multi_consume_still_errors`, the `implicit_fn_is_exempt`
family, …) stay green.

- [ ] **Step 11: Full crate regression**

Run: `cargo test -p ailang-check`
Expected: PASS — the whole `ailang-check` suite green. The local-mode
read only fires for a tracked function-typed binder (a HOF param /
fn-valued `let`/`lam`); a global fn-ref callee is untracked and still
falls through to `self.globals`, so no existing outcome changes except
`c1_local_hof` flipping RED→GREEN.

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