Claude/p014 tier a semantic

.github/workflows/ci.yml

@@ -114,6 +114,9 @@ jobs:
             frontend/roslyn/samples/MessengerViewModel.cs \
             frontend/roslyn/samples/PooledBufferSample.cs \
             frontend/roslyn/samples/LocalDisposableSample.cs \
+            frontend/roslyn/samples/SelfOwnedViewModel.cs \
+            frontend/roslyn/samples/StaticHandlerViewModel.cs \
+            frontend/roslyn/samples/SampleTypes.cs \
             -o "$RUNNER_TEMP/facts.json"
           cat "$RUNNER_TEMP/facts.json"
       - name: Check facts through the core
@@ -173,6 +176,16 @@ jobs:
           if echo "$out" | grep -qE "'guarded'|'moved'"; then
             echo "FAIL: using/returned local wrongly reported"; exit 1
           fi
+          # P-004 self-owned exemption: a subscription whose source is a field the
+          # class constructs (owns) is a GC-collectable cycle, not a leak — silent.
+          if echo "$out" | grep -q "SelfOwnedViewModel.cs"; then
+            echo "FAIL: a self-owned subscription was wrongly reported"; exit 1
+          fi
+          # P-004 static-handler exemption: a static-method handler has a null
+          # delegate target — no instance retained, so not a leak — silent.
+          if echo "$out" | grep -q "StaticHandlerViewModel.cs"; then
+            echo "FAIL: a static-handler subscription was wrongly reported"; exit 1
+          fi
           echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool + local) at the C# location"
 
   # The distribution surface (Уровень 1): the own-check.sh orchestrator walks a

README.md

@@ -139,9 +139,10 @@ fn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel {
 ```
 
 **P-001 — настоящий C# (а не hand-reduced).** Узкий Roslyn-экстрактор
-(`frontend/roslyn/`, syntax-only) находит `event += без -=` в реальном `.cs` и
-эмитит OwnIR-факты; Python-мост (`python -m ownlang ownir facts.json`) прогоняет
-их через **то же ядро** и выдаёт OWN001 **на месте C#**:
+(`frontend/roslyn/`, type-aware: project-local `SemanticModel`, см. P-014) находит
+`event += без -=` в реальном `.cs` (по семантике: `sum += value` — не событие, а
+арифметика) и эмитит OwnIR-факты; Python-мост (`python -m ownlang ownir facts.json`)
+прогоняет их через **то же ядро** и выдаёт OWN001 **на месте C#**:
 
 ```text
 CustomerViewModel.cs:9: error: [OWN001] event 'bus.CustomerChanged' is subscribed

docs/ROADMAP.md

@@ -35,9 +35,12 @@ long-term identity the backlog is aiming at:
   - Concretely: prove Own.NET finds **one** real memory/resource bug in real C#,
     then widen the frontend to fit exactly the next real bug.
 - **Narrow C# frontend, intraprocedural first.** The frontend's job is not to
-  "understand C#" (SemanticModel hides async, generics, LINQ, closures, pattern
-  matching, overload resolution, nullable flow, source generators…). Its job is
-  to extract *facts*: acquire / borrow / use / release / escape / control-flow.
+  "understand C#" — it uses a project-local `SemanticModel` only for binding and
+  type resolution (is a `+=` LHS an event or a number? — [P-014](proposals/P-014-semantic-resolution.md)),
+  not for whole-language understanding (async, generics, LINQ, closures, pattern
+  matching, overload resolution, nullable flow, source generators stay out of
+  scope). Its job is to extract *facts*: acquire / borrow / use / release / escape
+  / control-flow.
 - **Refuse the soul-eating version.** Every proposal's Non-goals section is the
   most important one. Boredom keeps projects alive.
 

docs/howto-visual-studio.md

@@ -150,9 +150,10 @@ instead of the bash command.
 - **Heuristic findings can be false positives** (e.g. ownership handed to a
   callee). Treat output as a reviewer, not a gate, until you've calibrated it on
   your codebase — and prefer `--fail-on-finding` only once it's quiet.
-- **One method at a time, syntax-only.** The extractor does not do
-  interprocedural/`async`/whole-program analysis yet (by design — see the
-  ROADMAP). It honestly skips what it can't model rather than guessing.
+- **One method at a time, type-aware (project-local `SemanticModel`).** The
+  extractor does not do interprocedural/`async`/whole-program analysis yet (by
+  design — see the ROADMAP). It honestly skips what it can't model rather than
+  guessing.
 - **`bin`/`obj`/generated files are skipped**; paths are reported relative to the
   scan root so they resolve in the editor and on the PR.
 

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

@@ -9,7 +9,8 @@
 The `event += without -=` pattern, end-to-end, exactly along the recommended
 seam:
 
-- **Roslyn extractor** (`frontend/roslyn/OwnSharp.Extractor`, C#, syntax-only):
+- **Roslyn extractor** (`frontend/roslyn/OwnSharp.Extractor`, C#, type-aware:
+  project-local `SemanticModel` — see [P-014](P-014-semantic-resolution.md)):
   scans `.cs`, emits OwnIR facts (JSON) — built & run in CI (`wpf-extractor`).
 - **Python fact bridge** (`ownlang/ownir.py`, `python -m ownlang ownir`): lowers
   facts to a synthetic `.own` sketch, runs the **existing core**, and maps the
@@ -31,7 +32,9 @@ narrow class of leaks the core already models: event subscriptions, timers,
 `IDisposable` fields, ignored `Subscribe` results.
 
 This is **not** a full C# ownership front-end (generics, async, dataflow — that is
-human-years and explicitly rejected). It is a syntactic/local pattern extractor.
+human-years and explicitly rejected). It is a narrow, intraprocedural fact
+extractor — type-aware for the one fact that needs it (the type of a `+=` LHS),
+via a project-local `SemanticModel` ([P-014](P-014-semantic-resolution.md)).
 
 ## Scope (v0)
 

