------------------------------ MODULE RoostMembership ------------------------------
(***************************************************************************)
(* Membership, roles and bearer tokens of one multi-user tenant.           *)
(*                                                                         *)
(* People join a tenant through single-use invites, hold a role that an    *)
(* administrator can change, and can be removed.  Bearer tokens (static    *)
(* API tokens and OAuth access tokens alike) are minted for a member and   *)
(* outlive membership changes: they expire or are revoked on their own     *)
(* schedule.  Every USE of a token must therefore be decided against the   *)
(* membership row at decision time -- a per-request join -- rather than    *)
(* against anything captured when the token was minted.                   *)
(*                                                                         *)
(* Modeled (mirroring a Worker + relational control plane):                *)
(*   Invite     an admin issues an invite carrying a role                  *)
(*   Join       a user redeems an invite; the redemption is one atomic      *)
(*              conditional UPDATE (consumed = 0), so an invite admits      *)
(*              exactly one user                                           *)
(*   SetRole    change an active member's role                             *)
(*   Remove     mark a member removed (the row stays; status flips)        *)
(*   MintToken  mint a token for an active member; the token row records   *)
(*              the user (and, in the mutant, the role) at mint time       *)
(*   UseToken   a request arrives with the token: the server joins the     *)
(*              token to the membership row and serves iff the member is   *)
(*              active, with the role read in that same join              *)
(*   Revoke / Expire                                                       *)
(*                                                                         *)
(* `lastUse` is an observation variable: UseToken records what was served  *)
(* and every other action clears it, so the invariants compare the served  *)
(* decision with the true membership state at that very instant.          *)
(***************************************************************************)

EXTENDS Naturals, FiniteSets

CONSTANTS
  Users,     \* people
  Roles,     \* role names; "admin" is platform-known
  Tokens,    \* pool of token identities
  Invites,   \* pool of invite identities
  NoUser,    \* model value: no user
  NoRole,    \* model value: no role
  NoUse      \* model value: no observation

ASSUME "admin" \in Roles
ASSUME NoUser \notin Users
ASSUME NoRole \notin Roles

MemberStates == {"none", "active", "removed"}
InviteStates == {"free", "issued", "consumed"}
TokenStates  == {"free", "active", "revoked", "expired"}

VARIABLES
  member,      \* Users -> membership status
  role,        \* Users -> current role (NoRole when not a member)
  inviteSt,    \* Invites -> lifecycle
  inviteRole,  \* Invites -> role the invite grants
  joins,       \* Invites -> how many users this invite admitted
  tokSt,       \* Tokens -> lifecycle
  tokUser,     \* Tokens -> the member it was minted for
  tokMintRole, \* Tokens -> the role captured at mint time (never trusted here)
  lastUse      \* observation: NoUse or [tok, user, role] served by the last step

vars == <<member, role, inviteSt, inviteRole, joins, tokSt, tokUser, tokMintRole, lastUse>>

Observations == [tok: Tokens, user: Users, role: Roles]

TypeOK ==
  /\ member \in [Users -> MemberStates]
  /\ role \in [Users -> Roles \cup {NoRole}]
  /\ inviteSt \in [Invites -> InviteStates]
  /\ inviteRole \in [Invites -> Roles \cup {NoRole}]
  /\ joins \in [Invites -> 0..2]
  /\ tokSt \in [Tokens -> TokenStates]
  /\ tokUser \in [Tokens -> Users \cup {NoUser}]
  /\ tokMintRole \in [Tokens -> Roles \cup {NoRole}]
  /\ lastUse \in Observations \cup {NoUse}

(* One founding administrator; everyone else joins by invite. *)
Init ==
  /\ \E founder \in Users :
       /\ member = [u \in Users |-> IF u = founder THEN "active" ELSE "none"]
       /\ role = [u \in Users |-> IF u = founder THEN "admin" ELSE NoRole]
  /\ inviteSt = [i \in Invites |-> "free"]
  /\ inviteRole = [i \in Invites |-> NoRole]
  /\ joins = [i \in Invites |-> 0]
  /\ tokSt = [t \in Tokens |-> "free"]
  /\ tokUser = [t \in Tokens |-> NoUser]
  /\ tokMintRole = [t \in Tokens |-> NoRole]
  /\ lastUse = NoUse

Invite(i, r) ==
  /\ inviteSt[i] = "free"
  /\ inviteSt' = [inviteSt EXCEPT ![i] = "issued"]
  /\ inviteRole' = [inviteRole EXCEPT ![i] = r]
  /\ lastUse' = NoUse
  /\ UNCHANGED <<member, role, joins, tokSt, tokUser, tokMintRole>>

(* The atomic conditional UPDATE: only an issued invite admits, and it flips
   to consumed in the same step. A returning removed member may rejoin. *)
Join(i, u) ==
  /\ inviteSt[i] = "issued"
  /\ member[u] # "active"
  /\ inviteSt' = [inviteSt EXCEPT ![i] = "consumed"]
  /\ joins' = [joins EXCEPT ![i] = @ + 1]
  /\ member' = [member EXCEPT ![u] = "active"]
  /\ role' = [role EXCEPT ![u] = inviteRole[i]]
  /\ lastUse' = NoUse
  /\ UNCHANGED <<inviteRole, tokSt, tokUser, tokMintRole>>

SetRole(u, r) ==
  /\ member[u] = "active"
  /\ role[u] # r
  /\ role' = [role EXCEPT ![u] = r]
  /\ lastUse' = NoUse
  /\ UNCHANGED <<member, inviteSt, inviteRole, joins, tokSt, tokUser, tokMintRole>>

Remove(u) ==
  /\ member[u] = "active"
  /\ member' = [member EXCEPT ![u] = "removed"]
  /\ role' = [role EXCEPT ![u] = NoRole]
  /\ lastUse' = NoUse
  /\ UNCHANGED <<inviteSt, inviteRole, joins, tokSt, tokUser, tokMintRole>>

MintToken(t, u) ==
  /\ tokSt[t] = "free"
  /\ member[u] = "active"
  /\ tokSt' = [tokSt EXCEPT ![t] = "active"]
  /\ tokUser' = [tokUser EXCEPT ![t] = u]
  /\ tokMintRole' = [tokMintRole EXCEPT ![t] = role[u]]
  /\ lastUse' = NoUse
  /\ UNCHANGED <<member, role, inviteSt, inviteRole, joins>>

(* The per-request join: the token row is joined to the membership row and
   the request is served only if that row is active, with the role read
   from that row.  Nothing captured at mint time takes part. *)
UseToken(t) ==
  /\ tokSt[t] = "active"
  /\ member[tokUser[t]] = "active"
  /\ lastUse' = [tok |-> t, user |-> tokUser[t], role |-> role[tokUser[t]]]
  /\ UNCHANGED <<member, role, inviteSt, inviteRole, joins, tokSt, tokUser, tokMintRole>>

RevokeToken(t) ==
  /\ tokSt[t] = "active"
  /\ tokSt' = [tokSt EXCEPT ![t] = "revoked"]
  /\ lastUse' = NoUse
  /\ UNCHANGED <<member, role, inviteSt, inviteRole, joins, tokUser, tokMintRole>>

ExpireToken(t) ==
  /\ tokSt[t] = "active"
  /\ tokSt' = [tokSt EXCEPT ![t] = "expired"]
  /\ lastUse' = NoUse
  /\ UNCHANGED <<member, role, inviteSt, inviteRole, joins, tokUser, tokMintRole>>

Next ==
  \/ \E i \in Invites, r \in Roles : Invite(i, r)
  \/ \E i \in Invites, u \in Users : Join(i, u)
  \/ \E u \in Users, r \in Roles : SetRole(u, r)
  \/ \E u \in Users : Remove(u)
  \/ \E t \in Tokens, u \in Users : MintToken(t, u)
  \/ \E t \in Tokens : UseToken(t) \/ RevokeToken(t) \/ ExpireToken(t)

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

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

(* A request served with a token belongs to a member who is active NOW. *)
RemovedMemberNeverServes ==
  lastUse # NoUse => member[lastUse.user] = "active"

(* The role a request is served with is the member's role NOW, never the
   role at mint time. *)
RoleAtDecisionTime ==
  lastUse # NoUse => lastUse.role = role[lastUse.user]

(* An invite admits at most one person. *)
SingleUseInvite ==
  \A i \in Invites : joins[i] <= 1

(* A token always belongs to someone who was a member when it was minted. *)
TokensNameMembers ==
  \A t \in Tokens : tokSt[t] # "free" => tokUser[t] \in Users

=============================================================================