Bridge: compositional ownership contracts on the C# side (P-006/2b)

corpus/oracle-target.txt

@@ -4,12 +4,14 @@
 # Optional lines: ref=, paths=, build=, include_tests=. Dev-branch only.
 #
 # Cross-tool oracle on a Linux-buildable fixture, so ALL THREE tools run (Infer#
-# included — ScreenToGif's WPF won't build on Linux). Re-run #2 of the EXCEPTION-EDGE
-# slice after the first run surfaced two artifacts: (a) #3 (tfLeak) was double-reported
-# — a never-disposed local in a try leaks on BOTH the injected exceptional exit and the
-# normal end; now deduped in the bridge; (b) #4's anchors were >3 lines apart (Own.NET
-# acquire / CodeQL Dispose / Infer# last-access) so the ±3 window split it — the try is
-# now a one-liner adjacent to the acquire. Expect #2/#3/#4 in "Agree" (no dup), #1
-# Own.NET-only, 0 oracle-only. See the README.
+# included — ScreenToGif's WPF won't build on Linux). Re-run after the OWN014
+# migration (PR #35): the fixture's SUBSCRIPTION leak (#1 — SystemEvents.Display
+# SettingsChanged += with no -=) is now lowered by the extractor to a `capture`
+# fact and reported as OWN014 (region escape), not OWN001; OWN014 was added to the
+# comparator's OWN_LEAK set. So #1 must STILL land "Own.NET-only" (CodeQL / Infer#
+# have no event-subscription-leak query) — this run confirms the migration kept the
+# differentiation, on real cross-tool output rather than the selftest's fixtures.
+# Expect: #1 Own.NET-only (now OWN014), #2/#3/#4 dispose leaks in "Agree", 0
+# oracle-only.
 local:corpus/fixtures/systemevents-console
 build=SystemEventsLeak.csproj

corpus/real-world/ownership-handoff-consume/after.cs

@@ -0,0 +1,34 @@
+using System;
+using System.IO;
+
+static class Archiver
+{
+    public static void Archive(Stream source)
+    {
+        source.CopyTo(Stream.Null);
+        source.Dispose();                  // Archive owns and closes it
+    }
+
+    // FIX (leak): dispose what we own. `using` discharges it on every path.
+    static void Leak(string path)
+    {
+        using var s = File.OpenRead(path);
+        Console.WriteLine(s.Length);
+    }
+
+    // FIX (use-after-handoff): read everything we need BEFORE handing ownership
+    // off, then never touch the stream again.
+    static void Run(string path)
+    {
+        var s = File.OpenRead(path);
+        Console.WriteLine(s.Length);
+        Archive(s);                        // move ownership last
+    }
+
+    // Unchanged: this handoff was already correct.
+    static void RunOk(string path)
+    {
+        var s = File.OpenRead(path);
+        Archive(s);
+    }
+}

corpus/real-world/ownership-handoff-consume/before.cs

@@ -0,0 +1,40 @@
+using System;
+using System.IO;
+
+// A consumer that takes OWNERSHIP of the stream: it copies the stream, then
+// disposes it. Callers hand the stream over and must not touch it afterwards.
+// In OwnLang terms `Archive`'s parameter is `consume Stream` -- the release
+// obligation moves into Archive across the call.
+static class Archiver
+{
+    public static void Archive(Stream source)
+    {
+        source.CopyTo(Stream.Null);
+        source.Dispose();                  // Archive owns and closes it
+    }
+
+    // BUG (leak): the stream is neither disposed nor handed to a consumer, so
+    // on the only path it leaks. -> OWN001
+    static void Leak(string path)
+    {
+        var s = File.OpenRead(path);
+        Console.WriteLine(s.Length);
+    }
+
+    // BUG (use-after-handoff): ownership moved into Archive (which disposed it),
+    // then the stream is touched again. -> OWN002
+    static void Run(string path)
+    {
+        var s = File.OpenRead(path);
+        Archive(s);                        // ownership moves to Archive
+        Console.WriteLine(s.Length);       // use-after-dispose through s
+    }
+
+    // OK: same handoff, but nothing touches the stream after it. Correctly not
+    // a leak -- the obligation travelled to Archive.
+    static void RunOk(string path)
+    {
+        var s = File.OpenRead(path);
+        Archive(s);
+    }
+}

corpus/real-world/ownership-handoff-consume/case.own

