mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-11-02 07:29:17 +00:00
28 lines
764 B
Plaintext
28 lines
764 B
Plaintext
-------------------- MODULE DiscordRoleGatingHarness_BadIgnoresRole --------------------
|
|
EXTENDS Naturals
|
|
|
|
(******************************************************************************
|
|
* Negative model:
|
|
* BUG: role requirement is ignored, authorizing the action for everyone.
|
|
******************************************************************************)
|
|
|
|
CONSTANTS
|
|
RequiresRole,
|
|
HasRequiredRole
|
|
|
|
ASSUME
|
|
/\ RequiresRole \in BOOLEAN
|
|
/\ HasRequiredRole \in BOOLEAN
|
|
|
|
\* BUG: ignores role gating
|
|
Authorized == TRUE
|
|
|
|
Inv_NoRoleNoAuth == (RequiresRole /\ ~HasRequiredRole) => ~Authorized
|
|
|
|
VARIABLE dummy
|
|
Init == dummy = 0
|
|
Next == dummy' = dummy
|
|
Spec == Init /\ [][Next]_<<dummy>>
|
|
|
|
=============================================================================
|