# Iteration-discipline revert — Design Spec

**Date:** 2026-05-16
**Status:** Draft — awaiting user spec review
**Authors:** Brummel (orchestrator) + Claude

## Goal

Back the *Iteration-discipline* milestone out of the working language
and restore the pre-milestone iteration story, by a single **forward**
iteration (`main` is sacrosanct — no `git reset`/`git revert` of the
shipped commits `96db54d`/`a4be1e5`).

Why this is a milestone, not a tidy iteration: the milestone being
removed was an *identity-level* change (a new AST node family, a new
checker pass, a new effect, DESIGN.md Decision-3 prose). Reverting it
is an equally identity-level decision about what AILang's iteration
story *is*, and it touches DESIGN.md invariants. It earns a spec.

Root cause being corrected (recorded so a future reader does not
re-derive the same mistake):

- The milestone was scoped from fieldtest finding **F1**
  (`docs/specs/0030-fieldtest-mut-local.md`), which was tagged
  `[friction]` and whose *own* summary table named the honest minimal
  action: "tighten DESIGN.md to name the gap — less work, more
  honest". It was instead escalated into "retire `tail-app`,
  recursion is total-by-construction, add `Diverge`".
- That thesis recognised exactly **one** total-by-construction
  scheme (ADT-structural over an acyclic ADT). The it.3 corpus sweep
  proved it incomplete: `build(d: Int) = if d==0 then Leaf else
  Node(1, build(d-1), build(d-1))` — the single most LLM-natural
  tree-builder — is neither ADT-structural nor `loop`/`recur`-able,
  so the milestone *as specified* made a trivially-total,
  maximally-natural function inexpressible (it.3 BLOCKED).
- The only in-thesis escape (A1 / it.2b — Int-bounded recursion as a
  second total class) requires conceding the language's **first**
  documented-but-unenforced totality precondition (`build(-1)`
  diverges silently; Decision 4 keeps refinements opaque with no SMT,
  so `p >= 0` is unenforceable today *by construction*). That is a
  dilution of a purity pillar the user personally co-designed.
- `loop`/`recur` (it.1) was never run through the feature-acceptance
  gate for LLM-naturalness in its own right; it rode in on the
  thesis. it.2's `NonStructuralRecursion` checker is **not** a stable
  additive stopping point: it rejects bare non-structural recursion
  while *grandfathering* `tail`-marked calls, i.e. it half-enforces a
  dichotomy the language only commits to once the *destructive* it.3
  completes. "Mechanically additive" (nothing deleted) is not the
  same as "a coherent end-state".

