feat(borrow): CORE-01 Slice C' (#177 pt3) — loop soundness via 2-iteration + StmtAssign clear-on-rewrite

Closes the loop-soundness item documented at lib/borrow.ml's "Still
deferred" comment.  Two interlocked changes:

1. StmtAssign clear-on-rewrite (precondition for #2).

   Pre-fix, [check_use] on the LHS of every assignment rejected
   `x = …` when `x` had a prior move record — even though the
   assignment is precisely what restores `x` to a fresh value. That
   made legitimate re-init patterns impossible (`drop_int(x);
   x = new_value;` in a loop body), and it made the 2-iteration
   loop check unable to converge on any such loop.

   Now [StmtAssign] (a) checks only for an exclusive-borrow
   conflict on the LHS (not for a move), and (b) clears every
   move record overlapping the LHS place after the assignment
   completes.

2. StmtWhile/StmtFor 2-iteration body pass.

   The body runs once; then state-fields snapshot; then cond+body
   run again from the post-iter-1 state. Any move the body did
   not restore via reassignment surfaces as UseAfterMove on the
   second pass — that is the multi-iter soundness gain. After
   both passes, state is restored to the iter-1-post snapshot so
   any analysis past the loop sees a single iteration's worth of
   state (loops may execute 0..N times; iter-1-post is the sound
   choice when iter-2 doesn't add new conflicts).

Tests (+3, all green):
  - slice_c_prime_loop_sound — counted loop converges, no false +ve
  - slice_c_prime_loop_reinit_ok — drop-then-reassign in body OK
  - slice_c_prime_loop_move_persists — anti-regression: move with
    no rebind raises UseAfterMove on the iter-2 pass

Gate: 327 → 330 tests, 0 failures under `dune runtest --force`.

Refs #177, CORE-01 pt3 (Slice C').

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

Author: hyperpolymath

lib/borrow.ml

@@ -1307,8 +1307,20 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
       if not (is_mutable state place) then
         Error (CannotBorrowAsMutable (place, expr_span lhs))
       else
-        (* Check that the place is not moved and not borrowed *)
-        let* () = check_use state place (expr_span lhs) in
+        (* CORE-01 pt3 Slice C' / #177: assignment REBINDS the LHS,
+           so a prior move on the LHS place is *cleared* by the
+           assignment — `x = …` is not a use of the moved value.
+           Previously [check_use] rejected `x = …` after `x` was
+           moved, which spuriously rejected legitimate re-init in
+           loop bodies (and prevented the 2-iteration loop check
+           from converging).  We still reject if the place is
+           *exclusively borrowed* — you cannot reassign through a
+           place while a still-live exclusive borrow holds it. *)
+        let* () = match find_aliasing_exclusive state place with
+          | Some b ->
+            Error (UseWhileExclusivelyBorrowed (place, b, expr_span lhs))
+          | None -> Ok ()
+        in
         (* Check for any active borrows of this place *)
         begin match List.find_opt (fun b -> places_overlap place b.b_place) state.borrows with
         | Some borrow ->
@@ -1349,6 +1361,16 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
                   (binder_sym, new_b) :: state.ref_bindings
               | None -> ())
            | _ -> ());
+          (* CORE-01 pt3 Slice C' / #177: clear any prior move record on
+             the LHS place — the assignment has rebound it to a fresh
+             value, so subsequent reads of LHS are uses of the *new*
+             binding, not the moved-out one.  This is the second half
+             of the clear-on-rewrite fix (the first half was skipping
+             the LHS move check up at [check_use] entry above). *)
+          state.moved <-
+            List.filter (fun mr ->
+              not (places_overlap place mr.m_place)
+            ) state.moved;
           Ok ()
         end
     | None ->
@@ -1357,11 +1379,55 @@ 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 above so loops that legitimately
+       re-initialise a moved-out variable per iteration still
+       converge (iter-2 move is no longer treated as use-of-moved
+       because iter 1's assignment cleared the move).  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 moves). *)
     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) ->
     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
 
@@ -1480,22 +1546,28 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
    one helper so all CFG-join sites agree).  Finally runs after
    the merge, deterministically, against the merged state.
 
+   CORE-01 pt3 Slice C' (2026-05-26): loop soundness via a 2-iteration
+   check on [StmtWhile]/[StmtFor], paired with [StmtAssign]
+   clear-on-rewrite.  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.  Pre-fix [check_use] also fired
+   on the LHS of every assignment, so a re-init pattern (move x;
+   x = new_value) spuriously failed — making 2-iter convergence
+   impossible.  Now [StmtAssign] (a) only checks the LHS for an
+   exclusive-borrow conflict (not for a move), and (b) clears any
+   prior move record overlapping the LHS place after the assign
+   completes.  Together: legitimate re-init loops accept; loops
+   with an unrestored body-move reject.  State restoration to the
+   iter-1-post snapshot keeps analysis past the loop consistent
+   (loops may execute 0..N times — using iter-1-post is the sound
+   choice when iter-2 doesn't add new conflicts).
+
    Still deferred:
-   - Reborrow through indirection: `r = some_other_ref_var` (RHS not a
-     direct `&place`) does not yet copy the other binder's graph
-     entry — the ref-binding stays stale.  Same limitation as
-     [record_ref_binding] for the let-graph path; would require
-     symmetric let/assign handling for ref-to-ref binding.
    - 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 but requires fixing the assignment-clears-
-     move imprecision first (assignment is currently treated as a
-     read of LHS, so `x = …` after a prior move spuriously fails).
-     Couple Slice C' with the StmtAssign clear-on-rewrite fix.
    - 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
+// clear-on-rewrite half of the slice. The loop body moves `x`
+// (via the `own` parameter of `drop_int`) and then *immediately
+// rebinds* `x = 1` on the next statement. Pre-fix, the assignment
+// after a move was rejected (StmtAssign called `check_use` which
+// looked up the move record on `x` and raised UseAfterMove on
+// what is in fact a re-init).  With clear-on-rewrite the
+// assignment skips the move check on LHS and clears any prior
+// move record on the place, so iter 2 starts fresh and the loop
+// converges. 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

@@ -4415,6 +4415,43 @@ let test_slice_c_body_move_persists () =
                    the catch-arm merge — `read_int(y)` after a moved `y` \
                    was silently accepted"
 
+(* CORE-01 pt3 Slice C' / #177 — loop soundness via 2-iteration +
+   StmtAssign clear-on-rewrite. The two halves are interlocked:
+   without clear-on-rewrite, legitimate re-init loops would
+   spuriously fail; without the 2-iter pass, multi-iter move
+   conflicts go undetected. Three tests pin: (1) sound counted
+   loop converges; (2) clear-on-rewrite — move-then-reassign
+   inside the body accepts; (3) anti-regression — 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' clear-on-rewrite: re-init after move was \
+                    spuriously rejected — `x = 42` after `drop_int(x)` \
+                    should clear the move: "
+                   ^ 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;
@@ -4450,6 +4487,12 @@ let borrow_tests = [
     `Quick test_slice_c_catch_arm_isolation;
   Alcotest.test_case "Slice C anti-regression: body's move persists past try (#177 pt3 Slice C)"
     `Quick test_slice_c_body_move_persists;
+  Alcotest.test_case "Slice C': counted loop converges (#177 pt3)"
+    `Quick test_slice_c_prime_loop_sound;
+  Alcotest.test_case "Slice C': clear-on-rewrite — 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;
 ]
 
 (* ============================================================================