# PR #23586 proof audit, pass 2

## 1. Integrity
- AFTER tree `/home/ubuntu/wt/pr-23586` HEAD = 9d6926bdb5c912d3efa6fef3c7c387c5c2bef795 ✔; BEFORE `/home/ubuntu/wt/pr-23586-base` HEAD = 8d3b061121fe65669d5d43d011b48cd3027a4108 ✔.
- Local `driver/late-load.evidence.test.ts` sha256 = 6d9e8a39…44a9 ✔; `driver/load-error-proxy.mjs` sha256 = 5cbfea53…0e7 ✔.
- `curl -sL` of all three uploaded URLs is byte-identical (`cmp`) to the local driver, proxy and `transcript.txt` ✔.

## 2. Driver honesty (per row)
- Shared setup is the real `AcpSessionRuntime.make` over stdio to `acp-mock-agent.ts` with `DELAY_LOAD_SESSION_AFTER_REPLAY=1`, a 1500 ms delay and a 100 ms idle gap. Outcomes come from `requestLogger` (session/load started/succeeded/failed with timestamps), `getEvents()` tags, and `getConfigOptions`/`getModeState` read after the settle time. No row asserts, so the same bytes produce both before and after. Every late row's AFTER line shows `start()` resolving with `t3SessionLoadReady: "replay_idle"` (≈650 ms) before the late `succeeded(rpc…)`/`failed` log (≈2050 ms). The late reply really does arrive after `start()` has resolved.
- Supersession and write actions run right after `start()` (`row.action`), so they land mid-flight, about 1.4 s before the late reply.
- R1: `DELAY=0` plus `EMIT_LOAD_REPLAY`. The log shows only `succeeded(rpc)` with no idle entry, so it is a real control.
- R2: SessionSetupAdopted:1 and options populated (after) vs `[]` (before). Honest.
- R4b-mode: `setMode('code')` with empty provisional state falls through to `setConfigOption("mode")`, a counted write that the mock accepts. The late reply arrives (`succeeded(rpc:…ask…)@2026`) and is not adopted, and the mode stays `code`. This row exercises the counter and configOptionsRef identity together and can't tell which guard caused the drop.
- R4b-model: the mock has no `session/set_model`, so the write **fails**. The row proves "a failed set_model write blocks adoption". It does **not** prove that a successful set_model drops the late reply (see §4).
- R5: `_test/startup-metadata` sends an uncounted agent notification. The late reply arrives @2296 and is not adopted, and model=gpt-5.4 survives. Honest for the reference-identity guard.
- R6: the second `loadSession` starts @648. The first load's late reply (it would land at ≈2046) produces no log, which means it was interrupted. The only `succeeded(rpc)`, @2154 ≈ 648+1500, belongs to the second load and is adopted once. Honest, and it also shows that a superseding load can itself adopt.
- R7/R8/R9: no late log and no adoption after resume, fork or scope close. Caveat: the absence of a log can't distinguish "fiber interrupted" from "reply never processed". Code inspection (RT `cancelLateSessionLoad`, fiber/startState/stopping checks in `adoptLateResponse`, interrupt-only means no log) backs the claimed path. Acceptable.
- R10: the proxy rewrites every *wire* session/load result. The replay-idle result is synthetic and never on the wire, and the row issues only one load (one `replayFrom` request in `proxy-trace.txt`), so only the late reply is rewritten. `failed(proxy: late session/load failure)@2074` and a working prompt afterwards confirm the path. Honest.
- R11: `sessionLoadTimeout 1s` with a 3 s delay gives `failed(session/load timed out after replay idle)` at ≈start+1 s, no adoption, and a working prompt. Honest.
- R12: reads `runtime.providerSession.capabilities.sessions.supportsModelSwitchInSession` from the adapter's session at open and after settle, and collects `provider_session.updated` events. After: `atOpen=false afterLateResponse=true`, `[true@2118]`. Before: false/false and no event. Honest. It does not test the "never revokes" direction.

No row can produce its expected AFTER line without exercising the claimed path. The weak spots are R4b-model (it tests failure, not success) and R7–R9 (inferred from a missing log).

## 3. Independent rerun (R11, AFTER tree)
I copied the driver to `apps/server/src/provider/acp/late-load.evidence.test.ts` and ran `vp test run <file> -t "R11"`: 1 passed, 11 skipped, rc 0. I deleted the copy, and `git status --porcelain` was empty. The driver overwrites `/tmp/ev-23586/rows-after.txt`, so I backed it up and restored it. The rerun output is in `audit2/rows-after.r11-rerun.txt`.

