AILang/docs/specs/0032-iteration-discipline-revert.md

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.