Model terminal presentation ownership and restoration

docs/protocol/Lazaret.cfg

@@ -51,6 +51,7 @@ CONSTANTS
     TerminalAuthorityPlan <- TerminalNoAuthorityPlanFixture
     TerminalAdministrativeAuthorityValid <-
         TerminalNoAdministrativeAuthorityValidFixture
+    TerminalPresentationPlan <- TerminalNoPresentationPlanFixture
     TerminalRoutingFault = "Correct"
 
 SPECIFICATION Spec
@@ -91,6 +92,7 @@ INVARIANTS
     HostExecutionAuthorized
     AutoApprovalNoShell
     TerminalIsolation
+    TerminalPresentationIsolation
     TerminalInteractionAuthoritySeparated
     LocalTerminationAvailableWhileTransportBlocked
     NoOrphanHostProcess

docs/protocol/Lazaret.tla

@@ -75,6 +75,7 @@ CONSTANTS
     TerminalEventPlan,
     TerminalAuthorityPlan,
     TerminalAdministrativeAuthorityValid,
+    TerminalPresentationPlan,
     TerminalRoutingFault,
     D1,
     S1,
@@ -144,11 +145,14 @@ SessionPhases == {
     "HostExecuting", "Closed", "Failed"
 }
 TerminalRoutes == {"Detached", "Sandbox", "Prompt", "HostProcess"}
+TerminalPresentations == {"Normal", "Alternate"}
+TerminalPresentationOwners == {"None", "Guest", "Trusted"}
 SessionTerminalStates == {"Clean", "Intent", "Running", "ReleaseIntent"}
 TerminalEventKinds == {
     "Keyboard", "ExplicitSignal", "Resize", "Break", "LocalSuspend",
     "LocalResume", "LocalDisconnect", "HostSignal"
 }
+TerminalPresentationEventKinds == {"EnterAlternate", "ExitAlternate"}
 TerminalAuthorities == {
     "None", "Client", "Administrator", "LocalClient", "HostProcess"
 }
@@ -234,6 +238,10 @@ TerminalNoAuthorityPlanFixture ==
     (S1 :> <<>>) @@ (S2 :> <<>>)
 TerminalNoAdministrativeAuthorityValidFixture ==
     (S1 :> <<>>) @@ (S2 :> <<>>)
+TerminalNoPresentationPlanFixture ==
+    (S1 :> <<>>) @@ (S2 :> <<>>)
+TerminalPresentationPlanFixture ==
+    (S1 :> <<>>) @@ (S2 :> <<"EnterAlternate", "ExitAlternate">>)
 TerminalRoutingEventPlanFixture ==
     (S1 :> <<"Keyboard", "Resize">>) @@
     (S2 :> <<"ExplicitSignal", "ExplicitSignal">>)
@@ -361,7 +369,12 @@ VARIABLES
     terminalLastLocalDeliveries,
     terminalLastMetadataDeliveries,
     sessionClientSuspended,
-    sessionTerminalTransportState
+    sessionTerminalTransportState,
+    terminalPresentationIndex,
+    guestTerminalPresentation,
+    clientTerminalPresentation,
+    clientTerminalPresentationOwner,
+    guestAlternateSnapshotValid
 
 baseVars == <<
     domainPhase,
@@ -423,8 +436,17 @@ terminalEventRecordVars == <<
     terminalLastMetadataDeliveries
 >>
 
+terminalPresentationVars == <<
+    terminalPresentationIndex,
+    guestTerminalPresentation,
+    clientTerminalPresentation,
+    clientTerminalPresentationOwner,
+    guestAlternateSnapshotValid
+>>
+
 terminalInteractionVars == <<
-    terminalEventRecordVars, sessionClientSuspended, sessionTerminalTransportState
+    terminalEventRecordVars, sessionClientSuspended, sessionTerminalTransportState,
+    terminalPresentationVars
 >>
 
 terminalVars == <<terminalLifecycleVars, terminalInteractionVars>>
