iter loop-recur.1: additive Term::Loop / Term::Recur / LoopBinder foundation

First of three iterations of the standalone loop/recur milestone
(spec 97c1ed1). loop/recur become real parseable / printable /
round-trippable / hash-stable strictly-additive AST nodes across
every no-wildcard exhaustive Term match in all six crates, plus
parse/print, prose arms, DESIGN.md + form_a.md schema blocks,
drift/coverage/hash anchors, and the spec's worked sum_to program
as a green round-trip fixture. NO typecheck semantics and NO real
codegen this iter by design: synth and lower_term are stubbed
CheckError::Internal / CodegenError::Internal exactly as mut.1
(real typecheck = iter 2, real loop-header/phi/back-edge = iter 3).

Two binding Boss design calls recorded in the plan header and the
journal: (1) verify_tail_positions "byte-unchanged" = its tail-app
verification role is unchanged, not its source — it is an
exhaustive no-wildcard match so two descent-only arms are
mandatory; acceptance evidence is the tail-app non-regression test.
(2) codegen is in iter-1 scope as stubs/pass-throughs because the
workspace must compile for cargo test --workspace.

Three plan-pseudo-vs-reality substitutions (serde Type::Con
literal, bare Int -> (con Int), unqualified LoopBinder) and one
recon-undercount integration-test site, all intent-preserving and
journalled. Boss forward-fix folded in: the committed specs
themselves wrote bare Int in the loop-binder snippets (parses as
Type::Var) — corrected the three headline snippets to (con Int) for
doc-honesty (no design/schema change).

cargo test --workspace 600 -> 608 / 0 red (Boss-reran
independently); iter13a + new loop_recur hash pins green.

bench/orchestrator-stats/2026-05-17-iter-loop-recur.1.json

@@ -0,0 +1,21 @@
+{
+  "iter_id": "loop-recur.1",
+  "date": "2026-05-17",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 7,
+  "tasks_completed": 7,
+  "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 0, "6": 0, "7": 0 },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null,
+  "notes": {
+    "plan_pseudo_vs_reality_substitutions": 3,
+    "recon_undercount_sites": 1,
+    "boss_design_calls_honoured": 2,
+    "tests_before": 600,
+    "tests_after": 608,
+    "files_modified": 24,
+    "files_created": 1
+  }
+}

crates/ail/src/main.rs

@@ -1544,6 +1544,24 @@ fn walk_term(
             }
             walk_term(value, out, builtins, scope);
         }
+        Term::Loop { binders, body } => {
+            let mut newly = Vec::new();
+            for b in binders {
+                walk_term(&b.init, out, builtins, scope);
+                if scope.insert(b.name.clone()) {
+                    newly.push(b.name.clone());
+                }
+            }
+            walk_term(body, out, builtins, scope);
+            for n in newly {
+                scope.remove(&n);
+            }
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a, out, builtins, scope);
+            }
+        }
     }
 }
 
@@ -2785,6 +2803,42 @@ fn rewrite_def(
                     changed,
                 );
             }
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    rewrite_type(
+                        &mut b.ty,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                    rewrite_term(
+                        &mut b.init,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                }
+                rewrite_term(
+                    body,
+                    owning_module,
+                    local_types,
+                    import_names,
+                    changed,
+                );
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    rewrite_term(
+                        a,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                }
+            }
         }
     }
 

crates/ail/tests/codegen_import_map_fallback_pin.rs

@@ -101,6 +101,15 @@ fn synthesised_print_uses_user_module_show_via_fallback() {
                     || contains_xmod_show_var(body)
             }
             Term::Assign { value, .. } => contains_xmod_show_var(value),
+            // loop-recur iter 1: a `Term::Loop` cannot itself host a
+            // synthesised cross-module reference, but recurse
+            // defensively through binder inits / body / recur args,
+            // mirroring the `Term::Mut` arm above.
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| contains_xmod_show_var(&b.init))
+                    || contains_xmod_show_var(body)
+            }
+            Term::Recur { args } => args.iter().any(contains_xmod_show_var),
             Term::Lit { .. } => false,
         }
     }

crates/ailang-check/src/lib.rs

@@ -261,6 +261,23 @@ pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Typ
             name: name.clone(),
             value: Box::new(substitute_rigids_in_term(value, mapping)),
         },
+        Term::Loop { binders, body } => Term::Loop {
+            binders: binders
+                .iter()
+                .map(|b| ailang_core::ast::LoopBinder {
+                    name: b.name.clone(),
+                    ty: substitute_rigids(&b.ty, mapping),
+                    init: substitute_rigids_in_term(&b.init, mapping),
+                })
+                .collect(),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+        },
+        Term::Recur { args } => Term::Recur {
+            args: args
+                .iter()
+                .map(|a| substitute_rigids_in_term(a, mapping))
+                .collect(),
+        },
     }
 }
 
@@ -2679,6 +2696,31 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
         // be in tail position. Its `value` is also not in tail
         // position.
         Term::Assign { value, .. } => verify_tail_positions(value, false),
+        // loop-recur iter 1: binder inits are evaluated once on loop
+        // entry, NOT in tail position (mirror the Term::Mut arm
+        // above). The loop body inherits the enclosing tail position
+        // (the loop's value is the body's value on the exiting
+        // iteration). This arm only defines tail-app descent through
+        // the new node; it makes NO claim about recur tail-position
+        // (that is loop-recur iter 2's `verify_loop_body`). The
+        // tail-app verification role is unchanged — no pre-existing
+        // fixture contains a `loop`/`recur` node.
+        Term::Loop { binders, body } => {
+            for b in binders {
+                verify_tail_positions(&b.init, false)?;
+            }
+            verify_tail_positions(body, is_tail)
+        }
+        // recur transfers control and does not fall through, so there
+        // is no tail position to propagate. Its args are evaluated in
+        // non-tail position (call-argument-like). Introduces no
+        // tail-app violation.
+        Term::Recur { args } => {
+            for a in args {
+                verify_tail_positions(a, false)?;
+            }
+            Ok(())
+        }
     }
 }
 
@@ -3592,6 +3634,8 @@ pub(crate) fn synth(
                         Term::ReuseAs { .. } => "reuse-as",
                         Term::Mut { .. } => "mut",
                         Term::Assign { .. } => "assign",
+                        Term::Loop { .. } => "loop",
+                        Term::Recur { .. } => "recur",
                         Term::Ctor { .. } | Term::Lam { .. } => unreachable!(),
                     };
                     return Err(CheckError::ReuseAsNonAllocatingBody {
@@ -3687,6 +3731,15 @@ pub(crate) fn synth(
                 }
             }
         }
+        // loop-recur iter 1: typecheck semantics (binder typing,
+        // recur arity/type unification, verify_loop_body
+        // tail-position, the four Recur* CheckError variants) land
+        // in loop-recur iter 2. This iter stubs the dispatch so the
+        // workspace compiles and round-trips; no loop/recur fixture
+        // is typechecked in iter 1. Mirrors mut.1's synth stub.
+        Term::Loop { .. } | Term::Recur { .. } => Err(CheckError::Internal(
+            "Term::Loop/Term::Recur typecheck lands in loop-recur iter 2".into(),
+        )),
     }
 }
 

crates/ailang-check/src/lift.rs

@@ -397,6 +397,25 @@ impl<'a> Lifter<'a> {
                 name: name.clone(),
                 value: Box::new(self.lift_in_term(value, locals, in_def)?),
             }),
+            Term::Loop { binders, body } => Ok(Term::Loop {
+                binders: binders
+                    .iter()
+                    .map(|b| {
+                        Ok(ailang_core::ast::LoopBinder {
+                            name: b.name.clone(),
+                            ty: b.ty.clone(),
+                            init: self.lift_in_term(&b.init, locals, in_def)?,
+                        })
+                    })
+                    .collect::<Result<Vec<_>>>()?,
+                body: Box::new(self.lift_in_term(body, locals, in_def)?),
+            }),
+            Term::Recur { args } => Ok(Term::Recur {
+                args: args
+                    .iter()
+                    .map(|a| self.lift_in_term(a, locals, in_def))
+                    .collect::<Result<Vec<_>>>()?,
+            }),
             Term::LetRec { name, ty, params, body, in_term } => {
                 // Iter 16b.3: post-order traversal — lift any inner
                 // LetRecs first. Within the body's scope, `name` and
@@ -761,6 +780,10 @@ fn contains_any_letrec(m: &Module) -> bool {
                 vars.iter().any(|v| term_has_letrec(&v.init)) || term_has_letrec(body)
             }
             Term::Assign { value, .. } => term_has_letrec(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| term_has_letrec(&b.init)) || term_has_letrec(body)
+            }
+            Term::Recur { args } => args.iter().any(term_has_letrec),
         }
     }
     for def in &m.defs {

crates/ailang-check/src/linearity.rs

@@ -609,6 +609,17 @@ impl<'a> Checker<'a> {
                 // a tracked binder). Walk the `value` normally.
                 self.walk(value, Position::Consume);
             }
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a, Position::Consume);
+                }
+            }
         }
     }
 
