Skip to content

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

Closed
hyperpolymath wants to merge 1 commit into
mainfrom
claude/bold-brahmagupta-0T7Bh
Closed

feat(borrow): flow-sensitive escape via outer = &y (CORE-01 pt3 Slice B, Refs #177)#351
hyperpolymath wants to merge 1 commit into
mainfrom
claude/bold-brahmagupta-0T7Bh

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Summary

CORE-01 Phase 3 Slice B — flow-sensitive escape via re-assignment. let mut r = &x; r = &y now correctly updates the borrow graph: the old held borrow on x is released and the (r → new_borrow) entry is re-bound to the freshly-created borrow on y. 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):

let mut x = 1;
let mut y = 2;
let mut r = &x;
let z = *r;
r = &y;
x = 10;       // ← MoveWhileBorrowed: the &x held by r was never released
*r + x + z

After this PR: x = 10 is Ok, *r reads through the new borrow on y.

Mechanics 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:

  1. Pre-release the old held borrow (via end_borrow) and remove 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 a sequential-modelling artefact, not a real conflict.
  2. Check the RHS — record_borrow adds the new borrow to state.borrows the usual way.
  3. After RHS-check, look up the freshly-created borrow on the new target place and bind it into ref_bindings as (binder_sym, new_borrow) — the symmetric assignment-side of record_ref_binding's let-graph contract.

Tests (E2E Borrow Graph, +3)

Fixture Direction Expected Distinguishes
slice_b_outer_assign_releases_old.affine positive Ok Without pre-release, x = 10 still fails MoveWhileBorrowed
slice_b_nll_expires_new.affine positive Ok Without re-bind, NLL expires the wrong borrow, y = 10 fails
slice_b_new_borrow_still_protects.affine anti-regression MoveWhileBorrowed Confirms new borrow is tracked, not silently dropped

Anti-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 other StmtAssign shape (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):

  • 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.
  • Slice C — origin/region variables (Polonius surface) + loan-live-at-point dataflow across CFG joins for ExprHandle/ExprTry/loops. Needs an ADR for the type-system shape before implementation.
  • Slice D — tighter quantity-checker integration for captured linears.

Docs

  • STATE.a2ml borrow-checkerphase-3-parts-1-3-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

Test plan

  • CI build (opam exec -- dune build) green
  • CI lint + Run tests (opam exec -- dune runtest) — E2E Borrow Graph count +3 (the 3 new Slice B cases), all green
  • CI Run codegen WASM tests green — full stdlib AOT exercises the corpus
  • CI Check formatting green

Local-build caveat: container has no OCaml toolchain, so dune build / dune runtest were not run locally. CI is the source of truth.

Refs #177


Generated by Claude Code

…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 hyperpolymath self-assigned this May 24, 2026
@hyperpolymath
hyperpolymath enabled auto-merge May 24, 2026 20:17
hyperpolymath added a commit that referenced this pull request May 24, 2026
#356)

… STATE.a2ml)

Extracted doc-only changes from PR #351 to avoid merge conflicts.
TECH-DEBT.adoc renamed to TECH-DEBT-alt.adoc per user request.
auto-merge was automatically disabled May 24, 2026 20:36

Pull request was closed

@hyperpolymath
hyperpolymath deleted the claude/bold-brahmagupta-0T7Bh branch May 24, 2026 20:36
hyperpolymath pushed a commit that referenced this pull request May 25, 2026
…T.adoc

Three pure-rename/delete operations to unblock the standing Hypatia
`root_hygiene` rule for this repo and re-canonicalise the coordination
ledger filename that the rest of the repo points at.

- `AI.a2ml` → `0-AI-MANIFEST.a2ml`. Matches the sibling-repo convention
  (`road-skate/`, `affinescript-vite/`, `affinescriptiser/` all already
  carry `0-AI-MANIFEST.a2ml`) and clears the Hypatia HIGH finding
  "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only". Content
  preserved verbatim; canonical-structure refresh deferred to a later
  tidy phase so the rename is reviewable in isolation.

