P2: Extend MOS/effect summaries to protocol and barrier effects

[PhysShell]

Type

Enhancement / interprocedural analysis design.

Priority

P2 / Medium-High.

Tags

mos, method-summary, interprocedural, effects, protocols, barriers, ownir, future-slice

Context

D5 already frames ownership transfer as a method-summary problem, not a borrow-checker-core problem. Obligation protocols need the same move once the intraprocedural MVP exists.

Example that cannot be solved well with local-only analysis:

IsLoaded = false;
RebuildDocument(); // may call OnPropertyChanged(nameof(Document)) internally
IsLoaded = true;

The caller must know that RebuildDocument() may produce a notify(Document) barrier while DocumentLoading is open.

Proposed model

Add protocol/effect summaries alongside ownership MOS.

Sketch:

Method Protocol Summary:
  opens:
    DocumentLoading: must/may/no/unknown
  closes:
    DocumentLoading: must/may/no/unknown
  effects:
    notify(Document): may/no
    notify(Progress): may/no
    mutate(Document): may/no
    alloc: may/no
    throw: may/no

The checker should use summaries at call sites instead of recursively re-descending into callee bodies.

Scope

This should come after the local Obligation Protocol MVP.

Initial summary effects to consider:

• notify(PropertyName) from OnPropertyChanged / RaisePropertyChanged / PropertyChanged?.Invoke;
• mayThrow;
• obligation open/close propagation;
• optional future effect: alloc for GC-free/hot-path work.

Acceptance criteria

• A caller with an open obligation reports a violation when it calls a summarized method that may emit a forbidden barrier.
• Clean calls to summarized methods with only allowed effects stay silent.
• Unknown summaries degrade according to an explicit policy:
  • default should be precision-first / advisory, not CI-breaking;
  • strict mode can be added later.
• Summary computation reuses the D5/SCC/fixpoint direction where possible.
• Findings still include useful path/evidence:
  • open site in caller;
  • call site;
  • summarized callee effect.

Non-goals

• Do not make this part of the first obligation MVP.
• Do not build a context-sensitive interprocedural engine yet.
• Do not infer arbitrary behavior equivalence.

Why this matters

Local obligations catch the first killer demo. MOS/effect summaries are what make the same idea scale beyond one 1000-line method without turning the analyzer into a recursive spelunking expedition through the legacy swamp.