Skip to content

feat(borrow): CORE-01 ref-to-ref binding (#177 pt3) — let r2 = r / r = s alias the borrow-graph - #395

Merged
hyperpolymath merged 1 commit into
mainfrom
core-01/ref-to-ref-binding
May 27, 2026
Merged

feat(borrow): CORE-01 ref-to-ref binding (#177 pt3) — let r2 = r / r = s alias the borrow-graph#395
hyperpolymath merged 1 commit into
mainfrom
core-01/ref-to-ref-binding

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Summary

Closes the documented reborrow-through-indirection gap (the first item under "Still deferred" at the bottom of lib/borrow.ml). let r2 = r and r = s — where the RHS is itself a ref-binder, not a direct &place/&mut place — now extend the borrow-graph correctly.

  • New ref_source_borrow helper: unifies the &p / &mut p / ref-var lookup so record_ref_binding (let path) and the StmtAssign reborrow block both see one extra level of indirection.
  • New is_reborrow_source shape-only test: drives the pre-release decision on the assign path without consulting live borrow state.
  • expire_dead_ref_bindings now reference-counts borrows by b_id across surviving aliases — a borrow is ended only when no live ref-binder still holds it. This was the load-bearing fix: pre-change, let r = &x; let r2 = r would correctly alias r2 then drop the underlying borrow when r died, silently re-permitting writes to x.

Refs

Test plan

  • dune runtest --force — 327 → 330 tests, 0 failures
  • 3 new e2e fixtures + handlers:
    • ref_to_ref_let_aliases.affine — positive let-path (let r = &x; let r2 = r; *r + *r2)
    • ref_to_ref_protects_owner.affine — anti-regression (write to owner while alias is live must be rejected)
    • ref_to_ref_assign_aliases.affine — positive assign-path (r = s where s is a ref-binder)
  • No regression in existing borrow / Slice A / Slice B / Slice C fixtures

🤖 Generated with Claude Code

…r = s now alias the borrow-graph

Closes the reborrow-through-indirection gap documented at
lib/borrow.ml's "Still deferred" comment:

  - `let r2 = r` (where r is itself a ref-binder) now copies r's
    borrow-graph entry to r2 via a new `ref_source_borrow` helper.
    Pre-fix, the alias was never recorded — r2 had no entry, so
    subsequent uses of *r2 lost protection of the underlying owner.
  - `r = s` (assignment, RHS = another ref-binder) now goes through
    the same Slice B pre-release + re-alias path that already
    handles `r = &y`.  `is_reborrow_source` unifies the &p / &mut p
    / ref-var shape test.
  - `expire_dead_ref_bindings` now reference-counts borrows by
    `b_id` across surviving bindings: a borrow is ended only when
    no live ref-binder still aliases it.  This was the load-bearing
    fix — without it, `let r = &x; let r2 = r` would correctly
    record r2 but then drop the borrow when r died, silently
    re-permitting writes to x while r2 was still in flight.

Tests (+3, all green):
  - ref_to_ref_let_aliases: positive let-path
  - ref_to_ref_protects_owner: anti-regression (assign through
    owner while alias is live must be rejected)
  - ref_to_ref_assign_aliases: positive assign-path mirror of
    slice_b_outer_assign_releases_old with RHS = ref-var

Gate: 327 → 330 tests, 0 failures under `dune runtest --force`.

Refs #177, CORE-01 pt3 (ref-to-ref).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath

Copy link
Copy Markdown
Owner Author

Parallel-work review (from #400)

I drafted the same fix in #400 before noticing this PR existed. Per maintainer direction we're keeping both open as parallel implementations. This comment surfaces the two deltas that #400 has and this PR doesn't:

1. r = r self-assignment unbinds r

The current pre_release logic in StmtAssign:

match root_var place with
| Some binder_sym
  when is_reborrow_source state symbols rhs
    && List.mem_assoc binder_sym state.ref_bindings ->
  let old_borrow = List.assoc binder_sym state.ref_bindings in
  end_borrow state old_borrow;
  ...

When LHS = RHS = r (both resolve to the same ref-binder symbol), is_reborrow_source returns true and pre_release fires — ends r's borrow and removes r from ref_bindings. Then post-rebind calls ref_source_borrow rhs for r, which now finds r unbound and returns None. Net effect: r = r (a no-op assignment) silently strips r's borrow-graph entry and leaves the underlying place unprotected.

#400 guards this case explicitly:

let rhs_is_self =
  match peel rhs with
  | ExprVar id ->
    (match lookup_symbol_by_name symbols id.name with
     | Some sym -> sym.Symbol.sym_id = binder_sym
     | None -> false)
  | _ -> false
in
if rhs_is_self then None else ...

Pathological in practice (r = r is dead code), but it's a silent unsoundness rather than a no-op.

2. Missing return-escape coverage

The strongest proof that the let-graph propagation works is return r2 where r2 = r1 = &local — pre-fix this slipped past returned_borrow's ref_bindings lookup. #400's borrow_reborrow_indir_escape.affine pins it:

fn esc_via_indir() -> ref Int {
  let x = 5;
  let r1 = &x;
  let r2 = r1;
  return r2;
}

Expected: BorrowOutlivesOwner. The current 3 fixtures here (let_aliases, protects_owner, assign_aliases) cover positive let, anti-regression-on-write, and positive assign — they don't exercise the return-escape code path, which is the historically most-leaked path for this class of bug.

Note

The multi-binder gate in expire_dead_ref_bindings here and in #400 is byte-identical (same b'.b_id = b.b_id check). No delta there.

If the owner prefers this PR's structure (separate is_reborrow_source pre-check + ref_source_borrow post-check), folding the two items above is a ~10-line addition.

@hyperpolymath
hyperpolymath merged commit 1efc3f3 into main May 27, 2026
10 of 17 checks passed
@hyperpolymath
hyperpolymath deleted the core-01/ref-to-ref-binding branch May 27, 2026 01:00
hyperpolymath added a commit that referenced this pull request May 27, 2026
…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 added a commit that referenced this pull request May 27, 2026
…f (Refs #177, follow-up to #395)

Two deltas on top of #395's ref-to-ref binding work, surfaced by the
audit at the time #395 landed:

1. **Self-assign `r = r` guard in StmtAssign.** Without it,
   `is_reborrow_source` reports true for the ref-binder LHS=RHS case,
   `pre_release` ends `r`'s borrow and removes the binding, then
   post-rebind calls `ref_source_borrow` which 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 test fixture + 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`).

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.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 27, 2026
…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
…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 added a commit that referenced this pull request May 27, 2026
…closure at borrow check (#397)

## Summary

Tighter integration with the quantity checker for captured linears: the
borrow checker now refuses to let a closure capture a @linear (QOne)
binding. Pre-Slice-D, this case fell only to the quantity checker (which
scales lambda captures by QOmega and emits
\`LinearVariableUsedMultiple\`); now the same constraint fires earlier
in the pipeline (Typecheck → Borrow → Quantity) with a diagnostic that
points at the **lambda span** — the actual capture site — rather than
the downstream "used multiple times" message.

## Mechanism

- New \`state.linear_bindings\` tracks sym-ids of @linear bindings
declared in the current function: explicit \`@linear\` annotations on
\`let\`-statements and \`let\`-expressions, \`@linear\` function params,
and \`let x: Cmd[T] = …\` (linear-by-construction per ADR-002).
- At \`ExprLambda\`, the free-var walk now also looks up each captured
name's symbol and rejects with \`LinearCapturedByClosure(name,
lambda_span)\` if the sym-id is in \`linear_bindings\`.
- The Shared-borrow creation for non-linear captures is unchanged.

## Refs

- #177 (CORE-01 pt3)
- Third of three small slices being landed today; #395 (ref-to-ref) and
#396 (Slice C') are in flight. **Slice C-full (Polonius) is being handed
off to a separate Claude** — prompt incoming separately.

## Test plan

- [x] \`dune runtest --force\` — 327 → **330 tests, 0 failures**
- [x] 3 new e2e fixtures + handlers:
- \`slice_d_captured_linear_let_rejected.affine\` — \`@linear let x;
fn() => x + 1\` → \`LinearCapturedByClosure("x", _)\`
- \`slice_d_captured_linear_param_rejected.affine\` — \`fn foo(@linear
y: Int) { let f = fn() => y + 1; … }\` → \`LinearCapturedByClosure("y",
_)\`
- \`slice_d_captured_nonlinear_ok.affine\` — anti-regression: non-linear
capture must still pass

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 30, 2026
#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