docs: reorganize specification and model application protocol

docs/protocol/Lazaret.tla

@@ -0,0 +1,805 @@
+------------------------------ MODULE Lazaret ------------------------------
+EXTENDS Naturals, FiniteSets, Sequences, TLC
+
+(***************************************************************************
+Application-wide protocol model for Lazaret.
+
+The model covers Domain startup, ordered resource preparation, Client Session
+registration, host escalation, terminal ownership, failure, and teardown.
+Cryptographic algorithms, serialization, container commands, filesystems, and
+network packet handling are refinement boundaries validated by implementation
+tests rather than modeled internally.
+***************************************************************************)
+
+CONSTANTS
+    Domains,
+    Sessions,
+    Requests,
+    Commands,
+    NoSession,
+    NoRequest,
+    NoCommand,
+    NoApproval,
+    SessionDomain,
+    SessionFingerprint,
+    DomainFingerprint,
+    ConfigSafe,
+    RequestSession,
+    RequestCommand,
+    CertificateValid,
+    SignatureValid,
+    AutoRuleMatches,
+    CommandRequiresShell,
+    D1,
+    S1,
+    S2,
+    R1,
+    R2,
+    R3,
+    ExactCmd,
+    PromptCmd,
+    ShellCmd,
+    EditedCmd
+
+ASSUME
+    /\ IsFiniteSet(Domains)
+    /\ IsFiniteSet(Sessions)
+    /\ IsFiniteSet(Requests)
+    /\ IsFiniteSet(Commands)
+    /\ Domains # {}
+    /\ Sessions # {}
+    /\ Requests # {}
+    /\ NoSession \notin Sessions
+    /\ NoRequest \notin Requests
+    /\ NoCommand \notin Commands
+    /\ SessionDomain \in [Sessions -> Domains]
+    /\ SessionFingerprint \in [Sessions -> STRING]
+    /\ DomainFingerprint \in [Domains -> STRING]
+    /\ ConfigSafe \in [Domains -> BOOLEAN]
+    /\ RequestSession \in [Requests -> Sessions]
+    /\ RequestCommand \in [Requests -> Commands]
+    /\ CertificateValid \in [Requests -> BOOLEAN]
+    /\ SignatureValid \in [Requests -> BOOLEAN]
+    /\ AutoRuleMatches \in [Requests -> BOOLEAN]
+    /\ CommandRequiresShell \in [Commands -> BOOLEAN]
+
+DomainPhases == {"Absent", "Starting", "Ready", "Stopping", "Failed"}
+CoordinatorStates == {"Absent", "Starting", "Ready", "Stopping", "Failed"}
+MountStates == {"Unmounted", "Mounted"}
+ResourceStates == {"Stopped", "Ready", "Failed"}
+SessionPhases == {
+    "New", "Waiting", "Registering", "Attached", "Prompting",
+    "HostExecuting", "Closed", "Failed"
+}
+TerminalRoutes == {"Detached", "Sandbox", "Prompt", "HostProcess"}
+ConnectionStates == {"Disconnected", "Connected"}
+RequestPhases == {
+    "Unused", "Verified", "AwaitingApproval", "Approved", "Executing",
+    "Completed", "Denied", "TimedOut", "Cancelled", "Failed"
+}
+ApprovalSources == {NoApproval, "AutoRule", "Developer"}
+TerminalRequestPhases == {"Completed", "Denied", "TimedOut", "Cancelled", "Failed"}
+
+(***************************************************************************
+Finite fixture operators used by Lazaret.cfg. The protocol itself depends only
+on the abstract constants above; other TLC configurations may override them with
+different finite operators.
+***************************************************************************)
+
+DomainsFixture == {D1}
+SessionsFixture == {S1, S2}
+RequestsFixture == {R1, R2, R3}
+CommandsFixture == {ExactCmd, PromptCmd, ShellCmd, EditedCmd}
+
+SessionDomainFixture == (S1 :> D1) @@ (S2 :> D1)
+SessionFingerprintFixture ==
+    (S1 :> "config-a") @@ (S2 :> "config-a")
+DomainFingerprintFixture == D1 :> "config-a"
+ConfigSafeFixture == D1 :> TRUE
+RequestSessionFixture ==
+    (R1 :> S1) @@ (R2 :> S2) @@ (R3 :> S1)
+RequestCommandFixture ==
+    (R1 :> ExactCmd) @@ (R2 :> PromptCmd) @@ (R3 :> ShellCmd)
+CertificateValidFixture ==
+    (R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> FALSE)
+SignatureValidFixture ==
+    (R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> FALSE)
+AutoRuleMatchesFixture ==
+    (R1 :> TRUE) @@ (R2 :> FALSE) @@ (R3 :> TRUE)
+CommandRequiresShellFixture ==
+    (ExactCmd :> FALSE) @@
+    (PromptCmd :> FALSE) @@
+    (ShellCmd :> TRUE) @@
+    (EditedCmd :> FALSE)
+
+VARIABLES
+    domainPhase,
+    coordinatorState,
+    stateAnchorState,
+    sidecarState,
+    sandboxState,
+    trustReady,
+    lockOwner,
+    published,
+    registered,
+    connected,
+    sessionPhase,
+    terminalRoute,
+    connectionState,
+    activeRequest,
+    requestPhase,
+    approvalSource,
+    approvedCommand,
+    hostRunning
+
+vars == <<
+    domainPhase,
+    coordinatorState,
+    stateAnchorState,
+    sidecarState,
+    sandboxState,
+    trustReady,
+    lockOwner,
+    published,
+    registered,
+    connected,
+    sessionPhase,
+    terminalRoute,
+    connectionState,
+    activeRequest,
+    requestPhase,
+    approvalSource,
+    approvedCommand,
+    hostRunning
+>>
+
+Dom(s) == SessionDomain[s]
+ReqSession(r) == RequestSession[r]
+ReqDomain(r) == Dom(ReqSession(r))
+IsTerminalRequest(r) == requestPhase[r] \in TerminalRequestPhases
+
+Interested(d) == {
+    s \in Sessions :
+        Dom(s) = d /\
+        sessionPhase[s] \in {
+            "Waiting", "Registering", "Attached", "Prompting", "HostExecuting"
+        }
+}
+
+RequestsForDomain(d) == {r \in Requests : ReqDomain(r) = d}
+
+Init ==
+    /\ domainPhase = [d \in Domains |-> "Absent"]
+    /\ coordinatorState = [d \in Domains |-> "Absent"]
+    /\ stateAnchorState = [d \in Domains |-> "Unmounted"]
+    /\ sidecarState = [d \in Domains |-> "Stopped"]
+    /\ sandboxState = [d \in Domains |-> "Stopped"]
+    /\ trustReady = [d \in Domains |-> FALSE]
+    /\ lockOwner = [d \in Domains |-> NoSession]
+    /\ published = {}
+    /\ registered = [d \in Domains |-> {}]
+    /\ connected = [d \in Domains |-> {}]
+    /\ sessionPhase = [s \in Sessions |-> "New"]
+    /\ terminalRoute = [s \in Sessions |-> "Detached"]
+    /\ connectionState = [s \in Sessions |-> "Disconnected"]
+    /\ activeRequest = [s \in Sessions |-> NoRequest]
+    /\ requestPhase = [r \in Requests |-> "Unused"]
+    /\ approvalSource = [r \in Requests |-> NoApproval]
+    /\ approvedCommand = [r \in Requests |-> NoCommand]
+    /\ hostRunning = {}
+
+(***************************************************************************
+Domain and Session lifecycle
+***************************************************************************)
+
+StartNewDomain(s) ==
+    LET d == Dom(s) IN
+    /\ sessionPhase[s] = "New"
+    /\ ConfigSafe[d]
+    /\ domainPhase[d] = "Absent"
+    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Starting"]
+    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Starting"]
+    /\ lockOwner' = [lockOwner EXCEPT ![d] = s]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Waiting"]
+    /\ UNCHANGED <<
+        stateAnchorState, sidecarState, sandboxState, trustReady, published,
+        registered, connected, terminalRoute, connectionState, activeRequest,
+        requestPhase, approvalSource, approvedCommand, hostRunning
+        >>
+
+StartReadySession(s) ==
+    LET d == Dom(s) IN
+    /\ sessionPhase[s] = "New"
+    /\ domainPhase[d] = "Ready"
+    /\ SessionFingerprint[s] = DomainFingerprint[d]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Registering"]
+    /\ connectionState' = [connectionState EXCEPT ![s] = "Connected"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        terminalRoute, activeRequest, requestPhase, approvalSource,
+        approvedCommand, hostRunning
+        >>
+
+WaitForDomain(s) ==
+    LET d == Dom(s) IN
+    /\ sessionPhase[s] = "New"
+    /\ domainPhase[d] \in {"Starting", "Stopping"}
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Waiting"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        terminalRoute, connectionState, activeRequest, requestPhase,
+        approvalSource, approvedCommand, hostRunning
+        >>
+
+RestartWaitingDomain(s) ==
+    LET d == Dom(s) IN
+    /\ sessionPhase[s] = "Waiting"
+    /\ ConfigSafe[d]
+    /\ domainPhase[d] = "Absent"
+    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Starting"]
+    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Starting"]
+    /\ lockOwner' = [lockOwner EXCEPT ![d] = s]
+    /\ UNCHANGED <<
+        stateAnchorState, sidecarState, sandboxState, trustReady, published,
+        registered, connected, sessionPhase, terminalRoute, connectionState,
+        activeRequest, requestPhase, approvalSource, approvedCommand,
+        hostRunning
+        >>
+
+MountStateAnchor(d) ==
+    /\ domainPhase[d] = "Starting"
+    /\ coordinatorState[d] = "Starting"
+    /\ stateAnchorState[d] = "Unmounted"
+    /\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Mounted"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, sidecarState, sandboxState, trustReady,
+        lockOwner, published, registered, connected, sessionPhase,
+        terminalRoute, connectionState, activeRequest, requestPhase,
+        approvalSource, approvedCommand, hostRunning
+        >>
+
+CreateTrustAnchor(d) ==
+    /\ domainPhase[d] = "Starting"
+    /\ coordinatorState[d] = "Starting"
+    /\ ~trustReady[d]
+    /\ trustReady' = [trustReady EXCEPT ![d] = TRUE]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, lockOwner, published, registered, connected,
+        sessionPhase, terminalRoute, connectionState, activeRequest,
+        requestPhase, approvalSource, approvedCommand, hostRunning
+        >>
+
+StartSidecar(d) ==
+    /\ domainPhase[d] = "Starting"
+    /\ stateAnchorState[d] = "Mounted"
+    /\ trustReady[d]
+    /\ sidecarState[d] = "Stopped"
+    /\ sidecarState' = [sidecarState EXCEPT ![d] = "Ready"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sandboxState,
+        trustReady, lockOwner, published, registered, connected, sessionPhase,
+        terminalRoute, connectionState, activeRequest, requestPhase,
+        approvalSource, approvedCommand, hostRunning
+        >>
+
+StartSandbox(d) ==
+    /\ domainPhase[d] = "Starting"
+    /\ sidecarState[d] = "Ready"
+    /\ sandboxState[d] = "Stopped"
+    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Ready"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        trustReady, lockOwner, published, registered, connected, sessionPhase,
+        terminalRoute, connectionState, activeRequest, requestPhase,
+        approvalSource, approvedCommand, hostRunning
+        >>
+
+PublishDomain(d) ==
+    /\ domainPhase[d] = "Starting"
+    /\ coordinatorState[d] = "Starting"
+    /\ stateAnchorState[d] = "Mounted"
+    /\ sidecarState[d] = "Ready"
+    /\ sandboxState[d] = "Ready"
+    /\ trustReady[d]
+    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Ready"]
+    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Ready"]
+    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
+    /\ published' = published \cup {d}
+    /\ UNCHANGED <<
+        stateAnchorState, sidecarState, sandboxState, trustReady, registered,
+        connected, sessionPhase, terminalRoute, connectionState,
+        activeRequest, requestPhase, approvalSource, approvedCommand,
+        hostRunning
+        >>
+
+AdvanceWaitingSession(s) ==
+    LET d == Dom(s) IN
+    /\ sessionPhase[s] = "Waiting"
+    /\ domainPhase[d] = "Ready"
+    /\ SessionFingerprint[s] = DomainFingerprint[d]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Registering"]
+    /\ connectionState' = [connectionState EXCEPT ![s] = "Connected"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        terminalRoute, activeRequest, requestPhase, approvalSource,
+        approvedCommand, hostRunning
+        >>
+
+RejectConfigurationMismatch(s) ==
+    LET d == Dom(s) IN
+    /\ sessionPhase[s] \in {"New", "Waiting"}
+    /\ domainPhase[d] = "Ready"
+    /\ SessionFingerprint[s] # DomainFingerprint[d]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Failed"]
+    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Detached"]
+    /\ connectionState' = [connectionState EXCEPT ![s] = "Disconnected"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        activeRequest, requestPhase, approvalSource, approvedCommand,
+        hostRunning
+        >>
+
+RegisterSession(s) ==
+    LET d == Dom(s) IN
+    /\ sessionPhase[s] = "Registering"
+    /\ connectionState[s] = "Connected"
+    /\ domainPhase[d] = "Ready"
+    /\ SessionFingerprint[s] = DomainFingerprint[d]
+    /\ registered' = [registered EXCEPT ![d] = @ \cup {s}]
+    /\ connected' = [connected EXCEPT ![d] = @ \cup {s}]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
+    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, connectionState,
+        activeRequest, requestPhase, approvalSource, approvedCommand,
+        hostRunning
+        >>
+
+DisconnectSession(s) ==
+    LET d == Dom(s)
+        r == activeRequest[s]
+    IN
+    /\ sessionPhase[s] \in {
+        "Waiting", "Registering", "Attached", "Prompting", "HostExecuting"
+        }
+    /\ registered' = [registered EXCEPT ![d] = @ \ {s}]
+    /\ connected' = [connected EXCEPT ![d] = @ \ {s}]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Closed"]
+    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Detached"]
+    /\ connectionState' = [connectionState EXCEPT ![s] = "Disconnected"]
+    /\ activeRequest' = [activeRequest EXCEPT ![s] = NoRequest]
+    /\ requestPhase' = [q \in Requests |->
+        IF r # NoRequest /\ q = r /\ ~IsTerminalRequest(q)
+        THEN "Cancelled"
+        ELSE requestPhase[q]]
+    /\ hostRunning' = IF r = NoRequest THEN hostRunning ELSE hostRunning \ {r}
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, approvalSource,
+        approvedCommand
+        >>
+
+BeginTeardown(d) ==
+    /\ domainPhase[d] = "Ready"
+    /\ Interested(d) = {}
+    /\ registered[d] = {}
+    /\ connected[d] = {}
+    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Stopping"]
+    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Stopping"]
+    /\ published' = published \ {d}
+    /\ UNCHANGED <<
+        stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
+        registered, connected, sessionPhase, terminalRoute, connectionState,
+        activeRequest, requestPhase, approvalSource, approvedCommand,
+        hostRunning
+        >>
+
+StopSandbox(d) ==
+    /\ domainPhase[d] = "Stopping"
+    /\ sandboxState[d] = "Ready"
+    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        trustReady, lockOwner, published, registered, connected, sessionPhase,
+        terminalRoute, connectionState, activeRequest, requestPhase,
+        approvalSource, approvedCommand, hostRunning
+        >>
+
+StopSidecar(d) ==
+    /\ domainPhase[d] = "Stopping"
+    /\ sandboxState[d] = "Stopped"
+    /\ sidecarState[d] = "Ready"
+    /\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sandboxState,
+        trustReady, lockOwner, published, registered, connected, sessionPhase,
+        terminalRoute, connectionState, activeRequest, requestPhase,
+        approvalSource, approvedCommand, hostRunning
+        >>
+
+UnmountStateAnchor(d) ==
+    /\ domainPhase[d] = "Stopping"
+    /\ sandboxState[d] = "Stopped"
+    /\ sidecarState[d] = "Stopped"
+    /\ stateAnchorState[d] = "Mounted"
+    /\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, sidecarState, sandboxState, trustReady,
+        lockOwner, published, registered, connected, sessionPhase,
+        terminalRoute, connectionState, activeRequest, requestPhase,
+        approvalSource, approvedCommand, hostRunning
+        >>
+
+FinishTeardown(d) ==
+    /\ domainPhase[d] = "Stopping"
+    /\ stateAnchorState[d] = "Unmounted"
+    /\ sidecarState[d] = "Stopped"
+    /\ sandboxState[d] = "Stopped"
+    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Absent"]
+    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
+    /\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
+    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
+    /\ UNCHANGED <<
+        stateAnchorState, sidecarState, sandboxState, published, registered,
+        connected, sessionPhase, terminalRoute, connectionState,
+        activeRequest, requestPhase, approvalSource, approvedCommand,
+        hostRunning
+        >>
+
+(***************************************************************************
+Host escalation protocol
+***************************************************************************)
+
+ReceiveEscalation(r) ==
+    LET s == ReqSession(r)
+        d == ReqDomain(r)
+    IN
+    /\ requestPhase[r] = "Unused"
+    /\ sessionPhase[s] = "Attached"
+    /\ activeRequest[s] = NoRequest
+    /\ s \in registered[d]
+    /\ s \in connected[d]
+    /\ CertificateValid[r]
+    /\ SignatureValid[r]
+    /\ requestPhase' = [requestPhase EXCEPT ![r] = "Verified"]
+    /\ activeRequest' = [activeRequest EXCEPT ![s] = r]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        sessionPhase, terminalRoute, connectionState, approvalSource,
+        approvedCommand, hostRunning
+        >>
+
+AutoApprove(r) ==
+    /\ requestPhase[r] = "Verified"
+    /\ AutoRuleMatches[r]
+    /\ ~CommandRequiresShell[RequestCommand[r]]
+    /\ requestPhase' = [requestPhase EXCEPT ![r] = "Approved"]
+    /\ approvalSource' = [approvalSource EXCEPT ![r] = "AutoRule"]
+    /\ approvedCommand' = [approvedCommand EXCEPT ![r] = RequestCommand[r]]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        sessionPhase, terminalRoute, connectionState, activeRequest, hostRunning
+        >>
+
+QueuePrompt(r) ==
+    /\ requestPhase[r] = "Verified"
+    /\ ~(AutoRuleMatches[r] /\ ~CommandRequiresShell[RequestCommand[r]])
+    /\ requestPhase' = [requestPhase EXCEPT ![r] = "AwaitingApproval"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        sessionPhase, terminalRoute, connectionState, activeRequest,
+        approvalSource, approvedCommand, hostRunning
+        >>
+
+BeginPrompt(r) ==
+    LET s == ReqSession(r) IN
+    /\ requestPhase[r] = "AwaitingApproval"
+    /\ sessionPhase[s] = "Attached"
+    /\ activeRequest[s] = r
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Prompting"]
+    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Prompt"]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        connectionState, activeRequest, requestPhase, approvalSource,
+        approvedCommand, hostRunning
+        >>
+
+DeveloperApprove(r, cmd) ==
+    LET s == ReqSession(r) IN
+    /\ requestPhase[r] = "AwaitingApproval"
+    /\ sessionPhase[s] = "Prompting"
+    /\ cmd \in Commands
+    /\ requestPhase' = [requestPhase EXCEPT ![r] = "Approved"]
+    /\ approvalSource' = [approvalSource EXCEPT ![r] = "Developer"]
+    /\ approvedCommand' = [approvedCommand EXCEPT ![r] = cmd]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        sessionPhase, terminalRoute, connectionState, activeRequest, hostRunning
+        >>
+
+DeveloperDeny(r) ==
+    LET s == ReqSession(r) IN
+    /\ requestPhase[r] = "AwaitingApproval"
+    /\ sessionPhase[s] = "Prompting"
+    /\ requestPhase' = [requestPhase EXCEPT ![r] = "Denied"]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
+    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
+    /\ activeRequest' = [activeRequest EXCEPT ![s] = NoRequest]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        connectionState, approvalSource, approvedCommand, hostRunning
+        >>
+
+StartHostExecution(r) ==
+    LET s == ReqSession(r)
+        d == ReqDomain(r)
+    IN
+    /\ requestPhase[r] = "Approved"
+    /\ activeRequest[s] = r
+    /\ s \in connected[d]
+    /\ sessionPhase[s] \in {"Attached", "Prompting"}
+    /\ requestPhase' = [requestPhase EXCEPT ![r] = "Executing"]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "HostExecuting"]
+    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "HostProcess"]
+    /\ hostRunning' = hostRunning \cup {r}
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        connectionState, activeRequest, approvalSource, approvedCommand
+        >>
+
+CompleteHostExecution(r) ==
+    LET s == ReqSession(r) IN
+    /\ requestPhase[r] = "Executing"
+    /\ r \in hostRunning
+    /\ requestPhase' = [requestPhase EXCEPT ![r] = "Completed"]
+    /\ hostRunning' = hostRunning \ {r}
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
+    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
+    /\ activeRequest' = [activeRequest EXCEPT ![s] = NoRequest]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        connectionState, approvalSource, approvedCommand
+        >>
+
+TimeoutRequest(r) ==
+    LET s == ReqSession(r) IN
+    /\ requestPhase[r] \in {"Verified", "AwaitingApproval", "Approved"}
+    /\ activeRequest[s] = r
+    /\ requestPhase' = [requestPhase EXCEPT ![r] = "TimedOut"]
+    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
+    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
+    /\ activeRequest' = [activeRequest EXCEPT ![s] = NoRequest]
+    /\ UNCHANGED <<
+        domainPhase, coordinatorState, stateAnchorState, sidecarState,
+        sandboxState, trustReady, lockOwner, published, registered, connected,
+        connectionState, approvalSource, approvedCommand, hostRunning
+        >>
+
+(***************************************************************************
+Failure and recovery
+***************************************************************************)
+
+FailDomain(d) ==
+    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping"}
+    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
+    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
+    /\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
+    /\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
+    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
+    /\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
+    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
+    /\ published' = published \ {d}
+    /\ registered' = [registered EXCEPT ![d] = {}]
+    /\ connected' = [connected EXCEPT ![d] = {}]
+    /\ sessionPhase' = [s \in Sessions |->
+        IF Dom(s) = d /\ sessionPhase[s] \notin {"New", "Closed"}
+        THEN "Failed"
+        ELSE sessionPhase[s]]
+    /\ terminalRoute' = [s \in Sessions |->
+        IF Dom(s) = d THEN "Detached" ELSE terminalRoute[s]]
+    /\ connectionState' = [s \in Sessions |->
+        IF Dom(s) = d THEN "Disconnected" ELSE connectionState[s]]
+    /\ activeRequest' = [s \in Sessions |->
+        IF Dom(s) = d THEN NoRequest ELSE activeRequest[s]]
+    /\ requestPhase' = [r \in Requests |->
+        IF ReqDomain(r) = d /\ requestPhase[r] # "Unused" /\ ~IsTerminalRequest(r)
+        THEN "Failed"
+        ELSE requestPhase[r]]
+    /\ hostRunning' = hostRunning \ RequestsForDomain(d)
+    /\ UNCHANGED <<approvalSource, approvedCommand>>
+
+ResetFailedDomain(d) ==
+    /\ domainPhase[d] = "Failed"
+    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Absent"]
+    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
+    /\ UNCHANGED <<
+        stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
+        published, registered, connected, sessionPhase, terminalRoute,
+        connectionState, activeRequest, requestPhase, approvalSource,
+        approvedCommand, hostRunning
+        >>
+
+DomainProgress(d) ==
+    \/ MountStateAnchor(d)
+    \/ CreateTrustAnchor(d)
+    \/ StartSidecar(d)
+    \/ StartSandbox(d)
+    \/ PublishDomain(d)
+    \/ BeginTeardown(d)
+    \/ StopSandbox(d)
+    \/ StopSidecar(d)
+    \/ UnmountStateAnchor(d)
+    \/ FinishTeardown(d)
+    \/ ResetFailedDomain(d)
+
+SessionProgress(s) ==
+    \/ StartNewDomain(s)
+    \/ StartReadySession(s)
+    \/ WaitForDomain(s)
+    \/ RestartWaitingDomain(s)
+    \/ AdvanceWaitingSession(s)
+    \/ RejectConfigurationMismatch(s)
+    \/ RegisterSession(s)
+
+RequestProgress(r) ==
+    \/ AutoApprove(r)
+    \/ QueuePrompt(r)
+    \/ BeginPrompt(r)
+    \/ (\E cmd \in Commands : DeveloperApprove(r, cmd))
+    \/ DeveloperDeny(r)
+    \/ StartHostExecution(r)
+    \/ CompleteHostExecution(r)
+    \/ TimeoutRequest(r)
+
+Next ==
+    \/ (\E s \in Sessions :
+        StartNewDomain(s) \/ StartReadySession(s) \/ WaitForDomain(s) \/
+        RestartWaitingDomain(s) \/ AdvanceWaitingSession(s) \/
+        RejectConfigurationMismatch(s) \/
+        RegisterSession(s) \/ DisconnectSession(s))
+    \/ (\E d \in Domains :
+        DomainProgress(d) \/ FailDomain(d))
+    \/ (\E r \in Requests :
+        ReceiveEscalation(r) \/ RequestProgress(r))
+
+Spec ==
+    /\ Init
+    /\ [][Next]_vars
+    /\ \A d \in Domains : WF_vars(DomainProgress(d))
+    /\ \A s \in Sessions : WF_vars(SessionProgress(s))
+    /\ \A r \in Requests : WF_vars(RequestProgress(r))
+
+(***************************************************************************
+Safety properties
+***************************************************************************)
+
+TypeOK ==
+    /\ domainPhase \in [Domains -> DomainPhases]
+    /\ coordinatorState \in [Domains -> CoordinatorStates]
+    /\ stateAnchorState \in [Domains -> MountStates]
+    /\ sidecarState \in [Domains -> ResourceStates]
+    /\ sandboxState \in [Domains -> ResourceStates]
+    /\ trustReady \in [Domains -> BOOLEAN]
+    /\ lockOwner \in [Domains -> Sessions \cup {NoSession}]
+    /\ published \subseteq Domains
+    /\ registered \in [Domains -> SUBSET Sessions]
+    /\ connected \in [Domains -> SUBSET Sessions]
+    /\ sessionPhase \in [Sessions -> SessionPhases]
+    /\ terminalRoute \in [Sessions -> TerminalRoutes]
+    /\ connectionState \in [Sessions -> ConnectionStates]
+    /\ activeRequest \in [Sessions -> Requests \cup {NoRequest}]
+    /\ requestPhase \in [Requests -> RequestPhases]
+    /\ approvalSource \in [Requests -> ApprovalSources]
+    /\ approvedCommand \in [Requests -> Commands \cup {NoCommand}]
+    /\ hostRunning \subseteq Requests
+
+ConfigurationConfinement ==
+    \A d \in Domains : domainPhase[d] # "Absent" => ConfigSafe[d]
+
+OrderedNetworkStartup ==
+    \A d \in Domains : sandboxState[d] = "Ready" => sidecarState[d] = "Ready"
+
+PublishedDomainsReady ==
+    \A d \in published :
+        /\ domainPhase[d] = "Ready"
+        /\ coordinatorState[d] = "Ready"
+        /\ stateAnchorState[d] = "Mounted"
+        /\ sidecarState[d] = "Ready"
+        /\ sandboxState[d] = "Ready"
+        /\ trustReady[d]
+
+RegisteredSessionsConnected ==
+    \A d \in Domains : registered[d] \subseteq connected[d]
+
+AttachedSessionsValid ==
+    \A s \in Sessions :
+        sessionPhase[s] \in {"Attached", "Prompting", "HostExecuting"} =>
+            /\ s \in registered[Dom(s)]
+            /\ s \in connected[Dom(s)]
+            /\ domainPhase[Dom(s)] = "Ready"
+            /\ SessionFingerprint[s] = DomainFingerprint[Dom(s)]
+
+AuthenticatedRequestsOnly ==
+    \A r \in Requests : requestPhase[r] # "Unused" =>
+        /\ CertificateValid[r]
+        /\ SignatureValid[r]
+
+HostExecutionAuthorized ==
+    \A r \in hostRunning :
+        /\ requestPhase[r] = "Executing"
+        /\ approvalSource[r] \in {"AutoRule", "Developer"}
+        /\ approvedCommand[r] \in Commands
+
+AutoApprovalNoShell ==
+    \A r \in Requests : approvalSource[r] = "AutoRule" =>
+        /\ approvedCommand[r] = RequestCommand[r]
+        /\ ~CommandRequiresShell[approvedCommand[r]]
+
+TerminalIsolation ==
+    \A s \in Sessions : sessionPhase[s] = "Prompting" =>
+        terminalRoute[s] = "Prompt"
+
+NoOrphanHostProcess ==
+    \A r \in hostRunning :
+        LET s == ReqSession(r) IN
+        /\ activeRequest[s] = r
+        /\ sessionPhase[s] = "HostExecuting"
+        /\ connectionState[s] = "Connected"
+
+StateAnchorOwnership ==
+    \A d \in Domains : stateAnchorState[d] = "Mounted" =>
+        coordinatorState[d] \in {"Starting", "Ready", "Stopping"}
+
+Safety ==
+    /\ TypeOK
+    /\ ConfigurationConfinement
+    /\ OrderedNetworkStartup
+    /\ PublishedDomainsReady
+    /\ RegisteredSessionsConnected
+    /\ AttachedSessionsValid
+    /\ AuthenticatedRequestsOnly
+    /\ HostExecutionAuthorized
+    /\ AutoApprovalNoShell
+    /\ TerminalIsolation
+    /\ NoOrphanHostProcess
+    /\ StateAnchorOwnership
+
+(***************************************************************************
+Liveness properties. TLC configurations may check these separately from the
+safety sweep when the state space grows.
+***************************************************************************)
+
+SessionEventuallyResolves ==
+    \A s \in Sessions :
+        sessionPhase[s] = "New" ~>
+        sessionPhase[s] \in {"Attached", "Closed", "Failed"}
+
+RequestEventuallyResolves ==
+    \A r \in Requests :
+        requestPhase[r] = "Verified" ~>
+        requestPhase[r] \in TerminalRequestPhases
+
+PromptEventuallyRestoresTerminal ==
+    \A s \in Sessions :
+        sessionPhase[s] \in {"Prompting", "HostExecuting"} ~>
+        terminalRoute[s] \in {"Sandbox", "Detached"}
+
+EmptyDomainEventuallyStops ==
+    \A d \in Domains :
+        (<>[](Interested(d) = {})) => <>(domainPhase[d] = "Absent")
+
+=============================================================================