From c77d7463c81889514b8e2b5a650cf79c89e7e227 Mon Sep 17 00:00:00 2001
From: Thomas Kosiewski <tk@coder.com>
Date: Thu, 29 Oct 2026 20:40:25 +0000
Subject: [PATCH 1/2] chore: cover the mouse encoder in the lifecycle model
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

PR #12 adds a second libghostty handle (mouse_encoder_) and encodeMouse,
which reads caller values in two places where JS can run: the TypeScript
normalizers after #assertUsable, and the native Get() reads. The old model
had neither, and its assumption "no JS runs inside a native method" is false
for encodeMouse.

Model the encoder handle (create, the constructor's failure path, dispose,
finalize), split encodeMouse at the JS windows, and add EncoderFreedOnce.
Three new mutants: the code before the F2 fix (handles taken before the
reads), no native null checks, and DisposeNative keeping mouse_encoder_.
Record F2, move the sync commit to the PR #12 head, and update the view.

Signed-off-by: Thomas Kosiewski <tk@coder.com>

---
_Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `xhigh`_

Change-Id: I2581fa76d309060eedd375edc79d0f9a2a3575a3
---
 .../skills/verify-native-lifecycle/SKILL.md   |  37 ++--
 .../model/AddonEnvLifecycle.tla               | 160 ++++++++++++++++--
 .../verify-native-lifecycle/model/chart.cfg   |   4 +
 .../verify-native-lifecycle/model/current.cfg |   4 +
 .../model/mutant-dispose-keeps-pointer.cfg    |   4 +
 .../model/mutant-handles-before-reads.cfg     |  21 +++
 .../model/mutant-keeps-encoder-pointer.cfg    |  21 +++
 .../model/mutant-no-native-guard.cfg          |  21 +++
 .../model/mutant-no-use-guards.cfg            |   7 +-
 .../model/mutant-process-static.cfg           |   4 +
 .../model/statechart-view.mjs                 |  17 +-
 .agents/skills/verify-native-lifecycle/run.sh |   8 +-
 12 files changed, 275 insertions(+), 33 deletions(-)
 create mode 100644 .agents/skills/verify-native-lifecycle/model/mutant-handles-before-reads.cfg
 create mode 100644 .agents/skills/verify-native-lifecycle/model/mutant-keeps-encoder-pointer.cfg
 create mode 100644 .agents/skills/verify-native-lifecycle/model/mutant-no-native-guard.cfg

diff --git a/.agents/skills/verify-native-lifecycle/SKILL.md b/.agents/skills/verify-native-lifecycle/SKILL.md
index 33f47ac..494632c 100644
--- a/.agents/skills/verify-native-lifecycle/SKILL.md
+++ b/.agents/skills/verify-native-lifecycle/SKILL.md
@@ -5,7 +5,7 @@ description: "Model-check, with TLA+, how the libghostty-vt-node native addon ke
 
 # Verify the native addon lifecycle
 
-This skill checks a TLA+ model of the addon's native state against four rules. A model checker (TLC) tries every order of steps in the model, within the bounds below. Tests only try the orders that someone wrote.
+This skill checks a TLA+ model of the addon's native state against five rules. A model checker (TLC) tries every order of steps in the model, within the bounds below. Tests only try the orders that someone wrote.
 
 ## The rules
 
@@ -14,34 +14,42 @@ This skill checks a TLA+ model of the addon's native state against four rules. A
 | `CreateUsesOwnClass` | `createTerminal` in a thread uses the class reference that this thread made. | The process aborts or segfaults when it creates a terminal. |
 | `LoadDeletesOnlyOwnRef` | Loading the addon in a thread never deletes another thread's reference. | One thread frees V8 state that belongs to another thread (a data race). |
 | `HandleFreedOnce` | libghostty frees each terminal handle at most once. | A double free corrupts the heap. |
-| `NoCallOnDeadHandle` | No libghostty call reaches a freed or null terminal handle. | Use after free: a crash or wrong terminal output. |
+| `EncoderFreedOnce` | libghostty frees each mouse encoder handle at most once. | A double free corrupts the heap. |
+| `NoCallOnDeadHandle` | No libghostty call reaches a freed or null terminal or mouse encoder handle. | Use after free: a crash, wrong terminal output, or mouse bytes from another terminal. |
 
 ## History: finding F1, fixed
 
 This check found F1 in the code before `4aa7039`. The addon kept its class in one `static Napi::FunctionReference constructor` for the whole process, and each environment's `TerminalWrap::Init` overwrote it. After the main thread and a Worker both loaded the addon, the main thread's `createTerminal` used the worker's reference: V8 aborted with `Cannot create a handle without a HandleScope`, or the process segfaulted after the worker exited. The fix keeps one reference for each environment in its instance data. `model/mutant-process-static.cfg` is the old code, and `run.sh` checks at each run that it still breaks `CreateUsesOwnClass` and `LoadDeletesOnlyOwnRef`.
 
