mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-10-30 18:46:45 +00:00
34 lines
982 B
Plaintext
34 lines
982 B
Plaintext
------------------------------ MODULE RoutingIsolationHarness_BadAlwaysMain ------------------------------
|
|
EXTENDS Naturals, Sequences, FiniteSets
|
|
|
|
(******************************************************************************
|
|
* BUG: DM session key always collapses to "main" regardless of dmScope.
|
|
******************************************************************************)
|
|
|
|
CONSTANTS
|
|
Peers,
|
|
DmScope,
|
|
IdentityLinks
|
|
|
|
ASSUME
|
|
/\ Peers /= {}
|
|
/\ DmScope \in {"main","per-peer"}
|
|
/\ IdentityLinks \subseteq (Peers \X Peers)
|
|
|
|
Linked(a,b) == <<a,b>> \in IdentityLinks \/ <<b,a>> \in IdentityLinks \/ a=b
|
|
|
|
\* BUG: always main
|
|
SessionKey(_p) == "main"
|
|
|
|
Inv_NoUnlinkedCollapse ==
|
|
DmScope = "per-peer" =>
|
|
\A p1 \in Peers: \A p2 \in Peers:
|
|
(~Linked(p1,p2)) => (SessionKey(p1) /= SessionKey(p2))
|
|
|
|
VARIABLE dummy
|
|
Init == dummy = 0
|
|
Next == dummy' = dummy
|
|
Spec == Init /\ [][Next]_<<dummy>>
|
|
|
|
=============================================================================
|