Bridge: contract inference — derive a callee's effects from its body (P-006/2b v1)#37
Merged
Merged
Conversation
…(P-006/2b v1)
The bounded inter-procedural step that lets first-party C# be checked without
annotating every method. When a function parameter carries no explicit `effect`,
infer its ownership contract from the callee's OWN body:
- the body discharges/escapes the param (release / return) -> CONSUME
(ownership taken);
- the param is only read and retained (use, no discharge) -> BORROW
(the caller keeps ownership and must still release it);
- the param is handed to another call -> ambiguous without that callee's
contract, so NOT inferred (stays plain / awaiting an annotation or a later
transitive pass).
Inference fires only on unambiguous signals and never guesses a consume/borrow,
and an explicit `effect` in the fact always wins over it. It reuses the existing
engine end to end: the inferred effect just picks the param's TypeRef, so
collect_signatures + lower_call resolve calls against the inferred signature with
no new checker.
contract_inference.facts.json proves it with ZERO annotations:
archive (releases s) -> inferred consume -> run trips OWN002 (use-after-handoff)
peek (only uses s) -> inferred borrow -> keep leaks OWN001 (caller still owns),
ok is clean (caller releases)
Additive + zero regression (only un-annotated params change behavior; explicit
contracts and annotation-free non-contract functions are unaffected). ownir
72/72, 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
📝 WalkthroughWalkthrough
Changesv1 Contract Inference for OwnIR Parameters
Estimated code review effort🎯 2 (Simple) | ⏱️ ~12 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://cdn.github.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: 7c46a89580
ℹ️ 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://cdn.github.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
ownlang/ownir.py (1)
384-390:⚠️ Potential issue | 🟠 Major | ⚡ Quick winValidate parameter identity fields before effect inference.
Line 385 validates only
effect; malformedparams[*].name/linestill pass shape-check and can be silently coerced downstream, which can mis-infer ownership contracts instead of failing fast on invalid OwnIR input.Suggested patch
for p in ps: + pname = p.get("name") + if not isinstance(pname, str) or not pname: + raise OwnIRError( + f"parameter 'name' must be a non-empty string, got {pname!r}") + pline = p.get("line", 0) + if not isinstance(pline, int) or isinstance(pline, bool): + raise OwnIRError( + f"parameter 'line' must be an integer, got {pline!r}") peff = p.get("effect") if peff is not None and peff not in ("consume", "borrow", "borrow_mut", "plain"): raise OwnIRError( f"parameter 'effect' must be consume/borrow/borrow_mut/plain, " f"got {peff!r}")🤖 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 `@ownlang/ownir.py` around lines 384 - 390, The parameter validation loop that checks the effect field at line 385-388 only validates the effect field, but parameters also have identity fields like name and line that should be validated before effect inference occurs. Add validation checks for these required identity fields (name and line) in the same loop that validates the effect field, ensuring they exist and have valid values before any downstream processing or coercion happens. This will catch malformed parameter definitions early rather than allowing them to silently propagate and cause incorrect ownership contract inference.
🧹 Nitpick comments (1)
tests/test_ownir.py (1)
693-725: ⚡ Quick winAdd a direct test for the “passed-to-call is ambiguous” branch.
This block validates consume/borrow + explicit override, but not the third rule (
passed=> no inference). Adding one focused case will lock the v1 contract boundary and prevent future regressions.Example assertion to add
if [(x.component, x.code) for x in ov] != [("g", "OWN001")]: fails.append(f"explicit `consume` should win over inferred borrow (owned " f"param leaks OWN001), got {[(x.component, x.code) for x in ov]}") + + # ambiguous handoff: param forwarded to another call => no inferred effect. + checks += 1 + amb = check_facts({"module": "M", "functions": [ + {"name": "forward", "file": "F.cs", + "params": [{"name": "s", "line": 1}], + "body": [{"op": "call", "callee": "sink", "args": ["s"], "line": 2}]}, + {"name": "sink", "file": "F.cs", + "params": [{"name": "x", "effect": "consume", "line": 5}], + "body": [{"op": "release", "var": "x", "line": 6}]}, + {"name": "caller", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "forward", "args": ["s"], "line": 11}, + {"op": "release", "var": "s", "line": 12}]}]}) + if any(x.component == "caller" for x in amb): + fails.append(f"ambiguous pass-through should not infer consume/borrow, got " + f"{[(x.component, x.code) for x in amb]}")🤖 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_ownir.py` around lines 693 - 725, The test block validates contract inference and the explicit override behavior, but does not cover the third rule where parameters passed-to-call (passed as arguments to other function calls) should not have inference applied. Add a new focused test case after the existing explicit consume override test using check_facts that creates a simple function with a parameter that is passed to another function call, verify the expected ownership behavior to ensure inference is correctly suppressed in this case, and add an assertion that validates the findings match the expected output to prevent future regressions.
🤖 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.
Outside diff comments:
In `@ownlang/ownir.py`:
- Around line 384-390: The parameter validation loop that checks the effect
field at line 385-388 only validates the effect field, but parameters also have
identity fields like name and line that should be validated before effect
inference occurs. Add validation checks for these required identity fields (name
and line) in the same loop that validates the effect field, ensuring they exist
and have valid values before any downstream processing or coercion happens. This
will catch malformed parameter definitions early rather than allowing them to
silently propagate and cause incorrect ownership contract inference.
---
Nitpick comments:
In `@tests/test_ownir.py`:
- Around line 693-725: The test block validates contract inference and the
explicit override behavior, but does not cover the third rule where parameters
passed-to-call (passed as arguments to other function calls) should not have
inference applied. Add a new focused test case after the existing explicit
consume override test using check_facts that creates a simple function with a
parameter that is passed to another function call, verify the expected ownership
behavior to ensure inference is correctly suppressed in this case, and add an
assertion that validates the findings match the expected output to prevent
future regressions.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Repository UI
Review profile: CHILL
Plan: Pro Plus
Run ID: c7a2159b-d462-475e-b47e-398955adfdca
📒 Files selected for processing (3)
ownlang/ownir.pytests/fixtures/ownir/contract_inference.facts.jsontests/test_ownir.py
Three review fixes for the contract-inference PR.
codex (P2) -- don't infer consume from returns, and stop value-returns crashing.
Two parts:
* inference no longer treats `return <param>` as a consume signal: the bridge
does not model returned (owned) VALUES, so a returned param is consume-and-
handed-back, not a plain consume -- inferring consume there is unsound until
return types are represented.
* a value-bearing `return` previously crashed (the bridge lowers every flow
function void, so the core's OWN035 "no return type but returns a value" had
no subject and check_facts raised). Now a body that returns a value gets an
owned return type, so the core models `return s` as a valid ESCAPE (the value
is discharged) -- no false leak -- and the return-type diagnostics the bridge
cannot represent (OWN033/OWN035) are skipped instead of crashing.
CodeRabbit (nitpick) -- the "passed-to-call is ambiguous" branch was untested and
crashed: an un-inferred (plain) param forwarded to a typed parameter produced a
subject-less OWN041 ("plain cannot satisfy a resource parameter") that raised.
Effect-kind mismatches (OWN034/OWN041) are bridge modeling-gap artifacts (an
ambiguous contract that could not be inferred), not real C# bugs, so they are
skipped too; the pass-through and its caller stay silent (no false positive).
Added a regression test for the branch.
CodeRabbit (major) -- validate params[*].name (non-empty string) and line
(integer) in load(), so malformed OwnIR input fails fast instead of being
silently coerced and mis-inferring a contract.
Regression tests for value-returns and the ambiguous pass-through. ownir 74/74,
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
Owner
Author
|
Following up on the CodeRabbit review — both points addressed in
Also from the codex review (same commit): inference no longer treats
Generated by Claude Code |
Owner
Author
|
@codex plz review |
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.
The bounded inter-procedural step that lets first-party C# be checked without annotating every method. When a function parameter carries no explicit
effect, infer its ownership contract from the callee's own body:release/return) → CONSUME (ownership taken);use, no discharge) → BORROW (the caller keeps ownership and must still release it);Inference fires only on unambiguous signals and never guesses a consume/borrow, and an explicit
effectin the fact always wins over it. It reuses the existing engine end to end: the inferred effect just picks the param'sTypeRef, socollect_signatures+lower_callresolve calls against the inferred signature with no new checker.Proof (
contract_inference.facts.json, zero annotations)archivesrun→ OWN002 (use-after-handoff)peekskeep→ OWN001 (caller still owns),ok→ clean (caller releases)Notes
ownir 72/72, full suite, ruff, mypy--strictall green.🤖 Generated with Claude Code
https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
Generated by Claude Code
Summary by CodeRabbit
New Features
Tests