diff --git a/.agents/skills/verify-claudecode-nvim/features/send-at-mention.md b/.agents/skills/verify-claudecode-nvim/features/send-at-mention.md index 98f8f81e9..f11aca5b5 100644 --- a/.agents/skills/verify-claudecode-nvim/features/send-at-mention.md +++ b/.agents/skills/verify-claudecode-nvim/features/send-at-mention.md @@ -11,7 +11,7 @@ The user hands Claude a file, a directory, or a line range as context. `:ClaudeC - `send-add-errors` sends nothing and shows an error for a missing path or a start line after the end line. - `send-mapped` sends from a Visual or Select mode mapping to `ClaudeCodeSend`, as in the README, and leaves the user in Normal mode. - `send-tree` sends the file under the cursor in netrw on `:ClaudeCodeTreeAdd` or `:ClaudeCodeSend`. -- `send-queue` holds a mention made while no client is connected and sends it to the next client that completes its WebSocket handshake within `connection_timeout` (default 10000 ms), `connection_wait_delay` (default 600 ms) after that handshake. Without such a client it shows "Connection timeout - clearing 1 queued @ mentions". +- `send-queue` holds a mention made while no client is connected and sends it to the next client that completes its WebSocket handshake within `connection_timeout` (default 10000 ms), `connection_wait_delay` (default 600 ms) after that handshake. Without such a client it shows "Connection timeout - clearing 1 queued @ mentions" at the deadline, `connection_timeout + connection_wait_delay` (10.6 s) after the send. While a client is connected but not ready yet, the text is "Send timeout - clearing 1 queued @ mentions that the connected Claude did not take in time". ## How to get to it (user POV) diff --git a/.agents/skills/verify-diff-lifecycle/covered.lock b/.agents/skills/verify-diff-lifecycle/covered.lock index f8acdf388..e89f1aaae 100644 --- a/.agents/skills/verify-diff-lifecycle/covered.lock +++ b/.agents/skills/verify-diff-lifecycle/covered.lock @@ -1,5 +1,5 @@ == lua/claudecode/config.lua -file lua/claudecode/config.lua 787fa0432d1d77d7 +file lua/claudecode/config.lua 3afb1bdeff27bfb6 == lua/claudecode/cwd.lua file lua/claudecode/cwd.lua 35b7af3572d13018 == lua/claudecode/diff.lua @@ -211,7 +211,7 @@ file lua/claudecode/tools/open_file.lua b277cbe8b86ac7c8 == lua/claudecode/tools/save_document.lua file lua/claudecode/tools/save_document.lua 584b046bec6cb1f6 == lua/claudecode/types.lua -file lua/claudecode/types.lua dbd0dcb8b70c8107 +file lua/claudecode/types.lua 69e2907853403759 == lua/claudecode/utils.lua file lua/claudecode/utils.lua c4a21fe74858afe2 == lua/claudecode/visual_commands.lua diff --git a/.agents/skills/verify-mention-queue/SKILL.md b/.agents/skills/verify-mention-queue/SKILL.md new file mode 100644 index 000000000..d2255ebab --- /dev/null +++ b/.agents/skills/verify-mention-queue/SKILL.md @@ -0,0 +1,152 @@ +--- +name: verify-mention-queue +description: Model-check the claudecode.nvim @ mention queue and the WebSocket clients it sends to (TLA+/TLC) against guards read from the current Lua code. Use after a change to how @ mentions are queued, flushed, timed out, or dropped, to when a client counts as connected or ready, to how a broadcast reports its writes, or to what a stop does to the queue (lua/claudecode/init.lua send_at_mention, _broadcast_at_mention, queue_mention, schedule_mention_flush, flush_mention_queue, expire_mentions, ms_until_a_client_is_ready, report_unwritten, clear_mention_queue, process_mention_queue, M.stop, on_open and broadcast in server/init.lua, the connect and broadcast paths in server/tcp.lua, the handshake, write and send paths in server/client.lua), and before trusting such a change. +--- + +# Verify the @ mention queue + +You send a file or a selection to Claude with `:ClaudeCodeSend`, `:ClaudeCodeAdd` or a tree command. The plugin puts the mention in one queue, oldest first. Each mention gets a deadline, `connection_timeout + connection_wait_delay` ms after the send (10.6 s by default). A flush sends the oldest mention once some connected client has been connected for `connection_wait_delay` ms since its WebSocket handshake. The broadcast reaches every connected client. A mention still queued at its deadline leaves with an error, unless a ready client is connected: then the queue drains to that client, 25 ms apart, also past the deadlines, and a flush that finds no ready client clears the mentions whose deadline passed meanwhile. This check explores every order of your sends, the clients' connects, handshakes, closes and drops, the plugin's timers and scheduled callbacks, and `:ClaudeCodeStop`/`:ClaudeCodeStart`, in a small model, with each guard switched on or off to match the code as it is now. + +## Rules + +| Rule | Plain sentence | Harm when broken | +| ------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------- | +| `NoSilentDrop` | A mention you sent reaches Claude, or you see an error, unless you stopped the integration first. | Claude never gets the context you sent, and nothing tells you, so you ask Claude about a file it never saw. | +| `SentInOrder` | Each Claude gets the mentions in the order you sent them. | Claude reads your context out of order, for example the follow-up selection before the file it refers to. | +| `AtMostOnce` | Each Claude gets each mention at most once. | Claude gets the same context twice and counts it twice. | +| `SentWhenReady` | A mention goes out only while some connected client has been connected for `connection_wait_delay` ms since its handshake. Default config only: `disable_broadcast_debouncing` breaks it, a known bug (see "Scope and bounds"). | Claude gets the mention inside the `connection_wait_delay` that the plugin leaves it to start up after its handshake. | +| `NothingAfterStop` | After `:ClaudeCodeStop`, no mention queued before the stop reaches Claude, and the queue raises no Lua error. | A Lua error appears after you stopped the integration, or a mention from before the stop reaches a new Claude session. | +| `NoStrandedMention` | Every queued mention leaves the queue: it is sent, dropped with an error at its deadline, or cleared by a stop (liveness). | The mention waits with no timer, so you never get the error that would tell you to send it again. | +| `ReadyDelivers` | While a ready Claude stays connected, every queued mention goes out to it (liveness). | Claude is connected and ready, and the mentions you sent never arrive, or leave as a timeout error while Claude takes the queue. | +| `FlushDelivers` | While a ready Claude stays connected, the flushes alone send it every queued mention: none waits for a deadline to pass first (liveness). | A mention reaches Claude only once a deadline passes, 10.6 s after the send, not 25 to 600 ms after Claude is ready. | + +The liveness rules assume that every timer fires, every scheduled callback runs, a 101 write completes, a closing socket closes, and time passes, so a client that stays connected becomes ready. They never assume that you or Claude act. `FlushDelivers` runs with no deadline that passes: in this untimed model a deadline can pass at any step, and a deadline that spares a ready Claude schedules a flush, so it would hide a flush path that leaves a ready Claude waiting for a deadline. + +## Run + +```bash +.agents/skills/verify-mention-queue/check.sh # about 60 s +.agents/skills/verify-mention-queue/check.sh --keep # same, keeps the TLC configs and output, prints the dir +.agents/skills/verify-mention-queue/check.sh --mutants # 25 to 50 min, after you edit the model or a fact +.agents/skills/verify-mention-queue/check.sh --record # rewrite covered.lock, only after "Update after an intended change" +.agents/skills/verify-mention-queue/check.sh --hash-only # under 1 s, no TLC: only compares covered.lock with the code (exit 0 or 3) +``` + +`check.sh` sources `scripts/tla/check-lib.sh`, the shared harness. Read its header for the options. CI runs every `.agents/skills/verify-*/check.sh` in the `covered-lock` job. The job is not required, so a PR that breaks a rule shows it red but can still merge. + +Needs bash 4 or newer, Java 11 or newer (`JAVA=/path/to/java` overrides `java`), `sha256sum` or `shasum`, and curl for the first run, which downloads TLC 1.7.4 to `~/.cache/claudecode-nvim-tla/` and refuses a jar whose sha256 differs. Run one copy at a time on a shared host. TLC is CPU heavy. + +Exit codes: + +- `0` is PASS. +- `1` means a rule 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. A broken rule exits 1 even when the record is stale. + +The main run checks the five invariants in one TLC run, which stops at the first break and names only that rule. Each liveness rule has its own run. To check one invariant alone, rerun with `--keep`, edit the `INVARIANT` line of `main.cfg` in the kept dir, and run TLC there on that cfg as `check-lib.sh` does (`java -cp tlc2.TLC -config main.cfg MentionQueue.tla`). + +## Does the change touch the verified code? + +Run the check. `covered.lock` records a hash of each covered file: `lua/claudecode/init.lua`, `lua/claudecode/config.lua`, `lua/claudecode/server/init.lua`, `lua/claudecode/server/tcp.lua` and `lua/claudecode/server/client.lua`. Any change to one of them reads `STALE` (exit 3, or 1 with a broken rule) until someone confirms that the model still describes the code. + +To show where to look, the record also hashes each block the model describes, and lists every non-comment line that names the queue, its timers, its functions, the connection or readiness check, `connected_at`, the handshake flag, the delays, `at_mentioned`, `on_open` or `on_written`, with its enclosing top-level statement. The STALE output prints a `was:`/`now:` pair for each changed file, block or line. + +Covered blocks: + +- In `init.lua`: `M.is_claude_connected`, `ms_until_a_client_is_ready`, `start_timer`, `clear_mention_queue`, `expire_mentions`, `report_unwritten`, `flush_mention_queue`, `schedule_mention_flush`, `queue_mention`, `M.process_mention_queue`, `M.send_at_mention`, `M._broadcast_at_mention`, `M.stop`. +- In `server/init.lua`: the `on_open` callback, `M.broadcast`, `M.get_status`. +- In `server/tcp.lua`: `M._handle_new_connection`, `M.broadcast`, `M.get_clients_info`. +- In `server/client.lua`: `write`, `M.process_data` (the handshake), `M.send_message`, `M.get_client_info`. +- `config.lua` by its file hash: the `connection_timeout` and `connection_wait_delay` defaults set the deadline. + +A changed file with no changed block or line still needs a look. The `VimLeavePre` autocmd in `M.setup` calls `M.stop`, or `clear_mention_queue()` when no server runs. The record lists that `clear_mention_queue()` line as a site of `M.setup`, and a change to the `M.stop` call shows only as a changed `init.lua`. The record groups lines by file, so two branches that edit different covered files and each re-record merge `covered.lock` without a conflict. Two branches that edit the same file conflict in `covered.lock` once one of them merges. To resolve it, merge `origin/main`, follow "Update after an intended change" on the merged code if it reaches the queue, run `check.sh --record`, and commit `covered.lock` with the merge. A PASS says that 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 read by a regex from the source. `TRUE` means the regex found the guard. `FALSE` means that the model runs without that guard. A `FALSE` you did not expect is either a removed guard (a bug) or a guard reworded past the regex (a modeling error). A change that keeps every fact `TRUE` reads only STALE: for example a broadcast that never reports its writes, a deadline that never comes, an `expire_mentions` that clears nothing, a closing client that counts as connected, a typo that stops `on_open` from scheduling the flush, a `get_client_info` without `handshake_complete`, a `schedule_mention_flush` that stops the deadline while Claude is connected, a refused piece of a large frame that hides its error, or a change of the readiness wait that keeps the `wait > 0` test (`math.max` in place of `math.min` over the clients, or 200 ms taken off the wait). The unit tests in `tests/unit/mention_queue_spec.lua`, `tests/unit/server_spec.lua` and `tests/unit/server/connection_lifecycle_spec.lua` catch those, so run them too. See below for how to tell them apart. + +| Fact | Code it reads | Rule without it | +| ------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `EnqueueArmsDeadline` | `queue_mention` appends the mention with its `deadline`, starts `connection_timer` with `expire_mentions` when none runs, then calls `schedule_mention_flush(debounce_delay)` | `NoStrandedMention` | +| `DeadlineReportsError` | `expire_mentions` calls `logger.error` ("Send timeout" while a Claude is connected, "Connection timeout" otherwise) before it removes the expired mentions | `NoSilentDrop` | +| `DeadlineRearms` | `expire_mentions` calls `clear_mention_queue()` when the queue is empty, and otherwise starts `connection_timer` for `queue[1].deadline` | `NoStrandedMention` | +| `DeadlineSparesReady` | `expire_mentions` returns at once while `ms_until_a_client_is_ready()` is 0: it clears nothing while a ready client is connected | `ReadyDelivers` | +| `SparedQueueFlushes` | in that branch, `expire_mentions` calls `schedule_mention_flush(inter_message_delay)` before it returns, so a flush is due even when the handshake's `on_open` callback has not run yet | `NoStrandedMention` | +| `FlushExpiresOverdue` | `flush_mention_queue` calls `expire_mentions()` when it finds no ready client: in the wait branch, and when no connected client took the frame | `NoStrandedMention` | +| `QueueKeepsDeadline` | `init.lua` stops `connection_timer` only in `clear_mention_queue` and in the empty-queue branch of `schedule_mention_flush`, and starts it only in `queue_mention` and `expire_mentions`: no handshake, flush or send moves a deadline | `NoStrandedMention`, only with `FlushExpiresOverdue` removed too. Alone it breaks no rule here: the next flush that finds no ready client clears the overdue mentions and starts the deadline again, so only the time of the error changes. The tests `A, F4: a Claude whose handshake comes 10.3 s after the send …` and `S: clients that connect every 700 ms and stay 300 ms …` (and `… 650 ms and stay 500 ms …`) in `tests/unit/mention_queue_spec.lua` catch it alone | +| `HandshakeFlushes` | the 101 write callback in `server/client.lua` sets state `connected`, then calls `on_open`. `server/tcp.lua` passes `server.on_open`, `on_open` in `server/init.lua` schedules `process_mention_queue(true)`, and that calls `schedule_mention_flush` | `FlushDelivers` | +| `ConnectedSchedulesFlush` | `schedule_mention_flush` starts `mention_timer` with `flush_mention_queue` while `is_claude_connected()` and no flush is due | `FlushDelivers` | +| `FlushWaitsForReady` | `flush_mention_queue` returns before the broadcast while `ms_until_a_client_is_ready()` is above 0 | `SentWhenReady` | +| `WaitRearmsFlush` | in that branch, `flush_mention_queue` starts `mention_timer` again for the end of the wait | `FlushDelivers` | +| `ReadyNeedsConnected` | `ms_until_a_client_is_ready` counts only a client in state `connected` with `handshake_complete` and `connected_at` | `SentWhenReady` | +| `ReadyFromHandshake` | `ms_until_a_client_is_ready` measures from `info.connected_at`, which only the 101 write callback sets, to the handshake time, and `get_client_info` returns | `SentWhenReady` | +| `FlushSendsHead` | `flush_mention_queue` broadcasts `queue[1]` and removes index 1 | `SentInOrder` | +| `FlushChecksDelivery` | `flush_mention_queue` returns and keeps the head when `server.broadcast` returned false. `server/init.lua` returns whether `broadcast` in `server/tcp.lua` sent to a client, and that counts only clients in state `connected` | `NoSilentDrop` | +| `FlushRemovesHead` | `flush_mention_queue` removes the head after the broadcast, then calls `schedule_mention_flush(inter_message_delay)` | `AtMostOnce` | +| `FailedWriteReported` | the flush passes `report_unwritten("queue", ...)`, which logs an error when no write succeeded. `broadcast` in `server/tcp.lua` counts the writes that succeeded and calls `on_written` once, after the last one | `NoSilentDrop` | +| `RefusedWriteReported` | `send_message` passes the error of a write that libuv refuses at once to the callback: `write` returns nil and that error | `NoSilentDrop` | +| `StopClearsQueue` | `M.stop` calls `M.state.server.stop()`, sets `M.state.server = nil`, then calls `clear_mention_queue()`, which empties the queue and stops both timers | `NothingAfterStop` | + +On `BROKEN`, the script prints the TLC trace as action names. Each action in `model/MentionQueue.tla` names the Lua function it models. The two client slots are `1` and `2`. Read the trace with the pstack `/statechart` skill: + +1. Rerun with `--keep`. +2. Copy the broken run's `.cfg` from the kept dir. Set `Mentions = 1`, `MaxConnects = 1` and `MaxStarts = 0`, then add a mention only if the path needs two (an order break), a connection only if it needs a second client, and a start only if it needs a restart. For a liveness rule, keep the `PROPERTY` line. Stop at the smallest config that still breaks the rule. +3. Give `/statechart` the kept `MentionQueue.tla`, that cfg, and the view `model/statechart-view.ts`. `/statechart` charts invariants. For a liveness rule, read the kept `live-.out` trace instead: it ends in `Stuttering` or `Back to state`, the point after which nothing more happens to the mention. + +The report tells the path in plain words, for example "you send a mention, Claude opens its socket, Claude asks for the WebSocket, the handshake completes, the handshake schedules a flush, Claude's socket goes away, the flush finds no client, a second Claude completes its handshake: the deadline never runs". Then decide which kind of failure it is: + +- **Real bug.** The path is one the code can take. A fact went `FALSE` because the change removed or moved a guard. Replay it on the real code before you report it: copy the closest script in `replays/` and drive the real functions in the path's order. 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 (for example `if info.handshake_complete == true and info.state == "connected" then` reads `FALSE` for `ReadyNeedsConnected`). Fix the regex or the model, run `--mutants`, and say what you changed. + +## Bugs this model found + +The first model of this queue, on the code before #454, broke five of its six rules. Each finding below was replayed on real Neovim, and each is fixed. Its replay under `replays/` now shows the promise kept on the code at the commit in `covered.lock`. + +1. `NoSilentDrop`, expired at the flush (#454 finding A, `replays/expired-at-flush.lua`). You sent while Claude was not connected, and Claude completed its handshake more than about 4.4 s later. The flush then dropped the mention as older than `queue_timeout` (5 s), with no error. Fixed in #454: a mention stays queued until a client took it or its wait ended with an error. #480 set the end of that wait to the deadline, which gives a Claude that completes its handshake within `connection_timeout` its `connection_wait_delay`. The untimed model does not see the deadline length. The `A:` tests in `tests/unit/mention_queue_spec.lua` pin it. +2. `NoSilentDrop`, lost in the wait (#454 finding H, `lost-in-wait.lua`, `lost-in-wait-reconnect.lua`). Claude dropped during the 600 ms wait after its handshake, and the plugin sent the mention to no client and logged success. Fixed in #454. Checked by `FlushChecksDelivery`. +3. `SentInOrder` (#454 finding E, `order.lua`). A send during the wait took the 50 ms debounce path and overtook the mention queued before it. Fixed in #454: one queue, and the flush sends its head. Checked by `FlushSendsHead`. +4. `NothingAfterStop` (#454 finding C, `stop-in-wait.lua`, `restart-leak.lua`). `:ClaudeCodeStop` during the wait raised `attempt to index field 'server' (a nil value)`, and a stop and a start sent the old mention to the new Claude. Fixed in #454. Checked by `StopClearsQueue`. +5. `NoStrandedMention`, the timer never reset (#454 finding B, `timer-never-reset.lua`). `M.state.connection_timer` stayed set after it fired, so a later mention never timed out. Fixed in #454. Checked by `EnqueueArmsDeadline` and `DeadlineRearms`. +6. `NoStrandedMention`, the connected path had no timer (#454 finding S, `drop-in-debounce.lua`). A send while Claude was connected started no timeout, so a drop within the 50 ms debounce left the mention with nothing that sent or dropped it. Fixed in #454. Checked by `EnqueueArmsDeadline`. +7. `NoStrandedMention`, a closing client counted as connected (#454 finding F, `closing-client.lua`). A send in the tick after Claude's CLOSE frame took the connected path and was stranded too. Fixed in #454: `is_claude_connected` needs state `connected`. With a deadline on every mention, a closing client that counts can no longer strand one, so no fact reads this guard. The replay and the `F:` test pin it. +8. `FlushDelivers`, the handshake window (#454 finding D, `handshake-window.lua`). The flush hook ran at the TCP accept, before the WebSocket handshake. A send in between waited for the timeout while Claude was connected. Fixed in #454 with `on_open`. Checked by `HandshakeFlushes`. +9. The path of a queued mention (#454 finding G). A queued mention kept the raw path you gave, while a connected send went through `_format_path_for_at_mention`. The model has no paths. Fixed in #454. The `G:` tests pin it. + +Four more came up in review of #454's fixes and while #480 was built, and this model's second version found one. #480 fixed all five. Items 13 and 14 were in #480's own intermediate commits and never reached main: + +10. A second client's handshakes postponed a flush that was due for a connected Claude (Codex, round 6 on #454). The readiness rule from `connected_at` fixed it. An untimed model cannot see a flush that comes later, so the test `D: handshakes of other clients do not postpone a flush that is due for a connected Claude` pins it. +11. `NoSilentDrop`, a refused write. A write that libuv refused at once never ran its callback, so the broadcast never reported, and the queue dropped the mention with no error. Checked by `RefusedWriteReported`. +12. `NoStrandedMention`, client churn (`churn.lua`). Clients that connected and left without overlap stopped the connection timeout at each handshake, and the mention waited with no error. The deadline per mention fixed it. The model catches a revert of that fix only together with `FlushExpiresOverdue` (see the facts table). The `S:` churn tests and `A, F4: …` in `tests/unit/mention_queue_spec.lua` catch it alone. `churn.lua` does not: each flush that finds no ready client starts the deadline again, so the mention still leaves on time. It catches the code before the deadline per mention (`08dbcae`, `d1a6724`), where no flush did that. +13. `ReadyDelivers`, a drain cut at the deadline (`drain.lua`). On a head of #480 before its drain rule (cefe258), with many mentions queued while Claude started, the first deadline cleared the rest while a ready Claude was taking them, 25 ms apart: with 100 mentions and a handshake 8.6 s after the send, fewer than half arrived, and the count changed with the host's load. `drain.lua` passes only when all 100 arrive, in order, with no error. Now no deadline clears a mention while a ready client is connected. Checked by `DeadlineSparesReady`. +14. `NoStrandedMention`, a spared queue with no flush due. This model found it in #480's drain rule before that reached a pushed head. Neovim runs the handshake's `on_open` callback late when its loop was busy, so the deadline found Claude ready before any flush was due, cleared nothing, and stopped. When that Claude left before `on_open` ran, nothing sent or cleared the queue. The spared deadline now schedules a flush. Checked by `SparedQueueFlushes`, and pinned by the test `F1: a ready Claude that leaves before its handshake callback ran does not strand the queue`. + +## Replays + +```bash +NVIM=nvim .agents/skills/verify-mention-queue/replays/run.sh # every replay, about 2 min +NVIM=nvim .agents/skills/verify-mention-queue/replays/run.sh order stop-in-wait # some of them +``` + +`run.sh` runs each replay in a fresh headless Neovim (`-u NONE -i NONE`, this checkout first on `runtimepath`) with its own `XDG_*_HOME`, `CLAUDE_CONFIG_DIR` and cwd under `OUT` (default: a new `mktemp -d` dir, printed first). `perl` ends a replay that runs past 120 s, so `run.sh` needs no GNU `timeout`. Each replay runs through `:luafile`, not `nvim -l`, so Neovim 0.8 runs them too. It prints one verdict line per replay (`KEPT : ...` or `BROKEN : ...`) and a count line, exits 1 when a replay is `BROKEN`, counts a replay as `KEPT` only when it printed `KEPT` and its Neovim exited 0, and writes each replay's timeline, with what the user sees and any Lua error, to `$OUT/.log`. `replays/lib.lua` plays Claude with real loopback WebSocket clients in the same Neovim. It reads the auth token from plugin state and never prints it. Each replay drives the real functions in the order of its model path, and `vim.wait` pumps the real event loop between steps, so the plugin's own timers and `vim.schedule` callbacks run with the default delays. `closing-client.lua` feeds Claude's CLOSE frame through the real `server/client.lua` `process_data` with the `on_close` that `server/tcp.lua` passes, so that the send lands in the same tick. Six replays wait for a deadline or a long drain, so they take 11 to 22 s each. + +## 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 queue, its timers, the connection or readiness check, the handshake, a broadcast or a stop (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 in `model/MentionQueue.tla` that cites that code. If a guard moved, change its fact regex in `check.sh`. If a new caller queues, flushes or clears mentions, model it as an action or add a fact for its guard. +3. Run `check.sh --mutants`. Every fact must be caught by its rule, and every rule must break at least once. +4. Run `check.sh` and read the result. Run `replays/run.sh` when the change can reach a replay's path. +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 invariants run with 3 mentions, 2 client slots, 2 TCP connects and 1 restart, about 270,000 distinct states. The liveness rules run with 2 mentions: about 58,000 states for `NoStrandedMention` and `ReadyDelivers`, and about 25,000 for `FlushDelivers`. +- Two client slots, so two clients can be connected at once. A broadcast reaches both, and the readiness rule counts both. A third client is not modeled: a bug that needs three clients at once, such as a third client's handshake that postpones a flush, is not caught here. The test `D: handshakes of other clients do not postpone a flush that is due for a connected Claude` connects 11 clients. +- Time is untimed. "`connection_wait_delay` has passed since the accept" and "since the handshake" are steps of each client, and any deadline can pass at any step. So the model does not check the deadline length or a flush that comes late. `tests/unit/mention_queue_spec.lua` checks both, with a fake clock, and the replays check them with real timers. +- A broadcast's writes all succeed, all fail later, or are all refused at once. When one client's write succeeds and another's fails, the code counts a success, and the model does not explore that mix. +- The model uses the default config, with `disable_broadcast_debouncing` off, so every send queues. With it on, a send while Claude is connected and the queue is empty goes out at once and skips the readiness wait. This is a known bug, which a follow-up PR fixes: a Claude whose handshake came less than `connection_wait_delay` ago gets the mention while it starts up. On real Neovim 0.8.0 and 0.12.3, a send right after the handshake reached Claude a few ms after it (3 to 10 in our runs), where the default config waits the full 600 ms. A PASS of `SentWhenReady` does not cover this config. With it on, a send that no client takes shows "Failed to broadcast …" at once. Under busted, `_broadcast_at_mention` broadcasts at once unless a test sets `enable_broadcast_debouncing_in_tests`. +- `start_timer` runs a callback only while its timer is still the one in `M.state`. The model takes that as given: a stop cancels the callbacks that wait for the main loop. If that check broke, a callback whose timer fired, and was then stopped or replaced before the main loop ran the callback, would still run once: it would stop the newer timer and run its flush or deadline check early. Both read the queue, the clients and the deadlines again when they run, so the user would see at most a mention that goes out before its 50 ms debounce or 25 ms gap ends. A verifier removed the check: the unit tests in `tests/unit/mention_queue_spec.lua`, `tests/unit/server_spec.lua` and `tests/unit/server/connection_lifecycle_spec.lua`, and the `stop-in-wait`, `restart-leak`, `lost-in-wait-reconnect` and `drain` replays, still passed. It found no harm. +- The model has no paths. A path that `_format_path_for_at_mention` refuses returns an error at once and is not queued. +- `VimLeavePre` is modeled as a stop. Neovim exits after it, so the steps after it in a path do not run. +- `ClaudeCodeSendComplete`, the terminal, logging other than the queue errors, selection tracking and ping timers are not modeled. `ClaudeCodeSendComplete` fires only for a send made while Claude counts as connected, when the plugin accepts the send and not when Claude gets it. A send made while Claude is not connected never fires it, also when the queue delivers it later. A bug in the others shows outside the queue: the terminal does not open or take focus, a selection reaches Claude wrong, or a ping timer drops a Claude that still works, which the model sees as one more drop. +- 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. diff --git a/.agents/skills/verify-mention-queue/check.sh b/.agents/skills/verify-mention-queue/check.sh new file mode 100755 index 000000000..3ba251403 --- /dev/null +++ b/.agents/skills/verify-mention-queue/check.sh @@ -0,0 +1,182 @@ +#!/usr/bin/env bash +# shellcheck disable=SC2329,SC2034,SC2154 # helpers run through as_bool; covered_block sets blocks by name +# Model-check the @ mention queue and the clients it sends to against facts read from the code. +# Usage: check.sh [--mutants] [--keep] [--record] | check.sh --hash-only +# exit 0 pass, 1 rule broken, 2 tool or script error, 3 stale (the covered code +# changed since the model was last confirmed against it: unverified) +here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +SKILL=verify-mention-queue MODEL=MentionQueue +source "$here/../../../scripts/tla/check-lib.sh" +tla_init "$@" + +MAIN=lua/claudecode/init.lua +CONFIG=lua/claudecode/config.lua +SERVER=lua/claudecode/server/init.lua +TCP=lua/claudecode/server/tcp.lua +CLIENT=lua/claudecode/server/client.lua +COVERED=("$MAIN" "$CONFIG" "$SERVER" "$TCP" "$CLIENT") +SITE_RE='(mention_queue|mention_timer|connection_timer|queue_mention|expire_mentions|schedule_mention_flush|flush_mention_queue|process_mention_queue|ms_until_a_client_is_ready|report_unwritten|is_claude_connected|connected_at|handshake_complete|connection_timeout|connection_wait_delay|at_mentioned|on_open|on_written)' + +covered_block is_connected "$MAIN" '^function M\.is_claude_connected\(' +covered_block until_ready "$MAIN" '^local function ms_until_a_client_is_ready\(' +covered_block start_timer "$MAIN" '^local function start_timer\(' +covered_block clear_queue "$MAIN" '^local function clear_mention_queue\(' +covered_block expire "$MAIN" '^local function expire_mentions\(' +covered_block unwritten "$MAIN" '^local function report_unwritten\(' +covered_block flush "$MAIN" '^local function flush_mention_queue\(' +covered_block schedule "$MAIN" '^schedule_mention_flush = function\(' +covered_block queue_mention "$MAIN" '^local function queue_mention\(' +covered_block process_queue "$MAIN" '^function M\.process_mention_queue\(' +covered_block send_at_mention "$MAIN" '^function M\.send_at_mention\(' +covered_block broadcast_mention "$MAIN" '^function M\._broadcast_at_mention\(' +covered_block main_stop "$MAIN" '^function M\.stop\(\)' +covered_block on_open "$SERVER" '^ *on_open = function\(client\)' +covered_block server_broadcast "$SERVER" '^function M\.broadcast\(' +covered_block server_status "$SERVER" '^function M\.get_status\(' +covered_block new_connection "$TCP" '^function M\._handle_new_connection\(' +covered_block tcp_broadcast "$TCP" '^function M\.broadcast\(' +covered_block clients_info "$TCP" '^function M\.get_clients_info\(' +covered_block write "$CLIENT" '^local function write\(' +covered_block process_data "$CLIENT" '^function M\.process_data\(' +covered_block send_message "$CLIENT" '^function M\.send_message\(' +covered_block client_info "$CLIENT" '^function M\.get_client_info\(' + +FACTS=(EnqueueArmsDeadline DeadlineReportsError DeadlineRearms DeadlineSparesReady SparedQueueFlushes FlushExpiresOverdue + QueueKeepsDeadline HandshakeFlushes ConnectedSchedulesFlush FlushWaitsForReady WaitRearmsFlush ReadyNeedsConnected + ReadyFromHandshake FlushSendsHead FlushChecksDelivery FlushRemovesHead FailedWriteReported RefusedWriteReported + StopClearsQueue) + +# queue_mention appends the mention, starts connection_timer for its deadline when none runs, then schedules a flush. +fact[EnqueueArmsDeadline]=$(as_bool in_order '^ *table\.insert\(queue, \{.*deadline = deadline' \ + '^ *if not M\.state\.connection_timer then$' '^ *start_timer\("connection_timer", [a-z_]+, expire_mentions\)$' \ + '^ *schedule_mention_flush\(debounce_delay\)$' <<<"$queue_mention") +fact[DeadlineReportsError]=$(as_bool in_order '^ *if expired > 0 then$' '^ *if M\.is_claude_connected\(\) then$' \ + '^ *logger\.error\($' '"Send timeout - clearing "' '^ *else$' \ + '^ *logger\.error\("queue", "Connection timeout - clearing "' '^ *table\.remove\(queue, 1\)$' <<<"$expire") +fact[DeadlineRearms]=$(as_bool in_order '^ *if #queue == 0 then$' '^ *clear_mention_queue\(\)$' '^ *else$' \ + '^ *start_timer\("connection_timer", queue\[1\]\.deadline - now, expire_mentions\)$' <<<"$expire") +# While a ready client is connected, the deadline clears nothing: the queue drains to that client. +fact[DeadlineSparesReady]=$(as_bool in_order '^ *if ms_until_a_client_is_ready\(\) == 0 then$' '^ *return$' '^ *end$' \ + '^ *local queue = mention_queue\(\)$' <<<"$expire") +# The spared queue keeps a flush due: the handshake's own flush can come later. +fact[SparedQueueFlushes]=$(as_bool in_order '^ *if ms_until_a_client_is_ready\(\) == 0 then$' \ + '^ *schedule_mention_flush\(inter_message_delay\)$' '^ *return$' <<<"$expire") +# A flush that finds no ready client clears the mentions whose deadline passed while a ready client took the queue. +flush_expires_overdue() { + in_order '^ *if wait and wait > 0 then$' '^ *expire_mentions\(\)$' '^ *if #mention_queue\(\) > 0 then$' \ + '^ *start_timer\("mention_timer", wait, flush_mention_queue\)$' <<<"$flush" && + in_order 'No connected client took queued @ mention' '^ *expire_mentions\(\)$' '^ *return$' <<<"$flush" +} +fact[FlushExpiresOverdue]=$(as_bool flush_expires_overdue) +# Only an empty queue stops the deadline: no handshake, flush or send does. start_timer stops a timer of the same name +# too, so the starts count as well. +queue_keeps_deadline() { + [[ $(grep -c 'stop_timer("connection_timer")' "$MAIN") == 2 ]] && + [[ $(grep -c 'start_timer("connection_timer"' "$MAIN") == 2 ]] && + in_order 'stop_timer\("connection_timer"\)' <<<"$clear_queue" && + in_order '^ *if #mention_queue\(\) == 0 then$' 'stop_timer\("connection_timer"\)' '^ *elseif ' <<<"$schedule" +} +fact[QueueKeepsDeadline]=$(as_bool queue_keeps_deadline) +# The 101 write callback marks the client connected, then calls on_open. server/tcp.lua passes the server's on_open, +# server/init.lua schedules process_mention_queue(true), and that schedules a flush. +handshake_flushes() { + in_order 'write\(client, response_from_handshake, function\(err\)$' '^ *client\.state = "connected"$' \ + '^ *on_open\(client\)$' <<<"$process_data" && + grep -q 'server\.auth_token, server\.on_open)' <<<"$new_connection" && + in_order 'vim\.schedule\(function\(\)$' 'main_module\.process_mention_queue\(true\)' <<<"$on_open" && + in_order '^ *if from_new_connection then$' '^ *schedule_mention_flush\(M\.state\.config\.connection_wait_delay\)$' \ + <<<"$process_queue" +} +fact[HandshakeFlushes]=$(as_bool handshake_flushes) +fact[ConnectedSchedulesFlush]=$(as_bool in_order \ + '^ *elseif M\.is_claude_connected\(\) and not M\.state\.mention_timer then$' \ + '^ *start_timer\("mention_timer", delay, flush_mention_queue\)$' <<<"$schedule") +fact[FlushWaitsForReady]=$(as_bool in_order '^ *local wait = ms_until_a_client_is_ready\(\)$' \ + '^ *if wait and wait > 0 then$' '^ *return$' '^ *end$' 'server\.broadcast\("at_mentioned"' <<<"$flush") +fact[WaitRearmsFlush]=$(as_bool in_order '^ *if wait and wait > 0 then$' \ + '^ *start_timer\("mention_timer", wait, flush_mention_queue\)$' '^ *return$' <<<"$flush") +fact[ReadyNeedsConnected]=$(as_bool in_order '^ *for _, info in ipairs\(' \ + '^ *if info\.state == "connected" and info\.handshake_complete == true and info\.connected_at then$' \ + '^ *local left = ' <<<"$until_ready") +# connected_at is the time of the handshake: the 101 write callback sets it, and nothing else does. +ready_from_handshake() { + grep -qE '^ *local left = math\.max\(0, info\.connected_at \+ M\.state\.config\.connection_wait_delay - vim\.loop\.now\(\)\)$' \ + <<<"$until_ready" && + in_order 'write\(client, response_from_handshake, function\(err\)$' '^ *client\.handshake_complete = true$' \ + '^ *client\.connected_at = vim\.loop\.now\(\)$' '^ *on_open\(client\)$' <<<"$process_data" && + grep -qE '^ *connected_at = client\.connected_at,$' <<<"$client_info" && + [[ $(grep -rE 'connected_at *= *[^=]' lua plugin | grep -cvE 'connected_at = client\.connected_at,$') == 1 ]] +} +fact[ReadyFromHandshake]=$(as_bool ready_from_handshake) +fact[FlushSendsHead]=$(as_bool in_order '^ *local mention = queue\[1\]$' 'server\.broadcast\("at_mentioned"' \ + '^ *table\.remove\(queue, 1\)$' <<<"$flush") +# A flush keeps the head when the broadcast reached no client: server/init.lua returns the count of tcp.lua's +# broadcast, which counts only "connected" clients. +flush_checks_delivery() { + in_order '^ *if not server\.broadcast\("at_mentioned", params, ' '^ *return$' '^ *end$' \ + '^ *table\.remove\(queue, 1\)$' <<<"$flush" && + grep -q 'return tcp_server\.broadcast(M\.state\.server, json_message, on_written) > 0' <<<"$server_broadcast" && + in_order '^ *if client\.state == "connected" then$' '^ *sent = sent \+ 1$' '^ *return sent$' <<<"$tcp_broadcast" +} +fact[FlushChecksDelivery]=$(as_bool flush_checks_delivery) +fact[FlushRemovesHead]=$(as_bool in_order 'server\.broadcast\("at_mentioned"' '^ *table\.remove\(queue, 1\)$' \ + '^ *schedule_mention_flush\(inter_message_delay\)$' <<<"$flush") +# A broadcast whose writes all failed shows an error: tcp.lua counts the writes and calls on_written once after the +# last one, and the flush passes report_unwritten, which logs an error when none succeeded. +failed_write_reported() { + grep -q 'report_unwritten("queue", mention\.file_path)' <<<"$flush" && + in_order '^ *if written == 0 then$' '^ *logger\.error\(component, ' <<<"$unwritten" && + in_order 'if dispatched and not reported and pending == 0 and sent > 0 then$' 'on_written\(written\)' \ + '^ *pending = pending \+ 1$' 'client_manager\.send_message\(client, message, function\(err\)$' \ + '^ *if not err then$' '^ *written = written \+ 1$' '^ *finish\(\)$' '^ *dispatched = true$' '^ *finish\(\)$' \ + <<<"$tcp_broadcast" +} +fact[FailedWriteReported]=$(as_bool failed_write_reported) +# libuv returns nil and the error for a write it refuses at once, and never runs that write's callback. +refused_write_reported() { + in_order '^ *local queued, err = write\(client, text_frame, callback\)$' '^ *if not queued and err and callback then$' \ + '^ *callback\(err\)$' <<<"$send_message" && + in_order '^ *return client\.tcp_handle:write\(data, callback\)$' '^ *return queued, err$' <<<"$write" +} +fact[RefusedWriteReported]=$(as_bool refused_write_reported) +stop_clears_queue() { + in_order 'M\.state\.server\.stop\(\)' '^ *M\.state\.server = nil$' '^ *clear_mention_queue\(\)$' <<<"$main_stop" && + in_order '^ *M\.state\.mention_queue = \{\}$' '^ *stop_timer\("mention_timer"\)$' \ + '^ *stop_timer\("connection_timer"\)$' <<<"$clear_queue" +} +fact[StopClearsQueue]=$(as_bool stop_clears_queue) + +RULES=(NoSilentDrop SentInOrder AtMostOnce SentWhenReady NothingAfterStop) +LIVE=(NoStrandedMention ReadyDelivers FlushDelivers) +EXPECT=( + [EnqueueArmsDeadline]=NoStrandedMention + [DeadlineReportsError]=NoSilentDrop + [DeadlineRearms]=NoStrandedMention + [DeadlineSparesReady]=ReadyDelivers + [SparedQueueFlushes]=NoStrandedMention + [FlushExpiresOverdue]=NoStrandedMention + ["QueueKeepsDeadline+FlushExpiresOverdue"]=NoStrandedMention + [HandshakeFlushes]=FlushDelivers + [ConnectedSchedulesFlush]=FlushDelivers + [FlushWaitsForReady]=SentWhenReady + [WaitRearmsFlush]=FlushDelivers + [ReadyNeedsConnected]=SentWhenReady + [ReadyFromHandshake]=SentWhenReady + [FlushSendsHead]=SentInOrder + [FlushChecksDelivery]=NoSilentDrop + [FlushRemovesHead]=AtMostOnce + [FailedWriteReported]=NoSilentDrop + [RefusedWriteReported]=NoSilentDrop + [StopClearsQueue]=NothingAfterStop +) +# Invariants run with 3 mentions, liveness with 2. FlushDelivers runs with no deadline that passes: in this untimed +# model a deadline can pass at any step, and a spared deadline schedules a flush, so it would hide a flush path that +# leaves a ready Claude waiting for the deadline. +tla_constants() { + if [[ $2 == live ]]; then echo " Mentions = 2"; else echo " Mentions = 3"; fi + echo " MaxConnects = 2" + echo " MaxStarts = 1" + if [[ $1 == *FlushDelivers ]]; then echo " DeadlinesFire = FALSE"; else echo " DeadlinesFire = TRUE"; fi +} +CONSTRAINT=RecvBound +tla_main diff --git a/.agents/skills/verify-mention-queue/covered.lock b/.agents/skills/verify-mention-queue/covered.lock new file mode 100644 index 000000000..5ab4c37c5 --- /dev/null +++ b/.agents/skills/verify-mention-queue/covered.lock @@ -0,0 +1,121 @@ +== lua/claudecode/config.lua +file lua/claudecode/config.lua 3afb1bdeff27bfb6 +site lua/claudecode/config.lua: "connection_timeout must be a positive number" @ function M.validate(config) +site lua/claudecode/config.lua: "connection_wait_delay must be a non-negative number" @ function M.validate(config) +site lua/claudecode/config.lua: connection_timeout = 10000, @ M.defaults = { +site lua/claudecode/config.lua: connection_wait_delay = 600, -- Milliseconds to wait after connection before sending queued @ mentions @ M.defaults = { +site lua/claudecode/config.lua: queue_timeout = 5000, -- Unused, kept so that configs that set it stay valid (see connection_timeout) @ M.defaults = { +site lua/claudecode/config.lua: type(config.connection_timeout) == "number" and config.connection_timeout > 0, @ function M.validate(config) +site lua/claudecode/config.lua: type(config.connection_wait_delay) == "number" and config.connection_wait_delay >= 0, @ function M.validate(config) +== lua/claudecode/init.lua +file lua/claudecode/init.lua fc28de832b4056df +block is_connected 21c035c32b5cee13 +block until_ready cd0663523297ab20 +block start_timer 067cb9333a8fbff9 +block clear_queue 4312e85f7da39bbd +block expire 1b7f50cc49d9a9d3 +block unwritten 6d6b0cfe1d094994 +block flush 33c98740183b82fd +block schedule d927c59c32177eac +block queue_mention 22183b749ca8f79a +block process_queue 816e89295bbfc620 +block send_at_mention 508de16084cc702a +block broadcast_mention f270a13f4fab1104 +block main_stop d754def6d5865650 +site lua/claudecode/init.lua: M.state.mention_queue = M.state.mention_queue or {} @ local function mention_queue() +site lua/claudecode/init.lua: M.state.mention_queue = {} @ local function clear_mention_queue() +site lua/claudecode/init.lua: M.state.server.broadcast("at_mentioned", params, report_unwritten("command", formatted_path)) @ function M._broadcast_at_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: clear_mention_queue() @ function M.setup(opts) +site lua/claudecode/init.lua: clear_mention_queue() @ function M.stop() +site lua/claudecode/init.lua: clear_mention_queue() @ local function expire_mentions() +site lua/claudecode/init.lua: connection_timer = nil, @ M.state = { +site lua/claudecode/init.lua: elseif M.is_claude_connected() and not M.state.mention_timer then @ schedule_mention_flush = function(delay) +site lua/claudecode/init.lua: expire_mentions() @ local function flush_mention_queue() +site lua/claudecode/init.lua: expire_mentions() @ local function flush_mention_queue() +site lua/claudecode/init.lua: flush_mention_queue() @ function M.process_mention_queue(from_new_connection) +site lua/claudecode/init.lua: function M.is_claude_connected() @ function M.is_claude_connected() +site lua/claudecode/init.lua: function M.process_mention_queue(from_new_connection) @ function M.process_mention_queue(from_new_connection) +site lua/claudecode/init.lua: if #mention_queue() == 0 then @ schedule_mention_flush = function(delay) +site lua/claudecode/init.lua: if #mention_queue() > 0 then @ local function flush_mention_queue() +site lua/claudecode/init.lua: if M.is_claude_connected() then @ function M.send_at_mention(file_path, start_line, end_line, context) +site lua/claudecode/init.lua: if M.is_claude_connected() then @ local function expire_mentions() +site lua/claudecode/init.lua: if immediate and #mention_queue() == 0 then @ function M._broadcast_at_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: if info.state == "connected" and info.handshake_complete == true and info.connected_at then @ local function ms_until_a_client_is_ready() +site lua/claudecode/init.lua: if info.state == "connected" and info.handshake_complete == true then @ function M.is_claude_connected() +site lua/claudecode/init.lua: if ms_until_a_client_is_ready() == 0 then @ local function expire_mentions() +site lua/claudecode/init.lua: if not M.is_claude_connected() then @ function M._ensure_terminal_visible_if_connected() +site lua/claudecode/init.lua: if not M.state.connection_timer then @ local function queue_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: if not server.broadcast("at_mentioned", params, report_unwritten("queue", mention.file_path)) then @ local function flush_mention_queue() +site lua/claudecode/init.lua: local function clear_mention_queue() @ local function clear_mention_queue() +site lua/claudecode/init.lua: local function expire_mentions() @ local function expire_mentions() +site lua/claudecode/init.lua: local function flush_mention_queue() @ local function flush_mention_queue() +site lua/claudecode/init.lua: local function mention_queue() @ local function mention_queue() +site lua/claudecode/init.lua: local function ms_until_a_client_is_ready() @ local function ms_until_a_client_is_ready() +site lua/claudecode/init.lua: local function queue_mention(file_path, start_line, end_line) @ local function queue_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: local function report_unwritten(component, file_path) @ local function report_unwritten(component, file_path) +site lua/claudecode/init.lua: local left = math.max(0, info.connected_at + M.state.config.connection_wait_delay - vim.loop.now()) @ local function ms_until_a_client_is_ready() +site lua/claudecode/init.lua: local queue = mention_queue() @ local function clear_mention_queue() +site lua/claudecode/init.lua: local queue = mention_queue() @ local function expire_mentions() +site lua/claudecode/init.lua: local queue = mention_queue() @ local function flush_mention_queue() +site lua/claudecode/init.lua: local queue = mention_queue() @ local function queue_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: local schedule_mention_flush @ local schedule_mention_flush +site lua/claudecode/init.lua: local timeout = M.state.config.connection_timeout + M.state.config.connection_wait_delay @ local function queue_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: local wait = ms_until_a_client_is_ready() @ local function flush_mention_queue() +site lua/claudecode/init.lua: mention_queue = {}, @ M.state = { +site lua/claudecode/init.lua: mention_timer = nil, @ M.state = { +site lua/claudecode/init.lua: queue_mention(formatted_path, start_line, end_line) @ function M._broadcast_at_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: queue_mention(mention.file_path, mention.start_line, mention.end_line) @ function M.send_at_mention(file_path, start_line, end_line, context) +site lua/claudecode/init.lua: return M.state.mention_queue @ local function mention_queue() +site lua/claudecode/init.lua: schedule_mention_flush = function(delay) @ schedule_mention_flush = function(delay) +site lua/claudecode/init.lua: schedule_mention_flush(M.state.config.connection_wait_delay) @ function M.process_mention_queue(from_new_connection) +site lua/claudecode/init.lua: schedule_mention_flush(debounce_delay) @ local function flush_mention_queue() +site lua/claudecode/init.lua: schedule_mention_flush(debounce_delay) @ local function queue_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: schedule_mention_flush(inter_message_delay) @ local function expire_mentions() +site lua/claudecode/init.lua: schedule_mention_flush(inter_message_delay) @ local function flush_mention_queue() +site lua/claudecode/init.lua: start_timer("connection_timer", queue[1].deadline - now, expire_mentions) @ local function expire_mentions() +site lua/claudecode/init.lua: start_timer("connection_timer", timeout, expire_mentions) @ local function queue_mention(file_path, start_line, end_line) +site lua/claudecode/init.lua: start_timer("mention_timer", delay, flush_mention_queue) @ schedule_mention_flush = function(delay) +site lua/claudecode/init.lua: start_timer("mention_timer", wait, flush_mention_queue) @ local function flush_mention_queue() +site lua/claudecode/init.lua: stop_timer("connection_timer") @ local function clear_mention_queue() +site lua/claudecode/init.lua: stop_timer("connection_timer") @ schedule_mention_flush = function(delay) +site lua/claudecode/init.lua: stop_timer("mention_timer") @ local function clear_mention_queue() +site lua/claudecode/init.lua: stop_timer("mention_timer") @ schedule_mention_flush = function(delay) +== lua/claudecode/server/client.lua +file lua/claudecode/server/client.lua b8165df16f194471 +block write e4716d226ccc2499 +block process_data 309347512099d250 +block send_message 4224f2da335cf996 +block client_info f173ff23b4707508 +site lua/claudecode/server/client.lua: M.process_data(client, "", on_message, on_close, on_error, auth_token, on_open) @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: client.connected_at = vim.loop.now() @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: client.handshake_complete = true @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: connected_at = client.connected_at, @ function M.get_client_info(client) +site lua/claudecode/server/client.lua: function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: handshake_complete = client.handshake_complete, @ function M.get_client_info(client) +site lua/claudecode/server/client.lua: handshake_complete = false, @ function M.create_client(tcp_handle, keepalive_timeout) +site lua/claudecode/server/client.lua: if client.handshake_complete or client.state == "upgrading" then @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: if not client.handshake_complete then @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: if on_open then @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: on_open(client) @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +== lua/claudecode/server/init.lua +file lua/claudecode/server/init.lua 8da8851fff781946 +block on_open 605dc737a2bfdad0 +block server_broadcast fc69234ae8ed7cf0 +block server_status e2759841ce0f1b90 +site lua/claudecode/server/init.lua: function M.broadcast(method, params, on_written) @ function M.broadcast(method, params, on_written) +site lua/claudecode/server/init.lua: if diff and client.handshake_complete then @ function M.start(config, auth_token) +site lua/claudecode/server/init.lua: if main_module.process_mention_queue then @ function M.start(config, auth_token) +site lua/claudecode/server/init.lua: main_module.process_mention_queue(true) @ function M.start(config, auth_token) +site lua/claudecode/server/init.lua: on_open = function(client) @ function M.start(config, auth_token) +site lua/claudecode/server/init.lua: return tcp_server.broadcast(M.state.server, json_message, on_written) > 0 @ function M.broadcast(method, params, on_written) +== lua/claudecode/server/tcp.lua +file lua/claudecode/server/tcp.lua 8be1dd96671223ea +block new_connection e1daff4237326df4 +block tcp_broadcast 2b207928d69c9dbd +block clients_info b2d757e5dc9d2c2f +site lua/claudecode/server/tcp.lua: end, server.auth_token, server.on_open) @ function M._handle_new_connection(server) +site lua/claudecode/server/tcp.lua: function M.broadcast(server, message, on_written) @ function M.broadcast(server, message, on_written) +site lua/claudecode/server/tcp.lua: if on_written then @ function M.broadcast(server, message, on_written) +site lua/claudecode/server/tcp.lua: if on_written then @ function M.broadcast(server, message, on_written) +site lua/claudecode/server/tcp.lua: on_open = callbacks.on_open or function() end, @ function M.create_server(config, callbacks, auth_token) +site lua/claudecode/server/tcp.lua: on_written(written) @ function M.broadcast(server, message, on_written) diff --git a/.agents/skills/verify-mention-queue/model/MentionQueue.tla b/.agents/skills/verify-mention-queue/model/MentionQueue.tla new file mode 100644 index 000000000..472350354 --- /dev/null +++ b/.agents/skills/verify-mention-queue/model/MentionQueue.tla @@ -0,0 +1,397 @@ +---------------------------- MODULE MentionQueue ---------------------------- +(***************************************************************************) +(* The @ mention queue of claudecode.nvim and the WebSocket clients it *) +(* sends to (lua/claudecode/init.lua and lua/claudecode/server/). *) +(* *) +(* A send that does not go out at once waits in one queue, oldest first. *) +(* Two timers move it on. M.state.mention_timer is the next flush: a flush *) +(* sends only the head, only once some connected client has been connected *) +(* for connection_wait_delay ms, and the head leaves the queue only when a *) +(* connected client took the frame. M.state.connection_timer fires at the *) +(* deadline of the oldest mention, connection_timeout + *) +(* connection_wait_delay ms after its send, and clears every mention whose *) +(* deadline passed with an error, unless a ready client is connected: then *) +(* the queue drains to it, and a flush that finds no ready client clears *) +(* the overdue mentions. A timer's callback runs on the main loop and does *) +(* nothing once its timer was stopped or replaced. *) +(* *) +(* One action is one indivisible step of Neovim's main loop. Timers are *) +(* untimed: any pending timer can fire before any other, and the deadline *) +(* of any queued mention can pass at any step. Two client slots model the *) +(* broadcast to every connected client. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + Mentions, MaxConnects, MaxStarts, + DeadlinesFire, \* model switch: FALSE only for FlushDelivers, where no deadline passes + \* Code facts. TRUE is the code as written. + EnqueueArmsDeadline, \* init.lua queue_mention starts connection_timer when none runs + DeadlineReportsError, \* init.lua expire_mentions calls logger.error before it removes the expired mentions + DeadlineRearms, \* init.lua expire_mentions starts connection_timer again for the oldest mention left + DeadlineSparesReady, \* init.lua expire_mentions clears nothing while a ready client is connected + SparedQueueFlushes, \* init.lua expire_mentions then calls schedule_mention_flush, so a flush is due + FlushExpiresOverdue, \* init.lua flush_mention_queue calls expire_mentions when it finds no ready client + QueueKeepsDeadline, \* init.lua schedule_mention_flush stops connection_timer only when the queue is empty + HandshakeFlushes, \* client.lua calls on_open after the 101 write; server/init.lua schedules process_mention_queue(true) + ConnectedSchedulesFlush, \* init.lua schedule_mention_flush starts mention_timer while Claude is connected + FlushWaitsForReady, \* init.lua flush_mention_queue sends nothing while no connected client is ready + WaitRearmsFlush, \* init.lua flush_mention_queue starts mention_timer again for the end of that wait + ReadyNeedsConnected, \* init.lua ms_until_a_client_is_ready counts only clients in state "connected" + ReadyFromHandshake, \* client.lua sets connected_at when the handshake completes + FlushSendsHead, \* init.lua flush_mention_queue broadcasts the oldest mention, queue[1] + FlushChecksDelivery, \* init.lua flush_mention_queue keeps the head when no connected client took the frame + FlushRemovesHead, \* init.lua flush_mention_queue removes the head once a client took it + FailedWriteReported, \* a broadcast whose writes all failed shows an error (report_unwritten, tcp.lua broadcast) + RefusedWriteReported, \* client.lua send_message passes the error of a write that libuv refuses at once to its callback + StopClearsQueue \* init.lua M.stop calls clear_mention_queue (empties the queue, stops both timers) + +M == 1..Mentions +C == 1..2 + +VARIABLES + sent, queue, outcome, stopped, + recv, \* [C -> Seq(M)]: the mentions each client's Claude received, in order + cstate, \* [C -> client state]: "none", "connecting", "upgrading", "connected", "closing" + age, \* [C -> ...]: "fresh"; "accept" once connection_wait_delay has passed since the TCP accept; + \* "handshake" once it has passed since the handshake too + serverUp, connects, starts, + flushTimer, \* M.state.mention_timer: "nil", "running", or "fired" (its callback waits for the main loop) + dlTimer, \* M.state.connection_timer, the deadline timer: "nil", "running", or "fired" + dlFor, \* the mention whose deadline dlTimer was started for, 0 for none + openRuns, \* process_mention_queue(true) runs that on_open scheduled (a stop does not cancel them) + early, \* a mention went out while no connected client had been connected for connection_wait_delay + luaError, leaked + +vars == <> + +InSeq(m, s) == \E i \in 1..Len(s) : s[i] = m +Pending(m) == InSeq(m, queue) +Received(m) == \E c \in C : InSeq(m, recv[c]) + +(* init.lua M.is_claude_connected: a client in state "connected". *) +Connected == serverUp /\ \E c \in C : cstate[c] = "connected" + +(* init.lua ms_until_a_client_is_ready: the clients it counts, and the ones that are ready by its reading. *) +Counted(c) == IF ReadyNeedsConnected THEN cstate[c] = "connected" ELSE cstate[c] \in {"connected", "closing"} +CodeReady(c) == Counted(c) /\ IF ReadyFromHandshake THEN age[c] = "handshake" ELSE age[c] \in {"accept", "handshake"} +WaitForReady == (\E c \in C : Counted(c)) /\ ~\E c \in C : CodeReady(c) +TrulyReady == \E c \in C : cstate[c] = "connected" /\ age[c] = "handshake" +AnyCodeReady == \E c \in C : CodeReady(c) + +(* server/tcp.lua broadcast: the clients that take the frame. *) +Takers == {c \in C : cstate[c] = "connected"} + +(* init.lua schedule_mention_flush(delay) with queue q and the timers ft (mention_timer) and dt (connection_timer, *) +(* started for df): the new <>. An empty queue stops both timers. *) +Schedule(q, ft, dt, df) == + IF q = <<>> THEN <<"nil", "nil", 0>> + ELSE <> + +TypeOK == + /\ sent \in [M -> BOOLEAN] + /\ queue \in Seq(M) + /\ outcome \in [M -> {"none", "refused", "delivered", "failed", "lost", "errored", "silent", "cleared"}] + /\ stopped \in [M -> BOOLEAN] + /\ recv \in [C -> Seq(M)] + /\ cstate \in [C -> {"none", "connecting", "upgrading", "connected", "closing"}] + /\ age \in [C -> {"fresh", "accept", "handshake"}] + /\ serverUp \in BOOLEAN + /\ connects \in 0..MaxConnects + /\ starts \in 0..MaxStarts + /\ flushTimer \in {"nil", "running", "fired"} + /\ dlTimer \in {"nil", "running", "fired"} + /\ dlFor \in 0..Mentions + /\ openRuns \in 0..MaxConnects + /\ early \in BOOLEAN + /\ luaError \in BOOLEAN + /\ leaked \in BOOLEAN + +Init == + /\ sent = [m \in M |-> FALSE] + /\ queue = <<>> + /\ outcome = [m \in M |-> "none"] + /\ stopped = [m \in M |-> FALSE] + /\ recv = [c \in C |-> <<>>] + /\ cstate = [c \in C |-> "none"] + /\ age = [c \in C |-> "fresh"] + /\ serverUp = TRUE + /\ connects = 0 + /\ starts = 0 + /\ flushTimer = "nil" + /\ dlTimer = "nil" + /\ dlFor = 0 + /\ openRuns = 0 + /\ early = FALSE + /\ luaError = FALSE + /\ leaked = FALSE + +(* init.lua expire_mentions while no client is ready: the k oldest mentions, whose deadline passed, leave with one *) +(* logger.error. The mention connection_timer was started for is the head if it still waits, and its deadline *) +(* passed when the timer fired (from DeadlineRuns, atLeastOne), and any later deadline may have passed too. An empty *) +(* queue stops both timers, otherwise connection_timer runs again for the new head. *) +Expire(k, ft) == + /\ k = 0 \/ DeadlinesFire + /\ LET rest == SubSeq(queue, k + 1, Len(queue)) + IN /\ queue' = rest + /\ outcome' = [m \in M |-> IF \E i \in 1..k : queue[i] = m + THEN IF DeadlineReportsError THEN "errored" ELSE "silent" + ELSE outcome[m]] + /\ IF rest = <<>> + THEN /\ flushTimer' = "nil" + /\ dlTimer' = "nil" + /\ dlFor' = 0 + ELSE /\ flushTimer' = ft + /\ dlTimer' = IF DeadlineRearms THEN "running" ELSE "nil" + /\ dlFor' = IF DeadlineRearms THEN Head(rest) ELSE 0 + +----------------------------------------------------------------------------- +(* You *) + +(* init.lua M.send_at_mention: no server, an error. Otherwise *) +(* queue_mention appends the mention with its deadline, starts *) +(* connection_timer for it when none runs, then schedule_mention_flush. *) +(* This is the default config only. With disable_broadcast_debouncing *) +(* set, _broadcast_at_mention broadcasts at once while the queue is empty *) +(* and checks no readiness, so a Claude whose handshake just completed *) +(* gets the mention early: a known bug, which a follow-up PR fixes. That *) +(* path is not modeled, and a PASS of SentWhenReady does not cover it *) +(* (SKILL.md, "Scope and bounds"). *) +YouSend == + \E m \in M : + /\ ~sent[m] + /\ \A k \in M : k < m => sent[k] + /\ sent' = [sent EXCEPT ![m] = TRUE] + /\ IF ~serverUp + THEN /\ outcome' = [outcome EXCEPT ![m] = "refused"] + /\ UNCHANGED <> + ELSE LET q == Append(queue, m) + arm == EnqueueArmsDeadline /\ dlTimer = "nil" + t == Schedule(q, flushTimer, IF arm THEN "running" ELSE dlTimer, IF arm THEN m ELSE dlFor) + IN /\ queue' = q + /\ flushTimer' = t[1] + /\ dlTimer' = t[2] + /\ dlFor' = t[3] + /\ UNCHANGED outcome + /\ UNCHANGED <> + +(* init.lua M.stop: the server closes every client, M.state.server = nil, *) +(* and clear_mention_queue empties the queue and stops both timers. *) +YouStop == + /\ serverUp + /\ serverUp' = FALSE + /\ cstate' = [c \in C |-> "none"] + /\ stopped' = [m \in M |-> stopped[m] \/ Pending(m)] + /\ IF StopClearsQueue + THEN /\ queue' = <<>> + /\ outcome' = [m \in M |-> IF Pending(m) THEN "cleared" ELSE outcome[m]] + /\ flushTimer' = "nil" + /\ dlTimer' = "nil" + /\ dlFor' = 0 + ELSE UNCHANGED <> + /\ UNCHANGED <> + +YouStart == + /\ ~serverUp + /\ starts < MaxStarts + /\ serverUp' = TRUE + /\ starts' = starts + 1 + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Claude: each client slot *) + +ClientOnly == UNCHANGED <> + +(* server/tcp.lua _handle_new_connection: a new TCP client. *) +ClaudeConnects(c) == + /\ serverUp /\ cstate[c] = "none" /\ connects < MaxConnects + /\ cstate' = [cstate EXCEPT ![c] = "connecting"] + /\ age' = [age EXCEPT ![c] = "fresh"] + /\ connects' = connects + 1 + /\ UNCHANGED <> + +ClaudeUpgrades(c) == + /\ cstate[c] = "connecting" + /\ cstate' = [cstate EXCEPT ![c] = "upgrading"] + /\ UNCHANGED age + /\ ClientOnly + +(* server/client.lua, the 101 write callback: handshake_complete, state *) +(* "connected", connected_at, then on_open, which schedules *) +(* process_mention_queue(true). *) +HandshakeWritten(c) == + /\ cstate[c] = "upgrading" + /\ cstate' = [cstate EXCEPT ![c] = "connected"] + /\ openRuns' = IF HandshakeFlushes THEN openRuns + 1 ELSE openRuns + /\ UNCHANGED <> + +(* connection_wait_delay passes since the TCP accept. *) +AcceptWaitPasses(c) == + /\ cstate[c] # "none" /\ age[c] = "fresh" + /\ age' = [age EXCEPT ![c] = "accept"] + /\ UNCHANGED cstate + /\ ClientOnly + +(* connection_wait_delay passes since the handshake, which came after the accept. *) +HandshakeWaitPasses(c) == + /\ cstate[c] = "connected" /\ age[c] = "accept" + /\ age' = [age EXCEPT ![c] = "handshake"] + /\ UNCHANGED cstate + /\ ClientOnly + +(* Claude sends its CLOSE frame: the client is "closing" until its socket closes. *) +ClaudeCloses(c) == + /\ cstate[c] = "connected" + /\ cstate' = [cstate EXCEPT ![c] = "closing"] + /\ UNCHANGED age + /\ ClientOnly + +CloseCallbackRuns(c) == + /\ cstate[c] = "closing" + /\ cstate' = [cstate EXCEPT ![c] = "none"] + /\ UNCHANGED age + /\ ClientOnly + +ClaudeDrops(c) == + /\ cstate[c] # "none" + /\ cstate' = [cstate EXCEPT ![c] = "none"] + /\ UNCHANGED age + /\ ClientOnly + +----------------------------------------------------------------------------- +(* The plugin's timers and scheduled callbacks *) + +(* process_mention_queue(true): schedule_mention_flush(connection_wait_delay). *) +OpenRuns == + /\ openRuns > 0 + /\ openRuns' = openRuns - 1 + /\ LET t == Schedule(queue, flushTimer, dlTimer, dlFor) + IN /\ flushTimer' = t[1] + /\ dlTimer' = t[2] + /\ dlFor' = t[3] + /\ UNCHANGED <> + +FlushTimerFires == + /\ flushTimer = "running" + /\ flushTimer' = "fired" + /\ UNCHANGED <> + +(* The flush callback, flush_mention_queue. An empty queue stops both *) +(* timers. Otherwise assert(M.state.server). While some client counts but *) +(* none is ready, wait: mention_timer runs again. Otherwise broadcast the *) +(* head to every "connected" client. None took it: the head stays, and *) +(* the next handshake or the deadline moves it. Taken: the head leaves, *) +(* schedule_mention_flush(25 ms), and the writes finish: each write *) +(* succeeds, or all fail later, or libuv refuses them at once. *) +FlushRuns == + /\ flushTimer = "fired" + /\ IF queue = <<>> + THEN /\ flushTimer' = "nil" + /\ dlTimer' = "nil" + /\ dlFor' = 0 + /\ UNCHANGED <> + ELSE IF ~serverUp + THEN /\ luaError' = TRUE + /\ flushTimer' = "nil" + /\ UNCHANGED <> + ELSE IF FlushWaitsForReady /\ WaitForReady + THEN IF FlushExpiresOverdue + THEN /\ \E k \in 0..Len(queue) : Expire(k, IF WaitRearmsFlush THEN "running" ELSE "nil") + /\ UNCHANGED <> + ELSE /\ flushTimer' = IF WaitRearmsFlush THEN "running" ELSE "nil" + /\ UNCHANGED <> + ELSE LET took == Takers # {} + IN IF ~took /\ FlushChecksDelivery + THEN IF FlushExpiresOverdue + THEN /\ \E k \in 0..Len(queue) : Expire(k, "nil") + /\ UNCHANGED <> + ELSE /\ flushTimer' = "nil" + /\ UNCHANGED <> + ELSE \E i \in (IF FlushSendsHead THEN 1..1 ELSE 1..Len(queue)), result \in {"written", "failed", "refused"} : + LET m == queue[i] + q == IF FlushRemovesHead THEN SubSeq(queue, 1, i - 1) \o SubSeq(queue, i + 1, Len(queue)) + ELSE queue + t == Schedule(q, "nil", dlTimer, dlFor) + reported == IF result = "failed" THEN FailedWriteReported + ELSE RefusedWriteReported /\ FailedWriteReported + IN /\ queue' = q + /\ outcome' = [outcome EXCEPT ![m] = + IF ~took THEN "lost" + ELSE IF result = "written" THEN "delivered" + ELSE IF reported THEN "failed" ELSE "silent"] + /\ recv' = IF took /\ result = "written" + THEN [c \in C |-> IF c \in Takers THEN Append(recv[c], m) ELSE recv[c]] + ELSE recv + /\ early' = (early \/ (took /\ ~TrulyReady)) + /\ leaked' = (leaked \/ (took /\ result = "written" /\ stopped[m])) + /\ flushTimer' = t[1] + /\ dlTimer' = t[2] + /\ dlFor' = t[3] + /\ UNCHANGED luaError + /\ UNCHANGED <> + +DeadlineFires == + /\ DeadlinesFire + /\ dlTimer = "running" + /\ dlTimer' = "fired" + /\ UNCHANGED <> + +(* The deadline callback, expire_mentions. While a ready client is *) +(* connected, it clears nothing, makes sure a flush is due, and stops: *) +(* the queue drains to that client. The handshake's on_open callback can *) +(* still wait for the main loop then. Otherwise the mention it was *) +(* started for is the head if it still waits, and its deadline passed. *) +DeadlineRuns == + /\ dlTimer = "fired" + /\ IF DeadlineSparesReady /\ AnyCodeReady + THEN /\ dlTimer' = "nil" + /\ dlFor' = 0 + /\ flushTimer' = IF SparedQueueFlushes THEN Schedule(queue, flushTimer, "nil", 0)[1] ELSE flushTimer + /\ UNCHANGED <> + ELSE \E k \in (IF dlFor # 0 /\ Pending(dlFor) THEN 1 ELSE 0)..Len(queue) : Expire(k, flushTimer) + /\ UNCHANGED <> + +Done == + /\ \A m \in M : sent[m] /\ ~Pending(m) + /\ UNCHANGED vars + +Next == + \/ YouSend \/ YouStop \/ YouStart + \/ \E c \in C : \/ ClaudeConnects(c) \/ ClaudeUpgrades(c) \/ HandshakeWritten(c) \/ AcceptWaitPasses(c) + \/ HandshakeWaitPasses(c) \/ ClaudeCloses(c) \/ CloseCallbackRuns(c) \/ ClaudeDrops(c) + \/ OpenRuns \/ FlushTimerFires \/ FlushRuns \/ DeadlineFires \/ DeadlineRuns + \/ Done + +Spec == + /\ Init /\ [][Next]_vars + /\ WF_vars(OpenRuns) /\ WF_vars(FlushTimerFires) /\ WF_vars(FlushRuns) + /\ WF_vars(DeadlineFires) /\ WF_vars(DeadlineRuns) + /\ \A c \in C : /\ WF_vars(HandshakeWritten(c)) /\ WF_vars(CloseCallbackRuns(c)) + /\ WF_vars(AcceptWaitPasses(c)) /\ WF_vars(HandshakeWaitPasses(c)) + +RecvBound == \A c \in C : Len(recv[c]) <= Mentions + 1 + +----------------------------------------------------------------------------- +(* Rules *) + +NoSilentDrop == \A m \in M : outcome[m] \in {"lost", "silent"} => stopped[m] +SentInOrder == \A c \in C : \A i, j \in 1..Len(recv[c]) : i < j => recv[c][i] <= recv[c][j] +AtMostOnce == \A c \in C : \A i, j \in 1..Len(recv[c]) : i # j => recv[c][i] # recv[c][j] +SentWhenReady == ~early +NothingAfterStop == ~luaError /\ ~leaked +NoStrandedMention == \A m \in M : Pending(m) ~> ~Pending(m) +WentOut(m) == outcome[m] \in {"delivered", "failed", "silent", "lost"} +ReadyDelivers == \A m \in M : (Pending(m) /\ TrulyReady) ~> (WentOut(m) \/ ~TrulyReady) +\* The same promise, checked where no deadline passes: the flushes alone must send the queue to a ready Claude. +FlushDelivers == ReadyDelivers +============================================================================= diff --git a/.agents/skills/verify-mention-queue/model/statechart-view.ts b/.agents/skills/verify-mention-queue/model/statechart-view.ts new file mode 100644 index 000000000..929e0d132 --- /dev/null +++ b/.agents/skills/verify-mention-queue/model/statechart-view.ts @@ -0,0 +1,98 @@ +// /statechart view for MentionQueue.tla: one region per Claude client slot, and one per @ mention. +const has = (seq: any, m: number) => Object.values(seq ?? {}).includes(m); + +const client = (v: any, c: number) => { + if (!v.serverUp) return "integration stopped"; + const state = ( + { + none: "not connected", + connecting: "connecting", + upgrading: "connecting", + connected: "connected", + closing: "hanging up", + } as Record + )[v.cstate[c]]; + if (v.cstate[c] === "connected") + return v.age[c] === "handshake" + ? "connected, ready" + : "connected, not ready yet"; + return state; +}; + +const outcomes: Record = { + refused: "refused with an error", + delivered: "Claude has it", + failed: "write failed, with an error", + lost: "lost, no error", + errored: "dropped at its deadline, with an error", + silent: "dropped, no error", + cleared: "cleared by the stop", +}; + +const mention = (v: any, m: number) => { + if (!v.sent[m]) return "not sent"; + if (has(v.queue, m)) { + const moving = + v.flushTimer !== "nil" || v.dlTimer !== "nil" || v.openRuns > 0; + return moving ? "queued" : "queued, nothing will send or drop it"; + } + return outcomes[v.outcome[m]] ?? v.outcome[m]; +}; + +const ids = (v: any) => + Object.keys(v.sent) + .map(Number) + .sort((a, b) => a - b); + +export const title = "Your @ mentions and the Claude clients (claudecode.nvim)"; + +export const state = (v: any) => { + const regions: Record = {}; + for (const c of [1, 2]) regions[`Claude ${c}`] = client(v, c); + for (const m of ids(v)) regions[`Mention ${m}`] = mention(v, m); + // /statechart needs the same regions in every state, so each harm region is there from the start, as "no". + regions["Sent early"] = v.early + ? "a mention went out before any client was ready" + : "no"; + regions["Lua error"] = v.luaError ? "Lua error" : "no"; + regions["Sent after a stop"] = v.leaked + ? "a mention queued before :ClaudeCodeStop reached a Claude after the stop" + : "no"; + return regions; +}; + +export const group = (v: any) => { + const all = ids(v).map((m) => mention(v, m)); + if ( + v.early || + v.luaError || + v.leaked || + all.some((s) => s.includes("no error") || s.includes("nothing will")) + ) + return "harm"; + if (all.every((s) => s === "Claude has it")) return "good"; + return "open"; +}; +export const colors = { harm: "pink", good: "teal", open: "blue" }; + +const labels: Record = { + YouSend: "you send a mention", + YouStop: "you run :ClaudeCodeStop", + YouStart: "you run :ClaudeCodeStart", + ClaudeConnects: "a Claude opens its socket", + ClaudeUpgrades: "Claude asks for the WebSocket", + HandshakeWritten: "the handshake completes", + AcceptWaitPasses: "600 ms pass since the socket opened", + HandshakeWaitPasses: "600 ms pass since the handshake: Claude is ready", + ClaudeCloses: "Claude hangs up", + CloseCallbackRuns: "Claude's socket goes away", + ClaudeDrops: "Claude's socket goes away", + OpenRuns: "the handshake schedules a flush", + FlushTimerFires: "a flush is due", + FlushRuns: "the flush runs", + DeadlineFires: "a deadline passes", + DeadlineRuns: "the deadline clears the expired mentions", + Done: "nothing more happens", +}; +export const step = (action: string) => + labels[action.replace(/\(.*$/, "")] ?? action; diff --git a/.agents/skills/verify-mention-queue/replays/churn.lua b/.agents/skills/verify-mention-queue/replays/churn.lua new file mode 100644 index 000000000..46b5e9dec --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/churn.lua @@ -0,0 +1,48 @@ +-- NoStrandedMention (the #480 churn finding): you send while no client is connected, and clients connect and leave +-- without overlap, a new one every 1000 ms that stays 300 ms, so none is ever ready. Each handshake once stopped the +-- connection timeout, and the mention waited with no error for as long as the clients kept coming. Now no handshake +-- moves the mention's deadline: it must leave with one error about connection_timeout + connection_wait_delay +-- (10.6 s) after the send, and no client may get it. +-- Model path: YouSend, then ClaudeConnects(c), ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, ClaudeDrops(c), +-- FlushTimerFires, FlushRuns, again and again, until DeadlineFires, DeadlineRuns. +local uv = vim.uv or vim.loop +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +local path = L.file("hello.txt") +local clients, sent_at, cleared_at = {}, nil, nil +local function now() + return uv.hrtime() / 1e6 +end +-- The plugin stamps the deadline with the loop clock (vim.loop.now()), which moves only when the loop turns, and +-- L.setup() gave it no turn. Refresh the loop clock before the send, and measure the send and the clearing on that +-- clock: a correct deadline then never reads less than 10600 ms after the send. +uv.update_time() +sent_at = uv.now() +L.send(path) +L.wait(500, "no client is connected yet") +for _ = 1, 14 do + local started = now() + local c = L.connect() + L.upgrade(c) + table.insert(clients, c) + L.wait(300 - (now() - started), "this client stays 300 ms") + L.drop(c) + if not cleared_at and L.queue_len() == 0 then + cleared_at = uv.now() + end + L.wait(1000 - (now() - started), "the next client connects 1000 ms after this one") + if not cleared_at and L.queue_len() == 0 then + cleared_at = uv.now() + end +end +local received = 0 +for _, c in ipairs(clients) do + received = received + #L.received(c) +end +local after = cleared_at and (cleared_at - sent_at) or -1 +L.log("queue=%d; notices=%d; received=%d; cleared %.0f ms after the send", L.queue_len(), #L.notices, received, after) +L.verdict( + L.queue_len() == 0 and #L.notices == 1 and received == 0 and after >= 10600 and after < 12000, + "NoStrandedMention", + string.format("clients that never overlap: errors=%d received=%d cleared after %.0f ms", #L.notices, received, after) +) diff --git a/.agents/skills/verify-mention-queue/replays/closing-client.lua b/.agents/skills/verify-mention-queue/replays/closing-client.lua new file mode 100644 index 000000000..68229af13 --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/closing-client.lua @@ -0,0 +1,57 @@ +-- NoStrandedMention (finding 6): Claude's CLOSE frame sets the client to "closing". is_claude_connected once still +-- counted it, so a send in that tick took the connected path, and the mention waited with nothing that sent or +-- dropped it. Now a closing client does not count, and the mention's deadline runs from the send: with no new +-- Claude, it leaves with the connection timeout error. The replay feeds the CLOSE frame through the real +-- server/client.lua process_data, with the on_close that server/tcp.lua passes, and sends in the same tick. +-- Model path: ClaudeConnects(c), ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, ClaudeCloses(c), YouSend, +-- CloseCallbackRuns(c), DeadlineFires, DeadlineRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +local path = L.file("hello.txt") +local c = L.connect() +L.upgrade(c) +local server = require("claudecode.server.init").state.server +local client_mod = require("claudecode.server.client") +local frame = require("claudecode.server.frame") +local tcp = require("claudecode.server.tcp") +local _, srv_client = next(server.clients) +client_mod.process_data( + srv_client, + frame.create_frame(frame.OPCODE.CLOSE, "\3\232", true, true), + function() end, + function(cl, code, reason) + tcp._disconnect_client(server, cl, code, reason) + end, + function() end, + require("claudecode").state.auth_token +) +L.log("Claude's CLOSE frame arrives: server-side state=%s", srv_client.state) +L.send(path) +L.log( + "ClaudeCodeSendComplete fired %d time(s); queue=%d; connection timer=%s", + L.send_complete, + L.queue_len(), + L.timer_state() +) +L.wait_for(11500, "the deadline clears the mention", function() + return L.queue_len() == 0 and #L.notices > 0 +end) +L.log( + "Claude received %d; queue=%d; client=%q; connection timer=%s; notices=%d", + #L.received(c), + L.queue_len(), + L.server_clients(), + L.timer_state(), + #L.notices +) +L.verdict( + L.send_complete == 0 and L.queue_len() == 0 and #L.notices == 1 and L.timer_state() == "nil", + "NoStrandedMention", + string.format( + "sent to a closing client: completes=%d queue=%d errors=%d timer=%s", + L.send_complete, + L.queue_len(), + #L.notices, + L.timer_state() + ) +) diff --git a/.agents/skills/verify-mention-queue/replays/drain.lua b/.agents/skills/verify-mention-queue/replays/drain.lua new file mode 100644 index 000000000..24a3f5a6e --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/drain.lua @@ -0,0 +1,35 @@ +-- ReadyDelivers (the #480 drain finding): you send 100 mentions at once, as a tree add of 100 files does, while +-- Claude starts. Its handshake comes 8.6 s later. The queue drains to it 25 ms apart, past the deadline at 10.6 s, +-- and the deadline once cleared the rest while Claude was taking them. Now no deadline clears a mention while a ready +-- client is connected: all 100 must arrive, in order, with no error. +-- Model path: YouSend (each mention), ClaudeConnects(c), ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, +-- AcceptWaitPasses(c), HandshakeWaitPasses(c), FlushTimerFires, FlushRuns, DeadlineFires, DeadlineRuns, then +-- FlushTimerFires, FlushRuns for each mention. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +local paths = {} +for index = 1, 100 do + paths[index] = L.file("f" .. index .. ".txt") +end +for _, path in ipairs(paths) do + require("claudecode").send_at_mention(path, nil, nil, "replay") +end +L.log("you send 100 mentions at once; queue=%d", L.queue_len()) +L.wait(8600, "Claude starts") +local c = L.connect() +L.upgrade(c) +L.wait_for(8000, "the queue drains", function() + return L.queue_len() == 0 +end) +L.wait(200, "Claude reads the last frames") +local got = L.received(c) +local in_order = #got == 100 +for index, path in ipairs(got) do + in_order = in_order and path == paths[index] +end +L.log("Claude received %d, in order: %s; notices=%d", #got, tostring(in_order), #L.notices) +L.verdict( + in_order and #L.notices == 0, + "ReadyDelivers", + string.format("100 at once, handshake at 8.6 s: received=%d errors=%d", #got, #L.notices) +) diff --git a/.agents/skills/verify-mention-queue/replays/drop-in-debounce.lua b/.agents/skills/verify-mention-queue/replays/drop-in-debounce.lua new file mode 100644 index 000000000..20386dacf --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/drop-in-debounce.lua @@ -0,0 +1,28 @@ +-- NoStrandedMention (finding 6): Claude's socket drops within the 50 ms debounce after a send while it was connected. +-- The connected path once started no timer, so the mention waited with nothing that sent or dropped it. Now its +-- deadline runs from the send: with no new Claude, the mention leaves with the connection timeout error. +-- Model path: ClaudeConnects(c), ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, AcceptWaitPasses(c), +-- HandshakeWaitPasses(c), YouSend, ClaudeDrops(c), FlushTimerFires, FlushRuns, DeadlineFires, DeadlineRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +local path = L.file("hello.txt") +local c = L.connect() +L.upgrade(c) +L.wait(800, "Claude is ready: connection_wait_delay passed since its handshake") +L.send(path) +L.drop(c) +L.wait_for(11500, "the deadline clears the mention", function() + return L.queue_len() == 0 and #L.notices > 0 +end) +L.log( + "queue=%d; connection timer=%s; notices=%d; received=%d", + L.queue_len(), + L.timer_state(), + #L.notices, + #L.received(c) +) +L.verdict( + L.queue_len() == 0 and #L.notices == 1 and #L.received(c) == 0 and L.timer_state() == "nil", + "NoStrandedMention", + string.format("dropped during the debounce: queue=%d errors=%d timer=%s", L.queue_len(), #L.notices, L.timer_state()) +) diff --git a/.agents/skills/verify-mention-queue/replays/expired-at-flush.lua b/.agents/skills/verify-mention-queue/replays/expired-at-flush.lua new file mode 100644 index 000000000..16740e1ee --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/expired-at-flush.lua @@ -0,0 +1,19 @@ +-- NoSilentDrop (finding 1): you send while Claude is not connected, and Claude completes its handshake 4.6 s later, as +-- a cold start often does. The plugin once dropped such a mention as older than queue_timeout at the flush, with no +-- error. Now the mention waits for Claude: it must arrive once, with no error. +-- Model path: YouSend, ClaudeConnects(c), ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, AcceptWaitPasses(c), +-- HandshakeWaitPasses(c), FlushTimerFires, FlushRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +L.send(L.file("hello.txt")) +L.wait(4600, "Claude starts slowly") +local c = L.connect() +L.upgrade(c) +L.wait(1500, "connection_wait_delay ends and the flush runs") +local got = L.received(c) +L.log("Claude received %d; queue=%d; notices=%d", #got, L.queue_len(), #L.notices) +L.verdict( + #got == 1 and #L.notices == 0 and L.queue_len() == 0, + "NoSilentDrop", + string.format("slow start: received=%d errors=%d queue=%d", #got, #L.notices, L.queue_len()) +) diff --git a/.agents/skills/verify-mention-queue/replays/handshake-window.lua b/.agents/skills/verify-mention-queue/replays/handshake-window.lua new file mode 100644 index 000000000..3bc317a18 --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/handshake-window.lua @@ -0,0 +1,20 @@ +-- FlushDelivers (finding 7): you send between Claude's TCP connect and its WebSocket handshake. The plugin once +-- flushed only on the TCP connect, so nothing flushed after the handshake, and the timeout cleared the mention while +-- Claude was connected. Now the handshake schedules the flush: the mention must arrive once, with no error. +-- Model path: ClaudeConnects(c), YouSend, ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, AcceptWaitPasses(c), +-- HandshakeWaitPasses(c), FlushTimerFires, FlushRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +local path = L.file("hello.txt") +local c = L.connect() +L.wait(50, "Claude has not asked for the WebSocket yet") +L.send(path) +L.upgrade(c) +L.wait(1500, "connection_wait_delay ends and the flush runs") +local got = L.received(c) +L.log("Claude received %d; queue=%d; client=%s; notices=%d", #got, L.queue_len(), L.server_clients(), #L.notices) +L.verdict( + #got == 1 and #L.notices == 0 and L.queue_len() == 0, + "FlushDelivers", + string.format("send before the handshake: received=%d errors=%d", #got, #L.notices) +) diff --git a/.agents/skills/verify-mention-queue/replays/lib.lua b/.agents/skills/verify-mention-queue/replays/lib.lua new file mode 100644 index 000000000..6e45fafeb --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/lib.lua @@ -0,0 +1,206 @@ +-- Shared helpers for the mention-queue replays. Each replay runs in a fresh headless Neovim (see run.sh), starts +-- the real plugin with the default delays and the "none" terminal provider, and plays Claude with real loopback +-- WebSocket clients in the same process. Every step of a replay is one model action, in the model's order, and +-- vim.wait pumps the real event loop between steps, so the plugin's own timers and vim.schedule callbacks run. +-- The auth token is read from plugin state and never printed. +local uv = vim.uv or vim.loop +local L = {} + +local start = uv.hrtime() +local function ms() + return math.floor((uv.hrtime() - start) / 1e6) +end + +function L.log(fmt, ...) + io.stdout:write(string.format("%6d ms ", ms()) .. string.format(fmt, ...) .. "\n") +end + +-- What the user sees: every vim.notify at WARN or above, and every Lua error Neovim reports. +L.notices = {} +local notify = vim.notify +vim.notify = function(msg, level, opts) + if (level or 0) >= vim.log.levels.WARN then + table.insert(L.notices, msg) + L.log("user sees: %s", msg) + end + return notify(msg, level, opts) +end +L.send_complete = 0 + +function L.setup() + local cc = require("claudecode") + cc.setup({ terminal = { provider = "none" }, track_selection = false }) + assert(cc.state.server, "the server did not start") + vim.api.nvim_create_autocmd("User", { + pattern = "ClaudeCodeSendComplete", + callback = function() + L.send_complete = L.send_complete + 1 + end, + }) + L.log( + "plugin started: connection_timeout=%d connection_wait_delay=%d", + cc.state.config.connection_timeout, + cc.state.config.connection_wait_delay + ) + return cc +end + +function L.wait(n, why) + L.log("wait %d ms (%s)", n, why) + vim.wait(n, function() + return false + end, 10) +end + +function L.wait_for(n, why, cond) + local ok = vim.wait(n, cond, 5) + L.log("%s: %s", why, ok and "yes" or "NO (timed out)") + return ok +end + +-- A file that exists, given as an absolute path, the way :ClaudeCodeAdd passes it after expand. +function L.file(name) + local path = vim.fn.getcwd() .. "/" .. name + vim.fn.writefile({ name }, path) + return path +end + +function L.send(path) + local cc = require("claudecode") + local connected = cc.is_claude_connected() + local ok, err = cc.send_at_mention(path, nil, nil, "replay") + L.log( + "you send %s (Claude counts as connected: %s): ok=%s%s", + vim.fn.fnamemodify(path, ":t"), + tostring(connected), + tostring(ok), + err and (" err=" .. err) or "" + ) +end + +function L.queue_len() + return #require("claudecode").state.mention_queue +end + +function L.server_clients() + local status = require("claudecode.server.init").get_status() + local out = {} + for _, info in ipairs(status.clients or {}) do + table.insert(out, info.state) + end + table.sort(out) + return table.concat(out, ",") +end + +function L.client_count() + return #(require("claudecode.server.init").get_status().clients or {}) +end + +function L.timer_state() + local t = require("claudecode").state.connection_timer + if not t then + return "nil" + end + return t:is_active() and "running" or "set but not running" +end + +-- Claude, played by a loopback client. +function L.connect() + local cc = require("claudecode") + local before = L.client_count() + local c = { tcp = uv.new_tcp(), buf = "", upgraded = false, texts = {}, eof = false } + c.tcp:connect("127.0.0.1", cc.state.port, function(err) + assert(not err, err) + c.tcp:read_start(function(rerr, data) + if rerr or not data then + c.eof = true + return + end + c.buf = c.buf .. data + if not c.upgraded then + local head_end = c.buf:find("\r\n\r\n", 1, true) + if not head_end then + return + end + c.status = c.buf:match("^HTTP/1%.1 (%d+)") + c.upgraded = c.status == "101" + c.buf = c.buf:sub(head_end + 4) + end + while #c.buf >= 2 do + local b1, b2 = c.buf:byte(1, 2) + local len, pos = b2 % 128, 3 + if len == 126 then + if #c.buf < 4 then + return + end + len, pos = c.buf:byte(3) * 256 + c.buf:byte(4), 5 + end + if #c.buf < pos + len - 1 then + return + end + if b1 % 16 == 1 then + table.insert(c.texts, c.buf:sub(pos, pos + len - 1)) + end + c.buf = c.buf:sub(pos + len) + end + end) + end) + L.wait_for(2000, "Claude opens its socket; the server lists it", function() + return L.client_count() > before + end) + return c +end + +function L.upgrade(c) + local token = require("claudecode").state.auth_token + local key = require("claudecode.server.utils").base64_encode("0123456789abcdef") + c.tcp:write(table.concat({ + "GET / HTTP/1.1", + "Host: 127.0.0.1", + "Upgrade: websocket", + "Connection: Upgrade", + "Sec-WebSocket-Key: " .. key, + "Sec-WebSocket-Version: 13", + "x-claude-code-ide-authorization: " .. token, + "", + "", + }, "\r\n")) + -- Claude reads the 101 reply after its write finished, and the write callback marked the client connected. + return L.wait_for(2000, "Claude asks for the WebSocket; the handshake completes", function() + return c.upgraded and L.server_clients():find("connected", 1, true) ~= nil + end) +end + +-- The at_mentioned file paths Claude received, in order. +function L.received(c) + local out = {} + for _, text in ipairs(c.texts) do + local ok, msg = pcall(vim.json.decode, text) + if ok and msg.method == "at_mentioned" then + table.insert(out, msg.params.filePath) + end + end + return out +end + +function L.drop(c) + local before = L.client_count() + c.tcp:read_stop() + c.tcp:close() + L.wait_for(2000, "Claude's socket drops; the server forgets the client", function() + return L.client_count() < before + end) +end + +-- The last Lua error Neovim reported (a vim.schedule or vim.defer_fn callback that raised), or "". +function L.errmsg() + return vim.v.errmsg +end + +-- One verdict line per replay: KEPT or BROKEN, the rule whose promise the replay checks, and the facts it rests on. +function L.verdict(kept, rule, facts) + io.stdout:write(string.format("%s %s: %s\n", kept and "KEPT" or "BROKEN", rule, facts)) + vim.cmd("qall!") +end + +return L diff --git a/.agents/skills/verify-mention-queue/replays/lost-in-wait-reconnect.lua b/.agents/skills/verify-mention-queue/replays/lost-in-wait-reconnect.lua new file mode 100644 index 000000000..0a2c4ffbf --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/lost-in-wait-reconnect.lua @@ -0,0 +1,24 @@ +-- NoSilentDrop (finding 2, with a reconnect): Claude's socket drops during the 600 ms wait, and a new Claude +-- connects 2 s later. The mention must reach the new Claude, once, with no error. +-- Model path: YouSend, ClaudeConnects(1), ClaudeUpgrades(1), HandshakeWritten(1), OpenRuns, ClaudeDrops(1), +-- FlushTimerFires, FlushRuns, ClaudeConnects(2), ClaudeUpgrades(2), HandshakeWritten(2), OpenRuns, +-- AcceptWaitPasses(2), HandshakeWaitPasses(2), FlushTimerFires, FlushRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +L.send(L.file("hello.txt")) +local c = L.connect() +L.upgrade(c) +assert(dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/sync.lua")(L), "no armed flush") +L.drop(c) +L.wait(2000, "Claude restarts") +L.log("queue=%d connection timer=%s", L.queue_len(), L.timer_state()) +local c2 = L.connect() +L.upgrade(c2) +L.wait(1500, "the 600 ms wait ends and the mention is sent") +local got = L.received(c2) +L.log("the new Claude received: %s; notices=%d", table.concat(got, ", "), #L.notices) +L.verdict( + #got == 1 and #L.notices == 0, + "NoSilentDrop", + string.format("reconnect after a drop in the wait: new client received=%d errors=%d", #got, #L.notices) +) diff --git a/.agents/skills/verify-mention-queue/replays/lost-in-wait.lua b/.agents/skills/verify-mention-queue/replays/lost-in-wait.lua new file mode 100644 index 000000000..d575b26ba --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/lost-in-wait.lua @@ -0,0 +1,24 @@ +-- NoSilentDrop (finding 2): Claude's socket drops during the connection_wait_delay wait after its handshake. The +-- plugin once sent the mention to no client and logged success at debug level. Now the mention stays queued, and +-- with no new Claude it leaves at its deadline (connection_timeout + connection_wait_delay after the send) with the +-- connection timeout error. +-- Model path: YouSend, ClaudeConnects(c), ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, ClaudeDrops(c), +-- FlushTimerFires, FlushRuns, DeadlineFires, DeadlineRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +L.send(L.file("hello.txt")) +local c = L.connect() +L.upgrade(c) +assert(dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/sync.lua")(L), "no armed flush") +L.drop(c) +L.wait(1500, "the 600 ms wait ends") +local queued = L.queue_len() +L.log("after the wait: queue=%d; connection timer=%s", queued, L.timer_state()) +L.wait(10000, "the deadline passes without a new Claude") +local got = L.received(c) +L.log("Claude received %d; queue=%d; notices=%d", #got, L.queue_len(), #L.notices) +L.verdict( + queued == 1 and #got == 0 and #L.notices == 1 and L.notices[1]:find("Connection timeout", 1, true) ~= nil, + "NoSilentDrop", + string.format("drop in the wait: queued after it=%d received=%d errors=%d", queued, #got, #L.notices) +) diff --git a/.agents/skills/verify-mention-queue/replays/order.lua b/.agents/skills/verify-mention-queue/replays/order.lua new file mode 100644 index 000000000..d2496898d --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/order.lua @@ -0,0 +1,29 @@ +-- SentInOrder (finding 3): you send mention 1 while Claude is not connected, Claude connects, and you send mention 2 +-- during the connection_wait_delay wait. Mention 2 once took the 50 ms debounce path and overtook mention 1. Now one +-- queue holds both: Claude must get mention 1, then mention 2. +-- Model path: YouSend, ClaudeConnects(c), ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, YouSend, +-- AcceptWaitPasses(c), HandshakeWaitPasses(c), FlushTimerFires, FlushRuns, FlushTimerFires, FlushRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +L.send(L.file("first.txt")) +local c = L.connect() +L.upgrade(c) +assert(dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/sync.lua")(L), "no armed flush") +L.send(L.file("second.txt")) +L.wait(1500, "the debounce and the 600 ms wait end") +local got = L.received(c) +L.log("Claude received, in order: %s", table.concat(got, " | ")) +local in_order = #got == 2 and got[1]:find("first.txt", 1, true) ~= nil and got[2]:find("second.txt", 1, true) ~= nil +L.verdict( + in_order, + "SentInOrder", + string.format( + "arrival order: %s", + table.concat( + vim.tbl_map(function(p) + return vim.fn.fnamemodify(p, ":t") + end, got), + ", " + ) + ) +) diff --git a/.agents/skills/verify-mention-queue/replays/restart-leak.lua b/.agents/skills/verify-mention-queue/replays/restart-leak.lua new file mode 100644 index 000000000..b35b61942 --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/restart-leak.lua @@ -0,0 +1,20 @@ +-- NothingAfterStop (finding 4, restart form): :ClaudeCodeStop then :ClaudeCodeStart during the connection_wait_delay +-- wait, and a new Claude connects. The mention from before the stop once reached the new Claude. Now the stop clears +-- it: the new Claude must get nothing. +-- Model path: YouSend, ClaudeConnects(1), ClaudeUpgrades(1), HandshakeWritten(1), OpenRuns, YouStop, YouStart, +-- ClaudeConnects(2), ClaudeUpgrades(2), HandshakeWritten(2), OpenRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +L.send(L.file("hello.txt")) +local c = L.connect() +L.upgrade(c) +assert(dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/sync.lua")(L), "no armed flush") +L.log("you run :ClaudeCodeStop, then :ClaudeCodeStart") +vim.cmd("ClaudeCodeStop") +vim.cmd("ClaudeCodeStart") +local c2 = L.connect() +L.upgrade(c2) +L.wait(1500, "the 600 ms wait ends") +local got = L.received(c2) +L.log("the new Claude received: %s; v:errmsg=%q", table.concat(got, ", "), L.errmsg()) +L.verdict(#got == 0, "NothingAfterStop", string.format("sent across a stop: new client received=%d", #got)) diff --git a/.agents/skills/verify-mention-queue/replays/run.sh b/.agents/skills/verify-mention-queue/replays/run.sh new file mode 100755 index 000000000..b44ed919f --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/run.sh @@ -0,0 +1,49 @@ +#!/usr/bin/env bash +# Replay each path that once broke a rule, against the real plugin in a fresh headless Neovim. +# Usage: replays/run.sh [NAME...] (default: every *.lua replay except lib.lua and sync.lua) +# NVIM overrides the Neovim binary. Each replay's full timeline goes to $OUT/.log (OUT defaults to a new +# mktemp -d dir, printed first). Prints one verdict line per replay (KEPT or BROKEN, and the rule) and a count line. +# A replay is KEPT only when it printed KEPT and its Neovim exited 0. +# Exits 0 when every replay kept its promise, 1 otherwise. +set -uo pipefail +here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +repo=$(git -C "$here" rev-parse --show-toplevel) +NVIM=${NVIM:-nvim} +OUT=${OUT:-$(mktemp -d "${TMPDIR:-/tmp}/mention-replays.XXXXXX")} +# Each replay runs from its own cwd, so a relative OUT or NVIM must become absolute first. +mkdir -p "$OUT" && OUT=$(cd "$OUT" && pwd) || exit 2 +if [[ $NVIM == */* ]]; then NVIM=$(cd "$(dirname "$NVIM")" && pwd)/$(basename "$NVIM") || exit 2; fi +echo "logs: $OUT" +names=("$@") +if ((${#names[@]} == 0)); then + for f in "$here"/*.lua; do + case $(basename "$f") in lib.lua | sync.lua) ;; *) names+=("$(basename "$f" .lua)") ;; esac + done +fi +kept=0 +for name in "${names[@]}"; do + run="$OUT/$name.run" + mkdir -p "$run/xdg-config" "$run/xdg-data" "$run/xdg-state" "$run/xdg-cache" "$run/claude" "$run/cwd" + # macOS has no `timeout`, so perl's alarm bounds the run. REPLAY_REPO and REPLAY_SCRIPT reach Neovim through the + # environment, so a checkout path with a space or another Ex-special character still works. `nvim -l` needs + # Neovim 0.9, so the replay runs through :luafile, as in .github/workflows/test.yml. A replay quits Neovim at its + # verdict. If it raises before that, the last -c exits 2. + (cd "$run/cwd" && XDG_CONFIG_HOME="$run/xdg-config" XDG_DATA_HOME="$run/xdg-data" XDG_STATE_HOME="$run/xdg-state" \ + XDG_CACHE_HOME="$run/xdg-cache" CLAUDE_CONFIG_DIR="$run/claude" \ + REPLAY_REPO="$repo" REPLAY_SCRIPT="$here/$name.lua" \ + perl -e 'alarm 120; exec @ARGV' "$NVIM" --headless -u NONE -i NONE \ + --cmd 'lua vim.opt.rtp:prepend(vim.env.REPLAY_REPO)' -c 'execute "luafile" fnameescape($REPLAY_SCRIPT)' \ + -c 'cquit 2') >"$OUT/$name.log" 2>&1 + rc=$? + verdict=$(grep -E '^(KEPT|BROKEN) ' "$OUT/$name.log" | tail -1) + if [[ -z $verdict ]]; then + verdict="BROKEN $name: the replay printed no verdict, and Neovim exited $rc (see $OUT/$name.log)" + elif ((rc != 0)); then + # A verdict, then a failed exit (a VimLeavePre error, the alarm): the run failed whatever the verdict said. + verdict="BROKEN $name: Neovim exited $rc after the verdict \"$verdict\" (see $OUT/$name.log)" + fi + [[ $verdict == KEPT* ]] && kept=$((kept + 1)) + echo "$name: $verdict" +done +echo "$kept of ${#names[@]} replays kept their promise" +((kept == ${#names[@]})) diff --git a/.agents/skills/verify-mention-queue/replays/stop-in-wait.lua b/.agents/skills/verify-mention-queue/replays/stop-in-wait.lua new file mode 100644 index 000000000..a19d409f0 --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/stop-in-wait.lua @@ -0,0 +1,21 @@ +-- NothingAfterStop (finding 4): :ClaudeCodeStop during the connection_wait_delay wait. A deferred send once indexed +-- M.state.server after M.stop set it to nil, and raised a Lua error. Now the stop clears the queue and stops its +-- timers: no Lua error, and Claude gets nothing. +-- Model path: YouSend, ClaudeConnects(c), ClaudeUpgrades(c), HandshakeWritten(c), OpenRuns, YouStop. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +local cc = L.setup() +L.send(L.file("hello.txt")) +local c = L.connect() +L.upgrade(c) +assert(dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/sync.lua")(L), "no armed flush") +L.log("you run :ClaudeCodeStop") +vim.cmd("ClaudeCodeStop") +L.log("server=%s queue=%d errmsg=%q", tostring(cc.state.server), L.queue_len(), L.errmsg()) +L.wait(1500, "the 600 ms wait ends") +local err = L.errmsg() +L.log("v:errmsg = %s", err) +L.verdict( + err == "" and #L.received(c) == 0, + "NothingAfterStop", + string.format("Lua error after stop: %s", err:match("init%.lua:%d+: [^\n]*") or err) +) diff --git a/.agents/skills/verify-mention-queue/replays/sync.lua b/.agents/skills/verify-mention-queue/replays/sync.lua new file mode 100644 index 000000000..ba402e002 --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/sync.lua @@ -0,0 +1,9 @@ +-- Waits until Claude's handshake started the 600 ms connection_wait_delay wait for the queued mention. Since #454 the +-- mention stays queued and the handshake arms the flush timer. Before #454 the handshake moved the queue into a +-- deferred batch, so the queue turned empty. Either point lets a replay act inside the wait on both designs. +return function(L) + return L.wait_for(1000, "the handshake starts the 600 ms wait for the queued mention", function() + local queued = L.queue_len() + return (require("claudecode").state.mention_timer ~= nil and queued >= 1) or queued == 0 + end) +end diff --git a/.agents/skills/verify-mention-queue/replays/timer-never-reset.lua b/.agents/skills/verify-mention-queue/replays/timer-never-reset.lua new file mode 100644 index 000000000..a831c9e8d --- /dev/null +++ b/.agents/skills/verify-mention-queue/replays/timer-never-reset.lua @@ -0,0 +1,26 @@ +-- NoStrandedMention (finding 5): the connection timer once stayed set after it fired, so a mention queued later, +-- while Claude was still not connected, got no timeout and no error. Now each mention has its own deadline: both +-- mentions must leave the queue with an error, about connection_timeout + connection_wait_delay after their send. +-- Model path: YouSend, DeadlineFires, DeadlineRuns, YouSend, DeadlineFires, DeadlineRuns. +local L = dofile(vim.fn.fnamemodify(debug.getinfo(1, "S").source:sub(2), ":h") .. "/lib.lua") +L.setup() +L.send(L.file("first.txt")) +L.wait_for(11500, "the deadline clears the first mention with an error", function() + return #L.notices == 1 and L.queue_len() == 0 +end) +L.send(L.file("second.txt")) +L.log("queue=%d connection timer=%s", L.queue_len(), L.timer_state()) +L.wait_for(11500, "the deadline clears the second mention with an error", function() + return #L.notices == 2 and L.queue_len() == 0 +end) +L.log("queue=%d connection timer=%s notices=%d", L.queue_len(), L.timer_state(), #L.notices) +L.verdict( + L.queue_len() == 0 and #L.notices == 2 and L.timer_state() == "nil", + "NoStrandedMention", + string.format( + "a second mention after a timeout: queue=%d errors=%d timer=%s", + L.queue_len(), + #L.notices, + L.timer_state() + ) +) diff --git a/dev-config.lua b/dev-config.lua index 2427d123d..259fa10fd 100644 --- a/dev-config.lua +++ b/dev-config.lua @@ -77,7 +77,7 @@ return { -- Connection Management -- connection_wait_delay = 600, -- Wait time after Claude's handshake before sending queued @ mentions (ms) -- connection_timeout = 10000, -- Time Claude Code has to connect before queued @ mentions time out (ms) - -- queue_timeout = 5000, -- Unused, still accepted: queued @ mentions wait up to connection_timeout + -- queue_timeout = 5000, -- Unused, still accepted (see connection_timeout) -- Diff Integration -- diff_opts = { diff --git a/fixtures/issue-70/init.lua b/fixtures/issue-70/init.lua index 23111d1eb..7fd5c3858 100644 --- a/fixtures/issue-70/init.lua +++ b/fixtures/issue-70/init.lua @@ -5,8 +5,9 @@ -- -- The symptom is downstream of ONE thing: the Claude CLI that the plugin launches -- never opens a WebSocket connection back to the plugin's server, so every queued --- @ mention sits in the queue until `connection_timeout` (default 10s) elapses and --- the queue is cleared with the error above. +-- @ mention sits in the queue until its deadline, `connection_timeout + +-- connection_wait_delay` (default 10.6s) after the send, and is cleared with the +-- error above. -- -- This fixture launches the REAL plugin with the native terminal provider so the -- Claude CLI runs inside Neovim. Because it loads the plugin from the repo, the diff --git a/lua/claudecode/config.lua b/lua/claudecode/config.lua index cf2b2d8b6..096514fd2 100644 --- a/lua/claudecode/config.lua +++ b/lua/claudecode/config.lua @@ -21,7 +21,7 @@ M.defaults = { -- Milliseconds Claude Code has to connect for queued @ mentions. Each one leaves with an error connection_timeout + -- connection_wait_delay ms after its send, unless a ready Claude takes the queue first. connection_timeout = 10000, - queue_timeout = 5000, -- Unused, kept so that configs that set it stay valid (connection_timeout bounds the wait) + queue_timeout = 5000, -- Unused, kept so that configs that set it stay valid (see connection_timeout) diff_opts = { layout = "vertical", open_in_new_tab = false, -- Open diff in a new tab (false = use current tab) diff --git a/lua/claudecode/types.lua b/lua/claudecode/types.lua index 5684a9fe9..17bc35436 100644 --- a/lua/claudecode/types.lua +++ b/lua/claudecode/types.lua @@ -153,7 +153,8 @@ ---@field initialized boolean ---@field mention_queue ClaudeCodeMention[] ---@field mention_timer uv.uv_timer_t? -- the next flush of the mention queue (compatible with vim.loop timer) ----@field connection_timer uv.uv_timer_t? -- the deadline of the oldest queued mention +---@field connection_timer uv.uv_timer_t? -- the deadline timer: runs while the queue holds a mention. It is nil after +--- a deadline passed while a ready client was connected, until queue_mention or a flush with no ready client starts it -- This module only defines types, no runtime functionality return {} diff --git a/tests/unit/mention_queue_spec.lua b/tests/unit/mention_queue_spec.lua index 1b1a81384..77165ab6f 100644 --- a/tests/unit/mention_queue_spec.lua +++ b/tests/unit/mention_queue_spec.lua @@ -541,6 +541,44 @@ describe("The @ mention queue", function() end ) + -- The flush comes 50 ms after the send and waits out the rest of connection_wait_delay: 150 ms after a send at 400 ms, + -- 10 ms after a send at 540 ms. A flush that sent while some of the wait was left would send by 590 ms. + for _, send_at in ipairs({ 400, 540 }) do + it( + ("D: a send %d ms after the handshake waits until connection_wait_delay has passed since the handshake"):format( + send_at + ), + function() + local claude = claude_connects() + claude.handshake() + run(send_at) + send("/project/a.lua") + run(590 - send_at) + assert.same({}, claude.received(), "nothing goes out before 600 ms after the handshake") + + run(20) + assert.same({ "a.lua" }, names(claude.received())) + assert.same({}, errors) + end + ) + end + + it("D: the first ready client sends the queue, though a second client connected later is not ready yet", function() + local first = claude_connects() + first.handshake() + run(500) + local second = claude_connects() + second.handshake() + run(200) + send("/project/a.lua") + -- The first client is ready since 600 ms, the second only at 1100 ms: the flush 50 ms after the send goes out. + run(60) + + assert.same({ "a.lua" }, names(first.received())) + assert.same({ "a.lua" }, names(second.received())) + assert.same({}, errors) + end) + it("D: a Claude whose handshake came 700 ms after its TCP connect still gets connection_wait_delay", function() local claude = claude_connects() run(700)