RoostMembership

------------------------------ 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 =============================================================================

CONSTANTS Users = {u1, u2} Roles = {"admin", "member", "readonly"} Tokens = {t1, t2} Invites = {i1} NoUser = NoUser NoRole = NoRole NoUse = NoUse SPECIFICATION Spec INVARIANT TypeOK INVARIANT RemovedMemberNeverServes INVARIANT RoleAtDecisionTime INVARIANT SingleUseInvite INVARIANT TokensNameMembers CHECK_DEADLOCK FALSE