Skip to content

fix(diff): save a line the user types into a CRLF proposal with CRLF - #577

Merged
ThomasK33 merged 13 commits into
mainfrom
fix/diff-crlf-new-lines
Nov 12, 2026
Merged

ThomasK33 merged 13 commits into
mainfrom
fix/diff-crlf-new-lines

Conversation

@ThomasK33

@ThomasK33 ThomasK33 commented Nov 12, 2026 •

Copy link
Copy Markdown
Member

Why

In the vertical and horizontal layouts, a proposal whose line breaks are all CRLF was loaded into the proposal buffer with 'fileformat' unix and a CR at the end of each line. The save joined the lines with LF. So a line that the user typed, or the join of two lines, came back with LF, or with a CR in the middle of a line, where Neovim's :w writes CRLF. A CRLF proposal that equals a CRLF file also showed every line as changed, because the file's own buffer is dos and holds its lines without CRs. I found it while verifying #551.

What changed

  1. _setup_blocking_diff (lua/claudecode/diff.lua) loads a proposal as Neovim loads a file. When 'fileformats' includes dos, and the proposal has a line break and only CRLF line breaks, the buffer gets 'fileformat' dos and lines without their CRs. Any other proposal gets 'fileformat' unix and is split at LF, as before. The diff sets 'fileformat' in both cases, because a new buffer takes the first entry of 'fileformats', and that entry can be dos.
  2. _resolve_diff_as_saved joins the lines with the line break of the buffer's 'fileformat' (LF, CRLF for dos, CR for mac), and adds the final one when 'eol' is on. Before, it always used LF. So :setlocal fileformat=dos on an LF proposal now answers CRLF, as :w writes it.
  3. The unified layout does not change. Its buffer is read-only, and its answer is the proposal.
  4. lua/claudecode/README.md states both rules, and that one empty line is saved as one line break of the buffer's 'fileformat'.
  5. tests/integration/diff_accept_crlf_spec.lua is new (159 tests). tests/mocks/vim.lua gives the mock vim.o the default fileformats = "unix,dos", because the unit specs of the diff now read it.
  6. covered.lock of verify-diff-lifecycle records the new hashes of diff.lua (the file, resolve_saved and setup_blocking).

What a user sees

  1. A line that the user types into an accepted CRLF proposal, or two lines that the user joins, comes back with CRLF, as :w writes it. For the proposal "a\r\nb\r\n" and a typed line after the last line, main answers "a\r\nb\r\nx\n" and this PR answers "a\r\nb\r\nx\r\n".
  2. A CRLF proposal that equals the CRLF file shows no difference. Main marked every line.
  3. An unedited proposal still comes back as exactly the proposal, in every layout, under every 'fileformats' value that I ran.
  4. Nothing else changes for the default 'fileformats' (unix,dos): the controls of the spec (an LF proposal, a proposal with CRLF and LF line breaks, a lone CR, no line break, unedited, emptied) give the same bytes on main and here.
  5. 'fileformats' unix (no dos) keeps a CRLF proposal as unix with its CRs, as the file's own buffer does. The equal-text view shows no difference there, and a typed line gets LF, as :w writes it.

Verification

