feat(skills): add verify-selection-tracking, a TLA+ model of selection tracking

.agents/skills/verify-selection-tracking/model/statechart-view.ts

@@ -0,0 +1,96 @@
+// /statechart view for SelectionTracking.tla: what you do, what Claude holds, and whether a timer still waits.
+const file = (b: string) =>
+  ({ f1: "a.txt", f2: "b.txt" })[b] ?? "the Claude terminal";
+
+const waiting = (v: any) =>
+  v.db !== "nil" ||
+  v.dbStale ||
+  v.dbLoose ||
+  v.dm !== "nil" ||
+  v.dmStale ||
+  v.chk ||
+  (v.dmLoose && v.dmLoose.length > 0);
+
+// What Claude holds. While a timer waits, a cursor that is behind is normal, so only a settled state says so.
+const what = (v: any) => {
+  const sel = v.latest;
+  if (!sel || sel.kind === undefined) return "nothing";
+  if (sel.kind === "cur") {
+    const behind = !waiting(v) && sel.buf === v.buf && sel.at !== v.cur;
+    return `the cursor in ${file(sel.buf)}${behind ? ", where it was" : ""}`;
+  }
+  if (sel.ver !== v.ver[sel.buf])
+    return `text you deleted from ${file(sel.buf)}`;
+  const live = v.mode === "v" && sel.buf === v.buf && sel.at === v.vsel;
+  const held =
+    v.hold &&
+    v.hold.kind === "vis" &&
+    v.hold.at === sel.at &&
+    v.hold.buf === sel.buf;
+  return live || held
+    ? `your selection in ${file(sel.buf)}`
+    : `an old selection in ${file(sel.buf)}`;
+};
+
+const you = (v: any) => {
+  if (v.buf === "term")
+    return v.mode === "v"
+      ? "you select in the Claude terminal"
+      : "you are in the Claude terminal";
+  if (v.mode === "v") return `you select in ${file(v.buf)}`;
+  if (v.hold && v.hold.kind === "vis") {
+    const changed = v.hold.ver !== v.ver[v.hold.buf] ? " and edited it" : "";
+    return `you released a selection in ${file(v.buf)}${changed}`;
+  }
+  return `your cursor is in ${file(v.buf)}`;
+};
+
+export const title = "What Claude sees as your selection (claudecode.nvim)";
+
+export const state = (v: any) => {
+  if (v.mode === "v" && waiting(v)) return `${you(v)}; a timer waits`;
+  return `${you(v)}; Claude holds ${what(v)}${waiting(v) ? "; a timer waits" : ""}`;
+};
+
+export const group = (v: any) => {
+  if (waiting(v)) return "waiting";
+  const sel = v.latest;
+  const otherFile =
+    sel && sel.kind !== undefined && v.buf !== "term" && sel.buf !== v.buf;
+  return otherFile || /deleted|old|where it was/.test(what(v))
+    ? "stale"
+    : "current";
+};
+export const colors = { stale: "pink", current: "teal", waiting: "blue" };
+
+const labels: Record<string, string> = {
+  YouStartSelecting: "you start selecting (v, V, gv)",
+  YouExtendSelection: "you extend the selection",
+  YouReleaseSelection: "you press Esc",
+  YouEditSelection: "you delete or change the selection (d, c)",
+  YouMoveCursor: "you move the cursor",
+  YouEditAtCursor: "you press x on the cursor",
+  YouEditElsewhere: "you edit another line",
+  YouEditByPlugin: "a plugin or a reload changes the text away from the cursor",
+  YouEditOtherBuffer: "a plugin or a reload changes a file that you are not in",
+  YouEditByPluginInVisual: "a plugin edits another line while you select",
+  YouWriteInVisual: "you save the file while you select (:write)",
+  ListenerCheckRuns: "the plugin's listener checks the held text",
+  DebounceTimerFires: "100 ms pass",
+  DebounceCallbackRuns: "the plugin updates Claude",
+  LooseDebounceCallbackRuns: "a lost debounce timer runs",
+  DemotionTimerFires: "the demotion delay passes",
+  DemotionCallbackRuns: "the plugin checks whether you moved",
+  LooseDemotionCallbackRuns: "a lost demotion timer runs",
+};
+
+// A callback of a cancelled timer returns at once in the code as written, so the chart hides it.
+export const step = (action: string, _from: any, to: any) => {
+  if (
+    action === "StaleDebounceCallbackRuns" ||
+    action === "StaleDemotionCallbackRuns"
+  )
+    return null;
+  if (action === "YouSwitchBuffer") return `you go to ${file(to.buf)}`;
+  return labels[action] ?? action;
+};

