fix(host): read a terminal session next to the destroy marker as destroyed

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

@@ -34,9 +34,11 @@
     "src/host/lifecycle.ts#waitForProcessesToExit": "bdab1d674a6856b8",
     "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a",
     "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c",
-    "src/host/lifecycle.ts#removeDeadHostSocket": "e4044ea706544ff8",
+    "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b",
     "src/host/lifecycle.ts#destroySession": "d840dd07a0e481f5",
-    "src/host/lifecycle.ts#reconcileSession": "c2904456d54b87c8",
+    "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c",
+    "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757",
+    "src/host/lifecycle.ts#reconcileSession": "4e5dac8144a0d9fb",
     "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb",
     "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1",
     "src/host/hostMain.ts#SHUTDOWN_KILL_GRACE_MS": "51171d9c5aa6c510",
@@ -87,16 +89,17 @@
     "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7",
     "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542",
     "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
-    "skill:model/SessionLifecycle.tla": "25bc78980b0d67cd",
-    "skill:scripts/facts.mjs": "86ec94456c10cb37",
-    "skill:scripts/check.sh": "422878fda4460ac0"
+    "skill:model/SessionLifecycle.tla": "f7270faba013acff",
+    "skill:scripts/facts.mjs": "6ae4fd3279517f42",
+    "skill:scripts/check.sh": "3a47553300cb217a"
   },
   "callSites": {
     "writeManifest": [
       "src/host/lifecycle.ts#allocateSession",
       "src/host/lifecycle.ts#reconcileSession",
       "src/host/lifecycle.ts#reconcileSession",
-      "src/host/lifecycle.ts#recordDestroyed"
+      "src/host/lifecycle.ts#recordDestroyed",
+      "src/host/lifecycle.ts#writeMarkedDestroyed"
     ],
     "persistManifest": [
       "src/host/hostMain.ts#runHost",
@@ -142,6 +145,7 @@
     "reconcileSession": [
       "src/cli/commands/gc.ts#gcSessions",
       "src/cli/commands/inspect.ts#runInspectCommand",
+      "src/cli/commands/inspect.ts#runInspectCommand",
       "src/host/lifecycle.ts#destroySession",
       "src/host/lifecycle.ts#destroySession",
       "src/host/lifecycle.ts#listSessions"

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

@@ -90,6 +90,9 @@ CONSTANTS
                             \*   destroy marker before destroyed, and a
                             \*   reconcile that finds it after its own write
                             \*   writes destroyed again
+    ReconcileRepairsMarked, \* lifecycle.ts: a reconcile that reads a
+                            \*   terminal manifest other than destroyed next
+                            \*   to the destroy marker writes destroyed
     CreateStopsOnGiveUp,    \* create.ts: a create that gives up on its
                             \*   host sends it SIGTERM, so the host stops
                             \*   its program and ends the session
@@ -139,7 +142,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal,
                  InsideCheckReadsEnv, RecordsProgramSync,
                  ProvesGroupOwnership, DestroyStopsLeftovers,
                  FallbackNeedsFolder, CreateStopsOnGiveUp,
-                 ReconcileRepairsDestroyed, TokenNamesProgram,
+                 ReconcileRepairsDestroyed, ReconcileRepairsMarked,
+                 TokenNamesProgram,
                  ReusedIdReadsGone, ProvesHostPid,
                  FreezesUnseenGroup, UnsharedGroupReadsUnknown} : b \in BOOLEAN
 
@@ -164,6 +168,8 @@ VARIABLES
     dmark,       \* the destroy marker file exists in the session directory
     rec,         \* program.json names the program with its token
     startFailed, \* ghost: the host died because its files were missing
+    readRepaired, \* ghost: a reconcile wrote destroyed from its first read
+                 \*   next to the destroy marker
     sock,        \* the RPC socket file exists (it is outside the directory)
     cpc,         \* create: "alloc", "write", "launch", "done", "failed"
                  \*   (it gave up on its host)
@@ -226,7 +232,7 @@ VARIABLES
 
 diskVars == <<dir, mst, mpid, morigin, mcode, mchild, wasTerminal, wasExited,
               wasNamed, dmark>>
-ghostVars == <<startFailed>>
+ghostVars == <<startFailed, readRepaired>>
 hostVars == <<hostAlive, hpc, hex, rsz, prog, foreign, left>>
 groupVars == <<rec, reused, hitUnrelated, diedUnrecorded, passedReused,
                hrec, hreused, hitUnrelatedHost>>
@@ -241,7 +247,7 @@ Init ==
     /\ mcode = FALSE /\ mchild = FALSE
     /\ wasTerminal = FALSE /\ wasExited = FALSE /\ wasNamed = FALSE
     /\ dmark = FALSE
-    /\ rec = FALSE /\ startFailed = FALSE
+    /\ rec = FALSE /\ startFailed = FALSE /\ readRepaired = FALSE
     /\ sock = FALSE
     /\ cpc = "alloc"
     /\ hostAlive = FALSE /\ hpc = "none" /\ hex = "none" /\ rsz = "none"
@@ -391,6 +397,7 @@ CliKillThrough(named) == IF OtherPidSpace THEN NoKill ELSE KillThrough(named)
 \* The host fails to start because its files are missing or were rewritten.
 HostFailsToStart ==
     /\ startFailed' = TRUE
+    /\ readRepaired' = readRepaired
     /\ hostAlive' = FALSE
     /\ hpc' = "dead"
     /\ hex' = IF hex = "none" THEN "none" ELSE "gone"
@@ -812,18 +819,29 @@ AfterReconcile(p) == IF p = "gc" THEN "readafter" ELSE "idle"
 \* isProcessAlive(manifest.hostPid). A null hostPid reads as a dead host.
 SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ hostAlive
 
-\* readManifestIfExists; return when it is null or terminal.
+\* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest
+\* other than destroyed next to the destroy marker (isMarkedDestroyed) goes
+\* to the repair write from this copy ("r_marked"). Otherwise it returns when
+\* the manifest is null or terminal.
 ReconcileReads(p) ==
     /\ pc[p] = "r_read"
-    /\ IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal)
+    /\ IF ReconcileRepairsMarked /\ dmark /\ mst \in Terminal
+          /\ mst # "destroyed"
+          THEN /\ pc' = [pc EXCEPT ![p] = "r_marked"]
+               /\ rd' = [rd EXCEPT ![p] = [st |-> mst, pid |-> mpid,
+                                           code |-> mcode, child |-> mchild,
+                                           grp |-> "none"]]
+               /\ UNCHANGED <<diskVars, readRepaired>>
+       ELSE IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal)
           THEN /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)]
