🤖 fix: a held Retry never appends an accepted input twice (send ids, PR1a) (#5537)

## Summary

A held Retry never appends an already-accepted input twice (H1). Every
manual send now carries a stable send id: the client's `sendId`, or one
the backend mints for clients that send none. The user row that accepts
a send records its ids (`metadata.sendIds`), and the history write path
refuses a second row for a known id. The check reads history under the
cross-process history write lock, right before the append.

This supersedes the acceptance half of #5518. #5518 stays open and
blocked, with its review history. The status lookup, the incremental
index and the refusal bookkeeping move to a follow-up (PR1b).

## Background

H1: a send's user row becomes durable, then the send still fails (for
example its stream start fails). The input stays held. Retry sends it
again, and the transcript gets a second copy.
`workspaceService.sendIds.test.ts` reproduces it end to end with the
real WorkspaceService, AgentSession, MessageQueue and HistoryService
(only the AI stream is mocked).

#5518 fixed H1 but also shipped a status RPC, an incremental send-id
index, pending and refused-id bookkeeping, and a partial-batch rebuild.
Its six Codex rounds (2, 2, 2, 4, 2, 2 findings, plus one after the cap)
kept landing in that extra machinery. This PR keeps only the acceptance
contract.

## Implementation

1. **Ids.** `WorkspaceService.sendMessage` assigns ids to manual sends
(not automatic, synthetic or agent-initiated ones). A minted id uses the
reserved `srv-` prefix. `SendIdSchema` refuses client ids with that
prefix. Queue entries, held inputs and re-sends carry every id.
2. **Acceptance check.** `HistoryService.acceptCompactionReplacement`
(the manual-origin publication) reads the archive and the live file
under its write lock (`sendIds.ts`). Only a readable row with the same
payload digest proves an id accepted.
- Every id accepted: no row, and the send succeeds without streaming. A
held Retry drops its entry.
- Some ids accepted, a different payload, the same id twice, or a line
that names the id but proves nothing (unparseable, not a readable
message, no digest, over 64 MiB): no row, Err. The input keeps every id.
A queued batch is held whole.
- No id known: append, and stamp `sendIds` and `sendDigests` on the row.
3. **No partial batch rebuild.** A queued batch publishes as one row, so
its ids are accepted together or not at all. A held re-send is queued
sealed (never batched). A client id already queued with the same payload
is not queued again. Any other overlap is queued on its own. A batch
that is only partly on rows can then arise only from a client reusing
its own ids across backends, and it is refused whole.
4. **Cost.** One full read takes 30 ms (20 MB), 90 ms (60 MB) and 190 ms
(210 MB) at 50,000 rows on a loaded 32-core host, with no lasting memory
growth. Under the write lock that is too much for every send. A minted
id that was never offered to a publication cannot be on disk, so its
first publication skips the read (`unpublished`). Held input drops that
flag. Client ids and re-sends always read. Nothing is cached: a negative
answer is used only for the append that follows it under the same lock.
5. **Advisory lookup.** `sendHeldInput` asks
`HistoryService.decideSendIds` before re-sending, so the common H1 case
ends before any preparation work. The in-lock check stays the authority
(tested with a stale negative lookup).
6. **Rejected-send rows.** The pricing and token-budget rejection paths
record the rejected input under the same check and surface its decision
(a conflict is no longer reported as a generic context-mutation error).
7. **Digest.** The text, attachments, edit target and client metadata.
It excludes model and agent settings, the ACP correlation mirror and
`muxMetadata.requestedModel`, which a retry may change.

## #5518 findings, by area

(a) acceptance, batching and duplicate checks. (b) index, status lookups
and refused-id bookkeeping.

| Round | Finding | Area | Here |
| --- | --- | --- | --- |
| 1 | pending retries with a changed digest | (b) | moved to PR1b
(pending bookkeeping) |
| 1 | prototype-free status record | (b) | moved to PR1b (status RPC);
digests are read with `Object.hasOwn` |
| 2 | batch with unverified or conflicting ids was filtered | (a) |
refused whole, tested |
| 2 | partial rebuild kept prefix rows | (a) | no rebuild |
| 3 | `__proto__` dropped by output validation | (b) | moved to PR1b (no
status RPC) |
| 3 | ACP mirror in the digest | (a) | excluded, tested |
| 4 | requested-model mirror in the digest | (a) | excluded, tested |
| 4 | rebuild kept the /compact metadata | (a) | no rebuild; refused
whole, tested |
| 4 | unreadable rows reported accepted | (b) | the append check treats
them as unverified, tested |
| 4 | Formal workflow path gate | (b) | gate lists `sendIds.ts` |
| 5 | rejected-send persistence dropped the in-lock decision | (a) |
decision surfaced |
| 5 | oversized torn line in the index | (b) | no index; one bounded
line at a time, tested |
| 6 | torn tail buffered past the cap | (b) | no index; bounded by
construction |
| 6 | digestless row reported accepted | (b) | unverified for the append
check, tested |
| after cap | malformed lines retained | (b) | nothing retained after a
read |

