From 0ff0941ac53856b8f05e309c971fdee5e473a1e7 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Fri, 30 Oct 2026 07:33:04 +0000 Subject: [PATCH 1/2] chore: sync verify-native-lifecycle to c54051e MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The coverage record now names ghostty_terminal_set and its failure path, the DATA_MODE read, and Resize's second call. The "no JS inside native methods" assumption now says which methods read arguments before RequireTerminal, and that it was false for snapshot until #46. #48 changes only a test, and #49 changes only Feed's argument checks, so the model's Use(t) step still describes them. Drafted in workspace 36beaed175. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `xhigh`_ Change-Id: Iea32c157625764a4779be3eb8230069cc925a18a Signed-off-by: Thomas Kosiewski --- .agents/skills/verify-native-lifecycle/SKILL.md | 14 +++++++------- .../model/AddonEnvLifecycle.tla | 8 +++++--- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/.agents/skills/verify-native-lifecycle/SKILL.md b/.agents/skills/verify-native-lifecycle/SKILL.md index e060e82..058b96d 100644 --- a/.agents/skills/verify-native-lifecycle/SKILL.md +++ b/.agents/skills/verify-native-lifecycle/SKILL.md @@ -30,25 +30,25 @@ This check found F2 in `encodeMouse` while #12 was in review, so the bug never r Run this skill when the diff since the sync commit changes any covered code: ```sh -git diff --stat 7366b7545170ad77f5151e445c60bbf5bb110d87 -- native/ test/workers.test.ts test/mouse-safety.test.ts src/index.ts src/loader.ts package.json package-lock.json +git diff --stat c54051ec9a4d2eeed2ebf09533ac2e9175fcc79c -- native/ test/workers.test.ts test/mouse-safety.test.ts src/index.ts src/loader.ts package.json package-lock.json ``` Also run it when a change adds a new place that stores a `Napi::Reference`, `Napi::FunctionReference`, or other static or global state in `native/`, or a new path that frees or uses `terminal_` or `mouse_encoder_`. Static or global JS-facing state is the F1 bug class: keep it in the environment's instance data. A native method that copies a handle and then calls `Get()` is the F2 bug class: read every argument before you take the handles. ## Coverage record -Sync commit: `7366b7545170ad77f5151e445c60bbf5bb110d87`. At this commit the model describes the code below. Move the sync commit forward only after you confirm that the model still describes the covered code at the new commit. +Sync commit: `c54051ec9a4d2eeed2ebf09533ac2e9175fcc79c`. At this commit the model describes the code below. Move the sync commit forward only after you confirm that the model still describes the covered code at the new commit. | Code | Model | |---|---| | `native/terminal.cc` `TerminalWrap::Init` and `TerminalWrap::Create` keep the class reference in `env.SetInstanceData` / `env.GetInstanceData` | `CtorStorage = "per_env"`, variable `slot` | | `native/addon.cc` `InitAll`, `NODE_API_MODULE`; `native/terminal.cc` `TerminalWrap::Init` (asserts an empty instance-data slot, then `env.SetInstanceData`) | `LoadAddon(e)` | | `src/loader.ts` `loadNative` (caches the addon, so each env loads it once) | `LoadAddon` is enabled only while `env[e] = "idle"` | -| `src/index.ts` `createTerminal`; `native/terminal.cc` `CreateTerminal`, `TerminalWrap::Create` (`constructor->New`), `TerminalWrap::TerminalWrap` (`ghostty_terminal_new`, then `ghostty_mouse_encoder_new`) | `CreateTerminal(e, t)` | -| `native/terminal.cc` `TerminalWrap::TerminalWrap` when `ghostty_mouse_encoder_new` fails: it frees the terminal, sets `terminal_ = nullptr`, and throws, so `~TerminalWrap` does not run | `CreateFails(e, t)` | -| `src/index.ts` `feed`, `resize`, `snapshot`, `getVisibleText`, `formatPlain`, `formatHtml`, `#assertUsable`; `native/terminal.cc` the same methods and `RequireTerminal` | `Use(t)`, constants `TsDisposedGuard`, `NativeNullGuard` | +| `src/index.ts` `createTerminal`; `native/terminal.cc` `CreateTerminal`, `TerminalWrap::Create` (`constructor->New`), `TerminalWrap::TerminalWrap` (`ghostty_terminal_new`, `ghostty_terminal_set` for the scrollback byte limit, then `ghostty_mouse_encoder_new`) | `CreateTerminal(e, t)` | +| `native/terminal.cc` `TerminalWrap::TerminalWrap` when `ghostty_terminal_set` fails (it frees the terminal before it sets `terminal_`) or `ghostty_mouse_encoder_new` fails (it frees the terminal and sets `terminal_ = nullptr`), and throws, so `~TerminalWrap` does not run | `CreateFails(e, t)` | +| `src/index.ts` `feed`, `resize`, `snapshot`, `getVisibleText`, `formatPlain`, `formatHtml`, `#assertUsable`; `native/terminal.cc` the same methods and `RequireTerminal`. `Resize` can call `ghostty_terminal_resize` twice, with no JS between | `Use(t)`, constants `TsDisposedGuard`, `NativeNullGuard` | | `src/index.ts` `encodeMouse` (`#assertUsable`, then `normalizeMouseOptions` and `normalizeMouseEvent` read the caller's objects) | `EncodeTs(t)` | -| `native/terminal.cc` `TerminalWrap::EncodeMouse`: `Get()` reads of geometry, `x`, `y`, `action`, `button`, `modifiers`, `anyButtonPressed`, `trackLastCell`; then `RequireTerminal`, `RequireMouseEncoder`, `ghostty_terminal_mode_get`, `ghostty_mouse_encoder_*` | `EncodeEnter(t)` (enter, reads), `EncodeCall(t)` (handles and libghostty calls), `EncodeThrows(t)`, constants `JsInNativeRead`, `TakeHandlesLast`, `NativeNullGuard` | +| `native/terminal.cc` `TerminalWrap::EncodeMouse`: `Get()` reads of geometry, `x`, `y`, `action`, `button`, `modifiers`, `anyButtonPressed`, `trackLastCell`; then `RequireTerminal`, `RequireMouseEncoder`, `ghostty_terminal_get(GHOSTTY_TERMINAL_DATA_MODE)`, `ghostty_mouse_encoder_*` | `EncodeEnter(t)` (enter, reads), `EncodeCall(t)` (handles and libghostty calls), `EncodeThrows(t)`, constants `JsInNativeRead`, `TakeHandlesLast`, `NativeNullGuard` | | `src/index.ts` `dispose`; `native/terminal.cc` `TerminalWrap::Dispose`, `DisposeNative` (frees `mouse_encoder_`, then `terminal_`, and sets each to `nullptr`) | `Dispose(t)`, `DisposeNative(r)`, constants `DisposeClearsPtr`, `EncoderClearsPtr` | | `native/terminal.cc` `TerminalWrap::~TerminalWrap` (ObjectWrap finalizer) | `Drop(t)`, `Finalize(t)` | | Node environment teardown when a Worker exits | `WorkerExit(w)` | @@ -108,7 +108,7 @@ Change the model from the code, before you rerun. Do not shape it by what makes - Assumption: when a Worker exits, Node runs the finalizers of its wrapped objects and invalidates the references that its env made. The model does not model the main thread's exit. - Assumption: each env loads the addon once. Node gives each load of the addon its own `napi_env`, even two `process.dlopen` calls in one thread, so `TerminalWrap::Init` asserts that the slot is empty. The model does not explore a second load. - JS can run where code reads a caller's values. The model has these points: the `encodeMouse` normalizers after `#assertUsable` (`EncodeTs`), and the native `Get()` reads in `EncodeMouse` (`EncodeEnter` to `EncodeCall`, while `JsInNativeRead`). A getter there can run any step of the model, for example `Dispose` of the same terminal. `snapshot` has the same window as `EncodeTs`: `normalizeSnapshotOptions` reads the caller's getters after `#assertUsable`, and the native null check covers it. The model keeps `snapshot` in the one-step `Use`. -- Assumption: no JS runs inside the other native methods after they take `terminal_`. `src/index.ts` passes them objects that it builds itself, with every key that they read set as an own property, so no getter runs in `OptionBool` or `options.Get`. The constructor reads `scrollbackLimit` with `Get()` before `ghostty_terminal_new`, so a getter there cannot reach a handle. +- Assumption: no JS runs inside the other native methods after they take `terminal_`. `Snapshot` reads its options with `Get()` before `RequireTerminal`, and it builds its result with `DefineValue` and `DefineIndex`, which run no setter. `Feed` and `Resize` call `RequireTerminal` first, but after that they only test argument types and read strings, bytes, and numbers, which runs no JS. `GetVisibleText`, `FormatPlain`, and `FormatHtml` read no arguments. Until #46 this was false for `snapshot`: it read its options after `RequireTerminal`, and `src/index.ts` sends `{}` when the caller passes no options, so `OptionBool` could run an `Object.prototype` getter after the check. `Set()` also ran `Object.prototype` setters while `BuildSnapshot` used `terminal_`. A getter or setter that called `dispose()` aborted or segfaulted Node (`test/snapshot-safety.test.ts`). The constructor reads `scrollbackLimit` with `Get()` before `ghostty_terminal_new`, so a getter there cannot reach a handle. - Assumption: while a call runs on a terminal, the program cannot drop that terminal, and its Worker cannot exit: the call keeps the object reachable, and a terminating Worker first unwinds its stack (`EncodeThrows`). ## Not covered diff --git a/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla index a83bb19..84407a0 100644 --- a/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla +++ b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla @@ -148,7 +148,8 @@ LoadAddon(e) == (* with env.GetInstanceData; process_static reads the static. Then *) (* FunctionReference::New runs in the env stored in the reference, not in *) (* the caller's env. The TerminalWrap constructor calls *) -(* ghostty_terminal_new, then ghostty_mouse_encoder_new. *) +(* ghostty_terminal_new and ghostty_terminal_set, then *) +(* ghostty_mouse_encoder_new. *) (***************************************************************************) CreateTerminal(e, t) == /\ env[e] = "loaded" @@ -211,8 +212,9 @@ Dispose(t) == (* (TakeHandlesLast = FALSE), it first copied terminal_ and *) (* mouse_encoder_ into locals (RequireTerminal, RequireMouseEncoder). *) (* EncodeCall: the reads end. With TakeHandlesLast, EncodeMouse checks and *) -(* copies the pointers here. Then it calls ghostty_terminal_mode_get and *) -(* the ghostty_mouse_encoder_* functions, and no JS runs until return. *) +(* copies the pointers here. Then it calls ghostty_terminal_get *) +(* (mode) and the ghostty_mouse_encoder_* functions, and no JS runs *) +(* until return. *) (* Without JsInNativeRead, EncodeEnter and EncodeCall are one step. *) (***************************************************************************) EncodeTs(t) == From 584c56142db36c468f27cd172d34495d822799bf Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Fri, 30 Oct 2026 07:54:52 +0000 Subject: [PATCH 2/2] chore: name feed's instanceof window and both CreateFails paths MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The lifecycle record now says that public feed runs a Proxy's getPrototypeOf trap in assertFeedData after #assertUsable, and that the native null check covers it. The CreateFails comment in the model now names the ghostty_terminal_set failure too, as the coverage row does. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `xhigh`_ Change-Id: I78a9534868aadd6f97ed08e3c4ae997c678f51bb Signed-off-by: Thomas Kosiewski --- .agents/skills/verify-native-lifecycle/SKILL.md | 2 +- .../verify-native-lifecycle/model/AddonEnvLifecycle.tla | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.agents/skills/verify-native-lifecycle/SKILL.md b/.agents/skills/verify-native-lifecycle/SKILL.md index 058b96d..49e709f 100644 --- a/.agents/skills/verify-native-lifecycle/SKILL.md +++ b/.agents/skills/verify-native-lifecycle/SKILL.md @@ -107,7 +107,7 @@ Change the model from the code, before you rerun. Do not shape it by what makes - Each action is atomic. Different envs run on different threads. With one class reference for each env, two envs share no addon state, so treating each step as atomic hides no interleaving of addon state. With a shared slot (`mutant-process-static`), the threads also race on it: that adds bad behaviors, and the model already finds the slot bugs without it. - Assumption: when a Worker exits, Node runs the finalizers of its wrapped objects and invalidates the references that its env made. The model does not model the main thread's exit. - Assumption: each env loads the addon once. Node gives each load of the addon its own `napi_env`, even two `process.dlopen` calls in one thread, so `TerminalWrap::Init` asserts that the slot is empty. The model does not explore a second load. -- JS can run where code reads a caller's values. The model has these points: the `encodeMouse` normalizers after `#assertUsable` (`EncodeTs`), and the native `Get()` reads in `EncodeMouse` (`EncodeEnter` to `EncodeCall`, while `JsInNativeRead`). A getter there can run any step of the model, for example `Dispose` of the same terminal. `snapshot` has the same window as `EncodeTs`: `normalizeSnapshotOptions` reads the caller's getters after `#assertUsable`, and the native null check covers it. The model keeps `snapshot` in the one-step `Use`. +- JS can run where code reads a caller's values. The model has these points: the `encodeMouse` normalizers after `#assertUsable` (`EncodeTs`), and the native `Get()` reads in `EncodeMouse` (`EncodeEnter` to `EncodeCall`, while `JsInNativeRead`). A getter there can run any step of the model, for example `Dispose` of the same terminal. `snapshot` has the same window as `EncodeTs`: `normalizeSnapshotOptions` reads the caller's getters after `#assertUsable`, and the native null check covers it. `feed` has it too: `assertFeedData` runs `data instanceof Uint8Array`, which runs a Proxy's `getPrototypeOf` trap after `#assertUsable`, and the native null check covers it. The model keeps `snapshot` and `feed` in the one-step `Use`. - Assumption: no JS runs inside the other native methods after they take `terminal_`. `Snapshot` reads its options with `Get()` before `RequireTerminal`, and it builds its result with `DefineValue` and `DefineIndex`, which run no setter. `Feed` and `Resize` call `RequireTerminal` first, but after that they only test argument types and read strings, bytes, and numbers, which runs no JS. `GetVisibleText`, `FormatPlain`, and `FormatHtml` read no arguments. Until #46 this was false for `snapshot`: it read its options after `RequireTerminal`, and `src/index.ts` sends `{}` when the caller passes no options, so `OptionBool` could run an `Object.prototype` getter after the check. `Set()` also ran `Object.prototype` setters while `BuildSnapshot` used `terminal_`. A getter or setter that called `dispose()` aborted or segfaulted Node (`test/snapshot-safety.test.ts`). The constructor reads `scrollbackLimit` with `Get()` before `ghostty_terminal_new`, so a getter there cannot reach a handle. - Assumption: while a call runs on a terminal, the program cannot drop that terminal, and its Worker cannot exit: the call keeps the object reachable, and a terminating Worker first unwinds its stack (`EncodeThrows`). diff --git a/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla index 84407a0..069082c 100644 --- a/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla +++ b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla @@ -159,9 +159,10 @@ CreateTerminal(e, t) == /\ handleUse' = NoHandleUse /\ UNCHANGED <> -\* ghostty_mouse_encoder_new fails: the constructor frees the terminal, sets -\* terminal_ = nullptr, and throws. ~TerminalWrap does not run, because the -\* C++ constructor did not finish. No JS object exists. +\* ghostty_terminal_set or ghostty_mouse_encoder_new fails: the constructor +\* frees the terminal once, leaves terminal_ = nullptr, and throws. +\* ~TerminalWrap does not run, because the C++ constructor did not finish. +\* No JS object exists. CreateFails(e, t) == /\ env[e] = "loaded" /\ term[t].js = "none"