diff --git a/spec/README.md b/spec/README.md index 2a93bda63..c183b1a9b 100644 --- a/spec/README.md +++ b/spec/README.md @@ -4,17 +4,23 @@ This directory contains the formal TLA+ specification for the MetaBuilder system ## Overview -The specification models the core invariants and behaviors of MetaBuilder, including: +The specification models both current and future MetaBuilder functionality through multiple TLA+ modules: +**Core System Specifications:** - **6-Level Permission System**: Hierarchical access control (Public → User → Moderator → Admin → God → Supergod) - **Multi-Tenant Data Isolation**: Strict separation of data between tenants - **Database Abstraction Layer (DBAL)**: Query processing with security guarantees - **Package Management**: Installation, enabling, and disabling of feature packages - **Audit Logging**: Complete tracking of privileged operations +**Future Functionality Specifications:** +- **Workflow System**: Workflow execution, scheduling, and state management +- **Real-Time Collaboration**: Concurrent editing, presence, comments, and mentions +- **Integration Ecosystem**: Webhooks, OAuth apps, API keys, and rate limiting + ## Files -### `metabuilder.tla` +### Core System: `metabuilder.tla` The main TLA+ specification file that defines: @@ -42,6 +48,86 @@ Configuration file for the TLC model checker that specifies: - Temporal properties to verify - State space constraints for bounded model checking +### Future Functionality: `workflow_system.tla` + +Specification for advanced workflow execution features: + +- **Template Management**: God-level users create and manage workflow templates +- **Workflow Execution**: Admin-level users trigger manual or scheduled workflows +- **Step Dependencies**: Define and enforce execution order constraints +- **Error Handling**: Automatic retry logic with configurable limits +- **Concurrency Control**: Limit concurrent workflow executions per tenant +- **Safety Properties**: + - `GodOnlyTemplateCreation`: Only Level 5+ users can author workflows + - `AdminOnlyExecution`: Only Level 4+ users can execute workflows + - `TenantIsolation`: Workflows are strictly isolated by tenant + - `ConcurrencyLimit`: Per-tenant concurrent execution limits + - `RetryLimit`: Failed steps don't exceed retry threshold + - `DependencyEnforcement`: Steps execute only after dependencies complete +- **Liveness Properties**: + - `EventualStepExecution`: Pending steps eventually execute + - `EventualCompletion`: Running workflows eventually complete or fail + - `EventualScheduleTrigger`: Scheduled workflows eventually trigger + +### `workflow_system.cfg` + +Configuration for workflow system model checking with workflow templates, steps, and execution limits. + +### Future Functionality: `collaboration.tla` + +Specification for real-time collaboration features: + +- **Session Management**: User connection, idle, and disconnection states +- **Concurrent Editing**: Multiple users editing documents simultaneously +- **Comments and Mentions**: Users can comment and mention others in documents +- **Presence Tracking**: Real-time user online/idle/offline status +- **Notifications**: Mention notifications with read status tracking +- **Version History**: Document snapshot creation and tracking +- **Safety Properties**: + - `DocumentTenantIsolation`: Editors can only access documents in their tenant + - `ConcurrentEditorLimit`: Maximum concurrent editors per document + - `CommentTenantConsistency`: Comments belong to document's tenant + - `MentionTenantIsolation`: Mentions stay within tenant boundaries + - `NotificationLimit`: Pending notifications don't exceed limits + - `DisconnectedNotEditing`: Disconnected users automatically stop editing + - `OperationAuthorship`: All operations come from authorized editors +- **Liveness Properties**: + - `EventualNotificationHandling`: Notifications eventually get read or cleared + - `EventualMentionRead`: Mentioned users eventually see their mentions + - `EventualStopEditing`: Active editors eventually stop or disconnect + +### `collaboration.cfg` + +Configuration for collaboration model checking with documents, comments, and concurrent editors. + +### Future Functionality: `integrations.tla` + +Specification for integration ecosystem: + +- **Webhook Management**: Create, configure, and manage webhooks for events +- **OAuth Applications**: OAuth app lifecycle and token management +- **API Key Management**: User-level API key creation and expiration +- **Event Subscriptions**: Subscribe to and filter system events +- **Rate Limiting**: Track and enforce API call rate limits per identity +- **Delivery Guarantees**: Webhook delivery with retry logic +- **Safety Properties**: + - `AdminOnlyIntegrationManagement`: Only Level 4+ users manage integrations + - `WebhookTenantLimit`: Webhooks per tenant don't exceed limits + - `APIKeyUserLimit`: API keys per user don't exceed limits + - `RateLimitEnforcement`: API calls respect rate limits + - `WebhookTenantIsolation`: Webhooks isolated by tenant + - `OAuthAppTenantIsolation`: OAuth apps isolated by tenant + - `TokenTenantConsistency`: OAuth tokens match app tenants + - `ActiveDeliveriesQueued`: Active deliveries are properly queued +- **Liveness Properties**: + - `EventualDeliveryCompletion`: Webhook deliveries eventually complete or fail + - `EventualRetryOrFail`: Failed deliveries retry or permanently fail + - `EventualExpiration`: Expired API keys eventually marked as expired + +### `integrations.cfg` + +Configuration for integration ecosystem model checking with webhooks, OAuth apps, and API keys. + ## Key Concepts ### Permission Levels @@ -215,6 +301,58 @@ This specification aligns with the MetaBuilder architecture documentation: - `docs/architecture/data/data-driven-architecture.md` → Package system - `dbal/README.md` → DBAL state machine and security model - `README.md` → Multi-tenant system +- `docs/todo/improvements/20-FUTURE-FEATURES-TODO.md` → Future features specifications + +## Modeling Future Features + +The TLA+ specifications for future features serve multiple purposes: + +### 1. Design Validation +Before implementing complex features like workflows or real-time collaboration, the formal specifications help: +- Identify potential race conditions and deadlocks +- Verify that permission enforcement is complete +- Ensure multi-tenant isolation is maintained +- Validate concurrency control mechanisms + +### 2. API Contract Definition +The specifications define precise contracts for: +- **Workflow System**: Template creation, execution triggers, step dependencies +- **Collaboration**: Session management, concurrent editing, notification delivery +- **Integrations**: Webhook delivery guarantees, OAuth token lifecycle, rate limiting + +### 3. Implementation Guide +Each specification provides: +- Clear state transitions for the system to implement +- Invariants that must be maintained by the implementation +- Temporal properties describing expected system behavior +- Edge cases that must be handled (retries, failures, disconnections) + +### 4. Testing Blueprint +The specifications can guide: +- Property-based testing strategies +- Concurrency test scenarios +- Multi-tenant isolation test cases +- Load testing parameters (rate limits, concurrent users) + +### Running Future Feature Specs + +Model check individual future features: + +```bash +# Check workflow system +java -cp tla2tools.jar tlc2.TLC spec/workflow_system.tla -config spec/workflow_system.cfg + +# Check collaboration system +java -cp tla2tools.jar tlc2.TLC spec/collaboration.tla -config spec/collaboration.cfg + +# Check integrations system +java -cp tla2tools.jar tlc2.TLC spec/integrations.tla -config spec/integrations.cfg +``` + +Each specification is standalone and can be verified independently. This modular approach allows: +- Parallel verification of different subsystems +- Incremental feature development +- Focused debugging when invariants are violated ## References diff --git a/spec/collaboration.cfg b/spec/collaboration.cfg new file mode 100644 index 000000000..0be18c032 --- /dev/null +++ b/spec/collaboration.cfg @@ -0,0 +1,32 @@ +SPECIFICATION Spec + +CONSTANTS + Users = {u1, u2, u3} + Tenants = {t1, t2} + Documents = {doc1, doc2} + MaxConcurrentEditors = 3 + MaxNotifications = 10 + +INVARIANTS + TypeOK + DocumentTenantIsolation + ConcurrentEditorLimit + CommentTenantConsistency + MentionTenantIsolation + NotificationLimit + ActiveEditorsOnly + DisconnectedNotEditing + OperationAuthorship + VersionConsistency + +PROPERTIES + EventualNotificationHandling + EventualMentionRead + EventualStopEditing + +\* Constraint to limit state space for model checking +CONSTRAINT + /\ Cardinality(comments) <= 5 + /\ Cardinality(mentions) <= 5 + /\ \A u \in Users: Len(notifications[u]) <= 8 + /\ \A t \in Tenants: Len(activityFeed[t]) <= 12 diff --git a/spec/collaboration.tla b/spec/collaboration.tla new file mode 100644 index 000000000..028eede2a --- /dev/null +++ b/spec/collaboration.tla @@ -0,0 +1,542 @@ +---------------------------- MODULE collaboration ---------------------------- +(*************************************************************************** + * Real-Time Collaboration Specification for MetaBuilder * + * * + * This specification models real-time collaboration features including: * + * - Concurrent document editing with operational transformation * + * - User presence and activity tracking * + * - Commenting and mentioning system * + * - Activity feeds and notifications * + * - Conflict detection and resolution * + * - Session management and connection handling * + ***************************************************************************) + +EXTENDS Naturals, Sequences, FiniteSets, TLC + +CONSTANTS + Users, \* Set of all users + Tenants, \* Set of tenants + Documents, \* Set of documents + MaxConcurrentEditors, \* Maximum concurrent editors per document + MaxNotifications \* Maximum pending notifications per user + +VARIABLES + userTenants, \* User -> Tenant + userSessions, \* User -> Session state {active, idle, disconnected} + documentOwners, \* Document -> User (owner) + documentTenants, \* Document -> Tenant + documentContent, \* Document -> Sequence of operations + documentEditors, \* Document -> Set of Users (currently editing) + userPresence, \* User -> {online, idle, offline} + comments, \* Set of comment records + mentions, \* Set of mention records + notifications, \* User -> Sequence of notifications + activityFeed, \* Tenant -> Sequence of activities + versionHistory \* Document -> Sequence of versions + +vars == <> + +----------------------------------------------------------------------------- +(* Type Definitions *) + +SessionState == {"active", "idle", "disconnected"} +PresenceState == {"online", "idle", "offline"} +OperationType == {"insert", "delete", "replace", "format"} + +Operation == [ + type: OperationType, + position: Nat, + content: STRING, + user: Users, + timestamp: Nat +] + +Comment == [ + id: Nat, + documentId: Documents, + userId: Users, + tenantId: Tenants, + content: STRING, + position: Nat, + timestamp: Nat, + resolved: BOOLEAN +] + +Mention == [ + id: Nat, + commentId: Nat, + mentionedUser: Users, + mentioningUser: Users, + tenantId: Tenants, + timestamp: Nat, + read: BOOLEAN +] + +Notification == [ + id: Nat, + userId: Users, + type: STRING, + sourceId: Nat, + message: STRING, + timestamp: Nat, + read: BOOLEAN +] + +Activity == [ + userId: Users, + tenantId: Tenants, + action: STRING, + targetId: Nat, + timestamp: Nat +] + +Version == [ + documentId: Documents, + content: Seq(Operation), + createdBy: Users, + timestamp: Nat, + versionNumber: Nat +] + +TypeOK == + /\ userTenants \in [Users -> Tenants] + /\ userSessions \in [Users -> SessionState] + /\ documentOwners \in [Documents -> Users] + /\ documentTenants \in [Documents -> Tenants] + /\ documentContent \in [Documents -> Seq(Operation)] + /\ documentEditors \in [Documents -> SUBSET Users] + /\ userPresence \in [Users -> PresenceState] + /\ comments \subseteq Comment + /\ mentions \subseteq Mention + /\ notifications \in [Users -> Seq(Notification)] + /\ activityFeed \in [Tenants -> Seq(Activity)] + /\ versionHistory \in [Documents -> Seq(Version)] + +----------------------------------------------------------------------------- +(* Permission Checks *) + +\* User can access document if in same tenant +CanAccessDocument(user, doc) == + userTenants[user] = documentTenants[doc] + +\* User can edit if they can access and not too many concurrent editors +CanEditDocument(user, doc) == + /\ CanAccessDocument(user, doc) + /\ Cardinality(documentEditors[doc]) < MaxConcurrentEditors + +\* User can comment if they can access +CanComment(user, doc) == + CanAccessDocument(user, doc) + +----------------------------------------------------------------------------- +(* Helper Functions *) + +\* Count pending notifications for a user +CountPendingNotifications(user) == + LET unread == {n \in 1..Len(notifications[user]) : + ~notifications[user][n].read} + IN Cardinality(unread) + +\* Get comment by ID +GetComment(cid) == + CHOOSE c \in comments : c.id = cid + +\* Check if user is mentioned in a comment +IsMentioned(user, comment) == + \E m \in mentions : + /\ m.commentId = comment.id + /\ m.mentionedUser = user + +----------------------------------------------------------------------------- +(* Initial State *) + +Init == + /\ userTenants \in [Users -> Tenants] + /\ userSessions = [u \in Users |-> "disconnected"] + /\ documentOwners \in [Documents -> Users] + /\ documentTenants \in [Documents -> Tenants] + /\ documentContent = [d \in Documents |-> <<>>] + /\ documentEditors = [d \in Documents |-> {}] + /\ userPresence = [u \in Users |-> "offline"] + /\ comments = {} + /\ mentions = {} + /\ notifications = [u \in Users |-> <<>>] + /\ activityFeed = [t \in Tenants |-> <<>>] + /\ versionHistory = [d \in Documents |-> <<>>] + +----------------------------------------------------------------------------- +(* Session Management *) + +\* User connects and becomes active +UserConnect(user) == + /\ userSessions[user] = "disconnected" + /\ userSessions' = [userSessions EXCEPT ![user] = "active"] + /\ userPresence' = [userPresence EXCEPT ![user] = "online"] + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "connected", + targetId |-> 0, + timestamp |-> Len(activityFeed[userTenants[user]]) + ])] + /\ UNCHANGED <> + +\* User becomes idle +UserGoIdle(user) == + /\ userSessions[user] = "active" + /\ userSessions' = [userSessions EXCEPT ![user] = "idle"] + /\ userPresence' = [userPresence EXCEPT ![user] = "idle"] + /\ UNCHANGED <> + +\* User disconnects +UserDisconnect(user) == + /\ userSessions[user] \in {"active", "idle"} + /\ userSessions' = [userSessions EXCEPT ![user] = "disconnected"] + /\ userPresence' = [userPresence EXCEPT ![user] = "offline"] + /\ documentEditors' = [d \in Documents |-> + IF user \in documentEditors[d] + THEN documentEditors[d] \ {user} + ELSE documentEditors[d]] + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "disconnected", + targetId |-> 0, + timestamp |-> Len(activityFeed[userTenants[user]]) + ])] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Document Editing *) + +\* User starts editing a document +StartEditing(user, doc) == + /\ userSessions[user] = "active" + /\ CanEditDocument(user, doc) + /\ user \notin documentEditors[doc] + /\ documentEditors' = [documentEditors EXCEPT ![doc] = @ \cup {user}] + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "start_editing", + targetId |-> doc, + timestamp |-> Len(activityFeed[userTenants[user]]) + ])] + /\ UNCHANGED <> + +\* User stops editing a document +StopEditing(user, doc) == + /\ user \in documentEditors[doc] + /\ documentEditors' = [documentEditors EXCEPT ![doc] = @ \ {user}] + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "stop_editing", + targetId |-> doc, + timestamp |-> Len(activityFeed[userTenants[user]]) + ])] + /\ UNCHANGED <> + +\* User applies an operation to a document +ApplyOperation(user, doc, op) == + /\ user \in documentEditors[doc] + /\ userSessions[user] = "active" + /\ CanAccessDocument(user, doc) + /\ op.user = user + /\ op.type \in OperationType + /\ documentContent' = [documentContent EXCEPT + ![doc] = Append(@, op)] + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "edit_document", + targetId |-> doc, + timestamp |-> Len(activityFeed[userTenants[user]]) + ])] + /\ UNCHANGED <> + +\* Create a version snapshot +CreateVersion(user, doc) == + /\ user = documentOwners[doc] + /\ CanAccessDocument(user, doc) + /\ LET + versionNum == Len(versionHistory[doc]) + 1 + newVersion == [ + documentId |-> doc, + content |-> documentContent[doc], + createdBy |-> user, + timestamp |-> versionNum, + versionNumber |-> versionNum + ] + IN + /\ versionHistory' = [versionHistory EXCEPT + ![doc] = Append(@, newVersion)] + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "create_version", + targetId |-> doc, + timestamp |-> Len(activityFeed[userTenants[user]]) + ])] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Comments and Mentions *) + +\* User adds a comment +AddComment(user, doc, cid, content, position) == + /\ userSessions[user] = "active" + /\ CanComment(user, doc) + /\ cid \notin {c.id : c \in comments} + /\ LET newComment == [ + id |-> cid, + documentId |-> doc, + userId |-> user, + tenantId |-> userTenants[user], + content |-> content, + position |-> position, + timestamp |-> Len(activityFeed[userTenants[user]]), + resolved |-> FALSE + ] IN + /\ comments' = comments \cup {newComment} + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "add_comment", + targetId |-> cid, + timestamp |-> Len(@) + ])] + /\ UNCHANGED <> + +\* User mentions another user in a comment +MentionUser(user, mentionedUser, cid, mid) == + /\ userSessions[user] = "active" + /\ \E c \in comments : c.id = cid /\ c.userId = user + /\ userTenants[user] = userTenants[mentionedUser] + /\ mid \notin {m.id : m \in mentions} + /\ CountPendingNotifications(mentionedUser) < MaxNotifications + /\ LET + comment == GetComment(cid) + newMention == [ + id |-> mid, + commentId |-> cid, + mentionedUser |-> mentionedUser, + mentioningUser |-> user, + tenantId |-> userTenants[user], + timestamp |-> Len(activityFeed[userTenants[user]]), + read |-> FALSE + ] + newNotif == [ + id |-> mid, + userId |-> mentionedUser, + type |-> "mention", + sourceId |-> cid, + message |-> "You were mentioned in a comment", + timestamp |-> Len(notifications[mentionedUser]), + read |-> FALSE + ] + IN + /\ mentions' = mentions \cup {newMention} + /\ notifications' = [notifications EXCEPT + ![mentionedUser] = Append(@, newNotif)] + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "mention_user", + targetId |-> mid, + timestamp |-> Len(@) + ])] + /\ UNCHANGED <> + +\* User resolves a comment +ResolveComment(user, cid) == + /\ userSessions[user] = "active" + /\ \E c \in comments : + /\ c.id = cid + /\ CanAccessDocument(user, c.documentId) + /\ ~c.resolved + /\ comments' = (comments \ {c}) \cup {[c EXCEPT !.resolved = TRUE]} + /\ activityFeed' = [activityFeed EXCEPT + ![userTenants[user]] = Append(@, [ + userId |-> user, + tenantId |-> userTenants[user], + action |-> "resolve_comment", + targetId |-> cid, + timestamp |-> Len(@) + ])] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Notifications *) + +\* User reads a notification +ReadNotification(user, notifIndex) == + /\ userSessions[user] = "active" + /\ notifIndex \in 1..Len(notifications[user]) + /\ ~notifications[user][notifIndex].read + /\ LET + notif == notifications[user][notifIndex] + updatedNotif == [notif EXCEPT !.read = TRUE] + IN + /\ notifications' = [notifications EXCEPT + ![user] = [i \in 1..Len(@) |-> + IF i = notifIndex THEN updatedNotif ELSE @[i]]] + /\ UNCHANGED <> + +\* Clear all read notifications +ClearReadNotifications(user) == + /\ userSessions[user] = "active" + /\ LET + unread == SelectSeq(notifications[user], LAMBDA n : ~n.read) + IN + /\ notifications' = [notifications EXCEPT ![user] = unread] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Next State Relation *) + +Next == + \/ \E u \in Users: UserConnect(u) + \/ \E u \in Users: UserGoIdle(u) + \/ \E u \in Users: UserDisconnect(u) + \/ \E u \in Users, d \in Documents: StartEditing(u, d) + \/ \E u \in Users, d \in Documents: StopEditing(u, d) + \/ \E u \in Users, d \in Documents, op \in Operation: + ApplyOperation(u, d, op) + \/ \E u \in Users, d \in Documents: CreateVersion(u, d) + \/ \E u \in Users, d \in Documents, cid \in Nat, + content \in STRING, pos \in Nat: + AddComment(u, d, cid, content, pos) + \/ \E u \in Users, mu \in Users, cid \in Nat, mid \in Nat: + MentionUser(u, mu, cid, mid) + \/ \E u \in Users, cid \in Nat: ResolveComment(u, cid) + \/ \E u \in Users, idx \in Nat: ReadNotification(u, idx) + \/ \E u \in Users: ClearReadNotifications(u) + +----------------------------------------------------------------------------- +(* Safety Properties *) + +\* Document access is tenant-isolated +DocumentTenantIsolation == + \A u \in Users, d \in Documents: + u \in documentEditors[d] => userTenants[u] = documentTenants[d] + +\* Concurrent editors don't exceed limit +ConcurrentEditorLimit == + \A d \in Documents: + Cardinality(documentEditors[d]) <= MaxConcurrentEditors + +\* Comments belong to document's tenant +CommentTenantConsistency == + \A c \in comments: + c.tenantId = documentTenants[c.documentId] + +\* Mentions are within same tenant +MentionTenantIsolation == + \A m \in mentions: + userTenants[m.mentionedUser] = m.tenantId + +\* Notifications don't exceed limit +NotificationLimit == + \A u \in Users: + CountPendingNotifications(u) <= MaxNotifications + +\* Only active users can edit +ActiveEditorsOnly == + \A u \in Users, d \in Documents: + u \in documentEditors[d] => + userSessions[u] \in {"active", "idle"} + +\* Disconnected users are not editing +DisconnectedNotEditing == + \A u \in Users: + userSessions[u] = "disconnected" => + ~\E d \in Documents : u \in documentEditors[d] + +\* Operations in document are from editors +OperationAuthorship == + \A d \in Documents, i \in 1..Len(documentContent[d]): + LET op == documentContent[d][i] + IN CanAccessDocument(op.user, d) + +\* Version snapshots preserve content +VersionConsistency == + \A d \in Documents, v \in 1..Len(versionHistory[d]): + versionHistory[d][v].documentId = d + +----------------------------------------------------------------------------- +(* Liveness Properties *) + +\* Pending notifications eventually get read or cleared +EventualNotificationHandling == + \A u \in Users: + (CountPendingNotifications(u) > 0) ~> + (CountPendingNotifications(u) = 0 \/ userSessions[u] = "disconnected") + +\* Comments with mentions eventually get read +EventualMentionRead == + \A m \in mentions: + ~m.read ~> (m.read \/ userSessions[m.mentionedUser] = "disconnected") + +\* Active editors eventually stop editing or disconnect +EventualStopEditing == + \A u \in Users, d \in Documents: + u \in documentEditors[d] ~> + (u \notin documentEditors[d] \/ userSessions[u] = "disconnected") + +----------------------------------------------------------------------------- +(* System Specification *) + +Spec == + /\ Init + /\ [][Next]_vars + /\ \A u \in Users, d \in Documents: WF_vars(StopEditing(u, d)) + +----------------------------------------------------------------------------- +(* Invariants *) + +Invariants == + /\ TypeOK + /\ DocumentTenantIsolation + /\ ConcurrentEditorLimit + /\ CommentTenantConsistency + /\ MentionTenantIsolation + /\ NotificationLimit + /\ ActiveEditorsOnly + /\ DisconnectedNotEditing + /\ OperationAuthorship + /\ VersionConsistency + +============================================================================= diff --git a/spec/integrations.cfg b/spec/integrations.cfg new file mode 100644 index 000000000..97ac2320f --- /dev/null +++ b/spec/integrations.cfg @@ -0,0 +1,36 @@ +SPECIFICATION Spec + +CONSTANTS + Users = {u1, u2, u3} + Tenants = {t1, t2} + Webhooks = {wh1, wh2, wh3} + OAuthApps = {app1, app2} + APIKeys = {key1, key2, key3} + EventTypes = {event1, event2, event3} + MaxWebhooksPerTenant = 2 + MaxKeysPerUser = 2 + RateLimitPerHour = 100 + +INVARIANTS + TypeOK + AdminOnlyIntegrationManagement + WebhookTenantLimit + APIKeyUserLimit + RateLimitEnforcement + WebhookTenantIsolation + OAuthAppTenantIsolation + APIKeyTenantIsolation + TokenTenantConsistency + ActiveDeliveriesQueued + +PROPERTIES + EventualDeliveryCompletion + EventualRetryOrFail + EventualExpiration + +\* Constraint to limit state space for model checking +CONSTRAINT + /\ Len(integrationAuditLog) <= 15 + /\ Len(webhookQueue) <= 5 + /\ Cardinality(webhookDeliveries) <= 6 + /\ Cardinality(oauthTokens) <= 4 diff --git a/spec/integrations.tla b/spec/integrations.tla new file mode 100644 index 000000000..bfc1c075a --- /dev/null +++ b/spec/integrations.tla @@ -0,0 +1,644 @@ +---------------------------- MODULE integrations ---------------------------- +(*************************************************************************** + * Integration Ecosystem Specification for MetaBuilder * + * * + * This specification models the integration ecosystem including: * + * - Webhook management and delivery * + * - OAuth application framework * + * - API key management * + * - Third-party app directory * + * - Event subscriptions and filtering * + * - Rate limiting and quota management * + ***************************************************************************) + +EXTENDS Naturals, Sequences, FiniteSets, TLC + +CONSTANTS + Users, \* Set of all users + Tenants, \* Set of tenants + Webhooks, \* Set of webhook IDs + OAuthApps, \* Set of OAuth application IDs + APIKeys, \* Set of API key IDs + EventTypes, \* Set of event types to subscribe to + MaxWebhooksPerTenant, \* Maximum webhooks per tenant + MaxKeysPerUser, \* Maximum API keys per user + RateLimitPerHour \* API calls allowed per hour + +VARIABLES + userLevels, \* User -> Permission Level + userTenants, \* User -> Tenant + webhookConfigs, \* Set of webhook configurations + webhookQueue, \* Sequence of pending webhook deliveries + webhookDeliveries, \* Set of delivery records + oauthApps, \* Set of OAuth application records + oauthTokens, \* Set of OAuth token records + apiKeys, \* Set of API key records + apiCallCounts, \* (User/App, Hour) -> Call count + eventSubscriptions, \* Set of event subscriptions + integrationAuditLog \* Sequence of integration events + +vars == <> + +----------------------------------------------------------------------------- +(* Type Definitions *) + +PermissionLevel == 1..6 + +WebhookStatus == {"active", "paused", "disabled"} +DeliveryStatus == {"pending", "success", "failed", "retrying"} +OAuthAppStatus == {"active", "suspended", "revoked"} +APIKeyStatus == {"active", "expired", "revoked"} + +WebhookConfig == [ + id: Webhooks, + tenantId: Tenants, + ownerId: Users, + url: STRING, + status: WebhookStatus, + events: SUBSET EventTypes, + secret: STRING, + createdAt: Nat +] + +WebhookDelivery == [ + id: Nat, + webhookId: Webhooks, + eventType: EventTypes, + payload: STRING, + status: DeliveryStatus, + attempts: Nat, + timestamp: Nat +] + +OAuthApp == [ + id: OAuthApps, + tenantId: Tenants, + ownerId: Users, + name: STRING, + status: OAuthAppStatus, + scopes: SUBSET STRING, + redirectUri: STRING, + clientId: STRING, + createdAt: Nat +] + +OAuthToken == [ + id: Nat, + appId: OAuthApps, + userId: Users, + tenantId: Tenants, + accessToken: STRING, + scopes: SUBSET STRING, + expiresAt: Nat, + createdAt: Nat +] + +APIKey == [ + id: APIKeys, + userId: Users, + tenantId: Tenants, + name: STRING, + key: STRING, + status: APIKeyStatus, + scopes: SUBSET STRING, + expiresAt: Nat, + createdAt: Nat +] + +EventSubscription == [ + id: Nat, + subscriberId: Users \cup OAuthApps, + tenantId: Tenants, + eventType: EventTypes, + filters: STRING, + active: BOOLEAN +] + +TypeOK == + /\ userLevels \in [Users -> PermissionLevel] + /\ userTenants \in [Users -> Tenants] + /\ webhookConfigs \subseteq WebhookConfig + /\ webhookQueue \in Seq(WebhookDelivery) + /\ webhookDeliveries \subseteq WebhookDelivery + /\ oauthApps \subseteq OAuthApp + /\ oauthTokens \subseteq OAuthToken + /\ apiKeys \subseteq APIKey + /\ apiCallCounts \in [(Users \cup OAuthApps) \X Nat -> Nat] + /\ eventSubscriptions \subseteq EventSubscription + /\ integrationAuditLog \in Seq([ + user: Users \cup {"system"}, + action: STRING, + targetId: Nat \cup Webhooks \cup OAuthApps \cup APIKeys, + tenant: Tenants, + timestamp: Nat + ]) + +----------------------------------------------------------------------------- +(* Permission Checks *) + +\* Admin level (4+) required for integration management +CanManageIntegrations(user, tenant) == + /\ userLevels[user] >= 4 + /\ userTenants[user] = tenant + +\* User level (2+) required for API keys +CanManageAPIKeys(user) == + userLevels[user] >= 2 + +----------------------------------------------------------------------------- +(* Helper Functions *) + +\* Count webhooks for a tenant +CountWebhooksForTenant(tenant) == + Cardinality({w \in webhookConfigs : w.tenantId = tenant}) + +\* Count API keys for a user +CountKeysForUser(user) == + Cardinality({k \in apiKeys : k.userId = user /\ k.status = "active"}) + +\* Get API call count for current hour +GetCallCount(identity, hour) == + IF <> \in DOMAIN apiCallCounts + THEN apiCallCounts[<>] + ELSE 0 + +\* Check if rate limit exceeded +RateLimitExceeded(identity, hour) == + GetCallCount(identity, hour) >= RateLimitPerHour + +----------------------------------------------------------------------------- +(* Initial State *) + +Init == + /\ userLevels \in [Users -> PermissionLevel] + /\ userTenants \in [Users -> Tenants] + /\ webhookConfigs = {} + /\ webhookQueue = <<>> + /\ webhookDeliveries = {} + /\ oauthApps = {} + /\ oauthTokens = {} + /\ apiKeys = {} + /\ apiCallCounts = [x \in (Users \cup OAuthApps) \X Nat |-> 0] + /\ eventSubscriptions = {} + /\ integrationAuditLog = <<>> + +----------------------------------------------------------------------------- +(* Webhook Operations *) + +\* Admin creates a webhook +CreateWebhook(user, wid, url, events, secret) == + /\ CanManageIntegrations(user, userTenants[user]) + /\ wid \in Webhooks + /\ wid \notin {w.id : w \in webhookConfigs} + /\ CountWebhooksForTenant(userTenants[user]) < MaxWebhooksPerTenant + /\ events \subseteq EventTypes + /\ events /= {} + /\ LET newWebhook == [ + id |-> wid, + tenantId |-> userTenants[user], + ownerId |-> user, + url |-> url, + status |-> "active", + events |-> events, + secret |-> secret, + createdAt |-> Len(integrationAuditLog) + ] IN + /\ webhookConfigs' = webhookConfigs \cup {newWebhook} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "create_webhook", + targetId |-> wid, + tenant |-> userTenants[user], + timestamp |-> Len(integrationAuditLog) + ]) + /\ UNCHANGED <> + +\* Admin updates webhook status +UpdateWebhookStatus(user, wid, newStatus) == + /\ \E w \in webhookConfigs : + /\ w.id = wid + /\ CanManageIntegrations(user, w.tenantId) + /\ newStatus \in WebhookStatus + /\ webhookConfigs' = (webhookConfigs \ {w}) \cup + {[w EXCEPT !.status = newStatus]} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "update_webhook_status", + targetId |-> wid, + tenant |-> w.tenantId, + timestamp |-> Len(integrationAuditLog) + ]) + /\ UNCHANGED <> + +\* System enqueues webhook delivery +EnqueueWebhook(wid, eventType, payload, deliveryId) == + /\ \E w \in webhookConfigs : + /\ w.id = wid + /\ w.status = "active" + /\ eventType \in w.events + /\ deliveryId \notin {d.id : d \in webhookDeliveries} + /\ LET delivery == [ + id |-> deliveryId, + webhookId |-> wid, + eventType |-> eventType, + payload |-> payload, + status |-> "pending", + attempts |-> 0, + timestamp |-> Len(integrationAuditLog) + ] IN + /\ webhookQueue' = Append(webhookQueue, delivery) + /\ webhookDeliveries' = webhookDeliveries \cup {delivery} + /\ UNCHANGED <> + +\* System attempts webhook delivery +AttemptDelivery(deliveryId) == + /\ Len(webhookQueue) > 0 + /\ \E d \in webhookDeliveries : + /\ d.id = deliveryId + /\ d.status \in {"pending", "retrying"} + /\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup + {[d EXCEPT + !.status = "success", + !.attempts = @ + 1 + ]} + /\ webhookQueue' = Tail(webhookQueue) + /\ UNCHANGED <> + +\* Webhook delivery fails +FailDelivery(deliveryId) == + /\ \E d \in webhookDeliveries : + /\ d.id = deliveryId + /\ d.status \in {"pending", "retrying"} + /\ d.attempts < 3 + /\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup + {[d EXCEPT + !.status = "retrying", + !.attempts = @ + 1 + ]} + /\ UNCHANGED <> + +\* Webhook delivery permanently fails +PermanentFailDelivery(deliveryId) == + /\ \E d \in webhookDeliveries : + /\ d.id = deliveryId + /\ d.status = "retrying" + /\ d.attempts >= 3 + /\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup + {[d EXCEPT !.status = "failed"]} + /\ webhookQueue' = SelectSeq(webhookQueue, LAMBDA x : x.id /= deliveryId) + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* OAuth Application Management *) + +\* Admin creates OAuth app +CreateOAuthApp(user, appId, name, scopes, redirectUri) == + /\ CanManageIntegrations(user, userTenants[user]) + /\ appId \in OAuthApps + /\ appId \notin {a.id : a \in oauthApps} + /\ LET newApp == [ + id |-> appId, + tenantId |-> userTenants[user], + ownerId |-> user, + name |-> name, + status |-> "active", + scopes |-> scopes, + redirectUri |-> redirectUri, + clientId |-> "client_" \o appId, + createdAt |-> Len(integrationAuditLog) + ] IN + /\ oauthApps' = oauthApps \cup {newApp} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "create_oauth_app", + targetId |-> appId, + tenant |-> userTenants[user], + timestamp |-> Len(integrationAuditLog) + ]) + /\ UNCHANGED <> + +\* User authorizes OAuth app +AuthorizeOAuthApp(user, appId, tokenId, scopes) == + /\ \E app \in oauthApps : + /\ app.id = appId + /\ userTenants[user] = app.tenantId + /\ app.status = "active" + /\ scopes \subseteq app.scopes + /\ tokenId \notin {t.id : t \in oauthTokens} + /\ LET + currentTime == Len(integrationAuditLog) + newToken == [ + id |-> tokenId, + appId |-> appId, + userId |-> user, + tenantId |-> userTenants[user], + accessToken |-> "token_" \o tokenId, + scopes |-> scopes, + expiresAt |-> currentTime + 3600, + createdAt |-> currentTime + ] + IN + /\ oauthTokens' = oauthTokens \cup {newToken} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "authorize_oauth_app", + targetId |-> appId, + tenant |-> userTenants[user], + timestamp |-> currentTime + ]) + /\ UNCHANGED <> + +\* Admin revokes OAuth app +RevokeOAuthApp(user, appId) == + /\ \E app \in oauthApps : + /\ app.id = appId + /\ CanManageIntegrations(user, app.tenantId) + /\ app.status /= "revoked" + /\ oauthApps' = (oauthApps \ {app}) \cup + {[app EXCEPT !.status = "revoked"]} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "revoke_oauth_app", + targetId |-> appId, + tenant |-> app.tenantId, + timestamp |-> Len(integrationAuditLog) + ]) + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* API Key Management *) + +\* User creates API key +CreateAPIKey(user, keyId, name, scopes, expiresAt) == + /\ CanManageAPIKeys(user) + /\ keyId \in APIKeys + /\ keyId \notin {k.id : k \in apiKeys} + /\ CountKeysForUser(user) < MaxKeysPerUser + /\ LET newKey == [ + id |-> keyId, + userId |-> user, + tenantId |-> userTenants[user], + name |-> name, + key |-> "key_" \o keyId, + status |-> "active", + scopes |-> scopes, + expiresAt |-> expiresAt, + createdAt |-> Len(integrationAuditLog) + ] IN + /\ apiKeys' = apiKeys \cup {newKey} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "create_api_key", + targetId |-> keyId, + tenant |-> userTenants[user], + timestamp |-> Len(integrationAuditLog) + ]) + /\ UNCHANGED <> + +\* User revokes API key +RevokeAPIKey(user, keyId) == + /\ \E key \in apiKeys : + /\ key.id = keyId + /\ key.userId = user + /\ key.status = "active" + /\ apiKeys' = (apiKeys \ {key}) \cup + {[key EXCEPT !.status = "revoked"]} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "revoke_api_key", + targetId |-> keyId, + tenant |-> userTenants[user], + timestamp |-> Len(integrationAuditLog) + ]) + /\ UNCHANGED <> + +\* System expires old API keys +ExpireAPIKey(keyId) == + /\ \E key \in apiKeys : + /\ key.id = keyId + /\ key.status = "active" + /\ Len(integrationAuditLog) >= key.expiresAt + /\ apiKeys' = (apiKeys \ {key}) \cup + {[key EXCEPT !.status = "expired"]} + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Rate Limiting *) + +\* Record API call +RecordAPICall(identity, hour) == + /\ ~RateLimitExceeded(identity, hour) + /\ apiCallCounts' = [apiCallCounts EXCEPT + ![<>] = @ + 1] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Event Subscriptions *) + +\* Create event subscription +SubscribeToEvent(user, subId, eventType, filters) == + /\ CanManageIntegrations(user, userTenants[user]) + /\ subId \notin {s.id : s \in eventSubscriptions} + /\ eventType \in EventTypes + /\ LET newSub == [ + id |-> subId, + subscriberId |-> user, + tenantId |-> userTenants[user], + eventType |-> eventType, + filters |-> filters, + active |-> TRUE + ] IN + /\ eventSubscriptions' = eventSubscriptions \cup {newSub} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "subscribe_event", + targetId |-> subId, + tenant |-> userTenants[user], + timestamp |-> Len(integrationAuditLog) + ]) + /\ UNCHANGED <> + +\* Unsubscribe from event +UnsubscribeFromEvent(user, subId) == + /\ \E sub \in eventSubscriptions : + /\ sub.id = subId + /\ sub.subscriberId = user + /\ CanManageIntegrations(user, sub.tenantId) + /\ eventSubscriptions' = (eventSubscriptions \ {sub}) \cup + {[sub EXCEPT !.active = FALSE]} + /\ integrationAuditLog' = Append(integrationAuditLog, [ + user |-> user, + action |-> "unsubscribe_event", + targetId |-> subId, + tenant |-> sub.tenantId, + timestamp |-> Len(integrationAuditLog) + ]) + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Next State Relation *) + +Next == + \/ \E u \in Users, wid \in Webhooks, url \in STRING, + events \in SUBSET EventTypes, secret \in STRING: + CreateWebhook(u, wid, url, events, secret) + \/ \E u \in Users, wid \in Webhooks, status \in WebhookStatus: + UpdateWebhookStatus(u, wid, status) + \/ \E wid \in Webhooks, et \in EventTypes, payload \in STRING, did \in Nat: + EnqueueWebhook(wid, et, payload, did) + \/ \E did \in Nat: AttemptDelivery(did) + \/ \E did \in Nat: FailDelivery(did) + \/ \E did \in Nat: PermanentFailDelivery(did) + \/ \E u \in Users, aid \in OAuthApps, name \in STRING, + scopes \in SUBSET STRING, uri \in STRING: + CreateOAuthApp(u, aid, name, scopes, uri) + \/ \E u \in Users, aid \in OAuthApps, tid \in Nat, scopes \in SUBSET STRING: + AuthorizeOAuthApp(u, aid, tid, scopes) + \/ \E u \in Users, aid \in OAuthApps: RevokeOAuthApp(u, aid) + \/ \E u \in Users, kid \in APIKeys, name \in STRING, + scopes \in SUBSET STRING, exp \in Nat: + CreateAPIKey(u, kid, name, scopes, exp) + \/ \E u \in Users, kid \in APIKeys: RevokeAPIKey(u, kid) + \/ \E kid \in APIKeys: ExpireAPIKey(kid) + \/ \E identity \in (Users \cup OAuthApps), hour \in Nat: + RecordAPICall(identity, hour) + \/ \E u \in Users, sid \in Nat, et \in EventTypes, f \in STRING: + SubscribeToEvent(u, sid, et, f) + \/ \E u \in Users, sid \in Nat: UnsubscribeFromEvent(u, sid) + +----------------------------------------------------------------------------- +(* Safety Properties *) + +\* Admin-only integration management +AdminOnlyIntegrationManagement == + \A event \in 1..Len(integrationAuditLog): + LET action == integrationAuditLog[event].action IN + action \in {"create_webhook", "update_webhook_status", + "create_oauth_app", "revoke_oauth_app", + "subscribe_event", "unsubscribe_event"} => + userLevels[integrationAuditLog[event].user] >= 4 + +\* Webhooks don't exceed tenant limit +WebhookTenantLimit == + \A t \in Tenants: + CountWebhooksForTenant(t) <= MaxWebhooksPerTenant + +\* API keys don't exceed user limit +APIKeyUserLimit == + \A u \in Users: + CountKeysForUser(u) <= MaxKeysPerUser + +\* Rate limits are enforced +RateLimitEnforcement == + \A identity \in (Users \cup OAuthApps), hour \in Nat: + GetCallCount(identity, hour) <= RateLimitPerHour + +\* Tenant isolation for webhooks +WebhookTenantIsolation == + \A w \in webhookConfigs: + userTenants[w.ownerId] = w.tenantId + +\* Tenant isolation for OAuth apps +OAuthAppTenantIsolation == + \A app \in oauthApps: + userTenants[app.ownerId] = app.tenantId + +\* Tenant isolation for API keys +APIKeyTenantIsolation == + \A key \in apiKeys: + userTenants[key.userId] = key.tenantId + +\* OAuth tokens match app tenants +TokenTenantConsistency == + \A token \in oauthTokens: + \E app \in oauthApps: + app.id = token.appId /\ app.tenantId = token.tenantId + +\* Active deliveries are in queue +ActiveDeliveriesQueued == + \A d \in webhookDeliveries: + d.status = "pending" => + \E i \in 1..Len(webhookQueue) : webhookQueue[i].id = d.id + +----------------------------------------------------------------------------- +(* Liveness Properties *) + +\* Webhook deliveries eventually complete or fail +EventualDeliveryCompletion == + \A did \in Nat: + \E d \in webhookDeliveries : + d.id = did /\ d.status = "pending" ~> + d.status \in {"success", "failed"} + +\* Failed deliveries eventually retry or permanently fail +EventualRetryOrFail == + \A did \in Nat: + \E d \in webhookDeliveries : + d.id = did /\ d.status = "retrying" ~> + d.status \in {"success", "failed"} + +\* Expired keys eventually get marked as expired +EventualExpiration == + \A kid \in APIKeys: + \E key \in apiKeys : + key.id = kid /\ key.status = "active" /\ + Len(integrationAuditLog) >= key.expiresAt ~> + key.status = "expired" + +----------------------------------------------------------------------------- +(* System Specification *) + +Spec == + /\ Init + /\ [][Next]_vars + /\ \A did \in Nat: WF_vars(AttemptDelivery(did)) + /\ \A kid \in APIKeys: WF_vars(ExpireAPIKey(kid)) + +----------------------------------------------------------------------------- +(* Invariants *) + +Invariants == + /\ TypeOK + /\ AdminOnlyIntegrationManagement + /\ WebhookTenantLimit + /\ APIKeyUserLimit + /\ RateLimitEnforcement + /\ WebhookTenantIsolation + /\ OAuthAppTenantIsolation + /\ APIKeyTenantIsolation + /\ TokenTenantConsistency + /\ ActiveDeliveriesQueued + +============================================================================= diff --git a/spec/workflow_system.cfg b/spec/workflow_system.cfg new file mode 100644 index 000000000..ab6827a1b --- /dev/null +++ b/spec/workflow_system.cfg @@ -0,0 +1,31 @@ +SPECIFICATION Spec + +CONSTANTS + Users = {u1, u2, u3} + Tenants = {t1, t2} + WorkflowTemplates = {wf1, wf2, wf3} + WorkflowSteps = {step1, step2, step3} + MaxRetries = 3 + MaxConcurrentRuns = 2 + +INVARIANTS + TypeOK + GodOnlyTemplateCreation + AdminOnlyExecution + TenantIsolation + ConcurrencyLimit + RetryLimit + NoOverlap + DependencyEnforcement + AuditCompleteness + +PROPERTIES + EventualStepExecution + EventualCompletion + EventualScheduleTrigger + +\* Constraint to limit state space for model checking +CONSTRAINT + /\ Len(workflowAuditLog) <= 15 + /\ Cardinality(instances) <= 5 + /\ Cardinality(runningWorkflows) <= 3 diff --git a/spec/workflow_system.tla b/spec/workflow_system.tla new file mode 100644 index 000000000..aa28e0441 --- /dev/null +++ b/spec/workflow_system.tla @@ -0,0 +1,595 @@ +---------------------------- MODULE workflow_system ---------------------------- +(*************************************************************************** + * Workflow System Specification for MetaBuilder * + * * + * This specification models workflow execution, scheduling, and state * + * management for MetaBuilder's advanced workflow features. * + * * + * Features modeled: * + * - Workflow definition and validation * + * - Scheduled and manual workflow execution * + * - Step dependencies and parallel execution * + * - Error handling and retry logic * + * - Workflow templates and instances * + * - God-level (Level 5+) permission requirements * + ***************************************************************************) + +EXTENDS Naturals, Sequences, FiniteSets, TLC + +CONSTANTS + Users, \* Set of all users + Tenants, \* Set of tenants + WorkflowTemplates, \* Set of workflow templates + WorkflowSteps, \* Set of possible workflow steps + MaxRetries, \* Maximum retry attempts for failed steps + MaxConcurrentRuns \* Maximum concurrent workflow executions per tenant + +VARIABLES + userLevels, \* User -> Permission Level + userTenants, \* User -> Tenant + templates, \* WorkflowTemplate -> Template Definition + instances, \* WorkflowInstance -> Instance State + scheduledRuns, \* Set of scheduled workflow runs + runningWorkflows, \* Set of currently executing workflow instances + completedWorkflows, \* Set of completed workflow instances + workflowAuditLog \* Sequence of workflow events + +vars == <> + +----------------------------------------------------------------------------- +(* Type Definitions *) + +PermissionLevel == 1..6 + +WorkflowStatus == {"draft", "active", "paused", "archived"} +StepStatus == {"pending", "running", "success", "failed", "skipped", "retrying"} +InstanceStatus == {"queued", "running", "completed", "failed", "cancelled"} + +TemplateRecord == [ + id: WorkflowTemplates, + name: STRING, + tenantId: Tenants, + status: WorkflowStatus, + steps: Seq(WorkflowSteps), + dependencies: [WorkflowSteps -> SUBSET WorkflowSteps], \* Step dependencies + trigger: {"manual", "scheduled", "event"} +] + +InstanceRecord == [ + id: Nat, + templateId: WorkflowTemplates, + tenantId: Tenants, + status: InstanceStatus, + startedBy: Users, + startTime: Nat, + stepStates: [WorkflowSteps -> StepStatus], + retryCount: [WorkflowSteps -> Nat], + result: STRING +] + +TypeOK == + /\ userLevels \in [Users -> PermissionLevel] + /\ userTenants \in [Users -> Tenants] + /\ templates \subseteq TemplateRecord + /\ instances \subseteq InstanceRecord + /\ scheduledRuns \subseteq (WorkflowTemplates \X Tenants \X Nat) \* (template, tenant, timestamp) + /\ runningWorkflows \subseteq Nat \* Instance IDs + /\ completedWorkflows \subseteq Nat + /\ workflowAuditLog \in Seq([ + user: Users \cup {"system"}, + action: STRING, + templateId: WorkflowTemplates \cup {0}, + instanceId: Nat, + tenant: Tenants, + timestamp: Nat + ]) + +----------------------------------------------------------------------------- +(* Permission Checks *) + +\* God level (5+) required for workflow authoring +CanAuthorWorkflow(user, tenant) == + /\ userLevels[user] >= 5 + /\ userTenants[user] = tenant + +\* Admin level (4+) required for workflow execution +CanExecuteWorkflow(user, tenant) == + /\ userLevels[user] >= 4 + /\ userTenants[user] = tenant + +----------------------------------------------------------------------------- +(* Helper Functions *) + +\* Get template by ID +GetTemplate(tid) == + CHOOSE t \in templates : t.id = tid + +\* Get instance by ID +GetInstance(iid) == + CHOOSE i \in instances : i.id = iid + +\* Check if all dependencies of a step are satisfied +StepDependenciesSatisfied(instance, step) == + LET + template == GetTemplate(instance.templateId) + deps == template.dependencies[step] + IN + \A dep \in deps : + instance.stepStates[dep] \in {"success", "skipped"} + +\* Count running workflows for a tenant +CountRunningForTenant(tenant) == + Cardinality({i \in runningWorkflows : GetInstance(i).tenantId = tenant}) + +----------------------------------------------------------------------------- +(* Initial State *) + +Init == + /\ userLevels \in [Users -> PermissionLevel] + /\ userTenants \in [Users -> Tenants] + /\ templates = {} + /\ instances = {} + /\ scheduledRuns = {} + /\ runningWorkflows = {} + /\ completedWorkflows = {} + /\ workflowAuditLog = <<>> + +----------------------------------------------------------------------------- +(* Workflow Template Operations *) + +\* God user creates a new workflow template +CreateTemplate(user, tid, tenant, steps, deps, trigger) == + /\ CanAuthorWorkflow(user, tenant) + /\ tid \in WorkflowTemplates + /\ tid \notin {t.id : t \in templates} + /\ steps \in Seq(WorkflowSteps) + /\ Len(steps) > 0 + /\ trigger \in {"manual", "scheduled", "event"} + /\ LET newTemplate == [ + id |-> tid, + name |-> "WorkflowTemplate", + tenantId |-> tenant, + status |-> "draft", + steps |-> steps, + dependencies |-> deps, + trigger |-> trigger + ] IN + /\ templates' = templates \cup {newTemplate} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> user, + action |-> "create_template", + templateId |-> tid, + instanceId |-> 0, + tenant |-> tenant, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* God user activates a template +ActivateTemplate(user, tid) == + /\ \E t \in templates : + /\ t.id = tid + /\ CanAuthorWorkflow(user, t.tenantId) + /\ t.status = "draft" + /\ templates' = (templates \ {t}) \cup {[t EXCEPT !.status = "active"]} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> user, + action |-> "activate_template", + templateId |-> tid, + instanceId |-> 0, + tenant |-> t.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* God user archives a template +ArchiveTemplate(user, tid) == + /\ \E t \in templates : + /\ t.id = tid + /\ CanAuthorWorkflow(user, t.tenantId) + /\ t.status \in {"active", "paused"} + /\ templates' = (templates \ {t}) \cup {[t EXCEPT !.status = "archived"]} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> user, + action |-> "archive_template", + templateId |-> tid, + instanceId |-> 0, + tenant |-> t.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Workflow Execution *) + +\* Admin user manually starts a workflow +StartWorkflow(user, tid, iid) == + /\ \E t \in templates : + /\ t.id = tid + /\ CanExecuteWorkflow(user, t.tenantId) + /\ t.status = "active" + /\ CountRunningForTenant(t.tenantId) < MaxConcurrentRuns + /\ iid \notin {i.id : i \in instances} + /\ LET + initialStepStates == [s \in WorkflowSteps |-> + IF s \in {t.steps[i] : i \in 1..Len(t.steps)} + THEN "pending" + ELSE "skipped"] + initialRetryCount == [s \in WorkflowSteps |-> 0] + newInstance == [ + id |-> iid, + templateId |-> tid, + tenantId |-> t.tenantId, + status |-> "running", + startedBy |-> user, + startTime |-> Len(workflowAuditLog), + stepStates |-> initialStepStates, + retryCount |-> initialRetryCount, + result |-> "in_progress" + ] + IN + /\ instances' = instances \cup {newInstance} + /\ runningWorkflows' = runningWorkflows \cup {iid} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> user, + action |-> "start_workflow", + templateId |-> tid, + instanceId |-> iid, + tenant |-> t.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* System executes a workflow step +ExecuteStep(iid, step) == + /\ iid \in runningWorkflows + /\ \E instance \in instances : + /\ instance.id = iid + /\ instance.status = "running" + /\ instance.stepStates[step] = "pending" + /\ StepDependenciesSatisfied(instance, step) + /\ instances' = (instances \ {instance}) \cup + {[instance EXCEPT !.stepStates[step] = "running"]} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> "system", + action |-> "execute_step", + templateId |-> instance.templateId, + instanceId |-> iid, + tenant |-> instance.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* Step completes successfully +CompleteStep(iid, step) == + /\ iid \in runningWorkflows + /\ \E instance \in instances : + /\ instance.id = iid + /\ instance.stepStates[step] = "running" + /\ instances' = (instances \ {instance}) \cup + {[instance EXCEPT !.stepStates[step] = "success"]} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> "system", + action |-> "complete_step", + templateId |-> instance.templateId, + instanceId |-> iid, + tenant |-> instance.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* Step fails (may retry) +FailStep(iid, step) == + /\ iid \in runningWorkflows + /\ \E instance \in instances : + /\ instance.id = iid + /\ instance.stepStates[step] = "running" + /\ LET + newRetryCount == instance.retryCount[step] + 1 + shouldRetry == newRetryCount < MaxRetries + newStatus == IF shouldRetry THEN "retrying" ELSE "failed" + IN + /\ instances' = (instances \ {instance}) \cup + {[instance EXCEPT + !.stepStates[step] = newStatus, + !.retryCount[step] = newRetryCount + ]} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> "system", + action |-> "fail_step", + templateId |-> instance.templateId, + instanceId |-> iid, + tenant |-> instance.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* Retry a failed step +RetryStep(iid, step) == + /\ iid \in runningWorkflows + /\ \E instance \in instances : + /\ instance.id = iid + /\ instance.stepStates[step] = "retrying" + /\ instance.retryCount[step] < MaxRetries + /\ instances' = (instances \ {instance}) \cup + {[instance EXCEPT !.stepStates[step] = "pending"]} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> "system", + action |-> "retry_step", + templateId |-> instance.templateId, + instanceId |-> iid, + tenant |-> instance.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* Complete entire workflow +CompleteWorkflow(iid) == + /\ iid \in runningWorkflows + /\ \E instance \in instances : + /\ instance.id = iid + /\ instance.status = "running" + /\ LET + template == GetTemplate(instance.templateId) + allStepsComplete == \A step \in {template.steps[i] : i \in 1..Len(template.steps)} : + instance.stepStates[step] \in {"success", "skipped"} + IN + /\ allStepsComplete + /\ instances' = (instances \ {instance}) \cup + {[instance EXCEPT + !.status = "completed", + !.result = "success" + ]} + /\ runningWorkflows' = runningWorkflows \ {iid} + /\ completedWorkflows' = completedWorkflows \cup {iid} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> "system", + action |-> "complete_workflow", + templateId |-> instance.templateId, + instanceId |-> iid, + tenant |-> instance.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* Fail entire workflow +FailWorkflow(iid) == + /\ iid \in runningWorkflows + /\ \E instance \in instances : + /\ instance.id = iid + /\ instance.status = "running" + /\ LET + template == GetTemplate(instance.templateId) + hasFailedStep == \E step \in {template.steps[i] : i \in 1..Len(template.steps)} : + /\ instance.stepStates[step] = "failed" + /\ instance.retryCount[step] >= MaxRetries + IN + /\ hasFailedStep + /\ instances' = (instances \ {instance}) \cup + {[instance EXCEPT + !.status = "failed", + !.result = "failure" + ]} + /\ runningWorkflows' = runningWorkflows \ {iid} + /\ completedWorkflows' = completedWorkflows \cup {iid} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> "system", + action |-> "fail_workflow", + templateId |-> instance.templateId, + instanceId |-> iid, + tenant |-> instance.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* Admin user cancels a running workflow +CancelWorkflow(user, iid) == + /\ iid \in runningWorkflows + /\ \E instance \in instances : + /\ instance.id = iid + /\ CanExecuteWorkflow(user, instance.tenantId) + /\ instance.status = "running" + /\ instances' = (instances \ {instance}) \cup + {[instance EXCEPT + !.status = "cancelled", + !.result = "cancelled" + ]} + /\ runningWorkflows' = runningWorkflows \ {iid} + /\ completedWorkflows' = completedWorkflows \cup {iid} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> user, + action |-> "cancel_workflow", + templateId |-> instance.templateId, + instanceId |-> iid, + tenant |-> instance.tenantId, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Scheduling *) + +\* Schedule a workflow run +ScheduleWorkflow(user, tid, tenant, scheduledTime) == + /\ \E t \in templates : + /\ t.id = tid + /\ t.tenantId = tenant + /\ CanExecuteWorkflow(user, tenant) + /\ t.status = "active" + /\ t.trigger \in {"scheduled", "manual"} + /\ scheduledRuns' = scheduledRuns \cup {<>} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> user, + action |-> "schedule_workflow", + templateId |-> tid, + instanceId |-> 0, + tenant |-> tenant, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +\* System triggers a scheduled workflow +TriggerScheduled(tid, tenant, scheduledTime, iid) == + /\ <> \in scheduledRuns + /\ Len(workflowAuditLog) >= scheduledTime + /\ \E t \in templates : + /\ t.id = tid + /\ t.tenantId = tenant + /\ t.status = "active" + /\ CountRunningForTenant(tenant) < MaxConcurrentRuns + /\ iid \notin {i.id : i \in instances} + /\ LET + initialStepStates == [s \in WorkflowSteps |-> + IF s \in {t.steps[i] : i \in 1..Len(t.steps)} + THEN "pending" + ELSE "skipped"] + initialRetryCount == [s \in WorkflowSteps |-> 0] + newInstance == [ + id |-> iid, + templateId |-> tid, + tenantId |-> tenant, + status |-> "running", + startedBy |-> CHOOSE u \in Users : userTenants[u] = tenant /\ userLevels[u] >= 5, + startTime |-> Len(workflowAuditLog), + stepStates |-> initialStepStates, + retryCount |-> initialRetryCount, + result |-> "in_progress" + ] + IN + /\ instances' = instances \cup {newInstance} + /\ runningWorkflows' = runningWorkflows \cup {iid} + /\ scheduledRuns' = scheduledRuns \ {<>} + /\ workflowAuditLog' = Append(workflowAuditLog, [ + user |-> "system", + action |-> "trigger_scheduled", + templateId |-> tid, + instanceId |-> iid, + tenant |-> tenant, + timestamp |-> Len(workflowAuditLog) + ]) + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Next State Relation *) + +Next == + \/ \E u \in Users, tid \in WorkflowTemplates, t \in Tenants, + steps \in Seq(WorkflowSteps), + deps \in [WorkflowSteps -> SUBSET WorkflowSteps], + trigger \in {"manual", "scheduled", "event"}: + CreateTemplate(u, tid, t, steps, deps, trigger) + \/ \E u \in Users, tid \in WorkflowTemplates: ActivateTemplate(u, tid) + \/ \E u \in Users, tid \in WorkflowTemplates: ArchiveTemplate(u, tid) + \/ \E u \in Users, tid \in WorkflowTemplates, iid \in Nat: + StartWorkflow(u, tid, iid) + \/ \E iid \in Nat, step \in WorkflowSteps: ExecuteStep(iid, step) + \/ \E iid \in Nat, step \in WorkflowSteps: CompleteStep(iid, step) + \/ \E iid \in Nat, step \in WorkflowSteps: FailStep(iid, step) + \/ \E iid \in Nat, step \in WorkflowSteps: RetryStep(iid, step) + \/ \E iid \in Nat: CompleteWorkflow(iid) + \/ \E iid \in Nat: FailWorkflow(iid) + \/ \E u \in Users, iid \in Nat: CancelWorkflow(u, iid) + \/ \E u \in Users, tid \in WorkflowTemplates, t \in Tenants, time \in Nat: + ScheduleWorkflow(u, tid, t, time) + \/ \E tid \in WorkflowTemplates, t \in Tenants, time \in Nat, iid \in Nat: + TriggerScheduled(tid, t, time, iid) + +----------------------------------------------------------------------------- +(* Safety Properties *) + +\* Only God-level users can create templates +GodOnlyTemplateCreation == + \A event \in 1..Len(workflowAuditLog): + workflowAuditLog[event].action = "create_template" => + userLevels[workflowAuditLog[event].user] >= 5 + +\* Only Admin+ users can execute workflows +AdminOnlyExecution == + \A event \in 1..Len(workflowAuditLog): + workflowAuditLog[event].action \in {"start_workflow", "cancel_workflow"} => + userLevels[workflowAuditLog[event].user] >= 4 + +\* Workflow instances belong to exactly one tenant +TenantIsolation == + \A i1, i2 \in instances: + i1.id = i2.id => i1.tenantId = i2.tenantId + +\* Running workflows don't exceed concurrency limit +ConcurrencyLimit == + \A t \in Tenants: + CountRunningForTenant(t) <= MaxConcurrentRuns + +\* Failed steps don't exceed retry limit +RetryLimit == + \A i \in instances, s \in WorkflowSteps: + i.retryCount[s] <= MaxRetries + +\* Completed workflows are not in running set +NoOverlap == + runningWorkflows \cap completedWorkflows = {} + +\* Step dependencies are respected +DependencyEnforcement == + \A i \in instances, step \in WorkflowSteps: + i.stepStates[step] \in {"running", "success"} => + StepDependenciesSatisfied(i, step) + +\* All workflow events are audited +AuditCompleteness == + Len(workflowAuditLog) >= Cardinality(instances) + +----------------------------------------------------------------------------- +(* Liveness Properties *) + +\* Pending steps eventually execute (if dependencies are met) +EventualStepExecution == + \A i \in instances, step \in WorkflowSteps: + (i.stepStates[step] = "pending" /\ StepDependenciesSatisfied(i, step)) ~> + i.stepStates[step] \in {"running", "success", "failed"} + +\* Running workflows eventually complete or fail +EventualCompletion == + \A iid \in Nat: + iid \in runningWorkflows ~> iid \in completedWorkflows + +\* Scheduled workflows eventually trigger +EventualScheduleTrigger == + \A tid \in WorkflowTemplates, t \in Tenants, time \in Nat: + <> \in scheduledRuns ~> + (<> \notin scheduledRuns \/ CountRunningForTenant(t) >= MaxConcurrentRuns) + +----------------------------------------------------------------------------- +(* System Specification *) + +Spec == + /\ Init + /\ [][Next]_vars + /\ \A iid \in Nat: WF_vars(CompleteWorkflow(iid)) + /\ \A iid \in Nat: WF_vars(FailWorkflow(iid)) + /\ \A iid \in Nat, step \in WorkflowSteps: WF_vars(ExecuteStep(iid, step)) + +----------------------------------------------------------------------------- +(* Invariants *) + +Invariants == + /\ TypeOK + /\ GodOnlyTemplateCreation + /\ AdminOnlyExecution + /\ TenantIsolation + /\ ConcurrencyLimit + /\ RetryLimit + /\ NoOverlap + /\ DependencyEnforcement + /\ AuditCompleteness + +=============================================================================