feat(ownir): OwnIR contract hardening — spec, fail-loud guards, version single-sourcing

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
 

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -2509,9 +2509,15 @@
 //     `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
@@ -3331,7 +3337,7 @@
     .Split(Path.PathSeparator, StringSplitOptions.RemoveEmptyEntries)
     .Where(p => p.EndsWith(".dll", StringComparison.OrdinalIgnoreCase))
     .ToList();
 var refNames = new HashSet<string>(tpa.Select(Path.GetFileName), StringComparer.OrdinalIgnoreCase);
 var references = tpa.Select(p => (MetadataReference)MetadataReference.CreateFromFile(p)).ToList();
 // P-004 WPF profile: widen the reference set with assemblies named by the
 // OWN_EXTRA_REF_DIRS env var (colon-separated dirs) — e.g. the WindowsDesktop ref

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)

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 ""

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