iframe-proxy

hyperpolymath · 2026-05-26T22:31:33Z

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

CORE-01: complete borrow checker Phase-3 (borrow-graph validation) #177 (CORE-01 pt3)
Third of three small slices being landed today; feat(borrow): CORE-01 ref-to-ref binding (#177 pt3) — let r2 = r / r = s alias the borrow-graph #395 (ref-to-ref) and feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on while/for (Refs #177) #396 (Slice C') are in flight. Slice C-full (Polonius) is being handed off to a separate Claude — prompt incoming separately.

Test plan

`dune runtest --force` — 327 → 330 tests, 0 failures
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

hyperpolymath · 2026-05-27T00:49:52Z

Parallel-work review (Slice D audit)

Slice D is the one deferred-items entry I didn't duplicate — I had no parallel PR open here. This is a fresh audit of the diff against the soundness story in the comment.

Two real bugs, two hygiene items, three suggested fixture adds.

1. `Cmd _`-typed parameters slip through the linear-capture check

Two paths populate state.linear_bindings:

Let-statements / let-expressions use the shared helper:

if let_is_linear lb.el_quantity lb.el_ty then
  state.linear_bindings <- sym.Symbol.sym_id :: state.linear_bindings

let_is_linear correctly falls back to borrow_quantity_of_ty ty_opt when the explicit quantity is None, so let x: Cmd[Int] = … (no explicit @linear) is tracked.

Parameters in check_function:

if p.p_quantity = Some QOne then
  state.linear_bindings <-
    sym.sym_id :: state.linear_bindings

This checks ONLY the explicit p_quantity = Some QOne annotation. A param c: Cmd[Int] (Cmd-typed, no explicit @linear) is QOne by Cmd _ inference but never reaches linear_bindings — the same call to borrow_quantity_of_ty that the let path makes is missing here.

Result: a closure capturing a Cmd-typed param silently slips through. The companion quantity-checker pass would still flag downstream "used multiple times" but the early borrow-side error that the PR comment promises does not fire.

Suggested fix — make the param path symmetric:

let p_is_linear =
  match p.p_quantity with
  | Some q -> q = QOne
  | None -> borrow_quantity_of_ty (Some p.p_ty) = QOne
in
if p_is_linear then
  state.linear_bindings <- sym.sym_id :: state.linear_bindings

(p.p_ty is not an option, so wrap in Some.)

2. The helper `borrow_quantity_of_ty` is unexercised by fixtures

Three fixtures, all using explicit @linear — none uses Cmd[T] to drive the inference branch of let_is_linear. So the helper's Some (TyApp ({ name = "Cmd"; _ }, _)) -> QOne arm is unreached by CI. If somebody later renames "Cmd" to "Linear" (or whatever the canonical name is) the linear inference silently breaks and no test catches it.

A fourth fixture along the lines of:

fn capture_cmd_let() -> Int {
  let c: Cmd[Int] = make_cmd();
  let f = fn() => use_cmd(c);
  f()
}

— expected LinearCapturedByClosure — would pin this path.

3. `linear_bindings` is not snapshot/restored at block exit

check_block snapshots borrows, block_local_syms, ref_bindings at entry and restores them at exit. linear_bindings is not in the snapshot:

let borrows_at_entry = state.borrows in
let block_locals_at_entry = state.block_local_syms in
let ref_bindings_at_entry = state.ref_bindings in
(* no linear_bindings_at_entry *)
...
state.borrows <- borrows_at_entry;
state.block_local_syms <- block_locals_at_entry;
state.ref_bindings <- ref_bindings_at_entry;
(* no restore of linear_bindings *)

So a @linear let x declared inside a nested block stays in linear_bindings after the block ends. Benign in practice because sym_ids don't recycle to in-scope symbols, but inconsistent with the rest of the state-field discipline and a foot-gun if a future change ever does mutate the linear_bindings list during block exit cleanup.

4. `merge_arm_results` does not unify `linear_bindings`

Same character as #3 — when match/try/handle arms merge, borrows/moved are unioned but linear_bindings entries created in arm $i$ aren't reconciled. Same benign-but-inconsistent footprint.

Coverage gaps in fixtures

Three adds that round out the matrix:

Cmd _ let captured (positive rejection via inference) — exercises borrow_quantity_of_ty's Cmd arm.
Cmd _ param captured (currently slips through per ci: Bump actions/setup-node from 4.0.2 to 6.3.0 #1) — would fail against the unfixed PR, pass against the patched version. The strongest regression for the param-path fix.
Shadowing: @linear let x = …; let x = 100; let f = fn() => x + 1; f() — the closure captures the inner non-linear x. Expected: Ok. Pins that the rejection scopes to the sym-id in linear_bindings, not the name.

What's architecturally fine

The borrow_quantity_of_ty / let_is_linear helpers are sensibly duplicated in borrow.ml with the comment pointing at the canonical helper in quantity.ml.
The lambda capture rejection fires before the existing shared-borrow loop — early exit and good span attribution.
LinearCapturedByClosure (name, lam_span) carries enough context for a clean diagnostic, and the formatter is good.
The deferred-items comment is correctly updated to remove the Slice D entry.

Nothing blocking — the only must-fix is #1 (param-path symmetry). Items #3 and #4 are hygiene; can land separately.

…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>

…closure at borrow check 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 more specific 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, collect-free walks the body; for each captured free-name we look up its symbol and reject with [LinearCapturedByClosure name * lambda_span] if the sym-id is in [linear_bindings]. - The Shared-borrow creation for non-linear captures is unchanged. Tests (+3, all green): - slice_d_captured_linear_let_rejected: @linear let captured → LinearCapturedByClosure("x", _) - slice_d_captured_linear_param_rejected: @linear param captured → LinearCapturedByClosure("y", _) - slice_d_captured_nonlinear_ok: anti-regression, non-linear capture must still pass Gate: 327 → 330 tests, 0 failures under `dune runtest --force`. Refs #177, CORE-01 pt3 (Slice D). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…efs #177) — surgical refile of #398 (#407) ## Summary Surgical refile of #398. The original branch `core-01/polonius-adr` carried 386 commits' worth of phantom history (commits with main equivalents at different SHAs after squash-merges), and a naive cherry-pick onto current main would have clobbered the `linear_bindings` work landed today via #397. This branch carries **only** the 3 intended changes from #398: - `docs/decisions/0022-polonius-origin-variables.adoc` (347 lines) — long-form ADR - `.machine_readable/6a2/META.a2ml` (143 lines) — structured `[[adr]]` block - `lib/borrow.ml` (5 lines net) — single in-comment edit in the closing residual-TODO block, pointing readers at ADR-022 Owner ratified the architectural bundle 2026-05-27: OCaml Polonius solver in `lib/borrow_polonius/`, surface-syntax fully elided for v1, M1–M4 stage gates with lexical checker as merge oracle through M3. ## Closes Closes #398 (the stale-base original). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-05-27T21:57:42Z

🔍 Hypatia Security Scan

Findings: 56 issues detected

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action actions/checkout@v6 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action denoland/setup-deno@v2 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in affine-vscode-publish.yml",
    "type": "unknown",
    "file": "affine-vscode-publish.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "unknown",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "unknown",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "unknown",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "unknown",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "unknown",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "unknown",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "unknown",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

#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>

hyperpolymath enabled auto-merge (squash) May 26, 2026 22:31

hyperpolymath mentioned this pull request May 26, 2026

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

Closed

5 tasks

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 force-pushed the core-01/slice-d-captured-linears branch from eb66a13 to 04ec7d7 Compare May 27, 2026 13:27

hyperpolymath merged commit 02a5914 into main May 27, 2026
9 of 10 checks passed

hyperpolymath deleted the core-01/slice-d-captured-linears branch May 27, 2026 13:27

hyperpolymath mentioned this pull request May 27, 2026

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

Merged

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 mentioned this pull request Jun 1, 2026

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

Open

Sunbelt Computer Software

PL/B Language Development and Support

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

feat(borrow): CORE-01 Slice D (#177 pt3) — reject @linear capture by closure at borrow check#397
hyperpolymath merged 1 commit into
mainfrom
core-01/slice-d-captured-linears

hyperpolymath commented May 26, 2026

Uh oh!

hyperpolymath commented May 27, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Sunbelt Computer Software

PL/B Language Development and Support

Uh oh!

Conversation

hyperpolymath commented May 26, 2026

Summary

Mechanism

Refs

Test plan

Uh oh!

hyperpolymath commented May 27, 2026

Parallel-work review (Slice D audit)

1. Cmd _-typed parameters slip through the linear-capture check

2. The helper borrow_quantity_of_ty is unexercised by fixtures

3. linear_bindings is not snapshot/restored at block exit

4. merge_arm_results does not unify linear_bindings

Coverage gaps in fixtures

What's architecturally fine

Uh oh!

Uh oh!

github-actions Bot commented May 27, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

1. `Cmd _`-typed parameters slip through the linear-capture check

2. The helper `borrow_quantity_of_ty` is unexercised by fixtures

3. `linear_bindings` is not snapshot/restored at block exit

4. `merge_arm_results` does not unify `linear_bindings`