fix(destroy): name an unreadable host.json in the HOST_TIMEOUT of an unshared group

.agents/skills/verify-session-lifecycle/SKILL.md

@@ -47,7 +47,7 @@ Yes, when the diff changes any of these:
 - `src/host/manifestWriter.ts` `createSerialManifestWriter`.
 - `src/cli/commands/gc.ts` `gcSessions` and `defaultDependencies`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, `writeMarkerOrLog` and `hostRuns`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`.
 - `src/host/sessionState.ts` `setDimensions`, `requestDestroy`, `recordDestroyed` and `recordExit`, `src/host/eventLog.ts` `EventLog.open`, `src/host/rpcServer.ts` `listen` and `close`, `src/host/rpcClient.ts` `toTransportCliError` (which socket errors read as `HOST_UNREACHABLE`).
-- `src/host/hostRecord.ts`: `captureHost`, `writeHostRecord`, `readHostRecord`, `pidExists`, `judgeHost`, `inPidNamespace`, `readTimeNamespace`, `inTimeNamespace`, `readMachineId`, `inHostPidSpace` and `sharesHostPids`.
+- `src/host/hostRecord.ts`: `captureHost`, `writeHostRecord`, `readHostRecord` with its `readHostRecordOrThrow`, `pidExists`, `judgeHost`, `inPidNamespace`, `readTimeNamespace`, `inTimeNamespace`, `readMachineId`, `inHostPidSpace` and `sharesHostPids`.
 - `src/storage/manifests.ts` `readValidatedJsonFile`, `replaceFileAtomic`, `replaceFileAtomicSync`, `writeValidatedJsonFileSync`, `writeManifest`, `writeDestroyMarker` and `writeCreateFailedMarker` with `writeEmptyMarker`.
 - The `SESSION_STATUS_POLICIES` table in `src/protocol/sessionStatusPolicy.ts`.
 - Any new or removed call to `writeManifest`, `persistManifest`, `replaceFileAtomic`, `writeValidatedJsonFile`, `writeTextFileAtomic`, `manifestPath`, `reconcileSession`, `writeProgramRecord` or `stopProgramGroup` (also through an import alias), or a recursive `rm` (one with `recursive: true`, whatever its argument is named), anywhere in `src/`.
@@ -65,7 +65,7 @@ From the repo root:
 .agents/skills/verify-session-lifecycle/scripts/check.sh
 ```
 
