fix(destroy): destroy --force ends a session whose program group it cannot read

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

@@ -20,6 +20,7 @@
     "ShutdownChecksCommandable": true,
     "DestroyRecordsDestroyed": true,
     "DestroyKeepsExitCode": true,
+    "ForceSkipsUnreadableGroup": true,
     "DestroyStopsLeftovers": true,
     "ProvesHostPid": true,
     "ReconcileRepairsDestroyed": true,
@@ -48,11 +49,14 @@
     "src/cli/commands/create.ts#hostRuns": "b80eac3bb9523aaf",
     "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6",
     "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522",
-    "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332",
-    "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7",
+    "src/cli/commands/gc.ts#gcSessions": "4d996cc35406473a",
+    "src/cli/commands/gc.ts#defaultDependencies": "ae2347cdb778b488",
     "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769",
     "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1",
-    "src/host/programGroup.ts#judgeFrozenGroup": "d18458e7d70a5664",
+    "src/host/programGroup.ts#judgeFrozenGroup": "e3a6c281e3f579fc",
+    "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9",
+    "src/host/programGroup.ts#isUnreadableGroupError": "e2d852aa5b45cb53",
+    "src/host/programGroup.ts#UNREADABLE_ERRNOS": "24de7f719ccf14be",
     "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7",
     "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509",
     "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec",
@@ -86,7 +90,7 @@
     "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a",
     "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c",
     "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b",
-    "src/host/lifecycle.ts#destroySession": "d840dd07a0e481f5",
+    "src/host/lifecycle.ts#destroySession": "05edb5d2825ed857",
     "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c",
     "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757",
     "src/host/lifecycle.ts#reconcileSession": "739c83bf945000c6",
@@ -143,9 +147,9 @@
     "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67",
     "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542",
     "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
