Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

plan: 0064 iter 2 — local function-typed binder modes (class 1) (#57)

Browse Source 
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<Vec<ParamMode>>, 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
This commit is contained in:
Brummel
2026-06-01 17:51:23 +02:00
parent 47964abf7c
commit 2ad58ada17
1 changed files with 444 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/plans/0123-harden-ownership-part2-class1.md
+444
View File
@@ -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<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.