docs: interprocedural roadmap — staged path from D5 today to 'proper interprocedural' - #177
Merged
Merged
Conversation
…interprocedural' Consolidates the scattered interprocedural state (d5 note's shipped slices, tech-debt register §3 prerequisite, deferred trackers #122/#146, the arity residual of d5 §10 q2) into one sequenced roadmap: - stage 0: spec the verdict-determining bridge inference + golden facts (the P-022 hard prerequisite, unlocks everything else) - stage 1: observability first — OWN051 advisory + MOS summary dump - stage 2: arity/signature key on call ops (additive optional field, no OWNIR_VERSION bump) to stop conservative overload merging - stage 3: aliasOf:i through return + out/ref fresh (Dapper/Polly become oracle anchors with a recorded reason) - stage 4: publisher provenance (#146) on top of stage 3's skeletons - stage 5: exclusivity axis (#122) strictly on its consumer trigger - stage 6: Tier C annotations + pessimistic mode Includes a definition of done, a dependency graph, on-record rejections (context sensitivity, IL decompilation, frontend inference), and a reading path into ownership.py/ownir.py for newcomers. Cross-linked from the d5 note's §10 open questions. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
…(P-022) Records the decision that the core rewrite is now in execution and applies the 'one checker' guardrail to the roadmap: a feature freeze on verdict-changing inference until parity/cutover (a new axis in Rust before parity diverges from the reference; a new axis in Python moves the parity target the port must chase). Stage re-keying: stage 0 (spec the bridge inference) is language-neutral and is the port's prerequisite — do now; stage 1's summary dump is requalified as a parity artifact (diff Python vs Rust MOS summaries); stage 2's extractor half runs parallel to the port while its consuming half, stages 3-4 and 6 land in Rust after cutover; #122 is unaffected. Also records what ports cheaply (the pure ownership.py solver, the language-neutral synthetic OwnIR tests) and the on-record caveat that an urgent precision fix during the port goes into Python and knowingly moves the parity target. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
…invariants, Rust-port requirements Deep-dive companion to interprocedural-roadmap.md. Pins the layer's actual semantics to code at adc1496 with file:line references: - normative rules as implemented: the Transfer lattice and path contributions, skeleton derivation (S), return inference (R), overload merging (M), the SCC fixpoint (F), call-site application (A) and tier precedence — the raw material for spec/Inference.md (stage 0) - five spec decision points (D1-D5), including a REPRODUCED precision defect: any-path release infers consume, so a callee that disposes a parameter conditionally fabricates OWN002 at a careful caller and OWN001 in the callee itself (violates the own-only-0 floor; verified by executing check_facts on synthetic facts). Recommended fix: branch-sensitive release derivation (all-paths -> dispose, partial -> may -> plain), to be decided BEFORE the port so bit-parity does not enshrine the bug. Also: the dead escapes axis, reserved adopt/return path kinds, the aliasOf hop degradation, and the silent solver degrade (except -> empty MOS) that should become observable - twelve numbered invariants (precision floor, determinism-from-input, tier precedence, closed op vocabulary, byte-exact output texts) as review blockers - Rust-port requirements for own-bridge: type mapping, determinism rules (no hash-order reaching output), error policy matching the Python degrade, --dump-summaries as a third oracle_exact surface, and the port order (solver -> derivation -> application), each phase behind its parity gate - concrete work cards for roadmap stages 2-4: signature key with fallback rules that preserve Tier A suppression, aliasOf:i through return (first slice, direct calls only), and #146 with a hard visibility gate — each with its test matrix and DoD Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
📝 WalkthroughWalkthroughThis PR adds interprocedural ownership-transfer documentation, a new summaries CLI command, MOS-driven advisory reporting, and updated diagnostics, serialization, and tests for the bridge. ChangesInterprocedural ownership layer
Estimated code review effort: 5 (Critical) | ~120 minutes Possibly related PRs
🚥 Pre-merge checks | ✅ 4✅ Passed checks (4 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d25a8b425c
ℹ️ 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".
…Z D1) The skeleton derivation and the direct contract inference collapsed the release signal to a boolean: a release on ANY path produced a lone dispose path action, so a callee that disposes a parameter conditionally (the ubiquitous null-guard dispose-helper idiom, `if (x != null) x.Dispose()`) was inferred `consume`. That flattened `must` charged a caller's defensive dispose a false OWN002 and the helper itself a false OWN001 — reproduced on synthetic facts before the fix, and a direct hit on the own-only-0 precision floor. The d5 note always defined `must` as 'released on ALL normal-return paths'; the code now matches it. `_definite_release` walks the op tree tracking the release state of live paths (released on none / some / all) plus whether every early `return` was reached already-released: release in both branches or before every exit stays a definite dispose (consume recall preserved — the careless caller keeps its true OWN002); a one-branch, in-loop (zero-trip), or guarded-by-early-return release now also emits a kept path, so the lattice joins to `may` and the caller stays plain (silent). The walk ignores only ops that cannot hide a release — anything new fails loud in _lower_flow first (IR4), so the walk can never be lied to. Six regression tests pin the matrix from the TZ: conditional release silent, both-branch consume kept, while-body release silent, early return blocks the claim, release-then-return credited, and a wrapper forwarding to a partial releaser degrading to plain transitively. Full suite green (ownir 236/236); no existing behaviour depended on the flattened consume. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
…ly (TZ D5)
The bridge wraps the interprocedural summary solve in a blanket
'except Exception: mos = {}': the right call (never crash the checker),
but it put the ENTIRE interprocedural layer out silently — every
cross-method consume/borrow/fresh contract skipped with no trace, against
the honest-skip culture every other coverage gap follows (OWN050).
to_module now takes an optional notes out-list (the loc-counter house
pattern) and records the degrade reason; check_facts surfaces each as an
advisory OWN052 finding — file-level (no single C# site failed),
module-scoped, advisory like OWN050: rendered as a warning, level:note
in SARIF (region omitted for line 0), never the exit code. The
__main__ summary names the advisory codes actually present instead of
the hard-coded '(OWN050)' label — byte-identical output when only
OWN050 notes exist. 'explain OWN052' answers with the long form.
Tests: a patched-to-raise solver yields exactly one OWN052 and zero
fabricated verdicts (forwards degrade to plain, the caller stays
silent); the same facts with a healthy solver carry no OWN052 and keep
their true OWN002. No real facts input can make solve() throw today —
which is exactly why the silent except went unnoticed.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
…t (TZ D2) The two-axis d5 model reserves an escape axis orthogonal to transfer, but no producer sets it: skeleton derivation always leaves False, so ParamSummary.escapes is constant False in every real run. to_dict still emitted it — and the summary dump is about to become the stage-1 Python<->Rust parity artifact, which would freeze an always-False lie into the frozen surface (and force the Rust port to reproduce a field that carries no information). to_dict now omits the field until a producer lands; the model keeps the axis (fields stay, documented RESERVED in ownership.py), and a test pins the omission so re-adding it is a deliberate act paired with the producer, not a drive-by. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
… D3) The solver's contrib() understands adopt and return as must-transfer, but skeleton derivation never emits them (adopt awaits interprocedural T4b ctor-adopt summaries; a returned param is deliberately not a consume signal until owned return values are modelled). Without the marker a port would carry dead semantics as live and could expect them from real facts. The PathAction docstring now names both as RESERVED with each kind's activation condition. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
… parity surface) 'python -m ownlang summaries facts.json' prints the solved Method Ownership Summaries plus the extern-boundary log as one deterministic JSON document: summaries sorted by method key, the unresolved log sorted by solve_with_log, fixed field order — byte-identical output under any functions[] input permutation (pinned by test). Two consumers, one contract: the debugging answer to 'why did this call stay plain/consume/fresh' without reading bridge code, and the frozen surface the Rust port of the inference layer will be diffed against — summary- level parity is finer than diffing final diagnostics, where an inference bug can hide behind an unrelated silence. Skeletons now carry the declaring file from the facts (merged overloads take the smallest (file, line) pair so the dump stays input-order- independent); a failed solve degrades exactly like the checking path — empty summaries with the reason in 'degraded', rc stays 0 (the surface reports state, it does not judge), rc 2 only for unreadable facts. Wiring into oracle_exact SURFACES rides with the Rust own-bridge consumer, which does not exist yet. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
…/unknown call (TZ D6)
d5 §5's optimistic default says an unverified-ownership call site resolves
to 'the caller no longer owns' -> silence. The implementation lowered
may/unknown contracts to a PLAIN arg instead — which is not silence: plain
leaves the obligation with the caller, so DROPPING a local after a
may-call fabricated OWN001. The channel predates D1 (conditional
forwards), but the D1 fix widened it to every null-guard dispose helper:
'var r = new X(); Cleanup(r);' — the normal usage, Cleanup IS the
disposer — read as a leak.
Untrack makes the default real: _unverified_transfer_calls collects every
arg at a may/unknown position of a summarized callee; such locals are not
minted at all (acquire / fresh result / alias target skipped, branch-hoist
excluded), so neither a missing nor a defensive dispose after the call can
be charged. A call with may/unknown positions routes through the existing
per-argument $consume/$borrow channel (the overload path, now shared) so
an untracked name is never referenced in emitted code — the first run's
loud OWN030 (map-or-raise doing its job) proved why. Verified contracts
are untouched: borrow-drop keeps its true OWN001 (T3) and consume-reuse
its OWN002 (T2), both pinned.
The gap is now honest instead of silent-or-wrong: advisory OWN051
('ownership transfer unverified — local not checked past this call') at
the call site, gated on args that actually carry an obligation (acquired
or fresh-factory locals — no noise for plain values), advisory like
OWN050/052: warning, SARIF note, never the exit code, hidden at
--verbosity quiet. explain OWN051 answers. Seven existing may-shape tests
updated from 'empty' to 'exactly one OWN051 advisory'; three new tests pin
the closed FP, the preserved T3 recall, and the owned-local gate.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
Owner
Author
|
@codex review and propose changes |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f9e4f04df2
ℹ️ 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".
…layer (roadmap stage 0) Lifts the verdict-determining inference layer from an undocumented bridge concern (architecture-review R2, tech-debt-register §3's hard port prerequisite) into a normative, descriptive spec pinned by tests — the same posture as OwnIR.md. Covers: the MOS artifact and its two axes; the transfer lattice and join (INF-L); parameter skeleton derivation (INF-S, incl. the definite-release rule from D1 and the reserved adopt/return kinds from D3); return inference (INF-R); overload merge and the arity residual (INF-M); the SCC-condensation fixpoint (INF-F, incl. the observable-degradation rule from D5); call-site application and the tier ladder (INF-A, incl. the optimistic untrack from D6); the reporting policy and advisories OWN051/OWN052 (INF-P); the deterministic summary-dump serialization (incl. the omitted escapes axis from D2). Honestly marks every reserved element (escapes, adopt/return, strict mode, Tier C, source tiers beyond 'inferred') as 'in the model, no producer'. §11 maps every INF-* rule to its pinning test in test_ownership.py / test_ownir.py; registered in spec/README.md; OWN051/052 documented in spec/Diagnostics.md with a new interprocedural-advisory section. A conformance check pins the codes the spec names to the catalogue. Full suite green (ownir 245/245). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
Owner
Author
|
@codex is all good |
|
You have reached your Codex usage limits. You can see your limits in the Codex usage dashboard. |
Owner
Author
|
@codex is all good |
Summary
Testing
Note: the working tree still has an unrelated untracked file, |
# Conflicts: # ownlang/__main__.py
Codex's follow-up run flagged two Ruff findings its sandbox commit never reached this branch with: the un-formatted import block in cmd_summaries (I001) and the quoted Finding annotation in to_module (UP037). Applied the same fixes here.
…rdicts (Codex P1+P2) Two review findings on the interprocedural layer, both reproduced before fixing: P2 (S2 / INF-S3): a body like 'if (c) return; Sink(x)' kept exactly one top-level forward, so the shape counted as an unconditional handoff and solved to must — leaking the callee's own parameter on the guard path and charging the caller's defensive Dispose a false OWN002. The unconditional test now also requires no return reachable before the forward (_early_return_before_forward), the forward twin of D1's partial-release rule. Recorded as TZ D7. P1 (INF-A5): the optimistic untrack applied to the whole body, so a local passed to a may/unknown position anywhere lost its PRE-call verdicts too (acquire s; release s; use s; maybe(s) reported nothing but OWN051). Split into two mechanisms (_kill_sites_for_unverified): a top-level unverified call keeps the local fully tracked up to the call, discharges it there with a $consume on the handle (sound: a top-level call lies on every path to the exit), and unmaps it after — so the checked region now matches OWN051's 'not checked past this call'. In-branch calls keep the conservative whole-body untrack (a branch-local discharge would fabricate OWN001/OWN009 on the other path); the residual is recorded in TZ D6 and INF-A5b. Spec: INF-S3 + INF-A5a/A5b updated, conformance list extended. Tests: 3 new pins (pre-call OWN002 beside OWN051, post-call silence, early-return forward), 248/248 bridge checks green.
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.
Что и зачем
Сводит разрозненное состояние межпроцедурного слоя (d5-нота, tech-debt register §3, трекеры #122/#146, arity-остаток d5 §10 q2) в один секвенированный roadmap (стадии 0–6: спека bridge-инференции → наблюдаемость OWN051/MOS-дамп → arity-ключ → aliasOf через return → publisher provenance → exclusivity → Tier C аннотации), плюс выполняет стадии 0–1 по ходу: нормативная спека
spec/Inference.md+ рабочее ТЗ, CLI-командаsummaries(детерминированный parity-дамп MOS), advisory-коды OWN051/OWN052, и исправления, найденные при написании ТЗ (D1 частичный release →may; D2 мёртвая осьescapes; D5 наблюдаемая деградация решателя; D7 раннийreturnдо форварда →may; kill-site-уточнение untrack-семантики — до-вызовные вердикты больше не глотаются).Тип изменения
Как проверено
python tests/run_tests.py— зелёный (132/132 analysis, 248/248 bridge, 45/45 ownership, 70/70 obligations, 3000 fuzz)ruff check .иmypy— чистоСвязанные issue
Refs #122, #146 (deferred-трекеры, секвенированы в roadmap). Closes нет.
Чеклист
test_ownir.py+ существующие D1/D5/D6-матрицы)spec/Inference.md,spec/Diagnostics.md,spec/README.md, roadmap + ТЗ, d5-нота)docs:,fix:,feat:,spec:)Co-Authored-By: Claude noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi
Summary by CodeRabbit
ownlang summariesCLI command to emit deterministic solved method-ownership summaries from an OwnIR facts file.dump_summariesAPI for generating summaries, unresolved entries, and degradation details.