feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on while/for (Refs #177)

Rebased reduction of the original Slice C' PR. The StmtAssign
clear-on-rewrite half is dropped — that work landed in #399 with a
strictly better `is_whole_place_write` predicate (whole-place writes
clear the move; sub-place writes still apply `check_use`).  This PR
keeps only the loop-soundness piece.

What lands:

  - `StmtWhile` / `StmtFor`: run cond+body once, snapshot state-fields,
    run cond+body a second time from the post-iter-1 state.  Any move
    the body didn't restore surfaces as UseAfterMove on the 2nd pass.
    State is restored to the iter-1-post snapshot for post-loop
    analysis (the loop may execute 0..N times — iter-1-post is the
    sound choice when iter-2 doesn't add new conflicts).

  - Pairs with #399's clear-on-rewrite to make legitimate re-init
    loops accept: iter 1 moves and reassigns, iter 2 sees the
    reassigned (cleared) state.

Three new fixtures pin the cases:

  - `slice_c_prime_loop_sound.affine` — counted loop, no moves: Ok
    (anti-regression against the 2-iter pass introducing false
    positives).
  - `slice_c_prime_loop_reinit_ok.affine` — move + immediate rebind:
    Ok (the #399 × Slice C' interaction).
  - `slice_c_prime_loop_move_persists.affine` — move without rebind:
    Error UseAfterMove (the soundness gain).

Suite: **335/335 green** (332 prior + 3 new).

Deferred-items comment at `lib/borrow.ml:1483` updated — loop-
soundness entry removed, only Polonius and captured-linears Slice D
remain.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

lib/borrow.ml

@@ -1444,11 +1444,58 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
       check_expr ctx state symbols rhs
     end
   | StmtWhile (cond, body) ->
+    (* CORE-01 pt3 Slice C' / #177 — loop soundness via 2-iteration.
+       A single body pass misses multi-iter conflicts: a move at iter
+       1 that the body never restores would, at iter 2, be a
+       UseAfterMove.  We run cond+body twice; iter 2 starts from the
+       post-iter-1 state, so an unrestored move surfaces as
+       UseAfterMove on the second pass.  Pairs with the StmtAssign
+       clear-on-rewrite fix (#399, [is_whole_place_write]) so loops
+       that legitimately re-initialise a moved-out variable per
+       iteration still converge — iter-2's read of the freshly-
+       reassigned place is not a UseAfterMove because iter 1's
+       assignment cleared the move record.  After both passes we
+       restore state to the iter-1-post snapshot so any analysis
+       past the loop sees a single iter's worth of state (the loop
+       may execute 0..N times — using iter-1-post is the sound
+       choice when iter-2 doesn't add new conflicts). *)
     let* () = check_expr ctx state symbols cond in
-    check_block ctx state symbols body
+    let* () = check_block ctx state symbols body in
+    let snap_borrows = state.borrows in
+    let snap_moved = state.moved in
+    let snap_ref_bindings = state.ref_bindings in
+    let snap_block_locals = state.block_local_syms in
+    let snap_mutable = state.mutable_bindings in
+    let r =
+      let* () = check_expr ctx state symbols cond in
+      check_block ctx state symbols body
+    in
+    state.borrows <- snap_borrows;
+    state.moved <- snap_moved;
+    state.ref_bindings <- snap_ref_bindings;
+    state.block_local_syms <- snap_block_locals;
+    state.mutable_bindings <- snap_mutable;
+    r
   | StmtFor (_pat, iter, body) ->
+    (* CORE-01 pt3 Slice C' / #177 — same 2-iteration pass as
+       [StmtWhile]; see comment there for rationale. *)
     let* () = check_expr ctx state symbols iter in
-    check_block ctx state symbols body
+    let* () = check_block ctx state symbols body in
+    let snap_borrows = state.borrows in
+    let snap_moved = state.moved in
+    let snap_ref_bindings = state.ref_bindings in
+    let snap_block_locals = state.block_local_syms in
+    let snap_mutable = state.mutable_bindings in
+    let r =
+      let* () = check_expr ctx state symbols iter in
+      check_block ctx state symbols body
+    in
+    state.borrows <- snap_borrows;
+    state.moved <- snap_moved;
+    state.ref_bindings <- snap_ref_bindings;
+    state.block_local_syms <- snap_block_locals;
+    state.mutable_bindings <- snap_mutable;
+    r
 
 (** Check a function
 
@@ -1578,17 +1625,20 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
    to work; the new path is `r = r_other`.  Closes the
    reborrow-through-indirection gap in #177 / CORE-01 pt3.
 
+   CORE-01 pt3 Slice C' (2026-05-27): loop soundness via a 2-iteration
+   check on [StmtWhile]/[StmtFor].  The body runs once; then state-
+   fields snapshot; then cond+body run again from the post-iter-1
+   state.  Any move that the body didn't restore (no rebinding
+   assignment) surfaces as UseAfterMove on the 2nd pass.  Pairs with
+   the StmtAssign clear-on-rewrite from #399 ([is_whole_place_write])
+   so legitimate re-init loops still accept while loops with an
+   unrestored body-move reject.
+
    Still deferred:
    - Origin/region variables (true Polonius surface) — a region
      var on each [TyRef]/[TyMut] with subset constraints and a
      proper datalog-style loan-live-at-point solver.  Architectural
      change to the type system; ADR-gated.
-   - Loop soundness (`StmtWhile`/`StmtFor`): a single body pass
-     misses multi-iteration move conflicts.  A 2-iteration check
-     would catch them.  Slice C''s StmtAssign clear-on-rewrite
-     half is now landed (see [StmtAssign] above and the
-     [is_whole_place_write] gate); the loop-soundness half can
-     proceed independently.
    - Tighter integration with the quantity checker for captured
      linears (Slice D).
 *)

test/e2e/fixtures/slice_c_prime_loop_move_persists.affine

@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice C' / #177: anti-regression — multi-iteration
+// move conflict. The loop body moves `x` via `drop_int(x)` and
+// then DOES NOT rebind it. Pre-fix, a single-pass body check
+// silently accepted this loop because iter 1 moves x cleanly and
+// no further use is visible *within iter 1*. With the 2-iteration
+// check, iter 2 begins with `x` already moved (moves persist
+// across block exit by design), so the iter-2 read of `x` at
+// `drop_int(x)` surfaces as UseAfterMove. This is the soundness
+// gain. Expected: Error UseAfterMove.
+
+module SliceCPrimeLoopMovePersists;
+
+fn drop_int(x: own Int) -> Unit = ();
+
+fn loop_move_no_rebind() -> Int {
+  let mut x = 10;
+  let mut i = 0;
+  while i < 3 {
+    drop_int(x);
+    i = i + 1;
+  }
+  0
+}

test/e2e/fixtures/slice_c_prime_loop_reinit_ok.affine

@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice C' / #177: positive case demonstrating the
+// interaction between the 2-iteration loop check (this slice) and
+// the clear-on-rewrite half landed in #399 ([is_whole_place_write]).
+// The loop body moves `x` (via `drop_int`'s `own` param) and then
+// *immediately rebinds* `x = 42`.  Without clear-on-rewrite, iter 1's
+// assignment after the move would already fail (Pre-#399 behaviour);
+// without the 2-iter pass, the loop would falsely accept any
+// no-rebind body.  Both halves together: iter 1 moves then rebinds
+// (Ok, move cleared), iter 2 starts from rebound state and repeats.
+// Expected: Ok.
+
+module SliceCPrimeLoopReinitOk;
+
+fn drop_int(x: own Int) -> Unit = ();
+
+fn loop_reinit() -> Int {
+  let mut x = 10;
+  let mut i = 0;
+  while i < 3 {
+    drop_int(x);
+    x = 42;
+    i = i + 1;
+  }
+  x
+}

test/e2e/fixtures/slice_c_prime_loop_sound.affine

@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice C' / #177: positive case for the 2-iteration
+// loop check. An ordinary counted loop with no moves and no borrows
+// must converge on the second pass — iter 2 sees the same state as
+// iter 1 (modulo mutable_bindings/borrows snapshot restoration), so
+// the body's reads/assignments stay legal. Pre-2-iter, this case
+// already passed; this fixture pins that the 2-iter pass did not
+// break it. Expected: Ok.
+
+module SliceCPrimeLoopSound;
+
+fn loop_counted() -> Int {
+  let mut acc = 0;
+  let mut i = 0;
+  while i < 5 {
+    acc = acc + i;
+    i = i + 1;
+  }
+  acc
+}

test/test_e2e.ml

@@ -4486,6 +4486,40 @@ let test_borrow_assign_clears_move () =
                     spuriously rejected — whole-place write should revive \
                     the moved place: " ^ Borrow.format_borrow_error e)
 
+(* CORE-01 pt3 Slice C' / #177 — loop soundness via 2-iteration on
+   [StmtWhile]/[StmtFor].  Three tests pin: (1) sound counted loop
+   converges; (2) interaction with #399's clear-on-rewrite — a
+   move-then-rebind body accepts; (3) anti-regression — a move
+   without rebind raises UseAfterMove on the 2nd pass. *)
+let test_slice_c_prime_loop_sound () =
+  match borrow_result (fixture "slice_c_prime_loop_sound.affine") with
+  | Ok () -> ()
+  | Error e ->
+    Alcotest.fail ("Slice C': counted loop was spuriously rejected — \
+                    iter-2 pass introduced a false positive: "
+                   ^ Borrow.format_borrow_error e)
+
+let test_slice_c_prime_loop_reinit_ok () =
+  match borrow_result (fixture "slice_c_prime_loop_reinit_ok.affine") with
+  | Ok () -> ()
+  | Error e ->
+    Alcotest.fail ("Slice C' × #399 interaction: re-init after move \
+                    was spuriously rejected — `x = 42` after `drop_int(x)` \
+                    should clear the move-record and let iter 2 converge: "
+                   ^ Borrow.format_borrow_error e)
+
+let test_slice_c_prime_loop_move_persists () =
+  match borrow_result (fixture "slice_c_prime_loop_move_persists.affine") with
+  | Error (Borrow.UseAfterMove _) -> ()
+  | Error e ->
+    Alcotest.fail ("Slice C' anti-regression: expected UseAfterMove on \
+                    the iter-2 `drop_int(x)` after iter-1 moved `x`, \
+                    got: " ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "Slice C' regressed: multi-iter move conflict was \
+                   silently accepted — the 2-iteration pass did not \
+                   catch the unrestored move on `x`"
+
 let borrow_tests = [
   Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block"
     `Quick test_borrow_outlives_owner;
@@ -4531,6 +4565,12 @@ let borrow_tests = [
     `Quick test_ref_to_ref_return_escape;
   Alcotest.test_case "assignment-clears-move: whole-place write revives moved place (#177)"
     `Quick test_borrow_assign_clears_move;
+  Alcotest.test_case "Slice C': counted loop converges (#177 pt3)"
+    `Quick test_slice_c_prime_loop_sound;
+  Alcotest.test_case "Slice C' × #399: re-init in loop OK (#177 pt3)"
+    `Quick test_slice_c_prime_loop_reinit_ok;
+  Alcotest.test_case "Slice C' anti-regression: multi-iter move rejected (#177 pt3)"
+    `Quick test_slice_c_prime_loop_move_persists;
 ]
 
 (* ============================================================================