Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses

[PhysShell]

Описание

Problem. When a statement-level first-party call receives a tracked resource, the Roslyn frontend decides the callee's ownership effect itself. It then lowers the call to one of three guesses, so the call itself never reaches the language-neutral core:

Frontend's verdict on the callee	What the core receives
definite consumer (ConsumesParam → DisposesLocal / IsDefiniteInBody)	a release of the argument at the call site
anything else, and the argument is a tracked parameter	a use → INF-S4 borrow → summary no
anything else, and the argument is a tracked local	an escape: the local is untracked; if nothing else in the method is tracked, the caller's functions[] record is not emitted at all

Code at fb06adc:

• handoff in EmitFlowExpr: L4159–L4167
• argument-escape rule: L7057–L7122
• ConsumeReleaseArgs
• ConsumesParam
• DisposesLocal
• IsDefiniteInBody

Today only one shape keeps an OwnIR call: the factory initializer var r = FirstPartyFactory(args) (P-005 D5.2, L3651–L3684).

• Before ConsumesParam flattens guarded release into unconditional handoff, causing false OWN009 and false must summaries #380, a guarded first-party consume collapsed to call → fabricated release. That produced real false findings and false must summaries.
• After ConsumesParam flattens guarded release into unconditional handoff, causing false OWN009 and false must summaries #380 (fix: only a definite release makes a call-site handoff (INF-S2, #380) #381, merged as fb06adc), the fabricated must is gone. A partial or guarded call now degrades instead:
  • tracked local → escape, no caller record;
  • forwarded parameter → use → summary no.

So the lowering still destroys two facts: that an interprocedural call happened, and which callee parameter received which resource. This causes two architectural problems.

1. The core cannot derive the correct partial semantics. The Inference rules that decide this case are all defined over call ops and the forward edges built from them:

   • INF-S2: partial release ⇒ may;
   • INF-S3: a straight-line forward resolves to the callee's transfer; a conditional forward gives may/no;
   • INF-A1: may → plain;
   • INF-A5: optimistic untrack plus advisory OWN051.

   A call that the frontend already lowered to release/use/escape can reach none of them.

2. Every frontend would have to reinvent interprocedural inference. ConsumesParam, DisposesLocal and IsDefiniteInBody re-implement, over Roslyn syntax, rules the core already owns: INF-S2's _definite_release and INF-S3's forward derivation in _build_skeletons. Another frontend (OwnTS exists as the cross-language seam proof, P-020) would have to port them again, and every port can drift from the core. ConsumesParam flattens guarded release into unconditional handoff, causing false OWN009 and false must summaries #380 was exactly that kind of drift. This defeats the language-neutral boundary of the core.

Concrete witnesses

• ConsumesParam flattens guarded release into unconditional handoff, causing false OWN009 and false must summaries #380 / fix: only a definite release makes a call-site handoff (INF-S2, #380) #381. The fix restores the precision floor by refusing to fabricate an unconditional consume. By design it does not produce may.

• The pinned limitation (410431a).

  ForwardDynamic(Stream forwarded, bool dispose)
      -> MaybeClose(forwarded, dispose)        // MaybeClose: if (dispose) s.Dispose();
  

  • Current summary after ConsumesParam flattens guarded release into unconditional handoff, causing false OWN009 and false must summaries #380: forwarded = no.
  • It is pinned as a KNOWN LIMITATION: tests/test_guarded_consume.py L159–L172, fixture GuardedConsumeSample.cs L114–L122.
  • The correct path-insensitive transfer is may: an INF-S3 straight-line forward to a callee whose own INF-S2 summary is may.