.agents/skills/verify-selection-tracking/replays/cursor_after_return.lua

@@ -0,0 +1,23 @@
+-- ClaudeSeesCursor: with visual_demotion_delay_ms longer than two debounces (here 1000 ms), release a selection,
+-- move right, wait, move back. Claude must not keep the cursor position you left. Before #452 it did.
+-- DELAY_MS=50 (the default delay) reruns the same keys.
+local driver = require("driver")
+local delay = tonumber(os.getenv("DELAY_MS") or "1000")
+driver.run({
+  setup = { visual_demotion_delay_ms = delay },
+  prepare = function()
+    driver.files({ { "a.txt", { "alpha beta" } } })
+  end,
+}, {
+  { 50, "ve", "ve (select alpha)" },
+  { 300, "<Esc>", "<Esc> (release it)" },
+  { 250, "l", "l (move right)" },
+  { 250, "h", "h (move back)" },
+}, function(_, sel)
+  local cursor = vim.api.nvim_win_get_cursor(0)
+  if not sel or not sel.selection.isEmpty or sel.selection.start.character == cursor[2] then
+    return true, "Claude holds the cursor where it is, or the held selection"
+  end
+  return false,
+    string.format("the cursor is at 0:%d, Claude holds the cursor at 0:%d", cursor[2], sel.selection.start.character)
+end)

.agents/skills/verify-selection-tracking/replays/driver.lua

