docs: reconcile stale proposal/roadmap statuses with shipped code

docs/ROADMAP.md

@@ -232,16 +232,19 @@ own scan. Label them as estimates wherever they appear.
 
 | # | Track | Tier | Status |
 |---|-------|------|--------|
-| [P-001](proposals/P-001-csharp-extractor.md) | C# → OwnIR extractor (WPF leak spike) | P0 | in progress (v0 built) |
+| [P-001](proposals/P-001-csharp-extractor.md) | C# → OwnIR extractor (WPF leak spike) | P0 | in progress (well past v0: WPF001–005 + DI graph + pool + flow facts + semantic resolution) |
 | [P-002](proposals/P-002-verification-backend.md) | Verification backend (Boogie/Dafny) | horizon | draft |
 | [P-003](proposals/P-003-lifetime-visualization.md) | Lifetime visualization (RustOwl-style) | horizon | draft |
 | [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-005](proposals/P-005-idisposable-ownership.md) | `IDisposable` ownership profile | P0 | in progress (D1/D2 built via WPF003; D3/D4 path-sensitive via `--flow-locals`) |
 | [P-006](proposals/P-006-di-lifetimes.md) | DI lifetime / captive dependency | P0 | in progress (DI001–DI005 end-to-end: core + extractor) |
 | [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 |
 | [P-011](proposals/P-011-editor-tooling.md) | Editor tooling & syntax highlighting | side-track | draft |
-| [P-012](proposals/P-012-bug-corpus-mining.md) | Real-world bug corpus & mining | enabling | draft |
+| [P-012](proposals/P-012-bug-corpus-mining.md) | Real-world bug corpus & mining | enabling | in progress (corpus benchmark + real-world cases, CI-gated) |
 | [P-013](proposals/P-013-distribution-surface.md) | Distribution surface (CI Action + dotnet tool) | enabling | v0 built |
+| [P-014](proposals/P-014-semantic-resolution.md) | Project-local semantic resolution (`+=` event vs number) | P0 | in progress (Tier A shipped & default-on; Tier B deferred) |
+| [P-015](proposals/P-015-configuration-surface.md) | Configuration surface (check selection & severity) | P2 | draft (stub) |
+| [P-016](proposals/P-016-deep-fact-extraction.md) | Deep C# fact extraction (CFG + flow lowering) | P1 | in progress (B0a/B0b/B2/A1 via `--flow-locals`) |

docs/proposals/P-001-csharp-extractor.md

@@ -1,7 +1,13 @@
 # P-001 — C# → OwnIR extractor (the WPF leak spike)
 
-- **Status:** in progress — **v0 built** (`event += without -=`). Seam and v0
-  scope decided as recommended below.
+- **Status:** in progress — **well past v0.** The seam (Roslyn extractor → OwnIR → Python
+  core) is built and now extracts far more than the original `event += without -=` spike:
+  WPF001–005 (events, timers, `IDisposable` fields, ignored `Subscribe`, static-event region
+  escape → OWN014), the **DI registration + constructor graph** (DI001–DI005, P-006), the
+  **ArrayPool/Span** facts (POOL001–003 built; 004/005 first slices, P-007), **path-sensitive per-method flow** facts
+  (`--flow-locals`: acquire/use/release/loops/try, OWN001/002/003, P-016), and **project-local
+  semantic resolution** (`SemanticModel`-bound `+=`, OWN050 for unresolved types, P-014 Tier A).
+  All CI-validated end-to-end on the extractor samples.
 - **Depends on:** `spec/OwnCore.md`, `spec/Lifetimes.md` (the fact vocabulary)
 
 ## What is built (v0)

docs/proposals/P-005-idisposable-ownership.md

@@ -1,8 +1,13 @@
 # P-005 — `IDisposable` ownership profile
 
 - **Status:** in progress (P0 — the most down-to-earth resource module). **D1
-  (local never disposed)** built, plus **D2 (owned field never disposed)** via
-  WPF003 ([P-004](P-004-wpf-lifetime-profile.md)); D3/D4/D5 next.
+  (local never disposed)** built (path-sensitive under `--flow-locals`, P-016), plus
+  **D2 (owned field never disposed)** via WPF003 ([P-004](P-004-wpf-lifetime-profile.md)).
+  **D3 (double dispose → OWN003)** and **D4 (use-after-dispose → OWN002)** are also built —
+  via the `--flow-locals` per-method flow lattice, plus a field-mediated use-after-dispose pass
+  (a disposed field read in a live event handler). **D5 (ownership transfer through a callee)**
+  is a heuristic at the call boundary (bounded first-party `consume`/`borrow` contracts; no
+  cross-library model) and remains the main open frontier.
 - **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release,
   OWN003 double-release), [P-001](P-001-csharp-extractor.md) (the C# seam).
   Shares the resource core with [P-004](P-004-wpf-lifetime-profile.md).

docs/proposals/P-014-semantic-resolution.md

@@ -1,6 +1,14 @@
 # P-014 — Project-local semantic resolution for the C# extractor
 
-- **Status:** draft (P0 — the extractor is currently unusable on real desktop code)
+- **Status:** in progress (P0) — **Tier A shipped (T0–T6 done), default-on.** A `+=` is a
+  subscription only when the `SemanticModel` binds its LHS to an `IEventSymbol`, so arithmetic
+  (`sum += value`, for-loop steps) no longer leaks; an unresolved external event surfaces as the
+  advisory **OWN050** ("declaring type unresolved — leakage analysis skipped"), never a guessed
+  leak. One `CSharpCompilation` over the inputs with framework + `OWN_EXTRA_REF_DIRS` references;
+  the `--event-leaks`/`--no-event-leaks` gate defaults ON. CI-validated on the extractor sample.
+  **Tier B** (opt-in *full*-reference resolution via `MSBuildWorkspace` / a built `bin/**/*.dll`
+  reference set, to resolve third-party/DevExpress event types beyond the framework set) is
+  deferred (open question Q3), as are monorepo scoping (Q1) and a general check-selection surface (Q2).
 - **Depends on:**
   - [P-001](P-001-csharp-extractor.md) — the seam this deepens. P-001 defines the
     Roslyn-extractor → OwnIR → Python-core pipeline (P-001:71-77) *and* owns the

docs/proposals/README.md

@@ -22,22 +22,22 @@ proposal is marked `done` with a pointer.
 
 | # | Title | Status |
 |---|-------|--------|
-| [P-001](P-001-csharp-extractor.md) | C# → OwnIR extractor (the WPF leak spike) | in progress (v0 built) |
+| [P-001](P-001-csharp-extractor.md) | C# → OwnIR extractor (the WPF leak spike) | in progress (well past v0: WPF001–005 + DI + pool + flow + semantic resolution) |
 | [P-002](P-002-verification-backend.md) | Verification backend (Boogie/Dafny) | draft |
 | [P-003](P-003-lifetime-visualization.md) | Lifetime visualization (RustOwl-style) | draft |
-| [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-004](P-004-wpf-lifetime-profile.md) | WPF / UI lifetime leak profile | in progress (WPF001–005 built) |
+| [P-005](P-005-idisposable-ownership.md) | `IDisposable` ownership profile | in progress (D1/D2 built; D3/D4 via `--flow-locals`) |
+| [P-006](P-006-di-lifetimes.md) | DI lifetime / captive dependency | in progress (DI001–DI005 end-to-end) |
 | [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 |
 | [P-011](P-011-editor-tooling.md) | Editor tooling & syntax highlighting | draft |
-| [P-012](P-012-bug-corpus-mining.md) | Real-world bug corpus & mining | draft |
+| [P-012](P-012-bug-corpus-mining.md) | Real-world bug corpus & mining | in progress (corpus benchmark + real-world cases, CI-gated) |
 | [P-013](P-013-distribution-surface.md) | Distribution surface (how people run Own.NET) | v0 built (CI/Action + dotnet tool) |
-| [P-014](P-014-semantic-resolution.md) | Project-local semantic resolution (kills `+=` false positives) | draft (P0) |
+| [P-014](P-014-semantic-resolution.md) | Project-local semantic resolution (kills `+=` false positives) | in progress (Tier A shipped & default-on; Tier B deferred) |
 | [P-015](P-015-configuration-surface.md) | Configuration surface (check selection & per-category severity) | draft (stub) |
-| [P-016](P-016-deep-fact-extraction.md) | Deep C# fact extraction (CFG + flow lowering; loops) | draft |
+| [P-016](P-016-deep-fact-extraction.md) | Deep C# fact extraction (CFG + flow lowering; loops) | in progress (B0a/B0b/B2/A1 via `--flow-locals`) |
 
 > For priorities, milestones, the framing, and the design philosophy across all
 > of these, see the strategy hub: [`docs/ROADMAP.md`](../ROADMAP.md). P-004 … P-016