@@ -0,0 +1,36 @@
+// OwnLang model of an inter-procedural ownership HANDOFF. `acquire`/`release`
+// == a Stream's open/Dispose. `archive` takes the stream BY VALUE (a resource
+// type => CONSUME): ownership MOVES into it and it closes the stream, so a
+// caller must not touch the stream after the handoff.
+//
+// This is the compositional island: `run`/`run_ok` are verified against
+// `archive`'s CONTRACT (consume), not its body -- the release obligation
+// travels across the call. No whole-program analysis: the signature is the cut.
+module Corpus
+resource Stream {
+  acquire open
+  release close
+}
+// first-party consumer: it OWNS the stream (CONSUME) and closes it.
+fn archive(s: Stream) {
+  use s;
+  release s;
+}
+// BUG: an owned stream that is neither closed nor handed to a consumer leaks.
+fn leak() {
+  let s = acquire Stream();
+  use s;
+}
+// BUG: the stream is used after ownership was moved into `archive`.
+fn run() {
+  let s = acquire Stream();
+  archive(s);          // ownership consumed by archive (moves across the call)
+  use s;               // <-- touch after handoff
+}
+// happy path: same handoff, nothing touches the stream afterwards. The
+// obligation travelled to `archive`; `run_ok` neither uses nor releases it,
+// and that is correctly NOT a leak -- the contract discharged it.
+fn run_ok() {
+  let s = acquire Stream();
+  archive(s);
+}

corpus/real-world/ownership-handoff-consume/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN001 OWN002

corpus/real-world/ownership-handoff-consume/notes.md

@@ -0,0 +1,49 @@
+# Inter-procedural ownership handoff (consume)
+
+**Pattern:** one method takes *ownership* of a disposable — it consumes the
+resource and is responsible for releasing it (`Archive(Stream source)` copies,
+then `Dispose()`s). Callers hand the resource over. Two real bugs cluster around
+this shape:
+
+1. **use-after-handoff** — the caller touches the resource after passing it to
+   the consumer, which has already disposed it (`Run`).
+2. **leak** — a resource is acquired but neither disposed nor handed to a
+   consumer on some path (`Leak`).
+
+This is the everyday version of Rust's *move*: passing an owned value to a
+function that takes it by value. It shows up wherever a method's contract is
+"give me this and I'll own it" — `Stream`/`HttpContent` consumers, builders that
+take ownership of their inputs, `IDisposable` sinks.
+
+**What the checker says (on `case.own`):**
+
+- `archive(s: Stream)` — a resource-typed by-value parameter is a **consume**
+  contract: the obligation to `release` moves *into* `archive`, which discharges
+  it. Clean.
+- `leak()` — owned but never released or handed off → **OWN001**.
+- `run()` — `s` is used after `archive(s)` consumed it → **OWN002**
+  (use-after-consume).
+- `run_ok()` — the same handoff, with nothing touching `s` afterwards. Correctly
+  **silent**: `run_ok` never calls `release`, yet it does not leak, because the
+  obligation travelled to `archive` via its *contract*. This no-false-positive
+  on a legitimate handoff is the point — the caller is verified against the
+  callee's signature, not its body.
+
+```text
+$ python -m ownlang check corpus/real-world/ownership-handoff-consume/case.own
+case.own:22:7: error: [OWN001] 's' is owned but not released at end of function (leaks on at least one path)
+case.own:28:7: error: [OWN002] use 's' after it was consumed
+2 errors.
+```
+
+**Why it matters / the honesty caveat:** this is the **compositional /
+inter-procedural island** in miniature. The cross-procedure proof — "acquire in
+the caller, release in the consumer, never use after the move" — composes two
+*intra-procedural* checks glued at `archive`'s contract. No whole-program
+points-to is involved: the signature `consume Stream` is the cut point, exactly
+as Rust's borrow checker is modular against function signatures.
+
+As with every corpus case, `case.own` is a faithful hand reduction of the C#
+pattern in `before.cs` / `after.cs`, **not** C# the checker ingested — OwnLang
+has no C# front-end. The corpus shows the ownership *logic* maps onto real bugs,
+not that the tool scanned real C#.

ownlang/cfg.py

@@ -280,6 +280,12 @@ def build(self) -> CFG:
                 sym = self.declare(p.name, Kind.PLAIN, p.line)
             sym.type_name = p.type.name
             sym.resource_kind = self.resource_kinds.get(p.type.name)
+            # a parameter can be the SUBJECT of a diagnostic (an owned/consume param
+            # that leaks -> OWN001, a borrow misused -> OWN013/OWN004), so give it a
+            # stable origin (name#line) just like an acquired local. Without it the
+            # diagnostic carries subject=None and a consumer that maps findings by
+            # origin (the OwnIR bridge) cannot attribute it.
+            sym.origin = f"{p.name}#{p.line}"
             self.params.append(sym)
 
         entry = self.new_block("entry")