lazaret/docs/protocol/Lazaret.tla

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

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

The model covers Domain startup under a multi-process Session Coordinator
realized as Host Coordinator, Runtime Supervisor, and attached runsc; ordered
resource preparation owned by the supervisor; Host Coordinator lifetime lease;
role-separated runtime identity tuples; sandbox launch isolation; Client Session
registration; host escalation; correlated result delivery; terminal ownership;
failure; lease-driven teardown; recovery; and abstract durable generation-document
intent with mismatch refuse (DR-M3 vocabulary).

Product names SessionCoordinatorPresent and Session Coordinator ID alias the
existing multi-process predicates and DomainCoordinatorIdentity fixture (SC1–SC3).
Cryptographic algorithms, serialization, container commands, filesystems, typed
redb tables, and network packet handling are refinement boundaries.
***************************************************************************)

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"
}
MountStates == {"Unmounted", "Mounted"}
ResourceStates == {"Stopped", "Ready", "Failed"}
PhysicalProcessStates == {"Absent", "Alive", "Stopped", "Dead"}
RuntimeCausalEdgeStates == {"Unarmed", "Armed"}
SupervisorLeaseStates == {"Unarmed", "Held", "Lost"}
MaxDomainGeneration == 4
\* DR-M3 generation-document decision lifecycle (abstract; not typed redb tables).
DurableDecisions == {"None", "Preparing", "Published", "Clean"}
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,
    stateAnchorState,
    sidecarState,
    sandboxState,
    trustReady,
    lockOwner,
    published,
    registered,
    connected,
    sessionPhase,
    terminalRoute,
    connectionState,
    activeRequest,
    requestPhase,
    approvalSource,
    approvedCommand,
    hostRunning,
    domainLockHeld,
    hostCoordinatorProc,
    runtimeSupervisorProc,
    attachedRunscProc,
    runtimeCausalEdge,
    supervisorLease,
    runtimeFaultsRemaining,
    domainGeneration,
    durableDecision,
    durableSandboxIntent,
    pathMismatch

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

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"

HostCoordinatorAlive(d) == hostCoordinatorProc[d] = "Alive"

HostCoordinatorPresent(d) == ProcessPresent(hostCoordinatorProc[d])

RuntimeSupervisorAlive(d) == runtimeSupervisorProc[d] = "Alive"

\* published means the generation is committed for authenticated join when the
\* Host Coordinator is responsive. Admission always requires HostCoordinatorAlive.
RegistrationAdmissible(d) ==
    /\ d \in published
    /\ domainPhase[d] = "Ready"
    /\ HostCoordinatorAlive(d)

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

\* Multi-process Session Coordinator product vocabulary (saga 18 SC1–SC3).
\* Constitutive processes: Host Coordinator (protocol face), Runtime Supervisor,
\* attached runsc. Present = Alive or Stopped; Dead/Absent do not count.
SessionCoordinatorPresent(d) == RuntimeLogicalAuthorityPresent(d)
SessionCoordinatorAbsent(d) == ~SessionCoordinatorPresent(d)
\* SandboxRunning(d) ≜ sandboxState[d] = "Ready"
\* Coupling: SandboxRunning(d) ⇒ SessionCoordinatorPresent(d)

\* SC3: one logical SC ID per instance; fixture DomainCoordinatorIdentity is not
\* reminted on domainGeneration. HC alone serves session-control Protocol Identity.
SessionCoordinatorIdentity(d) == DomainCoordinatorIdentity[d]
SessionCoordinatorProtocolFaceAlive(d) == HostCoordinatorAlive(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"
    /\ supervisorLease[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)
    /\ HostCoordinatorAlive(d)
    /\ 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}

FailOpenSessionsAndRequests(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)

Init ==
    /\ domainPhase = [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"]
    /\ supervisorLease = [d \in Domains |-> "Unarmed"]
    /\ runtimeFaultsRemaining = [d \in Domains |-> 2]
    /\ domainGeneration = [d \in Domains |-> 0]
    /\ durableDecision = [d \in Domains |-> "None"]
    /\ durableSandboxIntent = [d \in Domains |-> FALSE]
    /\ pathMismatch = [d \in Domains |-> FALSE]

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

Startup ownership:
  Host Coordinator: Domain lock, trust anchor, publication, protocol.
  Runtime Supervisor: State Anchor, Network Sidecar, causal edge, runsc.
***************************************************************************)

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