-It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. `CHECK_JOBS` runs run at a time (a new one starts as soon as one ends; the bash 3.2 of macOS waits for each batch). The runs that expect pass share the CPUs as TLC workers, at least 1 each, and the others keep 1 worker, so their traces stay the shortest. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=90` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=<folder>` keeps the results in that folder (default: a new temp folder, printed at the end).
+It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. `CHECK_JOBS` runs run at a time (a new one starts as soon as one ends; the bash 3.2 of macOS waits for each batch). The runs that expect pass share the CPUs as TLC workers, at least 1 each, and the others keep 1 worker, so their traces stay the shortest. Thirteen runs explore more than 20 million distinct states each, so `CHECK_JOBS=90` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=<folder>` keeps the results in that folder (default: a new temp folder, printed at the end).
 
 What it does:
 

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

@@ -70,7 +70,8 @@
     "src/host/lifecycle.ts#killHostBestEffort": "25fcfd52894e189c",
     "src/host/hostRecord.ts#captureHost": "2cf2057461621536",
     "src/host/hostRecord.ts#writeHostRecord": "be58a9c34e8fad35",
-    "src/host/hostRecord.ts#readHostRecord": "6e0fc70b53f945bc",
+    "src/host/hostRecord.ts#readHostRecord": "ae72a381b617a36e",
+    "src/host/hostRecord.ts#readHostRecordOrThrow": "cff845ca6764b043",
     "src/host/hostRecord.ts#pidExists": "d539275a0f6041ea",
     "src/host/hostRecord.ts#judgeHost": "85b37d524df156a4",
     "src/host/hostRecord.ts#inPidNamespace": "aaa5cdfdfbb99f33",
@@ -87,7 +88,7 @@
     "src/host/lifecycle.ts#readSessionManifestOrThrow": "9709f28e5e9cca4b",
     "src/host/lifecycle.ts#waitForTerminalManifest": "3f14811e8d2f5f7f",
     "src/host/lifecycle.ts#waitForProcessesToExit": "bdab1d674a6856b8",
-    "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a",
+    "src/host/lifecycle.ts#stopSessionProcesses": "5359cc5db2eefe4e",
     "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c",
     "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b",
     "src/host/lifecycle.ts#destroySession": "05edb5d2825ed857",
@@ -148,7 +149,7 @@
     "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542",
     "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
     "skill:model/SessionLifecycle.tla": "cd8639012467f13e",
-    "skill:scripts/facts.mjs": "3ef7fa152ec0af36",
+    "skill:scripts/facts.mjs": "69cbe689f7e9713d",
     "skill:scripts/check.sh": "17f2ce5bd1b1b090"
   },
   "callSites": {

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

@@ -1766,6 +1766,7 @@ const COVERED = [
   ['src/host/hostRecord.ts', 'captureHost'],
   ['src/host/hostRecord.ts', 'writeHostRecord'],
   ['src/host/hostRecord.ts', 'readHostRecord'],
+  ['src/host/hostRecord.ts', 'readHostRecordOrThrow'],
   ['src/host/hostRecord.ts', 'pidExists'],
   ['src/host/hostRecord.ts', 'judgeHost'],
   ['src/host/hostRecord.ts', 'inPidNamespace'],

docs/USAGE.md

@@ -316,7 +316,7 @@ agent-tty record diff <session-id> <session-id> --at-seq-a 0 --json
 On Linux it also ends those processes when the program has already exited or the session has failed.
 A group whose processes each fork their successor and end too fast for any scan of `/proc` to show one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT.
 `destroy --force` kills the host and the program's group without asking the host first.
-When a read of the program's group fails with an error that every later read repeats, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), `gc` keeps the session and reports "failed to check the session's program group (destroy --force removes it)", or "failed to reconcile session (destroy --force removes it)" for a session whose host died. Those errors are EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. A plain `destroy` fails on the same read. When the read of `program.json` or the first check of the group fails that way twice, 100 ms apart, `destroy --force` stops the host alone, without the group, and records the session as `destroyed` once the host has ended, so the next `gc` removes it. A process that the program left can outlive such a `destroy --force`. When the second read passes, `destroy --force` stops the group as usual. A read that fails after that first check, a group that reads alive, or a host that does not end (`HOST_TIMEOUT`) still fails it. Other errors, such as EMFILE, ENOMEM or EAGAIN, can pass, so `gc` gives no such hint and `destroy --force` fails on them too. A `host.json` that cannot be read counts as missing, so the group reads as out of view: `destroy --force` fails with `HOST_TIMEOUT`, and `gc` removes the session, as in another pid namespace.
+When a read of the program's group fails with an error that every later read repeats, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), `gc` keeps the session and reports "failed to check the session's program group (destroy --force removes it)", or "failed to reconcile session (destroy --force removes it)" for a session whose host died. Those errors are EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. A plain `destroy` fails on the same read. When the read of `program.json` or the first check of the group fails that way twice, 100 ms apart, `destroy --force` stops the host alone, without the group, and records the session as `destroyed` once the host has ended, so the next `gc` removes it. A process that the program left can outlive such a `destroy --force`. When the second read passes, `destroy --force` stops the group as usual. A read that fails after that first check, a group that reads alive, or a host that does not end (`HOST_TIMEOUT`) still fails it. Other errors, such as EMFILE, ENOMEM or EAGAIN, can pass, so `gc` gives no such hint and `destroy --force` fails on them too. A `host.json` that cannot be read counts as missing, so the group reads as out of view, as in another pid namespace: `destroy --force` fails with `HOST_TIMEOUT`, and its message names `host.json` and the error. When the read was refused (EACCES or EPERM), make that file readable and run `destroy` again. Until then, `gc` removes such a session once it has ended, but a session whose host died while it ran stays `running`, because its group reads alive.
 `list`, `inspect`, `destroy` and `gc` reconcile a session whose host died: they kill the program's group and record the session as `failed` (or `exited` or `destroyed`).
 A `destroy` that runs inside the session, such as one typed into the session's shell, runs again outside the session and prints its result once the session has ended.
 The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`.

src/host/README.md

