Quality gate, lifetimes module (WPF leaks), spec + proposals, and a real C# leak pipeline

.github/workflows/ci.yml

@@ -1,12 +1,36 @@
 name: CI
 
+# Least privilege: every job only reads the repo (no job pushes or needs write).
+# Action SHA-pinning / persist-credentials hardening is deliberately deferred to
+# a Dependabot/hardening pass — see README "где оно жульничает" item #7.
+permissions:
+  contents: read
+
 on:
   push:
     branches: ["**"]
   pull_request:
   workflow_dispatch:
 
 jobs:
+  # Quality gate: ruff (style/bugs) on the whole tree, and mypy --strict on the
+  # ownlang package (tests are dynamic/fuzzer code, covered by ruff only). These
+  # are the "tighten the screws on Python" guard rails — see README.
+  lint:
+    name: lint (ruff + mypy --strict)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+      - name: Install linters
+        run: pip install "ruff==0.15.8" "mypy==1.19.1"
+      - name: ruff
+        run: ruff check .
+      - name: mypy --strict (ownlang)
+        run: mypy
+
   tests:
     name: tests (py${{ matrix.python-version }})
     runs-on: ubuntu-latest
@@ -66,3 +90,37 @@ jobs:
           cp examples/golden_arraypool/Program.cs "$RUNNER_TEMP/golden_app/Program.cs"
           dotnet run --project "$RUNNER_TEMP/golden_app"
 
+  # P-001: prove the C# leak pipeline end-to-end on real C# — the Roslyn
+  # extractor turns sample .cs into OwnIR facts, and the core surfaces the
+  # subscription leak at its C# location (and stays silent on the disposed one).
+  wpf-extractor:
+    name: C# leak extractor (Roslyn) -> OwnIR -> core
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.13"
+      - uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: "8.0.x"
+      - name: Extract OwnIR facts from sample C#
+        run: |
+          dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \
+            frontend/roslyn/samples/CustomerViewModel.cs \
+            frontend/roslyn/samples/OrdersViewModel.cs \
+            -o "$RUNNER_TEMP/facts.json"
+          cat "$RUNNER_TEMP/facts.json"
+      - name: Check facts through the core
+        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; }
+          if echo "$out" | grep -q "OrdersViewModel.cs"; then
+            echo "FAIL: disposed subscription wrongly reported"; exit 1
+          fi
+          echo "OK: real C# -> facts -> OWN001 at the C# location"
+

README.md

@@ -93,6 +93,74 @@ examples/gallery/05_dispose_while_view_live.own:9:13: error: [OWN008] cannot rel
                   ^
 ```
 
+### Бизнес-применение: WPF lifetime-утечки (модуль `lifetimes`)
+
+Performance-профиль (`stackalloc`/pool) — это игрушка для performance-зоопарка.
+Бизнес-софт чаще умирает не от того, что `Span<byte>` на 7 нс медленнее, а от
+зомби-ViewModel: кто-то подписался на singleton-event и не отписался — окно
+закрыто, а `CustomerViewModel` жива весь день, потому что event bus держит на неё
+strong-ссылку. GC не телепат.
+
+Ключевой разворот: **это уже выразимо текущим ownership-ядром.** Моделируем
+ViewModel как scope (конструктор = начало, `Dispose` = конец); подписка =
+`acquire` токена, отписка = `release`. Тогда «подписался и не Dispose» —
+это обычный **OWN001**, а «тронул после Dispose» — **OWN002**. Новый, доменно-
+нейтральный кусок: у `resource` появился тег `kind`, который вешается на
+диагностику как `[resource: ...]` — это шов, за который позже зацепится WPF-
+профиль/Roslyn-фронт, не зная про WPF в самом ядре.
+
+```text
+$ python -m ownlang check corpus/wpf/zombie-viewmodel/case.own
+case.own:16:9: error: [OWN001] 'customerChanged' is owned but not released at
+  end of function (leaks on at least one path) [resource: subscription token]
+  16 |     let customerChanged = acquire Subscription(bus);
+               ^
+```
+
+**Slice #2 — lifetime-регионы (region escape).** Это уже *новый* анализ, а не
+переиспользование. Объявляем регионы с порядком и вешаем lifetime на объект и
+сервисы; сильная подписка на более долгоживущий источник промотит объект до его
+lifetime и течёт — `OWN014`. Именно **порядок** делает это утечкой: подписка на
+равный-или-более-короткий источник — чисто.
+
+```text
+$ python -m ownlang check corpus/wpf/viewmodel-escapes-to-app/case.own
+case.own:15:23: error: [OWN014] 'bus' (lifetime 'App') outlives the captured
+  object 'CustomerViewModel' (lifetime 'ViewModel'); the strong subscription
+  promotes 'CustomerViewModel' to 'App' and it leaks (no release path)
+  15 |     subscribe self to bus;
+                            ^
+```
+```ownlang
+lifetime App;  lifetime Window < App;  lifetime ViewModel < Window;
+fn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel {
+    subscribe self to bus;          // App > ViewModel -> промоушн -> OWN014
+}
+```
+
+**P-001 — настоящий C# (а не hand-reduced).** Узкий Roslyn-экстрактор
+(`frontend/roslyn/`, syntax-only) находит `event += без -=` в реальном `.cs` и
+эмитит OwnIR-факты; Python-мост (`python -m ownlang ownir facts.json`) прогоняет
+их через **то же ядро** и выдаёт OWN001 **на месте C#**:
+
+```text
+CustomerViewModel.cs:9: error: [OWN001] event 'bus.CustomerChanged' is subscribed
+  (handler 'OnCustomerChanged') but never unsubscribed — ... (leak)
+  [resource: subscription token]
+```
+Ядро одно (не второй чекер на C#): экстрактор только производит факты. dotnet
+есть лишь в CI (job `wpf-extractor` гоняет экстрактор на сэмплах сквозняком);
+Python-мост тестируется локально (`tests/test_ownir.py`) на рукописных фактах.
+Объём v0 и не-цели — в [`docs/proposals/P-001`](docs/proposals/P-001-csharp-extractor.md).
+
+`corpus/wpf/` — self-checking корпус реальных WPF-паттернов (`before.cs`/
+`after.cs`/`case.own`/expected), прибитый `tests/test_wpf.py`; региональная
+теорема — `tests/test_lifetimes.py` (10 кейсов). Полный план модуля (каталог
+OWN-WPF, границы слайсов, что отложено) — в [`docs/lifetimes.md`](docs/lifetimes.md).
+Честно: `case.own` — hand reduction паттерна, не C#, который чекер съел (C#-фронта
+нет, это поздний слайс); `self`/`source` — это scope самой функции и её параметры,
+без cross-procedural points-to.
+
 ### Golden-пример: настоящий ArrayPool
 
 ```bash