@@ -640,6 +662,11 @@ Init ==
     /\ terminalLastMetadataDeliveries = [s \in Sessions |-> 0]
     /\ sessionClientSuspended = [s \in Sessions |-> FALSE]
     /\ sessionTerminalTransportState = [s \in Sessions |-> "Ready"]
+    /\ terminalPresentationIndex = [s \in Sessions |-> 1]
+    /\ guestTerminalPresentation = [s \in Sessions |-> "Normal"]
+    /\ clientTerminalPresentation = [s \in Sessions |-> "Normal"]
+    /\ clientTerminalPresentationOwner = [s \in Sessions |-> "None"]
+    /\ guestAlternateSnapshotValid = [s \in Sessions |-> FALSE]
 
 (***************************************************************************
 Domain and Session lifecycle
@@ -952,6 +979,14 @@ RegisterSession(s) ==
     /\ connected' = [connected EXCEPT ![d] = @ \cup {s}]
     /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
     /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
+    /\ guestTerminalPresentation' =
+        [guestTerminalPresentation EXCEPT ![s] = "Normal"]
+    /\ clientTerminalPresentation' =
+        [clientTerminalPresentation EXCEPT ![s] = "Normal"]
+    /\ clientTerminalPresentationOwner' =
+        [clientTerminalPresentationOwner EXCEPT ![s] = "Guest"]
+    /\ guestAlternateSnapshotValid' =
+        [guestAlternateSnapshotValid EXCEPT ![s] = FALSE]
     /\ UNCHANGED <<
         domainPhase, stateAnchorState, sidecarState,
         sandboxState, trustReady, lockOwner, published, connectionState,
@@ -962,6 +997,9 @@ RegisterSession(s) ==
         domainGeneration,
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
+    /\ UNCHANGED <<terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState,
+                    terminalPresentationIndex>>
 
 DisconnectSession(s) ==
     LET d == Dom(s)
@@ -1124,6 +1162,14 @@ CurrentTerminalAdministrativeAuthorityValid(s) ==
     THEN TerminalAdministrativeAuthorityValid[s][terminalEventIndex[s]]
     ELSE FALSE
 
+TerminalPresentationEventAvailable(s) ==
+    terminalPresentationIndex[s] <= Len(TerminalPresentationPlan[s])
+
+CurrentTerminalPresentationEvent(s) ==
+    IF TerminalPresentationEventAvailable(s)
+    THEN TerminalPresentationPlan[s][terminalPresentationIndex[s]]
+    ELSE "None"
+
 OtherSession(s) == CHOOSE t \in Sessions : t # s
 
 TerminalDelivery(disposition, destination, target, bytes, signals, local, metadata) ==
@@ -1227,7 +1273,7 @@ DeliverPtyTerminalEvent(s) ==
     /\ sessionTerminalTransportState[s] = "Ready"
     /\ RecordTerminalEvent(s)
     /\ UNCHANGED <<baseVars, terminalLifecycleVars, sessionClientSuspended,
-                    sessionTerminalTransportState>>
+                    sessionTerminalTransportState, terminalPresentationVars>>
 
 SuspendLocalTerminalClient(s) ==
     /\ TerminalInteractionAdmissible(s)
@@ -1238,7 +1284,7 @@ SuspendLocalTerminalClient(s) ==
     /\ sessionClientSuspended' =
         [sessionClientSuspended EXCEPT ![s] = TRUE]
     /\ UNCHANGED <<baseVars, terminalLifecycleVars,
-                    sessionTerminalTransportState>>
+                    sessionTerminalTransportState, terminalPresentationVars>>
 
 ResumeLocalTerminalClient(s) ==
     /\ TerminalInteractionAdmissible(s)
@@ -1249,7 +1295,7 @@ ResumeLocalTerminalClient(s) ==
     /\ sessionClientSuspended' =
         [sessionClientSuspended EXCEPT ![s] = FALSE]
     /\ UNCHANGED <<baseVars, terminalLifecycleVars,
-                    sessionTerminalTransportState>>
+                    sessionTerminalTransportState, terminalPresentationVars>>
 
 DisconnectTerminalFromLocalAuthority(s, event) ==
     /\ event \in {"LocalDisconnect", "HostSignal"}
@@ -1265,7 +1311,7 @@ DisconnectTerminalFromLocalAuthority(s, event) ==
     /\ sessionClientSuspended' =
         [sessionClientSuspended EXCEPT ![s] = FALSE]
     /\ UNCHANGED <<sessionPtyOpen, sessionExecPresent, sessionGuestKnown,
-                    sessionTerminalTransportState>>
+                    sessionTerminalTransportState, terminalPresentationVars>>
 
 BlockSessionTerminalTransport(s) ==
     /\ TerminalInteractionAdmissible(s)
@@ -1273,14 +1319,50 @@ BlockSessionTerminalTransport(s) ==
     /\ sessionTerminalTransportState' =
         [sessionTerminalTransportState EXCEPT ![s] = "Blocked"]
     /\ UNCHANGED <<baseVars, terminalLifecycleVars, terminalEventRecordVars,
-                    sessionClientSuspended>>
+                    sessionClientSuspended, terminalPresentationVars>>
 
 UnblockSessionTerminalTransport(s) ==
     /\ sessionTerminalTransportState[s] = "Blocked"
     /\ sessionTerminalTransportState' =
         [sessionTerminalTransportState EXCEPT ![s] = "Ready"]
     /\ UNCHANGED <<baseVars, terminalLifecycleVars, terminalEventRecordVars,
-                    sessionClientSuspended>>
+                    sessionClientSuspended, terminalPresentationVars>>
+
+GuestEnterAlternatePresentation(s) ==
+    /\ TerminalInteractionAdmissible(s)
+    /\ TerminalPresentationEventAvailable(s)
+    /\ CurrentTerminalPresentationEvent(s) = "EnterAlternate"
+    /\ guestTerminalPresentation[s] = "Normal"
+    /\ terminalPresentationIndex' =
+        [terminalPresentationIndex EXCEPT ![s] = @ + 1]
+    /\ guestTerminalPresentation' =
+        [guestTerminalPresentation EXCEPT ![s] = "Alternate"]
+    /\ clientTerminalPresentation' =
+        [clientTerminalPresentation EXCEPT ![s] = "Alternate"]
+    /\ clientTerminalPresentationOwner' =
+        [clientTerminalPresentationOwner EXCEPT ![s] = "Guest"]
+    /\ guestAlternateSnapshotValid' =
+        [guestAlternateSnapshotValid EXCEPT ![s] = FALSE]
+    /\ UNCHANGED <<baseVars, terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState>>
+
+GuestExitAlternatePresentation(s) ==
+    /\ TerminalInteractionAdmissible(s)
+    /\ TerminalPresentationEventAvailable(s)
+    /\ CurrentTerminalPresentationEvent(s) = "ExitAlternate"
+    /\ guestTerminalPresentation[s] = "Alternate"
+    /\ terminalPresentationIndex' =
+        [terminalPresentationIndex EXCEPT ![s] = @ + 1]
+    /\ guestTerminalPresentation' =
+        [guestTerminalPresentation EXCEPT ![s] = "Normal"]
+    /\ clientTerminalPresentation' =
+        [clientTerminalPresentation EXCEPT ![s] = "Normal"]
+    /\ clientTerminalPresentationOwner' =
+        [clientTerminalPresentationOwner EXCEPT ![s] = "Guest"]
+    /\ guestAlternateSnapshotValid' =
+        [guestAlternateSnapshotValid EXCEPT ![s] = FALSE]
+    /\ UNCHANGED <<baseVars, terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState>>
 
 TerminalInteraction(s) ==
     \/ DeliverPtyTerminalEvent(s)
@@ -1288,6 +1370,8 @@ TerminalInteraction(s) ==
     \/ ResumeLocalTerminalClient(s)
     \/ BlockSessionTerminalTransport(s)
     \/ UnblockSessionTerminalTransport(s)
+    \/ GuestEnterAlternatePresentation(s)
+    \/ GuestExitAlternatePresentation(s)
     \/ (\E event \in {"LocalDisconnect", "HostSignal"} :
         DisconnectTerminalFromLocalAuthority(s, event))
 
@@ -1518,6 +1602,26 @@ QueuePrompt(r) ==
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
 
+PresentTrustedTerminal(s) ==
+    /\ guestTerminalPresentation' = guestTerminalPresentation
+    /\ clientTerminalPresentation' =
+        [clientTerminalPresentation EXCEPT ![s] = "Alternate"]
+    /\ clientTerminalPresentationOwner' =
+        [clientTerminalPresentationOwner EXCEPT ![s] = "Trusted"]
+    /\ guestAlternateSnapshotValid' =
+        [guestAlternateSnapshotValid EXCEPT
+            ![s] = (guestTerminalPresentation[s] = "Alternate")]
+
+RestoreGuestTerminalPresentation(s) ==
+    /\ guestTerminalPresentation' = guestTerminalPresentation
+    /\ clientTerminalPresentation' =
+        [clientTerminalPresentation EXCEPT
+            ![s] = guestTerminalPresentation[s]]
+    /\ clientTerminalPresentationOwner' =
+        [clientTerminalPresentationOwner EXCEPT ![s] = "Guest"]
+    /\ guestAlternateSnapshotValid' =
+        [guestAlternateSnapshotValid EXCEPT ![s] = FALSE]
+
 BeginPrompt(r) ==
     LET s == ReqSession(r)
         d == ReqDomain(r)
@@ -1528,6 +1632,7 @@ BeginPrompt(r) ==
     /\ activeRequest[s] = r
     /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Prompting"]
     /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Prompt"]
+    /\ PresentTrustedTerminal(s)
     /\ UNCHANGED <<
         domainPhase, stateAnchorState, sidecarState,
         sandboxState, trustReady, lockOwner, published, registered, connected,
@@ -1538,6 +1643,9 @@ BeginPrompt(r) ==
         domainGeneration,
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
+    /\ UNCHANGED <<terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState,
+                    terminalPresentationIndex>>
 
 DeveloperApprove(r, cmd) ==
     LET s == ReqSession(r)
@@ -1574,6 +1682,7 @@ DeveloperDeny(r) ==
     /\ requestPhase' = [requestPhase EXCEPT ![r] = "DenialPending"]
     /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
     /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
+    /\ RestoreGuestTerminalPresentation(s)
     /\ UNCHANGED <<
         domainPhase, stateAnchorState, sidecarState,
         sandboxState, trustReady, lockOwner, published, registered, connected,
@@ -1584,6 +1693,9 @@ DeveloperDeny(r) ==
         domainGeneration,
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
+    /\ UNCHANGED <<terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState,
+                    terminalPresentationIndex>>
 
 StartHostExecution(r) ==
     LET s == ReqSession(r)
@@ -1599,6 +1711,7 @@ StartHostExecution(r) ==
     /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "HostExecuting"]
     /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "HostProcess"]
     /\ hostRunning' = hostRunning \cup {r}
