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

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

The model covers Domain startup, ordered resource preparation, 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,
    NoSession,
    NoRequest,
    NoCommand,
    NoApproval,
    SessionDomain,
    SessionFingerprint,
    DomainFingerprint,
    ConfigSafe,
    SandboxIsolationSafe,
    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]
    /\ SandboxIsolationSafe \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",
    "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}

SessionDomainFixture == (S1 :> D1) @@ (S2 :> D1)
SessionFingerprintFixture ==
    (S1 :> "config-a") @@ (S2 :> "config-a")
DomainFingerprintFixture == D1 :> "config-a"
ConfigSafeFixture == D1 :> TRUE
SandboxIsolationSafeFixture == 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"
    /\ SandboxIsolationSafe[d]
    /\ 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] = "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
        >>

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] = "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
        >>

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
        >>

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
        >>

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
        >>

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
        >>

(***************************************************************************
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)
    \/ 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 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]

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]

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

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
    /\ RegisteredSessionsConnected
    /\ AttachedSessionsValid
    /\ AuthenticatedRequestsOnly
    /\ HostExecutionAuthorized
    /\ AutoApprovalNoShell
    /\ TerminalIsolation
    /\ NoOrphanHostProcess
    /\ StateAnchorOwnership
    /\ 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")

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