-    "skill:model/SessionLifecycle.tla": "7f1c6dd7943968c3",
-    "skill:scripts/facts.mjs": "6ee4da3ef9b6bac3",
-    "skill:scripts/check.sh": "b48bc5fd343aefb5"
+    "skill:model/SessionLifecycle.tla": "cd8639012467f13e",
+    "skill:scripts/facts.mjs": "2de6761bed77fb19",
+    "skill:scripts/check.sh": "fe2da7911682462a"
   },
   "callSites": {
     "writeManifest": [

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

@@ -166,7 +166,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 GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker"
+GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker ForceSkipsUnreadableGroup"
 # 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;
@@ -199,6 +199,11 @@ ZOMBIES=FALSE
 OTHER=FALSE
 # WIN32: whether SIGTERM ends the host at once, as on Windows.
 WIN32=FALSE
+# CHECKFAILS: whether destroy, list and gc fail every read of program.json.
+CHECKFAILS=FALSE
+# REFUSED: whether /proc of destroy, list and gc refuses the program's
+# autogroup.
+REFUSED=FALSE
 write_run() {
   local name=$1 expect=$2 invariants=$3 overrides=$4 note=$5 must=${6:-}
   local dir="$OUT/$name" fact guard value
@@ -222,6 +227,8 @@ write_run() {
     echo "  ZombiesInView = $ZOMBIES"
     echo "  OtherPidSpace = $OTHER"
     echo "  Win32 = $WIN32"
+    echo "  CheckFails = $CHECKFAILS"
+    echo "  Refused = $REFUSED"
     echo "  MaxListReconciles = 2"
     echo "SPECIFICATION Spec"
     echo "CHECK_DEADLOCK TRUE"
@@ -295,6 +302,22 @@ write_run mutant-UnsharedGroupReadsUnknown-otherspace violated DestroyedSessionS
 write_run mutant-CreateRecordsHost-otherspace violated HostDeathOnlyWhenDead "CreateRecordsHost=FALSE" "without the record from create, a reconcile in another pid space reads the starting host dead and records it failed" HostDeathOnlyWhenDead
 OTHER=FALSE
 
+# destroy, list and gc cannot read program.json (EACCES), or /proc fails with
+# a system error. gc keeps the session, and destroy --force ends it without
+# the read.
+CHECKFAILS=TRUE
+write_run current-checkfails pass "$RULES" "" "the code with program.json unreadable for destroy, list and gc: every rule holds"
+write_run witness-WitnessUncheckedForceDestroys-checkfails violated WitnessUncheckedForceDestroys "" "destroy --force ends a session whose group it cannot read while a process that the program left runs"
+write_run mutant-ForceSkipsUnreadableGroup-checkfails pass WitnessUncheckedForceDestroys "ForceSkipsUnreadableGroup=FALSE" "without the fallback, destroy --force fails on the read, so no command removes the session"
+CHECKFAILS=FALSE
+
+# /proc of destroy, list and gc refuses the autogroup of the program's
+# processes. gc cannot check the group, and destroy cannot prove it.
+REFUSED=TRUE
+write_run current-refused pass "$RULES" "" "the code with a /proc that refuses the program's autogroup: every rule holds"
+write_run witness-WitnessRefusedGcRemovesLeftover-refused violated WitnessRefusedGcRemovesLeftover "" "gc cannot check the group, so it removes an exited session while a process that the program left runs"
+REFUSED=FALSE
+
 # Without a token every kill falls back to the id that a manifest or the
 # host's own record names, as before program.json existed.
 TOKEN=FALSE

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

@@ -704,19 +704,15 @@ function destroyFacts() {
     const block = force.thenStatement;
     const first = indexOfStatement(
       block,
-      /^await stopSessionProcesses\(\s*sessionId,\s*await readSessionHost\(sessionDirectory, manifest\),\s*await readProgramGroup\(/,
+      /^await stopUnlessUnreadable\(\s*await readSessionHost\(sessionDirectory, manifest\),\s*\(\) => readProgramGroup\(sessionDirectory, manifest\.childPid\),?\s*\);$/,
     );
     const reread = indexOfStatement(
       block,
       /^const current = await readSessionManifestOrThrow\(/,
     );
     const group = indexOfStatement(
       block,
-      /^const group = await readProgramGroup\(/,
-    );
-    const second = indexOfStatement(
-      block,
-      /^await stopSessionProcesses\(\s*sessionId,\s*await readSessionHost\(sessionDirectory, current\),\s*group,/,
+      /^const group = await stopUnlessUnreadable\(\s*await readSessionHost\(sessionDirectory, current\),\s*\(\) => readProgramGroup\(sessionDirectory, current\.childPid\),?\s*\);$/,
     );
     const records = indexOfStatement(
       block,
@@ -726,8 +722,8 @@ function destroyFacts() {
       first >= 0 &&
       reread > first &&
       group > reread &&
-      second > group &&
-      records > second &&
+      records > group &&
+      stopsThenRecords.stops &&
       calls(block, 'reconcileSession').length === 0;
   }
   const stop = requireDeclaration(
@@ -757,6 +753,7 @@ function destroyFacts() {
       stopWaits &&
       waitsForProcessesOnly,
     DestroyKeepsExitCode: keepsExitCode,
+    ForceSkipsUnreadableGroup: forceRecords && stopsThenRecords.skipsUnreadable,
     DestroyStopsLeftovers:
       stopsThenRecords.records &&
       stopsThenRecords.stops &&
@@ -771,52 +768,155 @@ function destroyFacts() {
   };
 }
 
-// The statements of destroySession's local stopLeftoversThenRecordDestroyed:
-// with DestroyStopsLeftovers it stops the group that program.json proves,
-// waits for it, and only then records destroyed. readProvenProgramGroup
-// returns the record whenever it has a token, or the unshared group when
-// this process cannot prove that it shares the host's pid space. A session
-// that a process which saw the group recorded destroyed gets no wait for an
-// unshared group (trustsDestroyed).
+// destroySession's local stopLeftoversThenRecordDestroyed hands
+// stopUnlessUnreadable the read of program.json, and only then records
+// destroyed. readProvenProgramGroup returns the record whenever it has a
+// token, or the unshared group when this process cannot prove that it
+// shares the host's pid space. A session that a process which saw the
+// group recorded destroyed gets no wait for an unshared group
+// (trustsDestroyed). stopUnlessUnreadable reads the group, stops it and
+// waits. With skipsUnreadable, destroy --force that cannot read the group
+// (a system error) stops the host alone instead.
 const UNSHARED_RETURN =
   'return (await sharesHostPids(sessionDirectory, false)) ? record : UNSHARED_GROUP;';
-const STOP_UNLESS_TRUSTED =
-  "await stopSessionProcesses( sessionId, null, terminal.status === 'destroyed' && group !== null && 'unshared' in group ? null : group, sessionDirectory, signal, );";
-const STOP_ALWAYS =
-  'await stopSessionProcesses( sessionId, null, group, sessionDirectory, signal, );';
+const RETURN_UNLESS_TRUSTED =
+  "return terminal.status === 'destroyed' && group !== null && 'unshared' in group ? null : group;";
 
-function stopLeftoversThenRecordDestroyed(destroy) {
-  let found = [];
+function localArrows(destroy) {
+  const out = new Map();
   walk(destroy.body, (node) => {
     if (
       ts.isVariableDeclaration(node) &&
-      node.name.getText() === 'stopLeftoversThenRecordDestroyed' &&
       node.initializer !== undefined &&
       ts.isArrowFunction(node.initializer) &&
       ts.isBlock(node.initializer.body)
     ) {
-      found = node.initializer.body.statements.map((st) =>
-        normalize(st.getText()),
-      );
+      out.set(node.name.getText(), node.initializer.body.statements);
     }
   });
+  return out;
+}
+
+function statementsOf(block) {
+  return block.statements.map((st) => normalize(st.getText()));
+}
+
+function stopUnlessUnreadableFacts(arrows) {
+  const st = arrows.get('stopUnlessUnreadable') ?? [];
+  const [judge, declared, attempt, ...after] = st;
+  // readAndJudge reads the group and judges it once, with no kill.
+  const judges =
+    judge !== undefined &&
+    ts.isVariableStatement(judge) &&
+    judge.declarationList.declarations[0]?.name.getText() === 'readAndJudge' &&
+    (arrows.get('readAndJudge') ?? [])
+      .map((s) => normalize(s.getText()))
+      .join('\n') ===
+      [
+        'const group = await readGroup();',
+        'isProgramGroupAlive(group);',
+        'return group;',
+      ].join('\n');
+  if (
+    !judges ||
+    declared === undefined ||
+    normalize(declared.getText()) !== 'let group: ProgramGroup | null;' ||
+    attempt === undefined ||
+    !ts.isTryStatement(attempt) ||
+    attempt.catchClause === undefined ||
+    attempt.finallyBlock !== undefined
+  ) {
+    return { stops: false, skipsUnreadable: false };
+  }
+  // Only a read or a judgement that fails in the try can skip the group: the
+  // stop comes after the try, so a read that fails after a verdict fails the
+  // destroy. With --force, an unreadable read is read again after a poll
+  // interval, and only a second unreadable read skips the group.
+  const tried = statementsOf(attempt.tryBlock).join('\n');
+  const caught = attempt.catchClause.block.statements;
+  const stops =
+    tried === 'group = await readAndJudge();' &&
+    after.map((s) => normalize(s.getText())).join('\n') ===
+      [
+        'await stopSessionProcesses( sessionId, host, group, sessionDirectory, signal, );',
+        'return group;',
+      ].join('\n');
+  const [rethrows, waits, again, ...more] = caught;
+  const skipsUnreadable =
+    more.length === 0 &&
+    normalize(rethrows?.getText() ?? '') ===
+      'if (force !== true || !isUnreadableGroupError(error)) { throw error; }' &&
+    normalize(waits?.getText() ?? '') ===
+      'await pollDelay(DESTROY_POLL_INTERVAL_MS, signal);' &&
+    again !== undefined &&
+    ts.isTryStatement(again) &&
+    again.catchClause !== undefined &&
+    again.finallyBlock === undefined &&
+    statementsOf(again.tryBlock).join('\n') ===
+      'group = await readAndJudge();' &&
+    statementsOf(again.catchClause.block).join('\n') ===
+      [
+        'if (!isUnreadableGroupError(secondError)) { throw secondError; }',
+        'await stopSessionProcesses( sessionId, host, null, sessionDirectory, signal, );',
+        'return null;',
+      ].join('\n') &&
+    bodyIs(
+      'isUnreadableGroupError',
+      "const cause = hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR) ? (error as Error).cause : error; const code: unknown = cause instanceof Error ? (cause as { code?: unknown }).code : undefined; return ( !(cause instanceof CliError) && typeof code === 'string' && UNREADABLE_ERRNOS.has(code) );",
+    );
+  const rethrowsAll =
+    caught.map((s) => normalize(s.getText())).join('\n') === 'throw error;';
+  return {
+    stops: stops && (rethrowsAll || skipsUnreadable),
+    skipsUnreadable: stops && skipsUnreadable,
+  };
+}
+
+function stopLeftoversThenRecordDestroyed(destroy) {
+  const arrows = localArrows(destroy);
+  const found = arrows.get('stopLeftoversThenRecordDestroyed') ?? [];
+  const first = found[0];
+  let read = [];
+  if (
+    first !== undefined &&
+    ts.isExpressionStatement(first) &&
+    ts.isAwaitExpression(first.expression) &&
+    ts.isCallExpression(first.expression.expression)
+  ) {
+    const call = first.expression.expression;
+    const reader = call.arguments[1];
+    if (
+      call.expression.getText() === 'stopUnlessUnreadable' &&
+      call.arguments.length === 2 &&
+      call.arguments[0].getText() === 'null' &&
+      reader !== undefined &&
+      ts.isArrowFunction(reader) &&
+      ts.isBlock(reader.body)
+    ) {
+      read = statementsOf(reader.body);
+    }
+  }
+  const unless = stopUnlessUnreadableFacts(arrows);
   return {
     records:
       found.length > 0 &&
       /^await recordDestroyed\(manifestFile, socketFile, terminal, null\);$/.test(
-        found.at(-1),
+        normalize(found.at(-1).getText()),
       ),
     stops:
-      found.length === 3 &&
-      found[0] ===
+      found.length === 2 &&
+      read.length === 2 &&
+      read[0] ===
         'const group = await readProvenProgramGroup(sessionDirectory);' &&
-      [STOP_UNLESS_TRUSTED, STOP_ALWAYS].includes(found[1]) &&
+      [RETURN_UNLESS_TRUSTED, 'return group;'].includes(read[1]) &&
+      unless.stops &&
       bodyIs(
         'readProvenProgramGroup',
         `const record = await readProgramRecord(sessionDirectory); if (typeof record !== 'object' || !hasToken(record)) { return null; } ${UNSHARED_RETURN}`,
       ) &&
       bodyIs('hasToken', 'return record.bootId !== null;'),
-    trustsDestroyed: found[1] === STOP_UNLESS_TRUSTED,
+    trustsDestroyed: read[1] === RETURN_UNLESS_TRUSTED,
+    skipsUnreadable: unless.skipsUnreadable,
   };
 }
 
@@ -1404,6 +1504,53 @@ function rerunFacts() {
   };
 }
 
+// judgeFrozenGroup freezes and judges at most FROZEN_JUDGEMENTS times: SIGSTOP
+// where /proc shows this process's pid space, a judgement, and SIGCONT in a
+// finally. A frozen judgement other than gone decides; gone freezes again,
+// and gone after the last freeze is inconclusive, so gc judges again.
+function frozenJudgesTwice() {
+  const module = 'src/host/programGroup.ts';
+  const limit = requireDeclaration(module, 'FROZEN_JUDGEMENTS').initializer;
+  const statements = requireDeclaration(module, 'judgeFrozenGroup').body
+    .statements;
+  const loop = statements[0];
+  if (
+    limit === undefined ||
+    !ts.isNumericLiteral(limit) ||
+    !Number.isInteger(Number(limit.text)) ||
+    Number(limit.text) < 1 ||
+    statements.length !== 2 ||
+    loop === undefined ||
+    !ts.isForStatement(loop) ||
+    !ts.isBlock(loop.statement) ||
+    normalize(statements[1].getText()) !== 'return null;'
+  ) {
+    return false;
+  }
+  const head = normalize(
+    `${loop.initializer?.getText()}; ${loop.condition?.getText()}; ${loop.incrementor?.getText()}`,
+  );
+  const [stop, declared, judged, decides, ...rest] = loop.statement.statements;
+  return (
+    head === 'let frozen = 0; frozen < FROZEN_JUDGEMENTS; frozen += 1' &&
+    rest.length === 0 &&
+    normalize(stop?.getText() ?? '') ===
+      "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }" &&
+    normalize(declared?.getText() ?? '') ===
+      "let verdict: GroupJudgement['verdict'];" &&
+    judged !== undefined &&
+    ts.isTryStatement(judged) &&
+    judged.catchClause === undefined &&
+    judged.finallyBlock !== undefined &&
+    statementsOf(judged.tryBlock).join('\n') ===
+      'verdict = judgeLiveGroup(group).verdict;' &&
+    statementsOf(judged.finallyBlock).join('\n') ===
+      "signalProcessGroup(group.pid, 'SIGCONT');" &&
+    normalize(decides?.getText() ?? '') ===
+      "if (verdict !== 'gone') { return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; }"
+  );
+}
+
 function gcFacts() {
   const fn = requireDeclaration('src/cli/commands/gc.ts', 'gcSessions');
   let loop;
@@ -1536,11 +1683,7 @@ function gcFacts() {
     probes &&
     last ===
       'return live === null ? true : live ? null : judgeFrozenGroup(group);' &&
-    body('judgeFrozenGroup').join('\n') ===
-      [
-        "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }",
-        "try { const { verdict } = judgeLiveGroup(group); return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; } finally { signalProcessGroup(group.pid, 'SIGCONT'); }",
-      ].join('\n');
+    frozenJudgesTwice();
   return {
     GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile,
     GcFinalCheck: finalCheck,
@@ -1599,6 +1742,9 @@ const COVERED = [
   ['src/host/programGroup.ts', 'provenProgramGroupRuns'],
   ['src/host/programGroup.ts', 'judgeGroupForGc'],
   ['src/host/programGroup.ts', 'judgeFrozenGroup'],
+  ['src/host/programGroup.ts', 'FROZEN_JUDGEMENTS'],
+  ['src/host/programGroup.ts', 'isUnreadableGroupError'],
+  ['src/host/programGroup.ts', 'UNREADABLE_ERRNOS'],
   ['src/host/programGroup.ts', 'GC_JUDGEMENTS'],
   ['src/host/programGroup.ts', 'probeFindsGroup'],
   ['src/host/lifecycle.ts', 'allocateSession'],