Network channel audit

Audit #netadv1, 2026-10-05, against v0.35.456. This is phase 1 of the network-adversarial-correctness plan. The formal-model half lives in formal/tla/README.md § Network channel assumptions.

The operator requirement is that agent-doc is provably correct under varying network conditions. The design point is a Coder remote workspace (JetBrains Remote Dev backend) with Zscaler in the path, which brings high and variable latency, silent half-open stalls, and lost messages. The target property set:

• Safety holds under any delay, reorder, loss, duplication, and reconnect.
• No timeout value is part of a safety argument.
• Liveness holds when a message re-sent infinitely often is eventually delivered.

Cites are file:line relative to the repository root. rpc.rs means agent-doc-controller-io/src/project_controller/rpc.rs. JB/ means editors/jetbrains/src/main/kotlin/com/github/btakita/agentdoc/.

1. Topology: where the network actually is

Every agent-doc channel is local to the workspace host:

No audited crate uses TCP. Zscaler sits only on the JetBrains thin-client ↔ backend link, which is JetBrains’ own protocol. That has three consequences:

1. Network faults reach agent-doc as slow or wedged peers, not as lost packets. Examples are an EDT stalled behind remote-dev traffic, delayed or coalesced editor events, a controller starved by load, or a hung tmux server. In this audit a “half-open stall” means a peer that accepted a connection and stopped answering. A “lost message” means a single-attempt send whose failure or timeout is not followed by a resend or a pull.
2. “Editor visible” means the backend Document. agent-doc has no witness for what the thin client renders.
3. Remote Dev has no currentWindow or EditorWindow on the backend (JB/EditorTabSyncListener.kt:241-259, :489-490; agent-doc-editor-surface/src/remote_layout.rs:1-38). When the layout evidence is ambiguous, the surface reuses the previous layout.

Coder defect: the controller socket path is hard-wired (agent-doc-controller/src/paths.rs:15-17; JB/CpRouteClient.kt:1168; JB/CrdtReplicaForwarder.kt:1030). The editor socket honours AGENT_DOC_SOCKET_DIR (agent-doc-ipc-io/src/lib.rs:68-73); the controller socket does not. On a workspace volume that refuses AF_UNIX binds, every controller lane fails.

The adversarial-channel requirement still applies. Each of these hops behaves like a channel with unbounded delay, because peer latency is unbounded. A single-attempt send whose timeout is read as a verdict is the local equivalent of trusting a lossy network.

2. Protocol table

P7 deadline interpretation

The generic 5.0s receive deadline is expected only at a process boundary: an external caller can observe it while a live controller is scheduled late or is not servicing its socket. The associated records describe different outcomes:

• controller_state_event_deadline_retry is a first-expiry recovery record. A stable event id permits exactly one replay; only the second expiry is returned.
• controller_crdt_current_text_read_unavailable is a bounded observation miss with idle_disk_fallback; retained_write_settlement_local_fallback derives a conservative local settlement rather than losing retained intent.
• document_model_controller_lookup_error falls back to the embedded relay when present. With no embedded replica it is an unavailable-read error, not proof that a write or route failed.

Controller-owned request and effect workers are not expected to reach P7 at all. They carry controller-local identity and read the reactive projection in process. In particular, synchronous VS Code Run and the JetBrains async-command worker share that invariant. A five-second self-RPC appearing in an editor_command_async_completed failure is a context-propagation defect, not an operator route verdict; the repair is local context propagation, never blind whole-route replay after potentially ambiguous pane dispatch.

3. Serial round trips on hot paths

These are counts for one operation on the happy path. Every one of them multiplies by peer latency under load.

Response delivery (CRDT path). About 11 serial UDS round trips plus 2 EDT hops:

1. CLI → controller CP write: 1 round trip (agent-doc-crdt-relay-io/src/lib.rs:3490-3592).
2. Controller → editor deliver_crdt_remote: 2 round trips, handshake plus receipt (:5361-5378).
3. Editor → controller flushDocumentOps then replica_pull: 2 round trips (JB/CrdtReplicaForwarder.kt:871-875).
4. EDT apply.
5. replica_projection ACK: 1 round trip.
6. CLI visible-receipt long poll: at least 1 round trip (agent-doc-document-realtime-io/src/lib.rs:1229-1297).
7. CLI → editor persist_current: 2 round trips, followed by an EDT saveDocument.
8. replica_projection(disk_persisted): 1 round trip.
9. Re-observe authority: 1 round trip (document-realtime-io/lib.rs:1681-1716).

Response delivery (socket patch path). About 2 editor connects, plus the hello round trip, plus accepted/applied, plus at least 6 serial controller RPCs: registration lookups ×1-2, the visible-write status/await loop at ≥3 per iteration, and the canonical fold ≥1 (agent-doc-write-ipc-io/src/transport.rs:354-1090).