+    /\ PresentTrustedTerminal(s)
     /\ UNCHANGED <<
         domainPhase, stateAnchorState, sidecarState,
         sandboxState, trustReady, lockOwner, published, registered, connected,
@@ -1609,6 +1722,9 @@ StartHostExecution(r) ==
         domainGeneration,
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
+    /\ UNCHANGED <<terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState,
+                    terminalPresentationIndex>>
 
 CompleteHostExecution(r) ==
     LET s == ReqSession(r)
@@ -1621,6 +1737,7 @@ CompleteHostExecution(r) ==
     /\ hostRunning' = hostRunning \ {r}
     /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
     /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
+    /\ RestoreGuestTerminalPresentation(s)
     /\ UNCHANGED <<
         domainPhase, stateAnchorState, sidecarState,
         sandboxState, trustReady, lockOwner, published, registered, connected,
@@ -1631,6 +1748,9 @@ CompleteHostExecution(r) ==
         domainGeneration,
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
+    /\ UNCHANGED <<terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState,
+                    terminalPresentationIndex>>
 
 TimeoutRequest(r) ==
     LET s == ReqSession(r)
@@ -1643,6 +1763,7 @@ TimeoutRequest(r) ==
     /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
     /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
     /\ hostRunning' = hostRunning \ {r}
