Merge pull request #176 from PhysShell/claude/own-net-typestate-analysis-q6k0k0

feat(obligations): obligation protocols — barrier-sensitive project invariants (P-025, first slice)

Author: PhysShell

docs/ROADMAP.md

@@ -325,3 +325,4 @@ own scan. Label them as estimates wherever they appear.
 | [P-017](proposals/P-017-multi-stack-frontends.md) | Multi-stack frontends (OwnTS / OwnJVM: OwnJava + OwnKotlin) | horizon | draft |
 | [P-020](proposals/P-020-ownts-react-effects.md) | OwnTS React effects profile (`Own.React`) — effect-storm angle | horizon | draft |
 | [P-021](proposals/P-021-async-audit-pack.md) | Async audit pack (`Own.Async`) — safety-first WPF/application async lifecycle diagnostics | P2 | draft |
+| [P-025](proposals/P-025-obligation-protocols.md) | Obligation protocols (`Own.Protocols`) — barrier-sensitive project invariants (OBL001–005) | P1 | first slice built (core + bridge + fixtures; extractor pending) |

docs/proposals/P-025-obligation-protocols.md

@@ -0,0 +1,190 @@
+# P-025 — Obligation protocols (`Own.Protocols`) — barrier-sensitive project invariants
+
+- **Status:** first slice built (core + bridge + spec + fixtures, `OBL001–005`
+  end-to-end over hand-written facts); the Roslyn extractor slice is designed
+  below but **not** implemented (this sandbox has no dotnet; extractor work is
+  CI-validated).
+- **Built:** [`ownlang/obligations.py`](../../ownlang/obligations.py) (the
+  path-sensitive checker), the `protocols[]` / `protocol_functions[]` OwnIR
+  blocks ([spec/OwnIR.md §8](../../spec/OwnIR.md)), the `OBL001–OBL005` codes,
+  [`tests/test_obligations.py`](../../tests/test_obligations.py) (64 checks),
+  and the `protocol_isloaded_*` killer-demo fixtures.
+- **Depends on:** [spec/OwnIR.md](../../spec/OwnIR.md) (the facts seam),
+  [P-016](P-016-deep-fact-extraction.md) (the flow lowering the extractor slice
+  reuses), [P-006](P-006-di-lifetimes.md)/[P-020](P-020-ownts-react-effects.md)
+  (the sidecar-analysis precedent this copies).
+- **Relation to [P-010](P-010-type-disciplines.md):** P-010's `protocol` blocks
+  are *typestate on an object across its lifetime* (state machines, consume-self
+  transitions on the affine core). P-025 is deliberately smaller: *temporal
+  obligations inside a method*, checked against project-declared barriers. P-010
+  can later subsume these rules; nothing here blocks it.
+
+## Motivation — the invariant the type system cannot know
+
+A legacy WPF method breaks its own invariant on purpose, briefly:
+
+```csharp
+IsLoaded = false;          // the document tree is now inconsistent — on purpose
+RebuildIndexes();
+if (hasWarnings)
+    OnPropertyChanged(nameof(Document));   // ← published the broken object
+IsLoaded = true;
+OnPropertyChanged(nameof(Document));       // this one is fine
+```
+
+`IsLoaded = false` is not a bug; **publishing the object while the flag is
+down** is. No general checker can know that `IsLoaded` means "the document is
+consistent", that `PropertyChanged("Document")` hands the object to bindings
+*right now*, or that `PropertyChanged("Progress")` is harmless meanwhile. That
+knowledge is project-specific. Existing tools stop exactly here: analyzers know
+universal protocols (dispose your `IDisposable`, unsubscribe your event);
+NDepend/CodeQL can query structure but have no barrier-sensitive obligation
+model; typestate research languages don't speak legacy C#. The niche is real:
+**barrier-sensitive, project-specific obligation checking for code review** —
+and the OwnAudit STS corpus already shows the shape in the wild (17k
+INPC findings, 8 recorded `IsLoaded` findings, `BrokerDataClasses` as the
+subscription-leak epicenter).
+
+The same three verbs cover the whole family:
+
+```text
+IsLoaded=false            must become true      before PropertyChanged(Document)
+_suppressNotifications    must be restored      before return/throw
+BeginUpdate               must meet EndUpdate   before Refresh / method exit
+SuspendCalculation        must be resumed       before results are published
+```
+
+## The model — obligation / barrier / require-closed-before
+
+One protocol = three matchers and a scope (the full shape and its normative
+semantics live in [spec/OwnIR.md §8](../../spec/OwnIR.md)):
+
+- **opens** — the event that creates the obligation (`IsLoaded = false`, or a
+  call: `BeginUpdate()`);
+- **closes** — the event that discharges it;
+- **barriers** — events it must not cross while open: configured calls (with an
+  optional distinguished-argument set, so `OnPropertyChanged` can be unsafe for
+  `Document` but allowed for `Progress`) plus, by default, every method exit
+  (`return`, `throw`, falling off the end — the OWN001 shape).
+
+The checker ([`ownlang/obligations.py`](../../ownlang/obligations.py)) walks the
+method's ordered event tree path-sensitively; the obligation state is a set over
+{OPEN, CLOSED} joined by union at merges, so **definite vs maybe** falls out of
+the lattice exactly as OWN002 vs OWN009 do. Loops are solved to a local fixpoint
+and emit once. Findings carry the ordered evidence slice — *opened here → barrier
+fired here → closed only here, after the barrier* — which SARIF renders as a
+click-through `codeFlows` trace.
+
+| Code | Meaning |
+|------|---------|
+| OBL001 | obligation still open when a barrier fires (every path) |
+| OBL002 | obligation may still be open at a barrier (some path) |
+| OBL003 | obligation not closed before the method exits (every path) |
+| OBL004 | obligation may not be closed before an exit (some path) |
+| OBL005 | advisory: a protocol's scope matched no reported method (dead rule) |
+
+## Precision policy (the standing red line, applied here)
+
+False positives kill this feature faster than any competitor — a rule that
+cries on every `IsLoaded=false` gets switched off like a smoke alarm that hates
+toast. Three normative rules (all tested):
+
+1. **Never invent.** An opaque write to a tracked flag (`IsLoaded = Compute()`)
+   may *discharge* an open obligation (state gains CLOSED → the crossing
+   degrades to a *maybe*) but never *creates* one.
+2. **Unnamed calls are neutral.** A call the protocol doesn't mention neither
+   discharges nor crosses. A callee that flips the flag internally is invisible
+   in v1 — that is the phase-3 interprocedural slice, not a v1 guess.
+3. **Scope is the throttle.** `scope.methods` restricts a rule to named
+   methods; the MVP posture is *one protocol, one method, one historical bug*.
+   A scoped rule matching nothing is surfaced (OBL005), not silently dead.
+
+## Why this shape (decisions on the record)
+
+- **Sidecar analysis, not new core instructions.** `di.py`/`effects.py` set the
+  pattern: a fact family + a small core analysis routed via `check_facts`. The
+  alternative (new `Instr` variants in `cfg.py`) touches the frozen
+  `cfg_json.py` oracle seam, `codegen.py`, the grammar, and the Rust mirror —
+  all for no v1 gain. Revisit when protocols need loans/RID interplay.
+- **Additive OwnIR blocks, no version bump.** `services` and `effects` landed
+  additively at v0; `protocols`/`protocol_functions` follow the same IR3 rule.
+  An older core ignores them; their internal vocabularies (`ev`, matcher
+  `kind`) are fail-loud per IR4 and version *with the blocks*.
+- **Rules are data, not a language.** The chat-derived requirement is explicit:
+  nobody wants to learn OwnLang — including its author. Protocols are declared
+  as JSON facts (later: generated from attributes/inference and *approved*, see
+  the roadmap), never hand-written `.own`. OwnLang stays what Own.NET
+  understands, not what users write.
+- **Messages are line-free.** OwnAudit fingerprints findings on
+  (path, rule, message) for the baseline ratchet and the FP-judge overlay; a
+  line number in the message would break both on every unrelated edit. Lines
+  live in the evidence slice.
+
+## The extractor slice (designed, not built — needs CI/dotnet)
+
+`OwnSharp.Extractor` already collects everything required; the slice is
+emission, not analysis (one checker: the extractor reports, the core decides):
+
+1. **Events.** Extend the P-016 flow lowering (`LowerFlowStmt`/`EmitFlowExpr`,
+   with its `onReturn`/`onThrow` continuation threading, so `finally` and
+   exceptional paths come sound for free) to emit `protocol_functions[].events`
+   for methods in some protocol's scope: member assigns with literal boolean
+   RHS (`AssignedFieldName`/`ThisFieldName` already normalize the LHS; a
+   non-literal RHS emits an opaque assign with no `value`), self-calls with a
+   `nameof(X)`/string-literal first argument as `{"ev":"call","arg":"X"}`
+   (`SelfCallName` already recognizes the receiver), and `return`/`throw`.
+   Scope-gating keeps the facts file small and the honest-skip discipline
+   (`methods_skipped_unmodelled`) carries over.
+2. **Rules.** A project file (e.g. `.own-protocols.json`, schema =
+   `$defs/protocol`) merged into the facts by `own-check.sh` — configuration
+   travels with the repo, not the tool invocation.
+3. **CI.** A `samples/LoadingProtocolSample.cs` + grep assertions in the
+   `wpf-extractor` job, and a corpus case once real-world instances are mined
+   (the OwnAudit STS stand is the natural first target).
+
+## Roadmap (each phase lands only after the previous one holds on real code)
+
+1. **v1 (this slice):** core + bridge + fixtures. Killer demo:
+   `python -m ownlang ownir tests/fixtures/ownir/protocol_isloaded_violation.facts.json`
+   → `OBL001` at `BigDocumentViewModel.cs:241` with the three-hop path.
+2. **Extractor emission** (above) — the same demo on real C#.
+3. **Interprocedural obligations:** per-method summaries
+   (`mayOpen/mustClose/mayCross` per protocol) on the MOS/SCC channel of
+   [`ownership.py`](../../ownlang/ownership.py), so `ApplyWarnings()` that
+   notifies internally stops being invisible. Same tier ladder as D5
+   (inferred → curated → annotation).
+4. **Authoring surfaces:** `[OwnProtocol]`-style C# attributes and/or inferred
+   candidate protocols ("in 27 places `IsLoaded=false` … `true` precedes the
+   Document notify; 2 places violate — adopt this rule?") emitted as *suggested*
+   config a human approves and commits.
+5. **Consumption:** OwnAudit picks OBL findings up as canonical finding records
+   (SARIF evidence/codeFlows already flow through `report/sarif.py`; register
+   the category for severity mapping and the runtime correlator), and the
+   diff-aware baseline gate makes them review-time signals ("fail only new
+   violations").
+
+## Non-goals
+
+- **Not a general temporal-logic engine.** No LTL, no arbitrary predicates, no
+  cross-object protocols. Three verbs and a scope; the moment a rule needs a
+  formula, it is a P-010/P-002 customer.
+- **Not typestate.** No per-object state machines, no consume-self transitions,
+  no aliasing of obligation carriers (the protocol tracks *the method's own*
+  flags/calls; `this`-aliasing is out of scope for v1 by construction, and the
+  RID machinery exists when that changes).
+- **Not a DSL for people to write.** Facts in, findings out. Any future
+  human-facing surface is attributes or approved generated config.
+- **Not on by default anywhere.** No built-in protocol ships with the tool; an
+  empty `protocols[]` means the analysis does not exist for that repo.
+
+## Open questions
+
+1. **`await` as a barrier.** During an `await` the broken state is observable
+   by the UI thread; is that a barrier by default, opt-in
+   (`{"kind": "await"}` in `barriers`), or a per-protocol flag? (The extractor
+   currently skips most async bodies anyway — honest-skip.)
+2. **Cross-member protocols** (open in `BeginLoad`, close in `OnLoaded`): needs
+   obligation state on the *component*, not the method — the RID model fits,
+   but the facts shape does not yet.
+3. **Suggested-protocol mining:** does inference live in the core (over
+   `protocol_functions` without rules) or in OwnAudit (over the corpus)?

docs/proposals/README.md

@@ -44,6 +44,7 @@ proposal is marked `done` with a pointer.
 | [P-022](P-022-rust-core-migration.md) | Rust core migration: crate DAG, patterns, prior art, differential oracle (Python = golden) | draft / exploratory |
 | [P-023](P-023-architecture-guard.md) | Architecture guard (`Own.Arch`): rules.yaml intent model + dependency-graph gate + baseline ratchet | draft |
 | [P-024](P-024-security-audit-profile.md) | Security audit profile (external tools + SARIF adapters; rejects own scanner engine) | draft |
+| [P-025](P-025-obligation-protocols.md) | Obligation protocols (`Own.Protocols`): barrier-sensitive project invariants (OBL001–005) | first slice built (core + bridge + fixtures; extractor pending) |
 
 > 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-016

ownlang/__main__.py

@@ -307,7 +307,7 @@ def cmd_ownir(path: str, fmt: str = "human", severity: str = "error",
     selects the surface: human (CLI), github (CI annotations), msbuild (VS),
     sarif (SARIF 2.1.0 log);
     `severity` picks how the host shows them (error/warning); `verbosity` is
-    `quiet` (errors only — hide the advisory OWN050 notes), `normal` (default), or
+    `quiet` (errors only — hide the advisory notes), `normal` (default), or
     `verbose` (also print a per-code breakdown)."""
     from .ownir import OwnIRError, build_sarif, check_facts, load, render_finding
     try:
@@ -321,9 +321,9 @@ def cmd_ownir(path: str, fmt: str = "human", severity: str = "error",
     # pollute that stream.
     machine = fmt in {"github", "msbuild", "sarif"}
     summary_to = sys.stderr if machine else sys.stdout
-    # OWN050 "leakage analysis skipped" notes are advisory (P-014 Tier A): always
-    # shown as warnings regardless of --severity, and never affect the exit code —
-    # they are coverage notes ("we could not check this"), not verdicts.
+    # Advisory findings (OWN050 "leakage analysis skipped", OBL005 "dead protocol
+    # rule") are always shown as warnings regardless of --severity, and never
+    # affect the exit code — they are coverage/hygiene notes, not verdicts.
     leaks = [f for f in findings if not f.advisory]
     notes = [f for f in findings if f.advisory]
     shown = leaks if verbosity == "quiet" else findings
@@ -351,8 +351,11 @@ def cmd_ownir(path: str, fmt: str = "human", severity: str = "error",
     n = len(leaks)
     summary = f"\n{n} finding{'s' if n != 1 else ''}"
     if notes:
-        summary += (f" ({len(notes)} unchecked hidden)" if verbosity == "quiet"
-                    else f", {len(notes)} unchecked (OWN050)")
+        # the advisory band is no longer only OWN050 (OBL005 rides it too) —
+        # name the codes actually present instead of hardcoding one.
+        note_codes = "/".join(sorted({x.code for x in notes}))
+        summary += (f" ({len(notes)} advisory hidden)" if verbosity == "quiet"
+                    else f", {len(notes)} advisory ({note_codes})")
     print(summary + ".", file=summary_to)
     if verbosity == "verbose" and findings:
         by_code: dict[str, int] = {}

ownlang/diagnostics.py

@@ -8,6 +8,9 @@
   040-041  extern / call-boundary
   050      C# front-end resolution coverage (P-014; advisory, never a verdict)
 
+Sidecar analysis families carry their own prefixes (DI, EFF, OBL) — each is a
+separate analysis the OwnIR bridge routes facts to, not the core lattice.
+
 The split between *definite* (002 use-after-release, 005 use-after-move) and
 *maybe* (009, 010) codes is deliberate: a fault that holds on every path is a
 different, sharper message than one that holds on only some path through a
@@ -88,6 +91,12 @@ class Severity(Enum):
     "DI005": "disposable transient resolved from a long-lived scope (delayed disposal)",
     # ---- reactive-effect stability (P-020; a separate analysis, like DI001) ----
     "EFF001": "reactive effect re-runs on an unstable dependency identity (render-time IO storm)",
+    # ---- obligation protocols (P-025; a separate analysis, like DI001) ----
+    "OBL001": "obligation still open when a barrier fires (open on every path)",
+    "OBL002": "obligation may still be open when a barrier fires (open on some path)",
+    "OBL003": "obligation not closed before the method exits (on every path)",
+    "OBL004": "obligation may not be closed before the method exits (on some path)",
+    "OBL005": "protocol scope matched no reported method -- rule is dead (advisory)",
 }
 
 
@@ -178,6 +187,46 @@ class Severity(Enum):
         "Fix: resolve disposable transients within a short-lived scope you dispose, or manage "
         "their lifetime explicitly."
     ),
+    "OBL001": (
+        "A project-declared obligation protocol (e.g. \"`IsLoaded = false` must be closed by "
+        "`IsLoaded = true`\") is still open when a declared barrier fires — on every path that "
+        "reaches the barrier. The classic WPF shape: a method flips a consistency flag down, "
+        "rebuilds state, and raises `PropertyChanged(\"Document\")` before flipping the flag "
+        "back up, publishing an inconsistent object to bindings and listeners.\n"
+        "Fix: close the obligation before the barrier (move the closing assignment/call above "
+        "the notification), or — if that notification is genuinely safe while open — add it to "
+        "the protocol's `allow` list."
+    ),
+    "OBL002": (
+        "Like OBL001, but the obligation is open on only *some* paths that reach the barrier — "
+        "whether the notification publishes a broken object depends on the branch taken (the "
+        "same definite/maybe split as OWN002 vs OWN009).\n"
+        "Fix: close the obligation on every path before the barrier (or on none — make the "
+        "state unambiguous), or add the call to the protocol's `allow` list if it is genuinely "
+        "safe while open."
+    ),
+    "OBL003": (
+        "A project-declared obligation is opened but not closed before the method exits "
+        "(return / throw / falling off the end) on every path — the object is left in its "
+        "\"temporarily broken\" state for the outside world to observe. The exception path is "
+        "the classic culprit: `IsLoaded = false; Load(); IsLoaded = true;` leaves the flag down "
+        "forever when `Load()` throws.\n"
+        "Fix: close in a `finally`, or on every early-return path."
+    ),
+    "OBL004": (
+        "Like OBL003, but the obligation is left open on only *some* exit paths — whether the "
+        "object stays broken depends on the branch taken (typically an early return or a "
+        "may-throw call before the close).\n"
+        "Fix: close on every exit path — a `finally` covers the throw paths; move the close "
+        "above the early returns."
+    ),
+    "OBL005": (
+        "Advisory, not a verdict: a protocol's `scope.methods` matched none of the methods the "
+        "frontend reported events for — the rule is dead (usually a typo'd or renamed method "
+        "name). A silently dead project rule is worse than none: it reads as coverage that "
+        "does not exist.\n"
+        "Fix: correct the scope, or delete the rule."
+    ),
     "EFF001": (
         "A React `useEffect` re-runs whenever one of its declared dependencies changes identity. "
         "A dependency that is an object/array literal created in render scope gets a fresh "