feat(pool): POOL005 over-read of a pooled byte[] FIELD viewed full-length

.github/workflows/ci.yml

@@ -1106,7 +1106,9 @@ jobs:
         # — lowered to a synthetic acquire/release/use flow -> OWN002. That pass also covers POOLED owners:
         # an `IMemoryOwner<T>` field released in `Dispose()` and a `Memory` VIEW field of it (`_view =
         # _owner.Memory`) read in such a handler is the view-in-a-field dangle -> OWN002 (`pooled-view-after-
-        # dispose`). Remaining backlog: an ArrayPool `byte[]`-buffer-field view, a TWO-plus-hop indirect field
+        # dispose`). The POOL005 field pass now also catches a full-length view of an ArrayPool `byte[]`
+        # buffer FIELD read past its logical length -> OWN025 (`arraypool-field-fullspan-overread`).
+        # Remaining backlog: a full-length view STORED into another field, a TWO-plus-hop indirect field
         # use, and an injected-source region-escape. A drop below the floor is a regression.
-        run: python scripts/benchmark.py --min-recall 23
+        run: python scripts/benchmark.py --min-recall 24
 

corpus/real-world/arraypool-field-fullspan-overread/after.cs

@@ -0,0 +1,46 @@
+// AFTER (fixed). Every full-length view of a pooled field is BOUNDED to the logical
+// length — `_buf.AsSpan(0, _n)` and `_meta.AsSpan(0, _metaLen)` — so only the valid
+// payload bytes are read; the oversized `[len, Length)` tail is never touched. With
+// no unbounded view (and no `.Length`-spelled view) over either field — the
+// assignment-rented `_buf` or the initializer-rented `_meta` — the extractor emits
+// no `overspan` fact and the checker is silent.
+using System;
+using System.Buffers;
+
+sealed class FieldPoolFramer : IDisposable
+{
+    private byte[] _buf;
+    private int _n;
+
+    private const int MetaCap = 64;
+    private readonly byte[] _meta = ArrayPool<byte>.Shared.Rent(MetaCap);
+    private int _metaLen;
+
+    public void Capture(int n)
+    {
+        _n = n;
+        _buf = ArrayPool<byte>.Shared.Rent(n);
+        Fill(_buf, n);
+        _metaLen = 8;
+        Fill(_meta, _metaLen);
+    }
+
+    public byte[] Flush()
+    {
+        return _buf.AsSpan(0, _n).ToArray();   // bounded view: only the logical [0, n)
+    }
+
+    public byte[] FlushMeta()
+    {
+        return _meta.AsSpan(0, _metaLen).ToArray();   // bounded view: only the logical [0, _metaLen)
+    }
+
+    public void Dispose()
+    {
+        if (_buf is not null)                    // null until Capture; Return(null) would throw
+            ArrayPool<byte>.Shared.Return(_buf);
+        ArrayPool<byte>.Shared.Return(_meta);    // initializer-rented, never null
+    }
+
+    static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
+}

corpus/real-world/arraypool-field-fullspan-overread/before.cs

