fix(host): record the host at create, read a token without host.json as unshared, freeze again

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

@@ -5,7 +5,7 @@
     "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6",
     "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522",
     "src/cli/commands/gc.ts#gcSessions": "667e4ebc3ca3029c",
-    "src/host/lifecycle.ts#allocateSession": "77dab09b34fedce5",
+    "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec",
     "src/host/lifecycle.ts#launchHost": "597a5a6b9eb58cc8",
     "src/host/lifecycle.ts#isProcessAlive": "1ca1fe6ad6c41711",
     "src/host/lifecycle.ts#killProcessBestEffort": "1dd0cb4ee9bbc676",
@@ -19,12 +19,12 @@
     "src/host/hostRecord.ts#readHostRecord": "6e0fc70b53f945bc",
     "src/host/hostRecord.ts#pidExists": "d539275a0f6041ea",
     "src/host/hostRecord.ts#judgeHost": "85b37d524df156a4",
-    "src/host/hostRecord.ts#inPidNamespace": "4f4858fadf4acf81",
+    "src/host/hostRecord.ts#inPidNamespace": "aaa5cdfdfbb99f33",
     "src/host/hostRecord.ts#readTimeNamespace": "cd26abbdf639f1b8",
     "src/host/hostRecord.ts#inTimeNamespace": "3aa522616ace5b7a",
     "src/host/hostRecord.ts#readMachineId": "0873b5375df35f8f",
     "src/host/hostRecord.ts#inHostPidSpace": "66124bf9c4e33e0b",
-    "src/host/hostRecord.ts#sharesHostPids": "7669f6af0754088d",
+    "src/host/hostRecord.ts#sharesHostPids": "0c2a1fd9532efab5",
     "src/host/lifecycle.ts#ownLinuxSessionId": "e5f4eb175dab90da",
     "src/host/lifecycle.ts#ownProcessGroupId": "b480c93782250b9a",
     "src/host/lifecycle.ts#controllingTerminal": "d7c4b308f169a1fe",
@@ -54,11 +54,11 @@
     "src/host/programGroup.ts#readAutogroup": "2023ceccd585dcd8",
     "src/host/programGroup.ts#readBootId": "ceccda3fef7163f2",
     "src/host/programGroup.ts#captureToken": "4e948dddc8d0dba9",
-    "src/host/programGroup.ts#captureProgram": "f07d6160f3f22aed",
+    "src/host/programGroup.ts#captureProgram": "a8efb46d449ad2e6",
     "src/host/programGroup.ts#writeProgramRecord": "1845322710155185",
     "src/host/programGroup.ts#readProgramRecord": "b02c48c2bff248a7",
-    "src/host/programGroup.ts#readProvenProgramGroup": "a81172c2ed27f450",
-    "src/host/programGroup.ts#readProgramGroup": "ec7a4a291705bcbc",
+    "src/host/programGroup.ts#readProvenProgramGroup": "79abfacfdeb33135",
+    "src/host/programGroup.ts#readProgramGroup": "c783266ad349892e",
     "src/host/programGroup.ts#judgeProgramGroup": "b8b3053a25f95bbf",
     "src/host/programGroup.ts#readGroupMembers": "8f8103d1d5186e91",
     "src/host/programGroup.ts#judgeLiveGroup": "29c9c4bfd01c4338",
@@ -70,7 +70,8 @@
     "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b",
     "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1",
     "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82",
-    "src/host/programGroup.ts#stopProgramGroup": "b6cfc91dd3027346",
+    "src/host/programGroup.ts#stopProgramGroup": "2a512f574e7bd5ae",
+    "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328",
     "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd",
     "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9",
     "src/host/sessionState.ts#SessionState.requestDestroy": "f66074e815527ff1",
@@ -86,13 +87,13 @@
     "src/storage/manifests.ts#writeManifest": "1bcc99f09acfc577",
     "src/storage/manifests.ts#writeDestroyMarker": "7387a50b983a97c6",
     "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d",
-    "src/host/hostMain.ts#runHost(parts)": "10d2a8569f3b263e",
+    "src/host/hostMain.ts#runHost(parts)": "37e8ce5dc771d29c",
     "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": "f7270faba013acff",
