------------------------------ MODULE Lazaret ------------------------------
EXTENDS Naturals, FiniteSets, Sequences, TLC

(***************************************************************************
Application-wide protocol model for Lazaret.

The model covers Domain startup, ordered resource preparation, role-separated
runtime identity tuples, sandbox launch isolation, Client Session registration,
host escalation, correlated result delivery, 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,
    Identities,
    SessionAnchors,
    NoSession,
    NoRequest,
    NoCommand,
    NoApproval,
    SessionDomain,
    SessionFingerprint,
    DomainFingerprint,
    DomainCoordinatorIdentity,
    DomainSidecarIdentity,
    DomainSandboxIdentity,
    SessionCliIdentity,
    SessionAnchorIdentity,
    CoordinatorCertificateValid,
    SidecarCertificateValid,
    SandboxCertificateValid,
    CliCertificateValid,
    ConfigSafe,
    SandboxIsolationSafe,
    RequestSession,
    RequestCommand,
    RequestSandboxIdentity,
    RequestCliIdentity,
    RequestSessionAnchor,
    RequestCredentialValid,
    RequestSignatureValid,
    ApprovalCliIdentity,
    ApprovalSessionAnchor,
    ApprovalSignatureValid,
    ApprovalCommand,
    AutoRuleMatches,
    CommandRequiresShell,
    CommandContentSafe,
    D1,
    S1,
    S2,
    R1,
    R2,
    R3,
    ExactCmd,
    PromptCmd,
    ShellCmd,
    EditedCmd

ASSUME
    /\ IsFiniteSet(Domains)
    /\ IsFiniteSet(Sessions)
    /\ IsFiniteSet(Requests)
    /\ IsFiniteSet(Commands)
    /\ IsFiniteSet(Identities)
    /\ IsFiniteSet(SessionAnchors)
    /\ Domains # {}
    /\ Sessions # {}
    /\ Requests # {}
    /\ NoSession \notin Sessions
    /\ NoRequest \notin Requests
    /\ NoCommand \notin Commands
    /\ SessionDomain \in [Sessions -> Domains]
    /\ SessionFingerprint \in [Sessions -> STRING]
    /\ DomainFingerprint \in [Domains -> STRING]
    /\ DomainCoordinatorIdentity \in [Domains -> Identities]
    /\ DomainSidecarIdentity \in [Domains -> Identities]
    /\ DomainSandboxIdentity \in [Domains -> Identities]
    /\ SessionCliIdentity \in [Sessions -> Identities]
    /\ SessionAnchorIdentity \in [Sessions -> SessionAnchors]
    /\ CoordinatorCertificateValid \in [Domains -> BOOLEAN]
    /\ SidecarCertificateValid \in [Domains -> BOOLEAN]
    /\ SandboxCertificateValid \in [Domains -> BOOLEAN]
    /\ CliCertificateValid \in [Sessions -> BOOLEAN]
    /\ ConfigSafe \in [Domains -> BOOLEAN]
    /\ SandboxIsolationSafe \in [Domains -> BOOLEAN]
    /\ RequestSession \in [Requests -> Sessions]
    /\ RequestCommand \in [Requests -> Commands]
    /\ RequestSandboxIdentity \in [Requests -> Identities]
    /\ RequestCliIdentity \in [Requests -> Identities]
    /\ RequestSessionAnchor \in [Requests -> SessionAnchors]
    /\ RequestCredentialValid \in [Requests -> BOOLEAN]
    /\ RequestSignatureValid \in [Requests -> BOOLEAN]
    /\ ApprovalCliIdentity \in [Requests -> Identities]
    /\ ApprovalSessionAnchor \in [Requests -> SessionAnchors]
    /\ ApprovalSignatureValid \in [Requests -> BOOLEAN]
    /\ ApprovalCommand \in [Requests -> Commands]
    /\ AutoRuleMatches \in [Requests -> BOOLEAN]
    /\ CommandRequiresShell \in [Commands -> BOOLEAN]
    /\ CommandContentSafe \in [Commands -> BOOLEAN]

DomainPhases == {
    "Absent", "Starting", "Ready", "Stopping", "Failed", "Recovering"
}
CoordinatorStates == {"Absent", "Starting", "Ready", "Stopping", "Failed"}
MountStates == {"Unmounted", "Mounted"}
ResourceStates == {"Stopped", "Ready", "Failed"}
PhysicalProcessStates == {"Absent", "Starting", "Alive", "Stopped", "Dead"}
RuntimeCausalEdgeStates == {"Unarmed", "Armed"}
SessionPhases == {
    "New", "Waiting", "Registering", "Attached", "Prompting",
    "HostExecuting", "Closed", "Failed"
}
TerminalRoutes == {"Detached", "Sandbox", "Prompt", "HostProcess"}
ConnectionStates == {"Disconnected", "Connected"}
RequestPhases == {
    "Unused", "Verified", "AwaitingApproval", "Approved", "Executing",
    "CompletionPending", "DenialPending", "TimeoutPending",
    "CancellationPending", "FailurePending",
    "Completed", "Denied", "TimedOut", "Cancelled", "Failed"
}
ApprovalSources == {NoApproval, "AutoRule", "Developer"}
PendingResultPhases == {
    "CompletionPending", "DenialPending", "TimeoutPending",
    "CancellationPending", "FailurePending"
}
TerminalRequestPhases == {"Completed", "Denied", "TimedOut", "Cancelled", "Failed"}

DeliveredResultPhase(p) ==
    CASE p = "CompletionPending" -> "Completed"
      [] p = "DenialPending" -> "Denied"
      [] p = "TimeoutPending" -> "TimedOut"
      [] p = "CancellationPending" -> "Cancelled"
      [] p = "FailurePending" -> "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}
IdentitiesFixture == {
    "coordinator-1", "sidecar-1", "sandbox-1", "sandbox-other",
    "cli-1", "cli-2"
}
SessionAnchorsFixture == {"anchor-1", "anchor-2"}

SessionDomainFixture == (S1 :> D1) @@ (S2 :> D1)
SessionFingerprintFixture ==
    (S1 :> "config-a") @@ (S2 :> "config-a")
DomainFingerprintFixture == D1 :> "config-a"
DomainCoordinatorIdentityFixture == D1 :> "coordinator-1"
DomainSidecarIdentityFixture == D1 :> "sidecar-1"
DomainSandboxIdentityFixture == D1 :> "sandbox-1"
SessionCliIdentityFixture == (S1 :> "cli-1") @@ (S2 :> "cli-2")
SessionAnchorIdentityFixture ==
    (S1 :> "anchor-1") @@ (S2 :> "anchor-2")
CoordinatorCertificateValidFixture == D1 :> TRUE
SidecarCertificateValidFixture == D1 :> TRUE
SandboxCertificateValidFixture == D1 :> TRUE
CliCertificateValidFixture == (S1 :> TRUE) @@ (S2 :> TRUE)
ConfigSafeFixture == D1 :> TRUE
SandboxIsolationSafeFixture == D1 :> TRUE
RequestSessionFixture ==
    (R1 :> S1) @@ (R2 :> S2) @@ (R3 :> S1)
RequestCommandFixture ==
    (R1 :> ExactCmd) @@ (R2 :> PromptCmd) @@ (R3 :> ShellCmd)
RequestSandboxIdentityFixture ==
    (R1 :> "sandbox-1") @@
    (R2 :> "sandbox-1") @@
    (R3 :> "sandbox-other")
RequestCliIdentityFixture ==
    (R1 :> "cli-1") @@ (R2 :> "cli-2") @@ (R3 :> "cli-1")
RequestSessionAnchorFixture ==
    (R1 :> "anchor-1") @@
    (R2 :> "anchor-2") @@
    (R3 :> "anchor-1")
RequestCredentialValidFixture ==
    (R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> TRUE)
RequestSignatureValidFixture ==
    (R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> TRUE)
ApprovalCliIdentityFixture ==
    (R1 :> "cli-1") @@ (R2 :> "cli-2") @@ (R3 :> "cli-1")
ApprovalSessionAnchorFixture ==
    (R1 :> "anchor-1") @@
    (R2 :> "anchor-2") @@
    (R3 :> "anchor-1")
ApprovalSignatureValidFixture ==
    (R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> TRUE)
ApprovalCommandFixture ==
    (R1 :> ExactCmd) @@ (R2 :> EditedCmd) @@ (R3 :> ShellCmd)
AutoRuleMatchesFixture ==
    (R1 :> TRUE) @@ (R2 :> FALSE) @@ (R3 :> TRUE)
CommandRequiresShellFixture ==
    (ExactCmd :> FALSE) @@
    (PromptCmd :> FALSE) @@
    (ShellCmd :> TRUE) @@
    (EditedCmd :> FALSE)
CommandContentSafeFixture ==
    (ExactCmd :> TRUE) @@
    (PromptCmd :> TRUE) @@
    (ShellCmd :> TRUE) @@
    (EditedCmd :> TRUE)

VARIABLES
    domainPhase,
    coordinatorState,
    stateAnchorState,
    sidecarState,
    sandboxState,
    trustReady,
    lockOwner,
    published,
    registered,
    connected,
    sessionPhase,
    terminalRoute,
    connectionState,
    activeRequest,
    requestPhase,
    approvalSource,
    approvedCommand,
    hostRunning,
    domainLockHeld,
    hostCoordinatorProc,
    runtimeSupervisorProc,
    attachedRunscProc,
    runtimeCausalEdge,
    runtimeFaultsRemaining

vars == <<
    domainPhase,
    coordinatorState,
    stateAnchorState,
    sidecarState,
    sandboxState,
    trustReady,
    lockOwner,
    published,
    registered,
    connected,
    sessionPhase,
    terminalRoute,
    connectionState,
    activeRequest,
    requestPhase,
    approvalSource,
    approvedCommand,
    hostRunning,
    domainLockHeld,
    hostCoordinatorProc,
    runtimeSupervisorProc,
    attachedRunscProc,
    runtimeCausalEdge,
    runtimeFaultsRemaining
>>

Dom(s) == SessionDomain[s]
ReqSession(r) == RequestSession[r]
ReqDomain(r) == Dom(ReqSession(r))
IsTerminalRequest(r) == requestPhase[r] \in TerminalRequestPhases

ProcessPresent(state) == state \in {"Alive", "Stopped"}

ProcessResponsive(state) == state = "Alive"

RuntimeLogicalAuthorityPresent(d) ==
    \/ ProcessPresent(hostCoordinatorProc[d])
    \/ ProcessPresent(runtimeSupervisorProc[d])
    \/ ProcessPresent(attachedRunscProc[d])

RuntimeAuthorityResponsive(d) ==
    \/ ProcessResponsive(hostCoordinatorProc[d])
    \/ ProcessResponsive(runtimeSupervisorProc[d])
    \/ ProcessResponsive(attachedRunscProc[d])

RuntimeGenerationAbsent(d) ==
    /\ ~domainLockHeld[d]
    /\ hostCoordinatorProc[d] = "Absent"
    /\ runtimeSupervisorProc[d] = "Absent"
    /\ attachedRunscProc[d] = "Absent"
    /\ runtimeCausalEdge[d] = "Unarmed"

ConsumeRuntimeFault(d) ==
    /\ runtimeFaultsRemaining[d] > 0
    /\ runtimeFaultsRemaining' =
        [runtimeFaultsRemaining EXCEPT ![d] = @ - 1]

RuntimeIdentityTupleAuthorized(d) ==
    /\ trustReady[d]
    /\ domainPhase[d] = "Ready"
    /\ d \in published
    /\ sidecarState[d] = "Ready"
    /\ sandboxState[d] = "Ready"
    /\ RuntimeLogicalAuthorityPresent(d)
    /\ CoordinatorCertificateValid[d]
    /\ SidecarCertificateValid[d]
    /\ SandboxCertificateValid[d]
    /\ Cardinality({
        DomainCoordinatorIdentity[d],
        DomainSidecarIdentity[d],
        DomainSandboxIdentity[d]
        }) = 3

RuntimeIdentityTupleReady(d) ==
    /\ RuntimeIdentityTupleAuthorized(d)
    /\ hostCoordinatorProc[d] = "Alive"
    /\ RuntimeAuthorityResponsive(d)

SessionIdentityTupleRegistered(s) ==
    /\ s \in registered[Dom(s)]
    /\ s \in connected[Dom(s)]
    /\ CliCertificateValid[s]

RequestIdentityTupleMatches(r) ==
    LET s == ReqSession(r)
        d == ReqDomain(r)
    IN
    /\ RequestSandboxIdentity[r] = DomainSandboxIdentity[d]
    /\ RequestCliIdentity[r] = SessionCliIdentity[s]
    /\ RequestSessionAnchor[r] = SessionAnchorIdentity[s]

ApprovalIdentityTupleMatches(r) ==
    LET s == ReqSession(r) IN
    /\ ApprovalCliIdentity[r] = SessionCliIdentity[s]
    /\ ApprovalSessionAnchor[r] = SessionAnchorIdentity[s]
    \* This predicate abstracts verification over the request ID, decision, and
    \* exact approved command bytes, not merely verification of any signature by
    \* the registered key.
    /\ ApprovalSignatureValid[r]

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 = {}
    /\ domainLockHeld = [d \in Domains |-> FALSE]
    /\ hostCoordinatorProc = [d \in Domains |-> "Absent"]
    /\ runtimeSupervisorProc = [d \in Domains |-> "Absent"]
    /\ attachedRunscProc = [d \in Domains |-> "Absent"]
    /\ runtimeCausalEdge = [d \in Domains |-> "Unarmed"]
    /\ runtimeFaultsRemaining = [d \in Domains |-> 2]

(***************************************************************************
Domain and Session lifecycle
***************************************************************************)

StartNewDomain(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "New"
    /\ ConfigSafe[d]
    /\ domainPhase[d] = "Absent"
    /\ RuntimeGenerationAbsent(d)
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Starting"]
    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Starting"]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = s]
    /\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = TRUE]
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Waiting"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, trustReady, published,
        registered, connected, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

StartReadySession(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "New"
    /\ domainPhase[d] = "Ready"
    /\ d \in published
    /\ hostCoordinatorProc[d] = "Alive"
    /\ 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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

RestartWaitingDomain(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "Waiting"
    /\ ConfigSafe[d]
    /\ domainPhase[d] = "Absent"
    /\ RuntimeGenerationAbsent(d)
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Starting"]
    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Starting"]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = s]
    /\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = TRUE]
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, trustReady, published,
        registered, connected, sessionPhase, terminalRoute, connectionState,
        activeRequest, requestPhase, approvalSource, approvedCommand,
        hostRunning, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, runtimeFaultsRemaining
        >>

MountStateAnchor(d) ==
    /\ domainPhase[d] = "Starting"
    /\ coordinatorState[d] = "Starting"
    /\ hostCoordinatorProc[d] = "Alive"
    /\ 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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

CreateTrustAnchor(d) ==
    /\ domainPhase[d] = "Starting"
    /\ coordinatorState[d] = "Starting"
    /\ hostCoordinatorProc[d] = "Alive"
    /\ ~trustReady[d]
    /\ CoordinatorCertificateValid[d]
    /\ trustReady' = [trustReady EXCEPT ![d] = TRUE]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

StartSidecar(d) ==
    /\ domainPhase[d] = "Starting"
    /\ hostCoordinatorProc[d] = "Alive"
    /\ stateAnchorState[d] = "Mounted"
    /\ trustReady[d]
    /\ SidecarCertificateValid[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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

StartRuntimeSupervisor(d) ==
    /\ domainPhase[d] = "Starting"
    /\ hostCoordinatorProc[d] = "Alive"
    /\ sidecarState[d] = "Ready"
    /\ runtimeSupervisorProc[d] = "Absent"
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Alive"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, attachedRunscProc,
        runtimeCausalEdge, runtimeFaultsRemaining
        >>

ArmRuntimeCausalEdge(d) ==
    /\ domainPhase[d] = "Starting"
    /\ hostCoordinatorProc[d] = "Alive"
    /\ runtimeSupervisorProc[d] = "Alive"
    /\ attachedRunscProc[d] = "Absent"
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Armed"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeFaultsRemaining
        >>

StartSandbox(d) ==
    /\ domainPhase[d] = "Starting"
    /\ hostCoordinatorProc[d] = "Alive"
    /\ runtimeSupervisorProc[d] = "Alive"
    /\ runtimeCausalEdge[d] = "Armed"
    /\ sidecarState[d] = "Ready"
    /\ sandboxState[d] = "Stopped"
    /\ attachedRunscProc[d] = "Absent"
    /\ SandboxIsolationSafe[d]
    /\ SandboxCertificateValid[d]
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Ready"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Alive"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

PublishDomain(d) ==
    /\ domainPhase[d] = "Starting"
    /\ coordinatorState[d] = "Starting"
    /\ hostCoordinatorProc[d] = "Alive"
    /\ RuntimeAuthorityResponsive(d)
    /\ 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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

AdvanceWaitingSession(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "Waiting"
    /\ domainPhase[d] = "Ready"
    /\ d \in published
    /\ hostCoordinatorProc[d] = "Alive"
    /\ 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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

RegisterSession(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "Registering"
    /\ connectionState[s] = "Connected"
    /\ domainPhase[d] = "Ready"
    /\ d \in published
    /\ hostCoordinatorProc[d] = "Alive"
    /\ SessionFingerprint[s] = DomainFingerprint[d]
    /\ CliCertificateValid[s]
    /\ 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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

DisconnectSession(s) ==
    LET d == Dom(s)
        r == activeRequest[s]
        leaderLost ==
            lockOwner[d] = s /\ domainPhase[d] = "Starting"
    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}
    /\ domainPhase' = [domainPhase EXCEPT
        ![d] = IF leaderLost THEN "Failed" ELSE @]
    /\ coordinatorState' = [coordinatorState EXCEPT
        ![d] = IF leaderLost THEN "Failed" ELSE @]
    /\ trustReady' = [trustReady EXCEPT
        ![d] = IF leaderLost THEN FALSE ELSE @]
    /\ lockOwner' = [lockOwner EXCEPT
        ![d] = IF leaderLost THEN NoSession ELSE @]
    /\ published' = IF leaderLost THEN published \ {d} ELSE published
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, approvalSource,
        approvedCommand, domainLockHeld, hostCoordinatorProc,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

