GeezerVison

The World Wide Web, restored to 800 pixels of glory.

GeezerVison is showing github.com — feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on while/for (Refs #177) by hyperpolymath · Pull Request #396 · hyperpolymath/affinescript

Conversation

hyperpolymath commented May 26, 2026 •

edited

Loading

Uh oh!

There was an error while loading. Please reload this page.

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.

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.

All reactions

hyperpolymath enabled auto-merge (squash)

May 26, 2026 22:20

This was referenced May 26, 2026

feat(borrow): CORE-01 Slice D (#177 pt3) — reject @linear capture by closure at borrow check #397

Merged

docs(adr): ADR-022 — origin variables + Polonius-style loan solver (Refs #177) #398

Closed

hyperpolymath commented May 27, 2026

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).

All reactions

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.

hyperpolymath mentioned this pull request

May 27, 2026

docs: session handoff 2026-05-27 — borrow deferred-items roundup (humans + machines) #401

Merged

3 tasks

hyperpolymath added a commit that referenced this pull request

May 27, 2026


          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) <[email protected]>


          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) <[email protected]>

hyperpolymath changed the title ~~feat(borrow): CORE-01 Slice C' (#177 pt3) — loop soundness via 2-iteration + StmtAssign clear-on-rewrite~~ feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on while/for (Refs #177)

May 27, 2026

hyperpolymath force-pushed the core-01/slice-c-prime-loop branch from 6c4f3de to 3ffb940 Compare

May 27, 2026 01:21

hyperpolymath merged commit 21edc15 into main

May 27, 2026

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


          feat(borrow): CORE-01 Slice D (#177 pt3) — reject @linear capture by …

02a5914

…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) <[email protected]>

hyperpolymath mentioned this pull request

May 30, 2026

docs(tech-debt): mark CORE-01 (S1) borrow-checker Phase-3 DONE — closes #177 #473

Merged

3 tasks

hyperpolymath added a commit that referenced this pull request

May 30, 2026


          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) <[email protected]>

hyperpolymath mentioned this pull request

Jun 1, 2026

Proof: borrow-graph soundness (no use-after-move + no conflict + BorrowOutlivesOwner) #515

Open

Reviewers

No reviews

Uh oh!

There was an error while loading. Please reload this page.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Uh oh!

There was an error while loading. Please reload this page.

1 participant

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.

You are visitor 01402503 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.

GeezerVison

Conversation

hyperpolymath commented May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

What lands

Three new fixtures

Comment update

Coordination

Uh oh!

hyperpolymath commented May 27, 2026

Parallel-work review (from #399)

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

Suggested fix

Note on the loop-soundness half

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

hyperpolymath commented May 26, 2026 •

edited

Loading

Uh oh!

There was an error while loading. Please reload this page.