corpus(wpf): a -= that exists is not a -= that runs — regression guard for #278

corpus/wpf/unsubscribe-behind-a-flag/after.cs

@@ -0,0 +1,60 @@
+// FIXED. The release is unconditional and in a teardown.
+//
+// Two things changed, and both matter:
+//
+//   1. the `-=` moved into `Dispose()` — a teardown context, which is what P-001/P-004 require;
+//   2. the flag no longer guards it. `UnregisterChildren` still exists for the callers that only
+//      wanted the child rows detached, but it can no longer be mistaken for a full teardown, and
+//      it cannot silently skip the static detach.
+//
+// own-check MUST treat this as released (silent). The point of the pair is that `before.cs` and
+// `after.cs` differ ONLY in whether the release is provably reached — the `+=` and the `-=` name
+// the same (receiver, handler) pair in both files. A model that keys on the mere existence of a
+// matching `-=` cannot tell these two apart, which is exactly the soundness gap this case pins.
+using System;
+using System.ComponentModel;
+
+public static class AppSettings
+{
+    public static readonly NotifyingOptions Options = new NotifyingOptions();
+}
+
+public class NotifyingOptions : INotifyPropertyChanged
+{
+    public event PropertyChangedEventHandler PropertyChanged;
+}
+
+public sealed class Document : IDisposable
+{
+    public Document()
+    {
+        AppSettings.Options.PropertyChanged += new PropertyChangedEventHandler(OnOptionsChanged);
+    }
+
+    public void Dispose()
+    {
+        // Unconditional, in a teardown. This is the one the subscription is paired with.
+        AppSettings.Options.PropertyChanged -= OnOptionsChanged;
+        UnregisterChildren();
+    }
+
+    // Narrowed and honestly named: it detaches the child rows, and nothing else. It can no longer
+    // be handed a flag that quietly turns it into a no-op for the static subscription.
+    public void UnregisterChildren()
+    {
+        // ... detach the child rows only ...
+    }
+
+    private void OnOptionsChanged(object sender, PropertyChangedEventArgs e) { /* ... */ }
+}
+
+public sealed class ImportService
+{
+    public void Import()
+    {
+        using (var doc = new Document())
+        {
+            // ... map / import ...
+        }   // Dispose() detaches it from the static publisher
+    }
+}

corpus/wpf/unsubscribe-behind-a-flag/before.cs

@@ -0,0 +1,62 @@
+// BUGGY. A `-=` that exists is not a `-=` that runs.
+//
+// The document subscribes to a STATIC event in its constructor. A matching `-=` does exist —
+// so own-check's release model ("any matching `-=` in the class releases it") falls silent —
+// but it is unreachable in practice on two independent counts:
+//
+//   1. it lives in `UnregisterEventHandlers`, which is not a teardown (`Dispose`/`OnClosed`/
+//      `Unloaded`); P-001 and P-004 both specify the release must be *in* a teardown, and the
+//      extractor is looser than its own spec;
+//   2. even when that method IS called, the `-=` sits behind `if (!unregOnlyChildren)`, and the
+//      calling code passes `true`.
+//
+// The publisher is static, so the handler pins the whole document graph for the life of the
+// process. Reduced from SectorTS `BrokerDataClasses/GTD.cs:5192` (subscribe) / `:5259`
+// (the flag-guarded release); heap-proven — 66% of the heap still reachable from the GC roots
+// after 31 documents, retention path
+// [PinnedHandle] -> static KernelProperty -> GBProperty -> PropertyChangedEventHandler -> GTD.
+using System.ComponentModel;
+
+// The app-lifetime settings object. Static => lives for the whole process.
+public static class AppSettings
+{
+    public static readonly NotifyingOptions Options = new NotifyingOptions();
+}
+
+public class NotifyingOptions : INotifyPropertyChanged
+{
+    public event PropertyChangedEventHandler PropertyChanged;
+}
+
+public sealed class Document
+{
+    public Document()
+    {
+        // Subscribed to a STATIC publisher. Nothing detaches this unless somebody calls
+        // UnregisterEventHandlers(false) — and nobody does. -> OWN001
+        AppSettings.Options.PropertyChanged += new PropertyChangedEventHandler(OnOptionsChanged);
+    }
+
+    // NOT a teardown, and the release is guarded away by the parameter every caller passes.
+    public void UnregisterEventHandlers(bool unregOnlyChildren = false)
+    {
+        if (!unregOnlyChildren)
+        {
+            AppSettings.Options.PropertyChanged -= OnOptionsChanged;   // the `-=` that never runs
+        }
+
+        // ... detach the child rows only ...
+    }
+
+    private void OnOptionsChanged(object sender, PropertyChangedEventArgs e) { /* ... */ }
+}
+
+public sealed class ImportService
+{
+    public Document Import()
+    {
+        var doc = new Document();
+        doc.UnregisterEventHandlers(true);   // true => the static `-=` above is skipped
+        return doc;
+    }
+}

