diff --git a/.machine_readable/sessions/2026-05-27-borrow-deferred-items.a2ml b/.machine_readable/sessions/2026-05-27-borrow-deferred-items.a2ml new file mode 100644 index 00000000..0557c06a --- /dev/null +++ b/.machine_readable/sessions/2026-05-27-borrow-deferred-items.a2ml @@ -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 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" diff --git a/docs/history/SESSION-HANDOFF-2026-05-27.adoc b/docs/history/SESSION-HANDOFF-2026-05-27.adoc new file mode 100644 index 00000000..6ef48565 --- /dev/null +++ b/docs/history/SESSION-HANDOFF-2026-05-27.adoc @@ -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.