iter loop-recur.tidy GREEN: reject lambda-captures-loop-binder at check + milestone-close audit resolution

GREEN side of the RED audit-trail commit 39380d3. The loop/recur
milestone-close audit found a [high] correctness defect — a lambda
capturing a loop binder passed `ail check` then panicked
unreachable!() at codegen (crates/ailang-codegen/src/lambda.rs:102)
on type-correct input. Fixed symmetrically to mut.4-tidy: new
CheckError::LoopBinderCapturedByLambda (code
loop-binder-captured-by-lambda, bracket-free F2 Display), the
Term::Lam escape guard gained a parallel loop_stack pass. Minimal
mechanism: loop_stack element Vec<Type> -> Vec<(String,Type)> so
the already-threaded per-loop frame carries binder names; recur
still reads .1 by position (Boss-call-2 positional invariant
preserved verbatim — the name is a second field for the escape
guard only, a consumer iter-2 did not anticipate). Codegen
byte-unchanged (typecheck-only fix). carve_out 17->18 + ct1-F2 +
DESIGN.md note lockstep.

Folded in (Boss-side, audit resolution): the two [medium]
doc-honesty edits the audit surfaced (mut_var_allocas rustdoc now
states its mut-var+loop-binder dual use; Term::Loop doc-comment
now describes the real shipped state, not iter-1's stale
"per-binder phi" forward-look) + a [low] P2 roadmap todo
(plan-recon undercount countermeasure, pairs with planner Step-5
items 7+8). Bench gate: all 3 scripts exit 0, 25 metrics 0
regressed — pristine, carry-on (no baseline/ratify).

cargo test --workspace 619 -> 622 / 0 red (Boss-reran
independently, hash_pin 11/0). The loop/recur milestone is
audit-clean; fieldtest is the only remaining step before close.

crates/ail/tests/ct1_check_cli.rs

@@ -226,6 +226,13 @@ fn check_human_mode_renders_mut_diagnostic_code_exactly_once() {
             "test_mut_var_captured_by_lambda.ail.json",
             "mut-var-captured-by-lambda",
         ),