```
rerun:      start()=693 meta=replay_idle options=[] SessionSetupAdopted:0 post=prompt:end_turn log=started@564,succeeded(idle)@693,failed(session/load timed out after replay idle)@1571 crash=none
transcript: start()=630 meta=replay_idle options=[] SessionSetupAdopted:0 post=prompt:end_turn log=started@504,succeeded(idle)@630,failed(session/load timed out after replay idle)@1507 crash=none
```
The rerun matches the transcript. Only the timings differ, and both put the timeout at start+~1000 ms.

## 4. Finding (1): failed writes block adoption
**Real.** `runLoggedSessionWrite` (RT:1386-1393) runs `Ref.update(sessionWriteCountRef, +1)` *before* `runLoggedRequest`, and nothing rolls the count back on failure. `adoptLateResponse` (RT:2004) compares the count to the value captured at provisional time, so any attempted write blocks adoption, whether it succeeded, failed or timed out. R4b-model shows this: the agent rejects `session/set_model`, the late reply arrives, and the session ends with `options=[]`. That is the exact symptom the PR fixes.

**Assessment: conservative and acceptable, worth a non-blocking note to the author.** Counting before the send is deliberate, because it covers "a write whose reply is still pending" (R3, JT:1104). Counting only on success would reopen that race. A failed write with a definite JSON-RPC error left the agent's state unchanged, so adoption would be safe there. A transport failure or timeout has an unknown outcome, so blocking there is correct. In practice this window is narrow:
- During the provisional window, `setSessionModel` is reached only when `sessionSetupResult.models` is non-null, and the provisional result has none.
- The adapter's model branch needs a model option, and the provisional options are empty.
So the realistic triggers are a user action that fails during the ~1–3 s window, or a flavor `sessionModeForPolicy` write. Antigravity's `sessionModeForPolicy` → `setMode` → `setConfigOption("mode")` on empty provisional options (RT:2806-2817) is a counted write. If Antigravity loads through the replay-idle path, it would **never** adopt, and it would also be blocked if that write succeeded. That is worth one line to the author ("does Antigravity hit this?"). I verified it by inspection only.

A possible refinement if the author wants one: undo the bump when the request fails with a definite agent error (not transport/timeout). Low priority.

Finding (2), a dropped late reply still logged as `session/load succeeded`, is confirmed in R4b-mode, R4b-model and R5 (after). It is cosmetic or observability-only and doesn't affect correctness.

## 5. Row table

| Row | Sources | Status |
|---|---|---|
| R1 final before idle | PR transcript, capture R1, implicit JT:1170 | COVERED |
| R2 late adopted + SessionSetupAdopted | JT:1041, capture R2 (event counted) | COVERED |
| R3 selection sent, reply pending: dropped | JT:1104 | COVERED |
| R4 selection applied: dropped | JT:1072 | COVERED |
| R4b set_mode / set_model writes | capture R4b-mode (counted write, dropped); R4b-model shows only the failed-write case | COVERED for set_mode. The successful set_model drop is UNVERIFIED (mock has no handler). It runs through the same `runLoggedSessionWrite` counter, so it is covered by construction |
| R5 agent notification: dropped | capture R5 | COVERED |
| R6 superseded by load | capture R6 (first reply silent, second adopted once) | COVERED |
| R7 superseded by resume | capture R7 plus inspection | COVERED (absence-of-log evidence) |
| R8 superseded by fork | capture R8 plus inspection | COVERED (absence-of-log evidence) |
| R9 shutdown/close | capture R9 (no log, no event, no crash) | COVERED at the runtime level. The internal runtime-scope logs were not captured, so a spurious unhandled-error log can't be ruled out |
| R10 late error | capture R10 via proxy | COVERED |
| R11 late timeout | capture R11 plus my rerun | COVERED |
| R12 capability false→true + provider_session.updated | AT:2184, capture R12 | COVERED. The upgrade-only ("never revokes") direction is UNVERIFIED (inspection AD:6932-6953) |
| R13a one catalog publish | AT:2184 | COVERED |
| R13b thread model on next turn | AT:2261 | COVERED (pass-1 PLAUSIBLE race AD:6902 untested) |
| R13c Plan restore | AT:2357 | COVERED |
| R13d PSM getter | inspection only (PSM:1737) | UNVERIFIED. Needs a PSM harness. The getter is trivial, so I don't judge it load-bearing for proof |
| R14 adoption for other/no active session ignored | inspection only (AD:5951) | UNVERIFIED (low value, defensive guard) |

Notes for the author (non-blocking): the failed-write/Antigravity interaction (§4), and the "succeeded" log on a dropped late reply.

VERDICT: SUFFICIENT