+    /\ RestoreGuestTerminalPresentation(s)
     /\ UNCHANGED <<
         domainPhase, stateAnchorState, sidecarState,
         sandboxState, trustReady, lockOwner, published, registered, connected,
@@ -1653,6 +1774,9 @@ TimeoutRequest(r) ==
         domainGeneration,
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
+    /\ UNCHANGED <<terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState,
+                    terminalPresentationIndex>>
 
 CancelRequest(r) ==
     LET s == ReqSession(r)
@@ -1668,6 +1792,7 @@ CancelRequest(r) ==
     /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
     /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
     /\ hostRunning' = hostRunning \ {r}
+    /\ RestoreGuestTerminalPresentation(s)
     /\ UNCHANGED <<
         domainPhase, stateAnchorState, sidecarState,
         sandboxState, trustReady, lockOwner, published, registered, connected,
@@ -1678,6 +1803,9 @@ CancelRequest(r) ==
         domainGeneration,
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
+    /\ UNCHANGED <<terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState,
+                    terminalPresentationIndex>>
 
 FailHostExecution(r) ==
     LET s == ReqSession(r)
@@ -1691,6 +1819,7 @@ FailHostExecution(r) ==
     /\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
     /\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
     /\ hostRunning' = hostRunning \ {r}
