Model actor-attributed terminal recovery

docs/protocol/Lazaret.cfg

@@ -54,6 +54,7 @@ CHECK_DEADLOCK FALSE
 
 INVARIANTS
     TypeOK
+    SessionTerminalPhysicalConsistency
     ConfigurationConfinement
     SandboxNamespaceIsolation
     OrderedNetworkStartup
@@ -104,3 +105,4 @@ PROPERTIES
     EmptyDomainEventuallyStops
     FailedDomainEventuallyRecovers
     LeaseLossUnmountRetainsPreparedLowerLease
+    PreIdentityExitEventuallyCleansAfterRuntimeAbsence

docs/protocol/Lazaret.tla

@@ -18,15 +18,16 @@ realized as Host Coordinator, Runtime Supervisor, and attached runsc; ordered
 resource preparation owned by the supervisor; Host Coordinator lifetime lease;
 role-separated runtime identity tuples; sandbox launch isolation; Client Session
 registration; host escalation; correlated result delivery; terminal ownership;
-failure; lease-driven teardown; recovery; and abstract durable generation-document
+durable Session Terminal and PTY lifecycle; failure; lease-driven teardown;
-intent with mismatch refuse.
+recovery; and abstract durable generation-document intent with mismatch refuse.
 
 Product names SessionCoordinatorPresent and Session Coordinator ID alias the
 multi-process presence predicates and generation-scoped genCoordinatorId.
 Durable participant intent is multi-role; networkReady gates publication;
 preparedLowerLeased and helperProc refine physical ownership under RS.
 Cryptographic algorithms, serialization, container commands, filesystems, typed
-redb tables, and network packet handling remain refinement boundaries.
+redb tables, PTY descriptor identities, process identifiers, signal mechanics,
+and network packet handling remain refinement boundaries.
 ***************************************************************************)
 
 CONSTANTS
@@ -136,6 +137,7 @@ SessionPhases == {
     "HostExecuting", "Closed", "Failed"
 }
 TerminalRoutes == {"Detached", "Sandbox", "Prompt", "HostProcess"}
+SessionTerminalStates == {"Clean", "Intent", "Running", "ReleaseIntent"}
 ConnectionStates == {"Disconnected", "Connected"}
 RequestPhases == {
     "Unused", "Verified", "AwaitingApproval", "Approved", "Executing",
@@ -273,9 +275,13 @@ VARIABLES
     genSandboxId,
     networkReady,
     preparedLowerLeased,
-    helperProc
+    helperProc,
+    sessionTerminalState,
+    sessionPtyOpen,
+    sessionExecPresent,
+    sessionGuestKnown
 
-vars == <<
+baseVars == <<
     domainPhase,
     stateAnchorState,
     sidecarState,
@@ -312,6 +318,15 @@ vars == <<
     helperProc
 >>
 
+terminalVars == <<
+    sessionTerminalState,
+    sessionPtyOpen,
+    sessionExecPresent,
+    sessionGuestKnown
+>>
+
+vars == <<baseVars, terminalVars>>
+
 Dom(s) == SessionDomain[s]
 ReqSession(r) == RequestSession[r]
 ReqDomain(r) == Dom(ReqSession(r))
@@ -381,6 +396,14 @@ RuntimeGenerationAbsent(d) ==
     /\ ~preparedLowerLeased[d]
     /\ ~networkReady[d]
 
+RuntimeAbsentForTerminal(d) ==
+    /\ sandboxState[d] = "Stopped"
+    /\ ~ProcessPresent(runtimeSupervisorProc[d])
+    /\ ~ProcessPresent(attachedRunscProc[d])
+
+SessionTerminalsClean(d) ==
+    \A s \in Sessions : Dom(s) = d => sessionTerminalState[s] = "Clean"
+
 ConsumeRuntimeFault(d) ==
     /\ runtimeFaultsRemaining[d] > 0
     /\ runtimeFaultsRemaining' =
@@ -493,6 +516,10 @@ Init ==
     /\ networkReady = [d \in Domains |-> FALSE]
     /\ preparedLowerLeased = [d \in Domains |-> FALSE]
     /\ helperProc = [d \in Domains |-> "Absent"]
+    /\ sessionTerminalState = [s \in Sessions |-> "Clean"]
+    /\ sessionPtyOpen = [s \in Sessions |-> FALSE]
+    /\ sessionExecPresent = [s \in Sessions |-> FALSE]
+    /\ sessionGuestKnown = [s \in Sessions |-> FALSE]
 
 (***************************************************************************
 Domain and Session lifecycle
@@ -852,6 +879,97 @@ DisconnectSession(s) ==
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
 
+(***************************************************************************
+Session Terminal and PTY lifecycle
+
+The model retains durable state plus abstract PTY, exec-client, and guest
+identity facts. Descriptor identities, PID reuse checks, and signal delivery
+remain physical refinements.
+***************************************************************************)
+
+BeginSessionTerminal(s) ==
+    LET d == Dom(s) IN
+    /\ sessionPhase[s] = "Attached"
+    /\ terminalRoute[s] = "Sandbox"
+    /\ RegistrationAdmissible(d)
+    /\ sessionTerminalState[s] = "Clean"
+    /\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Intent"]
+    /\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = TRUE]
+    /\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = TRUE]
+    /\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
+    /\ UNCHANGED baseVars
+
+CommitSessionTerminal(s) ==
+    /\ sessionPhase[s] = "Attached"
+    /\ terminalRoute[s] = "Sandbox"
+    /\ HostCoordinatorAlive(Dom(s))
+    /\ sessionTerminalState[s] = "Intent"
+    /\ sessionPtyOpen[s]
+    /\ sessionExecPresent[s]
+    /\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Running"]
+    /\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = TRUE]
+    /\ UNCHANGED <<baseVars, sessionPtyOpen, sessionExecPresent>>
+
+DisconnectCleanSession(s) ==
+    /\ sessionTerminalState[s] = "Clean"
+    /\ DisconnectSession(s)
+    /\ UNCHANGED terminalVars
+
+DisconnectLiveSessionTerminal(s) ==
+    /\ sessionTerminalState[s] \in {"Intent", "Running"}
+    /\ DisconnectSession(s)
+    /\ sessionTerminalState' =
+        [sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
+    /\ UNCHANGED <<sessionPtyOpen, sessionExecPresent, sessionGuestKnown>>
+
+CompleteSessionTerminal(s) ==
+    /\ sessionTerminalState[s] = "Running"
+    /\ DisconnectSession(s)
+    /\ sessionTerminalState' =
+        [sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
+    /\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
+    /\ UNCHANGED <<sessionPtyOpen, sessionGuestKnown>>
+
+ExitSessionTerminalBeforeGuestIdentity(s) ==
+    /\ sessionTerminalState[s] = "Intent"
+    /\ DisconnectSession(s)
+    /\ sessionTerminalState' =
+        [sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
+    /\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = FALSE]
+    /\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
+    /\ UNCHANGED sessionGuestKnown
+
+RetainFailedSessionTerminal(s) ==
+    /\ sessionPhase[s] = "Failed"
+    /\ sessionTerminalState[s] \in {"Intent", "Running"}
+    /\ sessionTerminalState' =
+        [sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
+    /\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = FALSE]
+    /\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
+    /\ UNCHANGED <<baseVars, sessionGuestKnown>>
+
+CleanKnownSessionTerminal(s) ==
+    /\ sessionPhase[s] \in {"Closed", "Failed"}
+    /\ sessionTerminalState[s] = "ReleaseIntent"
+    /\ sessionGuestKnown[s]
+    /\ HostCoordinatorAlive(Dom(s))
+    /\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Clean"]
+    /\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = FALSE]
+    /\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
+    /\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
+    /\ UNCHANGED baseVars
+
+BootstrapCleanSessionTerminalAfterRuntimeAbsence(s) ==
+    /\ sessionPhase[s] \in {"Closed", "Failed"}
+    /\ sessionTerminalState[s] = "ReleaseIntent"
+    /\ ~sessionPtyOpen[s]
+    /\ ~sessionExecPresent[s]
+    /\ RuntimeAbsentForTerminal(Dom(s))
+    /\ HostCoordinatorAlive(Dom(s))
+    /\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Clean"]
+    /\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
+    /\ UNCHANGED <<baseVars, sessionPtyOpen, sessionExecPresent>>
+
 BeginTeardown(d) ==
     /\ domainPhase[d] = "Ready"
     /\ HostCoordinatorAlive(d)
@@ -1970,6 +2088,17 @@ SessionProgress(s) ==
     \/ RejectConfigurationMismatch(s)
     \/ RegisterSession(s)
 
+SessionTerminalProgress(s) ==
+    \/ BeginSessionTerminal(s)
+    \/ CommitSessionTerminal(s)
+    \/ DisconnectCleanSession(s)
+    \/ DisconnectLiveSessionTerminal(s)
+    \/ CompleteSessionTerminal(s)
+    \/ ExitSessionTerminalBeforeGuestIdentity(s)
+    \/ RetainFailedSessionTerminal(s)
+    \/ CleanKnownSessionTerminal(s)
+    \/ BootstrapCleanSessionTerminalAfterRuntimeAbsence(s)
+
 RequestProgress(r) ==
     \/ AutoApprove(r)
     \/ QueuePrompt(r)
@@ -1983,12 +2112,12 @@ RequestProgress(r) ==
     \/ FailHostExecution(r)
     \/ DeliverResult(r)
 
-Next ==
+BaseNext ==
     \/ (\E s \in Sessions :
         StartNewDomain(s) \/ StartReadySession(s) \/ WaitForDomain(s) \/
         RestartWaitingDomain(s) \/ AdvanceWaitingSession(s) \/
         RejectConfigurationMismatch(s) \/
-        RegisterSession(s) \/ DisconnectSession(s))
+        RegisterSession(s))
     \/ (\E d \in Domains :
         DomainServiceProgress(d) \/ FailDomain(d))
     \/ (\E d \in Domains :
@@ -1996,14 +2125,23 @@ Next ==
     \/ (\E r \in Requests :
         ReceiveEscalation(r) \/ RequestProgress(r))
 
+Next ==
+    \/ /\ BaseNext
+       /\ UNCHANGED terminalVars
+    \/ (\E s \in Sessions : SessionTerminalProgress(s))
+
 \* Resume transitions are enabled but not weakly fair: permanent stop is a
 \* modeled stuck state for safety, not a guaranteed progress path.
 Spec ==
     /\ Init
     /\ [][Next]_vars
-    /\ \A d \in Domains : WF_vars(DomainServiceProgress(d))
+    /\ \A d \in Domains :
-    /\ \A s \in Sessions : WF_vars(SessionProgress(s))
+        WF_vars(DomainServiceProgress(d) /\ UNCHANGED terminalVars)
-    /\ \A r \in Requests : WF_vars(RequestProgress(r))
+    /\ \A s \in Sessions :
+        WF_vars(SessionProgress(s) /\ UNCHANGED terminalVars)
+    /\ \A s \in Sessions : WF_vars(SessionTerminalProgress(s))
+    /\ \A r \in Requests :
+        WF_vars(RequestProgress(r) /\ UNCHANGED terminalVars)
 
 (***************************************************************************
 Safety properties
@@ -2044,6 +2182,27 @@ TypeOK ==
     /\ preparedLowerLeased \in [Domains -> BOOLEAN]
     /\ helperProc \in [Domains -> HelperProcStates]
     /\ pathMismatch \in [Domains -> BOOLEAN]
+    /\ sessionTerminalState \in [Sessions -> SessionTerminalStates]
+    /\ sessionPtyOpen \in [Sessions -> BOOLEAN]
+    /\ sessionExecPresent \in [Sessions -> BOOLEAN]
+    /\ sessionGuestKnown \in [Sessions -> BOOLEAN]
+
+SessionTerminalPhysicalConsistency ==
+    \A s \in Sessions :
+        /\ (sessionTerminalState[s] = "Clean" =>
+            /\ ~sessionPtyOpen[s]
+            /\ ~sessionExecPresent[s]
+            /\ ~sessionGuestKnown[s])
+        /\ (sessionTerminalState[s] = "Intent" =>
+            /\ sessionPtyOpen[s]
+            /\ sessionExecPresent[s]
+            /\ ~sessionGuestKnown[s])
+        /\ (sessionTerminalState[s] = "Running" =>
+            /\ sessionPtyOpen[s]
+            /\ sessionExecPresent[s]
+            /\ sessionGuestKnown[s])
+        /\ (sessionPtyOpen[s] => sessionTerminalState[s] # "Clean")
+        /\ (sessionExecPresent[s] => sessionTerminalState[s] # "Clean")
 
 ConfigurationConfinement ==
     \A d \in Domains : domainPhase[d] # "Absent" => ConfigSafe[d]
@@ -2353,6 +2512,7 @@ NetworkReadinessBoundToSandbox ==
 
 Safety ==
     /\ TypeOK
+    /\ SessionTerminalPhysicalConsistency
     /\ ConfigurationConfinement
     /\ SandboxNamespaceIsolation
     /\ OrderedNetworkStartup
@@ -2429,4 +2589,15 @@ FailedDomainEventuallyRecovers ==
             \/ domainPhase[d] = "Absent"
             \/ <>[](hostCoordinatorProc[d] = "Stopped")
 
+PreIdentityExitEventuallyCleansAfterRuntimeAbsence ==
+    \A s \in Sessions :
+        /\ sessionPhase[s] = "Closed"
+        /\ sessionTerminalState[s] = "ReleaseIntent"
+        /\ ~sessionGuestKnown[s]
+        /\ ~sessionPtyOpen[s]
+        /\ ~sessionExecPresent[s]
+        /\ RuntimeAbsentForTerminal(Dom(s))
+        ~> \/ sessionTerminalState[s] = "Clean"
+           \/ <>[](~HostCoordinatorAlive(Dom(s)))
+
 =============================================================================

docs/specification.md

@@ -390,9 +390,10 @@ publication, escalation, generation-scoped identities, durable intent, network
 readiness, prepared-lower lease, and connectivity-helper ownership—is defined by
 the [TLA+ application protocol model](protocol/Lazaret.tla). Product
 implementation refines that model with physical resources (prepared-lower trees,
-mounts, `slirp4netns`, PTYs, runsc clients, durable store encoding, and exact
+mounts, `slirp4netns`, PTY descriptors and attachment, runsc clients, durable
-ownership records). Physical recovery enumerates and inspects those resources
+store encoding, and exact ownership records). Durable Session Terminal state and
-independently of process liveness.
+recovery progress remain in the application model. Physical recovery enumerates
+and inspects those resources independently of process liveness.
 
 #### Host process identity and causal acquisition refinement