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

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