Hello from MCP server
---------------------------- MODULE DataAccessLayer ----------------------------
(*
* TLA+ Specification of Pricebook Platform Data Access Layer
*
* This spec models the high-level behavior of the hybrid dual-database
* architecture with remote PocketBase and local SQLite synchronization.
*)
EXTENDS Naturals, Sequences, FiniteSets
CONSTANTS
Users, \* Set of user IDs
Organizations, \* Set of organization IDs
Collections, \* Set of collection names (books, menus, etc.)
Actions, \* {create, read, update, delete, list}
Roles \* {admin, author, tech, support}
VARIABLES
remoteDb, \* Remote PocketBase: [org -> [collection -> records]]
localDb, \* Local SQLite cache: [collection -> records]
syncTime, \* Last sync timestamp
permCache, \* Permission cache: [org -> [role -> [action -> [collection -> allow/deny]]]]
userSessions, \* Active user sessions: [user -> {org, roles, authToken}]
pendingChanges, \* Changesets awaiting application
clock \* Logical clock for sync timing
vars == <<remoteDb, localDb, syncTime, permCache, userSessions, pendingChanges, clock>>
-----------------------------------------------------------------------------
(* Type Definitions *)
Record == [id: Nat, data: Nat, org: Organizations, refId: Nat]
Session == [org: Organizations, roles: SUBSET Roles, authenticated: BOOLEAN]
Change == [op: {"create", "update", "delete"}, collection: Collections, record: Record]
TypeInvariant ==
/\ remoteDb \in [Organizations -> [Collections -> SUBSET Record]]
/\ localDb \in [Collections -> SUBSET Record]
/\ syncTime \in Nat
/\ clock \in Nat
-----------------------------------------------------------------------------
(* Permission Checking *)
\* Check if a role has permission for an action on a collection
HasPermission(org, role, action, collection) ==
permCache[org][role][action][collection] = "allow"
\* Check if user can perform action (any of their roles grants it)
UserCanPerform(user, action, collection) ==
LET session == userSessions[user]
org == session.org
IN \E role \in session.roles: HasPermission(org, role, action, collection)
\* Admin bypass - admins can do anything
IsAdmin(user) ==
"admin" \in userSessions[user].roles
\* Authorization check combining admin bypass and role permissions
Authorized(user, action, collection) ==
/\ userSessions[user].authenticated
/\ (IsAdmin(user) \/ UserCanPerform(user, action, collection))
-----------------------------------------------------------------------------
(* CRUD Operations - Remote Database *)
\* CREATE: Add a new record to remote database
Create(user, collection, record) ==
/\ Authorized(user, "create", collection)
/\ LET org == userSessions[user].org
IN remoteDb' = [remoteDb EXCEPT ![org][collection] = @ \union {record}]
/\ UNCHANGED <<localDb, syncTime, permCache, userSessions, pendingChanges, clock>>
\* READ: Query records from remote (returns subset matching filter)
Read(user, collection, filter) ==
/\ Authorized(user, "read", collection)
/\ UNCHANGED vars \* Read is a query, no state change
\* UPDATE: Modify existing record in remote database
Update(user, collection, recordId, newData) ==
/\ Authorized(user, "update", collection)
/\ LET org == userSessions[user].org
oldRecord == CHOOSE r \in remoteDb[org][collection]: r.id = recordId
newRecord == [oldRecord EXCEPT !.data = newData]
IN remoteDb' = [remoteDb EXCEPT
![org][collection] = (@ \ {oldRecord}) \union {newRecord}]
/\ UNCHANGED <<localDb, syncTime, permCache, userSessions, pendingChanges, clock>>
\* DELETE: Remove record from remote database
Delete(user, collection, recordId) ==
/\ Authorized(user, "delete", collection)
/\ LET org == userSessions[user].org
record == CHOOSE r \in remoteDb[org][collection]: r.id = recordId
IN remoteDb' = [remoteDb EXCEPT ![org][collection] = @ \ {record}]
/\ UNCHANGED <<localDb, syncTime, permCache, userSessions, pendingChanges, clock>>
-----------------------------------------------------------------------------
(* Synchronization *)
SYNC_INTERVAL == 10 \* 10 time units between syncs
\* Check if sync is needed (10 minutes elapsed)
SyncNeeded == clock - syncTime >= SYNC_INTERVAL
\* Sync remote to local for a given organization
SyncDatabase(user) ==
/\ SyncNeeded
/\ userSessions[user].authenticated
/\ LET org == userSessions[user].org
IN localDb' = [c \in Collections |-> remoteDb[org][c]]
/\ syncTime' = clock
/\ UNCHANGED <<remoteDb, permCache, userSessions, pendingChanges, clock>>
\* Time advances
Tick ==
/\ clock' = clock + 1
/\ UNCHANGED <<remoteDb, localDb, syncTime, permCache, userSessions, pendingChanges>>
-----------------------------------------------------------------------------
(* Changeset Processing - Batch Updates *)
\* Validate a changeset before applying
ValidateChangeset(change) ==
/\ change.collection \in Collections
/\ change.op \in {"create", "update", "delete"}
\* Apply a single change within a transaction context
ApplyChange(org, change) ==
CASE change.op = "create" ->
remoteDb' = [remoteDb EXCEPT ![org][change.collection] =
@ \union {change.record}]
[] change.op = "update" ->
LET old == CHOOSE r \in remoteDb[org][change.collection]:
r.refId = change.record.refId
IN remoteDb' = [remoteDb EXCEPT ![org][change.collection] =
(@ \ {old}) \union {change.record}]
[] change.op = "delete" ->
LET old == CHOOSE r \in remoteDb[org][change.collection]:
r.refId = change.record.refId
IN remoteDb' = [remoteDb EXCEPT ![org][change.collection] = @ \ {old}]
\* Process all pending changesets atomically (transaction)
ProcessChangesets(user) ==
/\ pendingChanges # <<>>
/\ Authorized(user, "update", "pricebookChanges")
/\ \A change \in Range(pendingChanges): ValidateChangeset(change)
/\ LET org == userSessions[user].org
IN \* Apply all changes - in real impl this is in a transaction
/\ \A i \in 1..Len(pendingChanges): ApplyChange(org, pendingChanges[i])
/\ pendingChanges' = <<>>
/\ UNCHANGED <<localDb, syncTime, permCache, userSessions, clock>>
-----------------------------------------------------------------------------
(* Authentication *)
\* User logs in and establishes session
Login(user, org, roles) ==
/\ userSessions' = [userSessions EXCEPT ![user] =
[org |-> org, roles |-> roles, authenticated |-> TRUE]]
/\ UNCHANGED <<remoteDb, localDb, syncTime, permCache, pendingChanges, clock>>
\* User logs out
Logout(user) ==
/\ userSessions' = [userSessions EXCEPT ![user].authenticated = FALSE]
/\ UNCHANGED <<remoteDb, localDb, syncTime, permCache, pendingChanges, clock>>
\* Refresh auth token (called by getApi)
AuthRefresh(user) ==
/\ userSessions[user].authenticated
/\ UNCHANGED vars \* Token refresh doesn't change logical state
-----------------------------------------------------------------------------
(* Organization Creation Hook *)
\* When a new org is created, initialize default permissions and roles
CreateOrganization(user, newOrg) ==
/\ IsAdmin(user)
/\ remoteDb' = [remoteDb EXCEPT
![newOrg] = [c \in Collections |-> {}]]
/\ permCache' = [permCache EXCEPT
![newOrg] = [r \in Roles |-> [a \in Actions |-> [c \in Collections |->
IF r = "admin" THEN "allow" ELSE "deny"]]]]
/\ UNCHANGED <<localDb, syncTime, userSessions, pendingChanges, clock>>
-----------------------------------------------------------------------------
(* Local Database Operations - Offline Reads *)
\* Read from local cache (no auth check - already synced)
LocalRead(collection) ==
/\ UNCHANGED vars \* Read operation, returns localDb[collection]
\* Check if local data is stale
LocalDataStale == clock - syncTime > SYNC_INTERVAL
-----------------------------------------------------------------------------
(* Safety Properties *)
\* All local data corresponds to authorized remote data
LocalDataConsistency ==
\A c \in Collections:
localDb[c] \subseteq UNION {remoteDb[o][c]: o \in Organizations}
\* Users can only access data from their active organization
OrganizationIsolation ==
\A u \in Users:
userSessions[u].authenticated =>
LET org == userSessions[u].org
IN localDb = [c \in Collections |-> remoteDb[org][c]]
\/ LocalDataStale
\* Permission cache matches actual permission grants
PermissionCacheValid ==
\* In real system, cache is built from permissions collection
TRUE
-----------------------------------------------------------------------------
(* Liveness Properties *)
\* Eventually data will sync
EventuallySynced ==
[]<>(~LocalDataStale)
\* All valid changesets are eventually processed
ChangesetsProcessed ==
[](pendingChanges # <<>> => <>(pendingChanges = <<>>))
-----------------------------------------------------------------------------
(* Initial State *)
Init ==
/\ remoteDb = [o \in Organizations |-> [c \in Collections |-> {}]]
/\ localDb = [c \in Collections |-> {}]
/\ syncTime = 0
/\ clock = 0
/\ permCache = [o \in Organizations |->
[r \in Roles |-> [a \in Actions |-> [c \in Collections |-> "deny"]]]]
/\ userSessions = [u \in Users |->
[org |-> CHOOSE o \in Organizations: TRUE,
roles |-> {},
authenticated |-> FALSE]]
/\ pendingChanges = <<>>
\* Next state relation
Next ==
\/ \E u \in Users, c \in Collections, r \in Record:
Create(u, c, r) \/ Read(u, c, {}) \/ Update(u, c, r.id, r.data) \/ Delete(u, c, r.id)
\/ \E u \in Users: SyncDatabase(u) \/ ProcessChangesets(u) \/ AuthRefresh(u)
\/ \E u \in Users, o \in Organizations, rs \in SUBSET Roles: Login(u, o, rs)
\/ \E u \in Users: Logout(u)
\/ \E u \in Users, o \in Organizations: CreateOrganization(u, o)
\/ Tick
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
-----------------------------------------------------------------------------
(* Helper *)
Range(seq) == {seq[i]: i \in 1..Len(seq)}
=============================================================================