StartReadySession(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "New"
    /\ RegistrationAdmissible(d)
    /\ SessionFingerprint[s] = DomainFingerprint[d]
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Registering"]
    /\ connectionState' = [connectionState EXCEPT ![s] = "Connected"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        terminalRoute, activeRequest, requestPhase, approvalSource,
        approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

WaitForDomain(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "New"
    /\ domainPhase[d] \in {"Starting", "Stopping"}
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Waiting"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

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

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

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

MountStateAnchor(d) ==
    /\ domainPhase[d] = "Starting"
    /\ HostCoordinatorAlive(d)
    /\ RuntimeSupervisorAlive(d)
    /\ supervisorLease[d] = "Held"
    /\ stateAnchorState[d] = "Unmounted"
    /\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Mounted"]
    /\ UNCHANGED <<
        domainPhase, sidecarState, sandboxState, trustReady,
        lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

StartSidecar(d) ==
    /\ domainPhase[d] = "Starting"
    /\ HostCoordinatorAlive(d)
    /\ RuntimeSupervisorAlive(d)
    /\ supervisorLease[d] = "Held"
    /\ stateAnchorState[d] = "Mounted"
    /\ trustReady[d]
    /\ SidecarCertificateValid[d]
    /\ sidecarState[d] = "Stopped"
    /\ sidecarState' = [sidecarState EXCEPT ![d] = "Ready"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sandboxState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

ArmRuntimeCausalEdge(d) ==
    /\ domainPhase[d] = "Starting"
    /\ HostCoordinatorAlive(d)
    /\ RuntimeSupervisorAlive(d)
    /\ supervisorLease[d] = "Held"
    /\ stateAnchorState[d] = "Mounted"
    /\ sidecarState[d] = "Ready"
    /\ attachedRunscProc[d] = "Absent"
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Armed"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

StartSandbox(d) ==
    /\ domainPhase[d] = "Starting"
    /\ HostCoordinatorAlive(d)
    /\ RuntimeSupervisorAlive(d)
    /\ supervisorLease[d] = "Held"
    /\ runtimeCausalEdge[d] = "Armed"
    /\ sidecarState[d] = "Ready"
    /\ sandboxState[d] = "Stopped"
    /\ attachedRunscProc[d] = "Absent"
    /\ SandboxIsolationSafe[d]
    /\ SandboxCertificateValid[d]
    /\ ~durableSandboxIntent[d]
    /\ ~pathMismatch[d]
    \* Durable sandbox Intent is recorded with the generation document before the
    \* external sandbox create completes (DR-M3 intent-before-create).
    /\ durableSandboxIntent' = [durableSandboxIntent EXCEPT ![d] = TRUE]
    /\ durableDecision' = [durableDecision EXCEPT ![d] = "Preparing"]
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Ready"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Alive"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, runtimeCausalEdge,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        pathMismatch
        >>

PublishDomain(d) ==
    /\ domainPhase[d] = "Starting"
    /\ HostCoordinatorAlive(d)
    /\ RuntimeSupervisorAlive(d)
    /\ supervisorLease[d] = "Held"
    /\ stateAnchorState[d] = "Mounted"
    /\ sidecarState[d] = "Ready"
    /\ sandboxState[d] = "Ready"
    /\ trustReady[d]
    /\ durableSandboxIntent[d]
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Ready"]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
    /\ published' = published \cup {d}
    /\ durableDecision' = [durableDecision EXCEPT ![d] = "Published"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, trustReady, registered,
        connected, sessionPhase, terminalRoute, connectionState,
        activeRequest, requestPhase, approvalSource, approvedCommand,
        hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableSandboxIntent, pathMismatch
        >>

AdvanceWaitingSession(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "Waiting"
    /\ RegistrationAdmissible(d)
    /\ SessionFingerprint[s] = DomainFingerprint[d]
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Registering"]
    /\ connectionState' = [connectionState EXCEPT ![s] = "Connected"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        terminalRoute, activeRequest, requestPhase, approvalSource,
        approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

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, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        activeRequest, requestPhase, approvalSource, approvedCommand,
        hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

RegisterSession(s) ==
    LET d == Dom(s) IN
    /\ sessionPhase[s] = "Registering"
    /\ connectionState[s] = "Connected"
    /\ RegistrationAdmissible(d)
    /\ 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, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, connectionState,
        activeRequest, requestPhase, approvalSource, approvedCommand,
        hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

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 @]
    /\ 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,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

BeginTeardown(d) ==
    /\ domainPhase[d] = "Ready"
    /\ HostCoordinatorAlive(d)
    /\ Interested(d) = {}
    /\ registered[d] = {}
    /\ connected[d] = {}
    /\ domainPhase' = [domainPhase 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, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

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

StopSidecar(d) ==
    /\ domainPhase[d] = "Stopping"
    /\ HostCoordinatorAlive(d)
    /\ RuntimeSupervisorAlive(d)
    /\ supervisorLease[d] = "Held"
    /\ sandboxState[d] = "Stopped"
    /\ sidecarState[d] = "Ready"
    /\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sandboxState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

UnmountStateAnchor(d) ==
    /\ domainPhase[d] = "Stopping"
    /\ HostCoordinatorAlive(d)
    /\ RuntimeSupervisorAlive(d)
    /\ supervisorLease[d] = "Held"
    /\ sandboxState[d] = "Stopped"
    /\ sidecarState[d] = "Stopped"
    /\ stateAnchorState[d] = "Mounted"
    /\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
    /\ UNCHANGED <<
        domainPhase, sidecarState, sandboxState, trustReady,
        lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

GracefulSupervisorExit(d) ==
    /\ domainPhase[d] = "Stopping"
    /\ HostCoordinatorAlive(d)
    /\ RuntimeSupervisorAlive(d)
    /\ supervisorLease[d] = "Held"
    /\ sandboxState[d] = "Stopped"
    /\ sidecarState[d] = "Stopped"
    /\ stateAnchorState[d] = "Unmounted"
    /\ attachedRunscProc[d] = "Absent"
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Dead"]
    /\ supervisorLease' = [supervisorLease EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, attachedRunscProc,
        runtimeCausalEdge, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

FinishTeardown(d) ==
    /\ domainPhase[d] = "Stopping"
    /\ HostCoordinatorAlive(d)
    /\ stateAnchorState[d] = "Unmounted"
    /\ sidecarState[d] = "Stopped"
    /\ sandboxState[d] = "Stopped"
    /\ supervisorLease[d] = "Unarmed"
    /\ ~ProcessPresent(runtimeSupervisorProc[d])
    /\ attachedRunscProc[d] = "Absent"
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ ~pathMismatch[d]
    /\ domainPhase' = [domainPhase 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"]
    /\ supervisorLease' = [supervisorLease EXCEPT ![d] = "Unarmed"]
    /\ durableDecision' = [durableDecision EXCEPT ![d] = "Clean"]
    /\ durableSandboxIntent' = [durableSandboxIntent EXCEPT ![d] = FALSE]
    /\ pathMismatch' = [pathMismatch EXCEPT ![d] = FALSE]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, published, registered,
        connected, sessionPhase, terminalRoute, connectionState,
        activeRequest, requestPhase, approvalSource, approvedCommand,
        hostRunning, runtimeFaultsRemaining,
        domainGeneration
        >>

(***************************************************************************
Host escalation protocol

All coordinator-side request progress requires a responsive Host Coordinator.
***************************************************************************)

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, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, approvalSource,
        approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

AutoApprove(r) ==
    LET d == ReqDomain(r) IN
    /\ requestPhase[r] = "Verified"
    /\ HostCoordinatorAlive(d)
    /\ AutoRuleMatches[r]
    /\ ~CommandRequiresShell[RequestCommand[r]]
    /\ requestPhase' = [requestPhase EXCEPT ![r] = "Approved"]
    /\ approvalSource' = [approvalSource EXCEPT ![r] = "AutoRule"]
    /\ approvedCommand' = [approvedCommand EXCEPT ![r] = RequestCommand[r]]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

QueuePrompt(r) ==
    LET d == ReqDomain(r) IN
    /\ requestPhase[r] = "Verified"
    /\ HostCoordinatorAlive(d)
    /\ ~(AutoRuleMatches[r] /\ ~CommandRequiresShell[RequestCommand[r]])
    /\ requestPhase' = [requestPhase EXCEPT ![r] = "AwaitingApproval"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

BeginPrompt(r) ==
    LET s == ReqSession(r)
        d == ReqDomain(r)
    IN
    /\ requestPhase[r] = "AwaitingApproval"
    /\ HostCoordinatorAlive(d)
    /\ sessionPhase[s] = "Attached"
    /\ activeRequest[s] = r
    /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Prompting"]
    /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Prompt"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, requestPhase, approvalSource,
        approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

DeveloperApprove(r, cmd) ==
    LET s == ReqSession(r)
        d == ReqDomain(r)
    IN
    /\ requestPhase[r] = "AwaitingApproval"
    /\ HostCoordinatorAlive(d)
    /\ 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, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

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

StartHostExecution(r) ==
    LET s == ReqSession(r)
        d == ReqDomain(r)
    IN
    /\ requestPhase[r] = "Approved"
    /\ HostCoordinatorAlive(d)
    /\ 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, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

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

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

CancelRequest(r) ==
    LET s == ReqSession(r)
        d == ReqDomain(r)
    IN
    /\ requestPhase[r] \in {
        "Verified", "AwaitingApproval", "Approved", "Executing"
        }
    /\ HostCoordinatorAlive(d)
    /\ 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, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

FailHostExecution(r) ==
    LET s == ReqSession(r)
        d == ReqDomain(r)
    IN
    /\ requestPhase[r] = "Executing"
    /\ HostCoordinatorAlive(d)
    /\ 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, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        connectionState, activeRequest, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

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

(***************************************************************************
Failure, Host Coordinator lease loss, and recovery

Hard Host Coordinator loss withdraws publication and marks the generation
Failed without itself stopping the sandbox. The surviving Runtime Supervisor
observes supervisorLease = Lost and performs ordered teardown, then exits.
External recovery begins only after the supervisor is no longer present.
***************************************************************************)

FailDomain(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping"}
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
    /\ published' = published \ {d}
    /\ FailOpenSessionsAndRequests(d)
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, approvalSource,
        approvedCommand, domainLockHeld, hostCoordinatorProc,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

HardLoseHostCoordinator(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping"}
    /\ HostCoordinatorPresent(d)
    /\ ConsumeRuntimeFault(d)
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
    /\ published' = published \ {d}
    /\ FailOpenSessionsAndRequests(d)
    /\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Dead"]
    /\ supervisorLease' = [supervisorLease EXCEPT
        ![d] = IF supervisorLease[d] = "Held" THEN "Lost" ELSE @]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, approvalSource,
        approvedCommand, domainLockHeld, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

HardLoseRuntimeSupervisor(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
    /\ ProcessPresent(runtimeSupervisorProc[d])
    /\ ConsumeRuntimeFault(d)
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
    /\ published' = published \ {d}
    /\ FailOpenSessionsAndRequests(d)
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Dead"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT
        ![d] = IF runtimeCausalEdge[d] = "Armed"
                  /\ ProcessPresent(attachedRunscProc[d])
               THEN "Dead"
               ELSE @]
    /\ sandboxState' = [sandboxState EXCEPT
        ![d] = IF runtimeCausalEdge[d] = "Armed" THEN "Stopped" ELSE @]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ supervisorLease' = [supervisorLease EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

HardLoseAttachedRunsc(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
    /\ ProcessPresent(attachedRunscProc[d])
    /\ ConsumeRuntimeFault(d)
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
    /\ published' = published \ {d}
    /\ FailOpenSessionsAndRequests(d)
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Dead"]
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        supervisorLease,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

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

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

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

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

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

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

\* Surviving Host Coordinator health kill of an unresponsive or leftover runtime.
HostCoordinatorTerminateUnresponsiveRuntime(d) ==
    /\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
    /\ HostCoordinatorAlive(d)
    /\ supervisorLease[d] \in {"Held", "Unarmed"}
    /\ \/ runtimeSupervisorProc[d] = "Stopped"
       \/ attachedRunscProc[d] = "Stopped"
       \/ /\ domainPhase[d] = "Failed"
          /\ (ProcessPresent(runtimeSupervisorProc[d])
              \/ ProcessPresent(attachedRunscProc[d]))
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
    /\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
    /\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
    /\ published' = published \ {d}
    /\ FailOpenSessionsAndRequests(d)
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT
        ![d] = IF ProcessPresent(runtimeSupervisorProc[d]) THEN "Dead" ELSE @]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT
        ![d] = IF ProcessPresent(attachedRunscProc[d]) THEN "Dead" ELSE @]
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ supervisorLease' = [supervisorLease EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, approvalSource, approvedCommand,
        domainLockHeld, hostCoordinatorProc, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

\* Ordered Runtime Supervisor teardown after Host Coordinator hard loss.
LeaseTeardownStopSandbox(d) ==
    /\ domainPhase[d] = "Failed"
    /\ supervisorLease[d] = "Lost"
    /\ RuntimeSupervisorAlive(d)
    /\ sandboxState[d] = "Ready"
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT
        ![d] = IF ProcessPresent(attachedRunscProc[d]) THEN "Dead" ELSE "Absent"]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

