Bridge: compositional ownership contracts on the C# side (P-006/2b)#36
Merged
Conversation
Bump the push-triggered oracle sentinel to re-run the cross-tool comparison (Own.NET vs CodeQL vs Infer#) on corpus/fixtures/systemevents-console after the OWN001 -> OWN014 migration for static-event subscriptions (PR #35). The fixture's subscription leak now reports as OWN014; with OWN014 in the comparator's OWN_LEAK set it must still land "Own.NET-only" (the oracles have no subscription-leak query). Confirms the differentiation survived on real tool output, not just the --selftest fixtures. Eval-only; no product code changes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
…-006 + P-004)
Slice 1 of injected-tier -> region: prove the region engine can catch a zombie VM
whose event source is a DI-injected dependency, by sourcing the source's lifetime
from the registration graph instead of a local annotation.
.NET DI lifetimes ARE a region order (singleton=Process > scoped > transient), so
the bridge extends the capture region chain and, for an injected subscription
carrying `source_type`, looks the type up in the `services` graph and routes it
through the SAME check_lifetimes engine:
- source provably outlives the subscriber (singleton vs an un-registered
Window/VM, or singleton vs scoped) -> OWN014 captive/region escape;
- provably shorter-or-equal (transient) -> proven SAFE, silent (no honest-warning
hedge once the lifetime is known);
- unresolved source_type / no services -> unchanged OWN001 warning.
Additive + zero regression: gated on the new optional `source_type` field, which no
current fact/extractor emits. ownir 64/64, full suite, ruff, mypy --strict green.
Verified end-to-end through the CLI on di_capture.facts (singleton IEventBus ->
OWN014; transient IProbe -> silent).
Answers whether the model can reason about lifetimes it cannot know
intra-procedurally: yes, from the DI registration graph. Slice 2 (extractor emits
source_type + the subscriber's registration; real-code type-resolution risk) next.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
Add a real-world corpus case demonstrating cross-procedure ownership transfer
verified compositionally against a callee's contract -- the "island" mechanism,
end to end, on running code rather than prose.
`archive(s: Stream)` takes a resource-typed param by value => a CONSUME contract:
the release obligation moves INTO archive across the call. The case shows all
three faces in one file:
- leak() -> OWN001 (linear must-discharge: owned, never released/handed off)
- run() -> OWN002 (affine: use after ownership was consumed by archive)
- run_ok() -> silent (handoff DISCHARGES the caller's obligation -- no false
leak, though run_ok never calls release, because it is
verified against archive's signature, not its body)
The cross-procedure proof composes two intra-procedural checks glued at the
`consume Stream` cut point -- modular against the signature, exactly like Rust's
borrow checker, no whole-program points-to. before.cs/after.cs carry the real C#
shape (an IDisposable sink that owns and disposes its input); notes.md keeps the
standard honesty caveat (case.own is a hand reduction, not ingested C#).
corpus 5/5, full suite, ruff, mypy --strict all green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
Bring the inter-procedural island to C#-derived facts. A method's ownership
CONTRACT -- its parameters' effects -- now lowers through the bridge, and a `call`
flow op lowers to the core's Call, so cross-method ownership transfer is checked
compositionally by the SAME analyze() the .own DSL uses. No new checker, no
whole-program analysis: the callee's signature is the cut point.
Mechanism (reusing the existing engine end to end):
- a function fact may carry `params` with an `effect`
(consume/borrow/borrow_mut/plain). _lower_fn_params encodes each as the
TypeRef collect_signatures reads (resource-typed value => CONSUME, borrowed =>
BORROW/BORROW_MUT), so the core signature table resolves the contract.
- a `call` flow op lowers to A.Call; build_cfg.lower_call resolves each arg's
effect from that signature -> Invoke; analyze applies it (consume => the arg
escapes, a later use is OWN002; an undischarged owned param leaks OWN001).
- a consume param is an owned obligation in the callee, exactly as in .own --
the release obligation moves IN from the caller.
handoff_contract.facts.json proves it through the real CLI:
archive(consume s) -> clean (obligation moved in, discharged)
leak() -> OWN001 (never discharged)
run() -> OWN002 (use after the handoff consumed s)
run_ok() -> SILENT (correct handoff is NOT a false leak, though it
never releases: verified against archive's
contract, not its body)
This is the .own corpus case `ownership-handoff-consume`, now reproduced on
C#-shaped facts -- the compositional island on the product (Track 2b) side.
Additive + zero regression (gated on the new optional `params`/`call`). ownir
67/67, full suite, ruff, mypy --strict green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Repository UI Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (3)
🚧 Files skipped from review as they are similar to previous changes (1)
📝 WalkthroughWalkthroughTwo features are added to the OwnIR bridge: (1) DI-lifetime region-escape detection that maps DI service lifetimes to regions and lowers unreleased DI-sourced subscriptions as capture handles emitting OWN014 findings; (2) inter-procedural ownership-contract lowering that validates effect parameters, builds contract local maps, and emits ChangesDI-sourced region escape (OWN014)
Inter-procedural ownership handoff (OWN001/OWN002)
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ 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: b76ef818eb
ℹ️ 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".
![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 451-454: The condition at the location where `sub.get("source") ==
"injected"` is checked needs to be restricted to subscription resources only.
Currently, any unreleased fact with source set to "injected" triggers DI
lifetime rerouting, which incorrectly affects non-subscription resources that
may have incidental source or source_type fields. Add an additional condition to
verify that the resource is actually a subscription fact before proceeding with
the DI capture path rerouting. Apply this same fix to both occurrences of this
pattern (the one around line 451 and the one around line 592-595) to ensure
consistency across the codebase.
🪄 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: Repository UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 59bf6835-2991-4c49-b7cf-6f2ebbfe7573
📒 Files selected for processing (10)
corpus/oracle-target.txtcorpus/real-world/ownership-handoff-consume/after.cscorpus/real-world/ownership-handoff-consume/before.cscorpus/real-world/ownership-handoff-consume/case.owncorpus/real-world/ownership-handoff-consume/expected-diagnostics.txtcorpus/real-world/ownership-handoff-consume/notes.mdownlang/ownir.pytests/fixtures/ownir/di_capture.facts.jsontests/fixtures/ownir/handoff_contract.facts.jsontests/test_ownir.py
…ions Two review fixes for PR #36. codex (P2) -- an undischarged `consume` parameter crashed check_facts. The core stamps an origin (name#line) on acquired locals but NOT on parameters, so the OWN001 it emits for an owned param carried subject=None; the bridge's origin-based handle mapping then raised "cannot map back" instead of reporting the leak. Fix in the core (cfg.py): give every parameter symbol a stable origin, exactly like an acquired local -- a param can be the subject of a diagnostic (owned-param leak OWN001, borrow misuse OWN013/OWN004), so it must be attributable. Now an undischarged consume param maps to OWN001 at the parameter. CodeRabbit (Major) -- the DI region-escape reroute fired for any unreleased fact with source == "injected", regardless of resource kind. A non-subscription resource (e.g. a timer) with an incidental injected source/source_type could be lowered into the DI capture path and mis-reported. Scope both reroute sites (to_own and to_module) to rkind == "subscription"; a timer/disposable now keeps its own analysis path. Regression tests for both: an undischarged consume param maps to OWN001 (not a crash); a timer with an injected source stays a timer leak, not OWN014. ownir 69/69, full suite, ruff, mypy --strict green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
This was referenced Jun 19, 2026
This was referenced Jul 4, 2026
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.
Bridge: compositional ownership contracts on the C# side (P-006/2b)
Bring the inter-procedural island to C#-derived facts. A method's ownership
CONTRACT -- its parameters' effects -- now lowers through the bridge, and a
callflow op lowers to the core's Call, so cross-method ownership transfer is checked
compositionally by the SAME analyze() the .own DSL uses. No new checker, no
whole-program analysis: the callee's signature is the cut point.
Mechanism (reusing the existing engine end to end):
paramswith aneffect(consume/borrow/borrow_mut/plain). _lower_fn_params encodes each as the
TypeRef collect_signatures reads (resource-typed value => CONSUME, borrowed =>
BORROW/BORROW_MUT), so the core signature table resolves the contract.
callflow op lowers to A.Call; build_cfg.lower_call resolves each arg'seffect from that signature -> Invoke; analyze applies it (consume => the arg
escapes, a later use is OWN002; an undischarged owned param leaks OWN001).
the release obligation moves IN from the caller.
handoff_contract.facts.json proves it through the real CLI:
archive(consume s) -> clean (obligation moved in, discharged)
leak() -> OWN001 (never discharged)
run() -> OWN002 (use after the handoff consumed s)
run_ok() -> SILENT (correct handoff is NOT a false leak, though it
never releases: verified against archive's
contract, not its body)
This is the .own corpus case
ownership-handoff-consume, now reproduced onC#-shaped facts -- the compositional island on the product (Track 2b) side.
Additive + zero regression (gated on the new optional
params/call). ownir67/67, full suite, ruff, mypy --strict green.
Co-Authored-By: Claude Opus 4.8 (1M context) noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
Summary by CodeRabbit
OWN014, including correct routing based on DI lifetime information.