@@ -795,6 +806,8 @@ fn make_reuse_as_source_not_bare_var(def: &str, source: &Term, body: &Term) -> D
         Term::ReuseAs { .. } => "reuse-as",
         Term::Mut { .. } => "mut",
         Term::Assign { .. } => "assign",
+        Term::Loop { .. } => "loop",
+        Term::Recur { .. } => "recur",
     };
     let replacement = term_to_form_a(body);
     Diagnostic::error(
@@ -934,6 +947,14 @@ fn any_sub_binder_consumed_for(
         Term::Assign { value, .. } => {
             any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors)
         }
+        Term::Loop { binders, body } => {
+            binders.iter().any(|b| {
+                any_sub_binder_consumed_for(&b.init, pname, uniq, def_name, ctors)
+            }) || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
+        }
+        Term::Recur { args } => args.iter().any(|a| {
+            any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)
+        }),
     }
 }
 

crates/ailang-check/src/mono.rs

@@ -1243,6 +1243,17 @@ fn rewrite_mono_calls(
         Term::Assign { value, .. } => {
             rewrite_mono_calls(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
         }
+        Term::Loop { binders, body } => {
+            for b in binders.iter_mut() {
+                rewrite_mono_calls(&mut b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+            }
+            rewrite_mono_calls(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+        }
+        Term::Recur { args } => {
+            for a in args.iter_mut() {
+                rewrite_mono_calls(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+            }
+        }
         Term::Lit { .. } => {}
     }
 }
@@ -1617,6 +1628,17 @@ fn interleave_slots(
         Term::Assign { value, .. } => {
             interleave_slots(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
         }
+        Term::Loop { binders, body } => {
+            for b in binders {
+                interleave_slots(&b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+            interleave_slots(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                interleave_slots(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+        }
         Term::Lit { .. } => {}
     }
 }

crates/ailang-check/src/pre_desugar_validation.rs

@@ -133,6 +133,18 @@ fn walk_term(t: &Term) -> Result<(), CheckError> {
             walk_term(body)
         }
         Term::Assign { value, .. } => walk_term(value),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_term(&b.init)?;
+            }
+            walk_term(body)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a)?;
+            }
+            Ok(())
+        }
     }
 }
 

crates/ailang-check/src/reuse_shape.rs

@@ -265,6 +265,17 @@ impl<'a> Checker<'a> {
                 self.walk(body);
             }
             Term::Assign { value, .. } => self.walk(value),
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init);
+                }
+                self.walk(body);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a);
+                }
+            }
         }
     }
 

crates/ailang-check/src/uniqueness.rs

@@ -352,6 +352,17 @@ impl<'a> Walker<'a> {
             Term::Assign { value, .. } => {
                 self.walk(value, Position::Consume);
             }
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a, Position::Consume);
+                }
+            }
         }
     }
 

crates/ailang-codegen/src/escape.rs

@@ -201,6 +201,17 @@ fn walk(t: &Term, out: &mut NonEscapeSet) {
             walk(body, out);
         }
         Term::Assign { value, .. } => walk(value, out),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk(&b.init, out);
+            }
+            walk(body, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk(a, out);
+            }
+        }
         Term::Lit { .. } | Term::Var { .. } => {}
     }
 }
@@ -395,6 +406,22 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             escapes(body, tainted, in_tail)
         }
         Term::Assign { value, .. } => escapes(value, tainted, false),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                if escapes(&b.init, tainted, false) {
+                    return true;
+                }
+            }
+            escapes(body, tainted, in_tail)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                if escapes(a, tainted, false) {
+                    return true;
+                }
+            }
+            false
+        }
     }
 }
 
@@ -524,6 +551,24 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<
             }
             collect_free_vars(value, bound, out);
         }
+        Term::Loop { binders, body } => {
+            let mut newly: Vec<String> = Vec::new();
+            for b in binders {
+                collect_free_vars(&b.init, bound, out);
+                if bound.insert(b.name.clone()) {
+                    newly.push(b.name.clone());
+                }
+            }
+            collect_free_vars(body, bound, out);
+            for n in newly {
+                bound.remove(&n);
+            }
+        }
+        Term::Recur { args } => {
+            for a in args {
+                collect_free_vars(a, bound, out);
+            }
+        }
     }
 }
 

crates/ailang-codegen/src/lambda.rs

@@ -505,6 +505,24 @@ impl<'a> Emitter<'a> {
                 }
                 Self::collect_captures(value, bound, captures, captures_set, builtins, top_level);
             }
+            Term::Loop { binders, body } => {
+                let mut newly_bound: Vec<String> = Vec::new();
+                for b in binders {
+                    Self::collect_captures(&b.init, bound, captures, captures_set, builtins, top_level);
+                    if bound.insert(b.name.clone()) {
+                        newly_bound.push(b.name.clone());
+                    }
+                }
+                Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
+                for n in newly_bound {
+                    bound.remove(&n);
+                }
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
+                }
+            }
         }
     }
 

crates/ailang-codegen/src/lib.rs

@@ -1837,6 +1837,14 @@ impl<'a> Emitter<'a> {
                 ));
                 Ok(("0".into(), "i8".into()))
             }
+            // loop-recur iter 1: real codegen (loop-header block,
+            // per-binder phi, back-edge br) lands in iter 3. This
+            // iter stubs the dispatch so the workspace compiles; no
+            // loop/recur program is codegen'd in iter 1. Mirrors
+            // mut.1's lower_term stub.
+            Term::Loop { .. } | Term::Recur { .. } => Err(CodegenError::Internal(
+                "Term::Loop/Term::Recur lowering lands in loop-recur iter 3".into(),
+            )),
         }
     }
 
@@ -3093,6 +3101,13 @@ impl<'a> Emitter<'a> {
             // is exhaustive on Term so the arms must exist.
             Term::Mut { body, .. } => self.synth_with_extras(body, extras),
             Term::Assign { .. } => Ok(Type::unit()),
+            // loop-recur iter 1: a Term::Loop's static type is the
+            // body's type (mirror Term::Mut). Term::Recur does not
+            // fall through; a Unit stub is safe — this arm is never
+            // hit on the shipping path because lower_term stubs
+            // Loop/Recur, and iter 1 codegens no loop/recur program.
+            Term::Loop { body, .. } => self.synth_with_extras(body, extras),
+            Term::Recur { .. } => Ok(Type::unit()),
         }
     }
 }

crates/ailang-core/specs/form_a.md

@@ -286,6 +286,8 @@ Parenthesised forms:
 (mut (var NAME TYPE INIT)* BODY-TERM+)  ; local mutable-state block (Iter mut.1)
 (var NAME TYPE INIT)                    ; mut-var declaration; only inside (mut ...)
 (assign NAME VALUE-TERM)                ; mut-var update; only inside (mut ...)