+    /\ RestoreGuestTerminalPresentation(s)
     /\ UNCHANGED <<
         domainPhase, stateAnchorState, sidecarState,
         sandboxState, trustReady, lockOwner, published, registered, connected,
@@ -1701,6 +1830,9 @@ FailHostExecution(r) ==
         domainGeneration,
         durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
         >>
+    /\ UNCHANGED <<terminalLifecycleVars, terminalEventRecordVars,
+                    sessionClientSuspended, sessionTerminalTransportState,
+                    terminalPresentationIndex>>
 
 DeliverResult(r) ==
     LET s == ReqSession(r)
@@ -2433,22 +2565,38 @@ RequestProgress(r) ==
     \/ FailHostExecution(r)
     \/ DeliverResult(r)
 
-BaseNext ==
+UnchangedTerminalRequestProgress(r) ==
+    \/ AutoApprove(r)
+    \/ QueuePrompt(r)
+    \/ (\E cmd \in Commands : DeveloperApprove(r, cmd))
+    \/ DeliverResult(r)
+
+PresentationRequestProgress(r) ==
+    \/ BeginPrompt(r)
+    \/ DeveloperDeny(r)
+    \/ StartHostExecution(r)
+    \/ CompleteHostExecution(r)
+    \/ TimeoutRequest(r)
+    \/ CancelRequest(r)
+    \/ FailHostExecution(r)
+
+UnchangedTerminalBaseNext ==
     \/ (\E s \in Sessions :
         StartNewDomain(s) \/ StartReadySession(s) \/ WaitForDomain(s) \/
         RestartWaitingDomain(s) \/ AdvanceWaitingSession(s) \/
-        RejectConfigurationMismatch(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))
+        ReceiveEscalation(r) \/ UnchangedTerminalRequestProgress(r))
 
 Next ==
-    \/ /\ BaseNext
+    \/ /\ UnchangedTerminalBaseNext
        /\ UNCHANGED terminalVars
+    \/ (\E s \in Sessions : RegisterSession(s))
+    \/ (\E r \in Requests : PresentationRequestProgress(r))
     \/ (\E s \in Sessions : SessionTerminalProgress(s))
     \/ (\E s \in Sessions : TerminalInteraction(s))
 
@@ -2463,10 +2611,10 @@ Spec ==
     /\ \A d \in Domains :
         WF_vars(DomainServiceProgress(d) /\ UNCHANGED terminalVars)
     /\ \A s \in Sessions :
-        WF_vars(SessionProgress(s) /\ UNCHANGED terminalVars)
+        WF_vars(SessionProgress(s))
     /\ \A s \in Sessions : WF_vars(SessionTerminalProgress(s))
     /\ \A r \in Requests :