-    "skill:scripts/facts.mjs": "82adfcc9fbc7fbb7",
-    "skill:scripts/check.sh": "3a47553300cb217a"
+    "skill:model/SessionLifecycle.tla": "7986bb289034aa6c",
+    "skill:scripts/facts.mjs": "ea6bebdccb255054",
+    "skill:scripts/check.sh": "66a765237f244773"
   },
   "callSites": {
     "writeManifest": [

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

@@ -103,6 +103,9 @@ CONSTANTS
     ReusedIdReadsGone,      \* programGroup.ts: isProgramGroupAlive reads a
                             \*   group gone when its live members carry
                             \*   another autogroup (unproven)
+    CreateRecordsHost,      \* lifecycle.ts: allocateSession writes host.json
+                            \*   for the launched host before the first
+                            \*   manifest
     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
@@ -144,7 +147,7 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal,
                  FallbackNeedsFolder, CreateStopsOnGiveUp,
                  ReconcileRepairsDestroyed, ReconcileRepairsMarked,
                  TokenNamesProgram,
-                 ReusedIdReadsGone, ProvesHostPid,
+                 ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost,
                  FreezesUnseenGroup, UnsharedGroupReadsUnknown} : b \in BOOLEAN
 
 Readers == {"gc", "list"}   \* the two processes that run reconcileSession
@@ -386,8 +389,8 @@ GroupSeen(kind) ==
 \* sharesHostPids reads host.json. With UnsharedGroupReadsUnknown,
 \* readProgramGroup and readProvenProgramGroup give a group with a token
 \* that reads alive instead, so their waits time out. The host always runs
-\* in its own pid space, so it keeps GroupSeen and HostKill. OtherPidSpace
-\* leaves the CLI's view of the host as it is (see Scope).
+\* in its own pid space, so it keeps GroupSeen and HostKill. CliHostAlive
+\* gives the CLI's view of the host.
 CliGroupSeen(kind) ==
     IF OtherPidSpace
     THEN kind = "proven" /\ UnsharedGroupReadsUnknown
@@ -439,14 +442,21 @@ CreateWritesManifest ==
     /\ UNCHANGED <<ghostVars, sock, hostVars, shutVars, readerVars,
                    destroyVars, groupVars>>
 
-\* launchHost spawns the detached `_host` process.
+\* launchHost spawns the detached `_host` process. With CreateRecordsHost,
+\* captureHost reads the new host in the same synchronous block, and
+\* writeHostRecord writes host.json, which fails once gc removed the folder.
+\* The model leaves out a capture that fails (no /proc, or off Linux), after
+\* which only the host writes the record.
 CreateLaunchesHost ==
     /\ cpc = "launch"
     /\ hostAlive' = TRUE
     /\ hpc' = "boot"
     /\ cpc' = IF CreateRecordsHostPid THEN "write" ELSE "done"
+    /\ hrec' = (CreateRecordsHost /\ dir)
     /\ UNCHANGED <<diskVars, ghostVars, sock, hex, rsz, prog, foreign, left,
-                   shutVars, readerVars, destroyVars, groupVars>>
+                   shutVars, readerVars, destroyVars, rec, reused,
+                   hitUnrelated, diedUnrecorded, passedReused, hreused,
+                   hitUnrelatedHost>>
 
 \* runCreateCommand's readiness loop gives up after 50 inspect RPCs that
 \* fail, which the model lets happen at any step after the start-up, since
@@ -815,9 +825,15 @@ HostPidReused ==
 
 AfterReconcile(p) == IF p = "gc" THEN "readafter" ELSE "idle"
 
+\* isHostAlive as destroy, list and gc see it. In another pid space,
+\* judgeHost reads a host that host.json names as unknown, which reads alive
+\* also after the host ended. Before host.json exists it probes the pid in
+\* its own pid space, where no process has it, and reads the host dead.
+CliHostAlive == IF OtherPidSpace THEN hrec ELSE hostAlive
+
 \* `if (manifest.hostPid !== null && hostAlive) return`, where hostAlive is
-\* isProcessAlive(manifest.hostPid). A null hostPid reads as a dead host.
-SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ hostAlive
+\* isHostAlive(manifest.hostPid). A null hostPid reads as a dead host.
+SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ CliHostAlive
 
 \* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest
 \* other than destroyed next to the destroy marker (isMarkedDestroyed) goes
@@ -1018,7 +1034,7 @@ GcFinalRead ==
     /\ pc["gc"] = "final"
     /\ IF GcFinalCheck /\ mst # "none" /\ mst \notin Collectable
           THEN GcSkips
-          ELSE GcGoesTo(IF mpid /\ hostAlive THEN "rm" ELSE "rmsock")
+          ELSE GcGoesTo(IF mpid /\ CliHostAlive THEN "rm" ELSE "rmsock")
     /\ UNCHANGED <<diskVars, ghostVars, sock, cpc, hostVars, shutVars, rd,
                    lruns, destroyVars, groupVars>>
 
@@ -1138,7 +1154,7 @@ DestroyReads ==
           THEN /\ dpc' = "kill" /\ drd' = ReadCopy
                /\ UNCHANGED <<dres, dsaw>>
           ELSE /\ dpc' = "rpc" /\ UNCHANGED <<drd, dres, dsaw>>
-    /\ sock' = (sock /\ (mst # "destroyed" \/ (mpid /\ hostAlive)))
+    /\ sock' = (sock /\ (mst # "destroyed" \/ (mpid /\ CliHostAlive)))
     /\ UNCHANGED <<diskVars, ghostVars, cpc, hostVars, shutVars,
                    readerVars, dforce, dinside, dkill, groupVars>>
 
@@ -1197,9 +1213,10 @@ DestroyUnlinksSocket ==
 \* ProvesHostPid it kills only a host that hostMatches proves: the live host
 \* once host.json names it, never a process that took its pid. Without it,
 \* the kill reaches whatever has the pid. The copy that destroy read after
-\* the first kill names the same host.
+\* the first kill names the same host. In another pid space, hostMatches
+\* never proves the host, so nothing gets the kill.
 KillsHost ==
-    IF dpc \in {"kill", "rkill"} /\ drd.pid /\ hostAlive
+    IF dpc \in {"kill", "rkill"} /\ drd.pid /\ hostAlive /\ ~OtherPidSpace
           /\ (hrec \/ ~ProvesHostPid)
     THEN /\ HostDies /\ dkill' = TRUE /\ UNCHANGED hitUnrelatedHost
     ELSE IF dpc \in {"kill", "rkill"} /\ drd.pid /\ hreused /\ ~ProvesHostPid
@@ -1237,7 +1254,7 @@ DestroyPollsGroup ==
     /\ DestroyAt({"kwait", "rwait", "twait"})
     /\ passedReused' = (passedReused \/
                          (reused /\ drd.grp = "proven" /\ ~CliGroupSeen(drd.grp)))
