From 9e779808fb91dd71b08fc7caa9979c472f697c5f Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 15:19:29 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat(obligations):=20obligation=20protocols?= =?UTF-8?q?=20=E2=80=94=20barrier-sensitive=20project=20invariants=20(P-02?= =?UTF-8?q?5,=20first=20slice)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01NXzqX7Qwn5QzBLGVCATdgm --- docs/ROADMAP.md | 1 + docs/proposals/P-025-obligation-protocols.md | 190 ++++++ docs/proposals/README.md | 1 + ownlang/__main__.py | 7 +- ownlang/diagnostics.py | 34 ++ ownlang/obligations.py | 564 ++++++++++++++++++ ownlang/ownir.py | 145 +++++ spec/OwnIR.md | 98 ++- spec/ownir.schema.json | 160 +++++ .../ownir/protocol_isloaded_clean.facts.json | 39 ++ .../protocol_isloaded_violation.facts.json | 39 ++ tests/test_obligations.py | 515 ++++++++++++++++ 12 files changed, 1785 insertions(+), 8 deletions(-) create mode 100644 docs/proposals/P-025-obligation-protocols.md create mode 100644 ownlang/obligations.py create mode 100644 tests/fixtures/ownir/protocol_isloaded_clean.facts.json create mode 100644 tests/fixtures/ownir/protocol_isloaded_violation.facts.json create mode 100644 tests/test_obligations.py diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index d81c6830..0cabf97f 100644 --- a/docs/ROADMAP.md +++ b/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) | diff --git a/docs/proposals/P-025-obligation-protocols.md b/docs/proposals/P-025-obligation-protocols.md new file mode 100644 index 00000000..5cf33a3c --- /dev/null +++ b/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)? diff --git a/docs/proposals/README.md b/docs/proposals/README.md index b811b47c..b382cd7f 100644 --- a/docs/proposals/README.md +++ b/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 diff --git a/ownlang/__main__.py b/ownlang/__main__.py index 900d6d04..ce628ee4 100644 --- a/ownlang/__main__.py +++ b/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] = {} diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py index 6b803b92..d0cecd77 100644 --- a/ownlang/diagnostics.py +++ b/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 " diff --git a/ownlang/obligations.py b/ownlang/obligations.py new file mode 100644 index 00000000..c0880387 --- /dev/null +++ b/ownlang/obligations.py @@ -0,0 +1,564 @@ +"""Obligation-protocol analysis — project-specific temporal invariants (P-025). + +A legacy method often breaks one of its *own* invariants on purpose, briefly: +`IsLoaded = false` while the document tree is rebuilt, `_suppressNotifications = +true` around a batch update, `BeginUpdate()` before a bulk edit. The invariant is +allowed to be false — *locally*. The bug is publishing that broken state to the +outside world: raising `PropertyChanged("Document")`, returning, or throwing +while the flag is still down. No general-purpose checker knows that `IsLoaded` +means "the document is consistent"; the project does. + +This analyzer checks exactly that shape, declared per project as an **obligation +protocol**: + + - an *opening* event creates the obligation (`IsLoaded = false`); + - a *closing* event discharges it (`IsLoaded = true`); + - a *barrier* is a point the obligation must not cross while open — a + configured call (`OnPropertyChanged("Document")`) or a method exit + (`return` / `throw` / falling off the end). + +Like `di.py` over the DI registration graph and `effects.py` over the +render-scope binding graph, this is its own small analysis the OwnIR bridge +feeds facts to — one checker, several analyses. The frontend (Roslyn extractor +or a hand-written fixture) only reports *what the method does*, as an ordered +event tree (`protocol_functions[]`); the protocol *rules* (`protocols[]`) are +project configuration; the verdict is decided here. + +The walk is path-sensitive over the structured event tree (`if`/`while` mirror +the flow-op shape of OwnIR §5): the obligation state is a **set** over +{OPEN, CLOSED} joined by union at merges, so the definite/maybe split falls out +of the lattice exactly as it does for OWN002 vs OWN009 in the core. Loops are +solved to a local fixpoint silently and their bodies re-walked once on the +converged header state, so a barrier inside a loop reports once — the same +two-phase emission discipline as `analysis._Analyzer`. + +Precision policy (the project's standing red line — never invent a violation): + + - an *opaque* write to a tracked flag (`IsLoaded = Compute()`) may discharge + the obligation but never creates one: if OPEN is possible the state gains + CLOSED (the write may have closed it), but a closed state stays closed; + - a call the protocol does not name is neutral — it neither discharges nor + crosses. A callee that flips the flag internally is invisible in v1 + (interprocedural obligation summaries are the P-025 phase-3 slice, on the + MOS channel of `ownership.py`); + - protocols are explicitly scoped (`scope.methods`) — a rule only ever fires + where the project asked for it. +""" +from __future__ import annotations + +from dataclasses import dataclass +from typing import Any + +# obligation state lattice: a set over {OPEN, CLOSED}, joined by union. +OPEN = "open" +CLOSED = "closed" + +# the closed event vocabulary of `protocol_functions[].events` — the `ev` +# discriminator. Mirrors the flow-op rule (OwnIR §5): a present-but-unknown +# value is rejected, never skipped (spec/ownir.schema.json pins this set). +EVENT_KINDS = frozenset({"assign", "call", "return", "throw", "if", "while"}) + +# matcher vocabulary for `opens`/`closes`/`barriers`/`allow`. +MATCHER_KINDS = frozenset({"assign", "call"}) + + +class ProtocolFactsError(ValueError): + """A malformed protocol/event fact. `load()` wraps this in `OwnIRError` + (fail-loud); the direct `check_facts` path skips the malformed entry + (defensive, mirroring `_effect_findings`).""" + + +# --------------------------------------------------------------------------- +# rule side: matchers and protocols (`protocols[]`) +# --------------------------------------------------------------------------- + +@dataclass(frozen=True) +class Matcher: + """One event pattern. `kind` selects the shape: + + - `assign`: matches an assign event with the same `target`; `value` + narrows to a specific written boolean (None = any value, including an + opaque one). + - `call`: matches a call event with the same `callee`; a non-empty `args` + narrows to calls whose distinguished argument is in the set (a call + with an *unknown* argument does not match a narrowed matcher — we do + not invent a barrier crossing we cannot prove). + """ + + kind: str + target: str = "" # assign: member name; call: callee name + value: bool | None = None # assign only + args: frozenset[str] = frozenset() # call only + + def matches(self, ev: AssignEv | CallEv) -> bool: + if self.kind == "assign" and isinstance(ev, AssignEv): + if ev.target != self.target: + return False + return self.value is None or ev.value is self.value + if self.kind == "call" and isinstance(ev, CallEv): + if ev.callee != self.target: + return False + if not self.args: + return True + return ev.arg is not None and ev.arg in self.args + return False + + def describe(self) -> str: + """A stable, line-free human phrase for messages ('IsLoaded = true', + 'EndUpdate()').""" + if self.kind == "assign": + if self.value is None: + return f"{self.target} = ..." + return f"{self.target} = {str(self.value).lower()}" + return f"{self.target}()" + + +@dataclass(frozen=True) +class Protocol: + """One project-declared obligation protocol (see the module docstring).""" + + name: str + opens: Matcher + closes: Matcher + barriers: tuple[Matcher, ...] = () + allow: tuple[Matcher, ...] = () + # `return` / `throw` / end-of-body are barriers too (the OWN001 shape: + # an obligation may not leak out of the method). + exit_barriers: bool = True + # explicit scope: method names the protocol applies to (exact, or a + # trailing `Type.Method` suffix so fixtures need not spell namespaces). + # Empty = every method that reports events. Tight scoping is the false- + # positive control: a rule only fires where the project asked. + methods: tuple[str, ...] = () + description: str = "" + + def applies_to(self, fn_name: str) -> bool: + if not self.methods: + return True + return any(fn_name == m or fn_name.endswith("." + m) for m in self.methods) + + def tracks_target(self, target: str) -> bool: + """Is `target` one of the flags whose assigns drive this protocol? + (Used for the opaque-write discharge rule.)""" + return any(m.kind == "assign" and m.target == target + for m in (self.opens, self.closes)) + + +# --------------------------------------------------------------------------- +# fact side: the ordered event tree (`protocol_functions[]`) +# --------------------------------------------------------------------------- + +@dataclass(frozen=True) +class AssignEv: + target: str + value: bool | None # None = opaque (the frontend saw a non-literal RHS) + line: int + + +@dataclass(frozen=True) +class CallEv: + callee: str + arg: str | None # the distinguished argument (nameof/string literal), if known + line: int + + +@dataclass(frozen=True) +class ReturnEv: + line: int + + +@dataclass(frozen=True) +class ThrowEv: + line: int + + +@dataclass(frozen=True) +class IfEv: + line: int + then: tuple[Event, ...] + orelse: tuple[Event, ...] + + +@dataclass(frozen=True) +class WhileEv: + line: int + body: tuple[Event, ...] + + +Event = AssignEv | CallEv | ReturnEv | ThrowEv | IfEv | WhileEv + + +@dataclass(frozen=True) +class MethodEvents: + """One method's ordered event tree, as reported by a frontend.""" + + name: str + file: str + events: tuple[Event, ...] + + +# --------------------------------------------------------------------------- +# parsing (shared by load()'s fail-loud gate and the defensive bridge path) +# --------------------------------------------------------------------------- + +def _require_str(raw: dict[str, Any], key: str, ctx: str) -> str: + v = raw.get(key) + if not isinstance(v, str) or not v: + raise ProtocolFactsError(f"{ctx}: '{key}' must be a non-empty string, got {v!r}") + return v + + +def _opt_line(raw: dict[str, Any], ctx: str) -> int: + v = raw.get("line", 0) + if not isinstance(v, int) or isinstance(v, bool): + raise ProtocolFactsError(f"{ctx}: 'line' must be an integer, got {v!r}") + return v + + +def parse_matcher(raw: Any, ctx: str, require_value: bool = False) -> Matcher: + """Parse one matcher object. `require_value` is set for `opens`/`closes` + assign matchers: an open/close condition must name the written boolean — + 'any write opens' is not a checkable protocol.""" + if not isinstance(raw, dict): + raise ProtocolFactsError(f"{ctx} must be an object, got {raw!r}") + kind = raw.get("kind") + if kind not in MATCHER_KINDS: + raise ProtocolFactsError( + f"{ctx}: unknown matcher kind {kind!r} — the vocabulary is " + f"{sorted(MATCHER_KINDS)} (spec/OwnIR.md §8)") + if kind == "assign": + target = _require_str(raw, "target", ctx) + value = raw.get("value") + if value is not None and not isinstance(value, bool): + raise ProtocolFactsError( + f"{ctx}: assign 'value' must be a boolean, got {value!r}") + if require_value and value is None: + raise ProtocolFactsError( + f"{ctx}: an opens/closes assign matcher must state the written " + f"boolean 'value' — 'any write' cannot open or close an obligation") + return Matcher(kind="assign", target=target, value=value) + callee = _require_str(raw, "callee", ctx) + args_raw = raw.get("args", []) + if not isinstance(args_raw, list) or not all(isinstance(a, str) for a in args_raw): + raise ProtocolFactsError(f"{ctx}: call 'args' must be an array of strings") + return Matcher(kind="call", target=callee, args=frozenset(args_raw)) + + +def parse_protocol(raw: Any) -> Protocol: + """Parse one `protocols[]` entry, fail-loud on any shape violation.""" + if not isinstance(raw, dict): + raise ProtocolFactsError(f"a protocol must be an object, got {raw!r}") + name = _require_str(raw, "name", "protocol") + ctx = f"protocol '{name}'" + if "opens" not in raw or "closes" not in raw: + raise ProtocolFactsError(f"{ctx}: 'opens' and 'closes' are both required") + opens = parse_matcher(raw["opens"], f"{ctx} 'opens'", require_value=True) + closes = parse_matcher(raw["closes"], f"{ctx} 'closes'", require_value=True) + barriers_raw = raw.get("barriers", []) + if not isinstance(barriers_raw, list): + raise ProtocolFactsError(f"{ctx}: 'barriers' must be an array") + barriers = tuple(parse_matcher(b, f"{ctx} barrier") for b in barriers_raw) + allow_raw = raw.get("allow", []) + if not isinstance(allow_raw, list): + raise ProtocolFactsError(f"{ctx}: 'allow' must be an array") + allow = tuple(parse_matcher(a, f"{ctx} allow") for a in allow_raw) + exit_barriers = raw.get("exit_barriers", True) + if not isinstance(exit_barriers, bool): + raise ProtocolFactsError(f"{ctx}: 'exit_barriers' must be a boolean") + if not barriers and not exit_barriers: + raise ProtocolFactsError( + f"{ctx}: no barriers and exit_barriers is false — the protocol can " + f"never fire (a rule that structurally never fires is decoration)") + if opens in barriers: + # the walk checks opens before barriers, so this barrier is silently + # dead — the same never-fires rule as above. (A barrier equal to + # `closes` is merely redundant: the close discharges at that point, + # which is exactly what the barrier asks for.) Re-entrancy rules + # ("BeginUpdate while already updating") are a later feature, not a + # silently ignored config. + raise ProtocolFactsError( + f"{ctx}: a barrier equals the 'opens' matcher — the open wins and " + f"the barrier can never fire (re-entrancy checks are not " + f"supported yet)") + scope = raw.get("scope", {}) + if not isinstance(scope, dict): + raise ProtocolFactsError(f"{ctx}: 'scope' must be an object") + methods_raw = scope.get("methods", []) + if not isinstance(methods_raw, list) or not all( + isinstance(m, str) and m for m in methods_raw): + raise ProtocolFactsError( + f"{ctx}: 'scope.methods' must be an array of non-empty strings") + desc = raw.get("description", "") + if not isinstance(desc, str): + raise ProtocolFactsError(f"{ctx}: 'description' must be a string") + return Protocol(name=name, opens=opens, closes=closes, barriers=barriers, + allow=allow, exit_barriers=exit_barriers, + methods=tuple(methods_raw), description=desc) + + +def parse_events(raw: Any, ctx: str) -> tuple[Event, ...]: + """Parse an ordered event list (recursive over `if`/`while`), fail-loud on + an unknown `ev` — the same rule as an unknown flow op (OwnIR IR4).""" + if not isinstance(raw, list): + raise ProtocolFactsError(f"{ctx}: events must be an array, got {raw!r}") + out: list[Event] = [] + for e in raw: + if not isinstance(e, dict): + raise ProtocolFactsError(f"{ctx}: each event must be an object, got {e!r}") + ev = e.get("ev") + if ev not in EVENT_KINDS: + raise ProtocolFactsError( + f"{ctx}: unknown protocol event {ev!r} — the vocabulary is " + f"{sorted(EVENT_KINDS)} (spec/OwnIR.md §8)") + line = _opt_line(e, ctx) + if ev == "assign": + target = _require_str(e, "target", f"{ctx} assign") + value = e.get("value") + if value is not None and not isinstance(value, bool): + raise ProtocolFactsError( + f"{ctx}: assign 'value' must be a boolean or absent " + f"(absent = opaque write), got {value!r}") + out.append(AssignEv(target=target, value=value, line=line)) + elif ev == "call": + callee = _require_str(e, "callee", f"{ctx} call") + arg = e.get("arg") + if arg is not None and not isinstance(arg, str): + raise ProtocolFactsError( + f"{ctx}: call 'arg' must be a string or absent, got {arg!r}") + out.append(CallEv(callee=callee, arg=arg, line=line)) + elif ev == "return": + out.append(ReturnEv(line=line)) + elif ev == "throw": + out.append(ThrowEv(line=line)) + elif ev == "if": + out.append(IfEv(line=line, + then=parse_events(e.get("then", []), ctx), + orelse=parse_events(e.get("else", []), ctx))) + else: # "while" — EVENT_KINDS is closed, checked above + out.append(WhileEv(line=line, body=parse_events(e.get("body", []), ctx))) + return tuple(out) + + +def parse_method(raw: Any) -> MethodEvents: + """Parse one `protocol_functions[]` entry.""" + if not isinstance(raw, dict): + raise ProtocolFactsError(f"a protocol function must be an object, got {raw!r}") + name = _require_str(raw, "name", "protocol function") + file = raw.get("file", "?") + if not isinstance(file, str): + raise ProtocolFactsError(f"protocol function '{name}': 'file' must be a string") + events = parse_events(raw.get("events", []), f"protocol function '{name}'") + return MethodEvents(name=name, file=file, events=events) + + +# --------------------------------------------------------------------------- +# the checker +# --------------------------------------------------------------------------- + +@dataclass(frozen=True) +class Violation: + """One obligation-protocol violation, ready for the bridge to phrase. + + `line` anchors where the violation manifests: the barrier site for a + `barrier`/`return`/`throw` crossing, the *open* site for an obligation + leaking off the end of the method (the OWN001 precedent: a leak anchors at + the acquire). `definite` is the lattice split: True when the obligation is + open on *every* path reaching the point, False when only on some path. + `close_line` is the earliest close site after `line`, if one exists — the + "closed only here, after the barrier" evidence hop.""" + + protocol: str + method: str + file: str + line: int + kind: str # "barrier" | "exit" + definite: bool + open_line: int + barrier_desc: str # "OnPropertyChanged(Document)" | "return" | "throw" | "end of method" + close_line: int | None = None + + +# a path state: which obligation states are possible, plus the earliest open +# site among the paths where it is open (evidence provenance, min-line joined +# like analysis._join_sites). +_State = tuple[frozenset[str], int | None] + +_BOTTOM: _State = (frozenset(), None) + + +def _join(a: _State, b: _State) -> _State: + states = a[0] | b[0] + lines = [ln for ln in (a[1], b[1]) if ln is not None] + return (states, min(lines) if lines else None) + + +class _Walker: + """Path-sensitive walk of one method's event tree against one protocol. + + Sequences and branches are walked exactly once (the emitting pass); a loop + body is iterated to a fixpoint with emission off, then re-walked once on + the converged header state — the two-phase discipline of the core + analyzer, applied per loop.""" + + def __init__(self, proto: Protocol, method: MethodEvents) -> None: + self.proto = proto + self.method = method + self.silent = False + self.violations: list[Violation] = [] + + # -- event handling ---------------------------------------------------- + + def _emit(self, kind: str, line: int, st: _State, desc: str) -> None: + if self.silent: + return + states, open_line = st + self.violations.append(Violation( + protocol=self.proto.name, method=self.method.name, + file=self.method.file, line=line, kind=kind, + definite=(states == frozenset({OPEN})), + open_line=open_line if open_line is not None else line, + barrier_desc=desc)) + + def _leaf(self, ev: AssignEv | CallEv, st: _State) -> _State: + p = self.proto + if p.opens.matches(ev): + # (re-)open: keep the earliest open site as provenance. + prev = st[1] + return (frozenset({OPEN}), + ev.line if prev is None else min(prev, ev.line)) + if p.closes.matches(ev): + return (frozenset({CLOSED}), None) + states, open_line = st + if OPEN in states: + # allow beats barrier: an explicitly safe event never crosses. + if not any(a.matches(ev) for a in p.allow): + for b in p.barriers: + if b.matches(ev): + desc = (f"{ev.callee}({ev.arg or ''})" + if isinstance(ev, CallEv) else ev.target + " = ...") + self._emit("barrier", ev.line, st, desc) + break + # opaque write to a tracked flag: may discharge, never opens + # (the never-invent asymmetry — see the module docstring). + if (isinstance(ev, AssignEv) and ev.value is None + and p.tracks_target(ev.target)): + return (states | {CLOSED}, open_line) + return st + + def _exit(self, line: int, st: _State, desc: str) -> None: + if self.proto.exit_barriers and OPEN in st[0]: + self._emit("exit", line, st, desc) + + # -- tree walk ----------------------------------------------------------- + + def walk_seq(self, events: tuple[Event, ...], st: _State) -> tuple[_State, bool]: + """Returns (state, alive): alive is False when every path through the + sequence has already left the method.""" + alive = True + for ev in events: + st, alive = self.walk(ev, st) + if not alive: + break + return st, alive + + def walk(self, ev: Event, st: _State) -> tuple[_State, bool]: + if isinstance(ev, (AssignEv, CallEv)): + return self._leaf(ev, st), True + if isinstance(ev, ReturnEv): + self._exit(ev.line, st, "return") + return _BOTTOM, False + if isinstance(ev, ThrowEv): + self._exit(ev.line, st, "throw") + return _BOTTOM, False + if isinstance(ev, IfEv): + s1, a1 = self.walk_seq(ev.then, st) + s2, a2 = self.walk_seq(ev.orelse, st) + if not a1 and not a2: + return _BOTTOM, False + merged = _join(s1 if a1 else _BOTTOM, s2 if a2 else _BOTTOM) + return merged, True + if isinstance(ev, WhileEv): + # local fixpoint on the header state, silently (finite lattice: + # states only grow under union, so this terminates). + header = st + was_silent = self.silent + self.silent = True + while True: + out, body_alive = self.walk_seq(ev.body, header) + nxt = _join(header, out if body_alive else _BOTTOM) + if nxt == header: + break + header = nxt + self.silent = was_silent + # one emitting pass over the body on the converged header state + # (skipped when an enclosing loop is still in its silent phase). + if not self.silent: + self.walk_seq(ev.body, header) + # zero iterations are always possible: the exit state is the header. + return header, True + raise AssertionError(f"unhandled protocol event {ev!r}") + + def run(self) -> list[Violation]: + st, alive = self.walk_seq(self.method.events, (frozenset({CLOSED}), None)) + if alive: + states, open_line = st + if self.proto.exit_barriers and OPEN in states: + # anchor the leak at the open site (the OWN001 precedent). + anchor = open_line if open_line is not None else 0 + self._emit("exit", anchor, st, "end of method") + return self.violations + + +def _close_lines(proto: Protocol, events: tuple[Event, ...]) -> list[int]: + """Every close-event line in the tree, reachability ignored — evidence for + the 'closed only here, after the barrier' hop.""" + out: list[int] = [] + for ev in events: + if isinstance(ev, (AssignEv, CallEv)): + if proto.closes.matches(ev): + out.append(ev.line) + elif isinstance(ev, IfEv): + out.extend(_close_lines(proto, ev.then)) + out.extend(_close_lines(proto, ev.orelse)) + elif isinstance(ev, WhileEv): + out.extend(_close_lines(proto, ev.body)) + return out + + +def check_protocols(protocols: list[Protocol], + methods: list[MethodEvents]) -> list[Violation]: + """Check every protocol against every method in its scope. Deterministic; + sorted by location.""" + out: list[Violation] = [] + for proto in protocols: + for method in methods: + if not proto.applies_to(method.name): + continue + violations = _Walker(proto, method).run() + if violations: + closes = sorted(_close_lines(proto, method.events)) + for v in violations: + # the late-close evidence hop only makes sense for a + # barrier crossing ("the close exists, but after the + # publish"); an exit leak has no barrier to be late for. + late = (next((c for c in closes if c > v.line), None) + if v.kind == "barrier" else None) + if late is not None: + v = Violation( + protocol=v.protocol, method=v.method, file=v.file, + line=v.line, kind=v.kind, definite=v.definite, + open_line=v.open_line, barrier_desc=v.barrier_desc, + close_line=late) + out.append(v) + out.sort(key=lambda v: (v.file, v.line, v.protocol, v.barrier_desc)) + return out + + +def unmatched_scopes(protocols: list[Protocol], + methods: list[MethodEvents]) -> list[Protocol]: + """Protocols whose scope matched no reported method — a dead rule (likely a + typo'd scope). Surfaced as an advisory, never a verdict: a rule that + structurally never fires is decoration, and silently dead project rules are + worse than none.""" + return [p for p in protocols + if p.methods and not any(p.applies_to(m.name) for m in methods)] diff --git a/ownlang/ownir.py b/ownlang/ownir.py index ff6cac15..6aee86cf 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -146,6 +146,16 @@ from .effects import Effect as ReactEffect from .effects import find_effect_storms from .evidence import code_flow, di_path_steps +from .obligations import ( + MethodEvents, + Protocol, + ProtocolFactsError, + Violation, + check_protocols, + parse_method, + parse_protocol, + unmatched_scopes, +) from .ownership import ( MethodSkeleton, ParamSkeleton, @@ -642,6 +652,37 @@ def load(path: str) -> dict[str, Any]: raise OwnIRError( f"parameter 'effect' must be one of {sorted(_PARAM_EFFECTS)}, " f"got {peff!r}") + # Optional obligation protocols (OBL001-005 — P-025). Additive/optional like + # `services`/`effects`: an older core ignores both blocks. Their internal + # vocabularies (matcher kinds, the `ev` discriminator) are fail-loud like a + # flow op (IR4): a present-but-unknown value is rejected at load, never + # skipped. The shared parser (ownlang/obligations.py) is the single shape + # authority for both this gate and the bridge path. + protos = result.get("protocols", []) + if not isinstance(protos, list): + raise OwnIRError("OwnIR 'protocols' must be a JSON array of objects") + proto_names: set[str] = set() + for praw in protos: + try: + parsed = parse_protocol(praw) + except ProtocolFactsError as e: + raise OwnIRError(str(e)) from e + # the name is the identity the bridge maps verdicts back by (the + # handle rule, IR5) — two protocols sharing one name would make that + # mapping ambiguous and can collapse distinct findings in the dedup. + if parsed.name in proto_names: + raise OwnIRError( + f"duplicate protocol name '{parsed.name}' — protocol names " + f"are the identity findings map back by and must be unique") + proto_names.add(parsed.name) + pfns = result.get("protocol_functions", []) + if not isinstance(pfns, list): + raise OwnIRError("OwnIR 'protocol_functions' must be a JSON array of objects") + for fraw in pfns: + try: + parse_method(fraw) + except ProtocolFactsError as e: + raise OwnIRError(str(e)) from e return result @@ -2196,6 +2237,13 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: # syntactically is — the stability verdict is the core's. findings.extend(_effect_findings(facts)) + # OBL001-005 (obligation protocols, P-025): a separate path-sensitive core + # analysis over the project-declared protocol rules and per-method event + # trees (ownlang/obligations.py), NOT the acquire/release model. The bridge + # routes the optional `protocols`/`protocol_functions` facts to it; the + # frontend only reports what the method does — the verdict is the core's. + findings.extend(_protocol_findings(facts)) + # OWN050 (P-014 Tier A): a `+=` whose declaring type could not be resolved — # an advisory "leakage analysis skipped" note, never a leak. Routed through # this side path so it bypasses the ERROR-only diagnostic mapping above. @@ -2463,6 +2511,103 @@ def _effect_findings(facts: dict[str, Any]) -> list[Finding]: return out +_OBL_CODE = { + # (kind, definite) -> code: the definite/maybe split is the same lattice + # story as OWN002 vs OWN009 — open on every path vs open on some path. + ("barrier", True): "OBL001", + ("barrier", False): "OBL002", + ("exit", True): "OBL003", + ("exit", False): "OBL004", +} + + +def _protocol_message(v: Violation, proto: Protocol) -> str: + """The finding message. Deliberately line-free: OwnAudit fingerprints + findings on (path, rule, message), so a line number here would break the + baseline ratchet and the FP-judge overlay on every unrelated edit. The + lines live in the evidence slice instead.""" + close = proto.closes.describe() + if v.kind == "barrier": + state = ("is still open" if v.definite + else "may still be open (open on some path)") + return (f"obligation '{v.protocol}' {state} when barrier " + f"'{v.barrier_desc}' fires in '{v.method}' — '{close}' must " + f"happen first") + state = ("is not closed" if v.definite + else "may not be closed (open on some path)") + exit_desc = ("the method falls off the end" if v.barrier_desc == "end of method" + else f"'{v.method}' exits via {v.barrier_desc}") + return (f"obligation '{v.protocol}' {state} when {exit_desc} — the object " + f"is published in its in-between state; close with '{close}' on " + f"every path (a finally block covers the throw paths)") + + +def _protocol_findings(facts: dict[str, Any]) -> list[Finding]: + """Run the obligation-protocol check over the facts' `protocols` / + `protocol_functions` blocks and map each violation to a Finding at its C# + location (ownlang/obligations.py). Additive/optional, like `services` and + `effects`: absent blocks -> no findings. Entries are re-validated here and + a malformed one is SKIPPED (not coerced) — load() already fail-louds on + this, but the direct check_facts() path (tests / embedders) never went + through load().""" + raw_protos = facts.get("protocols", []) + raw_fns = facts.get("protocol_functions", []) + if not isinstance(raw_protos, list) or not isinstance(raw_fns, list): + return [] + protocols: list[Protocol] = [] + for praw in raw_protos: + try: + parsed = parse_protocol(praw) + except ProtocolFactsError: + continue + # a duplicate name is rejected by load(); on the direct path skip the + # later one (first wins, deterministically) — the name is the identity + # the violation->protocol re-pairing below relies on. + if any(p.name == parsed.name for p in protocols): + continue + protocols.append(parsed) + methods: list[MethodEvents] = [] + for fraw in raw_fns: + try: + methods.append(parse_method(fraw)) + except ProtocolFactsError: + continue + if not protocols: + return [] + out: list[Finding] = [] + for v in check_protocols(protocols, methods): + proto = next(p for p in protocols if p.name == v.protocol) + component = v.method.rsplit(".", 2)[-2] if "." in v.method else v.method + opened = proto.opens.describe() + flow: list[tuple[int, str]] = [ + (v.open_line, f"obligation '{v.protocol}' opens here ({opened})")] + if v.kind == "barrier": + flow.append((v.line, f"barrier '{v.barrier_desc}' fires while it is open")) + elif v.line != v.open_line: + flow.append((v.line, f"the method exits here via {v.barrier_desc} " + f"while it is open")) + if v.close_line is not None: + flow.append((v.close_line, + "closed here — after the barrier has already fired")) + out.append(Finding( + file=v.file, line=v.line, code=_OBL_CODE[(v.kind, v.definite)], + component=component, event=v.protocol, + handler=v.method.rsplit(".", 1)[-1], + message=_protocol_message(v, proto), + kind="protocol obligation", + flow=tuple((v.file, ln, label) for ln, label in flow if ln >= 1))) + # a scoped protocol that matched no reported method is a dead rule — + # surface it honestly (advisory, never fails the build), like OWN050. + for p in unmatched_scopes(protocols, methods): + out.append(Finding( + file="?", line=0, code="OBL005", component="?", event=p.name, + handler="", advisory=True, kind="protocol obligation", + message=(f"protocol '{p.name}' is scoped to " + f"{sorted(p.methods)} but no reported method matches — " + f"the rule is dead (typo in scope.methods?)"))) + return out + + def _unresolved_findings(facts: dict[str, Any]) -> list[Finding]: """Surface every "unresolved-subscription" marker as an advisory OWN050 finding (P-014 Tier A): the extractor saw a `+=` that looks like an event diff --git a/spec/OwnIR.md b/spec/OwnIR.md index ce806edc..725ce186 100644 --- a/spec/OwnIR.md +++ b/spec/OwnIR.md @@ -2,7 +2,7 @@ > **Status: normative, descriptive.** This document specifies the OwnIR fact > contract *as it is today*, derived from the working bridge -> (`ownlang/ownir.py`) and pinned by tests (see [§9 Conformance](#9-conformance)). +> (`ownlang/ownir.py`) and pinned by tests (see [§10 Conformance](#10-conformance)). > Forward-looking ideas live in [`docs/proposals/`](../docs/proposals/), never > here. @@ -24,12 +24,14 @@ A facts document is a single JSON object: "components": [ /* §4 owned-resource records, grouped by type */ ], "functions": [ /* §5 flow bodies (intra-procedural CFG facts) */ ], "services": [ /* §6 DI registration graph */ ], - "effects": [ /* §7 reactive-effect graph (EFF001) */ ] + "effects": [ /* §7 reactive-effect graph (EFF001) */ ], + "protocols": [ /* §8 obligation protocols (OBL001-005): rules */ ], + "protocol_functions": [ /* §8 obligation protocols: per-method events */ ] } ``` -`ownir_version` (int) and `module` (string) are required; `components`, -`functions`, `services`, and `effects` are each optional and default to empty. +`ownir_version` (int) and `module` (string) are required; every other top-level +block is optional and defaults to empty. `load()` ([`ownir.py`](../ownlang/ownir.py)) validates the shape and raises `OwnIRError` (a `ValueError`) with an actionable message on any violation — types, the `bool`-is-`int` trap, empty identity strings, unknown DI lifetime enums, and @@ -176,7 +178,87 @@ dep is unstable is EFF001 (the effect storm — "not all lifecycle bugs leak mem some leak requests"). Like `services`, this block is additive/optional; the core decides identity stability, not the frontend. -## 8. Rules +## 8. Obligation protocols (`protocols[]` / `protocol_functions[]`) + +Two optional top-level arrays feeding the **OBL001–OBL005** obligation-protocol +checks (P-025) — a separate path-sensitive core analysis +([`ownlang/obligations.py`](../ownlang/obligations.py)) for *project-specific +temporal invariants*: a method briefly breaks one of its own invariants +(`IsLoaded = false` while the document rebuilds) and must restore it before a +*barrier* — a configured call (`OnPropertyChanged("Document")`) or a method +exit. The general checker cannot know that `IsLoaded` means "the document is +consistent"; the project declares it. + +`protocols[]` is the **rule side** (project configuration): + +```json +"protocols": [ + {"name": "DocumentLoading", + "opens": {"kind": "assign", "target": "IsLoaded", "value": false}, + "closes": {"kind": "assign", "target": "IsLoaded", "value": true}, + "barriers": [{"kind": "call", "callee": "OnPropertyChanged", + "args": ["Document", "Rows", "Totals"]}], + "allow": [{"kind": "call", "callee": "OnPropertyChanged", + "args": ["IsLoaded", "IsBusy", "Progress"]}], + "exit_barriers": true, + "scope": {"methods": ["BigDocumentViewModel.LoadBigDocument"]}} +] +``` + +`opens`/`closes` are required matchers (`assign` with a stated boolean `value`, +or `call`); `barriers` lists the events the obligation must not cross while +open (`allow` exempts explicitly safe ones); `exit_barriers` (default `true`) +makes `return`/`throw`/end-of-body barriers too; `scope.methods` restricts the +rule to named methods (exact, or a trailing `Type.Method` suffix). Tight +scoping is the false-positive control: a rule only fires where the project +asked. A scoped protocol matching no reported method is surfaced as the +advisory **OBL005** (a dead rule), never a verdict. + +`protocol_functions[]` is the **fact side** — one ordered event tree per +method, in the flow-body shape of §5 (`if`/`while` nest; frontends thread +`finally` bodies onto exits exactly like the flow lowering): + +```json +"protocol_functions": [ + {"name": "Broker.BigDocumentViewModel.LoadBigDocument", + "file": "BigDocumentViewModel.cs", + "events": [ + {"ev": "assign", "target": "IsLoaded", "value": false, "line": 184}, + {"ev": "if", "line": 220, "then": [ + {"ev": "call", "callee": "OnPropertyChanged", "arg": "Document", "line": 241} + ], "else": []}, + {"ev": "assign", "target": "IsLoaded", "value": true, "line": 260} + ]} +] +``` + +The event vocabulary is `assign` / `call` / `return` / `throw` / `if` / +`while` — closed and fail-loud like a flow op (IR4): a present-but-unknown +`ev` or matcher `kind` is rejected at load. Both blocks are additive/optional +(an older core ignores them — the IR3 additive rule), and their internal +vocabularies version *with the blocks*: extending them is a vocabulary change +under IR3/IR4. + +The obligation state is a set over {OPEN, CLOSED} joined by union at merges, +so the definite/maybe split (OBL001/OBL003 vs OBL002/OBL004) falls out of the +lattice the same way OWN002 vs OWN009 does. Precision rules (normative): + +- an **opaque write** to a tracked flag (`"value"` absent) may *discharge* an + open obligation but never *creates* one — the checker never invents a + violation; +- a **call the protocol does not name is neutral** (no discharge, no + crossing); interprocedural obligation summaries are a later slice (P-025); +- a call with an **unknown argument** does not match an args-narrowed barrier. + +Findings anchor at the barrier site (OBL001/002, and OBL003/004 for +`return`/`throw`) or at the *open* site for an obligation leaking off the end +of the method (the OWN001 anchor-at-acquire precedent), and carry an ordered +evidence slice: *opened here → barrier fired here (→ closed only here, after +the barrier)*. Messages are deliberately line-free so baseline ratchets and +FP-judge overlays that fingerprint on (path, rule, message) survive unrelated +edits. + +## 9. Rules - **IR1.** `ownir_version` must equal the core's `OWNIR_VERSION` (or be absent); otherwise `load()` raises `OwnIRError`. @@ -190,7 +272,7 @@ decides identity stability, not the frontend. never a silently dropped verdict. - **IR6.** A frontend emits facts only; all verdicts come from the core. -## 9. Conformance +## 10. Conformance Pinned by [`tests/test_ownir.py`](../tests/test_ownir.py) (the bridge suite, `python tests/test_ownir.py`), not `test_spec.py` (OwnIR is a bridge contract, @@ -206,6 +288,10 @@ not a surface-language rule): "cannot map back" instead of reporting the leak), not a dedicated raise-test. - **§4/§5/§6/§7** — the resource-kind, flow-op, DI, and effect fixtures (`tests/fixtures/ownir/*.facts.json`) each assert their expected code. +- **§8** — pinned by [`tests/test_obligations.py`](../tests/test_obligations.py): + the event/matcher vocabularies are bound to the schema's `protocolEvent`/ + `protocolMatcher` consts both ways, an unknown `ev`/`kind` raises at load, + and the `protocol_isloaded_*` fixtures assert the OBL codes end-to-end. A change to this spec without a matching change under `tests/test_ownir.py` (or vice-versa) is a red build. diff --git a/spec/ownir.schema.json b/spec/ownir.schema.json index 9e500b3b..ff5b6fea 100644 --- a/spec/ownir.schema.json +++ b/spec/ownir.schema.json @@ -33,6 +33,16 @@ "description": "The reactive-effect graph feeding the EFF001 effect-storm check (spec/OwnIR.md §7).", "type": "array", "items": { "$ref": "#/$defs/effect" } + }, + "protocols": { + "description": "Project-declared obligation protocols feeding the OBL001-005 checks (spec/OwnIR.md §8) — the rule side of the pair; the event side is protocol_functions.", + "type": "array", + "items": { "$ref": "#/$defs/protocol" } + }, + "protocol_functions": { + "description": "Per-method ordered obligation-event trees the protocols are checked against (spec/OwnIR.md §8) — the fact side of the pair.", + "type": "array", + "items": { "$ref": "#/$defs/protocolFunction" } } }, "$defs": { @@ -296,6 +306,156 @@ "refs": { "type": "array", "items": { "type": "string" } }, "line": { "type": "integer" } } + }, + "protocolMatcher": { + "description": "One event pattern for barriers/allow (spec/OwnIR.md §8); opens/closes use the stricter protocolOpenClose variant. The `kind` discriminator is a closed vocabulary pinned to ownlang/obligations.py::MATCHER_KINDS by tests/test_obligations.py; an unknown kind is rejected at load (IR4).", + "type": "object", + "required": ["kind"], + "oneOf": [ + { + "title": "assign", + "description": "Matches an assign event on `target`; `value` narrows to a written boolean (null/absent = any written value).", + "properties": { + "kind": { "const": "assign" }, + "target": { "type": "string", "minLength": 1 }, + "value": { "type": ["boolean", "null"] } + }, + "required": ["kind", "target"] + }, + { + "title": "call", + "description": "Matches a call event on `callee`; a non-empty `args` narrows to calls whose distinguished argument is in the set (a call with an unknown argument does not match a narrowed matcher — never invent a crossing).", + "properties": { + "kind": { "const": "call" }, + "callee": { "type": "string", "minLength": 1 }, + "args": { "type": "array", "items": { "type": "string" } } + }, + "required": ["kind", "callee"] + } + ] + }, + "protocolOpenClose": { + "description": "The opens/closes matcher: like protocolMatcher, but an assign variant MUST state the written boolean `value` — 'any write' cannot open or close an obligation (ownlang/obligations.py::parse_matcher require_value).", + "type": "object", + "required": ["kind"], + "oneOf": [ + { + "title": "assign", + "properties": { + "kind": { "const": "assign" }, + "target": { "type": "string", "minLength": 1 }, + "value": { "type": "boolean" } + }, + "required": ["kind", "target", "value"] + }, + { + "title": "call", + "properties": { + "kind": { "const": "call" }, + "callee": { "type": "string", "minLength": 1 }, + "args": { "type": "array", "items": { "type": "string" } } + }, + "required": ["kind", "callee"] + } + ] + }, + "protocol": { + "description": "One obligation protocol (spec/OwnIR.md §8): `opens` creates the obligation, `closes` discharges it, `barriers` are points it must not cross while open, `allow` exempts explicitly safe events from barrier matching, `exit_barriers` (default true) makes return/throw/end-of-body barriers too. `scope.methods` restricts the rule to named methods (exact, or trailing 'Type.Method' suffix) — tight scoping is the false-positive control. Parser-enforced beyond this schema (ownlang/obligations.py::parse_protocol): protocol names must be unique per document, `barriers` may not be empty while `exit_barriers` is false (the rule could never fire), and a barrier equal to `opens` is rejected (silently dead).", + "type": "object", + "required": ["name", "opens", "closes"], + "properties": { + "name": { "type": "string", "minLength": 1 }, + "description": { "type": "string" }, + "opens": { "$ref": "#/$defs/protocolOpenClose" }, + "closes": { "$ref": "#/$defs/protocolOpenClose" }, + "barriers": { "type": "array", "items": { "$ref": "#/$defs/protocolMatcher" } }, + "allow": { "type": "array", "items": { "$ref": "#/$defs/protocolMatcher" } }, + "exit_barriers": { "type": "boolean", "default": true }, + "scope": { + "type": "object", + "properties": { + "methods": { "type": "array", "items": { "type": "string", "minLength": 1 } } + } + } + } + }, + "protocolEvent": { + "description": "One ordered obligation event (spec/OwnIR.md §8). The `ev` discriminator is the complete vocabulary ownlang/obligations.py::parse_events handles, pinned to EVENT_KINDS by tests/test_obligations.py; any other value is rejected at load (fail-loud, the flow-op rule).", + "type": "object", + "required": ["ev"], + "oneOf": [ + { + "title": "assign", + "description": "A member/flag assignment; a null/absent `value` is an opaque write (non-literal RHS) — it may discharge an open obligation but never creates one.", + "properties": { + "ev": { "const": "assign" }, + "target": { "type": "string", "minLength": 1 }, + "value": { "type": ["boolean", "null"] }, + "line": { "type": "integer" } + }, + "required": ["ev", "target"] + }, + { + "title": "call", + "description": "An invocation; `arg` is the distinguished argument (a nameof()/string literal), null/absent when unknown.", + "properties": { + "ev": { "const": "call" }, + "callee": { "type": "string", "minLength": 1 }, + "arg": { "type": ["string", "null"] }, + "line": { "type": "integer" } + }, + "required": ["ev", "callee"] + }, + { + "title": "return", + "description": "A normal method exit.", + "properties": { + "ev": { "const": "return" }, + "line": { "type": "integer" } + }, + "required": ["ev"] + }, + { + "title": "throw", + "description": "An exceptional method exit. Frontends thread finally bodies onto exits, like the flow lowering (§5).", + "properties": { + "ev": { "const": "throw" }, + "line": { "type": "integer" } + }, + "required": ["ev"] + }, + { + "title": "if", + "description": "A branch with both arms lowered.", + "properties": { + "ev": { "const": "if" }, + "line": { "type": "integer" }, + "then": { "type": "array", "items": { "$ref": "#/$defs/protocolEvent" } }, + "else": { "type": "array", "items": { "$ref": "#/$defs/protocolEvent" } } + }, + "required": ["ev"] + }, + { + "title": "while", + "description": "A loop; the checker solves the body to a local fixpoint.", + "properties": { + "ev": { "const": "while" }, + "line": { "type": "integer" }, + "body": { "type": "array", "items": { "$ref": "#/$defs/protocolEvent" } } + }, + "required": ["ev"] + } + ] + }, + "protocolFunction": { + "description": "One method's ordered obligation-event tree, as reported by a frontend (spec/OwnIR.md §8).", + "type": "object", + "required": ["name"], + "properties": { + "name": { "type": "string", "minLength": 1 }, + "file": { "type": "string" }, + "events": { "type": "array", "items": { "$ref": "#/$defs/protocolEvent" } } + } } } } diff --git a/tests/fixtures/ownir/protocol_isloaded_clean.facts.json b/tests/fixtures/ownir/protocol_isloaded_clean.facts.json new file mode 100644 index 00000000..5b55a906 --- /dev/null +++ b/tests/fixtures/ownir/protocol_isloaded_clean.facts.json @@ -0,0 +1,39 @@ +{ + "ownir_version": 0, + "module": "Extracted", + "components": [], + "protocols": [ + { + "name": "DocumentLoading", + "description": "The fixed twin of protocol_isloaded_violation: the flag is restored before any unsafe notification on every path.", + "opens": {"kind": "assign", "target": "IsLoaded", "value": false}, + "closes": {"kind": "assign", "target": "IsLoaded", "value": true}, + "barriers": [ + {"kind": "call", "callee": "OnPropertyChanged", + "args": ["Document", "Rows", "Totals", "SelectedItem"]} + ], + "allow": [ + {"kind": "call", "callee": "OnPropertyChanged", + "args": ["IsLoaded", "IsBusy", "Progress", "StatusText"]} + ], + "exit_barriers": true, + "scope": {"methods": ["BigDocumentViewModel.LoadBigDocument"]} + } + ], + "protocol_functions": [ + { + "name": "Broker.BigDocumentViewModel.LoadBigDocument", + "file": "BigDocumentViewModel.cs", + "events": [ + {"ev": "assign", "target": "IsLoaded", "value": false, "line": 184}, + {"ev": "call", "callee": "OnPropertyChanged", "arg": "IsBusy", "line": 185}, + {"ev": "call", "callee": "RebuildIndexes", "line": 190}, + {"ev": "assign", "target": "IsLoaded", "value": true, "line": 238}, + {"ev": "if", "line": 240, "then": [ + {"ev": "call", "callee": "OnPropertyChanged", "arg": "Document", "line": 241} + ], "else": []}, + {"ev": "call", "callee": "OnPropertyChanged", "arg": "Document", "line": 261} + ] + } + ] +} diff --git a/tests/fixtures/ownir/protocol_isloaded_violation.facts.json b/tests/fixtures/ownir/protocol_isloaded_violation.facts.json new file mode 100644 index 00000000..5c34234f --- /dev/null +++ b/tests/fixtures/ownir/protocol_isloaded_violation.facts.json @@ -0,0 +1,39 @@ +{ + "ownir_version": 0, + "module": "Extracted", + "components": [], + "protocols": [ + { + "name": "DocumentLoading", + "description": "The document tree is inconsistent while IsLoaded == false; publishing Document/Rows/Totals in that window hands bindings a broken object.", + "opens": {"kind": "assign", "target": "IsLoaded", "value": false}, + "closes": {"kind": "assign", "target": "IsLoaded", "value": true}, + "barriers": [ + {"kind": "call", "callee": "OnPropertyChanged", + "args": ["Document", "Rows", "Totals", "SelectedItem"]} + ], + "allow": [ + {"kind": "call", "callee": "OnPropertyChanged", + "args": ["IsLoaded", "IsBusy", "Progress", "StatusText"]} + ], + "exit_barriers": true, + "scope": {"methods": ["BigDocumentViewModel.LoadBigDocument"]} + } + ], + "protocol_functions": [ + { + "name": "Broker.BigDocumentViewModel.LoadBigDocument", + "file": "BigDocumentViewModel.cs", + "events": [ + {"ev": "assign", "target": "IsLoaded", "value": false, "line": 184}, + {"ev": "call", "callee": "OnPropertyChanged", "arg": "IsBusy", "line": 185}, + {"ev": "call", "callee": "RebuildIndexes", "line": 190}, + {"ev": "if", "line": 220, "then": [ + {"ev": "call", "callee": "OnPropertyChanged", "arg": "Document", "line": 241} + ], "else": []}, + {"ev": "assign", "target": "IsLoaded", "value": true, "line": 260}, + {"ev": "call", "callee": "OnPropertyChanged", "arg": "Document", "line": 261} + ] + } + ] +} diff --git a/tests/test_obligations.py b/tests/test_obligations.py new file mode 100644 index 00000000..0bf069cf --- /dev/null +++ b/tests/test_obligations.py @@ -0,0 +1,515 @@ +#!/usr/bin/env python3 +"""Obligation-protocol tests — OBL001-005 (P-025). + +Three layers, all zero-dependency: + 1. the pure core analysis (ownlang/obligations.py): the path-sensitive walk, + the {OPEN, CLOSED} set lattice (definite/maybe split), loop fixpoints with + single emission, exit barriers, allow lists, the opaque-write discharge + asymmetry, and scoping; + 2. the OwnIR bridge (ownlang/ownir.py): the optional `protocols` / + `protocol_functions` blocks route through check_facts to OBL Findings at + their C# locations, with the opened -> barrier (-> closed-late) evidence + slice, line-free messages, and fail-loud load() validation; + 3. the schema pin (spec/ownir.schema.json): the event and matcher + vocabularies are bound to the code's authoritative sets BOTH ways, the + flow-op discipline applied to the new blocks. + +Run: python tests/test_obligations.py + python tests/run_tests.py (runs it as part of the suite) +""" +from __future__ import annotations + +import json +import os +import sys +import tempfile + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) + +from ownlang.obligations import ( + EVENT_KINDS, + MATCHER_KINDS, + AssignEv, + CallEv, + IfEv, + Matcher, + MethodEvents, + Protocol, + ProtocolFactsError, + ReturnEv, + ThrowEv, + WhileEv, + check_protocols, + parse_events, + parse_method, + parse_protocol, + unmatched_scopes, +) +from ownlang.ownir import OwnIRError, build_sarif, check_facts, load + +_REPO = os.path.join(os.path.dirname(__file__), "..") +_FIXTURES = os.path.join(os.path.dirname(__file__), "fixtures", "ownir") + + +def _proto(**kw: object) -> Protocol: + """The canonical test protocol: IsLoaded=false opens, IsLoaded=true closes, + OnPropertyChanged(Document|Rows) is a barrier, OnPropertyChanged(IsBusy) + is allowed.""" + base: dict[str, object] = { + "name": "DocLoad", + "opens": Matcher("assign", "IsLoaded", value=False), + "closes": Matcher("assign", "IsLoaded", value=True), + "barriers": (Matcher("call", "OnPropertyChanged", + args=frozenset({"Document", "Rows"})),), + "allow": (Matcher("call", "OnPropertyChanged", + args=frozenset({"IsBusy", "IsLoaded"})),), + } + base.update(kw) + return Protocol(**base) # type: ignore[arg-type] + + +def _method(*events: object, name: str = "Ns.VM.Load") -> MethodEvents: + return MethodEvents(name=name, file="VM.cs", events=tuple(events)) # type: ignore[arg-type] + + +_OPEN = AssignEv("IsLoaded", False, 10) +_CLOSE = AssignEv("IsLoaded", True, 90) +_NOTIFY_DOC = CallEv("OnPropertyChanged", "Document", 50) + + +def run() -> int: + fails: list[str] = [] + checks = 0 + + def check(cond: bool, msg: str) -> None: + nonlocal checks + checks += 1 + if not cond: + fails.append(msg) + + def codes(vs: list[object]) -> list[tuple[str, bool, int]]: + return [(v.kind, v.definite, v.line) for v in vs] # type: ignore[attr-defined] + + # ---- 1. the core walk ------------------------------------------------- + + # straight line: open -> barrier -> close = one definite barrier crossing. + vs = check_protocols([_proto()], [_method(_OPEN, _NOTIFY_DOC, _CLOSE)]) + check(codes(vs) == [("barrier", True, 50)], + f"open->barrier->close must be one definite crossing, got {vs}") + check(vs and vs[0].open_line == 10, "provenance must point at the open site") + check(vs and vs[0].close_line == 90, "the late close must be recorded as evidence") + + # the fixed twin: close before the barrier = silence. + vs = check_protocols([_proto()], [_method(_OPEN, _CLOSE, _NOTIFY_DOC)]) + check(vs == [], f"close-before-barrier must be clean, got {vs}") + + # an allow-listed notification is safe while open. + vs = check_protocols([_proto()], [_method( + _OPEN, CallEv("OnPropertyChanged", "IsBusy", 20), _CLOSE)]) + check(vs == [], f"an allowed call while open must be clean, got {vs}") + + # an args-narrowed barrier does not match other args or an unknown arg. + vs = check_protocols([_proto()], [_method( + _OPEN, CallEv("OnPropertyChanged", "Totals", 20), + CallEv("OnPropertyChanged", None, 21), _CLOSE)]) + check(vs == [], f"non-matching/unknown args must not cross, got {vs}") + + # a barrier hit in only one branch is still definite: the crossing path + # carries a definitely-open state (the branch is where the flow goes, not + # where the obligation becomes conditional). + vs = check_protocols([_proto()], [_method( + _OPEN, IfEv(20, then=(_NOTIFY_DOC,), orelse=()), _CLOSE)]) + check(codes(vs) == [("barrier", True, 50)], + f"barrier inside a branch must stay definite, got {vs}") + + # closed in one branch only -> the barrier after the merge is a MAYBE. + vs = check_protocols([_proto()], [_method( + _OPEN, + IfEv(20, then=(AssignEv("IsLoaded", True, 21),), orelse=()), + CallEv("OnPropertyChanged", "Document", 30), + AssignEv("IsLoaded", True, 40))]) + check(codes(vs) == [("barrier", False, 30)], + f"half-closed at a merge must be a maybe crossing, got {vs}") + + # opened in one branch only -> also a maybe. + vs = check_protocols([_proto()], [_method( + IfEv(20, then=(_OPEN,), orelse=()), + CallEv("OnPropertyChanged", "Document", 30))]) + got = codes(vs) + check(("barrier", False, 30) in got, + f"open-on-some-path must be a maybe crossing, got {vs}") + + # exit barriers: open with no close = leak off the end, anchored at the + # open site (the OWN001 anchor-at-acquire precedent). + vs = check_protocols([_proto()], [_method(_OPEN)]) + check(codes(vs) == [("exit", True, 10)], + f"open falling off the end must be a definite exit leak, got {vs}") + + # an early return while open reports at the return line. + vs = check_protocols([_proto()], [_method( + _OPEN, IfEv(20, then=(ReturnEv(25),), orelse=()), _CLOSE)]) + check(codes(vs) == [("exit", True, 25)], + f"early return while open must report at the return, got {vs}") + + # a throw while open reports at the throw line. + vs = check_protocols([_proto()], [_method(_OPEN, ThrowEv(30))]) + check(codes(vs) == [("exit", True, 30)], + f"throw while open must report at the throw, got {vs}") + + # the late-close hop belongs to barrier crossings only: an exit leak has + # no barrier to be late for, even when a close exists later in the tree. + vs = check_protocols([_proto()], [_method( + _OPEN, IfEv(20, then=(ThrowEv(25),), orelse=()), _CLOSE)]) + check(codes(vs) == [("exit", True, 25)] and vs[0].close_line is None, + f"an exit leak must not carry a late-close hop, got {vs}") + + # code after a return is on the other path only: close-after-early-return + # still leaves the return-path leak, and only that. + vs = check_protocols([_proto()], [_method( + _OPEN, IfEv(20, then=(ReturnEv(25),), orelse=(_CLOSE,)))]) + check(codes(vs) == [("exit", True, 25)], + f"only the returning path leaks, got {vs}") + + # exit_barriers=False silences exits but not barriers. + vs = check_protocols([_proto(exit_barriers=False)], [_method(_OPEN)]) + check(vs == [], f"exit_barriers=false must silence the exit leak, got {vs}") + + # loops: close inside the body -> after the loop the state is {OPEN (0 + # iterations), CLOSED} -> a maybe crossing; and the loop emits ONCE. + vs = check_protocols([_proto()], [_method( + _OPEN, + WhileEv(20, body=(AssignEv("IsLoaded", True, 21),)), + CallEv("OnPropertyChanged", "Document", 30), + AssignEv("IsLoaded", True, 40))]) + check(codes(vs) == [("barrier", False, 30)], + f"loop may run zero times: barrier after it is a maybe, got {vs}") + + # a barrier inside a loop body while open: exactly one finding (the + # fixpoint iterations are silent; only the converged pass emits). + vs = check_protocols([_proto()], [_method( + _OPEN, WhileEv(20, body=(_NOTIFY_DOC,)), _CLOSE)]) + check(codes(vs) == [("barrier", True, 50)], + f"a barrier in a loop must report exactly once, got {vs}") + + # nested loops still emit once. + vs = check_protocols([_proto()], [_method( + _OPEN, WhileEv(20, body=(WhileEv(21, body=(_NOTIFY_DOC,)),)), _CLOSE)]) + check(codes(vs) == [("barrier", True, 50)], + f"a barrier in a nested loop must report exactly once, got {vs}") + + # re-open inside a loop (close at the top of the body, re-open at the + # bottom): the header join must reach a fixpoint, and the crossing stays + # DEFINITE — every path (zero iterations or n) leaves the flag down. + vs = check_protocols([_proto()], [_method( + AssignEv("IsLoaded", False, 10), + WhileEv(20, body=(AssignEv("IsLoaded", True, 21), + AssignEv("IsLoaded", False, 22))), + CallEv("OnPropertyChanged", "Document", 30), + AssignEv("IsLoaded", True, 40))]) + check(codes(vs) == [("barrier", True, 30)], + f"open/close cycling in a loop must converge (and every path is " + f"open at the barrier), got {vs}") + + # the opaque-write asymmetry: while OPEN an opaque write to the tracked + # flag downgrades the crossing to a maybe (it may have closed)... + vs = check_protocols([_proto()], [_method( + _OPEN, AssignEv("IsLoaded", None, 20), _NOTIFY_DOC, _CLOSE)]) + check(codes(vs) == [("barrier", False, 50)], + f"an opaque write may discharge -> maybe crossing, got {vs}") + # ...but while CLOSED an opaque write must NOT invent an obligation. + vs = check_protocols([_proto()], [_method( + AssignEv("IsLoaded", None, 5), _NOTIFY_DOC)]) + check(vs == [], f"an opaque write must never open an obligation, got {vs}") + # an opaque write to an untracked member is inert either way. + vs = check_protocols([_proto()], [_method( + _OPEN, AssignEv("Title", None, 20), _NOTIFY_DOC, _CLOSE)]) + check(codes(vs) == [("barrier", True, 50)], + f"an untracked opaque write must not discharge, got {vs}") + + # a call the protocol does not name is neutral (no discharge, no crossing). + vs = check_protocols([_proto()], [_method( + _OPEN, CallEv("RebuildIndexes", None, 20), _NOTIFY_DOC, _CLOSE)]) + check(codes(vs) == [("barrier", True, 50)], + f"an unnamed call must stay neutral, got {vs}") + + # call-based protocols: BeginUpdate/EndUpdate with a bare-call barrier. + begin_end = Protocol( + name="BatchUpdate", + opens=Matcher("call", "BeginUpdate"), + closes=Matcher("call", "EndUpdate"), + barriers=(Matcher("call", "Refresh"),)) + vs = check_protocols([begin_end], [_method( + CallEv("BeginUpdate", None, 10), CallEv("Refresh", None, 20), + CallEv("EndUpdate", None, 30))]) + check(codes(vs) == [("barrier", True, 20)], + f"call-open protocols must work, got {vs}") + + # two protocols are independent states over the same method. + vs = check_protocols([_proto(), begin_end], [_method( + _OPEN, CallEv("BeginUpdate", None, 20), CallEv("EndUpdate", None, 30), + _NOTIFY_DOC, _CLOSE)]) + check(codes(vs) == [("barrier", True, 50)], + f"protocols must not interfere, got {vs}") + + # scoping: exact and Type.Method-suffix match in, others out. + scoped = _proto(methods=("VM.Load",)) + vs = check_protocols([scoped], [_method(_OPEN, _NOTIFY_DOC, _CLOSE)]) + check(len(vs) == 1, f"a Type.Method suffix must match Ns.VM.Load, got {vs}") + vs = check_protocols([scoped], [ + _method(_OPEN, _NOTIFY_DOC, _CLOSE, name="Ns.VM.LoadAll"), + _method(_OPEN, _NOTIFY_DOC, _CLOSE, name="Ns.OtherVM.Load2")]) + check(vs == [], f"out-of-scope methods must stay silent, got {vs}") + check([p.name for p in unmatched_scopes( + [scoped], [_method(_OPEN, name="Ns.OtherVM.Reload")])] == ["DocLoad"], + "a scope matching nothing must surface as a dead rule") + check(unmatched_scopes([_proto()], []) == [], + "an unscoped protocol is never a dead rule") + + # determinism: findings sorted by (file, line, protocol). + vs = check_protocols([_proto()], [_method( + _OPEN, _NOTIFY_DOC, CallEv("OnPropertyChanged", "Rows", 60), _CLOSE)]) + check([v.line for v in vs] == [50, 60], f"findings must be ordered, got {vs}") + + # ---- 2. parsing: fail-loud vocabulary --------------------------------- + + def rejects(fn: object, raw: object, why: str) -> None: + nonlocal checks + checks += 1 + try: + fn(raw) # type: ignore[operator] + fails.append(f"{why}: not rejected") + except ProtocolFactsError: + pass + + rejects(parse_protocol, {"name": "P"}, "opens/closes are required") + rejects(parse_protocol, + {"name": "P", "opens": {"kind": "flip", "target": "x"}, + "closes": {"kind": "assign", "target": "x", "value": True}}, + "an unknown matcher kind") + rejects(parse_protocol, + {"name": "P", "opens": {"kind": "assign", "target": "x"}, + "closes": {"kind": "assign", "target": "x", "value": True}}, + "an opens assign matcher without a value") + rejects(parse_protocol, + {"name": "P", "opens": {"kind": "assign", "target": "x", "value": False}, + "closes": {"kind": "assign", "target": "x", "value": True}, + "exit_barriers": False}, + "no barriers and no exit barriers (a rule that cannot fire)") + rejects(parse_protocol, + {"name": "P", "opens": {"kind": "call", "callee": "BeginUpdate"}, + "closes": {"kind": "call", "callee": "EndUpdate"}, + "barriers": [{"kind": "call", "callee": "BeginUpdate"}]}, + "a barrier equal to opens (shadowed, silently dead)") + rejects(parse_method, {"name": "m", "events": [{"ev": "goto", "line": 1}]}, + "an unknown protocol event") + rejects(parse_method, {"name": "m", "events": [{"ev": "assign", "line": 1}]}, + "an assign event without a target") + rejects(parse_method, + {"name": "m", "events": [{"ev": "assign", "target": "x", "value": 1, + "line": 1}]}, + "a non-boolean assign value (the bool-is-int trap)") + checks += 1 + try: + parse_events([{"ev": "if", "then": [{"ev": "nope"}], "else": []}], "t") + fails.append("an unknown ev nested under if/then was not rejected") + except ProtocolFactsError: + pass + + # ---- 3. the bridge: fixtures end-to-end ------------------------------- + + with open(os.path.join(_FIXTURES, "protocol_isloaded_violation.facts.json"), + encoding="utf-8") as f: + bad = json.load(f) + findings = check_facts(bad) + check(len(findings) == 1, f"the killer fixture must yield exactly one finding, " + f"got {[(x.code, x.line) for x in findings]}") + if findings: + f0 = findings[0] + check(f0.code == "OBL001" and f0.file == "BigDocumentViewModel.cs" + and f0.line == 241, + f"expected OBL001 at BigDocumentViewModel.cs:241, got " + f"{f0.code} at {f0.file}:{f0.line}") + check(f0.component == "BigDocumentViewModel" + and f0.event == "DocumentLoading" + and f0.handler == "LoadBigDocument", + f"finding identity fields drifted: {f0.component}/{f0.event}/{f0.handler}") + check(f0.kind == "protocol obligation" and not f0.advisory, + "an OBL001 is an error-tier protocol-obligation verdict") + # the evidence slice: opened -> barrier -> closed-late, in order. + check([ln for (_, ln, _) in f0.flow] == [184, 241, 260], + f"evidence slice must be open->barrier->late-close, got {f0.flow}") + # messages are line-free (OwnAudit fingerprints on path|rule|message). + check(not any(ch.isdigit() for ch in f0.message.replace("IsLoaded", "")), + f"the message must not embed line numbers: {f0.message!r}") + check("IsLoaded = true" in f0.message and "OnPropertyChanged(Document)" + in f0.message, f"the message must name the fix and the barrier: " + f"{f0.message!r}") + + with open(os.path.join(_FIXTURES, "protocol_isloaded_clean.facts.json"), + encoding="utf-8") as f: + good = json.load(f) + clean = check_facts(good) + check(clean == [], f"the fixed twin must be silent, got " + f"{[(x.code, x.line) for x in clean]}") + + # exit leak through the bridge: OBL003 anchored at the open site, and the + # SARIF rules catalogue knows the code. + leak = check_facts({ + "ownir_version": 0, "module": "S", + "protocols": [{ + "name": "Suppress", + "opens": {"kind": "assign", "target": "_suppress", "value": True}, + "closes": {"kind": "assign", "target": "_suppress", "value": False}}], + "protocol_functions": [{ + "name": "VM.Batch", "file": "VM.cs", "events": [ + {"ev": "assign", "target": "_suppress", "value": True, "line": 7}, + {"ev": "if", "line": 8, + "then": [{"ev": "throw", "line": 9}], "else": []}, + {"ev": "assign", "target": "_suppress", "value": False, + "line": 12}]}]}) + check([(x.code, x.line) for x in leak] == [("OBL003", 9)], + f"a throw while open must be OBL003 at the throw, got " + f"{[(x.code, x.line) for x in leak]}") + sarif = build_sarif(leak) + rules = {r["id"]: r["shortDescription"]["text"] + for r in sarif["runs"][0]["tool"]["driver"]["rules"]} + check("OBL003" in rules, "OBL003 must reach the SARIF rules catalogue") + + # OBL005: a scoped protocol matching no reported method is an advisory. + dead = check_facts({ + "ownir_version": 0, "module": "S", + "protocols": [{ + "name": "Ghost", + "opens": {"kind": "assign", "target": "x", "value": False}, + "closes": {"kind": "assign", "target": "x", "value": True}, + "scope": {"methods": ["VM.Misspelled"]}}], + "protocol_functions": [{"name": "VM.Load", "file": "VM.cs", + "events": []}]}) + check([(x.code, x.advisory) for x in dead] == [("OBL005", True)], + f"a dead scope must be the OBL005 advisory, got " + f"{[(x.code, x.advisory) for x in dead]}") + + # malformed blocks degrade gracefully on the direct check_facts path + # (load() fail-louds; embedders/tests may skip it). + check(check_facts({"ownir_version": 0, "components": [], + "protocols": "nope"}) == [], + "a malformed protocols block must not crash check_facts") + check(check_facts({"ownir_version": 0, "components": [], + "protocols": [{"name": "P"}], + "protocol_functions": [{"name": "m"}]}) == [], + "a malformed protocol entry is skipped on the direct path") + + # duplicate protocol names: the name is the identity findings map back by. + # On the direct path the first wins deterministically (the second is + # skipped — never a mixed message or a dedup-collapsed pair of findings)... + dup = check_facts({ + "ownir_version": 0, "module": "S", + "protocols": [ + {"name": "Dup", + "opens": {"kind": "assign", "target": "A", "value": False}, + "closes": {"kind": "assign", "target": "A", "value": True}, + "barriers": [{"kind": "call", "callee": "Notify"}]}, + {"name": "Dup", + "opens": {"kind": "call", "callee": "BeginUpdate"}, + "closes": {"kind": "call", "callee": "EndUpdate"}, + "barriers": [{"kind": "call", "callee": "Notify"}]}], + "protocol_functions": [{"name": "VM.Go", "file": "VM.cs", "events": [ + {"ev": "assign", "target": "A", "value": False, "line": 10}, + {"ev": "call", "callee": "BeginUpdate", "line": 11}, + {"ev": "call", "callee": "Notify", "line": 20}, + {"ev": "assign", "target": "A", "value": True, "line": 30}, + {"ev": "call", "callee": "EndUpdate", "line": 31}]}]}) + check([(x.code, x.line) for x in dup] == [("OBL001", 20)] + and dup and "A = true" in dup[0].message, + f"duplicate names: first must win whole, got " + f"{[(x.code, x.message) for x in dup]}") + + # load() is the fail-loud gate: an unknown ev is rejected with OwnIRError, + # and so is a duplicate protocol name (ambiguous identity). + def load_rejects(doc: dict[str, object], why: str) -> None: + nonlocal checks + with tempfile.NamedTemporaryFile("w", suffix=".facts.json", delete=False, + encoding="utf-8") as tf: + json.dump(doc, tf) + tmp = tf.name + checks += 1 + try: + load(tmp) + fails.append(f"load() accepted {why}") + except OwnIRError: + pass + finally: + os.unlink(tmp) + + load_rejects({"ownir_version": 0, "module": "S", + "protocol_functions": [{"name": "m", "events": + [{"ev": "goto", "line": 1}]}]}, + "an unknown protocol event") + _p = {"name": "Dup", + "opens": {"kind": "assign", "target": "A", "value": False}, + "closes": {"kind": "assign", "target": "A", "value": True}} + load_rejects({"ownir_version": 0, "module": "S", "protocols": [_p, dict(_p)]}, + "a duplicate protocol name") + + # both fixtures pass the real load() gate (shape-valid on disk). + for fx in ("protocol_isloaded_violation", "protocol_isloaded_clean"): + checks += 1 + try: + load(os.path.join(_FIXTURES, f"{fx}.facts.json")) + except OwnIRError as e: + fails.append(f"fixture {fx} rejected by load(): {e}") + + # ---- 4. schema <-> code binding (the flow-op discipline, spec §8) ----- + + with open(os.path.join(_REPO, "spec", "ownir.schema.json"), + encoding="utf-8") as f: + schema = json.load(f) + defs = schema.get("$defs", {}) + for prop in ("protocols", "protocol_functions"): + check(prop in schema.get("properties", {}), + f"schema must declare the top-level '{prop}' block") + evs = [b.get("properties", {}).get("ev", {}).get("const") + for b in defs.get("protocolEvent", {}).get("oneOf", [])] + check(None not in evs and len(evs) == len(set(evs)), + f"schema protocolEvent consts malformed: {evs}") + check(set(evs) == set(EVENT_KINDS), + f"schema protocolEvent consts {sorted(x for x in evs if x)} != code " + f"EVENT_KINDS {sorted(EVENT_KINDS)} — vocabulary drift") + kinds = [b.get("properties", {}).get("kind", {}).get("const") + for b in defs.get("protocolMatcher", {}).get("oneOf", [])] + check(set(kinds) == set(MATCHER_KINDS), + f"schema protocolMatcher consts {sorted(x for x in kinds if x)} != " + f"code MATCHER_KINDS {sorted(MATCHER_KINDS)} — vocabulary drift") + # the opens/closes variant must exist and require `value` on its assign + # branch (the require_value rule, structurally enforced in the schema). + oc = defs.get("protocolOpenClose", {}).get("oneOf", []) + check({b.get("properties", {}).get("kind", {}).get("const") + for b in oc} == set(MATCHER_KINDS), + "schema protocolOpenClose must cover the matcher vocabulary") + oc_assign = next((b for b in oc + if b.get("properties", {}).get("kind", {}).get("const") + == "assign"), {}) + check("value" in oc_assign.get("required", []), + "schema protocolOpenClose assign branch must require 'value'") + # drive every declared ev through the parser: a phantom set entry + # (declared but unparseable) reddens this, mirroring the flow-op check. + for ev in sorted(EVENT_KINDS): + node: dict[str, object] = {"ev": ev, "line": 1} + if ev == "assign": + node["target"] = "x" + if ev == "call": + node["callee"] = "f" + checks += 1 + try: + parse_events([node], "pin") + except ProtocolFactsError as e: + fails.append(f"EVENT_KINDS lists {ev!r} but parse_events rejects it: {e}") + + for msg in fails: + print(f"OBLIGATIONS FAIL: {msg}") + print(f"obligations: {checks - len(fails)}/{checks} protocol checks passed") + return 1 if fails else 0 + + +if __name__ == "__main__": + raise SystemExit(run()) From 3fbb33e2f581f49cd63a9e574dca3205213f8461 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 15:43:27 +0000 Subject: [PATCH 2/2] docs(obligations): address CodeRabbit review on #176 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - P-025: tag the protocol-verbs fence as text (MD040; the C# fence was already tagged) - __main__: de-OWN050-ify the cmd_ownir docstring and the advisory comment block — the band now carries OBL005 too - diagnostics: EXPLANATIONS for the maybe-siblings OBL002/OBL004, mirroring OBL001/OBL003 so ownlang explain answers all four symmetrically Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01NXzqX7Qwn5QzBLGVCATdgm --- docs/proposals/P-025-obligation-protocols.md | 2 +- ownlang/__main__.py | 8 ++++---- ownlang/diagnostics.py | 15 +++++++++++++++ 3 files changed, 20 insertions(+), 5 deletions(-) diff --git a/docs/proposals/P-025-obligation-protocols.md b/docs/proposals/P-025-obligation-protocols.md index 5cf33a3c..32da0721 100644 --- a/docs/proposals/P-025-obligation-protocols.md +++ b/docs/proposals/P-025-obligation-protocols.md @@ -47,7 +47,7 @@ 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 diff --git a/ownlang/__main__.py b/ownlang/__main__.py index ce628ee4..ac74c7ac 100644 --- a/ownlang/__main__.py +++ b/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 diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py index d0cecd77..bc2fdbd2 100644 --- a/ownlang/diagnostics.py +++ b/ownlang/diagnostics.py @@ -197,6 +197,14 @@ class Severity(Enum): "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 " @@ -205,6 +213,13 @@ class Severity(Enum): "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 "