[ThomasK33]

This updates the verify-native-lifecycle model to describe the code that #12 added. The sync commit is 7366b7545170ad77f5151e445c60bbf5bb110d87, the squash commit of #12 on main.

Why

#12 adds a second libghostty handle (mouse_encoder_) and encodeMouse. The old model had neither. Its assumption "JS code cannot run inside a native method" is false for encodeMouse: Get() runs getters, including Object.prototype getters for keys that src/index.ts leaves out. That window let a getter dispose the terminal while EncodeMouse held copies of the handles (finding F2, fixed in #12 before it merged).

What changes

• The model gets the encoder handle: allocation, the constructor's failure path, DisposeNative, and the finalizer.
• encodeMouse is split at its JS windows: the TypeScript normalizers after #assertUsable (EncodeTs), the native Get() reads (EncodeEnter), and the libghostty calls (EncodeCall). EncodeThrows covers a getter that throws.
• New rule EncoderFreedOnce. NoCallOnDeadHandle also covers the encoder handle.
• New mutants:
  • mutant-handles-before-reads: the code before the F2 fix.
  • mutant-no-native-guard: no RequireTerminal or RequireMouseEncoder check.
  • mutant-keeps-encoder-pointer: DisposeNative does not clear mouse_encoder_.
• SKILL.md records F2 and the new coverage rows, bounds and assumptions. It corrects one sentence: removing only the native null checks does break NoCallOnDeadHandle, because a getter can dispose the terminal after #assertUsable passed.
• statechart-view.mjs labels the new steps and the encoder handle.

Result

run.sh exits 0. All 35 rows match EXPECT, and current.cfg has 8,661 distinct states (it had 2,121).

CONFIG	RULE	RESULT	EXPECT
current	CreateUsesOwnClass	holds	holds
current	LoadDeletesOnlyOwnRef	holds	holds
current	HandleFreedOnce	holds	holds
current	EncoderFreedOnce	holds	holds
current	NoCallOnDeadHandle	holds	holds
mutant-process-static	CreateUsesOwnClass	breaks	breaks
mutant-process-static	LoadDeletesOnlyOwnRef	breaks	breaks
mutant-process-static	HandleFreedOnce	holds	holds
mutant-process-static	EncoderFreedOnce	holds	holds
mutant-process-static	NoCallOnDeadHandle	holds	holds
mutant-dispose-keeps-pointer	CreateUsesOwnClass	holds	holds
mutant-dispose-keeps-pointer	LoadDeletesOnlyOwnRef	holds	holds
mutant-dispose-keeps-pointer	HandleFreedOnce	breaks	breaks
mutant-dispose-keeps-pointer	EncoderFreedOnce	holds	holds
mutant-dispose-keeps-pointer	NoCallOnDeadHandle	holds	holds
mutant-no-use-guards	CreateUsesOwnClass	holds	holds
mutant-no-use-guards	LoadDeletesOnlyOwnRef	holds	holds
mutant-no-use-guards	HandleFreedOnce	holds	holds
mutant-no-use-guards	EncoderFreedOnce	holds	holds
mutant-no-use-guards	NoCallOnDeadHandle	breaks	breaks
mutant-no-native-guard	CreateUsesOwnClass	holds	holds
mutant-no-native-guard	LoadDeletesOnlyOwnRef	holds	holds
mutant-no-native-guard	HandleFreedOnce	holds	holds
mutant-no-native-guard	EncoderFreedOnce	holds	holds
mutant-no-native-guard	NoCallOnDeadHandle	breaks	breaks
mutant-keeps-encoder-pointer	CreateUsesOwnClass	holds	holds
mutant-keeps-encoder-pointer	LoadDeletesOnlyOwnRef	holds	holds
mutant-keeps-encoder-pointer	HandleFreedOnce	holds	holds
mutant-keeps-encoder-pointer	EncoderFreedOnce	breaks	breaks
mutant-keeps-encoder-pointer	NoCallOnDeadHandle	holds	holds
mutant-handles-before-reads	CreateUsesOwnClass	holds	holds
mutant-handles-before-reads	LoadDeletesOnlyOwnRef	holds	holds
mutant-handles-before-reads	HandleFreedOnce	holds	holds
mutant-handles-before-reads	EncoderFreedOnce	holds	holds
mutant-handles-before-reads	NoCallOnDeadHandle	breaks	breaks

The mutant-handles-before-reads counterexample is the F2 bug: load the addon, create t1, call encodeMouse, copy the handles in native code, dispose t1 in a getter, then call libghostty on the freed handles. test/mouse-safety.test.ts on #12 replays it against the real addon. That test fails on the code before the fix and passes after it.

Not covered: the mouse argument checks, the encoded bytes and the mouse mode cache. #12's tests cover those.

---

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