+## History: finding F2, fixed
+
+This check found F2 in `encodeMouse` before `a414395`. `TerminalWrap::EncodeMouse` copied `terminal_` and `mouse_encoder_` into locals, and then read its arguments with `Get()`. `Get()` runs getters, including a getter on `Object.prototype` for a key that `src/index.ts` leaves out of the object it passes (`button`, `modifiers`). A getter that called `dispose()` made the libghostty calls use freed handles. Through the package API, the call then encoded with another terminal's encoder state. Through the raw native object, the process crashed. The fix reads every argument first, then takes the handles, and runs no JS until the call returns. `model/mutant-handles-before-reads.cfg` is the old code, and `run.sh` checks at each run that it still breaks `NoCallOnDeadHandle`. `test/mouse-safety.test.ts` replays the getter cases in child processes.
+
 ## Does my change touch the verified code?
 
 Run this skill when the diff since the sync commit changes any covered code:
 
 ```sh
-git diff --stat 0d255369dd8233e3ed1bce0575ab98b2bbd98d07 -- native/ test/workers.test.ts src/index.ts src/loader.ts package.json package-lock.json
+git diff --stat d6c5659826a3883da7a1e49ba67986cf8e13b089 -- 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_`. Static or global JS-facing state is the F1 bug class: keep it in the environment's instance data.
+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: `0d255369dd8233e3ed1bce0575ab98b2bbd98d07`. 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: `d6c5659826a3883da7a1e49ba67986cf8e13b089`. 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`) | `CreateTerminal(e, t)` |
+| `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` `dispose`; `native/terminal.cc` `TerminalWrap::Dispose`, `DisposeNative` | `Dispose(t)`, `DisposeNative(r)`, constant `DisposeClearsPtr` |
+| `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` |
+| `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)` |
 | node-addon-api 8.9.2 `FunctionReference::New` (uses the env stored in the reference) and `Reference::~Reference` / `operator=` (run `napi_delete_reference` with the stored env) | `CreateTerminal` sets `refUse` with the slot's owner; `LoadAddon` sets `refUse` with the old owner |
@@ -62,9 +70,12 @@ It takes about 20 seconds. It runs TLC once for each config and rule, and prints
 | `model/current.cfg` | The current code. Main thread, 2 workers, 2 terminals. | none |
 | `model/mutant-process-static.cfg` | The old code: one class reference for the whole process (F1). | `CreateUsesOwnClass`, `LoadDeletesOnlyOwnRef` |
 | `model/mutant-dispose-keeps-pointer.cfg` | Current code, but `DisposeNative` does not set `terminal_ = nullptr`. | `HandleFreedOnce` |
-| `model/mutant-no-use-guards.cfg` | Current code, but no `#assertUsable` and no `RequireTerminal` null check. | `NoCallOnDeadHandle` |
+| `model/mutant-no-use-guards.cfg` | Current code, but no `#assertUsable` and no native null checks. | `NoCallOnDeadHandle` |
+| `model/mutant-no-native-guard.cfg` | Current code, but no `RequireTerminal` or `RequireMouseEncoder` null check. `#assertUsable` stays. | `NoCallOnDeadHandle` |
+| `model/mutant-keeps-encoder-pointer.cfg` | Current code, but `DisposeNative` does not set `mouse_encoder_ = nullptr`. | `EncoderFreedOnce` |
+| `model/mutant-handles-before-reads.cfg` | The old code: `EncodeMouse` copies the handles, then reads its arguments (F2). | `NoCallOnDeadHandle` |
 
-The mutant configs prove at each run that each rule can fail. Removing only one of the two use guards breaks nothing, because the other guard still stops the call.
+The mutant configs prove at each run that each rule can fail. Removing only `#assertUsable` breaks nothing, because the native null checks still stop the call. Removing only the native null checks breaks `NoCallOnDeadHandle`: a getter that the `encodeMouse` normalizers or the native `Get()` reads run can dispose the terminal after `#assertUsable` passed.
 
 `test/workers.test.ts` replays the worker counterexamples against the real addon, in child processes: a live worker, a worker that exited, and two workers. `npm test` runs it. It crashed in all three scenarios before the F1 fix.
 
@@ -92,15 +103,17 @@ Change the model from the code, before you rerun. Do not shape it by what makes
 
 ## Bounds and assumptions
 
-- Bounds: the main thread and 2 workers, 2 terminals. `current.cfg` has 2,121 distinct states.
+- Bounds: the main thread and 2 workers, 2 terminals. `current.cfg` has 8,661 distinct states.
 - 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.
