fix(destroy): probe a group that no scan shows before the wait reads it ended

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

@@ -33,6 +33,7 @@
     "RecordsProgramSync": true,
     "ProvesGroupOwnership": true,
     "FreezesUnseenGroup": true,
+    "WaitProbesUnseenGroup": true,
     "FallbackNeedsFolder": true,
     "UnsharedGroupReadsUnknown": true,
     "TokenNamesProgram": true,
@@ -53,7 +54,7 @@
     "src/cli/commands/gc.ts#defaultDependencies": "ae2347cdb778b488",
     "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769",
     "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1",
-    "src/host/programGroup.ts#judgeFrozenGroup": "e3a6c281e3f579fc",
+    "src/host/programGroup.ts#judgeFrozenGroup": "8bfe9ea5c92a1c8f",
     "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9",
     "src/host/programGroup.ts#isUnreadableGroupError": "e2d852aa5b45cb53",
     "src/host/programGroup.ts#UNREADABLE_ERRNOS": "24de7f719ccf14be",
@@ -121,11 +122,11 @@
     "src/host/programGroup.ts#procHidesOtherUsers": "214f60a56d6573fa",
     "src/host/programGroup.ts#groupHasLiveProcess": "1d8026f335463a72",
     "src/host/programGroup.ts#scanGroup": "babc9d5767424243",
-    "src/host/programGroup.ts#isProcessGroupAlive": "ce1b8fca10085d51",
+    "src/host/programGroup.ts#isProcessGroupAlive": "cb20b5d3ec5d2979",
     "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b",
     "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1",
     "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82",
-    "src/host/programGroup.ts#stopProgramGroup": "215a685d9337aeb3",
+    "src/host/programGroup.ts#stopProgramGroup": "cf13959e57ccad10",
     "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328",
     "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd",
     "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9",
@@ -148,9 +149,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": "cd8639012467f13e",
-    "skill:scripts/facts.mjs": "ff97d3d2dfab5811",
-    "skill:scripts/check.sh": "17f2ce5bd1b1b090"
+    "skill:model/SessionLifecycle.tla": "9d2f5e19d5de78d2",
+    "skill:scripts/facts.mjs": "36ed7de152b0c580",
+    "skill:scripts/check.sh": "81d1f6f959f1dfca"
   },
   "callSites": {
     "writeManifest": [

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

@@ -137,6 +137,9 @@ CONSTANTS
     ProvesHostPid,          \* lifecycle.ts, hostRecord.ts: destroy --force
                             \*   kills the host only while its pid shows the
                             \*   boot id and start time that host.json holds
+    WaitProbesUnseenGroup,  \* programGroup.ts: isProcessGroupAlive probes
+                            \*   the group again when no scan shows a member,
+                            \*   and reads it alive while the probe finds it
     FreezesUnseenGroup,     \* programGroup.ts: stopProgramGroup sends
                             \*   SIGSTOP to a group that no scan shows and
                             \*   judges it again
@@ -150,6 +153,10 @@ CONSTANTS
     Unseen,                 \* the environment: no scan of /proc shows a
                             \*   live process of the program, as for a fork
                             \*   chain whose processes each live about 2 ms
+    FreezeMisses,           \* the environment: with Unseen, no freeze of
+                            \*   stopProgramGroup brings a member into view,
+                            \*   as when a SIGCONT from another process comes
+                            \*   before each judgement
     ZombiesInView,          \* the environment: with Unseen, the scans show
                             \*   zombies of the program's group, as under a
                             \*   PID 1 that never reaps
@@ -173,6 +180,7 @@ CONSTANTS
 ASSUME MaxListReconciles \in 1..3
 ASSUME Token \in BOOLEAN
 ASSUME Unseen \in BOOLEAN
+ASSUME FreezeMisses \in BOOLEAN
 ASSUME ZombiesInView \in BOOLEAN
 ASSUME OtherPidSpace \in BOOLEAN
 ASSUME Win32 \in BOOLEAN
@@ -197,7 +205,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup,
                  ReconcileRepairsDestroyed, ReconcileRepairsMarked,
                  TokenNamesProgram,
                  ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost,
-                 FreezesUnseenGroup, UnsharedGroupReadsUnknown} : b \in BOOLEAN
+                 FreezesUnseenGroup, WaitProbesUnseenGroup,
+                 UnsharedGroupReadsUnknown} : b \in BOOLEAN
 
 Readers == {"gc", "list"}   \* the two processes that run reconcileSession
 \* The group that a kill went through, and that the wait after it probes:
@@ -394,7 +403,8 @@ NoKill == UNCHANGED <<prog, left, hitUnrelated>>
 ProvenKill ==
     IF ~TokenNamesProgram THEN NoKill
     ELSE IF ProvesGroupOwnership /\ reused THEN NoKill
-    ELSE IF Unseen /\ ~FreezesUnseenGroup /\ ~reused /\ ~foreign THEN NoKill
+    ELSE IF Unseen /\ (~FreezesUnseenGroup \/ FreezeMisses) /\ ~reused
+            /\ ~foreign THEN NoKill
     ELSE KillsGroupId
 
 \* Without a token, readProgramGroup falls back to the childPid of the