Closeout ACK. Traced in #netadv5 (finalize of a CRDT document with an attached editor, run_stream). Every non-embedded request_controller* call pays a connect_or_launch status round trip before its real request.

Floor: about 26 serial round trips after the #netadv5 trim, realistically 50 or more once the dynamic cycle-state projection reads are counted. The claim/release budget is asserted by closeout_owner_claim_and_release_stay_within_round_trip_budget through the per-thread probe controller_round_trips_on_this_thread. Each editor intent is asserted at 2 round trips (EDITOR_INTENT_SERIAL_ROUND_TRIPS, editor_intent_costs_two_serial_round_trips). The send_ndjson_request_to_actor funnel in agent-doc-state-wire is not yet counted.

Fixed sleeps on this path: native-save fallback 25→250ms backoff (agent-doc-document-realtime-io/src/lib.rs:1825, bounded by CRDT_PROJECTION_OBSERVATION_TIMEOUT_MS) and the CRDT write-frontier backoff (:3999). Both poll an observable state rather than deciding by time, but should become wake-driven.

Focus projection. 1-2 plugin round trips (focus lane plus spanning lane), then about 12-16 serial subprocesses in the controller. #netadv5 trace of the Focus intent: 1 i3-msg -t get_tree (rpc.rs:9879; the second one runs only on the fenced async-focus path) and 14 tmux subprocesses (15 with list-windows), including three separate list-panes -a and two repeated display-message #{window_id}; no pane-snapshot scope is open. Not yet asserted by a test: the handler takes a concrete tmux_router::Tmux, so the TmuxCommandRunner fakes cannot be injected. Original audit list:

• 2 × i3-msg -t get_tree (rpc.rs:9857, :24681)
• pane_alive ×2, pane_pid, pane_session, active_window, active_pane, pane_window, list-windows
• /proc ownership checks
• select-pane (rpc.rs:24424-24737)

Layout reconcile. The comments record about 109 subprocess spawns, which the cache reduces to 35 distinct tmux commands (agent-doc-sync-io/src/sync.rs:2776-2779). That is followed by a read-back survey.

Prompt injection (direct pane). About 10 or more tmux subprocesses before dispatch-start polling begins (agent-doc-route-io/src/dispatch.rs:866-1040).

4. Ranked: protocols whose safety depends on timing or reliable delivery

Ranked worst first. Severity weighs how easily load or latency triggers the fault against how irreversible the result is.

R1. A busy controller is killed by a 1s focus timeout.

• Chain:
  1. EDITOR_FOCUS_OBSERVE_TIMEOUT_MS = 1_000L (JB/CpRouteClient.kt:160).
  2. selfHealOnTimeout reads the timeout as a controller that is bound but not serving (JB/CpRouteClient.kt:1294-1335).
  3. That calls agent_doc_ensure_controller_running (src/ffi.rs:3383-3393), which runs ensure_serving_controller (rpc.rs:12906-12933).
  4. If the status RPC does not answer within CONTROLLER_RPC_TIMEOUT (5s), discover_stale_duplicate_pids(root, None) adds the bootstrap pid, which is the live controller (rpc.rs:4741-4767).
  5. reap_verified_controller_pid sends SIGTERM, waits 750ms, then SIGKILL (rpc.rs:4770-4786).
• Why it is a safety problem: two timeouts become a verdict to kill the authority mid-write, mid-closeout or mid-handoff. A wedged tmux makes this more likely, because Command::output() has no deadline (agent-doc-tmux-io/src/lib.rs:192-215). A hung tmux stalls the focus handler, which trips the 1s timeout.
• Formal coverage: no model has this edge.

R2. A slow editor attach is classified as a definitive refusal, and the replica is dropped from the delivery cut.

• Chain:
  1. deliver_crdt_remote forces a re-register, then waits CRDT_AWAIT_ATTACH_TIMEOUT_MS = 750L (JB/CrdtReplicaManager.kt:151, :1245-1250). A timeout returns false.
  2. The plugin answers APPLY_FAILED (rejected) (JB/PatchWatcher.kt:641-650).
  3. recovering_send_error_is_definitive(receipt_rejected, ..) returns true for any rejected receipt (agent-doc-crdt-relay-io/src/lib.rs:3721-3726). That gives DefinitivelyRefusedByAll (:5170-5176), then DropFromDeliveryCut (:5280-5290), then drop_definitively_refused_replica (:3788).
  4. The persist lane does the same: CRDT_AWAIT_PERSIST_CURRENT_TIMEOUT_MS 5s counts as native_save_definitive_refusals (JB/CrdtReplicaManager.kt:157; lib.rs:5093). The submitted save is not cancelled and may still land.