BeginTeardown(d) ==
    /\ domainPhase[d] = "Ready"
    /\ hostCoordinatorProc[d] = "Alive"
    /\ 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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

StopSandbox(d) ==
    /\ domainPhase[d] = "Stopping"
    /\ RuntimeAuthorityResponsive(d)
    /\ sandboxState[d] = "Ready"
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, runtimeFaultsRemaining
        >>

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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

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]
    /\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = FALSE]
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Absent"]
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Absent"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, published, registered,
        connected, sessionPhase, terminalRoute, connectionState,
        activeRequest, requestPhase, approvalSource, approvedCommand,
        hostRunning, runtimeFaultsRemaining
        >>

(***************************************************************************
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]
    /\ RuntimeIdentityTupleReady(d)
    /\ SessionIdentityTupleRegistered(s)
    /\ RequestIdentityTupleMatches(r)
    /\ RequestCredentialValid[r]
    /\ RequestSignatureValid[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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

DeveloperApprove(r, cmd) ==
    LET s == ReqSession(r) IN
    /\ requestPhase[r] = "AwaitingApproval"
    /\ sessionPhase[s] = "Prompting"
    /\ ApprovalIdentityTupleMatches(r)
    /\ cmd \in Commands
    /\ cmd = ApprovalCommand[r]
    /\ 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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

DeveloperDeny(r) ==
    LET s == ReqSession(r) IN
    /\ requestPhase[r] = "AwaitingApproval"
    /\ sessionPhase[s] = "Prompting"
    /\ ApprovalIdentityTupleMatches(r)
    /\ requestPhase' = [requestPhase EXCEPT ![r] = "DenialPending"]
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, approvalSource, approvedCommand,
        hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

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"}
    /\ CommandContentSafe[approvedCommand[r]]
    /\ 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,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

CompleteHostExecution(r) ==
    LET s == ReqSession(r) IN
    /\ requestPhase[r] = "Executing"
    /\ r \in hostRunning
    /\ requestPhase' = [requestPhase EXCEPT ![r] = "CompletionPending"]
    /\ hostRunning' = hostRunning \ {r}
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

TimeoutRequest(r) ==
    LET s == ReqSession(r) IN
    /\ requestPhase[r] \in {"Verified", "AwaitingApproval", "Approved", "Executing"}
    /\ activeRequest[s] = r
    /\ requestPhase' = [requestPhase EXCEPT ![r] = "TimeoutPending"]
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
    /\ hostRunning' = hostRunning \ {r}
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

CancelRequest(r) ==
    LET s == ReqSession(r) IN
    /\ requestPhase[r] \in {
        "Verified", "AwaitingApproval", "Approved", "Executing"
        }
    /\ activeRequest[s] = r
    /\ connectionState[s] = "Connected"
    /\ requestPhase' = [requestPhase EXCEPT ![r] = "CancellationPending"]
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
    /\ hostRunning' = hostRunning \ {r}
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

FailHostExecution(r) ==
    LET s == ReqSession(r) IN
    /\ requestPhase[r] = "Executing"
    /\ activeRequest[s] = r
    /\ connectionState[s] = "Connected"
    /\ requestPhase' = [requestPhase EXCEPT ![r] = "FailurePending"]
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
    /\ hostRunning' = hostRunning \ {r}
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

DeliverResult(r) ==
    LET s == ReqSession(r) IN
    /\ requestPhase[r] \in PendingResultPhases
    /\ activeRequest[s] = r
    /\ connectionState[s] = "Connected"
    /\ sessionPhase[s] = "Attached"
    /\ requestPhase' = [requestPhase EXCEPT
        ![r] = DeliveredResultPhase(@)]
    /\ activeRequest' = [activeRequest EXCEPT ![s] = NoRequest]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, approvalSource,
        approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

