3046 lines
126 KiB
Text
3046 lines
126 KiB
Text
------------------------------ MODULE Lazaret ------------------------------
|
|
EXTENDS Naturals, FiniteSets, Sequences, TLC
|
|
|
|
(***************************************************************************
|
|
Application-wide protocol model for Lazaret.
|
|
|
|
Authoritative for protocol lifecycle and communication semantics (Domain phases,
|
|
publication, session registration, escalation, durableDecision vocabulary,
|
|
checked invariants). The product specification states north star, vocabulary,
|
|
below-abstraction architecture, and requirements; it must not redefine this
|
|
state machine. Durable generation decisions are exactly
|
|
DurableDecisions = {"None", "Preparing", "Published", "Clean"} — there is no
|
|
"Commit" decision. Session Coordinator, Network Sidecar, and Agent Sandbox
|
|
protocol IDs are generation-scoped variables reminted on each new generation.
|
|
|
|
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;
|
|
durable Session Terminal and PTY lifecycle; failure; lease-driven teardown;
|
|
recovery; and abstract durable generation-document intent with mismatch refuse.
|
|
|
|
Product names SessionCoordinatorPresent and Session Coordinator ID alias the
|
|
multi-process presence predicates and generation-scoped genCoordinatorId.
|
|
Durable participant intent is multi-role; networkReady gates publication;
|
|
preparedLowerLeased and helperProc refine physical ownership under RS.
|
|
Cryptographic algorithms, serialization, container commands, filesystems, typed
|
|
redb tables, PTY descriptor identities, process identifiers, terminal byte and
|
|
signal mechanics, and network packet handling remain refinement boundaries.
|
|
The model does distinguish keyboard PTY delivery, explicit guest-group signals,
|
|
local Client controls, and terminal metadata because those carry different
|
|
authorities.
|
|
***************************************************************************)
|
|
|
|
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,
|
|
TerminalEventPlan,
|
|
TerminalAuthorityPlan,
|
|
TerminalAdministrativeAuthorityValid,
|
|
TerminalRoutingFault,
|
|
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
|
|
DurableDecisions == {"None", "Preparing", "Published", "Clean"}
|
|
SessionPhases == {
|
|
"New", "Waiting", "Registering", "Attached", "Prompting",
|
|
"HostExecuting", "Closed", "Failed"
|
|
}
|
|
TerminalRoutes == {"Detached", "Sandbox", "Prompt", "HostProcess"}
|
|
SessionTerminalStates == {"Clean", "Intent", "Running", "ReleaseIntent"}
|
|
TerminalEventKinds == {
|
|
"Keyboard", "ExplicitSignal", "Resize", "Break", "LocalSuspend",
|
|
"LocalResume", "LocalDisconnect", "HostSignal"
|
|
}
|
|
TerminalAuthorities == {
|
|
"None", "Client", "Administrator", "LocalClient", "HostProcess"
|
|
}
|
|
TerminalDispositions == {"None", "Delivered", "Refused"}
|
|
TerminalTargets == {
|
|
"None", "GuestPtyForeground", "RecordedGuestGroup", "LocalClient",
|
|
"ExactSessionPty"
|
|
}
|
|
TerminalRoutingFaults == {
|
|
"Correct", "KeyboardRecordedGroup", "KeyboardDuplicated",
|
|
"CrossSession", "ClientAdministrativeSignal",
|
|
"BlockedTransportPreventsLocalControl"
|
|
}
|
|
TerminalTransportStates == {"Ready", "Blocked"}
|
|
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", "coordinator-2", "coordinator-3", "coordinator-4",
|
|
"sidecar-1", "sidecar-2", "sidecar-3", "sidecar-4",
|
|
"sandbox-1", "sandbox-2", "sandbox-3", "sandbox-4", "sandbox-other",
|
|
"cli-1", "cli-2"
|
|
}
|
|
\* Generation-scoped mint sequences (1-indexed by domainGeneration).
|
|
CoordinatorIds == <<"coordinator-1", "coordinator-2", "coordinator-3", "coordinator-4">>
|
|
SidecarIds == <<"sidecar-1", "sidecar-2", "sidecar-3", "sidecar-4">>
|
|
SandboxIds == <<"sandbox-1", "sandbox-2", "sandbox-3", "sandbox-4">>
|
|
DurableRoles == {"prepared_lower", "anchor", "network", "sandbox", "helper"}
|
|
HelperProcStates == {"Absent", "Alive", "Dead"}
|
|
EmptyDurableIntent == [role \in DurableRoles |-> FALSE]
|
|
SessionAnchorsFixture == {"anchor-1", "anchor-2"}
|
|
|
|
SessionDomainFixture == (S1 :> D1) @@ (S2 :> D1)
|
|
TerminalEventPlanFixture ==
|
|
(S1 :> <<
|
|
"Keyboard", "Resize", "LocalSuspend", "LocalResume",
|
|
"LocalDisconnect"
|
|
>>) @@
|
|
(S2 :> <<
|
|
"ExplicitSignal", "ExplicitSignal", "Break", "Keyboard", "HostSignal"
|
|
>>)
|
|
TerminalAuthorityPlanFixture ==
|
|
(S1 :> <<
|
|
"Client", "Client", "LocalClient", "LocalClient", "LocalClient"
|
|
>>) @@
|
|
(S2 :> <<
|
|
"Client", "Administrator", "LocalClient", "Client", "HostProcess"
|
|
>>)
|
|
TerminalAdministrativeAuthorityValidFixture ==
|
|
(S1 :> <<FALSE, FALSE, FALSE, FALSE, FALSE>>) @@
|
|
(S2 :> <<FALSE, TRUE, FALSE, FALSE, FALSE>>)
|
|
TerminalNoEventPlanFixture ==
|
|
(S1 :> <<>>) @@ (S2 :> <<>>)
|
|
TerminalNoAuthorityPlanFixture ==
|
|
(S1 :> <<>>) @@ (S2 :> <<>>)
|
|
TerminalNoAdministrativeAuthorityValidFixture ==
|
|
(S1 :> <<>>) @@ (S2 :> <<>>)
|
|
TerminalRoutingEventPlanFixture ==
|
|
(S1 :> <<"Keyboard", "Resize">>) @@
|
|
(S2 :> <<"ExplicitSignal", "ExplicitSignal">>)
|
|
TerminalRoutingAuthorityPlanFixture ==
|
|
(S1 :> <<"Client", "Client">>) @@
|
|
(S2 :> <<"Client", "Administrator">>)
|
|
TerminalRoutingAdministrativeAuthorityValidFixture ==
|
|
(S1 :> <<FALSE, FALSE>>) @@
|
|
(S2 :> <<FALSE, TRUE>>)
|
|
TerminalLocalControlEventPlanFixture ==
|
|
(S1 :> <<"LocalSuspend", "LocalResume", "LocalDisconnect">>) @@
|
|
(S2 :> <<"Break", "HostSignal">>)
|
|
TerminalLocalControlAuthorityPlanFixture ==
|
|
(S1 :> <<"LocalClient", "LocalClient", "LocalClient">>) @@
|
|
(S2 :> <<"LocalClient", "HostProcess">>)
|
|
TerminalLocalControlAdministrativeAuthorityValidFixture ==
|
|
(S1 :> <<FALSE, FALSE, FALSE>>) @@
|
|
(S2 :> <<FALSE, FALSE>>)
|
|
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,
|
|
durableIntent,
|
|
pathMismatch,
|
|
genCoordinatorId,
|
|
genSidecarId,
|
|
genSandboxId,
|
|
networkReady,
|
|
preparedLowerLeased,
|
|
helperProc,
|
|
sessionTerminalState,
|
|
sessionPtyOpen,
|
|
sessionExecPresent,
|
|
sessionGuestKnown,
|
|
terminalEventIndex,
|
|
terminalLastEventId,
|
|
terminalLastEvent,
|
|
terminalLastSourceSession,
|
|
terminalLastAuthority,
|
|
terminalLastAdministrativeAuthorityValid,
|
|
terminalLastDisposition,
|
|
terminalLastDestination,
|
|
terminalLastTarget,
|
|
terminalLastByteDeliveries,
|
|
terminalLastSignalDeliveries,
|
|
terminalLastLocalDeliveries,
|
|
terminalLastMetadataDeliveries,
|
|
sessionClientSuspended,
|
|
sessionTerminalTransportState
|
|
|
|
baseVars == <<
|
|
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,
|
|
durableIntent,
|
|
pathMismatch,
|
|
genCoordinatorId,
|
|
genSidecarId,
|
|
genSandboxId,
|
|
networkReady,
|
|
preparedLowerLeased,
|
|
helperProc
|
|
>>
|
|
|
|
terminalLifecycleVars == <<
|
|
sessionTerminalState,
|
|
sessionPtyOpen,
|
|
sessionExecPresent,
|
|
sessionGuestKnown
|
|
>>
|
|
|
|
terminalEventRecordVars == <<
|
|
terminalEventIndex,
|
|
terminalLastEventId,
|
|
terminalLastEvent,
|
|
terminalLastSourceSession,
|
|
terminalLastAuthority,
|
|
terminalLastAdministrativeAuthorityValid,
|
|
terminalLastDisposition,
|
|
terminalLastDestination,
|
|
terminalLastTarget,
|
|
terminalLastByteDeliveries,
|
|
terminalLastSignalDeliveries,
|
|
terminalLastLocalDeliveries,
|
|
terminalLastMetadataDeliveries
|
|
>>
|
|
|
|
terminalInteractionVars == <<
|
|
terminalEventRecordVars, sessionClientSuspended, sessionTerminalTransportState
|
|
>>
|
|
|
|
terminalVars == <<terminalLifecycleVars, terminalInteractionVars>>
|
|
|
|
vars == <<baseVars, terminalVars>>
|
|
|
|
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])
|
|
|
|
\* 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)
|
|
|
|
\* Generation-scoped Session Coordinator ID (minted on StartNewDomain / restart).
|
|
\* HC alone serves session-control Protocol Identity face.
|
|
SessionCoordinatorIdentity(d) == genCoordinatorId[d]
|
|
SessionCoordinatorProtocolFaceAlive(d) == HostCoordinatorAlive(d)
|
|
NetworkSidecarIdentity(d) == genSidecarId[d]
|
|
AgentSandboxIdentity(d) == genSandboxId[d]
|
|
|
|
MintGenerationIdentities(d, g) ==
|
|
/\ genCoordinatorId' = [genCoordinatorId EXCEPT ![d] = CoordinatorIds[g]]
|
|
/\ genSidecarId' = [genSidecarId EXCEPT ![d] = SidecarIds[g]]
|
|
/\ genSandboxId' = [genSandboxId EXCEPT ![d] = SandboxIds[g]]
|
|
|
|
ClearGenerationProductState(d) ==
|
|
/\ durableIntent' = [durableIntent EXCEPT ![d] = EmptyDurableIntent]
|
|
/\ pathMismatch' = [pathMismatch EXCEPT ![d] = FALSE]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = FALSE]
|
|
/\ helperProc' = [helperProc EXCEPT ![d] = "Absent"]
|
|
|
|
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"
|
|
/\ helperProc[d] \in {"Absent", "Dead"}
|
|
/\ ~preparedLowerLeased[d]
|
|
/\ ~networkReady[d]
|
|
|
|
RuntimeAbsentForTerminal(d) ==
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ ~ProcessPresent(runtimeSupervisorProc[d])
|
|
/\ ~ProcessPresent(attachedRunscProc[d])
|
|
|
|
SessionTerminalsClean(d) ==
|
|
\A s \in Sessions : Dom(s) = d => sessionTerminalState[s] = "Clean"
|
|
|
|
ConsumeRuntimeFault(d) ==
|
|
/\ runtimeFaultsRemaining[d] > 0
|
|
/\ runtimeFaultsRemaining' =
|
|
[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({
|
|
genCoordinatorId[d],
|
|
genSidecarId[d],
|
|
genSandboxId[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] = genSandboxId[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"]
|
|
/\ durableIntent = [d \in Domains |-> EmptyDurableIntent]
|
|
/\ pathMismatch = [d \in Domains |-> FALSE]
|
|
/\ genCoordinatorId = [d \in Domains |-> "coordinator-1"]
|
|
/\ genSidecarId = [d \in Domains |-> "sidecar-1"]
|
|
/\ genSandboxId = [d \in Domains |-> "sandbox-1"]
|
|
/\ networkReady = [d \in Domains |-> FALSE]
|
|
/\ preparedLowerLeased = [d \in Domains |-> FALSE]
|
|
/\ helperProc = [d \in Domains |-> "Absent"]
|
|
/\ sessionTerminalState = [s \in Sessions |-> "Clean"]
|
|
/\ sessionPtyOpen = [s \in Sessions |-> FALSE]
|
|
/\ sessionExecPresent = [s \in Sessions |-> FALSE]
|
|
/\ sessionGuestKnown = [s \in Sessions |-> FALSE]
|
|
/\ terminalEventIndex = [s \in Sessions |-> 1]
|
|
/\ terminalLastEventId = [s \in Sessions |-> 0]
|
|
/\ terminalLastEvent = [s \in Sessions |-> "None"]
|
|
/\ terminalLastSourceSession = [s \in Sessions |-> NoSession]
|
|
/\ terminalLastAuthority = [s \in Sessions |-> "None"]
|
|
/\ terminalLastAdministrativeAuthorityValid =
|
|
[s \in Sessions |-> FALSE]
|
|
/\ terminalLastDisposition = [s \in Sessions |-> "None"]
|
|
/\ terminalLastDestination = [s \in Sessions |-> NoSession]
|
|
/\ terminalLastTarget = [s \in Sessions |-> "None"]
|
|
/\ terminalLastByteDeliveries = [s \in Sessions |-> 0]
|
|
/\ terminalLastSignalDeliveries = [s \in Sessions |-> 0]
|
|
/\ terminalLastLocalDeliveries = [s \in Sessions |-> 0]
|
|
/\ terminalLastMetadataDeliveries = [s \in Sessions |-> 0]
|
|
/\ sessionClientSuspended = [s \in Sessions |-> FALSE]
|
|
/\ sessionTerminalTransportState = [s \in Sessions |-> "Ready"]
|
|
|
|
(***************************************************************************
|
|
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"]
|
|
/\ LET g == domainGeneration[d] + 1 IN
|
|
/\ domainGeneration' = [domainGeneration EXCEPT ![d] = g]
|
|
/\ MintGenerationIdentities(d, g)
|
|
/\ 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"]
|
|
/\ ClearGenerationProductState(d)
|
|
/\ 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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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"]
|
|
/\ LET g == domainGeneration[d] + 1 IN
|
|
/\ domainGeneration' = [domainGeneration EXCEPT ![d] = g]
|
|
/\ MintGenerationIdentities(d, g)
|
|
/\ lockOwner' = [lockOwner EXCEPT ![d] = s]
|
|
/\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = TRUE]
|
|
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
|
|
/\ durableDecision' = [durableDecision EXCEPT ![d] = "None"]
|
|
/\ ClearGenerationProductState(d)
|
|
/\ 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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
MountStateAnchor(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ supervisorLease[d] = "Held"
|
|
/\ preparedLowerLeased[d]
|
|
/\ durableIntent[d]["prepared_lower"]
|
|
/\ stateAnchorState[d] = "Unmounted"
|
|
/\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Mounted"]
|
|
/\ durableIntent' = [durableIntent EXCEPT ![d] =
|
|
[@ EXCEPT !["anchor"] = TRUE]]
|
|
/\ 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, pathMismatch, genCoordinatorId, genSidecarId,
|
|
genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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"]
|
|
/\ durableIntent' = [durableIntent EXCEPT ![d] =
|
|
[@ EXCEPT !["network"] = TRUE]]
|
|
/\ 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, pathMismatch, genCoordinatorId, genSidecarId,
|
|
genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
StartSandbox(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ supervisorLease[d] = "Held"
|
|
/\ runtimeCausalEdge[d] = "Armed"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ durableIntent[d]["network"]
|
|
/\ helperProc[d] = "Alive"
|
|
/\ durableIntent[d]["helper"]
|
|
/\ durableIntent[d]["anchor"]
|
|
/\ durableIntent[d]["prepared_lower"]
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ attachedRunscProc[d] = "Absent"
|
|
/\ SandboxIsolationSafe[d]
|
|
/\ SandboxCertificateValid[d]
|
|
/\ ~durableIntent[d]["sandbox"]
|
|
/\ ~pathMismatch[d]
|
|
\* Intent and external creation are one abstract step; implementations
|
|
\* must persist Intent before the resource can outlive the caller.
|
|
/\ durableIntent' = [durableIntent EXCEPT ![d] =
|
|
[@ EXCEPT !["sandbox"] = 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, genCoordinatorId, genSidecarId, genSandboxId,
|
|
networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
PublishDomain(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ supervisorLease[d] = "Held"
|
|
/\ stateAnchorState[d] = "Mounted"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ sandboxState[d] = "Ready"
|
|
/\ trustReady[d]
|
|
/\ networkReady[d]
|
|
/\ durableIntent[d]["sandbox"]
|
|
/\ durableIntent[d]["network"]
|
|
/\ durableIntent[d]["anchor"]
|
|
/\ durableIntent[d]["prepared_lower"]
|
|
/\ 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,
|
|
durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId,
|
|
networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
(***************************************************************************
|
|
Session Terminal and PTY lifecycle
|
|
|
|
The model retains durable state plus abstract PTY, exec-client, and guest
|
|
identity facts. It distinguishes interaction authorities and target classes.
|
|
Descriptor identities, PID reuse checks, control-character values, terminal
|
|
modes, and physical byte or signal delivery remain refinements.
|
|
***************************************************************************)
|
|
|
|
BeginSessionTerminal(s) ==
|
|
LET d == Dom(s) IN
|
|
/\ sessionPhase[s] = "Attached"
|
|
/\ terminalRoute[s] = "Sandbox"
|
|
/\ RegistrationAdmissible(d)
|
|
/\ sessionTerminalState[s] = "Clean"
|
|
/\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Intent"]
|
|
/\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = TRUE]
|
|
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = TRUE]
|
|
/\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
|
|
/\ UNCHANGED baseVars
|
|
/\ UNCHANGED terminalInteractionVars
|
|
|
|
CommitSessionTerminal(s) ==
|
|
/\ sessionPhase[s] = "Attached"
|
|
/\ terminalRoute[s] = "Sandbox"
|
|
/\ HostCoordinatorAlive(Dom(s))
|
|
/\ sessionTerminalState[s] = "Intent"
|
|
/\ sessionPtyOpen[s]
|
|
/\ sessionExecPresent[s]
|
|
/\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Running"]
|
|
/\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = TRUE]
|
|
/\ UNCHANGED <<baseVars, sessionPtyOpen, sessionExecPresent>>
|
|
/\ UNCHANGED terminalInteractionVars
|
|
|
|
DisconnectCleanSession(s) ==
|
|
/\ sessionTerminalState[s] = "Clean"
|
|
/\ DisconnectSession(s)
|
|
/\ UNCHANGED terminalVars
|
|
|
|
DisconnectLiveSessionTerminal(s) ==
|
|
/\ sessionTerminalState[s] \in {"Intent", "Running"}
|
|
/\ DisconnectSession(s)
|
|
/\ sessionTerminalState' =
|
|
[sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
|
|
/\ UNCHANGED <<sessionPtyOpen, sessionExecPresent, sessionGuestKnown>>
|
|
/\ UNCHANGED terminalInteractionVars
|
|
|
|
CompleteSessionTerminal(s) ==
|
|
/\ sessionTerminalState[s] = "Running"
|
|
/\ DisconnectSession(s)
|
|
/\ sessionTerminalState' =
|
|
[sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
|
|
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
|
|
/\ UNCHANGED <<sessionPtyOpen, sessionGuestKnown>>
|
|
/\ UNCHANGED terminalInteractionVars
|
|
|
|
ExitSessionTerminalBeforeGuestIdentity(s) ==
|
|
/\ sessionTerminalState[s] = "Intent"
|
|
/\ DisconnectSession(s)
|
|
/\ sessionTerminalState' =
|
|
[sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
|
|
/\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = FALSE]
|
|
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
|
|
/\ UNCHANGED sessionGuestKnown
|
|
/\ UNCHANGED terminalInteractionVars
|
|
|
|
RetainFailedSessionTerminal(s) ==
|
|
/\ sessionPhase[s] = "Failed"
|
|
/\ sessionTerminalState[s] \in {"Intent", "Running"}
|
|
/\ sessionTerminalState' =
|
|
[sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
|
|
/\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = FALSE]
|
|
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
|
|
/\ UNCHANGED <<baseVars, sessionGuestKnown>>
|
|
/\ UNCHANGED terminalInteractionVars
|
|
|
|
CleanKnownSessionTerminal(s) ==
|
|
/\ sessionPhase[s] \in {"Closed", "Failed"}
|
|
/\ sessionTerminalState[s] = "ReleaseIntent"
|
|
/\ sessionGuestKnown[s]
|
|
/\ HostCoordinatorAlive(Dom(s))
|
|
/\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Clean"]
|
|
/\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = FALSE]
|
|
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
|
|
/\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
|
|
/\ UNCHANGED baseVars
|
|
/\ UNCHANGED terminalInteractionVars
|
|
|
|
BootstrapCleanSessionTerminalAfterRuntimeAbsence(s) ==
|
|
/\ sessionPhase[s] \in {"Closed", "Failed"}
|
|
/\ sessionTerminalState[s] = "ReleaseIntent"
|
|
/\ ~sessionPtyOpen[s]
|
|
/\ ~sessionExecPresent[s]
|
|
/\ RuntimeAbsentForTerminal(Dom(s))
|
|
/\ HostCoordinatorAlive(Dom(s))
|
|
/\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Clean"]
|
|
/\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
|
|
/\ UNCHANGED <<baseVars, sessionPtyOpen, sessionExecPresent,
|
|
terminalInteractionVars>>
|
|
|
|
TerminalInteractionAdmissible(s) ==
|
|
/\ sessionPhase[s] = "Attached"
|
|
/\ connectionState[s] = "Connected"
|
|
/\ terminalRoute[s] = "Sandbox"
|
|
/\ sessionTerminalState[s] = "Running"
|
|
/\ HostCoordinatorAlive(Dom(s))
|
|
|
|
TerminalEventAvailable(s) ==
|
|
terminalEventIndex[s] <= Len(TerminalEventPlan[s])
|
|
|
|
CurrentTerminalEvent(s) ==
|
|
IF TerminalEventAvailable(s)
|
|
THEN TerminalEventPlan[s][terminalEventIndex[s]]
|
|
ELSE "None"
|
|
|
|
CurrentTerminalAuthority(s) ==
|
|
IF TerminalEventAvailable(s)
|
|
THEN TerminalAuthorityPlan[s][terminalEventIndex[s]]
|
|
ELSE "None"
|
|
|
|
CurrentTerminalAdministrativeAuthorityValid(s) ==
|
|
IF TerminalEventAvailable(s)
|
|
THEN TerminalAdministrativeAuthorityValid[s][terminalEventIndex[s]]
|
|
ELSE FALSE
|
|
|
|
OtherSession(s) == CHOOSE t \in Sessions : t # s
|
|
|
|
TerminalDelivery(disposition, destination, target, bytes, signals, local, metadata) ==
|
|
[disposition |-> disposition,
|
|
destination |-> destination,
|
|
target |-> target,
|
|
byteDeliveries |-> bytes,
|
|
signalDeliveries |-> signals,
|
|
localDeliveries |-> local,
|
|
metadataDeliveries |-> metadata]
|
|
|
|
NoTerminalDelivery ==
|
|
TerminalDelivery("None", NoSession, "None", 0, 0, 0, 0)
|
|
|
|
RefusedTerminalDelivery ==
|
|
TerminalDelivery("Refused", NoSession, "None", 0, 0, 0, 0)
|
|
|
|
ExpectedTerminalDelivery(s, event, authority, administrativeAuthorityValid) ==
|
|
CASE /\ event = "Keyboard"
|
|
/\ authority = "Client" ->
|
|
TerminalDelivery("Delivered", s, "GuestPtyForeground", 1, 0, 0, 0)
|
|
[] /\ event = "ExplicitSignal"
|
|
/\ authority = "Administrator"
|
|
/\ administrativeAuthorityValid ->
|
|
TerminalDelivery("Delivered", s, "RecordedGuestGroup", 0, 1, 0, 0)
|
|
[] event = "ExplicitSignal" -> RefusedTerminalDelivery
|
|
[] /\ event = "Resize"
|
|
/\ authority = "Client" ->
|
|
TerminalDelivery("Delivered", s, "ExactSessionPty", 0, 0, 0, 1)
|
|
[] /\ event = "Break"
|
|
/\ authority = "LocalClient" ->
|
|
TerminalDelivery("Delivered", s, "ExactSessionPty", 0, 0, 0, 1)
|
|
[] /\ event \in {"LocalSuspend", "LocalResume", "LocalDisconnect"}
|
|
/\ authority = "LocalClient" ->
|
|
TerminalDelivery("Delivered", s, "LocalClient", 0, 0, 1, 0)
|
|
[] /\ event = "HostSignal"
|
|
/\ authority = "HostProcess" ->
|
|
TerminalDelivery("Delivered", s, "LocalClient", 0, 0, 1, 0)
|
|
[] OTHER -> RefusedTerminalDelivery
|
|
|
|
RoutedTerminalDelivery(s, event, authority, administrativeAuthorityValid) ==
|
|
LET expected == ExpectedTerminalDelivery(
|
|
s, event, authority, administrativeAuthorityValid) IN
|
|
CASE /\ TerminalRoutingFault = "KeyboardRecordedGroup"
|
|
/\ event = "Keyboard" ->
|
|
TerminalDelivery("Delivered", s, "RecordedGuestGroup", 0, 1, 0, 0)
|
|
[] /\ TerminalRoutingFault = "KeyboardDuplicated"
|
|
/\ event = "Keyboard" ->
|
|
TerminalDelivery("Delivered", s, "GuestPtyForeground", 1, 1, 0, 0)
|
|
[] /\ TerminalRoutingFault = "CrossSession"
|
|
/\ expected.disposition = "Delivered" ->
|
|
[expected EXCEPT !.destination = OtherSession(s)]
|
|
[] /\ TerminalRoutingFault = "ClientAdministrativeSignal"
|
|
/\ event = "ExplicitSignal"
|
|
/\ authority = "Client" ->
|
|
TerminalDelivery("Delivered", s, "RecordedGuestGroup", 0, 1, 0, 0)
|
|
[] OTHER -> expected
|
|
|
|
RecordTerminalEvent(s) ==
|
|
LET event == CurrentTerminalEvent(s)
|
|
authority == CurrentTerminalAuthority(s)
|
|
administrativeAuthorityValid ==
|
|
CurrentTerminalAdministrativeAuthorityValid(s)
|
|
delivery == RoutedTerminalDelivery(
|
|
s, event, authority, administrativeAuthorityValid)
|
|
IN
|
|
/\ terminalEventIndex' =
|
|
[terminalEventIndex EXCEPT ![s] = @ + 1]
|
|
/\ terminalLastEventId' =
|
|
[terminalLastEventId EXCEPT ![s] = terminalEventIndex[s]]
|
|
/\ terminalLastEvent' = [terminalLastEvent EXCEPT ![s] = event]
|
|
/\ terminalLastSourceSession' =
|
|
[terminalLastSourceSession EXCEPT ![s] = s]
|
|
/\ terminalLastAuthority' =
|
|
[terminalLastAuthority EXCEPT ![s] = authority]
|
|
/\ terminalLastAdministrativeAuthorityValid' =
|
|
[terminalLastAdministrativeAuthorityValid EXCEPT
|
|
![s] = administrativeAuthorityValid]
|
|
/\ terminalLastDisposition' =
|
|
[terminalLastDisposition EXCEPT ![s] = delivery.disposition]
|
|
/\ terminalLastDestination' =
|
|
[terminalLastDestination EXCEPT ![s] = delivery.destination]
|
|
/\ terminalLastTarget' =
|
|
[terminalLastTarget EXCEPT ![s] = delivery.target]
|
|
/\ terminalLastByteDeliveries' =
|
|
[terminalLastByteDeliveries EXCEPT ![s] = delivery.byteDeliveries]
|
|
/\ terminalLastSignalDeliveries' =
|
|
[terminalLastSignalDeliveries EXCEPT ![s] = delivery.signalDeliveries]
|
|
/\ terminalLastLocalDeliveries' =
|
|
[terminalLastLocalDeliveries EXCEPT ![s] = delivery.localDeliveries]
|
|
/\ terminalLastMetadataDeliveries' =
|
|
[terminalLastMetadataDeliveries EXCEPT ![s] = delivery.metadataDeliveries]
|
|
|
|
DeliverPtyTerminalEvent(s) ==
|
|
/\ TerminalInteractionAdmissible(s)
|
|
/\ TerminalEventAvailable(s)
|
|
/\ CurrentTerminalEvent(s) \in {
|
|
"Keyboard", "ExplicitSignal", "Resize", "Break"
|
|
}
|
|
/\ ~sessionClientSuspended[s]
|
|
/\ sessionTerminalTransportState[s] = "Ready"
|
|
/\ RecordTerminalEvent(s)
|
|
/\ UNCHANGED <<baseVars, terminalLifecycleVars, sessionClientSuspended,
|
|
sessionTerminalTransportState>>
|
|
|
|
SuspendLocalTerminalClient(s) ==
|
|
/\ TerminalInteractionAdmissible(s)
|
|
/\ TerminalEventAvailable(s)
|
|
/\ CurrentTerminalEvent(s) = "LocalSuspend"
|
|
/\ ~sessionClientSuspended[s]
|
|
/\ RecordTerminalEvent(s)
|
|
/\ sessionClientSuspended' =
|
|
[sessionClientSuspended EXCEPT ![s] = TRUE]
|
|
/\ UNCHANGED <<baseVars, terminalLifecycleVars,
|
|
sessionTerminalTransportState>>
|
|
|
|
ResumeLocalTerminalClient(s) ==
|
|
/\ TerminalInteractionAdmissible(s)
|
|
/\ TerminalEventAvailable(s)
|
|
/\ CurrentTerminalEvent(s) = "LocalResume"
|
|
/\ sessionClientSuspended[s]
|
|
/\ RecordTerminalEvent(s)
|
|
/\ sessionClientSuspended' =
|
|
[sessionClientSuspended EXCEPT ![s] = FALSE]
|
|
/\ UNCHANGED <<baseVars, terminalLifecycleVars,
|
|
sessionTerminalTransportState>>
|
|
|
|
DisconnectTerminalFromLocalAuthority(s, event) ==
|
|
/\ event \in {"LocalDisconnect", "HostSignal"}
|
|
/\ TerminalEventAvailable(s)
|
|
/\ CurrentTerminalEvent(s) = event
|
|
/\ sessionTerminalState[s] \in {"Intent", "Running"}
|
|
/\ \/ TerminalRoutingFault # "BlockedTransportPreventsLocalControl"
|
|
\/ sessionTerminalTransportState[s] = "Ready"
|
|
/\ DisconnectSession(s)
|
|
/\ sessionTerminalState' =
|
|
[sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
|
|
/\ RecordTerminalEvent(s)
|
|
/\ sessionClientSuspended' =
|
|
[sessionClientSuspended EXCEPT ![s] = FALSE]
|
|
/\ UNCHANGED <<sessionPtyOpen, sessionExecPresent, sessionGuestKnown,
|
|
sessionTerminalTransportState>>
|
|
|
|
BlockSessionTerminalTransport(s) ==
|
|
/\ TerminalInteractionAdmissible(s)
|
|
/\ sessionTerminalTransportState[s] = "Ready"
|
|
/\ sessionTerminalTransportState' =
|
|
[sessionTerminalTransportState EXCEPT ![s] = "Blocked"]
|
|
/\ UNCHANGED <<baseVars, terminalLifecycleVars, terminalEventRecordVars,
|
|
sessionClientSuspended>>
|
|
|
|
UnblockSessionTerminalTransport(s) ==
|
|
/\ sessionTerminalTransportState[s] = "Blocked"
|
|
/\ sessionTerminalTransportState' =
|
|
[sessionTerminalTransportState EXCEPT ![s] = "Ready"]
|
|
/\ UNCHANGED <<baseVars, terminalLifecycleVars, terminalEventRecordVars,
|
|
sessionClientSuspended>>
|
|
|
|
TerminalInteraction(s) ==
|
|
\/ DeliverPtyTerminalEvent(s)
|
|
\/ SuspendLocalTerminalClient(s)
|
|
\/ ResumeLocalTerminalClient(s)
|
|
\/ BlockSessionTerminalTransport(s)
|
|
\/ UnblockSessionTerminalTransport(s)
|
|
\/ (\E event \in {"LocalDisconnect", "HostSignal"} :
|
|
DisconnectTerminalFromLocalAuthority(s, event))
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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"]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ UNCHANGED <<
|
|
domainPhase, stateAnchorState, sidecarState,
|
|
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning, domainLockHeld,
|
|
hostCoordinatorProc, runtimeSupervisorProc, supervisorLease,
|
|
runtimeFaultsRemaining,
|
|
domainGeneration,
|
|
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
StopSidecar(d) ==
|
|
/\ domainPhase[d] = "Stopping"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ supervisorLease[d] = "Held"
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
|
|
/\ helperProc' = [helperProc EXCEPT
|
|
![d] = IF helperProc[d] # "Absent" THEN "Dead" ELSE @]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ 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, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, preparedLowerLeased
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
ReleasePreparedLowerLease(d) ==
|
|
/\ domainPhase[d] = "Stopping"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ stateAnchorState[d] = "Unmounted"
|
|
/\ preparedLowerLeased[d]
|
|
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = FALSE]
|
|
/\ 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, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, networkReady, helperProc
|
|
>>
|
|
|
|
GracefulSupervisorExit(d) ==
|
|
/\ domainPhase[d] = "Stopping"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ supervisorLease[d] = "Held"
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ sidecarState[d] = "Stopped"
|
|
/\ stateAnchorState[d] = "Unmounted"
|
|
/\ ~preparedLowerLeased[d]
|
|
/\ attachedRunscProc[d] = "Absent"
|
|
/\ runtimeCausalEdge[d] = "Unarmed"
|
|
/\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Dead"]
|
|
/\ supervisorLease' = [supervisorLease EXCEPT ![d] = "Unarmed"]
|
|
/\ helperProc' = [helperProc EXCEPT
|
|
![d] = IF helperProc[d] # "Absent" THEN "Dead" ELSE @]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ 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, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, preparedLowerLeased
|
|
>>
|
|
|
|
FinishTeardown(d) ==
|
|
/\ domainPhase[d] = "Stopping"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ stateAnchorState[d] = "Unmounted"
|
|
/\ ~preparedLowerLeased[d]
|
|
/\ 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"]
|
|
/\ ClearGenerationProductState(d)
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, sandboxState, published, registered,
|
|
connected, sessionPhase, terminalRoute, connectionState,
|
|
activeRequest, requestPhase, approvalSource, approvedCommand,
|
|
hostRunning, runtimeFaultsRemaining,
|
|
domainGeneration, genCoordinatorId, genSidecarId, genSandboxId
|
|
>>
|
|
|
|
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]
|
|
/\ networkReady[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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
(***************************************************************************
|
|
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, stops runtime use, unmounts the State Anchor,
|
|
and exits while retaining the prepared-lower lease. External recovery begins
|
|
only after the supervisor is no longer present and releases that lease.
|
|
***************************************************************************)
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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"]
|
|
/\ helperProc' = [helperProc EXCEPT
|
|
![d] = IF helperProc[d] = "Alive" THEN "Dead" ELSE @]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, approvalSource, approvedCommand,
|
|
domainLockHeld, hostCoordinatorProc,
|
|
domainGeneration,
|
|
durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, preparedLowerLeased
|
|
>>
|
|
|
|
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"]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, approvalSource, approvedCommand,
|
|
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
|
supervisorLease,
|
|
domainGeneration,
|
|
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
\* 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"]
|
|
/\ helperProc' = [helperProc EXCEPT
|
|
![d] = IF helperProc[d] = "Alive" THEN "Dead" ELSE @]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, approvalSource, approvedCommand,
|
|
domainLockHeld, hostCoordinatorProc, runtimeFaultsRemaining,
|
|
domainGeneration,
|
|
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, preparedLowerLeased
|
|
>>
|
|
|
|
\* 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"]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ UNCHANGED <<
|
|
domainPhase, stateAnchorState, sidecarState,
|
|
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning, domainLockHeld,
|
|
hostCoordinatorProc, runtimeSupervisorProc, supervisorLease,
|
|
runtimeFaultsRemaining,
|
|
domainGeneration,
|
|
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
LeaseTeardownStopSidecar(d) ==
|
|
/\ domainPhase[d] = "Failed"
|
|
/\ supervisorLease[d] = "Lost"
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
|
|
/\ helperProc' = [helperProc EXCEPT
|
|
![d] = IF helperProc[d] # "Absent" THEN "Dead" ELSE @]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ 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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, preparedLowerLeased
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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"]
|
|
/\ helperProc' = [helperProc EXCEPT
|
|
![d] = IF helperProc[d] # "Absent" THEN "Dead" ELSE @]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ UNCHANGED <<
|
|
domainPhase, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
sessionPhase, terminalRoute, connectionState, activeRequest,
|
|
requestPhase, approvalSource, approvedCommand, hostRunning,
|
|
domainLockHeld, hostCoordinatorProc, runtimeFaultsRemaining,
|
|
domainGeneration,
|
|
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, preparedLowerLeased
|
|
>>
|
|
|
|
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"]
|
|
/\ helperProc' = [helperProc EXCEPT
|
|
![d] = IF helperProc[d] # "Absent" THEN "Dead" ELSE @]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ UNCHANGED <<
|
|
domainPhase, stateAnchorState, sidecarState,
|
|
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning, domainLockHeld,
|
|
hostCoordinatorProc, runtimeFaultsRemaining,
|
|
domainGeneration,
|
|
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, preparedLowerLeased
|
|
>>
|
|
|
|
\* 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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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.
|
|
/\ (sandboxState[d] # "Stopped" => durableIntent[d]["sandbox"])
|
|
/\ 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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
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, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
RecoverPreparedLowerLease(d) ==
|
|
/\ domainPhase[d] = "Recovering"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ attachedRunscProc[d] \in {"Absent", "Dead"}
|
|
/\ runtimeCausalEdge[d] = "Unarmed"
|
|
/\ ~ProcessPresent(runtimeSupervisorProc[d])
|
|
/\ sidecarState[d] = "Stopped"
|
|
/\ stateAnchorState[d] = "Unmounted"
|
|
/\ preparedLowerLeased[d]
|
|
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = FALSE]
|
|
/\ 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, durableIntent, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, networkReady, helperProc
|
|
>>
|
|
|
|
FinishRecovery(d) ==
|
|
/\ domainPhase[d] = "Recovering"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ stateAnchorState[d] = "Unmounted"
|
|
/\ ~preparedLowerLeased[d]
|
|
/\ 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"]
|
|
/\ ClearGenerationProductState(d)
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, sandboxState, published,
|
|
registered, connected, sessionPhase, terminalRoute, connectionState,
|
|
activeRequest, requestPhase, approvalSource, approvedCommand,
|
|
hostRunning, runtimeFaultsRemaining,
|
|
domainGeneration, genCoordinatorId, genSidecarId, genSandboxId
|
|
>>
|
|
|
|
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, durableIntent, genCoordinatorId, genSidecarId,
|
|
genSandboxId, networkReady, preparedLowerLeased, helperProc
|
|
>>
|
|
|
|
\* 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
|
|
|
|
|
|
\* Lazaret-owned prepared lower lease before State Anchor mount.
|
|
LeasePreparedLower(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ supervisorLease[d] = "Held"
|
|
/\ ~preparedLowerLeased[d]
|
|
/\ ~durableIntent[d]["prepared_lower"]
|
|
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = TRUE]
|
|
/\ durableIntent' = [durableIntent EXCEPT ![d] =
|
|
[@ EXCEPT !["prepared_lower"] = 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, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, networkReady, helperProc
|
|
>>
|
|
|
|
\* Connectivity helper supervised under RS lease (not constitutive SC).
|
|
StartConnectivityHelper(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ supervisorLease[d] = "Held"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ durableIntent[d]["network"]
|
|
/\ helperProc[d] = "Absent"
|
|
/\ helperProc' = [helperProc EXCEPT ![d] = "Alive"]
|
|
/\ durableIntent' = [durableIntent EXCEPT ![d] =
|
|
[@ EXCEPT !["helper"] = 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, pathMismatch, genCoordinatorId,
|
|
genSidecarId, genSandboxId, networkReady, preparedLowerLeased
|
|
>>
|
|
|
|
\* Physical readiness evidence is an atomic refinement boundary here.
|
|
MarkNetworkReady(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ HostCoordinatorAlive(d)
|
|
/\ RuntimeSupervisorAlive(d)
|
|
/\ supervisorLease[d] = "Held"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ sandboxState[d] = "Ready"
|
|
/\ attachedRunscProc[d] = "Alive"
|
|
/\ runtimeCausalEdge[d] = "Armed"
|
|
/\ durableIntent[d]["sandbox"]
|
|
/\ durableIntent[d]["network"]
|
|
/\ helperProc[d] = "Alive"
|
|
/\ durableIntent[d]["helper"]
|
|
/\ ~networkReady[d]
|
|
/\ networkReady' = [networkReady 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, durableIntent, pathMismatch,
|
|
genCoordinatorId, genSidecarId, genSandboxId, preparedLowerLeased,
|
|
helperProc
|
|
>>
|
|
|
|
\* Helper-only hard loss: SC remains present; network readiness withdrawn.
|
|
HardLoseConnectivityHelper(d) ==
|
|
\* Helper-only loss after publish (degraded net). Mid-start helper loss is
|
|
\* covered by failing the generation via other hard-loss paths.
|
|
/\ domainPhase[d] = "Ready"
|
|
/\ helperProc[d] = "Alive"
|
|
/\ ConsumeRuntimeFault(d)
|
|
/\ helperProc' = [helperProc EXCEPT ![d] = "Dead"]
|
|
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
|
|
/\ UNCHANGED <<
|
|
domainPhase, stateAnchorState, sidecarState, sandboxState, trustReady,
|
|
lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning, domainLockHeld,
|
|
hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
|
|
runtimeCausalEdge, supervisorLease,
|
|
domainGeneration, durableDecision, durableIntent, pathMismatch,
|
|
genCoordinatorId, genSidecarId, genSandboxId, preparedLowerLeased
|
|
>>
|
|
|
|
\* Refuse reclaim of prepared lower while a generation lease is held.
|
|
RefusePreparedLowerReclaim(d) ==
|
|
/\ preparedLowerLeased[d]
|
|
/\ UNCHANGED vars
|
|
|
|
DomainServiceProgress(d) ==
|
|
\/ CreateTrustAnchor(d)
|
|
\/ StartRuntimeSupervisor(d)
|
|
\/ LeasePreparedLower(d)
|
|
\/ MountStateAnchor(d)
|
|
\/ StartSidecar(d)
|
|
\/ StartConnectivityHelper(d)
|
|
\/ ArmRuntimeCausalEdge(d)
|
|
\/ StartSandbox(d)
|
|
\/ MarkNetworkReady(d)
|
|
\/ PublishDomain(d)
|
|
\/ BeginTeardown(d)
|
|
\/ StopSandbox(d)
|
|
\/ StopSidecar(d)
|
|
\/ UnmountStateAnchor(d)
|
|
\/ ReleasePreparedLowerLease(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)
|
|
\/ RecoverPreparedLowerLease(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)
|
|
\/ HardLoseConnectivityHelper(d)
|
|
\/ RefusePreparedLowerReclaim(d)
|
|
|
|
SessionProgress(s) ==
|
|
\/ StartNewDomain(s)
|
|
\/ StartReadySession(s)
|
|
\/ WaitForDomain(s)
|
|
\/ RestartWaitingDomain(s)
|
|
\/ AdvanceWaitingSession(s)
|
|
\/ RejectConfigurationMismatch(s)
|
|
\/ RegisterSession(s)
|
|
|
|
SessionTerminalProgress(s) ==
|
|
\/ BeginSessionTerminal(s)
|
|
\/ CommitSessionTerminal(s)
|
|
\/ DisconnectCleanSession(s)
|
|
\/ DisconnectLiveSessionTerminal(s)
|
|
\/ CompleteSessionTerminal(s)
|
|
\/ ExitSessionTerminalBeforeGuestIdentity(s)
|
|
\/ RetainFailedSessionTerminal(s)
|
|
\/ CleanKnownSessionTerminal(s)
|
|
\/ BootstrapCleanSessionTerminalAfterRuntimeAbsence(s)
|
|
|
|
RequestProgress(r) ==
|
|
\/ AutoApprove(r)
|
|
\/ QueuePrompt(r)
|
|
\/ BeginPrompt(r)
|
|
\/ (\E cmd \in Commands : DeveloperApprove(r, cmd))
|
|
\/ DeveloperDeny(r)
|
|
\/ StartHostExecution(r)
|
|
\/ CompleteHostExecution(r)
|
|
\/ TimeoutRequest(r)
|
|
\/ CancelRequest(r)
|
|
\/ FailHostExecution(r)
|
|
\/ DeliverResult(r)
|
|
|
|
BaseNext ==
|
|
\/ (\E s \in Sessions :
|
|
StartNewDomain(s) \/ StartReadySession(s) \/ WaitForDomain(s) \/
|
|
RestartWaitingDomain(s) \/ AdvanceWaitingSession(s) \/
|
|
RejectConfigurationMismatch(s) \/
|
|
RegisterSession(s))
|
|
\/ (\E d \in Domains :
|
|
DomainServiceProgress(d) \/ FailDomain(d))
|
|
\/ (\E d \in Domains :
|
|
RuntimePhysicalInterleaving(d))
|
|
\/ (\E r \in Requests :
|
|
ReceiveEscalation(r) \/ RequestProgress(r))
|
|
|
|
Next ==
|
|
\/ /\ BaseNext
|
|
/\ UNCHANGED terminalVars
|
|
\/ (\E s \in Sessions : SessionTerminalProgress(s))
|
|
\/ (\E s \in Sessions : TerminalInteraction(s))
|
|
|
|
\* Resume transitions are enabled but not weakly fair: permanent stop is a
|
|
\* modeled stuck state for safety, not a guaranteed progress path.
|
|
SafetySpec ==
|
|
/\ Init
|
|
/\ [][Next]_vars
|
|
|
|
Spec ==
|
|
/\ SafetySpec
|
|
/\ \A d \in Domains :
|
|
WF_vars(DomainServiceProgress(d) /\ UNCHANGED terminalVars)
|
|
/\ \A s \in Sessions :
|
|
WF_vars(SessionProgress(s) /\ UNCHANGED terminalVars)
|
|
/\ \A s \in Sessions : WF_vars(SessionTerminalProgress(s))
|
|
/\ \A r \in Requests :
|
|
WF_vars(RequestProgress(r) /\ UNCHANGED terminalVars)
|
|
|
|
(***************************************************************************
|
|
Safety properties
|
|
***************************************************************************)
|
|
|
|
TypeOK ==
|
|
/\ TerminalEventPlan \in [Sessions -> Seq(TerminalEventKinds)]
|
|
/\ TerminalAuthorityPlan \in [Sessions -> Seq(TerminalAuthorities)]
|
|
/\ TerminalAdministrativeAuthorityValid \in [Sessions -> Seq(BOOLEAN)]
|
|
/\ \A s \in Sessions :
|
|
/\ Len(TerminalEventPlan[s]) = Len(TerminalAuthorityPlan[s])
|
|
/\ Len(TerminalEventPlan[s]) =
|
|
Len(TerminalAdministrativeAuthorityValid[s])
|
|
/\ TerminalRoutingFault \in TerminalRoutingFaults
|
|
/\ (TerminalRoutingFault = "CrossSession" => Cardinality(Sessions) > 1)
|
|
/\ 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]
|
|
/\ durableIntent \in [Domains -> [DurableRoles -> BOOLEAN]]
|
|
/\ genCoordinatorId \in [Domains -> Identities]
|
|
/\ genSidecarId \in [Domains -> Identities]
|
|
/\ genSandboxId \in [Domains -> Identities]
|
|
/\ networkReady \in [Domains -> BOOLEAN]
|
|
/\ preparedLowerLeased \in [Domains -> BOOLEAN]
|
|
/\ helperProc \in [Domains -> HelperProcStates]
|
|
/\ pathMismatch \in [Domains -> BOOLEAN]
|
|
/\ sessionTerminalState \in [Sessions -> SessionTerminalStates]
|
|
/\ sessionPtyOpen \in [Sessions -> BOOLEAN]
|
|
/\ sessionExecPresent \in [Sessions -> BOOLEAN]
|
|
/\ sessionGuestKnown \in [Sessions -> BOOLEAN]
|
|
/\ \A s \in Sessions :
|
|
terminalEventIndex[s] \in 1..(Len(TerminalEventPlan[s]) + 1)
|
|
/\ \A s \in Sessions :
|
|
terminalLastEventId[s] \in 0..Len(TerminalEventPlan[s])
|
|
/\ terminalLastEvent \in [Sessions -> TerminalEventKinds \cup {"None"}]
|
|
/\ terminalLastSourceSession \in [Sessions -> Sessions \cup {NoSession}]
|
|
/\ terminalLastAuthority \in [Sessions -> TerminalAuthorities]
|
|
/\ terminalLastAdministrativeAuthorityValid \in [Sessions -> BOOLEAN]
|
|
/\ terminalLastDisposition \in [Sessions -> TerminalDispositions]
|
|
/\ terminalLastDestination \in [Sessions -> Sessions \cup {NoSession}]
|
|
/\ terminalLastTarget \in [Sessions -> TerminalTargets]
|
|
/\ terminalLastByteDeliveries \in [Sessions -> 0..1]
|
|
/\ terminalLastSignalDeliveries \in [Sessions -> 0..1]
|
|
/\ terminalLastLocalDeliveries \in [Sessions -> 0..1]
|
|
/\ terminalLastMetadataDeliveries \in [Sessions -> 0..1]
|
|
/\ sessionClientSuspended \in [Sessions -> BOOLEAN]
|
|
/\ sessionTerminalTransportState \in [Sessions -> TerminalTransportStates]
|
|
|
|
SessionTerminalPhysicalConsistency ==
|
|
\A s \in Sessions :
|
|
/\ (sessionTerminalState[s] = "Clean" =>
|
|
/\ ~sessionPtyOpen[s]
|
|
/\ ~sessionExecPresent[s]
|
|
/\ ~sessionGuestKnown[s])
|
|
/\ (sessionTerminalState[s] = "Intent" =>
|
|
/\ sessionPtyOpen[s]
|
|
/\ sessionExecPresent[s]
|
|
/\ ~sessionGuestKnown[s])
|
|
/\ (sessionTerminalState[s] = "Running" =>
|
|
/\ sessionPtyOpen[s]
|
|
/\ sessionExecPresent[s]
|
|
/\ sessionGuestKnown[s])
|
|
/\ (sessionPtyOpen[s] => sessionTerminalState[s] # "Clean")
|
|
/\ (sessionExecPresent[s] => sessionTerminalState[s] # "Clean")
|
|
|
|
ConfigurationConfinement ==
|
|
\A d \in Domains : domainPhase[d] # "Absent" => ConfigSafe[d]
|
|
|
|
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"
|
|
/\ durableIntent[d]["network"]
|
|
/\ durableIntent[d]["sandbox"]
|
|
|
|
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")
|
|
|
|
HostCoordinatorRequiresDomainOwnership ==
|
|
\A d \in Domains :
|
|
hostCoordinatorProc[d] # "Absent" =>
|
|
/\ domainPhase[d] # "Absent"
|
|
/\ domainLockHeld[d]
|
|
|
|
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] \notin {"Unused"} \cup TerminalRequestPhases =>
|
|
/\ RequestCredentialValid[r]
|
|
/\ RequestSignatureValid[r]
|
|
/\ RequestIdentityTupleMatches(r)
|
|
|
|
RuntimeRoleIdentitySeparation ==
|
|
/\ \A d \in Domains :
|
|
Cardinality({
|
|
genCoordinatorId[d],
|
|
genSidecarId[d],
|
|
genSandboxId[d]
|
|
}) = 3
|
|
/\ \A s \in Sessions :
|
|
LET d == Dom(s) IN
|
|
SessionCliIdentity[s] \notin {
|
|
genCoordinatorId[d],
|
|
genSidecarId[d],
|
|
genSandboxId[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"
|
|
|
|
ObservedTerminalDelivery(s) ==
|
|
TerminalDelivery(
|
|
terminalLastDisposition[s],
|
|
terminalLastDestination[s],
|
|
terminalLastTarget[s],
|
|
terminalLastByteDeliveries[s],
|
|
terminalLastSignalDeliveries[s],
|
|
terminalLastLocalDeliveries[s],
|
|
terminalLastMetadataDeliveries[s])
|
|
|
|
TerminalInteractionAuthoritySeparated ==
|
|
\A s \in Sessions :
|
|
/\ terminalEventIndex[s] = terminalLastEventId[s] + 1
|
|
/\ IF terminalLastEventId[s] = 0
|
|
THEN /\ terminalLastEvent[s] = "None"
|
|
/\ terminalLastSourceSession[s] = NoSession
|
|
/\ terminalLastAuthority[s] = "None"
|
|
/\ ~terminalLastAdministrativeAuthorityValid[s]
|
|
/\ ObservedTerminalDelivery(s) = NoTerminalDelivery
|
|
ELSE LET event == TerminalEventPlan[s][terminalLastEventId[s]]
|
|
authority == TerminalAuthorityPlan[s][terminalLastEventId[s]]
|
|
administrativeAuthorityValid ==
|
|
TerminalAdministrativeAuthorityValid[s][terminalLastEventId[s]]
|
|
IN /\ terminalLastEvent[s] = event
|
|
/\ terminalLastSourceSession[s] = s
|
|
/\ terminalLastAuthority[s] = authority
|
|
/\ terminalLastAdministrativeAuthorityValid[s] =
|
|
administrativeAuthorityValid
|
|
/\ ObservedTerminalDelivery(s) =
|
|
ExpectedTerminalDelivery(
|
|
s, event, authority, administrativeAuthorityValid)
|
|
|
|
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)
|
|
|
|
DurableIntentBeforeSandboxReady ==
|
|
\A d \in Domains :
|
|
sandboxState[d] = "Ready" => durableIntent[d]["sandbox"]
|
|
|
|
\* Published generation document decision tracks authenticated publication.
|
|
DurableDecisionPublicationConsistent ==
|
|
\A d \in Domains :
|
|
/\ (d \in published => durableDecision[d] = "Published")
|
|
/\ (durableDecision[d] = "Published" =>
|
|
/\ durableIntent[d]["sandbox"]
|
|
/\ durableIntent[d]["network"])
|
|
\* Live helper implies attested readiness; helper-only loss may clear
|
|
\* networkReady while durable network intent remains.
|
|
/\ (d \in published /\ helperProc[d] = "Alive" => networkReady[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
|
|
|
|
|
|
NetworkReadyBeforePublish ==
|
|
\A d \in Domains :
|
|
\* Publication requires readiness; helper-only loss may clear networkReady
|
|
\* while the Domain remains published (degraded connectivity).
|
|
durableDecision[d] = "Published" => durableIntent[d]["network"]
|
|
|
|
PreparedLowerLeaseBeforeMount ==
|
|
\A d \in Domains :
|
|
stateAnchorState[d] = "Mounted" =>
|
|
/\ preparedLowerLeased[d]
|
|
/\ durableIntent[d]["prepared_lower"]
|
|
|
|
LeaseLossUnmountRetainsPreparedLowerLeaseAction ==
|
|
\A d \in Domains :
|
|
LeaseTeardownUnmountStateAnchor(d) => preparedLowerLeased'[d]
|
|
|
|
LeaseLossUnmountRetainsPreparedLowerLease ==
|
|
[][LeaseLossUnmountRetainsPreparedLowerLeaseAction]_vars
|
|
|
|
HelperUnderSupervisor ==
|
|
\A d \in Domains :
|
|
helperProc[d] = "Alive" =>
|
|
/\ ProcessPresent(runtimeSupervisorProc[d])
|
|
/\ supervisorLease[d] \in {"Held", "Lost"}
|
|
|
|
GenerationScopedIdentitiesDistinct ==
|
|
\A d \in Domains :
|
|
domainPhase[d] # "Absent" =>
|
|
Cardinality({
|
|
genCoordinatorId[d],
|
|
genSidecarId[d],
|
|
genSandboxId[d]
|
|
}) = 3
|
|
|
|
MultiRoleDurableIntent ==
|
|
\A d \in Domains :
|
|
/\ (stateAnchorState[d] = "Mounted" => durableIntent[d]["anchor"])
|
|
/\ (networkReady[d] => durableIntent[d]["network"])
|
|
/\ (helperProc[d] = "Alive" => durableIntent[d]["helper"])
|
|
|
|
NetworkReadinessBoundToSandbox ==
|
|
\A d \in Domains :
|
|
networkReady[d] =>
|
|
/\ sandboxState[d] = "Ready"
|
|
/\ ProcessPresent(attachedRunscProc[d])
|
|
/\ runtimeCausalEdge[d] = "Armed"
|
|
/\ helperProc[d] = "Alive"
|
|
|
|
Safety ==
|
|
/\ TypeOK
|
|
/\ SessionTerminalPhysicalConsistency
|
|
/\ ConfigurationConfinement
|
|
/\ SandboxNamespaceIsolation
|
|
/\ OrderedNetworkStartup
|
|
/\ PublishedDomainsReady
|
|
/\ DomainLockLifetime
|
|
/\ RuntimeCausalEdgeArmedBeforeSandbox
|
|
/\ RuntimeCausalEdgeOwnerPresent
|
|
/\ SandboxRunningImpliesCoordinatorPresent
|
|
/\ PublishedRuntimeAuthorityPresent
|
|
/\ SupervisorLeaseConsistency
|
|
/\ RuntimeResourceOwnership
|
|
/\ CoordinatorPhysicalConsistency
|
|
/\ HostCoordinatorRequiresDomainOwnership
|
|
/\ NoVanishPresentRuntime
|
|
/\ OrderedLeaseTeardown
|
|
/\ DomainGenerationBounds
|
|
/\ DurableIntentBeforeSandboxReady
|
|
/\ DurableDecisionPublicationConsistent
|
|
/\ PathMismatchNotAdopted
|
|
/\ ExclusiveBootstrapOwnership
|
|
/\ TeardownNotJoinable
|
|
/\ RegisteredSessionsConnected
|
|
/\ AttachedSessionsValid
|
|
/\ AuthenticatedRequestsOnly
|
|
/\ RuntimeRoleIdentitySeparation
|
|
/\ RegisteredSessionIdentityUniqueness
|
|
/\ LiveRequestIdentityAuthorized
|
|
/\ DeveloperApprovalAuthenticated
|
|
/\ HostExecutionAuthorized
|
|
/\ AutoApprovalNoShell
|
|
/\ TerminalIsolation
|
|
/\ TerminalInteractionAuthoritySeparated
|
|
/\ NoOrphanHostProcess
|
|
/\ StateAnchorOwnership
|
|
/\ FailedDomainIsolation
|
|
/\ OrderedFailureRecovery
|
|
/\ ResultDeliveryStateConsistent
|
|
/\ NetworkReadinessBoundToSandbox
|
|
|
|
TerminalEventAdvanced(s) ==
|
|
/\ terminalLastEventId'[s] = terminalEventIndex[s]
|
|
/\ terminalEventIndex'[s] = terminalEventIndex[s] + 1
|
|
|
|
TerminalSessionProjection(s) == <<
|
|
sessionPhase[s], terminalRoute[s], connectionState[s], activeRequest[s],
|
|
sessionTerminalState[s], sessionPtyOpen[s], sessionExecPresent[s],
|
|
sessionGuestKnown[s], terminalEventIndex[s], terminalLastEventId[s],
|
|
terminalLastEvent[s], terminalLastSourceSession[s],
|
|
terminalLastAuthority[s], terminalLastAdministrativeAuthorityValid[s],
|
|
terminalLastDisposition[s],
|
|
terminalLastDestination[s], terminalLastTarget[s],
|
|
terminalLastByteDeliveries[s], terminalLastSignalDeliveries[s],
|
|
terminalLastLocalDeliveries[s], terminalLastMetadataDeliveries[s],
|
|
sessionClientSuspended[s], sessionTerminalTransportState[s]
|
|
>>
|
|
|
|
DomainRuntimeProjection(d) == <<
|
|
domainPhase[d], stateAnchorState[d], sidecarState[d], sandboxState[d],
|
|
trustReady[d], domainLockHeld[d], hostCoordinatorProc[d],
|
|
runtimeSupervisorProc[d], attachedRunscProc[d], runtimeCausalEdge[d],
|
|
supervisorLease[d], domainGeneration[d], durableDecision[d],
|
|
durableIntent[d], genCoordinatorId[d], genSidecarId[d], genSandboxId[d],
|
|
networkReady[d], preparedLowerLeased[d], helperProc[d]
|
|
>>
|
|
|
|
TerminalPeerIsolationAction ==
|
|
\A s \in Sessions :
|
|
TerminalEventAdvanced(s) =>
|
|
\A t \in Sessions \ {s} : UNCHANGED TerminalSessionProjection(t)
|
|
|
|
TerminalPeerIsolation ==
|
|
[][TerminalPeerIsolationAction]_vars
|
|
|
|
LocalTerminalControlKinds == {
|
|
"LocalSuspend", "LocalResume", "LocalDisconnect", "HostSignal"
|
|
}
|
|
|
|
TerminalLocalControlPreservesDomainAction ==
|
|
\A s \in Sessions :
|
|
/\ TerminalEventAdvanced(s)
|
|
/\ CurrentTerminalEvent(s) \in LocalTerminalControlKinds
|
|
/\ \E t \in Sessions \ {s} : connectionState[t] = "Connected"
|
|
=> UNCHANGED DomainRuntimeProjection(Dom(s))
|
|
|
|
TerminalLocalControlPreservesDomain ==
|
|
[][TerminalLocalControlPreservesDomainAction]_vars
|
|
|
|
LocalTerminationAvailableWhileTransportBlocked ==
|
|
\A s \in Sessions :
|
|
/\ sessionTerminalTransportState[s] = "Blocked"
|
|
/\ sessionPhase[s] = "Attached"
|
|
/\ connectionState[s] = "Connected"
|
|
/\ sessionTerminalState[s] \in {"Intent", "Running"}
|
|
/\ TerminalEventAvailable(s)
|
|
/\ CurrentTerminalEvent(s) \in {"LocalDisconnect", "HostSignal"}
|
|
=> ENABLED DisconnectTerminalFromLocalAuthority(
|
|
s, CurrentTerminalEvent(s))
|
|
|
|
(***************************************************************************
|
|
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")
|
|
|
|
PreIdentityExitEventuallyCleansAfterRuntimeAbsence ==
|
|
\A s \in Sessions :
|
|
/\ sessionPhase[s] = "Closed"
|
|
/\ sessionTerminalState[s] = "ReleaseIntent"
|
|
/\ ~sessionGuestKnown[s]
|
|
/\ ~sessionPtyOpen[s]
|
|
/\ ~sessionExecPresent[s]
|
|
/\ RuntimeAbsentForTerminal(Dom(s))
|
|
~> \/ sessionTerminalState[s] = "Clean"
|
|
\/ <>[](~HostCoordinatorAlive(Dom(s)))
|
|
|
|
=============================================================================
|