-    /\ IF CliGroupSeen(drd.grp) \/ (dpc # "twait" /\ drd.pid /\ hostAlive)
+    /\ IF CliGroupSeen(drd.grp) \/ (dpc # "twait" /\ drd.pid /\ CliHostAlive)
           THEN DestroyEnds("error")
           ELSE IF dpc = "kwait"
           THEN /\ dpc' = IF DestroyRecordsDestroyed THEN "reread" ELSE "final"

.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 ReconcileRepairsMarked 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 CreateRecordsHost 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 WitnessMarkedRepaired 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"
 
 # --- 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 witness-WitnessUnrecordedHostMeetsKill violated WitnessUnrecordedHostMeetsKill "CreateRecordsHost=FALSE" "without a record from create, as when its capture fails, a kill meets a host that host.json does not name yet"
 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"
@@ -229,6 +230,7 @@ OTHER=TRUE
 write_run current-otherspace pass "$RULES" "" "the code with destroy, list and gc in another pid space: every rule holds"
 write_run witness-WitnessUnsharedDestroyCompletes-otherspace violated WitnessUnsharedDestroyCompletes "" "a plain destroy from another pid space still succeeds"
 write_run mutant-UnsharedGroupReadsUnknown-otherspace violated DestroyedSessionStopped "UnsharedGroupReadsUnknown=FALSE" "with the group read gone where no scan or probe shows it, destroy of an exited session records destroyed while a process it left runs" DestroyedSessionStopped
+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
 
 # Without a token every kill falls back to the id that a manifest or the