• Why it is a safety problem: VisibleDeliveryReceipt.tla permits the drop edge only on proof that “the endpoint answered and refused”, and in this chain a timeout manufactures that proof. A coalesced re-register within 5s also answers rejected (JB/CrdtReplicaManager.kt:180, :4644-4648).

R3. One slow connect unlinks a live editor’s socket.

• Chain: is_listener_active_for_pid runs std::fs::remove_file(&sock) on any connect error, including the 3s watchdog (agent-doc-ipc-io/src/lib.rs:314-327).
• Why it is a safety problem: the listener calls an unlinked name “dead for good” (:1354-1360). The function sits on the hot delivery path (agent-doc-write-ipc-io/src/transport.rs:518), the reposition path, the commit path, and discovery/prune. The listener-start path uses the round-trip probe_endpoint (:398-440); this one does not.

R4. Closeout owner lease: one-shot claim and a heartbeat that stops after one failure.

• Lost claim response: the claim is sent once, so if the response is lost or late after the CAS applied, the live owner pid holds a 300s lease no one uses. Every later closeout then gets HeldByOther (agent-doc-write-runtime-io/src/lib.rs:608-621; rpc.rs:68-72, :5301-5357).
• Failed refresh: one refresh that does not return Acquired, including a single RPC timeout, breaks the heartbeat loop while the foreground closeout continues (write-runtime-io/lib.rs:655-679). The lease then expires under a live owner, which permits concurrent takeover.

R5. Controller unreachable is read as “no live editor”.

• Chain: reliable_sync_editor_live_for_file returns false on a connect error but true on a timeout (rpc.rs:17111-17114 vs :17123-17132). The result feeds editor_crdt_authority_attached and the absent-editor write path (agent-doc-write-runtime-io/src/run_entry.rs:2564-2577).
• Mitigation: the local durable reliable-sync plane is checked first (rpc.rs:17100-17102), so the edge is reached only on a durable-plane miss during a controller handoff or recycle.
• Why it is a safety problem: a connection refused during handoff is evidence about the controller, not about the editor.

R6. A supervisor lease that is fresh only with traffic gates claim takeover.

• Chain: freshness requires a heartbeat within 60s (agent-doc-controller/src/status.rs:774-784; project_controller.rs:8944), but the lease is refreshed only on state transitions. A live supervisor that is idle for more than 60s reads as not fresh, so fresh_foreign_supervisor_lease_holds_document returns false (project_controller.rs:8970-8990). That permits claim’s cross-session auto-force (agent-doc-claim-io/src/lib.rs:358-388).
• Formal coverage: PaneExecutionAuthority.tla models ownership with an atomic check-and-set and a single rebind race.

R7. A contended sync runs without its lock.

• Chain: after SYNC_LOCK_WAIT_BUDGET = 3s (agent-doc-sync/src/lib.rs:32), only SafePassive aborts. Every other mode continues the stash and join-pane reconcile without exclusion (agent-doc-sync-io/src/sync.rs:2748-2773).
• Why it is a safety problem: mutual exclusion lasts only until a timer fires.

R8. Prompt injection can deliver twice.

• Stranded-draft path: a bare Enter, then a 3s admission wait (agent-doc-controller/src/dispatch.rs:3227-3233). If it times out, Ok(None) falls through to the normal path, which sends the full trigger again (agent-doc-route-io/src/dispatch.rs:829-861, :887-915).
• Supervisor inject: a 10s effect timeout (agent-doc-supervisor-io/src/ipc.rs:58) reports failure after delivery. The dedupe key is in memory and is lost on supervisor re-exec (agent-doc-start-runtime-io/src/lib.rs:2469-2503).
• Pass-through: Cleared vs re-Enter is decided by a 150ms settle (dispatch.rs:2937).
• Why it is a safety problem: receivers have no idempotency key. Duplicate protection is screen observation within a time window.

R9. Supervisor restart timeout escalates to a cold start, and the recycle TTL is treated as proof of loss.

• Restart: a response timeout leads to a probe of a live socket and a Failed result, which decide_supervisor_replacement_escalation maps to EscalateColdStart (rpc.rs:27193-27245; agent-doc-controller/src/supervisor_replacement.rs:190-193). This contradicts “mutating commands must never be replayed merely because that receipt was late” (agent-doc-supervisor-io/src/ipc.rs:63-69) and risks a duplicate supervisor.
• Recycle TTL: RECYCLE_INFLIGHT_SETTLE_TTL_SECS=120 (agent-doc-controller/src/dispatch.rs:2222) is treated as proof the settle was lost. RecycleSettleDispatch.tla:114-119 encodes exactly that.

