From 000f9154c455b3687312227270960841a64cfd1e Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 24 May 2026 19:41:07 +0000 Subject: [PATCH] feat(borrow): flow-sensitive escape via `outer = &y` (CORE-01 pt3 Slice B, Refs #177) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .machine_readable/6a2/STATE.a2ml | 2 +- docs/CAPABILITY-MATRIX.adoc | 15 +++-- docs/TECH-DEBT.adoc | 29 ++++++--- lib/borrow.ml | 64 ++++++++++++++++--- .../slice_b_new_borrow_still_protects.affine | 22 +++++++ .../fixtures/slice_b_nll_expires_new.affine | 24 +++++++ .../slice_b_outer_assign_releases_old.affine | 22 +++++++ test/test_e2e.ml | 39 +++++++++++ 8 files changed, 194 insertions(+), 23 deletions(-) create mode 100644 test/e2e/fixtures/slice_b_new_borrow_still_protects.affine create mode 100644 test/e2e/fixtures/slice_b_nll_expires_new.affine create mode 100644 test/e2e/fixtures/slice_b_outer_assign_releases_old.affine diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 44bce89c..87b639c4 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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)" diff --git a/docs/CAPABILITY-MATRIX.adoc b/docs/CAPABILITY-MATRIX.adoc index 57bc2c38..ad3e795a 100644 --- a/docs/CAPABILITY-MATRIX.adoc +++ b/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` diff --git a/docs/TECH-DEBT.adoc b/docs/TECH-DEBT.adoc index 5d2411ac..2b6afbe9 100644 --- a/docs/TECH-DEBT.adoc +++ b/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 diff --git a/lib/borrow.ml b/lib/borrow.ml index b3c5359a..1e3e7513 100644 --- 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 new file mode 100644 index 00000000..00134f3c --- /dev/null +++ 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 new file mode 100644 index 00000000..55c81324 --- /dev/null +++ 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 new file mode 100644 index 00000000..5ad82c17 --- /dev/null +++ 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 index 3e872b3b..18c3ace9 100644 --- a/test/test_e2e.ml +++ b/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; ] (* ============================================================================