AILang/docs/plans/0076-loop-recur.1.md

# loop-recur.1 — Additive AST-Node Foundation — Implementation Plan

> **Parent spec:** `docs/specs/0034-loop-recur.md`
>
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
> to run this plan. Steps use `- [ ]` checkboxes for tracking.

**Goal:** `loop` / `recur` become real, parseable, printable,
round-trippable, hash-stable, strictly-additive AST nodes; the whole
workspace compiles and `cargo test --workspace` is green — with NO
typecheck semantics and NO real codegen lowering yet.

**Architecture:** Three additive items in `ailang-core::ast` —
`Term::Loop { binders: Vec<LoopBinder>, body: Box<Term> }`,
`Term::Recur { args: Vec<Term> }`, `struct LoopBinder { name, ty,
init }` (the triple mirrors `MutVar` exactly). Every exhaustive
`match`-on-`Term` in the workspace has NO `_` wildcard, so the two
new variants force an arm at ~30 sites across all six crates plus the
drift tests. Sites split into four classes: (a) structural
pass-through arms (mirror the existing `Term::Mut`/`Term::Assign`
arm shape, substituting `binders`/`init`/`body` and `args`); (b)
head-name helpers (`"loop"` / `"recur"` string); (c) the two
*semantic* dispatch points — typecheck `synth` and codegen
`lower_term` — which get `CheckError::Internal` / `CodegenError::Internal`
**stubs** in this iter exactly as mut.1 did (real semantics land in
iter 2 / iter 3); (d) schema-drift / hash anchors.

**Tech Stack:** `ailang-core` (ast, desugar, workspace, specs/form_a.md,
drift+hash tests), `ailang-surface` (parse, print), `ailang-check`
(lib, lift, mono, linearity, uniqueness, reuse_shape,
pre_desugar_validation), `ailang-codegen` (lib, lambda, escape),
`ailang-prose` (lib), `ail` (main), `docs/DESIGN.md`.

---

## Boss design calls baked into this plan (do not re-litigate at execution time)

1. **`verify_tail_positions` "byte-unchanged" reading (spec Open
   Q1).** The spec's "`verify_tail_positions` … byte-unchanged"
   means its **tail-app verification role/behaviour** is unchanged,
   NOT that the function's source text is frozen — the function is
   an exhaustive `match`-on-`Term` with no `_` wildcard
   (`crates/ailang-check/src/lib.rs:2672` is the existing
   `Term::Mut` arm inside it), so the additive variant *requires*
   two new arms there or `ailang-check` does not compile. The arms
   added here (Task 5, Step 6) only define how the tail-app walker
   *descends through two brand-new node kinds that no pre-existing
   fixture contains*; they introduce zero behaviour change for any
   pre-existing construct. The spec's own §"Testing strategy"
   already operationalises "byte-unchanged" as
   "`tail-app` non-regression — existing tail-app IR-snapshot and
   e2e fixtures byte-identical" — that test (Task 7, Step 7) is the
   acceptance evidence, not a frozen-source diff. mut.1 set the
   exact precedent (it added `Term::Mut`/`Term::Assign` arms inside
   the same function). This is settled; the executor does not
   reopen it.

2. **Codegen is in iter-1 scope as stubs/pass-throughs (recon
   under-scoped it).** The brainstorm carrier said "no codegen in
   iter 1", meaning *no real loop-header/phi/back-edge lowering*
   (correct — that is iter 3). But `ailang-codegen` also carries
   no-wildcard exhaustive `Term` matches (`lambda.rs:478`,
   `escape.rs:197/389/506`, `lib.rs:1762`, `lib.rs:3094`); the
   workspace will not compile — so `cargo test --workspace` (the
   iter-1 goal) cannot be green — without arms there. mut.1
   resolved exactly this by adding **`CodegenError::Internal`
   stub** at the `lower_term` dispatch and **real structural
   pass-through** at the pure analysis walkers + `synth_with_extras`.
   Task 6 mirrors mut.1 site-for-site. No real loop lowering is
   written in this iter.

3. **`binders` has no `skip_serializing_if`.** Mirrors `Term::Mut.vars`
   exactly (the field is part of the shape; empty stays `[]` in
   canonical JSON). `recur`'s `args` likewise plain `Vec<Term>`.
   Whether ≥1 binder is *required* is a typecheck question deferred
   to iter 2; the parser here accepts zero-or-more binders (mirrors
   `parse_mut`).

---

## Files this plan creates or modifies

- Modify: `crates/ailang-core/src/ast.rs:543` — add `Term::Loop` /
  `Term::Recur` variants; `:584` — add `struct LoopBinder`; `:952`
  — two serde round-trip unit tests.