-- Assumption: JS code cannot run inside a native method. This holds because `src/index.ts` passes plain option objects that it builds itself, so no getter runs in `OptionBool` or `options.Get`. A caller that reaches the native object directly is outside the model.
+- 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: 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
 
 - libghostty itself: VT parsing and every `ghostty_*` call are trusted.
 - The content of snapshots and visible text (`ReadLine`, `ReadCellText`, `BuildCellObject`, `ResolveStyleColor`).
-- Argument validation, `getNativeInfo`, prebuild loading, and packaging.
+- Argument validation (the mouse geometry and coordinate checks included), the encoded mouse bytes, the mouse mode cache (`mouse_modes_dirty_`), `getNativeInfo`, prebuild loading, and packaging.
 - More than one load of the addon in one env, for example two copies of the package at different paths.
diff --git a/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla
index cca5227..a83bb19 100644
--- a/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla
+++ b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla
@@ -26,11 +26,22 @@ CONSTANTS
                       \* ghostty_terminal_free (native/terminal.cc). Code: TRUE.
     TsDisposedGuard,  \* Terminal.#assertUsable throws after dispose
                       \* (src/index.ts). Code: TRUE.
-    NativeNullGuard   \* TerminalWrap::RequireTerminal throws when terminal_ is
-                      \* nullptr (native/terminal.cc). Code: TRUE.
+    NativeNullGuard,  \* TerminalWrap::RequireTerminal throws when terminal_ is
+                      \* nullptr, and RequireMouseEncoder when mouse_encoder_
+                      \* is nullptr (native/terminal.cc). Code: TRUE.
+    EncoderClearsPtr, \* DisposeNative sets `mouse_encoder_ = nullptr` after
+                      \* ghostty_mouse_encoder_free. Code: TRUE.
+    JsInNativeRead,   \* JS can run while TerminalWrap::EncodeMouse reads its
+                      \* arguments with Get(): a getter on Object.prototype for a
+                      \* key that src/index.ts omits (`button`, `modifiers`), or a
+                      \* caller that holds the raw native object. Code: TRUE.
+    TakeHandlesLast   \* EncodeMouse reads every argument before it copies
+                      \* terminal_ and mouse_encoder_ into locals. Code: TRUE.
+                      \* FALSE is the code before the F2 fix.
 
 ASSUME CtorStorage \in {"process_static", "per_env"}
-ASSUME {DisposeClearsPtr, TsDisposedGuard, NativeNullGuard} \subseteq BOOLEAN
+ASSUME {DisposeClearsPtr, TsDisposedGuard, NativeNullGuard,
+        EncoderClearsPtr, JsInNativeRead, TakeHandlesLast} \subseteq BOOLEAN
 ASSUME Main \notin Workers
 
 Envs == {Main} \cup Workers
@@ -55,29 +66,54 @@ NoHandleUse == [op |-> "none", t |-> None, state |-> "none"]
 \* ptr:    TerminalWrap::terminal_ != nullptr
 \* handle: the GhosttyTerminal: "none", "live", or "freed"
 \* frees:  how many times ghostty_terminal_free ran on this handle
-Unborn == [in |-> None, js |-> "none", ptr |-> FALSE, handle |-> "none", frees |-> 0]
+\* encPtr, enc, encFrees: the same three for mouse_encoder_ (GhosttyMouseEncoder)
+\* call:   where an encodeMouse call on this terminal is: "idle"; "ts" (in
+\*         Terminal.encodeMouse after #assertUsable, while the normalizers read
+\*         the caller's objects, so caller getters can run); "native" (in
+\*         TerminalWrap::EncodeMouse, reading arguments with Get())
+\* took:   what the native locals `terminal` and `encoder` hold: "none" (not
+\*         copied yet), "ptr" (copies of terminal_ and mouse_encoder_), "null"
+Unborn == [in |-> None, js |-> "none", ptr |-> FALSE, handle |-> "none", frees |-> 0,
+           encPtr |-> FALSE, enc |-> "none", encFrees |-> 0, call |-> "idle", took |-> "none"]
+Born(e) == [in |-> e, js |-> "live", ptr |-> TRUE, handle |-> "live", frees |-> 0,
+            encPtr |-> TRUE, enc |-> "live", encFrees |-> 0, call |-> "idle", took |-> "none"]
 
 SlotOf(e) == IF CtorStorage = "process_static" THEN slot ELSE slot[e]
 SetSlot(e, owner) ==
     IF CtorStorage = "process_static" THEN owner ELSE [slot EXCEPT ![e] = owner]
 
 \* TerminalWrap::DisposeNative (native/terminal.cc):
-\*   if (terminal_ == nullptr) return;
-\*   ghostty_terminal_free(terminal_);
-\*   terminal_ = nullptr;
+\*   if (mouse_encoder_ != nullptr) { ghostty_mouse_encoder_free(..); mouse_encoder_ = nullptr; }
+\*   if (terminal_ != nullptr) { ghostty_terminal_free(terminal_); terminal_ = nullptr; }
 DisposeNative(r) ==