@@ -426,8 +436,14 @@ GroupAlive == prog \/ foreign
 \* isProcessGroupAlive probes kill(-pgid, 0): every process with that group
 \* id reads alive, also one of an unrelated group that took it. EPERM, when
 \* every process left belongs to another user, reads alive only with
-\* ProbeCountsDeniedGroup.
-ProbeSees == prog \/ left \/ reused \/ (ProbeCountsDeniedGroup /\ foreign)
+\* ProbeCountsDeniedGroup. When the probe finds the group, the scans after it
+\* decide: with Unseen they show no process of the program, and with
+\* WaitProbesUnseenGroup a second probe that still finds the group reads it
+\* alive. Scans that show only zombies read the group ended either way.
+ProbeFindsUnseen == WaitProbesUnseenGroup /\ ~ZombiesInView
+ProbeSees ==
+    \/ (prog \/ left) /\ (~Unseen \/ ProbeFindsUnseen)
+    \/ reused \/ (ProbeCountsDeniedGroup /\ foreign)
 
 \* isProgramGroupAlive in waitForProcessesToExit, for the group that the
 \* kill before it went through. With a token it reads the group alive while
@@ -441,16 +457,23 @@ ProbeSees == prog \/ left \/ reused \/ (ProbeCountsDeniedGroup /\ foreign)
 \* TokenNamesProgram no member carries the recorded autogroup, so the group
 \* reads gone. Without ReusedIdReadsGone a group that took the id reads
 \* alive, because its members carry another autogroup. With Unseen the scans
-\* show no process of the program, and the probe after them reads the
-\* group gone, since the wait does not freeze it.
-GroupSeen(kind) ==
+\* show no process of the program, so the group reads gone, and the probe
+\* after them decides (ProbeFindsUnseen). GroupJudged leaves out that probe
+\* of a group with a token: gc judges such a group with its own probe
+\* (GcSeesGroup).
+GroupJudged(kind) ==
     /\ KillsProgramGroup
     /\ \/ kind = "proven" /\ TokenNamesProgram
           /\ (((prog \/ left) /\ ~Unseen) \/ foreign)
        \/ kind = "proven" /\ ~ReusedIdReadsGone /\ reused
        \/ kind = "bare" /\ ProbeSees
        \/ kind = "numeric" /\ FallbackReaches /\ ProbeSees
 
+GroupSeen(kind) ==
+    \/ GroupJudged(kind)
+    \/ /\ KillsProgramGroup /\ kind = "proven"
+       /\ Unseen /\ ProbeFindsUnseen /\ (prog \/ left)
+
 \* The group as destroy and reconcile see it. With OtherPidSpace no scan and
 \* no probe of theirs shows the program's processes: a group with a token
 \* reads gone, and gets no kill, because no member is in view.
@@ -1240,7 +1263,7 @@ GcReadsReconciled ==
 \* often.
 GcSeesGroup ==
     /\ ~OtherPidSpace /\ ~Refused
-    /\ \/ GroupSeen("proven")
+    /\ \/ GroupJudged("proven")
        \/ /\ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left)
           /\ (~ZombiesInView \/ GcFreezesUnseenGroup)
 

.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 ForceSkipsUnreadableGroup"
+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 WaitProbesUnseenGroup"
 # 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;
@@ -195,6 +195,10 @@ UNSEEN=FALSE
 # ZOMBIES: whether, with UNSEEN, the scans show zombies of the program's
 # group, as under a PID 1 that never reaps.
 ZOMBIES=FALSE
+# MISSES: whether, with UNSEEN, no freeze of stopProgramGroup brings a
+# member into view, as when a SIGCONT from another process comes before
+# each judgement.
+MISSES=FALSE
 # OTHER: whether destroy, list and gc run in another pid space than the host.
 OTHER=FALSE
 # WIN32: whether SIGTERM ends the host at once, as on Windows.