(***************************************************************************
Failure and recovery
***************************************************************************)

FailDomain(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping"}
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
    /\ 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 <<
        stateAnchorState, sidecarState, sandboxState, approvalSource,
        approvedCommand, domainLockHeld, hostCoordinatorProc,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

HardLoseHostCoordinator(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping"}
    /\ ProcessPresent(hostCoordinatorProc[d])
    /\ ConsumeRuntimeFault(d)
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
    /\ 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)
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Dead"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, approvalSource,
        approvedCommand, domainLockHeld, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge
        >>

HardLoseRuntimeSupervisor(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
    /\ ProcessPresent(runtimeSupervisorProc[d])
    /\ ConsumeRuntimeFault(d)
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
    /\ 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)
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Dead"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT
        ![d] = IF runtimeCausalEdge[d] = "Armed" THEN "Dead" ELSE @]
    /\ sandboxState' = [sandboxState EXCEPT
        ![d] = IF runtimeCausalEdge[d] = "Armed" THEN "Stopped" ELSE @]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc
        >>

HardLoseAttachedRunsc(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
    /\ ProcessPresent(attachedRunscProc[d])
    /\ ConsumeRuntimeFault(d)
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
    /\ 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)
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Dead"]
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc
        >>

StopHostCoordinatorProcess(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
    /\ hostCoordinatorProc[d] = "Alive"
    /\ ConsumeRuntimeFault(d)
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Stopped"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge
        >>

ResumeHostCoordinatorProcess(d) ==
    /\ hostCoordinatorProc[d] = "Stopped"
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, runtimeFaultsRemaining
        >>

StopRuntimeSupervisorProcess(d) ==
    /\ runtimeSupervisorProc[d] = "Alive"
    /\ ConsumeRuntimeFault(d)
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Stopped"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, attachedRunscProc,
        runtimeCausalEdge
        >>

ResumeRuntimeSupervisorProcess(d) ==
    /\ runtimeSupervisorProc[d] = "Stopped"
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Alive"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, attachedRunscProc,
        runtimeCausalEdge, runtimeFaultsRemaining
        >>

StopAttachedRunscProcess(d) ==
    /\ attachedRunscProc[d] = "Alive"
    /\ ConsumeRuntimeFault(d)
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Stopped"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        runtimeCausalEdge
        >>

ResumeAttachedRunscProcess(d) ==
    /\ attachedRunscProc[d] = "Stopped"
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Alive"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        runtimeCausalEdge, runtimeFaultsRemaining
        >>

BeginRecovery(d) ==
    /\ domainPhase[d] = "Failed"
    /\ registered[d] = {}
    /\ connected[d] = {}
    /\ hostRunning \cap RequestsForDomain(d) = {}
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Recovering"]
    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Stopping"]
    /\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = TRUE]
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
        published, registered, connected, sessionPhase, terminalRoute,
        connectionState, activeRequest, requestPhase, approvalSource,
        approvedCommand, hostRunning, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

