feat(d5): D5.1b — per-call-site ownership-contract channel

docs/notes/d5-ownership-transfer.md

@@ -239,12 +239,45 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa
   first-party. Live catches, proven by synthetic OwnIR tests: double-dispose / use-after
   across a *transitive* (multi-hop) consuming call (OWN002), and the precision win where a
   correct forwarded handoff that used to read as a false OWN001 leak is now silent.
-- **D5.1b — `leaveOpen` Tier-B slice (next).** `StreamReader(stream, leaveOpen:…)` &c. is a
-  *per-call-site* contract — the same ctor consumes or borrows by the bool literal — so it
-  needs a per-call effect channel on the `call` op plus the extractor reading the literal,
-  rather than a per-method summary. Small, additive; pairs with a CI A/B sample on the real
-  extractor output (the end-to-end validation that first-party `call` ops are emitted for
-  forwarding chains).
+- **D5.1b — the per-call-site ownership-contract channel (shipped).** `StreamReader(stream,
+  leaveOpen:…)` &c. is a *per-call-site* contract — the same ctor consumes or borrows by the
+  bool literal — so it needs a per-call effect channel rather than a per-method summary. The
+  bridge now pre-declares three fixed sink externs (`$consume` / `$borrow` / `$borrow_mut`)
+  in every lowered `Module`; the extractor routes any call's per-argument ownership through
+  them (`call $consume [x]`), and they resolve via the **same** `collect_signatures` +
+  `lower_call` path as any contracted call — no new checker, no new flow lowering. The `$`
+  prefix cannot collide with a real C# member. The solver also reads a forward to a sink as a
+  *known* transfer (`$consume`→must, `$borrow`→no), so the channel propagates **transitively**
+  through first-party wrappers, not just at the direct call. `$borrow_mut` is intentionally
+  excluded from the *transitive* shortcut — the transfer lattice has no shared-vs-exclusive
+  axis, so a wrapper summary would silently downgrade an exclusive loan to a shared one; the
+  honest move is to decline that claim (the wrapper param stays plain) while the *direct*
+  `$borrow_mut` call keeps full exclusivity through `lower_call` (Codex P2). Proven by synthetic
+  OwnIR tests:
+  use/double-release after `$consume` (OWN002), a `$borrow`'d-then-never-released local still
+  leaking (OWN001), a clean borrow-then-release, and transitive propagation through a wrapper.
+  The remaining piece is **CI/C#-only**: the extractor emitting these sink calls from the bool
+  literal / annotation (paired with an A/B sample on real extractor output) — Tier-B breadth
+  rides into D5.3.
+- **D5.1c — transitive borrow-kind propagation (deferred).** The D5.0 summary solver is
+  *transfer*-oriented: its `Transfer` lattice (no/must/may/unknown) has no shared-vs-exclusive
+  axis, so an explicit `borrow`/`borrow_mut` and a `$borrow_mut` forward both seed the same
+  summary-side `borrow` bucket. The **core checker already distinguishes them** (`cfg.py`
+  emits `Effect.BORROW` vs `BORROW_MUT`; `analysis.py` routes them to `_check_shared_borrowable`
+  vs `_check_mut_borrowable`), so the *direct* `$borrow_mut` call keeps full exclusivity — only
+  the *transitive* claim through a first-party wrapper is lost. D5.1b takes the precision-safe
+  decline (a wrapper that only forwards to `$borrow_mut` stays plain — a tolerated false-
+  negative, never a false shared-borrow assertion). The clean fix is **not** one more `Transfer`
+  enum value but an **orthogonal borrow-kind axis** (`none | shared | mut`) on the summary,
+  structured sink semantics (don't normalize `$borrow_mut` away before inference), and the same
+  brutally-conservative rule the must-consume path uses: 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. Deliverables: borrow-kind on the summary, direct
+  behaviour unchanged, `$borrow_mut` wrapper tests, and mixed-path regressions proving ambiguous
+  flows degrade to silence (not shared borrow). Prior art: Rust `&`/`&mut`, RustBelt exclusivity,
+  Oxide's `shrd|uniq`, Polonius's per-loan invalidation — exclusivity is a distinct semantic
+  axis, not coarser metadata. Tracked here so the deferral is recorded, not buried (Codex P2 /
+  CodeRabbit Major on #113).
 - **D5.2 — T1.** `fresh`-returning calls become acquire sites → factory leaks. Includes
   `out`/`ref`-owned (another `fresh` door) before async.
 - **D5.3 — Tier B breadth.** The rest of the documented BCL ownership table + `fresh`

ownlang/ownir.py

@@ -106,7 +106,10 @@
 from .ast_nodes import (
     Acquire,
     Call,
+    Effect,
+    EffectParam,
     Expr,
+    ExternDecl,
     FnDecl,
     If,
     Let,
@@ -848,7 +851,9 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]]
                     if _returns_value(nodes) else None)
             functions.append(FnDecl(fname, fparams, fret, fbody, 0))
     return (Module(str(facts.get("module", "Extracted")),
-                   resources=_prelude_resources(), functions=functions,
+                   resources=_prelude_resources(),
+                   externs=list(_OWNERSHIP_SINK_EXTERNS),
+                   functions=functions,
                    lifetimes=list(_CAPTURE_LIFETIMES) if any_capture else []),
             handles)
 
