Skip to content

feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on while/for (Refs #177) - #396

Merged
hyperpolymath merged 1 commit into
mainfrom
core-01/slice-c-prime-loop
May 27, 2026
Merged

feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on while/for (Refs #177)#396
hyperpolymath merged 1 commit into
mainfrom
core-01/slice-c-prime-loop

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented May 26, 2026

Copy link
Copy Markdown
Owner

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 fix(borrow): whole-place assignment clears move-record (Refs #177) #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.

@hyperpolymath

Copy link
Copy Markdown
Owner Author

Parallel-work review (from #399)

I drafted the StmtAssign-half of this fix in #399 before noticing this PR existed. Per maintainer direction we're keeping both open as parallel implementations. This PR is a superset (it also does the loop-soundness 2-iteration pass that #399 does not). The comment below flags one real soundness divergence in the StmtAssign half.

Sub-place writes silently clear move-records on the parent

Current StmtAssign change:

let* () = match find_aliasing_exclusive state place with
  | Some b ->
    Error (UseWhileExclusivelyBorrowed (place, b, expr_span lhs))
  | None -> Ok ()
in
...
state.moved <-
  List.filter (fun mr ->
    not (places_overlap place mr.m_place)
  ) state.moved;

This unconditionally (a) skips the find_move check and (b) clears any overlapping move-record. That's correct for whole-place writes (x = e — the place is rebound, the prior move is no longer load-bearing). It is unsound for sub-place writes because places_overlap is root-coarse: places_overlap x.f x = true.

Concretely:

fn unsound() -> Point {
  let x = Point { ... };
  drop_point(x);  // move x
  x.f = 5;        // currently: silently accepted, move-record on x cleared
  x               // currently: silently accepted (x treated as un-moved)
}

The semantics: after move x, the struct x is consumed — it does not exist. Writing x.f = 5 is writing through a dangling pointer, and clearing the move-record on x (because places_overlap(x.f, x) = true) then revives x for reads of the moved-out value. Both should be UseAfterMove.

None of the three fixtures here exercise sub-place writes after moves, so CI doesn't catch this:

  • slice_c_prime_loop_sound.affine — counted loop, no moves
  • slice_c_prime_loop_reinit_ok.affine — whole-place reassign (x = 42)
  • slice_c_prime_loop_move_persists.affine — whole-place, no reassign

Suggested fix

#399 uses an is_whole_place_write predicate to gate both the move-check skip and the move-record clearing:

let is_whole_place_write =
  match place with PlaceVar _ -> true | _ -> false
in
let* () =
  if is_whole_place_write then
    match find_aliasing_exclusive state place with
    | Some b -> Error (UseWhileExclusivelyBorrowed (place, b, expr_span lhs))
    | None -> Ok ()
  else
    check_use state place (expr_span lhs)
in
...
if is_whole_place_write then
  state.moved <-
    List.filter (fun mr -> not (places_overlap mr.m_place place))
      state.moved;

This preserves the loop-reinit semantics this PR needs (whole-place reassign clears the move) while keeping x.f = / x[i] = sub-place writes subject to check_use. A new fixture along the lines of:

fn subplace_after_move_still_rejected() -> Unit {
  let p = make_point();
  drop_point(p);
  p.x = 5;  // expect: UseAfterMove
  ()
}

would pin the anti-regression.

Note on the loop-soundness half

The 2-iteration check + state-restore in StmtWhile/StmtFor is independent of the StmtAssign hole and looks correct from a quick read — running the body twice from the iter-1-post snapshot, then restoring to iter-1-post for post-loop state. The fixtures cover the three load-bearing cases (counted, re-init, unrestored-move).

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>
…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 hyperpolymath changed the title feat(borrow): CORE-01 Slice C' (#177 pt3) — loop soundness via 2-iteration + StmtAssign clear-on-rewrite May 27, 2026
@hyperpolymath
hyperpolymath force-pushed the core-01/slice-c-prime-loop branch from 6c4f3de to 3ffb940 Compare May 27, 2026 01:21
@hyperpolymath
hyperpolymath merged commit 21edc15 into main May 27, 2026
@hyperpolymath
hyperpolymath deleted the core-01/slice-c-prime-loop branch May 27, 2026 01:21
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