- Modify: `crates/ailang-surface/src/parse.rs:1198` head dispatch +
  unknown-head message; new `parse_loop` / `parse_recur` after
  `parse_assign` (`:1643`); `:2551` parse unit tests.
- Modify: `crates/ailang-surface/src/print.rs:596` — `Term::Loop` /
  `Term::Recur` print arms.
- Modify: `crates/ailang-core/specs/form_a.md:288` — grammar lines;
  `:326` — notes paragraph.
- Modify: `crates/ailang-prose/src/lib.rs:937` (write_term_prec),
  `:1135` (count_free_var), `:1287` (subst_var_with_term).
- Modify: `crates/ailang-core/src/desugar.rs` — 9 arm sites; 
  `crates/ailang-core/src/workspace.rs` — 2 arm sites.
- Modify: `crates/ailang-check/src/lib.rs` — substitute_rigids_in_term
  (`:263`), verify_tail_positions (`:2681`), head-name helper
  (`:3594`), synth STUB (`:3645`); `lift.rs` ×2; `mono.rs` ×2;
  `linearity.rs` ×3; `uniqueness.rs` ×1; `reuse_shape.rs` ×1;
  `pre_desugar_validation.rs` ×1.
- Modify: `crates/ailang-codegen/src/lambda.rs` ×1; `escape.rs` ×3;
  `lib.rs` — lower_term STUB (`:1762`-region) + synth_with_extras
  (`:3095`).
- Modify: `crates/ail/src/main.rs` — `:1534` (walk_term) + `:2754`
  (rewrite_term) arm sites.
- Modify: `docs/DESIGN.md:2422` — `"t":"loop"` / `"t":"recur"`
  schema blocks.
- Modify: `crates/ailang-core/tests/design_schema_drift.rs:153` +
  `:174`; `spec_drift.rs:130` + `:153`; `schema_coverage.rs:51`,
  `:98`, `:246`; `hash_pin.rs` — new pin test.
- Create: `examples/loop_sum_to.ail` — the spec's worked `sum_to`
  program (round-trip auto-covered by `round_trip.rs`).
- No edit: `crates/ailang-surface/tests/round_trip.rs` (auto-discovers
  `examples/*.ail`); `crates/ailang-core/tests/carve_out_inventory.rs`
  (iter-1 adds no `.ail.json` negative fixtures — those are iter 2).

---

## Task 1: Core AST nodes + serde + round-trip unit tests

**Files:**
- Modify: `crates/ailang-core/src/ast.rs`

- [ ] **Step 1: Write the two failing round-trip unit tests**

In `crates/ailang-core/src/ast.rs`, inside `#[cfg(test)] mod tests`
(after `term_assign_round_trips_through_json`, before the closing
`}` at line 952), add:

```rust
    /// 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":{"t":"con","name":"Int","args":[]},"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:?}"),
        }
    }
```

- [ ] **Step 2: Run tests to verify they fail to compile**

Run: `cargo test -p ailang-core --lib term_loop_one_binder term_recur_round_trips 2>&1 | tail -5`
Expected: FAIL — `error[E0599]: no variant ... Loop` / `Recur` /
`cannot find struct ... LoopBinder` (the variants do not exist yet).

- [ ] **Step 3: Add `Term::Loop` and `Term::Recur` variants**

In `crates/ailang-core/src/ast.rs`, immediately after the
`Term::Assign { name: String, value: Box<Term> }` variant (ends
line 542), before the enum's closing `}` (line 543), add:

```rust
    /// 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/0034-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>,
    },
```

- [ ] **Step 4: Add `struct LoopBinder`**

In `crates/ailang-core/src/ast.rs`, immediately after the
`struct MutVar { ... }` definition (ends line 584), add:

```rust
/// 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,
}
```

- [ ] **Step 5: Run tests to verify they pass**

Run: `cargo test -p ailang-core --lib term_loop_one_binder term_recur_round_trips 2>&1 | tail -5`
Expected: PASS — `test result: ok. 2 passed`.

(`ailang-core` itself now compiles; downstream crates still fail
exhaustiveness — fixed in Tasks 2-7. Do not run `--workspace` yet.)

---

## Task 2: Surface parser + printer + grammar + parse unit tests

**Files:**
- Modify: `crates/ailang-surface/src/parse.rs`
- Modify: `crates/ailang-surface/src/print.rs`
- Modify: `crates/ailang-core/specs/form_a.md`

- [ ] **Step 1: Write the failing parser unit test**

In `crates/ailang-surface/src/parse.rs`, in the unit-tests module
near the existing mut-family parse tests (after line 2551), add:

```rust
    #[test]
    fn parse_loop_and_recur_round_trip_via_term() {
        let src = "(loop (acc Int 0) (i Int 1) (if (app > i n) acc (recur (app + acc i) (app + i 1))))";
        let mut p = Parser::new(lex(src).expect("lex"));
        let t = p.parse_term().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:?}"),
        }
    }
```

(If `Parser::new` / `lex` are not the exact local test helpers,
mirror the helper used by the adjacent `parse_mut` test verbatim —
do not invent a new harness.)

- [ ] **Step 2: Run test to verify it fails**

Run: `cargo test -p ailang-surface --lib parse_loop_and_recur 2>&1 | tail -5`
Expected: FAIL — unknown term head `loop` (parser has no arm yet).

- [ ] **Step 3: Add head-dispatch arms + extend unknown-head message**

In `crates/ailang-surface/src/parse.rs`, in the `match head { ... }`
at line 1198: add two arms immediately after the
`"assign" => self.parse_assign(),` line (1214):

```rust
                    "loop" => self.parse_loop(),
                    "recur" => self.parse_recur(),
```

In the same `match`'s `other =>` error message (the `format!`
string spanning lines 1219-1224), change the trailing
`` `assign`, `lit-unit` `` to:

```rust
                                `assign`, `loop`, `recur`, `lit-unit`"
```

(The whole message string must read `… `mut`, `assign`, `loop`,
`recur`, `lit-unit`"` contiguously on its closing line — the
`spec_drift.rs` / unknown-head expectations key on substrings.)

- [ ] **Step 4: Add `parse_loop` and `parse_recur`**

In `crates/ailang-surface/src/parse.rs`, immediately after
`fn parse_assign` (ends line 1643), add:

```rust
    /// 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 — same triple as
    /// `(var ...)`'s tail), then ≥ 1 trailing terms right-folded
    /// into `Term::Seq` (mirrors `parse_mut`).
    fn parse_loop(&mut self) -> Result<Term, ParseError> {
        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(), Some(Token { tok: Tok::LParen, .. })) {
            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 })
    }
```

(The binder loop reads a bare `(NAME TYPE INIT)` — note: unlike
`parse_mut`'s `(var NAME TYPE INIT)`, the spec's surface is
`(loop (NAME TYPE INIT) … BODY)` with no `var` keyword inside the
binder. Confirm against the spec's worked example
`(loop (acc Int 0) (i Int 1) …)` — there is no `var`. The
`while matches! LParen` loop terminates when the next form is a
non-parenthesised term or the closing `)`; a parenthesised *body*
form like `(if …)` is correctly NOT consumed as a binder because a
binder's first inner token is an ident NAME, whereas `(if …)`'s is
a keyword — but the loop as written would mis-consume `(if …)` as a
binder. Guard the binder loop with: only treat a leading `(` as a
binder when its head is NOT a known term-head keyword. Implement the
guard as: `while self.peek_is_lparen() && !self.peek_inner_is_term_head()`
using the existing `peek_head_ident` helper —
`while matches!(self.peek_lparen_inner_head(), Some(h) if !is_term_head(h))`.
If no such helper exists, the robust shape mirrored from the spec is
to require the binder list to be syntactically distinct; the
**executor must verify** the spec's worked example parses to exactly
2 binders + an `if` body via the Step-1 test and adjust the binder
terminator predicate until it does. This is the one genuine parser
judgement in the task; the Step-1 test is the oracle.)

- [ ] **Step 5: Add printer arms**

In `crates/ailang-surface/src/print.rs`, in `fn write_term`'s
`match t { ... }`, immediately after the `Term::Assign { name,
value } => { ... }` arm (ends line 596), before the match's closing
`}` (line 597), add:

```rust
        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(')');
        }
```

- [ ] **Step 6: Add grammar lines + notes to `form_a.md`**

In `crates/ailang-core/specs/form_a.md`, in the parenthesised-forms
code block, immediately after the `(assign NAME VALUE-TERM)` line
(288), add:

```
(loop (NAME TYPE INIT)* BODY-TERM+)     ; strict iteration block (loop-recur)
(recur ARG*)                            ; re-enter enclosing loop (loop-recur)
```

In the `Notes:` list, immediately after the `(assign …)` note
paragraph (ends line 326), add:

```
- `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/0034-loop-recur.md`.
```

- [ ] **Step 7: Run the parser test + surface build**

Run: `cargo test -p ailang-surface --lib parse_loop_and_recur 2>&1 | tail -5`
Expected: PASS. (Other crates still fail exhaustiveness; continue.)

---

## Task 3: Prose projection arms

**Files:**
- Modify: `crates/ailang-prose/src/lib.rs`

