diff --git a/docs/notes/tech-debt-register.md b/docs/notes/tech-debt-register.md index d303ba57..82232b16 100644 --- a/docs/notes/tech-debt-register.md +++ b/docs/notes/tech-debt-register.md @@ -122,21 +122,24 @@ The formalization stack, in order of actual protection delivered: normalized facts for the pinned samples, and feed the same goldens to `test_ownir.py` so the Python suite also consumes *extractor-produced* facts, not only hand-written ones. -3. **`spec/OwnIR.md` + `spec/ownir.schema.json`** (JSON Schema draft 2020-12, - `ownir_version` as a `const`) *(now/short)*. Validate all - `tests/fixtures/ownir/*.json` and the extractor's CI output against it. - Note: the schema must encode the *deliberate* open points — unknown - resource kinds coerce to `subscription` by documented design - (`ownir.py:66-70`), so the resource-kind enum is open, and the schema's job - is shape/type/enum guarantees, not vocabulary closure. -4. **A written evolution policy** *(now, one paragraph in the spec)*: additive - optional fields do not bump `OWNIR_VERSION`; a **new op or changed op - semantics does**. Today's policy only covers the first half, which is - exactly the gap item 1 exploits. -5. Version single-sourcing across the three producers (`ownir.py:159`, - `Program.cs:4360`, `ownts.py:580`) *(with next touch)* — worth doing, but - understand what it does not protect: the dangerous case is *nobody* bumping, - which only items 1–4 catch. +3. **`spec/OwnIR.md`** ✅ (shipped) **+ `spec/ownir.schema.json`** (JSON Schema + draft 2020-12, `ownir_version` as a `const`) — **the schema's trigger has now + fired** (see the box below). Validate all `tests/fixtures/ownir/*.json` and + each frontend's output against it. The resource-kind enum is **closed** for + *present* values — a present-but-unknown kind is rejected at load (it changes + routing; a new kind bumps `OWNIR_VERSION`), while an *absent* `resource` field + still defaults to `subscription`; the schema should mirror that (enum of known + kinds, field optional). Its job is shape/type/enum guarantees. +4. **A written evolution policy** ✅ *(now shipped in `spec/OwnIR.md` §2, rules + IR1–IR6)*: additive optional fields / new resource kinds do not bump + `OWNIR_VERSION`; a **new op or changed op semantics does**. +5. Version single-sourcing ✅ *(enforced)* — a `test_ownir.py` check now greps + each frontend producer (`Program.cs`, `ownts.py`) and asserts its + `ownir_version` literal equals the core's `OWNIR_VERSION`, so "bumped the + core, forgot a frontend" (or the reverse) fails loudly. Understand what it + does **not** protect: the dangerous case is *nobody* bumping, which only + items 1/4 catch. When the P-022 `own-ir` crate lands (a **fourth** producer), + add it to this check — or, better, generate all four from the schema (§below). 6. Reconcile or explicitly document the BCL fresh-factory asymmetry *(now, small)*: the extractor's `IsOwningFactory` knows the ADO.NET family (`ExecuteReader`/`CreateCommand`/`BeginTransaction`, @@ -146,9 +149,28 @@ The formalization stack, in order of actual protection delivered: only consulted for first-party `call` ops), but the lockstep is comment-enforced and has already quietly diverged. -Later, if a Rust/C# core materializes: generate types from the same schema -(serde via typify / System.Text.Json source-gen). Protobuf/FlatBuffers only if -fact volume ever makes JSON parse time measurable — no evidence today. +> **Why the schema is now worth building (the argument that was strong all +> along, recovered).** OwnIR is not a nice-to-have file — it is *the one language +> every frontend and the core speak* ("frontends only produce/consume OwnIR", +> ROADMAP design philosophy). **A language without a formal grammar is a language +> that lies about itself.** Until now the schema looked redundant: `ownlang`'s +> hand-written `load()` was the sole validator, so a JSON Schema only *duplicated* +> its shape checks — a second source of truth to drift against, needing a +> `jsonschema` dependency the zero-dep core avoids. **That calculus flips the +> moment there is a second language-native type set** — which has now arrived: +> P-022 #170 ships `crates/own-ir`, hand-writing Rust `serde` structs under the +> rule "accept exactly what Python `load()` accepts," kept in sync only by a +> fixture round-trip. That is two hand-maintained validators of one contract, in +> two languages — the exact drift the OwnIR formalization exists to kill. The +> schema stops being a *shadow* of `load()` and becomes the *source both are +> generated from* (Rust `serde` via `typify`/`schemars`; C#/TS types via +> source-gen), collapsing the hand-synced fact shapes **and** the now-four +> `ownir_version` literals into one authority. So: `spec/OwnIR.md` (done) is the +> prose grammar; `spec/ownir.schema.json` is the machine grammar, and it should be +> **co-designed with the `own-ir` crate** (generate the Rust types from it, don't +> hand-write them twice) rather than bolted on after. JSON stays the wire format; +> Protobuf/FlatBuffers only if measured parse cost ever demands it — no evidence +> today. ## 3. The extractor↔bridge "mirror" (LowerFlowStmt / _lower_flow) @@ -186,18 +208,22 @@ Python walkers (§2.1). ### Now (standalone value; days-scale; ordered by protection-per-effort) +> **Progress (branch `claude/ownir-contract-hardening`):** N1 ✅, N4 ✅ (spec +> shipped; JSON Schema still pending), N6 ✅ (validation, not a full enum — see +> below), N9 ✅. N8 re-scoped (not surgical — see note). The rest stand. + | # | Item | Where | Why now | |---|------|-------|---------| -| N1 | `else: raise` on unknown flow ops (+ the five walkers) | `ownlang/ownir.py:1692-1836` | Silent fact-swallowing → fabricated/missed verdicts (§2.1) | -| N2 | Auto-discovery in the test runner | `tests/run_tests.py:1144-1149` | 25-term hand-rolled `or`; a forgotten `rc` silently stops gating | +| N1 ✅ | `else: raise` on unknown flow ops | `ownlang/ownir.py` `_lower_flow` | Silent fact-swallowing → fabricated/missed verdicts (§2.1). *Done: raises `OwnIRError`; pinned by test_ownir. The five read-only walkers legitimately ignore ops they don't consume, so the guard is scoped to `_lower_flow` (the only pass that must handle every op or lose facts).* | +| N2 ✅ | Auto-discovery in the test runner | `tests/run_tests.py` | 25-term hand-rolled `or`; a forgotten `rc` silently stopped gating. *Done: the runner now globs `test_*.py`, calls each module's `run()`, and gates on `any(rc)` — a new test file is auto-included, a module without `run()` fails the suite, and a discovery of zero modules fails loud. `test_codegen_props` keeps its lighter in-suite iteration count via a small special-case map.* | | N3 | Golden facts snapshots in CI + feed to `test_ownir.py` | `ci.yml` wpf-extractor job | The seam is never diffed at the facts level (§2.2) | -| N4 | `spec/OwnIR.md` + JSON Schema + evolution policy | new; `ownir.py:1-97` is the source | §2.3–2.4 | +| N4 ◑ | `spec/OwnIR.md` ✅ + evolution policy ✅ + version single-sourcing ✅ + JSON Schema (trigger now fired) | `spec/OwnIR.md`, `tests/test_ownir.py` | §2. *Done: normative spec with the version evolution policy (IR1–IR6), registered in `spec/README.md`; and a producer-version-consistency check (each frontend's `ownir_version` must equal the core's). Remaining: `spec/ownir.schema.json` — its trigger has now fired (P-022 #170's `own-ir` crate = a second hand-written type set), so **co-design it with that crate and generate the Rust types from it**, per the §2 box; do NOT bolt a `jsonschema` CI validator onto the zero-dep core first.* | | N5 | DI001–005 + EFF001 into `spec/` + `Diagnostics.md` + `test_spec.py` | `ownlang/di.py`, `effects.py` | Second-largest analyzer has zero normative governance | -| N6 | Diagnostic `Code` enum (replace bare string literals) | `ownlang/diagnostics.py:243` + emit sites | New codes land weekly; a typo'd code silently renders `""` | +| N6 ✅ | Fail-loud on unknown diagnostic code | `ownlang/diagnostics.py` `Diagnostic.__post_init__` | New codes land weekly; a typo'd code silently rendered `""`. *Done: `Diagnostic` now rejects any code absent from `TITLES` at construction (full suite confirms every emitted code is registered), and `title` indexes instead of `.get(...,"")`. A full `StrEnum` is the heavier follow-up; this closes the silent-`""` hole cheaply.* | | N7 | Split `ownir.py` → `ownir/{render,load,lower,inference,check}` | `ownlang/ownir.py` (2430 lines) | Fastest-accreting file in the repo; `check_facts` grows a branch per resource kind; deferring = paying the god-file tax on every feature | -| N8 | Dedicated syntax-error code (stop filing `ParseError` as OWN020) | `ownlang/__main__.py:80` | Miscategorized as "unsupported construct" | -| N9 | Bare `assert` on the loan invariant → raise | `ownlang/analysis.py:200-203` | Stripped under `python -O`; silent wrong answer if block-scoping is ever relaxed | -| N10 | Reconcile/document BCL table asymmetry | `Program.cs:2545-2568` vs `ownir.py:1179-1199` | Lockstep already quietly diverged (§2.6) | +| N8 ⚠️ | Dedicated syntax-error code (stop filing `ParseError` as OWN020) | `ownlang/__main__.py:80` | **Re-scoped: not surgical.** OWN020 is the suite-wide code for *any* parse/lex rejection — `for`/`loop`/`async` are lexer-*rejected keywords* (LexError → OWN020 by design), and the corpus/gallery/wpf/rid/loops test helpers all treat OWN020 as "parse rejected". Splitting a genuine syntax error from an unsupported-construct rejection means distinguishing the two at the lexer/parser and updating ~6 test files + `Grammar.md`/`CLI.md`/`OwnCore.md`. A real UX win, but a small refactor, not a one-liner. | +| N9 ✅ | Bare `assert` on the loan invariant → raise | `ownlang/analysis.py` `join()` | Stripped under `python -O`. *Done: mirrors the explicit-raise pattern already used at `_join_handle_rid`, so the invariant holds in every build.* | +| N10 ✅ | Reconcile/document BCL table asymmetry | `Program.cs` `IsOwningFactory` + `ownir.py` `_BCL_FRESH_BY_NS` | Lockstep already quietly diverged (§2.6). *Done: documented, not reconciled — because the two are NOT a mirror. `IsOwningFactory` is the emission authority (a match emits an `acquire`), so it is the SUPERSET incl. ADO.NET + network `Accept*`; the bridge table is consulted only for `call`-op results (`_callee_returns_fresh`), and owning factories are emitted as `acquire` not `call`, so it is a deliberate SUBSET — the C#-only entries never arrive as `call`s. Forcing the lists identical would add dead entries; instead the misleading "kept in lockstep" comments on both sides now state the real roles + the safety invariant (owning factory ⇒ `acquire`) + the generate-from-schema exit.* | ### With next touch diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index a51d600b..c625e621 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -2509,9 +2509,15 @@ void Visit(ExpressionSyntax e) // `JsonDocument.ParseAsync` is excluded. // Curated + symbol-resolved, so a borrowed/cached disposable handed back by some other API is // never mistaken for an owned acquire (precision over recall — the set grows only as -// ownership is certain). Kept in lockstep with the bridge table `_BCL_FRESH_BY_NS` -// (ownlang/ownir.py): the extractor decides whether to EMIT the factory call fact, the bridge -// recognises the callee name as `fresh`. +// ownership is certain). +// +// Relationship to the bridge table `_BCL_FRESH_BY_NS` (ownlang/ownir.py) — NOT a mirror. This +// function is the emission AUTHORITY: a match makes the extractor emit the local as an `acquire` +// fact. So this list is the SUPERSET — it also covers ADO.NET and network `Accept*`, which the +// bridge table omits. The bridge table is consulted only on the OTHER path — a `call` op whose +// result the bridge decides is `fresh` — and since owning factories are emitted as `acquire` (not +// `call`), it need only cover the shared File/crypto/Xml/Json seam, never the ADO.NET/network +// entries. If a factory here is ever emitted as a `call` instead, add it to the bridge table too. static bool IsOwningFactory(ExpressionSyntax? e, SemanticModel model) { if (e is not InvocationExpressionSyntax i diff --git a/ownlang/analysis.py b/ownlang/analysis.py index 7ae63d68..9f626ae8 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -197,10 +197,14 @@ def join(a: State, b: State) -> State: # holds across loop back-edges too: a borrow opened inside a loop body closes # within the same iteration, so the loan set at the body exit equals the one on # the entry edge. Assert the invariant rather than paper over a builder bug. - assert set(a.loans) == set(b.loans), ( - "active loans differ at a control-flow merge; this should be impossible " - "for block-scoped borrows (they close within the scope that opened them)" - ) + # An explicit raise, not `assert`: `python -O` strips asserts, and a silently + # mismatched loan set at a merge would defeat the invariant this locks (same as + # `_join_handle_rid` above). Keep it loud in every build. + if set(a.loans) != set(b.loans): + raise AssertionError( + "active loans differ at a control-flow merge; this should be impossible " + "for block-scoped borrows (they close within the scope that opened them)" + ) out.loans = dict(a.loans) out.handle_rid = _join_handle_rid(a.handle_rid, b.handle_rid) out.moved_at = _join_sites(a.moved_at, b.moved_at) diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py index f4f27d32..6b803b92 100644 --- a/ownlang/diagnostics.py +++ b/ownlang/diagnostics.py @@ -239,9 +239,20 @@ class Diagnostic: # contract (code, message, line, severity, subject, resource_kind) is preserved. evidence: tuple[Evidence, ...] = () + def __post_init__(self) -> None: + # A code with no TITLES entry is a bug, not a blank finding: `title` used to + # silently return "" for a typo'd or forgotten code. Fail loudly at + # construction so a mis-typed code can never ship a titleless diagnostic — + # the one stringly-typed contract in a --strict codebase. + if self.code not in TITLES: + raise ValueError( + f"unknown diagnostic code {self.code!r} (not in diagnostics.TITLES); " + f"a code and its title must be added together" + ) + @property def title(self) -> str: - return TITLES.get(self.code, "") + return TITLES[self.code] def _kind_suffix(self) -> str: return f" [resource: {self.resource_kind}]" if self.resource_kind else "" diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 0cac20f0..f8e755cd 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -66,8 +66,11 @@ advisory OWN050 "leakage analysis skipped" note, never a leak (P-014 Tier A). An unreleased entry is the core's OWN001 (owned-but-not-released) at the C# -`line`. The `resource`/`type` fields are additive and optional, so they do NOT -bump `ownir_version`: an older core just reads every entry as a subscription. +`line`. The `resource`/`type` FIELDS are additive and optional — an older core +that predates them reads an entry with no `resource` as a subscription. But a new +resource-kind VALUE is a vocabulary change, not additive metadata: the kind +selects the analysis path, so a PRESENT-but-unknown kind is rejected at load +(fail-loud), and introducing one MUST bump `ownir_version` (spec/OwnIR.md §2). A `capture` entry instead routes through the lifetime/region engine and surfaces as OWN014 (region escape) when its source provably outlives — see docs/proposals/ P-004 and docs/lifetimes.md (the C# facts now reach the region core, not only the @@ -214,6 +217,16 @@ def _esc_prop(s: str) -> str: "pool": ("PooledBuffer", "pooled buffer"), } +# Every resource-kind discriminator the core routes on (the `_RESOURCES` owned +# kinds, plus `capture` — routed to the lifetime/region engine — and +# `unresolved-subscription` — skipped to an advisory OWN050). The kind CHANGES the +# analysis path (§4 of spec/OwnIR.md), so it is NOT metadata: a PRESENT-but-unknown +# kind is rejected at load (fail-loud, like an unknown flow op), never silently +# routed as a `subscription`. An ABSENT `resource` field still defaults to +# `subscription` (an old extractor that predates the field). Consequence: adding a +# new kind is a vocabulary change that MUST bump OWNIR_VERSION (spec/OwnIR.md §2). +_KNOWN_RESOURCE_KINDS = frozenset(_RESOURCES) | {"capture", "unresolved-subscription"} + # --- P-004 region escape (the `capture` resource kind) ---------------------- # A `capture` is a tokenless strong subscription routed NOT through the # acquire/release ownership model but through the lifetime/region engine @@ -472,6 +485,15 @@ def load(path: str) -> dict[str, Any]: if not isinstance(r, str): raise OwnIRError( f"subscription 'resource' must be a string, got {r!r}") + # A present-but-unknown kind changes routing (§4), so reject it rather + # than let it fall through to the owned/subscription path and mis-route + # — the same fail-loud rule as an unknown flow op. A new kind must bump + # OWNIR_VERSION (spec/OwnIR.md §2). An absent field defaulted to + # "subscription" above, which is known. + if r not in _KNOWN_RESOURCE_KINDS: + raise OwnIRError( + f"unknown resource kind {r!r} — a new kind is a vocabulary " + f"change that must bump OWNIR_VERSION (see spec/OwnIR.md §2)") t = s.get("type") if t is not None and not isinstance(t, str): raise OwnIRError( @@ -1188,8 +1210,20 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str], # P1a (stdlib contract pack): more well-known static factories whose result the caller # OWNS and must dispose. `XmlReader`/`XmlWriter.Create` return a fresh reader/writer; a # `JsonDocument` from `Parse` pools memory and must be disposed (a `var doc = - # JsonDocument.Parse(json)` that drops `doc` is a common real leak). Kept in lockstep with - # the extractor's `IsOwningFactory` (frontend/roslyn/.../Program.cs). + # JsonDocument.Parse(json)` that drops `doc` is a common real leak). + # + # Relationship to the extractor's `IsOwningFactory` (frontend/roslyn/.../Program.cs) — NOT a + # mirror, despite the old "kept in lockstep" wording. The two play different roles. The + # extractor is the emission AUTHORITY: seeing `var x = Factory()` it emits `x` as an `acquire` + # fact directly, so its list is the SUPERSET — File, crypto by `Create*`-prefix, Xml/Json, PLUS + # ADO.NET (`ExecuteReader`/`CreateCommand`/`BeginTransaction`) and network `Accept*`. THIS table + # is consulted only on the other path: a `call` op whose result the bridge must decide is + # `fresh` (`_callee_returns_fresh`). Owning BCL factories are emitted as `acquire`, not `call`, + # so this table is a deliberate SUBSET — the C#-only entries never arrive here as `call`s, so + # adding them would be dead weight. Safety invariant: an owning BCL factory is emitted as + # `acquire`. If the extractor ever emits a `call` op for one, add it here too (better: generate + # both sides from `spec/ownir.schema.json` — see the tech-debt register). Keep the shared + # File/crypto/Xml/Json entries aligned on that seam. "System.Xml": ( "XmlReader.Create", "XmlWriter.Create", ), @@ -1834,6 +1868,17 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, "ever_released": result in released_vars, "pool": False} body.append(Let(handle, Acquire("Disposable", [], line), line)) + else: + # Fail loud on an op this core cannot lower. Silently skipping it would + # drop the acquire/release facts nested inside it — fabricating a leak (a + # lost release) or hiding one (a lost acquire) while every existing fixture + # still passes. A NEW op is a vocabulary change, not an additive optional + # field, so it must bump OWNIR_VERSION on both the extractor and the core + # (see spec/OwnIR.md); until then, refuse rather than mis-analyze. + raise OwnIRError( + f"unknown OwnIR flow op {op!r} ({ffile}:{line}) — extractor/core " + f"vocabulary skew; a new op must bump OWNIR_VERSION (see spec/OwnIR.md)" + ) return body diff --git a/spec/OwnIR.md b/spec/OwnIR.md new file mode 100644 index 00000000..ce806edc --- /dev/null +++ b/spec/OwnIR.md @@ -0,0 +1,211 @@ +# OwnIR Specification + +> **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)). +> Forward-looking ideas live in [`docs/proposals/`](../docs/proposals/), never +> here. + +OwnIR is the **seam** between a language frontend and the OwnLang core: a +frontend (the Roslyn C# extractor, the OwnTS spike, or a hand-written fixture) +emits *facts* in this vocabulary, and the Python core +([`ownlang/ownir.py`](../ownlang/ownir.py)) lowers them onto the same checker the +`.own` DSL uses. There is **one checker** — a frontend never renders a verdict, +only facts. OwnIR is a data schema at rest (JSON), not a language. + +## 1. Envelope + +A facts document is a single JSON object: + +```json +{ + "ownir_version": 0, + "module": "WpfApp", + "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) */ ] +} +``` + +`ownir_version` (int) and `module` (string) are required; `components`, +`functions`, `services`, and `effects` are each optional and default 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 +a present-but-unknown resource kind are all rejected at load, before any analysis. + +## 2. Versioning and the evolution policy (normative) + +`OWNIR_VERSION` is a single integer, defined in +[`ownlang/ownir.py`](../ownlang/ownir.py) and **stamped identically by every +producer**: the Python core, the Roslyn extractor (`OwnSharp.Extractor`), and the +OwnTS frontend. A document whose `ownir_version` differs from the core's raises +`OwnIRError` at load — a mismatched extractor/core pair fails loudly rather than +silently mis-reading facts. A document that omits the field is read as the +current version (legacy v0 producers). + +What bumps the version — the rule that keeps the three producers honest: + +| Change | Bumps `OWNIR_VERSION`? | +|---|---| +| Add an **optional** field with a safe default (e.g. `type`, `source_type`) | **No** — an older core reads the record without it (see §4). | +| Add a new **resource kind** discriminator value (§4) | **Yes** — the kind selects the analysis path (§4 routing), so it is a vocabulary change, not additive metadata; a present-but-unknown kind is rejected at load. | +| Add, rename, remove, or change the meaning of a **flow op** (§5) | **Yes** — vocabulary change (see the guard below). | +| Remove or rename a required field, or change a field's semantics | **Yes** — not backward-readable. | + +**Fail-loud guarantee (unknown vocabulary).** Two discriminators select an +analysis path and so must never be silently mis-read: + +- **Flow op (§5).** The flow lowerer (`_lower_flow`) handles exactly the ops in + [§5](#5-flow-bodies-functions); any other op raises `OwnIRError` — never a + silent skip, because skipping a compound op would drop the acquire/release facts + nested inside it and flip verdicts (a fabricated leak from a lost release, or a + hidden leak from a lost acquire) while every existing fixture still passes. +- **Resource kind (§4).** A `resource` value the core does not know changes + routing (`capture` → the region engine, `pool` → a pooled buffer, …), so a + present-but-unknown kind raises at load rather than falling through to the + `subscription` path and mis-classifying the fact. An **absent** `resource` + field still defaults to `subscription` — that is the old-extractor-predates-the- + field case, and adding the field is genuinely additive. + +A newer extractor that introduces either against an un-bumped core therefore fails +the run instead of mis-analyzing it — which is why both **must** bump +`OWNIR_VERSION` per the table above. + +## 3. What OwnIR is not + +Verdict logic never lives in a frontend. The core's diagnostics (OWN0xx) come +from the same analyses the `.own` path uses +([OwnCore.md](OwnCore.md), [Lifetimes.md](Lifetimes.md), the DI/effect analyses). +The bridge's own **drift tripwire**: if the core emits a diagnostic the bridge +cannot map back to a fact handle, the bridge raises rather than dropping the +finding — a frontend cannot silently lose a verdict. + +## 4. Owned-resource records (`components[].subscriptions[]`) + +Each component has a `name`, a `file`, and a list historically keyed +`subscriptions` (it is really the list of owned-resource records). Each record +carries a `line` and, optionally, `released` (bool) and a `resource` +discriminator. An unreleased record is the core's **OWN001** (owned-but-not- +released) at `line`; a released one nets to a balanced acquire/release and stays +silent. The `resource`/`type` fields are additive (§2), so an older core reads +every record as a `subscription`. + +| `resource` | Meaning | Tag | +|---|---|---| +| `subscription` (default) | `event +=` acquires; a matching `-=` releases | `[resource: subscription token]` | +| `timer` | a started `DispatcherTimer`/`Timer` whose `Tick`/`Elapsed` is never detached/stopped | `[resource: timer]` | +| `disposable` | an `IDisposable` field the class `new`s and never `Dispose()`s (optional `type`) | `[resource: disposable field]` | +| `subscribe` | an `X.Subscribe(...)` whose `IDisposable` result is ignored (tiered by `source`, below) | `[resource: subscription token]` | +| `capture` | a *tokenless* strong subscription whose event source provably outlives the subscriber — routes to the **lifetime/region** engine, surfaces as **OWN014** (region escape), not OWN001 | `[resource: subscription token]` | +| `local-disposable` | a local `new` of an `IDisposable` type, never disposed, not `using`-guarded, not returned | `[resource: disposable]` | +| `pool` | an `ArrayPool`/`MemoryPool` buffer `Rent`ed but never `Return`ed | `[resource: pooled buffer]` | +| `unresolved-subscription` | a `+=` whose LHS could not be bound to an event (external unreferenced assembly) — **not** owned; surfaced as advisory **OWN050**, never a leak | — | + +**Source tiers** (for `subscription`/`subscribe`/`capture`, via the record's +`source`): `self` (a self-rooted, GC-collectible cycle → silent), `injected` +(unknown lifetime → OWN001 *warning*; may escalate via the DI graph, §6), +`static`/external/`unknown` (process- or longer-lived → leak). The region model +(`capture`) is precise where the token model only warns. + +## 5. Flow bodies (`functions[]`) + +A flow function has a `name`, a `file`, and a `body`: an ordered list of flow +ops modelling one method's intra-procedural CFG (P-016). Each op has an `op` and +a `line`. The lowerer mints a globally-unique handle per acquire so a finding +maps back to the exact C# local. The **complete** op vocabulary: + +| `op` | Fields | Lowers to | +|---|---|---| +| `acquire` | `var`, optional `kind` (`"pool"`) | a new owned local (`Let`+`Acquire`); `kind:"pool"` tags it a pooled buffer | +| `release` | `var` | `Release` of the local's handle | +| `use` | `var` | `Use` of the handle | +| `overspan` | `var` | `Overspan` (POOL005: a full-length view of a pooled buffer) | +| `return` | optional `var` | `Return` (ownership transfer out) | +| `alias_join` | `var`, `src` | a new owning handle joined to `src`'s alias set (wrap/adopt, D5.4) | +| `call` | `callee`, `args`, optional `result` | a `Call` checked against the callee's contract; a `fresh`-returning callee mints an acquire for `result` (D5.2) | +| `if` | `then`, `else` (sub-bodies) | an `If` with both branches lowered | +| `while` | `body` (sub-body) | a `While` — a back-edge the core's worklist fixpoint converges over (A1) | + +Anything else is a hard error (§2, fail-loud). Overwriting a tracked local (a +re-bound `call` result or `alias_join` target) kills its previous ownership +binding, so a lost prior obligation leaks rather than reading as clean. + +## 6. DI registration graph (`services[]`) + +An optional array feeding the **DI001** captive-dependency check (P-006), a +separate core analysis ([`ownlang/di.py`](../ownlang/di.py)): + +```json +"services": [ + {"name": "EmailSender", "lifetime": "singleton", "deps": ["AppDbContext"], + "file": "Startup.cs", "line": 12}, + {"name": "AppDbContext", "lifetime": "scoped", "deps": []} +] +``` + +`lifetime` ∈ {`singleton`, `scoped`, `transient`}. A singleton that reaches a +scoped service — directly or through a transient — is a DI001 finding at its +registration site. The graph is additive/optional (§2). It also feeds the region +engine: an `injected` subscription carrying a `source_type` that resolves here +uses that type's DI lifetime as a region (singleton > scoped > transient), so a +source proven to outlive the subscriber escalates its OWN001 warning to **OWN014** +(a proven captive/region escape); a co-lifetimed-or-shorter source is refuted and +silent; an unresolved `source_type` stays the honest OWN001 warning. + +## 7. Reactive effects (`effects[]`) + +An optional top-level array feeding the **EFF001** effect-storm check (P-020, the +OwnTS `Own.React` profile) — a separate core analysis +([`ownlang/effects.py`](../ownlang/effects.py)) over an effect's dependency array +and the stability of the render-scope values it closes over: + +```json +"effects": [ + {"io": true, "line": 20, "deps": ["query"], + "bindings": [{"name": "query", "init": "useState", "refs": [], "line": 8}]} +] +``` + +Each effect carries `io` (bool — whether it performs I/O; default `false`), +`line` (int), `deps` (array of dependency names), and `bindings` (the render-scope +binding table: each a `{name, init, refs, line}` — an unstable dependency, e.g. an +object/array rebuilt every render, re-triggers the effect). An I/O effect whose +dep is unstable is EFF001 (the effect storm — "not all lifecycle bugs leak memory; +some leak requests"). Like `services`, this block is additive/optional; the core +decides identity stability, not the frontend. + +## 8. Rules + +- **IR1.** `ownir_version` must equal the core's `OWNIR_VERSION` (or be absent); + otherwise `load()` raises `OwnIRError`. +- **IR2.** Every producer stamps the same `OWNIR_VERSION`. +- **IR3.** Additive optional *fields* do **not** bump the version; a new/changed/ + removed **flow op** or **resource-kind value**, or a changed/removed required + field, **does** (both are analysis-path vocabulary — see IR4). +- **IR4.** A present-but-unknown **flow op** or **resource kind** raises + `OwnIRError` — never a silent skip or a fall-through to the wrong path. +- **IR5.** A core diagnostic the bridge cannot map to a fact handle raises — + never a silently dropped verdict. +- **IR6.** A frontend emits facts only; all verdicts come from the core. + +## 9. 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, +not a surface-language rule): + +- **IR1/IR2** — a mismatched `ownir_version` raises; a versionless document is + accepted as current; each frontend producer's `ownir_version` literal is + asserted equal to the core's `OWNIR_VERSION`. +- **IR4** — a `functions[].body` with an unknown op (`{"op": "try", …}`) raises + `OwnIRError`; likewise a present-but-unknown `resource` kind. +- **IR5** — the unmappable-diagnostic tripwire is an internal invariant + exercised by the flow/escape fixtures (a broken handle mapping would raise + "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. + +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/README.md b/spec/README.md index 6e26e54f..38602c91 100644 --- a/spec/README.md +++ b/spec/README.md @@ -14,6 +14,7 @@ stop aspirational docs from lying about the code. | [Lifetimes.md](Lifetimes.md) | lifetime regions and the region-escape theorem, rules L1–L4 | | [Diagnostics.md](Diagnostics.md) | every OWN code, grouped, linked to the rule that raises it | | [CodegenContract.md](CodegenContract.md) | the checker↔codegen contract C1–C4, lowering modes | +| [OwnIR.md](OwnIR.md) | the frontend↔core fact seam (JSON): envelope, versioning + evolution policy, resource-kind + flow-op vocabulary, DI graph, rules IR1–IR6 | | [CLI.md](CLI.md) | the `check` / `emit` / `cfg` / `report` commands | ## Spec ↔ tests (conformance) diff --git a/tests/run_tests.py b/tests/run_tests.py index a2fcb3bd..6cccc9cb 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1058,102 +1058,37 @@ def run() -> int: print(f"ordering: {'PASS' if not order_fails else 'FAIL'}") print(f"helper: {'PASS' if not helper_fails else 'FAIL'}") - # Content-level codegen assertions + property fuzzer: these inspect the - # generated C# itself (release placement/count, declaration order), catching - # lowerings that are silently wrong rather than ones that merely throw. - import test_codegen - cc_rc = test_codegen.run() - import test_codegen_props - pf_rc = test_codegen_props.run(iterations=3000, seed=1234) - - # The "what it catches" gallery: every examples/gallery/ file must still - # produce exactly the diagnostic it advertises, so the demo can't drift. - import test_gallery - gl_rc = test_gallery.run() - - # Real-world corpus: each case.own (a reduction of a real ArrayPool/Dispose - # bug) must still produce the diagnostics it documents. - import test_corpus - co_rc = test_corpus.run() - - # WPF lifetime corpus (lifetimes slice #1): subscription/timer leaks caught - # by the generic ownership checker, carrying the [resource: ] tag. - import test_wpf - wpf_rc = test_wpf.run() - - # Lifetime-region analysis (lifetimes slice #2): the region-escape theorem - # (a short-lived object captured by a longer-lived source -> OWN014). - import test_lifetimes - lt_rc = test_lifetimes.run() - - # Loop support (P-016 A1): `while` is analysed via a worklist fixpoint over the - # back-edge — cross-iteration leak/use-after-release/double-release, not OWN020. - import test_loops - loops_rc = test_loops.run() - - # Spec conformance pilot: every normative spec/ rule fires on its example. - import test_spec - spec_rc = test_spec.run() - - # OwnIR fact bridge (P-001): C#-extracted facts route through the core and - # surface a subscription leak at its C# location. - import test_ownir - ownir_rc = test_ownir.run() - - # Interprocedural ownership summaries (P-005 D5.0): the MOS solver — transfer - # lattice, depth-capped forward resolution, recursion convergence. Infra only; - # no findings wired yet (D5.1+). - import test_ownership - own5_rc = test_ownership.run() - - # RID indirection (P-005 D5.4 step 0): the no-op handle->RID layer the alias - # model (step 1) builds on — 1:1 identity, the join invariant, behaviour - # unchanged. - import test_rid - rid_rc = test_rid.run() - - # Diagnostic rendering (P-015): the empty-evidence invariant (render()/render_pretty() - # byte-for-byte unchanged) plus the ordered `note:` slice and the SARIF evidence builders. - import test_diagnostics - diag_rc = test_diagnostics.run() - - # `explain` command: the diagnostic-catalogue CLI surface (text + exit codes + - # --json code harvest + DI catalogue coverage + dispatch). - import test_explain - explain_rc = test_explain.run() - - # Evidence coverage (execution-surfaces ADR §3/§5): OWN015/OWN016/OWN005 carry - # a structured acquire->escape / move->use reachability slice, rendered as - # ordered `note:` lines, with the merge-point move site labelled honestly. - import test_evidence_coverage - evid_rc = test_evidence_coverage.run() - - # Flow-diagnostic SARIF (execution-surfaces ADR §3.1): `check --format sarif` - # projects each Diagnostic's evidence slice into SARIF relatedLocations / - # codeFlows via the shared ownlang.evidence builders, for GitHub code scanning. - import test_diag_sarif - dsarif_rc = test_diag_sarif.run() - - # Canonical CFG JSON seam (P-022 step 0): the frozen CFG-layer contract the - # Rust-port differential oracle diffs — envelope, symbol-table identity, - # instruction vocabulary, determinism. - import test_cfg_json - cfgjson_rc = test_cfg_json.run() - - # Reactive-effect stability (P-020): the EFF001 effect-storm analysis — the - # identity lattice, reference propagation, cycle safety, and the OwnIR bridge - # mapping the optional `effects` block to an EFF001 finding (a new core - # analysis dimension, like DI001, not the acquire/release leak model). - import test_effects - effects_rc = test_effects.run() + # Every sibling `test_*.py` module contributes a `run() -> int`. AUTO-DISCOVER + # them instead of importing each by hand and threading its rc through a + # hand-maintained `or` chain: a forgotten term there would silently drop a whole + # module from the gate (the exact failure this replaces). Adding a test file now + # needs no edit here. Each `run()` prints its own PASS/FAIL summary, so + # per-module output is preserved (the order is now sorted by filename). + # `test_codegen_props` takes an explicit lighter iteration count for the in-suite + # pass; every other module runs argless. + import importlib + + special = {"test_codegen_props": lambda m: m.run(iterations=3000, seed=1234)} + here = os.path.dirname(os.path.abspath(__file__)) + module_rcs: list[int] = [] + for fname in sorted(os.listdir(here)): + if not (fname.startswith("test_") and fname.endswith(".py")): + continue + name = fname[:-3] + mod = importlib.import_module(name) + runner = special.get(name) + if runner is None and not hasattr(mod, "run"): + print(f"run_tests: FAIL — {name} has no run(); every test_*.py must expose one") + module_rcs.append(1) + continue + module_rcs.append(runner(mod) if runner is not None else mod.run()) + if not module_rcs: + print("run_tests: FAIL — no test_*.py modules discovered") + return 1 return 1 if (failed or cg_fail or golden_fails or buffer_fails or escape_fails or branchy_fails or nest_fails - or order_fails or helper_fails or cc_rc or pf_rc - or gl_rc or co_rc or wpf_rc or lt_rc or loops_rc - or spec_rc or ownir_rc or own5_rc or rid_rc or diag_rc - or explain_rc or effects_rc or evid_rc or dsarif_rc - or cfgjson_rc) else 0 + or order_fails or helper_fails or any(module_rcs)) else 0 if __name__ == "__main__": diff --git a/tests/test_diagnostics.py b/tests/test_diagnostics.py index c4e0bd07..7809ffd6 100644 --- a/tests/test_diagnostics.py +++ b/tests/test_diagnostics.py @@ -29,7 +29,7 @@ sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) from ownlang import evidence -from ownlang.diagnostics import Diagnostic, Evidence +from ownlang.diagnostics import TITLES, Diagnostic, Evidence # a source whose line 3 names `b`, so render_pretty can place a caret under it. _SOURCE = "module M\nfn f() {\n use b;\n}\n" @@ -146,12 +146,28 @@ def _evidence_builders() -> list[str]: return fails +def _code_validation() -> list[str]: + """A Diagnostic must reject a code with no TITLES entry, so a typo can never + ship a titleless finding (the stringly-typed-code contract).""" + fails: list[str] = [] + try: + Diagnostic(code="OWN999", message="typo", line=1) + fails.append("an unknown diagnostic code was accepted (should raise ValueError)") + except ValueError: + pass + # a known code still constructs and titles correctly. + if Diagnostic(code="OWN001", message="m", line=1).title != TITLES["OWN001"]: + fails.append("a known code lost its title") + return fails + + def run() -> int: """Run every diagnostics-rendering case; return 0/1.""" fails: list[str] = [] fails += _empty_evidence_invariant() fails += _evidence_slice() fails += _evidence_builders() + fails += _code_validation() for f in fails: print(f"DIAGNOSTICS FAIL: {f}") print(f"diagnostics: {'PASS' if not fails else 'FAIL'} " diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 60ae713c..ad41320d 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -19,6 +19,7 @@ import json import os +import re import sys sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) @@ -229,6 +230,65 @@ def _sub(source: str | None) -> list[Finding]: except OwnIRError as e: fails.append(f"versionless facts wrongly rejected: {e}") + # an unknown flow op (a newer extractor emitting a vocabulary the core can't + # lower) must RAISE, not be silently dropped — else the acquire/release facts + # nested inside it vanish and verdicts flip with every fixture still green. + checks += 1 + unknown_op = {"ownir_version": OWNIR_VERSION, "module": "X", "components": [], + "functions": [{"name": "F", "file": "F.cs", "body": [ + {"op": "acquire", "var": "c", "line": 1}, + {"op": "try", "line": 2, "body": [ + {"op": "release", "var": "c", "line": 3}]}]}]} + try: + check_facts(unknown_op) + fails.append("unknown flow op was silently accepted (should raise OwnIRError)") + except OwnIRError: + pass + + # A present-but-unknown resource kind changes routing (§4), so load must reject + # it (fail-loud) rather than fall through to the subscription path and + # mis-classify. An ABSENT `resource` field still defaults to subscription. + checks += 1 + bad_kind = {"ownir_version": OWNIR_VERSION, "module": "X", + "components": [{"name": "C", "file": "C.cs", "subscriptions": [ + {"event": "e", "line": 1, "resource": "mutex"}]}]} + if not _load_raises(bad_kind): + fails.append("present-but-unknown resource kind was accepted (should raise OwnIRError)") + checks += 1 + ok_absent = {"ownir_version": OWNIR_VERSION, "module": "X", + "components": [{"name": "C", "file": "C.cs", "subscriptions": [ + {"event": "e", "line": 1}]}]} # no `resource` -> defaults to subscription + if _load_raises(ok_absent): + fails.append("an absent resource field was wrongly rejected (must default to subscription)") + + # Version single-sourcing (IR2): every producer must stamp the SAME + # ownir_version as the core. The literal is hand-kept in each frontend today — + # once P-022's `own-ir` crate lands there are FOUR producers, so a schema will + # make this a generated constant (spec/OwnIR.md §2). Until then, assert the + # frontends match the core here, so "bumped the core, forgot a frontend" (or the + # reverse) fails loudly instead of silently mis-reading facts at runtime. + _ver = re.compile(r'ownir_version["\s]*[=:]\s*(\d+)') + _repo = os.path.join(os.path.dirname(__file__), "..") + _producers = { + "Roslyn extractor (Program.cs)": + os.path.join(_repo, "frontend", "roslyn", "OwnSharp.Extractor", "Program.cs"), + "OwnTS frontend (ownts.py)": + os.path.join(_repo, "frontend", "ownts", "ownts.py"), + } + for _label, _path in _producers.items(): + checks += 1 + try: + with open(_path, encoding="utf-8") as _f: + _m = _ver.search(_f.read()) + except OSError as _e: + fails.append(f"{_label}: cannot read producer ({_e})") + continue + if _m is None: + fails.append(f"{_label}: no `ownir_version` literal found (moved? update this check)") + elif int(_m.group(1)) != OWNIR_VERSION: + fails.append(f"{_label}: ownir_version {_m.group(1)} != core OWNIR_VERSION " + f"{OWNIR_VERSION} — bump every producer together") + # --- WPF002 timer profile: a started timer never stopped/detached leaks, # a stopped one stays silent, and the finding is tagged [resource: timer]. with open(_TIMER_FIXTURE, encoding="utf-8") as f: