plan: mut.4-tidy — close mut-local audit drift

Eight tasks addressing the architect's two [high] drift items (lambda-captures-of-mut-var diagnostic + codegen comment cleanup), two [medium] items (stale mut.1-stub history comments in DESIGN.md and codegen), plus the bench compile_check.py check_ms regression (~30-50% relative; closed by short-circuiting the empty mut_scope_stack walk in synth's Term::Var arm). Architect's [low] item (prose render of MutVar drops type annotation) deliberately deferred per architect recommendation — prose surface design is itself pending. Plan unblocks the follow-on Stateful-islands milestone (effect- handler infrastructure + !Mut + refs) per architect gate.
2026-05-15 02:05:22 +02:00
parent 03fb633d85
commit 6966cce702
1 changed files with 657 additions and 0 deletions
@@ -0,0 +1,657 @@
+# mut.4-tidy — Implementation Plan
+
+> **Parent spec:** `docs/specs/2026-05-15-mut-local.md` (covered by
+> audit-mut-local findings; no new spec).
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
+> to run this plan. Steps use `- [ ]` checkboxes for tracking.
+
+**Goal:** Close the mut-local milestone audit by addressing the
+architect's drift findings and the bench check_ms regression.
+Specifically: (a) add a typecheck diagnostic that rejects
+lambda-captures-of-mut-var (`CheckError::MutVarCapturedByLambda`)
+and a negative fixture; (b) replace the codegen `lambda.rs` blame-
+typechecker comment + Internal-error path with an `unreachable!`
+once the typecheck gate is in place; (c) clean stale mut.1-stub
+history comments in DESIGN.md §"Term" and
+`crates/ailang-codegen/src/lib.rs`; (d) short-circuit the empty
+`mut_scope_stack` walk in the `Term::Var` arm of `synth` to
+eliminate the per-Var-resolution overhead for programs with no mut
+blocks.
+
+**Architecture:** Architect's two `[high]` drift items are downstream
+of one spec gap: `docs/specs/2026-05-15-mut-local.md` does not
+enumerate "lambda body referencing an enclosing mut-var" as a
+diagnostic. The fix has three sites — typecheck adds the diagnostic
+in `Term::Lam`'s synth arm, codegen replaces its blame-comment path
+with `unreachable!`, and the spec gets an "Out of scope" amendment
+noting that mut-vars cannot escape into closures in this milestone.
+The bench check_ms regression has one root cause — the
+`mut_scope_stack.iter().rev().find_map(...)` walk at every
+`Term::Var` resolution runs even when the stack is empty (every
+program with no mut blocks); short-circuiting on `is_empty()` makes
+the path zero-cost for the existing corpus.
+
+**Tech Stack:** `ailang-check`, `ailang-codegen`, `docs/`. Plus one
+new negative fixture and one driver-test extension.
+
+---
+
+**Files this plan creates or modifies:**
+
+- Create: `examples/test_mut_var_captured_by_lambda.ail.json` —
+  negative fixture: a lambda inside a mut block references a
+  mut-var from the enclosing scope.
+- Modify: `crates/ailang-check/src/lib.rs:638-746` — add
+  `CheckError::MutVarCapturedByLambda { name }` variant + `code()`
+  arm `mut-var-captured-by-lambda` + `ctx()` arm + Display.
+- Modify: `crates/ailang-check/src/lib.rs` (`Term::Lam` arm of
+  `synth`) — walk the lambda's body for free Vars that resolve to
+  the enclosing `mut_scope_stack`; reject with
+  `MutVarCapturedByLambda` if any match.
+- Modify: `crates/ailang-check/src/lib.rs` (`Term::Var` arm of
+  `synth`) — short-circuit when `mut_scope_stack.is_empty()`.
+- Modify: `crates/ailang-codegen/src/lambda.rs:88-99` (capture-not-
+  in-locals path) — replace the `CodegenError::Internal(... blames
+  typechecker ...)` with `unreachable!("typecheck rejects
+  lambda-capture-of-mut-var via MutVarCapturedByLambda since
+  mut.4-tidy")`.
+- Modify: `crates/ailang-codegen/src/lambda.rs:466-467` — remove
+  the doc-comment promise that mut.2 typecheck rejects lambda
+  captures (it does as of mut.4); rewrite to reflect current
+  reality.
+- Modify: `crates/ailang-check/src/lift.rs:379` — same comment
+  cleanup.
+- Modify: `crates/ailang-codegen/src/lib.rs:1749-1758` — remove the
+  stale mut.1-stub comment block above the real Term::Mut arm.
+- Modify: `docs/DESIGN.md:2369-2402` (§"Term (expression)" mut/assign
+  jsonc block) — remove the trailing paragraph describing the
+  mut.1-stub dispatch state; replace with a paragraph describing the
+  current end-to-end mut.3 state.
+- Modify: `docs/specs/2026-05-15-mut-local.md` (§"Out of scope" or
+  equivalent) — add a bullet naming "Lambda capture of a mut-var"
+  as explicitly rejected, with the diagnostic name.
+- Modify: `crates/ailang-check/tests/mut_typecheck_pin.rs` — add
+  driver test for the new fixture asserting the
+  `mut-var-captured-by-lambda` diagnostic code.
+- Modify: `crates/ailang-core/tests/carve_out_inventory.rs` —
+  EXPECTED extended 12 → 13 for the new negative fixture.
+
+---
+
+## Task 1 — `CheckError::MutVarCapturedByLambda`
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs:638-746`
+
+- [ ] **Step 1: Write the failing pin test**
+
+In `#[cfg(test)] mod tests`:
+
+```rust
+#[test]
+fn mut_var_captured_by_lambda_diagnostic_has_kebab_code() {
+    let e = CheckError::MutVarCapturedByLambda { name: "sum".into() };
+    assert_eq!(e.code(), "mut-var-captured-by-lambda");
+    let _ = e.ctx();
+}
+```
+
+- [ ] **Step 2: Run to verify red**
+
+Run: `cargo test --workspace -p ailang-check mut_var_captured_by_lambda_diagnostic_has_kebab_code`
+Expected: FAIL — variant does not exist.
+
+- [ ] **Step 3: Add the variant + code() + ctx() + Display**
+
+In the `CheckError` enum body, immediately after
+`UnsupportedMutVarType`, insert:
+
+```rust
+    /// Iter mut.4-tidy: `Term::Lam` reached typecheck inside a
+    /// `Term::Mut` scope, and the lambda's body references a mut-var
+    /// declared in that enclosing scope. Spec
+    /// `docs/specs/2026-05-15-mut-local.md` §"Out of scope": mut-vars
+    /// cannot escape — they are alloca-resident and lexically scoped.
+    /// Capturing one into a closure would require either lifting it
+    /// to the heap (deferred milestone) or rejecting the capture.
+    /// This milestone takes the latter route.
+    #[error("[mut-var-captured-by-lambda] mut-var `{name}` cannot be captured by a lambda — mut-vars are alloca-resident and do not escape their enclosing mut block. Either move the lambda outside the mut block, or restructure to pass `{name}` as a lambda parameter (deferring escape to a future milestone with ref-types and the !Mut effect).")]
+    MutVarCapturedByLambda { name: String },
+```
+
+Then the `code()` arm immediately after `UnsupportedMutVarType`'s:
+
+```rust
+            CheckError::MutVarCapturedByLambda { .. } => "mut-var-captured-by-lambda",
+```
+
+And the `ctx()` arm:
+
+```rust
+            CheckError::MutVarCapturedByLambda { name } => json!({
+                "name": name,
+            }),
+```
+
+- [ ] **Step 4: Verify**
+
+Run: `cargo test --workspace -p ailang-check mut_var_captured_by_lambda_diagnostic_has_kebab_code`
+Expected: PASS.
+
+---
+
+## Task 2 — Reject lambda-captures-of-mut-var in `Term::Lam` synth arm
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs` (`Term::Lam` arm of `synth`)
+
+The arm is around `lib.rs:3374-3407` per the architect's report.
+The lambda's body is typechecked in a fresh `locals` scope with the
+lambda's params bound — but `mut_scope_stack` carries over from the
+caller. The fix is: BEFORE descending into the lambda body, scan
+the body for free Vars whose names resolve in `mut_scope_stack`.
+If any do, reject.
+
+- [ ] **Step 1: Write the failing pin (positive — lambda outside mut still works)**
+
+Add to `#[cfg(test)] mod tests`:
+
+```rust
+#[test]
+fn lambda_outside_mut_still_typechecks_clean() {
+    // (lam (params (typed x (con Int))) (ret (con Int)) (body (app + x 1)))
+    let term = Term::Lam {
+        params: vec!["x".into()],
+        param_types: vec![Type::int()],
+        ret_type: Type::int(),
+        effects: vec![],
+        body: Box::new(Term::App {
+            func: Box::new(Term::Var { name: "+".into() }),
+            args: vec![
+                Term::Var { name: "x".into() },
+                Term::Lit { lit: Literal::Int { value: 1 } },
+            ],
+            // tail-call default field name
+        }),
+    };
+    let (_ty, _) = synth_in_builtins_env(&term);
+    // No assertion on the returned type beyond that it doesn't panic
+    // / fail — this is a regression test that lambda synth wasn't
+    // broken by the new lambda-body free-var scan.
+}
+```
+
+This test should PASS even before Task 2 Step 2 — it's a regression
+guard.
+
+- [ ] **Step 2: Write the failing negative pin**
+
+```rust
+#[test]
+fn lambda_inside_mut_capturing_mut_var_emits_mut_var_captured_by_lambda() {
+    // (mut (var x (con Int) 0)
+    //   (let f (lam (params) (ret (con Int)) (body x))     ;; captures x
+    //     0))
+    let term = Term::Mut {
+        vars: vec![ailang_core::ast::MutVar {
+            name: "x".into(),
+            ty: Type::int(),
+            init: Term::Lit { lit: Literal::Int { value: 0 } },
+        }],
+        body: Box::new(Term::Let {
+            name: "f".into(),
+            value: Box::new(Term::Lam {
+                params: vec![],
+                param_types: vec![],
+                ret_type: Type::int(),
+                effects: vec![],
+                body: Box::new(Term::Var { name: "x".into() }),
+            }),
+            body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
+        }),
+    };
+    let err = synth_in_builtins_env_expect_err(&term);
+    match err {
+        CheckError::MutVarCapturedByLambda { name } => assert_eq!(name, "x"),
+        other => panic!("expected MutVarCapturedByLambda, got {:?}", other),
+    }
+}
+```
+
+(`synth_in_builtins_env_expect_err` is whatever helper the existing
+tests use to drive synth and unwrap an Err — match the convention.)
+
+- [ ] **Step 3: Run to verify red**
+
+Run: `cargo test --workspace -p ailang-check lambda_inside_mut_capturing_mut_var_emits_mut_var_captured_by_lambda`
+Expected: FAIL — currently the lambda body resolves `x` against the
+outer `mut_scope_stack` and types as Int with no diagnostic.
+
+- [ ] **Step 4: Add the scan to `Term::Lam`'s synth arm**
+
+In the `Term::Lam { params, param_types, body, .. }` arm of `synth`,
+BEFORE descending into the body (i.e. before the call to
+`synth(body, &lambda_locals, mut_scope_stack, ...)`), insert:
+
+```rust
+// Iter mut.4-tidy: reject lambda-captures-of-mut-var.
+// Walk the lambda body for free Vars (names not bound by the
+// lambda's own params) that match any mut-var on the enclosing
+// stack. If any match, reject with MutVarCapturedByLambda.
+if !mut_scope_stack.is_empty() {
+    let captured = collect_free_vars_in_term(body);
+    let lambda_param_names: std::collections::BTreeSet<&str> =
+        params.iter().map(|s| s.as_str()).collect();
+    for free_name in &captured {
+        if lambda_param_names.contains(free_name.as_str()) {
+            continue;
+        }
+        for frame in mut_scope_stack.iter() {
+            if frame.contains_key(free_name) {
+                return Err(CheckError::MutVarCapturedByLambda {
+                    name: free_name.clone(),
+                });
+            }
+        }
+    }
+}
+```
+
+The helper `collect_free_vars_in_term(t: &Term) -> Vec<String>` may
+already exist (the codebase has free-var walkers in `desugar.rs:1154`-
+area). If a directly-callable helper does not exist, write a small
+local one:
+
+```rust
+fn collect_free_vars_in_term(t: &Term) -> Vec<String> {
+    fn walk(t: &Term, bound: &mut Vec<String>, out: &mut Vec<String>) {
+        match t {
+            Term::Var { name } => {
+                if !bound.contains(name) && !out.contains(name) {
+                    out.push(name.clone());
+                }
+            }
+            Term::Let { name, value, body } => {
+                walk(value, bound, out);
+                bound.push(name.clone());
+                walk(body, bound, out);
+                bound.pop();
+            }
+            Term::LetRec { name, body, in_term, .. } => {
+                bound.push(name.clone());
+                walk(body, bound, out);
+                walk(in_term, bound, out);
+                bound.pop();
+            }
+            Term::Lam { params, body, .. } => {
+                let n = bound.len();
+                for p in params { bound.push(p.clone()); }
+                walk(body, bound, out);
+                bound.truncate(n);
+            }
+            Term::Mut { vars, body } => {
+                for v in vars { walk(&v.init, bound, out); }
+                let n = bound.len();
+                for v in vars { bound.push(v.name.clone()); }
+                walk(body, bound, out);
+                bound.truncate(n);
+            }
+            Term::Assign { name, value } => {
+                // Assign's name IS a use of the binding — counts as a free var if not bound.
+                if !bound.contains(name) && !out.contains(name) {
+                    out.push(name.clone());
+                }
+                walk(value, bound, out);
+            }
+            Term::App { func, args, .. } => {
+                walk(func, bound, out);
+                for a in args { walk(a, bound, out); }
+            }
+            Term::If { cond, then, else_ } => {
+                walk(cond, bound, out);
+                walk(then, bound, out);
+                walk(else_, bound, out);
+            }
+            Term::Match { scrutinee, arms } => {
+                walk(scrutinee, bound, out);
+                for arm in arms {
+                    // pattern bindings... for simplicity, scan body
+                    // without removing pattern-bound names — over-
+                    // approximates free vars (worst-case: emits the
+                    // diagnostic when none was needed). The over-
+                    // approximation is conservative-safe for
+                    // capture-rejection; a false-positive can be
+                    // tightened in a future iter.
+                    walk(&arm.body, bound, out);
+                }
+            }
+            Term::Seq { lhs, rhs } => {
+                walk(lhs, bound, out);
+                walk(rhs, bound, out);
+            }
+            Term::Clone { value } => walk(value, bound, out),
+            Term::ReuseAs { source, body } => {
+                walk(source, bound, out);
+                walk(body, bound, out);
+            }
+            Term::Ctor { args, .. } => for a in args { walk(a, bound, out); },
+            Term::Do { args, .. } => for a in args { walk(a, bound, out); },
+            Term::Lit { .. } => {}
+        }
+    }
+    let mut bound = Vec::new();
+    let mut out = Vec::new();
+    walk(t, &mut bound, &mut out);
+    out
+}
+```
+
+(The exact match-arm shape must be exhaustive against the post-mut.1
+Term enum. Pattern bindings inside Term::Match arms are
+over-approximated for the first cut; a tightening pass can land in a
+future tidy iter.)
+
+- [ ] **Step 5: Verify**
+
+Run: `cargo test --workspace -p ailang-check lambda_outside_mut_still_typechecks_clean lambda_inside_mut_capturing_mut_var_emits_mut_var_captured_by_lambda`
+Expected: both PASS.
+
+Run: `cargo test --workspace 2>&1 | grep -E 'FAILED|failures' | head -5`
+Expected: no failures introduced. (If any existing test broke,
+likely cause: the over-approximation in pattern bindings — check
+which test, decide whether to tighten the helper or to add a
+specific bound-name extraction for Term::Match arms.)
+
+---
+
+## Task 3 — Short-circuit empty `mut_scope_stack` in `Term::Var` arm
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs:2743-2747`
+
+- [ ] **Step 1: Locate the existing prepend**
+
+Find the iter mut.2 prepend in the `Term::Var` arm of `synth`,
+introduced at `lib.rs:2743-2747`:
+
+```rust
+for frame in mut_scope_stack.iter().rev() {
+    if let Some(ty) = frame.get(name) {
+        return Ok((ty.clone(), /* ... */));
+    }
+}
+```
+
+- [ ] **Step 2: Wrap in an `is_empty` guard**
+
+```rust
+if !mut_scope_stack.is_empty() {
+    for frame in mut_scope_stack.iter().rev() {
+        if let Some(ty) = frame.get(name) {
+            return Ok((ty.clone(), /* ... */));
+        }
+    }
+}
+```
+
+This is a single-instruction short-circuit. For the existing test
+corpus (zero mut blocks outside the four mut*.ail fixtures), this
+collapses the prepend cost to one `is_empty()` check per Var
+resolution — effectively zero overhead.
+
+- [ ] **Step 3: Verify the existing pin tests still pass**
+
+Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5`
+Expected: PASS.
+
+- [ ] **Step 4: Re-run `compile_check.py` to confirm regression closes**
+
+Run: `bench/compile_check.py 2>&1 | tail -10`
+Expected: zero `REGRESSION` lines on check_ms. (If the short-circuit
+brings check_ms back within tolerance, the bench exit drops to 0
+for this script. If not, additional optimization is needed — but
+the prepend cost is the only known introduced overhead in mut.2.)
+
+---
+
+## Task 4 — Codegen comment cleanup + unreachable blame fix
+
+**Files:**
+- Modify: `crates/ailang-codegen/src/lambda.rs:88-99`
+- Modify: `crates/ailang-codegen/src/lambda.rs:466-467`
+- Modify: `crates/ailang-codegen/src/lib.rs:1749-1758`
+
+- [ ] **Step 1: `lambda.rs:88-99` — replace Internal blame with unreachable!**
+
+Locate the existing path where a lambda capture is not found in
+`self.locals`. The current arm raises `CodegenError::Internal` with
+a message blaming the typechecker. Replace with:
+
+```rust
+            None => {
+                // Iter mut.4-tidy: post-Task-2 the typechecker
+                // rejects this via `CheckError::MutVarCapturedByLambda`.
+                // Reaching this path means typecheck was skipped or
+                // a bug let the AST through — both are bugs in
+                // upstream layers, not in codegen.
+                unreachable!(
+                    "lambda capture {name:?} not in locals — \
+                     typecheck should have rejected via MutVarCapturedByLambda",
+                );
+            }
+```
+
+- [ ] **Step 2: `lambda.rs:466-467` — comment cleanup**
+
+The existing comment promises mut.2 rejects lambda captures of
+mut-vars. Update to:
+
+```rust
+// Mut-var captures by lambdas are rejected at typecheck by
+// CheckError::MutVarCapturedByLambda (mut.4-tidy). codegen does
+// not see them.
+```
+
+- [ ] **Step 3: `lib.rs:1749-1758` — remove stale mut.1-stub comment**
+
+The architect's report names this site as still describing the
+mut.1 stub state. Read the current comment and either delete it (if
+purely historical) or rewrite to reflect the mut.3 reality. The new
+comment should NOT mention "stub", "deferred to mut.3", or
+"Internal-error". A one-line comment summarising the arm's purpose
+("Lower a mut-block: per-var alloca emit + body lower + scope
+exit") is sufficient.
+
+- [ ] **Step 4: Verify build green**
+
+Run: `cargo build --workspace 2>&1 | tail -5`
+Expected: green.
+
+Run: `cargo test --workspace 2>&1 | tail -5`
+Expected: green.
+
+---
+
+## Task 5 — `lift.rs` comment cleanup
+
+**Files:**
+- Modify: `crates/ailang-check/src/lift.rs:379`
+
+- [ ] **Step 1: Update the comment**
+
+The existing comment promises mut.2 rejects lambda captures of
+mut-vars. Update to match the mut.4-tidy reality, in the same form
+as Task 4 Step 2.
+
+- [ ] **Step 2: Verify build green**
+
+Run: `cargo build --workspace 2>&1 | tail -5`
+Expected: green.
+
+---
+
+## Task 6 — DESIGN.md amendment
+
+**Files:**
+- Modify: `docs/DESIGN.md:2369-2402` (§"Term (expression)" mut/assign block)
+
+- [ ] **Step 1: Update the trailing paragraph**
+
+The current jsonc block ends with a paragraph describing the
+mut.1-stub state. Replace with:
+
+```
+Both shapes ship in fully-lowered form as of iter mut.3 (2026-05-15):
+typecheck binds mut-vars in a lexical scope stack, codegen lowers
+them as entry-block allocas, and `Term::Assign` emits a `store`
+yielding the canonical Unit SSA. Mut-vars must be of one of the
+stack-resident scalar types {Int, Float, Bool, Unit}; capturing a
+mut-var into a lambda is rejected at typecheck via
+`CheckError::MutVarCapturedByLambda`. See
+`docs/specs/2026-05-15-mut-local.md`.
+```
+
+- [ ] **Step 2: Verify schema-drift tests still pass**
+
+Run: `cargo test --workspace -p ailang-core schema_drift 2>&1 | tail -5`
+Expected: PASS.
+
+---
+
+## Task 7 — Spec amendment
+
+**Files:**
+- Modify: `docs/specs/2026-05-15-mut-local.md` (§"Out of scope" or §"Acceptance criteria")
+
+- [ ] **Step 1: Add bullet to §"Out of scope"**
+
+In the §"Out of scope" subsection, append a bullet:
+
+```
+- **Lambda capture of a mut-var.** A lambda body whose free vars
+  include a mut-var of an enclosing `Term::Mut` is rejected at
+  typecheck with `CheckError::MutVarCapturedByLambda`. Mut-vars are
+  alloca-resident and lexically scoped; lifting them to the heap
+  for closure-capture would require ref-types and the `!Mut`
+  effect, both of which are deferred to the follow-on
+  Stateful-islands milestone (the layered effect-handler + ref-type
+  combo). The rejection diagnostic was added in iter mut.4-tidy.
+```
+
+---
+
+## Task 8 — Negative fixture + driver test extension
+
+**Files:**
+- Create: `examples/test_mut_var_captured_by_lambda.ail.json`
+- Modify: `crates/ailang-check/tests/mut_typecheck_pin.rs`
+- Modify: `crates/ailang-core/tests/carve_out_inventory.rs`
+
+- [ ] **Step 1: Write the fixture**
+
+Create `examples/test_mut_var_captured_by_lambda.ail.json`:
+
+```json
+{
+  "name": "test_mut_var_captured_by_lambda",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "ty": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" } },
+      "params": [],
+      "body": {
+        "t": "mut",
+        "vars": [
+          { "name": "x", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } }
+        ],
+        "body": {
+          "t": "let",
+          "name": "f",
+          "value": {
+            "t": "lam",
+            "params": [],
+            "paramTypes": [],
+            "retType": { "k": "con", "name": "Int" },
+            "effects": [],
+            "body": { "t": "var", "name": "x" }
+          },
+          "body": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+        }
+      }
+    }
+  ]
+}
+```
+
+Verify the exact root-key + field-name shape against an existing
+sibling fixture (e.g. `examples/test_mut_assign_out_of_scope.ail.json`).
+
+- [ ] **Step 2: Add driver test**
+
+In `crates/ailang-check/tests/mut_typecheck_pin.rs`:
+
+```rust
+#[test]
+fn lambda_capturing_mut_var_emits_mut_var_captured_by_lambda() {
+    let codes = check_fixture("test_mut_var_captured_by_lambda.ail.json");
+    assert_eq!(codes, vec!["mut-var-captured-by-lambda".to_string()]);
+}
+```
+
+- [ ] **Step 3: Update carve-out inventory**
+
+In `crates/ailang-core/tests/carve_out_inventory.rs`, bump the
+EXPECTED count from 12 → 13 (the new fixture joins the existing
+twelve `.ail.json` carve-outs).
+
+- [ ] **Step 4: Run all driver tests**
+
+Run: `cargo test --workspace -p ailang-check mut_typecheck_pin 2>&1 | tail -5`
+Expected: all six tests PASS (five from mut.2 + the new one).
+
+Run: `cargo test --workspace -p ailang-core carve_out_inventory 2>&1 | tail -3`
+Expected: PASS.
+
+Run: `cargo test --workspace 2>&1 | tail -5`
+Expected: full workspace green.
+
+---
+
+## Self-review checklist
+
+- [ ] **Drift coverage:** all four architect items (two `[high]` +
+  two `[medium]`) plus the bench check_ms regression are addressed.
+  Architect `[low]` items (prose render of MutVar) deliberately
+  deferred per architect's recommendation.
+
+- [ ] **Placeholder scan:** grep for "TBD" / "TODO" / "implement
+  later" / "similar to Task" / "appropriate error handling" — no
+  hits in this plan.
+
+- [ ] **Type-name consistency:** `CheckError::MutVarCapturedByLambda`,
+  `mut-var-captured-by-lambda` (kebab code), `collect_free_vars_in_term`
+  (local helper), `mut_scope_stack`, `unreachable!` — each appears
+  identically across tasks.
+
+- [ ] **Step granularity:** each step is 2-5 minutes.
+
+- [ ] **No commit steps:** verified.
+
+---
+
+## Acceptance gate for iter mut.4-tidy
+
+- `cargo build --workspace` green.
+- `cargo test --workspace` green, including the new negative-fixture
+  pin and the carve_out_inventory bump.
+- `bench/compile_check.py` check_ms regression closed (within
+  tolerance vs. baseline).
+- `bench/check.py` and `bench/cross_lang.py` unchanged from their
+  pre-mut.4 state (tail-noise envelope holds; runtime stable).
+- All architect-flagged comments rewritten to reflect the post-mut.3
+  reality.
+- The follow-on Stateful-islands milestone is now unblocked per the
+  architect's gate.