-    IF r.ptr
-    THEN [r EXCEPT !.handle = "freed", !.frees = r.frees + 1, !.ptr = ~DisposeClearsPtr]
-    ELSE r
+    LET r1 == IF r.encPtr
+              THEN [r EXCEPT !.enc = "freed", !.encFrees = r.encFrees + 1,
+                             !.encPtr = ~EncoderClearsPtr]
+              ELSE r
+    IN IF r1.ptr
+       THEN [r1 EXCEPT !.handle = "freed", !.frees = r1.frees + 1, !.ptr = ~DisposeClearsPtr]
+       ELSE r1
+
+\* The state of the handles that the libghostty calls in EncodeMouse reach.
+CallState(r, took) ==
+    IF took = "ptr"
+    THEN IF r.handle = "live" /\ r.enc = "live" THEN "live" ELSE "freed"
+    ELSE "null"
+Usable(r) == r.ptr /\ r.encPtr
 
 TypeOK ==
     /\ env \in [Envs -> {"idle", "loaded", "exited"}]
     /\ \A t \in Terminals :
          /\ term[t].in \in Envs \cup {None}
-         /\ term[t].js \in {"none", "live", "disposed", "dropped", "finalized"}
+         /\ term[t].js \in {"none", "failed", "live", "disposed", "dropped", "finalized"}
          /\ term[t].ptr \in BOOLEAN
          /\ term[t].handle \in {"none", "live", "freed"}
          /\ term[t].frees \in 0..2
+         /\ term[t].encPtr \in BOOLEAN
+         /\ term[t].enc \in {"none", "live", "freed"}
+         /\ term[t].encFrees \in 0..2
+         /\ term[t].call \in {"idle", "ts", "native"}
+         /\ term[t].took \in {"none", "ptr", "null"}
 
 Init ==
     /\ env = [e \in Envs |-> "idle"]
@@ -112,14 +148,25 @@ 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.                                                   *)
+(* ghostty_terminal_new, then ghostty_mouse_encoder_new.                  *)
 (***************************************************************************)
 CreateTerminal(e, t) ==
     /\ env[e] = "loaded"
     /\ term[t].js = "none"
     /\ refUse' = [op |-> "createTerminal uses class reference", by |-> e, owner |-> SlotOf(e)]
-    /\ term' = [term EXCEPT ![t] =
-                  [in |-> e, js |-> "live", ptr |-> TRUE, handle |-> "live", frees |-> 0]]
+    /\ term' = [term EXCEPT ![t] = Born(e)]
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED <<env, slot>>
+
+\* 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.
+CreateFails(e, t) ==
+    /\ env[e] = "loaded"
+    /\ term[t].js = "none"
+    /\ refUse' = [op |-> "createTerminal uses class reference", by |-> e, owner |-> SlotOf(e)]
+    /\ term' = [term EXCEPT ![t] = [Unborn EXCEPT !.in = e, !.js = "failed",
+                                                   !.handle = "freed", !.frees = 1]]
     /\ handleUse' = NoHandleUse
     /\ UNCHANGED <<env, slot>>
 
@@ -154,8 +201,79 @@ Dispose(t) ==
     /\ handleUse' = NoHandleUse
     /\ UNCHANGED <<env, slot>>
 
