|
| 1 | +# P-037-X Stage 4 — relational ownership flags: the (resource, ownsResource) pair (EXPLORATORY) |
| 2 | + |
| 3 | +Research branch `research/p037-max-v1`. Pre-registered in Own.NET-paperwork |
| 4 | +`paper-eval/p037-max/stage4-relational-prereg-v1.json` (frozen before any code of this stage); |
| 5 | +evidence in `paper-eval/p037-max/stage4-relational-v1.json`. #304 is frozen and unchanged; nothing |
| 6 | +here is a production result; the Python reference, the kernel and the owning-factory table are |
| 7 | +untouched. Wording: *P-037-X later made FinishSend's shape representable after exploratory |
| 8 | +extensions; the frozen instance remains behind the owning-factory boundary.* Never "case 2 recovered". |
| 9 | + |
| 10 | +## 1. The question and where it stood (REPOSITORY FACT) |
| 11 | + |
| 12 | +Stage 3 left case 2 (`HttpClient.FinishSend`) OUTSIDE_FROZEN_VOCABULARY: the callee's contract is |
| 13 | +exact (`FinishSend.cts = Split(disposeCts) [must, no]`), but every frozen site hands the resource |
| 14 | +over together with a caller local produced by the same producer (`(cts, disposeCts, _) = |
| 15 | +PrepareCancellationTokenSource(...)`), which G-A1 joins. The prereg's test: *does FinishSend become |
| 16 | +representable, and at what cost*. Three independent blockers stood between the frozen vocabulary |
| 17 | +and the site: the relation itself (vocabulary), the tuple-bound handle and the owned-slot gap of the |
| 18 | +canonical carrier (carrier), and the producer's fresh acquire (`CreateLinkedTokenSource` is outside |
| 19 | +the extractor's owning-factory table: an R boundary). The stage removes the first two generically |
| 20 | +and leaves the third untouched by rule. |
| 21 | + |
| 22 | +## 2. The abstraction (REPOSITORY FACT; six generic rules, none reads an API name) |
| 23 | + |
| 24 | +Behind two opt-ins (`OWEN_P037X_RELATIONAL=1` for the emission, the existing `OWEN_P037X_GUARDED=1` |
| 25 | +for the seam), with facts byte-identical otherwise: |
| 26 | + |
| 27 | +- **R4-1 producer facts.** A pair/tuple-returning record carries `result_slots[]` (`resource` | |
| 28 | + `flag` | `other`) and every `return` carries `values[]` aligned with them (a tracked local's name, |
| 29 | + a boolean literal, or null; `"opaque"` for a non-literal return). A `new`-created candidate |
| 30 | + returned inside such a tuple is the D5.2 transfer out, not an escape. |
| 31 | +- **R4-2 consumer facts.** A deconstruction of a first-party call is one `call` op with |
| 32 | + `results[]` by slot; the resource-slot designations are candidates the core decides on. |
| 33 | +- **R4-3 sidecar.** A boolean local nothing assigns after its binding is `flag_var{name}`; the |
| 34 | + driver reads it as `opaque` everywhere but the witness match. |
| 35 | +- **R4-4 relation.** Resource slot `i` is `fresh_iff(k)` when every literal return has |
| 36 | + (`values[i]` acquired in the body) ⇔ (`values[k] == true`), both polarities occur and no return |
| 37 | + is opaque. Always-fresh and never-fresh slots are deliberately no relation. |
| 38 | +- **R4-5 site rule.** A local bound at a related slot is owned-iff its witness. A later call whose |
| 39 | + callee coordinate for that slot is `Split(h)` with finalized cells `(must, no)` and whose |
| 40 | + argument at ordinal `h` is `flag_var{witness}` discharges it: the core sees the handoff and the |
| 41 | + name is unmapped at a top-level site (a nested site keeps the map — the legacy kill-site |
| 42 | + restriction, because the map is shared by every branch). Every other site keeps the frozen |
| 43 | + reading (the collapse → INF-A5b untracking with OWN051). |
| 44 | +- **R4-6 carrier.** An owned slot holding an untracked identifier is carried by that name; both |
| 45 | + engines apply the callee's contract per mapped argument and the filler is inert. |
| 46 | + |
| 47 | +Bounded by construction: one relation value per result slot in {none, fresh_iff(k)}, one witness |
| 48 | +name per handle, no state that grows with callers or paths; the kernel is untouched. |
| 49 | + |
| 50 | +## 3. Results (MEASURED OBSERVATION) |
| 51 | + |
| 52 | +| control (frozen) | off / facts-on+engine-off / Python | on | report | held | |
| 53 | +|---|---|---|---|---| |
| 54 | +| X4-P1 abstract shape | none | `OWN001` ×1 at `NeverCaller` (the owned path leaks) | `Produce` slot 0 `fresh_iff(1)`, slot 2 none; `Matched` (try/finally) and `MatchedPlain` RELATIONAL_DISCHARGE; `AlwaysCaller` must-discharged | yes | |
| 55 | +| X4-P2 case-2 SHAPE TWIN | none | none | `PrepareCancellationTokenSource` slot 0 `fresh_iff(1)`; RELATIONAL_DISCHARGE at every `FinishSend` site of the four callers; `HandleFailure` a borrow | yes | |
| 56 | +| X4-C1 unrelated flag | none | `OWN051` ×1 | witness `owns`, site carries `flag_var{other}`: no discharge | yes | |
| 57 | +| X4-C2 reassigned flag | none | `OWN051` ×1 | the site's argument is opaque (unstable local): no discharge | yes | |
| 58 | +| X4-C3 cross-association | none | `OWN051` ×2 (Crossed); Straight clean | Crossed: two witnessed, unmatched rows; Straight: two discharges | yes | |
| 59 | +| X4-C4 polarity | none | `OWN051` ×1 | `(no, must)` is not the match | yes | |
| 60 | +| X4-C5 owned-slot filler | none | none | `[first, r]` carried; `r` discharged; `first` never a handle | yes | |
| 61 | + |
| 62 | +Every historical row (F3 8/8, the #380 family, the gallery anchor, the shapes, the B0 probes, the |
| 63 | +B1 fixture, all 2b/2c/2d controls: 61 documents) is identical to Stage 2d in all three arms, with |
| 64 | +facts byte-identical off vs on (no pair-returning producer anywhere in them). B1 acceptance and |
| 65 | +every own-guarded test green (10 + 7 + 5 + 8). The frozen case 2 under the opt-in: the four |
| 66 | +`FinishSend` sites gain rows (`var:cts`, EQUAL, unselected, no witness) and no relation forms — |
| 67 | +`PrepareCancellationTokenSource` carries no record because its fresh CTS is a BCL factory outside |
| 68 | +the owning-factory table; verdict 0 in every arm; the frozen instance stays ANALYZER_SCOPE_LIMIT. |
| 69 | +Cases 1, 3, 4, 5, 6 unchanged in every arm. |
| 70 | + |
| 71 | +Population: repository tree (82 files): facts byte-identical to Stage 2d in both arms, verdicts |
| 72 | +identical (off 158 = Python, on 154 = Stage 2d on), 16 summary coordinates unchanged, no relation. |
| 73 | +Corpus (137 documents): facts byte-identical to Stage 2d without the opt-in and byte-identical off vs on on every document (no pair-returning producer in the population); the same 8 documents move on-vs-off as in Stage 2d (the F3 refinements) and no other; class totals unchanged (summary EQUAL 33 / NGE 7; application REFINEMENT 8 / EQUAL 17 / NGE 49); no relation, no discharge. |
| 74 | + |
| 75 | +Mutants (reader side, each rebuilt into the release engine): M1 (any flag at the guard ordinal matches) turns X4-C1 and X4-C3/Crossed clean and fails three acceptance tests; M2 (an opaque guard slot accepted when a witness exists) turns X4-C2 clean and fails its test; M3 (polarity ignored) turns X4-C4 clean and fails its test — each red at both levels, the reader restored to the recorded binaries (byte-identical digests after the rebuild). |
| 76 | + |
| 77 | +## 4. Cost (MEASURED; the ledger has the full entry) |
| 78 | + |
| 79 | +Handwritten lines against the Stage 3 tree: frontend +148/−2 (estimate +150..+220: within); core +413/−28 (own-guarded +275/−16, own-bridge +138/−12; estimate +180..+260: 1.59× the upper bound); joint +561 against +330..+480 (1.17×, within the frozen 1.5× criterion); tests and controls +215 (Rust) +43/−24 (Python harness) +386 (C# controls) +36/−1 (spec), fixtures/records +2248 (JSON, not code). New: 2 IR concepts (the positional result relation; the flag witness), 3 schema |
| 80 | +fields + 1 sidecar argument kind, 1 relation value (`fresh_iff(k)`), 1 solver state (the witness |
| 81 | +binding, with the lowering depth that scopes the unmap); 0 lattice dimensions, 0 transforms, |
| 82 | +0 kernel lines, 0 Python lines. |
| 83 | + |
| 84 | +## 5. Result |
| 85 | + |
| 86 | +**KEEP** by the frozen decision rule — every control and expectation held, the mutants are red, the population did not move, no kernel or Python line changed, and the joint cost is within the criterion — with a recorded caveat: the core component alone is 1.59× its own estimate, so a per-component reading of the same rule says KEEP_BUT_COSTLY; this is the most expensive stage of the track, bought for one shape whose frozen instance still stands behind the owning-factory boundary. Stop condition G (complexity up sharply, instance-level real-witness coverage flat) is on the edge and is recorded as the boundary: any further step toward the frozen instance must buy an instance-level witness or the track stops on G. What the frozen instance still needs is one record — its fresh CTS is `CancellationTokenSource.CreateLinkedTokenSource`, outside the curated owning-factory set; extending that set for one row is forbidden here, and a generic factory rule is a production precision decision of the frontend, not a guard-vocabulary matter. |
| 87 | + |
| 88 | +## 6. Not claimed |
| 89 | + |
| 90 | +That #304 is reopened; that the frozen case 2 is recovered (the shape twin is not the frozen |
| 91 | +input); parity with the opt-ins on; a false-transfer report on the not-owned path of a `must` |
| 92 | +consumer (a stated limit); any change to the frozen census artefacts. |
0 commit comments