iter remove-mut-var-assign.1: atomic removal of mut/var/assign

mut/var/assign removed from AILang entirely and atomically. Deleted:
Term::Mut/Term::Assign/struct MutVar; the three Form-A keywords +
parse_mut/parse_assign + grammar EBNF; the 4 mut CheckError variants;
the mut_scope_stack synth threading (param dropped from synth + every
internal/external/test caller); the two lower_term arms; and every
exhaustive no-_ Term::Mut/Term::Assign match arm across 17 source
files — cut in lockstep with DESIGN.md, fixtures, the drift trio,
carve-out and roadmap so the schema is honest at every commit. No
catch-all wildcard introduced (verified). loop/recur + let/if are
the surviving forms.

The shared codegen alloca machinery survives (loop reuses it):
mut_var_allocas renamed binder_allocas (representation-only, loop
codegen byte-identical) and the shared Term::Lam escape guard
simplified to !loop_stack.is_empty() with the loop half
(LoopBinderCapturedByLambda) byte-equivalent. Feature-acceptance
applied inverted: the removed feature fails clause 2 (redundant)
and clause 3 (IS the iterated-mutable-state bug class).

Behaviour preservation is executable: mut_counter/mut_sum_floats
still print 55 after the faithful let/if rewrite. The removal is
made executable by the new mut_removed_pin.rs (4 must-fail pins).
Independent verification: cargo test --workspace 605/0, zero
residual mut symbols in any crate source, loop/recur non-regression
all green (55 / 500000500000 / infinite-compiles / the
lambda_capturing_loop_binder pin), roundtrip_cli PASS.

One DONE_WITH_CONCERNS: a 4th recurrence of the recon-undercount
class (in-source mod tests + a drift-pin fn + 5 orphaned mut
.ail.json carve-outs + a non-enumerated E0599); all resolved within
implementer remit, no behaviour change. Milestone-close audit then
fieldtest remain.

spec docs/specs/2026-05-18-remove-mut-var-assign.md (grounding PASS)
plan docs/plans/remove-mut-var-assign.1.md

crates/ail/src/main.rs

@@ -1513,37 +1513,6 @@ fn walk_term(
             walk_term(source, out, builtins, scope);
             walk_term(body, out, builtins, scope);
         }