User decision (2026-05-16): **full revert to the pre-milestone state.**
Both it.1 and it.2 come out. `tail-app` / structural recursion remain
the iteration mechanism exactly as before `9973546`. The genuine
iteration-totality ambition is *not* abandoned — it is re-sequenced
behind a future `Nat`/refinement-types milestone, because doing it
*properly* (enforced non-negativity) requires type machinery the
language has not built. Stateful-islands (P2, the real descendant of
the user's `~/sma_factory.myc` streaming analysis) is untouched: that
analysis motivates the *streaming* milestone, not the iteration story.

The revert is gate-satisfied by **subtraction**: the milestone fails
feature-acceptance clause 3 (via A1); the revert restores the
pre-milestone state, which already passed all three clauses. The only
*addition* is a DESIGN.md documentation note for F1/F4 — and the
criterion states verbatim that "a documentation note is not a
reshape", so it introduces no bug class and asserts nothing at the
typecheck level.

## Architecture

One forward iteration. The target tree state for the
**iteration/checker/codegen/AST/surface/fixture** surface is the
state at commit `1ff7e81` (the last commit before milestone-start
`9973546`). The revert is **surgical, not a range revert**, because
three hunks landed *with* the milestone but are independently sound
and are *kept*:

| Landed in | Hunk | Disposition |
|---|---|---|
| `9973546` | DESIGN.md feature-acceptance **clause 3** | **KEEP** — independently sound; it is the very tool that diagnosed the over-escalation. |
| `9973546` | `skills/brainstorm/SKILL.md` Step-4 clause-3 wording | **KEEP** — part of the clause-3 strengthening (see §Components for the worked-example caveat). |
| `9973546` | `docs/roadmap.md` Iteration-discipline milestone entry | **REVERT** — replaced by a deferred future entry. |
| `4079f09` | `docs/roadmap.md` F3 (zero-arg `(app f)`) P2 todo | **KEEP** — independent of the iteration story; stays a P2 todo. |

`git revert 9973546..a4be1e5` is therefore **forbidden twice over**:
(1) it is a history-rewind class operation on `main`; (2) it would
also delete clause 3 and the F3 todo. The revert is reconstructed
forward, file by file, against the `1ff7e81` tree as the reference,
and committed as new `main` history.

## Components

The exact removal / restoration / addition surface. The planner turns
this into bite-sized tasks; the implementer executes against
`1ff7e81` as the byte reference (`git show 1ff7e81:<path>` is the
oracle for every *restored* file).

### Remove (it.1 + it.2 production surface)

- **AST (`crates/ailang-core/src/ast.rs`).** `Term::Loop { binders,
  body }`, `Term::Recur { args }`, `struct LoopBinder`, and their
  serde round-trip unit tests. Restore the `Term` enum and its serde
  to the `1ff7e81` shape.
- **Schema-drift / coverage anchors.**
  `crates/ailang-core/tests/design_schema_drift.rs`,
  `schema_coverage.rs`, `spec_drift.rs`,
  `crates/ailang-core/tests/carve_out_inventory.rs`: remove the
  `Term::Loop → "loop"` / `Term::Recur → "recur"` anchors and the
  it.2 carve-out additions; recompute the `EXPECTED` inventory count
  back to its `1ff7e81` value.
- **Surface (`crates/ailang-surface`).** `parse.rs`: `parse_loop` /
  `parse_recur`, the dispatch arms, the keyword-list entries, the
  EBNF block. `print.rs`: the `Term::Loop` / `Term::Recur` arms.
- **Prose (`crates/ailang-prose/src/lib.rs`).** The read + rebuild
  arms for `Term::Loop` / `Term::Recur`.
- **Form-A grammar (`crates/ailang-core/specs/form_a.md`).** The
  `loop` / `recur` grammar entries.
- **Check (`crates/ailang-check/src/lib.rs`).** `Term::Loop` typing,
  `Term::Recur` unification, the `loop_stack` threading,
  `verify_loop_body`; the **whole** `verify_structural_recursion`
  pass (it.2, ~772 lines) including `term_contains_loop`, the
  `Diverge` injection at the `FnDef`/lam-arrow/`LetRec` effect-
  reconciliation sites, the `tail==false` grandfather and the
  no-ADT-candidate skip. `verify_tail_positions` is restored to its
  pure pre-it.1 `tail-app` role (it.1 repurposed it to also enforce
  `recur`-in-tail-position; that addition is removed — the function
  itself stays, only the it.1 arms are deleted). Walker arms for
  `Term::Loop` / `Term::Recur` removed from `desugar.rs`, `lift.rs`,
  `mono.rs`, `linearity.rs`, `uniqueness.rs`, `reuse_shape.rs`,
  `pre_desugar_validation.rs`, `builtins.rs` (~25 sites, the it.1
  blast radius in reverse).
- **`CheckError` (`crates/ailang-check`).** Remove the five
  variants `RecurOutsideLoop`, `RecurArityMismatch`,
  `RecurTypeMismatch`, `RecurNotInTailPosition`,
  `NonStructuralRecursion`, including their `code()` arms **and their
  `ctx()` arms**. The `ctx()` removal is **not** uniform (the
  original draft wrongly said no `ctx()` arms exist — corrected here
  after Step-7.5 grounding): `RecurArityMismatch`,
  `RecurTypeMismatch`, and `NonStructuralRecursion` each carry a
  *dedicated* `ctx()` arm (`crates/ailang-check/src/lib.rs` ~870–878)
  which must be deleted; `RecurOutsideLoop` and
  `RecurNotInTailPosition` fall into the `_ =>` catch-all (`lib.rs`
  ~879) and need no `ctx()` edit. The diagnostic-code registry is
  `CheckError::code()` itself; the `//!` "Stable codes" doc-list in
  `crates/ailang-check/src/diagnostic.rs` ends at mq.3 and never
  gained `loop`/`recur`/`non-structural-recursion` entries (it.1
  already proved the "add codes to a doc-list" premise false — see
  project memory `feedback_plan_pseudo_vs_reality`), so there is
  **nothing in `diagnostic.rs` for the revert to touch**.
- **Codegen (`crates/ailang-codegen`).** `lib.rs`: the loop-header
  basic-block + per-binder `phi` lowering, the `Term::Recur`
  back-edge `br`, and the **new parallel `block_terminated` setter**
  it.1 added — the `block_terminated` seam returns to being solely
  tail-driven (`emit_call` / `emit_indirect_call` / `lower_effect_op`
  on `tail: true`), exactly as at `1ff7e81`. `escape.rs`: the
  `Term::Loop` / `Term::Recur` escape-walk arms. `lambda.rs`: the
  `loop_frames` save/restore. `crates/ail/src/main.rs`: any it.1
  loop wiring. `crates/ailang-core/src/workspace.rs`: it.1 additions.
- **CLI / e2e wiring.** `crates/ail/tests/e2e.rs`,
  `crates/ail/tests/codegen_import_map_fallback_pin.rs`,
  `crates/ailang-check/tests/loop_recur_pin.rs`,
  `crates/ailang-check/tests/structural_recursion_pin.rs`: the it.1
  and it.2 pin files are **deleted** (they pin the removed surface).

### DESIGN.md

> **Handling rule (forestalls the obvious failure mode).** DESIGN.md
> is edited **in place, hunk by hunk** — it is *never* wholesale-
> restored to `git show 1ff7e81:docs/DESIGN.md`, because the
> `1ff7e81` DESIGN.md does **not** contain clause 3 (clause 3 landed
> *with* the milestone in `9973546` and is explicitly KEPT). Only the
> two named hunks below are reverted, using `1ff7e81` as the
> *per-hunk* byte oracle for those hunks only.

- **Decision 3** restored to its pre-`9973546` placeholder wording
  (`Diverge` is nominal/wired-up-only, *not* "the real effect of
  `loop`-bearing code"). Use the Decision-3 section of
  `git show 1ff7e81:docs/DESIGN.md` as the per-hunk byte oracle —
  diff-and-apply that one section, do not touch the rest of the file.
- The §"Data model" `loop` / `recur` entries removed.
- **Decision 8** is *untouched* — it.3 never ran, so `tail-app` /
  Decision 8 are already exactly in their pre-milestone state.
- **Feature-acceptance criterion clause 3** is **kept** (the
  `9973546` DESIGN.md hunk for clause 3 stays). One caveat: the
  clause-3 *canonical worked example* added in `9973546` uses "the
  iteration story" (structural recursion + named `loop`/`recur`
  passing all three clauses) as its illustration. After the revert
  there is no `loop`/`recur` in the language, so any sentence that
  reads as "we *shipped* X" must be rephrased to "consider X" /
  hypothetical-illustration form. The example is retained as a
  *teaching* illustration of the criterion (it does not depend on the
  machinery existing); it is only de-claimed from "shipped" to
  "illustrative". This is the one prose edit inside the kept clause-3
  block; the brainstorm SKILL.md Step-4 wording that points at it
  needs the same de-claiming pass.
- **Add the F1/F4 note (the only net addition).** A short, honest
  paragraph in the DESIGN.md §"Local mutable state" / iteration
  vicinity: the accumulator-over-an-iteration shape from the
  mut-local motivation is *not* achievable by `mut` alone; until a
  future iteration-totality milestone (gated behind `Nat`/refinement
  types) lands, the canonical pattern for that shape is the
  tail-recursive accumulator-parameter helper, and
  `examples/mut_counter.ail` is the reference. Phrased explicitly as
  a documented idiom, **not** an enforced rule (gate-honest per the
  criterion's "a documentation note is not a reshape"). This
  discharges F1 and F4 by the fieldtester's own named minimal action.

### Fixtures

- **Delete** (it.1 / it.2 net-new): `examples/loop_counter.ail`,
  `examples/loop_in_lambda_e2e.ail`, `examples/loop_nested_in_lambda.ail`,
  `examples/loop_smoke.ail`, `examples/loop_needs_diverge.ail`,
  `examples/struct_rec_foldl_sum.ail`, `examples/struct_rec_list_len.ail`,
  `examples/struct_rec_sum_e2e.ail`, `examples/struct_rec_tree_forest.ail`,
  `examples/test_recur_arity_mismatch.ail.json`,
  `examples/test_recur_not_in_tail_position.ail.json`,
  `examples/test_recur_outside_loop.ail.json`,
  `examples/test_recur_type_mismatch.ail.json`,
  `examples/test_loop_missing_diverge.ail.json`,
  `examples/test_non_structural_recursion.ail.json`,
  `examples/test_mutual_cross_family.ail.json`.
  (The planner's recon re-derives the exact file set off
  `git diff --stat 1ff7e81 HEAD -- examples/`; this list is the
  spec's best enumeration, not a substitute for that diff.)
- **Restore** (pre-milestone fixtures that it.2 *modified* — must be
  reverted to content, not deleted): `examples/rc_pin_recurse_implicit.ail`,
  `examples/rc_let_alias_implicit_param.ail`. Byte oracle:
  `git show 1ff7e81:examples/<file>`. `examples/mut_counter.ail` /
  `examples/mut_sum_floats.ail` were *not* migrated by it.1/it.2
  (migration was the never-run it.3) — verify they are already at
  their `1ff7e81` content and leave them.
- **Delete** `bench/it3-oracle/` in its entirety (40 `.out` files +
  `MANIFEST.tsv`) — the it.3 Task-1 deliverable, dead weight once the
  milestone is reverted. Forward delete (the revert commit moves
  `main` forward; nothing is rewound).

### Working tree / docs hygiene

- Discard the uncommitted A1 amendment to
  `docs/specs/0031-iteration-discipline.md`
  (`git checkout -- docs/specs/0031-iteration-discipline.md`),
  then add a **superseded header** to that committed spec pointing to
  this one (specs are per-milestone historical records — superseded,
  not deleted). The it.1/it.2/it.3 plans under `docs/plans/` and the
  it.1/it.2/it.3 journals stay as historical record (append-only
  discipline; they record what happened).
- **Roadmap (`docs/roadmap.md`).** Remove the Iteration-discipline
  P1 milestone entry *and* the "blocking fork" section. Add one
  deferred entry: `[idea]`/`[milestone]` "Iteration-totality story —
  structural + Int-bounded total recursion with *enforced*
  non-negativity", `depends on:` a future `Nat`/refinement-types
  milestone, `context:` this spec + the it.3 journal (so the genuine
  ambition and *why it was deferred* are not lost). Stateful-islands
  and the F3 P2 todo are left exactly as they are.

## Data flow

After the revert the pipeline is byte-for-byte the `1ff7e81` path:

`.ail` → `ailang_surface::parse` → JSON-AST (no `Term::Loop` /
`Term::Recur` node exists) → `ailang-check`: typecheck → the
`verify_tail_positions` pass in its pre-it.1 `tail-app`-only role →
effect reconciliation **without** any `Diverge`-injection (no
guardedness pass at all) → desugar / lift / mono (walkers with no
Loop/Recur arms) → `ailang-codegen` (no loop-header path; the
`block_terminated` seam is solely `tail: true`-driven) → LLVM text →
`clang -O2`. There is no new back-edge class; the only iteration in
generated IR is tail-call / structural recursion exactly as before
the milestone.

## Error handling

No new diagnostics — the revert *removes* six `CheckError` variants
(five `Recur*` + `NonStructuralRecursion`), their `code()` arms, and
the three dedicated `ctx()` arms for `RecurArityMismatch` /
`RecurTypeMismatch` / `NonStructuralRecursion` (the other two
`Recur*` variants use the `ctx()` catch-all and need no edit — see
§Components/`CheckError` for the exact split). `UndeclaredEffect`
returns to its pre-milestone behaviour (no `Diverge` antecedent
path). `verify_tail_positions` emits exactly the
diagnostics it emitted at `1ff7e81` (the `tail-app` tail-position
checks). The schema-drift / diagnostic-code surface is validated by
the existing drift tests once they are reverted to their `1ff7e81`
anchor set.

## Testing strategy

- **Revert-completeness pins (RED → GREEN for the revert).**
  - `crates/ailang-core/tests/design_schema_drift.rs` passes with
    **no** `loop`/`recur` anchors and **with** the `1ff7e81` anchor
    set. This is the structural proof the AST/schema surface is fully
    reverted.
  - `structural_recursion_pin.rs` and `loop_recur_pin.rs` are
    *deleted*; their absence + a green `cargo test --workspace` is
    the proof the pinned surface is gone (no orphan references).
  - `carve_out_inventory` `EXPECTED` equals its `1ff7e81` value.
- **Behavioural-equivalence pins (the correctness gate).** Every
  example fixture that existed at `1ff7e81` and still exists must
  `ail check` and `ail run` to **byte-identical** stdout vs. its
  `1ff7e81` behaviour — in particular the two *restored* fixtures
  (`rc_pin_recurse_implicit.ail`, `rc_let_alias_implicit_param.ail`)
  and the RC-regression guards they exist for. This proves the
  revert reintroduced no behavioural drift. Drive it off a corpus
  `ail check` / `ail run` sweep, diffing against
  `git show 1ff7e81:` behaviour (the planner scripts the exact
  comparison; the `bench/it3-oracle/` snapshots are *not* the oracle
  — they are deleted; `1ff7e81` is the oracle).
- **Doc-presence anchor.** A test (mirroring the existing DESIGN.md
  drift-anchor mechanism) asserts the F1/F4 note is present in
  DESIGN.md, so a future careless edit cannot silently drop the
  documented fallback the fieldtest finding required.
- **Full suite.** `cargo test --workspace` green. Milestone-close
  `audit` runs the three bench regression scripts; the baseline is
  expected **pristine** (the revert returns codegen to the
  `1ff7e81` path — any non-pristine result is a revert defect, not a
  ratifiable delta).

## Acceptance criteria

- `Term::Loop` / `Term::Recur` / `LoopBinder` / `verify_structural_
  recursion` / `term_contains_loop` / the `Diverge`-injection / the
  five `Recur*` + `NonStructuralRecursion` `CheckError` variants /
  the loop codegen path / the it.1 parallel `block_terminated`
  setter are all absent; `verify_tail_positions` is byte-equivalent
  to its `1ff7e81` role.
- `design_schema_drift.rs` green with the `1ff7e81` anchor set and
  no `loop`/`recur` anchors; `structural_recursion_pin.rs` /
  `loop_recur_pin.rs` deleted; `cargo test --workspace` green.
- DESIGN.md Decision 3 is back to its placeholder wording; the
  §"Data model" loop/recur entries are gone; Decision 8 is unchanged;
  feature-acceptance **clause 3 is retained**, with its worked
  example de-claimed from "shipped" to "illustrative" (and the
  matching brainstorm SKILL.md wording de-claimed in lockstep).
- The F1/F4 documentation note is present in DESIGN.md, phrased as a
  documented idiom (not an enforced rule), naming the tail-recursive
  accumulator-parameter fallback and `examples/mut_counter.ail`; a
  doc-presence test guards it.
- Every `1ff7e81`-era fixture `ail check` + `ail run` byte-identical
  to its `1ff7e81` behaviour; `rc_pin_recurse_implicit.ail` /
  `rc_let_alias_implicit_param.ail` restored to `1ff7e81` content;
  `bench/it3-oracle/` deleted.
- The uncommitted A1 spec amendment is discarded; the
  `2026-05-15-iteration-discipline.md` spec carries a superseded
  header pointing here; the it.1/it.2/it.3 journals and plans remain
  as historical record.
- `docs/roadmap.md`: the Iteration-discipline milestone entry and
  the blocking-fork section removed; one deferred entry added for the
  iteration-totality ambition, `depends on:` a future `Nat`/
  refinement milestone; Stateful-islands and the F3 P2 todo
  untouched.
- Milestone-close `audit`: bench baseline pristine (not ratified —
  pristine), drift review clean against the restored DESIGN.md.
- Net effect: AILang's iteration story is exactly the pre-`9973546`
  state (structural / tail recursion; `tail-app` intact), plus one
  honest documentation note, plus a retained-and-de-claimed
  feature-acceptance clause 3. The genuine total-Int-recursion
  ambition is preserved on the roadmap, correctly sequenced behind
  the type machinery it needs, not diluted to fit today.