From 40f95eddbc31dc97ba257d6d5845339883219c46 Mon Sep 17 00:00:00 2001
From: PhysShell <45852143+PhysShell@users.noreply.github.com>
Date: Mon, 20 Jul 2026 06:28:30 +0500
Subject: [PATCH 1/5] docs: add interprocedural semantic architecture proposal

---
 ...6-interprocedural-semantic-architecture.md | 1016 +++++++++++++++++
 1 file changed, 1016 insertions(+)
 create mode 100644 docs/proposals/P-036-interprocedural-semantic-architecture.md

diff --git a/docs/proposals/P-036-interprocedural-semantic-architecture.md b/docs/proposals/P-036-interprocedural-semantic-architecture.md
new file mode 100644
index 00000000..f94962d7
--- /dev/null
+++ b/docs/proposals/P-036-interprocedural-semantic-architecture.md
@@ -0,0 +1,1016 @@
+# P-036 - Interprocedural semantic architecture
+
+Status: **draft**
+
+Related work:
+
+- [P-016 - deep C# fact extraction](P-016-deep-fact-extraction.md)
+- [P-022 - Rust core migration](P-022-rust-core-migration.md)
+- [P-025 - obligation protocols](P-025-obligation-protocols.md)
+- [`spec/Inference.md`](../../spec/Inference.md)
+- [`docs/notes/interprocedural-roadmap.md`](../notes/interprocedural-roadmap.md)
+- [`docs/notes/interprocedural-tz.md`](../notes/interprocedural-tz.md)
+- #258 / #259 / #260: bridge contract, Rust bridge, dual-engine parity
+- #278: a release that exists syntactically but is not reachable
+- #272 / #274: obligation protocols and protocol/effect summaries
+- #275: consume-or-exit loop progress
+- #122 / #146: exclusivity and publisher provenance
+- #282: structured-concurrency contracts
+
+## Decision in one paragraph
+
+Own.NET should treat interprocedural analysis as a first-class semantic layer, not
+as additional logic inside AST visitors or the OwnIR bridge. The external
+versioned **OwnIR** JSON contract remains the frontend seam. It lowers into an
+internal, typed, syntax-independent **OwnHIR** method representation. The
+existing **OwnCFG** is the MIR-equivalent control-flow representation and should
+remain the execution substrate for local dataflow. A derived call graph and
+first-class **MethodSummary** artifacts carry effects across method boundaries.
+A generic SCC/fixpoint summary engine composes domain-specific summaries for
+ownership, obligations, progress, regions, and tasks. Diagnostics consume
+ordered derivation evidence from those layers. OwnAudit remains the runtime
+witness/correlation consumer; 007 remains the gate and replay consumer.
+
+This proposal names and separates the elephant already visible in the current
+code and roadmap. It does not replace the shipped MOS solver, the existing CFG,
+or the P-022 parity plan. It defines the architecture those pieces should grow
+into after the Rust cutover instead of allowing `own-bridge` to become the
+permanent home of every future semantic.
+
+## Motivation
+
+Own.NET already has more than a raw AST checker:
+
+- frontends emit versioned OwnIR facts;
+- `.own` source has a parser and AST;
+- `own-cfg` provides canonical intraprocedural CFG lowering;
+- `own-analysis` has a worklist solver and several flow-sensitive domains;
+- `ownership.py` already performs SCC condensation and bottom-up MOS inference;
+- `spec/Inference.md` normatively defines the current method-ownership summaries;
+- diagnostics already carry ordered Evidence and SARIF code flows.
+
+The missing part is an explicit architectural home for the semantics between a
+frontend fact and a cross-method verdict.
+
+Today, `ownlang/ownir.py` is not merely a JSON loader. It validates facts,
+normalizes identities, lowers flow operations, mints handles and RIDs, resolves
+calls, infers method ownership summaries, applies branch-local behavior,
+prepares DI/effect inputs, drives analyses, and maps results back to source
+locations. #258 correctly treats this as verdict-determining behavior that must
+be specified before #259 ports it.
+
+That concentration was acceptable for the proof of concept. It is not an
+acceptable permanent substrate for the next classes of work:
+
+- #278 needs release reachability through lifecycle call chains, not a class-wide
+  search for a matching `-=` or `Stop()`;
+- obligation protocols need effects to be produced in one method and discharged
+  in another;
+- loop progress needs callees to summarize whether they advance a controlling
+  measure or exit;
+- field, closure, timer, and callback escapes need stable places and heap
+  identities rather than syntax-node coincidence;
+- async and structured concurrency need task creation, capture, join, cancel,
+  and scope effects to cross method boundaries;
+- runtime correlation needs a static derivation trace with stable identities,
+  not only a final warning line.
+
+Adding each of these as another special case in the bridge would preserve the
+file layout while destroying the architecture. The result would be a second
+compiler hidden inside a deserializer, with more side effects than a pharma
+commercial.
+
+## Scope
+
+This proposal defines:
+
+1. the distinction between external OwnIR and internal semantic IR;
+2. the internal method representation used by all frontends;
+3. the role of the existing CFG as the MIR-equivalent local execution model;
+4. call-target and call-graph representation;
+5. first-class, serializable method summaries;
+6. SCC/fixpoint composition of summaries;
+7. domain boundaries for ownership, protocols, progress, regions, and tasks;
+8. evidence and uncertainty requirements;
+9. an incremental migration sequence compatible with P-022 parity;
+10. acceptance criteria for the first real consumer, #278.
+
+## Non-goals
+
+This proposal does **not**:
+
+- change verdicts before the P-022 Rust-default cutover gate (#262);
+- replace Roslyn or reimplement C# semantics in Rust;
+- turn OwnLang into a language users must author;
+- build a complete C# compiler or a sound whole-program points-to analysis;
+- require LLVM IR, MLIR, SSA, IFDS, separation logic, or Datalog in the first
+  implementation;
+- make `own-bridge` a generic analysis engine;
+- move runtime heap analysis into Own.NET;
+- move static semantics into OwnAudit;
+- make 007 a checker;
+- claim formal proof of arbitrary C# behavior;
+- promise perfect resolution of reflection, dynamic dispatch, native callbacks,
+  or third-party code without models.
+
+The target is a compositional, evidence-producing analysis architecture with
+explicit uncertainty. It is not omniscience wearing a compiler badge.
+
+## Terminology and layer boundaries
+
+### External OwnIR
+
+**OwnIR** keeps its current meaning: the versioned JSON fact contract emitted by
+Roslyn and future frontends. It is a wire format and compatibility seam.
+
+OwnIR should describe what the frontend learned from the source environment:
+
+- canonical symbols and signatures;
+- source spans;
+- declarations and calls;
+- resource/protocol observations;
+- frontend-resolved types and targets;
+- explicit unknown or degraded resolution;
+- language/framework-specific facts that the bridge can normalize.
+
+OwnIR is not the solver IR. It may preserve source-level facts that are useful
+for compatibility but inconvenient for analysis. It must not become a dump of
+Rust implementation structs.
+
+### OwnHIR
+
+**OwnHIR** is the internal, typed, syntax-independent semantic representation.
+It normalizes different frontend spellings into the operations the analyses
+actually understand.
+
+The name is intentionally modest. OwnHIR is not a second user language and not
+another wire contract. It is an internal program model that can be constructed
+from:
+
+- OwnLang AST;
+- C# OwnIR facts;
+- future TypeScript/JVM facts;
+- synthetic test fixtures.
+
+A first vocabulary should include operations such as:
+
+```text
+Acquire(resource, kind)
+Use(place)
+Borrow(place, permission)
+Transfer(place, destination)
+Release(place, protocol_event)
+StoreField(base, field, value)
+LoadField(base, field)
+AliasJoin(left, right)
+ProtocolEvent(subject, protocol, event)
+Call(callsite, target_set, receiver, arguments, result)
+Return(value)
+Throw(value)
+Await(task)
+SpawnTask(task, captures)
+JoinTask(task)
+CancelTask(task)
+Barrier(kind, subject)
+Progress(measure, relation)
+```
+
+The exact enum is a later spec. The architectural rule is immediate: analyses
+consume normalized semantic operations, not Roslyn syntax kinds and not bridge
+JSON dictionaries.
+
+### OwnCFG
+
+The existing **OwnCFG** is the MIR-equivalent layer. It should represent each
+method as basic blocks containing OwnHIR operations and explicit terminators:
+
+```text
+Goto
+Branch
+Switch
+Call
+Return
+Throw
+AwaitSuspend
+```
+
+Normal, exceptional, and suspension edges must be distinguishable when a domain
+cares about them.
+
+This proposal does not require a separate `OwnMIR` merely to imitate compiler
+naming conventions. A new layer is justified only by a semantic difference. If
+OwnCFG already provides normalized linear instructions in basic blocks, calling
+another copy MIR would add letters, files, and opportunities for drift while
+adding no reasoning power.
+
+### Interprocedural graph
+
+The interprocedural graph is a derived view over methods and callsites:
+
+- method nodes;
+- callsite nodes or labelled call edges;
+- candidate callees;
+- return continuations;
+- exceptional continuations;
+- lifecycle roots and framework callbacks;
+- unresolved/external targets with explicit precision.
+
+The graph should not be the sole source of truth. Method CFGs and callsite
+bindings remain canonical; the call graph and ICFG are derived and rebuildable.
+
+### MethodSummary
+
+A **MethodSummary** is the first-class interprocedural artifact. It records only
+the behavior observable across a method boundary. Internal temporary variables
+and block identities do not escape into the summary.
+
+The existing MOS is the first summary domain, not a disposable special case.
+Future domains extend the same composition architecture.
+
+## Target architecture
+
+```text
+                    FRONTENDS
+
+  .own source          C# / Roslyn          future TS/JVM
+      |                    |                     |
+  own-syntax AST       OwnIR facts           OwnIR facts
+      |                    |                     |
+      +--------- frontend-specific lowering ----+
+                           |
+                           v
+                       OwnHIR
+          typed places, calls, semantic operations
+                           |
+                           v
+                       OwnCFG
+       basic blocks, normal/exception/suspend edges
+                           |
+             +-------------+--------------+
+             |                            |
+             v                            v
+        Local analyses              Call graph / ICFG
+   ownership, loans, regions       targets, roots, SCCs
+             |                            |
+             +-------------+--------------+
+                           v
+                  MethodSummary engine
+       infer, join, apply, cache, explain, serialize
+                           |
+          +----------------+-------------------+
+          |                |                   |
+          v                v                   v
+    Ownership/MOS     ObligationSummary   ProgressSummary
+          |                |                   |
+          +----------------+-------------------+
+                           |
+                 later Region/Task summaries
+                           |
+                           v
+                  Diagnostics + Evidence
+                           |
+                 text / SARIF / ownreport
+                           |
+        +------------------+------------------+
+        |                                     |
+        v                                     v
+     OwnAudit                            007 consumers
+ runtime witness/correlation        gates, replay, promotion
+```
+
+## Program identities and places
+
+Interprocedural ownership analysis fails quickly if identity is based on source
+text or object addresses. The internal representation needs stable IDs.
+
+Recommended identity families:
+
+```text
+MethodId
+TypeId
+FieldId
+ParameterId
+LocalId
+CallsiteId
+AllocationSiteId
+ResourceId
+ProtocolInstanceId
+TaskId
+BlockId
+```
+
+Recommended place model:
+
+```text
+This
+Parameter(method, index)
+Local(method, local_id)
+StaticField(field_id)
+Field(base_place, field_id)
+ReturnValue(callsite_id)
+Allocation(allocation_site_id)
+Captured(closure_or_task, place)
+UnknownHeap(type_or_region)
+```
+
+The first implementation does not need a perfect heap model. It needs a model
+that is better than matching variable names:
+
+- field-sensitive for project-local fields;
+- allocation-site-sensitive for resources created in analyzed code;
+- receiver/type based for modeled external APIs;
+- an explicit `UnknownHeap` fallback;
+- no conversion of unknown identity into a silent clean result.
+
+## Call resolution
+
+Every callsite records both targets and resolution precision:
+
+```text
+Exact(method)
+FiniteSet(methods)
+External(model_key)
+Unknown(reason)
+```
+
+Resolution may use:
+
+- the Roslyn-resolved `IMethodSymbol` and canonical signature;
+- static/private/sealed dispatch;
+- conservative virtual/interface target sets;
+- delegate targets when statically known;
+- framework callback models;
+- external annotations and resource model files;
+- explicit unknown fallback.
+
+A call by textual method name is a compatibility fallback, not the target
+architecture. The shipped signature work in the interprocedural roadmap is the
+minimum identity baseline.
+
+## Summary domains
+
+### Common summary envelope
+
+Every domain-specific summary should share a common envelope:
+
+```text
+MethodSummary {
+    method_id
+    input_contract
+    normal_exit_effect
+    exceptional_exit_effect
+    unresolved_calls
+    precision
+    dependencies
+    evidence
+    format_version
+}
+```
+
+`dependencies` records the callee summaries and external models used to derive
+the result. This makes invalidation, explanation, and differential replay
+possible.
+
+### Ownership summary
+
+The current MOS remains authoritative for existing behavior. Its future internal
+shape may include:
+
+```text
+ParameterEffect = Plain | Borrow | BorrowMut | Consume | MayEscape | Unknown
+ReturnEffect = Plain | Fresh | AliasOf(parameter) | AliasOf(receiver) | Unknown
+ReceiverEffect
+FieldEffects
+MayAcquire
+MayRelease
+MustRelease
+MayLeaveLive
+```
+
+The critical distinction is **may** versus **must**. A release on one branch is
+not a release on all branches. Unknown is not clean.
+
+### Obligation summary
+
+Obligation protocols need summaries that can create, transform, discharge, or
+propagate obligations:
+
+```text
+Produces(protocol_state, subject)
+Discharges(protocol_state, subject)
+Transforms(from, event, to)
+Requires(before_call)
+Forbids(after_barrier)
+Propagates(subject_mapping)
+```
+
+Example:
+
+```text
+BeginTransaction:
+    produces MustEventually(CommitOrRollback, return)
+
+Commit:
+    discharges MustEventually(CommitOrRollback, receiver)
+```
+
+This is the architectural destination of P-025 and #274. It is not a second
+protocol engine in the bridge.
+
+### Progress summary
+
+#275 needs a domain that describes whether a method advances a measure or exits:
+
+```text
+MustAdvance(measure, relation)
+MayAdvance(measure, relation)
+MustExit
+MayExit
+NoProgress
+Unknown
+```
+
+At a loop back-edge, the local CFG analysis combines local mutations with callee
+progress summaries. A call named `ReadNext` does not count as progress merely
+because a human chose an optimistic verb.
+
+### Region summary
+
+Region/lifetime summaries describe captures and escapes:
+
+```text
+Escapes(parameter, destination_region)
+Captures(receiver_or_parameter, owner)
+ReturnsBorrowedFrom(parameter_or_receiver)
+Promotes(subject, region)
+```
+
+This extends the existing lifetime/DI region reasoning without moving DI
+registration extraction into the generic solver.
+
+### Task summary
+
+Structured-concurrency work should wait until narrower async facts are stable.
+When introduced, the summary domain should include:
+
+```text
+Spawns(task, captures)
+ReturnsTask(task)
+Awaits(task)
+Joins(task)
+Detaches(task)
+Cancels(task)
+RequiresJoinBefore(scope_exit)
+```
+
+This is a future consumer of the architecture, not a prerequisite for the first
+implementation.
+
+## Summary inference and composition
+
+### Local analysis
+
+Each method is analyzed over its OwnCFG with current callee summaries as input.
+A domain transfer function updates an abstract state for each instruction.
+Control-flow joins use the domain lattice and preserve may/must distinctions.
+
+### Callsite application
+
+At a callsite, formal places are bound to actual places:
+
+```text
+callee.receiver -> caller actual receiver
+callee.parameter[0] -> caller argument[0]
+callee.return -> caller result place
+```
+
+The callee summary is instantiated through that binding and applied to the
+caller state. This gives callsite-sensitive effects without requiring a unique
+summary for every caller.
+
+### SCC and recursion
+
+The call graph is condensed into strongly connected components. Acyclic SCCs
+are solved bottom-up. Recursive SCCs iterate summaries to a fixpoint:
+
+```text
+summary_0 = bottom or explicit unknown baseline
+summary_n+1 = analyze(method, summaries_n)
+stop when all summaries stabilize
+```
+
+Every domain must define a finite-height lattice or a widening strategy. The
+existing ownership solver already demonstrates the SCC/fixpoint pattern; the
+new architecture generalizes its home and artifacts rather than replacing its
+semantics.
+
+### Context sensitivity
+
+Default policy:
+
+- one context-insensitive summary per resolved method signature;
+- callsite-sensitive parameter/receiver binding;
+- allocation-site/resource-sensitive facts where available;
+- selective specialization only when an observed false positive/negative
+  justifies it.
+
+Possible later specializations:
+
+- receiver-type-sensitive virtual summaries;
+- one-callsite sensitivity for wrapper/factory patterns;
+- bounded generic instantiation keys;
+- framework lifecycle contexts.
+
+Unbounded call strings are not an MVP. Precision is useful; combinatorial
+self-harm is not.
+
+## Unknown and external calls
+
+Unknown behavior must be visible and policy controlled.
+
+The engine distinguishes:
+
+1. **analyzed body**: infer a summary;
+2. **trusted model**: apply a versioned external summary;
+3. **finite but unresolved target set**: join candidate summaries;
+4. **unknown target**: apply conservative domain defaults and record degraded
+   precision;
+5. **unsupported construct**: emit an advisory or explicit skip reason.
+
+External models belong in declarative model files or dedicated framework model
+modules. They do not belong as scattered name tables in analysis transfer
+functions.
+
+Optimistic and pessimistic policies may differ by check, but both consume the
+same explicit `Unknown` evidence. A rule may choose not to fail CI on unknown;
+it may not pretend the call was proven harmless.
+
+## Lifecycle roots and reachability
+
+#278 shows that intraclass syntax matching is not lifecycle reasoning. A
+reachable-release analysis needs explicit roots and entry contracts.
+
+Examples of roots:
+
+- `IDisposable.Dispose` / `IAsyncDisposable.DisposeAsync`;
+- WPF `Closed`, `Unloaded`, `OnClosed`, and modeled framework teardown;
+- DI scope disposal;
+- application shutdown;
+- test fixture teardown;
+- project-declared lifecycle methods.
+
+For each acquired obligation, the analysis should answer:
+
+```text
+Which lifecycle roots can own this resource?
+Which root-to-exit paths are reachable?
+Which callees are traversed?
+Is release guaranteed on every required path?
+Which path proves the missing release?
+```
+
+A release in a dead method, an unregistered callback, or a conditional branch
+must not discharge a must-release obligation globally.
+
+## Evidence and explanations
+
+Every interprocedural conclusion should be explainable without reading solver
+code.
+
+Required evidence kinds:
+
+```text
+Acquire
+Call
+CallTarget
+SummaryApplied
+Branch
+Return
+ExceptionalReturn
+Transfer
+Escape
+ProtocolTransition
+Release
+Barrier
+LoopBackEdge
+UnknownCall
+ModelApplied
+```
+
+A #278-style finding should be able to render a witness such as:
+
+```text
+Subscription acquired at ViewModel.cs:42
+Close() called from OnClosed() at ViewModel.cs:91
+Close() calls Cleanup() at ViewModel.cs:96
+Cleanup() reaches `return` when `_flag == false`
+Unsubscribe at ViewModel.cs:121 is not reached on that path
+```
+
+The evidence graph should retain stable method/callsite/resource IDs and source
+spans. Diagnostic formatting is a projection. OwnAudit may correlate those IDs
+with runtime resource identities and classify the result as static-only,
+runtime-only, or confirmed. OwnAudit does not recompute the static summary.
+
+## Incrementality and caching
+
+The IDE path is a primary P-022 motivation, so summaries must be cacheable.
+
+A summary cache key should include at least:
+
+```text
+method body semantic hash
+resolved signature
+relevant frontend fact/model versions
+analysis domain version
+callee summary dependency hashes
+configuration/profile hash
+```
+
+Changing a leaf method invalidates:
+
+1. its local CFG/summary;
+2. callers that depended on the changed summary;
+3. affected SCC peers;
+4. diagnostics whose evidence depends on changed artifacts.
+
+It should not invalidate unrelated methods because a source file timestamp
+changed. The dependency graph in each summary is therefore a correctness input,
+not only a performance optimization.
+
+## Logical module boundaries
+
+The exact Rust crate split is an implementation decision, but the logical
+boundaries are required:
+
+### Frontend / OwnIR
+
+Responsibilities:
+
+- source-language semantic resolution;
+- canonical symbols, signatures, spans;
+- OwnIR serialization;
+- explicit degradation.
+
+Must not:
+
+- infer ownership verdicts;
+- run protocol fixpoints;
+- decide CI severity.
+
+### Bridge lowering
+
+Responsibilities:
+
+- validate OwnIR;
+- normalize identities;
+- lower facts to OwnHIR;
+- report unmappable facts explicitly.
+
+Must not:
+
+- own domain-specific fixpoint semantics;
+- contain the permanent MOS/protocol/progress solver;
+- emit final findings except malformed/unmappable-input diagnostics.
+
+`own-bridge` may remain the public facade during migration, but internally it
+must delegate these responsibilities instead of remaining one verdict-owning
+module.
+
+### CFG
+
+Responsibilities:
+
+- basic blocks and terminators;
+- normal/exception/suspend edges;
+- local dominance/reachability helpers;
+- deterministic serialization for parity/debugging.
+
+Must not:
+
+- know WPF policy;
+- decide resource protocols;
+- construct SARIF.
+
+### Interprocedural engine
+
+Responsibilities:
+
+- call graph and lifecycle roots;
+- SCC condensation;
+- generic summary iteration;
+- summary dependency tracking;
+- external model lookup;
+- summary dumps and traces.
+
+Must not:
+
+- hard-code every domain lattice;
+- parse Roslyn syntax;
+- render user diagnostics.
+
+### Analysis domains
+
+Responsibilities:
+
+- define lattices and transfer functions;
+- define summary join/apply semantics;
+- produce domain-neutral derivations;
+- turn proven violations into diagnostic data.
+
+Each domain should be an independent implementation over common CFG and summary
+interfaces. The current interleaving inside a single analyzer is migration debt,
+not the desired design.
+
+### Diagnostics and evidence
+
+Responsibilities:
+
+- stable diagnostic/evidence data model;
+- human text, SARIF, ownreport projection;
+- deterministic ordering;
+- source-location rendering.
+
+Must not:
+
+- rerun analysis;
+- infer missing call targets;
+- mutate summaries.
+
+## Repository responsibility boundary
+
+### Own.NET
+
+Own.NET owns:
+
+- OwnIR, OwnHIR, OwnCFG;
+- call graph and summary semantics;
+- static ownership/protocol/progress/region/task domains;
+- diagnostic derivations;
+- static uncertainty.
+
+### OwnAudit
+
+OwnAudit owns:
+
+- runtime acquisition/release witnesses;
+- heap retention and lifecycle observations;
+- static/runtime correlation;
+- confirmed/static-only/runtime-only buckets;
+- audit aggregation and remediation workflow.
+
+OwnAudit consumes Own.NET artifacts. It does not become the second static
+checker.
+
+### 007
+
+007 owns:
+
+- execution gates;
+- artifact capture;
+- replay and promotion;
+- policy over evidence completeness;
+- orchestration across repositories.
+
+007 consumes reports and evidence. It does not infer ownership or protocol
+summaries.
+
+## Migration plan
+
+### Phase 0 - documentation and parity freeze
+
+Timing: before #262.
+
+- Land this proposal as architecture direction only.
+- Finish #258 and merge the normative current bridge contract.
+- Preserve the verdict-changing inference freeze.
+- Add no new summary axis in only one engine.
+- Treat current summary dumps and diagnostics as parity artifacts.
+
+Acceptance:
+
+- no production behavior change;
+- no oracle drift;
+- no new crate required merely to land the proposal.
+
+### Phase 1 - internal seam after Rust bridge parity
+
+Timing: after #259/#260 are stable, ideally after #262.
+
+- Introduce an explicit internal method/operation representation, whether named
+  `OwnHIR` in code or represented by equivalent Rust types.
+- Make bridge lowering produce that representation.
+- Move generic call graph/SCC/summary orchestration out of bridge-specific logic.
+- Preserve existing MOS behavior exactly.
+- Emit deterministic method-summary and call-graph dumps.
+
+Acceptance:
+
+- Python/Rust or old/new shadow comparison remains zero-diff;
+- `own-bridge` validation/lowering is testable independently from analysis;
+- MOS can be implemented and tested without reading OwnIR JSON dictionaries;
+- every summary records dependencies and precision.
+
+### Phase 2 - #278 as the first feature consumer
+
+Implement lifecycle-root reachability and must-release composition for event
+subscriptions and timers.
+
+Required fixtures:
+
+1. matching `-=` in a reachable teardown path on every exit: clean;
+2. matching `-=` behind a flag: finding with branch witness;
+3. matching `-=` in an uncalled method: finding with unreachable-release
+   evidence;
+4. helper method that always unsubscribes: clean through summary application;
+5. helper that may unsubscribe: finding/advisory according to rule policy;
+6. virtual/external cleanup target: explicit degraded precision;
+7. exceptional exit bypassing cleanup: finding with exceptional path;
+8. runtime-correlated SectorTS scenario: static-only becomes confirmed when the
+   runtime identity matches.
+
+Acceptance:
+
+- class-wide existence of release no longer discharges an obligation;
+- the finding contains a call/branch witness;
+- no regression in current clean anchors;
+- runtime correlation uses stable static identities;
+- no rule-specific traversal duplicates the generic summary engine.
+
+### Phase 3 - obligation summaries
+
+- Extend the common summary envelope with protocol production/discharge.
+- Use P-025/#272 as the intraprocedural foundation.
+- Implement #274 across helper methods and barriers.
+- Keep protocol automata declarative and domain-owned.
+
+Acceptance:
+
+- an obligation produced in method A and discharged in method B is recognized;
+- discharge on only some callee exits remains `may`, not `must`;
+- external model uncertainty is visible.
+
+### Phase 4 - progress summaries
+
+- Implement #275 with local loop CFG and callee `ProgressSummary`.
+- Support consume-or-exit witnesses.
+- Keep numeric reasoning narrow and monotonic.
+
+Acceptance:
+
+- helper calls can prove progress;
+- helper calls can prove no progress;
+- unknown progress remains explicit;
+- recursive helper SCCs converge.
+
+### Phase 5 - selective heap, region, and task expansion
+
+Triggered by real consumers:
+
+- #122 for cross-method exclusivity;
+- #146 for caller-to-callee publisher provenance;
+- field/closure/timer escape findings;
+- #282 after Own.Async facts stabilize.
+
+This phase may introduce field-sensitive heap facts, reverse propagation, or
+selective context sensitivity. It must be driven by a concrete false negative or
+accepted rule, not by a desire to collect fashionable analysis acronyms.
+
+## Testing strategy
+
+Every new interprocedural feature requires four levels of tests.
+
+### Summary unit tests
+
+Input:
+
+- a normalized method body and callee summaries.
+
+Assert:
+
+- exact summary lattice value;
+- precision and unknown reasons;
+- dependency set;
+- deterministic serialization.
+
+### Callsite composition tests
+
+Assert:
+
+- formal-to-actual binding;
+- receiver and field identity;
+- normal versus exceptional effects;
+- alias/fresh/consume propagation;
+- multi-target joins.
+
+### End-to-end OwnIR tests
+
+Assert:
+
+- frontend facts lower correctly;
+- final diagnostics and ordered evidence;
+- no hidden dependence on dictionary order;
+- exact parity artifacts during migration.
+
+### Negative mutation tests
+
+Starting from a clean fixture, mutate one semantic condition:
+
+- move release behind a branch;
+- move release into an uncalled helper;
+- replace `-=` with `+=`;
+- insert an early return;
+- change the released receiver;
+- remove `finally`;
+- make the call target external/unknown;
+- remove loop progress.
+
+The mutation must produce the intended diagnostic or explicit uncertainty.
+Positive tests show the tool does not obstruct code. Negative tests show it
+actually detects the bug.
+
+## Architecture fitness checks
+
+The repository should eventually enforce:
+
+- bridge lowering does not import domain analysis implementations;
+- diagnostics does not depend on solver internals;
+- frontend crates do not depend on analysis;
+- analysis consumes OwnHIR/OwnCFG, not OwnIR JSON maps;
+- call graph and summary dumps are deterministic;
+- unknown targets cannot be serialized as clean exact targets;
+- summary format versions fail loudly on incompatible changes;
+- every diagnostic evidence edge references valid stable IDs;
+- old/new or Python/Rust shadow modes emit zero unexplained summary diffs during
+  migration.
+
+These are architecture checks, not style preferences. Without them the bridge
+will slowly reabsorb the solver because that is always the shortest local path
+and the worst global one.
+
+## Prior art and chosen posture
+
+Relevant models:
+
+- Infer: compositional procedure summaries and SCC/fixpoint reasoning;
+- CodeQL: separation of source syntax from semantic/dataflow representations and
+  explicit library models;
+- Roslyn: authoritative C# semantic model and per-body CFG;
+- IFDS/IDE frameworks: useful later for finite distributive domains such as
+  taint-like obligation propagation;
+- separation logic/bi-abduction: useful prior art for heap ownership, but too
+  large a prerequisite for the first slices;
+- MLIR/LLVM analysis frameworks: useful implementation references, not a suitable
+  source-level C# semantic substrate for Own.NET.
+
+Chosen posture:
+
+1. Roslyn remains the C# semantic authority.
+2. OwnIR remains the versioned frontend seam.
+3. OwnHIR normalizes semantics inside the core.
+4. OwnCFG remains the local dataflow substrate.
+5. Method summaries are the unit of interprocedural composition.
+6. A generic SCC/fixpoint engine hosts domain summaries.
+7. Unknown behavior is explicit.
+8. Evidence is produced with the verdict.
+9. Advanced frameworks are introduced only when a measured analysis need
+   justifies them.
+
+## Open questions
+
+1. Should the internal type be named `OwnHIR`, `MethodIR`, or `SemanticProgram` in
+   code? The semantic boundary matters more than the acronym.
+2. Does the generic interprocedural engine belong inside `own-analysis` or in a
+   new `own-interproc` crate after cutover?
+3. Which summary data is part of a stable debug/parity format versus an internal
+   cache format?
+4. What is the canonical `MethodId` for generics, explicit interface methods,
+   local functions, and lambdas?
+5. Which WPF/DI lifecycle roots are built in, and which are project-declared?
+6. What conservative policy should each rule use for unknown external calls?
+7. How much field sensitivity is required for the first #278 slice?
+8. How are callback registration and delegate target sets represented without
+   pretending reflection is statically resolved?
+9. Which dependency hashes are sufficient for IDE summary invalidation?
+10. Which post-cutover issue owns the structural seam, and which issue owns the
+    first #278 feature consumer?
+
+## Acceptance criteria for this proposal
+
+This proposal is accepted when maintainers agree on the following decisions:
+
+- OwnIR remains the external fact contract, not the permanent solver IR;
+- an internal normalized semantic representation is required;
+- OwnCFG is the MIR-equivalent local analysis representation;
+- interprocedural behavior is expressed through first-class method summaries;
+- summaries are inferred/composed through a generic SCC/fixpoint engine;
+- bridge lowering, analysis, diagnostics, OwnAudit, and 007 have the boundaries
+  described above;
+- no verdict-changing implementation begins before the P-022 parity/cutover
+  discipline permits it;
+- #278 is the preferred first production consumer because it is a confirmed
+  soundness hole that syntax-only release existence cannot solve.
+
+Acceptance of the architecture is not acceptance of every future domain. Each
+new summary axis still requires its own issue, fixtures, precision policy, and
+measured consumer.

From 337376314c5dd3ec28d9baffc5ce5494ef9f779b Mon Sep 17 00:00:00 2001
From: PhysShell <45852143+PhysShell@users.noreply.github.com>
Date: Mon, 20 Jul 2026 06:29:18 +0500
Subject: [PATCH 2/5] docs: index P-036 interprocedural architecture

---
 docs/proposals/README.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/docs/proposals/README.md b/docs/proposals/README.md
index e936b801..d01edbd5 100644
--- a/docs/proposals/README.md
+++ b/docs/proposals/README.md
@@ -55,6 +55,7 @@ proposal is marked `done` with a pointer.
 | [P-033](P-033-probabilistic-data-structures.md) | In-process sketches & bitmap indexes for legacy .NET diagnostics (Top-K, CMS, t-digest, Bloom) | draft |
 | [P-034](P-034-runtime-lifetime-guard.md) | Runtime lifetime guard & disposal quarantine — the "enterprise malloc" idea, correctly scoped for .NET | draft |
 | [P-035](P-035-custom-weak-subscription.md) | Project-declared weak-subscription conventions — recognise/suggest a repo's own weak-subscribe API, not just the BCL WeakEventManager | draft |
+| [P-036](P-036-interprocedural-semantic-architecture.md) | Interprocedural semantic architecture: OwnHIR, OwnCFG, call graph, first-class summaries, and evidence | draft |
 
 > For priorities, milestones, the framing, and the design philosophy across all
 > of these, see the strategy hub: [`docs/ROADMAP.md`](../ROADMAP.md). P-004 … P-016

From 9468a2409bbab61a434c7dfa450af12b867629f4 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sat, 25 Jul 2026 19:54:52 +0000
Subject: [PATCH 3/5] =?UTF-8?q?docs(P-036):=20address=20Codex=20review=20?=
 =?UTF-8?q?=E2=80=94=20SCC-level=20cache=20keys,=20span=20re-projection?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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
---
 ...6-interprocedural-semantic-architecture.md | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/docs/proposals/P-036-interprocedural-semantic-architecture.md b/docs/proposals/P-036-interprocedural-semantic-architecture.md
index f94962d7..8f56264c 100644
--- a/docs/proposals/P-036-interprocedural-semantic-architecture.md
+++ b/docs/proposals/P-036-interprocedural-semantic-architecture.md
@@ -627,6 +627,27 @@ callee summary dependency hashes
 configuration/profile hash
 ```
 
+Two consequences of that key shape must be designed in rather than discovered
+in production:
+
+- **Recursive SCCs cache at SCC granularity.** Inside a recursive component,
+  each member's callee dependency hashes include the other members, so
+  per-method keys cannot be reconstructed before some entry is retrieved. The
+  cacheable unit for a recursive component is the SCC itself: its key derives
+  from the members' local inputs (body hashes, signatures, domain/config
+  versions) plus the dependency hashes of summaries *outside* the component —
+  all reconstructible bottom-up over the acyclic condensation. Per-method
+  entries inside the component stay locally addressable; their cross-member
+  dependency hashes are validated after loading, never used for lookup.
+- **Evidence spans are a projection, not cached truth.** A semantic body hash
+  deliberately survives edits that only move code (inserting lines above an
+  otherwise unchanged method), but source spans captured in cached evidence do
+  not. A cache hit may reuse semantic effects and evidence *structure* (stable
+  IDs and edges); the spans rendered to users are re-projected from the current
+  frontend facts at diagnostic time — the same "formatting is a projection"
+  rule the evidence section imposes. Equivalently: a cached span is valid only
+  together with the source-map version it was minted against.
+
 Changing a leaf method invalidates:
 
 1. its local CFG/summary;

From 1b65d01100380c361e76580df1bdce8793f787e7 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sat, 25 Jul 2026 20:03:51 +0000
Subject: [PATCH 4/5] =?UTF-8?q?docs(P-036):=20address=20arbiter=20review?=
 =?UTF-8?q?=20=E2=80=94=20landed=20reality,=20guarded=20effects,=20enrollm?=
 =?UTF-8?q?ent=20split?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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
---
 ...6-interprocedural-semantic-architecture.md | 165 +++++++++++++++---
 1 file changed, 142 insertions(+), 23 deletions(-)

diff --git a/docs/proposals/P-036-interprocedural-semantic-architecture.md b/docs/proposals/P-036-interprocedural-semantic-architecture.md
index 8f56264c..39b599ce 100644
--- a/docs/proposals/P-036-interprocedural-semantic-architecture.md
+++ b/docs/proposals/P-036-interprocedural-semantic-architecture.md
@@ -10,8 +10,10 @@ Related work:
 - [`spec/Inference.md`](../../spec/Inference.md)
 - [`docs/notes/interprocedural-roadmap.md`](../notes/interprocedural-roadmap.md)
 - [`docs/notes/interprocedural-tz.md`](../notes/interprocedural-tz.md)
-- #258 / #259 / #260: bridge contract, Rust bridge, dual-engine parity
-- #278: a release that exists syntactically but is not reachable
+- #258 (closed) / #259 / #260: bridge contract, Rust bridge, dual-engine parity
+- #278 (closed by #293, extended by #302): a release that exists syntactically
+  but is not reachable — the historical motivating incident; #304 tracks the
+  post-cutover summary-backed generalization
 - #272 / #274: obligation protocols and protocol/effect summaries
 - #275: consume-or-exit loop progress
 - #122 / #146: exclusivity and publisher provenance
@@ -56,14 +58,16 @@ Today, `ownlang/ownir.py` is not merely a JSON loader. It validates facts,
 normalizes identities, lowers flow operations, mints handles and RIDs, resolves
 calls, infers method ownership summaries, applies branch-local behavior,
 prepares DI/effect inputs, drives analyses, and maps results back to source
-locations. #258 correctly treats this as verdict-determining behavior that must
-be specified before #259 ports it.
+locations. #258 (now closed) correctly treated this as verdict-determining
+behavior and specified it before #259 ported it.
 
 That concentration was acceptable for the proof of concept. It is not an
 acceptable permanent substrate for the next classes of work:
 
-- #278 needs release reachability through lifecycle call chains, not a class-wide
-  search for a matching `-=` or `Stop()`;
+- the #278 class needs release reachability through lifecycle call chains, not a
+  class-wide search for a matching `-=` or `Stop()` — the landed #293/#302
+  extractor predicates are the current bounded implementation, and #304 tracks
+  their summary-backed generalization;
 - obligation protocols need effects to be produced in one method and discharged
   in another;
 - loop progress needs callees to summarize whether they advance a controlling
@@ -93,7 +97,8 @@ This proposal defines:
 7. domain boundaries for ownership, protocols, progress, regions, and tasks;
 8. evidence and uncertainty requirements;
 9. an incremental migration sequence compatible with P-022 parity;
-10. acceptance criteria for the first real consumer, #278.
+10. acceptance criteria for the first real consumer, #304 (the #278 class,
+    generalizing the landed #293/#302 predicates).
 
 ## Non-goals
 
@@ -181,19 +186,30 @@ JSON dictionaries.
 
 ### OwnCFG
 
-The existing **OwnCFG** is the MIR-equivalent layer. It should represent each
-method as basic blocks containing OwnHIR operations and explicit terminators:
+The existing **OwnCFG** is the local-analysis substrate and the *intended*
+MIR-equivalent layer. Today it lowers the OwnLang AST into basic blocks with
+plain successor edges — calls and returns are ordinary instructions, and the
+crate still re-exports the AST for analyses the CFG does not model — so
+"MIR-equivalent" is the target contract, not the current state. To serve this
+architecture it must be extended to carry normalized OwnHIR operations and
+explicit typed terminators:
 
 ```text
 Goto
 Branch
 Switch
-Call
+Invoke   (call terminator: normal + exceptional successors)
 Return
 Throw
 AwaitSuspend
 ```
 
+One model, stated once: a plain call whose exceptional or suspension flow is
+not modeled stays an ordinary OwnHIR `Call` operation *inside* a block;
+`Invoke` is the terminator form a domain opts into when the
+exceptional/suspension successors must be distinguished. `Call` never appears
+as both an instruction and a terminator in the same method lowering.
+
 Normal, exceptional, and suspension edges must be distinguishable when a domain
 cares about them.
 
@@ -371,6 +387,12 @@ MethodSummary {
 the result. This makes invalidation, explanation, and differential replay
 possible.
 
+`input_contract` is not decorative: it carries the guarded-effect predicates
+(see the MVP policy under the ownership summary) under which conditional
+effects apply, plus the argument facts a callsite is allowed to substitute
+(statically-known constants). An empty contract means the summary's effects
+are unconditional.
+
 ### Ownership summary
 
 The current MOS remains authoritative for existing behavior. Its future internal
@@ -390,6 +412,39 @@ MayLeaveLive
 The critical distinction is **may** versus **must**. A release on one branch is
 not a release on all branches. Unknown is not clean.
 
+One context-insensitive summary per method is not enough for the flagship
+lifecycle case, and this proposal says so now rather than discovering it in
+Phase 2. The heap-proven SectorTS shape is:
+
+```csharp
+void Teardown(bool skip)
+{
+    if (!skip)
+        publisher.Event -= handler;   // the release
+}
+
+Teardown(true);                        // the callsite that never releases
+```
+
+An unconditional summary can say at most `MayRelease` — true and useless.
+Binding `parameter[0] -> true` decides the case only if the summary preserved
+the guard. The MVP policy is therefore:
+
+```text
+MVP guarded effects:
+  summaries preserve guarded effects over simple boolean/null parameter
+    predicates (a release/consume/protocol effect may carry
+    `when <param> == <const>` / `when <param> is null | non-null`);
+  callsite application substitutes statically-known constant arguments and
+    resolves the guard before joining;
+  any predicate outside that vocabulary degrades the effect to May/Unknown —
+    never to Must, and never to silence.
+```
+
+A full symbolic executor is explicitly out of scope. But without at least this
+much, the summary layer would be weaker than the landed #293/#302 extractor
+predicates on the exact case that motivated it.
+
 ### Obligation summary
 
 Obligation protocols need summaries that can create, transform, discharge, or
@@ -547,8 +602,12 @@ it may not pretend the call was proven harmless.
 
 ## Lifecycle roots and reachability
 
-#278 shows that intraclass syntax matching is not lifecycle reasoning. A
-reachable-release analysis needs explicit roots and entry contracts.
+#278 showed that intraclass syntax matching is not lifecycle reasoning (a
+heap-proven leak hid behind a flag-guarded `-=` in a method callers skip). The
+landed #293/#302 extractor predicates close that reported class with bounded
+teardown-context and guard reasoning; they are the floor this section
+generalizes, not the ceiling. A reachable-release analysis needs explicit
+roots and entry contracts.
 
 Examples of roots:
 
@@ -572,6 +631,25 @@ Which path proves the missing release?
 A release in a dead method, an unregistered callback, or a conditional branch
 must not discharge a must-release obligation globally.
 
+Two different theorems hide here, and the analysis must keep them apart:
+
+```text
+LifecycleEffect:
+  IF a lifecycle root runs, release happens on all its required exits
+  (proved by the call graph + summaries under that root)
+
+LifecycleEnrollment:
+  THIS instance actually reaches that root
+  (proved by `using`, DI scope membership, a wired framework callback,
+   an owner whose own teardown calls Dispose, a registered handler,
+   or a framework model that guarantees the teardown)
+```
+
+Proving a perfect `Dispose()` that nothing ever calls proves nothing. A
+must-release obligation is discharged only by LifecycleEffect *and*
+LifecycleEnrollment together; effect without enrollment yields a degraded or
+conditional verdict — never clean.
+
 ## Evidence and explanations
 
 Every interprocedural conclusion should be explainable without reading solver
@@ -608,7 +686,13 @@ Unsubscribe at ViewModel.cs:121 is not reached on that path
 ```
 
 The evidence graph should retain stable method/callsite/resource IDs and source
-spans. Diagnostic formatting is a projection. OwnAudit may correlate those IDs
+spans. Two representations, one truth: the full derivation exists once as a
+**proof DAG** keyed by those stable IDs; summaries carry only compact
+provenance/dependency references into it, and the diagnostic layer selects one
+deterministic **displayed witness** path per finding. The derivation graph is
+never duplicated into every summary, and the witness is a projection of the
+DAG, not a second derivation. Diagnostic formatting is a projection. OwnAudit
+may correlate those IDs
 with runtime resource identities and classify the result as static-only,
 runtime-only, or confirmed. OwnAudit does not recompute the static summary.
 
@@ -798,12 +882,27 @@ summaries.
 
 ## Migration plan
 
+### Who owns the bridge boundary, when
+
+P-022/#259 deliberately place lowering, MOS inference, and callsite
+application inside `own-bridge`, mirroring `ownir.py` for byte-parity. This
+proposal calls that concentration migration debt. Both are right — at
+different times — and a reader acting on only one of the two documents will
+re-architect the wrong period:
+
+| period | authoritative boundary |
+|---|---|
+| until Rust parity + cutover (#262) | #258/#259: MOS and lowering live in `own-bridge`, byte-parity with `ownir.py`; no seam moves |
+| after cutover | a dedicated extraction slice per this proposal: `own-bridge` validates/lowers only; the generic interproc engine moves out (open question 2) |
+| invariant across both | the OwnIR wire schema, verdicts, and parity artifacts do not change as part of the seam move |
+
 ### Phase 0 - documentation and parity freeze
 
 Timing: before #262.
 
 - Land this proposal as architecture direction only.
-- Finish #258 and merge the normative current bridge contract.
+- #258 is closed: `spec/Bridge.md` and its behavior matrix are the merged
+  normative bridge contract — keep them current as the parity baseline.
 - Preserve the verdict-changing inference freeze.
 - Add no new summary axis in only one engine.
 - Treat current summary dumps and diagnostics as parity artifacts.
@@ -832,11 +931,20 @@ Acceptance:
 - MOS can be implemented and tested without reading OwnIR JSON dictionaries;
 - every summary records dependencies and precision.
 
-### Phase 2 - #278 as the first feature consumer
+### Phase 2 - summary-backed lifecycle release reachability (#304)
 
 Implement lifecycle-root reachability and must-release composition for event
 subscriptions and timers.
 
+The historical motivator, #278, is **closed**: PR #293 landed the bounded
+extractor predicates (teardown context, parameter guards, symbol-based helper
+reachability), and PR #302 extended the same invariant to WPF002 `Stop()`.
+The landed #293/#302 extractor predicates are the current bounded
+implementation and the regression floor. The first post-cutover consumer of
+P-036 — tracked as #304 — will replace or generalize them with CFG-backed,
+summary-composed lifecycle reasoning; #278 stays the motivating incident, not
+a reusable implementation issue.
+
 Required fixtures:
 
 1. matching `-=` in a reachable teardown path on every exit: clean;
@@ -850,11 +958,18 @@ Required fixtures:
 8. runtime-correlated SectorTS scenario: static-only becomes confirmed when the
    runtime identity matches.
 
+Fixtures 1-3 are already caught (or deliberately kept silent) by the landed
+#293/#302 predicates and enter this phase as regression anchors; fixtures 4-8
+are the genuinely new summary-backed capability.
+
 Acceptance:
 
-- class-wide existence of release no longer discharges an obligation;
+- class-wide existence of release no longer discharges an obligation (landed
+  behavior — must not regress);
 - the finding contains a call/branch witness;
-- no regression in current clean anchors;
+- no regression in current clean anchors or in the #293/#302 caught set;
+- helper release is proven through summary application, not extractor-side
+  symbol fixpoints;
 - runtime correlation uses stable static identities;
 - no rule-specific traversal duplicates the generic summary engine.
 
@@ -1009,12 +1124,13 @@ Chosen posture:
    local functions, and lambdas?
 5. Which WPF/DI lifecycle roots are built in, and which are project-declared?
 6. What conservative policy should each rule use for unknown external calls?
-7. How much field sensitivity is required for the first #278 slice?
+7. How much field sensitivity is required for the first #304 slice?
 8. How are callback registration and delegate target sets represented without
    pretending reflection is statically resolved?
 9. Which dependency hashes are sufficient for IDE summary invalidation?
-10. Which post-cutover issue owns the structural seam, and which issue owns the
-    first #278 feature consumer?
+10. Which post-cutover issue owns the structural seam? (The first feature
+    consumer — summary-backed lifecycle release reachability — is tracked as
+    #304.)
 
 ## Acceptance criteria for this proposal
 
@@ -1022,15 +1138,18 @@ This proposal is accepted when maintainers agree on the following decisions:
 
 - OwnIR remains the external fact contract, not the permanent solver IR;
 - an internal normalized semantic representation is required;
-- OwnCFG is the MIR-equivalent local analysis representation;
+- OwnCFG is the local-analysis substrate to be extended into the
+  MIR-equivalent representation (OwnHIR operations + typed terminators);
 - interprocedural behavior is expressed through first-class method summaries;
 - summaries are inferred/composed through a generic SCC/fixpoint engine;
 - bridge lowering, analysis, diagnostics, OwnAudit, and 007 have the boundaries
   described above;
 - no verdict-changing implementation begins before the P-022 parity/cutover
   discipline permits it;
-- #278 is the preferred first production consumer because it is a confirmed
-  soundness hole that syntax-only release existence cannot solve.
+- summary-backed lifecycle release reachability (#304) is the preferred first
+  production consumer: it generalizes the landed #293/#302 predicates on the
+  confirmed soundness class (#278) that syntax-only release existence could
+  not solve.
 
 Acceptance of the architecture is not acceptance of every future domain. Each
 new summary axis still requires its own issue, fixtures, precision policy, and

From 872cc31a73e44a240606959af17c68d8ff4309e6 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sat, 25 Jul 2026 20:13:40 +0000
Subject: [PATCH 5/5] =?UTF-8?q?docs(P-036):=20P2=20=E2=80=94=20Call/Invoke?=
 =?UTF-8?q?=20lowering=20is=20profile-driven,=20not=20domain=20opt-in?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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
---
 ...6-interprocedural-semantic-architecture.md | 22 ++++++++++++-------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/docs/proposals/P-036-interprocedural-semantic-architecture.md b/docs/proposals/P-036-interprocedural-semantic-architecture.md
index 39b599ce..c566ffbd 100644
--- a/docs/proposals/P-036-interprocedural-semantic-architecture.md
+++ b/docs/proposals/P-036-interprocedural-semantic-architecture.md
@@ -25,8 +25,9 @@ Own.NET should treat interprocedural analysis as a first-class semantic layer, n
 as additional logic inside AST visitors or the OwnIR bridge. The external
 versioned **OwnIR** JSON contract remains the frontend seam. It lowers into an
 internal, typed, syntax-independent **OwnHIR** method representation. The
-existing **OwnCFG** is the MIR-equivalent control-flow representation and should
-remain the execution substrate for local dataflow. A derived call graph and
+existing **OwnCFG** is the local-analysis substrate, intended to become the
+MIR-equivalent control-flow representation, and should remain the execution
+substrate for local dataflow. A derived call graph and
 first-class **MethodSummary** artifacts carry effects across method boundaries.
 A generic SCC/fixpoint summary engine composes domain-specific summaries for
 ownership, obligations, progress, regions, and tasks. Diagnostics consume
@@ -59,7 +60,7 @@ normalizes identities, lowers flow operations, mints handles and RIDs, resolves
 calls, infers method ownership summaries, applies branch-local behavior,
 prepares DI/effect inputs, drives analyses, and maps results back to source
 locations. #258 (now closed) correctly treated this as verdict-determining
-behavior and specified it before #259 ported it.
+behavior and specified it so that #259 can port it under a frozen contract.
 
 That concentration was acceptable for the proof of concept. It is not an
 acceptable permanent substrate for the next classes of work:
@@ -204,11 +205,16 @@ Throw
 AwaitSuspend
 ```
 
-One model, stated once: a plain call whose exceptional or suspension flow is
-not modeled stays an ordinary OwnHIR `Call` operation *inside* a block;
-`Invoke` is the terminator form a domain opts into when the
-exceptional/suspension successors must be distinguished. `Call` never appears
-as both an instruction and a terminator in the same method lowering.
+One model, stated once: lowering selects `Call` or `Invoke` deterministically
+from the configured CFG profile and the available frontend facts — never from
+the analysis domain. When exceptional or suspension flow is represented, the
+call is lowered as `Invoke` for **all** domains; a domain that does not care
+about those successors may ignore them, but it does not request a different
+lowering for the same method and profile. A plain call whose exceptional flow
+the profile does not represent stays an ordinary OwnHIR `Call` operation
+inside a block. One method, one profile, one CFG shape — shared summaries,
+serialization, and cache keys all assume it — and `Call` never appears as both
+an instruction and a terminator in the same method lowering.
 
 Normal, exceptional, and suspension edges must be distinguishable when a domain
 cares about them.