docs/proposals/P-004-wpf-lifetime-profile.md

@@ -1,8 +1,8 @@
 # P-004 — WPF / UI lifetime leak profile
 
 - **Status:** in progress (P0) — WPF001 (v0) + **WPF002 (timer)** + **WPF003
-  (IDisposable field)** + **WPF004 (ignored Subscribe) built**; WPF005 (escape)
-  next
+  (IDisposable field)** + **WPF004 (ignored Subscribe)** + **self-owned & static-
+  handler exemptions (P-014 Tier A) built**; WPF005 (escape) next
 - **Depends on:** [P-001](P-001-csharp-extractor.md) (the extractor + OwnIR seam),
   `spec/OwnCore.md`, `spec/Lifetimes.md` (OWN001 leak, OWN014 region escape).
   See [`docs/ROADMAP.md`](../ROADMAP.md) for where this sits (Milestones 1–2).
@@ -46,6 +46,23 @@ escapes(this, App)  -> a strong capture by a longer-lived source  (feeds OWN014)
 Dispose/OnClosed/Unloaded -> a permitted release region
 ```
 
+**Lifetime exemptions (built, P-014 Tier A).** Two sound, syntax-cheap cases where
+a `+=` without `-=` is provably *not* a leak and is dropped — decided semantically
+(symbols, not text):
+- **Self-owned source** — the event source is `this`, or a field/local the class
+  constructs (and so owns); the `source <-> this` cycle outlives nothing and is
+  GC-collectable.
+- **Static handler** — `+= StaticMethod` stores a delegate whose `Target` is null,
+  so no instance is retained, however long-lived the source.
+
+Timers are excluded from both (a *running* timer is dispatcher-rooted regardless).
+Samples: `SelfOwnedViewModel.cs` / `StaticHandlerViewModel.cs` (silent) vs
+`CustomerViewModel.cs` (injected instance source → leak). On GTM these keep
+`VCreate`/`VRibbon`'s *instance* subscriptions to the static
+`LicContext.LicenseDataChanged` as leaks, while dropping the static-class
+`Context`'s subscription to the *same* event — the deciding factor is the
+subscriber/handler, not the source.
+
 The corpus already pins three of these against real core codes:
 `corpus/wpf/zombie-viewmodel` (OWN001), `viewmodel-escapes-to-app` (OWN014),
 `handler-use-after-dispose` (OWN002). WPF004/WPF005 are the increments that emit

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

@@ -261,7 +261,10 @@ T1→T2 are sequential (infra then fix); T3/T4 land with T2; T5 (docs) any time;
   **P-004** — its mechanisms are `[OwnIgnore("source lifetime is shorter")]`
   (P-004:60-61) and WPF005 firing OWN014 only on a *longer-lived* source
   (P-004:35,45). P-014 removes the *gross* noise (arithmetic, unresolved
-  externals) so P-004's heuristic operates on real subscriptions only.
+  externals) so P-004's heuristic operates on real subscriptions only. (The first
+  P-004 increment — the self-owned-source exemption, skipping a subscription whose
+  source is `this` or a field the class constructs — landed alongside this work;
+  see P-004.)
 - **Requiring a green build for Tier A.** The compilation degrades gracefully:
   partial resolution still types the locals/fields Tier A needs.
 - **A new `info`/`note` severity level.** The unresolved channel is a `warning`.

docs/proposals/P-016-deep-fact-extraction.md

@@ -0,0 +1,157 @@
+# P-016 — Deep C# fact extraction: CFG + flow lowering
+
+- **Status:** draft (P1 — the "make the core actually bite real C#" track)
+- **Depends on:**
+  - [P-014](P-014-semantic-resolution.md) Tier A — the `SemanticModel` (**DONE**).
+    The hard prerequisite: typed ownership facts are impossible without binding.
+  - [P-001](P-001-csharp-extractor.md) — the extractor → OwnIR → core seam, and the
+    `ownir_version` contract.
+  - [P-005](P-005-idisposable-ownership.md) — the first deep profile this unlocks
+    (IDisposable acquire/release on all paths); [P-004](P-004-wpf-lifetime-profile.md)
+    (lifetime), [P-007](P-007-arraypool-span.md) (borrow/Span).
+  - `spec/OwnCore.md`, `spec/Lifetimes.md` — the fact vocabulary the core *already*
+    checks (acquire / move / borrow / use / release / escape / control-flow).
+- **Strategy hub:** [`docs/ROADMAP.md`](../ROADMAP.md).
+
+## Motivation
+
+The core (`ownlang`) is a sound, tested, flow-sensitive ownership / borrow /
+lifetime checker — **but only on the `.own` DSL.** On real C#, the Roslyn frontend
+feeds it a *flat list of pattern-matched resource facts* (`event +=`, IDisposable
+field, pool, local-disposable). None of the core's deep machinery —
+release-on-all-paths across branches, use-after-release, double-release, move,
+borrow aliasing, lifetime ordering — is exercised on real code. The engine runs;
+the fuel line to real C# is a trickle. Two concrete gaps:
+
+1. **The frontend emits no control flow and no per-statement operations.** It does
+   not lower real method bodies into acquire / use / release / move / borrow over a
+   CFG, so OWN001/002/003/005/… never fire on real C# beyond the shallow patterns.
+2. **The core does not model loops.** `cfg.py`: *"There are no loops, so the CFG is
+   a DAG and a single topological pass suffices — this is exactly where loop support
+   (worklist + fixpoint) would later plug in."* `OWN020` marks loops/async
+   unsupported. Real C# is full of loops.
+
+P-014 Tier A removed the hard prerequisite (the frontend now has a `SemanticModel`).
+This proposal is the plan to feed the *existing* core real facts — a CFG plus
+acquire/use/release/move/borrow — from real C#, **one fact-type per increment**,
+plus the core loop support that lets those facts be checked on real (loopy) methods.
+
+This is the honest answer to "does Own.NET work, or only on paper?": prove one real
+flow-sensitive verdict on real C# end-to-end. If the thin vertical slice (B0+B2
+below) lights up a true OWN001 on GTM, the concept is proven; if it proves
+intractable, far better to learn that now than after more breadth.
+
+## Dependencies — what we depend on to start
+
+| # | Dependency | Status |
+|---|------------|--------|
+| 1 | Types in the frontend (no typed ownership facts without binding) | ✅ **DONE — P-014 Tier A `SemanticModel`** |
+| 2 | A control-flow graph from real C# | Roslyn `ControlFlowGraph` / `IOperation` exists — needs lowering |
+| 3 | OwnIR (and the bridge) able to carry per-method operations + a CFG | schema growth — see **B0** |
+| 4 | The core handles loops | ❌ missing (`OWN020`); worklist + fixpoint — the set-of-states lattice is finite & union-merged, so it converges — see **A1** |
+| 5 | An honest-skip path for shapes we cannot model (async, exotic flow) | ✅ already the project's philosophy |
+
+Replace the "single topological pass" with a worklist, and the flat fact list with
+a CFG-carrying bridge, and the existing core checks real code.
+
+## Scope — the increments (two tracks that meet at the rich-fact bridge)
+
+### Track A — core only (pure DSL, no frontend, `.own`-tested)
+
+- **A1 — Loops.** Replace the single topological pass over the DAG (`cfg.py`,
+  `analysis.py`) with a worklist + fixpoint over back-edges. The lattice is the
+  finite set-of-states (OwnCore §3, union at merges) → monotone → it converges
+  (confirm whether widening is even needed). Removes the `OWN020` "loops" clause.
+  Fully independent of the frontend; pinned by new `.own` loop cases + the gallery.
+
+### Track B — frontend depth (needs the `SemanticModel`, now present)
+
+- **B0 — Direct-Module bridge (and kill the double parse).** Two steps:
+  - **B0a (refactor, no behavior change):** today the bridge lowers OwnIR facts to
+    `.own` **source text** (`ownir.py` `to_own`) and the core **re-parses that text**
+    (`__main__._collect` → `parse`) before checking — a parse of a tree we just
+    built, a round-trip that has existed since P-001 and doubles the lowering work
+    (every new fact must be expressible as, *and survive a round-trip through*,
+    generated `.own` text). Replace it: build the core `Module` AST
+    (`ast_nodes`) **directly** from facts and call `check_module` — no text, no
+    re-parse. The seam is already split for this (`ownir.py`: *"builds a Module and
+    calls `__main__.check_module` directly … the seam is already split so that
+    switch is additive, not a rewrite"*). Pin against the existing fixtures: same
+    findings, one fewer parse.
+  - **B0b (enabler):** extend OwnIR — and the direct `Module` construction — to carry
+    per-method **basic blocks + acquire / use / release / move / borrow / return**
+    operations: the schema the deep checks need. Bumps `OWNIR_VERSION` (a new fact
+    *category*, NOT additive like P-014's OWN050; the version gate already forces the
+    extractor and core to move together).
+- **B1 / B2 — IDisposable flow for locals.** Lower a method's `new` / `using` /
+  `.Dispose()` / `return` into acquire / release / escape over a Roslyn CFG → real
+  **OWN001** (leaked on an exception/early-return path), **OWN002** (use after
+  dispose), **OWN003** (double dispose) on live C#. The IDisposable story (P-005) —
+  the most common .NET resource bug, and the first time the core's flow analysis
+  bites real code. B2 (`using`/try-finally → scoped release) is the smallest first
+  slice; do it before the general case.
+- **B3 — Move / ownership transfer.** `return disposable`, or passing it to a callee
+  that consumes it → move / escape (P-005 D5). Intraprocedural, driven by declared
+  signatures, not whole-program tracing.
+- **B4 — Borrow / Span.** `Rent` → view → `Return`, `Span`/`ref` aliasing (P-007) —
+  the borrow checker's crown jewel, hardest on C# (ref structs, Span lifetimes).
+- **B5 — Lifetime ordering.** WPF005 escape (`OWN014`) and DI captive (P-006,
+  partly built) — the hardest; needs an explicit lifetime model.
+
+**Dependency order:** `B0 → B1 → B3 → B4 / B5`. `A1` is independent but needed for
+B1 to cover loopy methods — until A1 lands, a method containing a loop is honestly
+skipped (`OWN020`), not guessed. B0+B2 and A1 can proceed in parallel.
+
+## Non-goals
+
+- A full C# semantic front-end. We lower the operations the core already models, not
+  the language. `async`/`await` stays an honest skip (`OWN020`) until a real bug
+  demands it; whole-program/interprocedural analysis beyond signature-declared
+  transfer; the XAML/binding engine. The "refuse the soul-eating version" rule holds.
+- Rewriting the core. A1 *extends* the existing flow engine (worklist) — it does not
+  replace the lattice. B0–B5 only feed the core; they decide no verdicts.
+
+## Sketch
+
+```text
+            A1: worklist+fixpoint (loops)  ─────────────┐
+                                                        v
+real *.cs ─[Roslyn CFG + IOperation]─[B1..B5: acquire/use/release/move/borrow]
+          ─[B0b: per-method ops+blocks OwnIR]─[B0a: build Module directly]
+          ─[the one core]──> OWN001/002/003/005/014 @ the C# line
+```
+
+## Relationship to the spec & docs (anti-drift)
+
+- **`spec/` core semantics: unchanged by Track B.** The core already models
+  acquire/borrow/move/lifetime for `.own`; B0–B5 *feed* it those facts from C#, they
+  do not change what it means. **A1 does change the core** (it analyses loops): when
+  it lands, `spec/OwnCore.md`'s "loops out of scope" (§10) and the `OWN020`
+  loops clause are updated to describe the worklist — spec follows code.
+- **OwnIR contract:** B0b **bumps `OWNIR_VERSION`** — rich per-method facts are a new
+  category, not an additive optional field (contrast P-014's OWN050, which did not
+  bump). The load-time version gate already makes a mismatched extractor/core fail
+  loudly, so the bump is safe by construction.
+- **No new diagnostic codes** — B1–B5 reuse the existing OWN001/002/003/005/008/014.
+  The only catalogue change is *removing* the loops clause from OWN020 when A1 ships.
+- **"One checker" preserved:** B0a removes a parse, not a decider; the core remains
+  the single source of truth.
+
+## Open questions
+
+1. **B0b schema shape.** Grow the OwnIR JSON with a per-function ops+blocks array
+   the bridge maps to a `Module`, or have the extractor emit a serialized `Module`
+   directly? (Lean: ops+blocks JSON — keeps the extractor decider-free.)
+2. **try-finally / `using` modeling.** Map to a "release on all paths" region, or to
+   explicit release on each CFG exit edge?
+3. **How much of Roslyn's `ControlFlowGraph` to consume** (its basic blocks + the
+   operations we map) vs build our own CFG from syntax. (Lean: consume Roslyn's — it
+   already normalizes `using`/`try`/short-circuits.)
+4. **Loop fixpoint:** does the finite set-of-states lattice converge fast enough
+   as-is, or is widening warranted on pathological back-edges? (Likely converges.)
+5. **Honest-skip granularity:** on an unsupported construct, skip the whole method,
+   or analyse the modelable prefix and skip the rest? (Conservative: skip the method,
+   emit `OWN020` once.)
+6. **Which slice proves the concept fastest** — B0a+B2 on loop-free methods is the
+   proposed existential spike; confirm it surfaces a real OWN001 on GTM before
+   investing in B3–B5.

docs/proposals/README.md

@@ -37,9 +37,10 @@ proposal is marked `done` with a pointer.
 | [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-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 |
 
 > 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-015
+> of these, see the strategy hub: [`docs/ROADMAP.md`](../ROADMAP.md). P-004 … P-016
 > capture ideas raised in design discussion — they are *on the record for
 > consideration*, drafts, not commitments.
 

frontend/roslyn/OwnSharp.Extractor/OwnSharp.Extractor.csproj

@@ -21,7 +21,9 @@
   </PropertyGroup>
 
   <ItemGroup>
-    <!-- Syntax-only Roslyn: we parse C# source text, no compilation/references. -->
+    <!-- Type-aware Roslyn (P-014 Tier A): project-local CSharpCompilation +
+         SemanticModel over the runtime's framework references, still fact-only
+         and intraprocedural. -->
     <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="4.9.2" />
   </ItemGroup>