The spec compares the answer with the bytes that Neovim's own :w writes for the same text after the same commands (an oracle that reads the text as a file under the same 'fileformats'), or with an exact expected text.

  1. Red, then green, run on Neovim 0.12.3, 0.11.5, 0.10.4, 0.9.5 and 0.8.0 (all five give the same counts): 159 tests pass with the fix. With origin/main's diff.lua, 105 pass and 54 fail. The unified cases run on 0.8.0 too (fix(diff): say the unified layout runs on Neovim 0.8.0, and run its specs there #564).

  2. Fourteen mutants of the changed lines are each red on Neovim 0.12.3 (the last seven also on 0.8.0, with the same counts). Failed tests per mutant:

    • Split and join: the CRs stay in the lines 70, the join always uses LF 66, the final break is always LF 56, mac is ignored 2, dos for any text with a CRLF 12, dos for a text with no line break 2, dos even with a lone LF 32.
    • 'fileformats' check: no check (always dos) 8, an exact match of unix,dos or dos,unix 4, dos for any value except unix 4, dos only when it is the first entry 42, 'fileformat' always unix 64, always dos 48, set only for dos 12.
  3. A probe of 1860 cases per run on Neovim 0.12.3 and 0.8.0 (three layouts, four old files, 15 proposals, 15 edits) compares each answer with the bytes of a fresh nvim --clean that reads the proposal as a file under the same 'fileformats', runs the same commands and writes with :w. The columns give mismatches. The two Neovim versions give the same numbers.

    'fileformats' main this PR unedited answers that differ from the proposal (main / this PR)
    unix,dos 748 144 0 / 0
    dos,unix 788 184 0 / 0
    unix 304 192 0 / 0
    dos 1104 516 0 / 0
    unix,mac 608 544 0 / 0

    Every mismatch that remains is one of the items under "Not fixed here", or a fold (see below). Cleanup leaves no state, buffer, window or tab behind in any case. Under unix,dos, dos,unix and unix, the equal-text view marks 0 lines in every case.

  4. The only cases where this PR has a mismatch that main does not have are dup_line and dd_first (yyp and dd on line one) against an old file that equals the proposal, for CRLF proposals: 28 cases for each of unix,dos, dos,unix and dos. Diff mode folds every line of an equal text, so those commands act on the whole fold. Main does the same for an equal LF text (same|lf|dup_line), and showed every line of an equal CRLF text as changed, so it did not fold. This follows from item 2 of "What a user sees".

  5. An independent verifier ran its own probe (2604 cases per run) under unix,dos, dos,unix, unix and dos on all five Neovim versions, and under unix,dos,mac, unix,mac and dos,mac on 0.12.3. In every run, 0 unedited answers differ from the proposal.

Not fixed here

These items are tracked in #581. All of them exist on origin/main already. An independent probe that compares each answer with :w of the same buffer found this PR never worse than main.

  1. A CR inside a line, then :setlocal ff=mac. :w writes that CR as NL, and the save keeps the CR. The proposal "a\rb\n" gives "a\rb\r", and :w gives "a\nb\r". Main joined with LF, which was also wrong.
  2. With 'fileformats' unix,mac, Neovim reads a text such as "a\r\nb\r\r\n" as mac. The diff never detects mac (main neither). In 24 cases (an ff=mac edit only), main's answer equals the file-read oracle and this PR's answer does not, because main ignores 'fileformat' when it joins. Against :w of the same buffer, both are wrong in these 24 cases.
  3. An empty proposal, then typed lines. 'eol' stays off (fix(diff): accept a proposal without a final line break as it is in the split layouts #542), so Gox gives "\nx", where :w of an empty file gives "\nx\n".
  4. 'fileformats' that starts with dos, and a proposal with no LF ("", "a", "a\r"). Neovim reads it as dos. The diff keeps unix, so a typed line gets LF where :w writes CRLF.
  5. 'fileformats' with the single entry dos. Neovim then reads every file as dos, an LF file too. An LF or mixed proposal stays unix, so a typed line gets LF where :w of the file writes CRLF. Neovim reads the equal file as dos, so the equal-text view still marks lines for a text that is not all CRLF: this PR marks 2 of the 15 probe texts (a mixed text, and one with a leading lone LF), and main marks 11 of 15.

Gates

The head is 1c7b5adcfc165963ffc250ab9ebeedad00ddf954. It merges origin/main at 7dbad04b. Main moved three times while this PR was in progress, and each time only covered.lock conflicted. The gates below ran in full at 4525dad1 (the merge with origin/main at c43b6a30). The last merge brought #574. At the head I ran the checks of item 6, and CI runs the rest on this head.

  1. mise run all (BUSTED_SEED=97531) exits 0: 1837 successes, 0 failures, 0 errors, 34 pending. luacheck: 0 warnings, 0 errors in 194 files.

  2. mise run format-check exits 0.

  3. scripts/run_integration_tests_individually.sh exits 0 on Neovim 0.12.3 (Total Success 828, Failed 0, Errors 0) and on Neovim 0.8.0 (Total Success 810, Failed 0, Errors 0). The new spec alone gives 159 passes on Neovim 0.12.3, 0.11.5, 0.10.4, 0.9.5 and 0.8.0.

  4. check.sh --hash-only of the four verify-* skills exits 0. The full check.sh of verify-diff-lifecycle exits 0 (main 93477 distinct states, live-DisconnectedCallsAnswered 5557). The merge with main conflicted in covered.lock only. I took my side, ran the full check.sh on the merged tree (all 23 facts TRUE, the model passes), and then ran --record. The last merge moved only file hashes (diff.lua, init.lua, selection.lua) and no block. Against origin/main, the lock moves 3 lines: the file hash of diff.lua, and the blocks resolve_saved and setup_blocking. No guard moved. The change decides which bytes the accepted text holds. It does not change a diff's status, who gets its answer, or when.

  5. At the head, after the last merge: the full check.sh of verify-diff-lifecycle (all 23 facts TRUE, main 93477, live-DisconnectedCallsAnswered 5557) and then --record. fix(diff): keep Neovim 0.8 and 0.9 alive when a handler raises during an openDiff setup #574 changed the blocks open_blocking, handle_invoke and setup_blocking on main, and the lock of this PR moves only the 3 lines of this PR against origin/main (the file hash of diff.lua, resolve_saved, setup_blocking).

  6. At the head: format-check exits 0, check.sh --hash-only of the four skills exits 0, the new spec gives 159 passes on Neovim 0.12.3 and 0.8.0, and the 44 unit specs of the diff, tools and server modules give 752 successes, 0 failures.


Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh

… breaks

The split layouts joined the proposal buffer's lines with LF, and a CRLF
proposal kept the CR inside each line with 'fileformat' unix. A line that the
user types, or the join of two lines, came back with an LF or a stray CR in
the middle of a line, where Neovim's own :w writes CRLF. The unified layout's
buffer is read-only, so its answer is the proposal.

The spec runs each case in a real Neovim and compares the answer with the
bytes that :w writes for the same text read from a file after the same
commands. It fails on main for every typed line, join and 'fileformat' case,
and it passes for the controls that already matched.
A proposal whose every line break is CRLF now gets 'fileformat' dos and lines
without their CRs, as the same text read from a file does. The save joins the
proposal buffer's lines with the line break of its 'fileformat' (LF, CRLF for
dos, CR for mac), and ends the text with it, so the answer is what :w writes
for that buffer. Any other proposal stays unix with its CRs inside its lines,
which :w writes back unchanged.