RecoverSandbox(d) ==
    /\ domainPhase[d] = "Recovering"
    /\ sandboxState[d] # "Stopped"
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Dead"]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sidecarState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, runtimeFaultsRemaining
        >>

RecoverSidecar(d) ==
    /\ domainPhase[d] = "Recovering"
    /\ sandboxState[d] = "Stopped"
    /\ sidecarState[d] # "Stopped"
    /\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
    /\ UNCHANGED <<
        domainPhase, coordinatorState, stateAnchorState, sandboxState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

RecoverStateAnchor(d) ==
    /\ domainPhase[d] = "Recovering"
    /\ 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, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
        >>

FinishRecovery(d) ==
    /\ domainPhase[d] = "Recovering"
    /\ stateAnchorState[d] = "Unmounted"
    /\ sidecarState[d] = "Stopped"
    /\ sandboxState[d] = "Stopped"
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Absent"]
    /\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
    /\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
    /\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = FALSE]
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Absent"]
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Absent"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, published,
        registered, connected, sessionPhase, terminalRoute, connectionState,
        activeRequest, requestPhase, approvalSource, approvedCommand,
        hostRunning, runtimeFaultsRemaining
        >>

DomainProgress(d) ==
    \/ MountStateAnchor(d)
    \/ CreateTrustAnchor(d)
    \/ StartSidecar(d)
    \/ StartRuntimeSupervisor(d)
    \/ ArmRuntimeCausalEdge(d)
    \/ StartSandbox(d)
    \/ PublishDomain(d)
    \/ BeginTeardown(d)
    \/ StopSandbox(d)
    \/ StopSidecar(d)
    \/ UnmountStateAnchor(d)
    \/ FinishTeardown(d)
    \/ BeginRecovery(d)
    \/ RecoverSandbox(d)
    \/ RecoverSidecar(d)
    \/ RecoverStateAnchor(d)
    \/ FinishRecovery(d)
    \/ ResumeHostCoordinatorProcess(d)
    \/ ResumeRuntimeSupervisorProcess(d)
    \/ ResumeAttachedRunscProcess(d)