@@ -278,9 +346,15 @@ fn process(size: int) {
 | OWN032 | owned-ресурс скопирован без `move` |
 | OWN033 | функция с типом возврата может дойти до конца без `return` |
 | OWN034 | операция применена не к owned-ресурсу |
+| OWN035 | несовпадение типа возврата |
+| OWN036 | циклический порядок lifetime-регионов |
 | OWN040 | вызов необъявленной функции (неизвестные вызовы запрещены) |
 | OWN041 | несовместимость аргумента вызова (арность / kind / plain-vs-resource) |
 
+Lifetime-регионы (модуль `lifetimes`): **OWN014** — объект промотится в более
+долгоживущий регион через сильную подписку (region escape); **OWN036** — цикл в
+`<`-порядке; ссылки на необъявленный регион — **OWN030**.
+
 Разделение **definite (002/005)** против **maybe (009/010)** — прямо по ревью:
 ошибка на *всех* путях и ошибка на *каком-то* пути — это разные по резкости
 сообщения, и это разделение естественно выпадает из решётки множеств состояний.
@@ -622,13 +696,49 @@ ownlang/
     buffers.py      # storage policies: режимы, резолв policy+intent, валидация
     cfg.py          # resolver (Symbol/Kind) + collect_signatures + lowering, Invoke
     analysis.py     # flow-sensitive dataflow: var-states + active loans + permissions
+    lifetimes.py    # lifetime-регионы: region-escape (OWN014) + валидация порядка
+    ownir.py        # C#-факты (OwnIR) -> ядро -> диагностика на месте C# (P-001)
     diagnostics.py  # коды OWN0xx в одном месте
     codegen.py      # C# codegen (emit_* шаблоны, try/finally hoist + inline, буферы)
     report.py       # compile-time buffer report -> stdout + .ownreport.json
     __main__.py     # CLI: check / emit / cfg / report
   examples/
     ok_*.own                  # проходят
     bad_*.own                 # падают с конкретным кодом
+    gallery/                  # «что оно ловит» — narrated примеры, пинятся тестом
     golden_arraypool/         # buffer.own + Program.cs (host-код; .csproj не входит)
-  tests/run_tests.py          # 42 кейса анализа + codegen smoke + golden smoke
+  corpus/real-world/          # hand-reduced реальные ArrayPool-баги + expected-коды
+  corpus/wpf/                 # WPF lifetime-баги (zombie-VM, use-after-dispose)
+  spec/                       # НОРМАТИВНАЯ спека: OwnCore/Buffer/Lifetimes/Diag/Codegen
+  docs/proposals/             # forward-looking RFC: P-001 C#-extractor, P-002 verif, ...
+  docs/lifetimes.md           # дизайн модуля lifetimes (WPF, регионы, слайсы)
+  tests/
+    run_tests.py              # кейсы анализа + codegen smoke + golden smoke
+    test_codegen.py           # content-assertions на сгенерённый C#
+    test_codegen_props.py     # property-фаззер с независимым AST-оракулом
+    test_gallery.py           # пинит каждый gallery-пример к его коду
+    test_corpus.py            # пинит каждый corpus-кейс к expected-диагностикам
+    test_wpf.py               # WPF-корпус: коды + [resource: kind] метадата
+    test_lifetimes.py         # region-escape (OWN014) + валидация lifetime-порядка
+    test_spec.py              # conformance: каждое правило spec/ срабатывает на примере
+    test_ownir.py             # OwnIR-мост: C#-факты -> ядро -> OWN001 на месте C#
+  frontend/roslyn/            # C#-экстрактор (Roslyn, CI-only) + сэмплы .cs (P-001)
+  pyproject.toml              # gate: ruff + mypy --strict (см. ниже)
 ```
+
+### Гейт качества (ruff + mypy --strict)
+
+Python взяли ради скорости прототипа, но без типов он легко скрывает «забыл ветку»
+класс багов (ровно такие плодил старый кодоген). Поэтому прикручены гайки, и они
+блокируют CI (job `lint`):
+
+- **ruff** (`E,W,F,I,B,UP,C4,RUF`) — стиль + bugbear-ловушки на всём дереве;
+- **mypy `--strict`** на пакете `ownlang` (тесты — динамический фаззер-код, их
+  держит только ruff);
+- **`typing.assert_never`** в каждом разборе по видам узлов (`lower_stmt`, `step`,
+  `_stmt_inline`): новый невручённый вариант union'а — это **ошибка компиляции
+  типов**, дешёвая замена exhaustive-match. Включение это уже поймало реальную
+  дыру — buffer-`let`, незакрытый в inline-эмиттере.
+
+Локально: `ruff check . && mypy`. Это не заменяет regression-сеть (фаззер/оракул/
+корпус ловят логику, линтер — опечатки и типы), а дополняет её.

corpus/real-world/arraypool-use-after-return/notes.md

@@ -18,8 +18,9 @@ case.own:14:14: error: [OWN002] borrow 'quotient' after it was released
                     ^
 ```
 
-**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not C#
-the checker ingested — OwnLang has no C# front-end. It demonstrates that the
+**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not
+direct C# extractor output (the narrow P-001 extractor covers event-subscription
+leaks, not ArrayPool). It demonstrates that the
 ownership *logic* maps onto the real bug: had the code been written in OwnLang,
 the checker would have rejected it. The real-world specifics (the division math,
 the exact slice bounds) are abstracted to `acquire`/`release`/`borrow`.