LeaseTeardownStopSidecar(d) ==
    /\ domainPhase[d] = "Failed"
    /\ supervisorLease[d] = "Lost"
    /\ RuntimeSupervisorAlive(d)
    /\ sandboxState[d] = "Stopped"
    /\ sidecarState[d] = "Ready"
    /\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sandboxState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

LeaseTeardownUnmountStateAnchor(d) ==
    /\ domainPhase[d] = "Failed"
    /\ supervisorLease[d] = "Lost"
    /\ RuntimeSupervisorAlive(d)
    /\ sandboxState[d] = "Stopped"
    /\ sidecarState[d] = "Stopped"
    /\ stateAnchorState[d] = "Mounted"
    /\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
    /\ UNCHANGED <<
        domainPhase, sidecarState, sandboxState, trustReady,
        lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

LeaseTeardownSupervisorExit(d) ==
    /\ domainPhase[d] = "Failed"
    /\ supervisorLease[d] = "Lost"
    /\ RuntimeSupervisorAlive(d)
    /\ sandboxState[d] = "Stopped"
    /\ sidecarState[d] = "Stopped"
    /\ stateAnchorState[d] = "Unmounted"
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Dead"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT
        ![d] = IF attachedRunscProc[d] \in {"Alive", "Stopped"} THEN "Dead" ELSE @]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ supervisorLease' = [supervisorLease EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

