|
| 1 | +# P-037-X Stage 7 — the six frozen TypeScript twins through the unchanged core (EXPLORATORY) |
| 2 | + |
| 3 | +Research branch `research/p037-max-v1`. Pre-registered in Own.NET-paperwork |
| 4 | +`paper-eval/p037-max/stage7-cross-language-prereg-v1.json` (frozen before any TypeScript frontend |
| 5 | +change); evidence in `paper-eval/p037-max/stage7-cross-language-v1.json`. Architecture evidence |
| 6 | +only — never TypeScript support. #304 is frozen and unchanged. |
| 7 | + |
| 8 | +## 1. Gate (REPOSITORY FACT) |
| 9 | + |
| 10 | +Stage 7 runs "only if the core abstraction is stable": the kernel is untouched since Stage 2 and |
| 11 | +Stages 2b–4 changed the driver, the seam and the frontends only. Stages 5 and 6 are not entered |
| 12 | +by their own gates — Stage 4 revealed no transport need beyond the witness identity, and case 5's |
| 13 | +timing witness sits behind a record absence (the iterator carries no record: R). |
| 14 | + |
| 15 | +## 2. What was built (REPOSITORY FACT) |
| 16 | + |
| 17 | +A twin-only OwnIR `functions[]` emitter for the OwnTS spike (`frontend/ownts/ownts_p037x.py`, |
| 18 | +heuristic like the spike, no TypeScript parser), with the frozen rules: an interface with |
| 19 | +`close(): void` / `dispose(): void` is a resource type; a `declare function` returning one is an |
| 20 | +ambient factory (`acquire`); `r.close()` is a `release`; a statement-form call of an in-file |
| 21 | +function that carries a handle is one canonical `call` op plus the sidecar record with the raw |
| 22 | +argument facts by declared ordinal (var / param / param negated / bool_const / opaque); |
| 23 | +`if (p)` / `if (!p)` on an own boolean parameter is a body `if` plus a sidecar guard; `return e;` |
| 24 | +is a bare return; owned parameters carry their declared `ordinal` (R3), which `--no-ordinal` |
| 25 | +omits. The six Group E twins are copied byte for byte under `corpus/p037x-controls/ownts/` |
| 26 | +(sha256 asserted against the master prereg) next to the opaque-flag control. Zero core lines |
| 27 | +changed; the Stage 4 binaries are the ones every document ran through. |
| 28 | + |
| 29 | +## 3. Results (MEASURED OBSERVATION) |
| 30 | + |
| 31 | +| document | legacy (Python == Rust off) | guarded (Rust on) | report | held | |
| 32 | +|---|---|---|---|---| |
| 33 | +| e1 guarded-release bug | `OWN051` | `OWN001` | `closeUnlessKept.r = split(1) [no, must]`; the site selects pos → borrow | yes | |
| 34 | +| e2 guarded-release safe | `OWN051` | clean | the site selects neg → consume | yes | |
| 35 | +| e3 wrapper-id bug | `OWN051` | `OWN001` | `outer.r` imports `inner`'s split through the id edge; pos → borrow | yes | |
| 36 | +| e4 wrapper-id safe | `OWN051` | clean | neg → consume | yes | |
| 37 | +| e5 wrapper-neg bug | `OWN051` | `OWN001` | `outer.r = split(1) [must, no]` through the neg edge; `false` → neg → borrow | yes | |
| 38 | +| e6 wrapper-neg safe | `OWN051` | clean | `true` → pos → consume | yes | |
| 39 | +| X7-C1 opaque flag | `OWN051` | `OWN051` | the site is unselected (the join), never a fabricated release | yes | |
| 40 | +| X7-C2 no-ordinal facts | `OWN051` | `OWN051` | `NO_GUARDED_EVIDENCE(ordinal_map)`: the A17 allowlist knows C# type names only | yes | |
| 41 | + |
| 42 | +Leaked assumptions found: the A17 ordinal allowlist (C# type names) — present in the driver, |
| 43 | +neutralised by the R3 `params[].ordinal` fact (X7-C2 is the counterfactual: without the fact the |
| 44 | +TypeScript document cannot be placed); the diagnostic wording (`IDisposable local 'r' is never |
| 45 | +disposed` on a `.ts` file) — cosmetic; the `disposable` kind — a vocabulary word; `sig` and name |
| 46 | +handling — inert on TypeScript spellings. Nothing semantic. |
| 47 | + |
| 48 | +## 4. Cost and result |
| 49 | + |
| 50 | +Frontend-specific: the emitter (about 190 handwritten Python lines) and the pin test; core lines |
| 51 | +changed: 0; core reused: the Python reference, own-cli (door, bridge + seam, driver, kernel, |
| 52 | +core) and the report, all unchanged. **KEEP**: the frozen §8 rows 1/7/8 guarded semantics |
| 53 | +reproduce on TypeScript through the unchanged core, and the one C#-specific assumption the core |
| 54 | +carries is bypassed by a fact the C# side already emits. |
| 55 | + |
| 56 | +## 5. Not claimed |
| 57 | + |
| 58 | +TypeScript support; that Stage 4's relational facts work on TypeScript (not emitted, not |
| 59 | +exercised); that #304 is reopened. |
0 commit comments