feat(d5): D5.1b — per-call-site ownership-contract channel#113
Conversation
Pre-declare three fixed sink externs ($consume / $borrow / $borrow_mut) in every lowered Module so the extractor can route a call's per-argument ownership through them. They resolve via the same collect_signatures + lower_call path as any contracted call -- no new checker, no new flow lowering. The solver also reads a forward to a sink as a known transfer, so the channel propagates transitively through first-party wrappers. This is the locally-testable mechanism for per-call-site contracts (BCL leaveOpen, annotations); the extractor emitting the sink calls from the bool literal is the CI/C#-only remaining piece. Tests: use/double-release after $consume (OWN002), $borrow'd-then-leaked local (OWN001), clean borrow-then-release, transitive propagation through a wrapper. 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 (1)
✅ Files skipped from review due to trivial changes (1)
📝 WalkthroughWalkthroughThis PR adds fixed ownership-sink externs to lowered OwnIR, routes forwarded calls through sink-specific path actions, and updates tests and notes for consume, borrow, and wrapper propagation behavior. ChangesOwnership sink channel
Sequence Diagram(s)sequenceDiagram
participant to_module
participant Module
participant _build_skeletons
participant _forward_path_action
participant PathAction
to_module->>Module: include $consume, $borrow, $borrow_mut externs
_build_skeletons->>_forward_path_action: resolve forward target
_forward_path_action->>PathAction: return dispose, borrow, or forward
_build_skeletons->>PathAction: record parameter skeleton action
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~25 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 4✅ Passed checks (4 passed)
✨ Finishing Touches🧪 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: 087214a73a
ℹ️ 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".
| # `$borrow`/`$borrow_mut` is a kept loan — rather than a `forward` edge to an | ||
| # unsummarized callee (which the solver would degrade to `unknown`, diluting a real | ||
| # `must` to plain). Kept in sync with `_OWNERSHIP_SINK_EXTERNS`. | ||
| _SINK_PATH_ACTION = {"$consume": "dispose", "$borrow": "borrow", "$borrow_mut": "borrow"} |
There was a problem hiding this comment.
When a parameter is forwarded only to $borrow_mut, this map records the path as a plain borrow, so the solver returns Transfer.NO and _infer_param_effect lowers the wrapper's parameter to a shared borrow signature. Any first-party wrapper around a mutable-borrow sink therefore loses the exclusivity requirement: a caller passing a shared-borrow parameter is accepted through the wrapper even though a direct $borrow_mut call would require borrow_mut and the wrapper's internal OWN041 is later skipped by the bridge. The per-call-site channel should keep $borrow_mut distinct when propagating the contract transitively.
Useful? React with 👍 / 👎.
…ummaries (Codex P2) The transfer lattice (no/must/may/unknown) carries no shared-vs-exclusive axis, so the transitive sink shortcut mapping $borrow_mut to a plain borrow would silently weaken an exclusive loan to a shared one in a wrapper's contract. Drop $borrow_mut from the known-transfer map: it degrades to unknown -> the wrapper param stays plain (no false shared-borrow claim). The direct call $borrow_mut [x] channel is unaffected and keeps full exclusivity through lower_call. Adds direct $borrow_mut channel tests (leak + clean) and documents the decline. 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: 1
🤖 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 `@ownlang/ownir.py`:
- Around line 939-945: Preserve the mutable-borrow distinction in the sink
skeleton flow: `_SINK_PATH_ACTION` currently normalizes `$borrow_mut` to the
same action as `$borrow`, which causes `_build_skeletons()` and wrapper
inference to lose exclusivity semantics. Update the action/skeleton handling in
`ownlang/ownir.py` so `$borrow_mut` carries a mutability marker through the
layer instead of being collapsed to plain borrow, and ensure the wrapper path
still resolves to the `BORROW_MUT`-equivalent behavior used by the sink
inference logic.
🪄 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: 33d77baf-8607-474b-b4f1-2020c92e6a38
📒 Files selected for processing (3)
docs/notes/d5-ownership-transfer.mdownlang/ownir.pytests/test_ownir.py
…D5.1c The D5.0 summary solver is transfer-oriented and has no shared-vs-exclusive axis, so it flattens borrow/borrow_mut into one bucket. The core checker already distinguishes them (analysis.py _check_mut_borrowable vs _check_shared_borrowable), so the direct $borrow_mut call keeps exclusivity; only the transitive wrapper claim is lost, which D5.1b declines (precision-safe). Records the clean follow-up shape -- an orthogonal borrow-kind axis on the summary, not another Transfer enum value -- so the deferral is tracked, not buried (Codex P2 / CodeRabbit Major). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
2 participants
P-005 D5.1b — the per-call-site ownership-contract channel
StreamReader(stream, leaveOpen: …)& friends are a per-call-site contract — the same constructor consumes or borrows depending on the bool literal — so they need a per-call effect channel, not a per-method summary. This slice builds that channel as a locally-testable mechanism.What ships
The bridge pre-declares three fixed sink externs in every lowered
Module:The extractor routes any call's per-argument ownership through them (
call $consume [x]), and they resolve via the samecollect_signatures+lower_callpath as any contracted call — no new checker, no new flow lowering. Externs are declaration-only (never leak-checked themselves), and the$prefix cannot collide with a real C# member name.Transitive coherence
The summary solver also reads a forward-to-a-sink as a known transfer (
$consume→ must,$borrow*→ no) via_SINK_PATH_ACTION. Without that, a param forwarded only to$consumewould degrade tounknownand dilute to plain — so the channel now propagates transitively through first-party wrappers, not just at the direct call.Tests (synthetic OwnIR, 137 → 141 bridge checks)
acquire x; call $consume [x]; use x→ OWN002 (ownership left at the call)$consume→ OWN002 (double-discharge)acquire x; call $borrow [x]never released → OWN001 (borrow keeps ownership — no over-consume)$consume→ method becomes a must-consumer → caller's later use is OWN002 (transitive)Full suite green (
run_tests.pyexit 0),ruff+mypy --strictclean.Out of scope (CI/C#-only)
The extractor emitting these sink calls from the bool literal / annotation — paired with an A/B sample on real extractor output — rides into D5.3 (Tier-B breadth).
🤖 Generated with Claude Code
https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
Generated by Claude Code
Summary by CodeRabbit
New Features
Bug Fixes
Documentation
Tests