-        WF_vars(RequestProgress(r) /\ UNCHANGED terminalVars)
+        WF_vars(RequestProgress(r))
 
 (***************************************************************************
 Safety properties
@@ -2476,6 +2624,8 @@ TypeOK ==
     /\ TerminalEventPlan \in [Sessions -> Seq(TerminalEventKinds)]
     /\ TerminalAuthorityPlan \in [Sessions -> Seq(TerminalAuthorities)]
     /\ TerminalAdministrativeAuthorityValid \in [Sessions -> Seq(BOOLEAN)]
+    /\ TerminalPresentationPlan \in
+        [Sessions -> Seq(TerminalPresentationEventKinds)]
     /\ \A s \in Sessions :
         /\ Len(TerminalEventPlan[s]) = Len(TerminalAuthorityPlan[s])
         /\ Len(TerminalEventPlan[s]) =
@@ -2522,6 +2672,9 @@ TypeOK ==
     /\ sessionGuestKnown \in [Sessions -> BOOLEAN]
     /\ \A s \in Sessions :
         terminalEventIndex[s] \in 1..(Len(TerminalEventPlan[s]) + 1)
+    /\ \A s \in Sessions :
+        terminalPresentationIndex[s] \in
+            1..(Len(TerminalPresentationPlan[s]) + 1)
     /\ \A s \in Sessions :
         terminalLastEventId[s] \in 0..Len(TerminalEventPlan[s])
     /\ terminalLastEvent \in [Sessions -> TerminalEventKinds \cup {"None"}]
@@ -2537,6 +2690,11 @@ TypeOK ==
     /\ terminalLastMetadataDeliveries \in [Sessions -> 0..1]
     /\ sessionClientSuspended \in [Sessions -> BOOLEAN]
     /\ sessionTerminalTransportState \in [Sessions -> TerminalTransportStates]
+    /\ guestTerminalPresentation \in [Sessions -> TerminalPresentations]
+    /\ clientTerminalPresentation \in [Sessions -> TerminalPresentations]
+    /\ clientTerminalPresentationOwner \in
+        [Sessions -> TerminalPresentationOwners]
+    /\ guestAlternateSnapshotValid \in [Sessions -> BOOLEAN]
 
 SessionTerminalPhysicalConsistency ==
     \A s \in Sessions :
@@ -2726,6 +2884,21 @@ TerminalIsolation ==
     \A s \in Sessions : sessionPhase[s] = "Prompting" =>
         terminalRoute[s] = "Prompt"
 
+TerminalPresentationIsolation ==
+    \A s \in Sessions :
+        /\ (sessionPhase[s] = "Attached" /\ terminalRoute[s] = "Sandbox" =>
+            /\ clientTerminalPresentation[s] = guestTerminalPresentation[s]
+            /\ clientTerminalPresentationOwner[s] = "Guest"
+            /\ ~guestAlternateSnapshotValid[s])
+        /\ (terminalRoute[s] \in {"Prompt", "HostProcess"} =>
+            /\ clientTerminalPresentation[s] = "Alternate"
+            /\ clientTerminalPresentationOwner[s] = "Trusted"
+            /\ (guestAlternateSnapshotValid[s] <=>
+                guestTerminalPresentation[s] = "Alternate"))
+        /\ (guestAlternateSnapshotValid[s] =>
+            /\ clientTerminalPresentationOwner[s] = "Trusted"
+            /\ guestTerminalPresentation[s] = "Alternate")
+
 ObservedTerminalDelivery(s) ==
     TerminalDelivery(
         terminalLastDisposition[s],
@@ -2927,6 +3100,7 @@ Safety ==
     /\ HostExecutionAuthorized
     /\ AutoApprovalNoShell
     /\ TerminalIsolation
+    /\ TerminalPresentationIsolation
     /\ TerminalInteractionAuthoritySeparated
     /\ NoOrphanHostProcess
     /\ StateAnchorOwnership

docs/protocol/LazaretTerminalLocalControl.cfg

@@ -51,6 +51,7 @@ CONSTANTS
     TerminalAuthorityPlan <- TerminalLocalControlAuthorityPlanFixture
     TerminalAdministrativeAuthorityValid <-
         TerminalLocalControlAdministrativeAuthorityValidFixture
+    TerminalPresentationPlan <- TerminalNoPresentationPlanFixture
     TerminalRoutingFault = "Correct"
 
 SPECIFICATION SafetySpec
@@ -59,6 +60,7 @@ CHECK_DEADLOCK FALSE
 INVARIANTS
     TypeOK
     SessionTerminalPhysicalConsistency
+    TerminalPresentationIsolation
     TerminalInteractionAuthoritySeparated
     LocalTerminationAvailableWhileTransportBlocked
 

docs/protocol/LazaretTerminalPeerIsolation.cfg

@@ -51,6 +51,7 @@ CONSTANTS
     TerminalAuthorityPlan <- TerminalRoutingAuthorityPlanFixture
     TerminalAdministrativeAuthorityValid <-
         TerminalRoutingAdministrativeAuthorityValidFixture
+    TerminalPresentationPlan <- TerminalNoPresentationPlanFixture
     TerminalRoutingFault = "Correct"
 
 SPECIFICATION SafetySpec
@@ -59,6 +60,7 @@ CHECK_DEADLOCK FALSE
 INVARIANTS
     TypeOK
     SessionTerminalPhysicalConsistency
+    TerminalPresentationIsolation
     TerminalInteractionAuthoritySeparated
     LocalTerminationAvailableWhileTransportBlocked
 

docs/protocol/LazaretTerminalPresentationSafety.cfg

@@ -0,0 +1,107 @@
+CONSTANTS
+    D1 = d1
+    S1 = s1
+    S2 = s2
+    R1 = r1
+    R2 = r2
+    R3 = r3
+    ExactCmd = exactCmd
+    PromptCmd = promptCmd
+    ShellCmd = shellCmd
+    EditedCmd = editedCmd
+    Identities <- IdentitiesFixture
+    SessionAnchors <- SessionAnchorsFixture
+    Domains <- DomainsFixture
+    Sessions <- SessionsFixture
+    Requests <- RequestsFixture
+    Commands <- CommandsFixture
+    NoSession = NoSession
+    NoRequest = NoRequest
+    NoCommand = NoCommand
+    NoApproval = NoApproval
+    SessionDomain <- SessionDomainFixture
+    SessionFingerprint <- SessionFingerprintFixture
+    DomainFingerprint <- DomainFingerprintFixture
+    DomainCoordinatorIdentity <- DomainCoordinatorIdentityFixture
+    DomainSidecarIdentity <- DomainSidecarIdentityFixture
+    DomainSandboxIdentity <- DomainSandboxIdentityFixture
+    SessionCliIdentity <- SessionCliIdentityFixture
+    SessionAnchorIdentity <- SessionAnchorIdentityFixture
+    CoordinatorCertificateValid <- CoordinatorCertificateValidFixture
+    SidecarCertificateValid <- SidecarCertificateValidFixture
+    SandboxCertificateValid <- SandboxCertificateValidFixture
+    CliCertificateValid <- CliCertificateValidFixture
+    ConfigSafe <- ConfigSafeFixture
+    SandboxIsolationSafe <- SandboxIsolationSafeFixture
+    RequestSession <- RequestSessionFixture
+    RequestCommand <- RequestCommandFixture
+    RequestSandboxIdentity <- RequestSandboxIdentityFixture
+    RequestCliIdentity <- RequestCliIdentityFixture
+    RequestSessionAnchor <- RequestSessionAnchorFixture
+    RequestCredentialValid <- RequestCredentialValidFixture
+    RequestSignatureValid <- RequestSignatureValidFixture
+    ApprovalCliIdentity <- ApprovalCliIdentityFixture
+    ApprovalSessionAnchor <- ApprovalSessionAnchorFixture
+    ApprovalSignatureValid <- ApprovalSignatureValidFixture
+    ApprovalCommand <- ApprovalCommandFixture
+    AutoRuleMatches <- AutoRuleMatchesFixture
+    CommandRequiresShell <- CommandRequiresShellFixture
+    CommandContentSafe <- CommandContentSafeFixture
+    TerminalEventPlan <- TerminalNoEventPlanFixture
+    TerminalAuthorityPlan <- TerminalNoAuthorityPlanFixture
+    TerminalAdministrativeAuthorityValid <-
+        TerminalNoAdministrativeAuthorityValidFixture
+    TerminalPresentationPlan <- TerminalPresentationPlanFixture
+    TerminalRoutingFault = "Correct"
+
+SPECIFICATION SafetySpec
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    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
+    TerminalPresentationIsolation
+    TerminalInteractionAuthoritySeparated
+    LocalTerminationAvailableWhileTransportBlocked
+    NoOrphanHostProcess
+    StateAnchorOwnership
+    FailedDomainIsolation
+    OrderedFailureRecovery
+    ResultDeliveryStateConsistent
+    MultiRoleDurableIntent
+    NetworkReadinessBoundToSandbox
+    GenerationScopedIdentitiesDistinct
+    HelperUnderSupervisor
+    PreparedLowerLeaseBeforeMount
+    NetworkReadyBeforePublish

docs/protocol/LazaretTerminalSafety.cfg

@@ -51,6 +51,7 @@ CONSTANTS
     TerminalAuthorityPlan <- TerminalAuthorityPlanFixture
     TerminalAdministrativeAuthorityValid <-
         TerminalAdministrativeAuthorityValidFixture
+    TerminalPresentationPlan <- TerminalNoPresentationPlanFixture
     TerminalRoutingFault = "Correct"
 
 SPECIFICATION SafetySpec
@@ -90,6 +91,7 @@ INVARIANTS
     HostExecutionAuthorized
     AutoApprovalNoShell
     TerminalIsolation
+    TerminalPresentationIsolation
     TerminalInteractionAuthoritySeparated
     LocalTerminationAvailableWhileTransportBlocked
     NoOrphanHostProcess

tests/tooling/test_verify.py

@@ -740,6 +740,7 @@ class VerificationTests(unittest.TestCase):
                 ("Lazaret.tla", "Lazaret.cfg"),
                 ("Lazaret.tla", "LazaretTerminalLocalControl.cfg"),
                 ("Lazaret.tla", "LazaretTerminalPeerIsolation.cfg"),
+                ("Lazaret.tla", "LazaretTerminalPresentationSafety.cfg"),
                 ("Lazaret.tla", "LazaretTerminalSafety.cfg"),
                 ("PreparedLower.tla", "PreparedLower.cfg"),
             },
@@ -791,6 +792,7 @@ class VerificationTests(unittest.TestCase):
         configs = [
             ROOT / "docs/protocol/Lazaret.cfg",
             ROOT / "docs/protocol/LazaretTerminalSafety.cfg",
+            ROOT / "docs/protocol/LazaretTerminalPresentationSafety.cfg",
             ROOT / "docs/protocol/LazaretTerminalPeerIsolation.cfg",
             ROOT / "docs/protocol/LazaretTerminalLocalControl.cfg",
         ]
@@ -809,6 +811,10 @@ class VerificationTests(unittest.TestCase):
             invariants(ROOT / "docs/protocol/LazaretTerminalSafety.cfg"),
             invariants(ROOT / "docs/protocol/Lazaret.cfg"),
         )
+        self.assertEqual(
+            invariants(ROOT / "docs/protocol/LazaretTerminalPresentationSafety.cfg"),
+            invariants(ROOT / "docs/protocol/Lazaret.cfg"),
+        )
 
 
 if __name__ == "__main__":

tools/lazaret_verify.py

@@ -24,6 +24,10 @@ MODEL_CONFIGURATIONS = (
         ROOT / "docs/protocol/Lazaret.tla",
         ROOT / "docs/protocol/LazaretTerminalSafety.cfg",
     ),
+    (
+        ROOT / "docs/protocol/Lazaret.tla",
+        ROOT / "docs/protocol/LazaretTerminalPresentationSafety.cfg",
+    ),
     (
         ROOT / "docs/protocol/Lazaret.tla",
         ROOT / "docs/protocol/LazaretTerminalPeerIsolation.cfg",