- [ ] **Step 1: Add `write_term_prec` arms**

In `crates/ailang-prose/src/lib.rs`, in `fn write_term_prec`'s
`match t`, immediately after the `Term::Assign { name, value } =>
{ ... }` arm (ends line 937), before the match's closing `}`
(line 938), add:

```rust
        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(')');
        }
```

- [ ] **Step 2: Add `count_free_var` arms**

In `crates/ailang-prose/src/lib.rs`, in `fn count_free_var`'s
`match`, immediately after the `Term::Assign { name: assign_name,
value } => { ... }` arm (ends line 1135), before the match closing
`}` (line 1136), add:

```rust
        // 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()
        }
```

- [ ] **Step 3: Add `subst_var_with_term` arms**

In `crates/ailang-prose/src/lib.rs`, in `fn subst_var_with_term`'s
`match t`, immediately after the `Term::Assign { name: assign_name,
value } => Term::Assign { ... }` arm (ends line 1287), before the
match closing `}` (line 1288), add:

```rust
        // 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(),
        },
```

- [ ] **Step 4: Build prose crate**

Run: `cargo build -p ailang-prose 2>&1 | tail -3`
Expected: prose-crate-local exhaustiveness satisfied (it may still
fail building due to its dep on `ailang-check`; that is expected
until Task 5 — the acceptance gate for this task is that
`prose/src/lib.rs` has no `non-exhaustive patterns` error; grep the
output for `prose/src/lib.rs` — there must be none).

---

## Task 4: ailang-core walker arms (desugar + workspace)

**Files:**
- Modify: `crates/ailang-core/src/desugar.rs`
- Modify: `crates/ailang-core/src/workspace.rs`

Each step below adds two arms immediately after the existing
`Term::Assign` arm at the cited line. The arm shape mirrors the
adjacent `Term::Mut` arm at that site (substitute
`binders`/`b.init`/`body` for `vars`/`v.init`/`body`, and `args`
for the Recur form). The literal arm is given per site.

- [ ] **Step 1: `desugar.rs` `collect_used_in_term` (after `:360`)**

`collect_used_in_term` is a free fn (`fn collect_used_in_term(t:
&Term, used: &mut BTreeSet<String>)` at `:283`), not a method.
After the `Term::Assign { name, value } => { ... }` arm following
`Term::Mut` at `:349` (the Assign arm starts `:360`), add:

```rust
        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);
            }
        }
```

- [ ] **Step 2: `desugar.rs` `desugar_term` (after `:588`)**

The `Term::Mut` arm at `:559-588` extends scope per-var via
`inner.insert(v.name.clone(), ScopeEntry::LetBound)` (a
`BTreeMap`-style `scope` clone, `scope` is the second param of
`desugar_term`). After the `Term::Assign { name, value } =>
Term::Assign { ... }` arm following it (Assign starts `:589`), add:

```rust
            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<ailang_core::ast::LoopBinder> = binders
                    .iter()
                    .map(|b| {
                        let init = self.desugar_term(&b.init, &inner);
                        inner.insert(b.name.clone(), ScopeEntry::LetBound);
                        ailang_core::ast::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(),
            },
```

- [ ] **Step 3: `desugar.rs` `free_vars_in_term` (after `:1228`)**

`free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut
BTreeSet<String>)` (`:1138`). The `Term::Mut` arm at `:1214-1227`
clones `bound` into a local `b`, walks each init under the growing
`b`, inserts each var name into `b`, then walks the body under `b`.
After the `Term::Assign` arm following it (Assign starts `:1228`),
add:

```rust
        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);
            }
        }
```

- [ ] **Step 4: `desugar.rs` `subst_var` (after `:1416`)**

`pub fn subst_var(t: &Term, from: &str, to: &str) -> Term`
(`:1272`). The `Term::Mut` arm at `:1381-1414` is shadow-aware
(stop substituting once a var named `from` is declared). After the
`Term::Assign { name, value } => Term::Assign { ... }` arm
following it (Assign starts `:1416`), add:

```rust
        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<ailang_core::ast::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;
                    }
                    ailang_core::ast::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(),
        },
```

- [ ] **Step 5: `desugar.rs` `subst_call_with_extras` (after `:1567`)**

After the `Term::Assign` arm following the `Term::Mut` rebuild at
`:1551`, add:

```rust
        Term::Loop { binders, body } => Term::Loop {
            binders: binders
                .iter()
                .map(|b| ailang_core::ast::LoopBinder {
                    name: b.name.clone(),
                    ty: b.ty.clone(),
                    init: subst_call_with_extras(&b.init, target, extras),
                })
                .collect(),
            body: Box::new(subst_call_with_extras(body, target, extras)),
        },
        Term::Recur { args } => Term::Recur {
            args: args
                .iter()
                .map(|a| subst_call_with_extras(a, target, extras))
                .collect(),
        },
```