@@ -224,6 +228,7 @@ write_run() {
     done
     echo "  Token = $TOKEN"
     echo "  Unseen = $UNSEEN"
+    echo "  FreezeMisses = $MISSES"
     echo "  ZombiesInView = $ZOMBIES"
     echo "  OtherPidSpace = $OTHER"
     echo "  Win32 = $WIN32"
@@ -283,13 +288,20 @@ write_run mutant-ShutdownBothChecks violated TerminalIsFinal "ShutdownChecksComm
 # group is frozen.
 UNSEEN=TRUE
 write_run current-unseen pass "$RULES" "" "the code with a program that no scan shows: every rule holds"
-write_run mutant-FreezesUnseenGroup-unseen violated DestroyedProgramStopped "FreezesUnseenGroup=FALSE" "without the freeze, the kill finds no member in view, and destroy records destroyed while a fork chain runs" DestroyedProgramStopped
+# The wait probes the group that no scan shows, so the freeze and the probe
+# each keep destroy from recording destroyed while the chain runs.
+write_run mutant-UnseenBothGuards-unseen violated DestroyedProgramStopped "FreezesUnseenGroup=FALSE WaitProbesUnseenGroup=FALSE" "with neither the freeze nor the wait's probe, the kill finds no member in view, and destroy records destroyed while a fork chain runs" DestroyedProgramStopped
 write_run mutant-GcProbesUnseenGroup-unseen violated RemovedSessionStopped "GcProbesUnseenGroup=FALSE" "without the probe, gc removes program.json while a fork chain that the program left runs" RemovedSessionStopped
 # Under a PID 1 that never reaps, the chain also leaves zombies in view.
 # With every guard, that changes nothing, so current-unseen covers it.
 ZOMBIES=TRUE
 write_run mutant-GcFreezesUnseenGroup-unseen-zombies violated RemovedSessionStopped "GcFreezesUnseenGroup=FALSE" "without the freeze, gc reads a fork chain behind its zombies ended and removes program.json while it runs" RemovedSessionStopped
 ZOMBIES=FALSE
+# Every freeze misses the chain. The wait then times out.
+MISSES=TRUE
+write_run current-unseen-misses pass "$RULES" "" "the code with a fork chain that every freeze misses: every rule holds"
+write_run mutant-WaitProbesUnseenGroup-unseen-misses violated DestroyedProgramStopped "WaitProbesUnseenGroup=FALSE" "without the probe, the wait after a missed freeze reads the chain ended, and destroy records destroyed while it runs" DestroyedProgramStopped
+MISSES=FALSE
 UNSEEN=FALSE
 
 # destroy, list and gc run without /proc, or in another pid namespace or on

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

@@ -1273,14 +1273,33 @@ function ownershipFacts() {
       signalParam === "signal: 'SIGSTOP' | 'SIGCONT'" &&
       !stray,
     FreezesUnseenGroup: freezeFacts(stop.body),
+    WaitProbesUnseenGroup: waitProbeFacts(),
   };
 }
 
+// isProcessGroupAlive, which every wait reads through isProgramGroupAlive,
+// probes the group again when its probe found the group but no scan showed
+// a member, live or zombie, and reads the group alive while that probe finds
+// it. Without the second probe it reads such a group ended.
+function waitProbeFacts() {
+  const module = 'src/host/programGroup.ts';
+  const alive = requireDeclaration(module, 'isProcessGroupAlive').body
+    .statements;
+  return (
+    normalize(alive.at(-1)?.getText() ?? '') ===
+      'return groupHasLiveProcess(pgid) ?? probeFindsGroup(pgid);' &&
+    normalize(requireDeclaration(module, 'probeFindsGroup').body.getText()) ===
+      "{ try { process.kill(processGroupTarget(pgid), 0); return true; } catch (error) { if (hasErrorCode(error, 'ESRCH')) { return false; } if (hasErrorCode(error, 'EPERM')) { return true; } throw error; } }"
+  );
+}
+
 // In stopProgramGroup's loop, each judgement that gets no kill and is not
 // unproven sends SIGSTOP to the group and judges again: gone, unknown, and
 // owned with a witness that ended before its read. So a member that a scan
 // never shows, or that ends between two reads, stops and stays in view,
-// while /proc names this process by its pid. The finally block sends a
+// while /proc names this process by its pid. Before the first freeze, a
+// group that shows a stopped member gets none, so the SIGCONT cannot resume
+// a member that job control stopped. The finally block sends a
 // frozen group that got no kill SIGCONT, also when a scan throws.
 function freezeFacts(body) {
   const guarded = body.statements.find(ts.isTryStatement);
@@ -1300,13 +1319,14 @@ function freezeFacts(body) {
     before.at(-2) === 'let frozen = false;' &&
     before.at(-1) === 'let killed = false;' &&
     guarded.tryBlock.statements.length === 1 &&
-    st.length === 7 &&
+    st.length === 8 &&
     st[1] ===
       "if ( judgement.verdict === 'unproven' || (judgement.verdict === 'unknown' && !judgement.running) ) { return; }" &&
     st[2].startsWith("if (judgement.verdict === 'owned') {") &&
     st.slice(3).join('\n') ===
       [
         'if (!procShowsOwnPidSpace()) { return; }',
+        'if (!frozen && showsStoppedMember(group.pid)) { return; }',
         "frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen;",
         'if (!frozen) { return; }',
         'Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS);',
@@ -1558,7 +1578,10 @@ function frozenJudgesTwice() {
     judged.catchClause === undefined &&
     judged.finallyBlock !== undefined &&
     statementsOf(judged.tryBlock).join('\n') ===
-      'verdict = judgeLiveGroup(group).verdict;' &&
+      [
+        'Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS);',
+        'verdict = judgeLiveGroup(group).verdict;',
+      ].join('\n') &&
     statementsOf(judged.finallyBlock).join('\n') ===
       "signalProcessGroup(group.pid, 'SIGCONT');" &&
     normalize(decides?.getText() ?? '') ===