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

A new sidecar analysis family (the di.py/effects.py pattern): project-declared
obligation protocols checked path-sensitively per method. An opening event
(IsLoaded = false) creates an obligation, a closing event discharges it, and it
must be closed before every declared barrier (OnPropertyChanged(Document)) and,
by default, every method exit (return / throw / end of body).

- ownlang/obligations.py: matchers, protocols, event trees (assign/call/return/
  throw/if/while), the {OPEN, CLOSED} set lattice with union joins (the
  definite/maybe split of OWN002 vs OWN009), local loop fixpoints with
  single-shot emission, open-site provenance, the opaque-write discharge
  asymmetry (may discharge, never invents), and explicit method scoping as the
  false-positive throttle.
- ownlang/ownir.py: additive OwnIR blocks protocols[]/protocol_functions[]
  (no version bump — the services/effects precedent; internal vocabularies are
  fail-loud per IR4, duplicate protocol names rejected at load),
  _protocol_findings beside _di_findings/_effect_findings, line-free messages
  (OwnAudit fingerprints on path|rule|message), evidence flow
  opened -> barrier -> late close (SARIF codeFlows).
- Codes OBL001-004 (barrier/exit x definite/maybe) + OBL005 (dead-scope
  advisory, never fails the build) in diagnostics.TITLES/EXPLANATIONS; the
  cmd_ownir summary now names the advisory codes present instead of
  hardcoding OWN050.
- spec/OwnIR.md §8 (Rules -> §9, Conformance -> §10) + ownir.schema.json
  $defs (protocol/protocolMatcher/protocolOpenClose/protocolEvent/
  protocolFunction), vocabularies pinned both ways by the tests.
- tests/test_obligations.py (70 checks) + killer-demo fixtures: OBL001 at
  BigDocumentViewModel.cs:241 (IsLoaded=false at 184, PropertyChanged(Document)
  at 241 on the warnings branch, closed only at 260), and its fixed twin
  staying silent.
- docs/proposals/P-025-obligation-protocols.md: decisions on the record, the
  Roslyn extractor emission slice (designed; extractor is CI-only), the
  MOS-based interprocedural phase, and non-goals.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NXzqX7Qwn5QzBLGVCATdgm

Author: claude

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:
+
+```
+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

@@ -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,31 @@ 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."
+    ),
+    "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."
+    ),
+    "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 "