# 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.