corpus/wpf/unsubscribe-behind-a-flag/case.own

@@ -0,0 +1,26 @@
+// OwnLang model of SectorTS `BrokerDataClasses/GTD.cs` — a document that subscribes to a STATIC
+// publisher in its constructor (`:5192`) and whose `-=` lives behind a parameter, in a method that
+// is not a teardown (`UnregisterEventHandlers(bool UnregOnlyGoodys)`, `:5259`). Callers pass `true`;
+// one whole subsystem (DocCloud) never calls it at all.
+//
+// `acquire` == `AppSettings.Options.PropertyChanged += h`, `release` == the matching `-=`.
+// The flag is modelled as the branch that returns before the release — the path that skips cleanup —
+// so the core flags the un-released subscription as OWN001.
+//
+// NOTE what this reduction proves: **the core already gets this right.** Give it a release that is
+// not reached on every path and it says so. The bug is upstream, in the extractor's release-matching,
+// which emits `released: true` from the mere *existence* of a matching `-=` in the class
+// (`OwnSharp.Extractor/Program.cs:13`) and never asks whether it runs. See notes.md and #278.
+module Corpus
+resource Subscription {
+  acquire Subscribe
+  release Dispose
+  kind "subscription token"
+}
+fn Document(options: int, unregOnlyChildren: int) {
+  let sub = acquire Subscription(options);   // ctor: `+=` on the process-wide static publisher
+  if (unregOnlyChildren) {
+    return;                                   // caller passed `true` -> the static `-=` is skipped
+  }
+  release sub;                                // the `-=` only a caller passing `false` ever reaches
+}

corpus/wpf/unsubscribe-behind-a-flag/expected-diagnostics.txt

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

corpus/wpf/unsubscribe-behind-a-flag/notes.md

