Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
May 27, 2026
+382 −0
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
180 changes: 180 additions & 0 deletions .machine_readable/sessions/2026-05-27-borrow-deferred-items.a2ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,180 @@
# SPDX-License-Identifier: MPL-2.0
# SPDX-FileCopyrightText: 2026 hyperpolymath
#
# Session record — 2026-05-27 — lib/borrow.ml deferred-items roundup
#
# Human-readable companion: docs/history/SESSION-HANDOFF-2026-05-27.adoc
# Canonical comment in code: lib/borrow.ml:1483-1505

[metadata]
schema = "a2ml/session-record/v1"
session-date = "2026-05-27"
session-topic = "lib/borrow.ml CORE-01 #177 deferred-items roundup"
repo = "hyperpolymath/affinescript"
canonical-code-anchor = "lib/borrow.ml:1483-1505"
human-companion = "docs/history/SESSION-HANDOFF-2026-05-27.adoc"
parallel-sessions-detected = true
parallel-detection-method = "PR title cross-reference after PR creation"

# ── The four deferred-items entries ────────────────────────────────────
# Each entry tracks: which PR(s) address it, parallel-implementation
# overlap, and any audit findings.

[[deferred-item]]
id = "reborrow-through-indirection"
description = "let r2 = r1 / r2 = r1 where RHS is itself a ref-binder"
parallel-claude-pr = 395
my-pr = 400
overlap = "equivalent"
multi-binder-gate-byte-identical = true
my-pr-extra-coverage = ["self-assign-guard", "return-escape-fixture"]
audit-comment = "https://github.com/hyperpolymath/affinescript/pull/395#issuecomment-4550230871"

[[deferred-item]]
id = "loop-soundness-and-clear-on-rewrite"
description = "StmtAssign treats LHS as a use; loops need 2-iter convergence"
parallel-claude-pr = 396
my-pr = 399
overlap = "parallel-pr-is-superset"
parallel-pr-extra = ["loop-soundness-2-iteration"]
my-pr-extra = ["sub-place-write-soundness-fix"]
audit-finding-severity = "real-bug"
audit-finding-summary = "places_overlap is root-coarse, so x.f = e after move x silently clears the move-record on x"
audit-comment = "https://github.com/hyperpolymath/affinescript/pull/396#issuecomment-4550232584"
recommended-fix = "rebase #396 to incorporate is_whole_place_write predicate from #399"

[[deferred-item]]
id = "captured-linears-slice-d"
description = "reject @linear bindings captured by closures at borrow check"
parallel-claude-pr = 397
my-pr = ""
overlap = "none — I had no parallel PR"
audit-finding-severity = "real-bug"
audit-finding-summary = "param-path tracks only explicit @linear; misses Cmd[T]-typed params that let_is_linear would catch"
audit-hygiene-findings = [
"linear_bindings not snapshot/restored at block exit",
"linear_bindings not unified in merge_arm_results",
"borrow_quantity_of_ty's Cmd-inference branch unreached by any fixture"
]
audit-comment = "https://github.com/hyperpolymath/affinescript/pull/397#issuecomment-4550278071"

[[deferred-item]]
id = "origin-variables-polonius"
description = "true Polonius surface — region vars on TyRef/TyMut with datalog loan solver"
parallel-claude-pr = ""
my-pr = 398
overlap = "ADR-only — architectural; multi-week"
adr = "ADR-022"
adr-doc = "docs/decisions/0022-polonius-origin-variables.adoc"
m1-sketch-branch = "core-01/polonius-m1-sketch"
m1-sketch-commit = "b28757c"
m1-pushed = false
owner-ratify-one-liner = "gh pr ready 398 && gh pr merge 398 --auto --squash --delete-branch"

# ── Open-PR state at handoff ───────────────────────────────────────────

[[open-pr]]
number = 395
title = "feat(borrow): CORE-01 ref-to-ref binding (#177 pt3) — let r2 = r / r = s alias the borrow-graph"
draft = false
auto-merge = "SQUASH"
state = "BLOCKED on CI queue"
owner = "hyperpolymath"
parallel-pair-mine = 400
my-review = "https://github.com/hyperpolymath/affinescript/pull/395#issuecomment-4550230871"

