Model startup-sealed workspace routing authority

docs/protocol/IgnoredWorkspaceRouting.cfg

@@ -0,0 +1,17 @@
+CONSTANTS
+    Correct = Correct
+    LiveReconcile = LiveReconcile
+    InitialHostImport = InitialHostImport
+    StaleOverlay = StaleOverlay
+    IsolatedExport = IsolatedExport
+    EagerAdmission = EagerAdmission
+    UnstableClone = UnstableClone
+    Mode = Correct
+
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    TypeOK
+    RoutingSafety
+

docs/protocol/IgnoredWorkspaceRouting.tla

@@ -0,0 +1,490 @@
+------------------------ 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
+
+=============================================================================
+