Verify Selection Tracking

---
name: verify-selection-tracking
description: Model-check what Claude sees as the user's current selection in claudecode.nvim (TLA+/TLC) against guards read from the current Lua code, and replay paths on headless Neovim. Use after a change to selection tracking (lua/claudecode/selection.lua, its enable/disable calls in lua/claudecode/init.lua, server.broadcast or on_connect in lua/claudecode/server/init.lua, or the getCurrentSelection and getLatestSelection tools), to the debounce or demotion timers, the visual-exit flush, or held-selection behavior (issue #246), and before trusting such a change.
---

# Verify selection tracking

While Claude is connected, `lua/claudecode/selection.lua` pushes the user's selection as a `selection_changed` notification. `getCurrentSelection` and `getLatestSelection` return the same value, `M.state.latest_selection`. Each send sets it first, so this check treats `latest_selection` as what Claude holds. If it is wrong, Claude answers about text the user did not select, about text that is gone, or about the wrong file. When nothing is tracked, `getCurrentSelection` reads the editor itself (#457, #463). The model makes no claim about that answer.

A selection survives Esc: Claude holds it until the cursor moves or its text changes (issue #246). The plugin keeps that hold in `last_active_visual_selection`, `cursor_at_flush` and `selection_tick`, and ends it from `CursorMoved`, `BufEnter`, `TextChanged`, `ModeChanged`, two one-shot timers, and a listener on the buffer of the held selection (`nvim_buf_attach`: `on_lines`, `on_reload`).

The check explores every order of keys, mode changes, buffer switches, timer firings and timer callbacks in a small model, with each guard switched on or off to match the code as it is now. The model has no clock, so it covers every `visual_demotion_delay_ms`.

## Rules

| Rule                  | Plain sentence                                                                                                                                                                                           | Harm when broken                                                                            |
| --------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------- |
| `ReleaseSent`         | Right after you release a selection in a file (Esc), Claude holds it, also when you made it faster than the 100 ms debounce, and when a plugin edited another line or a `:write` ran while you selected. | A quick selection never reaches Claude (issue #246).                                        |
| `NoPhantomSelection`  | Claude only gets text you selected, never the text at the `'<,'>` marks after an operator such as `d` changed it.                                                                                        | Claude gets a selection the user never made.                                                |
| `NoTerminalSelection` | Claude never gets a selection in the Claude terminal buffer.                                                                                                                                             | Claude's own prompt text becomes the context.                                               |
| `HeldUntilMoved`      | Once events settle in a file, a selection you released stays with Claude while the cursor has not moved and its text is unchanged.                                                                       | The selection the user means to ask about is gone before they type (issue #246).            |
| `HeldInTerminal`      | Once events settle in the Claude terminal, Claude still holds the selection you released while its text is unchanged.                                                                                    | The selection is gone when the user goes to the terminal to type the question (issue #246). |
| `HeldEndsWhenMoved`   | Once events settle in a file, Claude holds a released selection only while the cursor has not moved since you released it.                                                                               | Claude answers about an old selection after the user moved on.                              |
| `SameFile`            | Once events settle in a file, Claude's selection is in that file.                                                                                                                                        | Claude thinks the user is in another file.                                                  |
| `ClaudeSeesCursor`    | Once events settle in a file, a cursor-only selection that Claude holds is where the cursor is, and in visual mode Claude holds the live selection.                                                      | Claude points at the wrong line or column.                                                  |
| `NoDeletedText`       | Once events settle, Claude holds no selection text that its buffer no longer has.                                                                                                                        | Claude answers about text the user deleted.                                                 |
| `TimerClosedOnce`     | No timer handle is closed twice.                                                                                                                                                                         | Neovim shows `handle ... is already closing`, a Lua error, while the user moves or types.   |

"Once events settle" means no debounce or demotion timer runs, no timer callback waits in the `vim.schedule` queue, and the check that the buffer listener queued with `vim.schedule` has run.

## Run

```bash
.agents/skills/verify-selection-tracking/check.sh            # about 1 min
.agents/skills/verify-selection-tracking/check.sh --keep     # same, keeps the TLC configs and output, prints the dir
.agents/skills/verify-selection-tracking/check.sh --mutants  # about 1 to 1.5 h (4486 s to 4990 s at a load average of 22 to 31), after you edit the model or a fact
.agents/skills/verify-selection-tracking/check.sh --record   # rewrite covered.lock, only after "Update after an intended change"
.agents/skills/verify-selection-tracking/check.sh --hash-only  # about 5 s, no TLC: only compares covered.lock with the code
```

The shared harness is `scripts/tla/check-lib.sh` (read its header). It pins TLC 1.7.4 by sha256 and downloads it to `~/.cache/claudecode-nvim-tla/` on the first run. It needs bash 4 or newer, Java 11 or newer (`JAVA=/path/to/java` overrides), and `sha256sum` or `shasum`. CI runs every `.agents/skills/verify-*/check.sh`. Run one TLC job at a time on a shared host.

Exit codes:

- `0` is PASS.
- `1` means a rule broke. A rule that breaks on a stale tree exits `1`, not `3`. With `--mutants`, `1` also means a guard no rule caught, or a rule that never broke.
- `2` is a tool or script error, or a model whose `TypeOK` breaks.
- `3` is STALE. The covered code changed since the model was last confirmed, so the change is unverified.

## Does the change touch the verified code?

Run `check.sh --hash-only`. `covered.lock` records, for each covered file, its hash, the hash of each block the model describes, and each line that reads or writes the selection state, a timer field, or calls a send, with its enclosing top-level statement. Any change to a covered file reads `STALE` (exit 3) and prints `was:`/`now:` lines for the changed file, blocks and sites.

Covered files and blocks:

- `lua/claudecode/selection.lua`: `cursor_unmoved_since_flush`, `clear_held_state`, `selection_text_is_there`, `cursor_in_other_buffer`, `demote_if_selection_text_changed`, `holds_selection_of`, `visual_entry_of`, `note_visual_edit`, `watch_selection_buffer`, `record_selection_read`, `reconcile_held_selection`, `M.enable`, `M.disable`, `M._cancel_debounce_timer`, `M._cancel_demotion_timer`, `M._create_autocommands`, `M.on_cursor_moved`, `M.on_mode_changed`, `M.on_text_changed`, `M.debounce_update`, `M.update_selection`, `M.handle_selection_demotion`, `M.get_visual_selection_from_marks`, `M.flush_visual_selection`, `M.has_selection_changed`, `M.send_selection_update`, `M.is_claude_terminal_buffer`, `M.get_latest_selection`.
- `lua/claudecode/init.lua`: `M.start` (calls `selection.enable(M.state.server, visual_demotion_delay_ms)`) and `M.stop` (calls `selection.disable()`, then stops the server).
- `lua/claudecode/server/init.lua`: `M.broadcast` and the `on_connect` callback.
- `lua/claudecode/tools/get_current_selection.lua` and `get_latest_selection.lua`: the `handler`, which starts from `get_latest_selection()`.

`git log -- .agents/skills/verify-selection-tracking/covered.lock` shows each confirmation. Move it forward, with `--record`, only after you confirm that the model describes the code at the new commit.

Not covered, so a change there shows nothing: `lua/claudecode/utils.lua` `selection_type` (which modes count as visual, Select mode among them), `valid_utf8` (decides whether the held text is still at its range) and `utf8_sequence_length` (keeps a cursor off the middle of a character), `lua/claudecode/terminal.lua` `get_active_terminal_bufnr` (the second check in `is_claude_terminal_buffer`), and `tools/get_open_editors.lua`, which also reads `get_latest_selection()`. A PASS says the model holds for the guards the facts read, on code that matches the record. It does not review a change. STALE never means "probably fine".

## Read the result

`check.sh` prints the code facts first. Each fact is a guard that a regex reads from the source. `TRUE` means the regex found the guard. `FALSE` means the model runs without that guard.

| Fact                          | Code it reads (all in `selection.lua`)                                                                                                                                                                                                                               |
| ----------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| `FlushOnVisualExit`           | the `ModeChanged` autocmd calls `on_mode_changed`, which calls `M.flush_visual_selection()` when `leaving_visual`                                                                                                                                                    |
| `FlushSkipsOperator`          | `on_mode_changed` makes `visual_entry` (`bufnr`, `consumed`, `unchecked_edits`) when visual mode starts. The flush returns when `entry.consumed or entry.unchecked_edits > 0` (an operator such as `d` consumed the selection)                                       |
| `FlushSkipsTerminal`          | the flush returns when `M.is_claude_terminal_buffer(current_buf)`                                                                                                                                                                                                    |
| `FlushRecordsCursor`          | the flush sets `M.state.cursor_at_flush` to the buffer and the window cursor                                                                                                                                                                                         |
| `UpdateSkipsTerminal`         | `update_selection` cancels the demotion and returns when `M.is_claude_terminal_buffer(current_buf)`                                                                                                                                                                  |
| `PendingKeepsHeld`            | in `update_selection`, while `M.state.demotion_timer` is set: `latest_selection` stays when `cursor_unmoved_since_flush`, else the cursor. That function compares the cursor with `cursor_at_flush` in the same buffer and reads `.left`                             |
| `ElseClearsHeldState`         | `update_selection`'s last branch (no demotion, no held selection here) clears `last_active_visual_selection` and `cursor_at_flush`                                                                                                                                   |
| `DemotionWaitsForMove`        | `handle_selection_demotion` returns while `cursor_unmoved_since_flush` (Condition 3)                                                                                                                                                                                 |
| `DemotionClearsHeldState`     | `handle_selection_demotion` clears the original buffer's `last_active_visual_selection` and `cursor_at_flush` after it demotes                                                                                                                                       |
| `DemotionIgnoresTerminal`     | `handle_selection_demotion` returns at once in a Claude terminal (Condition 1) and leaves `last_active_visual_selection` alone, so the return to the file keeps the selection                                                                                        |
| `DebounceIgnoresStale`        | the debounce callback returns unless `M.state.debounce_timer` is its own timer                                                                                                                                                                                       |
| `DemotionIgnoresStale`        | the demotion callback returns unless `M.state.demotion_timer` is its own timer                                                                                                                                                                                       |
| `ClearsBeforeClose`           | both `_cancel_*_timer` functions and both callbacks set the state field to `nil` before `timer:close()`                                                                                                                                                              |
| `EntryClearsHeld`             | `on_mode_changed` calls `clear_held_state()` when visual mode starts, except in the Claude terminal                                                                                                                                                                  |
| `FlushSkipReports`            | the flush skipped for an operator calls `clear_held_state()`, then `M.update_selection()` when `latest_selection` is not empty                                                                                                                                       |
| `PendingClearsHeld`           | the cursor branch of `update_selection`'s pending-demotion case calls `clear_held_state()` when it reports the cursor                                                                                                                                                |
| `ReconcileOnCursorMoved`      | `on_cursor_moved` calls `reconcile_held_selection(not entered_buffer)` before the debounce, and the `CursorMoved`, `CursorMovedI` and `BufEnter` autocmd passes `args.event == "BufEnter"` (the window cursor is not restored yet at `BufEnter`)                     |
| `ReconcileOnTextChanged`      | `on_text_changed` calls `reconcile_held_selection(true)` before the debounce, from the `TextChanged`, `TextChangedI` and `TextChangedP` autocmd                                                                                                                      |
| `TextChangeReports`           | `reconcile_held_selection` returns after `demote_if_selection_text_changed()`, which clears the held state and calls `update_selection` when the changedtick of the selection's buffer moved since the selection was read and `selection_text_is_there` says no      |
| `MoveReports`                 | `reconcile_held_selection` clears the held state and calls `update_selection` when `compare_cursor` and the cursor is not `cursor_unmoved_since_flush`                                                                                                               |
| `LeaveNoted`                  | `reconcile_held_selection` notes another buffer in `cursor_at_flush.away`, and sets `cursor_at_flush.left` for one that is not the Claude terminal, once the next event arrives                                                                                      |
| `ReadRecordsTick`             | the flush and the in-visual `update_selection` call `record_selection_read`, which records `selection_tick` (the buffer and its changedtick) next to the selection they read                                                                                         |
| `ListensToSelectionBuffer`    | `record_selection_read` also calls `watch_selection_buffer`, which attaches an `nvim_buf_attach` listener (`on_lines`, `on_reload`) whose callback schedules `demote_if_selection_text_changed`. `TextChanged` fires only for the current buffer                     |
| `TerminalReportsHeldBuffer`   | `demote_if_selection_text_changed` also runs when the Claude terminal is current and the selection's buffer is another one (`from_terminal`): it clears the held state and sends `cursor_in_other_buffer`, because `update_selection` does nothing in the terminal   |
| `UpdateChecksHeldText`        | `update_selection` in the Claude terminal calls `demote_if_selection_text_changed()` after it cancels the demotion, because a new terminal is not registered when `BufEnter` fires                                                                                   |
| `ListenerNotesVisualEdit`     | `on_mode_changed` calls `watch_selection_buffer(buf)` when visual mode starts in a buffer that is not the Claude terminal. Its `on_lines` finds the buffer's `visual_entry` (`visual_entry_of`) and `note_visual_edit` adds one to `unchecked_edits`                 |
| `VisualCheckSparesPluginEdit` | `note_visual_edit` schedules a check with `vim.schedule` that takes the edit back and sets `consumed` only when visual mode is over: a plugin's edit leaves the selection on the screen, an operator ends visual mode                                                |
| `FlushIgnoresTick`            | neither `on_mode_changed` nor the flush reads a changedtick (comments apart). `FALSE` models the code before #524: the flush returned when the changedtick moved since visual mode started, which took a plugin's edit of another line or a `:write` for an operator |

Five guards break no rule alone, because another guard covers for them. `--mutants` removes each with the guard that covers for it, and the rule that breaks is the one `EXPECT` in `check.sh` names. `LeaveNoted` breaks `HeldEndsWhenMoved` alone, but only with 2 files, so `--mutants` runs that rule with 2 files. `ReconcileOnTextChanged` breaks `NoDeletedText` alone in the model, because of `YouEditByPlugin`. On real Neovim that guard and `TextChangeReports` are not the only ones that end the hold after an edit of the current buffer: the listener's `on_lines` fires for that edit too and runs the same check, so the running plugin still ends the hold without either guard (`replays/held_after_plugin_edit.lua` prints `OK` with the call removed from `on_text_changed`). The model lets the listener see only an edit of a buffer that is not current (`YouEditOtherBuffer`). A `BROKEN` trace for one of these two guards is a counterexample of the model, not a failure of the running plugin. `--mutants` still requires them, because the model has no other way to end the hold at that edit.

| Removed together                                 | Rule that breaks    | The two guards                                                                                                                                |
| ------------------------------------------------ | ------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- |
| `DemotionClearsHeldState` and `MoveReports`      | `ClaudeSeesCursor`  | The demotion forgets the held selection after it reports the cursor. A cursor move reports the cursor and forgets the held selection at once. |
| `PendingClearsHeld` and `ReconcileOnCursorMoved` | `ClaudeSeesCursor`  | A pending-demotion update forgets the held selection when it reports the cursor. `CursorMoved` and `BufEnter` reconcile the hold at once.     |
| `ElseClearsHeldState` and `LeaveNoted`           | `SameFile`          | The last branch of `update_selection` forgets the held selection. A buffer entered other than the Claude terminal ends the hold.              |
| `EntryClearsHeld` and `FlushSkipReports`         | `HeldEndsWhenMoved` | A new visual selection forgets the held one. A flush skipped for an operator forgets it.                                                      |

The model also has three environment switches that are not facts. `check.sh` sets them in `tla_constants`:

- `DelayBelowDebounce`: `TRUE` restricts the model to the default order (`visual_demotion_delay_ms` 50 < `debounce_ms` 100): a demotion timer fires before any debounce timer started after it. `check.sh` uses `FALSE`, which covers every delay.
- `WithTerminal`: `TRUE` lets the user go to a Claude terminal buffer. `FALSE` models `terminal.provider = "none"` or `"external"`. `check.sh` always uses `TRUE`.
- `MaxEdits`: edits per file, 1.

On `BROKEN`, the script prints the TLC trace as action names. Each action names the step it models: `YouStartSelecting`, `YouExtendSelection`, `YouReleaseSelection` (Esc), `YouEditSelection` (`d`, `c`), `YouMoveCursor`, `YouEditAtCursor` (`x`), `YouEditByPlugin` (a plugin or reload changes the text: `TextChanged` without `CursorMoved`), `YouEditByPluginInVisual` and `YouWriteInVisual` (a plugin edits another line, or `:write` runs, while you select: only the changedtick moves), `YouEditOtherBuffer` (the same for a file that is not the current buffer: no `TextChanged`, no `BufEnter`), `YouEditElsewhere`, `YouSwitchBuffer`, and for each timer `...TimerFires` (the uv timer fires and queues its callback) and `...CallbackRuns`. `ListenerCheckRuns` is the check that the buffer listener queued with `vim.schedule`. Read the trace with the pstack `/statechart` skill:

1. Rerun with `--keep`.
2. Copy the broken run's `.cfg` from the kept dir. Shrink it: `Files = {f1}` unless the rule is `SameFile`, `HeldEndsWhenMoved` or `NoDeletedText`, `Ranges = {r1}`, `Pos = {p1}` unless the path moves the cursor, `MaxEdits = 0` unless it edits, `WithTerminal = FALSE` unless it visits the Claude terminal. Stop at the smallest config that still breaks the rule.
3. Give `/statechart` the kept `SelectionTracking.tla`, that cfg, and the view `model/statechart-view.ts`.

The report tells the path in plain words, for example "you start selecting, you press Esc, you press x on the cursor, 100 ms pass, the plugin updates Claude: Claude holds text you deleted from a.txt". That is the path of the `NoDeletedText` bug below.

Then decide which kind of failure it is:

- **Real bug.** A fact went `FALSE` because the change removed or moved a guard, or the facts are `TRUE` and the path is one the code can take. Replay it on headless Neovim with a probe in `replays/` (see below) before you report it. Report it in the code's words. Never weaken a rule or the model to make it pass.
- **Modeling error.** The facts are `TRUE` but the path needs a step the code cannot take, or a fact reads `FALSE` because the guard was reworded and still works. Fix the regex or the model, run `--mutants`, and say what you changed. If a replay does not show the bug, assume the model is wrong until you show it is not.

## Replays

Each probe in `replays/` starts the plugin through the real `require("claudecode").start()` with `terminal.provider = "none"`, then types keys through Neovim's main loop with real timers. It replaces only `server.broadcast`, in its own process, to record each `selection_changed`. It prints one line per step, the settled state, `OK` or `BUG`, and a count line, and Neovim exits 0 for `OK` and 1 for `BUG`. Each probe replays a path that once broke a rule (see "Bugs this model found"), or a limit that the model does not cover (the rows whose rule is `none`), so `OK` shows the promise kept or the limit as documented. A probe does not prove that one guard is needed on its own: the listener also covers for `ReconcileOnTextChanged` and `TextChangeReports` at runtime (see "Read the result").

```bash
NVIM=~/.local/share/mise/installs/neovim/0.12.3/bin/nvim \
  .agents/skills/verify-selection-tracking/replays/run.sh held_after_operator.lua
```

`run.sh` puts this checkout first on `runtimepath` and gives each run a fresh `XDG_*_HOME`, `CLAUDE_CONFIG_DIR` and `TMPDIR` under `$XUM_SCRATCH_DIR` (or `/tmp`), removed afterwards. `DELAY_MS=50` reruns the two long-delay probes (`other_file_after_return.lua`, `cursor_after_return.lua`) with the default delay. They use 1000 ms.

| Probe                                          | Keys                                                                       | Rule                                 |
| ---------------------------------------------- | -------------------------------------------------------------------------- | ------------------------------------ |
| `held_after_operator.lua`                      | `vb`, Esc, `gv`, `d`                                                       | `HeldEndsWhenMoved`, `NoDeletedText` |
| `held_after_quick_move.lua`                    | `ve`, Esc, `l`, then `h` 30 ms later                                       | `HeldEndsWhenMoved`                  |
| `held_after_edit.lua`                          | `viw`, Esc, `x`, `x`                                                       | `NoDeletedText`                      |
| `held_after_plugin_edit.lua`                   | `Vj`, Esc, a plugin deletes text of line 1                                 | `NoDeletedText`                      |
| `held_after_reload_in_terminal.lua`            | `ve`, Esc, the Claude terminal, Neovim reloads the rewritten file          | `NoDeletedText`                      |
| `held_after_edit_in_terminal.lua`              | `ve`, Esc, the Claude terminal, a plugin deletes the selected text         | `NoDeletedText`                      |
| `other_file_after_return.lua`                  | `ve`, Esc, `:b b.txt`, `:b a.txt`, a long delay                            | `SameFile`                           |
| `cursor_after_return.lua`                      | `ve`, Esc, `l`, `h` 250 ms later, a long delay                             | `ClaudeSeesCursor`                   |
| `held_after_line_inserted_above.lua`           | `ve`, Esc, a plugin inserts a line above the selection                     | none: a limit that the model skips   |
| `release_after_plugin_edit_in_visual.lua`      | `ve`, a plugin edits line 2, Esc within 100 ms                             | `ReleaseSent`, `HeldUntilMoved`      |
| `release_after_plugin_append_in_visual.lua`    | `ve`, a plugin appends two lines, Esc within 100 ms                        | `ReleaseSent`, `HeldUntilMoved`      |
| `release_after_write_in_visual.lua`            | a modified buffer, `ve`, `:write`, Esc within 100 ms                       | `ReleaseSent`, `HeldUntilMoved`      |
| `release_in_same_typeahead_as_plugin_edit.lua` | `ve`, then one mapping edits line 2 and presses Esc                        | `ReleaseSent`, `HeldUntilMoved`      |
| `release_with_key_during_plugin_callback.lua`  | `ve`, a timer callback edits line 2 and `nvim_input` sends Esc during it   | `ReleaseSent`, `HeldUntilMoved`      |
| `release_after_autocmd_edit_in_visual.lua`     | `ve<Esc>` in one typeahead, a `ModeChanged` autocmd for `n:v` edits line 2 | `ReleaseSent`, `HeldUntilMoved`      |
| `v_escape_selects_one_character.lua`           | `ve`, Esc, then `v` and Esc with no motion                                 | none: shows a bare `v` Esc selects   |

## Bugs this model found

The first version of the model found four broken rules on the code before #452. Each was replayed on Neovim 0.12.3 with the probe named, and #452 fixed all four:

1. **`HeldEndsWhenMoved`: Claude kept a released selection after the cursor left it, when the cursor stood where the selection was released again by the time the debounce fired.** You select `alpha` backwards (`vb`), press Esc, press `gv`, press `d` (`held_after_operator.lua`). Or you select `alpha` (`ve`), press Esc, press `l` and then `h` within 100 ms (`held_after_quick_move.lua`). The plugin compared the cursor with `cursor_at_flush` only when a timer fired, and a new selection or an operator did not clear it.
2. **`NoDeletedText`: Claude kept a held selection after you edited its text without moving the cursor.** You select `alpha` (`viw`), press Esc, then `x` twice. Claude still held `alpha` after the line became `alphbeta gamma` (`held_after_edit.lua`). Nothing compared the held text with the buffer.
3. **`SameFile`: with a long `visual_demotion_delay_ms`, Claude held another file's cursor.** With 1000 ms: you select `alpha` in `a.txt`, press Esc, `:b b.txt`, `:b a.txt`. Claude held `b.txt` 0:0 until the cursor moved (`other_file_after_return.lua`).
4. **`ClaudeSeesCursor`: with a long `visual_demotion_delay_ms`, Claude held a cursor position you had left.** With 1000 ms: you select `alpha`, press Esc, press `l`, wait, press `h`. The cursor was at 0:4 and Claude held 0:5 (`cursor_after_return.lua`).

#452 ends the hold when the cursor leaves, when a new selection starts, when an operator consumes the selection, and when its text changes. The model has each as a guard (`MoveReports`, `EntryClearsHeld`, `FlushSkipReports`, `TextChangeReports`).

A review of #452 found one more path, and #471 fixed it: Claude holds selection A, you start selection B, an operator consumes B before the 100 ms in-visual debounce, and you enter the Claude terminal inside that 100 ms. Claude kept A for the whole visit. The model has the fixed flush-skip step (`FlushSkipReports`). `tests/integration/selection_held_spec.lua` replays that exact path with a real terminal buffer. See "Scope and bounds" for what the model can and cannot say about it.

A reviewer of this skill found one more path that no model step could express then, and #481 fixed it: Claude holds selection A, you go to the Claude terminal, and A's file changes while you are there (Claude rewrites it and Neovim reloads it, or a plugin edits it). `TextChanged` fires only for the current buffer, so Claude kept A's old text until you came back (`replays/held_after_reload_in_terminal.lua`, `replays/held_after_edit_in_terminal.lua`). The model has a step for it (`YouEditOtherBuffer`) and three guards: `ListensToSelectionBuffer`, `TerminalReportsHeldBuffer` and `UpdateChecksHeldText`. The model found the last one in the first version of that fix: a file that changes while you are in another file, just before you open a new Claude terminal, finds the terminal unregistered at `BufEnter`, so only the debounce can send the cursor.

An advisor of this skill found a last path that the model could not express, and #524 fixed it: you select, a plugin edits another line (or a `:write` runs) while you are still in visual mode, and you press Esc inside the 100 ms debounce. Entering visual mode had recorded the buffer's changedtick, and the flush took a moved changedtick for an operator that consumed the selection, so Claude got the cursor and not the selection, although its text was untouched (`replays/release_after_plugin_edit_in_visual.lua`, `release_after_plugin_append_in_visual.lua`, `release_after_write_in_visual.lua`). #524 replaced the comparison with a `visual_entry` that the buffer listener marks: an operator's edit counts and ends in a skipped flush, a plugin's edit is checked once visual mode is known to be on, and a `:write` fires no callback. The model has two steps that move only the changedtick (`YouEditByPluginInVisual`, `YouWriteInVisual`) and three guards for the new code (`FlushSkipsOperator`, `ListenerNotesVisualEdit`, `VisualCheckSparesPluginEdit`). `FlushIgnoresTick` keeps the old comparison out: put it back into `selection.lua` and `check.sh` exits 1 and prints the first broken rule, `ReleaseSent` (you select, a plugin edits another line, you press Esc). `--mutants` lists the others that break with it: `HeldUntilMoved` and `HeldInTerminal`. #540 fixed three more paths of the same kind, in which the check of an edit had not run when the next key arrived: a mapping that edits and presses Esc in one typeahead, a key that arrives while a callback runs (the plugin's own, or another one that was queued before the check), and an autocmd that edits when visual mode starts with the Esc already in the typeahead (`replays/release_in_same_typeahead_as_plugin_edit.lua`, `release_with_key_during_plugin_callback.lua` and `release_after_autocmd_edit_in_visual.lua`). A plugin's edit now has its check run from `vim.schedule` and from a `vim.on_key` listener, whichever comes first, and `VisualCheckSparesPluginEdit` reads both. The three replays print `BUG` on the code before #540.

## Update after an intended change

1. Read every `was:`/`now:` line of the STALE output and the code behind it.
   - If only `file` lines changed, and the change cannot reach the selection state, a timer, a send, or the tools (for example a diff or terminal change in `init.lua`), say so in the PR. Then skip to step 4.
2. If the behavior changed, change the action or operator in `model/SelectionTracking.tla` that cites that code (`Update`, `Demote`, `Flush`, `Reconcile`, `OnModeChanged`, `DebounceUpdate`, the `Cancel*` operators, the listener operators `OnOtherBufferChanged`, `ListenerCheck`, `TerminalChanged` and `ReportHeldBuffer`, the entry operators `TickMoved`, `EntryEdited` and `PluginEditedInVisual`, or a `You*` step). If a guard moved, change its fact regex in `check.sh`. A regex must read its own guard only: remove each guard from `lua/` alone and see that only its own fact reads `FALSE`. If a rule breaks on the new code, that is a finding: replay it, and fix the code, not the rule.
3. Run `check.sh --mutants`. Every fact must be caught by its rule, alone or in a listed pair (`EXPECT`), and every rule must break at least once.
4. Run `check.sh` and read the result.
5. Run `check.sh --record` only once you have confirmed that the model describes the code at this commit. Commit `covered.lock` with the change.

## Scope and bounds

- The main run uses 2 files, the Claude terminal, 2 cursor positions, 2 selection ranges and 1 edit per file, any `visual_demotion_delay_ms` (129,986 distinct states). The `--mutants` runs use 1 file, except `SameFile`, `HeldEndsWhenMoved` and `NoDeletedText` with 2.
- One model step is one key or command together with the autocmds it fires (`ModeChanged`, `TextChanged`, `CursorMoved`, `BufEnter`). They run in the same main-loop iteration as the key, before Neovim polls libuv again, so no timer callback runs between them. A window command such as `<C-w>w` in visual mode fires `ModeChanged` in the old buffer first (checked on Neovim 0.12.3), so the model splits it into Esc and a buffer switch. Each uv timer firing and each scheduled callback is its own step, the listener's queued check included (`ListenerCheckRuns`). The one exception is the check of a plugin's edit while you select: the model runs it in the step of the edit. The code runs it from `vim.schedule` and from a `vim.on_key` listener, whichever comes first, so it runs before the flush of the next Esc (see the bullet on edits in visual mode). The model can fire a timer between any two keys, which also covers typeahead. Typed one key at a time, each key fires its autocmds before the next. Keys that run with no main-loop turn between them (a mapping, a macro, `:normal!`, typeahead) fire `CursorMoved` and `TextChanged` later or not at all: #471 was such a path. `YouEditSelection` leaves both out, so it is the case in which they have not fired yet.
- An operator in visual mode (`d`, `c`, `>`) sets the mode to normal before it changes the text, and `ModeChanged` (`v` to `n`) fires after the change: the listener's `on_lines` runs first, with the mode already normal, and the flush that `ModeChanged` triggers comes second. That order holds for 8 of 8 operators (`d`, `c`, `>`, `gU`, `~`, `J`, `r` and `x`) on Neovim 0.8.0 and 0.12.3, and the mode in `on_lines` is normal for these operators also on 0.9.5, 0.10.4 and 0.11.4. So the edit is counted before the flush. The cursor lands on any position. A plugin's edit in visual mode runs `on_lines` with the mode `n` on 0.8 and 0.9 (Neovim ends visual mode for the length of `nvim_buf_set_lines` and `nvim_buf_set_text`) and `v` from 0.10, so the code tests the mode in a `vim.schedule` callback, after the call. The model has no mode inside a call and runs that check before the next key.
- At `BufEnter` the window cursor is not restored yet, so the model compares it only at `CursorMoved` and `TextChanged`. A new Claude terminal is not registered when `BufEnter` fires, so the model lets the plugin not know it yet (`termKnown`) and decide at the next event.
- An edit changes the held text (`YouEditSelection`, `YouEditAtCursor`, `YouEditByPlugin`, `YouEditOtherBuffer`) or leaves it alone (`YouEditElsewhere`, and, while you select, `YouEditByPluginInVisual` and `YouWriteInVisual`, which move only the changedtick). The model keeps the changedtick as one bit on the visual entry ("moved since visual mode started"), not as a number per buffer: the code before #524 only compared it with the value recorded at entry, and a changedtick only grows. Each buffer has one text version, so the model cannot tell the text of the held selection from the text of another selection in the same buffer: the #471 path (an operator consumes a different selection) is checked by `tests/integration/selection_held_spec.lua`, and `FlushSkipReports` breaks no rule alone, because the held text is found at the next check anyway (the debounce in the Claude terminal, `UpdateChecksHeldText`, or the next `CursorMoved`). It is caught together with `EntryClearsHeld`. An edit that moves the held range's lines, such as a line added above, is not modeled. The code reads the range again with `nvim_buf_get_text`, and reports the cursor when the held text is not there. A user sees Claude lose the selection and get the cursor on the shifted line, although the selected text still exists (`replays/held_after_line_inserted_above.lua`). That is a limit, not a rule.
- The listener on the buffer of the held selection (`ListensToSelectionBuffer`) is attached once the selection is read. It only queues the check with `vim.schedule` (`check_soon`), so the model sets a queued-check bit at the edit and runs the check in a separate step (`ListenerCheckRuns`), after any other step: in the Claude terminal it sends the cursor of the selection's buffer, in the buffer of the selection it ends the hold, in another file it does nothing. A scheduled callback runs after the command that made a new Claude terminal returned, so the plugin knows the terminal then. That `:edit`, `:edit!` and `:bunload` detach it (`on_detach`), that the listener attaches itself again (from a `vim.schedule` callback, and only for a loaded buffer, because `nvim_buf_attach` returns `false` for an unloaded buffer and the `watched_buffers` entry would then block the next listener), and that `:checktime` keeps it (`on_reload`) are not modeled: `tests/selection_test.lua` and `tests/integration/selection_held_spec.lua` check them. If one of them went wrong, the listener would be gone (or doubled) after such a command, and a user in the Claude terminal would see Claude keep text that a reload or a plugin deleted until they come back.
- A held selection whose buffer becomes a Claude terminal after the selection was read is not modeled: the buffers of the model are files and the terminal `Term`, and no step turns one into the other. The triggers that were reproduced are `termopen()` in the buffer and a rename to a `term://...claude` name. A reload with a custom `terminal_cmd` did not reproduce it. Before #493, a change of that buffer's text made `update_selection` and `demote_if_selection_text_changed` call each other until Neovim raised `stack overflow` (from `CursorMoved`, `TextChanged` and `vim.schedule` callbacks) on every event, and Claude kept the old text. In another Claude terminal, the check also sent the cursor of that buffer, with a `term://` path. #493 fixed both: the check sends no cursor of a Claude terminal, cancels a pending demotion and forgets the read. `tests/selection_test.lua` and three cases of `tests/integration/selection_held_spec.lua` ("does not overflow the stack when the buffer of the held selection is taken for the Claude terminal", "does not send a cursor of the buffer that became the Claude terminal when a demotion is pending" and "sends nothing when the buffer of the held selection became a Claude terminal and you are in another") cover it. A change that brings the recursion back reads STALE here, and no rule breaks.
- `latest_selection` is what Claude holds: every send sets it first, `M.server` is always set while tracking runs, and both tools return it when it is set.
- `is_claude_terminal_buffer` finds the Claude terminal by a `term://` buffer name whose command contains `claude`, or by `terminal.get_active_terminal_bufnr()`. The model has one terminal buffer, `Term`, and treats both checks as one. So does `handle_selection_demotion`: its Condition 1 uses `is_claude_terminal_buffer`. It used to check only the active terminal, and a demotion that fired in a terminal that only its name marks cleared the held-state records of its buffer, which lost the selection when you came back.
- "After `:ClaudeCodeStop` nothing is sent" is not a rule, because no `selection.lua` guard can break it alone. `init.lua` `M.stop` calls `selection.disable()`, which clears the autocmds, both timers and `M.server`, and then stops the server, and `server.broadcast` returns `false` without a server. Start, stop and restart are not modeled.
- Not modeled, each with what a user sees when the code goes wrong there (read from the code, not replayed):
  - Select mode as distinct from Visual mode: `utils.selection_type` maps both to the same selection type, so Claude would answer about a selection in Select mode as in Visual mode. A wrong mapping makes Claude miss that selection.
  - Empty selections (no text): the flush skips them. If the skip went wrong, Claude would hold a selection with no text. A bare `v` and Esc is not empty: it selects the character under the cursor, and Claude gets that character in place of the held selection (`replays/v_escape_selects_one_character.lua`).
  - A second Claude terminal: the model has one. `handle_selection_demotion` takes Condition 1 in any buffer that `is_claude_terminal_buffer` accepts, the active terminal or one that only its name marks, and does nothing there.
  - `send_current_selection`: no code in `lua/` calls it. A bug there reaches a user only through a mapping the user wrote.
  - `:ClaudeCodeSend` at-mentions: they send a file and range mention, not the tracked selection. A bug there makes Claude get the wrong mention.
  - Insert mode as distinct from normal mode: `TextChangedI` and `TextChangedP` run the same handler as `TextChanged`. If they stopped doing so, Claude would keep a held selection that you typed over in insert mode.
  - A held selection whose buffer is unloaded while you are in the Claude terminal (`:bunload`): `demote_if_selection_text_changed` returns for a buffer that is not loaded, so the selection stays held. The model has no unloaded buffer. A user sees Claude keep the selection of a file that is not loaded until they come back, and then get the cursor (checked on Neovim 0.8.0 and 0.12.3 with `:bunload` in a Claude terminal tab and `:buffer` after it). The text on disk did not change, so Claude holds no text that is gone. Without the return, the check could not find the text in the unloaded buffer, would take it for gone, and would send the cursor of a file that is not loaded (read from the code). The listener is detached by the unload (`on_detach`) and attaches itself again only for a loaded buffer.
- Edits while you are in visual mode that the model leaves out: an edit of the selected text itself (the debounce or the listener's check reads the new text). The model runs the check of a plugin's edit in the step of the edit, and the code guarantees that since #540: `note_visual_edit` runs `check_visual_edits` from `vim.schedule` (after the command or callback that made the edit returns) and from a `vim.on_key` listener (before the next key is processed, also a key of a mapping or one that a UI sends while a callback runs), whichever comes first. The flush on Esc comes after the first of them. When the key came first, the schedule usually runs later, after the flush, and finds nothing to do. A `ModeChanged` handler that runs before the plugin's and turns the main loop (`vim.wait`) runs it earlier: after Neovim ended visual mode and before the flush. The key listener has already checked the edit then, so that second check finds nothing to do either way (the `unchecked_edits == 0` guard of `check_visual_edits`, which a unit test and an integration case pin). When the schedule came first, the key listener finds nothing. Before #540 only the schedule ran it, so a key that came first reached the flush with an edit that nobody had checked, and the flush took it for an operator's: Claude got the cursor and not the selection, although its text was untouched. Three ways to get there were reproduced on Neovim 0.8.0 and 0.12.3: a mapping that edits and presses Esc in one typeahead, a key that arrives while a callback runs (`nvim_input`, the way a UI sends a key: during the plugin's own callback, or during another one that was queued before the check), and an autocmd that edits when visual mode starts with the Esc already in the typeahead (a `ModeChanged` handler for `n:v`). The three replays print `OK` now and `BUG` on the code before #540. The model has no step in which a key comes before the check, so removing the key listener or the schedule shows only as `VisualCheckSparesPluginEdit` reading `FALSE` (the fact reads both triggers, and the model then breaks `ReleaseSent`).
- A reload or `:edit` while you select (`on_reload` and `on_detach` set `consumed`) counts as an operator, because it replaces the text under the selection. It is not modeled: a user sees Claude get the cursor and not the selection after the file was reloaded under it.
- Coming back from the Claude terminal to the file of a held selection with the cursor where it was: `HeldUntilMoved` applies there, so Claude keeps the selection. The model used to allow either outcome (`holdLoose`), because a demotion that fired in the terminal cleared `last_active_visual_selection` and the return then sent the cursor. A new terminal is not registered at its `BufEnter`, so nothing cancelled that demotion, and with the default 50 ms it fires before the debounce of the terminal does. `DemotionIgnoresTerminal` reads the code that no longer clears it, and a tree where that line is back breaks `HeldUntilMoved`. The replay-style probe is `tests/integration/selection_demotion_in_terminal_spec.lua`.
- A Claude that connects after the last change gets no `selection_changed` until the selection changes: `on_connect` sends none, and `has_selection_changed` stops a resend of an unchanged selection. PROTOCOL.md promises a notification only when the selection changes, and the tools answer on request, so this is not a rule.
- A pass covers this model at these bounds, for the facts `check.sh` reads, on the covered files exactly as recorded in `covered.lock`. Any other tree reads STALE.