The model has no text contents and no guard moved, so only covered.lock
records the new hashes of the two blocks that changed.
…file with the same text

The proposal buffer kept a CR inside each line, so every line of a CRLF
proposal differed from the file's own buffer ('fileformat' dos, no CRs), and the
diff marked each line as changed.
# Conflicts:
#	.agents/skills/verify-diff-lifecycle/covered.lock
…only when 'fileformats' includes it

A new scratch buffer takes the first entry of 'fileformats' as its 'fileformat'.
The diff set 'fileformat' only for a CRLF proposal, so a user whose
'fileformats' starts with dos got an LF proposal, or one that mixes CRLF and LF,
back with a CR before each LF when it accepted the text unedited. The diff now
sets the option in both cases.

A CRLF proposal also took dos when 'fileformats' was unix. The file's own buffer
then keeps its CRs as part of each line, so the diff marked every line of an
equal proposal as changed, and a typed line got a CRLF where :w writes an LF.
The diff now takes dos only for a value that includes dos.

The README line states both rules and that one empty line is saved as one line
break of the buffer's 'fileformat'. The spec runs under three values of
'fileformats' and now runs its unified cases on Neovim 0.8.0, which #564 made
work.
…m has

The diff now reads vim.o.fileformats when it builds a proposal buffer, and the
mock vim.o had no such key.
…includes dos

The spec ran 'fileformats' unix,dos, dos,unix and unix. A check that matched
those two values exactly, or that took dos for any value except unix, kept it
green. Add the single entry dos and unix,mac, with the cases that tell them
apart: the unedited text, a typed line in a CRLF proposal against :w, and an
equal CRLF text, which shows no difference.
A text with no line break at all has no CRLF line break, and the diff keeps it
unix. The README line and the comment in _setup_blocking_diff said "every line
break is CRLF", which also holds for such a text.
# Conflicts:
#	.agents/skills/verify-diff-lifecycle/covered.lock
# Conflicts:
#	.agents/skills/verify-diff-lifecycle/covered.lock
@ThomasK33

Copy link
Copy Markdown
Member Author

@codex review

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex security review

@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Nov 12, 2026 •

Copy link
Copy Markdown
Codex Review Summary: ✅ Completed

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-11-12T19:55:45.791661Z 1c7b5ad Manual request
🔒 Security Review ✅ Completed 2026-11-12T19:54:04.184277Z 1c7b5ad Manual request
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. Chef's kiss.

Reviewed commit: 4525dad172

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@chatgpt-codex-connector