@@ -0,0 +1,77 @@
+# Unsubscribe behind a flag, in a method nobody calls (release-reachability FN)
+
+> **This case is RED today.** `before.cs` is a real, heap-proven leak and own-check is **silent** on it.
+> It is a regression guard for #278, not a passing test. It goes green when release-matching stops
+> concluding "released" from the mere *existence* of a `-=`.
+
+**Pattern.** A document subscribes to a **static** publisher in its constructor. A matching `-=` does
+exist in the class — so the current model pairs them and says nothing — but it never runs:
+
+```csharp
+public Document()
+{
+    AppSettings.Options.PropertyChanged += new PropertyChangedEventHandler(OnOptionsChanged);  // static publisher
+}
+
+public void UnregisterEventHandlers(bool unregOnlyChildren = false)   // NOT a teardown
+{
+    if (!unregOnlyChildren)                                            // callers pass true
+        AppSettings.Options.PropertyChanged -= OnOptionsChanged;       // the `-=` that never runs
+}
+```
+
+Three independent reasons the release is unreachable, any one of which is enough:
+
+1. `UnregisterEventHandlers` is **not a teardown** — not `Dispose`, `OnClosed` or `Unloaded`.
+   `docs/proposals/P-001-csharp-extractor.md:51` and `P-004-wpf-lifetime-profile.md:33` both specify the
+   release must be *in* one of those. The extractor is looser than its own spec
+   (`OwnSharp.Extractor/Program.cs:13`: *"released by a matching `-=` **in the class**"*).
+2. The `-=` sits behind a **parameter guard**, and the calling code passes `true`.
+3. Whole subsystems **never call the method at all**.
+
+**Why it matters.** The publisher is static, so the handler pins the subscriber for the life of the
+process — the strongest leak tier P-004 defines, and the one the analyzer is supposed to call a *provable*
+leak rather than a possible one.
+
+**Provenance.** Reduced from SectorTS `BrokerDataClasses/GTD.cs:5192` (subscribe to the static
+`AppData.Properties.GBProperty`) and `:5259` (`UnregisterEventHandlers(bool UnregOnlyGoodys)`).
+`Service/GTDService.cs` passes `true` at five sites; `BrokerDataClasses/DocCloud/**` — including eight
+AutoMapper `.ConstructUsing(x => new GTD(null, null))` profiles that build a document per mapping —
+never calls it at all.
+
+Proven at runtime with a ClrMD root walk, after **31 documents**:
+
+```
+on the heap          : 1 685 951 objects   223 MB
+REACHABLE from roots : 1 569 072 objects   148 MB
+>>> 66.3% of the heap is genuinely RETAINED
+
+[PinnedHandle] System.Object[]
+  KernelProperty                 <- AppData.Properties (static)
+    GBProperty
+      PropertyChangedEventHandler
+        System.Object[]           <- the delegate's invocation list
+          PropertyChangedEventHandler
+            GTD                   <- the whole document graph
+```
+
+Detaching after each document (`UnregisterEventHandlers(false)`) makes the process memory-flat —
+peak RSS 2.71 GB → 0.61 GB on the same 389 documents, **byte-identical output** — which confirms the
+diagnosis rather than merely being consistent with it.
+
+**Relation to the known gap.** `corpus/wpf/subscription-explicit-delegate-release/notes.md:28-41`
+already records that the release model is not flow-sensitive ("*it treats any matching `-=` in the class
+as releasing the subscription … that soundness gap is pre-existing*", Codex P2 on #163). That note scoped
+the gap to a **rebinding setter** and deferred it. This case shows the surface is much wider — a
+parameter guard, a non-teardown method, and an uncalled method are all ordinary code — and gives the gap
+its first real, heap-proven instance.
+
+**Regression guard.** `scripts/benchmark.py` runs the real C# through the extractor + core:
+
+* `before.cs` must be **caught** (OWN001) — it is a genuine leak. *Currently it is not: this is the bug.*
+* `after.cs` must be **silent** — the release is unconditional and in `Dispose`. It must stay silent
+  after the fix, or the fix has simply traded a false negative for a false positive.
+
+The pair differs **only** in whether the release is provably reached; the `+=` and the `-=` name the same
+`(receiver, handler)` in both. That is deliberate: a model that keys on the existence of a matching `-=`
+cannot tell these two files apart.

tests/fixtures/cfg_parity.json

@@ -241,6 +241,12 @@
       "cfg": "{\n  \"functions\": [\n    {\n      \"blocks\": [\n        {\n          \"id\": 0,\n          \"instrs\": [],\n          \"label\": \"entry\",\n          \"succ\": []\n        }\n      ],\n      \"entry\": 0,\n      \"has_return_type\": false,\n      \"name\": \"GraphicsConfigurationDialog\",\n      \"params\": [\n        0\n      ],\n      \"symbols\": [\n        {\n          \"borrow_is_mut\": null,\n          \"buffer\": null,\n          \"def_line\": 20,\n          \"is_param_borrow\": false,\n          \"kind\": \"plain\",\n          \"name\": \"systemEvents\",\n          \"origin\": \"systemEvents#20\",\n          \"resource_kind\": null,\n          \"type_name\": \"SystemEvents\"\n        }\n      ]\n    }\n  ],\n  \"ownlang_cfg_version\": 0\n}",
       "diags": []
     },