+(loop (NAME TYPE INIT)* BODY-TERM+)     ; strict iteration block (loop-recur)
+(recur ARG*)                            ; re-enter enclosing loop (loop-recur)
 ```
 
 Notes:
@@ -324,6 +326,17 @@ Notes:
   pass (iter mut.2) rejects it with `mut-assign-out-of-scope`. The
   expression's static type is Unit. See spec
   `docs/specs/2026-05-15-mut-local.md`.
+- `loop` opens a strict iteration block. `(NAME TYPE INIT)` binder
+  triples (zero or more) are followed by a body of zero or more
+  Unit-typed statements and exactly one final expression (right-
+  folded into `Term::Seq` like `mut`). `recur` re-enters the
+  lexically innermost enclosing `loop`, rebinding its binders
+  positionally; `(recur ARG*)`'s arg count must equal the binder
+  count and `recur` must be in tail position of the loop body —
+  both enforced at typecheck (`recur-arity-mismatch`,
+  `recur-not-in-tail-position`). `loop`/`recur` make no termination
+  claim: a `loop` with no non-`recur` exit runs forever. See
+  `docs/specs/2026-05-17-loop-recur.md`.
 
 ## Patterns
 

crates/ailang-core/src/ast.rs

@@ -540,6 +540,33 @@ pub enum Term {
         name: String,
         value: Box<Term>,
     },
+    /// loop-recur iter 1: a strict iteration block. `binders`
+    /// declares one or more loop parameters (name, type, init),
+    /// evaluated in order on loop entry; `body` is evaluated with
+    /// all binders in scope. The loop's value is `body`'s value on
+    /// the iteration that exits via a non-`recur` branch. Strictly
+    /// 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`.
+    Loop {
+        binders: Vec<LoopBinder>,
+        body: Box<Term>,
+    },
+    /// loop-recur iter 1: re-enter the lexically innermost enclosing
+    /// `Term::Loop`, rebinding its binders positionally to `args`.
+    /// Transfers control (no fall-through); valid only in tail
+    /// position of its enclosing loop — enforced at typecheck in
+    /// iter 2 (`RecurNotInTailPosition`). Additive `"t":"recur"`
+    /// tag; pre-existing fixtures hash bit-identically.
+    Recur {
+        args: Vec<Term>,
+    },
 }
 
 /// One arm of a [`Term::Match`].
@@ -583,6 +610,27 @@ pub struct MutVar {
     pub init: Term,
 }
 
+/// loop-recur iter 1: one binder of a [`Term::Loop`]. Mirrors
+/// [`MutVar`]'s `(name, type, init)` triple exactly so the Form-A
+/// surface vocabulary is shared (`(NAME TYPE INIT)`); it is a
+/// nested field of `Term::Loop`, not a first-class `Term` (loop
+/// binders cannot escape the enclosing loop). `recur` rebinds these
+/// positionally per iteration. The `ty` JSON field is `"type"`,
+/// matching `MutVar` and the spec schema.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct LoopBinder {
+    /// The binder's lexical name. Within the enclosing `Term::Loop`,
+    /// a `Term::Var { name }` resolves to this binding.
+    pub name: String,
+    /// The binder's declared type.
+    #[serde(rename = "type")]
+    pub ty: Type,
+    /// Initial value, evaluated once on loop entry in scope of the
+    /// outer environment plus already-declared binders of the same
+    /// `Term::Loop` (declaration order).
+    pub init: Term,
+}
+
 /// A match pattern.
 ///
 /// The JSON discriminator is the `p` field. Patterns are linear: each
@@ -949,4 +997,59 @@ mod tests {
             other => panic!("variant mismatch: {other:?}"),
         }
     }
+
+    /// loop-recur iter 1: pin the canonical-bytes shape of a
+    /// `Term::Loop` with one binder. Mirrors the mut-empty-vars pin:
+    /// `binders` stays present (no `skip_serializing_if`).
+    #[test]
+    fn term_loop_one_binder_serialises_with_explicit_binders_field() {
+        let t = Term::Loop {
+            binders: vec![LoopBinder {
+                name: "i".into(),
+                ty: Type::int(),
+                init: Term::Lit {
+                    lit: Literal::Int { value: 0 },
+                },
+            }],
+            body: Box::new(Term::Var { name: "i".into() }),
+        };
+        let bytes = serde_json::to_string(&t).expect("serialise");
+        assert_eq!(
+            bytes,
+            r#"{"t":"loop","binders":[{"name":"i","type":{"k":"con","name":"Int"},"init":{"t":"lit","lit":{"kind":"int","value":0}}}],"body":{"t":"var","name":"i"}}"#,
+        );
+        let back: Term = serde_json::from_str(&bytes).expect("deserialise");
+        match back {
+            Term::Loop { binders, body } => {
+                assert_eq!(binders.len(), 1);
+                assert_eq!(binders[0].name, "i");
+                match *body {
+                    Term::Var { name } => assert_eq!(name, "i"),
+                    other => panic!("body mismatch: {other:?}"),
+                }
+            }
+            other => panic!("variant mismatch: {other:?}"),
+        }
+    }
+
+    /// loop-recur iter 1: round-trip a `Term::Recur` through JSON.
+    /// Pins `{ "t": "recur", "args": [...] }`.
+    #[test]
+    fn term_recur_round_trips_through_json() {
+        let t = Term::Recur {
+            args: vec![Term::Lit {
+                lit: Literal::Int { value: 1 },
+            }],
+        };
+        let bytes = serde_json::to_string(&t).expect("serialise");
+        assert_eq!(
+            bytes,
+            r#"{"t":"recur","args":[{"t":"lit","lit":{"kind":"int","value":1}}]}"#,
+        );
+        let back: Term = serde_json::from_str(&bytes).expect("deserialise");
+        match back {
+            Term::Recur { args } => assert_eq!(args.len(), 1),
+            other => panic!("variant mismatch: {other:?}"),
+        }
+    }
 }

crates/ailang-core/src/desugar.rs

@@ -363,6 +363,18 @@ fn collect_used_in_term(t: &Term, used: &mut BTreeSet<String>) {
             used.insert(name.clone());
             collect_used_in_term(value, used);
         }
+        Term::Loop { binders, body } => {
+            for b in binders {
+                used.insert(b.name.clone());
+                collect_used_in_term(&b.init, used);
+            }
+            collect_used_in_term(body, used);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                collect_used_in_term(a, used);
+            }
+        }
     }
 }
 
@@ -590,6 +602,37 @@ impl Desugarer {
                 name: name.clone(),
                 value: Box::new(self.desugar_term(value, scope)),
             },
+            Term::Loop { binders, body } => {
+                // loop-recur iter 1: structural recursion mirroring
+                // the Term::Mut arm. Each binder's init is desugared
+                // in scope of the outer env plus already-declared
+                // binders; the body sees all binders. The LetBound
+                // sentinel keeps generated fresh names off binder
+                // names.
+                let mut inner = scope.clone();
+                let new_binders: Vec<LoopBinder> = binders
+                    .iter()
+                    .map(|b| {
+                        let init = self.desugar_term(&b.init, &inner);
+                        inner.insert(b.name.clone(), ScopeEntry::LetBound);
+                        LoopBinder {
+                            name: b.name.clone(),
+                            ty: b.ty.clone(),
+                            init,
+                        }
+                    })
+                    .collect();
+                Term::Loop {
+                    binders: new_binders,
+                    body: Box::new(self.desugar_term(body, &inner)),
+                }
+            }
+            Term::Recur { args } => Term::Recur {
+                args: args
+                    .iter()
+                    .map(|a| self.desugar_term(a, scope))
+                    .collect(),
+            },
             Term::LetRec { name, ty, params, body, in_term } => {
                 // Iter 16b.1: lift to a synthetic top-level fn (no-capture).
                 // Iter 16b.2: extend the lift to the path-1 safe subset —
@@ -1234,6 +1277,22 @@ pub fn free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut BTreeSet<
             }
             free_vars_in_term(value, bound, out);
         }
+        Term::Loop { binders, body } => {
+            // loop-recur iter 1: binder names bind inside the loop —
+            // each init sees the outer env plus already-declared
+            // binders; the body sees all. Mirrors the Term::Mut arm.
+            let mut b = bound.clone();
+            for bd in binders {
+                free_vars_in_term(&bd.init, &b, out);
+                b.insert(bd.name.clone());
+            }
+            free_vars_in_term(body, &b, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                free_vars_in_term(a, bound, out);
+            }
+        }
     }
 }
 
@@ -1427,6 +1486,43 @@ pub fn subst_var(t: &Term, from: &str, to: &str) -> Term {
             name: name.clone(),
             value: Box::new(subst_var(value, from, to)),
         },
