extractor: pooled-buffer-transfer FP fixes (Redis oracle sweep) + FP re-triage

corpus/oracle-fp-baseline.txt

@@ -37,17 +37,28 @@ protobuf-net/protobuf-net | ProtoTranscoder.cs | OWN001 | 'sync' | non-product (
 # a get-only property over a constructed XsltArgumentList field, handler captures `this`).
 # Now fixed at the source by PropertyReturnsOwnedMember — confirmed cleared on a live
 # protobuf oracle run (own-only 0, the finding absent from own-only and baselined) — deleted.
-# FIX LANDED (using-statement local release): `using (timer) { ... }` over an already-acquired
-# local is now threaded as a scope-exit release in --flow-locals. Kept here pending a live-oracle
-# re-run on protobuf to confirm-and-delete. Fixture: local-dispose-via-using-statement.
-protobuf-net/protobuf-net | Page.xaml.cs | OWN001 | local 'timer' | non-product (assorted/ Silverlight sample); the timer is disposed by an enclosing `using (timer) { ... }` the extractor missed
+# RE-TRIAGED 2026-06-28 (live protobuf oracle run + raw source). This is a TRUE POSITIVE, not an
+# FP: `Stopwatch` here is `Nuxleus.Performance.Stopwatch` (the file has `using Nuxleus.Performance;`
+# and uses `Stopwatch.UnitPrecision`/`UnitPrecision.NANOSECONDS`/`timer.Scope = () => …` — NOT
+# System.Diagnostics.Stopwatch), a custom IDisposable scope-timer. `Stopwatch timer = new Stopwatch()`
+# is genuinely never disposed: the disposing `using (timer) { … }` block is COMMENTED OUT. The
+# extractor flags it via the flow-locals path, which requires ImplementsIDisposable — so it
+# correctly resolved the custom type as IDisposable. Kept baselined as NON-PRODUCT sample (assorted/
+# Silverlight perf demo), exactly like the assorted/ NetTranscoder `sync` entry. The earlier
+# "missed using" and "non-IDisposable Stopwatch FP" readings were both wrong; issue #161 is closed.
+protobuf-net/protobuf-net | Page.xaml.cs | OWN001 | local 'timer' | non-product (assorted/ Silverlight perf demo); TRUE POSITIVE — `timer` is a custom IDisposable Nuxleus.Performance.Stopwatch genuinely never disposed (the using(timer) block is commented out). Baselined as non-product, not as an FP
 
 # --- JamesNK/Newtonsoft.Json ----------------------------------------------------
-# STAYS BASELINED (soundness wall): JsonTextWriter is a THIRD-PARTY wrapper — the BCL pass-through
-# exemption (IsNoOpDisposeWrapper) covers only StreamReader/StreamWriter/BinaryReader/BinaryWriter,
-# whose disposal contract is known. Proving JsonTextWriter.Dispose is a no-op needs body analysis we
-# don't do. See docs/notes/no-op-dispose-wrapper.md.
-JamesNK/Newtonsoft.Json | TraceJsonReader.cs | OWN001 | _textWriter | no-op dispose: a JsonTextWriter over an in-memory StringWriter/StringBuilder holds no unmanaged resource, so leaving it undisposed releases nothing
+# STAYS BASELINED — and NOT soundly auto-fixable (investigated 2026-06-28, JsonTextWriter source).
+# JsonTextWriter is NOT a no-op type to dispose: Close() runs base.Close() (auto-completes open JSON
+# tokens — writes closing brackets to the underlying writer) and CloseBufferAndWriter(), which RETURNS
+# its rented `_writeBuffer` to `_arrayPool` when an ArrayPool is configured — a real pooled-buffer
+# release (the very POOL-leak class Own.NET tracks elsewhere) — and closes the underlying writer. So a
+# recursive "Dispose-is-a-no-op" recognizer would be UNSOUND (it can leak a pooled buffer) or would
+# correctly DECLINE — either way it does not clear this. The `_textWriter` instance is benign only by
+# INSTANCE facts (no ArrayPool set + the sink is a StringWriter), not a type-level no-op, so it stays
+# baselined — consistent with excluding writers from IsNoOpDisposeWrapper. See no-op-dispose-wrapper.md.
+JamesNK/Newtonsoft.Json | TraceJsonReader.cs | OWN001 | _textWriter | benign-by-instance, NOT a no-op type: JsonTextWriter.Close() returns a (possibly pooled) write buffer and auto-completes JSON tokens; harmless here only because no ArrayPool is set and the sink is a StringWriter — kept baselined (not soundly auto-fixable)
 JamesNK/Newtonsoft.Json | JsonSerializer.cs | OWN001 | serializer.Error | intra-call self-subscription: the serializer is freshly created from the same JsonSerializerSettings whose .Error handler it subscribes; source and handler are co-lifetimed
 
 # --- JoshClose/CsvHelper --------------------------------------------------------

corpus/real-world/pool-transfer-via-wrapper-local/after.cs

@@ -0,0 +1,23 @@
+using System;
+using System.Buffers;
+
+sealed class Holder : IDisposable
+{
+    readonly int[] _buf;
+    public Holder(int[] buf) => _buf = buf;
+    public void Dispose() => ArrayPool<int>.Shared.Return(_buf);
+}
+
+static class Demo
+{
+    // FIX: the rented buffer is wrapped into a local Holder that is RETURNED — ownership transfers to
+    // the Holder (which Returns the buffer on Dispose), so the buffer does not leak here. The extractor
+    // follows the buffer through the wrapper local because that local provably leaves the method
+    // (`return holder`), so it stays silent. Mirrors StackExchange.Redis Lease<T>.Create.
+    public static Holder Run(int n)
+    {
+        var buf = ArrayPool<int>.Shared.Rent(n);
+        var holder = new Holder(buf);
+        return holder;
+    }
+}

corpus/real-world/pool-transfer-via-wrapper-local/before.cs

@@ -0,0 +1,24 @@
+using System;
+using System.Buffers;
+
+// A wrapper that takes ownership of a rented buffer and returns it to the pool on Dispose.
+sealed class Holder : IDisposable
+{
+    readonly int[] _buf;
+    public Holder(int[] buf) => _buf = buf;
+    public void Dispose() => ArrayPool<int>.Shared.Return(_buf);
+}
+
+static class Demo
+{
+    // BUG: the rented buffer is wrapped into a LOCAL Holder that never leaves the method — it is
+    // dropped (never disposed, never returned, never handed out) — so the buffer is genuinely never
+    // returned to the pool. A real pooled-buffer leak (OWN001). The wrapper being method-scoped is
+    // exactly the case the transfer exemption must NOT cover.
+    public static void Run(int n)
+    {
+        var buf = ArrayPool<int>.Shared.Rent(n);
+        var holder = new Holder(buf);   // method-scoped; dropped -> buffer leaks
+        _ = holder.GetHashCode();
+    }
+}

corpus/real-world/pool-transfer-via-wrapper-local/case.own

@@ -0,0 +1,19 @@
+// OwnLang model of a rented ArrayPool buffer that (in the fix) is transferred to a wrapper which
+// leaves the method through a local — StackExchange.Redis Lease<T>.Create (`var lease = new
+// Lease(arr); return lease;`) and RedisServer scan (`var r = new ScanResult(keys); SetResult(m, r)`).
+// The before.cs wraps the buffer in a METHOD-SCOPED Holder that is dropped, so the buffer is never
+// returned -> a real leak, modelled here as an acquire with no `release` (OWN001). The after.cs
+// returns the wrapper, so the extractor follows the transfer through the escaping local and stays
+// silent (extractor-level; the before.cs/after.cs benchmark exercises it end to end). See notes.md.
+module Corpus
+resource Buffer {
+  acquire rent
+  release give
+  emit_type    "int[]"
+  emit_acquire "ArrayPool<int>.Shared.Rent({args})"
+  emit_release "ArrayPool<int>.Shared.Return({0})"
+}
+fn Run(n: int) {
+  let buf = acquire Buffer(n);   // ArrayPool.Rent; wrapped in a method-scoped Holder, never returned
+  // no `release buf;` -> OWN001
+}

corpus/real-world/pool-transfer-via-wrapper-local/expected-diagnostics.txt

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

corpus/real-world/pool-transfer-via-wrapper-local/notes.md

@@ -0,0 +1,45 @@
+# pool-transfer-via-wrapper-local
+
+A rented `ArrayPool<T>` buffer handed to a **wrapper object bound to a local**, where that local
+then **leaves the method** — `var w = new Wrapper(buf); return w;` / `Sink(m, w);` — is an ownership
+**transfer** (the wrapper carries the buffer out and is responsible for `Return`), not a leak here.
+Generalises the existing direct `return new Wrapper(buf)` / `_field = new Wrapper(buf)` transfer to
+the one-extra-hop case an intermediate local introduces.
+
+Mined on **StackExchange.Redis** (2026-07-01 oracle sweep):
+
+- `Lease<T>.Create` — `var arr = ArrayPool<T>.Shared.Rent(length); var lease = new Lease<T>(arr,
+  length); … return lease;`
+- `RedisServer` scan — `keys = ArrayPool<RedisKey>.Shared.Rent(count); … var r = new ScanResult(
+  cursor, keys, count, true); SetResult(message, r);`
+
+Both were false `OWN001` "rented but never returned" — the buffer is transferred to `Lease`/
+`ScanResult`, which owns the `Return`.
+
+- **before.cs** — the buffer is wrapped into a **method-scoped** `Holder` that is dropped (never
+  disposed / returned / handed out) → the buffer genuinely leaks → `OWN001` (the bug is caught; the
+  transfer exemption must **not** cover a wrapper that never leaves the method).
+- **after.cs** — the `Holder` local is **returned** → the buffer transfers out with it → **clean**.
+
+## Recognition rule
+
+`PassedToEscapingCtor` already exempts a pooled buffer passed to a constructor whose result is the
+direct `return` value or is assigned to a real field. `WrapperLocalEscapes` adds the one-extra-hop
+case: the `new Wrapper(buf)` is bound to a **local** `w`, and `w` provably leaves the method —
+`return w`, `<field> = w`, or `w` handed as a **call argument**. The Codex one-level rule is
+preserved for the non-escaping case: a wrapper local that stays method-scoped is a borrow and the
+buffer still leaks.
+
+## Honesty caveat
+
+Precision-first, mirroring the direct-transfer rule: we cannot prove the wrapper actually `Return`s
+the buffer, so a wrapper that escapes but silently drops the buffer would be a (rare) missed leak.
+The `w`-as-call-argument signal is the loosest — a `Sink(w)` that merely reads `w` and drops it would
+be exempted — but handing a buffer-owning wrapper to a call is a transfer in idiomatic pooling code,
+and erring toward no-false-positive matches the existing transfer stance.
+
+To stay sound against a **reused local** (Codex P2), the exemption is bound to the **declaration
+form only** (`var w = new Wrapper(buf)`) and **bails if `w` is reassigned anywhere** — otherwise
+`var w = new Wrapper(buf); w = other; return w;` (or `Sink(w); … w = new Wrapper(buf);`) would let a
+`return`/call of a *different* value untrack `buf`, missing a real leak. A reused wrapper local keeps
+the buffer flagged.

docs/ROADMAP.md

@@ -186,9 +186,21 @@ architectural strictness, and the borrow-checker showcase):
    the subscriber stays silent (no false positive) where the token tier only warns,
    and a released `-=` mitigates the capture. Proven by the `capture` fixture, the
    `StaticEventEscapeViewModel` sample (CI `wpf-extractor` → OWN014), and the