+    {
+      "name": "corpus/wpf/unsubscribe-behind-a-flag/case.own",
+      "source": "// OwnLang model of SectorTS `BrokerDataClasses/GTD.cs` — a document that subscribes to a STATIC\n// publisher in its constructor (`:5192`) and whose `-=` lives behind a parameter, in a method that\n// is not a teardown (`UnregisterEventHandlers(bool UnregOnlyGoodys)`, `:5259`). Callers pass `true`;\n// one whole subsystem (DocCloud) never calls it at all.\n//\n// `acquire` == `AppSettings.Options.PropertyChanged += h`, `release` == the matching `-=`.\n// The flag is modelled as the branch that returns before the release — the path that skips cleanup —\n// so the core flags the un-released subscription as OWN001.\n//\n// NOTE what this reduction proves: **the core already gets this right.** Give it a release that is\n// not reached on every path and it says so. The bug is upstream, in the extractor's release-matching,\n// which emits `released: true` from the mere *existence* of a matching `-=` in the class\n// (`OwnSharp.Extractor/Program.cs:13`) and never asks whether it runs. See notes.md and #278.\nmodule Corpus\nresource Subscription {\n  acquire Subscribe\n  release Dispose\n  kind \"subscription token\"\n}\nfn Document(options: int, unregOnlyChildren: int) {\n  let sub = acquire Subscription(options);   // ctor: `+=` on the process-wide static publisher\n  if (unregOnlyChildren) {\n    return;                                   // caller passed `true` -> the static `-=` is skipped\n  }\n  release sub;                                // the `-=` only a caller passing `false` ever reaches\n}\n",
+      "cfg": "{\n  \"functions\": [\n    {\n      \"blocks\": [\n        {\n          \"id\": 0,\n          \"instrs\": [\n            {\n              \"line\": 21,\n              \"op\": \"acquire\",\n              \"resource\": \"Subscription\",\n              \"sym\": 2\n            }\n          ],\n          \"label\": \"entry\",\n          \"succ\": [\n            1,\n            2\n          ]\n        },\n        {\n          \"id\": 1,\n          \"instrs\": [\n            {\n              \"line\": 23,\n              \"op\": \"return\",\n              \"sym\": null\n            }\n          ],\n          \"label\": \"then\",\n          \"succ\": []\n        },\n        {\n          \"id\": 2,\n          \"instrs\": [],\n          \"label\": \"else\",\n          \"succ\": [\n            3\n          ]\n        },\n        {\n          \"id\": 3,\n          \"instrs\": [\n            {\n              \"line\": 25,\n              \"op\": \"release\",\n              \"sym\": 2\n            }\n          ],\n          \"label\": \"merge\",\n          \"succ\": []\n        }\n      ],\n      \"entry\": 0,\n      \"has_return_type\": false,\n      \"name\": \"Document\",\n      \"params\": [\n        0,\n        1\n      ],\n      \"symbols\": [\n        {\n          \"borrow_is_mut\": null,\n          \"buffer\": null,\n          \"def_line\": 20,\n          \"is_param_borrow\": false,\n          \"kind\": \"plain\",\n          \"name\": \"options\",\n          \"origin\": \"options#20\",\n          \"resource_kind\": null,\n          \"type_name\": \"int\"\n        },\n        {\n          \"borrow_is_mut\": null,\n          \"buffer\": null,\n          \"def_line\": 20,\n          \"is_param_borrow\": false,\n          \"kind\": \"plain\",\n          \"name\": \"unregOnlyChildren\",\n          \"origin\": \"unregOnlyChildren#20\",\n          \"resource_kind\": null,\n          \"type_name\": \"int\"\n        },\n        {\n          \"borrow_is_mut\": null,\n          \"buffer\": null,\n          \"def_line\": 21,\n          \"is_param_borrow\": false,\n          \"kind\": \"owned\",\n          \"name\": \"sub\",\n          \"origin\": \"sub#21\",\n          \"resource_kind\": \"subscription token\",\n          \"type_name\": \"Subscription\"\n        }\n      ]\n    }\n  ],\n  \"ownlang_cfg_version\": 0\n}",
+      "diags": []
+    },
     {
       "name": "corpus/wpf/viewmodel-escapes-to-app/case.own",
       "source": "module WpfRegionEscape\n\n// Lifetime regions: a Window-lived ViewModel must not outlive its window, and\n// the App-lived event bus outlives everything.\nlifetime App;\nlifetime Window < App;\nlifetime ViewModel < Window;\n\n// The ViewModel (ViewModel-lived) strongly subscribes itself to the App-lived\n// bus. Because App strictly outlives ViewModel, the subscription promotes the\n// VM to App lifetime -> it can never die while the app runs => OWN014. This is\n// the region-escape theorem: the *ordering* is what makes it a leak (subscribing\n// to a same/shorter-lived source would be fine).\nfn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel {\n    subscribe self to bus;\n}\n",

tests/fixtures/diag_parity.json

@@ -405,6 +405,16 @@
         ]
       ]
     },