-               /\ UNCHANGED rd
+               /\ UNCHANGED <<rd, diskVars, readRepaired>>
           ELSE /\ pc' = [pc EXCEPT ![p] = "r_check"]
                /\ rd' = [rd EXCEPT ![p] = [st |-> mst, pid |-> mpid,
                                            code |-> mcode, child |-> mchild,
                                            grp |-> "none"]]
-    /\ UNCHANGED <<diskVars, ghostVars, sock, cpc, hostVars, shutVars, gres,
-                   lruns, destroyVars, groupVars>>
+               /\ UNCHANGED <<diskVars, readRepaired>>
+    /\ UNCHANGED <<startFailed, sock, cpc, hostVars, shutVars, gres, lruns,
+                   destroyVars, groupVars>>
 
 \* After its group kill, reconcileSession waits for the group, or, without
 \* ReconcileWaitsForGroup, writes at once.
@@ -931,6 +949,21 @@ ReconcileRepairs(p) ==
     /\ UNCHANGED <<ghostVars, sock, cpc, hostVars, shutVars, rd, gres, lruns,
                    destroyVars, groupVars>>
 
+\* writeMarkedDestroyed: writeManifest destroyed from the copy that the read
+\* took, with hostPid and childPid null and the exit code kept. When gc
+\* removed the folder in the meantime, the write throws SESSION_NOT_FOUND,
+\* and reconcile returns. Otherwise it unlinks the socket and returns.
+ReconcileWritesMarked(p) ==
+    /\ pc[p] = "r_marked"
+    /\ IF WriteLands
+          THEN /\ Write("destroyed", FALSE, "none", rd[p].code, FALSE)
+               /\ pc' = [pc EXCEPT ![p] = "r_unlink"]
+               /\ readRepaired' = TRUE
+          ELSE /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)]
+               /\ UNCHANGED <<diskVars, readRepaired>>
+    /\ UNCHANGED <<startFailed, sock, cpc, hostVars, shutVars, rd, gres, lruns,
+                   destroyVars, groupVars>>
+
 \* unlinkIfPresent(socketPath(sessionDirectory))
 ReconcileUnlinksSocket(p) ==
     /\ pc[p] = "r_unlink"
@@ -1295,7 +1328,7 @@ Next ==
           \/ ReconcileRereadsManifest(p) \/ ReconcileReadsRecord(p)
           \/ ReconcilePollsGroup(p)
           \/ ReconcileWrites(p) \/ ReconcileRepairs(p)
-          \/ ReconcileUnlinksSocket(p)
+          \/ ReconcileWritesMarked(p) \/ ReconcileUnlinksSocket(p)
     \/ GcFindsDirectory \/ GcReadsManifest \/ GcReadsReconciled
     \/ GcFinalRead \/ GcRemoves
     \/ ListStartsReconcile
@@ -1315,7 +1348,7 @@ Spec == Init /\ [][Next]_vars
 TypeOK ==
     /\ dmark => dir
     /\ {dir, mpid, mchild, wasTerminal, wasExited, wasNamed, dmark, startFailed,
-        sock,
+        readRepaired, sock,
         hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, rec, left,
         reused, hitUnrelated, diedUnrecorded, passedReused, hrec, hreused,
         hitUnrelatedHost}