+        Term::Loop { binders, body } => {
+            // loop-recur iter 1: binders lexically shadow outer
+            // names, symmetric to the Term::Mut arm — once a binder
+            // named `from` is declared, later inits and the body
+            // stop being substituted.
+            let mut shadowed = false;
+            let new_binders: Vec<LoopBinder> = binders
+                .iter()
+                .map(|b| {
+                    let init = if shadowed {
+                        b.init.clone()
+                    } else {
+                        subst_var(&b.init, from, to)
+                    };
+                    if b.name == from {
+                        shadowed = true;
+                    }
+                    LoopBinder {
+                        name: b.name.clone(),
+                        ty: b.ty.clone(),
+                        init,
+                    }
+                })
+                .collect();
+            let body_rw = if shadowed {
+                (**body).clone()
+            } else {
+                subst_var(body, from, to)
+            };
+            Term::Loop {
+                binders: new_binders,
+                body: Box::new(body_rw),
+            }
+        }
+        Term::Recur { args } => Term::Recur {
+            args: args.iter().map(|a| subst_var(a, from, to)).collect(),
+        },
     }
 }
 
@@ -1568,6 +1664,23 @@ pub fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[Stri
             name: assign_name.clone(),
             value: Box::new(subst_call_with_extras(value, name, lifted, extras)),
         },
+        Term::Loop { binders, body } => Term::Loop {
+            binders: binders
+                .iter()
+                .map(|b| LoopBinder {
+                    name: b.name.clone(),
+                    ty: b.ty.clone(),
+                    init: subst_call_with_extras(&b.init, name, lifted, extras),
+                })
+                .collect(),
+            body: Box::new(subst_call_with_extras(body, name, lifted, extras)),
+        },
+        Term::Recur { args } => Term::Recur {
+            args: args
+                .iter()
+                .map(|a| subst_call_with_extras(a, name, lifted, extras))
+                .collect(),
+        },
     }
 }
 
@@ -1640,6 +1753,13 @@ pub fn find_non_callee_use(t: &Term, name: &str) -> Option<Term> {
                 find_non_callee_use(value, name)
             }
         }
+        Term::Loop { binders, body } => binders
+            .iter()
+            .find_map(|b| find_non_callee_use(&b.init, name))
+            .or_else(|| find_non_callee_use(body, name)),
+        Term::Recur { args } => {
+            args.iter().find_map(|a| find_non_callee_use(a, name))
+        }
     }
 }
 
@@ -1687,6 +1807,10 @@ mod tests {
                 vars.iter().any(|v| any_nested_ctor(&v.init)) || any_nested_ctor(body)
             }
             Term::Assign { value, .. } => any_nested_ctor(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_nested_ctor(&b.init)) || any_nested_ctor(body)
+            }
+            Term::Recur { args } => args.iter().any(any_nested_ctor),
         }
     }
 
@@ -1717,6 +1841,10 @@ mod tests {
                 vars.iter().any(|v| any_let_rec(&v.init)) || any_let_rec(body)
             }
             Term::Assign { value, .. } => any_let_rec(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_let_rec(&b.init)) || any_let_rec(body)
+            }
+            Term::Recur { args } => args.iter().any(any_let_rec),
         }
     }
 
@@ -2838,6 +2966,10 @@ mod tests {
                 vars.iter().any(|v| any_lit_pattern(&v.init)) || any_lit_pattern(body)
             }
             Term::Assign { value, .. } => any_lit_pattern(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_lit_pattern(&b.init)) || any_lit_pattern(body)
+            }
+            Term::Recur { args } => args.iter().any(any_lit_pattern),
         }
     }
 

crates/ailang-core/src/workspace.rs

@@ -1259,6 +1259,19 @@ where
             walk_term_embedded_types(body, f)
         }
         Term::Assign { value, .. } => walk_term_embedded_types(value, f),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_type(&b.ty, f)?;
+                walk_term_embedded_types(&b.init, f)?;
+            }
+            walk_term_embedded_types(body, f)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term_embedded_types(a, f)?;
+            }
+            Ok(())
+        }
     }
 }
 
@@ -1392,6 +1405,18 @@ where
             walk_term(body, f)
         }
         Term::Assign { value, .. } => walk_term(value, f),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_term(&b.init, f)?;
+            }
+            walk_term(body, f)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a, f)?;
+            }
+            Ok(())
+        }
     }
 }
 

crates/ailang-core/tests/design_schema_drift.rs

@@ -151,6 +151,17 @@ fn design_md_anchors_every_term_variant() {
                 value: Box::new(Term::Lit { lit: Literal::Unit }),
             },
         ),
+        (
+            r#""t": "loop""#,
+            Term::Loop {
+                binders: Vec::new(),
+                body: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
+        (
+            r#""t": "recur""#,
+            Term::Recur { args: vec![] },
+        ),
     ];
 
     for (anchor, term) in exemplars {
@@ -172,6 +183,8 @@ fn design_md_anchors_every_term_variant() {
             Term::ReuseAs { .. } => "reuse-as",
             Term::Mut { .. } => "mut",
             Term::Assign { .. } => "assign",
+            Term::Loop { .. } => "loop",
+            Term::Recur { .. } => "recur",
         };
         assert!(
             data_model_section().contains(anchor),

crates/ailang-core/tests/hash_pin.rs

@@ -87,6 +87,28 @@ fn iter13a_schema_extension_preserves_pre_13a_hashes() {
     assert_eq!(def_hash(int_list_def), "b082192bd0c99202");
 }
 
+/// loop-recur iter 1 regression: adding `Term::Loop` / `Term::Recur`
+/// (and `struct LoopBinder`) must NOT change canonical-JSON hashes
+/// of any pre-loop-recur definition. The additive variant carries a
+/// new `"t"` tag absent from every pre-existing fixture, so the
+/// recorded hashes below must stay byte-identical. If this fires,
+/// the extension is non-additive (a `skip_serializing_if` is missing
+/// or an existing variant's shape drifted).
+#[test]
+fn loop_recur_schema_extension_preserves_pre_loop_recur_hashes() {
+    let examples = examples_dir();
+
+    let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
+        .expect("examples/sum.ail loads");
+    let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
+    assert_eq!(def_hash(sum_def), "db33f57cb329935e");
+
+    let list_mod = ailang_surface::load_module(&examples.join("list.ail"))
+        .expect("examples/list.ail loads");
+    let int_list_def = list_mod.defs.iter().find(|d| d.name() == "IntList").unwrap();
+    assert_eq!(def_hash(int_list_def), "b082192bd0c99202");
+}
+
 /// Iter 19b regression: adding `suppress` to FnDef must NOT change
 /// canonical-JSON hashes of any pre-19b fn whose `suppress` is empty.
 /// The `skip_serializing_if = "Vec::is_empty"` predicate on the field

crates/ailang-core/tests/schema_coverage.rs

@@ -49,6 +49,8 @@ enum VariantTag {
     TermReuseAs,
     TermMut,
     TermAssign,
+    TermLoop,
+    TermRecur,
     // Pattern
     PatternWild,
     PatternVar,
@@ -96,6 +98,8 @@ const EXPECTED_VARIANTS: &[VariantTag] = &[
     VariantTag::TermReuseAs,
     VariantTag::TermMut,
     VariantTag::TermAssign,
+    VariantTag::TermLoop,
+    VariantTag::TermRecur,
     VariantTag::PatternWild,
     VariantTag::PatternVar,
     VariantTag::PatternLit,
@@ -244,6 +248,20 @@ fn visit_term(t: &Term, observed: &mut HashSet<VariantTag>) {
             observed.insert(VariantTag::TermAssign);
             visit_term(value, observed);
         }
+        Term::Loop { binders, body } => {
+            observed.insert(VariantTag::TermLoop);
+            for b in binders {
+                visit_type(&b.ty, observed);
+                visit_term(&b.init, observed);
+            }
+            visit_term(body, observed);
+        }
+        Term::Recur { args } => {
+            observed.insert(VariantTag::TermRecur);
+            for a in args {
+                visit_term(a, observed);
+            }
+        }
     }
 }
 

crates/ailang-core/tests/spec_drift.rs

@@ -128,6 +128,17 @@ fn spec_mentions_every_term_variant() {
                 value: Box::new(Term::Lit { lit: Literal::Unit }),
             },
         ),
+        (
+            "(loop",
+            Term::Loop {
+                binders: Vec::new(),
+                body: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
+        (
+            "(recur",
+            Term::Recur { args: vec![] },
+        ),
     ];
 
     for (anchor, term) in exemplars {
@@ -151,6 +162,8 @@ fn spec_mentions_every_term_variant() {
             Term::ReuseAs { .. } => "reuse-as",
             Term::Mut { .. } => "mut",
             Term::Assign { .. } => "assign",
+            Term::Loop { .. } => "loop",
+            Term::Recur { .. } => "recur",
         };
         assert!(
             FORM_A_SPEC.contains(anchor),

crates/ailang-prose/src/lib.rs

@@ -935,6 +935,34 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, ow
             out.push_str(" := ");
             write_term(out, value, level, owning_module);
         }
+        Term::Loop { binders, body } => {
+            // loop-recur iter 1: minimal-correctness Form-B render.
+            // Prose surface for loop is not yet designed; render the
+            // shape so a reader sees it without overcommitting.
+            out.push_str("loop {\n");
+            for b in binders {
+                indent(out, level + 1);
+                out.push_str(&b.name);
+                out.push_str(" = ");
+                write_term(out, &b.init, level + 1, owning_module);
+                out.push_str(";\n");
+            }
+            indent(out, level + 1);
+            write_term(out, body, level + 1, owning_module);
+            out.push('\n');
+            indent(out, level);
+            out.push('}');
+        }
+        Term::Recur { args } => {
+            out.push_str("recur(");
+            for (i, a) in args.iter().enumerate() {
+                if i > 0 {
+                    out.push_str(", ");
+                }
+                write_term(out, a, level, owning_module);
+            }
+            out.push(')');
+        }
     }
 }
 
@@ -1133,6 +1161,28 @@ fn count_free_var(name: &str, t: &Term) -> usize {
             let n_use = if assign_name == name { 1 } else { 0 };
             n_use + count_free_var(name, value)
         }
+        // loop-recur iter 1: a binder named `name` shadows the outer
+        // binding for later binder inits and the body. Inits before
+        // the shadowing binder still see the outer `name`.
+        Term::Loop { binders, body } => {
+            let mut total = 0usize;
+            let mut shadowed = false;
+            for b in binders {
+                if !shadowed {
+                    total += count_free_var(name, &b.init);
+                }
+                if b.name == name {
+                    shadowed = true;
+                }
+            }
+            if !shadowed {
+                total += count_free_var(name, body);
+            }
+            total
+        }
+        Term::Recur { args } => {
+            args.iter().map(|a| count_free_var(name, a)).sum()
+        }
     }
 }
 
