plan: it.3 retire tail-app/tail-do + corpus migration — 7 tasks

Destructive terminal iteration. Safe order: oracle-capture →
migrate corpus → remove it.2 exemptions (the migration-completeness
gate) → remove tail machinery + 18g.1 husk-dec → DESIGN/drift
lockstep → accept. DD-4 carries the OQ1 RC-RSS contingency as an
explicit RED-gated step (Task 5.5) with named remediation
(owned-loop-binder-drop-on-recur, Task 5b) per the corrected spec.
DD-5 keeps is_false (shared with drop_iterative). Class-(b)
enumeration is a live sweep (Task 1.3, spec-delegated). Spec
fda9b78 + corrections 2018178/10a0595.

docs/plans/2026-05-15-iter-it.3.md

@@ -0,0 +1,560 @@
+# it.3 — retire tail-app/tail-do + corpus migration — Implementation Plan
+
+> **Parent spec:** `docs/specs/2026-05-15-iteration-discipline.md`
+> (scope-corrected at 2018178 + it.3-recon-corrected at 10a0595)
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
+> to run this plan. Steps use `- [ ]` checkboxes for tracking.
+
+**Goal:** Delete the marked-tail-call concept entirely
+(`Term::App.tail`/`Term::Do.tail`, both surface keywords, the
+`musttail` lowering, `verify_tail_positions`' tail-app role,
+`TailCallNotInTailPosition`, the 18g.1 husk-dec, the it.2
+transitional grandfather + no-ADT-candidate skip, Decision 8 →
+tombstone) and migrate the full corpus non-structural-recursion set
+to `(loop …)`/`recur` (or plain structural calls), every fixture
+byte-identical in observable behaviour to before.
+
+**Architecture:** Destructive + migration. The safe order is
+**oracle → migrate → remove-exemptions → remove-machinery →
+docs/drift → accept**. Migration *before* removal keeps the
+round-trip invariant green throughout (a migrated `.ail` has no
+`(tail-app …)` so it parses even while the field still exists).
+Removing the it.2 exemptions *before* removing the tail machinery is
+the correctness proof that migration was complete (if any fixture
+still needed the grandfather, that task goes RED — a migration bug,
+fixed in the migration task, never by re-adding the exemption). The
+one genuinely non-mechanical risk is the spec's §Codegen-rework
+contingency: deleting the 18g.1 husk-dec is RC-safe only if it.1
+loop codegen drops superseded owned binders across `recur`; this is
+a RED-gated step with a named remediation (Task 5b).
+
+**Tech Stack:** `ailang-core` (ast/serde), `ailang-surface`
+(parse/print), `ailang-prose`, `ailang-check`
+(verify_tail_positions, the it.2 exemptions, CheckError),
+`ailang-codegen` (musttail, 18g.1 husk-dec, loop-binder RC),
+DESIGN.md, `crates/ailang-core/specs/form_a.md`, the drift/spec/
+schema-coverage test crates, ~25+ `examples/*.ail` fixtures.
+
+---
+
+## Design decisions (Boss-resolved; not implementer judgement calls)
+
+- **DD-1 — oracle = existing tests first, captured snapshots only
+  for the gap.** Many migration-set fixtures already have an
+  e2e/round-trip/bench assertion (authoritative, already in
+  `cargo test --workspace`). The byte-identical-stdout requirement
+  is satisfied by: (a) those existing tests staying green across
+  migration; (b) for a fixture with a `main` but no dedicated stdout
+  test, a snapshot captured in Task 1 to
+  `bench/it3-oracle/<stem>.out` and diffed post-migration; (c) for a
+  check-only fixture (no `main`), the oracle is `ail check` exit
+  status + diagnostic-code list, captured the same way. No fixture
+  is migrated without an oracle.
+- **DD-2 — migrate before remove.** The `Term::App.tail` field stays
+  present through Tasks 1–4; only Task 5 deletes it. This keeps
+  parse/print/serde/round-trip compiling and green while fixtures
+  are rewritten. The field is simply unused by migrated fixtures.
+- **DD-3 — exemption-removal is the migration-completeness gate.**
+  Task 4 removes the it.2 `tail==false` grandfather AND the
+  no-ADT-candidate skip. Its green `cargo test --workspace` *is* the
+  proof that Task 3's migration left no fixture depending on either
+  exemption. A RED here is a Task-3 migration defect to fix in
+  Task 3, never by softening Task 4.
+- **DD-4 — the 18g.1 / RC-RSS contingency (spec §Codegen-rework).**
+  Task 5 deletes the 18g.1 pre-tail-call husk-dec
+  (`match_lower.rs:658–736`) — field-forced, it cannot compile once
+  `Term::App.tail` is gone. RC-safety is **not assumed**: Task 5
+  re-runs the RC-RSS bench pins (18f.2 + the RC-RSS suite) as a
+  hard gate. If RED → Task 5b: add owned-loop-binder-drop-on-`recur`
+  to it.1 loop codegen (the loop-side of the seam; in scope for
+  it.3 per the corrected spec). Keeping 18g.1 is not an option (it
+  cannot survive the field removal).
+- **DD-5 — `is_false` survives.** Recon: `is_false`
+  (`ast.rs:908–916`) is shared with `WorkspaceDef.drop_iterative`
+  (`ast.rs:168`). Delete only the two `tail`-field
+  `skip_serializing_if="is_false"` uses; keep the helper; re-scope
+  its doc-comment to `drop_iterative`.
+
+> Recon line numbers (agent ad6bb077) are HEAD-at-recon. Drive every
+> edit off `grep`/`cargo build` E0004/unused, not the literal
+> numbers (memory: recon misindexing recurs; symbols authoritative).
+
+---
+
+## Files this plan creates or modifies
+
+**Create:**
+- `bench/it3-oracle/MANIFEST.tsv` + `bench/it3-oracle/<stem>.out` —
+  pre-migration behavioural oracle (Task 1; deleted in Task 6 after
+  it has served its purpose, or kept under `bench/` if cheap — Boss
+  call at commit)
+- Test: `crates/ailang-check/tests/no_tail_grandfather_pin.rs` —
+  asserts a non-structural non-tail recursion now hard-fails
+  `non-structural-recursion` (the exemption is gone)
+
+**Modify (HEAD anchors from recon ad6bb077; verify by symbol):**
+- `crates/ailang-core/src/ast.rs:402–408` (`Term::App.tail`),
+  `:442–447` (`Term::Do.tail`), `:908–916` (`is_false` doc only),
+  `:974–1006` (serde test ctors dropping `tail:`)
+- `crates/ailang-surface/src/parse.rs:40–55,1203,1207,1224–1227,
+  1274–1317,1368–1395` (EBNF, dispatch, keyword list,
+  parse_tail_app/parse_tail_do, parse_app_body/parse_do_body `tail`
+  param)
+- `crates/ailang-surface/src/print.rs:417–422,464–466`
+- `crates/ailang-prose/src/lib.rs:573–597,655–658,782–784,
+  1203–1229` (+ delete tests `:1486–1494,2050,2177`)
+- `crates/ailang-check/src/lib.rs:558–562` (`TailCallNotInTailPosition`
+  variant), `:781` (`code()` arm), `:2706–2817`
+  (`verify_tail_positions` tail-app arms `:2709–2727`; KEEP Loop
+  `:2803–2808`/Recur `:2815` + `verify_loop_body:2829–2869`),
+  `:3026–3037` (grandfather `if !*tail` `:3027`), `:3197–3199`
+  (no-ADT-candidate skip)
+- `crates/ailang-codegen/src/lib.rs:2120,2397–2432,2445–2513,
+  2615–2654` (musttail in lower_app/emit_call/emit_indirect_call/
+  lower_effect_op), `crates/ailang-codegen/src/match_lower.rs:658–736`
+  (18g.1 husk-dec — delete)
+- `docs/DESIGN.md`: Decision 8 `:709–747+` (→ tombstone), EBNF
+  `:552–565` (`tail-app-term`/`tail-do-term`), §Data-model
+  `:2357–2359,2373–2375,2452–2467` (tail jsonc + transitional
+  paragraph). **Decision 3 `:163–176` UNTOUCHED** (it.2 payload).
+- `crates/ailang-core/specs/form_a.md:268,270,295–298,378–381,
+  405–407,508–539` (tail grammar + §4 tail-rec exhibit)
+- `crates/ailang-core/tests/design_schema_drift.rs:53–60,87–94`
+  (drop `tail:`), `spec_drift.rs:30–37,64–69` + delete
+  `spec_mentions_tail_variants:331–337`, `schema_coverage.rs`
+  (no tail anchor — verify only)
+- `examples/*.ail` — the full migration set (enumerated in Task 1)
+- `crates/ail/tests/e2e.rs` + any IR-snapshot — migrated/retired
+  per Task 1's fallout map
+
+---
+
+## Task 1: Pre-migration oracle + migration-set enumeration
+
+**Files:** `bench/it3-oracle/*` (create), no code change.
+
+- [ ] **Step 1.1: Build the current `ail` once.**
+
+Run: `cargo build -p ail 2>&1 | tail -1`
+Expected: clean build (HEAD = 10a0595, tail-app fully present).
+
+- [ ] **Step 1.2: Class-(a) — every `(tail-app|tail-do)` fixture.**
+
+Run: `grep -rl -E '\(tail-app|\(tail-do' examples/ | sort | tee /tmp/it3_class_a.txt | wc -l`
+Expected: 23 files (recon-confirmed).
+
+- [ ] **Step 1.3: Class-(b) — no-ADT-candidate counter recursions.**
+
+Read `crates/ailang-check/src/lib.rs` `verify_structural_recursion`
++ the grandfather (`:3027 if !*tail`) + the no-ADT-candidate skip
+(`:3197–3199 if cand.is_empty() && group.members.is_empty()`).
+These define exactly what it.2 currently spares. Then sweep every
+recursive `.ail`/`.ail.json` under `examples/` NOT in
+`/tmp/it3_class_a.txt`:
+
+Run:
+```
+for f in $(grep -rl -E '\(fn ' examples/ | grep -vFf /tmp/it3_class_a.txt); do
+  cargo run -q -p ail -- check "$f" >/dev/null 2>&1 && echo "CLEAN $f" || echo "ERR   $f"
+done | tee /tmp/it3_sweep.txt
+```
+Then, for each `CLEAN` fixture containing a self-recursive fn,
+classify by inspection against the two exemptions: a fixture that
+checks clean *only* because (cand is empty: recurses on a
+primitive/no-ADT param) OR (the rec call is `tail`-marked) is
+class-(b)/(a). Produce `/tmp/it3_migration_set.tsv` with columns:
+`stem  class(a|b|c)  migration(loop|plaincall|already-loop)
+runnable(main|checkonly)`. Recon-verified seeds: `bench_tree_walk`
+(`fn build_tree`, class-b pure, no tail-app), `bench_latency_explicit`
+(`build_tree` class-b + tail-app sites class-a). Class-(c) =
+`rc_pin_recurse_implicit`, `rc_let_alias_implicit_param` (recon
+items 1c).
+
+- [ ] **Step 1.4: Capture the behavioural oracle.**
+
+```
+mkdir -p bench/it3-oracle
+while IFS=$'\t' read stem class mig run; do
+  if [ "$run" = main ]; then
+    cargo run -q -p ail -- run "examples/$stem" > "bench/it3-oracle/$stem.out" 2>&1
+  else
+    cargo run -q -p ail -- check "examples/$stem" > "bench/it3-oracle/$stem.out" 2>&1
+  fi
+done < /tmp/it3_migration_set.tsv
+cp /tmp/it3_migration_set.tsv bench/it3-oracle/MANIFEST.tsv
+```
+
+- [ ] **Step 1.5: Map existing-test fallout.**
+
+Run: `grep -rln -E '$(paste -sd"|" <(cut -f1 /tmp/it3_migration_set.tsv))' crates/*/tests crates/*/src bench 2>/dev/null`
+Record, per migrated fixture, which e2e/round-trip/bench/IR-snapshot
+test references it (these are the primary oracle per DD-1; they must
+stay green across migration). Also list the tail-app-specific tests
+recon named for deletion: `prose` `:1486–1494 app_tail_renders_*`,
+`:2050 binop_with_tail_flag_*`, `:2177 not_with_tail_flag_*`;
+`spec_drift::spec_mentions_tail_variants`; any
+`tail_call_in_tail_position_is_accepted` /
+`iter14e_*musttail*` e2e.
+
+- [ ] **Step 1.6: Gate.**
+
+Expected: `bench/it3-oracle/MANIFEST.tsv` non-empty; every listed
+fixture has a `.out`; `/tmp/it3_migration_set.tsv` classifies every
+recursive corpus fixture. No code changed.
+
+---
+
+## Task 2: Migrate the corpus (tail-app field still present)
+
+**Files:** every `examples/*.ail` in `MANIFEST.tsv` with
+`migration ∈ {loop, plaincall}`.
+
+- [ ] **Step 2.1: Migrate `plaincall` fixtures.**
+
+For each `migration=plaincall` stem (structurally-decreasing
+recursion that only carried a redundant `tail-app` marker, e.g.
+`list_map_poly`, `sort`, `std_list`,
+`fieldtest/floats_2_average_int_list`): replace `(tail-app f …)`
+with `(app f …)` (drop the marker only — the recursion is already
+structural; it.2's checker will verify it total once the grandfather
+is irrelevant). One stem at a time:
+
+Run (per stem): `cargo run -q -p ail -- run examples/<stem> | diff - bench/it3-oracle/<stem>.out`
+(or `ail check` for check-only). Expected: empty diff (byte-identical).
+
+- [ ] **Step 2.2: Migrate `loop` fixtures.**
+
+For each `migration=loop` stem (accumulator/counter recursion:
+`bench_compute_collatz`, `bench_compute_intsum`,
+`bench_latency_explicit/_implicit`, `bench_list_sum*`,
+`rc_tail_sum_explicit_leak`, `mut_counter`, `mut_sum_floats`,
+`fieldtest/floats_1_newton_sqrt`, `fieldtest/forma_1_factorial`,
+`bench_closure_chain`, `bench_hof_pipeline`, `bench_mono_dispatch`,
+`ct_1_ordering_signum`, `rc_drop_iterative_long_list`,
+`test_mono_recursive_fn_bug`, the class-b `build_tree` fixtures,
+class-c `rc_pin_recurse_implicit`/`rc_let_alias_implicit_param`):
+rewrite the recursive helper as a `(loop ((var <p> <ty> <init>)…)
+<body-with-recur>)`. The accumulator/counter params become loop
+binders; the terminal `return`-value path becomes the non-`recur`
+exit; the recursive `(tail-app f a b)` / `(app f a b)` becomes
+`(recur a b)`. Preserve the function's public signature and add
+`!Diverge` to its effect row (loop-bearing ⇒ Diverge, per it.2;
+mirror the it.1 `loop_counter.ail` shape + the it.2-migrated
+`loop_needs_diverge.ail`). One stem at a time, each immediately
+gated:
+
+Run (per stem): `cargo run -q -p ail -- check examples/<stem>` →
+Expected: clean (the loop form passes it.2's checker; `!Diverge`
+declared).
+Run (per stem): `cargo run -q -p ail -- run examples/<stem> | diff - bench/it3-oracle/<stem>.out`
+→ Expected: empty diff. (For RC fixtures the e2e RC==GC guard is the
+real oracle — see 2.4.)
+
+- [ ] **Step 2.3: it.1 loop fixtures — confirm unaffected.**
+
+`loop_counter.ail`, `loop_smoke.ail`, `loop_nested_in_lambda.ail`,
+`loop_in_lambda_e2e.ail` have no `tail-app`; migration does not
+touch them. Run their e2e (`loop_counter`→55,
+`loop_in_lambda`→49) — Expected: still green (sanity).
+
+- [ ] **Step 2.4: Workspace gate (field still present).**
+
+Run: `cargo test --workspace 2>&1 | tail -3`
+Expected: green. Round-trip auto-rechecks every migrated `.ail`
+(globs `examples/*.ail`). The two RC fixtures' RC==GC e2e guards
+(`e2e.rs` `rc_pin_recurse_implicit`/`rc_let_alias_implicit_param`)
+stay green (the regression is in the unchanged `pin`/`pin_aliased`
+bodies; only the driver became a loop). If a bench fixture's e2e
+stdout pin moved, that is a migration error — fix the migration to
+restore byte-identical output, do NOT edit the pin.
+
+---
+
+## Task 3: (folded into Task 2 gating — no separate task)
+
+> Migration correctness is proven by Task 2.4 (green with the
+> exemptions still present) followed by Task 4 (green with the
+> exemptions removed). No standalone task; this header is kept so
+> the numbering matches the journal's task log.
+
+---
+
+## Task 4: Remove the it.2 transitional exemptions (completeness gate)
+
+**Files:** `crates/ailang-check/src/lib.rs`,
+`crates/ailang-check/tests/no_tail_grandfather_pin.rs` (create).
+
+- [ ] **Step 4.1: RED — the exemption is gone.**
+
+Create `crates/ailang-check/tests/no_tail_grandfather_pin.rs`
+(harness copied verbatim from `structural_recursion_pin.rs`):
+
+```rust
+#[test]
+fn tail_marked_non_structural_is_now_rejected() {
+    // A tail-marked non-structural self-call must NO LONGER be
+    // grandfathered once it.3 removes the exemption.
+    assert!(
+        check_fixture("test_non_structural_recursion.ail.json")
+            .contains(&"non-structural-recursion".to_string()));
+}
+```
+(Reuse the it.2 negative fixture; if it was tail-marked to exercise
+the grandfather, this pin asserts the grandfather is dead. If the
+it.2 fixture is not tail-marked, add a tail-marked sibling
+`examples/test_tail_marked_non_structural.ail.json` and inventory
+it in `carve_out_inventory.rs` EXPECTED 20→21.)
+
+Run: `cargo test --workspace -p ailang-check tail_marked_non_structural_is_now_rejected`
+Expected: PASS already if fixture untail-marked; FAIL (still
+grandfathered) if tail-marked — driving the removal.
+
+- [ ] **Step 4.2: Delete the `tail==false` grandfather.**
+
+In `verify_structural_recursion`'s rec-call collection
+(recon `lib.rs:3026–3037`, the `if !*tail {` guard at `:3027`):
+collect the recursive call **regardless of `tail`**. Delete the
+guard; the comment blocks `:2919–2927,3007–3014,3260–3262`
+referencing the grandfather are removed/re-scoped.
+
+- [ ] **Step 4.3: Delete the no-ADT-candidate skip.**
+
+Recon `lib.rs:3197–3199`: delete
+`if cand.is_empty() && group.members.is_empty() { return Ok(()) }`
+and its rationale comment `:3183–3196`. A no-candidate counter
+recursion now reaches the `guarded` verdict and emits
+`NonStructuralRecursion`. The only legitimate early-OKs that remain
+are `calls.is_empty()` (`:3215`) and `self_clear` (`:3247`).
+
+- [ ] **Step 4.4: GREEN — the completeness gate (DD-3).**
+
+Run: `cargo test --workspace 2>&1 | tail -3`
+Expected: **all green.** This is the proof Task 2 migrated the
+entire set. If ANY fixture now fires `non-structural-recursion`,
+that fixture was not fully migrated in Task 2 — fix it in Task 2's
+migration (re-open 2.1/2.2 for that stem), NOT by restoring the
+exemption. Re-run until green with zero exemptions.
+
+---
+
+## Task 5: Remove the tail-app/tail-do machinery + 18g.1 husk-dec
+
+**Files:** `ast.rs`, `parse.rs`, `print.rs`, `prose/lib.rs`,
+`check/lib.rs`, `codegen/lib.rs`, `codegen/match_lower.rs`.
+
+- [ ] **Step 5.1: Delete the AST fields (DD-5).**
+
+`ast.rs`: remove `Term::App.tail` (`:406–407`) + `Term::Do.tail`
+(`:445–446`) + their `#[serde]` attrs. **Keep `is_false`**; only
+delete its two `tail` uses; re-scope its doc-comment
+(`:908–912`) to mention only `WorkspaceDef.drop_iterative`. Fix
+serde-roundtrip test ctors (`:974–1006`) that pass `tail:`.
+
+- [ ] **Step 5.2: Build-driven removal sweep.**
+
+Run: `cargo build --workspace 2>&1 | grep -E "error|tail" | head -60`
+Every error is a `tail` read/construct site. Fix each by deleting
+the `tail` handling, driven off the compiler (authoritative over
+recon line numbers):
+- `parse.rs`: delete `parse_tail_app`/`parse_tail_do`, the
+  `"tail-app"`/`"tail-do"` dispatch + keyword-list strings, the
+  EBNF doc lines; collapse `parse_app_body`/`parse_do_body`'s
+  `tail` param.
+- `print.rs`: `Term::App`/`Term::Do` arms emit only `(app `/`(do `.
+- `prose/lib.rs`: `as_binop`/`as_unary_not` drop the `tail` guard;
+  render App/Do drop the `"tail "` emit; subst App/Do drop
+  `tail: *tail`. (Free-var counter arms use `..` — no change.)
+- `check/lib.rs`: delete `CheckError::TailCallNotInTailPosition` +
+  its `code()` arm (no `ctx()` arm exists — verify); in
+  `verify_tail_positions` delete the tail-app arms
+  (`Term::App`/`Term::Do` `if *tail && !is_tail` checks) but **keep
+  the function, the recursive walk skeleton, the `Term::Loop`/
+  `Term::Recur` arms, and `verify_loop_body`** (they are entangled
+  mutual recursion — `verify_loop_body` calls back into
+  `verify_tail_positions` at 7 sites; only the tail-app *arms* go).
+
+- [ ] **Step 5.3: Delete the 18g.1 husk-dec (DD-4).**
+
+`match_lower.rs:658–736`: the `arm_body_is_tail_call =
+matches!(&arm.body, Term::App{tail:true,..}|Term::Do{tail:true,..})`
+gate (`:697–704`) no longer compiles. Delete the entire 18g.1
+pre-tail-call shallow-dec block (recon: it is wholly tail-call
+specific, no recur analogue). Also delete the now-dead `musttail`
+lowering: `emit_call` `tail` param + `:2427–2431` ret-block,
+`emit_indirect_call` `:2508–2512`, `lower_effect_op` `:2627`
+`"tail call"` + `:2650–2653`, `lower_app`'s `tail` param threading.
+
+- [ ] **Step 5.4: Build + functional GREEN.**
+
+Run: `cargo build --workspace` → Expected: clean.
+Run: `cargo test --workspace 2>&1 | tail -3` → Expected: all green.
+
+- [ ] **Step 5.5: RC-RSS gate (DD-4 — the load-bearing risk).**
+
+Run the RC-RSS / 18f.2 tail-latency bench pins (the ones
+`match_lower.rs:674–677` cited):
+Run: `bash bench/run.sh 2>&1 | tail -20` (or the specific RC-RSS
+harness; identify it from `match_lower.rs:674–677`'s comment +
+`bench/`'s RC-RSS script). Compare against `bench/baseline*`.
+Expected: RC-RSS within the established noise envelope (no RSS
+regression on the migrated accumulators — loops strand no husk).
+
+- [ ] **Step 5b (CONDITIONAL — only if 5.5 RED): owned-binder
+  drop-on-recur.**
+
+If 5.5 shows an RC-RSS regression, it.1 loop codegen is not dropping
+superseded owned binder values across the `recur` back-edge. Add
+that drop: in the `Term::Recur` lowering (`codegen/lib.rs:1979–1996`)
+/ the loop-header phi machinery, before the back-edge `br`, emit an
+RC dec for each loop binder whose old value is owned and is being
+replaced by the recur arg (mirror the husk-dec shape 18g.1 used, but
+keyed on loop-binder ownership, not `tail`). RED test: the failing
+RC-RSS pin from 5.5. GREEN: 5.5 within envelope. (This is the
+loop-side of the seam the spec wrongly claimed it.1 fully shipped —
+in scope for it.3 per the corrected spec §Codegen-rework.)
+
+---
+
+## Task 6: DESIGN.md + form_a.md + drift lockstep
+
+**Files:** `docs/DESIGN.md`, `crates/ailang-core/specs/form_a.md`,
+`design_schema_drift.rs`, `spec_drift.rs`, `schema_coverage.rs`.
+
+- [ ] **Step 6.1: DESIGN.md.**
+
+Decision 8 (`:709–747+`): rewrite as a *superseded tombstone* —
+keep the heading, replace the body with "Superseded by the
+iteration-discipline milestone (2026-05-15): explicit tail calls
+were retired in favour of structural recursion (total by
+construction under Decision 10) + named `loop`/`recur`. See
+`docs/specs/2026-05-15-iteration-discipline.md`." EBNF block
+`:552–565`: remove `tail-app-term`/`tail-do-term` productions.
+§"Data model" `:2357–2359` (`"app"` tail jsonc + comment),
+`:2373–2375` (`"do"`), `:2452–2467` (the it.1/it.2 transitional
+paragraph's tail-app/tail-do + grandfather/retire sentences —
+reword to "retired in it.3"). **Decision 3 `:163–176` is NOT
+touched** (it.2 payload; the corrected spec struck the
+"remove Decision-3 Diverge line" clause).
+
+- [ ] **Step 6.2: form_a.md.**
+
+Remove tail grammar `:268,270`; tail prose `:295–298,378–381,
+405–407`; the §4 "Tail-recursive sum" exhibit `:508–539` (incl.
+`:527 (tail-app sum_acc …)`) — replace §4 with a `(loop …)`/`recur`
+worked example (mirror an it.1 loop fixture). Keep loop/recur
+grammar `:287–288,327–341`.
+
+- [ ] **Step 6.3: Drift/spec/coverage lockstep.**
+
+`design_schema_drift.rs:53–60,87–94`: drop `tail:false` from the
+App/Do ctors. `spec_drift.rs:30–37,64–69`: drop `tail:false`;
+**delete `spec_mentions_tail_variants` (`:331–337`)** (it asserts
+the form_a spec contains `tail-app`/`tail-do` — now false by
+design). `schema_coverage.rs`: no `tail` tag exists; verify
+`TermLoop`/`TermRecur` anchors untouched.
+
+Run: `cargo test --workspace -p ailang-core design_schema_drift spec_drift schema_coverage`
+Expected: green; `loop`/`recur` anchors present, zero `tail`
+anchors.
+
+- [ ] **Step 6.4: Delete the tail-app-specific tests (Task 1.5 list).**
+
+Delete `prose` `app_tail_renders_with_keyword`
+(`:1486–1494`), `binop_with_tail_flag_keeps_prefix_form` (`:2050`),
+`not_with_tail_flag_keeps_prefix_form` (`:2177`); any
+`tail_call_in_tail_position_is_accepted` /
+`tail_call_in_non_tail_position_is_rejected` (the
+`TailCallNotInTailPosition` pins — the diagnostic is gone); the
+`iter14e_*musttail*` e2e. Each deletion is justified: the behaviour
+it pinned was deliberately removed.
+
+Run: `cargo test --workspace 2>&1 | tail -3` → Expected: all green.
+
+---
+
+## Task 7: Acceptance gate
+
+**Files:** none (verification only).
+
+- [ ] **Step 7.1: No exemption remains (spec it.3 acceptance).**
+
+Run: `grep -n "if !\*tail\|cand.is_empty() && group" crates/ailang-check/src/lib.rs || echo "NONE — exemptions gone"`
+Expected: `NONE`. The `tail==false` grandfather and the
+no-ADT-candidate skip are gone.
+
+- [ ] **Step 7.2: No tail-app concept remains.**
+
+Run: `grep -rn "tail-app\|tail-do\|TailCallNotInTailPosition\|musttail\|\.tail\b" crates/ --include=*.rs | grep -v "block_terminated\|loop\|recur\|drop_iterative" | head`
+Expected: empty (or only unrelated `.tail` like iterator methods —
+inspect each; zero AILang-tail-call references).
+Run: `grep -rl -E '\(tail-app|\(tail-do' examples/` → Expected: empty.
+
+- [ ] **Step 7.3: Behavioural identity.**
+
+For every `MANIFEST.tsv` stem: re-run and diff against
+`bench/it3-oracle/<stem>.out`. Expected: every diff empty
+(byte-identical observable behaviour pre/post migration).
+
+- [ ] **Step 7.4: Full workspace + design-drift.**
+
+Run: `cargo test --workspace 2>&1 | tail -3` → Expected: all green.
+Run: `cargo build --workspace` → Expected: clean (no dead-code
+warnings from half-removed tail machinery).
+
+- [ ] **Step 7.5: Spec it.3 acceptance bullets, itemised.**
+
+Verify each: `Term::App.tail`/`Term::Do.tail`/both keywords/
+`musttail`/`verify_tail_positions` tail-app role/
+`TailCallNotInTailPosition`/Decision 8 all removed (7.2 + grep);
+`design_schema_drift` green with `loop`/`recur` anchors and no
+`tail` anchors (6.3); every migration-set fixture `ail check` clean
++ `ail run` byte-identical (7.3); no grandfather/no-candidate skip
+(7.1); `cargo test --workspace` green (7.4). Note for the
+milestone-close `audit`: bench may need re-ratification if
+loop-header codegen diverged from the retired `musttail` (5.5
+result + any 5b remediation is the evidence the audit consumes).
+
+---
+
+## Self-review (planner Step 5)
+
+1. **Spec coverage.** §Components it.3 §Remove → T5 + T6.1/6.2;
+   §Codegen-rework (incl. the corrected 18g.1/RC-RSS contingency)
+   → T5.3/5.5/5b; §Corpus-migration (full corrected set) → T1
+   (enumeration+oracle) + T2; the two exemptions → T4; Decision-8
+   tombstone + EBNF + §Data-model + form_a.md + drift → T6;
+   §Acceptance it.3 (incl. "no grandfather/no-candidate skip
+   remains") → T7. Decision 3 explicitly NOT touched (corrected
+   spec). Every it.3 spec clause has a task.
+2. **Placeholder scan.** No "TBD/TODO/implement later/similar to/
+   add appropriate". The build-driven removal (T5.2) is an exact
+   method (compiler enumerates sites), not a placeholder — same
+   device the planner memory mandates over recon line numbers. Per
+   memory `plan-pseudo-vs-reality`: no prose round-trip asserting
+   AST-equality is scripted; no `diagnostic.rs` doc-list claim
+   (T5.2 says delete the `code()` arm, explicitly notes no `ctx()`
+   arm exists). Recon lines flagged drift-prone in the DD preamble.
+3. **Type/name consistency.** `Term::App.tail`/`Term::Do.tail`,
+   `is_false` (kept), `verify_tail_positions`/`verify_loop_body`
+   (kept, arms deleted), `TailCallNotInTailPosition` (deleted),
+   18g.1/`arm_body_is_tail_call`, `bench/it3-oracle/`, the
+   exemption greps — consistent across tasks + files section.
+4. **Step granularity.** Each step is one action (one grep, one
+   fixture migration with its gate, one symbol-class removal). The
+   per-stem migration loops in T2 are explicitly "one stem at a
+   time, each immediately gated".
+5. **No commit steps.** None. Working tree only; Boss commits the
+   whole it.3 diff at iter end.
+
+Recorded risk (named, decision rule — not a placeholder): the
+class-(b) enumeration (T1.3) is the one step that cannot be fully
+pre-scripted (the spec + it.2 journal §1 explicitly delegate it to
+a live sweep). The method is exact (read the two exemptions, sweep,
+classify by the shape they spare). If the sweep reveals a fixture
+shape that is neither cleanly loop-able nor structural (a genuine
+non-structural recursion with no natural loop form), that is a
+real finding → it surfaces as a Task-2 BLOCKED to the Boss with the
+fixture named, not a silent reshape (memory: don't adapt fixtures
+to dodge — but here the fixture SHOULD become a loop; a fixture
+that resists looping is a spec-signal worth surfacing).