---- MODULE TpxRefresh ----
(***************************************************************************)
(* Client-side refresh-token rotation for the browser-direct TPX OAuth     *)
(* client (apps/web/src/lib/tpx.ts).                                       *)
(*                                                                         *)
(* The authorization server keeps ONE valid refresh-token generation       *)
(* (asGen).  A refresh presenting the current generation succeeds and      *)
(* rotates it (asGen + 1); presenting a stale generation is reuse and      *)
(* REVOKES the whole grant permanently.  Two browser tabs share one        *)
(* localStorage slot holding the latest known generation; each tab does    *)
(* read slot -> refresh -> write rotated token back.                       *)
(*                                                                         *)
(* The constant UseLock selects the design:                                *)
(*   FALSE: tabs interleave freely between read, request, and write-back.  *)
(*   TRUE:  the read-refresh-write section is a cross-tab critical         *)
(*          section (the Web Lock in accessToken()).                       *)
(*                                                                         *)
(* With UseLock = FALSE, TLC violates GrantSurvives in 5 states — the      *)
(* lost-token race that makes the Web Lock necessary, not defensive:       *)
(*   1. init: asGen = 0, slot = 0                                          *)
(*   2. Enter(t1): t1 reads slot, holds generation 0                       *)
(*   3. RefreshOK(t1): server rotates, asGen = 1; t1 holds 1, slot         *)
(*      still 0 (t1 has not written back yet)                              *)
(*   4. Enter(t2): t2 reads slot, holds STALE generation 0                 *)
(*   5. RefreshStale(t2): t2 presents 0 while asGen = 1 -> reuse           *)
(*      detected, revoked = TRUE.  GrantSurvives violated.                 *)
(* (17 states generated, 14 distinct.)                                     *)
(*                                                                         *)
(* The checked-in TpxRefresh.cfg uses UseLock = TRUE and passes            *)
(* (51 states generated, 49 distinct, depth 13): with the critical         *)
(* section, an honest pair of tabs can never trip reuse detection.         *)
(***************************************************************************)
EXTENDS Naturals, TLC

CONSTANT UseLock

MaxGen       == 4                \* 2 tabs x 2 refreshes: 4 rotations suffice
Tabs         == {"t1", "t2"}
MaxRefreshes == 2                \* per-tab refresh budget (bounds the model)
NoTab        == "none"
Gens         == 0..MaxGen

VARIABLES
  asGen,    \* authorization server: the one currently-valid refresh generation
  revoked,  \* TRUE once the server detects reuse and kills the grant
  slot,     \* shared storage slot: latest refresh generation known to clients
  lock,     \* mutex holder (meaningful only when UseLock)
  tab       \* per-tab client state

vars == <<asGen, revoked, slot, lock, tab>>

TabStates == [phase: {"idle", "read", "got"}, tok: Gens, done: 0..MaxRefreshes]

TypeOK ==
  /\ asGen \in Gens
  /\ revoked \in BOOLEAN
  /\ slot \in Gens
  /\ lock \in Tabs \cup {NoTab}
  /\ tab \in [Tabs -> TabStates]

Init ==
  /\ asGen = 0
  /\ revoked = FALSE
  /\ slot = 0
  /\ lock = NoTab
  /\ tab = [t \in Tabs |-> [phase |-> "idle", tok |-> 0, done |-> 0]]

Release(t) == IF lock = t THEN NoTab ELSE lock

(* Tab enters its refresh path: acquire the lock (a no-op when UseLock is  *)
(* FALSE) and read the shared slot.  The Web Locks callback reads storage  *)
(* immediately on entry, so acquire+read is one step in both designs.      *)
Enter(t) ==
  /\ tab[t].phase = "idle"
  /\ tab[t].done < MaxRefreshes
  /\ ~revoked
  /\ (UseLock => lock = NoTab)
  /\ lock' = IF UseLock THEN t ELSE lock
  /\ tab' = [tab EXCEPT ![t].phase = "read", ![t].tok = slot]
  /\ UNCHANGED <<asGen, revoked, slot>>

(* Server: the presented token is current -> rotate and hand out the next  *)
(* generation.  Request + response are one atomic step (the server's       *)
(* token endpoint is transactional).                                       *)
RefreshOK(t) ==
  /\ tab[t].phase = "read"
  /\ ~revoked
  /\ tab[t].tok = asGen
  /\ asGen < MaxGen
  /\ asGen' = asGen + 1
  /\ tab' = [tab EXCEPT ![t].phase = "got", ![t].tok = asGen + 1]
  /\ UNCHANGED <<revoked, slot, lock>>

(* Server: the presented token is stale -> reuse detection revokes the     *)
(* grant.  The client sees the rejection, drops its state, and releases    *)
(* the lock (tpx.ts clears tpx.tokens and throws NeedsGrantError).         *)
RefreshStale(t) ==
  /\ tab[t].phase = "read"
  /\ tab[t].tok # asGen
  /\ revoked' = TRUE
  /\ tab' = [tab EXCEPT ![t].phase = "idle", ![t].tok = 0, ![t].done = @ + 1]
  /\ lock' = Release(t)
  /\ UNCHANGED <<asGen, slot>>

(* Tab persists the rotated token to the shared slot and leaves the        *)
(* critical section.                                                       *)
WriteBack(t) ==
  /\ tab[t].phase = "got"
  /\ slot' = tab[t].tok
  /\ tab' = [tab EXCEPT ![t].phase = "idle", ![t].done = @ + 1]
  /\ lock' = Release(t)
  /\ UNCHANGED <<asGen, revoked>>

Next ==
  \E t \in Tabs : Enter(t) \/ RefreshOK(t) \/ RefreshStale(t) \/ WriteBack(t)

Spec == Init /\ [][Next]_vars

----------------------------------------------------------------------------
(* Invariants *)

(* Honest clients never trip reuse detection: the grant survives. *)
GrantSurvives == ~revoked

====