\* After HC hard loss, a stopped RS cannot run userspace lease teardown.
\* An external reaper may kill the stopped supervisor and apply the causal edge.
\* It does not clear sidecar or State Anchor; those remain for recovery.
ExternalReapStoppedSupervisorAfterHcLoss(d) ==
    /\ domainPhase[d] = "Failed"
    /\ supervisorLease[d] = "Lost"
    /\ runtimeSupervisorProc[d] = "Stopped"
    /\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Dead"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT
        ![d] = IF ProcessPresent(attachedRunscProc[d]) THEN "Dead" ELSE @]
    /\ sandboxState' = [sandboxState EXCEPT
        ![d] = IF runtimeCausalEdge[d] = "Armed" \/ sandboxState[d] = "Ready"
               THEN "Stopped"
               ELSE @]
    /\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
    /\ supervisorLease' = [supervisorLease EXCEPT ![d] = "Unarmed"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

\* New recovery principal after total HC hard loss and runtime reaps.
BootstrapRecoveryCoordinator(d) ==
    /\ domainPhase[d] = "Failed"
    /\ hostCoordinatorProc[d] = "Dead"
    /\ supervisorLease[d] = "Unarmed"
    /\ ~ProcessPresent(runtimeSupervisorProc[d])
    /\ ~ProcessPresent(attachedRunscProc[d])
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ registered[d] = {}
    /\ connected[d] = {}
    /\ hostRunning \cap RequestsForDomain(d) = {}
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Recovering"]
    /\ 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, supervisorLease,
        runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