@@ -0,0 +1,128 @@
+-- Replay driver for the verify-selection-tracking probes. Starts the real plugin (the real start path, the real
+-- selection.lua with real uv timers), records every selection_changed the server would broadcast, and types keys
+-- through the main loop one step at a time. Only server.broadcast is replaced, and only in this process.
+-- A probe calls run(opts, steps, verdict): each step is { wait_ms, keys or function, label }; verdict(log, sel)
+-- returns ok (boolean) and a one-line description. Neovim exits 0 for OK and 1 for BUG.
+local M = {}
+
+local function show(sel)
+  if not sel then
+    return "nil"
+  end
+  local s, e = sel.selection.start, sel.selection["end"]
+  return string.format(
+    "%s %q %d:%d-%d:%d%s",
+    vim.fn.fnamemodify(sel.filePath, ":t"),
+    sel.text,
+    s.line,
+    s.character,
+    e.line,
+    e.character,
+    sel.selection.isEmpty and " (cursor)" or ""
+  )
+end
+M.show = show
+
+-- Writes each { name, lines } to a fresh temp dir and opens them, the first one last (so it is current).
+-- Returns the paths in order.
+function M.files(list)
+  local dir = vim.fn.tempname()
+  vim.fn.mkdir(dir, "p")
+  local paths = {}
+  for i = #list, 1, -1 do
+    local path = dir .. "/" .. list[i][1]
+    vim.fn.writefile(list[i][2], path)
+    vim.cmd.edit(vim.fn.fnameescape(path))
+    paths[i] = path
+  end
+  return paths
+end
+
+function M.run(opts, steps, verdict)
+  local out = {}
+  local function say(line)
+    table.insert(out, line)
+  end
+  vim.o.showmode = false
+  local claudecode = require("claudecode")
+  claudecode.setup(vim.tbl_deep_extend("force", {
+    auto_start = false,
+    terminal = { provider = "none" },
+    log_level = "error",
+  }, opts.setup or {}))
+  local ok = claudecode.start(false)
+  assert(ok, "claudecode.start failed")
+  local sent = {}
+  require("claudecode.server.init").broadcast = function(method, params)
+    if method == "selection_changed" then
+      table.insert(sent, vim.deepcopy(params))
+      say(string.format("    sent selection_changed: %s", show(params)))
+    end
+    return true
+  end
+  local selection = require("claudecode.selection")
+  say(
+    string.format(
+      "nvim %s, debounce_ms=%d, visual_demotion_delay_ms=%d",
+      tostring(vim.version()),
+      selection.state.debounce_ms,
+      selection.state.visual_demotion_delay_ms
+    )
+  )
+  if opts.prepare then
+    opts.prepare()
+  end
+  local i = 0
+  local function finish()
+    local sel = selection.get_latest_selection()
+    local cursor = vim.api.nvim_win_get_cursor(0)
+    say(
+      string.format(
+        "settled: buffer %s, cursor %d:%d, line %q",
+        vim.fn.expand("%:t"),
+        cursor[1] - 1,
+        cursor[2],
+        vim.api.nvim_get_current_line()
+      )
+    )
+    say(string.format("Claude holds (getLatestSelection): %s", show(sel)))
+    local good, why = verdict(sent, sel)
+    say((good and "OK " or "BUG ") .. why)
+    say(string.format("%d selection_changed sent, result: %s", #sent, good and "rule holds" or "rule broken"))
+    io.stdout:write(table.concat(out, "\n") .. "\n")
+    vim.cmd(good and "qa!" or "cquit 1")
+  end
+  local function step()
+    i = i + 1
+    local s = steps[i]
+    if not s then
+      -- Let every timer settle: well past the debounce and the demotion delay.
+      vim.defer_fn(finish, 300 + 2 * selection.state.visual_demotion_delay_ms)
+      return
+    end
+    vim.defer_fn(function()
+      local cursor = vim.api.nvim_win_get_cursor(0)
+      say(
+        string.format(
+          "  now: mode=%s buf=%s cursor=%d:%d line=%q",
+          vim.api.nvim_get_mode().mode,
+          vim.fn.expand("%:t"),
+          cursor[1] - 1,
+          cursor[2],
+          vim.api.nvim_get_current_line()
+        )
+      )
+      local keys = s[2]
+      say(string.format("+%4dms %s", s[1], s[3] or keys))
+      if type(keys) == "function" then
+        keys()
+      else
+        vim.api.nvim_feedkeys(vim.api.nvim_replace_termcodes(keys, true, false, true), "t", false)
+      end
+      step()
+    end, s[1])
+  end
+  step()
+end
+
+return M

.agents/skills/verify-selection-tracking/replays/held_after_edit.lua

@@ -0,0 +1,23 @@
+-- NoDeletedText: release a selection, then press x on its last character without moving the cursor. Claude must
+-- not keep text the buffer no longer has: the plugin reports the cursor once the held text changed. Default delays.
+-- Before #452 the held selection survived until the cursor moved.
+local driver = require("driver")
+driver.run({
+  prepare = function()
+    driver.files({ { "a.txt", { "alpha beta gamma" } } })
+  end,
+}, {
+  { 50, "viw", "viw (select alpha)" },
+  { 300, "<Esc>", "<Esc> (release it)" },
+  { 300, "x", "x (delete the a under the cursor)" },
+  { 300, "x", "x (and the space)" },
+}, function(_, sel)
+  local line = vim.api.nvim_get_current_line()
+  if not sel or sel.selection.isEmpty then
+    return true, "Claude holds the cursor"
+  end
+  local s, e = sel.selection.start.character, sel.selection["end"].character
+  local there = line:sub(s + 1, e)
+  return there == sel.text,
+    string.format("Claude holds %q at %d-%d, the buffer has %q there (line %q)", sel.text, s, e, there, line)
+end)

.agents/skills/verify-selection-tracking/replays/held_after_edit_in_terminal.lua

@@ -0,0 +1,42 @@
+-- NoDeletedText: Claude holds a selection of a.txt, you are in the Claude terminal in the same window (a.txt is in no
+-- window), and a plugin deletes the selected text with nvim_buf_set_text. Neovim reports it to the buffer's listeners
+-- only. Claude must not keep text that is gone until you come back. Default delays.
+local driver = require("driver")
+local file_buf
+driver.run({
+  prepare = function()
+    driver.files({ { "a.txt", { "alpha beta gamma" } } })
+    file_buf = vim.api.nvim_get_current_buf()
+  end,
+}, {
+  { 50, "ve", "ve (select alpha)" },
+  { 300, "<Esc>", "<Esc> (release it)" },
+  {
+    300,
+    function()
+      vim.cmd("terminal sh -c 'sleep 20' claude")
+    end,
+    ":terminal ... claude (the Claude terminal, in a.txt's window)",
+  },
+  {
+    300,
+    function()
+      vim.cmd("stopinsert")
+    end,
+    "stopinsert",
+  },
+  {
+    300,
+    function()
+      vim.api.nvim_buf_set_text(file_buf, 0, 0, 0, 6, {})
+    end,
+    "a plugin deletes 'alpha ' in a.txt",
+  },
+  { 300, function() end, "wait" },
+}, function(_, sel)
+  if not sel or sel.selection.isEmpty then
+    return true, "Claude holds the cursor"
+  end
+  local lines = vim.api.nvim_buf_get_lines(file_buf, 0, -1, false)
+  return false, string.format("Claude holds %q, but a.txt is %q", sel.text, table.concat(lines, "|"))
+end)

.agents/skills/verify-selection-tracking/replays/held_after_line_inserted_above.lua

@@ -0,0 +1,22 @@
+-- A limit that the model does not cover, not a rule: a plugin inserts a line above a held selection. The held range now
+-- names other text, so the check that reads the range again finds that the selected text is not there and reports the
+-- cursor. Claude loses the selection, although its text still exists one line lower. OK means the plugin does that.
+local driver = require("driver")
+driver.run({
+  prepare = function()
+    driver.files({ { "a.txt", { "alpha beta gamma" } } })
+  end,
+}, {
+  { 100, "ve", "select alpha" },
+  { 200, "<Esc>", "release alpha" },
+  {
+    300,
+    function()
+      vim.api.nvim_buf_set_lines(0, 0, 0, false, { "inserted line" })
+    end,
+    "a plugin inserts a line above the held range",
+  },
+}, function(_, sel)
+  return sel and sel.selection.isEmpty and sel.selection.start.line == 1,
+    "Claude holds the cursor on the shifted line, not the selection"
+end)

.agents/skills/verify-selection-tracking/replays/held_after_operator.lua

@@ -0,0 +1,22 @@
+-- HeldEndsWhenMoved / NoDeletedText: a selection made backwards (cursor at its start), released with Esc, then
+-- reselected with gv and deleted with d. The cursor ends where the first flush left it. Claude must hold the
+-- cursor, not the deleted selection. Default delays. Before #452 the plugin took the deleted selection for a held one.
+local driver = require("driver")
+driver.run({
+  prepare = function()
+    driver.files({ { "a.txt", { "alpha beta gamma" } } })
+    vim.api.nvim_win_set_cursor(0, { 1, 4 })
+  end,
+}, {
+  { 50, "vb", "vb (select alpha backwards)" },
+  { 300, "<Esc>", "<Esc> (release it)" },
+  { 400, "gv", "gv (select it again)" },
+  { 300, "d", "d (delete it)" },
+}, function(_, sel)
+  local line = vim.api.nvim_get_current_line()
+  local cursor = vim.api.nvim_win_get_cursor(0)
+  if sel and sel.selection.isEmpty and sel.selection.start.character == cursor[2] then
+    return true, "Claude holds the cursor"
+  end
+  return false, string.format("Claude holds %q, but the line is now %q", sel and sel.text or "nil", line)
+end)

.agents/skills/verify-selection-tracking/replays/held_after_plugin_edit.lua

@@ -0,0 +1,27 @@
+-- NoDeletedText: a plugin (or a reload, or a command) changes the held text away from the cursor. TextChanged fires,
+-- CursorMoved does not. The TextChanged handler ends the hold, and so does the buffer listener (on_lines fires for an
+-- edit of the current buffer too), so this probe also passes with the TextChanged call removed: it does not prove
+-- that guard on its own (see SKILL.md, "Read the result"). Claude must not keep text the buffer no longer has.
+-- Default delays.
+local driver = require("driver")
+driver.run({
+  prepare = function()
+    driver.files({ { "a.txt", { "alpha beta", "gamma delta" } } })
+  end,
+}, {
+  { 50, "Vj", "Vj (select both lines)" },
+  { 300, "<Esc>", "<Esc> (release it)" },
+  {
+    300,
+    function()
+      vim.api.nvim_buf_set_text(0, 0, 0, 0, 6, {})
+    end,
+    "a plugin deletes 'alpha ' on line 1 (cursor stays on line 2)",
+  },
+}, function(_, sel)
+  if not sel or sel.selection.isEmpty then
+    return true, "Claude holds the cursor"
+  end
+  local lines = vim.api.nvim_buf_get_lines(0, 0, -1, false)
+  return false, string.format("Claude holds %q, but the buffer is %q", sel.text, table.concat(lines, "\n"))
+end)