# it.3 — retire tail-app/tail-do + corpus migration — Implementation Plan

> **Parent spec:** `docs/specs/0031-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/0031-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).