feat(extractor): --stats coverage + lock the lambda-handler event leak

.github/workflows/ci.yml

@@ -115,6 +115,8 @@ jobs:
         run: |
           dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \
             frontend/roslyn/samples/CustomerViewModel.cs \
+            frontend/roslyn/samples/LambdaHandlerViewModel.cs \
+            frontend/roslyn/samples/AliasedSourceViewModel.cs \
             frontend/roslyn/samples/OrdersViewModel.cs \
             frontend/roslyn/samples/TimerViewModel.cs \
             frontend/roslyn/samples/DisposableFieldViewModel.cs \
@@ -130,13 +132,33 @@ jobs:
         run: |
           out=$(python -m ownlang ownir "$RUNNER_TEMP/facts.json" || true)
           echo "$out"
-          echo "$out" | grep -q "CustomerViewModel.cs" \
-            || { echo "FAIL: expected the CustomerViewModel leak"; exit 1; }
           echo "$out" | grep -q "OWN001" \
             || { echo "FAIL: expected OWN001"; exit 1; }
+          # P-004 tiering: CustomerViewModel subscribes to an INJECTED bus (a ctor
+          # param of unknown lifetime). We cannot prove it outlives the view model,
+          # so the leak is reported at WARNING level (an honest "possible leak"),
+          # not a hard error — until lifetime/ownership modelling lands.
+          echo "$out" | grep -qE "CustomerViewModel\.cs:[0-9]+: warning: \[OWN001\]" \
+            || { echo "FAIL: expected CustomerViewModel as a WARNING (injected source)"; exit 1; }
+          echo "$out" | grep -q "injected dependency whose lifetime is unknown" \
+            || { echo "FAIL: expected the injected-source wording"; exit 1; }
           if echo "$out" | grep -q "OrdersViewModel.cs"; then
             echo "FAIL: disposed subscription wrongly reported"; exit 1
           fi
+          # a lambda handler has no stored delegate, so it can NEVER be `-=`'d — the
+          # finding says so. (Same injected source as Customer -> also a warning.)
+          echo "$out" | grep -qE "LambdaHandlerViewModel\.cs:[0-9]+: warning: \[OWN001\]" \
+            || { echo "FAIL: expected the lambda-handler subscription leak (warning)"; exit 1; }
+          echo "$out" | grep -q "inline lambda it has no '-=' handle" \
+            || { echo "FAIL: expected the lambda no-handle wording"; exit 1; }
+          # P-004 provenance: a local that ALIASES an injected source (var src =
+          # _bus) is NOT method-bounded — it must warn, not be silently dropped. A
+          # local the scope CONSTRUCTS (var owned = new Calc()) IS bounded -> silent.
+          echo "$out" | grep -qE "AliasedSourceViewModel\.cs:[0-9]+: warning: \[OWN001\]" \
+            || { echo "FAIL: aliased-injected local should warn, not be dropped"; exit 1; }
+          if echo "$out" | grep -q "owned.Changed"; then
+            echo "FAIL: a locally-constructed publisher must be dropped"; exit 1
+          fi
           # WPF002: the started, never-stopped timer leaks with a [resource: timer]
           # tag; the timer stopped in Dispose stays silent.
           echo "$out" | grep -q "TimerViewModel.cs" \
@@ -234,6 +256,30 @@ jobs:
             if echo "$out" | grep -q "'$ok'"; then echo "FAIL: silent/exempt case '$ok' was reported"; exit 1; fi
           done
           echo "OK: flow-sensitive OWN001/002/003 on real C# (path-sensitive, loops via while/foreach, never-vs-every-path wording, dispose-optional exempt, beyond flat)"
+      - name: Coverage summary (--stats)
+        run: |
+          # --stats prints a flow-locals coverage line to stderr and stamps the same
+          # counts into the facts JSON: of the methods with a disposable local, how
+          # many were flow-analysed vs honestly skipped (an unmodelled construct).
+          cov=$(dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \
+            frontend/roslyn/samples/FlowLocalsSample.cs --flow-locals --stats \
+            -o "$RUNNER_TEMP/stats.json" 2>&1 >/dev/null)
+          echo "$cov"
+          echo "$cov" | grep -qE '^coverage: [0-9]+/[0-9]+ methods .* flow-analysed' \
+            || { echo "FAIL: expected a --stats coverage line on stderr"; exit 1; }
+          # Parse the JSON (not a substring grep): assert the stats object exists,
+          # all three counters are numbers, and the invariant holds — every method
+          # with a disposable local is either flow-analysed or honestly skipped.
+          jq -e '.stats as $s
+            | ($s.methods_with_local | type == "number")
+              and ($s.methods_flow_analysed | type == "number")
+              and ($s.methods_skipped_unmodelled | type == "number")
+              and ($s.methods_flow_analysed + $s.methods_skipped_unmodelled
+                   == $s.methods_with_local)' \
+            "$RUNNER_TEMP/stats.json" >/dev/null \
+            || { echo "FAIL: stats object missing / non-numeric / invariant violated";
+                 cat "$RUNNER_TEMP/stats.json"; exit 1; }
+          echo "OK: --stats coverage on stderr + valid stats object (invariant holds)"
       - name: Escape-via-projection leak — GTM UnitOfWork (--flow-locals, P-016 B0b/B2)
         run: |
           # A real GTM leak the flat detector misses: a UnitOfWork (IDisposable) used