@@ -27,7 +27,7 @@
 - `captureProgram(pid)` returns a `ProgramRecord` (`version`, `pid`, `bootId`, `autogroup`) for the program that the host just spawned, and `writeProgramRecord(sessionDirectory, record)` writes it to `program.json`. `bootId` is a string and `autogroup` a number, or both are `null`. [programGroup.ts:captureProgram] [programGroup.ts:writeProgramRecord]
 - `readProvenProgramGroup(sessionDirectory)` returns the `program.json` record when it has a token and `sharesHostPids` reads true, the unshared group (below) when it has a token and `sharesHostPids` reads false, else `null`. `readProgramGroup(sessionDirectory, childPid)` returns the same for a record with a token, else `{ childPid, sessionDirectory }`, or `null` when `childPid` is `null` or, on Linux, when `host.json` names another pid namespace or machine id than the CLI's (`sharesHostPids`). For a record with a token where `sharesHostPids` reads false, which includes a missing `host.json`, a CLI that cannot read `/proc/self/ns/pid` and a CLI whose `/proc/self` does not name its own pid, both return the unshared group `{ unshared: true }`: no scan or probe of this process shows the program's processes, so `isProgramGroupAlive` reads it alive and `stopProgramGroup` sends it nothing. A `program.json` that does not validate reads as `null` in both, so it gets no kill and no throw. [programGroup.ts:readProgramRecord] [programGroup.ts:readProvenProgramGroup] [programGroup.ts:readProgramGroup] [hostRecord.ts:sharesHostPids]
 - `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows gets SIGSTOP and another judgement, at each of up to 5 judgements while `/proc/self` names this process's pid, and SIGCONT when it gets no kill. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc/<pid>/stat` and `/proc/<pid>/autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat]
-- `captureHost(pid)` returns a `HostRecord` (`version`, `pid`, `bootId`, `startTicks`, `pidNamespace`, `timeNamespace`, `machineId`) on Linux when `/proc` shows the process and the boot id, else `null`. `machineId` is the first of `/etc/machine-id` and `/var/lib/dbus/machine-id` that holds 32 hex characters, else `null`. A record without `timeNamespace` and `machineId`, which a build between #260 and #267 wrote, still reads, and only the checks of those two fields are skipped. `writeHostRecord(sessionDirectory, record)` writes it as `host.json`, and `readHostRecord(sessionDirectory)` returns it, or `null` when it is missing or unreadable. `judgeHost(pid, record)` returns `dead` only when no process has the pid, a zombie has it, or the record names another boot id or start time, `alive` when both match, and `unknown` otherwise: also off Linux for a pid that exists, for a CLI in another pid namespace or on another machine than the record names, and, instead of a start time mismatch, for a CLI in another time namespace. [hostRecord.ts:captureHost] [hostRecord.ts:writeHostRecord] [hostRecord.ts:readHostRecord] [hostRecord.ts:judgeHost]
+- `captureHost(pid)` returns a `HostRecord` (`version`, `pid`, `bootId`, `startTicks`, `pidNamespace`, `timeNamespace`, `machineId`) on Linux when `/proc` shows the process and the boot id, else `null`. `machineId` is the first of `/etc/machine-id` and `/var/lib/dbus/machine-id` that holds 32 hex characters, else `null`. A record without `timeNamespace` and `machineId`, which a build between #260 and #267 wrote, still reads, and only the checks of those two fields are skipped. `writeHostRecord(sessionDirectory, record)` writes it as `host.json`, and `readHostRecord(sessionDirectory)` returns it, or `null` when it is missing or unreadable. `hostRecordError(sessionDirectory)` returns the error when the file exists but its read or its check fails, else `null`, so that the `HOST_TIMEOUT` of `destroySession` for an unshared group names `host.json` and that error instead of another pid namespace, and says to make the file readable only for EACCES or EPERM. `judgeHost(pid, record)` returns `dead` only when no process has the pid, a zombie has it, or the record names another boot id or start time, `alive` when both match, and `unknown` otherwise: also off Linux for a pid that exists, for a CLI in another pid namespace or on another machine than the record names, and, instead of a start time mismatch, for a CLI in another time namespace. [hostRecord.ts:captureHost] [hostRecord.ts:writeHostRecord] [hostRecord.ts:readHostRecord] [hostRecord.ts:hostRecordError] [hostRecord.ts:judgeHost]
 - `SessionState` holds the host's in-memory `SessionRecord` (type from `src/protocol/schemas.ts`). Methods: `snapshot`, `setChildPid`, `setDimensions`, `setFailureOrigin`, `requestDestroy`, `recordDestroyed` and `recordExit`. [sessionState.ts:SessionState]
 - `createSerialManifestWriter(path, snapshot, write?)` returns a function that writes `snapshot()` to `path`. The default `write` is `writeManifest` (`src/storage/manifests.ts`). `runHost` sends every manifest write through one such function. [manifestWriter.ts:createSerialManifestWriter] [hostMain.ts:runHost]
 - `EventLog` is the append-only JSONL event log with an in-memory buffer. Methods: `static open(filePath)`, `append(type, payload)` (returns the new `seq`), `startAppend('input_run', payload)` (returns `{ seq, written }` without an `await`), `getEvents`, `getEventsSince(afterSeq)`, `readAll` and `close`. [eventLog.ts:EventLog]

src/host/hostRecord.ts

@@ -139,24 +139,43 @@ export function writeHostRecord(
   });
 }
 
-export async function readHostRecord(
+async function readHostRecordOrThrow(
   sessionDirectory: string,
 ): Promise<HostRecord | null> {
   const path = hostRecordPath(sessionDirectory);
+  return await readValidatedJsonFile({
+    path,
+    pathLabel: 'host record path',
+    allowMissing: true,
+    readErrorMessage: `Failed to read the host record at ${path}.`,
+    invalidJsonMessage: `The host record contains invalid JSON at ${path}.`,
+    validate: validateHostRecord,
+  });
+}
+
+export async function readHostRecord(
+  sessionDirectory: string,
+): Promise<HostRecord | null> {
   try {
-    return await readValidatedJsonFile({
-      path,
-      pathLabel: 'host record path',
-      allowMissing: true,
-      readErrorMessage: `Failed to read the host record at ${path}.`,
-      invalidJsonMessage: `The host record contains invalid JSON at ${path}.`,
-      validate: validateHostRecord,
-    });
+    return await readHostRecordOrThrow(sessionDirectory);
   } catch {
     return null;
   }
 }
 
+// The error of a host.json that exists but whose read or check fails, so
+// that readHostRecord reads it as missing. null when it reads.
+export async function hostRecordError(
+  sessionDirectory: string,
+): Promise<Error | null> {
+  try {
+    await readHostRecordOrThrow(sessionDirectory);
+    return null;
+  } catch (error) {
+    return error instanceof Error ? error : new Error(String(error));
+  }
+}
+
 // Without host.json nothing names the host's pid space: a session from an
 // agent-tty version before it, or one whose create and host could not read
 // /proc. Since the host writes host.json before program.json, only a version

src/host/lifecycle.ts

@@ -44,6 +44,7 @@ import {
 } from './programGroup.js';
 import {
   captureHost,
+  hostRecordError,
   judgeHost,
   readHostRecord,
   writeHostRecord,
@@ -879,7 +880,7 @@ async function stopSessionProcesses(
               : 'End the session with a plain destroy, or run destroy --force where /proc is mounted.'
           }`
         : group !== null && 'unshared' in group