corpus/wpf/handler-use-after-dispose/after.cs

@@ -0,0 +1,27 @@
+// FIXED. The callback guards on the disposed flag (and/or the subscription is
+// disposed only after the dispatcher queue is drained), so nothing touches the
+// subscription-backed state after Dispose().
+public sealed class CustomerViewModel : IDisposable
+{
+    private readonly IDisposable _sub;
+    private bool _disposed;
+
+    public CustomerViewModel(IEventBus bus)
+    {
+        _sub = bus.Subscribe<CustomerChanged>(OnCustomerChanged);
+    }
+
+    private void OnCustomerChanged(CustomerChanged e)
+    {
+        if (_disposed) return;   // do not touch disposed state
+        Refresh();
+    }
+
+    private void Refresh() { /* ... */ }
+
+    public void Dispose()
+    {
+        _disposed = true;
+        _sub.Dispose();
+    }
+}

corpus/wpf/handler-use-after-dispose/before.cs

@@ -0,0 +1,29 @@
+// BUGGY (representative WPF pattern, hand-reduced into case.own).
+//
+// The VM disposes its subscription on close, but a callback that was already
+// queued on the dispatcher still runs and touches the (now disposed) state. In
+// real code this surfaces as an ObjectDisposedException or a read of torn state.
+public sealed class CustomerViewModel : IDisposable
+{
+    private readonly IDisposable _sub;
+    private bool _disposed;
+
+    public CustomerViewModel(IEventBus bus)
+    {
+        _sub = bus.Subscribe<CustomerChanged>(OnCustomerChanged);
+    }
+
+    private void OnCustomerChanged(CustomerChanged e)
+    {
+        // a late, already-dispatched callback: runs after Dispose()
+        Refresh();   // touches subscription-backed state after it was disposed
+    }
+
+    private void Refresh() { /* reads disposed state */ }
+
+    public void Dispose()
+    {
+        _disposed = true;
+        _sub.Dispose();
+    }
+}