@@ -289,12 +335,18 @@ jobs:
             || { echo "FAIL: expected the relative path to the Customer leak"; exit 1; }
           echo "$out" | grep -q "title=OWN001" \
             || { echo "FAIL: expected the OWN001 title in the annotation"; exit 1; }
-      - name: MSBuild diagnostic format over the sample tree
+      - name: MSBuild diagnostic format over the sample tree (severity tiering)
         run: |
           out=$(scripts/own-check.sh --format msbuild -- frontend/roslyn/samples)
           echo "--- diagnostics ---"; echo "$out"; echo "-------------------"
-          echo "$out" | grep -qE "CustomerViewModel\.cs\([0-9]+\): error OWN001:" \
-            || { echo "FAIL: expected an MSBuild-format error line"; exit 1; }
+          # P-004 tiering at the default severity, both sides: an injected-source
+          # subscription (CustomerViewModel's `bus` is a ctor param of unknown
+          # lifetime) renders as a WARNING, while a provable leak — the started,
+          # never-stopped timer — stays an ERROR.
+          echo "$out" | grep -qE "CustomerViewModel\.cs\([0-9]+\): warning OWN001:" \
+            || { echo "FAIL: expected CustomerViewModel as a warning (injected source)"; exit 1; }
+          echo "$out" | grep -qE "TimerViewModel\.cs\([0-9]+\): error OWN001:" \
+            || { echo "FAIL: expected the timer leak to stay an error"; exit 1; }
       - name: --severity warning renders advisory diagnostics
         run: |
           out=$(scripts/own-check.sh --format msbuild --severity warning -- frontend/roslyn/samples)

docs/notes/subscription-leaks-and-profiles.md

