plan: 0064 iter 1 — let-binder type table + value-typed let exemption (#57)

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
2026-06-01 17:34:28 +02:00
parent f6a8607518
commit ba981689fc
1 changed files with 440 additions and 0 deletions
@@ -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<Diagnostic> {
+    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<Diagnostic> {
+```
+
+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<String, Type>,
+    ctors: &HashMap<String, Vec<Type>>,
+    uniq: &UniquenessTable,
+    let_binder_types: &LetBinderTypes,
+    diags: &mut Vec<Diagnostic>,
+) {
+```
+
+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<crate::diagnostic::Diagnostic>`.
+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<Diagnostic>) -> Result<()>`.
+Add the param:
+
+```rust
+fn check_fn(
+    f: &FnDef,
+    env: &Env,
+    out_warnings: &mut Vec<Diagnostic>,
+    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<String, ModuleGlobals>, out_warnings: &mut Vec<Diagnostic>) -> Vec<CheckError>`.
+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.