Single-flight OAuth token refresh

specs/TokenRefresh.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CONSTANT Clients = {c1, c2}
+INVARIANT TypeOK
+INVARIANT NoStaleOverwrite

specs/TokenRefresh.tla

@@ -0,0 +1,120 @@
+---------------------------- MODULE TokenRefresh ----------------------------
+(***************************************************************************)
+(* Model of the CURRENT design of getAccessToken in src/store/authStore.ts *)
+(* (:97-120).                                                              *)
+(*                                                                         *)
+(* getAccessToken is re-entrant with no mutex. It read-modify-writes a      *)
+(* single localStorage record across an await: read at :98, refresh at     *)
+(* :109, write at :111 (success) or :114 (failure). There are nine         *)
+(* independent call sites -- save, loadProject, toggleShare,               *)
+(* deleteCloudProject, and five in the project list / import UI -- any of  *)
+(* which can be in flight together (e.g. autosave firing while the user    *)
+(* clicks Share).                                                          *)
+(*                                                                         *)
+(* This spec is expected to FAIL NoStaleOverwrite.                         *)
+(***************************************************************************)
+EXTENDS Naturals, FiniteSets
+
+CONSTANT Clients
+
+\* writePersisted(null) -- the record is gone and the user is signed out.
+NoSession == [exists |-> FALSE, tok |-> 0]
+
+VARIABLES
+    store,      \* the localStorage record (single shared cell)
+    pc,         \* client -> "idle" | "refreshing" | "done" | "failed"
+    snap,       \* client -> the record it read at :98, before its await
+    nextTok,    \* source of fresh access tokens
+    staleWrite  \* history variable: has anyone written based on a stale read?
+
+vars == <<store, pc, snap, nextTok, staleWrite>>
+
+Init ==
+    \* The initial token is within 60s of expiry, so every caller takes the
+    \* refresh branch -- the case of interest.
+    /\ store      = [exists |-> TRUE, tok |-> 1]
+    /\ pc         = [c \in Clients |-> "idle"]
+    /\ snap       = [c \in Clients |-> [exists |-> TRUE, tok |-> 1]]
+    /\ nextTok    = 2
+    /\ staleWrite = FALSE
+
+\* :98-99 -- no record at all.
+ReadNoSession(c) ==
+    /\ pc[c] = "idle"
+    /\ ~store.exists
+    /\ pc' = [pc EXCEPT ![c] = "failed"]
+    /\ UNCHANGED <<store, snap, nextTok, staleWrite>>
+
+\* :98 then :101 -- snapshot the record and start refreshing. Nothing marks
+\* the store as having a refresh in flight, so every client does this
+\* independently.
+ReadAndRefresh(c) ==
+    /\ pc[c] = "idle"
+    /\ store.exists
+    /\ snap' = [snap EXCEPT ![c] = store]
+    /\ pc'   = [pc EXCEPT ![c] = "refreshing"]
+    /\ UNCHANGED <<store, nextTok, staleWrite>>
+
+\* A write is stale if the record moved on after this client read it -- i.e.
+\* the client is clobbering someone else's newer write.
+IsStale(c) == snap[c] # store
+
+\* :109-112 -- POST succeeded; write {...persisted, accessToken} back. Note
+\* the spread is off this client's OWN snapshot, not off current storage.
+RefreshSucceeds(c) ==
+    /\ pc[c] = "refreshing"
+    /\ store'      = [exists |-> TRUE, tok |-> nextTok]
+    /\ nextTok'    = nextTok + 1
+    /\ pc'         = [pc EXCEPT ![c] = "done"]
+    /\ staleWrite' = (staleWrite \/ IsStale(c))
+    /\ UNCHANGED snap
+
+\* :113-117 -- ANY failure (network blip, 5xx, rotated refresh token) wipes
+\* the entire auth record and signs the user out.
+RefreshFails(c) ==
+    /\ pc[c] = "refreshing"
+    /\ store'      = NoSession
+    /\ pc'         = [pc EXCEPT ![c] = "failed"]
+    /\ staleWrite' = (staleWrite \/ IsStale(c))
+    /\ UNCHANGED <<snap, nextTok>>
+
+Terminating ==
+    /\ \A c \in Clients : pc[c] \in {"done", "failed"}
+    /\ UNCHANGED vars
+
+Next ==
+    \/ \E c \in Clients :
+        ReadNoSession(c) \/ ReadAndRefresh(c) \/ RefreshSucceeds(c) \/ RefreshFails(c)
+    \/ Terminating
+
+Spec == Init /\ [][Next]_vars
+
+(***************************************************************************)
+(* Properties.                                                             *)
+(***************************************************************************)
+
+TypeOK ==
+    /\ store.exists \in BOOLEAN
+    /\ \A c \in Clients : pc[c] \in {"idle", "refreshing", "done", "failed"}
+
+\* SAFETY.  No caller writes the auth record based on a read the record has
+\* already moved past. getAccessToken read-modify-writes across an await and
+\* never re-validates, so this is exactly the defect.
+\*
+\* VIOLATED: two callers snapshot the same record and refresh concurrently;
+\* the first succeeds and advances the record; the second then writes --
+\* clobbering a session established after its own read. When the second
+\* call fails (a blip, a 5xx, a rotated refresh token) that write is
+\* writePersisted(null), signing the user out mid-save.
+\*
+\* Note this is deliberately NOT "a successful refresh is never followed by
+\* a logout" -- that is too strong, since a later, sequential refresh may
+\* legitimately discover a dead token and sign out correctly.
+NoStaleOverwrite == ~staleWrite
+
+\* The mechanism behind the violation: nothing bounds concurrent refreshes.
+\* VIOLATED trivially with two clients.
+AtMostOneRefreshInFlight ==
+    Cardinality({c \in Clients : pc[c] = "refreshing"}) <= 1
+
+=============================================================================