BeginRecovery(d) ==
    /\ domainPhase[d] = "Failed"
    /\ HostCoordinatorAlive(d)
    /\ supervisorLease[d] = "Unarmed"
    /\ ~ProcessPresent(runtimeSupervisorProc[d])
    /\ ~ProcessPresent(attachedRunscProc[d])
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ registered[d] = {}
    /\ connected[d] = {}
    /\ hostRunning \cap RequestsForDomain(d) = {}
    /\ domainPhase' = [domainPhase EXCEPT ![d] = "Recovering"]
    /\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = TRUE]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
        published, registered, connected, sessionPhase, terminalRoute,
        connectionState, activeRequest, requestPhase, approvalSource,
        approvedCommand, hostRunning, hostCoordinatorProc,
        runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

RecoverSandbox(d) ==
    /\ domainPhase[d] = "Recovering"
    /\ HostCoordinatorAlive(d)
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ ~ProcessPresent(runtimeSupervisorProc[d])
    /\ ~ProcessPresent(attachedRunscProc[d])
    /\ ~pathMismatch[d]
    /\ \/ sandboxState[d] # "Stopped"
       \/ attachedRunscProc[d] = "Dead"
    \* Exact-owned Ready sandbox cleanup requires durable intent (DR-M3).
    /\ (sandboxState[d] # "Stopped" => durableSandboxIntent[d])
    /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
    /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, runtimeCausalEdge,
        supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

RecoverSidecar(d) ==
    /\ domainPhase[d] = "Recovering"
    /\ HostCoordinatorAlive(d)
    /\ sandboxState[d] = "Stopped"
    /\ attachedRunscProc[d] = "Absent"
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ ~ProcessPresent(runtimeSupervisorProc[d])
    /\ sidecarState[d] # "Stopped"
    /\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sandboxState,
        trustReady, lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

RecoverStateAnchor(d) ==
    /\ domainPhase[d] = "Recovering"
    /\ HostCoordinatorAlive(d)
    /\ sandboxState[d] = "Stopped"
    /\ attachedRunscProc[d] = "Absent"
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ ~ProcessPresent(runtimeSupervisorProc[d])
    /\ sidecarState[d] = "Stopped"
    /\ stateAnchorState[d] = "Mounted"
    /\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
    /\ UNCHANGED <<
        domainPhase, sidecarState, sandboxState, trustReady,
        lockOwner, published, registered, connected, sessionPhase,
        terminalRoute, connectionState, activeRequest, requestPhase,
        approvalSource, approvedCommand, hostRunning, domainLockHeld,
        hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
        runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
        domainGeneration,
        durableDecision, durableSandboxIntent, pathMismatch
        >>

FinishRecovery(d) ==
    /\ domainPhase[d] = "Recovering"
    /\ HostCoordinatorAlive(d)
    /\ stateAnchorState[d] = "Unmounted"
    /\ sidecarState[d] = "Stopped"
    /\ sandboxState[d] = "Stopped"
    /\ attachedRunscProc[d] \in {"Absent", "Dead"}
    /\ runtimeSupervisorProc[d] \in {"Absent", "Dead"}
    /\ ~ProcessPresent(runtimeSupervisorProc[d])
    /\ ~ProcessPresent(attachedRunscProc[d])
    /\ supervisorLease[d] = "Unarmed"
    /\ runtimeCausalEdge[d] = "Unarmed"
    /\ domainPhase' = [domainPhase 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"]
    /\ supervisorLease' = [supervisorLease EXCEPT ![d] = "Unarmed"]
    /\ durableDecision' = [durableDecision EXCEPT ![d] = "Clean"]
    /\ durableSandboxIntent' = [durableSandboxIntent EXCEPT ![d] = FALSE]
    \* Drop generation-document observation of path leftovers; physical foreign
    \* leftovers remain outside the model (SC6 unpublished leftovers).
    /\ pathMismatch' = [pathMismatch EXCEPT ![d] = FALSE]
    /\ UNCHANGED <<
        stateAnchorState, sidecarState, sandboxState, published,
        registered, connected, sessionPhase, terminalRoute, connectionState,
        activeRequest, requestPhase, approvalSource, approvedCommand,
        hostRunning, runtimeFaultsRemaining,
        domainGeneration
        >>


(***************************************************************************
Durable generation document / mismatch refuse (DR-M3 / FM4 abstract)

pathMismatch abstracts wrong-owner or missing-intent observation at the
deterministic sandbox path. Refuse leaves the claim in place; recovery never
adopts a mismatched path into sandboxState.
***************************************************************************)

ObservePathMismatch(d) ==
    /\ domainPhase[d] \in {"Failed", "Recovering"}
    /\ sandboxState[d] = "Stopped"
    /\ attachedRunscProc[d] = "Absent"
    /\ ~pathMismatch[d]
    /\ pathMismatch' = [pathMismatch EXCEPT ![d] = TRUE]
    /\ UNCHANGED <<
        domainPhase, stateAnchorState, sidecarState,
        sandboxState, trustReady, lockOwner, published, registered, connected,
        sessionPhase, terminalRoute, connectionState, activeRequest,
        requestPhase, approvalSource, approvedCommand, hostRunning,
        domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
        attachedRunscProc, runtimeCausalEdge, supervisorLease,
        runtimeFaultsRemaining, domainGeneration,
        durableDecision, durableSandboxIntent
        >>

\* Wrong-owner / missing-intent refuse: fail closed, do not delete or adopt.
RefusePathMismatchCleanup(d) ==
    /\ domainPhase[d] \in {"Failed", "Recovering"}
    /\ HostCoordinatorAlive(d)
    /\ pathMismatch[d]
    /\ UNCHANGED vars

DomainServiceProgress(d) ==
    \/ CreateTrustAnchor(d)
    \/ StartRuntimeSupervisor(d)
    \/ MountStateAnchor(d)
    \/ StartSidecar(d)
    \/ ArmRuntimeCausalEdge(d)
    \/ StartSandbox(d)
    \/ PublishDomain(d)
    \/ BeginTeardown(d)
    \/ StopSandbox(d)
    \/ StopSidecar(d)
    \/ UnmountStateAnchor(d)
    \/ GracefulSupervisorExit(d)
    \/ FinishTeardown(d)
    \/ HostCoordinatorTerminateUnresponsiveRuntime(d)
    \/ LeaseTeardownStopSandbox(d)
    \/ LeaseTeardownStopSidecar(d)
    \/ LeaseTeardownUnmountStateAnchor(d)
    \/ LeaseTeardownSupervisorExit(d)
    \/ ExternalReapStoppedSupervisorAfterHcLoss(d)
    \/ BootstrapRecoveryCoordinator(d)
    \/ BeginRecovery(d)
    \/ RecoverSandbox(d)
    \/ RecoverSidecar(d)
    \/ RecoverStateAnchor(d)
    \/ FinishRecovery(d)

RuntimePhysicalInterleaving(d) ==
    \/ HardLoseHostCoordinator(d)
    \/ HardLoseRuntimeSupervisor(d)
    \/ HardLoseAttachedRunsc(d)
    \/ StopHostCoordinatorProcess(d)
    \/ ResumeHostCoordinatorProcess(d)
    \/ StopRuntimeSupervisorProcess(d)
    \/ ResumeRuntimeSupervisorProcess(d)
    \/ StopAttachedRunscProcess(d)
    \/ ResumeAttachedRunscProcess(d)
    \/ ObservePathMismatch(d)
    \/ RefusePathMismatchCleanup(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 :
        DomainServiceProgress(d) \/ FailDomain(d))
    \/ (\E d \in Domains :
        RuntimePhysicalInterleaving(d))
    \/ (\E r \in Requests :
        ReceiveEscalation(r) \/ RequestProgress(r))

\* Resume transitions are enabled but not weakly fair: permanent stop is a
\* modeled stuck state for safety, not a guaranteed progress path.
Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ \A d \in Domains : WF_vars(DomainServiceProgress(d))
    /\ \A s \in Sessions : WF_vars(SessionProgress(s))
    /\ \A r \in Requests : WF_vars(RequestProgress(r))

(***************************************************************************
Safety properties
***************************************************************************)

TypeOK ==
    /\ domainPhase \in [Domains -> DomainPhases]
    /\ 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]
    /\ supervisorLease \in [Domains -> SupervisorLeaseStates]
    /\ runtimeFaultsRemaining \in [Domains -> 0..2]
    /\ domainGeneration \in [Domains -> 0..MaxDomainGeneration]
    /\ durableDecision \in [Domains -> DurableDecisions]
    /\ durableSandboxIntent \in [Domains -> BOOLEAN]
    /\ pathMismatch \in [Domains -> BOOLEAN]

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"
        /\ HostCoordinatorPresent(d)
        /\ RuntimeSupervisorAlive(d) \/ runtimeSupervisorProc[d] = "Stopped"
        /\ stateAnchorState[d] = "Mounted"
        /\ sidecarState[d] = "Ready"
        /\ sandboxState[d] = "Ready"
        /\ trustReady[d]
        /\ supervisorLease[d] = "Held"

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])
            /\ supervisorLease[d] \in {"Held", "Lost"}

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

