# PR #23671 proof audit, pass 2

Head d0186cbb21 (`/home/ubuntu/wt/pr-23671`), merge-base 60b35a1ee0 (`/home/ubuntu/wt/pr-23671-before`), red a8cd776ee5. All paths below are under `apps/server/src/`. PTS is `orchestration-v2/ProviderTurnStartService.test.ts`, CRS is `orchestration-v2/CheckpointRollbackService.test.ts`, DRV is the evidence driver `/tmp/ev-23671/evidence/driver/RestoreRace.driver.test.ts`, and HLP is `helper-rows-after.txt`. Both worktrees showed empty `git status --porcelain` after every run.

## Reruns done in this pass (outputs in /tmp/ev-23671/audit2/)

| File | What | Result |
|---|---|---|
| `rerun-after.txt` | `run-part1.sh` at head, same driver sha256 da3cd6b2… | Matches the captured `transcript-after.txt` exactly. Cases a, b, c have PROBE "NOT opened", then "files restored", then "session opened". Controls d and e open during the park |
| `three-files-head.txt` | The three files named in the PR body, at head | `Test Files 3 passed (3)`, `Tests 52 passed (52)`. The 52 count is confirmed |
| `red-rerun-a8cd776ee5.txt` | The PTS blob from a8cd776ee5 (that commit touches only this file) on merge-base sources, `-t "restore finishes"` | `Tests 3 failed \| 32 skipped (35)`, the same assertion the PR body quotes. The red claim is confirmed |
| `mutation-plain-lease.txt` | Merge-base worktree plus the head versions of the 5 PR files, with `CheckpointRollbackService.ts:374` changed from `withCheckpointRestoreReservation(…, rollback)` to `rollback`, so only the plain lease remains | CRS `restoreFiles true` fails with `expected [ 'turn start' ] to deeply equal []`. `false` passes. The PR claim is confirmed |
| `mutation-double-lease-INVALID.txt` | My first mutation attempt wrapped `rollback` in a second `withWorkspaceLease` on the same path | It deadlocked on the non-reentrant lease and hit the 120 s timeout. **This run is invalid as evidence.** It is kept only for the record, and incidentally confirms the PR's reason for keeping the reservation separate from the lease |
| `row5-red-8e4748be4d.txt` | Head versions of the PR files, with `workspace/workspaceLease.ts` from 8e4748be4d (before `canonicalize` existed) | Only the "not-yet-recreated worktree under a symlink alias" row fails (`1 failed \| 3 passed`). Row 5 is now red/green |

## Driver soundness (task 1)

- **Real services: yes.** DRV:940 builds `CheckpointRollbackService.layer` with the same stack as CRS:395. DRV:1011–1020 calls the public `execute`. The turn side calls `ProviderTurnStart.layer` through `makeLocalCommandHarness`, copied from the merge-base test (DRV:260, :686, :766). The driver imports no workspaceLease reservation helpers. The base portion imports only `withWorkspaceLease`, which exists at both SHAs. Mocked pieces: `ProviderSessionManagerV2.open` parks on a Deferred (DRV:972). `CheckpointServiceV2.restore` runs a real `git checkout -- file.txt` in a real temp repo (DRV:951). Symlinks and dirs are real.
- **Probe: sound.** At merge-base, cases a–d open within the 64 yields. That shows 64 yields are enough for an unblocked start to reach the provider when FS calls are sync. At head, the blocked cases park on `Deferred.await(reservationReleased)`, which cannot resolve without a release, so "NOT opened" is not a timing artifact. Control d (sibling `<wt>-other`) still opens within 64 yields at head, so the probe is not trivially negative.
- **Caveats:**
  - (1) `exists`/`realPath` on the turn side are sync `node:fs` (DRV:803). The real NodeServices FS is async and could only widen the window, so the wait is still deterministic.
  - (2) The rollback's `getShellSnapshot` returns `threads: []` (DRV:964). The isolation check therefore never sees the turn thread, which models a thread or worktree that appears after the check. That is the race window the PR describes.
  - (3) The driver parks only at provider open. The file-restore phase is parked separately by CRS:409/:456–464, not by the driver.
  - (4) The test asserts only `openedAt > -1` (DRV:1050). Ordering is reported in a RESULT line, not asserted, so the driver always "passes". Read the RESULT lines, not the pass count.
- **Red vs green test body.** The a8cd776ee5 test holds the restore with `withWorkspaceLease`, standing in for main's `execute`. The head test swaps that for `withCheckpointRestoreReservation` (PTS:1033). The two commits run two versions of the same test, not one identical test going red then green. DRV closes this gap: the same driver calls the real `execute` at both SHAs.

## Row-by-row (task 1)

| # | Row | Coverage now | SHAs | Status |
|---|---|---|---|---|
| 1 | Same dir | PTS:970 (project-root thread, restore of the same project checkout) | Red a8cd776ee5 (rerun), green head | OK. A same-dir *worktree* pair was already serialized on main by the literal lease, so it is not a differentiator |
| 2 | Symlink alias | PTS:977 (fake realPath); DRV case a (real symlink) | PTS red a8cd776ee5 / green head; DRV before :14–19 opened first, after :19–25 restored first, rerun matches | OK |
| 3a | Child dir | PTS:984; CRS:350 true; DRV case b | Red a8cd776ee5 and DRV before; green head | OK |
| 3b | Parent dir (turn cwd is an ancestor of the restore) | DRV case c: project-root thread whose workspaceRoot `<root>/project` is a parent of the restoring worktree | DRV before: did not wait; after and rerun: waited | OK (driver only, no PR test) |
| 4 | Project-root thread vs a restore of the project checkout | PTS:970; DRV case c | Red/green | OK |
| 5 | Missing worktree under a symlinked ancestor | PTS:991 | Green head; **red at 8e4748be4d (this pass, `row5-red-8e4748be4d.txt`)**. Can't run at merge-base because the test uses the new helper. Main fails the simpler alias row anyway | OK |
| 6 | Non-overlapping workspaces never wait | DRV case d (`<wt>` vs `<wt>-other`, the prefix trap); HLP row 1 (`b` vs `bc`, `c`) | DRV at both SHAs; HLP head | OK (no-regression) |
| 7 | Turn starts never wait on each other | HLP row 2 (same dir and nested); pre-existing PTS "starts another provider in the same checkout…" passes in the 52 | Head | OK |
| 8 | restoreFiles:false takes no reservation | CRS:466–469 false; DRV case e | CRS head; DRV both SHAs | OK |
| 9 | Project-root rollback takes no reservation | No test. **Verified by inspection.** `CheckpointRollbackService.ts:366` returns early. `CheckpointRestoreSafety.ts:34` (`shared = worktreePath == null`) makes `CheckpointRollbackService.ts:224–232` reject any file restore before `checkpoints.restore` at :279. A project-root rollback can only be conversation-only, which writes no files | n/a | OK by inspection; same code path as main |
| 10 | Project with no workspaceRoot → no reservation | No test. **Verified by inspection.** `ProviderTurnStartService.ts:1346–1352`: `cwd === undefined` runs `start(input)` bare, the same as main's project-root path. No restore can target a path that doesn't exist | n/a | OK by inspection |
| 11 | Restore failure releases | HLP rows 3 (fail) and 5 (die); `Effect.ensuring(release)` at `workspace/workspaceLease.ts` withReservation | Head | OK |
| 12 | Restore interrupt releases | HLP row 4 | Head | OK |
| 13 | Interrupted waiting turn start leaves nothing held | HLP row 6 | Head | OK |
| 14 | Overlapping restores serialize | HLP row 7 | Head | OK |
| 15 | Held turn start blocks a restore | HLP row 8 | Head | OK |
| 16 | Restore starvation behind a stream of turn starts | No test. **Design note**: `reserve` checks held reservations only (`workspaceLease.ts` reserve loop), so a restore can be overtaken by each new overlapping turn start. Turn-start reservations cover startup only, not the provider turn (`ProviderTurnStartService.ts:1343–1345` comment and the code), so each window is short | n/a | Not a claim of the PR; mention to the maintainer |
| 17 | File-restore phase covered, not just the provider rollback | CRS:456–464: a second turn start forked while parked in `restore` stays out of `calls`. The mutation run shows it fails without the reservation | Head; mutation red | OK. The capture agent's "file-restore phase not separately parked" applies only to DRV |
| 18 | Real execute + real start end to end | DRV a–e | Both SHAs plus my head rerun | OK (service layer, not a running server, labelled correctly) |

## PR-body claims (task 3)

**Change**
- *The reservation is in-memory and separate from `withWorkspaceLease`, and the lease is unchanged.* The diff touches only additions in `workspace/workspaceLease.ts`. **Accurate.**
- *Canonicalizes with realPath, walking up for a missing worktree.* `canonicalize` in workspaceLease.ts; PTS:991; row5 red/green. **Accurate.**
- *Conflict when the directories overlap and at least one is a restore; turn starts never wait on each other; non-overlapping dirs never wait.* HLP rows 1, 2, 7, 8; DRV d. **Accurate.**
- *The lease is non-reentrant and restores take a Git lease on the project root.* Non-reentrancy was shown incidentally by my invalid double-lease run, which deadlocked. I did not check the Git-lease half. It is rationale, not a behaviour claim.
- *Rollback reservation is outermost and covers the isolation check, the provider rollback and the file restore.* `CheckpointRollbackService.ts:369–374`: the reservation wraps the lease, which wraps `execute`. The provider-rollback phase is shown by CRS and DRV, and the file-restore phase by CRS:456–464. The isolation check sits inside `execute` (verified by inspection). **Accurate.**
- *Conversation-only and project-root rollbacks don't take it; the isolation check rejects project-root file restores.* CRS false and DRV e; inspection for row 9 (`CheckpointRestoreSafety.ts:34`). **Accurate.**
- *Turn start reserves the worktree or workspaceRoot around startup.* `ProviderTurnStartService.ts:1346–1361`; DRV c (workspaceRoot) and a/b (worktree). **Accurate.**
- *"Once it has started, the restore's isolation check sees it."* Not tested by the PR. By inspection, `CheckpointRestoreSafety.ts:51–87` rejects when any non-deleted thread overlaps, or when a live session's cwd overlaps. The thread's existence or projection is what matters, not "started", so the wording is slightly loose. Minor.
- *"No SQLite transaction or global lock is held across provider or Git work."* By inspection, workspaceLease.ts uses only a module `Set` and a `Deferred`, with no SQLite. The reservation *is* deliberately held across the provider rollback and the Git restore, but it is per-overlap, not global: DRV d and HLP row 1 show unrelated dirs proceed. The one shared `reservationReleased` Deferred is a wake-all signal (re-check on any release), not a lock. **Accurate.**

**Verification**
- *Red at a8cd776ee5, 3 failed \| 32 skipped (35).* Reproduced exactly. One wording nit: the red and green commits run two versions of the test body (see "Red vs green test body" above), not one unchanged test.
- *Green, 3 files, 52/52, including a fourth overlap case.* Reproduced. The fourth case is now also shown red at 8e4748be4d. Typo in the body: "parent.." has a double period.
- *CRS test pauses at provider open and inside the file restore; true parks, false is not blocked.* CRS:350–475, green at head. **Accurate.**
- *"Replacing the rollback's reservation with the plain lease makes the true case fail."* Reproduced in `mutation-plain-lease.txt`. That means removing the reservation, which leaves the existing plain lease. Literally *adding* a second plain lease deadlocks instead (timeout, not an assertion). The body's phrasing could be read either way, but the intended reading holds. Suggested wording: "Dropping the reservation, so only the plain lease remains, makes the `true` case fail."
- *`vp run check:changed` passes.* Not rerun; repo-wide checks are out of scope for this audit. Unverified, so CI owns it.
- *Not checked on case-insensitive FS.* An honest limitation.

## Remaining gaps (task 4)

Rows 9 and 10 are verified by inspection. They are early-return branches identical to main's behaviour and can't rewrite files, so they don't bear on the fix's claims. Row 5 is now red/green. Row 16 is a design note outside what the PR claims. Rows 11–15 are proven at head only, which is correct for no-regression and cleanup rows. Nothing material is missing for the stated claims.

Optional body edits for the author: reword the mutation sentence as suggested above, fix "parent..", and note that the red and green test bodies differ in the restore-side primitive.

FRICTION: My first mutation (double lease) deadlocked and burned the 120 s default timeout. Use `--testTimeout=20000` and mutate to plain `rollback`. Also, the head PTS rows can't run at merge-base because they import the new helper, so row 5's red has to target the intermediate commit 8e4748be4d. Assembling that in the before-worktree means overwriting 5 files and restoring them.

VERDICT: SUFFICIENT