@@ -0,0 +1,58 @@
+// BEFORE (buggy). The FIELD twin of the ArrayPool "full-length view over-read"
+// bug (P-007 POOL005). A pooled array is rented into a FIELD — by assignment
+// (`_buf = ArrayPool<T>.Shared.Rent(n)`) OR a field initializer (`byte[] _meta =
+// ArrayPool<T>.Shared.Rent(MetaCap)`) — so the oversized buffer (`Length >= n`)
+// outlives the method that filled it. A LATER member then takes a FULL-length
+// view of the field and reads through it, so the `n` valid bytes are processed
+// together with the stale `[n, Length)` tail a *previous* renter left behind: a
+// wrong-length read and an information disclosure. Two view spellings are pinned:
+// the bare `_buf.AsSpan()` over the assignment-rented field, and the `.Length`
+// spelling `_meta.AsSpan(0, _meta.Length)` over the initializer-rented field. The
+// per-method flow pass only tracks LOCAL rents, so these field-backed over-reads
+// are out of its reach; the field pass catches them. The fix is a bounded view,
+// `_buf.AsSpan(0, _n)` (see after.cs). Representative of the pattern (a pooled
+// scratch field viewed full-length on flush/serialize), not verbatim from one PR.
+using System;
+using System.Buffers;
+
+sealed class FieldPoolFramer : IDisposable
+{
+    private byte[] _buf;
+    private int _n;
+
+    // a SECOND pooled buffer, rented in the FIELD INITIALIZER (not an assignment) and viewed full-length
+    // below via the `.Length` spelling — exercises the field-initializer rent + the IsFieldLengthOf branch.
+    private const int MetaCap = 64;
+    private readonly byte[] _meta = ArrayPool<byte>.Shared.Rent(MetaCap);   // Length >= MetaCap
+    private int _metaLen;
+
+    public void Capture(int n)
+    {
+        _n = n;
+        _buf = ArrayPool<byte>.Shared.Rent(n);   // pooled buffer stored in a FIELD (Length >= n)
+        Fill(_buf, n);                            // valid payload is _buf[0..n]
+        _metaLen = 8;
+        Fill(_meta, _metaLen);                    // valid payload is _meta[0.._metaLen]
+    }
+
+    public byte[] Flush()
+    {
+        return _buf.AsSpan().ToArray();   // <-- BUG: full-length view of the pooled FIELD,
+                                          //     n payload bytes + the stale [n, Length) tail
+    }
+
+    public byte[] FlushMeta()
+    {
+        return _meta.AsSpan(0, _meta.Length).ToArray();   // <-- BUG (`.Length` spelling): the WHOLE
+                                                          //     oversized array, past _metaLen
+    }
+
+    public void Dispose()
+    {
+        if (_buf is not null)                    // null until Capture; Return(null) would throw
+            ArrayPool<byte>.Shared.Return(_buf); // class-wide Return: no leak
+        ArrayPool<byte>.Shared.Return(_meta);    // initializer-rented, never null
+    }
+
+    static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
+}

corpus/real-world/arraypool-field-fullspan-overread/case.own

@@ -0,0 +1,22 @@
+// OwnLang model of the ArrayPool full-length view over-read on a FIELD-backed pooled
+// buffer. `acquire` == ArrayPool.Rent into a field (the array is OVERSIZED:
+// Length >= n), `release` == ArrayPool.Return (here in Dispose, class-wide).
+// `overspan buf` models a FULL-length view `_buf.AsSpan()` (no length bound) taken
+// in a LATER member and read through — it reaches past the logical length n into the
+// stale [n, Length) tail. The bounded form `_buf.AsSpan(0, _n)` takes no full view,
+// so the fixed code has no `overspan` and is silent. `.own` has no fields/members, so
+// this single-function reduction pins the same core verdict the field pass produces;
+// the field-vs-local distinction lives in before.cs/after.cs (checked end to end by
+// the dotnet benchmark). The checker trips OWN025 (POOL005) at the view; the buffer
+// is still returned, so there is no leak (OWN001) and no use-after-return (OWN002).
+module Corpus
+resource Buffer {
+  acquire rent
+  release give
+  kind "pooled buffer"
+}
+fn capture_then_flush(n: int) {
+  let buf = acquire Buffer(n);   // _buf = ArrayPool.Rent(n)   (Length >= n)
+  overspan buf;                  // _buf.AsSpan() in a later member — full view past n -> OWN025
+  release buf;                   // ArrayPool.Return (Dispose)
+}

corpus/real-world/arraypool-field-fullspan-overread/expected-diagnostics.txt

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

corpus/real-world/arraypool-field-fullspan-overread/notes.md