+    {
+      "name": "corpus/wpf/unsubscribe-behind-a-flag/case.own",
+      "source": "// OwnLang model of SectorTS `BrokerDataClasses/GTD.cs` — a document that subscribes to a STATIC\n// publisher in its constructor (`:5192`) and whose `-=` lives behind a parameter, in a method that\n// is not a teardown (`UnregisterEventHandlers(bool UnregOnlyGoodys)`, `:5259`). Callers pass `true`;\n// one whole subsystem (DocCloud) never calls it at all.\n//\n// `acquire` == `AppSettings.Options.PropertyChanged += h`, `release` == the matching `-=`.\n// The flag is modelled as the branch that returns before the release — the path that skips cleanup —\n// so the core flags the un-released subscription as OWN001.\n//\n// NOTE what this reduction proves: **the core already gets this right.** Give it a release that is\n// not reached on every path and it says so. The bug is upstream, in the extractor's release-matching,\n// which emits `released: true` from the mere *existence* of a matching `-=` in the class\n// (`OwnSharp.Extractor/Program.cs:13`) and never asks whether it runs. See notes.md and #278.\nmodule Corpus\nresource Subscription {\n  acquire Subscribe\n  release Dispose\n  kind \"subscription token\"\n}\nfn Document(options: int, unregOnlyChildren: int) {\n  let sub = acquire Subscription(options);   // ctor: `+=` on the process-wide static publisher\n  if (unregOnlyChildren) {\n    return;                                   // caller passed `true` -> the static `-=` is skipped\n  }\n  release sub;                                // the `-=` only a caller passing `false` ever reaches\n}\n",
+      "diags": [
+        [
+          23,
+          "OWN001"
+        ]
+      ]
+    },
     {
       "name": "corpus/wpf/viewmodel-escapes-to-app/case.own",
       "source": "module WpfRegionEscape\n\n// Lifetime regions: a Window-lived ViewModel must not outlive its window, and\n// the App-lived event bus outlives everything.\nlifetime App;\nlifetime Window < App;\nlifetime ViewModel < Window;\n\n// The ViewModel (ViewModel-lived) strongly subscribes itself to the App-lived\n// bus. Because App strictly outlives ViewModel, the subscription promotes the\n// VM to App lifetime -> it can never die while the app runs => OWN014. This is\n// the region-escape theorem: the *ordering* is what makes it a leak (subscribing\n// to a same/shorter-lived source would be fine).\nfn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel {\n    subscribe self to bus;\n}\n",