-\* The program drops its last reference to the Terminal object.
+(***************************************************************************)
+(* encodeMouse is three steps, because caller JS can run between them.    *)
+(* EncodeTs: Terminal.encodeMouse runs #assertUsable, then the normalizers *)
+(*   read the caller's event and options. A getter there can run any JS,   *)
+(*   for example dispose() on this terminal.                               *)
+(* EncodeEnter: this.#native.encodeMouse enters TerminalWrap::EncodeMouse, *)
+(*   which reads its arguments with Get(). Before the F2 fix              *)
+(*   (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.   *)
+(* Without JsInNativeRead, EncodeEnter and EncodeCall are one step.        *)
+(***************************************************************************)
+EncodeTs(t) ==
+    LET r == term[t] IN
+    /\ r.js \in {"live", "disposed"}
+    /\ env[r.in] = "loaded"
+    /\ r.call = "idle"
+    /\ term' = IF TsDisposedGuard /\ r.js = "disposed"
+               THEN term                                 \* throws "disposed"
+               ELSE [term EXCEPT ![t].call = "ts"]
+    /\ refUse' = NoRefUse
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED <<env, slot>>
+
+\* What the native locals hold after RequireTerminal and RequireMouseEncoder,
+\* or "stop" when a null guard throws.
+Take(r) ==
+    IF Usable(r) THEN "ptr"
+    ELSE IF NativeNullGuard THEN "stop" ELSE "null"
+
+CallNow(t, took) ==
+    /\ handleUse' = IF took = "stop" THEN NoHandleUse
+                    ELSE [op |-> "libghostty call", t |-> t, state |-> CallState(term[t], took)]
+    /\ term' = [term EXCEPT ![t].call = "idle", ![t].took = "none"]
+
+EncodeEnter(t) ==
+    LET r == term[t] IN
+    /\ r.call = "ts"
+    /\ env[r.in] = "loaded"
+    /\ IF ~JsInNativeRead
+       THEN CallNow(t, Take(r))
+       ELSE /\ handleUse' = NoHandleUse
+            /\ term' = IF TakeHandlesLast
+                       THEN [term EXCEPT ![t].call = "native"]
+                       ELSE IF Take(r) = "stop"
+                            THEN [term EXCEPT ![t].call = "idle"]
+                            ELSE [term EXCEPT ![t].call = "native", ![t].took = Take(r)]
+    /\ refUse' = NoRefUse
+    /\ UNCHANGED <<env, slot>>
+
+EncodeCall(t) ==
+    LET r == term[t] IN
+    /\ JsInNativeRead
+    /\ r.call = "native"
+    /\ env[r.in] = "loaded"
+    /\ CallNow(t, IF TakeHandlesLast THEN Take(r) ELSE r.took)
+    /\ refUse' = NoRefUse
+    /\ UNCHANGED <<env, slot>>
+
+\* A getter throws in either read phase: the call ends without a libghostty call.
+EncodeThrows(t) ==
+    /\ term[t].call \in {"ts", "native"}
+    /\ term' = [term EXCEPT ![t].call = "idle", ![t].took = "none"]
+    /\ refUse' = NoRefUse
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED <<env, slot>>
+
+\* The program drops its last reference to the Terminal object. An object
+\* whose method is still running is reachable, so it cannot be dropped then.
 Drop(t) ==
+    /\ term[t].call = "idle"
     /\ term[t].js \in {"live", "disposed"}
     /\ env[term[t].in] = "loaded"
     /\ term' = [term EXCEPT ![t].js = "dropped"]
@@ -181,6 +299,8 @@ Finalize(t) ==
 (***************************************************************************)
 WorkerExit(w) ==
     /\ env[w] = "loaded"
+    \* A terminating Worker first unwinds its JS stack (EncodeThrows).
+    /\ \A t \in Terminals : term[t].in = w => term[t].call = "idle"
     /\ env' = [env EXCEPT ![w] = "exited"]
     /\ term' = [t \in Terminals |->
                   IF term[t].in = w /\ term[t].js \in {"live", "disposed", "dropped"}
@@ -193,6 +313,11 @@ WorkerExit(w) ==
 Next ==
     \/ \E e \in Envs : LoadAddon(e)
     \/ \E e \in Envs, t \in Terminals : CreateTerminal(e, t)
+    \/ \E e \in Envs, t \in Terminals : CreateFails(e, t)
+    \/ \E t \in Terminals : EncodeTs(t)
+    \/ \E t \in Terminals : EncodeEnter(t)
+    \/ \E t \in Terminals : EncodeCall(t)
+    \/ \E t \in Terminals : EncodeThrows(t)
     \/ \E t \in Terminals : Use(t)
     \/ \E t \in Terminals : Dispose(t)
     \/ \E t \in Terminals : Drop(t)
@@ -216,7 +341,10 @@ LoadDeletesOnlyOwnRef ==
 \* libghostty frees each terminal handle at most once.
 HandleFreedOnce == \A t \in Terminals : term[t].frees <= 1
 
-\* No libghostty call reaches a freed or null terminal handle.
+\* libghostty frees each mouse encoder at most once.
+EncoderFreedOnce == \A t \in Terminals : term[t].encFrees <= 1
+
+\* No libghostty call reaches a freed or null terminal or mouse encoder handle.
 NoCallOnDeadHandle ==
     handleUse.op = "libghostty call" => handleUse.state = "live"
 
diff --git a/.agents/skills/verify-native-lifecycle/model/chart.cfg b/.agents/skills/verify-native-lifecycle/model/chart.cfg
index ccd9b7b..78982de 100644
--- a/.agents/skills/verify-native-lifecycle/model/chart.cfg
+++ b/.agents/skills/verify-native-lifecycle/model/chart.cfg
@@ -7,6 +7,9 @@ CONSTANTS
     DisposeClearsPtr = TRUE
     TsDisposedGuard = TRUE
     NativeNullGuard = TRUE
+    EncoderClearsPtr = TRUE
+    JsInNativeRead = TRUE
+    TakeHandlesLast = TRUE
 SPECIFICATION Spec
 CHECK_DEADLOCK FALSE
 INVARIANTS
@@ -14,4 +17,5 @@ INVARIANTS
     CreateUsesOwnClass
     LoadDeletesOnlyOwnRef
     HandleFreedOnce
+    EncoderFreedOnce
     NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/current.cfg b/.agents/skills/verify-native-lifecycle/model/current.cfg
index a00c6e8..31bc3cf 100644
--- a/.agents/skills/verify-native-lifecycle/model/current.cfg
+++ b/.agents/skills/verify-native-lifecycle/model/current.cfg
@@ -7,6 +7,9 @@ CONSTANTS
     DisposeClearsPtr = TRUE
     TsDisposedGuard = TRUE
     NativeNullGuard = TRUE
+    EncoderClearsPtr = TRUE
+    JsInNativeRead = TRUE
+    TakeHandlesLast = TRUE
 SPECIFICATION Spec
 CHECK_DEADLOCK FALSE
 INVARIANTS
@@ -14,4 +17,5 @@ INVARIANTS
     CreateUsesOwnClass
     LoadDeletesOnlyOwnRef
     HandleFreedOnce
+    EncoderFreedOnce
     NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-dispose-keeps-pointer.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-dispose-keeps-pointer.cfg
index 4f10f6b..701df9b 100644
--- a/.agents/skills/verify-native-lifecycle/model/mutant-dispose-keeps-pointer.cfg
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-dispose-keeps-pointer.cfg
@@ -7,6 +7,9 @@ CONSTANTS
     DisposeClearsPtr = FALSE
     TsDisposedGuard = TRUE
     NativeNullGuard = TRUE
+    EncoderClearsPtr = TRUE
+    JsInNativeRead = TRUE
+    TakeHandlesLast = TRUE
 SPECIFICATION Spec
 CHECK_DEADLOCK FALSE
 INVARIANTS
@@ -14,4 +17,5 @@ INVARIANTS
     CreateUsesOwnClass
     LoadDeletesOnlyOwnRef
     HandleFreedOnce
+    EncoderFreedOnce
     NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-handles-before-reads.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-handles-before-reads.cfg
new file mode 100644
index 0000000..7bf8418
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-handles-before-reads.cfg
@@ -0,0 +1,21 @@
+\* The code before the F2 fix: EncodeMouse copies terminal_ and mouse_encoder_, then reads its arguments.
+CONSTANTS
+    Main = main
+    Workers = {w1, w2}
+    Terminals = {t1, t2}
+    CtorStorage = "per_env"
+    DisposeClearsPtr = TRUE
+    TsDisposedGuard = TRUE
+    NativeNullGuard = TRUE
+    EncoderClearsPtr = TRUE
+    JsInNativeRead = TRUE
+    TakeHandlesLast = FALSE
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    CreateUsesOwnClass
+    LoadDeletesOnlyOwnRef
+    HandleFreedOnce
+    EncoderFreedOnce
+    NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-keeps-encoder-pointer.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-keeps-encoder-pointer.cfg
new file mode 100644
index 0000000..59a9f24
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-keeps-encoder-pointer.cfg
@@ -0,0 +1,21 @@
+\* Current code with one break: DisposeNative does not set mouse_encoder_ = nullptr.
+CONSTANTS
+    Main = main
+    Workers = {w1, w2}
+    Terminals = {t1, t2}
+    CtorStorage = "per_env"
+    DisposeClearsPtr = TRUE
+    TsDisposedGuard = TRUE
+    NativeNullGuard = TRUE
+    EncoderClearsPtr = FALSE
+    JsInNativeRead = TRUE
+    TakeHandlesLast = TRUE
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    CreateUsesOwnClass
+    LoadDeletesOnlyOwnRef
+    HandleFreedOnce
+    EncoderFreedOnce
+    NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-no-native-guard.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-no-native-guard.cfg
new file mode 100644
index 0000000..e8b0851
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-no-native-guard.cfg
@@ -0,0 +1,21 @@
+\* Current code with one break: no RequireTerminal or RequireMouseEncoder null check (#assertUsable stays).
+CONSTANTS
+    Main = main
+    Workers = {w1, w2}
+    Terminals = {t1, t2}
+    CtorStorage = "per_env"
+    DisposeClearsPtr = TRUE
+    TsDisposedGuard = TRUE
+    NativeNullGuard = FALSE
+    EncoderClearsPtr = TRUE
+    JsInNativeRead = TRUE
+    TakeHandlesLast = TRUE
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    CreateUsesOwnClass
+    LoadDeletesOnlyOwnRef
+    HandleFreedOnce
+    EncoderFreedOnce
+    NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-no-use-guards.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-no-use-guards.cfg
index 6249def..8682aec 100644
--- a/.agents/skills/verify-native-lifecycle/model/mutant-no-use-guards.cfg
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-no-use-guards.cfg
@@ -1,4 +1,5 @@
-\* Current code with one break: no #assertUsable and no RequireTerminal null check.
+\* Current code with one break: no #assertUsable and no RequireTerminal or
+\* RequireMouseEncoder null check.
 CONSTANTS
     Main = main
     Workers = {w1, w2}
@@ -7,6 +8,9 @@ CONSTANTS
     DisposeClearsPtr = TRUE
     TsDisposedGuard = FALSE
     NativeNullGuard = FALSE
+    EncoderClearsPtr = TRUE
+    JsInNativeRead = TRUE
+    TakeHandlesLast = TRUE
 SPECIFICATION Spec
 CHECK_DEADLOCK FALSE
 INVARIANTS
@@ -14,4 +18,5 @@ INVARIANTS
     CreateUsesOwnClass
     LoadDeletesOnlyOwnRef
     HandleFreedOnce
+    EncoderFreedOnce
     NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-process-static.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-process-static.cfg
index 31fd31c..d9e57a5 100644
--- a/.agents/skills/verify-native-lifecycle/model/mutant-process-static.cfg
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-process-static.cfg
@@ -7,6 +7,9 @@ CONSTANTS
     DisposeClearsPtr = TRUE
     TsDisposedGuard = TRUE
     NativeNullGuard = TRUE
+    EncoderClearsPtr = TRUE
+    JsInNativeRead = TRUE
+    TakeHandlesLast = TRUE
 SPECIFICATION Spec
 CHECK_DEADLOCK FALSE
 INVARIANTS
@@ -14,4 +17,5 @@ INVARIANTS
     CreateUsesOwnClass
     LoadDeletesOnlyOwnRef
     HandleFreedOnce
+    EncoderFreedOnce
     NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/statechart-view.mjs b/.agents/skills/verify-native-lifecycle/model/statechart-view.mjs
index 22276e2..89551d6 100644
--- a/.agents/skills/verify-native-lifecycle/model/statechart-view.mjs
+++ b/.agents/skills/verify-native-lifecycle/model/statechart-view.mjs
@@ -7,12 +7,15 @@ const slots = (s) => (typeof s === "string" ? { "Class reference": owner(s) } :
   "Main's class reference": owner(s.main),
   "Worker's class reference": owner(s.w1),
 });
+const handleState = (state, frees) => (frees > 1 ? "freed twice" : state === "freed" ? "freed" : "open");
 const terminal = (t) => {
   if (t.js === "none") return "none";
   const where = t.in === "main" ? "main" : "worker";
-  const handle = t.frees > 1 ? "freed twice" : t.handle === "freed" ? "freed" : "open";
+  if (t.js === "failed") return `${where}: createTerminal threw, handle ${handleState(t.handle, t.frees)}`;
   const js = { live: "in use", disposed: "disposed", dropped: "unreachable", finalized: "collected" }[t.js];
-  return `${where}: ${js}, handle ${handle}`;
+  const call = { idle: "", ts: ", encodeMouse checking arguments", native: ", encodeMouse reading arguments" }[t.call];
+  return `${where}: ${js}, handle ${handleState(t.handle, t.frees)}, ` +
+    `mouse encoder ${handleState(t.enc, t.encFrees)}${call}`;
 };
 
 export const title = "libghostty-vt-node: the main thread and a worker, each with its own class reference";
@@ -36,6 +39,16 @@ export const step = (action, from, to) => {
       return `${who(from, to)} imports the package`;
     case "CreateTerminal":
       return `${creator(to)} calls createTerminal`;
+    case "CreateFails":
+      return `${creator(to)} calls createTerminal, and the mouse encoder allocation fails`;
+    case "EncodeTs":
+      return to.term.t1.call === "ts" ? "the program calls encodeMouse" : null;
+    case "EncodeEnter":
+      return to.handleUse.op === "none" ? "encodeMouse enters the addon" : "encodeMouse writes mouse bytes";
+    case "EncodeCall":
+      return to.handleUse.op === "none" ? null : "encodeMouse writes mouse bytes";
+    case "EncodeThrows":
+      return "a getter in the encodeMouse arguments throws";
     case "Use":
       return to.handleUse.op === "none" ? null : "the program feeds or reads the terminal";
     case "Dispose":
diff --git a/.agents/skills/verify-native-lifecycle/run.sh b/.agents/skills/verify-native-lifecycle/run.sh
index 98de60c..f2ac5af 100755
--- a/.agents/skills/verify-native-lifecycle/run.sh
+++ b/.agents/skills/verify-native-lifecycle/run.sh
@@ -17,7 +17,7 @@ TLA_VERSION=1.7.4
 TLA_SHA256=936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88
 JAVA="${JAVA:-java}"
 
-RULES=(CreateUsesOwnClass LoadDeletesOnlyOwnRef HandleFreedOnce NoCallOnDeadHandle)
+RULES=(CreateUsesOwnClass LoadDeletesOnlyOwnRef HandleFreedOnce EncoderFreedOnce NoCallOnDeadHandle)
 
 # EXPECT: the rules that each config must break. Every other rule must hold.
 # Each mutant is the current code with one break, and must break its rule.
@@ -28,10 +28,14 @@ expect_breaks() {
     mutant-process-static) echo "CreateUsesOwnClass LoadDeletesOnlyOwnRef" ;;
     mutant-dispose-keeps-pointer) echo "HandleFreedOnce" ;;
     mutant-no-use-guards) echo "NoCallOnDeadHandle" ;;
+    mutant-no-native-guard) echo "NoCallOnDeadHandle" ;;
+    mutant-keeps-encoder-pointer) echo "EncoderFreedOnce" ;;
+    mutant-handles-before-reads) echo "NoCallOnDeadHandle" ;;
     *) echo "error: no EXPECT entry for config $1" >&2; exit 2 ;;
   esac
 }
