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
Copy link
Copy Markdown
Owner

@hyperpolymath hyperpolymath commented May 26, 2026

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
Copy link
Copy Markdown
Owner Author

hyperpolymath commented May 26, 2026

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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@hyperpolymath