@@ -1446,6 +1479,7 @@ NoUnrelatedHostKilled == ~hitUnrelatedHost
 WitnessGcRemovesSession == gres # "removed"
 WitnessReconcileRepairs ==
     ~(dmark /\ mst = "failed" /\ \E p \in Readers : pc[p] = "r_repair")
+WitnessMarkedRepaired == ~readRepaired
 WitnessCreateGivesUp ==
     ~(cpc = "failed" /\ sig /\ mst = "destroyed" /\ ~hostAlive)
 WitnessSessionServes == ~(hpc = "serving" /\ sock /\ mst = "running" /\ mpid)

.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 ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid FreezesUnseenGroup UnsharedGroupReadsUnknown"
+GUARDS="GcSkipsNonCollectable GcFinalCheck 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 FreezesUnseenGroup UnsharedGroupReadsUnknown"
 # 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;
@@ -136,7 +136,7 @@ NO_TOKEN_RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal Recor
 # R15 and R16 are what the token adds, so only the runs with Token check them.
 RULES="$NO_TOKEN_RULES NoUnrelatedGroupKilled DestroyedSessionStopped"
 NO_TOKEN_WITNESSES="WitnessCreateGivesUp WitnessCrashReconciled WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessReconcileRepairs"
-WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessUnrecordedHostMeetsKill"
+WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessUnrecordedHostMeetsKill"
 
 # --- runs ----------------------------------------------------------------
 
@@ -207,6 +207,7 @@ write_run mutant-CreateStopsOnGiveUp violated FailedCreateStopped "CreateStopsOn
 write_run mutant-TokenNamesProgram violated DestroyedSessionStopped "TokenNamesProgram=FALSE" "with the host's autogroup as the token, no member carries it, and destroy records destroyed while the program's group runs" DestroyedSessionStopped
 write_run mutant-ReusedIdReadsGone pass WitnessWaitPassesReusedId "ReusedIdReadsGone=FALSE" "with a group that took the id read alive, no wait of destroy passes while that group runs"
 write_run mutant-ProvesHostPid violated NoUnrelatedHostKilled "ProvesHostPid=FALSE" "without the start-up record, destroy --force kills a process that took the host's pid" NoUnrelatedHostKilled
+write_run mutant-ReconcileRepairsMarked pass DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "redundant in the model: it has no crash of a reconciling process, so the repair after the reconcile's own write always runs"
 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

@@ -464,12 +464,36 @@ function repairFacts() {
     'src/storage/manifests.ts',
     'writeDestroyMarker',
   ).getText();
+  const reconcile = requireDeclaration(lifecycle, 'reconcileSession').body;
+  const marked = indexOfStatement(
+    reconcile,
+    /^if \(manifest !== null && isMarkedDestroyed\(sessionDirectory, manifest\)\) \{\s*if \(await writeMarkedDestroyed\(manifestFile, manifest\)\) \{\s*const socketFile = socketPath\(sessionDirectory\);\s*await unlinkIfPresent\(socketFile\);\s*await removeSocketDirectoryIfEmpty\(socketFile\);\s*\}\s*return;\s*\}$/,
+  );
+  const markedCheck = normalize(
+    requireDeclaration(lifecycle, 'isMarkedDestroyed').body.getText(),
+  );
+  const terminal = guardIndex(
+    reconcile,
+    'manifest === null || isTerminalSessionStatus(manifest.status)',
+    ts.SyntaxKind.ReturnStatement,
+  );
+  const rewrite = normalize(
+    requireDeclaration(lifecycle, 'writeMarkedDestroyed').body.getText(),
+  );
   return {
     ReconcileRepairsDestroyed:
       marks &&
       repairs &&
       marker.includes("await replaceFileAtomic(path, '')") &&
       !marker.includes('mkdir'),
+    ReconcileRepairsMarked:
+      marked >= 0 &&
+      marked < terminal &&
+      markedCheck ===
+        '{ return ( isTerminalSessionStatus(manifest.status) && !isDestroyedSessionStatus(manifest.status) && existsSync(destroyMarkerPath(sessionDirectory)) ); }' &&
+      rewrite.includes(
+        "await writeManifest(manifestFile, { ...rest, status: 'destroyed',",
+      ),
   };
 }
 
@@ -1318,6 +1342,8 @@ const COVERED = [
   ['src/host/lifecycle.ts', 'recordDestroyed'],
   ['src/host/lifecycle.ts', 'removeDeadHostSocket'],
   ['src/host/lifecycle.ts', 'destroySession'],
+  ['src/host/lifecycle.ts', 'isMarkedDestroyed'],
+  ['src/host/lifecycle.ts', 'writeMarkedDestroyed'],
   ['src/host/lifecycle.ts', 'reconcileSession'],
   ['src/host/hostMain.ts', 'waitForManifestFromCreate'],
   ['src/host/hostMain.ts', 'isSessionCommandable'],