corpus/wpf/handler-use-after-dispose/case.own

@@ -0,0 +1,17 @@
+module WpfHandlerAfterDispose
+
+// Same subscription-token protocol, tagged with its kind.
+resource Subscription {
+    acquire Subscribe
+    release Dispose
+    kind "subscription token"
+}
+
+// On window close the VM disposes (unsubscribes) its subscription, but a late
+// queued callback still touches it. Using a subscription after Dispose is the
+// generic use-after-release (OWN002), tagged with the resource kind.
+fn CloseHandler(bus: int) {
+    let sub = acquire Subscription(bus);
+    release sub;          // unsubscribed / disposed on close
+    use sub;              // a late callback still touches it -> OWN002
+}

corpus/wpf/handler-use-after-dispose/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN002

corpus/wpf/handler-use-after-dispose/notes.md

@@ -0,0 +1,25 @@
+# WPF subscription used after Dispose
+
+**Pattern:** a ViewModel unsubscribes / disposes its subscription on close, but a
+callback that was already queued on the dispatcher still runs and touches the
+disposed, subscription-backed state. In real code this is an
+`ObjectDisposedException` or a read of torn state — the use-after-dispose cousin
+of the zombie-ViewModel leak.
+
+**What the checker says:** using a resource after its `release` (Dispose) is the
+generic **OWN002** (use after release), carrying the resource-kind tag:
+
+```text
+$ python -m ownlang check corpus/wpf/handler-use-after-dispose/case.own
+case.own:16:9: error: [OWN002] use 'sub' after it was released
+  [resource: subscription token]
+  16 |     use sub;
+               ^
+```
+
+**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not
+direct C# extractor output (the C# extractor in P-001 is narrow — event
+subscriptions only). It shows the ownership
+*logic* maps onto the real bug; it does not model the dispatcher queue or
+exception flow. `before.cs` / `after.cs` are representative, not a verbatim copy
+of one PR.

corpus/wpf/viewmodel-escapes-to-app/after.cs

@@ -0,0 +1,21 @@
+// FIXED. The subscription is kept as a disposable token and released when the
+// VM is disposed (on window close), so the App-lived bus no longer holds the
+// Window-lived VM: the VM drops back to its intended Window lifetime and is
+// collectable. (In OwnLang terms this is the slice-#1 acquire/release token
+// pattern; the region check then sees a release path and stays quiet.)
+public sealed class CustomerViewModel : IDisposable
+{
+    private readonly IDisposable _customerChanged;
+
+    public CustomerViewModel(IEventBus appBus)
+    {
+        _customerChanged = appBus.Subscribe<CustomerChanged>(OnCustomerChanged);
+    }
+
+    private void OnCustomerChanged(CustomerChanged e) { /* ... */ }
+
+    public void Dispose()
+    {
+        _customerChanged.Dispose();   // release path -> VM no longer promoted
+    }
+}

corpus/wpf/viewmodel-escapes-to-app/before.cs

@@ -0,0 +1,18 @@
+// BUGGY (representative WPF pattern, hand-reduced into case.own).
+//
+// A Window-scoped ViewModel subscribes itself to an App-scoped (singleton) event
+// bus with a strong handler and keeps no unsubscribe token. The bus is reachable
+// from an App-lifetime GC root, and through the strong delegate so is the VM:
+// the VM is *promoted* to App lifetime. Close the window all you want -- the VM
+// lives until the process exits. The lifetime mismatch (VM expected Window,
+// actually App) is the leak.
+public sealed class CustomerViewModel
+{
+    public CustomerViewModel(IEventBus appBus)   // appBus: App lifetime (singleton)
+    {
+        // strong subscription, no token kept -> VM promoted to App lifetime
+        appBus.CustomerChanged += OnCustomerChanged;
+    }
+
+    private void OnCustomerChanged(object? sender, EventArgs e) { /* ... */ }
+}

corpus/wpf/viewmodel-escapes-to-app/case.own

@@ -0,0 +1,16 @@
+module WpfRegionEscape
+
+// Lifetime regions: a Window-lived ViewModel must not outlive its window, and
+// the App-lived event bus outlives everything.
+lifetime App;
+lifetime Window < App;
+lifetime ViewModel < Window;
+
+// The ViewModel (ViewModel-lived) strongly subscribes itself to the App-lived
+// bus. Because App strictly outlives ViewModel, the subscription promotes the
+// VM to App lifetime -> it can never die while the app runs => OWN014. This is
+// the region-escape theorem: the *ordering* is what makes it a leak (subscribing
+// to a same/shorter-lived source would be fine).
+fn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel {
+    subscribe self to bus;
+}

corpus/wpf/viewmodel-escapes-to-app/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN014