feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket connection lifecycle

.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

.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

.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)