feat(ownir)!: OwnIR v2 — must-understand proven_call (H1) + T0 Amendment 2

audit/static/run_static.py

@@ -363,7 +363,7 @@ def check(ok: bool, msg: str) -> None:  # total derives from the call count
 
     def _fake_own_check(target_, out_dir_, severity_, root=None):
         facts = Path(out_dir_) / "own-check.facts.json"
-        facts.write_text(json.dumps({"ownir_version": 1, "module": "App", "components": [
+        facts.write_text(json.dumps({"ownir_version": 2, "module": "App", "components": [
             {"name": "CustomerView", "file": "Views/CustomerView.xaml.cs", "subscriptions": [
                 {"event": "_bus.Changed", "handler": "OnChanged", "line": 21,
                  "released": False}]}]}), encoding="utf-8")
@@ -419,7 +419,7 @@ def _fake_own_check(target_, out_dir_, severity_, root=None):
             '             x:Class="App.Views.CustomerView" Loaded="OnLoaded" />\n',
             encoding="utf-8")
         (out5 / "own-check.facts.json").write_text(json.dumps({
-            "ownir_version": 1, "module": "Stale", "components": [
+            "ownir_version": 2, "module": "Stale", "components": [
                 {"name": "CustomerView", "file": "Views/CustomerView.xaml.cs",
                  "subscriptions": [{"event": "_bus.Changed", "handler": "OnChanged",
                                     "line": 21, "released": False}]}]}), encoding="utf-8")

audit/static/tools/xaml_join.py

@@ -303,7 +303,7 @@ def check(ok: bool, msg: str) -> None:
          "event_handlers": [{"event": "Loaded", "handler": "OnLoaded", "line": 4}],
          "bindings": [], "named_elements": []},
     ]}
-    ownir = {"ownir_version": 1, "module": "App", "components": [
+    ownir = {"ownir_version": 2, "module": "App", "components": [
         {"name": "CustomerView", "file": "Views/CustomerView.xaml.cs", "subscriptions": [
             {"event": "_bus.Changed", "handler": "OnChanged", "line": 21, "released": False}]},
         {"name": "CleanView", "file": "Views/CleanView.xaml.cs", "subscriptions": [
@@ -363,7 +363,7 @@ def check(ok: bool, msg: str) -> None:
     wrong_ns = {"documents": [{"file": "Features/Billing/CustomerView.xaml",
                 "x_class": "Billing.CustomerView",
                 "event_handlers": [{"event": "Loaded", "handler": "OnLoaded", "line": 4}]}]}
-    other = {"ownir_version": 1, "components": [
+    other = {"ownir_version": 2, "components": [
         {"name": "CustomerView", "file": "Legacy/CustomerView.cs", "subscriptions": [
             {"event": "_bus.Changed", "handler": "OnChanged", "line": 9, "released": False}]}]}
     check(join(wrong_ns, other) == [],

docs/evidence/calibration/p022-263a-design-constants.json

@@ -1,6 +1,6 @@
 {
   "artifact": "p022-263a-calibration-design-constants",
-  "bound_measurement_harness_digest": "1a26aa63fd5fbbe06e7ae72dd5e1c8f2d611bff8856af4a5b93ae36d2d23a9b1",
+  "bound_measurement_harness_digest": "b92f08c990fcf6d74df29aad333b330b6c3c4f9e1c1bad55efe8164c39dea57c",
   "bound_policy_implementation_digest": "c3068ed7fa880a7083866ead25fe8bf65c87889d242d8af1f7eee01582cd5cbf",
   "constants": {
     "G": [

docs/evidence/calibration/p022-263a-policy-freeze.json

@@ -1,6 +1,6 @@
 {
   "artifact": "p022-263a-calibration-policy-freeze",
-  "measurement_harness_digest": "1a26aa63fd5fbbe06e7ae72dd5e1c8f2d611bff8856af4a5b93ae36d2d23a9b1",
+  "measurement_harness_digest": "b92f08c990fcf6d74df29aad333b330b6c3c4f9e1c1bad55efe8164c39dea57c",
   "policy_implementation_digest": "c3068ed7fa880a7083866ead25fe8bf65c87889d242d8af1f7eee01582cd5cbf",
   "policy_implementation_digest_framing": "sha256 over the source set ordered by the UTF-8 bytes of each repo-relative POSIX path. Each file contributes, with no header and no separator: its path byte length as an 8-byte big-endian unsigned integer, its path's exact UTF-8 bytes, its blob byte length as an 8-byte big-endian unsigned integer, and its exact git blob bytes.",
   "policy_source_commit": "b4f657a0abdfdfaae199cbc7eee0c47acd8b0057",

docs/evidence/calibration/p022-263a-training-preregistration.json

@@ -30,8 +30,8 @@
   "anchor_commit": "eedf6d3ed44ecf7bda69fa509dcd23b45960cf76",
   "artifact": "p022-263a-calibration-training-preregistration",
   "bindings": {
-    "design_constants_blob_sha1": "0ff316d5aea6af92c01679babaf0f0251191dcee",
-    "measurement_harness_digest": "1a26aa63fd5fbbe06e7ae72dd5e1c8f2d611bff8856af4a5b93ae36d2d23a9b1",
+    "design_constants_blob_sha1": "1059a69fe53ff3c2286414731e6104f848596ca7",
+    "measurement_harness_digest": "b92f08c990fcf6d74df29aad333b330b6c3c4f9e1c1bad55efe8164c39dea57c",
     "policy_implementation_digest": "c3068ed7fa880a7083866ead25fe8bf65c87889d242d8af1f7eee01582cd5cbf",
     "training_scope_implementation_digest": "614bf9efe6ba2bb10e26a251c10d6c4a8fdaa99985d43ea03d76c6774447d25b",
     "training_scope_root": "scripts/training/"

docs/generated/p022-coord-census.md

@@ -10,8 +10,8 @@ Value classes follow the cp1 taxonomy's axis rather than blurring it: `outside-i
 
 | measure                            | value |
 |------------------------------------|------:|
-| JSON files scanned                 | 625 |
-| coordinate slots found             | 4175 |
+| JSON files scanned                 | 709 |
+| coordinate slots found             | 4535 |
 
 ## By value class
 
@@ -21,12 +21,12 @@ Value classes follow the cp1 taxonomy's axis rather than blurring it: `outside-i
 | `below-1` | 23 | 23 |
 | `bool` | 18 | 17 |
 | `float` | 3 | 3 |
-| `in-domain` | 3480 | 2193 |
+| `in-domain` | 3796 | 2424 |
 | `negative` | 26 | 26 |
-| `null` | 259 | 9 |
+| `null` | 261 | 9 |
 | `outside-int64` | 15 | 15 |
 | `string` | 19 | 19 |
-| `zero` | 308 | 26 |
+| `zero` | 350 | 26 |
 
 ## By family and slot
 
@@ -162,10 +162,12 @@ Value classes follow the cp1 taxonomy's axis rather than blurring it: `outside-i
 | `heap_effects` | `summaries[].line` | `in-domain` | — | 56 | 10 | — |
 | `lowered` | `components[].subscriptions[].line` | `in-domain` | yes | 24 | 10 | — |
 | `lowered` | `functions[].<nested>[].column` | `in-domain` | yes | 2 | 2 | — |
-| `lowered` | `functions[].<nested>[].line` | `in-domain` | yes | 903 | 112 | — |
-| `lowered` | `functions[].params[].line` | `in-domain` | yes | 460 | 79 | — |
+| `lowered` | `functions[].<nested>[].line` | `in-domain` | yes | 1082 | 138 | — |
+| `lowered` | `functions[].params[].line` | `in-domain` | yes | 512 | 105 | — |
 | `lowered` | `functions[].params[].line` | `zero` | yes | 4 | 3 | — |
-| `lowered` | `handles[].line` | `in-domain` | — | 343 | 56 | — |
+| `lowered` | `handles[].line` | `in-domain` | — | 363 | 61 | — |
+| `lowered` | `heap_effects.methods[].calls[].line` | `in-domain` | — | 25 | 17 | — |
+| `lowered` | `heap_effects.methods[].line` | `in-domain` | — | 38 | 18 | — |
 | `lowered` | `services[].line` | `in-domain` | yes | 2 | 1 | — |
 | `ownir` | `components[].subscriptions[].column` | `in-domain` | yes | 2 | 1 | — |
 | `ownir` | `components[].subscriptions[].line` | `in-domain` | yes | 20 | 10 | — |
@@ -201,7 +203,7 @@ Value classes follow the cp1 taxonomy's axis rather than blurring it: `outside-i
 | `repro` | `traces[].layers[].steps[].value.params[].line` | `in-domain` | — | 4 | 1 | — |
 | `summaries` | `functions[].<nested>[].line` | `in-domain` | yes | 37 | 9 | — |
 | `summaries` | `functions[].params[].line` | `in-domain` | yes | 25 | 8 | — |
-| `summaries` | `summaries[].line` | `zero` | — | 252 | 63 | — |
+| `summaries` | `summaries[].line` | `zero` | — | 294 | 84 | — |
 | `verdict_renders` | `components[].subscriptions[].column` | `in-domain` | yes | 1 | 1 | — |
 | `verdict_renders` | `components[].subscriptions[].line` | `in-domain` | yes | 11 | 5 | — |
 | `verdict_renders` | `functions[].<nested>[].line` | `in-domain` | yes | 3 | 2 | — |
@@ -220,8 +222,8 @@ Value classes follow the cp1 taxonomy's axis rather than blurring it: `outside-i
 | `verdicts` | `effects[].line` | `negative` | yes | 1 | 1 | `-3` |
 | `verdicts` | `effects[].line` | `zero` | yes | 1 | 1 | — |
 | `verdicts` | `findings[].column` | `in-domain` | — | 17 | 7 | — |
-| `verdicts` | `findings[].column` | `null` | — | 198 | 93 | — |
-| `verdicts` | `findings[].line` | `in-domain` | — | 200 | 89 | — |
+| `verdicts` | `findings[].column` | `null` | — | 200 | 95 | — |
+| `verdicts` | `findings[].line` | `in-domain` | — | 202 | 91 | — |
 | `verdicts` | `findings[].line` | `zero` | — | 15 | 12 | — |
 | `verdicts` | `functions[].<nested>[].column` | `below-1` | yes | 1 | 1 | `0` |
 | `verdicts` | `functions[].<nested>[].column` | `in-domain` | yes | 7 | 2 | — |

docs/generated/p022-cp4-census.md

@@ -8,18 +8,18 @@ Computed by `tests/verdict_census.py` and `tests/verdict_render_census.py` (the
 
 | measure                                                                 | value |
 |-------------------------------------------------------------------------|------:|
-| goldens — Python's complete truth, one per planned case                 | 133 |
+| goldens — Python's complete truth, one per planned case                 | 154 |
 | … swept from `tests/fixtures/ownir`                                     | 22 |
-| … swept from `tests/fixtures/lowered`                                   | 64 |
+| … swept from `tests/fixtures/lowered`                                   | 85 |
 | … swept from `tests/fixtures/summaries`                                 | 9 |
 | … synthetic controls (`manifest.json` cases)                            | 38 |
-| reference refusals over all goldens                                     | 9 |
-| reference findings over all goldens                                     | 215 |
+| reference refusals over all goldens                                     | 25 |
+| reference findings over all goldens                                     | 217 |
 | declared Rust exclusions — the executable ledger `rust_replay_excluded` | 2 |
 | … refused at the typed `OwnIr` door (#294 OD-1)                         | 2 |
-| replayed by Rust (goldens minus exclusions)                             | 131 |
-| … reference refusals among them (compared in full)                      | 9 |
-| … findings among them (compared on every `Finding` member)              | 213 |
+| replayed by Rust (goldens minus exclusions)                             | 152 |
+| … reference refusals among them (compared in full)                      | 25 |
+| … findings among them (compared on every `Finding` member)              | 215 |
 
 The differential counts over the replayed set — Python-only, Rust-only, changed, ordering-only, unexplained — are asserted, not measured here: the Rust replay compares every replayed case's full ordered verdict list (or its refusal text) against the golden on every member, collects every divergence without fail-fast, and fails if one exists. A green `cargo test -p own-bridge --test verdicts` is 0 / 0 / 0 / 0 / 0 by construction; a non-zero count is a red build.
 

docs/generated/p022-cp5-inventory.md

@@ -26,7 +26,7 @@ Checkpoint 4 proved identity, anchor, kind and tiering over the replayed set ([c
 | `flowlocal_own008` | bridge | flow-local release while borrowed | 1 | 1 |
 | `flowlocal_own011` | bridge | flow-local exclusive re-borrow | 4 | 4 |
 | `flowlocal_own012` | bridge | flow-local shared borrow under an exclusive one | 2 | 2 |
-| `flowlocal_own013` | bridge | flow-local direct use under an exclusive borrow | 5 | 5 |
+| `flowlocal_own013` | bridge | flow-local direct use under an exclusive borrow | 7 | 7 |
 | `flowlocal_own005_pool` | bridge | flow-local use after move on a pooled buffer | 1 | 1 |
 | `flowlocal_own007_pool` | bridge | flow-local consume/return while borrowed on a pooled buffer | 1 | 1 |
 | `flowlocal_own008_pool` | bridge | flow-local release while borrowed on a pooled buffer | 1 | 1 |

docs/generated/p022-shadow-census.md

@@ -24,12 +24,12 @@ acceptance work.
 
 | corpus | documents |
 |---|---|
-| `tests/fixtures/lowered` | 64 |
+| `tests/fixtures/lowered` | 85 |
 | `tests/fixtures/ownir` | 22 |
 | `tests/fixtures/repro` | 3 |
 | `tests/fixtures/summaries` | 9 |
 | `tests/fixtures/verdicts` | 38 |
-| **total** | **136** |
+| **total** | **157** |
 
 Every one of those documents is canonicalized and hashed by the reference
 (`ownlang/repro.py`) and re-hashed from the same file by the port
@@ -43,8 +43,8 @@ refuses to carry a foreign entry that has none rather than filling one in.
 
 | surface | count |
 |---|---|
-| documents captured and digest-pinned | 136 |
-| tamper controls (one changed character per document, refusal required) | 136 |
+| documents captured and digest-pinned | 157 |
+| tamper controls (one changed character per document, refusal required) | 157 |
 | documents both engines must REFUSE to name (`domain_refusals`) | 6 |
 | reproduction artifacts committed and replayed byte-for-byte | 10 |
 | structural negative controls on `verify` (each side) | 34 |

docs/notes/h1-proven-call.md

@@ -0,0 +1,112 @@
+# H1 — proven calls in a state-protocol region (OwnIR v2)
+
+Status: **landed** (owner ruling: OwnIR v2 and T0 Amendment 2 approved for H1).
+Base: `main` = `1c70e867eb408d931ae3dfffd8c0b351190f6547`. Follows
+[`h1-transport-stop.md`](h1-transport-stop.md), which found that the only
+fail-loud transport is a version bump, and [`heap-effect-summaries.md`](heap-effect-summaries.md)
+(H0), whose summaries this slice consumes.
+
+## What changes for a C# user
+
+```csharp
+static int Twice(int x) => x * 2;
+
+Protocol.WithApproved(order, approved =>
+{
+    var n = Twice(21);   // before H1: refused. Now: admitted, clean.
+    approved.Ship();
+});
+```
+
+| Call inside a region | Before H1 | With H1 |
+|---|---|---|
+| direct call, touches no entity or token, proven harmless | refusal (extractor) | **admitted** |
+| same, but not proven harmless (a write, an escape, a global, Unknown anywhere) | refusal (extractor) | refusal (**core**, exit 2), naming the clause |
+| a call handed the borrowed entity (`Mutates(order)`) | `use` → verdict | unchanged |
+| an external, virtual, delegate or local-function call (`Console.WriteLine`) | refusal (extractor) | unchanged, same text |
+
+## The transport
+
+- **`proven_call`** (`site`, `callee`, `line`): a new flow op, so `OWNIR_VERSION` 1 → 2 (spec/OwnIR.md §2, §5.4).
+- **`heap_effects`:** a top-level section holding the H0 source facts. It holds one record per call site (the call expression walked like a body, every variable from outside it read as `heap`) and the records of the methods those sites reach through `direct` edges.
+- **The frontend decides nothing.** It emits a `proven_call` only for a call the summary layer could prove at all, meaning a call whose H0 dispatch is `direct`. The same shared classifier (`HeapEffectFacts.Dispatch`) produces both that decision and every H0 call fact.
+- **Fail-loud.** A v1 core refuses a v2 document on the stamp (IR1). With the stamp stripped it refuses on the unknown op (IR4). C1 below runs the real v1 core to show both.
+- **No compatibility shim** in either direction: a v2 core refuses v1 facts.
+
+## The decision
+
+The decision is made in the core and only there: `_admit_proven_calls` in `ownlang/ownir.py`, ported in `own-bridge/src/proven.rs`.
+
+1. **When:** at the head of `to_module` / `lower_full`, before any function is lowered. The pass walks every function body through `then`/`else`/`body`, so no lowering path can carry a `proven_call` past it.
+2. **The predicate:** `heap_effects.site_verdict` / `harmless`. It lives in the shared summary layer, not in typestate code.
+3. **Strict on purpose:** a reference returned without an alias is still refused (`returns == []`). Unknown fails every clause it reaches.
+
+Predicate v1. A site is admitted iff all of these hold:
+
+- the site record exists and calls `callee` directly;
+- every call in the site is `direct` to a summarized method, and each such method is harmless;
+- the site's own solved summary is harmless.
+
+A summary is harmless iff:
+
+- every parameter and the receiver are at most `borrow`;
+- `writes.instance`, `writes.static` and `writes.indirect` are all `none`;
+- `returns` is `[]`.
+
+Refusals are `OwnIRError`, with identical text in both engines, in this order (spec/Bridge.md BR-L14):
+
+1. a malformed `site` or `callee`;
+2. a `proven_call` outside a region;
+3. no `heap_effects` section;
+4. a malformed section;
+5. no site record;
+6. a site that is not proven harmless.
+
+## Evidence
+
+**Kill fixtures.** Real C# files in `frontend/roslyn/protocol-samples/cases/H1*.cs`; the facts are committed as `typestate_cs_h1*`.
+
+| Case | Result |
+|---|---|
+| `Twice(21)` | admitted, clean |
+| A → B → pure | admitted, clean |
+| pure SCC (`Even` ⇄ `Odd`) | admitted, clean |
+| `TouchesGlobalState()` | refused: `writes.static is may` |
+| A → B → global | refused: `writes.static is may` |
+| polluted SCC (`Ping` ⇄ `Pong` writes) | refused: `writes.static is may` |
+| A → `Console.WriteLine` | refused: `writes.instance is unknown` |
+| `Fill(buffer)`, outer array | refused: `parameter 0 is borrow_mut` |
+| `Mutates(order)` / `Escapes(order)` | OWN013, as before H1 |
+| R9 backdoor (`Backdoor.AnnotateLast()`) | refused, by the core now: `writes.instance is may` |
+| R18 `Console.WriteLine`, R19 interface call | refused by the extractor, unchanged |
+
+**Compatibility controls** (`tests/test_proven_call.py`):
+
+- **C1, old core on new facts.** `ownlang/` at `1c70e867` is taken out of git history and run on the extractor's v2 facts. It exits 2 on `schema v2, but this core understands v1`. With the stamp stripped it exits 2 on `unknown OwnIR flow op 'proven_call'`.
+- **C2/C3, missing or malformed evidence.** Eleven documents, each derived from the real H1a facts by one corruption, are refused. The Layer 2 goldens pin each text, and Rust replays them byte for byte. The corruptions:
+  - no section;
+  - no site record;
+  - `site` is not a string;
+  - empty `callee`;
+  - the op outside the region;
+  - a malformed section;
+  - the wrong callee;
+  - no callee record;
+  - an Unknown callee;
+  - an Unknown site;
+  - a virtual call inside the site.
+- **C4, Unknown is poison.** A predicate that reads Unknown as harmless admits the transitive-Unknown fixture and both Unknown-derived documents. The real predicate refuses all three, so the pinned refusals go red under the mutant. The same mutant in the Rust port turns the Layer 2 replay red.
+- **C5, the op cannot be dropped.** Dropping the admission pass, or dropping the op from the facts, turns the four refused kill fixtures clean. Both differ from the pinned ledgers. The Rust mutant with no `admit` call is caught by the replay.
+
+**Parity.**
+- The protocol gate's 29 C#-derived documents are byte-identical on both public CLIs.
+- The Layer 2, summaries, verdict, CLI, repro and validation ledgers are regenerated at v2 by their own writers and replayed by Rust.
+- The H0 sidecar goldens are unchanged.
+
+## Not in this slice
+
+- logger, BCL or annotation summaries: `Console.WriteLine` stays refused;
+- devirtualization;
+- property getters, constructors and operators inside a region: still refused by the extractor;
+- typed write targets, which would be needed to admit a write to state that is provably not the entity's type family;
+- DB-side mutation gaps.