R10. Response delivery wake is one-shot, with no periodic pull.

• Liveness: a failed deliver_crdt_remote is only logged (agent-doc-crdt-relay-io/src/lib.rs:3563-3575, :5418-5428). The CLI wait’s signal_immediately is a no-op (agent-doc-document-realtime-io/src/lib.rs:661). JetBrains pulls only on events, and an idle no-op drain does not reschedule (JB/CrdtReplicaManager.kt:1720-1730).
• Recovery is latched once: the non-convergence recovery is latched on the first send (agent-doc-document-realtime/src/crdt_relay.rs:2471-2484). NonconvergingReplicaDisposition::Retry, which is what a send timeout yields, is never acted on outside tests (agent-doc-crdt-relay-io/src/lib.rs:3761-3766, :5290).
• Result: the response stays invisible until the operator interacts. Safety holds (it fails closed); liveness does not.

R11. GH #136: layout admission depends on which lane published last.

• Retained columns: focus escalation republishes whichever lane last published the “retained” columns (rpc.rs:21312-21328, :21376-21436). The focus and spanning lanes have no fence between them.
• Fail-open gate: the column gate admits the stale focused pane by design (agent-doc-sync-io/src/layout_column_audit.rs:353-354). It also admits Unknown freshness, and freshness reads Unknown during a supervisor re-exec window (:151-156, :172-192, :554-557).
• No restart reload: the desired layout is not reloaded from state.db when the controller restarts.

R12. Missing deadlines that turn a wedged peer into an unbounded stall. These are liveness problems, but R1 turns them into safety problems.

• JB/CrdtReplicaForwarder.kt:1032-1048: no read deadline. A wedged controller hangs the per-document worker that serialises pull, ACK, register and save (JB/CrdtReplicaManager.kt:4232).
• Controller and supervisor connect and write have no deadline (rpc.rs:588-600, :650-652, :15340-15342; agent-doc-supervisor-io/src/ipc.rs:873-880, :969-972).
• tmux subprocesses have no deadline (agent-doc-tmux-io/src/lib.rs:192-215).

For contrast: P5 (reliable-sync op push) and P8 (visible-write receipt) already satisfy the target shape. Both re-derive from durable state, apply idempotently by cursor or hash, and fail closed on timeout. They are the template for the fixes below.

5. Candidate fixes: one-shot notifications on correctness paths

This table is the original #netadv1 finding set. Each item names the missing property at audit time; the #netadv3 closure below records the fixes proved by the subsequent NetChannel models and deterministic regressions.

#netadv3 closure

• F4/F5: closeout claims reuse a caller-stable owner id and retry a lost claim; heartbeat transport loss retries, while an answered lease loss aborts before commit (AgentDocCloseoutNet plus deterministic write-runtime regressions).
• F9/F10/F13: delivery wake, recovery and retained-save paths are level-triggered and re-arm after lost/refused receipts (VisibleDeliveryReceiptNet).
• F14/F15: a failed editor-surface focus or structural publication retains the exact SurfaceIntent; the next matching observation reapplies it, and only a successful effect, an answered refusal, a document move or client retirement clears it (PassiveTmuxSyncNetAdvanceFirstWedge).
• SIM-F1/SIM-F2: lifecycle, heartbeat and queue-control level updates carry a monotonic send stamp. Reordered older updates in the same generation are rejected by the real handlers and by deterministic SimWorld traces (LifecycleSequenceReorderWedge).

6. Formal-model gap summary

The full table is in formal/tla/README.md. The original #netadv1 gap was closed for the selected hot paths by #netadv3: requests and receipts are split over NetChannel, safety runs under the full adversary, and liveness runs under fair loss with protocol resend fairness. Remaining gaps stay explicit in each model rather than being hidden behind an atomic receipt.

• Lossy channels: the *Net hot-path models now cover loss, delay, duplication, reordering, stalls and reconnect cuts.
• Believed refusals: VisibleDeliveryReceipt, EditorReplicaStrand and TransientRefusalLatch believe every refusal. Neither R2 (timeout read as refusal) nor R3 (connect failure read as stale socket) can be expressed.
• Timer-derived facts: RecycleSettleDispatch and WaitMachine encode a timer firing as a fact (Ttl, globalHangCeiling). That conflicts with the target property.
• First remodel targets for netadv3:
  • VisibleDeliveryReceipt: R2, R10.
  • EditorReplicaStrand: R2, R3.
  • A new controller-liveness/self-heal model: R1.
  • Closeout lease: R4.
  • RecycleSettleDispatch and the supervisor restart: R9.
  • GH #136 layout admission: R11.

Appendix: correctness-path timing constants

Values below 1s are localhost-tuned.