D5.1c: interprocedural exclusivity (borrow_mut) axis for MOS wrapper summaries

[PhysShell]

Tracking issue for the deferral already recorded as D5.1c — transitive borrow-kind propagation (deferred) in docs/notes/d5-ownership-transfer.md §7. Filed so the deferral lives as a live tracker, not only as a bullet in a design note.

Decision (standing): decline now, defer the fix

When a first-party wrapper method only forwards a parameter to a $borrow_mut sink, its MOS ParamSummary does not carry exclusivity — the wrapper param stays plain. This is the precision-safe choice: a tolerated false-negative, never a false shared-borrow assertion.

Three options were weighed:

1. Decline (leave as-is) — precision-first, no core change. ✅ current behaviour.
2. Propagate exclusivity through the solver — correct but a new analysis axis (heavy lift).
3. Defer + track — keep (1), record the fix. ✅ chosen.

Why this is the right call (sharper than "heavy lift")

• It's a new orthogonal axis, not a precision drop on an existing one. ownership.py's Transfer lattice (no/must/may/unknown) models only disposable ownership transfer. There is no shared-vs-exclusive dimension anywhere in ParamSkeleton/ParamSummary. Adding borrow_mut propagation = opening a second axis (none | shared | mut), not extending a near-complete one.
• Exclusivity is not lost — only its interprocedural propagation is. The core checker already distinguishes shared vs mutable borrows intraprocedurally (cfg.py → Effect.BORROW vs BORROW_MUT; analysis.py → _check_shared_borrowable vs _check_mut_borrowable → OWN006/011/012/013), and a direct $borrow_mut call keeps full exclusivity through lower_call. Only the transitive claim through a wrapper is declined.
• No reader today ⇒ no observable cost. The exclusivity axis has no interprocedural consumer: OWN006/011/012/013-class conflicts are checked intraprocedurally and at direct $borrow_mut calls, not across the call boundary via summaries. A summary axis with no reader can't produce a false-negative on output that doesn't exist.
• Cheap to reverse. The forward edges are already preserved in the skeleton (PathAction(kind="forward", callee, arg)), so the future work is additive — add the leaf borrow-kind to the extractor + a join over existing forward edges + a field on ParamSummary — not a solver rebuild.

Revisit trigger

Land the exclusivity axis alongside the first interprocedural exclusivity consumer — i.e. when an OWN006/011/012/013-class conflict is checked across the call boundary (today it isn't). Until then the decline costs no soundness and stays cheap to reverse.

Deliverables (when reactivated)

• Orthogonal borrow-kind axis (none | shared | mut) on the MOS summary; do not normalize $borrow_mut away before inference.
• Direct-call behaviour unchanged.
• Brutally-conservative inference: infer borrow_mut only on a single, unconditional, straight-line forward to $borrow_mut; any mix / fan-out / conditional / loop → degrade to plain/unknown and stay silent.
• Tests: $borrow_mut wrapper propagation, plus mixed-path regressions proving ambiguous flows degrade to silence (not a shared/exclusive borrow assertion).

Prior art

Rust &/&mut, RustBelt exclusivity, Oxide's shrd|uniq, Polonius per-loan invalidation — exclusivity is a distinct semantic axis, not coarser metadata. (cf. Checker Framework @MustCallAlias for the wrapper "one obligation, two handles" shape.)

Origin: Codex P2 / CodeRabbit Major on #113.