P-005 D5: ownership-transfer design + D5.0 summary solver (infra)#111
Merged
Conversation
Lock in the worked-out design for D5 as docs/notes/d5-ownership-transfer.md and point P-005 at it. Key decisions, sharpened by a literature/tooling review (RLC/RLC#, CA2000, ReSharper, Move, Polonius/Flowistry): - D5 is a summary-contract problem, not a borrow-checker-core one: an extractor-side Method Ownership Summary (MOS) pass feeding the core's EXISTING consume/borrow/owned-return vocabulary. Minimal new core code. - Schema keeps escape and transfer on SEPARATE axes (escape != ownership transfer); transfer is three-valued must/may/no(+unknown); returns add aliasOf:<i> for the MustCallAlias wrapper pattern (Dapper DbWrappedReader). - Tiered truth: A first-party SCC fixpoint (cap 3, logged), B curated BCL table (leaveOpen is the crown jewel), C annotations, D heuristic fallback. - Precision-first default (optimistic on unknown -> silent), with a strict mode and an OWN05x advisory for may/unknown computed regardless of mode. - Slices D5.0..D5.5 with a leaveOpen Tier-B slice folded into the first live-behavior milestone; out/ref-owned before IAsyncDisposable. - Prior-art reading list so we don't reinvent blindly. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
…t B) A third literature/tooling pass (Checker Framework RLC, RLC#, Clang ARC, ReSharper, Roslyn CA2000) converges with no reservations on the RID/alias-set model for the wrapper case. Lock it in: - New section 11: obligations live on a resource id (RID, state Open|Released), handles are access paths; an alias set is the handles sharing one RID, and disposing any owning member discharges it. Default 1:1 (today's behaviour); N:1 only on a *proven* alias. - T4a (factory returns wrapper) and T4b (ctor adopts into owning field) collapse to one primitive: alias_join — a new owning handle joins the arg's RID. Leak check becomes per-RID, not per-binding. - Hard v1 constraints: aliasOf is must-only (unproven -> silent); single source RID + single new handle (>1 owning field can't form the simple relation); owning-only (views stay in borrow machinery); no whole-program heap-alias — verified by forward-and-return or store-in-owning-field, the two RLC shapes. - Dapper DbWrappedReader worked as a mix: aliasOf:reader + cmd adopted as an ordinary owning field. Polly Bulkhead is the pure T4b form. - D5.4 lands as a three-commit cadence (no-op RID refactor -> alias_join lowering -> extractor aliasOf emission), de-risked behind the green D5.0-D5.3 corpus. Reading anchors: Checker Framework manual 8.5, RLC paper 4, RLC# resource-alias layer. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
First code for P-005 D5, per docs/notes/d5-ownership-transfer.md. Pure
data + algorithm; NO findings wired, no behaviour change (D5.1+ lowers
summaries into the core consume/borrow/acquire vocabulary).
ownlang/ownership.py: the Method Ownership Summary (MOS) types and a
depth-capped bottom-up solver over the first-party call graph.
- Transfer lattice {no, must, may, unknown} with an associative join
(unknown absorbs; a transfer-path joined with a keep-path -> may).
- Per-method skeleton (extractor-facing input) -> resolved summary:
direct dispose/adopt/return -> must, borrow -> no, forward -> the
callee's summary, extern or past-cap -> unknown, recursion edge -> no
(broken at the cycle). Precision-first: must is claimed only when
ownership leaves the caller on every recorded path.
- Depth cap = 3 (CA2000's max_interprocedural_method_call_chain default),
logged via solve_with_log (no silent truncation).
- Return kinds fresh / aliasOf:i / aliased / forward / none, with
aliasOf reserved for the D5.4 obligation-identity model.
- to_dict emits the detached summaries[] serialization.
tests/test_ownership.py (33 checks, wired into run_tests.py): the join
lattice, direct/forward/partial transfer, extern boundary, depth-cap
logging, mutual + self recursion convergence, return-kind resolution,
and serialization. Full suite stays green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (3)
✅ Files skipped from review due to trivial changes (1)
🚧 Files skipped from review as they are similar to previous changes (2)
📝 WalkthroughWalkthroughAdds D5 ownership-transfer design notes, implements an interprocedural ownership summary solver, and extends tests and the test runner to cover the new solver. ChangesInterprocedural ownership summaries
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Poem
🚥 Pre-merge checks | ✅ 4✅ Passed checks (4 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 27d9166c38
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+154
to
+156
| if skel is None or i < 0 or i >= len(skel.params): | ||
| return Transfer.UNKNOWN | ||
| p = skel.params[i] |
There was a problem hiding this comment.
PathAction.arg is the callee's parameter index, but this lookup treats it as a dense tuple offset. When the skeleton only contains disposable/interesting parameters or otherwise has a non-zero first ParamSkeleton.index (for example a wrapper Create(..., reader) at index 1), forwarding to arg=1 satisfies this out-of-range check and is downgraded to unknown, so first-party consumes/adoptions after earlier unmodeled parameters are silently lost instead of resolving through the summary.
Useful? React with 👍 / 👎.
| return "unknown" | ||
| if r.callee in stack: | ||
| return "unknown" | ||
| return _resolve_return(r.callee, depth + 1, stack | {r.callee}, cap, sk, capped) |
There was a problem hiding this comment.
_resolve_return returns the callee's aliasOf:<i> unchanged, but <i> is in the callee's parameter space. For a forwarding wrapper like Outer(a, b) => Inner(b) where Inner returns aliasOf:0, this summarizes Outer as aliasOf:0 instead of aliasOf:1; when lowered, the wrong argument RID would be joined/discharged while the actually adopted argument is missed. The forward-return summary needs to carry and apply the call's argument mapping before propagating aliasOf.
Useful? React with 👍 / 👎.
… (Codex) Two P2s in the D5.0 solver, both real: - _resolve_param indexed skel.params[i] as a tuple offset, but i is the callee's logical parameter index (ParamSkeleton.index). A sparse skeleton (e.g. a wrapper Create(cmd, reader) listing only reader at index 1) made a forward to arg=1 fall off the end and degrade to unknown, silently losing first-party consumes/adoptions after earlier unmodeled params. Now resolved by .index; solve_with_log passes the logical index too. - _resolve_return propagated a callee's aliasOf:<i> verbatim, but <i> is in the callee's param space; for Outer(a,b) => Inner(b) where Inner returns aliasOf:0, Outer was summarized aliasOf:0 instead of aliasOf:1, which would join/discharge the wrong RID at lowering. Remapping needs the call's arg mapping (arrives with the obligation-identity model in D5.4); until then degrade forward-return-of-aliasOf to unknown (precision-safe). fresh/aliased/none still propagate. Two regression tests added (35/35). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (1)
tests/test_ownership.py (1)
149-155: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winAdd a forwarded-
aliasOfremapping regression.The return tests only cover
forward -> fresh, so they won't catch the wrapper case where a callee resolves toaliasOf:<j>and the caller passes its own parameter in a different slot. A small reordered-argument case here would lock down the intended caller-local alias contract.Example test to add
s = solve([ _m("Make", ret=ReturnSkeleton("forward", callee="Inner")), _m("Inner", ret=ReturnSkeleton("fresh")), ]) expect(s["Make"].returns == "fresh", "forward-return propagates fresh") + + s = solve([ + _m("Wrap", + _p(0, PathAction("forward", "Inner", 1)), + ret=ReturnSkeleton("forward", callee="Inner")), + _m("Inner", + _p(0), + _p(1, PathAction("return")), + ret=ReturnSkeleton("aliasOf", arg=1)), + ]) + expect(s["Wrap"].returns == "aliasOf:0", + "forward-return remaps aliasOf to caller param")🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_ownership.py` around lines 149 - 155, Add a regression test in the ownership return suite to cover the forwarded alias remapping case, since the existing forward-return check in solve only verifies forward -> fresh. Extend the test around solve and ReturnSkeleton so a caller using forward to an aliasOf result from the callee still preserves the caller-local alias contract when arguments are reordered, and assert the caller’s returns reflect the remapped alias rather than the callee’s original slot.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/notes/d5-ownership-transfer.md`:
- Around line 74-93: The MOS schema in this section does not match the solver
output from MethodSummary.to_dict(), because it omits the explicit none return
state and treats via as part of the canonical summaries contract even though
D5.0 does not serialize it. Update the returnsOwned definition in this doc to
include none as a distinct return state alongside fresh, aliased, aliasOf:<i>,
and unknown, and revise the guidance around via to mark it as
optional/debug-only rather than canonical. Use MethodSummary.to_dict() and
ownlang/ownership.py as the anchors for the schema text so readers can map the
documented states to the actual serialized form.
In `@ownlang/ownership.py`:
- Around line 94-103: The `ReturnSkeleton`/`_resolve_return()` forwarding path
is preserving the callee’s `aliasOf:<i>` identity instead of the caller-local
argument identity, which breaks wrapper forwarding. Update `ReturnSkeleton` and
the forward-handling logic in `_resolve_return()` so forwarded returns can
retain or translate the call-site argument mapping from the wrapper, and if that
mapping is unavailable, conservatively downgrade forwarded `aliasOf` returns
rather than emitting the callee-local index.
- Around line 218-220: The skeleton aggregation in ownership.py currently builds
sk with a dict comprehension that silently overwrites duplicate method keys, so
update the logic around the skeletons-to-sk map to detect repeated s.key values
and fail fast instead of keeping the last one. Use the existing skeletons/sk
setup in the method that prepares MethodSummary data, and add an explicit
duplicate check before any later call-graph or summary processing so input order
cannot change the result.
- Around line 193-208: The _resolve_return logic in ownership.py is collapsing
every unrecognized ReturnSkeleton.kind into "none", which can hide owned-return
information. Update the kind dispatch so only the explicit "none" case returns
"none"; keep all other unknown kinds as "unknown" (or raise) in the same
_resolve_return function alongside the existing fresh, aliasOf, aliased, and
forward branches.
---
Nitpick comments:
In `@tests/test_ownership.py`:
- Around line 149-155: Add a regression test in the ownership return suite to
cover the forwarded alias remapping case, since the existing forward-return
check in solve only verifies forward -> fresh. Extend the test around solve and
ReturnSkeleton so a caller using forward to an aliasOf result from the callee
still preserves the caller-local alias contract when arguments are reordered,
and assert the caller’s returns reflect the remapped alias rather than the
callee’s original slot.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: 4b2f2af7-993e-4a33-8a71-3a846d48cb9f
📒 Files selected for processing (5)
docs/notes/d5-ownership-transfer.mddocs/proposals/P-005-idisposable-ownership.mdownlang/ownership.pytests/run_tests.pytests/test_ownership.py
…a (CodeRabbit) Three Major review items on the D5.0 solver: - solve_with_log: reject duplicate MethodSkeleton keys (raise ValueError) instead of silently keeping the last via a dict comprehension. Key collision-freedom is an open design question (note s10 q2); the silent overwrite would make summaries input-order dependent. - _resolve_return: an unrecognised ReturnSkeleton.kind now fails closed to 'unknown' rather than collapsing to 'none' (which would erase owned-return info); only the explicit 'none' kind returns 'none'. - d5-ownership-transfer.md: align the MOS schema with the solver — add the explicit 'none' return state (to_dict emits it; distinct from unknown), and mark 'via' as debug-only, not part of the canonical summaries[] contract and not serialized by D5.0. Two regression tests added (dup-key raises, unknown return kind -> unknown); 37/37, full suite green. The paired nitpick (a test expecting forward-return to *remap* aliasOf to the caller slot) is intentionally skipped: D5.0 deliberately degrades forwarded aliasOf to unknown — the arg-mapping needed to remap arrives with the obligation-identity model in D5.4 — and a degrade-to-unknown test already pins that. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
This was referenced Jun 26, 2026
9 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
What
The design for P-005 D5 (interprocedural
IDisposableownership transfer)plus its first code — the D5.0 summary solver. Design + infra in one pile, as
agreed; no behaviour change (no findings wired yet).
Design —
docs/notes/d5-ownership-transfer.md(+ P-005 pointer)Worked out across three literature/tooling reviews (Checker Framework RLC / RLC#,
CA2000, ReSharper, Move, Polonius/Flowistry). Headlines:
extractor-side Method Ownership Summary (MOS) pass feeding the core's existing
consume/borrow/owned-return vocabulary. Minimal new core code.
transfer); transfer is three-valued (must/may/no + unknown); returns add
aliasOf:<i>for the wrapper pattern.live on a resource id (RID,
Open|Released); handles are access paths; an aliasset is the handles sharing one RID, and disposing any owning member discharges
it. Default 1:1 (today's behaviour); N:1 only on a proven alias. T4a (factory
returns wrapper) and T4b (ctor adopts into owning field) collapse to one
primitive,
alias_join; the leak check becomes per-RID. Hard v1 constraints:aliasOfis must-only, single-source, owning-only, no whole-program heap-alias.Dapper
DbWrappedReaderworked as a mix (aliasOf:reader+cmdadopted).and an
OWN05xadvisory for may/unknown computed regardless.leaveOpentable → C annotations →D heuristic), slices D5.0–D5.5 (a
leaveOpenslice folded into the first livemilestone;
out/refbefore async), and a prior-art reading list.Code — D5.0
ownlang/ownership.py(+ tests)The MOS types and a depth-capped bottom-up solver over the first-party call
graph. Pure data + algorithm, locally testable, no extractor, no findings:
{no, must, may, unknown}with an associativejoin(unknownabsorbs; transfer-path ⊔ keep-path → may).
must,borrow →
no, forward → the callee's summary, extern / past-cap →unknown,recursion edge →
no(cycle broken).mustis claimed only when ownershipleaves the caller on every recorded path (precision-first).
max_interprocedural_method_call_chaindefault),logged via
solve_with_log— no silent truncation.fresh / aliasOf:i / aliased / forward / none;to_dictemits thedetached
summaries[]serialization.tests/test_ownership.py— 33 checks (wired intorun_tests.py): the joinlattice, direct/forward/partial transfer, extern boundary, depth-cap logging,
mutual + self recursion convergence, return-kind resolution, serialization. Full
suite stays green.
Not in scope (next slices)
D5.1 lowers summaries into the core
consume/borrow/acquirevocabulary (+ aleaveOpenTier-B slice); D5.4 adds the RID/alias_joinobligation-identitymodel in a three-commit cadence. This PR is design + the locally-testable solver
infra only.
🤖 Generated with Claude Code
Generated by Claude Code
Summary by CodeRabbit