specs/TokenRefreshFixed.cfg

@@ -0,0 +1,9 @@
+SPECIFICATION Spec
+
+CONSTANT Clients = {c1, c2, c3}
+CONSTANT NoLeader = NoLeader
+
+INVARIANT TypeOK
+INVARIANT NoStaleOverwrite
+INVARIANT AtMostOneRefreshInFlight
+INVARIANT WaitersDoNotRefresh

specs/TokenRefreshFixed.tla

@@ -0,0 +1,135 @@
+------------------------- MODULE TokenRefreshFixed --------------------------
+(***************************************************************************)
+(* Corrected getAccessToken protocol.                                      *)
+(*                                                                         *)
+(* Two changes relative to TokenRefresh.tla:                               *)
+(*                                                                         *)
+(*   1. Single-flight. The first caller to need a refresh becomes the       *)
+(*      leader and stores its in-flight promise; concurrent callers await   *)
+(*      that same promise instead of issuing their own refresh. At most one *)
+(*      refresh is ever in flight, so no caller can be signed out by        *)
+(*      another caller's failure.                                          *)
+(*                                                                         *)
+(*   2. Only a definitive auth failure clears the session. invalid_grant /  *)
+(*      401 means the refresh token is genuinely dead -> sign out. A        *)
+(*      network error or 5xx rejects the waiting callers but LEAVES the     *)
+(*      record intact, so a blip mid-save no longer logs the user out.      *)
+(*                                                                         *)
+(* All three properties hold.                                              *)
+(***************************************************************************)
+EXTENDS Naturals, FiniteSets
+
+\* NoLeader is a model value standing for "no refresh in flight".
+CONSTANTS Clients, NoLeader
+
+NoSession == [exists |-> FALSE, tok |-> 0]
+
+VARIABLES
+    store,
+    pc,         \* client -> "idle" | "refreshing" | "waiting" | "done" | "failed"
+    leader,     \* the client owning the in-flight refresh, or NoLeader
+    snap,       \* the leader's snapshot, taken when it acquired the lock
+    nextTok,
+    staleWrite  \* history variable, as in TokenRefresh.tla
+
+vars == <<store, pc, leader, snap, nextTok, staleWrite>>
+
+Init ==
+    /\ store      = [exists |-> TRUE, tok |-> 1]
+    /\ pc         = [c \in Clients |-> "idle"]
+    /\ leader     = NoLeader
+    /\ snap       = [exists |-> TRUE, tok |-> 1]
+    /\ nextTok    = 2
+    /\ staleWrite = FALSE
+
+ReadNoSession(c) ==
+    /\ pc[c] = "idle"
+    /\ ~store.exists
+    /\ pc' = [pc EXCEPT ![c] = "failed"]
+    /\ UNCHANGED <<store, leader, snap, nextTok, staleWrite>>
+
+\* No refresh in flight: take the lock and issue one.
+AcquireAndRefresh(c) ==
+    /\ pc[c] = "idle"
+    /\ store.exists
+    /\ leader = NoLeader
+    /\ leader' = c
+    /\ snap'   = store
+    /\ pc' = [pc EXCEPT ![c] = "refreshing"]
+    /\ UNCHANGED <<store, nextTok, staleWrite>>
+
+\* A refresh is already in flight: await the SAME promise rather than
+\* issuing a second one.
+JoinInflight(c) ==
+    /\ pc[c] = "idle"
+    /\ store.exists
+    /\ leader # NoLeader
+    /\ pc' = [pc EXCEPT ![c] = "waiting"]
+    /\ UNCHANGED <<store, leader, snap, nextTok, staleWrite>>
+
+\* Everyone sharing the in-flight promise settles together.
+Settle(c, outcome) ==
+    [x \in Clients |-> IF x = c \/ pc[x] = "waiting" THEN outcome ELSE pc[x]]
+
+LeaderSucceeds(c) ==
+    /\ leader = c
+    /\ pc[c] = "refreshing"
+    /\ store'      = [exists |-> TRUE, tok |-> nextTok]
+    /\ nextTok'    = nextTok + 1
+    /\ pc'         = Settle(c, "done")
+    /\ leader'     = NoLeader
+    /\ staleWrite' = (staleWrite \/ (snap # store))
+    /\ UNCHANGED snap
+
+\* invalid_grant / 401: the refresh token is dead. Signing out is correct.
+LeaderRejectedByProvider(c) ==
+    /\ leader = c
+    /\ pc[c] = "refreshing"
+    /\ store'      = NoSession
+    /\ pc'         = Settle(c, "failed")
+    /\ leader'     = NoLeader
+    /\ staleWrite' = (staleWrite \/ (snap # store))
+    /\ UNCHANGED <<snap, nextTok>>
+
+\* Network error / 5xx: fail the callers but KEEP the session. The old code
+\* wiped the record here, turning a dropped packet into a forced re-auth.
+LeaderTransientFailure(c) ==
+    /\ leader = c
+    /\ pc[c] = "refreshing"
+    /\ pc'     = Settle(c, "failed")
+    /\ leader' = NoLeader
+    /\ UNCHANGED <<store, snap, nextTok, staleWrite>>
+
+Terminating ==
+    /\ \A c \in Clients : pc[c] \in {"done", "failed"}
+    /\ UNCHANGED vars
+
+Next ==
+    \/ \E c \in Clients :
+        \/ ReadNoSession(c) \/ AcquireAndRefresh(c) \/ JoinInflight(c)
+        \/ LeaderSucceeds(c) \/ LeaderRejectedByProvider(c) \/ LeaderTransientFailure(c)
+    \/ Terminating
+
+Spec == Init /\ [][Next]_vars
+
+(***************************************************************************)
+(* Properties -- the first two are the same statements as TokenRefresh.tla.*)
+(***************************************************************************)
+
+TypeOK ==
+    /\ store.exists \in BOOLEAN
+    /\ \A c \in Clients : pc[c] \in {"idle", "refreshing", "waiting", "done", "failed"}
+    /\ leader \in Clients \cup {NoLeader}
+
+\* Same statement as TokenRefresh.tla. Holds here: the lock means no other
+\* client can write between the leader's read and its own write.
+NoStaleOverwrite == ~staleWrite
+
+AtMostOneRefreshInFlight ==
+    Cardinality({c \in Clients : pc[c] = "refreshing"}) <= 1
+
+\* A client waiting on the shared promise never issues its own refresh.
+WaitersDoNotRefresh ==
+    \A c \in Clients : pc[c] = "refreshing" => leader = c
+
+=============================================================================

src/auth/oauth.ts

@@ -135,6 +135,18 @@ export async function completeSignIn(): Promise<ExchangeResult> {
   };
 }
 
+/**
+ * A refresh that failed. `definitive` distinguishes "this refresh token is
+ * dead, sign the user out" from "the network hiccuped, keep the session".
+ * Treating the two alike turns a dropped packet into a forced re-auth.
+ */
+export class RefreshError extends Error {
+  constructor(message: string, readonly definitive: boolean) {
+    super(message);
+    this.name = 'RefreshError';
+  }
+}
+
 export async function refreshGoogleToken(refreshToken: string): Promise<{ accessToken: string; expiresAt: number }> {
   const res = await fetch('/api/auth/google/refresh', {
     method: 'POST',
@@ -143,7 +155,11 @@ export async function refreshGoogleToken(refreshToken: string): Promise<{ access
   });
   if (!res.ok) {
     const err = await res.json().catch(() => ({ error: res.statusText }));
-    throw new Error(err.error || `Refresh failed (${res.status})`);
+    // 400 invalid_grant / 401: the grant is genuinely gone. Anything else
+    // (5xx, 429, gateway errors) is transient — a fetch rejection never
+    // reaches here at all and is transient by construction.
+    const definitive = res.status === 400 || res.status === 401;
+    throw new RefreshError(err.error || `Refresh failed (${res.status})`, definitive);
   }
   const data = await res.json();
   return {