PublishedRuntimeAuthorityPresent ==
    \A d \in published :
        /\ SessionCoordinatorPresent(d)
        /\ HostCoordinatorPresent(d)

SupervisorLeaseConsistency ==
    \A d \in Domains :
        /\ (supervisorLease[d] = "Unarmed" =>
            ~ProcessPresent(runtimeSupervisorProc[d]))
        /\ (supervisorLease[d] = "Held" =>
            /\ HostCoordinatorPresent(d)
            /\ ProcessPresent(runtimeSupervisorProc[d]))
        /\ (supervisorLease[d] = "Lost" =>
            /\ hostCoordinatorProc[d] = "Dead"
            /\ ProcessPresent(runtimeSupervisorProc[d]))
        /\ (ProcessPresent(runtimeSupervisorProc[d]) =>
            supervisorLease[d] \in {"Held", "Lost"})

RuntimeResourceOwnership ==
    \A d \in Domains :
        domainPhase[d] \in {"Starting", "Ready", "Stopping"} =>
            /\ (stateAnchorState[d] = "Mounted" =>
                ProcessPresent(runtimeSupervisorProc[d]))
            /\ (sidecarState[d] = "Ready" =>
                ProcessPresent(runtimeSupervisorProc[d]))
            /\ (sandboxState[d] = "Ready" =>
                /\ ProcessPresent(runtimeSupervisorProc[d])
                /\ supervisorLease[d] = "Held")