-CONFIGS=(current mutant-process-static mutant-dispose-keeps-pointer mutant-no-use-guards)
+CONFIGS=(current mutant-process-static mutant-dispose-keeps-pointer mutant-no-use-guards
+         mutant-no-native-guard mutant-keeps-encoder-pointer mutant-handles-before-reads)
 for cfg in "${CONFIGS[@]}"; do expect_breaks "$cfg" >/dev/null; done
 
 command -v "$JAVA" >/dev/null || { echo "error: java not found; set JAVA or install Java 11+" >&2; exit 2; }

From cd59d692467adef078b17dd969c0b51ab68f4ba2 Mon Sep 17 00:00:00 2001
From: Thomas Kosiewski <tk@coder.com>
Date: Thu, 29 Oct 2026 22:39:24 +0000
Subject: [PATCH 2/2] chore: move the lifecycle sync commit to the #12 squash
 commit
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

7366b75, the covered code changed only in PositiveUint16 and
NonNegativeSize (argument checks from #30, which the model does not
describe) and in how test/mouse-safety.test.ts loads src/. run.sh still
matches EXPECT in all 35 rows.

Signed-off-by: Thomas Kosiewski <tk@coder.com>

---
_Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `xhigh`_

Change-Id: Id8a32feb7af0e8da355aa2ebeaaaa327fd7924be
---
 .agents/skills/verify-native-lifecycle/SKILL.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.agents/skills/verify-native-lifecycle/SKILL.md b/.agents/skills/verify-native-lifecycle/SKILL.md