+        // Iter loop-recur.tidy: symmetric loop-binder-capture variant.
+        // Its Display body is likewise bracket-`[code]`-free so the
+        // human formatter supplies `[<code>]` exactly once.
+        (
+            "test_loop_binder_captured_by_lambda.ail.json",
+            "loop-binder-captured-by-lambda",
+        ),
     ];
     for (fixture_name, code) in cases {
         let fixture = examples_dir().join(fixture_name);

crates/ailang-check/src/builtins.rs

@@ -351,7 +351,7 @@ mod tests {
         let mut warnings: Vec<crate::diagnostic::Diagnostic> = Vec::new();
         // loop-recur iter 2: test helper synths one term from top-of-
         // body — fresh empty loop-stack (mirrors mut_scope_stack).
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let ty = crate::synth(
             t,
             &env,
@@ -598,7 +598,7 @@ mod tests {
         let mut warnings: Vec<crate::diagnostic::Diagnostic> = Vec::new();
         // loop-recur iter 2: test helper synths one term from top-of-
         // body — fresh empty loop-stack (mirrors mut_scope_stack).
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let err = crate::synth(
             &term,
             &env,

crates/ailang-check/src/lib.rs

@@ -696,6 +696,19 @@ pub enum CheckError {
     #[error("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 },
 
+    /// loop-recur iter loop-recur.tidy: `Term::Lam` reached typecheck
+    /// inside a lexically-enclosing `Term::Loop`, and the lambda's body
+    /// references a loop binder declared by that enclosing loop. Loop
+    /// binders are alloca-resident (codegen reuses the
+    /// `mut_var_allocas` registry, `std::mem::take`-emptied at the
+    /// lambda frame boundary), exactly the mut-var escape rule. Symmetric
+    /// to `MutVarCapturedByLambda`: capturing one into a closure would
+    /// require lifting it to the heap (deferred) or rejecting the
+    /// capture; this milestone takes the latter route rather than
+    /// panicking codegen on type-correct input.
+    #[error("loop binder `{name}` cannot be captured by a lambda — loop binders are alloca-resident and do not escape their enclosing loop. Either move the lambda outside the loop, or restructure to pass `{name}` as a lambda parameter (deferring escape to a future milestone with ref-types and the !Mut effect).")]
+    LoopBinderCapturedByLambda { name: String },
+
     /// loop-recur iter 2: `Term::Recur` reached typecheck with no
     /// lexically-enclosing `Term::Loop` (the `loop_stack` was empty).
     #[error("`recur` is only valid inside a `loop` — there is no enclosing loop here")]
@@ -774,6 +787,7 @@ impl CheckError {
             CheckError::AssignTypeMismatch { .. } => "assign-type-mismatch",
             CheckError::UnsupportedMutVarType { .. } => "mut-var-unsupported-type",
             CheckError::MutVarCapturedByLambda { .. } => "mut-var-captured-by-lambda",
+            CheckError::LoopBinderCapturedByLambda { .. } => "loop-binder-captured-by-lambda",
             CheckError::RecurOutsideLoop => "recur-outside-loop",
             CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch",
             CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch",
@@ -852,6 +866,9 @@ impl CheckError {
             CheckError::MutVarCapturedByLambda { name } => {
                 serde_json::json!({"name": name})
             }
+            CheckError::LoopBinderCapturedByLambda { name } => {
+                serde_json::json!({"name": name})
+            }
             CheckError::RecurArityMismatch { expected, got } => {
                 serde_json::json!({"expected": expected, "actual": got})
             }
@@ -2006,7 +2023,7 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     // loop-recur iter 2: fresh per-fn-body loop-binder-type stack.
     // Empty at fn entry; pushed/popped by `Term::Loop` arms during
     // the synth walk; discarded after the body type-checks.
-    let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+    let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
     let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
     unify(&ret_ty, &body_ty, &mut subst)?;
     // mq.3: surface synth-time warnings into the caller-supplied
@@ -2893,7 +2910,7 @@ fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> R
     let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
     // loop-recur iter 2: a const value has no enclosing loop; any
     // `recur` in a const body correctly fires `RecurOutsideLoop`.
-    let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+    let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
     let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
     out_warnings.extend(warnings);
     unify(&c.ty, &v, &mut subst)?;
@@ -2919,15 +2936,18 @@ pub(crate) fn synth(
     // name through it. Position: locals-adjacent because both are
     // per-fn-body lexical scope state.
     mut_scope_stack: &mut Vec<IndexMap<String, Type>>,
-    // loop-recur iter 2: per-walk loop-binder-type stack. Each frame
-    // is one `Term::Loop`'s binder types in declaration order
-    // (positional — `recur` rebinds binders by position, not name,
-    // so this is `Vec<Type>` not name-keyed like `mut_scope_stack`).
-    // Pushed on `Term::Loop` body entry, popped on exit; consulted
-    // innermost-first by `Term::Recur` for arity + per-position type.
-    // Position: mut_scope_stack-adjacent — both are per-fn-body
-    // lexical-control scope state threaded identically.
-    loop_stack: &mut Vec<Vec<Type>>,
+    // loop-recur iter 2: per-walk loop-binder stack. Each frame is one
+    // `Term::Loop`'s binders in declaration order. `recur` rebinds
+    // binders by position, not name, so the type list is positional;
+    // iter loop-recur.tidy added the binder name alongside the type
+    // (so `Term::Lam`'s escape guard can reject a free var that is an
+    // in-scope loop binder, symmetric to `mut_scope_stack`). Pushed on
+    // `Term::Loop` body entry, popped on exit; consulted innermost-first
+    // by `Term::Recur` for arity + per-position type, and across all
+    // frames by `Term::Lam` for the escape check. Position:
+    // mut_scope_stack-adjacent — both are per-fn-body lexical-control
+    // scope state threaded identically.
+    loop_stack: &mut Vec<Vec<(String, Type)>>,
     effects: &mut BTreeSet<String>,
     in_def: &str,
     subst: &mut Subst,
@@ -3605,7 +3625,16 @@ pub(crate) fn synth(
             // `MutVarCapturedByLambda`. Reuses `desugar::free_vars_in_term`
             // (same walker `lift.rs` uses) which honours pattern bindings
             // inside `Term::Match` arms.
-            if !mut_scope_stack.is_empty() {
+            // Iter loop-recur.tidy: symmetrically reject
+            // lambda-captures-of-loop-binder. Loop binders are
+            // alloca-resident and `std::mem::take`-emptied at the
+            // lambda frame boundary in codegen, exactly like mut-vars
+            // — capturing one panics `unreachable!()` at codegen, so
+            // the type checker rejects it here instead. The free-var
+            // scan is shared with the mut-scope check below; gated on
+            // a non-empty enclosing scope so lambdas outside any
+            // mut/loop scope typecheck unchanged.
+            if !mut_scope_stack.is_empty() || !loop_stack.is_empty() {
                 let mut lam_bound: BTreeSet<String> = BTreeSet::new();
                 for p in params {
                     lam_bound.insert(p.clone());
@@ -3620,6 +3649,13 @@ pub(crate) fn synth(
                             });
                         }
                     }
+                    for frame in loop_stack.iter() {
+                        if frame.iter().any(|(n, _)| n == free_name) {
+                            return Err(CheckError::LoopBinderCapturedByLambda {
+                                name: free_name.clone(),
+                            });
+                        }
+                    }
                 }
             }
 
@@ -3894,12 +3930,13 @@ pub(crate) fn synth(
         // loop (declaration order; later inits + body see earlier
         // binders via `locals`, exactly as `Term::Let` binds its
         // name). The loop's static type is the body's type. The
-        // ordered binder types are pushed onto `loop_stack` for the
-        // body walk so an inner `Term::Recur` can position-check
-        // against them; popped on exit. Binder names are NOT in
-        // `loop_stack` (recur is positional, not by-name).
+        // ordered binders (name + type) are pushed onto `loop_stack`
+        // for the body walk so an inner `Term::Recur` can
+        // position-check the types and `Term::Lam`'s escape guard
+        // (iter loop-recur.tidy) can reject capture of a binder name;
+        // popped on exit.
         Term::Loop { binders, body } => {
-            let mut binder_tys: Vec<Type> = Vec::new();
+            let mut binder_frame: Vec<(String, Type)> = Vec::new();
             let mut restore: Vec<(String, Option<Type>)> = Vec::new();
             for b in binders {
                 let init_ty = synth(
@@ -3907,11 +3944,11 @@ pub(crate) fn synth(
                     in_def, subst, counter, residuals, free_fn_calls, warnings,
                 )?;
                 unify(&b.ty, &init_ty, subst)?;
-                binder_tys.push(b.ty.clone());
+                binder_frame.push((b.name.clone(), b.ty.clone()));
                 let prev = locals.insert(b.name.clone(), b.ty.clone());
                 restore.push((b.name.clone(), prev));
             }
-            loop_stack.push(binder_tys);
+            loop_stack.push(binder_frame);
             let body_result = synth(
                 body, env, locals, mut_scope_stack, loop_stack, effects,
                 in_def, subst, counter, residuals, free_fn_calls, warnings,
@@ -3939,13 +3976,13 @@ pub(crate) fn synth(
         // through, so it unifies with whatever sibling branch the
         // enclosing if/match requires.
         Term::Recur { args } => {
-            let binder_tys = match loop_stack.last() {
+            let binder_frame = match loop_stack.last() {
                 None => return Err(CheckError::RecurOutsideLoop),
-                Some(tys) => tys.clone(),
+                Some(frame) => frame.clone(),
             };
-            if args.len() != binder_tys.len() {
+            if args.len() != binder_frame.len() {
                 return Err(CheckError::RecurArityMismatch {
-                    expected: binder_tys.len(),
+                    expected: binder_frame.len(),
                     got: args.len(),
                 });
             }
@@ -3954,7 +3991,7 @@ pub(crate) fn synth(
                     a, env, locals, mut_scope_stack, loop_stack, effects,
                     in_def, subst, counter, residuals, free_fn_calls, warnings,
                 )?;
-                let applied_binder = subst.apply(&binder_tys[i]);
+                let applied_binder = subst.apply(&binder_frame[i].1);
                 let applied_arg = subst.apply(&arg_ty);
                 if applied_binder != applied_arg {
                     return Err(CheckError::RecurTypeMismatch {
@@ -4342,7 +4379,7 @@ mod tests {
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         // loop-recur iter 2: loop-free unit-test call site — fresh
         // empty loop-stack, mirroring the mut-scope above.
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4383,7 +4420,7 @@ mod tests {
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         // loop-recur iter 2: loop-free unit-test call site — fresh
         // empty loop-stack, mirroring the mut-scope above.
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let mut frame: IndexMap<String, Type> = IndexMap::new();
         frame.insert("x".into(), Type::float()); // inner mut-var
         mut_scope_stack.push(frame);
@@ -4427,7 +4464,7 @@ mod tests {
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         // loop-recur iter 2: loop-free unit-test call site — fresh
         // empty loop-stack, mirroring the mut-scope above.
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let mut outer: IndexMap<String, Type> = IndexMap::new();
         outer.insert("x".into(), Type::int());
         mut_scope_stack.push(outer);
@@ -4544,7 +4581,7 @@ mod tests {
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         // loop-recur iter 2: loop-free unit-test call site — fresh
         // empty loop-stack, mirroring the mut-scope above.
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4587,7 +4624,7 @@ mod tests {
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         // loop-recur iter 2: loop-free unit-test call site — fresh
         // empty loop-stack, mirroring the mut-scope above.
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4629,7 +4666,7 @@ mod tests {
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         // loop-recur iter 2: loop-free unit-test call site — fresh
         // empty loop-stack, mirroring the mut-scope above.
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4684,6 +4721,17 @@ mod tests {
         let _ = e.ctx();
     }
 
+    /// Iter loop-recur.tidy: `CheckError::LoopBinderCapturedByLambda`
+    /// carries the stable kebab code `loop-binder-captured-by-lambda`
+    /// and a non-panicking `ctx()` arm carrying the captured name —
+    /// symmetric to `mut_var_captured_by_lambda_diagnostic_has_kebab_code`.
+    #[test]
+    fn loop_binder_captured_by_lambda_diagnostic_has_kebab_code() {
+        let e = CheckError::LoopBinderCapturedByLambda { name: "acc".into() };
+        assert_eq!(e.code(), "loop-binder-captured-by-lambda");
+        let _ = e.ctx();
+    }
+
     /// loop-recur iter 2: the four `Recur*` `CheckError` variants carry
     /// the exact stable kebab codes the spec acceptance mandates
     /// (`recur-outside-loop` / `recur-arity-mismatch` /
@@ -4760,7 +4808,7 @@ mod tests {
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         // loop-recur iter 2: loop-free unit-test call site — fresh
         // empty loop-stack, mirroring the mut-scope above.
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4779,6 +4827,56 @@ mod tests {
         }
     }
 
+    /// Iter loop-recur.tidy: a lambda nested inside a `Term::Loop`
+    /// whose body references a loop binder declared by the enclosing
+    /// loop is rejected with `LoopBinderCapturedByLambda`. The
+    /// captured-name field reports the offending binder. Structurally
+    /// symmetric to
+    /// `lambda_inside_mut_capturing_mut_var_emits_mut_var_captured_by_lambda`.
+    #[test]
+    fn lambda_inside_loop_capturing_binder_emits_loop_binder_captured_by_lambda() {
+        // (loop (acc : Int = 0)
+        //   (let f = (lam () : Int -> acc) in 0))
+        let term = Term::Loop {
+            binders: vec![ailang_core::ast::LoopBinder {
+                name: "acc".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_tys: vec![],
+                    ret_ty: Box::new(Type::int()),
+                    effects: vec![],
+                    body: Box::new(Term::Var { name: "acc".into() }),
+                }),
+                body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
+            }),
+        };
+        let env = Env::default();
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals: Vec<ResidualConstraint> = Vec::new();
+        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+        let mut warnings: Vec<Diagnostic> = Vec::new();
+        let err = synth(
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
+            "<test>", &mut subst, &mut counter, &mut residuals,
+            &mut free_fn_calls, &mut warnings,
+        )
+        .expect_err("lambda capturing loop binder must be rejected");
+        match err {
+            CheckError::LoopBinderCapturedByLambda { name } => assert_eq!(name, "acc"),
+            other => panic!("expected LoopBinderCapturedByLambda, got {other:?}"),
+        }
+    }
+
     fn fn_def(name: &str, ty: Type, params: Vec<&str>, body: Term) -> Def {
         Def::Fn(FnDef {
             name: name.into(),
@@ -7502,7 +7600,7 @@ mod tests {
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         // loop-recur iter 2: loop-free unit-test call site — fresh
         // empty loop-stack, mirroring the mut-scope above.
-        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;

crates/ailang-check/src/lift.rs

@@ -746,7 +746,7 @@ impl<'a> Lifter<'a> {
         // loop-recur iter 2: lift's letrec-capture synth re-entry walks
         // one term at a time from a top-of-body position; fresh empty
         // loop-stack is correct (any `Term::Loop` pushes its own frame).
-        let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<(String, crate::Type)>> = Vec::new();
         let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
         Ok(subst.apply(&ty))
     }

crates/ailang-check/src/mono.rs

@@ -720,7 +720,7 @@ pub fn collect_mono_targets(
     // loop-recur iter 2: mono re-synth begins from top-of-body —
     // empty loop-stack (any `Term::Loop` pushes its own frame as the
     // walk descends), mirroring the fresh mut-scope above.
-    let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
+    let mut loop_stack: Vec<Vec<(String, crate::Type)>> = Vec::new();
     crate::synth(
         &f.body,
         &env,
@@ -1366,7 +1366,7 @@ pub(crate) fn collect_residuals_ordered(
     // loop-recur iter 2: mono re-synth begins from top-of-body —
     // empty loop-stack (any `Term::Loop` pushes its own frame as the
     // walk descends), mirroring the fresh mut-scope above.
-    let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
+    let mut loop_stack: Vec<Vec<(String, crate::Type)>> = Vec::new();
     crate::synth(
         &f.body,
         &env,

crates/ailang-codegen/src/lib.rs

@@ -714,14 +714,20 @@ struct Emitter<'a> {
     /// dec'ing, because Implicit and Borrow do not carry the "caller
     /// handed off ownership" signal that makes the dec safe.
     current_param_modes: BTreeMap<String, ParamMode>,
-    /// Iter mut.3: per-fn map of mut-var name → (alloca SSA name,
-    /// AIL element type). Populated when entering a `Term::Mut`
-    /// block; entries removed (or restored to their prior binding)
-    /// when leaving the block. Consulted by the `Term::Var` arm of
-    /// `lower_term` before `self.locals`, matching the typecheck-
-    /// side mut-scope-stack precedence (`synth` in `ailang-check`
-    /// walks `mut_scope_stack` innermost-first before falling
-    /// through to locals/globals).
+    /// Per-fn map of name → (alloca SSA name, AIL element type) for
+    /// the two alloca-resident binding classes. Populated on entry
+    /// to a `Term::Mut` block (iter mut.3 — mut-vars) AND on entry
+    /// to a `Term::Loop` (iter loop-recur.3 — loop binders ride the
+    /// same alloca representation; the `Term::Loop` arm inserts each
+    /// binder here and `recur` stores into the slot). Entries are
+    /// removed (or restored to their prior binding) on block exit.
+    /// Consulted by the `Term::Var` arm of `lower_term` before
+    /// `self.locals` — the single load path serving both classes.
+    /// Note: only the mut-var half mirrors a typecheck-side
+    /// `mut_scope_stack`; loop binders are tracked typecheck-side in
+    /// the ordinary `locals` plus `loop_stack` (positional), not in
+    /// `mut_scope_stack` — the shared codegen map is a
+    /// representation detail, not a scope-precedence claim.
     mut_var_allocas: BTreeMap<String, (String, Type)>,
     /// loop-recur iter 3: stack of enclosing `Term::Loop` codegen
     /// frames. Each frame is `(header_block_label, binder_slots)`

crates/ailang-core/src/ast.rs

@@ -548,12 +548,18 @@ pub enum Term {
     /// additive: pre-existing fixtures hash bit-identically because
     /// none carry the `"t":"loop"` tag. `binders` has no
     /// `skip_serializing_if` (mirrors `Term::Mut.vars` — the field
-    /// is part of the shape). Typecheck binder/recur semantics land
-    /// in loop-recur iter 2 (`synth` stubs with `CheckError::Internal`
-    /// in this iter); codegen (loop-header + per-binder phi +
-    /// back-edge) in iter 3 (`lower_term` stubs with
-    /// `CodegenError::Internal`). No totality claim — an infinite
-    /// loop is legal. See `docs/specs/2026-05-17-loop-recur.md`.
+    /// is part of the shape). Typecheck (loop-recur.2): `synth`
+    /// types each binder init, the loop's type is the body's type;
+    /// `recur` arity/type is checked positionally via `loop_stack`
+    /// and `verify_loop_body` enforces `recur`-in-tail-position; a
+    /// lambda capturing a binder is rejected
+    /// (`loop-binder-captured-by-lambda`, loop-recur.tidy). Codegen
+    /// (loop-recur.3): binders lower to entry-block allocas reached
+    /// from a `loop.header` block; `recur` stores + back-edges; the
+    /// loop-carried SSA / phi form is produced by `clang -O2`
+    /// mem2reg (NOT hand-emitted phi). No totality claim — an
+    /// infinite loop is legal. See
+    /// `docs/specs/2026-05-17-loop-recur.md`.
     Loop {
         binders: Vec<LoopBinder>,
         body: Box<Term>,

crates/ailang-core/tests/carve_out_inventory.rs

@@ -3,7 +3,7 @@
 //! under `examples/*.ail.json` after milestone close. The list is
 //! hardcoded; any change is a deliberate, brainstorm-level decision.
 //!
-//! Seventeen carve-outs post iter loop-recur.2 (2026-05-17):
+//! Eighteen carve-outs post iter loop-recur.tidy (2026-05-18):
 //! - §C4 (a) subject-matter: 7 fixtures from form-a.1 milestone
 //!   close (canonical-form rejection / unbound / class-def rejection).
 //! - Iter mut.2: 5 negative typecheck fixtures for the new mut /
@@ -23,6 +23,10 @@
 //!   recur-not-in-tail-position) — the diagnostic code is the
 //!   load-bearing assertion, mirroring the §C4(a) / mut.2
 //!   negative-fixture convention.
+//! - loop-recur iter loop-recur.tidy: 1 negative typecheck fixture
+//!   for the lambda-capture-of-loop-binder rejection
+//!   (loop-binder-captured-by-lambda) — symmetric to the mut.4-tidy
+//!   `test_mut_var_captured_by_lambda.ail.json` carve-out.
 
 use std::collections::BTreeSet;
 
@@ -43,6 +47,8 @@ const EXPECTED: &[&str] = &[
     "test_mut_var_unsupported_type.ail.json",
     // Iter mut.4-tidy — lambda-capture-of-mut-var rejection
     "test_mut_var_captured_by_lambda.ail.json",
+    // Iter loop-recur.tidy — lambda-capture-of-loop-binder rejection
+    "test_loop_binder_captured_by_lambda.ail.json",
     // loop-recur iter 2 — negative typecheck fixtures
     "test_recur_arity_mismatch.ail.json",
     "test_recur_not_in_tail_position.ail.json",