- `AI.djot` deleted. Hypatia HIGH "Superseded by 0-AI-MANIFEST.a2ml";
  the same project metadata is already covered by 0-AI-MANIFEST.a2ml
  and the six `.machine_readable/6a2/*.a2ml` files it points at.

- `docs/TECH-DEBT-alt.adoc` → `docs/TECH-DEBT.adoc`. The whole repo
  references `TECH-DEBT.adoc` (META.a2ml, STATE.a2ml, CAPABILITY-MATRIX,
  ECOSYSTEM, RESCRIPT-ELIMINATION, STDLIB-EXTERN-AUDIT, TYPED-WASM-
  ROADMAP all link to it). PR #356 had renamed it `-alt` as a conflict-
  avoidance manoeuvre during the #351 split; with #351 now resolved
  (via #355/#356) the alt suffix is dead weight and every cross-link
  was silently broken. Restoring the canonical name; no content change.

- One incidental edit: CONTRIBUTING.md's repo-layout block pointed at
  the old `AI.a2ml` path — updated to `0-AI-MANIFEST.a2ml`.

No-op on CI semantics; this is pure filesystem hygiene. Phase 2c
(#357) is unaffected — it lives on a separate branch and does not
touch any of these paths.
hyperpolymath pushed a commit that referenced this pull request May 25, 2026
…T.adoc

Three pure-rename/delete operations to unblock the standing Hypatia
`root_hygiene` rule for this repo and re-canonicalise the coordination
ledger filename that the rest of the repo points at.

- `AI.a2ml` → `0-AI-MANIFEST.a2ml`. Matches the sibling-repo convention
  (`road-skate/`, `affinescript-vite/`, `affinescriptiser/` all already
  carry `0-AI-MANIFEST.a2ml`) and clears the Hypatia HIGH finding
  "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only". Content
  preserved verbatim; canonical-structure refresh deferred to a later
  tidy phase so the rename is reviewable in isolation.

- `AI.djot` deleted. Hypatia HIGH "Superseded by 0-AI-MANIFEST.a2ml";
  the same project metadata is already covered by 0-AI-MANIFEST.a2ml
  and the six `.machine_readable/6a2/*.a2ml` files it points at.

- `docs/TECH-DEBT-alt.adoc` → `docs/TECH-DEBT.adoc`. The whole repo
  references `TECH-DEBT.adoc` (META.a2ml, STATE.a2ml, CAPABILITY-MATRIX,
  ECOSYSTEM, RESCRIPT-ELIMINATION, STDLIB-EXTERN-AUDIT, TYPED-WASM-
  ROADMAP all link to it). PR #356 had renamed it `-alt` as a conflict-
  avoidance manoeuvre during the #351 split; with #351 now resolved
  (via #355/#356) the alt suffix is dead weight and every cross-link
  was silently broken. Restoring the canonical name; no content change.

- One incidental edit: CONTRIBUTING.md's repo-layout block pointed at
  the old `AI.a2ml` path — updated to `0-AI-MANIFEST.a2ml`.

No-op on CI semantics; this is pure filesystem hygiene. Phase 2c
(#357) is unaffected — it lives on a separate branch and does not
touch any of these paths.
hyperpolymath added a commit that referenced this pull request May 25, 2026
…adoc (#359)

## Summary

Phase T-1 of the repo-tidy stack the owner requested ("tidy of the repo
and cleanup of any mess so it is all tidy and readable"). Three
pure-rename / delete operations:

1. **`AI.a2ml` → `0-AI-MANIFEST.a2ml`** — clears the standing Hypatia
HIGH finding `root_hygiene "Stray AI.a2ml in root -- use
0-AI-MANIFEST.a2ml only"` and matches the sibling-repo convention
(`road-skate/`, `affinescript-vite/`, `affinescriptiser/` already carry
`0-AI-MANIFEST.a2ml`). Content preserved verbatim; a canonical-structure
refresh (the sibling template's STOP-banner format declaring
canonical-location invariants) is deferred to a later tidy phase to keep
this PR reviewable.
2. **`AI.djot` deleted** — clears the Hypatia HIGH finding `root_hygiene
"Superseded by 0-AI-MANIFEST.a2ml"`. The same project metadata is
already covered by `0-AI-MANIFEST.a2ml` + the six
`.machine_readable/6a2/*.a2ml` files it points at.
3. **`docs/TECH-DEBT-alt.adoc` → `docs/TECH-DEBT.adoc`** — restores the
canonical filename every cross-link in the repo already points at
(`META.a2ml`, `STATE.a2ml`, `CAPABILITY-MATRIX.adoc`, `ECOSYSTEM.adoc`,
`RESCRIPT-ELIMINATION.adoc`, `STDLIB-EXTERN-AUDIT.adoc/.a2ml`,
`docs/specs/TYPED-WASM-ROADMAP.adoc`). PR #356 had appended `-alt`
during the #351 split to avoid a merge conflict; with #351 resolved via
#355/#356 the alt suffix is dead weight and every existing cross-link
was silently broken.

Incidental: one stale path in `CONTRIBUTING.md`'s repo-layout block
updated `AI.a2ml` → `0-AI-MANIFEST.a2ml`.

## Hypatia delta (expected)

Before this PR the standing scan reports two HIGH `root_hygiene`
findings against this exact pair of files. They should drop on the next
scan, taking the totals from the 143-finding baseline down to ~141. The
TypeScript-exemption findings under `affinescript-deno-test/` are out of
scope for this PR — they're documented carve-outs in `.claude/CLAUDE.md`
§"TypeScript Exemptions (Approved)" and the policy check has no
allowlist for them.

## Test plan

- [ ] CI `governance / Language / package anti-pattern policy` and
`vscode-smoke` remain at their pre-existing baseline-failure state
(these are the documented known-failing checks in `.claude/CLAUDE.md`
§"Known-failing baseline checks"; not introduced or worsened by this
PR).
- [ ] `build`, `lint`, `migration-assistant`, `governance / Workflow
security linter`, `governance / Security policy checks`, `governance /
Well-Known (RFC 9116 + RSR)`, `governance / Code quality + docs`,
`governance / Guix primary / Nix fallback policy`, `Semgrep OSS`,
`CodeQL`, `Hypatia`, `analyze (actions, none)`,
`enforce-lowercase-stdlib`, `spark-theatre-gate` all green.
- [ ] The next Hypatia scan comment drops the two `AI.a2ml` / `AI.djot`
HIGH lines.

## Stack

This is part of a stack the owner authorised — see issue thread for the
wider scope. Subsequent phases land on separate branches off `main`:

- **T-2** — delete out-of-scope game files (`DAMAGE-SYSTEM.md`,
`CONTROLS-REFERENCE.md`, `GAME-BUNDLING-STRATEGY.md`).
- **T-3** — move loose root docs (`ABI-FFI-README.md`,
`ALPHA-1-RELEASE-NOTES.md`, `BACKEND-*`, `COMPILER-CAPABILITIES.md`,
`KNOWN-ISSUES.md`, `LICENSING-GUIDE.md`, `NAVIGATION.adoc`,
`PROOF-NEEDS.md`, `ROADMAP.adoc`, `SECURITY-SETUP.md`, `EXPLAINME.adoc`,
`RSR_OUTLINE.adoc`) into the existing `docs/` subtree.
- **T-4** — add `RSR_COMPLIANCE.adoc` + `STATE.scm` per RSR template.
- **T-5** — refresh `wiki/`.
- **T-6** — issue/PR triage pass.

Phase 2c (#357) is on a separate branch and unaffected by this PR.

---
_Generated by [Claude
Code](https://claude.ai/code/session_01WNkH8UucP3PppG5R36kGcu)_

Co-authored-by: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

2 participants