-          ? " This process runs in another pid namespace or on another machine than the session's host, so it cannot prove which processes are the session's. Run destroy from the host's pid namespace on the host's machine."
+          ? await unsharedGroupHint(sessionDirectory)
           : '';
     throw makeCliError(ERROR_CODES.HOST_TIMEOUT, {
       message: `Timed out forcing session "${sessionId}" to exit.${hint}`,
@@ -888,6 +889,28 @@ async function stopSessionProcesses(
   }
 }
 
+// A group reads unshared when host.json names another pid space or machine,
+// and when this process cannot read host.json, which readHostRecord reads as
+// missing.
+async function unsharedGroupHint(sessionDirectory: string): Promise<string> {
+  const error = await hostRecordError(sessionDirectory);
+  if (error === null) {
+    return " This process runs in another pid namespace or on another machine than the session's host, so it cannot prove which processes are the session's. Run destroy from the host's pid namespace on the host's machine.";
+  }
+  const code: unknown =
+    error.cause instanceof Error
+      ? (error.cause as { code?: unknown }).code
+      : undefined;
+  // Only a read that the permissions refuse passes once the file is
+  // readable. A folder, invalid JSON or an invalid record does not.
+  const refused = code === 'EACCES' || code === 'EPERM';
+  return ` ${error.message.replace(/\.$/, '')}${
+    typeof code === 'string' ? ` (${code})` : ''
+  }, so this process cannot prove which processes are the session's.${
+    refused ? ' Make that file readable and run destroy again.' : ''
+  }`;
+}
+
 export interface DestroySessionOptions {
   readonly signal?: AbortSignal;
 }
@@ -1178,8 +1201,9 @@ export async function reconcileSession(
   const manifest = await readManifestIfExists(manifestFile);
 
   // Only recordDestroyed writes the marker, and only for a terminal manifest
-  // or once the host and the program's group are dead. So the host has
-  // ended or is ending, and the repair removes both sockets without a
+  // or once the host is dead. The program's group reads dead then too,
+  // except after a destroy --force that cannot read the group. So the host
+  // has ended or is ending, and the repair removes both sockets without a
   // liveness check.
   if (manifest !== null && isMarkedDestroyed(sessionDirectory, manifest)) {
     if (await writeMarkedDestroyed(manifestFile, manifest)) {