RoostPageReady

--------------------------- MODULE RoostPageReady --------------------------- (***************************************************************************) (* Page SDK readiness: calls wait for the transport handshake. *) (* *) (* A tenant page loads the browser SDK in one of three environments. In a *) (* normal tab on the org origin ("web") the SDK talks to the server with a *) (* same-origin fetch and that transport is final from the first line. In *) (* an about:srcdoc frame inside a chat host ("host") the SDK starts a *) (* ui/initialize handshake over postMessage, and when the host answers the *) (* transport becomes the bridge. In an about:srcdoc frame that is marked *) (* as an MCP surface but whose host never answers ("orphan") the handshake *) (* times out and the transport becomes dead: every call rejects with a *) (* clear error. It never falls back to fetch, because a relative fetch *) (* from a srcdoc frame has no usable origin, so the request goes nowhere *) (* useful and the page renders an error that names the wrong cause. *) (* *) (* The transport variable starts as "web" in every environment, and page *) (* scripts run at once: they may issue a call, or read the signed-in user, *) (* before the handshake has finished. The property the SDK must keep is *) (* that a call is only ever dispatched on the transport that ends up final *) (* for its environment. The SDK therefore holds every call behind *) (* transportReady and dispatches it afterwards, the session is loaded over *) (* the final transport, and ready resolves only after both. A page that *) (* awaits ready reads a user that is final. *) (* *) (* The constant Hold chooses between that design (TRUE) and the old *) (* behaviour (FALSE), where a call is dispatched immediately on whatever *) (* the transport is at that moment and the page reads the user without *) (* awaiting ready. The mutant violates NoWebCallInFrame in two steps: the *) (* page in a frame issues a call before the handshake completes. *) (***************************************************************************) EXTENDS Naturals, Sequences CONSTANTS Envs, \* the environments a page may load in: "web", "host", "orphan" MaxCalls, \* how many calls the page script issues Hold \* TRUE: calls and reads wait for readiness; FALSE: they go at once VARIABLES env, \* where this page loaded, fixed at load transport, \* "web" (fetch), "bridge" (postMessage), "dead" (rejects) transportReady, \* the transport is final sessionLoaded, \* the session has been fetched, so the user is final sessionVia, \* the transport the session fetch went out on, or "none" ready, \* the ready promise has resolved issued, \* calls the page script has issued so far queued, \* calls held by the SDK, waiting for transportReady dispatched, \* the transport each dispatched call used, in order userRead \* the page's read of the user: "none", "settled", "early" vars == <<env, transport, transportReady, sessionLoaded, sessionVia, ready, issued, queued, dispatched, userRead>> Transports == {"web", "bridge", "dead"} \* The transport each environment must end up on. Final(e) == CASE e = "web" -> "web" [] e = "host" -> "bridge" [] e = "orphan" -> "dead" Init == /\ env \in Envs /\ transport = "web" /\ transportReady = (env = "web") \* a normal tab has nothing to wait for /\ sessionLoaded = FALSE /\ sessionVia = "none" /\ ready = FALSE /\ issued = 0 /\ queued = 0 /\ dispatched = <<>> /\ userRead = "none" \* The host answers ui/initialize: the bridge replaces fetch. Handshake == /\ env = "host" /\ ~transportReady /\ transport' = "bridge" /\ transportReady' = TRUE /\ UNCHANGED <<env, sessionLoaded, sessionVia, ready, issued, queued, dispatched, userRead>> \* Nobody answers: the timer fires and the transport is dead, never fetch. Timeout == /\ env = "orphan" /\ ~transportReady /\ transport' = "dead" /\ transportReady' = TRUE /\ UNCHANGED <<env, sessionLoaded, sessionVia, ready, issued, queued, dispatched, userRead>> \* roost.call() from the page script, at any time. Held, or sent at once. IssueCall == /\ issued < MaxCalls /\ issued' = issued + 1 /\ IF Hold THEN /\ queued' = queued + 1 /\ UNCHANGED dispatched ELSE /\ dispatched' = Append(dispatched, transport) /\ UNCHANGED queued /\ UNCHANGED <<env, transport, transportReady, sessionLoaded, sessionVia, ready, userRead>> \* A held call goes out once the transport is final (a dead one rejects it). Drain == /\ queued > 0 /\ transportReady /\ queued' = queued - 1 /\ dispatched' = Append(dispatched, transport) /\ UNCHANGED <<env, transport, transportReady, sessionLoaded, sessionVia, ready, issued, userRead>> \* The session fetch. On a dead transport it settles as signed out, which is \* still a final answer for the user. LoadSession == /\ ~sessionLoaded /\ Hold => transportReady /\ sessionLoaded' = TRUE /\ sessionVia' = transport /\ UNCHANGED <<env, transport, transportReady, ready, issued, queued, dispatched, userRead>> \* ready resolves after the transport is final and the session is loaded. ResolveReady == /\ ~ready /\ transportReady /\ sessionLoaded /\ ready' = TRUE /\ UNCHANGED <<env, transport, transportReady, sessionLoaded, sessionVia, issued, queued, dispatched, userRead>> \* The page reads the user: after awaiting ready, or (mutant) straight away. ReadUser == /\ userRead = "none" /\ Hold => ready /\ userRead' = IF sessionLoaded THEN "settled" ELSE "early" /\ UNCHANGED <<env, transport, transportReady, sessionLoaded, sessionVia, ready, issued, queued, dispatched>> Next == \/ Handshake \/ Timeout \/ IssueCall \/ Drain \/ LoadSession \/ ResolveReady \/ ReadUser Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- TypeOK == /\ env \in Envs /\ transport \in Transports /\ transportReady \in BOOLEAN /\ sessionLoaded \in BOOLEAN /\ sessionVia \in Transports \cup {"none"} /\ ready \in BOOLEAN /\ issued \in 0..MaxCalls /\ queued \in 0..MaxCalls /\ Len(dispatched) + queued = issued /\ \A k \in 1..Len(dispatched) : dispatched[k] \in Transports /\ userRead \in {"none", "settled", "early"} \* A page in a frame never sends a call by fetch: there is no origin to \* send it to. NoWebCallInFrame == env \in {"host", "orphan"} => \A k \in 1..Len(dispatched) : dispatched[k] # "web" \* Every call went out on the transport its environment ends up on: \* web on web, host on the bridge, orphan rejected by the dead transport. CallsUseFinalTransport == \A k \in 1..Len(dispatched) : dispatched[k] = Final(env) \* transportReady is never announced on a transport that will change. ReadyTransportIsFinal == transportReady => transport = Final(env) \* ready means there is nothing left to wait for. ReadyMeansSettled == ready => /\ transportReady /\ transport = Final(env) /\ sessionLoaded \* The session itself was fetched over the final transport. SessionOnFinalTransport == sessionVia \in {"none", Final(env)} \* The page never saw a user that could still change. UserReadIsSettled == userRead # "early" =============================================================================

SPECIFICATION Spec CHECK_DEADLOCK FALSE CONSTANTS Envs = {"web", "host", "orphan"} MaxCalls = 2 Hold = TRUE INVARIANTS TypeOK NoWebCallInFrame CallsUseFinalTransport ReadyTransportIsFinal ReadyMeansSettled SessionOnFinalTransport UserReadIsSettled