Claude/pr351 no techdebt#355
Merged
Merged
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.
This removes TECH-DEBT.adoc, CAPABILITY-MATRIX.adoc, and STATE.a2ml changes so PR #351 can merge cleanly. Documentation will be updated separately after the code changes are merged.
🔍 Hypatia Security ScanFindings: 118 issues detected
View findings[
{
"reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
"type": "banned",
"file": "AI.a2ml",
"action": "delete",
"rule_module": "root_hygiene",
"severity": "high"
},
{
"reason": "Superseded by 0-AI-MANIFEST.a2ml",
"type": "banned",
"file": "AI.djot",
"action": "delete",
"rule_module": "root_hygiene",
"severity": "high"
},
{
"reason": "Issue in quality.yml",
"type": "missing_workflow",
"file": "quality.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in security-policy.yml",
"type": "missing_workflow",
"file": "security-policy.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Action actions/checkout@v6 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "TypeScript file detected -- banned language",
"type": "banned_language_file",
"file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/example/smoke_driver.ts",
"action": "flag",
"rule_module": "cicd_rules",
"severity": "critical"
},
{
"reason": "TypeScript file detected -- banned language",
"type": "banned_language_file",
"file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/cli.ts",
"action": "flag",
"rule_module": "cicd_rules",
"severity": "critical"
},
{
"reason": "TypeScript file detected -- banned language",
"type": "banned_language_file",
"file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/mod.ts",
"action": "flag",
"rule_module": "cicd_rules",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
3 tasks
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
2 participants
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.
No description provided.