From ba981689fc5fcbc925da4c34d25aacc866eb4237 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 17:34:28 +0200 Subject: [PATCH] =?UTF-8?q?plan:=200064=20iter=201=20=E2=80=94=20let-binde?= =?UTF-8?q?r=20type=20table=20+=20value-typed=20let=20exemption=20(#57)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First iteration of spec 0064 (#57 hardening). Tees the (def,binder)->Type table out of the typecheck pass (the inferred let-binder type computed at synth's Let arm and discarded today) and threads it into the linearity walk, then seeds BinderState.is_value for value-typed let-binders from the table -- closing false-positive class 3 (the class spec 0063 deferred). Two tasks, RED-first: Task 1 adds examples/c3_value_let.ail to the harden_ownership_false_positives_are_clean list (RED: use-after-consume on xnew); Task 2 threads the table end-to-end (synth -> check_fn -> check_in_workspace -> check_workspace -> check_module_with_visible -> Checker, all callers in one compile-atomic task) and seeds is_value at Term::Let (GREEN), plus two in-source unit tests (value-let clean, heap-let still errors). Fixes 1/2/4 (local fn-param modes, alias-redirect, partition_eithers rewrite) are later iterations of the same spec, explicitly out of scope here. plan-recon mapped the threading path; the parse-the-bytes gate fired on the inlined fixture (RED confirmed). refs #57 --- ...harden-ownership-part2-table-and-class3.md | 440 ++++++++++++++++++ 1 file changed, 440 insertions(+) create mode 100644 docs/plans/0122-harden-ownership-part2-table-and-class3.md diff --git a/docs/plans/0122-harden-ownership-part2-table-and-class3.md b/docs/plans/0122-harden-ownership-part2-table-and-class3.md new file mode 100644 index 0000000..2cf1ac8 --- /dev/null +++ b/docs/plans/0122-harden-ownership-part2-table-and-class3.md @@ -0,0 +1,440 @@ +# Harden ownership part 2 — iteration 1: let-binder type table + class 3 — 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:** Tee a `(def, binder) → Type` table out of the typecheck pass +and use it to exempt value-typed `let`-binders from consume-tracking, +closing false-positive class 3 (the class spec 0063 deferred). + +**Architecture:** The typecheck pass already computes every +`Term::Let` binder's inferred type at `synth`'s `Let` arm +(`lib.rs:3808`) and discards it. This iteration records it into a +per-module `LetBinderTypes` table, threads the table out of the +typecheck pass into the linearity walk (which runs strictly +post-typecheck on clean modules), and seeds `BinderState.is_value` +for `let`-binders from the table — the same per-binder flag #56 +already seeds at param / pattern / `lam` sites, now extended to the +`let` site. No schema change, no hash shift, no codegen change; the +linearity check stays a pure diagnostic pass. + +**Tech Stack:** `crates/ailang-check` (`lib.rs` typecheck pass + +`linearity.rs` walk), `examples/` fixture, `tests/workspace.rs` +assertion. + +**Scope:** FIRST iteration of spec 0064 only — the table +infrastructure + class 3 (value-typed `let`-binder). Out of scope this +iteration (later iterations of the same spec): class 1 +(`fn_param_modes` + `callee_arg_modes` local resolution), class 2 +(alias-redirect map + contract 0008:340 update), class 4 +(`partition_eithers` rewrite). Do NOT add `BinderState.fn_param_modes`, +`Checker.aliases`, or touch `examples/std_either_list.ail` / +`design/contracts/0008-memory-model.md` here. + +--- + +**Files this plan creates or modifies:** + +- Create: `examples/c3_value_let.ail` — class-3 RED→GREEN fixture + (value-typed `let`-binder used in cond + both branches). +- Modify: `crates/ailang-check/src/linearity.rs` — `LetBinderTypes` + type alias; `Checker` gains an immutable `let_binder_types` field; + `check_module` / `check_module_with_visible` / linearity `check_fn` + gain the table param; `Term::Let` seeds `is_value` from the table. +- Modify: `crates/ailang-check/src/lib.rs` — `synth` gains a `&mut + LetBinderTypes` out-param + the tee insert at the `Let` arm; + `check_fn` / `check_in_workspace` / `check_workspace` thread the + table; the linearity dispatch passes it in. +- Test: `crates/ailang-check/tests/workspace.rs` — add `c3_value_let` + to `harden_ownership_false_positives_are_clean`. +- Test: `crates/ailang-check/src/linearity.rs` in-source + `#[cfg(test)] mod tests` — value-typed `let`-binder clean (hand-built + table) + heap-typed `let`-binder still errors (type-gating guard). + +--- + +### Task 1: RED — class-3 fixture and its failing workspace assertion + +**Files:** +- Create: `examples/c3_value_let.ail` +- Test: `crates/ailang-check/tests/workspace.rs:726-738` + +- [ ] **Step 1: Create the fixture** + +Create `examples/c3_value_let.ail` with exactly: + +```ail +(module c3_value_let + (fn iterate + (doc "xnew is a Float let-binder used in cond and both branches") + (type (fn-type (params (own (con Float)) (own (con Float))) (ret (own (con Float))))) + (params x tol) + (body + (let xnew (app / x 2.0) + (if (app float_lt (app - xnew x) tol) + xnew + xnew))))) +``` + +- [ ] **Step 2: Add the fixture to the existing false-positive list** + +In `crates/ailang-check/tests/workspace.rs`, the test +`harden_ownership_false_positives_are_clean` (line 726) iterates a +literal array. Change exactly this line: + +```rust + for name in ["fp_value", "fp_hof", "fp_map"] { +``` + +to: + +```rust + for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let"] { +``` + +- [ ] **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 `c3_value_let must be linearity-clean; got: [...]` +with a `use-after-consume` diagnostic on `xnew`. (`fp_value` / `fp_hof` +/ `fp_map` stay clean; only the new entry fails.) + +--- + +### Task 2: GREEN — tee the table, thread it, seed `is_value` for value-typed `let`-binders + +**Files:** +- Modify: `crates/ailang-check/src/linearity.rs:223-240` (entries), + `:340-374` (check_fn + Checker construction), `:428-445` (Checker + struct), `:505-510` (`Term::Let`), plus the in-source test module. +- Modify: `crates/ailang-check/src/lib.rs:3319-3345` (synth sig), + `:3807-3820` (Let arm tee), `:2238` (check_fn), `:1877-1886` + (check_in_workspace), `:1163-1276` (check_workspace + dispatch). + +- [ ] **Step 1: Define the `LetBinderTypes` type alias** + +In `crates/ailang-check/src/linearity.rs`, near the top (after the +existing `use` lines, before `type_is_value` at `:173`), add: + +```rust +/// Per-fn inferred type of each `Term::Let` binder, teed out of the +/// typecheck pass (`synth`'s `Let` arm) so the linearity walk — which +/// runs after typechecking and does not re-infer — can read a +/// `let`-binder's type where the source pins no annotation. Keyed +/// `(def_name, binder_name)`. +pub(crate) type LetBinderTypes = HashMap<(String, String), Type>; +``` + +(`HashMap` and `Type` are already imported in this module.) + +- [ ] **Step 2: Add the `let_binder_types` field to `Checker`** + +In `crates/ailang-check/src/linearity.rs`, the `Checker<'a>` struct +(`:428-445`) ends with the `binders` field. Add, after `ctors` and +before `binders`: + +```rust + /// `(def, let-binder) → inferred type`, teed from the typecheck + /// pass. Read at the `Term::Let` arm to seed `is_value` for a + /// value-typed `let`-binder (the source pins no annotation there). + let_binder_types: &'a LetBinderTypes, +``` + +- [ ] **Step 3: Thread the table into the linearity entries and `check_fn`** + +In `crates/ailang-check/src/linearity.rs`: + +`check_module` (`:223-225`) — pass an empty table so the in-source / +no-workspace path is unchanged: + +```rust +pub(crate) fn check_module(m: &Module) -> Vec { + check_module_with_visible(m, &[], &LetBinderTypes::new()) +} +``` + +`check_module_with_visible` (`:237`) — add the param: + +```rust +pub(crate) fn check_module_with_visible( + m: &Module, + visible_extra: &[&Module], + let_binder_types: &LetBinderTypes, +) -> Vec { +``` + +Inside `check_module_with_visible`, find the call to `check_fn(...)` +(the per-def loop) and add `let_binder_types` as its final argument. + +linearity `check_fn` (`:340-346`) — add the param to the signature: + +```rust +fn check_fn( + f: &FnDef, + globals: &HashMap, + ctors: &HashMap>, + uniq: &UniquenessTable, + let_binder_types: &LetBinderTypes, + diags: &mut Vec, +) { +``` + +Checker construction (`:368-374`) — add the field: + +```rust + let mut checker = Checker { + globals, + diags, + def_name: &f.name, + ctors, + let_binder_types, + binders: HashMap::new(), + }; +``` + +- [ ] **Step 4: Seed `is_value` for value-typed `let`-binders at `Term::Let`** + +In `crates/ailang-check/src/linearity.rs`, the `Term::Let` arm +(`:505-510`) is today: + +```rust + Term::Let { name, value, body } => { + self.walk(value, Position::Consume); + self.with_binder(name, BinderState::default(), |this| { + this.walk(body, pos); + }); + } +``` + +Replace it with (value walk unchanged; the binder is seeded from the +table — alias handling for class 2 is a later iteration and is NOT +added here): + +```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); + }, + ); + } +``` + +- [ ] **Step 5: Add the `&mut LetBinderTypes` out-param to `synth` and tee the Let-binder type** + +In `crates/ailang-check/src/lib.rs`, `synth` (`:3319-3345`) currently +ends its parameter list with `warnings: &mut Vec`. +Add one more out-param after it (symmetric to `residuals` / +`free_fn_calls` / `warnings`): + +```rust + let_binder_types: &mut crate::linearity::LetBinderTypes, +``` + +In the `Term::Let` arm (`:3807-3820`), today: + +```rust + Term::Let { name, value, body } => { + let v = synth(value, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let prev = locals.insert(name.clone(), v); +``` + +insert the tee between the `synth` of the value and the `locals.insert`: + +```rust + Term::Let { name, value, body } => { + let v = synth(value, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?; + let_binder_types.insert((in_def.to_string(), name.clone()), subst.apply(&v)); + let prev = locals.insert(name.clone(), v); +``` + +(`in_def: &str` is in scope as a `synth` param; `subst` is in scope.) + +- [ ] **Step 6: Thread `let_binder_types` through every `synth` call site** + +The signature change breaks every `synth(...)` call in the crate (the +~22 recursive self-calls inside `synth`'s match arms, plus the +external callers below). Add `let_binder_types` as the final argument +to each. Do NOT hand-guess the recursive set — let the compiler +enumerate it (next step). The external (non-recursive) callers that +must each be threaded: + +- `crates/ailang-check/src/lib.rs:2410` — inside `check_fn` (production); thread the table `check_fn` now owns (Step 7). +- `crates/ailang-check/src/lib.rs:3306` — the const-`Def` value caller; pass the same per-module table `check_in_workspace` threads in (Step 8). Const-def `let`-binders are written to the table but never queried (linearity runs only on `Def::Fn`), so this is harmless. +- `crates/ailang-check/src/builtins.rs:316`, `:550` — `#[cfg(test)]` callers; pass `&mut crate::linearity::LetBinderTypes::new()`. +- `crates/ailang-check/src/lib.rs:5300`, `:5407`, `:7948` — `#[cfg(test)] mod tests` callers; pass `&mut crate::linearity::LetBinderTypes::new()`. + +- [ ] **Step 7: Thread the table through `check_fn`** + +In `crates/ailang-check/src/lib.rs`, the typecheck `check_fn` (`:2238`) +is today `fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec) -> Result<()>`. +Add the param: + +```rust +fn check_fn( + f: &FnDef, + env: &Env, + out_warnings: &mut Vec, + let_binder_types: &mut crate::linearity::LetBinderTypes, +) -> Result<()> { +``` + +and pass `let_binder_types` to the `synth(&f.body, …)` call at `:2410`. + +- [ ] **Step 8: Thread the table through `check_in_workspace`** + +In `crates/ailang-check/src/lib.rs`, `check_in_workspace` (`:1877`) is +today `fn check_in_workspace(m: &Module, ws: &Workspace, module_globals: &BTreeMap, out_warnings: &mut Vec) -> Vec`. +Add the param: + +```rust + let_binder_types: &mut crate::linearity::LetBinderTypes, +``` + +Pass `let_binder_types` to both `check_fn` calls (`:1999`, `:2097`) +and to the const-`Def` `synth` call (`:3306`). + +- [ ] **Step 9: Allocate the per-module table in `check_workspace` and feed the dispatch** + +In `crates/ailang-check/src/lib.rs`, `check_workspace` (`:1163`) builds +`synth_warnings` per module at `:1235` before calling +`check_in_workspace` at `:1236`. Mirror it: allocate the table next to +`synth_warnings`: + +```rust + let mut let_binder_types = crate::linearity::LetBinderTypes::new(); +``` + +Pass `&mut let_binder_types` to the `check_in_workspace` call at `:1236` +(and to the second `check_in_workspace` call on the single-error early +path at `:1425`, allocating a throwaway table there if it is a separate +scope). At the linearity dispatch (`:1276`), pass the now-populated +table: + +```rust + module_diags.extend(linearity::check_module_with_visible(m, &visible_extra, &let_binder_types)); +``` + +- [ ] **Step 10: Compile to enumerate and fix every remaining `synth` call site** + +Run: `cargo build -p ailang-check` +Expected: a sequence of E0061 "this function takes N arguments" +errors, one per un-threaded recursive `synth(...)` call inside +`synth`'s match arms. Add `let_binder_types` as the final argument to +each, then rebuild until: +Expected final: `cargo build -p ailang-check` succeeds, 0 errors. + +- [ ] **Step 11: 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 — `c3_value_let` is now linearity-clean (the `xnew` +`let`-binder is seeded `is_value` from the table and is no longer +consumed), and `fp_value` / `fp_hof` / `fp_map` stay clean. + +- [ ] **Step 12: Add in-source unit tests — value-typed let clean, heap-typed let still errors** + +In `crates/ailang-check/src/linearity.rs`, in the `#[cfg(test)] mod +tests` block (alongside `value_param_multi_read_is_clean` at `:1478`), +add. These call `check_module_with_visible(&m, &[], &table)` with a +hand-built table — the table is the unit under test, so the +`let`-value term is a trivial literal: + +```rust + /// A value-typed `let`-binder (type teed as `Float`) read twice + /// (`(let x 0 (seq x x))`) must NOT fire use-after-consume — the + /// `is_value` flag is seeded from the let-binder type table. RED + /// until the class-3 fix. + #[test] + fn value_let_binder_multi_read_is_clean() { + let body = Term::Let { + name: "x".into(), + value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }), + body: Box::new(Term::Seq { + lhs: Box::new(Term::Var { name: "x".into() }), + rhs: Box::new(Term::Var { name: "x".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 mut lbt = LetBinderTypes::new(); + lbt.insert(("f".into(), "x".into()), Type::Con { name: "Float".into(), args: vec![] }); + let diags = check_module_with_visible(&m, &[], &lbt); + assert!( + !diags.iter().any(|d| d.code == "use-after-consume"), + "a value-typed let-binder is never consumed; multi-read is legal; got {diags:?}" + ); + } + + /// Type-gating guard: a HEAP-typed `let`-binder (teed as `List`) + /// read twice MUST still fire use-after-consume — the exemption is + /// value-type-only, not blanket. (Regression guard, green after fix.) + #[test] + fn heap_let_binder_multi_read_still_errors() { + let body = Term::Let { + name: "x".into(), + value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }), + body: Box::new(Term::Seq { + lhs: Box::new(Term::Var { name: "x".into() }), + rhs: Box::new(Term::Var { name: "x".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 mut lbt = LetBinderTypes::new(); + lbt.insert(("f".into(), "x".into()), Type::Con { name: "List".into(), args: vec![] }); + let diags = check_module_with_visible(&m, &[], &lbt); + assert!( + diags.iter().any(|d| d.code == "use-after-consume"), + "a heap-typed let-binder consumed twice must still fire; got {diags:?}" + ); + } +``` + +(`Literal` is already imported in the test module via the parent `use`; +if not, add `use ailang_core::Literal;` to the test module.) + +- [ ] **Step 13: Run the in-source linearity unit tests** + +Run: `cargo test -p ailang-check --lib linearity::tests` +Expected: PASS — both new tests plus every pre-existing linearity unit +test (`value_param_multi_read_is_clean`, +`heap_param_multi_consume_still_errors`, `implicit_fn_is_exempt`, +`mixed_implicit_explicit_is_exempt`, …) stay green. + +- [ ] **Step 14: Full crate regression** + +Run: `cargo test -p ailang-check` +Expected: PASS — the whole `ailang-check` suite green (the table is a +new out-param written everywhere and read only at the linearity +`Term::Let` seeding; no existing typecheck or linearity outcome +changes except `c3_value_let` flipping RED→GREEN). + +- [ ] **Step 15: 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 — this is a diagnostic-only change; no +compile-baseline shift.