AILang/docs/plans/0072-iter-it.2.md

it.2 — guardedness checker + Diverge effect — Implementation Plan

Parent spec: docs/specs/0031-iteration-discipline.md

For agentic workers: REQUIRED SUB-SKILL: use skills/implement to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Make non-structural recursion-by-call a compile error (NonStructuralRecursion), keeping the accumulator-carrying structural walk classified as structural (pure, total), the 21 tail-app corpus fixtures grandfathered, and any loop-bearing function forced to declare the now-real Diverge effect.

Architecture: All work is in crates/ailang-check plus a DESIGN.md prose sync and fixtures. One new whole-body verification pass verify_structural_recursion runs as a sibling of verify_tail_positions in check_fn's post-synth region; one new CheckError::NonStructuralRecursion; one term_contains_loop syntactic check that injects "Diverge" into the raised effect set so the existing UndeclaredEffect reconciliation does the rest. No AST variant is added, so there is no walker-arm/schema-coverage fan-out. Nothing tail-related is removed (that is it.3).

Tech Stack: ailang-check (lib.rs: CheckError, check_fn, a new module-or-fn for the guardedness pass), DESIGN.md, examples/ fixtures, crates/ailang-check/tests/, the carve-out inventory test.

---

Design decisions (Boss-resolved; not implementer judgement calls)

• DD-1 — standalone post-synth pass. verify_structural_recursion( f: &FnDef, env: &Env) -> Result<(), CheckError> is a new whole-body walk invoked in check_fn immediately after the verify_tail_positions call (recon HEAD: lib.rs:2021), before the declared-vs-raised effect reconciliation (lib.rs:2023-2028). It is the structural sibling of verify_tail_positions / verify_loop_body (recon: lib.rs:2627/:2769), which already bind Term::App { tail }. It is NOT folded into the synth Term::App arm (lib.rs:3255, which discards tail via ..): guardedness is a body-shape invariant, not a type-synthesis fact, and it needs (a) the whole body to build the provenance map before judging any call and (b) the tail binding the synth arm drops.
• DD-2 — the smaller set algorithm (the structural check). For a recursive FnDef, for each candidate structural parameter position i (every parameter whose declared type is a Type::Con ADT — not a primitive, not a function type): walk the body maintaining smaller: HashSet<String> = variables known strictly structurally smaller than the parameter bound at position i. smaller starts empty. At Term::Match { scrutinee, arms } where scrutinee is Term::Var { name } and (name == the parameter-i binder name OR name ∈ smaller): for each arm, the variables bound by a constructor sub-pattern (Pattern::Ctor { fields }, recon ast.rs:611-626, type_check_pattern lib.rs:3994) are added to a per-arm copy of smaller while walking that arm's body. A recursive call (DD-3) is guarded at position i iff its argument expression at position i is Term::Var { name } with name ∈ smaller at that call site. The def is structural iff there exists at least one candidate position i guarded at every recursive call site (implicit inference per spec D1 — no annotation). Accumulator positions are never examined, so they are unconstrained (spec D1: the foldl-shape accumulator walk is structural). If no candidate position is guarded at all recursive call sites ⇒ NonStructuralRecursion.
• DD-3 — recursive-call identification + mutual grouping. Self-recursion: a Term::App whose callee_name(callee) (recon lib.rs:4127-4132) equals the enclosing def name (f.name; in_def is already threaded but unused for this — the new pass takes f directly). Term::LetRec clause bodies use the clause name as the recursion name. Mutual recursion: a module-level pre-pass computes ADT families as connected components of the ADT type-reference graph (nodes = type decl names; an undirected edge between T and U iff U appears in a constructor field type of T or vice versa; union-find). A set of FnDefs forms a mutual structural group iff they call each other (direct Term::App→Term::Var), every member has a structural parameter whose type head lies in one family component, and every self/cross recursive call passes, at the callee's structural position, a variable in the caller's smaller set. This admits exactly spec-D1's named set (even/odd-over-Nat — one family; mutual JSON — one family; tree/forest — one component via the cross-reference edge). A general lexicographic/size-measure ordering is out of scope (spec D1, deferred).
• DD-4 — Diverge injection. In check_fn, before the :2023-2028 reconcile loop: if term_contains_loop(&f.body) then insert "Diverge" into the raised effects BTreeSet. term_contains_loop recurses structurally but stops at Term::Lam boundaries (a lambda is a value with its own arrow effect row — a loop inside it executes on closure call, not here; this mirrors exactly how !IO inside a lam does not leak to the enclosing fn). The "calls a Diverge-declaring callee" half needs no new code: a callee's Type::Fn.effects already flows into the raised set at lib.rs:3295-3297, identically to IO. The lam-arrow case (a loop inside a Term::Lam body ⇒ the lam's arrow type carries Diverge) is wired at the existing lam sub-effect reconcile site (recon lib.rs:3582-3585) with the same term_contains_loop-stops-at-inner-lam check applied to the lam body. The existing UndeclaredEffect (recon lib.rs:438, code arm :751, raised at :2026) does the enforcement — no new diagnostic variant for Diverge. Structural recursion injects nothing.