@@ -913,6 +918,37 @@ def _returns_value(nodes: Any) -> bool:
     "borrow_mut": TypeRef("Disposable", True, True),  # exclusive loan, noescape
 }
 
+# P-005 D5.1b — the per-call-site ownership-contract channel. The extractor cannot
+# always pin a call's ownership effect from a first-party body: a BCL sink (e.g.
+# `new StreamReader(s, leaveOpen: false)`) or a `[ConsumesOwnership]`-style
+# annotation lives outside our summary set. Rather than grow a bespoke lowering for
+# each such case, we pre-declare three fixed sink externs and let the extractor
+# route any call's per-argument ownership through them: a `call $consume [x]` takes
+# ownership of `x`, `$borrow`/`$borrow_mut` lend it for the call. They resolve via
+# the SAME `collect_signatures` + `lower_call` path as any contracted call (so a
+# later use of a consumed `x` is OWN002, an un-discharged borrow is still OWN001) —
+# no new checker, no new flow lowering. Externs are declaration-only, never leak-
+# checked themselves, and the `$` prefix cannot collide with a real C# member name.
+_OWNERSHIP_SINK_EXTERNS = (
+    ExternDecl("$consume", [EffectParam(Effect.CONSUME, "Disposable", 0)], None, 0),
+    ExternDecl("$borrow", [EffectParam(Effect.BORROW, "Disposable", 0)], None, 0),
+    ExternDecl("$borrow_mut",
+               [EffectParam(Effect.BORROW_MUT, "Disposable", 0)], None, 0),
+)
+
+# A forward to a sink extern is a *known* transfer, so a skeleton can record the
+# resolved path action directly — `$consume` is ownership leaving (a must-transfer),
+# `$borrow` is a kept loan — rather than a `forward` edge to an unsummarized callee
+# (which the solver would degrade to `unknown`, diluting a real `must` to plain).
+# `$borrow_mut` is DELIBERATELY ABSENT (Codex P2): the transfer lattice carries no
+# shared-vs-exclusive axis, so mapping it to `borrow` would silently downgrade an
+# EXCLUSIVE loan to a shared one in the wrapper's contract — asserting something
+# weaker than the truth. We decline the transitive claim instead (it falls through
+# to a `forward` edge → `unknown` → the wrapper param stays plain, no false shared-
+# borrow contract). The DIRECT `call $borrow_mut [x]` channel is unaffected and keeps
+# full exclusivity through `lower_call`. Kept in sync with `_OWNERSHIP_SINK_EXTERNS`.
+_SINK_PATH_ACTION = {"$consume": "dispose", "$borrow": "borrow"}
+
 
 def _param_signals(pname: str, nodes: Any) -> tuple[bool, bool, bool]:
     """Scan a flow body for how parameter `pname` is treated, returning
@@ -970,6 +1006,17 @@ def _forward_targets(pname: str, nodes: Any,
     return out
 
 
+def _forward_path_action(callee: str, arg: int) -> PathAction:
+    """The skeleton path action for one forward edge. A forward to a fixed
+    ownership-sink extern (D5.1b) is a *resolved* transfer recorded directly
+    (`$consume` → `dispose`, `$borrow*` → `borrow`); any other callee is a
+    `forward` edge the solver resolves against that callee's summary."""
+    kind = _SINK_PATH_ACTION.get(callee)
+    if kind is not None:
+        return PathAction(kind)
+    return PathAction("forward", callee, arg)
+
+
 def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]:
     """Derive a Method Ownership Summary skeleton per first-party function from its
     flow body, for the D5.0 solver (P-005 D5.1). A parameter's path actions mirror
@@ -1025,7 +1072,7 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]:
                 elif passed:
                     allt = _forward_targets(cname, body)
                     top = _forward_targets(cname, body, recurse=False)
-                    paths = tuple(PathAction("forward", c, j) for c, j in allt)
+                    paths = tuple(_forward_path_action(c, j) for c, j in allt)
                     if not (len(allt) == 1 and len(top) == 1):
                         # not a single unconditional handoff: a no-transfer path
                         # exists (other branch / zero-trip loop / sibling call), so

tests/test_ownir.py

@@ -1254,6 +1254,95 @@ def _sub(source: str | None) -> list[Finding]:
     if cond:
         gotc = [(x.component, x.code) for x in cond]
         fails.append(f"D5.1 conditional forward must be `may`: caller stays silent, got {gotc}")
+    # --- P-005 D5.1b: the per-call-site ownership-contract channel. The extractor
+    #     routes a call's per-argument ownership through fixed sink externs
+    #     ($consume / $borrow / $borrow_mut) the bridge pre-declares, so an effect
+    #     the callee's body cannot reveal (a BCL `leaveOpen: false`, an annotation)
+    #     is checked through the SAME lower_call path — no new checker.
+    # $consume takes ownership: a local acquired then handed to $consume has left, so
+    # a later USE is OWN002 (anchored at the acquire, like every transitive handoff).
+    checks += 1
+    csink = check_facts({"module": "M", "functions": [
+        {"name": "use_after_consume", "file": "F.cs",
+         "body": [{"op": "acquire", "var": "x", "line": 10},
+                  {"op": "call", "callee": "$consume", "args": ["x"], "line": 11},
+                  {"op": "use", "var": "x", "line": 12}]}]})
+    gotcs = [(x.component, x.line, x.code) for x in csink]
+    if gotcs != [("use_after_consume", 10, "OWN002")]:
+        fails.append("D5.1b $consume channel: use after a $consume handoff must be "
+                     f"OWN002@10 (ownership left at the call), got {gotcs}")
+    # releasing AFTER $consume double-discharges (the obligation already moved out).
+    checks += 1
+    crel = check_facts({"module": "M", "functions": [
+        {"name": "release_after_consume", "file": "F.cs",
+         "body": [{"op": "acquire", "var": "x", "line": 20},
+                  {"op": "call", "callee": "$consume", "args": ["x"], "line": 21},
+                  {"op": "release", "var": "x", "line": 22}]}]})
+    gotcr = [(x.component, x.line, x.code) for x in crel]
+    if gotcr != [("release_after_consume", 20, "OWN002")]:
+        fails.append("D5.1b $consume channel: release after a $consume handoff must be "
+                     f"OWN002@20, got {gotcr}")
+    # $borrow only LENDS for the call: the caller keeps ownership, so a local handed
+    # to $borrow and never released is still a leak (OWN001) — the channel does NOT
+    # over-consume a borrow into a (silent) transfer.
+    checks += 1
+    bleak = check_facts({"module": "M", "functions": [
+        {"name": "borrow_then_leak", "file": "F.cs",
+         "body": [{"op": "acquire", "var": "x", "line": 30},
+                  {"op": "call", "callee": "$borrow", "args": ["x"], "line": 31}]}]})
+    gotbl = [(x.component, x.line, x.code) for x in bleak]
+    if gotbl != [("borrow_then_leak", 30, "OWN001")]:
+        fails.append("D5.1b $borrow channel: a borrowed-then-never-released local must "
+                     f"still leak OWN001@30 (borrow keeps ownership), got {gotbl}")
+    # and $borrow then releasing is clean — the loan is returned, the owner discharges.
+    checks += 1
+    bclean = check_facts({"module": "M", "functions": [
+        {"name": "borrow_then_release", "file": "F.cs",
+         "body": [{"op": "acquire", "var": "x", "line": 40},
+                  {"op": "call", "callee": "$borrow", "args": ["x"], "line": 41},
+                  {"op": "release", "var": "x", "line": 42}]}]})
+    if bclean:
+        fails.append("D5.1b $borrow channel: borrow-then-release must be clean, "
+                     f"got {[(x.component, x.code) for x in bclean]}")
+    # the DIRECT $borrow_mut channel keeps the exclusive loan: like $borrow, it lends
+    # for the call and the caller keeps ownership, so a never-released local still
+    # leaks (OWN001) and a released one is clean. (The transitive shortcut for
+    # $borrow_mut is deliberately declined — the transfer lattice has no shared-vs-
+    # exclusive axis, so a wrapper would silently downgrade it; see _SINK_PATH_ACTION.)
+    checks += 1
+    bmleak = check_facts({"module": "M", "functions": [
+        {"name": "borrow_mut_leak", "file": "F.cs",
+         "body": [{"op": "acquire", "var": "x", "line": 50},
+                  {"op": "call", "callee": "$borrow_mut", "args": ["x"], "line": 51}]}]})
+    gotbm = [(x.component, x.line, x.code) for x in bmleak]
+    if gotbm != [("borrow_mut_leak", 50, "OWN001")]:
+        fails.append("D5.1b $borrow_mut channel: a borrowed-then-never-released local "
+                     f"must still leak OWN001@50 (exclusive loan keeps ownership), got {gotbm}")
+    checks += 1
+    bmclean = check_facts({"module": "M", "functions": [
+        {"name": "borrow_mut_release", "file": "F.cs",
+         "body": [{"op": "acquire", "var": "x", "line": 60},
+                  {"op": "call", "callee": "$borrow_mut", "args": ["x"], "line": 61},
+                  {"op": "release", "var": "x", "line": 62}]}]})
+    if bmclean:
+        fails.append("D5.1b $borrow_mut channel: borrow_mut-then-release must be clean, "
+                     f"got {[(x.component, x.code) for x in bmclean]}")
+    # the channel resolves TRANSITIVELY too: a param ONLY forwarded to $consume makes
+    # the method a must-consumer (the solver reads the sink as a known transfer), so a
+    # caller using its arg after the handoff is OWN002 — same as forwarding to a
+    # first-party consumer, but sourced from the per-call channel.
+    checks += 1
+    ctrans = check_facts({"module": "M", "functions": [
+        {"name": "wrap_consume", "file": "F.cs", "params": [{"name": "s", "line": 1}],
+         "body": [{"op": "call", "callee": "$consume", "args": ["s"], "line": 2}]},
+        {"name": "caller_t", "file": "F.cs",
+         "body": [{"op": "acquire", "var": "s", "line": 10},
+                  {"op": "call", "callee": "wrap_consume", "args": ["s"], "line": 11},
+                  {"op": "use", "var": "s", "line": 12}]}]})
+    gotct = [(x.component, x.line, x.code) for x in ctrans]
+    if gotct != [("caller_t", 10, "OWN002")]:
+        fails.append("D5.1b $consume channel must propagate transitively: a param "
+                     f"forwarded to $consume makes the method consume, got {gotct}")
     # POOL005: a full-length view of a pooled buffer (`overspan` flow fact) raises
     # OWN025 at the VIEW site (line 12, not the Rent site), tagged a pooled buffer;
     # the buffer is still returned, so there is no OWN001 leak. Routes through the