docs: define interprocedural semantic architecture - #303
Conversation
|
Warning Review limit reached
Next review available in: 34 minutes Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (2)
✨ 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 |
![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: 337376314c
ℹ️ 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".
…jection Two P2 review points on the "Incrementality and caching" section, both accepted: - Recursive SCCs: per-method keys that embed callee summary hashes are circular inside a recursive component (A's key needs B's cached summary and vice versa). The cacheable unit for a recursive component is now the SCC itself, keyed by the members' local inputs plus dependencies OUTSIDE the component — reconstructible bottom-up over the acyclic condensation. Cross-member hashes are validated after load, never used for lookup. - Evidence spans: a semantic body hash survives pure line movement while cached spans go stale. Cache hits reuse semantic effects and evidence structure only; spans are re-projected from current frontend facts at diagnostic time (the existing "formatting is a projection" rule), i.e. a cached span is valid only with the source-map version it was minted against. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015de4MezSeUnZBoWq1fFU5M
…, enrollment split Four blockers plus the smaller fixes from the architecture review: 1. Migration plan no longer describes merged work as future. #258 is closed (spec/Bridge.md is the merged normative contract); #278 is closed by #293 and extended to WPF002 Stop() by #302 — those landed extractor predicates are named the current bounded implementation and the regression floor. Phase 2 is retargeted to the new post-cutover tracker #304 (summary-backed lifecycle release reachability); #278 stays the historical motivating incident, not a reusable implementation issue. 2. MVP guarded-effects policy defined: summaries preserve guards over simple boolean/null parameter predicates, callsite application substitutes statically-known constants, anything outside that vocabulary degrades to May/Unknown — never Must, never silence. Without this the summary layer loses to the landed predicates on the flagship Teardown(bool) case. input_contract semantics defined in the summary envelope. 3. Lifecycle reasoning split into two theorems: LifecycleEffect (release happens IF the root runs) vs LifecycleEnrollment (this instance provably reaches that root). Effect without enrollment is degraded/conditional, never clean — a perfect Dispose() nobody calls proves nothing. 4. Bridge-boundary authority table added: until parity+cutover #258/#259 own the boundary (MOS in own-bridge, byte-parity); after cutover a dedicated extraction slice per this proposal; wire schema, verdicts, and parity artifacts invariant across both. Also: OwnCFG claim corrected to intended-MIR-equivalent (today: plain succ edges, calls as instructions, AST re-export); Call-instruction vs Invoke-terminator model made explicit; evidence split into a single proof DAG vs a per-finding displayed witness. Refs #303 review; tracker: #304. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015de4MezSeUnZBoWq1fFU5M
…opt-in Arbiter re-review of 1b65d01: all prior blockers closed; one P2 remained — "Invoke is the terminator form a domain opts into" let each analysis domain request its own CFG shape, silently turning the shared substrate into a family of domain-specific CFGs (breaking shared summaries, deterministic serialization, and cache keys). Lowering now selects Call vs Invoke deterministically from the configured CFG profile and frontend facts; when exceptional/suspension flow is represented, the call is Invoke for ALL domains — a domain may ignore those successors but never alters the lowering for the same method and profile. Two textual fixes from the same round: the opening summary now matches the detailed section (OwnCFG is the local-analysis substrate INTENDED to become MIR-equivalent, not already it), and #259 is no longer past tense (#258 specified the contract so #259 can port under it — #259 is still open). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015de4MezSeUnZBoWq1fFU5M
2 participants
What changed
P-036, a docs-only proposal that names the missing interprocedural architecture between the external OwnIR seam and future cross-method verdicts;-=releases only in a proven, unguarded teardown context #293/fix(extractor): WPF002 Stop() teardown soundness — one doctrine with-=#302 predicates (historical motivator Soundness: OWN001 treats any-=in the class as a release — a-=behind a flag, or in a method nobody calls, silently swallows a real leak (heap-proven on SectorTS) #278), P-025/P1: Add Obligation Protocols for project-specific barrier-sensitive rules #272/P2: Extend MOS/effect summaries to protocol and barrier effects #274 obligations, feat(progress): Own.Progress — detect consume-or-exit loop stalls (PRG001) #275 progress, D5.1c: interprocedural exclusivity (borrow_mut) axis for MOS wrapper summaries #122/Subscription precision: suppress+=on a publisher that escapes by return (interprocedural — the dual of ownership transfer) #146, and Own.Concurrent: retrofit structured-concurrency contracts onto existing C# async code #282;docs/proposals/README.md.Review rounds incorporated on top of the original text:
-=releases only in a proven, unguarded teardown context #293/fix(extractor): WPF002 Stop() teardown soundness — one doctrine with-=#302 reality and retargeted to the new post-cutover tracker Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304; MVP guarded-effects policy (bool/null parameter predicates, constant substitution, degrade-to-May/Unknown) withinput_contractsemantics; LifecycleEffect vs LifecycleEnrollment split (effect without enrollment is never clean); the P-022/P-022 step 6b: implement Rust own-bridge with layered OwnIR parity #259 vs P-036 bridge-boundary authority table;Call/Invokelowering is selected deterministically by the CFG profile, never by an analysis domain (one method, one profile, one CFG shape); opening summary matches the detailed OwnCFG section (intended MIR-equivalent, not current state); P-022 step 6b: implement Rust own-bridge with layered OwnIR parity #259 no longer referred to in past tense.Why
The repository already has OwnIR facts, CFG, a worklist analysis core, MOS inference, and an interprocedural roadmap. What is missing is one explicit design document that says which layer owns normalization, local flow, call resolution, summaries, evidence, and future analysis domains. Without that boundary,
own-bridgerisks becoming the permanent home of every new semantic.Scope and behavior
Docs only. No production code, schema, diagnostic, oracle, or runtime behavior changes. The proposal explicitly preserves the P-022 verdict-changing feature freeze until the Rust parity/cutover discipline permits implementation.
Validation
mainand 0 behind;