|
| 1 | +# H1 — proven calls in a state-protocol region (OwnIR v2) |
| 2 | + |
| 3 | +Status: **landed** (owner ruling: OwnIR v2 and T0 Amendment 2 approved for H1). |
| 4 | +Base: `main` = `1c70e867eb408d931ae3dfffd8c0b351190f6547`. Follows |
| 5 | +[`h1-transport-stop.md`](h1-transport-stop.md), which found that the only |
| 6 | +fail-loud transport is a version bump, and [`heap-effect-summaries.md`](heap-effect-summaries.md) |
| 7 | +(H0), whose summaries this slice consumes. |
| 8 | + |
| 9 | +## What changes for a C# user |
| 10 | + |
| 11 | +```csharp |
| 12 | +static int Twice(int x) => x * 2; |
| 13 | + |
| 14 | +Protocol.WithApproved(order, approved => |
| 15 | +{ |
| 16 | + var n = Twice(21); // before H1: refused. Now: admitted, clean. |
| 17 | + approved.Ship(); |
| 18 | +}); |
| 19 | +``` |
| 20 | + |
| 21 | +| Call inside a region | Before H1 | With H1 | |
| 22 | +|---|---|---| |
| 23 | +| direct call, touches no entity or token, proven harmless | refusal (extractor) | **admitted** | |
| 24 | +| same, but not proven harmless (a write, an escape, a global, Unknown anywhere) | refusal (extractor) | refusal (**core**, exit 2), naming the clause | |
| 25 | +| a call handed the borrowed entity (`Mutates(order)`) | `use` → verdict | unchanged | |
| 26 | +| an external, virtual, delegate or local-function call (`Console.WriteLine`) | refusal (extractor) | unchanged, same text | |
| 27 | + |
| 28 | +## The transport |
| 29 | + |
| 30 | +- **`proven_call`** (`site`, `callee`, `line`): a new flow op, so `OWNIR_VERSION` 1 → 2 (spec/OwnIR.md §2, §5.4). |
| 31 | +- **`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. |
| 32 | +- **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. |
| 33 | +- **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. |
| 34 | +- **No compatibility shim** in either direction: a v2 core refuses v1 facts. |
| 35 | + |
| 36 | +## The decision |
| 37 | + |
| 38 | +The decision is made in the core and only there: `_admit_proven_calls` in `ownlang/ownir.py`, ported in `own-bridge/src/proven.rs`. |
| 39 | + |
| 40 | +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. |
| 41 | +2. **The predicate:** `heap_effects.site_verdict` / `harmless`. It lives in the shared summary layer, not in typestate code. |
| 42 | +3. **Strict on purpose:** a reference returned without an alias is still refused (`returns == []`). Unknown fails every clause it reaches. |
| 43 | + |
| 44 | +Predicate v1. A site is admitted iff all of these hold: |
| 45 | + |
| 46 | +- the site record exists and calls `callee` directly; |
| 47 | +- every call in the site is `direct` to a summarized method, and each such method is harmless; |
| 48 | +- the site's own solved summary is harmless. |
| 49 | + |
| 50 | +A summary is harmless iff: |
| 51 | + |
| 52 | +- every parameter and the receiver are at most `borrow`; |
| 53 | +- `writes.instance`, `writes.static` and `writes.indirect` are all `none`; |
| 54 | +- `returns` is `[]`. |
| 55 | + |
| 56 | +Refusals are `OwnIRError`, with identical text in both engines, in this order (spec/Bridge.md BR-L14): |
| 57 | + |
| 58 | +1. a malformed `site` or `callee`; |
| 59 | +2. a `proven_call` outside a region; |
| 60 | +3. no `heap_effects` section; |
| 61 | +4. a malformed section; |
| 62 | +5. no site record; |
| 63 | +6. a site that is not proven harmless. |
| 64 | + |
| 65 | +## Evidence |
| 66 | + |
| 67 | +**Kill fixtures.** Real C# files in `frontend/roslyn/protocol-samples/cases/H1*.cs`; the facts are committed as `typestate_cs_h1*`. |
| 68 | + |
| 69 | +| Case | Result | |
| 70 | +|---|---| |
| 71 | +| `Twice(21)` | admitted, clean | |
| 72 | +| A → B → pure | admitted, clean | |
| 73 | +| pure SCC (`Even` ⇄ `Odd`) | admitted, clean | |
| 74 | +| `TouchesGlobalState()` | refused: `writes.static is may` | |
| 75 | +| A → B → global | refused: `writes.static is may` | |
| 76 | +| polluted SCC (`Ping` ⇄ `Pong` writes) | refused: `writes.static is may` | |
| 77 | +| A → `Console.WriteLine` | refused: `writes.instance is unknown` | |
| 78 | +| `Fill(buffer)`, outer array | refused: `parameter 0 is borrow_mut` | |
| 79 | +| `Mutates(order)` / `Escapes(order)` | OWN013, as before H1 | |
| 80 | +| R9 backdoor (`Backdoor.AnnotateLast()`) | refused, by the core now: `writes.instance is may` | |
| 81 | +| R18 `Console.WriteLine`, R19 interface call | refused by the extractor, unchanged | |
| 82 | + |
| 83 | +**Compatibility controls** (`tests/test_proven_call.py`): |
| 84 | + |
| 85 | +- **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'`. |
| 86 | +- **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: |
| 87 | + - no section; |
| 88 | + - no site record; |
| 89 | + - `site` is not a string; |
| 90 | + - empty `callee`; |
| 91 | + - the op outside the region; |
| 92 | + - a malformed section; |
| 93 | + - the wrong callee; |
| 94 | + - no callee record; |
| 95 | + - an Unknown callee; |
| 96 | + - an Unknown site; |
| 97 | + - a virtual call inside the site. |
| 98 | +- **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. |
| 99 | +- **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. |
| 100 | + |
| 101 | +**Parity.** |
| 102 | +- The protocol gate's 29 C#-derived documents are byte-identical on both public CLIs. |
| 103 | +- The Layer 2, summaries, verdict, CLI, repro and validation ledgers are regenerated at v2 by their own writers and replayed by Rust. |
| 104 | +- The H0 sidecar goldens are unchanged. |
| 105 | + |
| 106 | +## Not in this slice |
| 107 | + |
| 108 | +- logger, BCL or annotation summaries: `Console.WriteLine` stays refused; |
| 109 | +- devirtualization; |
| 110 | +- property getters, constructors and operators inside a region: still refused by the extractor; |
| 111 | +- typed write targets, which would be needed to admit a write to state that is provably not the entity's type family; |
| 112 | +- DB-side mutation gaps. |
0 commit comments