feat(pool): POOL005 .Length spelling + MemoryPool tracking (POOL001/002/003)

.github/workflows/ci.yml

@@ -788,10 +788,14 @@ jobs:
         # `buf.AsMemory()`) is a borrow lowered to a use of the OWNER (`ViewOwner`), so using it
         # after `Return(buf)` trips OWN002 — including RETURNING a `Memory<T>` view (which, unlike a
         # ref-struct `Span`, can ESCAPE the method), a dangling borrow handed to the caller. A
-        # FULL-length view of a pooled buffer (`buf.AsSpan()` with no length bound) reaches past the
-        # rented logical length into the oversized tail -> OWN025 (P-007 POOL005, the over-read; the
-        # `arraypool-fullspan-overread` case). Remaining backlog: a FIELD-mediated cross-method
-        # use-after-dispose (dispose in one method, use in another via shared state), a view stored in
+        # view of a pooled buffer reaches past the rented length into the oversized tail -> OWN025
+        # (P-007 POOL005, the over-read): the unbounded `buf.AsSpan()` AND the `.Length` view spelling
+        # (`buf.AsSpan(0, buf.Length)`) — the `arraypool-fullspan-overread` / `arraypool-length-
+        # overread` cases (a write/wipe like `Array.Clear(buf, 0, buf.Length)` is not flagged).
+        # MemoryPool is now tracked too: a
+        # `MemoryPool<T>.Rent` IMemoryOwner is released by Dispose, so its leak / double-dispose /
+        # use-after-dispose ride the flow (POOL001/002/003 — the `memorypool-double-dispose` case ->
+        # OWN003). Remaining backlog: a FIELD-mediated cross-method use-after-dispose, a view stored in
         # a FIELD, and an injected-source region-escape. A drop below the floor is a regression.
-        run: python scripts/benchmark.py --min-recall 14
+        run: python scripts/benchmark.py --min-recall 16
 

corpus/real-world/arraypool-length-overread/after.cs

@@ -0,0 +1,20 @@
+// AFTER (fixed). The view is bound to the logical length `n` — `buf.AsSpan(0, n)` —
+// so only the `n` valid payload bytes are read; the oversized `[n, Length)` tail is
+// never touched. No `.Length`-spelled view remains, so the extractor emits no
+// `overspan` fact and the checker is silent.
+using System;
+using System.Buffers;
+
+static class PoolLengthOverread
+{
+    static void Frame(int n)
+    {
+        byte[] buf = ArrayPool<byte>.Shared.Rent(n);
+        Fill(buf, n);
+        Emit(buf.AsSpan(0, n));    // bounded by the rented length n
+        ArrayPool<byte>.Shared.Return(buf);
+    }
+
+    static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
+    static void Emit(ReadOnlySpan<byte> data) { }
+}

corpus/real-world/arraypool-length-overread/before.cs

@@ -0,0 +1,29 @@
+// BEFORE (buggy). POOL005, the `.Length` spelling of the over-read. A rented array
+// is OVERSIZED: `ArrayPool<T>.Shared.Rent(n)` returns an array of `Length >= n`.
+// Viewing it with `buf.Length` — the oversized backing length — as the bound,
+// `buf.AsSpan(0, buf.Length)`, spans the WHOLE array, so a consumer reads the `n`
+// valid bytes PLUS the stale `[n, Length)` tail a previous renter left: a wrong-
+// length read and an information disclosure. The fix is `buf.AsSpan(0, n)` (after.cs).
+//
+// Note: an over-CLEAR like `Array.Clear(buf, 0, buf.Length)` is deliberately NOT
+// flagged — it only overwrites the pooled tail with zeros (a safe clear-before-Return
+// idiom) and exposes nothing. The bug is READING/COPYING the tail, which the view
+// spelling does.
+//
+// Wrapped in a class so the extractor's per-class flow pass visits it; helpers stubbed.
+using System;
+using System.Buffers;
+
+static class PoolLengthOverread
+{
+    static void Frame(int n)
+    {
+        byte[] buf = ArrayPool<byte>.Shared.Rent(n);
+        Fill(buf, n);                       // valid payload is buf[0..n]
+        Emit(buf.AsSpan(0, buf.Length));    // <-- BUG: length is buf.Length, not n -> reads the stale tail
+        ArrayPool<byte>.Shared.Return(buf);
+    }
+
+    static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
+    static void Emit(ReadOnlySpan<byte> data) { }
+}