@@ -0,0 +1,48 @@
+# ArrayPool full-length view over-read on a FIELD-backed buffer (POOL005, field)
+
+**Pattern:** the FIELD twin of [`arraypool-fullspan-overread`](../arraypool-fullspan-overread/notes.md).
+A pooled array from `ArrayPool<T>.Shared.Rent(n)` is *oversized* — `Length >= n`, not
+exactly `n`. Here it is rented into a **field** (`_buf = ArrayPool<byte>.Shared.Rent(n)`)
+in one member and viewed full-length in a **later** member (`_buf.AsSpan()`,
+`this._buf.AsMemory()`, `new Span<T>(_buf)`, or the `.Length` spelling
+`_buf.AsSpan(0, _buf.Length)`). Reading or copying through that unbounded view
+processes the `n` valid bytes **plus** the stale `[n, Length)` tail a *previous*
+renter left behind — a correctness bug (wrong length) and an information disclosure.
+The fix is a bounded view: `_buf.AsSpan(0, _n)`.
+
+**Why a separate case.** The path-sensitive flow detector only tracks pooled buffers
+held in **locals**, so a field-backed rent — rented in one member, viewed in another —
+is out of its reach. The extractor's POOL005 **field pass** closes that gap: it
+collects the fields a class `Rent`s — by **assignment** (`_buf = ArrayPool.Rent(n)`,
+target resolved through the `this`/bare `ThisFieldName` shape so `other._buf` never
+seeds it) **and** by **field initializer** (`byte[] _meta = ArrayPool.Rent(MetaCap)`),
+the rent recognised by the shared `IsPoolRent` so an aliased pool receiver binds and a
+non-pool `.Rent` does not — and for each member that takes a full-length view of such
+a field (the over-read recognised by the same resolved `System.MemoryExtensions` /
+`System.Span<T>` BCL symbols as the local path) emits a synthetic
+`acquire`/`overspan`/`release` flow so the core raises **OWN025** at the view — no new
+diagnostic, the same synthetic-flow trick the field use-after-dispose and MemoryPool
+slices use. The scan is scoped to the class's **own (direct) members** — a nested
+type is analysed by its own pass, so its rents/views are never mixed into the outer
+class's flow. This case pins both view spellings: the bare `_buf.AsSpan()` over the
+assignment-rented field and the `.Length` spelling `_meta.AsSpan(0, _meta.Length)`
+over the initializer-rented field. A *write*/wipe (`Array.Clear(_buf, 0, _buf.Length)`)
+is not a view, so it is deliberately **not** flagged — only a read-capable VIEW is the
+over-read.
+
+**What the checker says:** OWN025 `[resource: pooled buffer]` at the view. The buffer
+is still `Return`ed (in `Dispose`, found class-wide by the POOL001 field pass), so
+there is no OWN001 leak and no OWN002 use-after-return; the only finding is the
+over-read itself.
+
+**Honesty / scope.** `case.own` is a faithful hand reduction — `.own` has no
+fields/members, so it pins the *core* OWN025 verdict the field pass produces, while
+the field-vs-local distinction lives in `before.cs` / `after.cs` (scanned end to end
+by the dotnet `corpus-benchmark` CI job). `before.cs` / `after.cs` are representative
+of the bug and its fix, not a verbatim PR diff. v0 of the field pass fires on the
+*first* full-length view of each pooled field per member (a read site); a full-length
+view of a pooled field **stored into another field** and only read elsewhere is a
+deeper alias-tracking frontier, left honest.
+
+Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target
+AiDotNet.Tensors pooled-buffer over-clear/over-read.

docs/ROADMAP.md

@@ -100,7 +100,8 @@ architectural strictness, and the borrow-checker showcase):
 4. `DI001` — singleton captures a scoped dependency ✅ (core check + C#
    registration-graph extractor built; end-to-end on real C#)
 5. `POOL001` — `ArrayPool` buffer `Rent`ed but never `Return`ed ✅
-   (`POOL002` `Span`/view used after `Return` next)
+   (`POOL002` `Span`/view used after `Return` ✅; `POOL003` double-return,
+   `POOL005` full-length over-read built too — see P-007)
 
 ### Milestones
 
@@ -151,6 +152,12 @@ architectural strictness, and the borrow-checker showcase):
    root-`GetService` form of DI003, and the consuming-constructor anchor.
 4. **Pool/Span** — `Rent`/`Return`, borrowed views, return-invalidates-views,
    known-bug replay corpus (P-007). The borrow checker on stage at full height.
