fix(extractor): #278 — a -= releases only in a proven, unguarded teardown context

corpus/real-world/screentogif-loaded-subscription/after.cs

@@ -1,6 +1,12 @@
 // Fix: subscribe with named handlers (so they have a `-=` handle) and detach them
-// in Window_Closing. The view-model no longer roots the window, and a repeated
-// Loaded no longer stacks duplicate handlers.
+// in Window_Closing, wired IN CODE (`Closing += Window_Closing`). The view-model
+// no longer roots the window, and a repeated Loaded no longer stacks duplicate
+// handlers.
+//
+// The code wiring is load-bearing (#278 follow-up): a `Window_Closing`-style NAME
+// alone proves nothing to the extractor (the XAML attach never reaches it, and a
+// bare name may be stale dead code), so the release is credited only because the
+// ctor provably attaches the handler to the window's own Closing event.
 using System;
 using System.Windows;
 
@@ -12,6 +18,7 @@ public VideoSource()
     {
         InitializeComponent();
         _viewModel = DataContext as VideoSourceViewModel;
+        Closing += Window_Closing;
     }
 
     private void Window_Loaded(object sender, RoutedEventArgs e)

corpus/real-world/screentogif-loaded-subscription/notes.md

@@ -38,3 +38,12 @@ produces the core's domain-neutral **OWN001** (the severity tiering lives in the
 extractor, above the core). As with the rest of the corpus, `case.own` is a hand
 reduction of the C# pattern, not verbatim extractor output; `before.cs` / `after.cs`
 are representative of the leak and its fix.
+
+**#278 follow-up.** `after.cs` wires `Closing += Window_Closing` in the ctor. The
+real ScreenToGif attaches the handler in XAML, which the extractor never sees — and
+since #278's follow-up a `Window_Closing`-style *name* alone is NOT a teardown
+context (a bare name may be stale dead code; the name-suffix exemption was a
+silent-FN hole). The corpus case therefore carries the wiring in code, which is the
+honest, provable form of the same fix; the name-only shape is pinned as a BAD case
+in `corpus/wpf/subscription-xaml-name-only-release`. A future XAML-aware slice can
+credit the XAML attach with actual evidence.

corpus/wpf/subscription-ambiguous-overload-wiring/after.cs

@@ -0,0 +1,29 @@
+// FIXED. Exactly ONE `Window_Closing` remains — the delegate-compatible one —
+// and it holds the `-=`. With the lifecycle event still unresolved, the name
+// is now UNAMBIGUOUS (a single same-named method in the immediate class), so
+// the fallback may credit it: whichever overload the delegate would pick, it
+// is this one.
+//
+// own-check MUST treat the subscription as released (silent); the unresolved
+// `Closing +=` itself stays the usual OWN050 advisory.
+using System;
+using System.ComponentModel;
+
+public partial class OrdersWindow : Window
+{
+    private readonly INotifyPropertyChanged _orders;   // injected, unknown lifetime
+
+    public OrdersWindow(INotifyPropertyChanged orders)
+    {
+        _orders = orders;
+        _orders.PropertyChanged += OnOrdersChanged;
+        Closing += Window_Closing;
+    }
+
+    private void Window_Closing(object sender, CancelEventArgs e)
+    {
+        _orders.PropertyChanged -= OnOrdersChanged;    // the one and only candidate
+    }
+
+    private void OnOrdersChanged(object sender, PropertyChangedEventArgs e) { /* ... */ }
+}

corpus/wpf/subscription-ambiguous-overload-wiring/before.cs

@@ -0,0 +1,41 @@
+// BUGGY (#278 follow-up 2 — the unresolved-overload fallback; hand-reduced
+// into case.own).
+//
+// The class wires `Closing += Window_Closing` on an UNRESOLVED lifecycle event
+// (the WPF `Window` base never resolves on a Linux runner without the
+// reference pack) and declares TWO `Window_Closing` overloads. The runtime
+// delegate attaches exactly ONE of them — chosen by the event's delegate
+// signature, which is precisely the information the extractor is missing. The
+// delegate-compatible overload detaches nothing; the `-=` sits in the OTHER,
+// never-attached overload.
+//
+// own-check MUST flag the subscription OWN001: an ambiguous name (2+ same-named
+// methods) may not ground the teardown, else a `-=` in the wrong overload
+// silently swallows the leak. (`Window` is deliberately not defined in-file —
+// the unresolved `Closing +=` itself surfaces as the usual OWN050 advisory.)
+using System;
+using System.ComponentModel;
+
+public partial class OrdersWindow : Window
+{
+    private readonly INotifyPropertyChanged _orders;   // injected, unknown lifetime
+
+    public OrdersWindow(INotifyPropertyChanged orders)
+    {
+        _orders = orders;
+        _orders.PropertyChanged += OnOrdersChanged;
+        Closing += Window_Closing;
+    }
+
+    private void Window_Closing(object sender, CancelEventArgs e)
+    {
+        // the delegate-compatible overload: detaches nothing
+    }
+
+    private void Window_Closing(object sender, EventArgs e)
+    {
+        _orders.PropertyChanged -= OnOrdersChanged;    // never attached at runtime
+    }
+
+    private void OnOrdersChanged(object sender, PropertyChangedEventArgs e) { /* ... */ }
+}

