feat(borrow): flow-sensitive escape via outer = &y (CORE-01 pt3 Slice B, Refs #177)

Under purely lexical analysis (and even after Slice A's NLL last-use),
re-assigning a ref-binder — `let mut r = &x; r = &y` — left the
*old* held borrow on `x` in `state.borrows` and the *stale*
`(r -> old_borrow)` entry in `state.ref_bindings`. The new borrow
on `y` was added by `check_expr(rhs)` but never wired into the
ref-graph, so:

- `x = 10` after the reassignment was rejected as MoveWhileBorrowed
  even though `r` no longer pointed at `x` (the bug this PR fixes).
- NLL last-use on `r` expired the WRONG borrow (the old one on `x`),
  leaving the new borrow on `y` hanging — masking valid writes to
  `y`.
- `check_return_escape` looked up the stale `(r -> &x)` entry rather
  than the actual current referent `&y`.

This is the "flow-sensitive escape via assignment to an outer
mutable" residual called out in the Slice A docstring.

Implementation in `lib/borrow.ml` `StmtAssign`:

When LHS is a ref-binder symbol that already holds a borrow AND RHS
is a direct `&p`/`&mut p`, the code now:

1. *Pre*-releases the old held borrow (via `end_borrow`) and removes
   the stale entry from `ref_bindings` BEFORE checking the RHS. The
   pre-release order matters for the same-target reborrow case
   (`r = &mut x` while `r` already holds `&mut x`): post-release
   ordering would trip `ConflictingBorrow` on the about-to-be-
   replaced exclusive borrow at `record_borrow` time, which is
   user-confusing because the conflict is purely an artefact of
   sequential modelling. Pre-release dissolves the conflict.

2. Checks the RHS, which creates the new borrow on `state.borrows`
   the usual way (`record_borrow`).

3. After RHS-check, looks up the freshly-created borrow on the new
   target place and binds it into `ref_bindings` as
   `(binder_sym, new_borrow)` — the symmetric assignment-side of
   `record_ref_binding`'s let-graph contract.

Sound: NLL last-use, in-block `BorrowOutlivesOwner`, and
`check_return_escape` now consult the current referent. The new
borrow continues to live on `state.borrows` and continues to be
visible to `find_aliasing_exclusive` / "active borrow of LHS"
detection — see the anti-regression test.

Tests (E2E Borrow Graph, +3):
- `slice_b_outer_assign_releases_old.affine` — `r = &y` then
  `x = 10` is now Ok (the old borrow on `x` was released).
- `slice_b_nll_expires_new.affine` — after `r = &y` and `r`'s last
  use, NLL expires the NEW borrow (on `y`), so subsequent writes to
  BOTH `x` and `y` succeed. Without the re-bind, NLL would expire
  the wrong borrow and `y = 10` would fail.
- `slice_b_new_borrow_still_protects.affine` — anti-regression:
  after `r = &y`, while `r` is still live, `y = 10` must still
  fail (MoveWhileBorrowed). Pins that the new borrow IS tracked.

Existing tests audited and remain green by construction:
- `borrow_return_refparam_ok.affine`: no re-assignment in scope; no
  Slice B trigger. Unaffected.
- `borrow_return_escape_{param,local}.affine`: `let r = &x` then
  `return r` (no reassignment); same path as before.
- `borrow_nll_still_rejects_live_borrow.affine`: no `&p`-form RHS
  in scope; Slice B doesn't fire.
- All existing borrow / quantity / linear-arrow fixtures are
  untouched by the new path — the assignment branch only deviates
  when LHS is a ref-binder AND RHS is a direct `&p`/`&mut p`.

Deferred (Slices C–D residual):
- Reborrow through indirection: `r = some_other_ref_var` (RHS not
  a direct `&place`) still leaves the ref-binding stale. Same
  limitation as `record_ref_binding`'s let-graph path; would need
  symmetric ref-to-ref binding for both let and assign.
- Origin/region variables (Polonius surface) + loan-live-at-point
  dataflow across CFG joins for `ExprHandle`/`ExprTry`/loops.
- Tighter quantity-checker integration for captured linears.

Docs updated: `STATE.a2ml` borrow-checker → "Slices A and B
landed"; `CAPABILITY-MATRIX.adoc` borrow-checker row records
Slice B; `TECH-DEBT.adoc` CORE-01 row records Slice B + narrows
residual to Slices C–D.

NOTE: this container has no OCaml toolchain; `dune build` /
`dune runtest` were not run locally. CI is the source of truth.
Mechanically scoped to one branch of `StmtAssign`'s `Some place →
None`-conflict-on-LHS arm; all other code paths are unchanged.

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -71,7 +71,7 @@ test-files = 54
 # the feature is not enforced on user programs through the CLI pipeline.
 affine-types = "wired-and-reachable (Track A Manhattan plan complete 2026-04-10. Quantity semiring in lib/quantity.ml; invoked from typecheck.ml:1206 inside the standard CLI pipeline. Surface syntax per ADR-007 hybrid: @linear/@erased/@unrestricted attributes (Option C primary) on let/stmt-let/param/lambda-param, AND :1/:0/:ω numeric sugar (Option B) on let/stmt-let. Scaled Let rule per ADR-002 implemented in lib/quantity.ml ExprLet/StmtLet — closes BUG-001 (ω-let smuggles linear values) and BUG-002 (zero-let erasure). Four regression fixtures in test/e2e/fixtures/ exercise both surface forms. Behavioural enforcement verified via E2E Quantity test suite — 4 new passing tests, 0 regressions.)"
 linear-arrows = "enforced (2026-04-11): Three-part fix landed. (1) typecheck.ml lambda synth: |@linear x: T| e now synthesises T -[1]-> U (was always QOmega). (2) typecheck.ml lambda check mode: explicit param quantity annotation validated against expected TArrow quantity; unannotated params inherit context quantity. (3) quantity.ml ExprLambda: added env.errors accumulator; annotated lambda params declared via env_declare so env_use tracks them; usage verified with check_quantity after body walk; violations pushed to env.errors and drained at end of check_function_quantities (step 4). Saved/restored env.quantities entries to prevent scope leakage. Two E2E fixtures + 2 passing tests. 75 tests total, 0 regressions. Commit d2f9b7b pushed."
-borrow-checker = "phase-3-part-3-slice-A-landed (CORE-01, Refs #177, 2026-05-24): pt1 (#240, gate 263/263) borrow-graph validation wired — BorrowOutlivesOwner emitted (&local escaping its block), shared-XOR-exclusive enforced at use sites (UseWhileExclusivelyBorrowed), ownership derived from param type TyOwn/TyRef/TyMut (owned/ref/mut discipline now enforced from real parsed source — closed a latent hole), call-arg borrows temporary, ref-binding graph tracked. pt2 (gate 271→274 and 278→281) return-escape (return-of-ref-rooted-at-callee-owned-binding caught) + &mut e parser surface (zero Menhir conflict delta — exclusive borrow finally expressible from real source). pt3 Slice A NLL last-use expiry: forward pre-pass compute_last_use_index maps each symbol to its greatest mentioning statement index; check_block expires ref-bindings introduced in-block once their binder is dead, releasing the underlying borrow. Unblocks `let r = &x; print(*r); x = 2` and `let m = &mut x; let y = *m; x` while still rejecting same-block live aliasing (2 positive + 1 anti-regression hermetic tests in E2E Borrow Graph). Residual (Slices B–D): flow-sensitive escape via `outer = &x`, origin/region variables (Polonius surface) + loan-live-at-point dataflow across CFG joins, tighter quantity integration. Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT.adoc CORE-01."
+borrow-checker = "phase-3-parts-1-3-Slices-A-and-B-landed (CORE-01, Refs #177, 2026-05-24): pt1 (#240, gate 263/263) borrow-graph validation wired — BorrowOutlivesOwner emitted (&local escaping its block), shared-XOR-exclusive enforced at use sites (UseWhileExclusivelyBorrowed), ownership derived from param type TyOwn/TyRef/TyMut, call-arg borrows temporary, ref-binding graph tracked. pt2 (gate 271→274 and 278→281) return-escape + &mut e parser surface (zero Menhir conflict delta — exclusive borrow finally expressible from real source). pt3 Slice A (PR #335) NLL last-use expiry: forward pre-pass compute_last_use_index maps each symbol to its greatest mentioning statement index; check_block expires ref-bindings introduced in-block once their binder is dead. Unblocks `let r = &x; print(*r); x = 2` and `let m = &mut x; let y = *m; x` (2 positive + 1 anti-regression in E2E Borrow Graph). pt3 Slice B (this PR) flow-sensitive escape via re-assignment: `outer = &y` in StmtAssign now pre-releases the held borrow and re-binds the (binder → new_borrow) ref-graph entry to the freshly-created borrow, so NLL last-use + return-escape see the *current* referent. 3 hermetic tests (2 positive + 1 anti-regression). Residual (Slices C–D): origin/region variables (Polonius surface) + loan-live-at-point dataflow for CFG joins in ExprHandle/ExprTry/loops; tighter quantity integration for captured linears; reborrow through indirection (RHS that is a ref-typed value rather than a direct &place). Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT.adoc CORE-01."
 row-polymorphism = "60% (records + effects rows implemented in typecheck/unify; not fully exercised end-to-end)"
 effects = "interpreter-complete (handler dispatch, PerformEffect propagation, ExprResume, multi-arg ops all wired in interp.ml 2026-04-11). WasmGC: ops registered as unreachable stubs; ExprHandle/ExprResume reject with UnsupportedFeature — full WASM dispatch needs EH proposal or CPS transform."
 dependent-types = "parse-only (TRefined AST node exists and refinement predicates parse, but predicates do not reduce; no SMT/decision procedure wired in)"

docs/CAPABILITY-MATRIX.adoc

@@ -100,10 +100,17 @@ ref-bindings expire at their binder's *last use*, not at block exit
 (`compute_last_use_index` pre-pass + per-statement expiry in
 `check_block`). Patterns like `let r = &x; print(*r); x = 2` and
 `let m = &mut x; let y = *m; x` now type-check, while still-live borrows
-continue to block aliasing assignments. *Deferred (Slices B–D):*
-flow-sensitive escape via `outer = &x`; origin/region variables
-(Polonius surface) + loan-live-at-point dataflow across CFG joins;
-tighter quantity integration for captured linears.
+continue to block aliasing assignments. *Part 3 Slice B* (Refs #177):
+flow-sensitive escape via re-assignment — `outer = &y` in `StmtAssign`
+now pre-releases the held borrow and re-binds the
+`(binder -> new_borrow)` ref-graph entry to the freshly-created borrow,
+so the NLL last-use + return-escape analyses see the *current* referent
+after re-assignment, not the stale original (3 hermetic tests: old
+released, new tracked by NLL, anti-regression that new borrow still
+protects). *Deferred (Slices C–D):* origin/region variables (Polonius
+surface) + loan-live-at-point dataflow across CFG joins for
+`ExprHandle`/`ExprTry`/loops; tighter quantity integration for captured
+linears; reborrow through indirection (RHS not a direct `&place`).
 
 |Quantity / affine types |*enforced* |QTT semiring in `lib/quantity.ml`,
 invoked inside the standard CLI pipeline. `@linear`/`@erased`/`@unrestricted`

docs/TECH-DEBT.adoc

@@ -154,16 +154,25 @@ index that mentions it; after each statement, `check_block` expires any
 ref-binding introduced in that block whose binder is now dead, releasing
 the underlying borrow. Unblocks the canonical NLL patterns
 (`let r = &x; print(*r); x = 2`; `let m = &mut x; let y = *m; x`) while
-preserving soundness — the anti-aliasing rules still fire against
-statements that *do* use the binder (3 hermetic tests in "E2E Borrow
-Graph", two positive + one anti-regression). *Slices B–D residual:*
-flow-sensitive escape via assignment to an outer mutable
-(`outer = &x`); origin/region variables (Polonius surface) + loan-live-
-at-point dataflow across CFG joins; tighter quantity integration for
-captured linears. |S1 |pt1 #240 + pt2 return-escape + `&mut` surface +
-pt3 Slice A NLL last-use DONE (Refs #177); residual = Slices B–D
-(flow-sensitive escape, origin variables, quantity integration) —
-issue #177
+preserving soundness. *Part 3 Slice B LANDED* (Refs #177): flow-sensitive
+escape via re-assignment — `outer = &y` in `StmtAssign` now
+pre-releases the held borrow and re-binds the
+`(binder -> new_borrow)` ref-graph entry to the freshly-created borrow,
+so the NLL last-use + return-escape analyses see the *current* referent
+after re-assignment, not the stale original. Pre-release order chosen so
+the same-target reborrow (`r = &mut x` while `r` already holds
+`&mut x`) does not trip `ConflictingBorrow` on the about-to-be-replaced
+exclusive borrow. 3 hermetic tests in "E2E Borrow Graph" (old released,
+new tracked by NLL, anti-regression that new borrow still protects its
+new target). *Slices C–D residual:* origin/region variables (Polonius
+surface) + loan-live-at-point dataflow across CFG joins for
+`ExprHandle`/`ExprTry`/loops; tighter quantity integration for captured
+linears; reborrow through indirection (`r = some_other_ref_var` RHS does
+not yet copy the other binder's graph entry — symmetric let/assign
+limitation, parks with the let-graph's same restriction). |S1 |pt1 #240
++ pt2 return-escape + `&mut` surface + pt3 Slices A+B DONE (Refs #177);
+residual = Slices C–D (origin variables, quantity integration,
+ref-to-ref binding) — issue #177
 |CORE-02 |Effect-handler dispatch on WasmGC (was `UnsupportedFeature`;
 the chosen path is CPS over the EH proposal). The #225 CPS line closed
 the async slice; #234 generalised the boundary recogniser from a

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).
 *)

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
+}

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
+}

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
+}

test/test_e2e.ml

@@ -4232,6 +4232,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;
@@ -4257,6 +4290,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;
 ]
 
 (* ============================================================================