• Real code (dotnet/runtime@49e04fa0; evidence in Own.NET-paperwork 3a4c1ae):

  • C12/C13, SymmetricCngTestHelpers.VerifyPersistedKey(..., disposeKey: false). The false OWN009 at :36 and :355 came from the pre-collapse into release. fix: only a definite release makes a call-site handoff (INF-S2, #380) #381 removed them, but the local is now an escape and the caller's record is no longer emitted.
  • C16, Mono.Options GetArguments(TextReader). The false must became no after fix: only a definite release makes a call-site handoff (INF-S2, #380) #381. no is right for this call site (close: false), so the immediate false positive is fixed. The representation still cannot express partial forwarding for a wrapper that forwards its guard.
  • Recall side. Before ConsumesParam flattens guarded release into unconditional handoff, causing false OWN009 and false must summaries #380, a guard-true caller that misused the resource afterwards was caught only by accident: the fabricated release happened to be true for it. It is now silent. The spec path for this case is INF-A5: plain plus advisory OWN051 at the call. That path cannot fire, because there is no call.

• Exploratory probe (hand-edited facts, not an implementation). Starting from facts extracted from GuardedConsumeSample.cs at fb06adc, only ForwardDynamic's body use forwarded was replaced with {"op":"call","callee":"GuardedConsumeSample.MaybeClose","sig":"System.IO.Stream,System.Boolean","args":["forwarded"]}.

  • python -m ownlang summaries: forwarded moves from no to may. MaybeClose.s stays may and BorrowingWrapper.borrowed stays no.
  • A synthetic caller hands a tracked local x to ForwardDynamic through a call op. It gets [OWN051] cannot verify whether 'GuardedConsumeSample.ForwardDynamic' takes ownership of 'x' (inferred contract: may) from both own-cli ownir and python -m ownlang ownir, with byte-identical output.

  So for this case the core-side semantics seem to exist already; what is missing is the call. The probe is evidence for the investigation, not a design.

None of these are P-037 failures. They follow from where the frontend/core boundary sits today.

Desired architectural property

A first-party call involving a tracked resource should survive frontend lowering as a canonical call relationship available to the language-neutral core, instead of being pre-decided into release/use/escape.

Minimum information to investigate:

• resolved callee identity or a stable target key (today: callee plus the optional per-overload sig, OwnIR §5.1)
• call-site identity and location (today: line, optional column)
• binding of each actual argument to its formal parameter
• identity of the tracked resource passed as the actual argument
• receiver binding, where relevant
• binding of named and reordered arguments
• unresolved or degraded target state (virtual/interface dispatch, delegates, unresolved symbols)
• enough information to tell a direct call apart from a frontend-inferred release/use/escape

Carrier first, schema second. Before inventing any schema, find out whether this belongs in one of these:

• The existing OwnIR call flow op (callee, args, optional result, optional sig). Both engines already read it:

  • for MOS forward edges: Python _build_skeletons and Rust own-bridge build_skeletons;
  • for call-site application: INF-A1, INF-A2, INF-A5.

  What it does not carry explicitly today:

  • args is a positional list, and binding is implied by position in it;
  • the D5.2 emitter keeps only positional tracked identifiers;
  • there is no receiver slot and no unresolved/degraded state.

• The MOS input (the skeletons derived from functions[].body). It takes its forward edges from that same call op, so this may be one decision, not two.

• Another carrier that already exists.

By OwnIR §2, adding optional fields needs no OWNIR_VERSION bump. Adding a flow op or changing what one means does.

Settle one transition constraint up front: a canonical call must replace the frontend's guess for that argument, not sit beside it. A call to a definite consumer plus the legacy release would charge the resource twice (OWN003).

Non-goals

This issue is:

• not a P-037 implementation;
• not a reopening of Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304;
• not arbitrary predicate solving (no guard cells, no guard evaluation);
• not general alias analysis;
• not whole-program symbolic execution;
• not a Rust-style borrow checker;
• not a verdict-policy change by itself. INF-A1/INF-A5 lowering stays as specified, and any verdict movement has to be explained by the representation change.

Acceptance direction

A future implementation should, at minimum, be able to show:

1. ForwardDynamic keeps a canonical first-party call visible to the core. The KNOWN-LIMITATION pin in tests/test_guarded_consume.py is built to fail loudly when that happens; it gets re-recorded deliberately, never silently.
2. The wrapper no longer has to become release or use just to encode the callee's ownership behaviour.
3. Existing definite-consumer behaviour stays intact: the handoff anchors keep their OWN002. These are GuardedConsumeSample DefiniteHandoffThenUse and FinallyHandoffThenUse, and examples/gallery/cs/07_use_after_handoff.
4. Python/Rust parity stays intact: ownir parity replay, shadow compare, MOS parity.
5. Another frontend can use the representation without Roslyn-specific semantics.
6. Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304 reopen condition 1 may be re-evaluated only after this architecture lands independently. This issue neither satisfies nor reopens it.

Relation to #304

The freeze ruling on #304 lists this as reopen condition 1:

Canonical calls: independent production work makes the call representation canonical. For example, the legacy body stops folding first-party forwards into release/use, so the honest call becomes the MOS's natural source.

That condition is an example of an external structural change that could later lower P-037's integration cost. This issue is independent architecture work, motivated by the frontend/core boundary described above. If it lands and really makes calls canonical, #304 can then be re-evaluated under its frozen governance. Nothing here claims in advance that the condition will be satisfied.

Two notes to keep the boundary clean:

• The A2.1 guarded_facts sidecar (OwnIR §5.2) also records call-shaped data. It is semantically inert by design and governed by Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304, and this issue does not propose reading or promoting it.
• P-037's evidence instruments (corpus/p037-shapes, scripts/p037_controls.py) will move once calls become canonical. That movement gets recorded as an explicit baseline transition, as fix: only a definite release makes a call-site handoff (INF-S2, #380) #381 did, not re-recorded silently.