Skip to content

fix(borrow): whole-place assignment clears move-record (Refs #177) - #399

Merged
hyperpolymath merged 1 commit into
mainfrom
core-01/assign-clears-move
May 27, 2026
Merged

fix(borrow): whole-place assignment clears move-record (Refs #177)#399
hyperpolymath merged 1 commit into
mainfrom
core-01/assign-clears-move

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented May 26, 2026

Copy link
Copy Markdown
Owner

Summary

StmtAssign in lib/borrow.ml treated the LHS as a read — every assignment ran check_use on its target, so let mut x; drop(x); x = …; use(x) was spuriously rejected with UseAfterMove even though the new value should revive the place.

This is the assignment-clears-move imprecision called out in the deferred-items comment at lib/borrow.ml:1483, the StmtAssign half of the Slice C' pairing the comment described. Decouples cleanly from loop-soundness (the other half) — that work can now proceed independently against this baseline.

What changes

  • lib/borrow.ml StmtAssign: gate find_move on a is_whole_place_write predicate (place is PlaceVar). Whole-place writes skip the use-check (keeping the exclusive-borrow aliasing check) and drop any overlapping move-record after the RHS is validated. Sub-place writes (x.f =, x[i] =) keep check_use because they navigate through a parent that must still be live.
  • Deferred-items comment updated (lib/borrow.ml:1496): notes that the StmtAssign half is landed; loop-soundness half now proceeds standalone.
  • New e2e fixture + test asserting the Ok case end-to-end (borrow_assign_clears_move.affine).

Anti-regression coverage

These existing tests pin the precision boundary; all still pass:

Fixture Pins
borrow_nll_still_rejects_live_borrow.affine (Slice A) Assignment to a place with a live shared borrow still errors MoveWhileBorrowed.
slice_c_body_move_persists.affine (Slice C) A moved local that is not reassigned still errors UseAfterMove on later reads.

Suite: 328 / 328 with the new case (327 before).

What is not changed

  • Sub-place writes' move semantics. x.f = … after move x still errors — the coarse places_overlap granularity treats moves at root level, so writing one field doesn't revive the others. That's the existing model.
  • Ref-binding / Slice B logic. The pre_release + ref-graph rebind path is untouched; the new move-record clearing happens after the RHS check, alongside (not instead of) the existing ref-graph rebind.

Notes for the maintainer

  • Auto-merge cannot be armed on drafts. When ready, run: 
    gh pr ready <PR#> && gh pr merge <PR#> --auto --squash --delete-branch
  • Drafted off fresh origin/main (1a57163). No conflicts expected with the Polonius/ADR work in flight on core-01/polonius-adr (docs(adr): ADR-022 — origin variables + Polonius-style loan solver (Refs #177) #398) — that one only touches type_expr / META.a2ml / docs and a single residual-TODO line; this PR touches check_stmt and its tests.

🤖 Generated with Claude Code
@hyperpolymath

hyperpolymath commented May 26, 2026

Copy link
Copy Markdown
Owner Author

Auto-merge cannot be armed on a draft. Owner one-liner for ratification:

gh pr ready 399 && gh pr merge 399 --auto --squash --delete-branch
This was referenced May 27, 2026
Merged
Merged
Merged
hyperpolymath added a commit that referenced this pull request May 27, 2026
@hyperpolymath @claude
docs: session handoff 2026-05-27 — borrow deferred-items roundup (hum…
f6782c4 
…ans + machines) (#401)

## Summary

Documents the entire round of work across **six open PRs** that together
cover the four entries in the \`lib/borrow.ml\` deferred-items comment
at lines 1483-1505. Two artefacts, one for each audience.

### For humans — \`docs/history/SESSION-HANDOFF-2026-05-27.adoc\`

\`.adoc\` per the repo's DOC-FORMAT rule. Sections:

- What this session actually did
- **Parallel-implementation map** — which of my PRs paired with which
existing PR
- PR state table (draft? auto-merge? mergeability?)
- **Audit findings** — the load-bearing deltas: self-assign hole +
return-escape gap (#395), sub-place soundness divergence (#396),
Cmd-typed-param tracking gap (#397)
- **Safe-to-close conditions per PR** — the matrix the next agent needs
- Cleanup performed
- Guidance for the next agent

### For machines —
\`.machine_readable/sessions/2026-05-27-borrow-deferred-items.a2ml\`

New \`sessions/\` subdirectory (the existing \`.machine_readable/6a2/\`
is the canonical state-snapshot dir; sessions are per-event records).
Schema declared as \`a2ml/session-record/v1\`. Structured records:

- One \`[[deferred-item]]\` per entry in the comment block
- One \`[[open-pr]]\` per the six PRs
- One \`[[close-condition]]\` per PR with fallback paths
- \`[cleanup]\`, \`[lessons]\` blocks

### Cleanup landed alongside

- \`.git/gc.log\` removed after \`git prune\` (the persistent
\"unreachable loose objects\" warning is gone).
- Two stale parallel-Claude untracked dirs (\`affinescript-vite/\`,
\`editors/vscode/node_modules/\`) **not touched** — they're not this
session's work.

## What's NOT in this PR

- No \`lib/\` changes. No \`test/\` changes.
- No closes/state-changes on the six open PRs
(#395/#396/#397/#398/#399/#400). Per maintainer direction \"keep both PR
sets open\", parallel implementations stay parallel.
- No edits to \`STATE.a2ml\` or other \`6a2/\` files — those are flagged
STALE and updating them is a separate disciplined task.

## Safe-to-close ledger (also in the docs)

| PR | Close condition | Fallback |
|---|---|---|
| **#395** | auto-merge fires once CI clears | n/a |
| **#396** | auto-merge fires once CI clears | if merges without
sub-place fix, **#399** stays open as follow-up |
| **#397** | auto-merge fires once CI clears | audit posted a must-fix;
owner can incorporate or file follow-up |
| **#398** | owner ratifies ADR-022 via the posted one-liner |
do-not-close — only deferred-item that needs an architectural change |
| **#399** | **#396** merges with sub-place fix | rebase as sub-place
soundness correction |
| **#400** | **#395** merges with self-assign-guard + return-escape test
| rebase as follow-up adding the two missing pieces |
| **this PR** | safe to close once merged | n/a — pure docs |

## Test plan

- [ ] CI green (this PR only touches \`docs/\` and
\`.machine_readable/\` — no test-relevant code).
- [ ] \`asciidoctor docs/history/SESSION-HANDOFF-2026-05-27.adoc\`
renders without errors (if you have asciidoctor installed; CI doesn't
enforce).
- [ ] The \`docs/history/SESSION-HANDOFF-2026-05-27.adoc\`
cross-references in the body resolve to actual PR numbers / file paths
in the repo.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath @claude
fix(borrow): whole-place assignment clears move-record (Refs #177)
9d919c5 
`x = e` where LHS is a `PlaceVar` is a *write*, not a read.  Pre-fix,
StmtAssign called `check_use` on the LHS, which fired `UseAfterMove`
whenever `x` had been moved earlier — spuriously rejecting `let mut x;
drop(x); x = …; use(x)`.  This is the assignment-clears-move imprecision
called out in the deferred-items comment at lib/borrow.ml:1483, the
StmtAssign half of the Slice C' pairing.

Whole-place writes now skip `find_move` (keeping the exclusive-borrow
aliasing check) and drop any overlapping move-record after the RHS is
validated, reviving the place for subsequent uses.  Sub-place writes
(`x.f =`, `x[i] =`) keep `check_use` because they navigate through a
parent that must still be live.

Anti-regression preserved:
  - borrow_nll_still_rejects_live_borrow.affine (Slice A): assignment
    to a place with a live shared borrow still errors MoveWhileBorrowed.
  - slice_c_body_move_persists.affine (Slice C): a moved local that is
    NOT reassigned still errors UseAfterMove on later reads.
  - 327 prior tests, all green (328/328 with the new case).

Loop-soundness (Slice C' StmtWhile/StmtFor) can now proceed
independently — comment at lib/borrow.ml:1496 updated accordingly.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath
hyperpolymath force-pushed the core-01/assign-clears-move branch from 9e01952 to 9d919c5 Compare May 27, 2026 01:15
@hyperpolymath
hyperpolymath marked this pull request as ready for review May 27, 2026 01:15
@hyperpolymath
hyperpolymath merged commit e73067d into main May 27, 2026
9 of 16 checks passed
@hyperpolymath
hyperpolymath deleted the core-01/assign-clears-move branch May 27, 2026 01:15
hyperpolymath added a commit that referenced this pull request May 27, 2026
@hyperpolymath @claude
fix(borrow): self-assign guard + return-escape coverage for ref-to-re…
2b8aa0b 
…f (Refs #177, follow-up to #395) (#400)

## Summary

Two deltas on top of #395's ref-to-ref binding work, surfaced by the
audit posted on #395 at the time it merged. **This PR was the original
parallel implementation; it has been rewritten as a thin follow-up now
that #395 covered the broader scope.**

### 1. Self-assign `r = r` guard

Without this guard, `is_reborrow_source` reports true for the ref-binder
LHS=RHS case → `pre_release` ends `r`'s borrow and removes the binding →
post-rebind calls `ref_source_borrow` which now finds `r` unbound and
returns None → net effect is `r` silently stripped from the
borrow-graph.

Pathological in practice (`r = r` is dead code) but a silent unsoundness
rather than a no-op. The guard short-circuits `pre_release` when the
RHS's source binder is the LHS binder itself.

### 2. Return-escape via indirection (new test)

The strongest proof that `record_ref_binding`'s delegation to
`ref_source_borrow` works is `return r2` where `r2 = r1 = &local` —
pre-fix this slipped past `returned_borrow`'s `ref_bindings` lookup.

The three fixtures landed in #395 (`let_aliases`, `protects_owner`,
`assign_aliases`) don't exercise the return-escape code path, which is
historically the most-leaked surface for this class of bug. New fixture
`test/e2e/fixtures/ref_to_ref_return_escape.affine` pins it — expects
`BorrowOutlivesOwner`.

## Tests

- 331 prior tests + 1 new = **332/332 green**
- No changes to `lib/borrow.ml` behaviour for any code path other than
the self-assign edge case.

## Coordination

- Rebased onto current main (post-#395 + post-#399). Force-pushed.
- GPG-signed.
- This was originally the parallel implementation of #395. After #395
merged via admin-merge during the deferred-items roundup, this PR was
rewritten to contain only the two deltas the audit flagged.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 27, 2026
@hyperpolymath @claude
feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on …
3ffb940 
…while/for (Refs #177)

Rebased reduction of the original Slice C' PR. The StmtAssign
clear-on-rewrite half is dropped — that work landed in #399 with a
strictly better `is_whole_place_write` predicate (whole-place writes
clear the move; sub-place writes still apply `check_use`).  This PR
keeps only the loop-soundness piece.

What lands:

  - `StmtWhile` / `StmtFor`: run cond+body once, snapshot state-fields,
    run cond+body a second time from the post-iter-1 state.  Any move
    the body didn't restore surfaces as UseAfterMove on the 2nd pass.
    State is restored to the iter-1-post snapshot for post-loop
    analysis (the loop may execute 0..N times — iter-1-post is the
    sound choice when iter-2 doesn't add new conflicts).

  - Pairs with #399's clear-on-rewrite to make legitimate re-init
    loops accept: iter 1 moves and reassigns, iter 2 sees the
    reassigned (cleared) state.

Three new fixtures pin the cases:

  - `slice_c_prime_loop_sound.affine` — counted loop, no moves: Ok
    (anti-regression against the 2-iter pass introducing false
    positives).
  - `slice_c_prime_loop_reinit_ok.affine` — move + immediate rebind:
    Ok (the #399 × Slice C' interaction).
  - `slice_c_prime_loop_move_persists.affine` — move without rebind:
    Error UseAfterMove (the soundness gain).

Suite: **335/335 green** (332 prior + 3 new).

Deferred-items comment at `lib/borrow.ml:1483` updated — loop-
soundness entry removed, only Polonius and captured-linears Slice D
remain.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 27, 2026
@hyperpolymath @claude
feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on …
21edc15 
…while/for (Refs #177) (#396)

## Summary

**Rebased reduction.** The original PR coupled loop-soundness with a
StmtAssign clear-on-rewrite. The StmtAssign half is now dropped — that
work landed in #399 with a strictly better `is_whole_place_write`
predicate (whole-place writes clear the move; sub-place writes still
apply `check_use`, which #396's original blanket skip got wrong).

This PR keeps only the loop-soundness piece.

## What lands

- `StmtWhile` / `StmtFor`: run cond+body once, snapshot state-fields,
run cond+body a second time from the post-iter-1 state. Any move the
body didn't restore surfaces as `UseAfterMove` on the 2nd pass.
- State is restored to the iter-1-post snapshot for post-loop analysis
(the loop may execute 0..N times — iter-1-post is the sound choice when
iter-2 doesn't add new conflicts).
- Pairs with #399's clear-on-rewrite so legitimate re-init loops accept:
iter 1 moves and reassigns, iter 2 sees the reassigned state.

## Three new fixtures

| Fixture | Asserts |
|---|---|
| `slice_c_prime_loop_sound.affine` | Counted loop, no moves: Ok
(anti-regression against false positives) |
| `slice_c_prime_loop_reinit_ok.affine` | Move + immediate rebind: Ok
(the #399 × Slice C' interaction) |
| `slice_c_prime_loop_move_persists.affine` | Move without rebind: Error
UseAfterMove (the soundness gain) |

**Suite: 335/335 green** (332 prior + 3 new).

## Comment update

Deferred-items at `lib/borrow.ml:1483` — loop-soundness entry removed;
only Polonius (origin-vars) and captured-linears Slice D remain.

## Coordination

Force-pushed onto current main (post-#395, post-#399, post-#400,
post-#401). GPG-signed.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath mentioned this pull request May 30, 2026
Merged
3 tasks
hyperpolymath added a commit that referenced this pull request May 30, 2026
@hyperpolymath @claude
docs(tech-debt): mark CORE-01 (S1) borrow-checker Phase-3 DONE — closes
e8978a7 
#177 (#473)

## Summary

- Refresh `docs/TECH-DEBT.adoc` CORE-01 row: ledger listed Slices C' / D
/ ref-to-ref binding as residual, but those landed (PRs #395 / #396 /
#397).
- Flip the Stage D ASCII status from `ACTIVE` to `CLOSED`.
- Mark the row `CLOSED 2026-05-30`; remaining residual is scoped
exclusively to ADR-022 (Polonius origin/region variables) which is a
separate, ADR-gated workstream filed at
`docs/decisions/0022-polonius-origin-variables.adoc` (PR #407).

## Why now

#177 was the issue tracking CORE-01 Phase-3 (borrow-graph validation,
S1). The stated scope — adding graph validation plus regression fixtures
under `tests/` — has shipped:

- **Code:** `lib/borrow.ml:1635-1715` documents pt1 + pt2 (return-escape
+ `&mut` parser surface) + pt3 Slices A (NLL last-use) / B
(flow-sensitive re-assignment) / C-light (CFG-join for
`ExprHandle`/`ExprTry`) / C' (loop soundness) / D (linear-capture by
closure) + ref-to-ref binding.
- **Tests:** `test/test_e2e.ml` "E2E Borrow Graph" suite — **28 hermetic
regression tests** (covering each landed slice with positive +
anti-regression cases).
- **Slices that landed since the ledger was last updated:** #395
(ref-to-ref binding), #396 (Slice C' loop soundness), #397 (Slice D
linear-capture), #399 (whole-place assignment clears moves), #400
(self-assign guard + return-escape coverage for ref-to-ref).
- **ADR-022 (#407):** Polonius origin/region variables — architectural
change to the type system. M1–M4 migration plan in the ADR; lexical
checker is the merge oracle through M3.

## Build oracle

Local toolchain has an unrelated cross-installation OCaml conflict
(`astring.cmxa` from opam vs system `stdlib.cmxa`); using CI-on-main as
oracle instead.

CI green on `main` at `4f0f3ca7` (2026-05-30 15:19Z) with all CORE-01
work present.

## Test plan

- [ ] CI green on this branch
- [ ] No code in the diff; doc-only change (no behaviour impact)
- [ ] `Closes #177` link resolves on merge

Closes #177.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

Labels

None yet

1 participant

@hyperpolymath