corpus/wpf/subscription-ambiguous-overload-wiring/case.own

@@ -0,0 +1,20 @@
+module WpfSubscriptionAmbiguousOverloadWiring
+
+// A subscription token: `+= handler` acquires the source<->listener edge; the
+// matching `-= handler` releases it. `kind` tags the resource so the generic
+// ownership finding carries a [resource: ...] note.
+resource Subscription {
+    acquire Subscribe
+    release Unsubscribe
+    kind "subscription token"
+}
+
+// The ctor subscribes; the wired teardown handler name is AMBIGUOUS (two
+// overloads, the event unresolved), and the `-=` sits in the overload the
+// delegate never attaches. The executed teardown path performs no release
+// => OWN001.
+fn OrdersWindow(orders: int) {
+    let sub = acquire Subscription(orders);
+    // the attached Window_Closing overload detaches nothing; the `-=` lives
+    // in the never-attached sibling overload (before.cs)
+}

corpus/wpf/subscription-ambiguous-overload-wiring/expected-diagnostics.txt

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

corpus/wpf/subscription-ambiguous-overload-wiring/notes.md

@@ -0,0 +1,40 @@
+# Subscription whose `-=` sits in the never-attached overload of an ambiguously-named wired handler (soundness FN)
+
+**Pattern (#278 follow-up 2 — the unresolved-overload fallback blocker).** The
+class wires `Closing += Window_Closing` where the lifecycle event does NOT
+resolve (WPF `Window` base on a Linux runner without the reference pack), and
+declares TWO `Window_Closing` overloads. A method group syntactically denotes
+its whole overload set, but the runtime delegate attaches exactly ONE member —
+selected by the event's delegate signature, which is precisely the information
+the extractor is missing. Here the delegate-compatible overload
+(`(object, CancelEventArgs)`) detaches nothing, and the `-=` sits in the other,
+never-attached overload.
+
+**The bug.** The previous slice's unresolved-event fallback added EVERY
+same-named own method to the teardown set, so the `-=` in the never-attached
+overload was silently credited as a release — the unresolved twin of the
+invocation-overload conflation pinned by
+`subscription-overload-conflated-cleanup`.
+
+**The fix.** When the handler binds no definite symbol, the name grounds a
+teardown ONLY if it is unambiguous — exactly one `IMethodSymbol` with that name
+in the immediate class. Zero or 2+ matches credit nothing and keep the honest
+warning. The symbol-resolved path is unchanged: when the event resolves, the
+delegate's exact target is credited even among overloads (pinned in the smoke
+matrix; `subscription-xaml-name-only-release/after.cs` keeps the resolved
+single-handler control). The prior fallback's `CandidateSymbols` crediting is
+gone with it — candidates of a failed method-group binding are the same
+ambiguous overload set by another name.
+
+**`before.cs`** → OWN001 (ambiguous, `-=` unproven). **`after.cs`** — the
+positive control: same unresolved event, exactly one `Window_Closing`, `-=`
+inside it → silent (whichever overload the delegate would pick, it is that
+one). Both keep the usual OWN050 advisory for the unresolved `Closing +=`
+itself.
+
+**What the checker says (`.own` reduction).** The scope acquires the token and
+the executed teardown path performs no release => **OWN001** with the
+subscription-token resource tag.
+
+**Regression guard.** `scripts/benchmark.py`: `before.cs` must be **caught**,
+`after.cs` must be **silent**.

corpus/wpf/subscription-finalizer-release/after.cs