-   `corpus/wpf/systemevents-region-escape` reduction (P-004 WPF005 ✅). Remaining:
-   migrating the *injected*-source subscription tier (today an honest OWN001
-   warning) once lifetime modelling can prove or refute those sources.
+   `corpus/wpf/systemevents-region-escape` reduction (P-004 WPF005 ✅). The
+   **injected-source tier migration is now shipped** via the DI graph (P-006 + P-004,
+   `di_source_life`): an injected `+=` whose `source_type` resolves in the registration
+   graph reroutes through the region engine — a source proven to strictly **outlive** the
+   subscriber escalates the OWN001 *warning* to **OWN014** (a proven captive/region escape,
+   error-tier), a source **co-lifetimed or shorter** is *refuted* and dropped silently, and
+   an **unresolved** source (not in the DI graph) correctly stays the honest OWN001 warning
+   ("may outlive"). Covered by `test_ownir.py` (208/208 bridge checks, incl. the DI-sourced
+   escape + the "no DI info → stays a warning" regression). Residual is by design, not a gap:
+   a non-DI injected source has no provable lifetime, so warning is the honest verdict.
+   Escalating *those* by a curated "known app-lived source type" allowlist (e.g. MVVM
+   `IMessenger`/`IEventAggregator`) is **deliberately deferred as FP-prone** — modern
+   CommunityToolkit `WeakReferenceMessenger` holds recipients *weakly* (no leak), so a
+   type-name allowlist would mis-flag the safe case; it needs weak-vs-strong reference
+   evidence we don't model.
 3. **DI lifetimes** — registration + constructor graph; captive dependency (P-006).
    ◑ *In progress* — DI001 lands end to end: the C# extractor builds the
    registration + constructor graph from `Add{Singleton,Scoped,Transient}` (generic

docs/notes/no-op-dispose-wrapper.md

@@ -55,22 +55,31 @@ The motivating oracle finding was Newtonsoft.Json's `TraceJsonReader._textWriter
 
 ```csharp
 _sw = new StringWriter(CultureInfo.InvariantCulture);
-_textWriter = new JsonTextWriter(_sw); // a no-op in truth — but JsonTextWriter is third-party
+_textWriter = new JsonTextWriter(_sw); // looks like a no-op — but JsonTextWriter is NOT a no-op type
 ```
 
-Structurally identical, but `JsonTextWriter` is a **third-party** wrapper (`JsonWriter`,
-not a BCL `TextWriter`). We cannot prove *its* `Dispose` is pass-through without modelling
-its body — and asserting a no-op we cannot prove is exactly the unsound over-reach that
-sank the static-class subscriber exemption (see
-[`oracle-known-fps.md` → Rejected approaches](oracle-known-fps.md)). So Newtonsoft's
-`_textWriter` stays a **baselined** finding in
-[`oracle-fp-baseline.txt`](../../corpus/oracle-fp-baseline.txt), not a silent drop.
-
-Retiring that baseline entry would need a general, recursive "Dispose is a no-op"
-analysis over a first-party type's body (it disposes only dispose-optional members and
-holds no unmanaged handle). That is a larger, higher-risk capability; until it lands, only
-the BCL pass-through adapters — whose disposal contract is documented and fixed — are
-exempted.
+It looks structurally identical to the BCL reader case, but a 2026-06-28 read of the real
+`JsonTextWriter` source shows it is **not a no-op type to dispose**:
+
+- `Close()` runs `base.Close()` — which **auto-completes open JSON tokens** (writes closing
+  brackets to the underlying writer) — then `CloseBufferAndWriter()`;
+- `CloseBufferAndWriter()` **returns its rented `_writeBuffer` to `_arrayPool`** when an
+  `ArrayPool` is configured — a real **pooled-buffer release** (the very POOL-leak class
+  Own.NET tracks elsewhere) — and closes the underlying writer.
+
+So disposal has genuine side effects (a conditional pooled-buffer return, token-completion
+writes). This is the same reason we **exclude writers** (`StreamWriter`/`BinaryWriter`) from
+`IsNoOpDisposeWrapper` — a writer's `Dispose` does real work. A recursive "Dispose is a
+no-op" recognizer over the body would therefore either be **unsound** (it can leak a pooled
+buffer) or correctly **decline** — so it would not clear this finding regardless. Asserting a
+no-op we cannot prove is exactly the unsound over-reach that sank the static-class subscriber
+exemption (see [`oracle-known-fps.md` → Rejected approaches](oracle-known-fps.md)).
+
+The `_textWriter` *instance* is benign only by **instance facts** — no `ArrayPool` is set on
+it, and its sink is a `StringWriter` — not by any type-level no-op property. So it stays a
+**baselined** finding in [`oracle-fp-baseline.txt`](../../corpus/oracle-fp-baseline.txt), not
+a silent drop, and the "recursive Dispose-no-op analysis" idea is **shelved as not worth
+building** (it wouldn't soundly clear the one case that motivated it).
 
 ## Corpus