@@ -0,0 +1,149 @@
+# Subscription leaks are a .NET concern, not a WPF one — codes vs. profiles
+
+Prompted by a good question: should `event += without -=` be a `WPFxxx` error?
+Short answer **no** — it is a general .NET lifetime/subscription bug, and the core
+already treats it that way (`OWN001` + `[resource: subscription token]`, never a
+"WPF" code). Recording the taxonomy so we don't re-open it, and so the *docs*
+stop reading as if this were WPF-only when the capability is .NET-wide.
+
+## What the core actually emits (we already did the right thing)
+
+`event += without -=` lowers to a resource and comes out as **`OWN001`** with a
+domain-neutral `[resource: kind]` tag — see the [README](../../README.md)
+"Бизнес-применение" section and [P-001](../proposals/P-001-csharp-extractor.md):
+
+```text
+case.own:16: error: [OWN001] '…' is owned but not released … [resource: subscription token]
+```
+
+The `[resource: kind]` tag is the **seam**: the WPF profile (and the Roslyn
+front-end) key off it without the core knowing a thing about WPF. That is already
+in the README ("шов, за который зацепится WPF-профиль, не зная про WPF в ядре").
+
+Crucially, the `WPF001..WPF005` in [P-004](../proposals/P-004-wpf-lifetime-profile.md)
+are **profile rule mnemonics, not diagnostic codes** — its own table maps each one
+to a core verdict:
+
+```text
+WPF001  source.Event += h, no matching -=        -> OWN001  [subscription token]
+WPF002  Timer Tick/Elapsed, no Stop()/ -=        -> OWN001  [timer]
+WPF003  owned IDisposable field, never Disposed  -> OWN001  [disposable field]
+WPF004  ignored Subscribe() IDisposable token    -> OWN001  [subscription token]
+WPF005  strong capture by a longer-lived source  -> OWN014  (region promotion)
+```
+
+So the core stays neutral; "WPF" is *recognition + lifetime context*, not the
+error itself. The critique is correct, and we mostly already shipped it.
+
+## The naming debt the critique correctly smells
+
+The capability is general. The *same* `source.Event += h` without `-=` leaks in
+**WinForms, Avalonia, MAUI, Unity, an ASP.NET singleton service, a console app
+with an event bus** — anywhere a publisher outlives its subscriber. The Rx flavour
+is `observable.Subscribe(x => …)` with the `IDisposable` token dropped. None of
+that is WPF.
+
+Yet P-001's subtitle ("the WPF leak spike"), P-004's `WPFxxx` rule names, and the
+README's "WPF lifetime-утечки" heading make a .NET-wide analysis *read* as
+WPF-only. That is naming a fire "kitchen thermodynamics." The fix is framing, not
+the core: **"subscription / lifetime analysis with a WPF profile,"** not "WPF leak
+analyzer."
+
+## Proposed code families (direction, not a now-rename)
+
+If/when the `[resource]` tag stops carrying enough and we want first-class codes:
+
+```text
+OWN   core ownership / borrow / release / lifetime promotion
+SUB   subscriptions / events / observer tokens
+TMR   timers
+DI    dependency-injection lifetimes
+POOL  ArrayPool / MemoryPool / Span storage
+EFF   effects / resources
+WPF   *truly* XAML-model retention (only the things below)
+```
+
+Today's profile rules would re-home cleanly: `WPF001 -> SUB001`,
+`WPF002 -> TMR001`, `WPF004 -> SUB004` (ignored token), `WPF003 -> IDisposable
+field (P-005)`, `WPF005 -> OWN014` (already neutral — it is lifetime promotion).
+
+`WPFxxx` is genuinely *earned* only where the diagnostic needs the XAML object
+model and cannot be a generic subscription/timer:
+
+```text
+DataContext retained after a View unloads
+Binding / CollectionView keeping its source alive
+ResourceDictionary / merged-dictionary retention
+DependencyProperty metadata callback capturing an instance
+Storyboard / animation / EventTrigger holding its target
+WeakEventManager should have been used for a long-lived source
+```
+
+## OwnIR stays domain-neutral; the profile only adds heuristics
+
+```text
+core facts (neutral — what the extractor emits):
+  acquire(subscription, loc)     release(subscription, loc)
+  owner(this, subscription)      handler(subscription, h)    captures(h, this)
+  source(subscription, publisher)
+  lifetime(this, ViewModel)      lifetime(publisher, App)     # when known
+
+wpf profile (heuristics layered on top — never inside the core):
+  class *ViewModel  /  : Window|UserControl|Page  -> lifetime ViewModel / UI
+  Application.Current  /  singleton service        -> lifetime App
+  Dispose / OnClosed / Unloaded                    -> cleanup regions
+  DispatcherTimer / WeakEventManager / …           -> WPF-specific sources
+```
+
+The same facts can later carry `profile = winforms | avalonia | maui | aspnet`
+without touching the checker. One core; many profiles. The seam already exists.
+
+## Severity follows what we can *prove* (the `OWN001` decision)
+
+We keep the code `OWN001`. The open behavioural question was: do we always shout
+`error` at a lambda handler? **No** — that would be "the analyzer named *молодец,
+нашёл C#*," which users mute faster than WPF leaks its first ViewModel. Without
+lifetime evidence, tier `OWN001`'s *severity* by what the source provably is:
+
+```text
+static event + capturing handler   -> error    process-lifetime: a provable leak
+field / ctor-param / property      -> warning  lifetime unknown — may leak if the
+                                               source outlives `this`; an inline
+                                               lambda has no handle to `-=` at all
+local publisher                    -> drop     dies with the scope (today a false
+                                               positive: `local` is not in the
+                                               self-owned set, so it leaks-by-mistake)
+this / constructed field           -> exempt   self-owned cycle, GC-collectable (P-004)
+```
+
+The punchline ties the two halves together: **the WPF profile is exactly the thing
+that turns that `warning` back into an `error`.** When the profile (or an explicit
+`lifetime` region) resolves the source to App-lifetime over a ViewModel subscriber,
+the hedge becomes the confident verdict the core *already* produces — **`OWN014`**
+(`App > ViewModel ⇒ promotion ⇒ leak`, see the README region example). "Warning
+without a profile, error with one" is not a cop-out: it is the honest contract, and
+the lifetime/region analysis is the upgrade path. Same mechanism, viewed twice.
+
+This also keeps us consistent with our own line — honest-skip (`--stats`, `OWN050`)
+and the oracle precision stance ([oracle.md](oracle.md): we ding Infer# for
+ownership-transfer false positives). Erroring on every lambda would be us doing the
+exact thing we flag the neighbours for.
+
+## What to actually change — and what not to
+
+- **Now (cheap, no code):** reframe the docs — P-001 subtitle, P-004 title and the
+  table's column header, the README heading, `ROADMAP` — from "WPF leak analyzer /
+  `WPFxxx` codes" to "subscription / lifetime analysis + a WPF *profile* (rule IDs)."
+  Keep emitting `OWN001`/`OWN014`; the `[resource: kind]` tag already names the
+  sub-domain.
+- **Later (only on demand):** mint `SUB`/`TMR` as first-class diagnostic codes *if*
+  the `[resource]` tag ever can't carry a distinction we need. Renaming shipped
+  behaviour costs goldens, `corpus/wpf/`, `tests/test_wpf.py` — and the codes users
+  see are already neutral, so there is no rush.
+- **Don't:** put any WPF knowledge into the core, or split `event += without -=` out
+  of `OWN001`. It *is* `OWN001`. WPF is a lens, not the lesson.
+
+**Verdict:** the core is already domain-neutral and correct. The work is (1) stop
+the *docs* over-claiming WPF, and (2) make `OWN001`'s severity honest about source
+lifetime, with the WPF/region profile as the evidence that escalates a hedge to a
+verdict.