@@ -0,0 +1,26 @@
+// FIXED. The release moved to Dispose — a deterministic teardown the OWNER
+// calls, which does not depend on the object first becoming unreachable. (A
+// finalizer may still exist for unmanaged state; it just cannot be the
+// subscription's release path.)
+//
+// own-check MUST treat this as released (silent).
+using System;
+using System.ComponentModel;
+
+public sealed class FinalizerDetachDocument : IDisposable
+{
+    private readonly INotifyPropertyChanged _properties;   // injected, unknown lifetime
+
+    public FinalizerDetachDocument(INotifyPropertyChanged properties)
+    {
+        _properties = properties;
+        _properties.PropertyChanged += OnPropertiesChanged;
+    }
+
+    public void Dispose()
+    {
+        _properties.PropertyChanged -= OnPropertiesChanged;   // deterministic teardown
+    }
+
+    private void OnPropertiesChanged(object sender, PropertyChangedEventArgs e) { /* ... */ }
+}

corpus/wpf/subscription-finalizer-release/before.cs

@@ -0,0 +1,32 @@
+// BUGGY (#278 follow-up, blocker 1; hand-reduced into case.own).
+//
+// The ctor subscribes to an injected publisher; the only matching `-=` sits in
+// the FINALIZER. That release can never run while it matters: the publisher's
+// delegate holds a strong reference to this object, so as long as the
+// subscription is live the subscriber is REACHABLE and the GC never finalizes
+// it. The `-=` exists precisely on the one path that the leak itself blocks.
+// (For a static/process-lived publisher the finalizer is simply never reached
+// for the life of the process — same argument, absolute.)
+//
+// own-check MUST flag this OWN001. Crediting the finalizer was a silent
+// false-negative path in the first #278 slice.
+using System.ComponentModel;
+
+public sealed class FinalizerDetachDocument
+{
+    private readonly INotifyPropertyChanged _properties;   // injected, unknown lifetime
+
+    public FinalizerDetachDocument(INotifyPropertyChanged properties)
+    {
+        _properties = properties;
+        _properties.PropertyChanged += OnPropertiesChanged;
+    }
+
+    ~FinalizerDetachDocument()
+    {
+        // unreachable while subscribed: the delegate keeps `this` alive
+        _properties.PropertyChanged -= OnPropertiesChanged;
+    }
+
+    private void OnPropertiesChanged(object sender, PropertyChangedEventArgs e) { /* ... */ }
+}

corpus/wpf/subscription-finalizer-release/case.own

@@ -0,0 +1,20 @@
+module WpfSubscriptionFinalizerRelease
+
+// A subscription token: `+= handler` acquires the source<->listener edge; the
+// matching `-= handler` releases it. `kind` tags the resource so the generic
+// ownership finding carries a [resource: ...] note.
+resource Subscription {
+    acquire Subscribe
+    release Unsubscribe
+    kind "subscription token"
+}
+
+// The ctor subscribes; the only `-=` lives in the finalizer. A finalizer runs
+// only after the object becomes unreachable — but the live subscription is
+// exactly what keeps it reachable, so the release path is blocked by the leak
+// it is supposed to fix. Modelled as the ctor scope with no release => OWN001.
+fn FinalizerDetachDocument(properties: int) {
+    let sub = acquire Subscription(properties);
+    // the finalizer `-=` is not modelled as a release: it cannot run while
+    // the subscription holds `this` reachable (before.cs)
+}

corpus/wpf/subscription-finalizer-release/expected-diagnostics.txt

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

corpus/wpf/subscription-finalizer-release/notes.md