corpus/real-world/arraypool-length-overread/case.own

@@ -0,0 +1,17 @@
+// OwnLang model of the POOL005 `.Length` over-read. `acquire` == ArrayPool.Rent
+// (oversized: Length >= n), `release` == ArrayPool.Return. `overspan buf` models a
+// view whose length is the buffer's OWN oversized `.Length` (`buf.AsSpan(0, buf.Length)`),
+// which spans the whole array — a consumer reads past the rented `n` into the stale
+// tail. Bounding by `n` takes no full view, so the fix has no `overspan` and is silent.
+// -> OWN025. The buffer is still returned, so there is no leak (OWN001).
+module Corpus
+resource Buffer {
+  acquire rent
+  release give
+  kind "pooled buffer"
+}
+fn frame(n: int) {
+  let buf = acquire Buffer(n);   // ArrayPool.Rent  (Length >= n)
+  overspan buf;                  // buf.AsSpan(0, buf.Length) — spans the whole array -> OWN025
+  release buf;                   // ArrayPool.Return
+}

corpus/real-world/arraypool-length-overread/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN025

corpus/real-world/arraypool-length-overread/notes.md

@@ -0,0 +1,28 @@
+# ArrayPool over-read — the `.Length` spelling (POOL005)
+
+**Pattern:** a pooled array from `ArrayPool<T>.Shared.Rent(n)` is *oversized*
+(`Length >= n`). A view that uses `buf.Length` — the oversized backing length — as
+its bound (`buf.AsSpan(0, buf.Length)`, `new Span<T>(buf, 0, buf.Length)`) spans the
+whole array, so reading or copying through it processes the `n` valid bytes **plus**
+the stale `[n, Length)` tail a previous renter left: a wrong-length read and a
+potential information disclosure. The fix is to bound by the logical length:
+`buf.AsSpan(0, n)`.
+
+This is the `.Length` sibling of `arraypool-fullspan-overread` (which catches the
+unbounded `buf.AsSpan()`): same OWN025, a different way of writing the oversized
+length. The extractor recognises the `.Length`-as-length argument on the buffer's
+own view (start `0`, resolved BCL symbols) and emits an `overspan` fact.
+
+**Not flagged: the over-clear.** `Array.Clear(buf, 0, buf.Length)` (and the single-arg
+`Array.Clear(buf)`) only *overwrite* the pooled tail with zeros — a safe
+clear-before-`Return` idiom that exposes nothing. POOL005 is about *reading/copying*
+too much, not *writing* too much (Codex review); only the **view** is flagged.
+
+**What the checker says:** **OWN025** `[resource: pooled buffer]` at the view. The
+buffer is still `Return`ed, so there is no OWN001 leak.
+
+**Honesty / scope.** `case.own` is a faithful hand reduction (not C# ingested by the
+checker); `before.cs` / `after.cs` are representative of the bug and its fix.
+
+Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target
+AiDotNet.Tensors pooled-buffer over-read.

corpus/real-world/memorypool-double-dispose/after.cs

@@ -0,0 +1,16 @@
+// AFTER (fixed). A `using` declaration disposes the owner exactly once, at the end
+// of the scope, on every path — no second Dispose. The pooled memory is released
+// once and returned to the pool cleanly, so the checker is silent.
+using System;
+using System.Buffers;
+
+static class MemoryPoolDoubleDispose
+{
+    static void Run(int n)
+    {
+        using IMemoryOwner<byte> owner = MemoryPool<byte>.Shared.Rent(n);
+        Work(owner.Memory);
+    }
+
+    static void Work(Memory<byte> data) { }
+}

corpus/real-world/memorypool-double-dispose/before.cs