@@ -1285,6 +1335,45 @@ fn subst_var_with_term(t: &Term, name: &str, replacement: &Term) -> Term {
             name: assign_name.clone(),
             value: Box::new(subst_var_with_term(value, name, replacement)),
         },
+        // loop-recur iter 1: lexical-shadow semantics symmetric to
+        // count_free_var — once a binder named `name` is declared,
+        // later inits and the body are not rewritten.
+        Term::Loop { binders, body } => {
+            let mut shadowed = false;
+            let new_binders: Vec<ailang_core::ast::LoopBinder> = binders
+                .iter()
+                .map(|b| {
+                    let init = if shadowed {
+                        b.init.clone()
+                    } else {
+                        subst_var_with_term(&b.init, name, replacement)
+                    };
+                    if b.name == name {
+                        shadowed = true;
+                    }
+                    ailang_core::ast::LoopBinder {
+                        name: b.name.clone(),
+                        ty: b.ty.clone(),
+                        init,
+                    }
+                })
+                .collect();
+            let body_rw = if shadowed {
+                (**body).clone()
+            } else {
+                subst_var_with_term(body, name, replacement)
+            };
+            Term::Loop {
+                binders: new_binders,
+                body: Box::new(body_rw),
+            }
+        }
+        Term::Recur { args } => Term::Recur {
+            args: args
+                .iter()
+                .map(|a| subst_var_with_term(a, name, replacement))
+                .collect(),
+        },
     }
 }
 

crates/ailang-surface/src/parse.rs

@@ -1212,6 +1212,8 @@ impl<'a> Parser<'a> {
                     "reuse-as" => self.parse_reuse_as(),
                     "mut" => self.parse_mut(),
                     "assign" => self.parse_assign(),
+                    "loop" => self.parse_loop(),
+                    "recur" => self.parse_recur(),
                     other => {
                         let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
                         Err(ParseError::Production {
@@ -1220,7 +1222,7 @@ impl<'a> Parser<'a> {
                                 "unknown term head `{other}`; expected one of \
                                 `app`, `tail-app`, `lam`, `let`, `let-rec`, `if`, `match`, `do`, \
                                 `tail-do`, `seq`, `term-ctor`, `clone`, `reuse-as`, `mut`, \
-                                `assign`, `lit-unit`"
+                                `assign`, `loop`, `recur`, `lit-unit`"
                             ),
                             pos,
                         })
@@ -1642,6 +1644,97 @@ impl<'a> Parser<'a> {
         })
     }
 
+    /// loop-recur iter 1: `(loop (NAME TYPE INIT)* BODY_TERM+)` —
+    /// strict iteration block. Reads zero or more `(NAME TYPE INIT)`
+    /// binder triples (bare, no leading keyword — unlike `(var ...)`,
+    /// the loop binder triple has no `var` keyword), then ≥ 1
+    /// trailing terms right-folded into `Term::Seq` (mirrors
+    /// `parse_mut`). The binder/body boundary is disambiguated by the
+    /// inner head: a binder's first inner token is an ident NAME
+    /// (never a term-head keyword), whereas a parenthesised body form
+    /// (`(if …)`, `(recur …)`, `(app …)`, …) opens with a term-head
+    /// keyword — so a leading `(` is treated as a binder only while
+    /// its inner head is not a term-head keyword.
+    fn parse_loop(&mut self) -> Result<Term, ParseError> {
+        fn is_term_head_kw(h: &str) -> bool {
+            matches!(
+                h,
+                "lit-unit"
+                    | "app"
+                    | "tail-app"
+                    | "term-ctor"
+                    | "match"
+                    | "do"
+                    | "tail-do"
+                    | "seq"
+                    | "lam"
+                    | "if"
+                    | "let"
+                    | "let-rec"
+                    | "clone"
+                    | "reuse-as"
+                    | "mut"
+                    | "assign"
+                    | "loop"
+                    | "recur"
+            )
+        }
+
+        let head_pos = self.peek().map(|t| t.span.start).unwrap_or(0);
+        self.expect_lparen("loop-term")?;
+        self.expect_keyword("loop")?;
+
+        let mut binders: Vec<ailang_core::ast::LoopBinder> = Vec::new();
+        while matches!(self.peek_head_ident(), Some(h) if !is_term_head_kw(h)) {
+            self.expect_lparen("loop-binder")?;
+            let name = self.expect_ident("loop-binder-name")?;
+            let ty = self.parse_type()?;
+            let init = self.parse_term()?;
+            self.expect_rparen("loop-binder")?;
+            binders.push(ailang_core::ast::LoopBinder { name, ty, init });
+        }
+
+        let mut body_stmts: Vec<Term> = Vec::new();
+        while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
+            body_stmts.push(self.parse_term()?);
+        }
+        if body_stmts.is_empty() {
+            return Err(ParseError::Production {
+                production: "loop-term",
+                message: "(loop ...) requires at least one body expression after binders".into(),
+                pos: head_pos,
+            });
+        }
+        self.expect_rparen("loop-term")?;
+
+        let mut body = body_stmts.pop().expect("non-empty after the check above");
+        while let Some(s) = body_stmts.pop() {
+            body = Term::Seq {
+                lhs: Box::new(s),
+                rhs: Box::new(body),
+            };
+        }
+        Ok(Term::Loop {
+            binders,
+            body: Box::new(body),
+        })
+    }
+
+    /// loop-recur iter 1: `(recur ARG*)` — re-enter the enclosing
+    /// loop. Positional args. The tail-position rule is enforced at
+    /// typecheck (iter 2, `recur-not-in-tail-position`); the parser
+    /// accepts the shape unconditionally.
+    fn parse_recur(&mut self) -> Result<Term, ParseError> {
+        self.expect_lparen("recur-term")?;
+        self.expect_keyword("recur")?;
+        let mut args: Vec<Term> = Vec::new();
+        while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
+            args.push(self.parse_term()?);
+        }
+        self.expect_rparen("recur-term")?;
+        Ok(Term::Recur { args })
+    }
+
     // ---- patterns -------------------------------------------------------
 
     fn parse_pattern(&mut self) -> Result<Pattern, ParseError> {
@@ -2583,4 +2676,28 @@ mod tests {
             "diagnostic should mention missing body, got: {msg}"
         );
     }