index 494632c..e060e82 100644
--- a/.agents/skills/verify-native-lifecycle/SKILL.md
+++ b/.agents/skills/verify-native-lifecycle/SKILL.md
@@ -23,21 +23,21 @@ This check found F1 in the code before `4aa7039`. The addon kept its class in on
 
 ## History: finding F2, fixed
 
-This check found F2 in `encodeMouse` before `a414395`. `TerminalWrap::EncodeMouse` copied `terminal_` and `mouse_encoder_` into locals, and then read its arguments with `Get()`. `Get()` runs getters, including a getter on `Object.prototype` for a key that `src/index.ts` leaves out of the object it passes (`button`, `modifiers`). A getter that called `dispose()` made the libghostty calls use freed handles. Through the package API, the call then encoded with another terminal's encoder state. Through the raw native object, the process crashed. The fix reads every argument first, then takes the handles, and runs no JS until the call returns. `model/mutant-handles-before-reads.cfg` is the old code, and `run.sh` checks at each run that it still breaks `NoCallOnDeadHandle`. `test/mouse-safety.test.ts` replays the getter cases in child processes.
+This check found F2 in `encodeMouse` while #12 was in review, so the bug never reached main. #12 landed with the fix as `7366b75`. `TerminalWrap::EncodeMouse` copied `terminal_` and `mouse_encoder_` into locals, and then read its arguments with `Get()`. `Get()` runs getters, including a getter on `Object.prototype` for a key that `src/index.ts` leaves out of the object it passes (`button`, `modifiers`). A getter that called `dispose()` made the libghostty calls use freed handles. Through the package API, the call then encoded with another terminal's encoder state. Through the raw native object, the process crashed. The fix reads every argument first, then takes the handles, and runs no JS until the call returns. `model/mutant-handles-before-reads.cfg` is the old code, and `run.sh` checks at each run that it still breaks `NoCallOnDeadHandle`. `test/mouse-safety.test.ts` replays the getter cases in child processes.
 
 ## Does my change touch the verified code?
 
 Run this skill when the diff since the sync commit changes any covered code:
 
 ```sh
-git diff --stat d6c5659826a3883da7a1e49ba67986cf8e13b089 -- native/ test/workers.test.ts test/mouse-safety.test.ts src/index.ts src/loader.ts package.json package-lock.json
+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
 ```
 
 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: `d6c5659826a3883da7a1e49ba67986cf8e13b089`. 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: `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.
 
 | Code | Model |
 |---|---|