[[open-pr]]
number = 396
title = "feat(borrow): CORE-01 Slice C' (#177 pt3) — loop soundness via 2-iteration + StmtAssign clear-on-rewrite"
draft = false
auto-merge = "SQUASH"
state = "BLOCKED on CI queue"
owner = "hyperpolymath"
parallel-pair-mine = 399
my-review = "https://github.com/hyperpolymath/affinescript/pull/396#issuecomment-4550232584"

[[open-pr]]
number = 397
title = "feat(borrow): CORE-01 Slice D (#177 pt3) — reject @linear capture by closure at borrow check"
draft = false
auto-merge = "SQUASH"
state = "BLOCKED on CI queue"
owner = "hyperpolymath"
parallel-pair-mine = ""
my-review = "https://github.com/hyperpolymath/affinescript/pull/397#issuecomment-4550278071"

[[open-pr]]
number = 398
title = "docs(adr): ADR-022 — origin variables + Polonius-style loan solver (Refs #177)"
draft = true
auto-merge = "OFF (drafts cannot arm)"
state = "BLOCKED on CI queue"
owner = "hyperpolymath"
ratify-one-liner = "gh pr ready 398 && gh pr merge 398 --auto --squash --delete-branch"

[[open-pr]]
number = 399
title = "fix(borrow): whole-place assignment clears move-record (Refs #177)"
draft = true
auto-merge = "OFF (drafts cannot arm)"
state = "BLOCKED on CI queue"
owner = "hyperpolymath"
parallel-pair-theirs = 396
close-condition = "#396 merges with sub-place soundness fix incorporated"

[[open-pr]]
number = 400
title = "fix(borrow): propagate ref-binding through reborrow indirection (Refs #177)"
draft = true
auto-merge = "OFF (drafts cannot arm)"
state = "BLOCKED on CI queue"
owner = "hyperpolymath"
parallel-pair-theirs = 395
close-condition = "#395 merges with self-assign-guard + return-escape-test incorporated"

# ── Safe-to-close ledger ──────────────────────────────────────────────

[[close-condition]]
pr = 400
condition = "#395 merges with self-assign-guard + return-escape-test"
fallback = "rebase onto main as follow-up adding the two missing pieces"

[[close-condition]]
pr = 399
condition = "#396 merges with sub-place soundness fix (is_whole_place_write predicate)"
fallback = "rebase onto main as sub-place soundness correction"

[[close-condition]]
pr = 398
condition = "owner ratifies ADR-022 via posted one-liner"
fallback = "do-not-close — only deferred-item that needs an architectural change"

[[close-condition]]
pr = 395
condition = "auto-merge fires once CI clears"
note = "owner-side; review comment is informational, not blocking"

[[close-condition]]
pr = 396
condition = "auto-merge fires once CI clears (with or without sub-place fix)"
followup-needed = "if-merges-without-fix"
followup-pr = 399

[[close-condition]]
pr = 397
condition = "auto-merge fires once CI clears"
note = "audit posted real-bug for Cmd-typed params; owner can incorporate or file follow-up"

# ── Cleanup performed this session ────────────────────────────────────

[cleanup]
git-gc-log-removed = true
git-prune-run = true
local-branches-kept = ["core-01/polonius-m1-sketch (b28757c, M1 sketch for ADR-022)"]

# ── Lessons for the next agent ────────────────────────────────────────

[lessons]
root-cause-of-duplicate-work = "previous-session-summary listed PRs only by status (MERGEABLE/BLOCKED), not by title; treated them as opaque siblings and re-did work"
mitigation = "before starting work on any open issue/area, gh pr list --state open and gh pr view <n> on every open PR in the touched area"
disambiguation-reminder = "AffineScript ≠ Ephapax; see feedback_affinescript_ephapax_siblings_not_impl_proof.md in user auto-memory"
202 changes: 202 additions & 0 deletions docs/history/SESSION-HANDOFF-2026-05-27.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,202 @@
// SPDX-License-Identifier: MPL-2.0
// SPDX-FileCopyrightText: 2026 hyperpolymath
= Session handoff — 2026-05-27 — `lib/borrow.ml` deferred-items roundup
:toc:
:toclevels: 2

[NOTE]
====
This session worked the four deferred-items entries at `lib/borrow.ml:1483-1505`
(the comment block beginning "Still deferred:") across multiple parallel Claude
sessions. The result is **six open PRs** that together cover the entire
deferred-items surface except origin-variables/Polonius, plus three formal
review comments documenting overlaps and audit findings. **Nothing is merged
yet** — everything is owner-gated either on draft-status or on the GitHub
Actions queue drain.
====