Recon line numbers are HEAD-at-recon and may have drifted. Drive every edit site off grep/cargo build, not the literal numbers (cf. memory: recon misindexing recurs; the numbers are anchors, the symbols are authoritative).

---

Files this plan creates or modifies

Create:

• Test: crates/ailang-check/tests/structural_recursion_pin.rs — driver mirroring loop_recur_pin.rs; positives + negatives
• Test: examples/struct_rec_list_len.ail — positive: structural list length (recurse on tail)
• Test: examples/struct_rec_foldl_sum.ail — positive: accumulator (foldl-shape) over a list — structural, Diverge-free
• Test: examples/struct_rec_tree_forest.ail — positive: mutual tree/forest, same family
• Test: examples/loop_needs_diverge.ail — positive: a fn that declares !Diverge and contains a loop
• Test: examples/test_non_structural_recursion.ail.json — negative: self-call on a non-decreasing arg, not tail-marked
• Test: examples/test_mutual_cross_family.ail.json — negative: mutual recursion across two unrelated ADT families
• Test: examples/test_loop_missing_diverge.ail.json — negative: loop-bearing fn that omits !Diverge

Modify:

• crates/ailang-check/src/lib.rs — CheckError enum (recon :401-735), code() (:743-787), ctx() (:791-867), check_fn post-synth region (:2011-2028), the new pass + helpers (new code, sited next to verify_tail_positions :2627/verify_loop_body :2769), the lam sub-effect reconcile (:3582-3585)
• crates/ailang-core/tests/carve_out_inventory.rs — EXPECTED 17 → 20 (three new .ail.json negatives) + the stale "Twelve" header comment (:6)
• docs/DESIGN.md — Decision 3 (:163-168), the Data-model it.2 hook sentence (:2449-2451)

---

Task 1: NonStructuralRecursion diagnostic plumbing

Files: crates/ailang-check/src/lib.rs.

• Step 1.1: RED — assert the code string exists.

In crates/ailang-check/tests/structural_recursion_pin.rs (new; copy the harness preamble of crates/ailang-check/tests/loop_recur_pin.rs verbatim — same check_fixture/check_workspace→Vec<String> helper):

mod common; // if loop_recur_pin uses an inline helper, inline it identically here instead
#[test]
fn non_structural_recursion_code_is_registered() {
    // A CheckError::NonStructuralRecursion must map to the kebab code.
    // Construct it directly and assert code(); mirrors how the it.1
    // Recur* variants are unit-tested if such a test exists, else
    // assert via a fixture in Task 2. This step only pins the code()
    // arm exists and returns the exact string.
    use ailang_check::CheckError;
    let e = CheckError::NonStructuralRecursion {
        callee: "f".into(),
        arg: "n".into(),
    };
    assert_eq!(e.code(), "non-structural-recursion");
}

