docs: interprocedural roadmap — staged path from D5 today to 'proper interprocedural'

docs/notes/d5-ownership-transfer.md

@@ -470,6 +470,9 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa
 
 ## 10. Open questions remaining
 
+> Sequencing for closing these — together with the deferred §7 slices, #122 and
+> #146 — lives in [interprocedural-roadmap.md](interprocedural-roadmap.md).
+
 1. ~~`aliasOf` in the core: shared resource id vs a synthetic discharge edge.~~
    **Resolved → §11 (the obligation-identity model): Variant B, a shared RID / alias-set.**
 2. ~~Signature-key canonicalisation across overloads / generics / partial classes (the

ownlang/__main__.py

@@ -9,6 +9,8 @@
     python -m ownlang report file.own      # buffer storage report + .ownreport.json
     python -m ownlang ownir  facts.json    # check OwnIR facts extracted from C# (P-001)
     python -m ownlang ownir  facts.json --format github|msbuild|human|sarif
+    python -m ownlang summaries facts.json # dump solved method-ownership summaries
+                                           # (MOS) + extern log — deterministic JSON
     python -m ownlang explain OWN001 [DI002 ...]     # explain diagnostic code(s): what/why/fix
     python -m ownlang explain --json findings.json   # explain every code in a findings/SARIF file
 
@@ -26,9 +28,10 @@
 `--severity` (ownir only) picks how the host shows a finding — `error` (default,
 fails a build / red check) or `warning` (advisory). It is a presentation choice;
 the finding is still the core's verdict.
-`--verbosity` (ownir only) is `quiet` (errors only — hide the advisory OWN050
-"leakage analysis skipped" notes, P-014 Tier A), `normal` (default), or `verbose`
-(also print a per-code breakdown).
+`--verbosity` (ownir only) is `quiet` (errors only — hide the advisory notes:
+OWN050 "leakage analysis skipped", OWN051 "ownership transfer unverified",
+OWN052 "summaries skipped"), `normal` (default), or `verbose` (also print a
+per-code breakdown).
 
 Exit code is non-zero if any error-level diagnostic was produced.
 """
@@ -300,6 +303,28 @@ def cmd_explain(codes: list[str], json_path: str | None) -> int:
     return 0
 
 
+def cmd_summaries(path: str) -> int:
+    """Dump the solved Method Ownership Summaries (MOS) + the extern-boundary
+    log for an OwnIR facts file as one deterministic JSON document on stdout
+    (roadmap stage 1). The debugging answer to "why did this call stay plain /
+    consume / fresh?" — and the frozen parity surface the Rust port of the
+    inference layer is diffed against, so its output contract is byte-stable:
+    sorted method keys, sorted extern log, fixed field order. Exit code is 0
+    even when the solve degraded (the `degraded` field carries the reason —
+    this surface reports state, it does not judge); 2 only for unreadable
+    facts, like `ownir`."""
+    import json
+
+    from .ownir import OwnIRError, dump_summaries, load
+    try:
+        doc = dump_summaries(load(path))
+    except OwnIRError as e:
+        print(f"{path}: error: {e}", file=sys.stderr)
+        return 2
+    print(json.dumps(doc, indent=2, sort_keys=True))
+    return 0
+
+
 def cmd_ownir(path: str, fmt: str = "human", severity: str = "error",
               verbosity: str = "normal") -> int:
     """Check OwnIR facts (extracted from real C# by the Roslyn frontend) through
@@ -351,8 +376,9 @@ def cmd_ownir(path: str, fmt: str = "human", severity: str = "error",
     n = len(leaks)
     summary = f"\n{n} finding{'s' if n != 1 else ''}"
     if notes:
-        # the advisory band is no longer only OWN050 (OBL005 rides it too) —
-        # name the codes actually present instead of hardcoding one.
+        # the advisory band is no longer only OWN050 (OBL005 and the OWN051/OWN052
+        # interprocedural notes ride it too) — name the codes actually present
+        # instead of hardcoding one.
         note_codes = "/".join(sorted({x.code for x in notes}))
         summary += (f" ({len(notes)} advisory hidden)" if verbosity == "quiet"
                     else f", {len(notes)} advisory ({note_codes})")
@@ -372,7 +398,8 @@ def cmd_ownir(path: str, fmt: str = "human", severity: str = "error",
 
 
 def main(argv: list[str]) -> int:
-    if not argv or argv[0] not in {"check", "emit", "cfg", "report", "ownir", "explain"}:
+    if not argv or argv[0] not in {"check", "emit", "cfg", "report", "ownir",
+                                   "summaries", "explain"}:
         print(__doc__)
         return 2
     cmd = argv[0]
@@ -475,7 +502,8 @@ def main(argv: list[str]) -> int:
         return cmd_check(path, fmt, severity)
     if cmd == "cfg":
         return cmd_cfg(path, fmt)
-    return {"emit": cmd_emit, "report": cmd_report}[cmd](path)
+    return {"emit": cmd_emit, "report": cmd_report,
+            "summaries": cmd_summaries}[cmd](path)
 
 
 if __name__ == "__main__":

ownlang/diagnostics.py

@@ -83,6 +83,8 @@ class Severity(Enum):
     "OWN041": "call argument mismatch",
     # ---- C# front-end resolution coverage (P-014; advisory) ----
     "OWN050": "declaring type unresolved -- leakage analysis skipped",
+    "OWN051": "ownership transfer unverified -- local not checked past this call",
+    "OWN052": "interprocedural summary inference failed -- method summaries skipped",
     # ---- DI container lifetimes (P-006; emitted by the OwnIR bridge) ----
     "DI001": "captive dependency: a shorter-lived service is captured by a longer-lived one",
     "DI002": "singleton captures a scoped service (captive dependency)",
@@ -160,6 +162,26 @@ class Severity(Enum):
         "Fix (to check it): give the extractor the type's assembly via `--ref-dir <bin>` so the "
         "SemanticModel can bind the event."
     ),
+    "OWN051": (
+        "Advisory, not a leak verdict: an owned local was passed to a method whose ownership "
+        "contract for that argument could not be verified — the inferred transfer is `may` "
+        "(the callee disposes it on some paths only) or `unknown` (the evidence crosses an "
+        "unanalyzable boundary). Per the optimistic default (own-only 0) the checker assumes "
+        "ownership left the caller and stops tracking the local at that call: a missing "
+        "dispose after it is NOT reported, and neither is a defensive one. This note is the "
+        "honest record of that gap. It never fails a build.\n"
+        "Fix (to make it checkable): make the callee's contract definite — dispose the "
+        "parameter on every path (or none), or annotate the intended contract when "
+        "annotations land (P-005 Tier C)."
+    ),
+    "OWN052": (
+        "Advisory, not a leak verdict: computing the method ownership summaries (the "
+        "interprocedural pass that resolves cross-method ownership transfer) failed, so the "
+        "bridge degraded to intraprocedural checking only for this run — every cross-method "
+        "consume/borrow/fresh contract was skipped, not guessed. It never fails a build.\n"
+        "Fix: this indicates malformed `functions[]` facts or a bridge bug — re-extract the "
+        "facts, and report the message's inner error if it persists."
+    ),
     "DI002": (
         "A singleton captures a scoped service: the scoped instance is pinned to the singleton "
         "for the whole app lifetime, defeating per-scope (e.g. per-request) semantics and often "

ownlang/ownership.py

@@ -80,7 +80,14 @@ class PathAction:
     kind: `dispose` (releases it) | `adopt` (stores it into an owning field) |
     `return` (returns it — escapes to the caller of *this* method) | `borrow`
     (only reads/uses) | `forward` (passes it to `callee` at position `arg`).
-    The first three are ownership *leaving the caller* on that path (`must`)."""
+    The first three are ownership *leaving the caller* on that path (`must`).
+
+    RESERVED kinds (TZ D3): `adopt` and `return` are understood by the solver but
+    have NO production producer yet — `_build_skeletons` (ownir.py) emits only
+    `dispose`/`borrow`/`forward`. `adopt` awaits interprocedural T4b (a ctor-adopt
+    summary), `return` awaits owned-return-value modelling (a returned param is
+    deliberately NOT a consume signal today, see `_infer_param_effect`). A port
+    must carry their semantics but must not expect to see them from real facts."""
 
     kind: str
     callee: str = ""
@@ -93,7 +100,11 @@ class ParamSkeleton:
     name: str = ""
     disposable: bool = True
     paths: tuple[PathAction, ...] = ()
-    escapes: bool = False  # the reference outlives the call (field/collection/return)
+    # RESERVED axis (TZ D2): "the reference outlives the call" (field / collection
+    # / return). The d5 model keeps escape orthogonal to transfer, but NO producer
+    # sets it yet (`_build_skeletons` always leaves False) — it is carried,
+    # unserialized, and must not be read as evidence until a producer lands.
+    escapes: bool = False
 
 
 @dataclass(frozen=True)
@@ -147,9 +158,13 @@ def to_dict(self) -> dict[str, object]:
             "file": self.file,
             "line": self.line,
             "source": self.source,
+            # `escapes` is deliberately NOT serialized (TZ D2): no producer sets
+            # the axis yet, so emitting it would freeze an always-False lie into
+            # the parity artifact this dump becomes (the roadmap's stage-1
+            # Python↔Rust diff surface). Serialize it the day a producer lands.
             "params": [
                 {"index": p.index, "name": p.name, "disposable": p.disposable,
-                 "transfer": p.transfer.value, "escapes": p.escapes}
+                 "transfer": p.transfer.value}
                 for p in self.params
             ],
             "returns": {"owned": self.returns},