@@ -0,0 +1,30 @@
+// BEFORE (buggy). POOL003 for the OTHER pool: a `MemoryPool<T>` hands back an
+// `IMemoryOwner<T>` released by `Dispose()` (there is no `Return`). Disposing the
+// same owner twice — here on the success path AND again in `finally` — is a double
+// release: the same memory can later be handed to two renters at once, exactly the
+// corruption dotnet/runtime#33767 describes for ArrayPool double-return. The fix is
+// to dispose exactly once (a `using` owner, see after.cs).
+//
+// Wrapped in a class so the extractor's per-class flow pass visits it; the helper
+// is stubbed so the reduction is self-contained.
+using System;
+using System.Buffers;
+
+static class MemoryPoolDoubleDispose
+{
+    static void Run(int n)
+    {
+        IMemoryOwner<byte> owner = MemoryPool<byte>.Shared.Rent(n);
+        try
+        {
+            Work(owner.Memory);
+            owner.Dispose();     // disposed here ...
+        }
+        finally
+        {
+            owner.Dispose();     // <-- ... and again here (double release)
+        }
+    }
+
+    static void Work(Memory<byte> data) { }
+}

corpus/real-world/memorypool-double-dispose/case.own

@@ -0,0 +1,14 @@
+// OwnLang model of the MemoryPool double-dispose. A MemoryPool<T> owner is
+// `acquire`d by Rent and `release`d by Dispose (there is no Return). Disposing it
+// twice is a double release -> OWN003 — the same verdict as an ArrayPool
+// double-return; the pool can then hand the same memory to two renters at once.
+module Corpus
+resource MemoryOwner {
+  acquire Rent
+  release Dispose
+}
+fn run(n: int) {
+  let owner = acquire MemoryOwner(n);   // MemoryPool.Rent
+  release owner;                        // owner.Dispose()
+  release owner;                        // owner.Dispose() again -> OWN003
+}

corpus/real-world/memorypool-double-dispose/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN003

corpus/real-world/memorypool-double-dispose/notes.md

@@ -0,0 +1,26 @@
+# MemoryPool double-dispose (POOL003, the Dispose-released pool)
+
+**Pattern:** `MemoryPool<T>.Shared.Rent(n)` returns an `IMemoryOwner<T>` whose
+backing memory is returned to the pool by **`Dispose()`** (there is no `Return`).
+Disposing the same owner twice — classically once on the normal path and again in a
+`finally`/`Dispose`, or two explicit `Dispose()` calls — double-releases the memory,
+so the pool can hand it to two renters simultaneously. This is the MemoryPool twin of
+`arraypool-double-return` (dotnet/runtime#33767).
+
+**What it adds:** the extractor now tracks `MemoryPool<T>.Shared.Rent` as an owned
+resource (an `IMemoryOwner` released by `Dispose`, the IDisposable path — *not* a
+`Return`-based pool buffer). With that one acquire recognised, the existing
+flow-sensitive checker covers the whole MemoryPool family: **POOL001** (never
+disposed → OWN001), **POOL002** (owner used after `Dispose` → OWN002), and
+**POOL003** (this case — disposed twice → **OWN003**).
+
+**What the checker says:** the OwnLang model and the real `before.cs` both trip
+**OWN003** (double release). The `using` fix in `after.cs` disposes exactly once and
+is silent.
+
+**Honesty / scope.** `case.own` is a faithful hand reduction (not C# ingested by the
+checker); `before.cs` / `after.cs` are representative of the bug and its fix. The
+`IMemoryOwner.Memory.Span` *view* tracking (a borrow of the owner) is a follow-up;
+this slice covers the owner's own acquire / use / release lifecycle.
+
+Reference: dotnet/runtime#33767; [P-007](../../../docs/proposals/P-007-arraypool-span.md).

docs/proposals/P-007-arraypool-span.md

@@ -12,8 +12,16 @@
   emits an `overspan` fact and the core raises OWN025 `[resource: pooled buffer]` at the view —
   both when the view is used in an EXPRESSION (`Emit(buf.AsSpan())`) and when it is a local-decl
   INITIALIZER (`var copy = buf.AsSpan().ToArray();`, `Span<T> s = buf.AsSpan();`) (corpus
-  `arraypool-fullspan-overread`). POOL003 (double-return — flow already catches OWN003), a view
-  stored in a FIELD, and the `Array.Clear(buf, 0, buf.Length)` spelling of POOL005 next
+  `arraypool-fullspan-overread`) — and the **`.Length` view spelling** too (`buf.AsSpan(0, buf.Length)`
+  / `new Span<T>(buf, 0, buf.Length)`, where the oversized self-`.Length` is the bound; corpus
+  `arraypool-length-overread`). A *write*/wipe like `Array.Clear(buf, 0, buf.Length)` is deliberately
+  NOT flagged — it zeros the tail (a safe clear-before-`Return`) and exposes nothing; only a
+  read-capable VIEW is the over-read. **POOL003 (double-return → OWN003) is built** for ArrayPool
+  (try/finally + aliased-receiver, corpus `arraypool-double-return` / `arraypool-aliased-receiver`),
+  and **MemoryPool is now tracked** — a `MemoryPool<T>.Rent` `IMemoryOwner` is released by Dispose,
+  so its leak / double-dispose / use-after-dispose ride the same flow as POOL001/002/003 (corpus
+  `memorypool-double-dispose` → OWN003). A POOL005 view stored in a FIELD, and the
+  `IMemoryOwner.Memory.Span` view borrow, are next
 - **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release,
   OWN003 double-release, OWN008 release-while-borrowed), the buffer/borrow model
   in `spec/`, [P-001](P-001-csharp-extractor.md). See