@@ -0,0 +1,30 @@
+# Subscription whose only `-=` is in the finalizer (soundness FN)
+
+**Pattern (#278 follow-up, blocker 1).** Ctor `+=` to an injected publisher; the
+matching `-=` sits in `~FinalizerDetachDocument()`. The release is circularly
+unreachable: a finalizer runs only after the object becomes unreachable, but the
+publisher's delegate (the subscription) is precisely what keeps the subscriber
+reachable. While the subscription is live the finalizer cannot run; once the
+finalizer can run, there is nothing left to release. For a static/process-lived
+publisher the same argument is absolute — the finalizer is never reached for the
+life of the process.
+
+**The bug.** The first #278 slice treated `DestructorDeclarationSyntax` as a
+teardown context, so this shape was silently credited as released — a
+false-negative path of exactly the kind the slice existed to remove.
+
+**The fix.** A finalizer is explicitly NOT a teardown context for subscription
+release. `before.cs` keeps the honest OWN001; `after.cs` releases in `Dispose`
+(deterministic, owner-called, does not depend on unreachability) and is silent.
+
+**What the checker says (`.own` reduction).** The ctor scope acquires the token
+and no reachable teardown path releases it => **OWN001** with the
+subscription-token resource tag.
+
+**Regression guard.** `scripts/benchmark.py`: `before.cs` must be **caught**,
+`after.cs` must be **silent**.
+
+**Honesty / scope.** `case.own` carries the acquire/release logic; the
+finalizer-reachability reasoning lives in the extractor
+(`InTeardownContext`: `DestructorDeclarationSyntax => false`). Timer `.Stop()`
+release and the rest of the teardown model are unchanged by this case.

corpus/wpf/subscription-nonteardown-release/after.cs

@@ -0,0 +1,32 @@
+// FIXED. The detach moved into a recognised lifecycle teardown: a handler the
+// class wires to its OWN `Unloaded` event in the ctor. The platform raises
+// `Unloaded` when the view leaves the tree, so the `-=` provably runs at the
+// subscriber's end-of-life — this is the P-004 teardown shape as written
+// ("no matching `-=` in Dispose/OnClosed/Unloaded" is the finding; a `-=` IN
+// one of those contexts is the fix).
+//
+// own-check MUST treat this as released (silent) — the recognised lifecycle
+// teardown keeps its existing no-finding behaviour under #278.
+using System;
+using System.ComponentModel;
+
+public sealed class PriceListener
+{
+    private readonly INotifyPropertyChanged _prices;   // injected, unknown lifetime
+
+    public event EventHandler Unloaded;                // raised by the host when the view is torn down
+
+    public PriceListener(INotifyPropertyChanged prices)
+    {
+        _prices = prices;
+        _prices.PropertyChanged += OnPricesChanged;
+        Unloaded += OnViewUnloaded;
+    }
+
+    private void OnViewUnloaded(object sender, EventArgs e)
+    {
+        _prices.PropertyChanged -= OnPricesChanged;    // teardown context: the class's own Unloaded hook
+    }
+
+    private void OnPricesChanged(object sender, PropertyChangedEventArgs e) { /* ... */ }
+}

corpus/wpf/subscription-nonteardown-release/before.cs

@@ -0,0 +1,30 @@
+// BUGGY (issue #278, rule 3; hand-reduced into case.own).
+//
+// A listener subscribes to an injected publisher in its ctor. The only matching
+// `-=` is UNCONDITIONAL — but it sits in an arbitrary method (`StopListening`)
+// that is not a teardown: nothing here proves any owner ever calls it (in the
+// real SectorTS analog, an entire subsystem constructs these objects and never
+// calls the unregister method). The mere EXISTENCE of a `-=` is not evidence
+// that it RUNS.
+//
+// own-check MUST flag this OWN001. The old "any matching `-=` in the class =
+// released" model silenced it — the false negative this case pins.
+using System.ComponentModel;
+
+public sealed class PriceListener
+{
+    private readonly INotifyPropertyChanged _prices;   // injected, unknown lifetime
+
+    public PriceListener(INotifyPropertyChanged prices)
+    {
+        _prices = prices;
+        _prices.PropertyChanged += OnPricesChanged;
+    }
+
+    public void StopListening()
+    {
+        _prices.PropertyChanged -= OnPricesChanged;    // unconditional, but nobody has to call this
+    }
+
+    private void OnPricesChanged(object sender, PropertyChangedEventArgs e) { /* ... */ }
+}

corpus/wpf/subscription-nonteardown-release/case.own

@@ -0,0 +1,20 @@
+module WpfSubscriptionNonTeardownRelease
+
+// A subscription token: `+= handler` acquires the source<->listener edge; the
+// matching `-= handler` releases it. `kind` tags the resource so the generic
+// ownership finding carries a [resource: ...] note.
+resource Subscription {
+    acquire Subscribe
+    release Unsubscribe
+    kind "subscription token"
+}
+
+// The ctor subscribes; the only `-=` lives in an arbitrary non-teardown method
+// (`StopListening`) that no lifecycle path is proven to call. Modelled as the
+// ctor scope alone: the token is acquired and never released within any
+// teardown => OWN001. (The `-=`'s existence elsewhere is not modelled as a
+// release — that is exactly the #278 rule: existence is not execution.)
+fn PriceListener(prices: int) {
+    let sub = acquire Subscription(prices);
+    // no `release sub;` on any teardown path -> unreleased subscription (before.cs)
+}

corpus/wpf/subscription-nonteardown-release/expected-diagnostics.txt

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