diff --git a/.agents/skills/verify-native-lifecycle/SKILL.md b/.agents/skills/verify-native-lifecycle/SKILL.md index e060e82..49e709f 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)` | @@ -107,8 +107,8 @@ 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`. -- 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. +- 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`). ## Not covered diff --git a/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla index a83bb19..069082c 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" @@ -158,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" @@ -211,8 +213,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) ==