490 lines
15 KiB
Text
490 lines
15 KiB
Text
|
------------------------ MODULE IgnoredWorkspaceRouting ------------------------
|
||
|
|
EXTENDS Naturals, TLC
|
||
|
|
|
||
|
|
(***************************************************************************
|
||
|
|
Generation-level safety model for ignored-workspace routing policy admission,
|
||
|
|
host-priority backing transitions, crash continuation, and unsafe controls.
|
||
|
|
Path traversal, object-copy durability, and Git encoding are refinements.
|
||
|
|
***************************************************************************)
|
||
|
|
|
||
|
|
CONSTANTS
|
||
|
|
Correct,
|
||
|
|
LiveReconcile,
|
||
|
|
InitialHostImport,
|
||
|
|
StaleOverlay,
|
||
|
|
IsolatedExport,
|
||
|
|
EagerAdmission,
|
||
|
|
UnstableClone,
|
||
|
|
Mode
|
||
|
|
|
||
|
|
Modes == {
|
||
|
|
Correct,
|
||
|
|
LiveReconcile,
|
||
|
|
InitialHostImport,
|
||
|
|
StaleOverlay,
|
||
|
|
IsolatedExport,
|
||
|
|
EagerAdmission,
|
||
|
|
UnstableClone
|
||
|
|
}
|
||
|
|
Policies == {"Host", "Isolated"}
|
||
|
|
SealedPolicies == Policies \cup {"None"}
|
||
|
|
Phases == {
|
||
|
|
"Down",
|
||
|
|
"Ready",
|
||
|
|
"CloneCopying",
|
||
|
|
"CloneInstalled",
|
||
|
|
"DeletePending",
|
||
|
|
"DeleteInstalled"
|
||
|
|
}
|
||
|
|
Payloads == {"Absent", "HostA", "HostB", "SandboxA", "Partial"}
|
||
|
|
Transitions == {"None", "Initial", "Same", "HostToIsolated", "IsolatedToHost"}
|
||
|
|
|
||
|
|
ASSUME Mode \in Modes
|
||
|
|
|
||
|
|
VARIABLES
|
||
|
|
phase,
|
||
|
|
online,
|
||
|
|
sourcePolicy,
|
||
|
|
sealedPolicy,
|
||
|
|
admittedPolicy,
|
||
|
|
targetPolicy,
|
||
|
|
generation,
|
||
|
|
host,
|
||
|
|
isolated,
|
||
|
|
staging,
|
||
|
|
cloneSource,
|
||
|
|
intent,
|
||
|
|
lastTransition,
|
||
|
|
hostClassDisclosed,
|
||
|
|
liveRouteChanged,
|
||
|
|
initialHostImported,
|
||
|
|
staleOverlayRetained,
|
||
|
|
isolatedExported,
|
||
|
|
incompleteAdmission,
|
||
|
|
unstableCloneAdmitted
|
||
|
|
|
||
|
|
vars == <<
|
||
|
|
phase,
|
||
|
|
online,
|
||
|
|
sourcePolicy,
|
||
|
|
sealedPolicy,
|
||
|
|
admittedPolicy,
|
||
|
|
targetPolicy,
|
||
|
|
generation,
|
||
|
|
host,
|
||
|
|
isolated,
|
||
|
|
staging,
|
||
|
|
cloneSource,
|
||
|
|
intent,
|
||
|
|
lastTransition,
|
||
|
|
hostClassDisclosed,
|
||
|
|
liveRouteChanged,
|
||
|
|
initialHostImported,
|
||
|
|
staleOverlayRetained,
|
||
|
|
isolatedExported,
|
||
|
|
incompleteAdmission,
|
||
|
|
unstableCloneAdmitted
|
||
|
|
>>
|
||
|
|
|
||
|
|
SafetyFlags == <<
|
||
|
|
liveRouteChanged,
|
||
|
|
initialHostImported,
|
||
|
|
staleOverlayRetained,
|
||
|
|
isolatedExported,
|
||
|
|
incompleteAdmission,
|
||
|
|
unstableCloneAdmitted
|
||
|
|
>>
|
||
|
|
|
||
|
|
TypeOK ==
|
||
|
|
/\ phase \in Phases
|
||
|
|
/\ online \in BOOLEAN
|
||
|
|
/\ sourcePolicy \in Policies
|
||
|
|
/\ sealedPolicy \in SealedPolicies
|
||
|
|
/\ admittedPolicy \in SealedPolicies
|
||
|
|
/\ targetPolicy \in SealedPolicies
|
||
|
|
/\ generation \in 0..3
|
||
|
|
/\ host \in Payloads
|
||
|
|
/\ isolated \in Payloads
|
||
|
|
/\ staging \in Payloads
|
||
|
|
/\ cloneSource \in Payloads
|
||
|
|
/\ intent \in BOOLEAN
|
||
|
|
/\ lastTransition \in Transitions
|
||
|
|
/\ hostClassDisclosed \in BOOLEAN
|
||
|
|
/\ liveRouteChanged \in BOOLEAN
|
||
|
|
/\ initialHostImported \in BOOLEAN
|
||
|
|
/\ staleOverlayRetained \in BOOLEAN
|
||
|
|
/\ isolatedExported \in BOOLEAN
|
||
|
|
/\ incompleteAdmission \in BOOLEAN
|
||
|
|
/\ unstableCloneAdmitted \in BOOLEAN
|
||
|
|
|
||
|
|
Init ==
|
||
|
|
/\ phase = "Down"
|
||
|
|
/\ online = TRUE
|
||
|
|
/\ sourcePolicy \in Policies
|
||
|
|
/\ sealedPolicy = "None"
|
||
|
|
/\ admittedPolicy = "None"
|
||
|
|
/\ targetPolicy = "None"
|
||
|
|
/\ generation = 0
|
||
|
|
/\ host = "HostA"
|
||
|
|
/\ isolated = "Absent"
|
||
|
|
/\ staging = "Absent"
|
||
|
|
/\ cloneSource = "Absent"
|
||
|
|
/\ intent = FALSE
|
||
|
|
/\ lastTransition = "None"
|
||
|
|
/\ hostClassDisclosed = FALSE
|
||
|
|
/\ liveRouteChanged = FALSE
|
||
|
|
/\ initialHostImported = FALSE
|
||
|
|
/\ staleOverlayRetained = FALSE
|
||
|
|
/\ isolatedExported = FALSE
|
||
|
|
/\ incompleteAdmission = FALSE
|
||
|
|
/\ unstableCloneAdmitted = FALSE
|
||
|
|
|
||
|
|
InitialStartHost ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "Down"
|
||
|
|
/\ generation = 0
|
||
|
|
/\ sealedPolicy = "None"
|
||
|
|
/\ sourcePolicy = "Host"
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ sealedPolicy' = "Host"
|
||
|
|
/\ admittedPolicy' = "Host"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ generation' = 1
|
||
|
|
/\ isolated' = "Absent"
|
||
|
|
/\ lastTransition' = "Initial"
|
||
|
|
/\ hostClassDisclosed' = TRUE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, host, staging, cloneSource, intent, SafetyFlags>>
|
||
|
|
|
||
|
|
InitialStartIsolated ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "Down"
|
||
|
|
/\ generation = 0
|
||
|
|
/\ sealedPolicy = "None"
|
||
|
|
/\ sourcePolicy = "Isolated"
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ sealedPolicy' = "Isolated"
|
||
|
|
/\ admittedPolicy' = "Isolated"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ generation' = 1
|
||
|
|
/\ isolated' = IF Mode = InitialHostImport THEN host ELSE "Absent"
|
||
|
|
/\ initialHostImported' = (Mode = InitialHostImport)
|
||
|
|
/\ lastTransition' = "Initial"
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, host, staging, cloneSource, intent,
|
||
|
|
hostClassDisclosed, liveRouteChanged, staleOverlayRetained,
|
||
|
|
isolatedExported, incompleteAdmission, unstableCloneAdmitted>>
|
||
|
|
|
||
|
|
MutateRoutingInput ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "Ready"
|
||
|
|
/\ sourcePolicy' = IF sourcePolicy = "Host" THEN "Isolated" ELSE "Host"
|
||
|
|
/\ sealedPolicy' = IF Mode = LiveReconcile THEN sourcePolicy' ELSE sealedPolicy
|
||
|
|
/\ liveRouteChanged' = (liveRouteChanged \/ (Mode = LiveReconcile))
|
||
|
|
/\ UNCHANGED <<phase, online, admittedPolicy, targetPolicy, generation, host, isolated,
|
||
|
|
staging, cloneSource, intent, lastTransition,
|
||
|
|
hostClassDisclosed, initialHostImported,
|
||
|
|
staleOverlayRetained, isolatedExported,
|
||
|
|
incompleteAdmission, unstableCloneAdmitted>>
|
||
|
|
|
||
|
|
SandboxWrite ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "Ready"
|
||
|
|
/\ IF sealedPolicy = "Host"
|
||
|
|
THEN /\ host' = IF host = "HostA" THEN "HostB" ELSE "HostA"
|
||
|
|
/\ isolated' = isolated
|
||
|
|
ELSE /\ isolated' = "SandboxA"
|
||
|
|
/\ host' = host
|
||
|
|
/\ UNCHANGED <<phase, online, sourcePolicy, sealedPolicy, admittedPolicy, targetPolicy,
|
||
|
|
generation, staging, cloneSource, intent, lastTransition,
|
||
|
|
hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
HostWrite ==
|
||
|
|
/\ online
|
||
|
|
/\ host' = IF host = "HostA" THEN "HostB" ELSE "HostA"
|
||
|
|
/\ UNCHANGED <<phase, online, sourcePolicy, sealedPolicy, admittedPolicy, targetPolicy,
|
||
|
|
generation, isolated, staging, cloneSource, intent,
|
||
|
|
lastTransition, hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
Stop ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "Ready"
|
||
|
|
/\ generation < 3
|
||
|
|
/\ phase' = "Down"
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, sealedPolicy, admittedPolicy, targetPolicy, generation,
|
||
|
|
host, isolated, staging, cloneSource, intent,
|
||
|
|
lastTransition, hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
RestartSamePolicy ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "Down"
|
||
|
|
/\ sealedPolicy \in Policies
|
||
|
|
/\ sourcePolicy = sealedPolicy
|
||
|
|
/\ generation < 3
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ admittedPolicy' = sealedPolicy
|
||
|
|
/\ generation' = generation + 1
|
||
|
|
/\ lastTransition' = "Same"
|
||
|
|
/\ hostClassDisclosed' = (hostClassDisclosed \/ (sealedPolicy = "Host"))
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, sealedPolicy, targetPolicy, host,
|
||
|
|
isolated, staging, cloneSource, intent, SafetyFlags>>
|
||
|
|
|
||
|
|
BeginHostToIsolated ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "Down"
|
||
|
|
/\ sealedPolicy = "Host"
|
||
|
|
/\ sourcePolicy = "Isolated"
|
||
|
|
/\ generation < 3
|
||
|
|
/\ phase' = "CloneCopying"
|
||
|
|
/\ targetPolicy' = "Isolated"
|
||
|
|
/\ staging' = "Partial"
|
||
|
|
/\ cloneSource' = host
|
||
|
|
/\ intent' = TRUE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, sealedPolicy, admittedPolicy, generation, host,
|
||
|
|
isolated, lastTransition, hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
FinishClone ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "CloneCopying"
|
||
|
|
/\ intent
|
||
|
|
/\ staging = "Partial"
|
||
|
|
/\ host = cloneSource
|
||
|
|
/\ staging' = cloneSource
|
||
|
|
/\ UNCHANGED <<phase, online, sourcePolicy, sealedPolicy, admittedPolicy, targetPolicy,
|
||
|
|
generation, host, isolated, cloneSource, intent,
|
||
|
|
lastTransition, hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
InstallClone ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "CloneCopying"
|
||
|
|
/\ intent
|
||
|
|
/\ staging = cloneSource
|
||
|
|
/\ host = cloneSource
|
||
|
|
/\ phase' = "CloneInstalled"
|
||
|
|
/\ isolated' = cloneSource
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, sealedPolicy, admittedPolicy, targetPolicy, generation,
|
||
|
|
host, staging, cloneSource, intent, lastTransition,
|
||
|
|
hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
PublishClone ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "CloneInstalled"
|
||
|
|
/\ intent
|
||
|
|
/\ isolated = cloneSource
|
||
|
|
/\ host = cloneSource
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ sealedPolicy' = "Isolated"
|
||
|
|
/\ admittedPolicy' = "Isolated"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ generation' = generation + 1
|
||
|
|
/\ staging' = "Absent"
|
||
|
|
/\ cloneSource' = "Absent"
|
||
|
|
/\ intent' = FALSE
|
||
|
|
/\ lastTransition' = "HostToIsolated"
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, host, isolated,
|
||
|
|
hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
AbortUnstableClone ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "CloneCopying"
|
||
|
|
/\ intent
|
||
|
|
/\ host # cloneSource
|
||
|
|
/\ phase' = "Down"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ staging' = "Absent"
|
||
|
|
/\ cloneSource' = "Absent"
|
||
|
|
/\ intent' = FALSE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, sealedPolicy, admittedPolicy, generation, host,
|
||
|
|
isolated, lastTransition, hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
UnsafeEagerAdmission ==
|
||
|
|
/\ Mode = EagerAdmission
|
||
|
|
/\ online
|
||
|
|
/\ phase = "CloneCopying"
|
||
|
|
/\ intent
|
||
|
|
/\ staging = "Partial"
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ sealedPolicy' = "Isolated"
|
||
|
|
/\ admittedPolicy' = "Isolated"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ generation' = generation + 1
|
||
|
|
/\ intent' = FALSE
|
||
|
|
/\ lastTransition' = "HostToIsolated"
|
||
|
|
/\ incompleteAdmission' = TRUE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, host, isolated, staging, cloneSource,
|
||
|
|
hostClassDisclosed, liveRouteChanged, initialHostImported,
|
||
|
|
staleOverlayRetained, isolatedExported,
|
||
|
|
unstableCloneAdmitted>>
|
||
|
|
|
||
|
|
UnsafePublishUnstableClone ==
|
||
|
|
/\ Mode = UnstableClone
|
||
|
|
/\ online
|
||
|
|
/\ phase = "CloneCopying"
|
||
|
|
/\ intent
|
||
|
|
/\ host # cloneSource
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ sealedPolicy' = "Isolated"
|
||
|
|
/\ admittedPolicy' = "Isolated"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ generation' = generation + 1
|
||
|
|
/\ isolated' = cloneSource
|
||
|
|
/\ staging' = "Absent"
|
||
|
|
/\ cloneSource' = "Absent"
|
||
|
|
/\ intent' = FALSE
|
||
|
|
/\ lastTransition' = "HostToIsolated"
|
||
|
|
/\ unstableCloneAdmitted' = TRUE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, host, hostClassDisclosed,
|
||
|
|
liveRouteChanged, initialHostImported,
|
||
|
|
staleOverlayRetained, isolatedExported,
|
||
|
|
incompleteAdmission>>
|
||
|
|
|
||
|
|
BeginIsolatedToHost ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "Down"
|
||
|
|
/\ sealedPolicy = "Isolated"
|
||
|
|
/\ sourcePolicy = "Host"
|
||
|
|
/\ generation < 3
|
||
|
|
/\ phase' = "DeletePending"
|
||
|
|
/\ targetPolicy' = "Host"
|
||
|
|
/\ intent' = TRUE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, sealedPolicy, admittedPolicy, generation, host,
|
||
|
|
isolated, staging, cloneSource, lastTransition,
|
||
|
|
hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
DeleteIsolated ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "DeletePending"
|
||
|
|
/\ intent
|
||
|
|
/\ phase' = "DeleteInstalled"
|
||
|
|
/\ isolated' = "Absent"
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, sealedPolicy, admittedPolicy, targetPolicy, generation,
|
||
|
|
host, staging, cloneSource, intent, lastTransition,
|
||
|
|
hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
PublishHost ==
|
||
|
|
/\ online
|
||
|
|
/\ phase = "DeleteInstalled"
|
||
|
|
/\ intent
|
||
|
|
/\ isolated = "Absent"
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ sealedPolicy' = "Host"
|
||
|
|
/\ admittedPolicy' = "Host"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ generation' = generation + 1
|
||
|
|
/\ intent' = FALSE
|
||
|
|
/\ lastTransition' = "IsolatedToHost"
|
||
|
|
/\ hostClassDisclosed' = TRUE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, host, isolated, staging, cloneSource,
|
||
|
|
SafetyFlags>>
|
||
|
|
|
||
|
|
UnsafeRetainStaleOverlay ==
|
||
|
|
/\ Mode = StaleOverlay
|
||
|
|
/\ online
|
||
|
|
/\ phase = "DeletePending"
|
||
|
|
/\ intent
|
||
|
|
/\ isolated # "Absent"
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ sealedPolicy' = "Host"
|
||
|
|
/\ admittedPolicy' = "Host"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ generation' = generation + 1
|
||
|
|
/\ intent' = FALSE
|
||
|
|
/\ lastTransition' = "IsolatedToHost"
|
||
|
|
/\ hostClassDisclosed' = TRUE
|
||
|
|
/\ staleOverlayRetained' = TRUE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, host, isolated, staging, cloneSource,
|
||
|
|
liveRouteChanged, initialHostImported, isolatedExported,
|
||
|
|
incompleteAdmission, unstableCloneAdmitted>>
|
||
|
|
|
||
|
|
UnsafeExportIsolated ==
|
||
|
|
/\ Mode = IsolatedExport
|
||
|
|
/\ online
|
||
|
|
/\ phase = "DeletePending"
|
||
|
|
/\ intent
|
||
|
|
/\ isolated # "Absent"
|
||
|
|
/\ phase' = "Ready"
|
||
|
|
/\ sealedPolicy' = "Host"
|
||
|
|
/\ admittedPolicy' = "Host"
|
||
|
|
/\ targetPolicy' = "None"
|
||
|
|
/\ generation' = generation + 1
|
||
|
|
/\ host' = isolated
|
||
|
|
/\ isolated' = "Absent"
|
||
|
|
/\ intent' = FALSE
|
||
|
|
/\ lastTransition' = "IsolatedToHost"
|
||
|
|
/\ hostClassDisclosed' = TRUE
|
||
|
|
/\ isolatedExported' = TRUE
|
||
|
|
/\ UNCHANGED <<online, sourcePolicy, staging, cloneSource,
|
||
|
|
liveRouteChanged, initialHostImported,
|
||
|
|
staleOverlayRetained, incompleteAdmission,
|
||
|
|
unstableCloneAdmitted>>
|
||
|
|
|
||
|
|
Crash ==
|
||
|
|
/\ online
|
||
|
|
/\ phase \in {
|
||
|
|
"CloneCopying", "CloneInstalled", "DeletePending", "DeleteInstalled"
|
||
|
|
}
|
||
|
|
/\ online' = FALSE
|
||
|
|
/\ UNCHANGED <<phase, sourcePolicy, sealedPolicy, admittedPolicy, targetPolicy, generation,
|
||
|
|
host, isolated, staging, cloneSource, intent,
|
||
|
|
lastTransition, hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
Recover ==
|
||
|
|
/\ ~online
|
||
|
|
/\ online' = TRUE
|
||
|
|
/\ UNCHANGED <<phase, sourcePolicy, sealedPolicy, admittedPolicy, targetPolicy, generation,
|
||
|
|
host, isolated, staging, cloneSource, intent,
|
||
|
|
lastTransition, hostClassDisclosed, SafetyFlags>>
|
||
|
|
|
||
|
|
Next ==
|
||
|
|
\/ InitialStartHost
|
||
|
|
\/ InitialStartIsolated
|
||
|
|
\/ MutateRoutingInput
|
||
|
|
\/ SandboxWrite
|
||
|
|
\/ HostWrite
|
||
|
|
\/ Stop
|
||
|
|
\/ RestartSamePolicy
|
||
|
|
\/ BeginHostToIsolated
|
||
|
|
\/ FinishClone
|
||
|
|
\/ InstallClone
|
||
|
|
\/ PublishClone
|
||
|
|
\/ AbortUnstableClone
|
||
|
|
\/ UnsafeEagerAdmission
|
||
|
|
\/ UnsafePublishUnstableClone
|
||
|
|
\/ BeginIsolatedToHost
|
||
|
|
\/ DeleteIsolated
|
||
|
|
\/ PublishHost
|
||
|
|
\/ UnsafeRetainStaleOverlay
|
||
|
|
\/ UnsafeExportIsolated
|
||
|
|
\/ Crash
|
||
|
|
\/ Recover
|
||
|
|
|
||
|
|
Spec == Init /\ [][Next]_vars
|
||
|
|
|
||
|
|
ReadyHasSealedPolicy == phase = "Ready" => sealedPolicy \in Policies
|
||
|
|
ReadyUsesGenerationPolicy == phase = "Ready" => sealedPolicy = admittedPolicy
|
||
|
|
UndisclosedHostNotImported ==
|
||
|
|
(~hostClassDisclosed /\ phase = "Ready" /\ sealedPolicy = "Isolated")
|
||
|
|
=> isolated \notin {"HostA", "HostB"}
|
||
|
|
DownOrTransitionNotAdmitted == phase # "Ready" => targetPolicy \in SealedPolicies
|
||
|
|
HostRouteHasNoIsolatedOverlay ==
|
||
|
|
(phase = "Ready" /\ sealedPolicy = "Host") => isolated = "Absent"
|
||
|
|
TransitionIntentIsDurable ==
|
||
|
|
phase \in {"CloneCopying", "CloneInstalled", "DeletePending", "DeleteInstalled"}
|
||
|
|
=> intent
|
||
|
|
NoUnsafeOutcome ==
|
||
|
|
/\ ~liveRouteChanged
|
||
|
|
/\ ~initialHostImported
|
||
|
|
/\ ~staleOverlayRetained
|
||
|
|
/\ ~isolatedExported
|
||
|
|
/\ ~incompleteAdmission
|
||
|
|
/\ ~unstableCloneAdmitted
|
||
|
|
|
||
|
|
RoutingSafety ==
|
||
|
|
/\ ReadyHasSealedPolicy
|
||
|
|
/\ ReadyUsesGenerationPolicy
|
||
|
|
/\ UndisclosedHostNotImported
|
||
|
|
/\ DownOrTransitionNotAdmitted
|
||
|
|
/\ HostRouteHasNoIsolatedOverlay
|
||
|
|
/\ TransitionIntentIsDurable
|
||
|
|
/\ NoUnsafeOutcome
|
||
|
|
|
||
|
|
=============================================================================
|
||
|
|
|