Copy link
Copy Markdown

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 4525dad172

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

  • You comment "@codex security review"
  • A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

# Conflicts:
#	.agents/skills/verify-diff-lifecycle/covered.lock
@ThomasK33

Copy link
Copy Markdown
Member Author

@codex review

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex security review

@chatgpt-codex-connector

Copy link
Copy Markdown

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 1c7b5adcfc

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

  • You comment "@codex security review"
  • A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1c7b5adcfc

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread lua/claudecode/diff.lua Resolved
@ThomasK33
ThomasK33 added this pull request to the merge queue Nov 12, 2026
Merged via the queue into main with commit 80c4f84 Nov 12, 2026
8 checks passed
@ThomasK33
ThomasK33 deleted the fix/diff-crlf-new-lines branch November 12, 2026 20:34
ThomasK33 added a commit that referenced this pull request Nov 12, 2026
A clean merge of #577 (diff.lua). Every covered.lock matches the code, so no lock needs a new record.
hareki pushed a commit to hareki/claudecode.nvim that referenced this pull request Nov 14, 2026
… connection lifecycle (coder#474)

Adds `.agents/skills/verify-ws-connection`: a TLA+ model of one
WebSocket connection between Claude and the plugin, checked with TLC
against guards that `check.sh` reads from the Lua source. It is the
second `verify-*` skill on the shared harness
(`scripts/tla/check-lib.sh`, coder#450), after `verify-diff-lifecycle`.

It describes the keepalive as coder#488 merged it (d63c9b3, with the fix for
the fresh clock at the tick). On the code of coder#479 it reads STALE, and
its facts for the new design read FALSE.

## What it checks

Six rules, from the TCP accept through the handshake, requests, Close
frames, keepalive pings and server stop:

| Rule | Plain sentence |
| --- | --- |
| `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. |
| `DisconnectReportedOnce` | `on_disconnect` runs at most once per
client. |
| `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). |
| `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 reads a fresh clock, only pings and stamps
the oldest unanswered ping. The check that drops a client runs after a
poll that read the sockets, judges nothing when its poll comes more than
1.5 intervals after its tick, and any bytes read from the client clear
the stamp. A Claude that stopped once is not covered. A pong that comes
later than one interval is not covered either: when a callback blocks
inside the poll phase and refreshes the loop time, the poll can miss it,
and the check closes that client once its ping is 2.5 intervals old (the
verifier's probe on Neovim 0.12.3 dropped a peer that answered 2.4, 1.4
and 0.4 intervals late. Main does the same.) A real Claude answers a
ping at once. The rule holds for any limit above `interval * 1.5`, the
window in which a check still judges: a limit of 1.2 intervals passes
the model, and real Neovim drops a Claude that answered within 100 ms
when a read callback blocks about 1.3 intervals in the poll after the
tick. The code keeps 2.5. |
| `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`. |
| `DroppedSocketCloses` | Once a client left `server.clients`, or the
server stopped, its socket eventually closes, as long as Claude reads
again. |

`covered.lock` hashes the five files the model describes
(`server/client.lua`, `tcp.lua`, `handshake.lua`, `server/init.lua`,
`init.lua`) and the blocks inside them, so a change there reads `STALE`
until someone confirms the model still fits. The model describes the
keepalive judgement only. The stall rule of coder#467 (`judge_stall`) and the
deadline of a Close frame are not modeled, and `SKILL.md` says what a
user sees for each.

## Bugs this model found

Its first run broke three rules on the code as it was. Each one was
replayed with real sockets and fixed in coder#455. Reviews of this PR then
found four more false timeouts that the first model could not see. coder#479
and coder#488 (three rounds of it) fixed them:

- `NoFalseTimeout`: a main loop blocked during the handshake got a
Claude that answers every ping dropped with 1011 before any ping reached
it. Since coder#488 a client has no stamp until a tick pings it, so no block
can time it out.
- `DeadClientDropped`: after a protocol error while Claude's window was
full, the client stayed in `server.clients` (and `is_claude_connected()`
stayed true) until Claude read again.
- `DroppedSocketCloses`: a stop between Claude's Close frame and the
scheduled `on_close` left the plugin's socket in `CLOSE_WAIT`.
- `NoFalseTimeout`, again (coder#479): a tick that Neovim ran late after a
block of 1.0 to 1.5 intervals can run before the plugin reads Claude's
pong, and found the last pong 2.3 intervals old. libuv runs timers
before it reads sockets: with libuv 1.44, which Neovim 0.8 bundles,
after a block in any callback, and with newer libuv after a block in a
check or I/O callback, not after one in `vim.schedule` or a timer
callback.
- `NoFalseTimeout`, a third time (coder#488): libuv 1.44 runs the timers at
the end of a pass of the main loop and again at the start of the next,
with Neovim's `vim.schedule` callbacks between. Two ticks ran with no
read between them, and coder#479 dropped a Claude that answered every ping.
No counter of ticks fixes that, so a tick now only pings and a libuv
check handle, which runs after the poll, does the dropping.
- `NoFalseTimeout`, a fourth time (the review of coder#488): the check ran on
a poll that did not reach Claude's answer. A pong waits behind more
unread data than the socket holds (any bytes from the client now clear
the stamp), or the machine sleeps between a tick and its poll (the check
judges nothing after a block longer than 1.5 intervals). Each of the two
guards alone leaves one path open. The model has both, and a replay for
each.

- `NoFalseTimeout`, a fifth time (Codex's review of coder#488): the tick read
`vim.loop.now()` before it called `update_time()`. libuv runs all timers
of a pass with the loop time of the start of the pass, so after a sleep
or a block of more than 1.5 intervals in an earlier timer callback of
the same pass the tick saw no gap, kept the old stamps, and the check
dropped a Claude that had no time to answer. The tick now updates the
loop time first. There is no replay for it (a replay cannot make a timer
callback run before the ping timer inside one pass), so the unit test of
coder#488 and the model pin it: with `ClockFreshAtTick` off, `NoFalseTimeout`
breaks.

The model in this PR describes the fixed code (18 guards, all read
TRUE).

## Round 7 (the one extra review round that the maintainer allowed)

This push carries the prepared fixes for the last findings of the two
verifiers of `77bb6e2`, and merges of main. The model (`model/`) and the
`EXPECT` map are the same as in `77bb6e2`.

- The limit that the promise holds for. `NoFalseTimeout` holds for any
limit above `interval * 1.5`, not for one interval or more. A limit of
1.2 intervals passes the model, and real Neovim drops a Claude that
answered within 100 ms when a read callback blocks about 1.3 intervals
in the poll after the tick. `SKILL.md` says so now. The code keeps 2.5.
- Which test catches which clock mutation. `SKILL.md` named the wrong
test for one of them. Deleting `update_time()`, or moving it after
`local elapsed` without reading `now` again, turns red only "ages a ping
from when it was sent...". Moving it after the wake test and reading
`now` again turns red only "takes a tick for a wake...". I ran both
mutations.
- The README and the comment of `start_ping_timer` say that the first
check that finds the oldest unanswered ping `interval * 2.5` old closes
a silent Claude, and that a block inside the poll phase refreshes the
loop time.
- `check.sh`: the record pattern lists `write(client, ` and
`handle:close()`, so a change to one of those lines reads STALE. The
`DispatchGuard` fact needs the `end` of its `if` right after
`on_message`. The `StopWaitsForCloseWrite` fact rejects
`release_socket`, `abandon_close_frame` and `drop_client` in
`stop_server`. Five wording fixes in `SKILL.md`, and a note that the
`sleep` case of the bytes-only contrast on Neovim 0.8.3 depends on
timing.
- Merges of main (the last one is coder#577). The server README keeps this
PR's keepalive paragraph and takes main's new bullets. After the first
two merges three locks read STALE and are recorded again:
`verify-diff-lifecycle` and `verify-mention-queue` (the hash of
`tcp.lua`, which differs from main only in the comment of
`start_ping_timer`), and `verify-ws-connection` (`tcp.lua`, and
`M.start` and `M.stop` in `server/init.lua`, where main's coder#539 changed a
log line in `on_open` and coder#558 answers in-flight requests before
`stop_server`). The second merge made the ws lock stale once more:
main's coder#541 changed `M._broadcast_at_mention` in `init.lua`, which the
model does not cover, and the covered blocks have the same hashes. The
model still fits: those answers are ordinary writes to a connected
client, the case the model has. The last two merges (coder#544 and coder#577,
terminal and diff files only) needed no new record.

## What changed since the first version of this PR

- The model follows coder#488: the facts `DropsOnSecondOverdueTick`,
`AliveTickClearsOverdue`, `PongResetsAge`, `WakeResetsPong` and
`UpgradeStartsKeepalive` are gone. `JudgesAfterRead`,
`ClockFreshAtTick`, `StampKeepsOldestPing`, `BytesClearStamp`, `GapSkip`
and `WakeClearsStamp` replace them. The environment steps are
`StaleLoopTime`, `PollMissesPong` and `SleepInWindow`. A `stale` tick
(an earlier callback of the pass blocked or slept) is a wake that only a
tick with a fresh clock sees.
- **`NoFalseTimeout` no longer counts awake time.** The first model
added one tick of awake time on a late tick, so its own sentence ("a
block does not count as awake time") was false, and a drop at a late
tick while a pong waited unread passed. The rule now asks whether a
Claude that never stopped answering was dropped, and the ticks run at
any point between reads. A variant that judges at the tick
(`JudgesAfterRead` off) breaks it in 12 states.
- The text of `SKILL.md` is fixed: the libuv wording, the timings, the
exit codes of `--hash-only`, the numbering of the update steps, the
order of the `/statechart` steps (the kept directory is deleted after
the view is handed over), the sentence about `--mutants`
(`RejectClosesSocket` is caught only together with
`UnlistedDisconnectReleases`), and each item that is not modeled now
says what a user sees. That includes a client that sends bytes and never
reads (coder#467 handles that stall) and a client that writes data but never
answers a ping, which coder#488 keeps by design.

## What this PR changes outside the skill

- `server/README.md` and the comment of `start_ping_timer` described the
silent close and the promise wrongly. A silent Claude is closed by the
first check that finds its oldest unanswered ping `interval * 2.5` old:
90 s after the ping when ticks come on time. One late tick delays it,
because a late tick moves the ticks after it back. Two late ticks in a
row, or a poll that a block delays after a tick, bring it as early as 75
s (2.6 intervals in the probes, never earlier). A tick more than
`interval * 1.5` after the tick before it is a wake and restarts the
count, so a block of more than half an interval just before a tick is
enough, not only one of 1.5 intervals. The promise of no false close is
now for a Claude that answers each ping before the next tick, as the
model checks it, and the README says what a pong later than one interval
costs under a block in the poll phase.
- A comment in `connection_lifecycle_spec.lua` still named the pong rule
and `pong_overdue`, which coder#488 removed. It names the keepalive and the
stall rule now.
- The comment-only edits to `client.lua`, `tcp.lua` and the spec that
this PR carried for the design of coder#479 are gone, because coder#488 replaced
that code.
- `DEVELOPMENT.md`: the two paragraphs about `covered.lock` name every
`verify-*` lock, not only that of `verify-diff-lifecycle` (unchanged in
this push).

## Proof

- `check.sh` on this branch (checked on the head before the last merge):
all 18 facts TRUE and `RESULT: PASS`. `main` 262,285 states,
`live-NoFalseTimeout` 256,264, `live-DeadClientDropped` 11,701,
`live-DroppedSocketCloses` 11,701. It took 256 s and 271 s in two runs
at a host load average of 14 to 40, and 2 to 6 min in other runs. The
`check.sh` of the other four skills (`verify-diff-lifecycle`,
`verify-mention-queue`, `verify-selection-tracking`,
`verify-terminal-lifecycle`) all pass too, and all five locks match the
code (`--hash-only`).
- `check.sh --mutants` (one TLC worker): I ran it uninterrupted on the
head of this push, before the last three merges of main (they change no
covered block of this skill): 18 rows, every guard caught, exit 0, 5,753
s at a load average of 14 to 40. Both verifiers of `77bb6e2` had run it
uninterrupted too (Opus: 4761 s, gpt: 4814 s, 18 rows each). `git diff
77bb6e2 HEAD -- .agents/skills/verify-ws-connection/model` is empty and
the `EXPECT` map is the same in all three runs. The new and changed
guards are caught by `NoFalseTimeout` (`JudgesAfterRead`,
`ClockFreshAtTick`, `BytesClearStamp`, `GapSkip`, `WakeClearsStamp`) and
`DeadClientDropped` (`KeepaliveReaps`, `StampKeepsOldestPing`).
`RejectClosesSocket` alone is caught by no rule, because
`_disconnect_client` also closes the socket of a client that left the
server, so it is removed together with `UnlistedDisconnectReleases`.
- A design check outside `check.sh` for the fresh clock: with the
`ClockFreshAtTick` fact forced FALSE, `main` passes (264,485 states) and
`live-NoFalseTimeout` breaks. So the fact is needed, and the model shows
why.
- A design check outside `check.sh`: with a clear of the stamp on a PONG
only, in place of the any-bytes clear (the design before the any-bytes
rule of coder#488), `NoFalseTimeout` breaks through `PollAndCheckPartial`,
the poll that reads only the first frame. So `BytesClearStamp` is
needed, and the model shows why. The verifier's run of that variant
found 83,746 states. The count depends on how the variant is cut, so I
give no count of my own.
- Fact fidelity: both verifiers removed each guard in the Lua and every
one of the 18 facts flipped to FALSE (26 direct removals in Opus's run).
Eight mutants that no fact saw now flip one: five in `tcp.lua` (no
`table.insert(pinged, client)`, no ping sent, `judge_silence` called at
the tick, `fn` run at once in `after_next_poll`, the `end` of the gap
`if` moved above the call), and three guard moves from the last round
(the `end` of the `DispatchGuard` if above `on_message`, and
`abandon_close_frame` with `release_socket`, or `drop_client`, in the
`stop_server` loop). I reran the verifier's 42 mutations on the new
`check.sh`: none is blind.
- `scripts/tla/test-check-lib.sh`: `COUNT cases=44 failed=0 skipped=0`.
- Replays (real Neovim, real sockets), run again on the head before the
last three merges of main, on Neovim 0.12.3 and on 0.8.3:
`gap-during-handshake` 3 of 3, `short-block-after-ping` 3 of 3,
`two-blocks-before-read` 3 of 3, `blocks-before-the-poll` 3 of 3,
`protocol-close-window-full` 5 of 5, `stop-before-on-close` 4 of 4.
`protocol-close-window-full.lua` changed for the merged code: it uses an
interval of 500 ms and checks the open socket after half a keepalive
window, because the deadline of `close_client` (merged on main since the
replay was written) closes a socket whose Close frame makes no progress
for one window, so it no longer stays open for ever while Claude does
not read. The first three of the older replays keep `1 of 3`, `3 of 5`
and `2 of 4` on main before coder#455 (3d4332c). `short-block-after-ping`
keeps `2 of 3` on main before coder#479 (b65d266). `two-blocks-before-read`
keeps `1 of 3` on the code of coder#479 on Neovim 0.8.3.
`blocks-before-the-poll` keeps `0 of 3` on the first push of coder#488
(f3576ea) and with no clear of the stamp at all. With the gap skip and a
clear on a PONG only it keeps `big-message` and `sleep` and breaks
`two-blocks`. With the any-bytes clear and no gap skip it keeps
`big-message` and `two-blocks` and breaks `sleep`. All on both Neovim
versions. Both verifiers reproduced the contrast numbers of the other
replays. The `sleep` run of the bytes-only build on Neovim 0.8.3 depends
on timing: it kept all three once and two of three in five repeats. The
last two replays run Claude in a second Neovim, because an in-process
Claude answers only when the blocked loop runs again.
- The full busted suite with CI's flags (`--coverage -v --shuffle`) on
this branch: seeds 424242 and 9 on the head before the last two merges
of main, each 1858 successes, 0 failures, 34 pending. Seed 424242 on
`a929777` (merged with main at coder#544) 1887 successes, 0 failures, 34
pending. The last merge (coder#577, `diff.lua` and its spec) I did not run
again as a whole suite. `luacheck` (with `--no-unused-args
--no-max-line-length`) reports 0 warnings in 196 files. `treefmt`
(stylua, prettier, shfmt, shellcheck) reports no change on the 16 files
this PR touches. Every `covered.lock` matches the code (`--hash-only`)
on the head of this push, and the full `check.sh` of
`verify-diff-lifecycle` and `verify-terminal-lifecycle` pass on
`a929777`.

## Run it

```bash
.agents/skills/verify-ws-connection/check.sh              # 2 to 6 min
.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 --hash-only  # no TLC: compares covered.lock with the code
NVIM=/path/to/nvim .agents/skills/verify-ws-connection/replays/run.sh blocks-before-the-poll.lua
```

CI's `covered-lock` job already runs every
`.agents/skills/verify-*/check.sh`. `SKILL.md` has the rules, how to
read a result, how to update the model, and its bounds.

---
_Generated with [`xum`](https://github.com/coder/xum) • Model:
`anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant