fix(storage): stop writeManifest from recreating a removed session folder

.agents/skills/verify-session-lifecycle/coverage.json

@@ -13,7 +13,7 @@
     "src/host/lifecycle.ts#stopSessionProcesses": "c2121dfa9d2c0d43",
     "src/host/lifecycle.ts#recordDestroyed": "6610e88a55a2aa0d",
     "src/host/lifecycle.ts#destroySession": "b2713e315822b08d",
-    "src/host/lifecycle.ts#reconcileSession": "32e17d1bc75bb636",
+    "src/host/lifecycle.ts#reconcileSession": "c506c699762d398f",
     "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb",
     "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1",
     "src/host/manifestWriter.ts#createSerialManifestWriter": "94a2decf4fedb2e2",
@@ -26,16 +26,16 @@
     "src/host/rpcServer.ts#RpcServer.listen": "aa62e1cd89eceaa4",
     "src/host/rpcServer.ts#RpcServer.close": "2d8092cceb4b8e13",
     "src/storage/manifests.ts#readValidatedJsonFile": "6287eb627b09bf80",
-    "src/storage/manifests.ts#writeTextFileAtomic": "87f4e3ecc13dbe59",
-    "src/storage/manifests.ts#writeManifest": "97c755b27788a6e5",
+    "src/storage/manifests.ts#replaceFileAtomic": "20532509b3dcaade",
+    "src/storage/manifests.ts#writeManifest": "1bcc99f09acfc577",
     "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d",
     "src/host/hostMain.ts#runHost(parts)": "d2cd124b6e820920",
     "src/host/hostMain.ts#runHost(final try)": "ad91fa180ff36ffb",
     "src/host/hostMain.ts#runHost>handlers.resize": "30dd1da32879d478",
     "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
-    "skill:model/SessionLifecycle.tla": "10ba06448b1bd6ff",
-    "skill:scripts/facts.mjs": "553e1cac7b74042a",
-    "skill:scripts/check.sh": "8059eab056acc01b"
+    "skill:model/SessionLifecycle.tla": "0b52bbddfeae290c",
+    "skill:scripts/facts.mjs": "82268d59fc07d657",
+    "skill:scripts/check.sh": "8ce08f1c1196895f"
   },
   "callSites": {
     "writeManifest": [
@@ -49,9 +49,12 @@
       "src/host/hostMain.ts#runHost>initiateShutdown",
       "src/host/hostMain.ts#runHost>resize"
     ],
+    "replaceFileAtomic": [
+      "src/storage/manifests.ts#writeManifest",
+      "src/storage/manifests.ts#writeTextFileAtomic"
+    ],
     "writeValidatedJsonFile": [
       "src/storage/artifactManifest.ts#writeArtifactManifest",
-      "src/storage/manifests.ts#writeManifest",
       "src/tools/canonicalBundleArtifacts.ts#writeCanonicalBundleManifest"
     ],
     "writeTextFileAtomic": [

.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla

@@ -47,6 +47,7 @@ CONSTANTS
                             \*   records destroyed through recordDestroyed
     DestroyKeepsExitCode,   \* lifecycle.ts: recordDestroyed writes
                             \*   { ...manifest, status, updatedAt } only
+    ManifestWriteNeedsFolder, \* manifests.ts: writeManifest runs no mkdir
     MaxListReconciles       \* how many times the "list" process reconciles
 
 ASSUME MaxListReconciles \in 1..3
@@ -55,7 +56,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal,
                  HostWaitsForManifest, ReconcileRereads,
                  HostSerializesWrites, HostStopsAfterTerminalWrite,
                  ShutdownChecksCommandable,
-                 DestroyRecordsDestroyed, DestroyKeepsExitCode} : b \in BOOLEAN
+                 DestroyRecordsDestroyed, DestroyKeepsExitCode,
+                 ManifestWriteNeedsFolder} : b \in BOOLEAN
 
 Readers == {"gc", "list"}   \* the two processes that run reconcileSession
 NoRead == [pid |-> FALSE, origin |-> "none", code |-> FALSE]
@@ -124,9 +126,13 @@ Init ==
     /\ dpc = "read" /\ dforce \in BOOLEAN /\ drd = NoRead /\ dres = "pending"
     /\ dsaw = FALSE /\ dkill = FALSE
 
-\* writeManifest -> writeTextFileAtomic in src/storage/manifests.ts: mkdir -p
-\* the session directory, write a temp file, rename it over session.json.
-\* The rename is the visible step. The mkdir brings back a removed directory.
+\* writeManifest in src/storage/manifests.ts: write a temp file in the session
+\* directory and rename it over session.json. The rename is the visible step.
+\* WriteLands: with ManifestWriteNeedsFolder there is no mkdir, so a write into
+\* a removed directory throws SESSION_NOT_FOUND and creates nothing. Without
+\* it, the write runs mkdir first and brings the directory back.
+WriteLands == dir \/ ~ManifestWriteNeedsFolder
+
 Write(s, pid, origin, code) ==
     /\ dir' = TRUE
     /\ mst' = s
@@ -168,7 +174,9 @@ CreateMakesDirectory ==
                    ghostVars, sock, hostVars, shutVars, readerVars,
                    destroyVars>>
 
-\* allocateSession: writeManifest with status "running".
+\* allocateSession: writeManifest with status "running". gc skips a directory
+\* without a manifest, so this write always finds its directory (TypeOK
+\* checks that).
 CreateWritesManifest ==
     /\ cpc = "write"
     /\ Write("running", CreateRecordsHostPid, "none", FALSE)
@@ -205,10 +213,12 @@ WriterStopped == HostSerializesWrites /\ HostStopsAfterTerminalWrite /\ hwt
 
 \* A host write lands, or writes nothing once the writer has stopped. The
 \* record carries the exit code once recordExit or recordDestroyed ran.
+\* WriteLands is false here only in a state that already breaks R1.
 HostWrite(s, code) ==
     IF WriterStopped
     THEN UNCHANGED <<diskVars, hwt>>
-    ELSE /\ Write(s, TRUE, "none", code)
+    ELSE /\ WriteLands
+         /\ Write(s, TRUE, "none", code)
          /\ hwt' = (hwt \/ s \in Terminal)
 
 \* A write lands. When the queued "destroying" write is next, its turn starts
@@ -427,14 +437,19 @@ ReconcileRereadsManifest(p) ==
 \* writeManifest(reconciledManifest): "running" becomes failed/host-death,
 \* "destroying" becomes destroyed, any other status that gets here becomes
 \* failed/unknown (the default branch). hostPid and childPid become null.
+\* When the directory is gone, the write throws SESSION_NOT_FOUND and
+\* reconcileSession returns.
 ReconcileWrites(p) ==
     /\ pc[p] = "r_write"
-    /\ CASE rd[p].st = "running" ->
-              Write("failed", FALSE, "host-death", rd[p].code)
-         [] rd[p].st = "destroying" ->
-              Write("destroyed", FALSE, "none", rd[p].code)
-         [] OTHER -> Write("failed", FALSE, "unknown", rd[p].code)
-    /\ pc' = [pc EXCEPT ![p] = "r_unlink"]
+    /\ IF WriteLands
+          THEN /\ CASE rd[p].st = "running" ->
+                         Write("failed", FALSE, "host-death", rd[p].code)
+                    [] rd[p].st = "destroying" ->
+                         Write("destroyed", FALSE, "none", rd[p].code)
+                    [] OTHER -> Write("failed", FALSE, "unknown", rd[p].code)
+               /\ pc' = [pc EXCEPT ![p] = "r_unlink"]
+          ELSE /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)]
+               /\ UNCHANGED diskVars
     /\ UNCHANGED <<ghostVars, sock, cpc, hostVars, shutVars, rd, gres, lruns,
                    destroyVars>>
 
@@ -554,14 +569,19 @@ DestroyReads ==
                    readerVars, dforce, dkill>>
 
 \* recordDestroyed: writeManifest({ ...manifest, status: 'destroyed' }) from
-\* the copy that destroy read. Its mkdir brings back a folder that gc
-\* removed in the meantime (coder/agent-tty#196).
+\* the copy that destroy read. When gc removed the directory in the meantime,
+\* the write throws SESSION_NOT_FOUND, and destroy reports that error.
 DestroyWritesDestroyed ==
     /\ dpc = "twrite"
-    /\ Write("destroyed", drd.pid, drd.origin, DestroyKeepsExitCode /\ drd.code)
-    /\ dpc' = "tunlink" /\ drd' = NoRead /\ dsaw' = TRUE
+    /\ IF WriteLands
+          THEN /\ Write("destroyed", drd.pid, drd.origin,
+                        DestroyKeepsExitCode /\ drd.code)
+               /\ dpc' = "tunlink" /\ drd' = NoRead /\ dsaw' = TRUE
+               /\ UNCHANGED dres
+          ELSE /\ DestroyEnds("error")
+               /\ UNCHANGED diskVars
     /\ UNCHANGED <<ghostVars, sock, cpc, hostVars, shutVars, readerVars,
-                   dforce, dres, dkill>>
+                   dforce, dkill>>
 
 \* recordDestroyed: unlinkIfPresent(socketFile). destroy reports success.
 DestroyUnlinksSocket ==
@@ -683,6 +703,7 @@ TypeOK ==
     /\ dsnap \in {"none", "destroying", "destroyed"}
     /\ (mst # "none") => dir
     /\ (dir /\ mst = "none") => cpc # "done"
+    /\ (cpc = "write") => dir
     /\ gres \in {"pending", "skipped", "removed"}
     /\ lruns \in 0..MaxListReconciles
     /\ dres \in {"pending", "ok", "error"}
@@ -740,6 +761,9 @@ DestroyedOnlyWhenEnded ==
 \* R9: destroy reports success only after it wrote destroyed or read it.
 DestroyEndsDestroyed == dres = "ok" => dsaw
 
+\* R10: once gc removed the session directory, no write brings it back.
+RemovedFolderStaysRemoved == gres = "removed" => ~dir
+
 \* Witnesses. check.sh expects TLC to report each one VIOLATED, which shows
 \* that the model reaches the state: the rules above are not true only
 \* because the model can never get there.

.agents/skills/verify-session-lifecycle/model/statechart-view.mjs

@@ -4,6 +4,8 @@
 const reader = (from, to) =>
   from.pc.gc === to.pc.gc ? 'another command' : 'gc';
 const reconciles = (from, to) => `${reader(from, to)} reconciles:`;
+const back = (from, to) =>
+  !from.dir && to.dir ? ' and brings back the session folder' : '';
 
 export const title =
   'One agent-tty session while gc, destroy and another command run';
@@ -89,7 +91,9 @@ export const step = (action, from, to) => {
     case 'ReconcileRereadsManifest':
       return `${reconciles(from, to)} reads the manifest again`;
     case 'ReconcileWrites':
-      return `${reconciles(from, to)} writes "${to.mst}"`;
+      return to.dir
+        ? `${reconciles(from, to)} writes "${to.mst}"${back(from, to)}`
+        : `${reconciles(from, to)} finds the folder gone and returns`;
     case 'ReconcileUnlinksSocket':
       return `${reconciles(from, to)} unlinks the socket file`;
     case 'GcFindsDirectory':
@@ -109,7 +113,9 @@ export const step = (action, from, to) => {
         ? 'destroy reads the manifest and fails'
         : 'destroy reads the manifest';
     case 'DestroyWritesDestroyed':
-      return 'destroy writes "destroyed"';
+      return to.dir
+        ? `destroy writes "destroyed"${back(from, to)}`
+        : 'destroy finds the folder gone and fails';
     case 'DestroyUnlinksSocket':
       return 'destroy unlinks the socket file and succeeds';
     case 'DestroyKills':

.agents/skills/verify-session-lifecycle/scripts/check.sh

@@ -122,7 +122,7 @@ TERMINAL=$(node -e '
   const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants;
   console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}");
 ' "$OUT/facts.json")
-GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode"
+GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder"
 # One "Guard=TRUE|FALSE" word per guard, read from the code by facts.mjs.
 FACTS_LINE=$(node -e '
   const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants;
@@ -132,7 +132,7 @@ FACTS_LINE=$(node -e '
   }).join(" "));
 ' "$OUT/facts.json" $GUARDS) || die "facts.json lacks a guard fact"
 
-RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal RecordedExitKept RunningSessionReachable HostStartsWhenCreated TerminalIsLastWrite DestroyedOnlyWhenEnded DestroyEndsDestroyed"
+RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal RecordedExitKept RunningSessionReachable HostStartsWhenCreated TerminalIsLastWrite DestroyedOnlyWhenEnded DestroyEndsDestroyed RemovedFolderStaysRemoved"
 WITNESSES="WitnessGcRemovesSession WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded"
 
 # --- runs ----------------------------------------------------------------
@@ -180,6 +180,7 @@ write_run mutant-ReconcileSkipsLiveHost violated HostDeathOnlyWhenDead "Reconcil
 write_run mutant-HostStopsAfterTerminalWrite violated TerminalIsLastWrite "HostStopsAfterTerminalWrite=FALSE" "without the stop, the exit write follows a destroyed record" TerminalIsLastWrite
 write_run mutant-DestroyRecordsDestroyed violated DestroyEndsDestroyed "DestroyRecordsDestroyed=FALSE" "without recordDestroyed, destroy succeeds on a session that is not destroyed" DestroyEndsDestroyed
 write_run mutant-DestroyKeepsExitCode violated RecordedExitKept "DestroyKeepsExitCode=FALSE" "without it, destroy writes destroyed without the exit code" RecordedExitKept
+write_run mutant-ManifestWriteNeedsFolder violated RemovedFolderStaysRemoved "ManifestWriteNeedsFolder=FALSE" "without it, a write after gc's rm brings the folder back" RemovedFolderStaysRemoved
 write_run mutant-ReconcileSkipsTerminal pass RecordedExitKept "ReconcileSkipsTerminal=FALSE" "redundant: the re-read returns on a terminal manifest"
 write_run mutant-GcSkipsNonCollectable pass NoLiveSessionDeleted "GcSkipsNonCollectable=FALSE" "redundant: the final check still skips"
 write_run mutant-GcFinalCheck pass NoLiveSessionDeleted "GcFinalCheck=FALSE" "redundant: the first check still skips"

.agents/skills/verify-session-lifecycle/scripts/facts.mjs

@@ -135,7 +135,7 @@ function reconcileFacts() {
     'manifest.hostPid !== null && hostAlive',
     ts.SyntaxKind.ReturnStatement,
   );
-  const write = indexOfStatement(body, /^await writeManifest\(/);
+  const write = indexOfStatement(body, /^(?:try \{\s*)?await writeManifest\(/);
   // The re-read after the host is found dead, its guard, and a reconciled
   // record built from that copy, all before the write.
   const reread = indexOfStatement(
@@ -418,6 +418,38 @@ function destroyFacts() {
   };
 }
 
+function manifestWriteFacts() {
+  const file = 'src/storage/manifests.ts';
+  const visited = new Set();
+  let renames = 0;
+  let mkdirs = 0;
+  const visit = (fn) => {
+    walk(fn.body, (node) => {
+      if (!ts.isCallExpression(node) || !ts.isIdentifier(node.expression)) {
+        return;
+      }
+      const name = node.expression.text;
+      if (name === 'rename') {
+        renames += 1;
+      }
+      if (name === 'mkdir' || name === 'mkdirSync') {
+        mkdirs += 1;
+      }
+      const local = findDeclaration(file, name);
+      if (
+        local !== undefined &&
+        ts.isFunctionDeclaration(local) &&
+        !visited.has(name)
+      ) {
+        visited.add(name);
+        visit(local);
+      }
+    });
+  };
+  visit(requireDeclaration(file, 'writeManifest'));
+  return { ManifestWriteNeedsFolder: renames > 0 && mkdirs === 0 };
+}
+
 function gcFacts() {
   const fn = requireDeclaration('src/cli/commands/gc.ts', 'gcSessions');
   let loop;
@@ -515,7 +547,7 @@ const COVERED = [
   ['src/host/rpcServer.ts', 'RpcServer.listen'],
   ['src/host/rpcServer.ts', 'RpcServer.close'],
   ['src/storage/manifests.ts', 'readValidatedJsonFile'],
-  ['src/storage/manifests.ts', 'writeTextFileAtomic'],
+  ['src/storage/manifests.ts', 'replaceFileAtomic'],
   ['src/storage/manifests.ts', 'writeManifest'],
   ['src/protocol/sessionStatusPolicy.ts', 'SESSION_STATUS_POLICIES'],
 ];
@@ -657,6 +689,7 @@ function hasRecursiveOption(call) {
 const TRACKED_CALLS = [
   'writeManifest',
   'persistManifest',
+  'replaceFileAtomic',
   'writeValidatedJsonFile',
   'writeTextFileAtomic',
   'manifestPath',
@@ -729,6 +762,7 @@ const constants = {
   ...createFacts(),
   ...hostFacts(),
   ...destroyFacts(),
+  ...manifestWriteFacts(),
   ...policyFacts(),
 };
 console.log(

src/host/README.md

@@ -41,8 +41,8 @@
 - The `signal` handler accepts only `SIGTERM`, `SIGINT`, `SIGKILL`, `SIGHUP`, `SIGUSR1` and `SIGUSR2`, and throws `INVALID_SIGNAL` for others. [hostMain.ts:runHost]
 - The `run` handler waits 30,000 ms by default. The `wait` handler needs exactly one of `exit` or `idleMs`, else it throws `INVALID_DURATION`. `waitForRender` polls every 200 ms. [hostMain.ts:runHost]
 - `runHost` handles PTY exit once. If the status is `destroying` it records `destroyed`, else `exited`. Shutdown runs once. [hostMain.ts:runHost]
-- `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest and `SESSION_ALREADY_DESTROYED` for a destroyed session. A terminal session moves to `destroyed` without a signal. A running session gets the `destroy` RPC, or `SIGKILL` with `force`. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. [lifecycle.ts:destroySession]
-- `reconcileSession` does nothing when the manifest is missing, the status is terminal or the host PID is alive. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. [lifecycle.ts:reconcileSession]
+- `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest, or when the session directory is gone at its `destroyed` write, and `SESSION_ALREADY_DESTROYED` for a destroyed session. A terminal session moves to `destroyed` without a signal. A running session gets the `destroy` RPC, or `SIGKILL` with `force`. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. [lifecycle.ts:destroySession]
+- `reconcileSession` does nothing when the manifest is missing, the status is terminal or the host PID is alive. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. When the session directory is gone at that write, it returns. [lifecycle.ts:reconcileSession]
 - `allocateSession` throws `INVALID_DIMENSIONS` for non-positive `cols` or `rows`, `STORAGE_READ_ERROR` when `cwd` is not a directory and `INVALID_INPUT` when the shell path is not a file. An empty `command` defaults to the shell path. It creates the session directory and calls `launch` only after these checks pass. [lifecycle.ts:allocateSession]
 - `buildReplayInput` validates the manifest with `SessionRecordSchema` and requires its `sessionId` to match. It validates the events with `validateEventRecords` unless `trustValidated` is set. `targetSeq` is -1 for no events, else from 0 to the last `seq`. [replay.ts:buildReplayInput]
 - `RpcServer.listen` removes a stale socket file (no answer within 1,000 ms, `ECONNREFUSED` or `ENOENT`) and throws when another server is listening. It asserts a socket path of at most 104 characters. [rpcServer.ts:RpcServer]

src/host/lifecycle.ts

@@ -742,6 +742,16 @@ export async function reconcileSession(
     ...(failureOrigin !== undefined ? { failureOrigin } : {}),
   };
 
-  await writeManifest(manifestFile, reconciledManifest);
+  try {
+    await writeManifest(manifestFile, reconciledManifest);
+  } catch (error) {
+    if (
+      error instanceof CliError &&
+      error.code === ERROR_CODES.SESSION_NOT_FOUND
+    ) {
+      return;
+    }
+    throw error;
+  }
   await unlinkIfPresent(socketPath(sessionDirectory));
 }