From 2ad58ada1760429ed6fc591698b8c8930e8839ab Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 17:51:23 +0200 Subject: [PATCH] =?UTF-8?q?plan:=200064=20iter=202=20=E2=80=94=20local=20f?= =?UTF-8?q?unction-typed=20binder=20modes=20(class=201)=20(#57)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second iteration of spec 0064. Closes false-positive class 1: applying a local function-typed binder (a HOF predicate param like std_list.filter's `p`) treats its args as Consume because callee_arg_modes resolves only globals -- so a heap arg reused after (app p h) false-fires use-after-consume. Fix: BinderState gains fn_param_modes: Option>, seeded at all three function-typed binder introduction sites -- params and lam-params from the signature (param_tys), let-binders from the LetBinderTypes table built in iter 1 -- via a new fn_modes_of helper (strip_forall + Type::Fn { param_modes }). callee_arg_modes reads a local Var callee's fn_param_modes before falling back to globals; the existing App arg-walk maps Borrow to a borrow walk unchanged. Scope call (orchestrator): all three seeding sites, not just the param path that unblocks filter -- the point of this hardening cycle is to leave no latent class (the #57-from-0063-deferral lesson), and the extraction is the same at each site with the table already built. Two tasks, RED-first: Task 1 adds examples/c1_local_hof.ail to the harden list (RED: use-after-consume on filter_box's h); Task 2 adds the field + seeding + callee_arg_modes read (GREEN), plus two in-source unit tests (param path via signature, let path via hand-built table) and a borrow-predicate test helper. Diagnostic-only; no schema/type change. plan-recon mapped current post-iter-1 line numbers; parse gate fired on the inlined fixture (RED confirmed). refs #57 --- .../0123-harden-ownership-part2-class1.md | 444 ++++++++++++++++++ 1 file changed, 444 insertions(+) create mode 100644 docs/plans/0123-harden-ownership-part2-class1.md diff --git a/docs/plans/0123-harden-ownership-part2-class1.md b/docs/plans/0123-harden-ownership-part2-class1.md new file mode 100644 index 0000000..80e6f81 --- /dev/null +++ b/docs/plans/0123-harden-ownership-part2-class1.md @@ -0,0 +1,444 @@ +# 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>`, 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> { + 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>, +``` + +(`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.