+
+    #[test]
+    fn parse_loop_and_recur_round_trip_via_term() {
+        let src = "(loop (acc (con Int) 0) (i (con Int) 1) (if (app > i n) acc (recur (app + acc i) (app + i 1))))";
+        let t = parse_term(src).expect("parse loop");
+        match t {
+            ailang_core::ast::Term::Loop { binders, body } => {
+                assert_eq!(binders.len(), 2);
+                assert_eq!(binders[0].name, "acc");
+                assert_eq!(binders[1].name, "i");
+                // body is an `if` whose else-branch is a `recur` of 2 args
+                match *body {
+                    ailang_core::ast::Term::If { else_, .. } => match *else_ {
+                        ailang_core::ast::Term::Recur { args } => {
+                            assert_eq!(args.len(), 2)
+                        }
+                        other => panic!("else not recur: {other:?}"),
+                    },
+                    other => panic!("body not if: {other:?}"),
+                }
+            }
+            other => panic!("not a loop: {other:?}"),
+        }
+    }
 }

crates/ailang-surface/src/print.rs

@@ -594,6 +594,46 @@ fn write_term(out: &mut String, t: &Term, level: usize) {
             write_term(out, value, level);
             out.push(')');
         }
+        Term::Loop { binders, body } => {
+            // loop-recur iter 1: print as
+            //   `(loop (NAME TYPE INIT)* STMT* FINAL_EXPR)`
+            // — inverse of parse_loop's binder read + Seq right-fold,
+            // mirroring the Term::Mut printer.
+            out.push_str("(loop");
+            for b in binders {
+                out.push_str(" (");
+                out.push_str(&b.name);
+                out.push(' ');
+                write_type(out, &b.ty);
+                out.push(' ');
+                write_term(out, &b.init, level);
+                out.push(')');
+            }
+            let mut cursor: &Term = body;
+            loop {
+                match cursor {
+                    Term::Seq { lhs, rhs } => {
+                        out.push(' ');
+                        write_term(out, lhs, level);
+                        cursor = rhs;
+                    }
+                    other => {
+                        out.push(' ');
+                        write_term(out, other, level);
+                        break;
+                    }
+                }
+            }
+            out.push(')');
+        }
+        Term::Recur { args } => {
+            out.push_str("(recur");
+            for a in args {
+                out.push(' ');
+                write_term(out, a, level);
+            }
+            out.push(')');
+        }
     }
 }
 

docs/DESIGN.md

@@ -2420,6 +2420,25 @@ are real surface forms.
 { "t": "assign",
   "name": "<id>",
   "value": Term }
