From 9c4d195806c90c45d02c8938cc143dac3a4973b1 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 18:07:29 +0200 Subject: [PATCH] =?UTF-8?q?plan:=200064=20iter=203=20=E2=80=94=20let-alias?= =?UTF-8?q?=20borrow=20propagation=20(class=202)=20(#57)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Third iteration of spec 0064. Closes false-positive class 2: Term::Let walks its value in Position::Consume, so (let a t (match a …)) over a borrow-mode t consumes t at the binding -> false consume-while-borrowed. Fix: Checker gains a scoped aliases: HashMap. A (let a t body) whose value is a bare Var resolving to a tracked binder records a -> root(t) for the body scope and skips the consume walk. A new resolve_alias helper maps a name to its root, PREFERRING a real binder at each chain step -- so an inner binder named `a` (nested let, pattern binder, lam param) automatically shadows the alias with NO change to with_binder/walk_arm/Lam (the shadowing is handled centrally in the resolver, not at three scattered introduction sites). Every binder-state lookup keyed by name resolves through the map first: use_var, the App borrow bump + decrement, callee_arg_modes, and the reuse-as source. Design calls (orchestrator): - Alias REDIRECT, not state clone (spec scope decision 3): consuming the alias marks the single root consumed, so a real double-consume through an alias is still caught -- a clone would miss it (unsound). Pinned by the let_alias_of_owned_double_consume_still_errors unit test. - resolve_alias prefers binders -> shadowing needs no edits to the three binder-introduction sites (simpler, lower-risk than clearing aliases at each). - reuse-as source (linearity.rs:663) is the 4th binder-state-reading site; the spec's Fix 3 named three illustratively. Resolving there too avoids a spurious reuse-as-source-not-bare-var on an aliased Var. Faithful completion of Fix 3, documented as such. Three tasks, RED-first: Task 1 adds examples/c2_let_alias.ail to the harden list (RED: consume-while-borrowed on count's t); Task 2 is the alias mechanism (GREEN) + the soundness unit test; Task 3 closes the design/contracts/0008-memory-model.md:340 let-alias carve-out (was "has not shipped yet") and extends the Ratified-by trailer to name linearity.rs. Diagnostic-only; no schema/type change. plan-recon mapped current post-iter-2 line numbers; parse gate fired on the inlined fixture (RED confirmed). Class 4 (partition_eithers rewrite) remains for the final iteration. refs #57 --- .../0124-harden-ownership-part2-class2.md | 562 ++++++++++++++++++ 1 file changed, 562 insertions(+) create mode 100644 docs/plans/0124-harden-ownership-part2-class2.md diff --git a/docs/plans/0124-harden-ownership-part2-class2.md b/docs/plans/0124-harden-ownership-part2-class2.md new file mode 100644 index 0000000..e8478d2 --- /dev/null +++ b/docs/plans/0124-harden-ownership-part2-class2.md @@ -0,0 +1,562 @@ +# Harden ownership part 2 — iteration 3: let-alias borrow propagation (class 2) — 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:** Stop a `let`-alias of a borrowed value from being treated as +a consume, closing false-positive class 2, while keeping a real +double-consume through an alias detectable. + +**Architecture:** The `Checker` gains a scoped `aliases: +HashMap` map. `(let a t body)` whose value is a bare +`Term::Var` resolving to a tracked binder records `a → root(t)` for the +body scope and skips the `Consume` walk of the value. A new +`resolve_alias` helper maps any name to its root, **preferring a real +binder at each chain step** — so an inner binder named `a` (a nested +`let`, a pattern binder, a `lam` param) automatically shadows the alias +with no change to the binder-introduction sites. Every binder-state +lookup keyed by name (`use_var`, the `App` borrow-count bump + +decrement, `callee_arg_modes`, `reuse-as` source) resolves through the +map first, so consume/borrow bookkeeping lands on the single root: a +borrow-position use of the alias does not consume the root (the fix), +and a consume of the alias marks the root consumed (so a later consume +of either is still caught — no false negative). Diagnostic-only; no +schema/type change. + +**Tech Stack:** `crates/ailang-check/src/linearity.rs` (the whole +fix), `examples/` fixture, `tests/workspace.rs` assertion, +`design/contracts/0008-memory-model.md` (the carve-out this closes). + +**Scope:** THIRD iteration of spec 0064 — class 2 only. Out of scope +(later iteration): class 4 (`partition_eithers` rewrite + +`c4_double_consume` fixture). Classes 1/3 already shipped. + +**Resolution-site completeness note.** Spec §"Fix 3" names `use_var`, +the `App` borrow bump, and `callee_arg_modes` as the resolution points. +The complete set of binder-state-reading sites in `linearity.rs` also +includes the `reuse-as` source path (`:663-685`): a `(reuse-as a …)` +whose `a` is an alias would otherwise mis-fire +`reuse-as-source-not-bare-var` (it IS a `Var`). The plan resolves +aliases there too — a faithful completion of Fix 3's "resolve a name to +its root before touching binders", not a scope addition. The +binder-introduction sites (`with_binder`, `walk_arm`, `Lam`) need NO +change because `resolve_alias` prefers a real binder at each step. + +--- + +**Files this plan creates or modifies:** + +- Create: `examples/c2_let_alias.ail` — class-2 RED→GREEN fixture + (`let`-alias of a borrow-mode param, matched). +- Modify: `crates/ailang-check/src/linearity.rs` — `Checker.aliases` + field + init; `resolve_alias` helper; `Term::Let` alias case; + alias-resolution in `use_var`, the `App` bump/decrement, + `callee_arg_modes`, and `reuse-as`; an alias-soundness unit test. +- Modify: `crates/ailang-check/tests/workspace.rs:728` — add + `c2_let_alias` to `harden_ownership_false_positives_are_clean`. +- Modify: `design/contracts/0008-memory-model.md:340-348` — the + let-alias carve-out bullet rewritten to "ships"; the `Ratified by:` + trailer extended to name `linearity.rs`. + +--- + +### Task 1: RED — class-2 fixture and its failing workspace assertion + +**Files:** +- Create: `examples/c2_let_alias.ail` +- Test: `crates/ailang-check/tests/workspace.rs:728` + +- [ ] **Step 1: Create the fixture** + +Create `examples/c2_let_alias.ail` with exactly: + +```ail +(module c2_let_alias + (data Tree + (doc "boxed tree") + (ctor TLeaf) + (ctor TNode (con Int) (con Tree) (con Tree))) + (fn count + (doc "alias a := borrowed t, then match a") + (type (fn-type (params (borrow (con Tree))) (ret (own (con Int))))) + (params t) + (body + (let a t + (match a + (case (pat-ctor TLeaf) 0) + (case (pat-ctor TNode v l r) 1)))))) +``` + +- [ ] **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", "c1_local_hof"] { +``` + +to: + +```rust + for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias"] { +``` + +- [ ] **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 `c2_let_alias must be linearity-clean; got: [...]` +with a `consume-while-borrowed` diagnostic on `t` in `count`. The other +five fixtures stay clean; only `c2_let_alias` fails. + +--- + +### Task 2: GREEN — the alias-redirect map + +**Files:** +- Modify: `crates/ailang-check/src/linearity.rs:460-481` (`Checker` + struct), `:398-405` (construction), `:541-555` (`Term::Let`), + `:752-786` (`use_var`), `:524-538` (`App` bump/decrement), + `:798-814` (`callee_arg_modes`), `:663-685` (`reuse-as`), plus the + in-source test module. + +- [ ] **Step 1: Add the `aliases` field to `Checker`** + +In `crates/ailang-check/src/linearity.rs`, the `Checker<'a>` struct +(`:460-481`) ends with the `binders` field. Add after it: + +```rust + /// `let`-alias → root binder name. A `(let a t …)` whose value is + /// a bare `Var t` resolving to a tracked binder records `a → + /// root(t)` here for the body scope; every binder-state lookup + /// resolves a name through this map first, so the alias shares the + /// root's consume/borrow state. Scoped: removed when the `let` + /// body ends. + aliases: HashMap, +``` + +- [ ] **Step 2: Initialise `aliases` in the `Checker` construction** + +In `crates/ailang-check/src/linearity.rs`, the construction literal in +`check_fn` (`:398-405`) names all fields. Add the init (after +`binders: HashMap::new(),`): + +```rust + aliases: HashMap::new(), +``` + +- [ ] **Step 3: Add the `resolve_alias` helper** + +In `crates/ailang-check/src/linearity.rs`, in the `impl<'a> Checker<'a>` +block, immediately before `fn use_var` (`:752`), add: + +```rust + /// Resolve a name to the binder it ultimately denotes, following + /// `let`-alias links. A real binder shadows an alias: at each step, + /// if the current name is a tracked binder we stop there, so an + /// inner `let`/pattern/`lam` binder of the same name takes + /// precedence over an outer alias without any change to the + /// binder-introduction sites. Returns an owned `String` so the + /// immutable borrow of `self.aliases` ends before any + /// `self.binders` mutation by the caller. + fn resolve_alias(&self, name: &str) -> String { + let mut cur = name.to_string(); + loop { + if self.binders.contains_key(&cur) { + return cur; + } + match self.aliases.get(&cur) { + Some(next) => cur = next.clone(), + None => return cur, + } + } + } +``` + +- [ ] **Step 4: Rewrite the `Term::Let` arm with the alias case** + +In `crates/ailang-check/src/linearity.rs`, the `Term::Let` arm +(`:541-555`) is currently: + +```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); + }, + ); + } +``` + +Replace it with (alias case first; non-alias case is today's body +unchanged): + +```rust + Term::Let { name, value, body } => { + // Class 2: a bare-Var value aliasing a tracked binder is + // a borrow-preserving rename, not a consume. Record + // `name → root` and skip the consume walk of the value; + // all binder-state lookups resolve through `aliases`. + let alias_root = match value.as_ref() { + Term::Var { name: vname } => { + let root = self.resolve_alias(vname); + if self.binders.contains_key(&root) { Some(root) } else { None } + } + _ => None, + }; + if let Some(root) = alias_root { + // Shadow any outer binder / alias of `name` for the + // body, install the alias, walk, then restore both. + let prev_binder = self.binders.remove(name); + let prev_alias = self.aliases.insert(name.clone(), root); + self.walk(body, pos); + self.aliases.remove(name); + if let Some(a) = prev_alias { + self.aliases.insert(name.clone(), a); + } + if let Some(b) = prev_binder { + self.binders.insert(name.clone(), b); + } + } else { + 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: Resolve aliases in `use_var`** + +In `crates/ailang-check/src/linearity.rs`, `use_var` (`:752-786`) +starts with `let state = match self.binders.get_mut(name) {`. Replace +its first lines: + +```rust + fn use_var(&mut self, name: &str, pos: Position) { + let state = match self.binders.get_mut(name) { + Some(s) => s, + None => return, + }; + if state.consumed { + self.diags + .push(make_use_after_consume(self.def_name, name)); + return; + } +``` + +with (resolve to the root first; report the root in the diagnostic): + +```rust + fn use_var(&mut self, name: &str, pos: Position) { + let root = self.resolve_alias(name); + let state = match self.binders.get_mut(&root) { + Some(s) => s, + None => return, + }; + if state.consumed { + self.diags + .push(make_use_after_consume(self.def_name, &root)); + return; + } +``` + +The `make_consume_while_borrowed(self.def_name, name)` call later in the +same fn must also report the root — change that one argument from `name` +to `&root`: + +```rust + if state.borrow_count > 0 { + self.diags + .push(make_consume_while_borrowed(self.def_name, &root)); + return; + } +``` + +- [ ] **Step 6: Resolve aliases in the `App` borrow bump and decrement** + +In `crates/ailang-check/src/linearity.rs`, the `App` borrow-bump block +(`:524-528`) is: + +```rust + if matches!(arg_pos, Position::Borrow) { + if let Term::Var { name } = arg { + if let Some(s) = self.binders.get_mut(name) { + s.borrow_count = s.borrow_count.saturating_add(1); + lent.push(name.clone()); + } + } + } +``` + +Replace with (resolve the arg name to its root; push the root so the +decrement targets the same key): + +```rust + if matches!(arg_pos, Position::Borrow) { + if let Term::Var { name } = arg { + let root = self.resolve_alias(name); + if let Some(s) = self.binders.get_mut(&root) { + s.borrow_count = s.borrow_count.saturating_add(1); + lent.push(root); + } + } + } +``` + +(The decrement loop `for name in lent { … self.binders.get_mut(&name) … }` +at `:535-538` is unchanged — `lent` now holds resolved roots.) + +- [ ] **Step 7: Resolve the callee alias in `callee_arg_modes`** + +In `crates/ailang-check/src/linearity.rs`, `callee_arg_modes` +(`:798-814`) binds `name` then reads the local binder. Replace: + +```rust + let name = match callee { + Term::Var { name } => name, + _ => return vec![], + }; + if let Some(s) = self.binders.get(name) { + if let Some(modes) = &s.fn_param_modes { + return modes.clone(); + } + } +``` + +with (resolve to root before the local-binder read; the global lookup +below is unchanged — `root == name` whenever the callee is a global): + +```rust + let name = match callee { + Term::Var { name } => name, + _ => return vec![], + }; + let root = self.resolve_alias(name); + if let Some(s) = self.binders.get(&root) { + if let Some(modes) = &s.fn_param_modes { + return modes.clone(); + } + } +``` + +- [ ] **Step 8: Resolve the `reuse-as` source through aliases** + +In `crates/ailang-check/src/linearity.rs`, the `reuse-as` source match +(`:663-685`) is: + +```rust + match source.as_ref() { + Term::Var { name } if self.binders.contains_key(name) => { + let already_consumed = self + .binders + .get(name) + .map(|s| s.consumed) + .unwrap_or(false); + if already_consumed { + self.diags + .push(make_use_after_consume_at_reuse_as(self.def_name, name, body)); + } else if let Some(s) = self.binders.get_mut(name) { + // Mark the source consumed at the reuse-as site. + s.consumed = true; + } + } + other => { + self.diags.push(make_reuse_as_source_not_bare_var( + self.def_name, + other, + body, + )); + } + } +``` + +Replace with (resolve a `Var` source to its root; a `Var` aliasing a +tracked binder is a valid bare-Var source, not "not bare var"): + +```rust + let resolved = match source.as_ref() { + Term::Var { name } => Some(self.resolve_alias(name)), + _ => None, + }; + match resolved { + Some(root) if self.binders.contains_key(&root) => { + let already_consumed = self + .binders + .get(&root) + .map(|s| s.consumed) + .unwrap_or(false); + if already_consumed { + self.diags + .push(make_use_after_consume_at_reuse_as(self.def_name, &root, body)); + } else if let Some(s) = self.binders.get_mut(&root) { + // Mark the source consumed at the reuse-as site. + s.consumed = true; + } + } + _ => { + self.diags.push(make_reuse_as_source_not_bare_var( + self.def_name, + source.as_ref(), + body, + )); + } + } +``` + +- [ ] **Step 9: Build the crate (compile gate)** + +Run: `cargo build -p ailang-check` +Expected: 0 errors. (Adding the `aliases` field broke only the +`Checker` construction literal, fixed in Step 2; `resolve_alias` is +used in Steps 4-8.) + +- [ ] **Step 10: Run the RED test from Task 1 — now GREEN** + +Run: `cargo test -p ailang-check --test workspace harden_ownership_false_positives_are_clean` +Expected: PASS — `c2_let_alias` is now linearity-clean (`a` aliases the +borrowed `t`; the `match a` scrutinee is a borrow use of the root, not a +consume), and the other five fixtures stay clean. + +- [ ] **Step 11: Add the alias-soundness unit test** + +In `crates/ailang-check/src/linearity.rs`, in the `#[cfg(test)] mod +tests` block (alongside `heap_let_binder_multi_read_still_errors`), add: + +```rust + /// Alias soundness: `(let a p0 (seq a p0))` over an OWN heap binder + /// `p0` — consuming the alias `a` then the root `p0` is a real + /// double-consume and MUST still fire use-after-consume. The + /// redirect shares one root state; it does not mask the second + /// consume (the clone alternative would). Empty table → the alias + /// path triggers structurally on the bare-Var value. + #[test] + fn let_alias_of_owned_double_consume_still_errors() { + let body = Term::Let { + name: "a".into(), + value: Box::new(Term::Var { name: "p0".into() }), + body: Box::new(Term::Seq { + lhs: Box::new(Term::Var { name: "a".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_modes("f", vec![ParamMode::Own], body)], + }; + let diags = check_module(&m); + assert!( + diags.iter().any(|d| d.code == "use-after-consume"), + "consuming an alias then its root is a real double-consume; got {diags:?}" + ); + } +``` + +- [ ] **Step 12: Run the in-source linearity unit tests** + +Run: `cargo test -p ailang-check --lib linearity::tests` +Expected: PASS — the new `let_alias_of_owned_double_consume_still_errors` +plus every pre-existing linearity unit test (the class-1/class-3 tests +from iters 1-2, `heap_param_multi_consume_still_errors`, the +`implicit_fn_is_exempt` family, …) stay green. + +- [ ] **Step 13: Full crate regression** + +Run: `cargo test -p ailang-check` +Expected: PASS — the whole `ailang-check` suite green. Alias resolution +is a no-op for every name that is not a recorded alias (`resolve_alias` +returns the name unchanged), so no non-alias outcome changes except +`c2_let_alias` flipping RED→GREEN. + +- [ ] **Step 14: 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. + +--- + +### Task 3: Close the contract carve-out + +**Files:** +- Modify: `design/contracts/0008-memory-model.md:340-348` + +- [ ] **Step 1: Rewrite the let-alias carve-out bullet** + +In `design/contracts/0008-memory-model.md`, the bullet under "What this +widening does NOT do" (`:340-346`) currently reads: + +``` +- Does not cover let-aliases of borrowed values. A let-binder + whose value is `Term::Var` referencing a `Borrow`-mode + param is not yet propagated through; the param-mode gates + treat such a binder as "owned" (its `current_param_modes` + lookup misses, default = owned). This is a known carve-out + shared by Iter A and the pre-tail-call shallow-dec arm; closing it is a propagation pass + through let-bindings that has not shipped yet. +``` + +Replace that bullet with: + +``` +- Covers let-aliases of borrowed values (spec 0064, class 2). A + let-binder whose value is a bare `Term::Var` resolving to a + tracked binder is recorded as an alias to that root in the + linearity walk (`crates/ailang-check/src/linearity.rs`, + `Checker.aliases` + `resolve_alias`); the binding does not + consume the source, and every binder-state lookup resolves + the alias to its root, so a borrow-position use of the alias + does not consume the root while a real double-consume through + the alias is still caught. +``` + +- [ ] **Step 2: Extend the `Ratified by:` trailer** + +In `design/contracts/0008-memory-model.md`, the section trailer +(`:348`) currently reads: + +``` +Ratified by: `crates/ailang-check/src/uniqueness.rs`. +``` + +Change it to name the linearity walk, which now hosts the let-alias +propagation: + +``` +Ratified by: `crates/ailang-check/src/uniqueness.rs`, +`crates/ailang-check/src/linearity.rs`. +``` + +- [ ] **Step 3: Verify the contract file is internally consistent** + +Run: `grep -n "let-alias\|Ratified by" design/contracts/0008-memory-model.md` +Expected: the carve-out bullet now states the propagation ships, and +the trailer names both `uniqueness.rs` and `linearity.rs`. No remaining +"has not shipped yet" / "Does not cover let-aliases" text.