RuntimePhysicalInterleaving(d) ==
    \/ HardLoseHostCoordinator(d)
    \/ HardLoseRuntimeSupervisor(d)
    \/ HardLoseAttachedRunsc(d)
    \/ StopHostCoordinatorProcess(d)
    \/ ResumeHostCoordinatorProcess(d)
    \/ StopRuntimeSupervisorProcess(d)
    \/ ResumeRuntimeSupervisorProcess(d)
    \/ StopAttachedRunscProcess(d)
    \/ ResumeAttachedRunscProcess(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)
    \/ CancelRequest(r)
    \/ FailHostExecution(r)
    \/ DeliverResult(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 d \in Domains :
        RuntimePhysicalInterleaving(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
    /\ domainLockHeld \in [Domains -> BOOLEAN]
    /\ hostCoordinatorProc \in [Domains -> PhysicalProcessStates]
    /\ runtimeSupervisorProc \in [Domains -> PhysicalProcessStates]
    /\ attachedRunscProc \in [Domains -> PhysicalProcessStates]
    /\ runtimeCausalEdge \in [Domains -> RuntimeCausalEdgeStates]
    /\ runtimeFaultsRemaining \in [Domains -> 0..2]

ConfigurationConfinement ==
    \A d \in Domains : domainPhase[d] # "Absent" => ConfigSafe[d]

SandboxNamespaceIsolation ==
    \A d \in Domains : sandboxState[d] = "Ready" => SandboxIsolationSafe[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]

DomainLockLifetime ==
    \A d \in Domains :
        /\ (domainPhase[d] = "Absent" => ~domainLockHeld[d])
        /\ (domainPhase[d] # "Absent" => domainLockHeld[d])
        /\ (~domainLockHeld[d] => RuntimeGenerationAbsent(d))

RuntimeCausalEdgeArmedBeforeSandbox ==
    \A d \in Domains :
        sandboxState[d] = "Ready" =>
            /\ runtimeCausalEdge[d] = "Armed"
            /\ ProcessPresent(attachedRunscProc[d])

RuntimeCausalEdgeOwnerPresent ==
    \A d \in Domains :
        runtimeCausalEdge[d] = "Armed" =>
            /\ domainLockHeld[d]
            /\ ProcessPresent(runtimeSupervisorProc[d])

SandboxRunningImpliesCoordinatorPresent ==
    \A d \in Domains :
        sandboxState[d] = "Ready" => RuntimeLogicalAuthorityPresent(d)

PublishedRuntimeAuthorityPresent ==
    \A d \in published :
        RuntimeLogicalAuthorityPresent(d)

ExclusiveBootstrapOwnership ==
    \A d \in Domains : lockOwner[d] # NoSession =>
        /\ domainPhase[d] = "Starting"
        /\ coordinatorState[d] = "Starting"
        /\ sessionPhase[lockOwner[d]] = "Waiting"

TeardownNotJoinable ==
    \A d \in Domains : domainPhase[d] \in {"Stopping", "Failed", "Recovering"} =>
        /\ d \notin published
        /\ registered[d] = {}
        /\ connected[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" =>
        /\ RequestCredentialValid[r]
        /\ RequestSignatureValid[r]
        /\ RequestIdentityTupleMatches(r)

RuntimeRoleIdentitySeparation ==
    /\ \A d \in Domains :
        Cardinality({
            DomainCoordinatorIdentity[d],
            DomainSidecarIdentity[d],
            DomainSandboxIdentity[d]
            }) = 3
    /\ \A s \in Sessions :
        LET d == Dom(s) IN
        SessionCliIdentity[s] \notin {
            DomainCoordinatorIdentity[d],
            DomainSidecarIdentity[d],
            DomainSandboxIdentity[d]
            }

RegisteredSessionIdentityUniqueness ==
    \A s1, s2 \in Sessions :
        /\ s1 # s2
        /\ s1 \in registered[Dom(s1)]
        /\ s2 \in registered[Dom(s2)]
        => /\ SessionCliIdentity[s1] # SessionCliIdentity[s2]
           /\ SessionAnchorIdentity[s1] # SessionAnchorIdentity[s2]

LiveRequestIdentityAuthorized ==
    \A r \in Requests :
        requestPhase[r] \notin {"Unused"} \cup TerminalRequestPhases =>
            /\ RuntimeIdentityTupleAuthorized(ReqDomain(r))
            /\ SessionIdentityTupleRegistered(ReqSession(r))

DeveloperApprovalAuthenticated ==
    \A r \in Requests : approvalSource[r] = "Developer" =>
        /\ ApprovalCliIdentity[r] = SessionCliIdentity[ReqSession(r)]
        /\ ApprovalSessionAnchor[r] = SessionAnchorIdentity[ReqSession(r)]
        /\ ApprovalSignatureValid[r]
        /\ approvedCommand[r] = ApprovalCommand[r]

HostExecutionAuthorized ==
    \A r \in hostRunning :
        /\ requestPhase[r] = "Executing"
        /\ approvalSource[r] \in {"AutoRule", "Developer"}
        /\ approvedCommand[r] \in Commands
        /\ CommandContentSafe[approvedCommand[r]]

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", "Failed"}

FailedDomainIsolation ==
    \A d \in Domains : domainPhase[d] \in {"Failed", "Recovering"} =>
        /\ d \notin published
        /\ registered[d] = {}
        /\ connected[d] = {}
        /\ ~trustReady[d]
        /\ hostRunning \cap RequestsForDomain(d) = {}

OrderedFailureRecovery ==
    \A d \in Domains : domainPhase[d] = "Recovering" =>
        /\ (sidecarState[d] = "Stopped" => sandboxState[d] = "Stopped")
        /\ (stateAnchorState[d] = "Unmounted" =>
            /\ sandboxState[d] = "Stopped"
            /\ sidecarState[d] = "Stopped")

ResultDeliveryStateConsistent ==
    /\ \A r \in Requests : requestPhase[r] \in PendingResultPhases =>
        LET s == ReqSession(r) IN
        /\ activeRequest[s] = r
        /\ connectionState[s] = "Connected"
        /\ sessionPhase[s] = "Attached"
        /\ r \notin hostRunning
    /\ \A r \in Requests : requestPhase[r] \in TerminalRequestPhases =>
        /\ activeRequest[ReqSession(r)] # r
        /\ r \notin hostRunning

Safety ==
    /\ TypeOK
    /\ ConfigurationConfinement
    /\ SandboxNamespaceIsolation
    /\ OrderedNetworkStartup
    /\ PublishedDomainsReady
    /\ DomainLockLifetime
    /\ RuntimeCausalEdgeArmedBeforeSandbox
    /\ RuntimeCausalEdgeOwnerPresent
    /\ SandboxRunningImpliesCoordinatorPresent
    /\ PublishedRuntimeAuthorityPresent
    /\ ExclusiveBootstrapOwnership
    /\ TeardownNotJoinable
    /\ RegisteredSessionsConnected
    /\ AttachedSessionsValid
    /\ AuthenticatedRequestsOnly
    /\ RuntimeRoleIdentitySeparation
    /\ RegisteredSessionIdentityUniqueness
    /\ LiveRequestIdentityAuthorized
    /\ DeveloperApprovalAuthenticated
    /\ HostExecutionAuthorized
    /\ AutoApprovalNoShell
    /\ TerminalIsolation
    /\ NoOrphanHostProcess
    /\ StateAnchorOwnership
    /\ FailedDomainIsolation
    /\ OrderedFailureRecovery
    /\ ResultDeliveryStateConsistent

(***************************************************************************
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")

FailedDomainEventuallyRecovers ==
    \A d \in Domains :
        domainPhase[d] = "Failed" ~> domainPhase[d] = "Absent"

=============================================================================