hyperpolymath · hyperpolymath · May 24, 2026 · May 24, 2026 · May 24, 2026 · May 24, 2026
diff --git a/lib/borrow.ml b/lib/borrow.ml
@@ -1233,8 +1233,41 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
           (* Can't assign while borrowed *)
           Error (MoveWhileBorrowed (place, borrow))
         | None ->
-          (* Assignment is ok, check the RHS *)
-          check_expr ctx state symbols rhs
+          (* Slice B (CORE-01 pt3 / #177): flow-sensitive escape via
+             `outer = &y`.  If LHS is a ref-binder symbol that already
+             holds a borrow and RHS is a fresh `&y`/`&mut y` reference,
+             the assignment *replaces* the held borrow.  We pre-release
+             the old held borrow before checking the RHS so the same-
+             target reborrow case (`r = &mut x` while `r` already holds
+             `&mut x`) does not trip [ConflictingBorrow] on the
+             about-to-be-replaced exclusive borrow; we then re-bind the
+             ref-graph entry to the freshly-created borrow.  Mirrors
+             [record_ref_binding]'s let-graph contract for the
+             assignment path so the NLL last-use + return-escape
+             analyses see the *current* referent after re-assignment,
+             not the stale original. *)
+          let pre_release =
+            match root_var place, ref_target symbols rhs with
+            | Some binder_sym, Some _
+              when List.mem_assoc binder_sym state.ref_bindings ->
+              let old_borrow = List.assoc binder_sym state.ref_bindings in
+              end_borrow state old_borrow;
+              state.ref_bindings <-
+                List.filter (fun (s, _) -> s <> binder_sym) state.ref_bindings;
+              Some binder_sym
+            | _ -> None
+          in
+          let* () = check_expr ctx state symbols rhs in
+          (match pre_release, ref_target symbols rhs with
+           | Some binder_sym, Some new_target ->
+             (match List.find_opt (fun b ->
+                      places_overlap b.b_place new_target) state.borrows with
+              | Some new_b ->
+                state.ref_bindings <-
+                  (binder_sym, new_b) :: state.ref_bindings
+              | None -> ())
+           | _ -> ());
+          Ok ()
         end
     | None ->
       (* LHS is not a place (e.g., function call result), check both sides *)
@@ -1341,11 +1374,26 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
    Outer-block ref-bindings are deliberately preserved — they expire
    only at their own block's exit.
 
-   Still deferred — region-/flow-sensitive remainder:
-   - Flow-sensitive escape via assignment to an outer mutable
-     (`outer = &x`): the assignment must update the borrow graph the
-     way [let r = &x] already does.
+   CORE-01 pt3 Slice B (flow-sensitive escape via re-assignment):
+   `outer = &y` now updates the borrow graph the way `let outer = &y`
+   does. In StmtAssign, when LHS is a ref-binder symbol with a held
+   borrow and RHS is a direct `&p`/`&mut p`, the old borrow is
+   pre-released (so a same-target reborrow like `r = &mut x` while
+   `r` already holds `&mut x` does not trip ConflictingBorrow on the
+   about-to-be-replaced exclusive borrow), then after the RHS check
+   the (binder -> new_borrow) ref-graph entry is re-bound to the
+   freshly-created borrow. NLL last-use + return-escape now see the
+   *current* referent after re-assignment, not the stale original.
+
+   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 (Polonius surface) + loan-live-at-point
-     dataflow across CFG joins (Slice C).
-   - Tighter integration with the quantity checker for captured linears.
+     dataflow across CFG joins for `ExprHandle`/`ExprTry`/loops
+     (Slice C).
+   - Tighter integration with the quantity checker for captured
+     linears (Slice D).
 *)
diff --git a/test/e2e/fixtures/slice_b_new_borrow_still_protects.affine b/test/e2e/fixtures/slice_b_new_borrow_still_protects.affine
@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice B / #177 anti-regression: after `r = &y`, the
+// NEW borrow on `y` must still protect `y` while `r` is live. A
+// buggy Slice B that dropped the ref-binding but failed to re-bind
+// to the new borrow would silently accept `y = 10` below — the
+// borrow-graph would lose track of who holds &y. With correct
+// Slice B, `(r, &y)` is in ref_bindings, the borrow on `y` is in
+// state.borrows, and the assignment to `y` is rejected as
+// MoveWhileBorrowed. Expected: Error MoveWhileBorrowed.
+
+module SliceBNewBorrowStillProtects;
+
+fn still_protected() -> Int {
+  let mut x = 1;
+  let mut y = 2;
+  let mut r = &x;
+  r = &y;
+  y = 10;
+  *r
+}
diff --git a/test/e2e/fixtures/slice_b_nll_expires_new.affine b/test/e2e/fixtures/slice_b_nll_expires_new.affine
@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice B / #177: after `r = &y`, the NLL last-use
+// machinery must track the NEW borrow (on `y`), not the stale old
+// one (on `x`). Without Slice B, the ref-binding entry stays
+// `(r, &x)`, so when NLL expires `r` after its last use it ends the
+// wrong borrow — leaving the new borrow on `y` alive and
+// spuriously rejecting the later `y = 10`. With Slice B, the entry
+// is `(r, &y)` post-reassignment, NLL expires the correct borrow,
+// and both `x = 5` and `y = 10` succeed. Expected: Ok.
+
+module SliceBNllExpiresNew;
+
+fn nll_after_reassign() -> Int {
+  let mut x = 1;
+  let mut y = 2;
+  let mut r = &x;
+  r = &y;
+  let z = *r;
+  x = 5;
+  y = 10;
+  x + y + z
+}
diff --git a/test/e2e/fixtures/slice_b_outer_assign_releases_old.affine b/test/e2e/fixtures/slice_b_outer_assign_releases_old.affine
@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice B / #177: flow-sensitive escape via `outer = &y`.
+// Pre-Slice-B, the borrow held by `r` on `x` was never released when
+// `r` was re-assigned to `&y` — so `x = 10` was rejected as
+// MoveWhileBorrowed even though `r` no longer pointed at `x`. With
+// Slice B, the assignment `r = &y` ends the held borrow on `x` and
+// re-binds `r` in the ref-graph to the freshly-created borrow on `y`,
+// so the subsequent write to `x` is legal. Expected: Ok.
+
+module SliceBOuterAssignReleasesOld;
+
+fn outer_reassign() -> Int {
+  let mut x = 1;
+  let mut y = 2;
+  let mut r = &x;
+  let z = *r;
+  r = &y;
+  x = 10;
+  *r + x + z
+}
diff --git a/test/test_e2e.ml b/test/test_e2e.ml
@@ -4354,6 +4354,39 @@ let test_borrow_nll_still_rejects_live_borrow () =
     Alcotest.fail "NLL over-expired a still-live borrow — assignment \
                    to a borrowed owner was accepted"
 
+(* CORE-01 pt3 Slice B / #177 — flow-sensitive escape via `outer = &y`.
+   The assignment `r = &y` (where `r` is an existing ref-binder) now
+   releases the old held borrow and re-binds `r` in the ref-graph to
+   the freshly-created borrow. Three tests pin: (1) the old target is
+   freed by the reassignment; (2) NLL last-use then correctly expires
+   the NEW borrow; (3) anti-regression — the new borrow still
+   protects its new target while the binder is live. *)
+let test_slice_b_outer_assign_releases_old () =
+  match borrow_result (fixture "slice_b_outer_assign_releases_old.affine") with
+  | Ok () -> ()
+  | Error e ->
+    Alcotest.fail ("Slice B: `r = &y` did not release the old borrow on \
+                    `x` — `x = …` after the reassignment was spuriously \
+                    rejected: " ^ Borrow.format_borrow_error e)
+
+let test_slice_b_nll_expires_new () =
+  match borrow_result (fixture "slice_b_nll_expires_new.affine") with
+  | Ok () -> ()
+  | Error e ->
+    Alcotest.fail ("Slice B: NLL last-use after `r = &y` did not expire \
+                    the new borrow on `y`: " ^ Borrow.format_borrow_error e)
+
+let test_slice_b_new_borrow_still_protects () =
+  match borrow_result (fixture "slice_b_new_borrow_still_protects.affine") with
+  | Error (Borrow.MoveWhileBorrowed _) -> ()
+  | Error e ->
+    Alcotest.fail ("Slice B anti-regression: expected MoveWhileBorrowed \
+                    on `y = …` (the new borrow must still protect `y`), \
+                    got: " ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "Slice B regressed: the new borrow on `y` was not \
+                   tracked, so the write to `y` was silently accepted"
+
 let borrow_tests = [
   Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block"
     `Quick test_borrow_outlives_owner;
@@ -4379,6 +4412,12 @@ let borrow_tests = [
     `Quick test_borrow_nll_read_after_mut_last_use;
   Alcotest.test_case "NLL anti-regression: still-live borrow blocks assign (#177 pt3 Slice A)"
     `Quick test_borrow_nll_still_rejects_live_borrow;
+  Alcotest.test_case "Slice B: `r = &y` releases old borrow on `x` (#177 pt3 Slice B)"
+    `Quick test_slice_b_outer_assign_releases_old;
+  Alcotest.test_case "Slice B: NLL expires the NEW borrow after `r = &y` (#177 pt3 Slice B)"
+    `Quick test_slice_b_nll_expires_new;
+  Alcotest.test_case "Slice B anti-regression: new borrow still protects `y` (#177 pt3 Slice B)"
+    `Quick test_slice_b_new_borrow_still_protects;
 ]
 
 (* ============================================================================