Run: cargo test --workspace -p ailang-check non_structural_recursion_code_is_registered Expected: FAIL — CheckError::NonStructuralRecursion does not exist (compile error: no variant).

• Step 1.2: Add the variant.

In crates/ailang-check/src/lib.rs CheckError enum, beside the it.1 RecurTypeMismatch/RecurNotInTailPosition variants (recon :716-727), add — Display body bracket-[code]-free (the CLI formatter prepends [code]; F2 convention; mirror the it.1 Recur* variants' exact attribute/field style):

#[error("recursive call to `{callee}` is not on a structurally-smaller argument (`{arg}`); express this iteration as `(loop …)` / `recur`")]
NonStructuralRecursion { callee: String, arg: String },

• Step 1.3: code() + ctx() arms.

In fn code() (recon :743-787), beside the RecurNotInTailPosition => "recur-not-in-tail-position" arm, add:

CheckError::NonStructuralRecursion { .. } => "non-structural-recursion",

In fn ctx() (recon :791-867), before the _ => empty-Object fallthrough (:865), add a structured arm mirroring RecurTypeMismatch's ctx shape (recon :862-864):

CheckError::NonStructuralRecursion { callee, arg } => {
    serde_json::json!({ "callee": callee, "arg": arg })
}

Do not add anything to diagnostic.rs — there is no doc-list there; code() is the authoritative registry (memory: plan-pseudo-vs-reality).

• Step 1.4: GREEN.

Run: cargo test --workspace -p ailang-check non_structural_recursion_code_is_registered Expected: PASS.

Run: cargo test --workspace 2>&1 | tail -3 Expected: green (additive variant; existing exhaustive CheckError matches — if any non-_ exhaustive match over CheckError fails to compile, add the mirror arm there; drive off cargo build E0004).

---

Task 2: Self-structural-recursion pass + it.2-only grandfather

Files: crates/ailang-check/src/lib.rs, examples/struct_rec_list_len.ail, examples/struct_rec_foldl_sum.ail, examples/test_non_structural_recursion.ail.json, crates/ailang-check/tests/structural_recursion_pin.rs, crates/ailang-core/tests/carve_out_inventory.rs.

• Step 2.1: RED — fixtures + pins.

Create (Form-A spellings copied verbatim from an existing list fixture — read examples/std_list.ail and match its type/match/ ctor surface; do not invent surface):

examples/struct_rec_list_len.ail — len(xs) recursing on the tail bound by a Cons pattern (structural, Diverge-free). examples/struct_rec_foldl_sum.ail — go(xs, acc) recursing on tail with acc threaded (accumulator; structural by the tail position; D1 — must pass clean, no Diverge). examples/test_non_structural_recursion.ail.json — a self-call where the structural-position arg is NOT a match-bound sub-component (e.g. f(n) = … f(n) … or f(xs) = … f(xs) …), and the call is not tail-marked.

Add to structural_recursion_pin.rs:

#[test]
fn structural_list_len_is_clean() {
    assert!(check_fixture("examples/struct_rec_list_len.ail").is_empty());
}
#[test]
fn foldl_accumulator_is_structural_and_clean() {
    assert!(check_fixture("examples/struct_rec_foldl_sum.ail").is_empty());
}
#[test]
fn non_structural_self_call_is_rejected() {
    assert!(check_fixture("examples/test_non_structural_recursion.ail.json")
        .contains(&"non-structural-recursion".to_string()));
}

Add the one new .ail.json to carve_out_inventory.rs EXPECTED (17 → 18; fix the stale :6 header comment count too).

Run: cargo test --workspace -p ailang-check --test structural_recursion_pin Expected: FAIL — no guardedness pass exists; all three fail (positives clean only by accident, negative not rejected).

• Step 2.2: The pass — self-recursion + smaller algorithm (DD-2/DD-3).

Add next to verify_tail_positions (recon :2627):

/// it.2: structural-recursion guardedness. A recursive call must
/// pass a structurally-smaller argument at some inferable parameter
/// position. Accumulator positions are unconstrained (spec D1).
/// it.2-only: a `tail: true`-marked recursive call is grandfathered
/// (spec it.2 "Transitional grandfather"; it.3 removes this).
fn verify_structural_recursion(f: &FnDef, env: &Env) -> Result<(), CheckError> {
    let rec_name = &f.name;
    // candidate structural positions: params whose decl type is an ADT Con
    let cand: Vec<usize> = adt_param_positions(&f.ty, env);
    let calls = collect_rec_calls(&f.body, rec_name); // Vec<&[Term]> arg-lists of unguarded-eligible calls
    if calls.is_empty() { return Ok(()); }
    for &i in &cand {
        if calls.iter().all(|c| call_guarded_at(c, i, f, env)) {
            return Ok(()); // some position is structural at every call
        }
    }
    // not structural at any position — but grandfather tail-marked calls
    let offending = first_unguarded_non_tail_call(&f.body, rec_name, &cand, f, env);
    match offending {
        None => Ok(()), // every unguarded call was tail:true (grandfathered)
        Some((callee, arg)) => Err(CheckError::NonStructuralRecursion { callee, arg }),
    }
}

Implement the helpers in the same module, fully:

• adt_param_positions(ty, env) — from the fn's Type::Fn { params, .. }, the indices whose Type is a Type::Con { name, .. } resolving (via env) to a type decl (not a primitive Int/Float/Bool/ Unit/Str, not Type::Fn). Use the existing env type-lookup (grep how synth resolves a Type::Con to its decl).
• collect_rec_calls(body, name) — walk body; collect the argument slice of every Term::App { callee, args, tail } where callee_name(callee) == name (recon callee_name :4127-4132) and tail == false (the grandfather: tail == true recursive calls are not collected, hence never cause rejection). Also walk into Term::LetRec clause bodies with the clause name. Stop at Term::Lam (a lambda body is a separate def's territory; its own FnDef-equivalent check covers it — keep it.2 conservative and consistent with DD-4's lam boundary).
• call_guarded_at(arg_slice, i, f, env) — arg_slice.get(i) is Some(Term::Var { name }) and name is in the smaller set in effect at that syntactic position. Implement smaller by a single recursive walk walk(term, smaller: &HashSet<String>) that, at Term::Match { scrutinee: Term::Var { name }, arms } where name == param_i_name || smaller.contains(name), extends a clone of smaller with every Pattern::Ctor-bound field variable of each arm (recon: patterns are flat post-desugar — Pattern::Ctor { fields } fields are Pattern::Var/Pattern::Wild, ast.rs:611- 626) before recursing into that arm body. The recursive-call argument check consults the smaller set live during this walk (fold the call-collection and the guardedness test into the one smaller-threaded walk rather than two passes, so position context is exact).
• first_unguarded_non_tail_call(...) — same walk; returns the (callee_name, arg_display) of the first non-tail recursive call not guarded at any candidate position, for the diagnostic.

(Use the real Env, Type, Pattern, Term, callee_name identifiers from the neighbouring code — grep each before use; do not invent. arg_display = the pretty/short form the it.1 Recur* diagnostics use for an argument.)

• Step 2.3: Wire into check_fn.

In check_fn, immediately after the verify_tail_positions(...) call (recon :2021) and before the effect reconcile (:2023):

verify_structural_recursion(f, &env)?;

(Match the exact env/binding names in scope at that point — grep the verify_tail_positions call site and mirror its argument sourcing.)

• Step 2.4: GREEN.

Run: cargo test --workspace -p ailang-check --test structural_recursion_pin Expected: PASS — list_len + foldl clean, non-structural rejected.

Run: cargo test --workspace 2>&1 | tail -3 Expected: green. Critical: the 21 tail-app corpus fixtures must still pass — they recurse non-structurally but are tail:true-marked, so collect_rec_calls skips them (grandfather). If any tail-app fixture now fails non-structural-recursion, the grandfather is wrong — fix collect_rec_calls's tail == false guard, do not weaken the structural check.

---

Task 3: Mutual recursion — ADT-family components

Files: crates/ailang-check/src/lib.rs, examples/struct_rec_tree_forest.ail, examples/test_mutual_cross_family.ail.json, crates/ailang-check/tests/structural_recursion_pin.rs, crates/ailang-core/tests/carve_out_inventory.rs.

• Step 3.1: RED.

examples/struct_rec_tree_forest.ail — mutual tree_size/ forest_size over type Tree = Node(Int, Forest) / type Forest = Nil | Cons(Tree, Forest) (the cross-reference makes them one family component). examples/test_mutual_cross_family.ail.json — f/g mutually recursive where f's structural param is a List and g's is an unrelated Tree (distinct components).

Add pins: tree_forest_mutual_is_clean (empty), and mutual_cross_family_is_rejected (contains "non-structural-recursion"). Add the new .ail.json to carve_out_inventory.rs EXPECTED (18 → 19).

Run: cargo test --workspace -p ailang-check --test structural_recursion_pin Expected: FAIL — tree/forest rejected (cross-calls not recognised as same-group) and/or cross-family not rejected.

• Step 3.2: ADT-family components + mutual grouping.

Add:

/// Connected components of the ADT type-reference graph.
/// Two `type` names share a family iff one transitively appears in
/// the other's constructor field types (undirected, union-find).
fn adt_families(env: &Env) -> UnionFind<String> { /* … */ }

/// FnDefs that (a) directly call each other and (b) each have a
/// structural param whose type head is in one family component.
fn mutual_structural_group<'a>(f: &'a FnDef, module: &'a [FnDef], fams: &UnionFind<String>) -> Vec<&'a FnDef> { /* … */ }

Extend verify_structural_recursion: if f is in a mutual_structural_group, a cross-call to a group member is treated like a self-call for the smaller/call_guarded_at test (the callee's structural arg must be in the caller's smaller set), and collect_rec_calls collects cross-group callees too (still tail == false only — grandfather still applies). A mutual fn whose group fails the family-component test, or whose cross-call arg is not smaller, yields NonStructuralRecursion.

(UnionFind — use a tiny inline BTreeMap-backed union-find in this module; do not add a dependency. The module FnDef list: grep how check_fn is iterated per workspace module and pass the sibling FnDefs in; if check_fn is called per-def without the sibling list, thread the module's &[FnDef] into verify_structural_recursion from the same caller that has the module — recon: confirm the workspace-check loop's module handle.)

• Step 3.3: GREEN.

Run: cargo test --workspace -p ailang-check --test structural_recursion_pin Expected: PASS — tree/forest clean, cross-family rejected.

Run: cargo test --workspace 2>&1 | tail -3 Expected: green; tail-app corpus still grandfathered-clean.

---

Task 4: Diverge effect injection (DD-4)

Files: crates/ailang-check/src/lib.rs, examples/loop_needs_diverge.ail, examples/test_loop_missing_diverge.ail.json, crates/ailang-check/tests/structural_recursion_pin.rs, crates/ailang-core/tests/carve_out_inventory.rs.

• Step 4.1: RED.

examples/loop_needs_diverge.ail — a fn whose body contains a (loop …) and whose signature declares !Diverge (copy the loop_counter.ail shape from it.1; add Diverge to its effect row — grep how !IO is written in a Form-A fn signature and mirror it for Diverge). examples/test_loop_missing_diverge.ail.json — the same fn but without Diverge in the declared effect row.

Pins:

#[test]
fn loop_fn_declaring_diverge_is_clean() {
    assert!(check_fixture("examples/loop_needs_diverge.ail").is_empty());
}
#[test]
fn loop_fn_missing_diverge_is_rejected() {
    assert!(check_fixture("examples/test_loop_missing_diverge.ail.json")
        .contains(&"undeclared-effect".to_string()));
}
#[test]
fn structural_recursion_is_diverge_free() {
    // struct_rec_list_len has no loop, no Diverge declared → clean
    assert!(check_fixture("examples/struct_rec_list_len.ail").is_empty());
}

Add the .ail.json to carve_out_inventory.rs EXPECTED (19 → 20).

Run: cargo test --workspace -p ailang-check --test structural_recursion_pin Expected: FAIL — loop_fn_missing_diverge_is_rejected fails (loop does not yet inject Diverge, so no undeclared-effect).

• Step 4.2: term_contains_loop + injection.

Add:

/// True iff `t` syntactically contains a `Term::Loop`, NOT
/// descending into `Term::Lam` bodies (a lambda's loop runs on
/// closure call; it carries Diverge on the lam's own arrow type,
/// not on the enclosing fn — coherent with how !IO scopes to lam).
fn term_contains_loop(t: &Term) -> bool {
    match t {
        Term::Loop { .. } => true,
        Term::Lam { .. } => false,
        // recurse into every other child; mirror the child set of
        // the existing structural Term walks (grep verify_tail_positions
        // arms for the exhaustive child list)
        _ => term_children(t).iter().any(|c| term_contains_loop(c)),
    }
}

(If no term_children helper exists, write the explicit match over all Term variants — drive the variant list off cargo build exhaustiveness, mirror verify_tail_positions' arm set; Term::Lam returns false, Term::Loop returns true, all others recurse their children incl. Term::Recur args, Term::Match arms, Term::Let/If/Seq/App/Do/Mut/Assign/....)

In check_fn, before the :2023-2028 declared-vs-raised reconcile loop, after the raised effects set is populated:

if term_contains_loop(&f.body) {
    effects.insert("Diverge".to_string());
}

(Use the exact raised-set identifier and type the reconcile loop reads — recon: a BTreeSet<String> named effects; grep the UndeclaredEffect-raising loop at :2023-2028 and match its source set name exactly.)

• Step 4.3: Lam-arrow Diverge coherence.

At the Term::Lam sub-effect reconcile site (recon :3582-3585): if the lam body term_contains_loop, ensure "Diverge" is in the lam's reconciled raised-effect set before it is checked against the lam's declared arrow effects (same term_contains_loop, applied to the lam body; the helper's own Term::Lam => false correctly stops at a further-nested lam). Mirror the existing !IO-through-lam reconcile shape verbatim, only adding the loop→Diverge insert.

• Step 4.4: GREEN.

Run: cargo test --workspace -p ailang-check --test structural_recursion_pin Expected: PASS — declaring-Diverge clean, missing-Diverge rejected with undeclared-effect, structural recursion still Diverge-free.

Run: cargo test --workspace 2>&1 | tail -3 Expected: green. The it.1 loop_counter.ail/loop_in_lambda_e2e.ail fixtures: if they have a (loop …) but no declared !Diverge, they now (correctly) require it — update those two it.1 fixtures' signatures to declare !Diverge (this is the first iteration where a bare loop is an error; it is in-scope: the spec's it.2 says loop-bearing fns carry !Diverge, and the it.1 fixtures are loop- bearing). Record the fixture-signature update in the journal. Do NOT instead weaken the injection.

---

Task 5: DESIGN.md prose sync

Files: docs/DESIGN.md.

• Step 5.1: Decision 3 amendment.

Edit docs/DESIGN.md Decision 3 (recon :163-168). Current text calls Diverge a nominally-wired MVP effect. Replace the relevant sentence so it states: Diverge is the effect carried by any function whose body contains a loop (or that calls a Diverge-declaring function); structural recursion is pure and total and carries no effect. Keep IO description intact.

• Step 5.2: Data-model it.2 hook sentence.

Edit the §"Data model" loop/recur block sentence (recon :2449-2451) that says "The structural-recursion restriction and the Diverge effect land in it.2" → state they are now in effect (present tense), tail-app/tail-do retirement remains it.3.

• Step 5.3: Drift-anchor regression check.

Run: cargo test --workspace -p ailang-core design_schema_drift schema_coverage spec_drift Expected: PASS — it.2 adds no AST variant; §"Data model" loop/ recur anchors are unchanged (only the trailing status sentence inside the block is reworded; verify the anchor strings the test greps are not the reworded substring). If the drift test scans a substring you changed, restore that exact substring and move the status note to an adjacent line.

---

Task 6: it.2 acceptance gate

Files: none (verification only).

• Step 6.1: Full workspace.

Run: cargo test --workspace 2>&1 | tail -3 Expected: all green.

• Step 6.2: Spec it.2 acceptance bullets (verbatim).

Verify each, by the named pin:

• structural list/tree/JSON walk + foldl accumulator clean, Diverge-free → structural_list_len_is_clean, foldl_accumulator_is_structural_and_clean, structural_recursion_is_diverge_free, tree_forest_mutual_is_clean

• non-structural recursion-by-call → non_structural_self_call_is_rejected

• loop-bearing fn missing !Diverge → loop_fn_missing_diverge_is_rejected

• mutual same-family passes, cross-family fails → tree_forest_mutual_is_clean, mutual_cross_family_is_rejected

• mut_counter/mut_sum_floats not migrated, still grandfathered: Run ail run examples/mut_counter.ail → still 55 (they use tail-app; grandfathered; unchanged)

• cargo test --workspace green → Step 6.1

• Step 6.3: tail-app corpus grandfather proof.

Run: ail check examples/bench_compute_intsum.ail examples/list_map_poly.ail examples/sort.ail Expected: all clean (non-structural but tail:true-marked → grandfathered; this is the load-bearing it.2 invariant that keeps the corpus alive until it.3 migrates it).

---

Self-review (planner Step 5)

1. Spec coverage. Spec §Components it.2 (a) guardedness → T2/T3; (b) grandfather → T2.2 (collect_rec_calls tail==false); (c) Diverge → T4; (d) DESIGN.md → T5. §Error-handling NonStructuralRecursion (one new variant, UndeclaredEffect reused) → T1/T4. §Data-flow steps 3–4 → T2/T3 (pass) + T4 (effect reconcile). §Testing-strategy it.2 + acceptance bullets → T2/T3/T4 pins + T6. D1 (implicit, foldl=structural, same-family) → DD-2/DD-3 + the foldl pin. D2 (Diverge, no new variant) → DD-4 + T4. All it.2 sections covered; it.3 explicitly excluded everywhere.
2. Placeholder scan. No "TBD/TODO/implement later/similar to Task/add appropriate". The pass helpers are specified with signatures + the exact algorithm (DD-2/DD-3) + the grep-the-real-identifier instruction; that is an exact transformation, not a placeholder. Per memory (plan-pseudo-vs-reality): no prose round-trip is scripted anywhere; no diagnostic.rs doc-list claim (Step 1.3 explicitly says code() is the registry, do not touch diagnostic.rs); recon line numbers are flagged drift-prone with "drive off grep/cargo build" in the DD preamble.
3. Type/name consistency. NonStructuralRecursion {callee,arg}, code non-structural-recursion, verify_structural_recursion, term_contains_loop, adt_families, mutual_structural_group, collect_rec_calls, call_guarded_at, structural_recursion_pin.rs, the eight fixtures — consistent across all tasks and the files section.
4. Step granularity. Each step is one action (one fixture set / one helper / one wire-in / one command) in the 2–5-min band; the largest (T2.2, the pass) is one cohesive algorithm with the algorithm given.
5. No commit steps. None. Work stays in the working tree; Boss commits the whole it.2 diff at iter end.

Recorded risk (named, with decision rule — not a placeholder): if check_fn is invoked per-FnDef without the sibling module &[FnDef] in scope (T3.2 needs it for mutual grouping), thread the module slice from the workspace-check loop that already owns it (recon flagged this as the one unconfirmed handle); the self-only path (T2) is unaffected and lands first, so T3 can be re-scoped to "self + same-file siblings via the existing module iteration" if the workspace handle proves awkward — T2's value ships regardless.