== What this session actually did

1. Drafted **ADR-022** at `docs/decisions/0022-polonius-origin-variables.adoc`
+ a structured `[[adr]]` block in `.machine_readable/6a2/META.a2ml`,
shipped as draft PR **#398**.
2. Cut a minimal **M1 sketch** for ADR-022 (`origin_var option` on
`TyRef`/`TyMut` + a `lib/borrow_polonius/` sublibrary skeleton) — kept
local on branch `core-01/polonius-m1-sketch` (commit `b28757c`), not
pushed pending ADR ratification.
3. Filed two more PRs landing scoped fixes for two of the four deferred-items
entries:
* **#399** — `fix(borrow): whole-place assignment clears move-record`
(the StmtAssign half of Slice C').
* **#400** — `fix(borrow): propagate ref-binding through reborrow indirection`
(the "reborrow through indirection" item).
4. Discovered three pre-existing PRs (**#395 / #396 / #397**) from a parallel
Claude session covering the same items. Per maintainer direction
("keep both PR sets open"), did not close mine; instead posted formal
audit comments on the parallel-Claude PRs documenting deltas and one
real soundness gap (see below).

== Parallel-implementation map

[cols="1,1,3,1", options="header"]
|===
| Deferred-item entry | Parallel-Claude PR | My PR | Same scope?
| Reborrow through indirection | #395 | #400 | Yes — equivalent
| Loop soundness + clear-on-rewrite | #396 | #399 | #396 is superset, but has a soundness gap
| Captured linears (Slice D) | #397 | _none_ | I had no parallel; only an audit comment
| Origin/region variables (Polonius) | #398 (mine) | #398 | ADR-only; M1 sketch local
|===

== PR state at handoff

[cols="1,1,1,1,3", options="header"]
|===
| PR | Draft? | Auto-merge | Mergeability | Notes
| #395 | non-draft | SQUASH ON | BLOCKED on CI | Owner-side; review comment posted
| #396 | non-draft | SQUASH ON | BLOCKED on CI | Owner-side; review comment flags one soundness gap
| #397 | non-draft | SQUASH ON | BLOCKED on CI | Owner-side; audit comment posted (must-fix flagged)
| #398 | **draft** | OFF (drafts can't arm) | BLOCKED on CI | Mine; owner-ratify one-liner posted in thread
| #399 | **draft** | OFF (drafts can't arm) | BLOCKED on CI | Mine; parallel-equivalent of #396
| #400 | **draft** | OFF (drafts can't arm) | BLOCKED on CI | Mine; parallel-equivalent of #395
|===

CI for every one of these PRs sat in the GitHub Actions runner queue at
session close (`QUEUED: 17, IN_PROGRESS: 0`). That is a GitHub-side backlog,
not a per-PR issue.

== Audit findings (the load-bearing deltas)

These are paraphrased; the full text lives on the GitHub PRs.

=== #395 vs #400 (reborrow through indirection)

Both PRs do the same three things:

* Recognise `let r2 = r1` / `r2 = r1` where the RHS is itself a ref-binder.
* Multi-binder gate in `expire_dead_ref_bindings` so a shared borrow only
ends when no live binder still aliases it — the `b'.b_id = b.b_id`
check (**byte-identical between the two PRs**).
* Symmetric handling on the `StmtAssign` reborrow path.

Two deltas only #400 has:

* Self-assign guard for `r = r`. Without it, the pre_release path ends `r`'s
borrow and the post-rebind never re-attaches, silently unbinding `r` from
the borrow-graph. Both PRs have the bug; only #400 guards it.
* `return r2` where `r2 = r1 = &local` is exercised by
`borrow_reborrow_indir_escape.affine`. #395's three fixtures (`let_aliases`,
`protects_owner`, `assign_aliases`) don't cover the return-escape path,
which is historically the most-leaked surface for this class of bug.

=== #396 vs #399 (clear-on-rewrite + loop soundness)

#396 is a **superset of #399 feature-wise** (it also does the 2-iteration
loop check that #399 doesn't). One real soundness divergence in the
StmtAssign half:

[source,affine]
----
fn unsound() -> Point {
let x = Point { ... };
drop_point(x); // move x
x.f = 5; // expected: UseAfterMove
// #399: rejects (is_whole_place_write predicate)
// #396: SILENTLY ACCEPTS — places_overlap is root-coarse,
// so this clears the move-record on x
x
}
----

#399 gates both the `find_move` skip and the move-record clearing on an
`is_whole_place_write` predicate (`place is PlaceVar _`). #396 unconditionally
skips the check and clears overlapping move-records, which is correct for
whole-place writes but unsound for sub-place writes (`x.f = …`, `x[i] = …`)
because the root-coarse `places_overlap` reports a sub-place as overlapping
its parent's move-record.

None of #396's three fixtures exercise sub-place writes after moves, so CI
does not catch this.

=== #397 audit (Slice D captured linears)

I had no parallel PR for this item; posted an audit-only review.

**One real bug:** Param-path tracking checks only `p.p_quantity = Some QOne`
and misses the `Cmd[T]`-typed param (no explicit `@linear`) case that the
let-statement path correctly catches via the `let_is_linear` helper. So
`fn f(c: Cmd[Int]) { let g = fn() => use(c); }` silently slips through
borrow-side rejection, falling back to the downstream quantity-checker
diagnostic (which is the regression Slice D's existence is meant to fix).

**Hygiene:** `linear_bindings` is not snapshot/restored at block exit (unlike
`borrows`, `block_local_syms`, `ref_bindings`) and is not unified in
`merge_arm_results`. Benign in practice (`sym_id`s don't recycle) but
inconsistent.

**Coverage gap:** The inference helper `borrow_quantity_of_ty` (the
`Cmd _ → QOne` branch) is unreached by any fixture. All three current
fixtures use explicit `@linear`. If somebody renames "Cmd", the inference
silently breaks.

== Safe-to-close conditions

Use this matrix when triaging the open PRs:

#400 (mine, reborrow indirection)::
**Safe to close once #395 merges**, provided #395 incorporates the two deltas
from the audit (self-assign guard + return-escape test). If #395 merges
without them, #400 stays open and is rebased onto main as a follow-up that
adds just the missing pieces.

#399 (mine, assign-clears-move)::
**Safe to close once #396 merges with the sub-place fix.** If #396 merges
without the `is_whole_place_write` predicate, #399 stays open and is rebased
onto main as a sub-place soundness correction.

#398 (mine, ADR-022 Polonius)::
Stays open as draft pending owner ratification. The one-liner
`gh pr ready 398 && gh pr merge 398 --auto --squash --delete-branch` is
posted in the thread; safe to close in a "won't-do" sense only if the
owner decides not to pursue origin-variables at all (unlikely — it's the
only deferred-item that genuinely needs an architectural change).

#395 / #396 / #397::
Owner-merge gated. Auto-merge SQUASH is armed; once the GH Actions runner
backlog drains and CI clears, they land. The review comments are
informational and don't block merge.

This documentation PR::
**Safe to close once merged.** Once on `main`, this doc serves as the
canonical handoff for the next session that touches `lib/borrow.ml`
deferred-items work.

== Cleanup performed this session

* `.git/gc.log` removed; `git prune` run to clear the warning that was
attached to every previous git operation.
* Two local-only branches kept for staged follow-ups:
* `core-01/polonius-m1-sketch` (commit `b28757c`) — M1 of ADR-022.
* (none others as of handoff time)

== For the next agent reading this

Before doing any more `lib/borrow.ml` work:

1. `gh pr list --state open` and confirm none of #395/#396/#397/#398/#399/#400
are already-merged. If they are, the deferred-items comment in
`lib/borrow.ml` will reflect which items have been crossed off.
2. If picking up a new deferred item, **`gh pr view` every open PR's title
first** to avoid re-doing parallel work. The previous-session summary
listing PRs only by status (MERGEABLE/BLOCKED) without titles was the
root cause of this session's duplicate work.
3. Cross-reference `feedback_affinescript_ephapax_siblings_not_impl_proof.md`
in user auto-memory — AffineScript ≠ Ephapax, the two share zero
borrow-checker code despite being substructural-logic siblings.

== References

* `lib/borrow.ml:1483-1505` — the canonical deferred-items list, updated
in-place by #395/#396/#397 to cross off completed items.
* `docs/decisions/0022-polonius-origin-variables.adoc` — ADR-022 design.
* `.machine_readable/sessions/2026-05-27-borrow-deferred-items.a2ml` —
machine-readable companion to this handoff.
Loading