[ThomasK33]

Why

The verify-native-lifecycle skill keeps a sync commit. At that commit, its TLA+ model describes the covered native code. The sync commit was still 7366b75 (#12). Since then, #40 to #43, #46, and #49 changed covered code. #46 promised this follow-up.

What changed

• The sync commit moves to c54051e, the current main. It includes test: check that encodeMouse reads every caller field once #48 and fix(native): reject typed arrays other than Uint8Array in feed #49.
• The coverage rows now name ghostty_terminal_set (scrollback byte limit) in the constructor and its failure path, Resize's second ghostty_terminal_resize call, and the GHOSTTY_TERMINAL_DATA_MODE read in EncodeMouse. Ghostty v1.4.0 (feat: pin Ghostty v1.4.0 so DECSTR soft resets apply #43) brought these.
• The "no JS inside native methods" assumption now says how each method reads its arguments:
  1. Snapshot reads its options before RequireTerminal, and it builds its result with DefineValue and DefineIndex.
  2. Feed and Resize call RequireTerminal first. After that, they only test types and read strings, bytes, and numbers, which runs no JS.
  3. GetVisibleText, FormatPlain, and FormatHtml read no arguments.
  4. The assumption was false for snapshot until fix(native): keep snapshot() from running JS while it uses the terminal #46.
• The bullet that lists where caller JS can run now names public feed: assertFeedData runs data instanceof Uint8Array, which runs a Proxy's getPrototypeOf trap after #assertUsable. The native null check covers it, as it does for snapshot.
• AddonEnvLifecycle.tla changes in comments only. The CreateFails comment now names the ghostty_terminal_set failure too.

The model itself does not change. #48 changes only a test. #49 changes only Feed's argument checks, so the Use(t) step still describes feed.

Verification

• I checked each row against native/terminal.cc and src/index.ts at c54051e.
• git diff 7366b75 c54051e on the covered paths adds no new static state, Napi::Reference, or new place that frees terminal_ or mouse_encoder_.
• run.sh: all 35 rows match EXPECT (OK: every result matches EXPECT.). The current config holds all 5 rules. Each of the 6 mutants breaks the rule it guards.

The verifier's two notes on 0ff0941 (the feed window and the CreateFails comment) are fixed in 584c561. run.sh still passes all 35 rows.

Workspace 36beaed175 drafted the first version of this commit. I corrected the assumption bullet: it said that every method reads its arguments before RequireTerminal, but Feed and Resize do not.

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: xhigh

[ThomasK33]

Verdict: PASS+NOTES
Head: 0ff0941

Parent: main c54051ec9a4d2eeed2ebf09533ac2e9175fcc79c. The diff changes only SKILL.md (7 lines) and 2 comment blocks in AddonEnvLifecycle.tla. git diff -U0 origin/main...HEAD -- '*.tla' has 0 changed lines outside (* ... *), so the model logic is unchanged.

Check 1. Rows and the assumption bullet against the head code. Every changed statement is true.

• Constructor row: ghostty_terminal_new (terminal.cc:242), then ghostty_terminal_set(SCROLLBACK_MAX_BYTES) (:249), then ghostty_mouse_encoder_new (:257).
• CreateFails row: when the set call fails, the code frees created before terminal_ = created (:250-254). When the encoder call fails, it frees terminal_ and sets it to nullptr (:258-261).
• Use row: Resize calls ghostty_terminal_resize twice (:347, :350). Only a ThrowResult that exits the method sits between the calls.
• EncodeMouse row: ghostty_terminal_get(GHOSTTY_TERMINAL_DATA_MODE) (:411) runs after RequireTerminal/RequireMouseEncoder (:406-407). No ghostty_terminal_mode_get is left in the code.
• Assumption bullet: Snapshot reads both options (:491-492) before RequireTerminal (:495). BuildSnapshot, BuildLines, and BuildCellObject use only DefineValue/DefineIndex (:157-165). Set() remains only in GetNativeInfo (:814-822), which uses no terminal. Feed (:296) and Resize (:331) call RequireTerminal first. After that they use only IsString/IsTypedArray/TypedArrayType/Utf8Value/Data/ByteLength and IsNumber/DoubleValue, with no coercion and no Get(). GetVisibleText, FormatPlain, and FormatHtml never read info. The #46 history matches 9f8ec06^: options were read after RequireTerminal, and src/index.ts:69 returns {} for no options.

Check 2. Coverage of git diff --stat 7366b75 c54051e on the covered paths (6 files, +291/-250). The diff adds no static or global state and no new Napi::Reference/FunctionReference. It adds no new path that frees or uses a handle outside the rows above. After a native method takes a handle, no JS runs. The other changes have no lifecycle effect: the dead IsExceptionPending checks are gone (#40), the IsBuffer branch is gone (#49), and ValidateUtf8MouseCoordinate lost is_row (#42). The src/index.ts changes are the read-once normalizers (#41), and the EncodeTs row still holds. package-lock.json changes only dev dependencies. node-addon-api stays 8.9.2, as the row says.

Check 3. Model run at the head. run.sh "$OUT_DIR" gave 35 of 35 rows matching EXPECT, OK: every result matches EXPECT., exit 0. current.cfg found 8661 distinct states, the number in SKILL.md. Then I set TakeHandlesLast = FALSE in current.cfg as a local edit (handles taken before the reads) and ran it again. current NoCallOnDeadHandle breaks holds <-- DIFFERS, exit 1. The trace was LoadAddon, CreateTerminal, EncodeTs, EncodeEnter, Dispose, EncodeCall. I reverted the edit, and git status is clean.

Check 4. Runtime probe (ReleaseFast addon, Node 26.12.1, one child process per case). I put traps on Object.prototype getters and setters, on valueOf/toString/Symbol.toPrimitive, on the %TypedArray%.prototype accessors, and on Proxy handlers. Each trap calls dispose().

• Raw feed ran with 10 inputs: string, Uint8Array, Buffer, a Uint8Array subclass, Uint16Array, DataView, Proxy(Uint8Array), a String object, a coercing object, and a number. Raw resize ran with 6 inputs: numbers, Number objects, coercing objects, strings, Proxy, and narrower+taller. No trap fired in any case. The 3 no-argument methods also fired no trap when I passed them coercing or Proxy arguments.
• Positive controls: raw snapshot({}) and snapshot(Proxy) fire the traps before the check. They then throw GhosttyVtTerminal has been disposed, and every process exits 0.
• npm test at the head: 6 files, 85 tests pass.

Notes (non-blocking):

1. The TLA comment above CreateFails (AddonEnvLifecycle.tla:162-164) still names only the ghostty_mouse_encoder_new failure. The row now also maps the ghostty_terminal_set failure to CreateFails. The comment is not false, but it is incomplete.
2. This note is about text from before this PR, which the PR does not change. The "JS can run where code reads a caller's values" bullet does not list public feed. There, data instanceof Uint8Array (src/index.ts:80) runs a Proxy getPrototypeOf trap after #assertUsable. The probe showed that the trap disposes the terminal and native RequireTerminal then throws "disposed", with no crash. The native null check covers this window, so the model's result holds.

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: xhigh

[ThomasK33]

Verdict: PASS
Head: 584c561

Delta since my last check: git diff 0ff0941 584c561 (SKILL.md 1 line, TLA 1 comment block). The TLA change has 0 lines outside comments.

• New CreateFails comment: true. When ghostty_terminal_set fails, the constructor frees created once, and terminal_ keeps its nullptr default (terminal.cc:250-254, terminal.hh:43). When ghostty_mouse_encoder_new fails, it frees terminal_ once and sets it to nullptr (terminal.cc:258-261). Both paths throw.
• New feed sentence: true. feed calls #assertUsable, then assertFeedData, whose data instanceof Uint8Array (src/index.ts:80, :223-225) runs a Proxy's getPrototypeOf trap. My earlier probe showed it: public feed(Proxy(Uint8Array)) fired 1 getPrototypeOf trap, dispose() ran in that trap, native RequireTerminal threw GhosttyVtTerminal has been disposed, and the process exited 0. Use(t) covers feed.
• run.sh "$OUT_DIR" at the head: 35 of 35 rows match EXPECT, 0 DIFFERS, OK: every result matches EXPECT., exit 0. current.cfg has 8661 distinct states.
• Main moved to 646fde4 (Release v0.1.0-beta.3 #47). On the covered paths that commit changes only the version string in package.json and package-lock.json, so the c54051e sync commit still describes the covered code.

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: xhigh