-        // Iter mut.1: each `var` introduces a new lexical binding;
-        // its `init` is in the outer scope plus already-declared
-        // vars; the body sees all of them. Mirrors `Term::Lam`'s
-        // newly-bound roll-back convention.
-        Term::Mut { vars, body } => {
-            let mut newly = Vec::new();
-            for v in vars {
-                walk_term(&v.init, out, builtins, scope);
-                if scope.insert(v.name.clone()) {
-                    newly.push(v.name.clone());
-                }
-            }
-            walk_term(body, out, builtins, scope);
-            for n in newly {
-                scope.remove(&n);
-            }
-        }
-        // Iter mut.1: the `value` is walked; the assigned `name` is
-        // a use of an in-scope mut-var. If the user wrote an
-        // out-of-scope assign, it surfaces as an unknown identifier
-        // in the dep walk, which is acceptable for the CLI's
-        // dependency view (typecheck would already have rejected).
-        Term::Assign { name, value } => {
-            if !name.contains('.')
-                && !scope.contains(name)
-                && !builtins.contains(name.as_str())
-            {
-                out.insert(name.clone());
-            }
-            walk_term(value, out, builtins, scope);
-        }
         Term::Loop { binders, body } => {
             let mut newly = Vec::new();
             for b in binders {
@@ -2765,44 +2734,6 @@ fn rewrite_def(
                     changed,
                 );
             }
-            // Iter mut.1: rewrite types embedded in each `MutVar.ty`
-            // (via `rewrite_type` — mut-vars carry full Type
-            // annotations) and recurse into each var's `init` and
-            // the block's body. `Term::Assign` has no embedded type.
-            Term::Mut { vars, body } => {
-                for v in vars {
-                    rewrite_type(
-                        &mut v.ty,
-                        owning_module,
-                        local_types,
-                        import_names,
-                        changed,
-                    );
-                    rewrite_term(
-                        &mut v.init,
-                        owning_module,
-                        local_types,
-                        import_names,
-                        changed,
-                    );
-                }
-                rewrite_term(
-                    body,
-                    owning_module,
-                    local_types,
-                    import_names,
-                    changed,
-                );
-            }
-            Term::Assign { value, .. } => {
-                rewrite_term(
-                    value,
-                    owning_module,
-                    local_types,
-                    import_names,
-                    changed,
-                );
-            }
             Term::Loop { binders, body } => {
                 for b in binders {
                     rewrite_type(

crates/ail/tests/codegen_import_map_fallback_pin.rs

@@ -91,20 +91,9 @@ fn synthesised_print_uses_user_module_show_via_fallback() {
             Term::ReuseAs { source, body } => {
                 contains_xmod_show_var(source) || contains_xmod_show_var(body)
             }
-            // Iter mut.1: a `Term::Mut` cannot itself host a
-            // `show_user_adt.show__<T>` reference (its body is a
-            // mut-block, not a synthesised polymorphic call), but
-            // recurse defensively so any nested reference inside a
-            // var init / body / assign-value still surfaces.
-            Term::Mut { vars, body } => {
-                vars.iter().any(|v| contains_xmod_show_var(&v.init))
-                    || contains_xmod_show_var(body)
-            }
-            Term::Assign { value, .. } => contains_xmod_show_var(value),
             // loop-recur iter 1: a `Term::Loop` cannot itself host a
             // synthesised cross-module reference, but recurse
-            // defensively through binder inits / body / recur args,
-            // mirroring the `Term::Mut` arm above.
+            // defensively through binder inits / body / recur args.
             Term::Loop { binders, body } => {
                 binders.iter().any(|b| contains_xmod_show_var(&b.init))
                     || contains_xmod_show_var(body)

crates/ail/tests/ct1_check_cli.rs

@@ -187,48 +187,23 @@ fn check_ordering_match_post_migration_is_clean() {
     );
 }
 
-/// Property (RED — fieldtest mut-local F2): in non-JSON (human) mode,
-/// the human-stderr formatter prepends the diagnostic code exactly once
-/// as the canonical `[code]` bracket prefix (the cli-diag-human format).
-/// The four mut-local `CheckError` variants
-/// (`mut-assign-out-of-scope`, `assign-type-mismatch`,
-/// `mut-var-unsupported-type`, `mut-var-captured-by-lambda`) must NOT
-/// also embed `[code] ` inside their `thiserror` Display body, which
-/// would render the bracketed code TWICE in the user-visible stderr
-/// line (`error: [code] fn: [code] message`).
+/// Property: in non-JSON (human) mode, the human-stderr formatter
+/// prepends the diagnostic code exactly once as the canonical
+/// `[code]` bracket prefix (the cli-diag-human format). The
+/// `loop-binder-captured-by-lambda` `CheckError` Display body must
+/// NOT also embed `[code] ` inside its `thiserror` Display body,
+/// which would render the bracketed code TWICE in the user-visible
+/// stderr line (`error: [code] fn: [code] message`).
 ///
 /// This pins the *observable* doubling on the real CLI human path
 /// (`crates/ail/src/main.rs` non-JSON `Cmd::Check` arm), not the raw
-/// Display string of one variant in isolation: it counts occurrences
-/// of the literal `[<code>]` token in the rendered stderr and requires
-/// exactly one. Drops to GREEN once the four Display bodies shed their
-/// leading `[<code>] ` prefix (the formatter's prefix then supplies it
-/// once). The non-mut variants are unaffected because they never
-/// embedded the bracket.
+/// Display string of the variant in isolation: it counts occurrences
+/// of the literal `[<code>]` token in the rendered stderr and
+/// requires exactly one (the formatter supplies it; the Display body
+/// must not also embed it).
 #[test]
-fn check_human_mode_renders_mut_diagnostic_code_exactly_once() {
-    // (fixture filename, kebab diagnostic code) for the four mut-local
-    // negative fixtures shipped by the mut-local milestone.
+fn check_human_mode_renders_loop_binder_diagnostic_code_exactly_once() {
     let cases = [
-        (
-            "test_mut_assign_out_of_scope.ail.json",
-            "mut-assign-out-of-scope",
-        ),
-        (
-            "test_mut_assign_type_mismatch.ail.json",
-            "assign-type-mismatch",
-        ),
-        (
-            "test_mut_var_unsupported_type.ail.json",
-            "mut-var-unsupported-type",
-        ),
-        (
-            "test_mut_var_captured_by_lambda.ail.json",
-            "mut-var-captured-by-lambda",
-        ),
-        // Iter loop-recur.tidy: symmetric loop-binder-capture variant.
-        // Its Display body is likewise bracket-`[code]`-free so the
-        // human formatter supplies `[<code>]` exactly once.
         (
             "test_loop_binder_captured_by_lambda.ail.json",
             "loop-binder-captured-by-lambda",

crates/ail/tests/e2e.rs

@@ -2853,20 +2853,17 @@ fn str_clone_cross_realisation_uniform_abi() {
     assert_eq!(live, 0, "no leaked heap-Str slabs allowed; live={live}");
 }
 
-/// Iter mut.3: `examples/mut_counter.ail` exercises `Term::Mut` +
-/// `Term::Assign` codegen with an `Int` mut-var. The body
-/// `(mut (var sum Int 0) (assign sum (sum_helper 1 10 0)) sum)`
-/// stores the helper's result into `sum`'s alloca and prints the
-/// loaded value. End-to-end gate for the entry-block-hoist /
-/// store / load lowering.
+/// `examples/mut_counter.ail` sums 1..10 via a tail-recursive
+/// `sum_helper` and prints the result. Behaviour-preservation gate:
+/// the fixture's value assertion stays `55` after the let/if rewrite,
+/// proving the rewrite loses no expressivity.
 #[test]
 fn mut_counter_prints_55() {
     let stdout = build_and_run("mut_counter.ail");
     assert_eq!(stdout.trim(), "55", "mut_counter must print 55, got {stdout:?}");
 }
 
-/// Iter mut.3: Float twin of `mut_counter_prints_55`. The mut-var
-/// is `Float`, init is `0.0`, the recursive helper returns the
+/// Float twin of `mut_counter_prints_55`: `sum_helper` returns the
 /// sum 1.0+...+10.0 = 55.0. The polymorphic `print` routes through
 /// `Show Float.show` → `float_to_str`'s libc `%g` formatter, which
 /// strips the trailing `.0` — so the canonical stdout for Float