diff --git a/.agents/skills/verify-diff-lifecycle/covered.lock b/.agents/skills/verify-diff-lifecycle/covered.lock index 0a4b4b91c..774a8fb45 100644 --- a/.agents/skills/verify-diff-lifecycle/covered.lock +++ b/.agents/skills/verify-diff-lifecycle/covered.lock @@ -164,7 +164,7 @@ site lua/claudecode/server/init.lua: if not _G.claude_deferred_responses then @ == lua/claudecode/server/mock.lua file lua/claudecode/server/mock.lua def1248d2793d559 == lua/claudecode/server/tcp.lua -file lua/claudecode/server/tcp.lua 8be1dd96671223ea +file lua/claudecode/server/tcp.lua 610f324845bca7b5 == lua/claudecode/server/utils.lua file lua/claudecode/server/utils.lua 2915ae87b48f04ca == lua/claudecode/terminal.lua diff --git a/.agents/skills/verify-mention-queue/covered.lock b/.agents/skills/verify-mention-queue/covered.lock index 9c7d96c3c..b1fae5d27 100644 --- a/.agents/skills/verify-mention-queue/covered.lock +++ b/.agents/skills/verify-mention-queue/covered.lock @@ -109,7 +109,7 @@ site lua/claudecode/server/init.lua: main_module.process_mention_queue(true) @ f 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 +file lua/claudecode/server/tcp.lua 610f324845bca7b5 block new_connection e1daff4237326df4 block tcp_broadcast 2b207928d69c9dbd block clients_info b2d757e5dc9d2c2f diff --git a/.agents/skills/verify-ws-connection/SKILL.md b/.agents/skills/verify-ws-connection/SKILL.md new file mode 100644 index 000000000..9dae2b1a5 --- /dev/null +++ b/.agents/skills/verify-ws-connection/SKILL.md @@ -0,0 +1,170 @@ +--- +name: verify-ws-connection +description: Model-check the claudecode.nvim WebSocket connection lifecycle (TLA+/TLC) against guards read from the current Lua code, from the TCP accept through the handshake, requests, Close frames, keepalive pings and server stop. Use after a change to lua/claudecode/server/client.lua, server/tcp.lua, server/handshake.lua, the start/stop or callback wiring in server/init.lua, or M.start/M.stop in init.lua, and before trusting such a change. +--- + +# Verify the WebSocket connection lifecycle + +Claude Code talks to the plugin over one WebSocket connection. The plugin must not run a request from a Claude that is gone, must report each disconnect once, must tell Claude why it closes, must not drop a Claude that answers its pings, and must not keep a dead connection or its socket forever. This check explores every order of Claude's frames, hang-ups and stalls, libuv read and write callbacks, ping-timer ticks, scheduled callbacks and server stops in a small model of one connection, with each guard switched on or off to match the code as it is now. + +## Rules + +| Rule | Plain sentence | Harm when broken | +| ------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -------------------------------------------------------------------------------------------------------------------------------------------------- | +| `NoRequestAfterEnd` | A request from Claude runs only after its 101 reply was written, and never after the plugin started to close the connection or saw it end. | A request from a Claude that hung up or closed still changes the editor (opens a diff, moves the cursor), and its answer goes nowhere. | +| `DisconnectReportedOnce` | `on_disconnect` runs at most once per client. | The disconnect cleanup (closing that client's pending diffs) runs twice. | +| `StatusCloseDelivered` | A Close frame for a protocol error (1002, 1003, 1007, 1009) or a server stop (1001) is written before the plugin closes the socket, as long as Claude keeps reading. A Claude whose queue makes no progress for one keepalive window loses the frame to the deadline of `close_client`, which closes the socket (not modeled). | Claude cannot tell a protocol error or a shutdown from a crash: the connection just drops. | +| `NoFalseTimeout` | A Claude that answers each ping before the next tick is never dropped by the ping timer, whatever blocks Neovim or sleeps the machine. A tick only pings and stamps the oldest unanswered ping. The check that drops a client runs after a poll that read the sockets. It judges nothing when its poll came more than 1.5 intervals after its tick, and any bytes the plugin reads from the client clear the stamp. A Claude that stopped once is not covered, and neither is a pong that comes later than one interval: with an unrelated read callback that blocks inside the poll phase and refreshes the loop time, the code closes that client once its ping is 2.5 intervals old (the model has no step for it). A real Claude answers a ping at once. | A Claude that answers each ping before the next tick is disconnected with 1011. | +| `DeadClientDropped` | A client whose Claude hung up or stopped answering, or whose connection the plugin started to close, eventually leaves `server.clients` with its `on_disconnect`. | The plugin keeps counting Claude as connected (`is_claude_connected()`), keeps the unsent writes in memory, and never runs the disconnect cleanup. | +| `DroppedSocketCloses` | Once a client left `server.clients`, or the server stopped, its socket eventually closes, as long as Claude reads again. | The socket stays open, in `CLOSE_WAIT` once Claude hangs up, until Neovim exits: one leaked file descriptor each time. | + +`DeadClientDropped` and `DroppedSocketCloses` are liveness rules ("eventually"). The others hold in every state. TLC reports only the first broken invariant of a run, and a `NoFalseTimeout` break is shorter than any other break, so `check.sh` checks `NoFalseTimeout` in a run of its own (`live-NoFalseTimeout`, written as `[](~falseTimeout)`). A new break of the other three then still shows in the `main` run. + +## Run + +```bash +.agents/skills/verify-ws-connection/check.sh # 2 to 6 min, 4 min at a host load average of 16 +.agents/skills/verify-ws-connection/check.sh --keep # same, keeps the TLC configs and output, prints the dir +.agents/skills/verify-ws-connection/check.sh --mutants # about 80 min at a load average of 14, after you edit the model or a fact +.agents/skills/verify-ws-connection/check.sh --record # rewrite covered.lock, only after "Update after an intended change" (refused together with --mutants) +.agents/skills/verify-ws-connection/check.sh --hash-only # 2 to 30 s, no TLC: only compares covered.lock with the code (exit 0 fresh, 2 error, 3 stale) +``` + +The shared harness `scripts/tla/check-lib.sh` does the work. Its header lists what `check.sh` sets. CI's `covered-lock` job runs every `.agents/skills/verify-*/check.sh` on each pull request, with the TLC jar cached. `Required` does not need that job. On the code as written this check passes, so a broken rule or `STALE` in that job's log for this check is news. + +Needs bash 4 or newer, Java 11 or newer (`JAVA=/path/to/java` overrides), `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. + +## Does the change touch the verified code? + +Run `check.sh --hash-only`. `covered.lock` records a hash of each covered file: `server/client.lua`, `server/tcp.lua`, `server/handshake.lua`, `server/init.lua` and `init.lua`. Any change to one of them reads `STALE` (exit 3) until someone confirms that the model still describes the code. `git log -1 -- .agents/skills/verify-ws-connection/covered.lock` gives the sync commit: the last commit at which someone confirmed the model against the code. Move it forward only by `check.sh --record`, after "Update after an intended change". + +To show where to look, the record also hashes each block the model describes and lists every non-comment line that changes a client's state, writes to or closes its socket, or adds, drops, stops or times out a client, with its enclosing top-level statement. The STALE output prints a `was:`/`now:` pair per changed file, block or line. Covered blocks: + +- In `server/client.lua`: `create_client`, `add_data_frame`, `fail_connection`, `process_data` (handshake, 101 write callback, frames, Close, PONG, the scheduled `on_message` guard), `send_message`, `send_ping`, `close_client`, `abandon_close_frame`. +- In `server/tcp.lua`: `_handle_new_connection` (accept, `read_start`, EOF and read errors), `release_socket`, `_disconnect_client`, `_remove_client`, `stop_server`, `after_next_poll` (the libuv check and idle handles that run a callback after the next poll), `judge_silence` (the keepalive judgement), `drop_client`, `start_ping_timer`. +- In `server/handshake.lua`: `process_handshake`, `extract_http_request`. +- In `server/init.lua`: `M.start` (the callbacks and the ping timer), `M.stop`. +- In `init.lua`: `M.start`, `M.stop` (`:ClaudeCodeStop` and `VimLeavePre` call it). + +A changed file with no changed block or line still needs a look, for example a new caller of `close_client` in another function. A PASS says the model holds for the guards the facts read, on code that matches the record. It does not review a change. STALE never means "probably fine". + +When two branches change the same covered file, `covered.lock` conflicts. Merge `origin/main`, follow "Update after an intended change" on the merged code, run `check.sh --record`, and commit the merge with the new `covered.lock`. + +## Read the result + +`check.sh` prints the code facts first. Each fact is a guard that a regex reads from the source. `TRUE` means the regex found the guard. `FALSE` means the model runs without that guard. A `FALSE` you did not expect is either a removed guard (a bug) or a guard reworded past the regex (a modeling error). A fact reads lines in order, not the structure of the code, so a guard that moves to a place where it no longer guards can still read `TRUE`. The verifiers found three such moves (the `end` of the `DispatchGuard` if above `on_message`, and `abandon_close_frame` with `release_socket` or `drop_client` in the `stop_server` loop). The facts read them now, and the unit tests in `gone_client_spec.lua` and `connection_lifecycle_spec.lua` catch each of them. + +| Fact | Code it reads | +| ---------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | +| `UpgradeInWriteCallback` | `process_data` sets `state = "upgrading"` on a good handshake, and sets `handshake_complete = true` and `state = "connected"` only in the 101 write callback, after `if err or not success` | +| `UpgradeRechecksState` | the 101 write callback returns when `client.state ~= "upgrading" or client.tcp_handle:is_closing()`, before it sets `handshake_complete` | +| `DispatchGuard` | the `vim.schedule`d `on_message` runs only `if client.state == "connected" and not client.tcp_handle:is_closing()` | +| `PeerCloseMarksClosing` | on Claude's Close frame, `process_data` writes the reply Close frame, sets `state = "closing"` and schedules `on_close` | +| `DisconnectOnce` | `_disconnect_client` returns when `server.clients[client.id]` is gone, before `server.on_disconnect` and `_remove_client` | +| `DisconnectClosesSocket` | `_remove_client` clears `server.clients[client.id]` and calls `release_socket`, which closes the handle | +| `UnlistedDisconnectReleases` | `_disconnect_client` calls `release_socket(client)` before it returns for a client that is no longer in `server.clients` | +| `CloseWriteOwnsSocket` | `release_socket` returns without closing while `client.close_pending`. `close_client` sets it before it writes the Close frame, its write callback clears it and closes the handle, and `drop_client` (the keepalive judgement) calls `abandon_close_frame`, which clears it, before `_disconnect_client`, so a timed-out client does not wait for the write | +| `RejectClosesSocket` | the write callback of a rejected handshake calls `on_error`, then closes the handle if it is not closing | +| `ProtocolReportsAtOnce` | each of the two protocol-error closes in `process_data` (a frame that `parse_frame` rejects, a data message that breaks the protocol) calls `fail_connection`, which runs `close_client(client, status, ...)` and then `on_error` without waiting for the Close write; `close_client` has no `on_done` | +| `StopWaitsForCloseWrite` | `stop_server` only calls `close_client(client, 1001, "Server shutting down")`, and closes no client handle itself (it closes the pending poll handles and the server handle): the Close write callback closes the client's handle | +| `KeepaliveReaps` | the ping timer arms `after_next_poll` once for the clients it pinged, and its callback runs `judge_silence(server, pinged, interval * 2.5)`. `judge_silence` drops a listed, connected client whose `ping_unanswered_since` is that old with `drop_client`: `close_client(client, 1011, ...)`, `abandon_close_frame`, then `_disconnect_client(server, client, 1006, ...)`. The model's `Limit` is 3 ticks: the third tick after the stamp | +| `JudgesAfterRead` | the ping timer closes and disconnects nothing. Only the callback that `after_next_poll` runs after a libuv check handle (`vim.loop.new_check()`, `check:start`, then `fn()`) judges and drops | +| `ClockFreshAtTick` | the ping timer calls `vim.loop.update_time()` before `local now = vim.loop.now()` and the wake test (`elapsed = now - last_run`), stamps with that `now` (`since or now`) and takes `tick_time = now`. libuv runs the timers of a pass with the loop time of the start of the pass, and an earlier callback of the pass can have blocked or slept since: a stale `now` hides the wake and stamps a ping with an old time | +| `StampKeepsOldestPing` | the stamp is `since or now`, where `since` is the client's `ping_unanswered_since`: a ping that finds a stamp leaves it, so the stamp is the oldest ping that no pong has answered | +| `BytesClearStamp` | the read callback of `_handle_new_connection` sets `client.ping_unanswered_since = nil` after its EOF check and before `process_data`, so any bytes from the client clear the stamp, not only a PONG | +| `GapSkip` | the callback that `after_next_poll` runs calls `judge_silence` only when `vim.loop.now() - tick_time <= interval * 1.5`: the machine can have slept between the tick and the poll, with Claude | +| `WakeClearsStamp` | after a tick gap above `interval * 1.5`, the ping timer clears `client.ping_unanswered_since` of each connected client, and it sets `last_run = now` each tick | + +On `BROKEN`, the script prints the TLC trace as action names. Each action of `model/WsConnection.tla` names the file and function it models. Read the trace with the pstack `/statechart` skill: + +1. Rerun with `--keep`. +2. Copy the broken run's `.cfg` from the kept dir. Lower `PeerBudget` to 1 (only the upgrade request), then raise it one frame at a time, only until the rule breaks again. Set `MaxSleeps` to 0 unless the path needs a delayed tick (a gap, a stale tick, or a sleep between a tick and its poll: each uses up one of the `MaxSleeps`). Stop at the smallest config that still breaks the rule. +3. Give `/statechart` the kept `WsConnection.tla`, that cfg, and the view `model/statechart-view.ts`. Delete the kept dir when you are done. + +The report tells the path in plain words, for example "Claude connects, the ping timer ticks four times while Claude answers each ping and the plugin reads none, then the ping timer drops Claude for no reply". That is the `NoFalseTimeout` finding below. + +Then decide which kind of failure it is: + +- **Real bug.** A fact went `FALSE` because the change removed or moved a guard, or a fixed finding's path is open again, and the code can take the path. Replay it on the real code (see `replays/`) before you report it, and 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 not (client.state == "connected") or ...`). Fix the regex or the model, run `--mutants`, and say what you changed. + +`--mutants` removes each guard alone and checks each rule alone: each fact must break the rule its `EXPECT` entry names, and each rule must break at least once. One guard is the exception. `RejectClosesSocket` alone breaks no rule, because `_disconnect_client` also closes the socket of a client that left the server, so `--mutants` removes it together with `UnlistedDisconnectReleases`. The environment steps of the bugs this model found (`WindowFullOnProtocolClose`, `StopBeforeOnClose`, `StaleLoopTime`, `PollMissesPong` and `SleepInWindow` in the model) stay on in every run. + +## Bugs this model found + +The first run of this model broke three rules on the code as it was. Each one was replayed on the real code, and PR #455 fixed all three. Reviews of this skill's own PR then found more false timeouts that the first model could not see. PR #479 and PR #488 fixed them, in four rounds (the last three from reviews), and the model describes the final design of #488. + +- **`NoFalseTimeout`.** The ping timer's wake reset touched only `connected` clients, so a Neovim main loop that blocked for more than `interval * 1.5` between the accept and the handshake left the new client with the `last_pong` that `create_client` set at the accept. The timer then dropped a Claude that answered every ping, one interval after its handshake, before any ping reached it. PR #455 made the 101 write callback set `last_pong`. Since #488 a client has no stamp until a tick pings it, so no block between the accept and the handshake can time it out, and the model needs no guard for it. +- **`DeadClientDropped`.** After a protocol error `close_client` queued its Close frame and left `on_error` to the write callback, which runs only once Claude reads again. A Claude with a full receive window kept its client in `server.clients`, `is_claude_connected()` returned `true`, and `on_disconnect` (the diff cleanup) did not run. `process_data` now reports the client at once (`ProtocolReportsAtOnce`). `client.close_pending` keeps `_remove_client` from closing the socket while the Close frame waits, so the frame is still delivered (`CloseWriteOwnsSocket`). +- **`DroppedSocketCloses`.** A server that stopped after Claude's Close frame was read and before the scheduled `on_close` ran dropped the client from `server.clients`, and nothing closed its socket: it stayed in `CLOSE_WAIT`. `_disconnect_client` now closes the socket of a client that is no longer listed (`UnlistedDisconnectReleases`). +- **`NoFalseTimeout`, again (#479).** A tick that Neovim ran late after a block of 1.0 to 1.5 intervals is below the wake threshold (`interval * 1.5`), so `last_pong` was not reset, and the tick can run before the plugin reads Claude's pong. libuv runs timers before it reads sockets. With libuv 1.44, which Neovim 0.8 bundles, that holds after a block in any callback. With newer libuv it holds after a block in a check callback or an I/O read callback, and not after a block in `vim.schedule` or a timer callback, which read the socket first. The tick found the last pong 2.3 intervals old and dropped a Claude that answers every ping. PR #479 pinged again at the first tick that found no pong, and dropped at the second. +- **`NoFalseTimeout`, a third time (#488).** libuv 1.44 runs the timers at the end of a pass of the main loop, after the check handles, and again at the start of the next pass. Neovim runs `vim.schedule` callbacks between the two. A tick at the end of one pass, a block in `vim.schedule`, and a tick at the start of the next ran with no read of Claude's socket between them, and the second tick of #479 dropped a Claude that answered every ping (`replays/two-blocks-before-read.lua`). Any number of ticks can run before a read, so no counter of ticks fixes it. A tick now only pings, and stamps the oldest unanswered ping. The callback of a libuv check handle, which libuv runs after the poll phase that reads the sockets, drops the client whose stamp is two and a half intervals old (`JudgesAfterRead`, `StampKeepsOldestPing`, `WakeClearsStamp`). The model needs no step for a late tick, because its ticks already run at any point between reads. With `JudgesAfterRead` off, `NoFalseTimeout` breaks after a connect, a handshake, and four ticks that Claude answers one by one with no read between them. `StaleLoopTime` is the step for a stamp from the loop time that libuv cached before an earlier callback of the pass blocked. +- **`NoFalseTimeout`, a fourth time (the review of #488).** The check can still run on a poll that does not reach Claude's answer, in two ways. First, Claude writes while Neovim is blocked, and a pong can wait behind more unread data than the socket holds: one poll reads the first part of a large message and stops (`PollMissesPong`). With only a PONG clearing the stamp, `NoFalseTimeout` breaks in the model, and a replay drops Claude after a block of 1.4 intervals twice in a row. The read callback now clears the stamp on any bytes (`BytesClearStamp`): Claude shows it is alive by writing anything. Second, the machine sleeps between a tick and the poll before its check (`SleepInWindow`): Neovim and Claude stop together, the loop time jumps, and Claude answers only after the poll, so no bytes arrive. The check now judges nothing when its poll came more than `interval * 1.5` after its tick (`GapSkip`), and the next tick sees the gap and clears the stamps, as for any wake. Each of the two guards alone leaves one of the two paths open. +- **`NoFalseTimeout`, a fifth time (Codex's review of #488).** The tick read `vim.loop.now()` before it called `vim.loop.update_time()`. libuv runs all timers of a pass with the loop time of the start of the pass, so when an earlier timer callback of the pass blocked for longer than `interval * 1.5`, or the machine slept in it, the tick saw no gap. It kept the stamps of the pings from before the sleep. The check after the poll, which comes right after the tick, then saw a small gap between the tick and the poll and a very old stamp, and dropped a Claude that had no time to answer. The tick now calls `update_time()` first (`ClockFreshAtTick`), sees the wake, and clears the stamps. In the model a `stale` tick is a wake that only a tick with a fresh clock sees (`StaleLoopTime`): with `ClockFreshAtTick` off, `NoFalseTimeout` breaks. There is no replay of this one, because a replay cannot make a timer callback run before the ping timer inside one pass. Two unit tests pin the fix. `ages a ping from when it was sent, though a callback of the pass blocked for half an interval before` turns red when the tick has no `update_time()` and when it comes after `local now = vim.loop.now()` (the stamp and the wake test then read the old time). `takes a tick for a wake when a callback before it in the pass blocked, though the loop time is old` turns red only when `update_time()` comes after the wake test and `now` is read again after it (the stamp is fresh and the wake test saw the old time). + +## Replays + +A replay runs one of these scenarios on the real code, in a headless Neovim with real sockets, the real ping timer at a short interval, and `vim.schedule`. Only Claude is played, by a luv TCP client in the same Neovim (`replays/harness.lua`), or, in `two-blocks-before-read.lua` and `blocks-before-the-poll.lua`, by a second headless Neovim that answers every ping at once (`spawn_claude`, `replays/claude-process.lua`): an in-process Claude answers only when the blocked loop runs again. `gap-during-handshake.lua` and `short-block-after-ping.lua` block the loop for more than one interval too, and use the in-process Claude, so they do not show a Claude that answers during the block. Each replay checks the promise that the fix keeps. Run one from the repo root: + +```bash +.agents/skills/verify-ws-connection/replays/run.sh .lua # NVIM=/path/to/nvim overrides; about 1 to 5 s +``` + +It prints one `KEPT` or `BROKEN` line per check and a count line, and exits 0 only when every check is kept. A check that the host cannot run prints `SKIPPED` and counts as neither kept nor broken: the kernel-state check of `stop-before-on-close.lua` reads `/proc/net/tcp`, so it prints `SKIPPED` on macOS and BSD, and the `is_closing()` check above it still decides. The replays run on Neovim 0.8 and newer, because `run.sh` starts them with `-c`, not `-l`. + +| Replay | Scenario | Promise | +| -------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `gap-during-handshake.lua` | The loop blocks for 700 ms (interval 200 ms) right after the accept, before the read of the upgrade request. | A Claude that answers every ping is pinged, gets no Close frame, and stays listed for 10 intervals. | +| `short-block-after-ping.lua` | One main-loop block of 1.3 intervals (interval 200 ms) starts right after a ping, in a libuv check callback, so the next tick runs before the socket read. Then Claude stops answering. | A Claude that answers every ping is not dropped by the late tick, and stays listed for 1500 ms. A Claude that stops answering is still dropped, with Close 1011. | +| `two-blocks-before-read.lua` | Two blocks of 1.3 intervals in a row, right after a ping: the first in a check callback, the second in `vim.schedule`. Claude runs in a second Neovim and answers every ping. Then Claude stops answering. | A Claude that answers every ping stays listed for 2000 ms: no tick drops it, and the check finds its pongs read. A Claude that stops answering is still dropped, with 1006 `Connection timeout`. On Neovim 0.8 the code of #479 breaks the first promise. | +| `blocks-before-the-poll.lua` | Three runs, each with a fresh plugin and a Claude in a second Neovim. `big-message`: a 2.7-interval block in an idle callback right after a tick, while Claude writes 300 KB and then its pong. `two-blocks`: two blocks of 1.4 intervals (below the gap of 1.5), with the same 300 KB. `sleep`: a 2.7-interval block, and Claude sleeps as long before its answer. | A Claude that answers every ping stays listed in all three. `big-message` needs one of `BytesClearStamp` and `GapSkip`, `two-blocks` needs `BytesClearStamp` (the gap skip with a clear on a PONG only breaks it), and `sleep` needs `GapSkip` (the any-bytes clear without the gap skip breaks it). The code before #488's review (f3576ea) breaks all three, and so does a build with no clear of the stamp at all. The `sleep` run of the any-bytes build without the gap skip depends on timing: on Neovim 0.8.3 it kept all three once and two of three in five repeats. | +| `protocol-close-window-full.lua` | Claude stops reading, the plugin fills its window with 4 MiB messages, and Claude sends a binary frame. | The client is gone from `server.clients`, reported once, and not counted by `is_claude_connected()` while Claude does not read. Its socket stays open for the Close frame, which Claude gets (1003) once it reads, and then the socket closes. | +| `stop-before-on-close.lua` | A libuv check handle calls `server/init.lua` `M.stop` in the same loop turn as the read of Claude's Close frame, before `on_close` runs. | The stop reports no client (`M.stop` rejects the pending diffs itself), and the socket closes: `is_closing()` is true and the kernel does not hold it in `CLOSE_WAIT`. The replay does not show that a typed `:ClaudeCodeStop` can land in that one loop turn. | + +`VimLeavePre` also stops the server, but Neovim exits right after. + +## 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 a client's state, its socket, `server.clients`, the ping timer or the server stop (for example a terminal or diff change in `init.lua`), say so in the PR. Then skip to step 4. +2. If the behavior changed, change the action in `model/WsConnection.tla` that cites that code. If a guard moved, change its fact regex in `check.sh`. If a guard is new, add a fact and its `EXPECT` entry. +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. +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 + +- One connection. Clients share only `server.clients` and the loops of the ping timer and `stop_server`, which treat each client alone. Client ids, the diffs a client owns, and the answers to its `openDiff` calls are checked by `verify-diff-lifecycle`. +- The safety rules run with Claude sending 3 frames, its upgrade request included (pongs and the hang-up come on top), and two delayed ticks (a gap above 1.5 intervals, a stale tick, or a sleep between a tick and its poll): 262,285 states in the joint run and 256,264 in the `NoFalseTimeout` run. The liveness rules run with 2 frames and no delayed tick: 11,701 states each. +- Writes follow libuv. A write goes into the kernel at once when nothing waits in libuv's queue and Claude's window has room. Its callback runs in a later step. Claude's window fills only when the plugin sends a large message while Claude does not read (`PluginSendsLarge`). When Claude reads again, libuv writes the whole queue in one step: the short gap between Claude making room and libuv's next write is not modeled. `uv_close` cancels what waits in the queue and runs the pending callbacks when the close finishes. +- One read carries one frame. `process_data` stops after a Close frame or a protocol error, and drops the bytes of a closing client, so a read of several frames reaches no other state. +- Every plugin step (reads, write callbacks, closes, scheduled callbacks, timer ticks, the poll with its check handles) is fair. Claude is never assumed to act. `DroppedSocketCloses` alone assumes that Claude reads again (`PeerEventuallyReads`). `NoFalseTimeout` alone assumes that a Claude that reads answers each ping before the next tick (`PeerAnswersBeforeTick`), except before a tick after a gap, because the machine slept with Claude. Delayed ticks (a gap, a stale tick) are bounded (`MaxSleeps`), so the timer cannot skip forever. +- Ticks and reads interleave freely: a tick can run before the read of a pong that is already in the socket, however many ticks run in a row. libuv allows fewer orders (two ticks with no read between them), so the model covers every real one. The poll reads every frame that reached the socket before it, or, with `PollMissesPong`, only the first frame of each client. It does not read what Claude sends after it, such as the answer to the ping of the same tick. The poll and the check handles after it are one step of the model. The other callbacks of that pass of the loop (write callbacks, closes) run before or after it. +- Time counts in ticks. A stamp is `Limit` ticks old at the third tick after it. Ticks on time are one interval apart, so `interval * 2.5` is reached 3 intervals after the first unanswered ping. One late tick delays it. Two late ticks in a row, or a poll that a block delays after a tick, can reach it as early as 2.5 intervals, and a tick more than 1.5 intervals after the one before it is a wake that restarts the count. The model does not count the length of a block. `MachineSleeps` stands for a block or a sleep longer than the gap: it marks the loop time as jumped, the next poll's check judges nothing, and the next tick is a wake. Why `2.5` and not `2`: a limit of whole intervals meets the 1 ms resolution of the loop time at exactly the boundary, and the half interval keeps timer jitter from moving the drop. `NoFalseTimeout` holds for any limit above `interval * 1.5`, the window in which a check still judges: the poll that precedes the check reads the pong, and a block inside the poll phase can add at most that much age. A limit of 1.0 to 1.5 intervals passes the model, and real Neovim still drops a Claude that answered in 30 to 100 ms when a read callback blocks about 1.3 intervals in the poll after the tick and refreshes the loop time (the model counts that block as one tick, and a tick as a whole interval). The limit sets how long a silent Claude lives, and how slow an answer can be. +- Not in the rules, on purpose: + - The keepalive Close frame (1011). A Claude whose window is full never gets it, because `_disconnect_client` closes the socket right after `close_client` queues it. `server/README.md` documents it. Claude sees its connection end without a status, and the log shows `Closed client_: no reply for s`. + - The reply to Claude's Close frame. The code makes no promise about it, and it is lost the same way when Claude's window is full: Claude sees the connection end without the reply. + - A connection that never finishes its handshake. The ping timer checks only `connected` clients, so a TCP connection that never sends its upgrade request stays in `server.clients` until it hangs up. The user sees nothing: `is_claude_connected()` counts handshaken clients. No code or doc promises otherwise. + - A client that writes data but never answers a ping. Any bytes clear the stamp, so the ping timer keeps it: it is alive, and the plugin does not judge what it writes. A real Claude answers each ping it reads, so this is a stalled or foreign process. The user sees it as connected (`is_claude_connected()` is true) until it stops reading or hangs up. Before #488 the ping timer dropped it. + - The stall rule of #467 (`judge_stall`), and a client that sends bytes and never reads its socket. Its bytes clear the stamp, so the keepalive never drops it, and the plugin keeps counting it as connected: every message for it waits in libuv's queue, in Neovim's memory. The stall rule runs in the same callback as the keepalive, for a client that answers its pings. It closes a client whose write queue makes no progress at two ticks in a row with 1011 "Not reading", `on_disconnect` gets 1006 "Write queue stalled", and the log shows `Closed client_: not reading for s, KB queued`. Until the kernel's socket buffers are full every write completes and an empty queue counts as progress, so the close comes later than that. The model has no queue size, so it checks the keepalive judgement only. + - The deadline of a Close frame (`start_close_timer` in `close_client`): a socket whose Close frame stays queued for one keepalive window with no progress is closed, and the queue with it. A Claude that never reads cannot hold the socket for good either. The user sees nothing in the log: Claude sees its connection end without the 1001, 1002, 1003, 1007 or 1009 status. The model does not describe the deadline, and keeps its weaker assumption that Claude reads again (`PeerEventuallyReads`). +- Not modeled, with what a user sees if the code gets it wrong: + - Frame encoding and parsing (`server/frame.lua`, unit tests): Claude disconnects with a protocol status (1002, 1003, 1007, 1009), or a request fails to decode (JSON-RPC error -32700). + - Fragmented messages: a request in several frames never runs, or the connection closes with 1007. + - Claude's own pings (the PONG reply is a write with no callback): Claude's ping gets no pong, and Claude can treat the connection as dead. + - The HTTP checks of `handshake.lua` (the model only knows "accepted" or "rejected"): a valid Claude is refused (`Rejected client_: ` at warn level), or a client without the right token is accepted. + - Deferred responses and diffs (`verify-diff-lifecycle`): a diff stays open, or a tool call gets no answer. + - The mention queue that `on_open` starts once a client's handshake completed (it only schedules `process_mention_queue`, and touches no client, socket or timer): an `@` mention reaches Claude late, or the plugin reports a connection timeout and drops the queue. + - The lock file: Claude Code finds no running IDE and does not connect. + - Port selection: `:ClaudeCodeStart` reports `No available ports in range -`. + - A restart (old clients keep the old server object, whose `clients` table is empty): a scheduled callback of the old server finds no client and does nothing. + - Two servers in one Neovim: the plugin starts one server per Neovim. +- Not facts: the closing checks at the top of `process_data` and in its frame loop. Removing one alone breaks no rule, because `DispatchGuard` and `DisconnectOnce` also stop what follows. The checks in the keepalive check callback (`server.clients[client.id] == client` and `client.state == "connected"`) are not facts either: `close_client` and `_disconnect_client` already do nothing for a client that left or is closing, so a check without them differs only by an info line in the log. `drop_client` also calls `abandon_close_frame`, which does nothing for a stamped client: a stamped client has no pending protocol or stop Close frame. +- 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-ws-connection/check.sh b/.agents/skills/verify-ws-connection/check.sh new file mode 100755 index 000000000..3c4533d91 --- /dev/null +++ b/.agents/skills/verify-ws-connection/check.sh @@ -0,0 +1,224 @@ +#!/usr/bin/env bash +# shellcheck disable=SC2034,SC2154 # check-lib.sh reads these variables; covered_block sets the blocks by name +# Model-check the WebSocket connection lifecycle (server/client.lua, server/tcp.lua) 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) +# --hash-only compares covered.lock with the code and runs no TLC: exit 0 fresh, 2 error, 3 stale. +# --record and --hash-only run no TLC, so they do not download it. +# The TLC pin, the option parsing, the TLC runs and the mutant loop live in scripts/tla/check-lib.sh. +here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +SKILL=verify-ws-connection MODEL=WsConnection +source "$here/../../../scripts/tla/check-lib.sh" +tla_init "$@" + +CLIENT=lua/claudecode/server/client.lua +TCP=lua/claudecode/server/tcp.lua +HANDSHAKE=lua/claudecode/server/handshake.lua +SERVER=lua/claudecode/server/init.lua +MAIN=lua/claudecode/init.lua +COVERED=("$CLIENT" "$TCP" "$HANDSHAKE" "$SERVER" "$MAIN") +# A site is a line that changes a client's state, writes to or closes its socket, or adds, drops, stops or +# times out a client. +SITE_RE='(close_client|_disconnect_client|_remove_client|stop_server|start_ping_timer|send_ping|drop_client|judge_silence|after_next_poll|tcp_handle:(write|close|read_start)|write\(client, |handle:close\(\)|client\.state = |handshake_complete = |last_pong = |ping_unanswered_since = |server\.clients\[|server\.stop\(\)|ping_timer:)' + +covered_block create_client "$CLIENT" '^function M\.create_client\(' +covered_block add_data_frame "$CLIENT" '^local function add_data_frame\(' +covered_block process_data "$CLIENT" '^function M\.process_data\(' +covered_block send_message "$CLIENT" '^function M\.send_message\(' +covered_block send_ping "$CLIENT" '^function M\.send_ping\(' +covered_block fail_connection "$CLIENT" '^local function fail_connection\(' +covered_block close_client "$CLIENT" '^function M\.close_client\(' +covered_block abandon_close_frame "$CLIENT" '^function M\.abandon_close_frame\(' +covered_block new_connection "$TCP" '^function M\._handle_new_connection\(' +covered_block release_socket "$TCP" '^local function release_socket\(' +covered_block disconnect "$TCP" '^function M\._disconnect_client\(' +covered_block remove_client "$TCP" '^function M\._remove_client\(' +covered_block stop_server "$TCP" '^function M\.stop_server\(' +covered_block after_next_poll "$TCP" '^local function after_next_poll\(' +covered_block drop_client "$TCP" '^local function drop_client\(' +covered_block judge_silence "$TCP" '^local function judge_silence\(' +covered_block ping_timer "$TCP" '^function M\.start_ping_timer\(' +covered_block process_handshake "$HANDSHAKE" '^function M\.process_handshake\(' +covered_block extract_request "$HANDSHAKE" '^function M\.extract_http_request\(' +covered_block server_start "$SERVER" '^function M\.start\(' +covered_block server_stop "$SERVER" '^function M\.stop\(\)' +covered_block main_start "$MAIN" '^function M\.start\(' +covered_block main_stop "$MAIN" '^function M\.stop\(\)' + +FACTS=(UpgradeInWriteCallback UpgradeRechecksState DispatchGuard PeerCloseMarksClosing + DisconnectOnce DisconnectClosesSocket UnlistedDisconnectReleases CloseWriteOwnsSocket RejectClosesSocket + ProtocolReportsAtOnce StopWaitsForCloseWrite KeepaliveReaps JudgesAfterRead ClockFreshAtTick StampKeepsOldestPing + BytesClearStamp GapSkip WakeClearsStamp) + +# The handshake completes in the 101 write callback, after its error check, and nowhere before. +upgrade_in_write_callback() { + [[ $(grep -c 'client\.handshake_complete = true' <<<"$process_data") == 1 ]] && + in_order '^ *if success then$' '^ *client\.state = "upgrading"$' \ + '^ *write\(client, response_from_handshake, function\(err\)$' '^ *if err or not success then$' \ + '^ *client\.handshake_complete = true$' '^ *client\.state = "connected"$' <<<"$process_data" +} +fact[UpgradeInWriteCallback]=$(as_bool upgrade_in_write_callback) +fact[UpgradeRechecksState]=$(as_bool in_order 'write\(client, response_from_handshake, function\(err\)$' \ + '^ *if client\.state ~= "upgrading" or client\.tcp_handle:is_closing\(\) then$' '^ *return$' \ + '^ *client\.handshake_complete = true$' <<<"$process_data") +# The scheduled on_message sits inside the guard: the end of the if follows it at once. +dispatch_guard() { + in_order '^ *vim\.schedule\(function\(\)$' \ + '^ *if client\.state == "connected" and not client\.tcp_handle:is_closing\(\) then$' \ + '^ *on_message\(client, message\)$' <<<"$process_data" && + grep -A1 -E '^ *on_message\(client, message\)$' <<<"$process_data" | grep -qE '^ *end$' +} +fact[DispatchGuard]=$(as_bool dispatch_guard) +fact[PeerCloseMarksClosing]=$(as_bool in_order 'elseif opcode == frame\.OPCODE\.CLOSE then$' \ + '^ *if client\.state == "connected" then$' '^ *write\(client, close_frame\)$' \ + '^ *client\.state = "closing"$' '^ *on_close\(client, code, reason\)$' <<<"$process_data") +fact[DisconnectOnce]=$(as_bool in_order '^ if not server\.clients\[client\.id\] then$' '^ return$' \ + '^ server\.on_disconnect\(client, code, reason\)$' '^ M\._remove_client\(server, client\)$' <<<"$disconnect") +# _remove_client clears the client and releases its socket, and release_socket closes the handle. +disconnect_closes_socket() { + in_order '^ if server\.clients\[client\.id\] then$' '^ server\.clients\[client\.id\] = nil$' \ + '^ release_socket\(client\)$' <<<"$remove_client" && + in_order '^ client\.tcp_handle:close\(\)$' <<<"$release_socket" +} +fact[DisconnectClosesSocket]=$(as_bool disconnect_closes_socket) +# _disconnect_client releases the socket of a client that is no longer listed before it returns. +fact[UnlistedDisconnectReleases]=$(as_bool in_order '^ if not server\.clients\[client\.id\] then$' \ + '^ release_socket\(client\)$' '^ return$' <<<"$disconnect") +# release_socket leaves a handle alone while the Close write callback will close it. close_client sets close_pending +# before it writes the frame, and its write callback clears it and closes the handle. drop_client (the keepalive +# check) calls abandon_close_frame, which clears it too, so that a timed-out client does not wait for the write. +close_write_owns_socket() { + in_order '^local function release_socket\(client\)$' \ + '^ if client\.close_pending or client\.tcp_handle:is_closing\(\) then$' '^ return$' \ + '^ client\.tcp_handle:close\(\)$' <<<"$release_socket" && + in_order '^ client\.close_pending = true$' '^ write\(client, close_frame, function\(\)$' \ + '^ client\.close_pending = nil$' '^ client\.state = "closed"$' '^ client\.tcp_handle:close\(\)$' \ + <<<"$close_client" && + in_order '^ client_manager\.close_client\(client, 1011, close_reason\)$' \ + '^ client_manager\.abandon_close_frame\(client\)$' '^ M\._disconnect_client\(server, client, 1006, disconnect_reason\)$' \ + <<<"$drop_client" && + in_order '^function M\.abandon_close_frame\(client\)$' '^ client\.close_pending = nil$' <<<"$abandon_close_frame" +} +fact[CloseWriteOwnsSocket]=$(as_bool close_write_owns_socket) +fact[RejectClosesSocket]=$(as_bool in_order '^ *if err or not success then$' '^ *on_error\(client, ' \ + '^ *if not client\.tcp_handle:is_closing\(\) then$' '^ *client\.tcp_handle:close\(\)$' '^ *return$' \ + <<<"$process_data") +# Each of the two protocol-error closes in process_data (a frame that parse_frame rejects, a data message that breaks the +# protocol) goes through fail_connection, which closes with the status and then calls on_error at once. close_client +# has no on_done. +protocol_reports_at_once() { + [[ $(grep -cE '^ *fail_connection\(client, [^)]*, on_error\)$' <<<"$process_data") == 2 ]] && + in_order '^local function fail_connection\(client, status, problem, on_error\)$' \ + '^ M\.close_client\(client, status, CLOSE_REASONS\[status\]\)$' '^ on_error\(client, problem\)$' \ + <<<"$fail_connection" && + ! grep -q 'on_done' <<<"$close_client" +} +fact[ProtocolReportsAtOnce]=$(as_bool protocol_reports_at_once) +# stop_server only calls close_client for each client: the Close write callback closes the socket. +stop_waits_for_close_write() { + grep -qE '^ client_manager\.close_client\(client, 1001, "Server shutting down"\)$' <<<"$stop_server" && + ! grep -qE 'tcp_handle|_remove_client|_disconnect_client|release_socket|abandon_close_frame|drop_client' <<<"$stop_server" && + in_order '^ write\(client, close_frame, function\(\)$' '^ client\.tcp_handle:close\(\)$' \ + <<<"$close_client" +} +fact[StopWaitsForCloseWrite]=$(as_bool stop_waits_for_close_write) +# The ping timer pings each connected client, collects it in pinged, and arms after_next_poll once for the clients it +# pinged. The callback runs judge_silence with a limit of interval * 2.5 (the third tick after the stamp, the model's +# Limit). judge_silence drops a client that is still listed and connected and whose stamp is that old, with drop_client: +# close_client(1011), abandon_close_frame, _disconnect_client(1006). +keepalive_reaps() { + in_order '^ client_manager\.send_ping\(client, "ping"\)$' '^ table\.insert\(pinged, client\)$' \ + '^ if #pinged > 0 then$' '^ after_next_poll\(server, function\(\)$' \ + '^ judge_silence\(server, pinged, interval \* 2\.5\)$' <<<"$ping_timer" && + in_order '^local function judge_silence\(server, clients, limit\)$' '^ local now = vim\.loop\.now\(\)$' \ + '^ for _, client in ipairs\(clients\) do$' '^ local since = client\.ping_unanswered_since$' \ + '^ if server\.clients\[client\.id\] == client and client\.state == "connected" and since and now - since >= limit then$' \ + '^ drop_client\(server, client, "Keepalive timeout", "Connection timeout"\)$' <<<"$judge_silence" && + in_order '^ client_manager\.close_client\(client, 1011, close_reason\)$' \ + '^ client_manager\.abandon_close_frame\(client\)$' '^ M\._disconnect_client\(server, client, 1006, disconnect_reason\)$' <<<"$drop_client" +} +fact[KeepaliveReaps]=$(as_bool keepalive_reaps) +# Only the callback that after_next_poll runs after a libuv check handle drops a client: libuv runs the check handle after +# the poll phase that reads the sockets. The timer callback closes and disconnects nothing, and arms the callback for the +# clients it pinged. +# judge_silence has one call in the timer callback, the one inside the callback that after_next_poll runs, and +# after_next_poll calls fn once, from the callback of its check handle. +judges_after_read() { + ! { grep -vE '^ *--' <<<"$ping_timer" | grep -qE 'close_client|_disconnect_client|drop_client'; } && + [[ $(grep -vE '^ *--' <<<"$ping_timer" | grep -c 'judge_silence(') == 1 ]] && + in_order '^ local check = vim\.loop\.new_check\(\)$' '^ check:start\(function\(\)$' '^ fn\(\)$' <<<"$after_next_poll" && + [[ $(grep -vE '^ *--' <<<"$after_next_poll" | grep -c 'fn()') == 1 ]] +} +fact[JudgesAfterRead]=$(as_bool judges_after_read) +# The tick calls update_time before it reads the clock for the wake test, the stamp and the gap: libuv runs the timers of a +# pass with the loop time of the start of the pass, and a callback that ran earlier in the pass can have blocked since, +# or the machine can have slept in it. +fact[ClockFreshAtTick]=$(as_bool in_order '^ vim\.loop\.update_time\(\)$' '^ local now = vim\.loop\.now\(\)$' \ + '^ local elapsed = now - last_run$' '^ client\.ping_unanswered_since = since or now$' '^ local tick_time = now$' <<<"$ping_timer") +# A ping that finds a stamp leaves it, so the stamp is the oldest ping that no pong has answered. +stamp_keeps_oldest_ping() { + in_order '^ local since = client\.ping_unanswered_since$' '^ client\.ping_unanswered_since = since or now$' <<<"$ping_timer" +} +fact[StampKeepsOldestPing]=$(as_bool stamp_keeps_oldest_ping) +# Any bytes that the read callback gets clear the stamp, before process_data runs: a pong can wait behind more unread data +# than the socket holds, and one poll does not reach it. +fact[BytesClearStamp]=$(as_bool in_order '^ client_tcp:read_start\(function\(err, data\)$' '^ if not data then$' \ + '^ client\.ping_unanswered_since = nil$' '^ client_manager\.process_data\(client, data, ' <<<"$new_connection") +# The callback judges the silence only when its loop time is at most interval * 1.5 after its tick: the machine can have +# slept between the tick and the poll, and Claude with it. +fact[GapSkip]=$(as_bool in_order '^ local tick_time = now$' '^ after_next_poll\(server, function\(\)$' \ + '^ if vim\.loop\.now\(\) - tick_time <= interval \* 1\.5 then$' '^ judge_silence\(server, pinged, interval \* 2\.5\)$' \ + '^ end$' '^ for _, client in ipairs\(stalled\) do$' <<<"$ping_timer") +fact[WakeClearsStamp]=$(as_bool in_order '^ local is_wake_from_sleep = elapsed > \(interval \* 1\.5\)$' \ + '^ if is_wake_from_sleep then$' '^ for _, client in pairs\(server\.clients\) do$' '^ if client\.state == "connected" then$' \ + '^ client\.ping_unanswered_since = nil$' '^ last_run = now$' <<<"$ping_timer") + +# NoFalseTimeout is a safety rule, but it runs alone (as [](~falseTimeout)): TLC stops at the first broken invariant +# of a run, and its known finding is shorter than any break of the other three. +RULES=(NoRequestAfterEnd DisconnectReportedOnce StatusCloseDelivered) +LIVE=(NoFalseTimeout DeadClientDropped DroppedSocketCloses) +EXPECT=( + [UpgradeInWriteCallback]=NoRequestAfterEnd [UpgradeRechecksState]=NoRequestAfterEnd + [DispatchGuard]=NoRequestAfterEnd [PeerCloseMarksClosing]=NoRequestAfterEnd + [DisconnectOnce]=DisconnectReportedOnce + [CloseWriteOwnsSocket]=StatusCloseDelivered [StopWaitsForCloseWrite]=StatusCloseDelivered + [BytesClearStamp]=NoFalseTimeout [GapSkip]=NoFalseTimeout [WakeClearsStamp]=NoFalseTimeout [ClockFreshAtTick]=NoFalseTimeout + [JudgesAfterRead]=NoFalseTimeout [StampKeepsOldestPing]=DeadClientDropped + [KeepaliveReaps]=DeadClientDropped [ProtocolReportsAtOnce]=DeadClientDropped + [DisconnectClosesSocket]=DroppedSocketCloses [UnlistedDisconnectReleases]=DroppedSocketCloses + ["RejectClosesSocket+UnlistedDisconnectReleases"]=DroppedSocketCloses +) +MUTANT_NOTES=(" RejectClosesSocket alone is caught by no rule: _disconnect_client also closes the socket of a client that left the server.") + +# Safety rules: one connection, Claude sends 3 frames (its upgrade request included), two delayed ticks (a gap above +# 1.5 intervals, a tick in a pass that an earlier callback blocked, or a sleep between a tick and its poll). Liveness +# rules: 2 frames and no delayed tick. A run takes 25 to 165 s (main 24 s, NoFalseTimeout 31 s, the two liveness runs +# 120 s and 162 s at a host load average of 7 to 20). DroppedSocketCloses alone assumes that Claude reads again. +# NoFalseTimeout alone assumes that a Claude that reads answers a ping before the next tick. +tla_constants() { + local reads=FALSE answers=FALSE + [[ $1 != *DroppedSocketCloses ]] || reads=TRUE + [[ $1 != *NoFalseTimeout ]] || answers=TRUE + echo " Conns = {c1}" + case $1 in + *DeadClientDropped | *DroppedSocketCloses) + echo " PeerBudget = 2" + echo " MaxSleeps = 0" + ;; + *) + echo " PeerBudget = 3" + echo " MaxSleeps = 2" + ;; + esac + echo " PeerEventuallyReads = $reads" + echo " PeerAnswersBeforeTick = $answers" + # The environment steps of the bugs this model found. Every run allows them, so that a removed guard breaks a rule. + echo " WindowFullOnProtocolClose = TRUE" + echo " StopBeforeOnClose = TRUE" + echo " StaleLoopTime = TRUE" + echo " PollMissesPong = TRUE" + echo " SleepInWindow = TRUE" +} + +tla_main "$@" diff --git a/.agents/skills/verify-ws-connection/covered.lock b/.agents/skills/verify-ws-connection/covered.lock new file mode 100644 index 000000000..fa1f85d19 --- /dev/null +++ b/.agents/skills/verify-ws-connection/covered.lock @@ -0,0 +1,106 @@ +== lua/claudecode/init.lua +file lua/claudecode/init.lua db4b58226c39fd20 +block main_start 7bf331d94d09a034 +block main_stop d754def6d5865650 +site lua/claudecode/init.lua: local success, error = M.state.server.stop() @ function M.stop() +site lua/claudecode/init.lua: server.stop() @ function M.start(show_startup_notification) +site lua/claudecode/init.lua: server.stop() @ function M.start(show_startup_notification) +== lua/claudecode/server/client.lua +file lua/claudecode/server/client.lua b8165df16f194471 +block create_client 24fa2a266b76e6ad +block add_data_frame 69425d49d1ca87c9 +block process_data 309347512099d250 +block send_message 4224f2da335cf996 +block send_ping d1b988ea53693ebd +block fail_connection 70123c02ed0a9b33 +block close_client 1deaceaa4a8a1684 +block abandon_close_frame c89fb13480726345 +site lua/claudecode/server/client.lua: M.close_client(client, status, CLOSE_REASONS[status]) @ local function fail_connection(client, status, problem, on_error) +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: client.last_pong = 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.state = "closed" @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: client.state = "closed" @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: client.state = "closed" @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: client.state = "closed" @ local function start_close_timer(client) +site lua/claudecode/server/client.lua: client.state = "closing" @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: client.state = "closing" @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: client.state = "closing" @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: client.state = "connected" @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: client.state = "upgrading" @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: client.tcp_handle:close() @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: client.tcp_handle:close() @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: client.tcp_handle:close() @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: client.tcp_handle:write(data:sub(first, first + WRITE_PIECE_BYTES - 1), last_piece and callback or nil) @ local function write(client, data, callback) +site lua/claudecode/server/client.lua: function M.close_client(client, code, reason) @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: function M.send_ping(client, data) @ function M.send_ping(client, data) +site lua/claudecode/server/client.lua: handle:close() @ local function start_close_timer(client) +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: last_pong = client.last_pong, @ function M.get_client_info(client) +site lua/claudecode/server/client.lua: last_pong = vim.loop.now(), @ function M.create_client(tcp_handle, keepalive_timeout) +site lua/claudecode/server/client.lua: local function write(client, data, callback) @ local function write(client, data, callback) +site lua/claudecode/server/client.lua: local queued, err = write(client, text_frame, callback) @ function M.send_message(client, message, callback) +site lua/claudecode/server/client.lua: return client.tcp_handle:write(data, callback) @ local function write(client, data, callback) +site lua/claudecode/server/client.lua: write(client, close_frame) @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: write(client, close_frame, function() @ function M.close_client(client, code, reason) +site lua/claudecode/server/client.lua: write(client, ping_frame) @ function M.send_ping(client, data) +site lua/claudecode/server/client.lua: write(client, pong_frame) @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +site lua/claudecode/server/client.lua: write(client, response_from_handshake, function(err) @ function M.process_data(client, data, on_message, on_close, on_error, auth_token, on_open) +== lua/claudecode/server/handshake.lua +file lua/claudecode/server/handshake.lua 3eca35d572094a55 +block process_handshake 46341209ae5ab06a +block extract_request 936e9a8b79d36106 +== lua/claudecode/server/init.lua +file lua/claudecode/server/init.lua dbc9b57cf9a7142b +block server_start 5eb961f0e8934ed0 +block server_stop 506e2e53358dc947 +site lua/claudecode/server/init.lua: M.state.ping_timer = tcp_server.start_ping_timer(server, 30000) -- Start ping timer to keep connections alive @ function M.start(config, auth_token) +site lua/claudecode/server/init.lua: M.state.ping_timer:close() @ function M.stop() +site lua/claudecode/server/init.lua: M.state.ping_timer:stop() @ function M.stop() +site lua/claudecode/server/init.lua: tcp_server.stop_server(M.state.server) @ function M.stop() +== lua/claudecode/server/tcp.lua +file lua/claudecode/server/tcp.lua 610f324845bca7b5 +block new_connection e1daff4237326df4 +block release_socket de7e50701ce4c83d +block disconnect 122662fc03352d6b +block remove_client b69196261758008d +block stop_server c4c96c6a0a8ecb6f +block after_next_poll f2b0a81f5d8c7b68 +block drop_client 6f41015bdc3839cc +block judge_silence 7761c3cdd58d9ed2 +block ping_timer 470f05d0f7ce1098 +site lua/claudecode/server/tcp.lua: M._disconnect_client(server, cl, 1006, "Client error: " .. error_msg) @ function M._handle_new_connection(server) +site lua/claudecode/server/tcp.lua: M._disconnect_client(server, cl, code, reason) @ function M._handle_new_connection(server) +site lua/claudecode/server/tcp.lua: M._disconnect_client(server, client, 1006, "Client read error: " .. err) @ function M._handle_new_connection(server) +site lua/claudecode/server/tcp.lua: M._disconnect_client(server, client, 1006, "EOF") @ function M._handle_new_connection(server) +site lua/claudecode/server/tcp.lua: M._disconnect_client(server, client, 1006, disconnect_reason) @ local function drop_client(server, client, close_reason, disconnect_reason) +site lua/claudecode/server/tcp.lua: M._remove_client(server, client) @ function M._disconnect_client(server, client, code, reason) +site lua/claudecode/server/tcp.lua: after_next_poll(server, function() @ function M.start_ping_timer(server, interval) +site lua/claudecode/server/tcp.lua: client.ping_unanswered_since = nil @ function M._handle_new_connection(server) +site lua/claudecode/server/tcp.lua: client.ping_unanswered_since = nil @ function M.start_ping_timer(server, interval) +site lua/claudecode/server/tcp.lua: client.ping_unanswered_since = since or now @ function M.start_ping_timer(server, interval) +site lua/claudecode/server/tcp.lua: client.tcp_handle:close() @ local function release_socket(client) +site lua/claudecode/server/tcp.lua: client_manager.close_client(client, 1001, "Server shutting down") @ function M.stop_server(server) +site lua/claudecode/server/tcp.lua: client_manager.close_client(client, 1011, close_reason) @ local function drop_client(server, client, close_reason, disconnect_reason) +site lua/claudecode/server/tcp.lua: client_manager.send_ping(client, "ping") @ function M.start_ping_timer(server, interval) +site lua/claudecode/server/tcp.lua: drop_client(server, client, "Keepalive timeout", "Connection timeout") @ local function judge_silence(server, clients, limit) +site lua/claudecode/server/tcp.lua: drop_client(server, client, "Not reading", "Write queue stalled") @ local function judge_stall(server, client) +site lua/claudecode/server/tcp.lua: function M._disconnect_client(server, client, code, reason) @ function M._disconnect_client(server, client, code, reason) +site lua/claudecode/server/tcp.lua: function M._remove_client(server, client) @ function M._remove_client(server, client) +site lua/claudecode/server/tcp.lua: function M.start_ping_timer(server, interval) @ function M.start_ping_timer(server, interval) +site lua/claudecode/server/tcp.lua: function M.stop_server(server) @ function M.stop_server(server) +site lua/claudecode/server/tcp.lua: handle:close() @ function M._bind_and_listen(server, port) +site lua/claudecode/server/tcp.lua: handle:close() @ function M._bind_and_listen(server, port) +site lua/claudecode/server/tcp.lua: handle:close() @ local function after_next_poll(server, fn) +site lua/claudecode/server/tcp.lua: handle:close() @ local function close_pending_polls(server) +site lua/claudecode/server/tcp.lua: if not server.clients[client.id] then @ function M._disconnect_client(server, client, code, reason) +site lua/claudecode/server/tcp.lua: if server.clients[client.id] == client and client.state == "connected" and since and now - since >= limit then @ local function judge_silence(server, clients, limit) +site lua/claudecode/server/tcp.lua: if server.clients[client.id] then @ function M._remove_client(server, client) +site lua/claudecode/server/tcp.lua: if server.clients[client.id] ~= client or client.state ~= "connected" then @ local function judge_stall(server, client) +site lua/claudecode/server/tcp.lua: judge_silence(server, pinged, interval * 2.5) @ function M.start_ping_timer(server, interval) +site lua/claudecode/server/tcp.lua: local client = server.clients[client_id] @ function M.send_to_client(server, client_id, message, callback) +site lua/claudecode/server/tcp.lua: local function after_next_poll(server, fn) @ local function after_next_poll(server, fn) +site lua/claudecode/server/tcp.lua: local function drop_client(server, client, close_reason, disconnect_reason) @ local function drop_client(server, client, close_reason, disconnect_reason) +site lua/claudecode/server/tcp.lua: local function judge_silence(server, clients, limit) @ local function judge_silence(server, clients, limit) +site lua/claudecode/server/tcp.lua: server.clients[client.id] = client @ function M._handle_new_connection(server) +site lua/claudecode/server/tcp.lua: server.clients[client.id] = nil @ function M._remove_client(server, client) diff --git a/.agents/skills/verify-ws-connection/model/WsConnection.tla b/.agents/skills/verify-ws-connection/model/WsConnection.tla new file mode 100644 index 000000000..3d565bc23 --- /dev/null +++ b/.agents/skills/verify-ws-connection/model/WsConnection.tla @@ -0,0 +1,603 @@ +--------------------------- MODULE WsConnection --------------------------- +(***************************************************************************) +(* The life of one WebSocket connection to the claudecode.nvim server. *) +(* *) +(* Claude connects over TCP, sends its HTTP upgrade request, gets the 101 *) +(* reply, then sends requests and answers the plugin's pings. It can hang *) +(* up, send a Close frame or a frame that breaks the protocol, or stop *) +(* reading. The plugin can stop the server, and its ping timer drops a *) +(* client that no longer answers: each tick pings and stamps the oldest *) +(* unanswered ping, and a libuv check handle, which libuv runs after the *) +(* poll phase that reads the sockets, drops the client whose ping is old. *) +(* *) +(* One step of the model is one indivisible step of the code: a libuv read *) +(* callback, a libuv write callback, the libuv close of a handle (which *) +(* runs the pending write callbacks), a ping-timer tick, one vim.schedule'd *) +(* closure, a poll phase with the check handles that follow it, or a *) +(* main-loop command such as :ClaudeCodeStop. *) +(* *) +(* Writes follow libuv: uv_write puts the bytes into the kernel at once *) +(* when nothing waits in the handle's write queue and the peer's receive *) +(* window has room; its callback still runs in a later step. Otherwise the *) +(* write waits in libuv's queue, and uv_close cancels it. *) +(* *) +(* Code facts (BOOLEAN constants) are read from the source by check.sh: *) +(* TRUE means the guard is in the code, FALSE models the code without it. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + Conns, \* TCP connections the listener accepts (model values) + PeerBudget, \* frames Claude sends on one connection, its upgrade request included (pongs and the hang-up not counted) + MaxSleeps, \* how many ping-timer ticks run delayed: after a gap above interval * 1.5 (Neovim suspended or blocked), or stale + PeerEventuallyReads, \* assumption, not a code fact: Claude never stops reading for good + PeerAnswersBeforeTick, \* assumption, not a code fact: a Claude that is reading answers a ping before the next tick. TRUE only in + \* the NoFalseTimeout run, which is about a Claude that answers every ping + \* Environment switches, not code facts. Each one allows the step of one bug this model found (see SKILL.md, "Bugs + \* this model found"). They are TRUE in every run, so that a removed guard breaks the rule that its bug broke. + WindowFullOnProtocolClose, \* the plugin can read a frame that breaks the protocol while Claude's window is full + StopBeforeOnClose, \* the server can stop between a Close frame from Claude and its scheduled on_close + StaleLoopTime, \* a tick can run in a pass of the main loop whose earlier callback blocked or slept for longer than the + \* limit: libuv caches the loop time when the pass starts, so the tick sees no gap + PollMissesPong, \* a poll can read the first frame of a client and stop: Claude wrote a large message while Neovim was + \* blocked, and its pong waits behind more unread data than the socket holds + SleepInWindow, \* the machine can sleep between a tick and the poll that precedes its check: Neovim and Claude stop + \* together, so the loop time jumps and Claude's pong comes only after the poll + + \* Code facts, see check.sh for the source lines each one reads. + UpgradeInWriteCallback, \* client.lua process_data: `connected` and handshake_complete are set in the 101 write callback + UpgradeRechecksState, \* client.lua 101 write callback: returns when the state is no longer "upgrading" or the handle closes + DispatchGuard, \* client.lua process_data: the scheduled on_message runs only for a connected client with an open handle + PeerCloseMarksClosing, \* client.lua process_data: a Close frame from Claude sets the state to "closing" + DisconnectOnce, \* tcp.lua _disconnect_client returns when the client is no longer in server.clients + DisconnectClosesSocket, \* tcp.lua _remove_client closes the client's TCP handle (release_socket) + UnlistedDisconnectReleases, \* tcp.lua _disconnect_client closes the handle of a client that is no longer in server.clients + CloseWriteOwnsSocket, \* tcp.lua release_socket leaves a handle alone while client.close_pending: its Close write callback closes it + RejectClosesSocket, \* client.lua: the write callback of a rejected handshake closes the handle + ProtocolReportsAtOnce, \* client.lua fail_connection: a protocol error runs close_client, then on_error, without waiting for the write + StopWaitsForCloseWrite, \* tcp.lua stop_server only calls close_client; the Close write callback closes the handle + KeepaliveReaps, \* tcp.lua judge_silence drops (drop_client) a connected client whose oldest ping is old + JudgesAfterRead, \* tcp.lua: only the callback that after_next_poll runs after a libuv check handle drops a client, never the tick + ClockFreshAtTick, \* tcp.lua ping timer: calls vim.loop.update_time() before it reads the clock for the wake test, the stamp and the gap + StampKeepsOldestPing, \* tcp.lua ping timer: a ping that finds a stamp leaves it, so the stamp is the oldest unanswered ping + BytesClearStamp, \* tcp.lua read callback: any bytes read from a client clear client.ping_unanswered_since + GapSkip, \* tcp.lua ping timer: the callback judges nothing when its loop time is more than interval * 1.5 + \* after its tick + WakeClearsStamp \* tcp.lua ping timer: after a tick gap above interval * 1.5, each client's stamp is cleared + +None == "none" +Frames == {"hello", "badhello", "req", "pong", "close", "bad", "eof"} +Limit == 3 \* ticks after the stamp at which the oldest ping is old enough to drop: interval * 2.5 is the third tick after it +States == {"none", "connecting", "upgrading", "connected", "closing", "closed"} +CbKinds == {"101", "reject", "close"} \* writes whose libuv callback does something +Min(a, b) == IF a < b THEN a ELSE b +Range(s) == {s[i] : i \in DOMAIN s} + +VARIABLES + st, \* client.state; "none" until the listener accepts the connection + hs, \* client.handshake_complete + listed, \* the client is in server.clients + handle, \* the client's TCP handle: "none", "open", "closing" (uv_close called, write callbacks pending), "closed" + kern, \* writes the kernel took (or that failed) whose libuv callback has not run: sequence of [k, err] + queued, \* writes waiting in libuv's queue because Claude's receive window is full + closeWhy, \* why close_client wrote this client's Close frame: None, "protocol", "keepalive" or "stop". With st = "closing" + \* it is client.close_pending, except for "keepalive": the ping timer clears close_pending + buf, \* frames read while the 101 reply is written (client.buffer) + sched, \* the vim.schedule queue (FIFO), records [c, k] + stamped, \* client.ping_unanswered_since is set: a ping went unanswered + age, \* ping-timer ticks since that stamp, up to Limit + pend, \* a tick pinged this client, and the check handle that it started has not run + jumped, \* the loop time jumped since the last tick (the machine slept): the next tick sees a gap above interval * 1.5 + peer, \* Claude's side: "idle", "live" (never stopped), "silent" (stopped reading and answering), "stuck" (silent, window + \* full), "resumed" (read again after it was silent), "gone" + inq, \* frames Claude sent that the plugin has not read yet + sent, \* frames Claude has sent (PeerBudget bounds it) + pingOut, \* a ping reached Claude and Claude has not answered it yet + serverUp, \* the server and its ping timer run + sleeps, \* delayed ticks so far (after a gap above interval * 1.5, or stale) + \* ghosts: what the rules read + upgraded, \* the 101 reply was written without error + ended, \* the plugin started to close this connection, or saw it end + reports, \* on_disconnect calls for this client + badDispatch, \* a request ran before its 101 reply was written, or after its connection ended + dropped, \* a Close frame for a protocol error or a server stop was cancelled by closing the handle + falseTimeout \* the ping timer dropped a client whose Claude never stopped answering + +vars == <> +env == <> + +(* The plugin-side state as a record, so that a step that runs several *) +(* functions in a row can chain the operators below. *) +W == [st |-> st, hs |-> hs, listed |-> listed, handle |-> handle, kern |-> kern, queued |-> queued, + closeWhy |-> closeWhy, buf |-> buf, sched |-> sched, stamped |-> stamped, age |-> age, pend |-> pend, + jumped |-> jumped, pingOut |-> pingOut, upgraded |-> upgraded, ended |-> ended, reports |-> reports, badDispatch |-> badDispatch, + dropped |-> dropped, falseTimeout |-> falseTimeout] + +SetW(w) == + /\ st' = w.st /\ hs' = w.hs /\ listed' = w.listed /\ handle' = w.handle /\ kern' = w.kern + /\ queued' = w.queued /\ closeWhy' = w.closeWhy /\ buf' = w.buf /\ sched' = w.sched /\ stamped' = w.stamped + /\ age' = w.age /\ pend' = w.pend /\ jumped' = w.jumped + /\ pingOut' = w.pingOut /\ upgraded' = w.upgraded /\ ended' = w.ended + /\ reports' = w.reports /\ badDispatch' = w.badDispatch /\ dropped' = w.dropped /\ falseTimeout' = w.falseTimeout + +(* tcp_handle:write(data, cb). k is "101", "reject" or "close" (a callback *) +(* that does something), or "echo", "ping", "data" (no callback). A write on *) +(* a handle that is closing fails at once and its callback never runs. *) +Write(w, c, k) == + IF w.handle[c] # "open" THEN w + ELSE IF w.queued[c] # {} \/ peer[c] = "stuck" + THEN [w EXCEPT !.queued[c] = @ \cup {k}] + ELSE LET w1 == IF k \in CbKinds THEN [w EXCEPT !.kern[c] = Append(@, [k |-> k, err |-> peer[c] = "gone"])] ELSE w + IN IF k = "ping" /\ peer[c] # "gone" THEN [w1 EXCEPT !.pingOut[c] = TRUE] ELSE w1 + +(* tcp_handle:close() (uv_close): the fd closes at once, and libuv cancels *) +(* every write still in its queue. Their callbacks run with ECANCELED when *) +(* the close finishes. *) +CloseHandle(w, c) == + IF w.handle[c] # "open" THEN w + ELSE [w EXCEPT !.handle[c] = "closing", + !.kern[c] = IF "close" \in w.queued[c] THEN Append(@, [k |-> "close", err |-> TRUE]) ELSE @, + !.queued[c] = {}, + !.ended[c] = TRUE, + !.dropped = @ \/ ("close" \in w.queued[c] /\ w.closeWhy[c] \in {"protocol", "stop"})] + +Schedule(w, c, k) == [w EXCEPT !.sched = Append(@, [c |-> c, k |-> k])] + +(* tcp.lua release_socket: close the handle unless the write callback of a queued Close frame *) +(* will (client.close_pending, which the ping timer clears: a keepalive close does not wait). *) +Release(w, c) == + IF CloseWriteOwnsSocket /\ w.st[c] = "closing" /\ w.closeWhy[c] \in {"protocol", "stop"} THEN w + ELSE CloseHandle(w, c) + +(* tcp.lua _disconnect_client, then _remove_client. A client that is no longer listed is only *) +(* released. *) +Disconnect(w, c) == + LET w1 == [w EXCEPT !.ended[c] = TRUE] + IN IF DisconnectOnce /\ ~w1.listed[c] THEN (IF UnlistedDisconnectReleases THEN Release(w1, c) ELSE w1) + ELSE LET w2 == [w1 EXCEPT !.reports[c] = Min(@ + 1, 2)] + IN IF ~w2.listed[c] THEN w2 + ELSE LET w3 == [w2 EXCEPT !.listed[c] = FALSE] + IN IF DisconnectClosesSocket THEN Release(w3, c) ELSE w3 + +(* client.lua close_client(client, code, reason). why names the caller. *) +(* onDone is TRUE only in the mutant of ProtocolReportsAtOnce: the code *) +(* without that guard reports the client from the Close write callback, *) +(* as close_client's on_done did before the guard. *) +CloseClient(w, c, why, onDone) == + LET w0 == [w EXCEPT !.ended[c] = TRUE] + IN IF w0.st[c] \in {"closing", "closed"} THEN (IF onDone THEN Schedule(w0, c, "done") ELSE w0) + ELSE LET w1 == [w0 EXCEPT !.buf[c] = <<>>] + IN IF w1.handle[c] # "open" + THEN LET w2 == [w1 EXCEPT !.st[c] = "closed"] IN IF onDone THEN Schedule(w2, c, "done") ELSE w2 + ELSE IF w1.hs[c] \/ w1.st[c] = "upgrading" + THEN [Write([w1 EXCEPT !.closeWhy[c] = why], c, "close") EXCEPT !.st[c] = "closing"] + ELSE LET w2 == CloseHandle([w1 EXCEPT !.st[c] = "closed"], c) + IN IF onDone THEN Schedule(w2, c, "done") ELSE w2 + +(* client.lua fail_connection, on a frame that breaks the protocol (a frame that *) +(* parse_frame rejects, a data message that is binary, out of order, too big or *) +(* not UTF-8): close_client, then on_error (_disconnect_client) at once. Without *) +(* the fact, on_error waits for the Close write callback. *) +ProtocolClose(w, c) == + IF ProtocolReportsAtOnce THEN Disconnect(CloseClient(w, c, "protocol", FALSE), c) + ELSE CloseClient(w, c, "protocol", TRUE) + +(* tcp.lua read_start callback, on bytes: it clears client.ping_unanswered_since before process_data runs. *) +ClearOnBytes(w, c) == IF BytesClearStamp THEN [w EXCEPT !.stamped[c] = FALSE] ELSE w + +(* client.lua process_data on one frame of a read. *) +ProcessFrame(w, c, f) == + IF w.st[c] \in {"closing", "closed"} THEN [w EXCEPT !.buf[c] = <<>>] + ELSE IF ~w.hs[c] THEN + IF w.st[c] = "upgrading" THEN [w EXCEPT !.buf[c] = Append(@, f)] + ELSE IF f = "hello" + THEN IF UpgradeInWriteCallback THEN Write([w EXCEPT !.st[c] = "upgrading"], c, "101") + ELSE Write([w EXCEPT !.st[c] = "connected", !.hs[c] = TRUE], c, "101") + ELSE Write([w EXCEPT !.st[c] = "closing", !.ended[c] = TRUE], c, "reject") + ELSE CASE f = "req" -> Schedule(w, c, "message") + [] f = "pong" -> w + [] f = "close" -> + LET w1 == IF w.st[c] = "connected" + THEN [Write(w, c, "echo") EXCEPT !.st[c] = IF PeerCloseMarksClosing THEN "closing" ELSE @] + ELSE w + IN Schedule([w1 EXCEPT !.ended[c] = TRUE, !.buf[c] = <<>>], c, "close") + [] OTHER -> ProtocolClose([w EXCEPT !.buf[c] = <<>>], c) + +(* The loop of one process_data call over several frames: it stops after a *) +(* Close frame or a protocol error. *) +RECURSIVE ProcessAll(_, _, _) +ProcessAll(w, c, fs) == + IF fs = <<>> THEN w + ELSE LET w1 == ProcessFrame(w, c, Head(fs)) + IN IF Head(fs) \in {"close", "bad"} THEN w1 ELSE ProcessAll(w1, c, Tail(fs)) + +(* The libuv callback of a write, with the error libuv passes. *) +Callback(w, c, e) == + CASE e.k = "101" -> + \* client.lua process_data, the 101 write callback + IF e.err THEN CloseHandle(Disconnect(w, c), c) + ELSE LET w1 == [w EXCEPT !.upgraded[c] = TRUE] + IN IF ~UpgradeInWriteCallback THEN w1 + ELSE IF UpgradeRechecksState /\ (w1.st[c] # "upgrading" \/ w1.handle[c] # "open") + THEN [w1 EXCEPT !.buf[c] = <<>>] + ELSE ProcessAll([w1 EXCEPT !.hs[c] = TRUE, !.st[c] = "connected", !.buf[c] = <<>>], c, w1.buf[c]) + [] e.k = "reject" -> + \* client.lua process_data, the write callback of a rejected handshake: on_error, then close + LET w1 == Disconnect(w, c) IN IF RejectClosesSocket THEN CloseHandle(w1, c) ELSE w1 + [] OTHER -> + \* client.lua close_client, the Close write callback: closed, close the handle, then on_done + LET w1 == CloseHandle([w EXCEPT !.st[c] = "closed"], c) + IN IF w.closeWhy[c] = "protocol" /\ ~ProtocolReportsAtOnce THEN Disconnect(w1, c) ELSE w1 + +RECURSIVE RunAll(_, _, _) +RunAll(w, c, es) == IF es = <<>> THEN w ELSE RunAll(Callback(w, c, Head(es)), c, Tail(es)) + +(* tcp.lua drop_client, for one client: close_client(1011), abandon_close_frame, _disconnect_client(1006). The *) +(* ghost falseTimeout records a client whose Claude never stopped answering. *) +Drop(w, c) == + Disconnect(CloseClient([w EXCEPT !.falseTimeout = @ \/ peer[c] = "live"], c, "keepalive", FALSE), c) + +(* One client of the ping timer's loop. mode: "normal", "wake" (the tick gap was above interval * 1.5, so the *) +(* clock jumped past the limit: Neovim or the machine was suspended or blocked) or "stale" (an earlier callback *) +(* of the pass blocked or slept for longer than the limit, and libuv's cached loop time hides it). A stale tick is *) +(* a wake that only a tick with a fresh clock (ClockFreshAtTick) sees: without it the stamps keep the age of the *) +(* sleep and a ping that finds no stamp is stamped with the old cached time. A tick pings a connected client and *) +(* stamps the oldest unanswered ping, and it starts the check handle. Without JudgesAfterRead it also drops the *) +(* client at once, as the code did before. *) +TickOne(w, c, mode) == + IF ~w.listed[c] THEN w + ELSE LET sees == mode = "wake" \/ (mode = "stale" /\ ClockFreshAtTick) + w0 == IF sees THEN (IF WakeClearsStamp THEN [w EXCEPT !.stamped[c] = FALSE] ELSE [w EXCEPT !.age[c] = Limit]) + ELSE IF mode = "stale" THEN [w EXCEPT !.age[c] = Limit] + ELSE w + IN IF w0.st[c] # "connected" THEN w0 + ELSE LET w1 == Write(w0, c, "ping") + w2 == IF w1.stamped[c] /\ StampKeepsOldestPing THEN [w1 EXCEPT !.age[c] = Min(@ + 1, Limit)] + ELSE [w1 EXCEPT !.stamped[c] = TRUE, + !.age[c] = IF mode = "stale" /\ ~ClockFreshAtTick THEN Limit ELSE 0] + w3 == [w2 EXCEPT !.pend[c] = TRUE] + IN IF ~JudgesAfterRead /\ KeepaliveReaps /\ w3.age[c] >= Limit THEN Drop(w3, c) ELSE w3 + +RECURSIVE TickAll(_, _, _) +TickAll(w, S, mode) == + IF S = {} THEN w ELSE LET c == CHOOSE x \in S : TRUE IN TickAll(TickOne(w, c, mode), S \ {c}, mode) + +(* libuv's poll phase for one client: it reads up to n frames that reached the socket, in order, while the handle is *) +(* open (the actions Read and ReadEOF, in a row). Returns the plugin state and the frames still unread. *) +RECURSIVE DrainOne(_, _, _, _) +DrainOne(w, c, q, n) == + IF n = 0 \/ q = <<>> \/ w.handle[c] # "open" \/ (Head(q) = "bad" /\ peer[c] = "stuck" /\ ~WindowFullOnProtocolClose) + THEN [w |-> w, q |-> q] + ELSE IF Head(q) = "eof" THEN DrainOne(Disconnect(w, c), c, Tail(q), n - 1) + ELSE DrainOne(ProcessFrame(ClearOnBytes(w, c), c, Head(q)), c, Tail(q), n - 1) + +RECURSIVE DrainAll(_, _, _, _) +DrainAll(w, S, qs, n) == + IF S = {} THEN [w |-> w, qs |-> qs] + ELSE LET c == CHOOSE x \in S : TRUE + r == DrainOne(w, c, qs[c], n) + IN DrainAll(r.w, S \ {c}, [qs EXCEPT ![c] = r.q], n) + +(* tcp.lua judge_silence, run by the check callback, for one client: it drops a client that is still listed and *) +(* connected and whose stamp is old enough. *) +CheckOne(w, c) == + IF ~w.pend[c] THEN w + ELSE LET w0 == [w EXCEPT !.pend[c] = FALSE] + IN IF KeepaliveReaps /\ w0.listed[c] /\ w0.st[c] = "connected" /\ w0.stamped[c] /\ w0.age[c] >= Limit + THEN Drop(w0, c) + ELSE w0 + +RECURSIVE CheckAll(_, _) +CheckAll(w, S) == IF S = {} THEN w ELSE LET c == CHOOSE x \in S : TRUE IN CheckAll(CheckOne(w, c), S \ {c}) + +(* tcp.lua stop_server, one client. *) +StopOne(w, c) == + IF ~w.listed[c] THEN w + ELSE LET w1 == CloseClient(w, c, "stop", FALSE) IN IF StopWaitsForCloseWrite THEN w1 ELSE CloseHandle(w1, c) + +RECURSIVE StopAll(_, _) +StopAll(w, S) == IF S = {} THEN w ELSE LET c == CHOOSE x \in S : TRUE IN StopAll(StopOne(w, c), S \ {c}) + +Reading == {"live", "resumed"} \* Claude reads and answers +Dead(c) == listed[c] /\ (peer[c] = "gone" \/ st[c] \in {"closing", "closed"} \/ (hs[c] /\ peer[c] \in {"silent", "stuck"})) + +TypeOK == + /\ st \in [Conns -> States] + /\ hs \in [Conns -> BOOLEAN] + /\ listed \in [Conns -> BOOLEAN] + /\ handle \in [Conns -> {"none", "open", "closing", "closed"}] + /\ \A c \in Conns : kern[c] \in Seq([k : CbKinds, err : BOOLEAN]) /\ Len(kern[c]) <= 3 + /\ queued \in [Conns -> SUBSET {"data", "ping", "close", "echo"}] + /\ closeWhy \in [Conns -> {None, "protocol", "keepalive", "stop"}] + /\ \A c \in Conns : buf[c] \in Seq(Frames) /\ inq[c] \in Seq(Frames) + /\ sched \in Seq([c : Conns, k : {"message", "close", "done"}]) + /\ stamped \in [Conns -> BOOLEAN] + /\ age \in [Conns -> 0..Limit] + /\ pend \in [Conns -> BOOLEAN] + /\ jumped \in BOOLEAN + /\ peer \in [Conns -> {"idle", "live", "silent", "stuck", "resumed", "gone"}] + /\ sent \in [Conns -> 0..PeerBudget] + /\ pingOut \in [Conns -> BOOLEAN] + /\ serverUp \in BOOLEAN + /\ sleeps \in 0..MaxSleeps + /\ upgraded \in [Conns -> BOOLEAN] + /\ ended \in [Conns -> BOOLEAN] + /\ reports \in [Conns -> 0..2] + /\ badDispatch \in BOOLEAN + /\ dropped \in BOOLEAN + /\ falseTimeout \in BOOLEAN + +Init == + /\ st = [c \in Conns |-> "none"] + /\ hs = [c \in Conns |-> FALSE] + /\ listed = [c \in Conns |-> FALSE] + /\ handle = [c \in Conns |-> "none"] + /\ kern = [c \in Conns |-> <<>>] + /\ queued = [c \in Conns |-> {}] + /\ closeWhy = [c \in Conns |-> None] + /\ buf = [c \in Conns |-> <<>>] + /\ sched = <<>> + /\ stamped = [c \in Conns |-> FALSE] + /\ age = [c \in Conns |-> 0] + /\ pend = [c \in Conns |-> FALSE] + /\ jumped = FALSE + /\ peer = [c \in Conns |-> "idle"] + /\ inq = [c \in Conns |-> <<>>] + /\ sent = [c \in Conns |-> 0] + /\ pingOut = [c \in Conns |-> FALSE] + /\ serverUp = TRUE + /\ sleeps = 0 + /\ upgraded = [c \in Conns |-> FALSE] + /\ ended = [c \in Conns |-> FALSE] + /\ reports = [c \in Conns |-> 0] + /\ badDispatch = FALSE + /\ dropped = FALSE + /\ falseTimeout = FALSE + +----------------------------------------------------------------------------- +(* Steps of the plugin *) + +(* tcp.lua _handle_new_connection: accept, create_client, add to server.clients, read_start, on_connect. *) +Accept(c) == + /\ serverUp /\ st[c] = "none" + /\ SetW([W EXCEPT !.st[c] = "connecting", !.listed[c] = TRUE, !.handle[c] = "open"]) + /\ peer' = [peer EXCEPT ![c] = "live"] + /\ UNCHANGED <> + +(* tcp.lua read_start callback with data -> client.lua process_data. One read carries one frame: *) +(* process_data handles the frames of one read in order and stops after a Close or a protocol *) +(* error, so a read of several frames reaches no state that one-frame reads do not. *) +Read(c) == + /\ handle[c] = "open" /\ inq[c] # <<>> /\ Head(inq[c]) # "eof" + /\ WindowFullOnProtocolClose \/ ~(Head(inq[c]) = "bad" /\ peer[c] = "stuck") + /\ SetW(ProcessFrame(ClearOnBytes(W, c), c, Head(inq[c]))) + /\ inq' = [inq EXCEPT ![c] = Tail(@)] + /\ UNCHANGED <> + +(* tcp.lua read_start callback with EOF or a read error -> _disconnect_client(1006). *) +ReadEOF(c) == + /\ handle[c] = "open" /\ inq[c] # <<>> /\ Head(inq[c]) = "eof" + /\ SetW(Disconnect(W, c)) + /\ inq' = [inq EXCEPT ![c] = Tail(@)] + /\ UNCHANGED <> + +(* libuv runs the callback of the oldest write the kernel took (client.lua: the 101 or reject *) +(* write callback in process_data, the Close write callback in close_client). *) +WriteDone(c) == + /\ handle[c] = "open" /\ kern[c] # <<>> + /\ SetW(Callback([W EXCEPT !.kern[c] = Tail(@)], c, Head(kern[c]))) + /\ UNCHANGED env + +(* libuv finishes the uv_close of the handle: it runs every pending write callback in order, *) +(* the cancelled ones with ECANCELED. *) +CloseFinishes(c) == + /\ handle[c] = "closing" + /\ SetW([RunAll([W EXCEPT !.kern[c] = <<>>], c, kern[c]) EXCEPT !.handle[c] = "closed"]) + /\ UNCHANGED env + +(* One vim.schedule'd closure runs: client.lua's on_message wrapper (guarded), the on_close *) +(* of a Close frame, or close_client's scheduled on_done; the last two call tcp.lua *) +(* _disconnect_client. *) +ScheduledRuns == + /\ sched # <<>> + /\ LET e == Head(sched) + c == e.c + w0 == [W EXCEPT !.sched = Tail(@)] + IN SetW(IF e.k = "message" + THEN IF DispatchGuard => (w0.st[c] = "connected" /\ w0.handle[c] = "open") + THEN [w0 EXCEPT !.badDispatch = @ \/ ~w0.upgraded[c] \/ w0.ended[c]] + ELSE w0 + ELSE Disconnect(w0, c)) + /\ UNCHANGED env + +(* A Claude that is reading answers a ping before the next tick (an assumption of NoFalseTimeout, which is about a *) +(* Claude that answers every ping): the pong is in the socket by then, and the plugin may not have read it. A tick *) +(* after a gap does not wait for it: the machine slept, and Claude slept with Neovim. *) +AnsweredBeforeTick == PeerAnswersBeforeTick => \A c \in Conns : peer[c] \in Reading => ~pingOut[c] + +(* tcp.lua start_ping_timer callback, a tick on time. It can run at any point between reads: libuv runs it before it *) +(* reads the socket after a block of the main loop (in any callback on Neovim 0.8, and in a check or I/O callback on *) +(* newer Neovim), and Neovim 0.8 runs the timers again at the end of a pass, so two ticks can run with no read *) +(* between them. After the loop time jumped, the next tick sees the gap: only TimerTicksAfterGap. *) +TimerTicks == + /\ serverUp /\ ~jumped /\ AnsweredBeforeTick + /\ SetW(TickAll(W, Conns, "normal")) + /\ UNCHANGED env + +(* tcp.lua start_ping_timer callback after a gap above interval * 1.5: Neovim was suspended or *) +(* its main loop was blocked, so the loop's clock jumped. *) +TimerTicksAfterGap == + /\ serverUp /\ (jumped \/ sleeps < MaxSleeps) + /\ SetW([TickAll(W, Conns, "wake") EXCEPT !.jumped = FALSE]) + /\ sleeps' = IF jumped THEN sleeps ELSE sleeps + 1 + /\ UNCHANGED <> + +(* tcp.lua start_ping_timer callback in a pass whose earlier callback blocked for longer than the limit, or in *) +(* which the machine slept (Claude slept with Neovim, so no answer is due): libuv runs the timers of a pass with *) +(* the loop time of its start, so the tick sees no gap and does not clear the stamps, and a ping that finds no *) +(* stamp is stamped with the old time, unless the tick calls vim.loop.update_time() first (ClockFreshAtTick). *) +TimerTicksStale == + /\ StaleLoopTime + /\ serverUp /\ ~jumped /\ sleeps < MaxSleeps + /\ SetW(TickAll(W, Conns, "stale")) + /\ sleeps' = sleeps + 1 + /\ UNCHANGED <> + +(* The machine sleeps after a tick and before the poll that precedes its check: Neovim and Claude stop together, and *) +(* the loop time jumps past the limit. Claude answers only after it wakes, which is after the poll. The next tick *) +(* sees the gap, takes it for a wake, and clears the stamps. *) +MachineSleeps == + /\ SleepInWindow + /\ serverUp /\ ~jumped /\ sleeps < MaxSleeps /\ \E c \in Conns : pend[c] + /\ SetW([W EXCEPT !.jumped = TRUE, !.age = [c \in Conns |-> IF W.stamped[c] THEN Limit ELSE W.age[c]]]) + /\ sleeps' = sleeps + 1 + /\ UNCHANGED <> + +(* libuv's poll phase reads up to n frames per client that reached a socket before it, then runs the check handles *) +(* that the ticks started: tcp.lua after_next_poll runs judge_silence. A check whose loop time jumped since its tick judges *) +(* nothing (GapSkip). Claude can answer after the poll, and the poll does not read what Claude sends after it. *) +PollStep(n) == + /\ \E c \in Conns : pend[c] + /\ LET r == DrainAll(W, Conns, inq, n) + w1 == IF GapSkip /\ r.w.jumped THEN [r.w EXCEPT !.pend = [c \in Conns |-> FALSE]] ELSE CheckAll(r.w, Conns) + IN /\ SetW(w1) + /\ inq' = r.qs + /\ UNCHANGED <> + +PollAndCheck == PollStep(99) + +(* A poll that reads only the first frame of each client: Claude's pong waits behind it. *) +PollAndCheckPartial == PollMissesPong /\ PollStep(1) + +(* :ClaudeCodeStop or VimLeavePre: init.lua M.stop -> server/init.lua M.stop (stops the ping *) +(* timer) -> tcp.lua stop_server (close_client 1001 for each client, clients = {}). *) +ServerStops == + /\ serverUp + /\ StopBeforeOnClose \/ \A i \in DOMAIN sched : sched[i].k # "close" + /\ SetW([StopAll(W, Conns) EXCEPT !.listed = [c \in Conns |-> FALSE]]) + /\ serverUp' = FALSE + /\ UNCHANGED <> + +(* server/init.lua send / broadcast -> client.lua send_message while Claude does not read: the *) +(* message fills Claude's receive window, and the rest waits in libuv's queue. *) +PluginSendsLarge(c) == + /\ peer[c] = "silent" /\ st[c] = "connected" /\ handle[c] = "open" + /\ SetW([W EXCEPT !.queued[c] = @ \cup {"data"}]) + /\ peer' = [peer EXCEPT ![c] = "stuck"] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Steps of Claude (the environment) *) + +(* Claude can write while it does not read: its process is busy, not gone. *) +ClaudeSends(c, f) == + /\ peer[c] \in Reading \cup {"silent", "stuck"} /\ sent[c] < PeerBudget + /\ f \in IF sent[c] = 0 THEN {"hello", "badhello"} ELSE {"req", "close", "bad"} + /\ inq' = [inq EXCEPT ![c] = Append(@, f)] + /\ sent' = [sent EXCEPT ![c] = @ + 1] + /\ UNCHANGED <> + +(* One unread pong answers as well as two, so Claude adds one only when none is unread. *) +ClaudeAnswersPing(c) == + /\ peer[c] \in Reading /\ pingOut[c] + /\ inq' = IF "pong" \in Range(inq[c]) THEN inq ELSE [inq EXCEPT ![c] = Append(@, "pong")] + /\ pingOut' = [pingOut EXCEPT ![c] = FALSE] + /\ UNCHANGED <> + +(* Claude stops reading and answering (for example its process is suspended). *) +ClaudeStopsReading(c) == + /\ peer[c] \in Reading /\ hs[c] + /\ peer' = [peer EXCEPT ![c] = "silent"] + /\ UNCHANGED <> + +(* Claude reads again; libuv's POLLOUT handler writes what waited in its queue. *) +ClaudeResumes(c) == + /\ peer[c] \in {"silent", "stuck"} + /\ peer' = [peer EXCEPT ![c] = "resumed"] + /\ SetW([W EXCEPT !.kern[c] = IF "close" \in queued[c] THEN Append(@, [k |-> "close", err |-> FALSE]) ELSE @, + !.pingOut[c] = @ \/ "ping" \in queued[c], + !.queued[c] = {}]) + /\ UNCHANGED <> + +(* Claude hangs up (FIN or RST). The plugin reads EOF after the frames before it, and writes *) +(* still in libuv's queue fail. *) +ClaudeHangsUp(c) == + /\ peer[c] \in Reading \cup {"silent", "stuck"} + /\ peer' = [peer EXCEPT ![c] = "gone"] + /\ inq' = [inq EXCEPT ![c] = Append(@, "eof")] + /\ SetW([W EXCEPT !.kern[c] = IF "close" \in queued[c] THEN Append(@, [k |-> "close", err |-> TRUE]) ELSE @, + !.queued[c] = {}]) + /\ UNCHANGED <> + +Next == + \/ \E c \in Conns : Accept(c) + \/ \E c \in Conns : Read(c) + \/ \E c \in Conns : ReadEOF(c) + \/ \E c \in Conns : WriteDone(c) + \/ \E c \in Conns : CloseFinishes(c) + \/ ScheduledRuns + \/ TimerTicks + \/ TimerTicksAfterGap + \/ TimerTicksStale + \/ MachineSleeps + \/ PollAndCheck + \/ PollAndCheckPartial + \/ ServerStops + \/ \E c \in Conns : PluginSendsLarge(c) + \/ \E c \in Conns, f \in Frames : ClaudeSends(c, f) + \/ \E c \in Conns : ClaudeAnswersPing(c) + \/ \E c \in Conns : ClaudeStopsReading(c) + \/ \E c \in Conns : ClaudeResumes(c) + \/ \E c \in Conns : ClaudeHangsUp(c) + +(* libuv runs ready callbacks and timers, and the main loop runs scheduled closures. Claude is *) +(* never assumed to act, except that with PeerEventuallyReads it never stops reading for good. *) +Spec == + /\ Init /\ [][Next]_vars + /\ \A c \in Conns : WF_vars(Read(c)) /\ WF_vars(ReadEOF(c)) /\ WF_vars(WriteDone(c)) /\ WF_vars(CloseFinishes(c)) + /\ WF_vars(ScheduledRuns) + /\ WF_vars(TimerTicks) + /\ WF_vars(PollAndCheck) + /\ \A c \in Conns : WF_vars(PeerEventuallyReads /\ ClaudeResumes(c)) + +----------------------------------------------------------------------------- +(* Rules *) + +(* A request from Claude runs only after its 101 reply was written, and never after the *) +(* plugin started to close the connection or saw it end. *) +NoRequestAfterEnd == ~badDispatch + +(* on_disconnect runs at most once per client. *) +DisconnectReportedOnce == \A c \in Conns : reports[c] <= 1 + +(* A Close frame for a protocol error (1002, 1003, 1007, 1009) or a server stop (1001) is *) +(* written before the plugin closes the socket, as long as Claude keeps reading. The *) +(* deadline of close_client (start_close_timer) closes the socket and drops the frame of a *) +(* Claude whose queue makes no progress for one keepalive window: the model has no such *) +(* step, so the rule does not cover that case. The keepalive Close frame (1011) is not in *) +(* the rule: server/README.md documents that a peer whose window is full does not get it. *) +StatusCloseDelivered == ~dropped + +(* A Claude that answers each ping before the next tick (PeerAnswersBeforeTick), or after a wake, is never *) +(* dropped by the ping timer, whatever blocks Neovim: a tick never *) +(* drops a client, the check that does runs after a poll, it judges nothing after a jump of the loop time, and *) +(* any bytes that the poll reads clear the stamp, so a pong that waits behind a large message cannot count *) +(* against the client. A Claude that stopped once is not covered. It holds in every state, written as a *) +(* temporal formula so that check.sh checks it in a run of its own: its known finding is shorter than any other *) +(* break, so in the joint run it would hide the others. *) +NoFalseTimeout == [](~falseTimeout) + +(* A client whose Claude hung up, stopped answering, or whose connection the plugin started *) +(* to close, eventually leaves server.clients with its on_disconnect, unless the server *) +(* stops or Claude comes back. *) +DeadClientDropped == + \A c \in Conns : Dead(c) ~> ((~listed[c] /\ reports[c] >= 1) \/ ~serverUp \/ (peer[c] \in Reading /\ st[c] = "connected")) + +(* Once a client left server.clients (or the server stopped), its socket eventually closes. *) +(* Run with PeerEventuallyReads = TRUE. *) +DroppedSocketCloses == \A c \in Conns : (st[c] # "none" /\ ~listed[c]) ~> (handle[c] = "closed") +============================================================================= diff --git a/.agents/skills/verify-ws-connection/model/statechart-view.ts b/.agents/skills/verify-ws-connection/model/statechart-view.ts new file mode 100644 index 000000000..683ad8ff7 --- /dev/null +++ b/.agents/skills/verify-ws-connection/model/statechart-view.ts @@ -0,0 +1,124 @@ +// /statechart view for WsConnection.tla: one Claude connection, as three regions: the plugin's view of the +// connection, Claude's side, and the server. A wrapper spec that narrows an action names it Flow; it gets +// the label of . +const has = (set: any, x: string) => Array.isArray(set) && set.includes(x); +const seq = (s: any): any[] => (s ? Object.values(s) : []); +const first = (vars: any) => Object.keys(vars.st).sort()[0]; + +const connection = (v: any, c: string) => { + const st = v.st[c]; + if (st === "none") return "not connected"; + const open = v.handle[c] === "open"; + if (!v.listed[c]) + return open ? "dropped, socket still open" : "dropped, socket closed"; + if (st === "connecting") return "TCP accepted, no handshake yet"; + if (st === "upgrading") return "handshake accepted, 101 being written"; + if (st === "connected") + return seq(v.sched).some((e: any) => e.c === c && e.k === "message") + ? "connected, a request waits to run" + : "connected"; + if (has(v.queued[c], "close")) return "closing, its Close frame waits"; + return "closing"; +}; + +const claude = (v: any, c: string) => + ({ + idle: "not started", + live: "reading", + resumed: "reading again", + silent: "not reading", + stuck: "not reading, window full", + gone: "hung up", + })[v.peer[c] as string] ?? v.peer[c]; + +export const title = + "One Claude connection to the claudecode.nvim WebSocket server"; + +export const state = (v: any) => ({ + Connection: connection(v, first(v)), + Claude: claude(v, first(v)), + Server: v.serverUp ? "running" : "stopped", +}); + +export const group = (v: any) => { + const label = connection(v, first(v)); + if (label.startsWith("dropped")) return "ended"; + if (label.startsWith("connected")) return "connected"; + return "transition"; +}; +export const colors = { ended: "teal", connected: "blue", transition: "pink" }; + +const labels: Record = { + Accept: "Claude connects", + Read: "the plugin reads what Claude sent", + ReadEOF: "the plugin sees Claude hang up", + WriteDone: "a write to Claude completes", + CloseFinishes: "the socket finishes closing", + ScheduledRuns: "the main loop runs a scheduled step", + TimerTicks: "the ping timer ticks", + TimerTicksAfterGap: "the ping timer ticks after Neovim was blocked", + TimerTicksStale: + "the ping timer ticks in a pass whose earlier callback blocked, with the loop time cached before the block", + MachineSleeps: + "the machine sleeps between a tick and the poll before its check", + PollAndCheck: + "libuv reads the sockets, then the keepalive check judges the pinged clients", + PollAndCheckPartial: + "libuv reads only the first frame of each client, then the keepalive check judges", + PollStep: + "libuv reads the sockets, then the keepalive check judges the pinged clients", + ServerStops: "you stop the server", + PluginSendsLarge: "the plugin sends Claude a large message", + ClaudeSends: "Claude sends a frame", + ClaudeAnswersPing: "Claude answers a ping", + ClaudeStopsReading: "Claude stops reading", + ClaudeResumes: "Claude reads again", + ClaudeHangsUp: "Claude hangs up", +}; + +const frames: Record = { + hello: "its upgrade request", + badhello: "a bad upgrade request", + req: "a request", + pong: "a pong", + close: "a Close frame", + bad: "a frame that breaks the protocol", +}; + +export const step = (name: string, from: any, to: any) => { + const action = name.replace(/^Flow/, ""); + const c = first(from); + if (action === "ClaudeSends") { + const sent = seq(to.inq[c]); + return `Claude sends ${frames[sent[sent.length - 1]] ?? "a frame"}`; + } + if (action === "Read") + return `the plugin reads ${frames[seq(from.inq[c])[0]] ?? "a frame"}`; + if (action === "WriteDone") { + const k = seq(from.kern[c])[0]?.k; + if (k === "101") return "the 101 reply is written"; + if (k === "reject") return "the rejection is written"; + return "the plugin's Close frame is written"; + } + if (action === "ScheduledRuns") { + const e = seq(from.sched)[0]; + if (e?.k === "message") + return to.badDispatch && !from.badDispatch + ? "the request runs [too late]" + : "the request runs"; + if (e?.k === "close") return "the plugin handles Claude's Close frame"; + return "the plugin handles the protocol error"; + } + if ( + action === "TimerTicks" || + action === "TimerTicksAfterGap" || + action === "TimerTicksStale" || + action === "PollAndCheck" || + action === "PollAndCheckPartial" || + action === "PollStep" + ) { + if (from.listed[c] && !to.listed[c]) + return "the ping timer drops Claude for no reply"; + } + return labels[action] ?? action; +}; diff --git a/.agents/skills/verify-ws-connection/replays/blocks-before-the-poll.lua b/.agents/skills/verify-ws-connection/replays/blocks-before-the-poll.lua new file mode 100644 index 000000000..6fc4d4569 --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/blocks-before-the-poll.lua @@ -0,0 +1,118 @@ +-- Scenario: the keepalive check runs after a poll that Claude's answer did not reach. Claude runs in a process of its +-- own and answers every ping. Interval 200 ms. Three runs, each with a fresh plugin and a fresh Claude: +-- big-message: the loop blocks for 2.7 intervals in an idle callback right after a tick. Claude writes a 300 KB text +-- frame and then its pong during the block, so the pong waits behind more unread data than the socket +-- holds, and the one poll after the block does not reach it. +-- two-blocks: a block of 1.4 intervals in a check callback right after a ping, then, after the late tick, a block +-- of 1.4 intervals in an idle callback before the poll. Each block is below the gap of 1.5 intervals, +-- and the oldest ping is 2.8 intervals old at the check. Claude writes 300 KB and then its pong. +-- sleep: the loop blocks for 2.7 intervals in an idle callback right after a tick, and Claude sleeps as long +-- before its answer, as a machine that sleeps with Neovim does. +-- Promise: Claude is not dropped. big-message needs one of the two guards: the read callback clears the stamp on any +-- bytes (BytesClearStamp), or the check judges nothing after a block longer than 1.5 intervals (GapSkip). two-blocks +-- needs BytesClearStamp (the gap skip with a clear on a PONG only still drops Claude), and sleep needs GapSkip (the +-- any-bytes clear without the gap skip still drops Claude). The code of f3576ea has neither and breaks all three. +-- Model path: MachineSleeps, PollAndCheck (the check is skipped), TimerTicksAfterGap (the wake clears the stamp). +local H = dofile(vim.fs.dirname(debug.getinfo(1, "S").source:sub(2)) .. "/harness.lua") +local INTERVAL = 200 +local BIG = 300000 +local SETTLE = 8 * INTERVAL + +---Start the plugin and Claude, wait for the second ping, and run `block(client)` when the third ping goes out. +local function scenario(mode, block) + local plugin = H.start_plugin(INTERVAL) + local claude = H.spawn_claude(plugin.port, plugin.token, mode) + local seen, pings = 0, 0 + H.wait(8000, function() + local client = plugin.client() + if client and client.state == "connected" and client.last_ping ~= seen then + seen, pings = client.last_ping, pings + 1 + end + return pings >= 2 + end) + local client = assert(plugin.client(), "no client") + seen = client.last_ping + local blocked = block(client, seen) + H.wait(SETTLE, function() + return #plugin.disconnects > 0 + end) + local dropped = plugin.disconnects[1] + claude.kill() + require("claudecode").stop() + return blocked(), dropped +end + +---A handle that runs `fn` once, in the iteration that runs the next tick, after the timers and before the poll. +local function once_before_poll(new_handle, client, seen, fn) + local ran = false + local handle = new_handle() + handle:start(function() + if not ran and client.last_ping ~= seen then + ran = true + handle:stop() + fn() + end + end) + return function() + return ran + end +end + +local function check_kept(name, ran, dropped) + H.check( + name, + ran and dropped == nil, + dropped + and string.format("on_disconnect(%s, %s, %q) at %d ms", dropped.id, dropped.code, dropped.reason, dropped.at) + or (ran and "no on_disconnect, still listed" or "the block never ran") + ) +end + +H.log("scenario big-message: block %d ms in an idle callback, Claude writes %d bytes and its pong", 2.7 * INTERVAL, BIG) +check_kept( + "a pong behind 300 KB, after a block of 2.7 intervals before the poll", + scenario("big:3:" .. BIG, function(client, seen) + return once_before_poll(H.uv.new_idle, client, seen, function() + H.uv.sleep(math.floor(2.7 * INTERVAL)) + end) + end) +) + +H.log("scenario two-blocks: 1.4 intervals in a check callback, then 1.4 intervals in an idle callback") +check_kept( + "a pong behind 300 KB, after two blocks of 1.4 intervals", + scenario("big:3:" .. BIG, function(client, seen) + local ran = false + local check = H.uv.new_check() + check:start(function() + if not ran and client.last_ping ~= seen then + ran = true + check:stop() + H.uv.sleep(math.floor(1.4 * INTERVAL)) + local idle = H.uv.new_idle() + local done = false + idle:start(function() + if not done then + done = true + idle:stop() + H.uv.sleep(math.floor(1.4 * INTERVAL)) + end + end) + end + end) + return function() + return ran + end + end) +) + +H.log("scenario sleep: block %d ms in an idle callback, Claude sleeps as long before its answer", 2.7 * INTERVAL) +check_kept( + "Claude that sleeps with Neovim for 2.7 intervals between a tick and its poll", + scenario("late:3:" .. math.floor(2.7 * INTERVAL), function(client, seen) + return once_before_poll(H.uv.new_idle, client, seen, function() + H.uv.sleep(math.floor(2.7 * INTERVAL)) + end) + end) +) +H.finish() diff --git a/.agents/skills/verify-ws-connection/replays/claude-process.lua b/.agents/skills/verify-ws-connection/replays/claude-process.lua new file mode 100644 index 000000000..5ff1c15df --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/claude-process.lua @@ -0,0 +1,33 @@ +-- Claude in its own Neovim, started by harness.lua spawn_claude: it connects to the plugin, sends its upgrade request, +-- and answers every ping at once until the flag file named by VWC_PEER_SILENT_FLAG exists. VWC_PEER_MODE can make one +-- ping special: "big::" sends a text frame of that many bytes before the pong of ping n, and "late::" +-- sleeps that long first. The parent kills it. +local H = dofile(os.getenv("VWC_HARNESS")) +local frame = H.frame +local claude = H.peer(tonumber(os.getenv("VWC_PEER_PORT"))) +claude.connect(function() + claude.hello(os.getenv("VWC_PEER_TOKEN")) +end) +local flag = os.getenv("VWC_PEER_SILENT_FLAG") +local kind, at, arg = (os.getenv("VWC_PEER_MODE") or ""):match("^(%a*):?(%d*):?(%d*)$") +at, arg = tonumber(at), tonumber(arg) +local answered = 0 +local timer = H.uv.new_timer() +timer:start(5, 5, function() + local pings = claude.count(frame.OPCODE.PING) + while answered < pings do + answered = answered + 1 + if answered == at and kind == "big" then + claude.send(frame.OPCODE.TEXT, string.rep("x", arg)) + elseif answered == at and kind == "late" then + H.uv.sleep(arg) + end + if not H.uv.fs_stat(flag) then + claude.send(frame.OPCODE.PONG, "") + end + end +end) +vim.wait(10 * 60 * 1000, function() + return false +end) +vim.cmd("qa!") diff --git a/.agents/skills/verify-ws-connection/replays/gap-during-handshake.lua b/.agents/skills/verify-ws-connection/replays/gap-during-handshake.lua new file mode 100644 index 000000000..11856cf8b --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/gap-during-handshake.lua @@ -0,0 +1,68 @@ +-- Scenario: a tick gap while Claude's handshake is still in flight. Before #455 the gap counted against Claude, and the +-- ping timer dropped it with 1011 one interval after its handshake, before any ping reached it. +-- Promise: a Claude that answers every ping is never dropped. Since #488 a client has no stamp until a tick pings it, so +-- a gap in the handshake cannot time it out. +-- Model path: Accept, TimerTicksAfterGap (the client is still connecting), Read (the upgrade request), WriteDone (101, +-- connected), TimerTicks (a ping, not a drop). +local H = dofile(vim.fs.dirname(debug.getinfo(1, "S").source:sub(2)) .. "/harness.lua") +local INTERVAL, STALL, WAIT = 200, 700, 2000 -- ms; the plugin's default interval is 30000, a gap is above interval * 1.5 + +local plugin = H.start_plugin(INTERVAL) +H.log("plugin: server on port %d, ping timer every %d ms", plugin.port, INTERVAL) + +-- A libuv check handle runs after the poll phase in which the listener accepted the connection, before the read of +-- Claude's upgrade request. It blocks the main loop there, as a suspended or busy Neovim would. +local accepted_at, stalled +local check = H.uv.new_check() +check:start(function() + local client = plugin.client() + if client and not stalled then + stalled = true + accepted_at = H.ms() + H.log("plugin: accepted %s (state %s); Neovim's main loop now blocks for %d ms", client.id, client.state, STALL) + H.uv.sleep(STALL) + check:stop() + end +end) + +local claude = H.peer(plugin.port) +claude.answer_pings = true +claude.connect(function() + H.log("claude: connected, sends its upgrade request at once") + claude.hello(plugin.token) +end) + +-- Claude answers every ping, so the plugin must keep it for at least ten intervals after the gap. +H.wait(WAIT, function() + return #plugin.disconnects > 0 +end) +local d = plugin.disconnects[1] +H.log("claude: status line %q at %s ms", tostring(claude.status_line), tostring(claude.opened_at)) +H.log( + "claude: got %d pings, Close frames %s, then EOF: %s", + claude.count(H.frame.OPCODE.PING), + vim.inspect(claude.close_frames()), + tostring(claude.eof) +) + +H.check( + "the gap fell inside the handshake", + stalled == true and claude.opened and claude.opened_at > accepted_at, + string.format("101 at %s ms, accept at %s ms, block %d ms", tostring(claude.opened_at), tostring(accepted_at), STALL) +) +H.check( + "Claude is not dropped", + d == nil and plugin.client() ~= nil and not claude.eof, + d and string.format("on_disconnect(%s, %s, %q) at %d ms", d.id, d.code, d.reason, d.at) + or string.format("no on_disconnect in %d ms (%d intervals), still listed", WAIT, math.floor(WAIT / INTERVAL)) +) +H.check( + "Claude is pinged, and gets no Close frame", + claude.count(H.frame.OPCODE.PING) >= 3 and #claude.close_frames() == 0, + string.format( + "%d pings, Close frames %s", + claude.count(H.frame.OPCODE.PING), + table.concat(claude.close_frames(), ",") + ) +) +H.finish() diff --git a/.agents/skills/verify-ws-connection/replays/harness.lua b/.agents/skills/verify-ws-connection/replays/harness.lua new file mode 100644 index 000000000..9418a9148 --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/harness.lua @@ -0,0 +1,260 @@ +-- Shared helpers for the verify-ws-connection replays. The plugin side is the real code: require("claudecode") +-- setup and start, the real server, its real ping timer (at a short interval), real sockets on 127.0.0.1. Only +-- Claude is played, by a luv TCP client in the same Neovim that speaks RFC 6455 with masked frames. +-- A replay runs a scenario in which the model found a bug (see SKILL.md, "Bugs this model found") and checks the +-- promise that the fix keeps. Each check prints KEPT or BROKEN, and the run exits 0 only when every check is kept. +local uv = vim.uv or vim.loop +local frame = require("claudecode.server.frame") +local utils = require("claudecode.server.utils") + +local M = {} +local start_ns = uv.hrtime() +local kept, total, skipped = 0, 0, 0 + +function M.ms() + return math.floor((uv.hrtime() - start_ns) / 1e6) +end + +function M.log(fmt, ...) + io.stdout:write(string.format("[%5d ms] " .. fmt .. "\n", M.ms(), ...)) +end + +-- One line per result, and a count line from finish(). +function M.check(name, ok, detail) + total = total + 1 + if ok then + kept = kept + 1 + end + io.stdout:write(string.format("%s %s: %s\n", ok and "KEPT" or "BROKEN", name, detail)) +end + +-- A check that this host cannot run. It counts as neither kept nor broken. +function M.skip(name, detail) + skipped = skipped + 1 + io.stdout:write(string.format("SKIPPED %s: %s\n", name, detail)) +end + +function M.finish() + io.stdout:write( + string.format("%d of %d kept%s\n", kept, total, skipped > 0 and string.format(", %d skipped", skipped) or "") + ) + io.stdout:flush() + vim.cmd(kept == total and "qa!" or "cq!") +end + +function M.wait(ms, cond) + return vim.wait(ms, cond or function() + return false + end, 5) +end + +-- Start the plugin as a user does (setup, then start). With interval, replace the 30 s ping timer by the real +-- tcp.start_ping_timer at that interval. Counts on_disconnect calls without changing what they do. +function M.start_plugin(interval) + require("claudecode").setup({ + auto_start = false, + log_level = "warn", + track_selection = false, + terminal = { provider = "none" }, + }) + local ok, port = require("claudecode").start(false) + assert(ok, tostring(port)) + local srv = require("claudecode.server.init") + if interval then + srv.state.ping_timer:stop() + srv.state.ping_timer:close() + srv.state.ping_timer = require("claudecode.server.tcp").start_ping_timer(srv.state.server, interval) + end + local plugin = { port = port, token = require("claudecode").state.auth_token, srv = srv, disconnects = {} } + local on_disconnect = srv.state.server.on_disconnect + srv.state.server.on_disconnect = function(client, code, reason) + table.insert(plugin.disconnects, { id = client.id, code = code, reason = reason, at = M.ms() }) + M.log("plugin: on_disconnect(%s, %s, %q)", client.id, tostring(code), tostring(reason)) + return on_disconnect(client, code, reason) + end + function plugin.client() + local _, client = next(srv.state.server.clients) + return client + end + return plugin +end + +-- Claude. Received frames are kept as { opcode, code (Close frames), at }. +function M.peer(port) + local p = { frames = {}, chunks = {}, size = 0, opened = false, eof = false, answer_pings = false } + p.tcp = uv.new_tcp() + + function p.feed(data) + table.insert(p.chunks, data) + p.size = p.size + #data + while p.size > 0 and (not p.need or p.size >= p.need) do + local raw = table.concat(p.chunks) + if not p.opened then + local i = raw:find("\r\n\r\n", 1, true) + if not i then + p.chunks = { raw } + return + end + p.status_line = raw:match("^[^\r]*") + p.opened = true + p.opened_at = M.ms() + raw = raw:sub(i + 4) + end + local f, consumed, code, detail = frame.parse_frame(raw) + if not f then + assert(not code, "server frame broke the protocol: " .. tostring(detail)) + p.need = detail + p.chunks, p.size = { raw }, #raw + return + end + p.need = nil + raw = raw:sub(consumed + 1) + p.chunks, p.size = { raw }, #raw + local got = { opcode = f.opcode, at = M.ms() } + if f.opcode == frame.OPCODE.CLOSE and #f.payload >= 2 then + got.code = f.payload:byte(1) * 256 + f.payload:byte(2) + end + table.insert(p.frames, got) + if f.opcode == frame.OPCODE.PING and p.answer_pings then + p.send(frame.OPCODE.PONG, f.payload) + end + end + end + + function p.start_reading() + p.tcp:read_start(function(err, data) + if err or not data then + p.eof = true + return + end + p.feed(data) + end) + end + + function p.stop_reading() + p.tcp:read_stop() + end + + function p.hello(token) + p.tcp:write(table.concat({ + "GET / HTTP/1.1", + "Host: 127.0.0.1:" .. port, + "Upgrade: websocket", + "Connection: Upgrade", + "Sec-WebSocket-Key: " .. utils.generate_websocket_key(), + "Sec-WebSocket-Version: 13", + "x-claude-code-ide-authorization: " .. token, + "", + "", + }, "\r\n")) + end + + function p.send(opcode, payload) + p.tcp:write(frame.create_frame(opcode, payload, true, true)) + end + + function p.count(opcode) + local n = 0 + for _, f in ipairs(p.frames) do + if f.opcode == opcode then + n = n + 1 + end + end + return n + end + + function p.close_frames() + local out = {} + for _, f in ipairs(p.frames) do + if f.opcode == frame.OPCODE.CLOSE then + table.insert(out, tostring(f.code)) + end + end + return out + end + + function p.connect(on_connect) + p.tcp:connect("127.0.0.1", port, function(err) + assert(not err, err) + p.connected = true + p.start_reading() + if on_connect then + on_connect() + end + end) + end + + return p +end + +-- Claude in a process of its own: a second headless Neovim that runs claude-process.lua, connects, and answers every +-- ping at once, whatever blocks this Neovim. The in-process Claude of M.peer answers only when this Neovim's loop runs, +-- so it cannot show a plugin that blocks for a few intervals. `mode` is "big::" (at ping n, send a text frame of +-- that many bytes before the pong) or "late::" (sleep that long before the pong of ping n, as a machine that +-- sleeps with Neovim does). `silence()` makes it stop answering. `kill()` ends it. +function M.spawn_claude(port, token, mode) + local here = vim.fs.dirname(debug.getinfo(1, "S").source:sub(2)) + local flag = vim.fn.tempname() + local env = {} + for k, v in pairs(vim.fn.environ()) do + table.insert(env, k .. "=" .. v) + end + vim.list_extend(env, { + "VWC_HARNESS=" .. here .. "/harness.lua", + "VWC_CHILD=" .. here .. "/claude-process.lua", + "VWC_PEER_PORT=" .. port, + "VWC_PEER_TOKEN=" .. token, + "VWC_PEER_SILENT_FLAG=" .. flag, + "VWC_PEER_MODE=" .. (mode or ""), + }) + local proc = uv.spawn(vim.v.progpath, { + args = { + "--headless", + "-u", + "NONE", + "-i", + "NONE", + "--cmd", + "lua vim.opt.rtp:prepend(os.getenv('VWC_REPO'))", + "-c", + -- The path goes through the environment, not into Ex syntax: `:luafile` would expand a `%`, `#` or `*` in it. + "lua dofile(os.getenv('VWC_CHILD'))", + }, + env = env, + }, function() end) + assert(proc, "could not start the Claude process") + local claude = {} + function claude.silence() + io.open(flag, "w"):close() + end + function claude.kill() + proc:kill("sigterm") + os.remove(flag) + end + return claude +end + +-- The kernel's TCP state of the plugin's end of the connection to Claude's local port (from /proc/net/tcp), "gone" +-- when no such connection is listed, and nil on a host without /proc/net/tcp (macOS, BSD). +function M.tcp_state(server_port, peer_port) + local file = io.open("/proc/net/tcp", "r") + if not file then + return nil + end + local names = + { ["01"] = "ESTABLISHED", ["06"] = "TIME_WAIT", ["07"] = "CLOSE", ["08"] = "CLOSE_WAIT", ["09"] = "LAST_ACK" } + local want_local, want_remote = string.format(":%04X", server_port), string.format(":%04X", peer_port) + for line in file:lines() do + local loc, rem, st = line:match("^%s*%d+: (%x+:%x+) (%x+:%x+) (%x%x)") + if loc and loc:sub(-5) == want_local and rem:sub(-5) == want_remote then + file:close() + return names[st] or st + end + end + file:close() + return "gone" +end + +M.frame = frame +M.uv = uv +return M diff --git a/.agents/skills/verify-ws-connection/replays/protocol-close-window-full.lua b/.agents/skills/verify-ws-connection/replays/protocol-close-window-full.lua new file mode 100644 index 000000000..5bec73dfc --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/protocol-close-window-full.lua @@ -0,0 +1,103 @@ +-- Scenario: Claude stops reading, a large message fills its receive window, and Claude sends a frame that breaks the +-- protocol. Before #455 the client stayed in server.clients, in state "closing", for as long as Claude did not read: +-- is_claude_connected() stayed true and on_disconnect (the diff cleanup) did not run. +-- Promise: a client the plugin closes is reported once and leaves server.clients at once, and its Close frame is still +-- delivered before its socket closes, as long as Claude reads within one keepalive window (two ticks). After that window +-- with no progress the deadline of close_client closes the socket and drops the frame. +-- Model path: Accept, Read (upgrade request), WriteDone (101), ClaudeStopsReading, PluginSendsLarge, Read (the bad +-- frame: close_client queues its Close frame, on_error reports the client), then Claude reads again. +local H = dofile(vim.fs.dirname(debug.getinfo(1, "S").source:sub(2)) .. "/harness.lua") +local INTERVAL = 500 -- ms; the Close frame has one keepalive window (2 ticks, 1000 ms) before its deadline closes the socket + +local plugin = H.start_plugin(INTERVAL) +H.log("plugin: server on port %d, ping timer every %d ms", plugin.port, INTERVAL) + +local claude = H.peer(plugin.port) +claude.answer_pings = true +claude.connect(function() + claude.hello(plugin.token) +end) +H.wait(2000, function() + local client = plugin.client() + return claude.opened and client and client.state == "connected" +end) +local client = assert(plugin.client(), "no client") +H.log("claude: %s; plugin: %s is %s", tostring(claude.status_line), client.id, client.state) + +-- Claude stops reading and answering. The plugin sends it a message (a notification with a large field) until +-- Claude's receive window is full and the rest waits in libuv's write queue. +claude.stop_reading() +claude.answer_pings = false +local sent = 0 +local blob = string.rep("x", 4 * 1024 * 1024) +while client.tcp_handle:get_write_queue_size() == 0 and sent < 64 do + plugin.srv.broadcast("test/large", { blob = blob }) + sent = sent + 4 + H.wait(20) +end +H.log( + "plugin: sent %d MiB to Claude; %d bytes wait in libuv's write queue", + sent, + client.tcp_handle:get_write_queue_size() +) +assert(client.tcp_handle:get_write_queue_size() > 0, "Claude's window did not fill") + +-- Claude sends a binary frame, which the plugin does not accept (close 1003). The client must leave at once, with +-- no help from Claude, whose window stays full. +claude.send(H.frame.OPCODE.BINARY, "not text") +H.wait(1000, function() + return #plugin.disconnects > 0 +end) +local wait_ms = INTERVAL -- half of the window: the client left long ago, and the socket is still open +H.wait(wait_ms) +local listed = plugin.srv.state.server.clients[client.id] == client +local status = plugin.srv.get_status() +local d = plugin.disconnects[1] +H.log("plugin: %s is %s after the binary frame", client.id, client.state) + +H.check( + "the client left server.clients and was reported once, while Claude does not read", + not listed and status.client_count == 0 and #plugin.disconnects == 1 and d.code == 1006, + string.format( + "listed=%s, client_count=%d, on_disconnect calls=%d, %d ms after the binary frame", + tostring(listed), + status.client_count, + #plugin.disconnects, + wait_ms + ) +) +H.check( + "the plugin no longer counts Claude as connected", + require("claudecode").is_claude_connected() == false, + "require('claudecode').is_claude_connected() = " .. tostring(require("claudecode").is_claude_connected()) +) +H.check( + "its socket stays open for the Close frame, which waits in libuv's queue, for half a keepalive window", + not client.tcp_handle:is_closing() and client.tcp_handle:get_write_queue_size() > 0, + string.format( + "is_closing()=%s, %d bytes in libuv's write queue", + tostring(client.tcp_handle:is_closing()), + client.tcp_handle:get_write_queue_size() + ) +) + +-- Claude reads again within the window: the queued writes and the Close frame go out, and only then does the socket close. +claude.start_reading() +H.wait(10000, function() + return claude.count(H.frame.OPCODE.CLOSE) > 0 and client.tcp_handle:is_closing() +end) +H.check( + "Claude gets the Close frame (1003) once it reads, and then the socket closes", + vim.deep_equal(claude.close_frames(), { "1003" }) and client.tcp_handle:is_closing(), + string.format( + "Close frames %s, is_closing()=%s", + table.concat(claude.close_frames(), ","), + tostring(client.tcp_handle:is_closing()) + ) +) +H.check( + "Claude's reading again reports nothing more", + #plugin.disconnects == 1, + string.format("%d on_disconnect call(s)", #plugin.disconnects) +) +H.finish() diff --git a/.agents/skills/verify-ws-connection/replays/run.sh b/.agents/skills/verify-ws-connection/replays/run.sh new file mode 100755 index 000000000..50f0cf235 --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/run.sh @@ -0,0 +1,23 @@ +#!/usr/bin/env bash +# Run one replay in a headless Neovim with this checkout first on 'runtimepath' and every XDG dir and +# CLAUDE_CONFIG_DIR in a fresh temp dir, so the run never touches your config or ~/.claude. +# The replay runs from -c, not -l, so that Neovim 0.8 runs it too. Paths pass through the environment, so a path with a +# space or a quote needs no escaping. +# Usage: run.sh .lua (NVIM=/path/to/nvim overrides the Neovim binary) +set -euo pipefail +here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +repo=$(git -C "$here" rev-parse --show-toplevel) +script=${1:?usage: run.sh .lua} +[[ -f $here/$script ]] || { + echo "no replay $here/$script" >&2 + exit 2 +} +nvim=${NVIM:-nvim} +tmp=$(mktemp -d "${TMPDIR:-/tmp}/verify-ws-connection-replay.XXXXXX") +trap 'rm -rf "$tmp"' EXIT +mkdir -p "$tmp"/{config,data,state,cache,claude} +# A replay ends the run with qa! or cq! (harness.lua finish). An error in one ends it with cq!, as -l did. +XDG_CONFIG_HOME=$tmp/config XDG_DATA_HOME=$tmp/data XDG_STATE_HOME=$tmp/state XDG_CACHE_HOME=$tmp/cache \ + CLAUDE_CONFIG_DIR=$tmp/claude VWC_REPO=$repo VWC_REPLAY=$here/$script "$nvim" --headless -u NONE -i NONE \ + --cmd "lua vim.opt.rtp:prepend(os.getenv('VWC_REPO'))" \ + -c "lua local ok, err = pcall(dofile, os.getenv('VWC_REPLAY')); if not ok then io.stderr:write(tostring(err), '\\n'); vim.cmd('cq!') end; vim.cmd('qa!')" diff --git a/.agents/skills/verify-ws-connection/replays/short-block-after-ping.lua b/.agents/skills/verify-ws-connection/replays/short-block-after-ping.lua new file mode 100644 index 000000000..b5547f018 --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/short-block-after-ping.lua @@ -0,0 +1,90 @@ +-- Scenario: one main-loop block of 1.3 ping intervals that starts right after a ping was sent. The late tick after it can +-- run before the read of Claude's pong. Before #479 that tick dropped a Claude that answers every ping with 1011: the +-- block is below the wake threshold (interval * 1.5), so last_pong was not reset, and now - last_pong was about 2.3 +-- intervals. Since #488 a tick never drops a client: only the keepalive check does, after the poll that read the pong. +-- Promise: a Claude that answers every ping is not dropped by such a block, and a Claude that stops answering is still +-- dropped, with 1006 for on_disconnect and Close 1011 for Claude. +-- Model path: TimerTicks (a ping), Claude answers, TimerTicks (a ping, Neovim blocks), Claude's pong stays unread, +-- TimerTicks (a ping, the tick stamps nothing new and drops nothing), PollAndCheck (the pong is read, the stamp clears). +-- The block runs in a libuv check callback, which runs after the poll phase of the loop iteration that ran the timer. So +-- the socket read comes only after the next tick. With libuv 1.44 (Neovim 0.8) any block does that. With newer libuv a +-- block in a check or I/O callback does, and a block in vim.schedule or a timer callback reads the socket first. +local H = dofile(vim.fs.dirname(debug.getinfo(1, "S").source:sub(2)) .. "/harness.lua") +local INTERVAL, BLOCK = 200, 260 -- ms: BLOCK / INTERVAL = 1.3, below the 1.5 wake threshold +local SETTLE, SILENT = 1500, 3000 -- ms: how long Claude must stay listed, and how long a silent Claude gets to be dropped + +local plugin = H.start_plugin(INTERVAL) +H.log("plugin: server on port %d, ping timer every %d ms", plugin.port, INTERVAL) +local claude = H.peer(plugin.port) +claude.answer_pings = true +claude.connect(function() + claude.hello(plugin.token) +end) +H.wait(5000, function() + local client = plugin.client() + return client and client.state == "connected" and claude.count(H.frame.OPCODE.PING) >= 3 +end) +local client = assert(plugin.client(), "no client") +H.log("claude: connected and answered %d pings", claude.count(H.frame.OPCODE.PING)) + +-- Right after the timer callback sent the next ping (last_ping changes), in the same loop iteration and before the next +-- poll phase can read Claude's pong, block the loop for 1.3 intervals. +local seen, blocked = client.last_ping, false +local check = H.uv.new_check() +check:start(function() + if not blocked and client.last_ping ~= seen then + blocked = true + check:stop() + H.log("plugin: a ping was just sent; the main loop blocks for %d ms (%.1f intervals)", BLOCK, BLOCK / INTERVAL) + H.uv.sleep(BLOCK) + end +end) + +H.wait(SETTLE, function() + return #plugin.disconnects > 0 +end) +local dropped = plugin.disconnects[1] +H.log( + "claude: %d pings, Close frames %s, EOF %s", + claude.count(H.frame.OPCODE.PING), + vim.inspect(claude.close_frames()), + tostring(claude.eof) +) +H.check("the block happened", blocked, "blocked = " .. tostring(blocked)) +H.check( + "Claude, which answers every ping, is not dropped by one 1.3-interval block", + dropped == nil and plugin.client() ~= nil, + dropped and string.format("on_disconnect(%s, %s, %q) at %d ms", dropped.id, dropped.code, dropped.reason, dropped.at) + or string.format("no on_disconnect in %d ms, still listed", SETTLE) +) + +-- Claude stops answering: it is still dropped, by the first check after a tick that finds its oldest unanswered ping +-- 2.5 intervals old. +claude.answer_pings = false +local silent_at = H.ms() +H.log("claude: stops answering pings") +H.wait(SILENT, function() + return #plugin.disconnects > 0 +end) +H.wait(500, function() + return claude.eof +end) +local silent = plugin.disconnects[1] +H.check( + "a Claude that stops answering is still dropped, with Close 1011", + silent ~= nil + and silent.code == 1006 + and silent.reason == "Connection timeout" + and vim.deep_equal(claude.close_frames(), { "1011" }), + silent + and string.format( + "on_disconnect(%s, %s, %q) %.1f intervals after Claude went silent, Close frames %s", + silent.id, + silent.code, + silent.reason, + (silent.at - silent_at) / INTERVAL, + table.concat(claude.close_frames(), ",") + ) + or string.format("no on_disconnect in %d ms", SILENT) +) +H.finish() diff --git a/.agents/skills/verify-ws-connection/replays/stop-before-on-close.lua b/.agents/skills/verify-ws-connection/replays/stop-before-on-close.lua new file mode 100644 index 000000000..ce583e4b1 --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/stop-before-on-close.lua @@ -0,0 +1,82 @@ +-- Scenario: the server stops between Claude's Close frame and the vim.schedule'd on_close. Before #455 nothing closed the +-- plugin's socket, which stayed in CLOSE_WAIT until Neovim exited. +-- Promise: every socket the plugin is done with gets closed. A stop reports no client (M.stop rejects the pending +-- diffs itself), and the socket of the client that it dropped still closes. +-- Model path: Accept, Read (upgrade request), WriteDone (101), Read (Claude's Close: the reply is written, the state is +-- "closing", on_close is scheduled), ServerStops, ScheduledRuns (on_close: _disconnect_client finds no client and +-- closes its socket), ReadEOF (Claude hung up). +local H = dofile(vim.fs.dirname(debug.getinfo(1, "S").source:sub(2)) .. "/harness.lua") + +local plugin = H.start_plugin(nil) +H.log("plugin: server on port %d", plugin.port) + +local claude = H.peer(plugin.port) +claude.answer_pings = true +claude.connect(function() + claude.hello(plugin.token) +end) +H.wait(2000, function() + local client = plugin.client() + return claude.opened and client and client.state == "connected" +end) +local client = assert(plugin.client(), "no client") +local claude_port = claude.tcp:getsockname().port +H.log("claude: %s; plugin: %s is %s", tostring(claude.status_line), client.id, client.state) + +-- A libuv check handle runs right after the poll phase in which the plugin read Claude's Close frame, before the +-- main loop runs the scheduled on_close. It stops the server there: server/init.lua M.stop, the call that init.lua +-- M.stop (:ClaudeCodeStop) makes. The rest of init.lua M.stop (lock file, selection, mention queue) does not touch +-- clients. +local stopped +local check = H.uv.new_check() +check:start(function() + if client.state == "closing" and not stopped then + stopped = true + check:stop() + H.log("plugin: read Claude's Close frame (state %s); the server stops before on_close runs", client.state) + local ok, err = plugin.srv.stop() + H.log("plugin: server/init.lua M.stop() = %s %s", tostring(ok), tostring(err)) + end +end) + +claude.send(H.frame.OPCODE.CLOSE, string.char(0x03, 0xE8) .. "bye") +H.wait(2000, function() + return claude.count(H.frame.OPCODE.CLOSE) > 0 +end) +H.log("claude: got Close %s back, and closes its socket", table.concat(claude.close_frames(), ",")) +claude.tcp:close() + +H.wait(1000) +H.check( + "the server stopped between the Close frame and on_close", + stopped == true and plugin.srv.state.server == nil, + "server/init.lua M.state.server = " .. tostring(plugin.srv.state.server) +) +H.check( + "the stop reported no client", + #plugin.disconnects == 0, + string.format("%d on_disconnect calls", #plugin.disconnects) +) +H.check( + "the plugin's socket is closed 1 s after Claude closed its end", + client.tcp_handle:is_closing(), + string.format( + "tcp_handle:is_closing() = %s, fileno = %s", + tostring(client.tcp_handle:is_closing()), + tostring(client.tcp_handle:fileno()) + ) +) +local state = H.tcp_state(plugin.port, claude_port) +if state == nil then + H.skip( + "the kernel does not hold it in CLOSE_WAIT", + "this host has no /proc/net/tcp; the is_closing() check above decides" + ) +else + H.check( + "the kernel does not hold it in CLOSE_WAIT", + state ~= "CLOSE_WAIT", + string.format("/proc/net/tcp: 127.0.0.1:%d <- :%d is %s", plugin.port, claude_port, state) + ) +end +H.finish() diff --git a/.agents/skills/verify-ws-connection/replays/two-blocks-before-read.lua b/.agents/skills/verify-ws-connection/replays/two-blocks-before-read.lua new file mode 100644 index 000000000..660e87519 --- /dev/null +++ b/.agents/skills/verify-ws-connection/replays/two-blocks-before-read.lua @@ -0,0 +1,82 @@ +-- Scenario: the main loop blocks twice in a row, each time for 1.3 ping intervals (interval 200 ms), starting right +-- after a ping: first in a libuv check callback, then in a vim.schedule callback. Claude runs in a process of its own and +-- answers every ping at once, so its pongs wait in the socket for the whole 2.6 intervals. On Neovim 0.8 (libuv 1.44) +-- libuv runs the timers at the end of a pass and again at the start of the next one, with the vim.schedule block +-- between them: two ticks run with no read of Claude's socket between them. Before the keepalive check (#488) the +-- second tick dropped Claude: #479 pinged again at the first tick that found no pong and dropped at the second. +-- Promise: a Claude that answers every ping is not dropped, and a Claude that stops answering is still dropped. +-- Model path: TimerTicks, TimerTicks (Claude answered before each, the plugin read none), PollAndCheck (the poll reads the +-- pongs, and the check finds the stamp cleared). Without JudgesAfterRead the second or third tick drops Claude. +-- Newer Neovim (libuv 1.52) reads the socket between these two blocks, so the replay passes there on the old code too. +local H = dofile(vim.fs.dirname(debug.getinfo(1, "S").source:sub(2)) .. "/harness.lua") +local INTERVAL, BLOCK = 200, 260 -- ms: BLOCK / INTERVAL = 1.3 +local SETTLE, SILENT = 2000, 3000 -- ms: how long Claude must stay listed, and how long a silent Claude gets to be dropped + +local plugin = H.start_plugin(INTERVAL) +H.log("plugin: server on port %d, ping timer every %d ms", plugin.port, INTERVAL) +local claude = H.spawn_claude(plugin.port, plugin.token) +local seen, pings = 0, 0 +H.wait(8000, function() + local client = plugin.client() + if client and client.state == "connected" and client.last_ping ~= seen then + seen, pings = client.last_ping, pings + 1 + end + return pings >= 4 +end) +local client = assert(plugin.client(), "no client") +H.log("claude: connected, %d pings seen", pings) + +-- Right after the timer callback sent the next ping (last_ping changes), in the same loop iteration, block for 1.3 +-- intervals in this check callback. A vim.schedule callback queued from it then blocks for 1.3 intervals again. +seen = client.last_ping +local blocks = 0 +local check = H.uv.new_check() +check:start(function() + if blocks == 0 and client.last_ping ~= seen then + check:stop() + H.log("plugin: a ping was just sent; block %d ms (%.1f intervals) in a check callback", BLOCK, BLOCK / INTERVAL) + H.uv.sleep(BLOCK) + blocks = 1 + vim.schedule(function() + H.log("plugin: block %d ms in vim.schedule", BLOCK) + H.uv.sleep(BLOCK) + blocks = 2 + end) + end +end) + +H.wait(SETTLE, function() + return #plugin.disconnects > 0 +end) +local dropped = plugin.disconnects[1] +H.check("both blocks happened", blocks == 2, "blocks = " .. blocks) +H.check( + "Claude, which answers every ping, is not dropped by two 1.3-interval blocks", + dropped == nil and plugin.client() ~= nil, + dropped and string.format("on_disconnect(%s, %s, %q) at %d ms", dropped.id, dropped.code, dropped.reason, dropped.at) + or string.format("no on_disconnect in %d ms, still listed", SETTLE) +) + +-- Claude stops answering: it is still dropped. +claude.silence() +local silent_at = H.ms() +H.log("claude: stops answering pings") +H.wait(SILENT, function() + return #plugin.disconnects > 0 +end) +local silent = plugin.disconnects[1] +H.check( + 'a Claude that stops answering is still dropped, with 1006 "Connection timeout"', + silent ~= nil and silent.at > silent_at and silent.code == 1006 and silent.reason == "Connection timeout", + silent + and string.format( + "on_disconnect(%s, %s, %q) %.1f intervals after Claude went silent", + silent.id, + silent.code, + silent.reason, + (silent.at - silent_at) / INTERVAL + ) + or string.format("no on_disconnect in %d ms", SILENT) +) +claude.kill() +H.finish() diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index c795908d7..6410b4af0 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -125,9 +125,9 @@ The block exits 0 only when all three hold: strace exits 0 (it returns the exit A unit test that writes files writes them in a folder from `tests/helpers/temp_dir.lua` (`temp_dir.new()` in `setup`, `temp_dir.remove(dir)` in `teardown`), not at a fixed path under `/tmp`. Every test run on a host shares `/tmp`, so two suites that run at once would overwrite and delete each other's files. -A PR that changes a `.lua` or `.vim` file under `lua/` or `plugin/` also changes what `.agents/skills/verify-diff-lifecycle/covered.lock` records, and the advisory `covered-lock` CI job turns red. Run `.agents/skills/verify-diff-lifecycle/check.sh --record` and commit `covered.lock`, or ask a maintainer to. +A PR that changes a `.lua` or `.vim` file under `lua/` or `plugin/` also changes what a `covered.lock` records, and the advisory `covered-lock` CI job turns red. `.agents/skills/verify-diff-lifecycle/covered.lock` records every such file. Each other `.agents/skills/verify-*/covered.lock` records the files that its model describes (the `COVERED` list in its `check.sh`). Run `for check in .agents/skills/verify-*/check.sh; do "$check" --hash-only; done` (a few seconds for each skill, no TLC) to see which locks are stale. A bare `verify-*` glob would pass the second script to the first as an argument. For each stale one, read the "Update after an intended change" section of its `SKILL.md`, run its `check.sh --record` once its model still describes the code, and commit its `covered.lock`, or ask a maintainer to. -Two PRs that edit the same Lua file, or that add or delete neighbouring Lua files, conflict in `covered.lock` once one of them merges. That conflict is expected, because the merged code needs a new record. To resolve it, merge `origin/main` into your branch, resolve any code conflicts, run `.agents/skills/verify-diff-lifecycle/check.sh --record`, `git add` `covered.lock`, and commit the merge. +Two PRs that edit the same Lua file, or that add or delete neighbouring Lua files, conflict in `covered.lock` once one of them merges. That conflict is expected, because the merged code needs a new record. To resolve it, merge `origin/main` into your branch, resolve any code conflicts, run the `check.sh --record` of each skill whose lock conflicts or reads stale, `git add` each `covered.lock`, and commit the merge. ## Release Automation diff --git a/lua/claudecode/server/README.md b/lua/claudecode/server/README.md index 007139e75..161689e62 100644 --- a/lua/claudecode/server/README.md +++ b/lua/claudecode/server/README.md @@ -97,7 +97,7 @@ Layers, top to bottom: - Notification handlers run in `pcall`. Their errors and return values are discarded, and an unknown notification is ignored without a reply [server/init.lua:M._handle_notification] - A deferred response is keyed by `tostring(coroutine)` in `_G.claude_deferred_responses`. It replies to `result.client` with the original request id. A result with `content` is sent as `result`, one with `error` is sent as `error`, and a result with neither becomes -32603 [server/init.lua:M._setup_deferred_response] - `_handle_request` records each request in `M.state.in_flight` while its handler runs. `M.stop` sends -32603 "Internal error" (`data`: "The server stopped before the call finished") for every request still recorded, before it stops the TCP server, and `_handle_request` sends nothing for that request afterwards. A blocking tool has no response sender before its handler yields, so nothing else can answer a request whose handler is still running [server/init.lua:M._handle_request] [server/init.lua:M.stop]. The README at the repository root, under Global Invariants, lists what Claude receives at an exit. -- A ping timer tick pings every connected client and never closes one for a missing answer. `client.ping_unanswered_since` holds the loop time of the oldest ping sent since bytes were last read from the client. The read callback clears it on any bytes, not only a pong: Claude shows it is alive by writing anything, and a pong that waits behind more unread data than the socket holds is not in the first poll after a block. The tick calls `vim.loop.update_time()` before it reads the clock, because libuv caches the loop time when a pass of the main loop starts and runs the timers of the pass with it, and a callback that ran before the tick in the pass can have blocked since, or the machine can have slept in it. A stale time would hide a wake and would stamp a ping older than it is. Each tick that pinged a client arms `after_next_poll` (below), and its callback runs `judge_silence` after the next poll. libuv runs the check handle right after the poll phase that reads the sockets, so every byte that reached a socket before the loop time of the check was read. The check closes each client that the tick pinged when its oldest ping is `interval * 2.5` old, but only if its loop time is at most `interval * 1.5` after the tick. After a longer block Neovim and Claude can have slept together (a suspended machine), and Claude has had no time to answer. A tick cannot decide this, because libuv can run a tick before it reads the pong that Claude sent: after a block in a check callback or an I/O read callback, and, with libuv 1.44 (bundled in Neovim 0.8), after a block in any callback. libuv 1.44 also runs the timers again at the end of a pass, so two ticks can run with no read between them. `vim.schedule` cannot decide it either, because Neovim runs its callbacks between two passes, so it can run one before the read. Drop bound: a block of the main loop, of any length and in any callback, does not close a Claude that writes something within `interval * 2.5` (75 s by default) of each ping. A tick never closes a client, a check judges only after a poll within `interval * 1.5` of its tick, and any bytes clear the stamp. A client that writes data but never answers a ping is not closed by this rule: it is alive, and the plugin does not judge what it writes (the stall rule below closes it when it stops reading, but only once the kernel's socket buffers are full and libuv's write queue backs up, because a queue that is empty counts as progress). A block longer than `interval * 1.5` restarts the count: the next tick sees the gap, takes it for a wake and clears every stamp. So a block delays the close of a silent Claude, and a run of such blocks can postpone it. Without a long block, a Claude that sends nothing is closed at the first read of its socket after the third tick that follows its first unanswered ping, which is 90 s by default after that ping. The Close frame of a dropped client carries 1011 "Keepalive timeout" (RFC 6455 reserves 1006, so no Close frame carries it), `on_disconnect` gets 1006 "Connection timeout", and the check logs `Closed client_: no reply for s` at info level. A peer that stopped reading does not get that Close frame: once its receive window is full, every write to it (replies, pings, and the Close frame) waits in libuv's queue, and closing the socket drops the queue [server/tcp.lua:M.start_ping_timer] [server/tcp.lua:judge_silence] [server/tcp.lua:drop_client] +- A ping timer tick pings every connected client and never closes one for a missing answer. `client.ping_unanswered_since` holds the loop time of the oldest ping sent since bytes were last read from the client. The read callback clears it on any bytes, not only a pong: Claude shows it is alive by writing anything, and a pong that waits behind more unread data than the socket holds is not in the first poll after a block. The tick calls `vim.loop.update_time()` before it reads the clock, because libuv caches the loop time when a pass of the main loop starts and runs the timers of the pass with it, and a callback that ran before the tick in the pass can have blocked since, or the machine can have slept in it. A stale time would hide a wake and would stamp a ping older than it is. Each tick that pinged a client arms `after_next_poll` (below), and its callback runs `judge_silence` after the next poll. libuv runs the check handle right after the poll phase that reads the sockets, so every byte that reached a socket before that poll started was read. The check closes each client that the tick pinged when its oldest ping is `interval * 2.5` old, but only if its loop time is at most `interval * 1.5` after the tick. After a longer block Neovim and Claude can have slept together (a suspended machine), and Claude has had no time to answer. A tick cannot decide this, because libuv can run a tick before it reads the pong that Claude sent: after a block in a check callback or an I/O read callback, and, with libuv 1.44 (bundled in Neovim 0.8), after a block in any callback. libuv 1.44 also runs the timers again at the end of a pass, so two ticks can run with no read between them. `vim.schedule` cannot decide it either, because Neovim runs its callbacks between two passes, so it can run one before the read. Drop bound: a Claude that answers each ping before the next tick is not closed by a block of the main loop of any length in any callback, or by a sleep of the machine. A tick never closes a client, a check judges only after a poll within `interval * 1.5` of its tick, and any bytes clear the stamp. A pong that comes later than one interval can wait unread in a socket: a callback that blocks inside the poll phase after the poll took its snapshot, and that refreshes the loop time, leaves the bytes that arrived during the block unread, and the check then closes the client once its oldest ping is `interval * 2.5` old (75 s by default). A real Claude answers a ping at once. A client that writes data but never answers a ping is not closed by this rule: it is alive, and the plugin does not judge what it writes (the stall rule below closes it when it stops reading, but only once the kernel's socket buffers are full and libuv's write queue backs up, because a queue that is empty counts as progress). A tick more than `interval * 1.5` after the tick before it is a wake: it takes the gap for a sleep, clears every stamp and restarts the count. A block of more than half an interval that starts just before a tick is enough, so a run of such blocks can postpone the close of a silent Claude. A silent Claude is closed by the first check that finds its oldest unanswered ping `interval * 2.5` old. That is 90 s after the ping when the ticks come on time. A tick that runs late moves the ticks after it back, so one late tick delays the close. Two late ticks in a row, or a poll that a block delays after a tick, can bring the close as early as 75 s, and never earlier. The Close frame of a dropped client carries 1011 "Keepalive timeout" (RFC 6455 reserves 1006, so no Close frame carries it), `on_disconnect` gets 1006 "Connection timeout", and the check logs `Closed client_: no reply for s` at info level. A peer that stopped reading does not get that Close frame: once its receive window is full, every write to it (replies, pings, and the Close frame) waits in libuv's queue, and closing the socket drops the queue [server/tcp.lua:M.start_ping_timer] [server/tcp.lua:judge_silence] [server/tcp.lua:drop_client] - A Claude that answers each ping but never reads would keep that queue, which is Neovim's memory, without limit, so the server also closes a connected client that answers and whose write queue made no progress at two ticks in a row. Each tick calls `is_client_reading` for each connected client, which calls `sample_write_progress`: it compares `queued_bytes - get_write_queue_size()` with its value at the last progress, and an empty queue counts as progress. A tick that finds progress clears `client.write_stalled`. The first tick that finds none sets it. The second asks for a confirmation, and a confirmation that still finds no progress drops the client: the Close frame carries 1011 "Not reading", `on_disconnect` gets 1006 "Write queue stalled", and the server logs `Closed client_: not reading for s, KB queued` at info level. The confirmation runs right after the next poll. libuv reports that a socket is writable again only in a poll phase, so a tick that Neovim runs after a main-loop block inside an I/O callback can find no progress although Claude read during the block, whether the tick is late or on time. `after_next_poll` arms a check handle, which libuv runs right after each poll phase in every version, and an idle handle, which keeps that poll from waiting for a timer or a socket. The check callback closes both handles, removes them from `server.pending_polls`, and judges the queue once more: progress clears `write_stalled`, and no progress drops the client. A client that left or started to leave in the meantime, because the poll read its EOF, a read error, its Close frame or a protocol error, is skipped without a log line. `stop_server` closes the handles of a confirmation that has not run, which `server.pending_polls` lists. If libuv cannot create a handle, the tick leaves the client for the next tick. The look is a sample at one moment, not proof. libuv takes its snapshot of the ready sockets when a poll starts, so a callback that blocks inside that poll, after the snapshot, hides what Claude reads during the block from the check callback that follows. A client that was stalled for the whole window and resumes during such a block is dropped. That is a deadline race, as with any timeout: the client was stalled when the window ended, and what it read afterwards is not reported yet. Verifier probes closed a reader that resumed 0.1 s into a 0.5 s to 1.5 s block inside the confirming poll, on Neovim 0.12.3 and 0.8.0, at 3 s, 5 s and 30 s intervals. A block after the tick and before that poll, or in a scheduled callback, keeps the reader. The bound is two to three ticks after the last progress, which is 60 s to 90 s at the default interval, plus the delay of late ticks, each of which comes at most `interval * 1.5` after the tick before it. A tick that comes more than `interval * 1.5` after the tick before it counts as a wake from sleep. A wake tick starts a fresh stall window: it clears the count and judges nothing, so it delays the drop by one tick when the count was clear, and by two ticks when the wake tick takes the place of the confirming tick. The next two ticks always count, wake ticks or not, because wake ticks that come again and again are a loop that stays blocked, not sleeps. So whatever the pattern of late ticks, a stalled client is closed at the second tick after a fresh window started. A wake tick three or more ticks after the last fresh start starts a new window. The bound is never the size of the queue, so a Claude that reads slowly, or is sent one message of tens of MB, stays connected while libuv writes any of it. libuv writes more only after the kernel reports the socket writable again, which took 1.2 to 1.5 MB of reading on a Linux loopback socket with default buffers (measured), so a Claude that reads less than about 1.4 MB per window counts as stalled while a backlog exists, and one that reads just faster than that still lets the queue grow as long as Neovim queues more than it reads. `write` queues a frame of more than 1 MiB in pieces of 1 MiB, because libuv on Windows lowers the queue only when a whole write request is done, so a large frame shows its progress per piece there too, and the callback of the last piece reports the frame. [server/tcp.lua:M.start_ping_timer] [server/tcp.lua:judge_stall] [server/tcp.lua:after_next_poll] [server/tcp.lua:M.stop_server] [server/client.lua:M.is_client_reading] [server/client.lua:M.sample_write_progress] [server/client.lua:write] - On one tick a client counts as answered when no ping of it waited for `interval * 2`. Only a client that answered is confirmed for a stall. A client that did not answer is dropped by the keepalive check above, whatever its write queue shows. A client that answers while its queue is stalled is not saved: its bytes clear the stamp, the next tick finds it answered, and then asks for the confirmation. Every connected client is sampled on every tick except one that starts a fresh stall window, answering or not, so "two ticks in a row" means consecutive ticks. A tick gap above `interval * 1.5` counts as a wake from sleep and clears `ping_unanswered_since` of each connected client. A wake tick that starts a fresh stall window also resets `last_drain`, clears `write_stalled`, and does not sample the queue. `last_drain` feeds only the `not reading for s` of the log line, so the reset keeps the sleep out of it. A wake tick within two ticks after the start of a fresh window clears the stamps only, and counts like any tick. A client that is not connected is not pinged, so a main loop that blocks during the handshake does not count against it [server/tcp.lua:M.start_ping_timer] [server/client.lua:M.process_data] - `_disconnect_client` is idempotent: `on_disconnect` fires once per client id. A client that already left the server (the server stopped before a scheduled `on_close` or an EOF ran) gets its socket closed there, unless the write callback of its Close frame will close it [server/tcp.lua:M._disconnect_client] diff --git a/lua/claudecode/server/tcp.lua b/lua/claudecode/server/tcp.lua index 5e8e7768e..da3673282 100644 --- a/lua/claudecode/server/tcp.lua +++ b/lua/claudecode/server/tcp.lua @@ -507,10 +507,16 @@ end ---Start a periodic ping task to keep connections alive. ---A tick pings every connected client and never drops one. A client whose oldest ping is `interval * 2.5` old is dropped ---at the first read of its socket after a tick [judge_silence], if the loop ran that read within `interval * 1.5` of the ----tick. A block longer than that restarts the count (the next tick is a wake). Any bytes read from a client clear its ----stamp, so a Claude that sends anything, also a large message before its pong, is not dropped. A Claude that sends ----nothing is dropped after the third tick that follows its first unanswered ping: the half interval keeps timer jitter ----from moving the drop. A client that answered is also judged for a stall of its write queue [judge_stall]. +---tick. A tick more than `interval * 1.5` after the tick before it is a wake: it clears every stamp and restarts the +---count (a block of more than half an interval that starts just before a tick is enough). Any bytes read from a client +---clear its stamp, so a Claude that sends anything, also a large message before its pong, is not dropped. A Claude that +---answers each ping before the next tick is not dropped by any block or sleep. A pong that comes later than one +---interval can wait unread when a callback blocks inside the poll phase and refreshes the loop time, and the client is +---then dropped once its ping is `interval * 2.5` old. A Claude that sends nothing is dropped by the first check that +---finds its oldest ping `interval * 2.5` old: 3 intervals after that ping when the ticks come on time. A late tick moves the ticks after +---it back, so one late tick delays the drop. Two late ticks in a row, or a poll that a block delays after a tick, can +---bring it as early as 2.5 intervals, and never earlier. A client that answered is also judged for a stall of its write +---queue [judge_stall]. ---@param server TCPServer The server object ---@param interval number Ping interval in milliseconds (default: 30000) ---@return table? timer The timer handle, or nil if creation failed diff --git a/tests/unit/server/connection_lifecycle_spec.lua b/tests/unit/server/connection_lifecycle_spec.lua index 9a06b55f7..1d58fe1c1 100644 --- a/tests/unit/server/connection_lifecycle_spec.lua +++ b/tests/unit/server/connection_lifecycle_spec.lua @@ -988,9 +988,9 @@ describe("The lifecycle of a WebSocket connection", function() end) end) - -- Two rules judge a connected client on each ping tick. The pong rule gives a client without a pong one more tick - -- (`pong_overdue`) and then drops it. The stall rule drops a client that answers, whose write queue made no progress at - -- two observations in a row. The pong rule runs first, so only a client that answers is judged for a stall. + -- Two rules judge a connected client on each ping tick. The keepalive drops a client whose oldest ping went unanswered + -- for `interval * 2.5` (`judge_silence`). The stall rule drops a client that answers, whose write queue made no progress + -- at two observations in a row (`judge_stall`). Only a client that answers is judged for a stall. describe("when a client misses a pong and its write queue stalls", function() local reply = string.rep("x", 262144)