@@ -43,9 +51,9 @@ The corpus already pins two real cases (`corpus/real-world/arraypool-double-retu
 |---------|---------|--------------|
 | **POOL001** rented not returned | `Rent(...)` with no matching `Return(buf)` in the same member | `OWN001` `[resource: pooled buffer]` ✅ |
 | **POOL002** view after return | a `Span`/`Memory` view used after the owner is `Return`ed | `OWN002` |
-| **POOL003** double return | `Return` reachable twice for the same buffer | `OWN003` |
+| **POOL003** double return | `Return`/`Dispose` reachable twice for the same buffer (ArrayPool *and* MemoryPool) | `OWN003` ✅ |
 | **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` |
-| **POOL005** clear/copy past length | a full-length view (`buf.AsSpan()`, no bound) reads/copies beyond the logical length of the rented region | `OWN025` `[resource: pooled buffer]` ✅ (view in an expression or initializer; `Array.Clear(buf, 0, buf.Length)` next) |
+| **POOL005** read/copy past length | a full-length **view** (`buf.AsSpan()`, no bound) **or** the `.Length` spelling (`buf.AsSpan(0, buf.Length)`) reads/copies beyond the logical length (a write/wipe like `Array.Clear(buf, 0, buf.Length)` is NOT flagged — it exposes nothing) | `OWN025` `[resource: pooled buffer]` ✅ (a view stored in a FIELD next) |
 
 Resource mapping:
 
@@ -97,5 +105,8 @@ Catching a real one of these is the milestone-4 success condition.
    the existing sensitive-buffer/clear-on-release check (OWN024)?
 3. How much of POOL004 (view escape) overlaps the existing OWN004/OWN015 escape
    rules — reuse, don't duplicate.
-4. `IMemoryOwner<T>` / `MemoryPool` `Dispose`-based release vs `ArrayPool`'s
-   explicit `Return` — one model with two release spellings?
+4. **(resolved)** `IMemoryOwner<T>` / `MemoryPool` `Dispose`-based release vs
+   `ArrayPool`'s explicit `Return` — yes, one flow model, two release spellings: a
+   `MemoryPool.Rent` owner is tracked as an IDisposable (released by `Dispose`,
+   arg-passing is an escape), an `ArrayPool.Rent` buffer by `Return` (arg-passing is
+   a borrow). Both feed the same acquire/use/release lattice → POOL001/002/003.