+   ◑ *In progress* — POOL001 (leak), POOL002 (view-after-return → OWN002),
+   POOL003 (double-return/dispose, ArrayPool *and* MemoryPool) built end to end;
+   POOL004 (view escape) and POOL005 (full-length over-read, local **and** pooled
+   `byte[]` FIELD) first slices built. Remaining: a POOL005 view stored INTO another
+   field, deeper POOL004 escape, and the real-world replay targets (dotnet/runtime,
+   Nethermind, AiDotNet.Tensors).
 5. **Effects** — `pure` / `use !Db` / `use !Log` / `use Clock`, layer policies
    (P-008). The architectural X-ray — landed *after* the leak checkers prove value.
 
@@ -219,7 +226,7 @@ own scan. Label them as estimates wherever they appear.
 | [P-004](proposals/P-004-wpf-lifetime-profile.md) | WPF / UI lifetime leak profile | P0 | in progress (WPF001–005 built) |
 | [P-005](proposals/P-005-idisposable-ownership.md) | `IDisposable` ownership profile | P0 | draft |
 | [P-006](proposals/P-006-di-lifetimes.md) | DI lifetime / captive dependency | P0 | in progress (DI001 end-to-end: core + extractor) |
-| [P-007](proposals/P-007-arraypool-span.md) | ArrayPool / Span borrow-view | P1 | draft |
+| [P-007](proposals/P-007-arraypool-span.md) | ArrayPool / Span borrow-view | P1 | in progress (POOL001–003 built; 004/005 first slices) |
 | [P-008](proposals/P-008-effects-and-resources.md) | Effects & resources (`Own.Effects`) | P1/P2 | draft |
 | [P-009](proposals/P-009-nogc-regions.md) | No-GC / allocation-free regions | horizon | draft |
 | [P-010](proposals/P-010-type-disciplines.md) | Richer type disciplines (`Own.Types`) | P2/horizon | draft |

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

@@ -26,7 +26,14 @@
   owner.Memory;` — which dangles after the implicit scope-exit dispose — is caught too:
   the flow desugars a tracked `using IMemoryOwner` declaration to `acquire; try { rest }
   finally { release }`, so the returned view is read after the release (**POOL004 → OWN002**;
-  corpus `memorypool-using-view-escape`). A POOL005 view stored in a FIELD is next
+  corpus `memorypool-using-view-escape`). **POOL005 now also covers a pooled `byte[]` FIELD** — a
+  buffer `Rent`ed into a field (`_buf = ArrayPool<T>.Shared.Rent(n)`) and viewed full-length in a
+  LATER member (`_buf.AsSpan()` / `this._buf.AsMemory()` / `new Span<T>(_buf)` / the `.Length`
+  spelling) over-reads the oversized `[n, Length)` tail; the per-method flow pass only tracks LOCAL
+  rents, so a class-level field pass collects the pooled fields (shared `IsPoolRent`) and emits a
+  synthetic `acquire`/`overspan`/`release` flow at the view → OWN025 (corpus
+  `arraypool-field-fullspan-overread`). A full-length view STORED into another field (read only
+  elsewhere) is the deeper alias-tracking frontier, left 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
@@ -58,7 +65,7 @@ The corpus already pins two real cases (`corpus/real-world/arraypool-double-retu
 | **POOL002** view after return | a `Span`/`Memory` view used after the owner is `Return`ed | `OWN002` |
 | **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** 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) |
+| **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]` ✅ (local **and** pooled `byte[]` FIELD; a view stored-into-a-field next) |
 
 Resource mapping:
 

docs/proposals/README.md

@@ -28,7 +28,7 @@ proposal is marked `done` with a pointer.
 | [P-004](P-004-wpf-lifetime-profile.md) | WPF / UI lifetime leak profile | draft |
 | [P-005](P-005-idisposable-ownership.md) | `IDisposable` ownership profile | draft |
 | [P-006](P-006-di-lifetimes.md) | DI lifetime / captive dependency | draft |
-| [P-007](P-007-arraypool-span.md) | ArrayPool / Span borrow-view | draft |
+| [P-007](P-007-arraypool-span.md) | ArrayPool / Span borrow-view | in progress (POOL001–003 built; 004/005 first slices) |
 | [P-008](P-008-effects-and-resources.md) | Effects & resources (`Own.Effects`) | draft |
 | [P-009](P-009-nogc-regions.md) | No-GC / allocation-free regions | draft |
 | [P-010](P-010-type-disciplines.md) | Richer type disciplines (`Own.Types`) | draft |