+
+// loop-recur iter 1: strict iteration block. `binders` declares
+// one or more loop parameters (name, type, init), evaluated in
+// order on loop entry; `body` is in scope of all binders. The
+// loop's value is `body`'s value on the iteration that exits via a
+// non-`recur` branch. Strictly additive (no `skip_serializing_if`;
+// pre-existing fixtures hash bit-identically — none carry the tag).
+// No totality claim — an infinite loop is legal. See
+// `docs/specs/2026-05-17-loop-recur.md`.
+{ "t": "loop",
+  "binders": [ { "name": "<id>", "type": Type, "init": Term }, ... ],
+  "body": Term }
+
+// loop-recur iter 1: re-enter the lexically innermost enclosing
+// `loop`, rebinding its binders positionally to `args`. Transfers
+// control (no fall-through); valid only in tail position of its
+// enclosing loop (enforced at typecheck, `recur-not-in-tail-position`).
+{ "t": "recur",
+  "args": [ Term, ... ] }
 ```
 
 In the MVP, `do` is only a direct call to a built-in effect op (no

docs/journals/2026-05-17-iter-loop-recur.1.md

@@ -0,0 +1,180 @@
+# iter loop-recur.1 — Additive AST-Node Foundation (Term::Loop / Term::Recur / LoopBinder)
+
+**Date:** 2026-05-17
+**Started from:** a5eebcd5fd9d703cc4f8a6374f95e00061d86c55
+**Status:** DONE
+**Tasks completed:** 7 of 7
+
+## Summary
+
+`loop` / `recur` become real, parseable, printable, round-trippable,
+hash-stable, strictly-additive AST nodes across all six crates plus
+the drift tests — with NO typecheck semantics and NO real codegen
+lowering (those are loop-recur iters 2 and 3). Added `Term::Loop {
+binders, body }`, `Term::Recur { args }`, and `struct LoopBinder`
+(mirroring `MutVar` exactly); Form-A `(loop (NAME TYPE INIT)* BODY+)`
+/ `(recur ARG*)` parse + print + grammar/notes; prose render /
+count_free_var / subst_var arms; ~30 structural pass-through walker
+arms; the two semantic dispatch points stubbed with
+`CheckError::Internal` (`synth`) / `CodegenError::Internal`
+(`lower_term`) exactly as mut.1 did; DESIGN.md + form_a.md schema
+blocks; drift/coverage/hash anchors; and the spec's worked `sum_to`
+program as a green `examples/loop_sum_to.ail` round-trip fixture.
+`cargo test --workspace` 608 green / 0 red; the iter13a + new
+loop-recur hash pins both green (additivity proven — pre-existing
+canonical-JSON hashes byte-stable); all `tail`-filtered tests green
+(Boss-call-1 operational evidence).
+
+## Per-task notes
+
+- iter loop-recur.1.1: Core AST — `Term::Loop`/`Term::Recur` variants
+  + `struct LoopBinder` + 2 serde round-trip unit tests. RED-first
+  (`error[E0599]`); GREEN after Task 4 (desugar/workspace are *in*
+  ailang-core, so the lib's own exhaustive matches gate it — see
+  Concerns). Both serde tests green.
+- iter loop-recur.1.2: Surface parser (`parse_loop`/`parse_recur` +
+  head dispatch + unknown-head message), printer arms, form_a.md
+  grammar+notes. Binder/body boundary disambiguated via an
+  `is_term_head_kw` discriminator (the plan's flagged "one genuine
+  parser judgement"). `parse_loop_and_recur_round_trip_via_term`
+  green (exactly 2 binders + `if` body + 2-arg recur).
+- iter loop-recur.1.3: Prose projection — `write_term_prec`,
+  `count_free_var`, `subst_var_with_term` Loop/Recur arms (verbatim
+  plan code, lexical-shadow-aware mirroring the Mut arms).
+- iter loop-recur.1.4: ailang-core walkers — 9 desugar.rs sites + 2
+  workspace.rs sites. `cargo build -p ailang-core` GREEN.
+- iter loop-recur.1.5: ailang-check — 14 steps across 7 files
+  including the Boss-call-1 `verify_tail_positions` two mandatory
+  additive arms and the Boss-call-2 `synth` `CheckError::Internal`
+  stub. `cargo build -p ailang-check` GREEN.
+- iter loop-recur.1.6: ailang-codegen + ail/main.rs — `lower_term`
+  `CodegenError::Internal` stub + real structural pass-through at
+  the pure analysis walkers (lambda/escape ×3) + `synth_with_extras`
+  pass-through + main.rs walk_term/rewrite_term. `cargo build
+  --workspace` GREEN.
+- iter loop-recur.1.7: DESIGN.md + form_a.md schema blocks;
+  design_schema_drift + spec_drift + schema_coverage anchors; new
+  loop_recur hash pin; `examples/loop_sum_to.ail` positive fixture.
+  Full suite 608/0; tail-app non-regression green.
+
+## Boss design calls (mirrored from the plan header at iter close)
+
+1. **`verify_tail_positions` "byte-unchanged" = tail-app role
+   unchanged, NOT source frozen.** `verify_tail_positions`
+   (`crates/ailang-check/src/lib.rs`) is an exhaustive no-`_`-wildcard
+   `match`-on-`Term`; the two additive variants *require* two new
+   arms there or `ailang-check` does not compile. The added arms
+   only define how the tail-app walker descends through two
+   brand-new node kinds that no pre-existing fixture contains —
+   zero behaviour change for any pre-existing construct. The
+   acceptance evidence is the tail-app non-regression test (all
+   `tail`-filtered tests green), NOT a frozen-source diff. mut.1 set
+   the exact precedent (it added `Term::Mut`/`Term::Assign` arms
+   inside the same function). Settled; not reopened — the
+   spec-compliance phase did NOT emit `unclear`/BLOCKED on the
+   anticipated "spec says byte-unchanged but the function changed"
+   tension, per the plan header's authority.
+2. **Codegen IS in iter-1 scope as stubs/pass-throughs (mirrors
+   mut.1 site-for-site).** "No codegen in iter 1" means no real
+   loop-header/phi/back-edge lowering (that is iter 3). But
+   `ailang-codegen` carries no-wildcard exhaustive `Term` matches;
+   the workspace would not compile without arms. Resolved exactly
+   as mut.1: `CodegenError::Internal` stub at the `lower_term`
+   dispatch + real structural pass-through at the pure analysis
+   walkers (lambda.rs collect_captures, escape.rs walk/escapes/
+   collect_free_vars) and `synth_with_extras`. No real loop lowering
+   written this iter.
+
+## Concerns
+
+- DONE_WITH_CONCERNS (iter loop-recur.1.1/1.2/1.4): three
+  plan-pseudo-vs-reality substitutions, all of the recurring
+  "specs need concrete code / plan pseudo vs reality" class
+  (`feedback_specs_need_concrete_code`, `feedback_plan_pseudo_vs_reality`),
+  each resolved by preserving the arm/test's evident intent and
+  fixing to the real codebase:
+  1. **Task-1 serde expected-bytes literal.** The plan asserted
+     `"type":{"t":"con","name":"Int","args":[]}`; the real canonical
+     `Type::Con` form is `{"k":"con","name":"Int"}` (discriminator
+     `"k"`, empty `args` omitted — established since mut.2). The
+     test's stated intent (pin one-binder Loop canonical bytes;
+     prove `binders` has no `skip_serializing_if`) is preserved;
+     only the mis-transcribed expected string was corrected. NOT a
+     bug-dodge — `{"k":"con",…}` is the canonical form every Type
+     fixture uses; the plan author mis-recalled the Type JSON.
+  2. **Bare `Int` vs `(con Int)` in binder triples.** The spec's
+     worked example and the plan's Step-1 test source / Step-6
+     fixture write `(loop (acc Int 0) …)` with bare `Int`. The real
+     `parse_type` parses a bare `Int` ident as `Type::Var{"Int"}`
+     (a type *variable*), not the Int constructor — semantically
+     wrong and inconsistent with every `mut` fixture
+     (`(var x (con Int) 0)`), the spec schema, and the Task-1 serde
+     pin. Corrected to `(con Int)` in the parser test source and the
+     `examples/loop_sum_to.ail` fixture. This is the LLM-natural AND
+     correct Form-A type (not a fixture-adapts-to-bug case — every
+     sibling fixture uses `(con Int)`).
+  3. **`ailang_core::ast::LoopBinder` path inside ailang-core.** The
+     plan's literal desugar.rs/workspace.rs arms used the
+     downstream-crate path `ailang_core::ast::LoopBinder`; inside
+     ailang-core itself (`use crate::ast::*;`) the correct path is
+     unqualified `LoopBinder` (consistent with the adjacent bare
+     `MutVar` usage). `subst_call_with_extras`'s plan arm also used
+     `(target, extras)`; the real signature is `(name, lifted,
+     extras)` — mirrored from the local Mut arm per the plan's own
+     instruction. ailang-check (downstream) correctly keeps the
+     `ailang_core::ast::LoopBinder` path.
+
+## Boss addendum (post-orchestrator, at commit)
+
+Concern 2 surfaced that the bare-`Int`-in-binder imprecision is not
+just in the plan/test but in the **committed specs themselves**:
+`docs/specs/2026-05-17-loop-recur.md`'s headline clause-1 worked
+example + the must-fail `bad_recur` fixture, and
+`docs/specs/2026-05-17-llm-surface-discipline.md` §5's illustrative
+anchor, all wrote `(loop (acc Int 0) (i Int 1) …)`. Bare `Int`
+parses as `Type::Var{"Int"}`, so the spec's *headline evidence* —
+the program an LLM author would copy verbatim — does not parse to
+the typed loop it claims. Same doc-honesty class as the mono.rs
+header / effect-doc-honesty: a spec must show code that actually
+parses to what it asserts. Boss forward-fixed all three snippets to
+`(con Int)` (the established convention every `mut` fixture + the
+spec's own schema use); folded into this iter's commit. No design,
+semantics, schema, or load-bearing assumption changed — a
+surface-syntax precision fix, so no re-brainstorm / re-grounding.
+
+## Known debt
+
+- No additional E2E fixture written (Phase 3). iter-1 ships NO
+  typecheck and NO codegen by design; an `ail run` e2e would only
+  exercise the deliberately-temporary `synth`/`lower_term`
+  `Internal` stubs (a negative-value test asserting a transient
+  error). The milestone invariant worth protecting at iter-1 —
+  additivity (hash pins), round-trip (the new fixture), drift trio,
+  tail-app non-regression — is fully covered by tests added in
+  Tasks 1/2/7. The spec's positive sum_to-runs-to-a-value E2E is
+  explicitly iter-3 scope.
+
+## Files touched
+
+- AST + core walkers: `crates/ailang-core/src/ast.rs`,
+  `desugar.rs`, `workspace.rs`
+- Surface: `crates/ailang-surface/src/parse.rs`, `print.rs`;
+  `crates/ailang-core/specs/form_a.md`
+- Prose: `crates/ailang-prose/src/lib.rs`
+- Check: `crates/ailang-check/src/{lib,lift,mono,linearity,
+  uniqueness,reuse_shape,pre_desugar_validation}.rs`
+- Codegen + CLI: `crates/ailang-codegen/src/{lambda,escape,lib}.rs`,
+  `crates/ail/src/main.rs`
+- Docs/drift/coverage/hash: `docs/DESIGN.md`,
+  `crates/ailang-core/tests/{design_schema_drift,spec_drift,
+  schema_coverage,hash_pin}.rs`,
+  `crates/ail/tests/codegen_import_map_fallback_pin.rs`
+  (recon-undercount: an integration-test exhaustive `Term` match
+  not in the plan's site inventory; same additive-arm class,
+  mirrors the Mut defensive-recursion shape — Boss-call-2-class
+  "recon under-scoped it")
+- New fixture: `examples/loop_sum_to.ail`
+
+## Stats
+
+bench/orchestrator-stats/2026-05-17-iter-loop-recur.1.json

docs/journals/INDEX.md

@@ -81,3 +81,4 @@
 - 2026-05-16 — iter revert: Iteration-discipline milestone (it.1 `96db54d` + it.2 `a4be1e5`) fully backed out by one **forward** iteration (`main` sacrosanct — never rewound; `1ff7e81`, the pre-`9973546` commit, is the per-region byte oracle). Root cause: the milestone was an over-escalation of fieldtest finding F1 (a `[friction]` item whose own minimal recommendation was a DESIGN.md note); its totality dichotomy made the maximally-LLM-natural `build(d:Int)=Node(1,build(d-1),build(d-1))` inexpressible (it.3 BLOCKED), and the only in-thesis escape (A1/it.2b) conceded the language's first documented-unenforced totality precondition — a purity-pillar dilution the user rejected. `Term::Loop`/`Term::Recur`/`LoopBinder`, the `verify_structural_recursion` guardedness pass + `term_contains_loop` + `Diverge`-injection + the transitively-it.2 `module_fns` plumbing, the five `Recur*`/`NonStructuralRecursion` `CheckError` variants (+ `code()` + 3 dedicated `ctx()` arms), the it.1 codegen loop-header/phi/back-edge + parallel `block_terminated` setter, and all walker arms are removed — `crates/ailang-check/src/lib.rs` and every reverted source/test file byte-identical to `1ff7e81`. Surgical keeps: feature-acceptance **clause 3** (DESIGN.md + brainstorm SKILL.md, worked example de-claimed "shipped"→hypothetical) and the F3 P2 todo. Sole net addition: an honest F1/F4 documented-idiom note (tail-recursive accumulator fallback; `examples/mut_counter.ail`) guarded by a doc-presence test. 16 it.1/it.2 fixtures + 2 pin files + `bench/it3-oracle/` deleted; 2 RC fixtures restored to `1ff7e81`; `bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json` kept (historical record). Roadmap: Iteration-discipline block + blocking-fork section removed; the genuine total-Int-recursion ambition preserved as a deferred P2 milestone sequenced behind a future `Nat`/refinement-types milestone (not abandoned — correctly sequenced). Correctness gate PRISTINE: 164 surviving `1ff7e81`-era fixtures `ail check`/`ail run` byte-identical to pre-milestone behaviour (1ff7e81 worktree reference compiler, zero drift); `cargo test --workspace` 600/0; zero residual it.1/it.2 production surface. The old it.* journals/plans + the superseded-headered `2026-05-15-iteration-discipline.md` stay as historical record → 2026-05-16-iter-revert.md
 - 2026-05-16 — audit iteration-discipline-revert (milestone close, clean): architect confirmed the revert byte-pristine (18 src + 5 test files byte-identical to `1ff7e81`, zero residual it.1/it.2 production surface, DESIGN.md coherent, roadmap/spec hygiene correct); one `[medium]` drift — a dangling `loop`/`recur` cross-reference into the reverted milestone inside the *live* Stateful-islands roadmap scope bullet — fixed inline (Boss doc-hygiene; reworded to keep the real "no `while`; repetition stays recursion" scope guard, drop the reverted-milestone reference). Bench: `compile_check.py`/`cross_lang.py` exit 0; `check.py` exit 1 on the single metric `bench_list_sum.bump_s` +12.71%. Bencher localisation: HEAD and `1ff7e81` bump binaries `cmp`-identical, interleaved 3×60-run measurement shows head−oracle delta ~0 (±1.5% stdev) with *both* ~+11% over the 2026-05-09 baseline → environmental/hardware drift, NOT a revert regression (third independent proof codegen == `1ff7e81`). Resolution: carry-on, baseline NOT ratified (Iron Law — nothing intentionally moved the metric; byte-identical codegen must not move the baseline; the spec's PRISTINE mandate is satisfied because pristine = "no regression introduced", proven). Pre-existing `*.bump_s` baseline-vs-hardware staleness (the `1ff7e81` oracle trips the same +11%) filed forward as a separate P2 `[todo]` (bench-harness recalibration, no language change), not mis-attributed to the revert. Fieldtest skipped (revert restores the already-field-tested pre-`9973546` surface; Task-11 164-fixture byte-equivalence is the stronger proof). Milestone closed clean → 2026-05-16-audit-iteration-discipline-revert.md
 - 2026-05-16 — iter effect-doc-honesty: standalone documentation-honesty tidy (split out from the retired effect-op-arg-modes bundle — user rejected bundling a real DESIGN.md fix with speculative build-ahead infra). Corrected three false effect-system claims the recon surfaced: DESIGN.md Decision 3 "row-polymorphic (`![IO | r]`)" (no `EffectRow`/row var exists — effect sets are flat closed sets unified by set-equality) + "`IO` and `Diverge` … are wired up" (`Diverge` is 100% vapour: zero code in any crate) → reconciled to IO-only/Diverge-reserved-unimplemented (modelled on Decision 4's reserved-refinements precedent); DESIGN.md §"What is not supported" "IO and Diverge ops" bullet; `ast.rs` `Term::Do` doc-comment "resolved against the effect-handler table at link time" → the real mechanism (typecheck `Env::effect_ops` lookup + `lower_effect_op` literal codegen match, no handler table). Satellite lockstep: `form_a.md:226` + rule-3, `main.rs:289` merge-prose CONTRACT example. Guarded by a new 4-test doc-presence pin `crates/ailang-core/tests/effect_doc_honesty_pin.rs` (fiction-absent + corrected-anchor-present, single-line substrings — wrap-robust). No language/checker/codegen change; `ail check`/`run` byte-unchanged by construction. `cargo test --workspace` 600 → 604; drift/coverage trio (`design_schema_drift`/`spec_drift`/`schema_coverage`) green, empirically confirming none scans the effect-prose region. One concern: the plan's Task-2 replacement body soft-wrapped a phrase the single-line pin asserts; orchestrator resolved correctly (exact wording + exact pin preserved, wrap column moved) — recurring-class planner gap, fixed forward by a Step-5 self-review tightening → 2026-05-16-iter-effect-doc-honesty.md
+- 2026-05-17 — iter loop-recur.1: standalone-`loop`/`recur` milestone (1 of 3) — the strictly-additive AST-node foundation. `Term::Loop { binders: Vec<LoopBinder>, body }` / `Term::Recur { args }` / `struct LoopBinder` (mirrors `MutVar`'s `(name,type,init)` triple; `binders` no `skip_serializing_if`) added end-to-end across all six crates' no-`_`-wildcard exhaustive `Term` matches (~30 sites incl. one recon-undercount integration-test pin): Form-A `parse_loop`/`parse_recur` (binder/body boundary disambiguated by an `is_term_head_kw` guard — the plan's flagged sole parser judgement) + print + `form_a.md` grammar/notes + prose render/free-var/subst lockstep + canonical-JSON serde/round-trip + DESIGN.md §Data-model `"t":"loop"`/`"t":"recur"` blocks + design_schema_drift/spec_drift/schema_coverage anchors + a new `loop_recur` hash pin (additivity proven: iter13a + new pin both green, pre-existing canonical-JSON bytes byte-stable) + `examples/loop_sum_to.ail` round-trip fixture. NO typecheck semantics + NO real codegen by design: the two semantic dispatch points stubbed `synth`→`CheckError::Internal` / `lower_term`→`CodegenError::Internal` exactly as mut.1; pure analysis walkers (escape/lambda/`synth_with_extras`) get real structural pass-through. Two binding Boss design calls (mirrored into the journal): (1) `verify_tail_positions` "byte-unchanged" = tail-app *role* unchanged not source-frozen — it is an exhaustive no-wildcard match so two additive descent-only arms are mandatory; acceptance evidence is the tail-app non-regression test (all `tail`-filtered tests byte-identical), mut.1 set the precedent; (2) codegen IS iter-1 scope as stubs/pass-throughs (no real loop-header/phi/back-edge — that is iter 3). Three plan-pseudo-vs-reality substitutions, all intent-preserving, recurring `feedback_specs_need_concrete_code`/`feedback_plan_pseudo_vs_reality` class: serde `Type::Con` literal `{"t":"con",…,"args":[]}`→real `{"k":"con","name":"Int"}`; bare `Int`→`(con Int)` in binder triples (bare `Int` parses as `Type::Var`); `ailang_core::ast::LoopBinder`→unqualified inside ailang-core. Boss forward-fix folded in: Concern 2 surfaced that the committed specs themselves (`2026-05-17-loop-recur.md` headline + `bad_recur`, `2026-05-17-llm-surface-discipline.md` §5) wrote bare `Int` — corrected all three snippets to `(con Int)` (doc-honesty, same class as the mono.rs header; no design/schema/assumption change, no re-brainstorm). `cargo test --workspace` 600→608 / 0 red (Boss-reran independently). Component 4 (typecheck) = iter 2; Component 5 (codegen) + positive/deep-`n` E2E = iter 3 → 2026-05-17-iter-loop-recur.1.md

docs/specs/2026-05-17-llm-surface-discipline.md

@@ -138,7 +138,7 @@ sugar; loop state is rebound parameters, not mutation):
   (type (fn-type (params (con Int)) (ret (con Int))))
   (params n)
   (body
-    (loop (acc Int 0) (i Int 1)
+    (loop (acc (con Int) 0) (i (con Int) 1)
       (if (app > i n)
           acc
           (recur (app + acc i) (app + i 1))))))

docs/specs/2026-05-17-loop-recur.md

@@ -106,7 +106,7 @@ What an LLM author writes for "sum 1..n" **with** `loop`/`recur`:
   (type (fn-type (params (con Int)) (ret (con Int))))
   (params n)
   (body
-    (loop (acc Int 0) (i Int 1)
+    (loop (acc (con Int) 0) (i (con Int) 1)
       (if (app > i n)
           acc
           (recur (app + acc i) (app + i 1))))))
@@ -143,7 +143,7 @@ is rejection)
   (type (fn-type (params (con Int)) (ret (con Int))))
   (params n)
   (body
-    (loop (i Int 0)
+    (loop (i (con Int) 0)
       (app + 1 (recur (app + i 1))))))   ; recur is an argument to +,
                                           ; NOT tail → RecurNotInTailPosition
 ```

examples/loop_sum_to.ail

@@ -0,0 +1,9 @@
+(module loop_sum_to
+  (fn sum_to
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params n)
+    (body
+      (loop (acc (con Int) 0) (i (con Int) 1)
+        (if (app > i n)
+            acc
+            (recur (app + acc i) (app + i 1)))))))