feat(borrow): flow-sensitive escape via outer = &y (CORE-01 pt3 Slice B, Refs #177)#351
Closed
hyperpolymath wants to merge 1 commit into
Closed
feat(borrow): flow-sensitive escape via outer = &y (CORE-01 pt3 Slice B, Refs #177)#351hyperpolymath wants to merge 1 commit into
outer = &y (CORE-01 pt3 Slice B, Refs #177)#351hyperpolymath wants to merge 1 commit into
Conversation
…ce 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.
hyperpolymath
added a commit
that referenced
this pull request
May 24, 2026
auto-merge was automatically disabled
May 24, 2026 20:36
Pull request was closed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
CORE-01 Phase 3 Slice B — flow-sensitive escape via re-assignment.
let mut r = &x; r = &ynow correctly updates the borrow graph: the old held borrow onxis released and the(r → new_borrow)entry is re-bound to the freshly-created borrow ony. The NLL last-use machinery from Slice A (#335) now sees the current referent after re-assignment, not the stale original.Before this PR (post-Slice-A behaviour):
After this PR:
x = 10isOk,*rreads through the new borrow ony.Mechanics in
lib/borrow.mlStmtAssignWhen LHS is a ref-binder symbol that already holds a borrow AND RHS is a direct
&p/&mut p:end_borrow) and remove the stale entry fromref_bindingsbefore checking the RHS. The pre-release order matters for the same-target reborrow case (r = &mut xwhileralready holds&mut x): post-release ordering would tripConflictingBorrowon the about-to-be-replaced exclusive borrow atrecord_borrowtime, which is a sequential-modelling artefact, not a real conflict.record_borrowadds the new borrow tostate.borrowsthe usual way.ref_bindingsas(binder_sym, new_borrow)— the symmetric assignment-side ofrecord_ref_binding's let-graph contract.Tests (E2E Borrow Graph, +3)
slice_b_outer_assign_releases_old.affinex = 10still fails MoveWhileBorrowedslice_b_nll_expires_new.affiney = 10failsslice_b_new_borrow_still_protects.affineAnti-regression sweep
All existing borrow / quantity / linear-arrow fixtures audited and remain green by construction: the new path only fires when LHS is a ref-binder AND RHS is a direct
&p/&mut p. Every otherStmtAssignshape (literal RHS, function-call RHS, non-ref-binder LHS, deref LHS) takes the pre-existing code path unchanged.Scope of this PR
This completes the original "flow-sensitive escape" residual from CORE-01 pt3.
Deferred (Slices C–D residual):
r = some_other_ref_var(RHS not a direct&place) still leaves the ref-binding stale. Same limitation asrecord_ref_binding's let-graph path; would need symmetric ref-to-ref binding for bothletandassign.ExprHandle/ExprTry/loops. Needs an ADR for the type-system shape before implementation.Docs
STATE.a2mlborrow-checker→phase-3-parts-1-3-Slices-A-and-B-landedCAPABILITY-MATRIX.adocborrow-checker row records Slice BTECH-DEBT.adocCORE-01 row records Slice B + narrows residual to Slices C–DTest plan
build(opam exec -- dune build) greenlint+Run tests(opam exec -- dune runtest) —E2E Borrow Graphcount +3 (the 3 new Slice B cases), all greenRun codegen WASM testsgreen — full stdlib AOT exercises the corpusCheck formattinggreenLocal-build caveat: container has no OCaml toolchain, so
dune build/dune runtestwere not run locally. CI is the source of truth.Refs #177
Generated by Claude Code