CoordinatorPhysicalConsistency ==
    \A d \in Domains :
        /\ (domainPhase[d] = "Absent" <=> hostCoordinatorProc[d] = "Absent")
        /\ (domainPhase[d] \in {"Starting", "Ready", "Stopping"} =>
            HostCoordinatorPresent(d))
        /\ (domainPhase[d] = "Recovering" => HostCoordinatorAlive(d))
        /\ (hostCoordinatorProc[d] = "Dead" => domainPhase[d] = "Failed")

ExclusiveBootstrapOwnership ==
    \A d \in Domains : lockOwner[d] # NoSession =>
        /\ domainPhase[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]]
        /\ HostCoordinatorPresent(ReqDomain(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" =>
        /\ domainPhase[d] # "Absent"
        /\ domainLockHeld[d]

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"
            /\ attachedRunscProc[d] \in {"Absent", "Dead"})
        /\ (stateAnchorState[d] = "Unmounted" =>
            /\ sandboxState[d] = "Stopped"
            /\ attachedRunscProc[d] \in {"Absent", "Dead"}
            /\ sidecarState[d] = "Stopped")

OrderedLeaseTeardown ==
    \A d \in Domains :
        (domainPhase[d] = "Failed" /\ supervisorLease[d] = "Lost") =>
            /\ (sidecarState[d] = "Stopped" => sandboxState[d] = "Stopped")
            /\ (stateAnchorState[d] = "Unmounted" =>
                /\ sandboxState[d] = "Stopped"
                /\ sidecarState[d] = "Stopped")

NoVanishPresentRuntime ==
    \A d \in Domains :
        /\ (runtimeSupervisorProc[d] = "Absent" =>
            supervisorLease[d] = "Unarmed")
        /\ (domainPhase[d] = "Recovering" =>
            /\ HostCoordinatorAlive(d)
            /\ supervisorLease[d] = "Unarmed"
            /\ ~ProcessPresent(runtimeSupervisorProc[d])
            /\ ~ProcessPresent(attachedRunscProc[d]))


DomainGenerationBounds ==
    \A d \in Domains :
        /\ domainGeneration[d] \in 0..MaxDomainGeneration
        /\ (domainPhase[d] # "Absent" => domainGeneration[d] > 0)

\* DR-M3 / FM4: Ready sandbox implies durable sandbox Intent was recorded.
DurableIntentBeforeSandboxReady ==
    \A d \in Domains :
        sandboxState[d] = "Ready" => durableSandboxIntent[d]

\* Published generation document decision tracks authenticated publication.
DurableDecisionPublicationConsistent ==
    \A d \in Domains :
        /\ (d \in published => durableDecision[d] = "Published")
        /\ (durableDecision[d] = "Published" => durableSandboxIntent[d])

\* pathMismatch blocks exact-owned sandbox cleanup (wrong-owner / missing-intent).
\* RefusePathMismatchCleanup stutters; RecoverSandbox requires ~pathMismatch.
PathMismatchNotAdopted ==
    \A d \in Domains :
        pathMismatch[d] => sandboxState[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
    /\ SupervisorLeaseConsistency
    /\ RuntimeResourceOwnership
    /\ CoordinatorPhysicalConsistency
    /\ NoVanishPresentRuntime
    /\ OrderedLeaseTeardown
    /\ DomainGenerationBounds
    /\ DurableIntentBeforeSandboxReady
    /\ DurableDecisionPublicationConsistent
    /\ PathMismatchNotAdopted
    /\ ExclusiveBootstrapOwnership
    /\ TeardownNotJoinable
    /\ RegisteredSessionsConnected
    /\ AttachedSessionsValid
    /\ AuthenticatedRequestsOnly
    /\ RuntimeRoleIdentitySeparation
    /\ RegisteredSessionIdentityUniqueness
    /\ LiveRequestIdentityAuthorized
    /\ DeveloperApprovalAuthenticated
    /\ HostExecutionAuthorized
    /\ AutoApprovalNoShell
    /\ TerminalIsolation
    /\ NoOrphanHostProcess
    /\ StateAnchorOwnership
    /\ FailedDomainIsolation
    /\ OrderedFailureRecovery
    /\ ResultDeliveryStateConsistent

(***************************************************************************
Liveness properties.

Permanent Host Coordinator stop is an allowed safety-stuck state: progress
obligations are discharged by resolution or by permanent unresponsiveness.
***************************************************************************)

SessionEventuallyResolves ==
    \A s \in Sessions :
        sessionPhase[s] = "New" ~>
            \/ sessionPhase[s] \in {"Attached", "Closed", "Failed"}
            \/ <>[](hostCoordinatorProc[Dom(s)] = "Stopped")

RequestEventuallyResolves ==
    \A r \in Requests :
        requestPhase[r] = "Verified" ~>
            \/ requestPhase[r] \in TerminalRequestPhases
            \/ <>[](hostCoordinatorProc[ReqDomain(r)] = "Stopped")

PromptEventuallyRestoresTerminal ==
    \A s \in Sessions :
        sessionPhase[s] \in {"Prompting", "HostExecuting"} ~>
            \/ terminalRoute[s] \in {"Sandbox", "Detached"}
            \/ <>[](hostCoordinatorProc[Dom(s)] = "Stopped")

EmptyDomainEventuallyStops ==
    \A d \in Domains :
        (<>[](Interested(d) = {} /\ HostCoordinatorAlive(d)
              /\ runtimeSupervisorProc[d] # "Stopped"
              /\ attachedRunscProc[d] # "Stopped")) =>
            <>(domainPhase[d] = "Absent")

FailedDomainEventuallyRecovers ==
    \A d \in Domains :
        domainPhase[d] = "Failed" ~>
            \/ domainPhase[d] = "Absent"
            \/ <>[](hostCoordinatorProc[d] = "Stopped")

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