## Moved to PR1b

- `getSendStatus` RPC and its pending, in-flight and refused-id
bookkeeping (receiver refusal memory).
- The incremental send-id index, only if the renderer starts sending ids
on every send (then every send would pay the read above).

## Validation

- `historyService.sendIds.test.ts`: two HistoryService instances on one
session dir, conflict, unverified lines, a row larger than the
session_history line limit, ids in text or client metadata, partial and
repeated ids, prototype-named ids, archive rotation, clearing.
- `workspaceService.sendIds.test.ts`: H1 (ID-less client), H1 with a
stale negative lookup, client retry and conflict, a queued batch partly
accepted by another backend (held whole; its Retry is refused, nothing
duplicated), a /compact batch, repeated client ids while queued, a
sealed held re-send.
- `sendIds.test.ts`: chunk-boundary lines, an over-long line searched
across chunks, torn last lines, digest exclusions.
- Mutation checks: disabling the in-lock check, the sealing of held
re-sends, the overlap sealing, the queue no-op, the partial refusal, the
search overlap, or the held-flag stripping each fails at least one test.
- Formal: `formal/composer-drafts/check.sh` passes for every config.
`MCS_pr1a` (one backend, post-append Errs, restarts): `NoHeldDup` holds
(H1 fixed), 15,894 states. `MCS_pr1a_clients` (two backends, a client
re-sending its own ids): `NoSilentLoss` and `NoHeldDup` hold over 16.5M
states, and the witness `PartialBatchUnreached` is violated (a partly
accepted batch is reachable and refused whole). `MCS_pr1a_mut_nodedupe`
(no in-lock check) violates `NoHeldDup`. The model's `Dispatch` now
refuses a partly known batch under `NarrowBackend` instead of filtering
it.

## Risks

- Medium, in the send path: every manual publication passes the new
check. Fresh minted ids skip the history read, so ordinary sends pay
nothing extra. A held Retry or a client-id send reads the whole history
once under the write lock.
- A batch refused as partly accepted stays held and cannot be re-sent as
is (Discard only). Today's renderer sends no ids, so only a client that
reuses its own ids across backends can reach it.
- Today's renderer still clears the draft before acceptance and restores
it on a failed reply, so D2, D4 and D5 remain (the renderer PR).

---

_Generated with [`xum`](https://github.com/coder/xum) • Model:
`anthropic:claude-opus-5-5` • Thinking: `high` • Cost: `$44.26`_

<!-- mux-attribution: model=anthropic:claude-opus-5-5 thinking=high
costs=44.26 -->

Author: ThomasK33

.github/workflows/formal.yml

@@ -52,6 +52,7 @@ on:
       - "src/node/services/initStateManager.ts"
       - "src/node/services/messageQueue.ts"
       - "src/node/services/retryManager.ts"
+      - "src/node/services/sendIds.ts"
       - "src/node/services/streamManager.ts"
       - "src/node/services/taskHandleStore.ts"
       - "src/node/services/taskService.ts"
@@ -137,6 +138,9 @@ jobs:
               - 'src/browser/utils/chatCommands.ts'
               - 'src/node/services/agentSession.ts'
               - 'src/node/services/draftService.ts'
+              - 'src/node/services/historyService.ts'
+              - 'src/node/services/messageQueue.ts'
+              - 'src/node/services/sendIds.ts'
               - 'src/node/services/workspaceService.ts'
             delegated-turns:
               - 'formal/delegated-turns/**'

formal/composer-drafts/ComposerSends.tla

@@ -0,0 +1,25 @@
+\* Sends today (no ids): lost reply, rollback, refusal after a durable row, queue and held Retry, restart.
+SPECIFICATION Spec
+CONSTANTS
+  Items = {"i1"}
+  AttachOnly = {}
+  TwoBackends = FALSE
+  TwoWindows = FALSE
+  WithQueue = TRUE
+  WithRollback = TRUE
+  WithRestart = TRUE
+  WithOtherWriter = FALSE
+  WithDowngrade = FALSE
+  FixIds = FALSE
+  FixRenderer = FALSE
+  NarrowBackend = FALSE
+  ClientIds = FALSE
+  MutRollbackAfterAppend = FALSE
+  MutNoRefusalMemory = FALSE
+  MutDeadIsAccepted = FALSE
+  MutNoDedupe = FALSE
+  MutBookOnly = FALSE
+  MutEmptyRule = FALSE
+  MutConflictAccept = FALSE
+  DowngradeSettledOnly = FALSE
+INVARIANTS TypeOK NoSilentLoss NoDup NoResurrection

formal/composer-drafts/MCS_current.cfg

@@ -0,0 +1,25 @@
+\* An attachment-only input next to a text input, with queue and restart.
+SPECIFICATION Spec
+CONSTANTS
+  Items = {"a1", "i1"}
+  AttachOnly = {"a1"}
+  TwoBackends = FALSE
+  TwoWindows = FALSE
+  WithQueue = TRUE
+  WithRollback = FALSE
+  WithRestart = TRUE
+  WithOtherWriter = FALSE
+  WithDowngrade = FALSE
+  FixIds = TRUE
+  FixRenderer = TRUE
+  NarrowBackend = FALSE
+  ClientIds = FALSE
+  MutRollbackAfterAppend = FALSE
+  MutNoRefusalMemory = FALSE
+  MutDeadIsAccepted = FALSE
+  MutNoDedupe = FALSE
+  MutBookOnly = FALSE
+  MutEmptyRule = FALSE
+  MutConflictAccept = FALSE
+  DowngradeSettledOnly = FALSE
+INVARIANTS TypeOK NoSilentLoss NoDup NoResurrection

formal/composer-drafts/MCS_fix_attach.cfg

@@ -0,0 +1,25 @@
+\* Lookup vs late arrival, repeated ids, a receiver restart, two backends and two windows.
+SPECIFICATION Spec
+CONSTANTS
+  Items = {"i1"}
+  AttachOnly = {}
+  TwoBackends = TRUE
+  TwoWindows = TRUE
+  WithQueue = FALSE
+  WithRollback = FALSE
+  WithRestart = TRUE
+  WithOtherWriter = FALSE
+  WithDowngrade = FALSE
+  FixIds = TRUE
+  FixRenderer = TRUE
+  NarrowBackend = FALSE
+  ClientIds = FALSE
+  MutRollbackAfterAppend = FALSE
+  MutNoRefusalMemory = FALSE
+  MutDeadIsAccepted = FALSE
+  MutNoDedupe = FALSE
+  MutBookOnly = FALSE
+  MutEmptyRule = FALSE
+  MutConflictAccept = FALSE
+  DowngradeSettledOnly = FALSE
+INVARIANTS TypeOK NoSilentLoss NoDup NoResurrection

formal/composer-drafts/MCS_fix_core.cfg

@@ -0,0 +1,25 @@
+\* The stated limit: downgrade right after an acceptance that was not yet reconciled.
+SPECIFICATION Spec
+CONSTANTS
+  Items = {"i1"}
+  AttachOnly = {}
+  TwoBackends = FALSE
+  TwoWindows = FALSE
+  WithQueue = FALSE
+  WithRollback = FALSE
+  WithRestart = TRUE
+  WithOtherWriter = FALSE
+  WithDowngrade = TRUE
+  FixIds = TRUE
+  FixRenderer = TRUE
+  NarrowBackend = FALSE
+  ClientIds = FALSE
+  MutRollbackAfterAppend = FALSE
+  MutNoRefusalMemory = FALSE
+  MutDeadIsAccepted = FALSE
+  MutNoDedupe = FALSE
+  MutBookOnly = FALSE
+  MutEmptyRule = FALSE
+  MutConflictAccept = FALSE
+  DowngradeSettledOnly = FALSE
+INVARIANTS TypeOK NoSilentLoss NoDup NoResurrection

formal/composer-drafts/MCS_fix_downgrade.cfg

@@ -0,0 +1,25 @@
+\* Downgrade, a write by the older build, upgrade, retry; downgrade only with no accepted entry awaiting removal.
+SPECIFICATION Spec
+CONSTANTS
+  Items = {"i1"}
+  AttachOnly = {}
+  TwoBackends = FALSE
+  TwoWindows = FALSE
+  WithQueue = FALSE
+  WithRollback = FALSE
+  WithRestart = TRUE
+  WithOtherWriter = FALSE
+  WithDowngrade = TRUE
+  FixIds = TRUE
+  FixRenderer = TRUE
+  NarrowBackend = FALSE
+  ClientIds = FALSE
+  MutRollbackAfterAppend = FALSE
+  MutNoRefusalMemory = FALSE
+  MutDeadIsAccepted = FALSE
+  MutNoDedupe = FALSE
+  MutBookOnly = FALSE
+  MutEmptyRule = FALSE
+  MutConflictAccept = FALSE
+  DowngradeSettledOnly = TRUE
+INVARIANTS TypeOK NoSilentLoss NoDup NoResurrection

formal/composer-drafts/MCS_fix_downgrade_settled.cfg

@@ -0,0 +1,25 @@
+\* A writer that does not know pendingSends edits the draft (digest mismatch).
+SPECIFICATION Spec
+CONSTANTS
+  Items = {"i1"}
+  AttachOnly = {}
+  TwoBackends = FALSE
+  TwoWindows = FALSE
+  WithQueue = FALSE
+  WithRollback = FALSE
+  WithRestart = TRUE
+  WithOtherWriter = TRUE
+  WithDowngrade = FALSE
+  FixIds = TRUE
+  FixRenderer = TRUE
+  NarrowBackend = FALSE
+  ClientIds = FALSE
+  MutRollbackAfterAppend = FALSE
+  MutNoRefusalMemory = FALSE
+  MutDeadIsAccepted = FALSE
+  MutNoDedupe = FALSE
+  MutBookOnly = FALSE
+  MutEmptyRule = FALSE
+  MutConflictAccept = FALSE
+  DowngradeSettledOnly = FALSE
+INVARIANTS TypeOK NoSilentLoss NoDup NoResurrection

formal/composer-drafts/MCS_fix_otherwriter.cfg

@@ -0,0 +1,25 @@
+\* Queue batches with repeated ids, dequeue refusal and held Retry, conflicting payloads, restart.
+SPECIFICATION Spec
+CONSTANTS
+  Items = {"i1", "i2"}
+  AttachOnly = {}
+  TwoBackends = FALSE
+  TwoWindows = FALSE
+  WithQueue = TRUE
+  WithRollback = FALSE
+  WithRestart = TRUE
+  WithOtherWriter = FALSE
+  WithDowngrade = FALSE
+  FixIds = TRUE
+  FixRenderer = TRUE
+  NarrowBackend = FALSE
+  ClientIds = FALSE
+  MutRollbackAfterAppend = FALSE
+  MutNoRefusalMemory = FALSE
+  MutDeadIsAccepted = FALSE
+  MutNoDedupe = FALSE
+  MutBookOnly = FALSE
+  MutEmptyRule = FALSE
+  MutConflictAccept = FALSE
+  DowngradeSettledOnly = FALSE
+INVARIANTS TypeOK NoSilentLoss NoDup NoResurrection

formal/composer-drafts/MCS_fix_queue.cfg

@@ -0,0 +1,25 @@
+\* Mutant: pending content only in pendingSends; an older build drops it.
+SPECIFICATION Spec
+CONSTANTS
+  Items = {"i1"}
+  AttachOnly = {}
+  TwoBackends = FALSE
+  TwoWindows = FALSE
+  WithQueue = FALSE
+  WithRollback = FALSE
+  WithRestart = FALSE
+  WithOtherWriter = FALSE
+  WithDowngrade = TRUE
+  FixIds = TRUE
+  FixRenderer = TRUE
+  NarrowBackend = FALSE
+  ClientIds = FALSE
+  MutRollbackAfterAppend = FALSE
+  MutNoRefusalMemory = FALSE
+  MutDeadIsAccepted = FALSE
+  MutNoDedupe = FALSE
+  MutBookOnly = TRUE
+  MutEmptyRule = FALSE
+  MutConflictAccept = FALSE
+  DowngradeSettledOnly = FALSE
+INVARIANTS TypeOK NoSilentLoss NoDup NoResurrection