(Match `subst_call_with_extras`'s real param names from its
signature — mirror the local `Term::Mut` arm at `:1551`.)

- [ ] **Step 6: `desugar.rs` `find_non_callee_use` (after `:1636`)**

After the `Term::Assign` arm following `Term::Mut` at `:1629`, add:

```rust
        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))
        }
```

- [ ] **Step 7: `desugar.rs` `any_nested_ctor` (after `:1689`)**

After the `Term::Assign` arm following `Term::Mut` at `:1686`, add:

```rust
            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),
```

- [ ] **Step 8: `desugar.rs` `any_let_rec` (after `:1719`)**

After the `Term::Assign` arm following `Term::Mut` at `:1716`, add:

```rust
            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),
```

- [ ] **Step 9: `desugar.rs` `any_lit_pattern` (after `:2840`)**

After the `Term::Assign` arm following `Term::Mut` at `:2837`, add:

```rust
            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),
```

- [ ] **Step 10: `workspace.rs` `walk_term_embedded_types` (after `:1260`)**

After the `Term::Assign` arm following `Term::Mut` at `:1254`, add:

```rust
        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(())
        }
```

- [ ] **Step 11: `workspace.rs` `walk_term` (after `:1394`)**

After the `Term::Assign { value, .. } => walk_term(value, f)` arm
following `Term::Mut` at `:1388`, add:

```rust
        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(())
        }
```

- [ ] **Step 12: Build ailang-core**

Run: `cargo build -p ailang-core 2>&1 | tail -3`
Expected: PASS — `ailang-core` compiles (all its exhaustive
`Term` matches now have arms).

---

## Task 5: ailang-check walker arms + verify_tail_positions pass-through + synth STUB

**Files:**
- Modify: `crates/ailang-check/src/lib.rs`
- Modify: `crates/ailang-check/src/lift.rs`
- Modify: `crates/ailang-check/src/mono.rs`
- Modify: `crates/ailang-check/src/linearity.rs`
- Modify: `crates/ailang-check/src/uniqueness.rs`
- Modify: `crates/ailang-check/src/reuse_shape.rs`
- Modify: `crates/ailang-check/src/pre_desugar_validation.rs`

- [ ] **Step 1: `lib.rs` `substitute_rigids_in_term` (after `:263`)**

After the `Term::Assign { name, value } => Term::Assign { ... }`
arm following `Term::Mut` at `:249`, add:

```rust
        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(),
        },
```

- [ ] **Step 2: `lift.rs` `lift_in_term` (after the `Term::Mut` rebuild at `:383`)**

The `Term::Mut` arm at `:383-395` is a method that threads
`self.lift_in_term(&v.init, locals, in_def)?`. After the
`Term::Assign { name, value } => Ok(Term::Assign { ... })` arm
following it (Assign at `:396-399`), add:

```rust
            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<_>>>()?,
            }),
```

- [ ] **Step 3: `lift.rs` `term_has_letrec` (after `:763`)**

After `Term::Assign { value, .. } => term_has_letrec(value)`
(`:763`) following `Term::Mut` at `:760`, add:

```rust
            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),
```

- [ ] **Step 4: `mono.rs` `rewrite_mono_calls` (after `:1243`)**

After the `Term::Assign` arm following `Term::Mut` at `:1237`
(in-place `&mut` walk), add (mirror the Mut arm's full call list
verbatim from `:1237-1242`):

```rust
        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);
            }
        }
```

- [ ] **Step 5: `mono.rs` `interleave_slots` (after `:1617`)**

After the `Term::Assign` arm following `Term::Mut` at `:1611`, add
(mirror the Mut arm's full call list from `:1611-1616`):

```rust
        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);
            }
        }
```

- [ ] **Step 6: `lib.rs` `verify_tail_positions` (after `:2681`) — the Boss-call-1 site**

After `Term::Assign { value, .. } => verify_tail_positions(value,
false)` (`:2681`) following `Term::Mut` at `:2672`, before the
match closing `}` (`:2682`), add:

```rust
        // 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(())
        }
```

- [ ] **Step 7: `lib.rs` head-name helper (after `:3594`)**

In the `match` whose arms map a `Term` to its tag string (the
`Term::Mut { .. } => "mut"` / `Term::Assign { .. } => "assign"`
arms at `:3593-3594`, ending with `Term::Ctor { .. } | Term::Lam
{ .. } => unreachable!()`), add immediately after the
`Term::Assign { .. } => "assign",` line (`:3594`):

```rust
                        Term::Loop { .. } => "loop",
                        Term::Recur { .. } => "recur",
```

- [ ] **Step 8: `lib.rs` `synth` STUB (after `:3645`) — Boss-call-2 site**

In `pub(crate) fn synth` (`:2719`), after the `Term::Assign { name,
value } => { ... }` arm following the `Term::Mut` arm at `:3614`
(the Assign arm ends around `:3680`; locate the arm immediately
before `synth`'s match closing brace), add:

```rust
        // 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(),
        )),
```

(`CheckError::Internal(String)` is defined at `lib.rs:687`
`#[error("internal: {0}")]`. `synth` returns `Result<Type>` over
`CheckError` — `Err(CheckError::Internal(...))` is the correct
stub return.)

- [ ] **Step 9: `linearity.rs` `walk` (after `:607`)**

After the `Term::Assign { value, .. } => { ... }` arm following
`Term::Mut` at `:601`, add (mirror the Mut arm's `self.walk(...,
Position::...)` calls verbatim from `:601-606`):

```rust
            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);
                }
            }
```

- [ ] **Step 10: `linearity.rs` head-name helper (after `:797`)**

After `Term::Assign { .. } => "assign",` (`:797`) following
`Term::Mut { .. } => "mut"` (`:796`), add:

```rust
        Term::Loop { .. } => "loop",
        Term::Recur { .. } => "recur",
```

- [ ] **Step 11: `linearity.rs` `any_sub_binder_consumed_for` (after `:935`)**

After the `Term::Assign` arm following `Term::Mut` at `:929`, add
(mirror the Mut arm's full call signature from `:929-933`):

```rust
        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)
        }),
```

- [ ] **Step 12: `uniqueness.rs` `walk` (after `:352`)**

After the `Term::Assign { value, .. } => { ... }` arm following
`Term::Mut` at `:346`, add (mirror the Mut arm's `self.walk`
calls + the `pos`/`Position::Consume` choice verbatim from
`:346-351`):

```rust
            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);
                }
            }
```

- [ ] **Step 13: `reuse_shape.rs` `walk` (after `:267`)**

After `Term::Assign { value, .. } => self.walk(value)` (`:267`)
following `Term::Mut` at `:261`, add:

```rust
            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);
                }
            }
```

- [ ] **Step 14: `pre_desugar_validation.rs` `walk_term` (after `:135`)**

After `Term::Assign { value, .. } => walk_term(value)` (`:135`)
following `Term::Mut` at `:129`, add:

```rust
        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(())
        }
```

- [ ] **Step 15: Build ailang-check**

Run: `cargo build -p ailang-check 2>&1 | tail -3`
Expected: PASS — `ailang-check` compiles.

---

## Task 6: ailang-codegen arms (stub + pass-through) + ail/main.rs arms

**Files:**
- Modify: `crates/ailang-codegen/src/lambda.rs`
- Modify: `crates/ailang-codegen/src/escape.rs`
- Modify: `crates/ailang-codegen/src/lib.rs`
- Modify: `crates/ail/src/main.rs`

- [ ] **Step 1: `lambda.rs` `collect_captures` (after `:478` Mut arm)**

After the `Term::Assign` arm following `Term::Mut` at `:478`
(newly-bound roll-back pattern), add (mirror the Mut arm's
`Self::collect_captures(...)` signature + `bound.insert` /
`newly_bound` roll-back verbatim from `:478-`):

```rust
            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);
                }
            }
```

- [ ] **Step 2: `escape.rs` `walk` (after `:203` Mut arm)**

After `Term::Assign { value, .. } => walk(value, out)` (`:203`)
following `Term::Mut` at `:197`, add:

```rust
        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);
            }
        }
```

- [ ] **Step 3: `escape.rs` `escapes` (after `:395` Mut arm)**

After the `Term::Assign` arm following `Term::Mut` at `:389`, add:

```rust
        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
        }
```

- [ ] **Step 4: `escape.rs` `collect_free_vars` (after `:506` Mut arm)**

After the `Term::Assign` arm following `Term::Mut` at `:506`
(add-then-walk-then-remove `newly` pattern), add (mirror the Mut
arm's `bound.insert`/`newly`/restore verbatim):

```rust
        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);
            }
        }
```

- [ ] **Step 5: `lib.rs` `lower_term` STUB (after the `Term::Mut` arm at `:1762`)**

The `Term::Mut { vars, body } =>` arm at `:1762` has real mut.3
lowering and ends with the saved-binding restore loop (around
`:1804`+) followed by a `Term::Assign` arm. After that
`Term::Assign` arm, before the `lower_term` match's closing brace,
add the iter-1 STUB (real loop-header/phi/back-edge lowering is
loop-recur iter 3):

```rust
            // 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(),
            )),
```

(`CodegenError::Internal(String)` is the same constructor used at
`lib.rs:1779` and `:3069`.)

- [ ] **Step 6: `lib.rs` `synth_with_extras` (after `:3095`)**

After `Term::Assign { .. } => Ok(Type::unit())` (`:3095`) following
`Term::Mut { body, .. } => self.synth_with_extras(body, extras)`
(`:3094`), before the match closing `}` (`:3096`), add:

```rust
            // 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()),
```

- [ ] **Step 7: `main.rs` `walk_term` (after `:1534` Mut arm)**

After the `Term::Assign` arm following `Term::Mut` at `:1520`
(newly-bound `scope` roll-back), add (mirror the Mut arm's
`scope.insert`/`newly`/`scope.remove` verbatim from `:1520-1534`):

```rust
        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);
            }
        }
```

- [ ] **Step 8: `main.rs` `rewrite_term` (after the `Term::Mut` arm at `:2754`)**

The `Term::Mut { vars, body } =>` arm at `:2754` rewrites each
`v.ty` via `rewrite_type` and each `v.init` + `body` via
`rewrite_term` (in-place `&mut`). After the `Term::Assign` arm
that follows it, add (mirror that arm's `rewrite_type` /
`rewrite_term` argument lists verbatim):

```rust
            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,
                    );
                }
            }
```

- [ ] **Step 9: Build the whole workspace**

Run: `cargo build --workspace 2>&1 | tail -3`
Expected: PASS — every crate compiles (no `non-exhaustive
patterns` errors anywhere).

---

## Task 7: Schema/drift anchors + DESIGN.md + hash pin + positive fixture + full suite

**Files:**
- Modify: `docs/DESIGN.md`
- Modify: `crates/ailang-core/tests/design_schema_drift.rs`
- Modify: `crates/ailang-core/tests/spec_drift.rs`
- Modify: `crates/ailang-core/tests/schema_coverage.rs`
- Modify: `crates/ailang-core/tests/hash_pin.rs`
- Create: `examples/loop_sum_to.ail`

- [ ] **Step 1: Add `"t":"loop"` / `"t":"recur"` schema blocks to DESIGN.md**

In `docs/DESIGN.md`, immediately after the `{ "t": "assign",
"name": "<id>", "value": Term }` block (the `"value": Term }` line
is 2422), before the closing ```` ``` ```` fence (line 2423), add:

```
// 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/0034-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, ... ] }
```

(The literal substrings `"t": "loop"` and `"t": "recur"` each
appear contiguously on one line — the `design_schema_drift.rs`
exemplar anchors `r#""t": "loop""#` / `r#""t": "recur""#` are
matched by `data_model_section().contains(...)`; no soft-wrap may
split them. This is the planner self-review item-6 pin/replacement
contiguity check, satisfied here.)

- [ ] **Step 2: Extend `design_schema_drift.rs`**

In `crates/ailang-core/tests/design_schema_drift.rs`, in the
`exemplars` vec, immediately after the `assign` tuple (ends `:153`),
add:

```rust
        (
            r#""t": "loop""#,
            Term::Loop {
                binders: Vec::new(),
                body: Box::new(Term::Lit { lit: Literal::Unit }),
            },
        ),
        (
            r#""t": "recur""#,
            Term::Recur { args: vec![] },
        ),
```

In the exhaustive tag `match term { ... }` (`:159-175`), after
`Term::Assign { .. } => "assign",` (`:174`), add:

```rust
            Term::Loop { .. } => "loop",
            Term::Recur { .. } => "recur",
```

- [ ] **Step 3: Extend `spec_drift.rs`**

In `crates/ailang-core/tests/spec_drift.rs`, in the `exemplars`
vec, immediately after the `(assign` tuple (ends `:130`), add:

```rust
        (
            "(loop",
            Term::Loop {
                binders: Vec::new(),
                body: Box::new(Term::Lit { lit: Literal::Unit }),
            },
        ),
        (
            "(recur",
            Term::Recur { args: vec![] },
        ),
```

In the exhaustive `match term { ... }` (`:138-154`), after
`Term::Assign { .. } => "assign",` (`:153`), add:

```rust
            Term::Loop { .. } => "loop",
            Term::Recur { .. } => "recur",
```

(The anchors `(loop` / `(recur` are the grammar lines added to
`form_a.md` in Task 2 Step 6 — `FORM_A_SPEC.contains("(loop")`
passes because `(loop (NAME TYPE INIT)* …` is present contiguously.)

- [ ] **Step 4: Extend `schema_coverage.rs`**

In `crates/ailang-core/tests/schema_coverage.rs`:
(a) in `enum VariantTag`, after `TermAssign,` (`:51`), add:

```rust
    TermLoop,
    TermRecur,
```

(b) in `const EXPECTED_VARIANTS`, after `VariantTag::TermAssign,`
(`:98`), add:

```rust
    VariantTag::TermLoop,
    VariantTag::TermRecur,
```

(c) in `fn visit_term`, after the `Term::Assign { value, .. } =>
{ ... }` arm (`:243-246`), before the match closing `}` (`:247`),
add:

```rust
        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);
            }
        }
```

- [ ] **Step 5: Add the hash-stability pin to `hash_pin.rs`**

In `crates/ailang-core/tests/hash_pin.rs`, immediately after the
`fn iter13a_schema_extension_preserves_pre_13a_hashes` test
(ends ~`:88`), add:

```rust
/// 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");
}
```

- [ ] **Step 6: Create the positive round-trip fixture**

Create `examples/loop_sum_to.ail` with exactly the spec's worked
clause-1 program:

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

(If the local `examples/*.ail` convention has no explicit
`(module …)` wrapper, mirror an existing sibling fixture's header
shape verbatim — e.g. `examples/sum.ail` — do not invent one. The
fixture must `ail parse`-round-trip; it is NOT typechecked in
iter 1, so `ail check` failing with the iter-1 `synth`
`CheckError::Internal` stub is expected and is NOT this fixture's
gate. The gate is `round_trip.rs` idempotency only.)

- [ ] **Step 7: Run the full workspace suite + tail-app non-regression**

Run: `cargo test --workspace 2>&1 | tail -15`
Expected: PASS — all tests green, including
`design_schema_drift`, `spec_drift`, `schema_coverage`,
`hash_pin::loop_recur_schema_extension_preserves_pre_loop_recur_hashes`,
`hash_pin::iter13a_schema_extension_preserves_pre_13a_hashes`
(still green — proves additivity), and
`round_trip::parse_then_print_then_parse_is_idempotent_on_every_ail_fixture`
(auto-covers the new `examples/loop_sum_to.ail`).

Run: `cargo test --workspace tail 2>&1 | tail -8`
Expected: PASS — every existing `tail-app` / `tail-do` test
byte-identical (this is the spec §"Testing strategy"
"`tail-app` non-regression" gate and the operational evidence for
Boss-call-1: `verify_tail_positions`' tail-app role is unchanged).

---

## Acceptance criteria (this iteration)

- `Term::Loop` / `Term::Recur` / `struct LoopBinder` exist as
  strictly-additive nodes with canonical JSON `"t":"loop"` /
  `"t":"recur"`; `binders` has no `skip_serializing_if`.
- `(loop …)` / `(recur …)` parse, print, and round-trip; the spec's
  worked `sum_to` program is a green `examples/*.ail` fixture under
  `round_trip.rs` auto-discovery.
- Every exhaustive `match`-on-`Term` in all six crates + the three
  drift tests has loop/recur arms; `cargo build --workspace` and
  `cargo test --workspace` are green.
- Pre-existing canonical-JSON hashes are bit-stable
  (`iter13a` + the new `loop_recur` hash pin both green).
- NO typecheck semantics (`synth` returns the `CheckError::Internal`
  stub for Loop/Recur) and NO real codegen (`lower_term` returns
  the `CodegenError::Internal` stub) — those are iters 2 and 3.
- `tail-app` / `tail-do` / Decision-8 tests byte-identical; no
  `Diverge`, no `verify_structural_recursion`, no
  `NonStructuralRecursion`, no `verify_loop_body` (iter 2).
- `verify_tail_positions`' tail-app verification role is unchanged
  (operational evidence: the tail-app non-regression test in
  Task 7 Step 7), satisfying the spec's "byte-unchanged"
  acceptance criterion under the Boss-call-1 reading.

## Cross-references

- Parent spec: `docs/specs/0034-loop-recur.md`
  (Components 1/2/3/6 = this iter; Component 4 = iter 2;
  Component 5 = iter 3).
- mut.1 precedent for the additive-node-across-no-wildcard-workspace
  pattern + the `Internal`-stub-at-the-two-dispatch-points shape:
  `docs/specs/0029-mut-local.md` §"Iteration mut.1".
- Boss-call-1 (`verify_tail_positions` byte-unchanged reading) and
  Boss-call-2 (codegen in iter-1 as stubs) are recorded in the
  plan header above and must be mirrored into the per-iter journal
  at iter close.