Add Vortex DSE specifications

README.md

@@ -108,6 +108,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [DAG-based Consensus](specifications/dag-consensus)                                                 | Giuliano Losa                                       |          |             |    ✔    |     ✔     |          |
 | [German Cache-Coherence Protocol](specifications/GermanProtocol)                                    | Markus Kuppe                                        |          |             |         |     ✔     |    ✔     |
 | [FLASH Cache-Coherence Protocol](specifications/FlashProtocol)                                      | Markus Kuppe                                        |          |             |         |     ✔     |    ✔     |
+| [Vortex DSE](specifications/VortexDSE)                                                             | Vasilis Nasopoulos                                 |          |      ✔      |         |     ✔     |          |
 
 
 ## Other Examples

specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg

@@ -0,0 +1,17 @@
+\* Safety model. The horizon is imposed inside MCTick; see the module
+\* header for why a state constraint does not work here.
+
+SPECIFICATION MCSpec
+
+CONSTANTS
+    Nodes   = {n1, n2}
+    MsgIDs  = {m1, m2}
+    MaxSlot = 2
+
+INVARIANT MCTypeInvariant
+INVARIANT NoFutureAdmission
+INVARIANT ExactlyOncePerNode
+INVARIANT NoPhantomProcess
+INVARIANT DecisionLocalityOnly
+
+

specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla

@@ -0,0 +1,73 @@
+---- MODULE MC_Vortex_DSE_CSlot ----
+(***************************************************************************)
+(* TLC harness for Vortex_DSE_CSlot.                                       *)
+(*                                                                          *)
+(* The specification has no slot horizon: Tick is unbounded and the        *)
+(* adversary may forge any slot in Nat. The horizon is a model-checking    *)
+(* concern and lives here.                                                  *)
+(*                                                                          *)
+(* It is imposed inside MCTick rather than as a state CONSTRAINT. A         *)
+(* constraint was tried first, as the review guidelines prefer, but TLC     *)
+(* evaluates invariants on the state that crosses the boundary before the   *)
+(* constraint discards it: with MaxSlot = 2 a Tick produces current_slot =  *)
+(* 3, and any invariant mentioning the horizon fails there. Bounding the    *)
+(* ticker instead keeps the reachable graph inside the horizon.             *)
+(*                                                                          *)
+(* It also avoids a second problem in the liveness model, where discarding  *)
+(* successor states can mask or invent violations of temporal properties.   *)
+(*                                                                          *)
+(* MCNext restricts the forged slot as well, because TLC cannot enumerate   *)
+(* Nat.                                                                     *)
+(***************************************************************************)
+EXTENDS Vortex_DSE_CSlot
+
+CONSTANT MaxSlot
+
+ASSUME MaxSlotAssumption == MaxSlot \in Nat
+
+Slots == 0..MaxSlot
+
+MCMsgRecord == [id: MsgIDs, cslot: Slots]
+
+\* The ticker stops at the horizon.
+MCTick ==
+    /\ current_slot < MaxSlot
+    /\ Tick
+
+MCNext ==
+    \/ \E id \in MsgIDs, k \in Slots : Send(id, k)
+    \/ \E n \in Nodes, m \in network : Process(n, m)
+    \/ \E n \in Nodes : Crash(n)
+    \/ \E n \in Nodes : Rejoin(n)
+        \/ MCTick
+
+MCSpec == Init /\ [][MCNext]_vars
+
+\* Type correctness within the horizon. TLC cannot evaluate the
+\* specification's own TypeInvariant, whose MsgRecord ranges over Nat.
+MCTypeInvariant ==
+    /\ current_slot \in Slots
+    /\ network      \subseteq MCMsgRecord
+    /\ processed    \in [Nodes -> SUBSET MsgIDs]
+    /\ persisted    \in [Nodes -> SUBSET MsgIDs]
+    /\ node_state   \in [Nodes -> {Up, Down}]
+
+-------------------------------------------------------------------------------
+(*                            LIVENESS HARNESS                              *)
+
+\* Strong fairness on Process is necessary, not decorative: with weak
+\* fairness the liveness model reports a temporal-property violation,
+\* because a crash intermittently disables Process.
+MCFairness ==
+    /\ WF_vars(MCTick)
+    /\ \A n \in Nodes : WF_vars(Rejoin(n))
+    /\ \A n \in Nodes : SF_vars(\E m \in network : Process(n, m))
+
+MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness
+
+\* Bounded counterpart of TickProgress, strengthened as suggested: once the
+\* ticker reaches the horizon MCTick is permanently disabled, so the slot
+\* counter stays there rather than merely visiting it.
+MCTickProgress == <>[](current_slot = MaxSlot)
+
+====

specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla

@@ -0,0 +1,51 @@
+---------------- MODULE MC_Vortex_DSE_CSlot_AE ----------------
+(***************************************************************************)
+(* Harness for Vortex_DSE_CSlot_AE, used by both TLC and Apalache.         *)
+(*                                                                          *)
+(* The specification has no slot horizon; NextCslot advances without bound  *)
+(* and DuplicateInject may forge any slot in Nat. The horizon is a          *)
+(* model-checking concern and is imposed here inside the actions, not as a  *)
+(* CONSTRAINT, so no successor state is discarded while temporal properties *)
+(* are checked.                                                             *)
+(*                                                                          *)
+(* Invariants are deliberately left separate rather than bundled into one   *)
+(* conjunction, so that a checker reports which one was violated.           *)
+(***************************************************************************)
+EXTENDS Vortex_DSE_CSlot_AE
+
+CONSTANT MaxSlot
+
+Slots == 0..MaxSlot
+
+MCNextCslot ==
+    /\ current_slot < MaxSlot
+    /\ NextCslot
+
+MCNext ==
+    \/ \E id \in MsgIDs, k \in Slots : Send(id, k)
+    \/ \E n \in Nodes, m \in network : Process(n, m)
+    \/ \E n \in Nodes : Freeze(n)
+    \/ Reconcile
+    \/ MCNextCslot
+
+MCSpec == Init /\ [][MCNext]_vars
+
+MCFairness ==
+    /\ WF_vars(Reconcile)
+    /\ WF_vars(MCNextCslot)
+    /\ \A n \in Nodes : WF_vars(Freeze(n))
+
+MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness
+
+MCTypeInvariant ==
+    /\ TypeInvariant
+    /\ current_slot \in Slots
+    /\ \A m \in network : m.cslot \in Slots
+
+\* Apalache entry point: constants fixed symbolically.
+ConstInit ==
+    /\ Nodes   = {"n1", "n2"}
+    /\ MsgIDs  = {"a", "b"}
+    /\ MaxSlot = 1
+
+===============================================================

specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg

@@ -0,0 +1,12 @@
+\* Liveness model. Bounded through MCNext rather than a CONSTRAINT.
+
+SPECIFICATION MCLiveSpec
+
+CONSTANTS
+    Nodes   = {n1, n2}
+    MsgIDs  = {m1}
+    MaxSlot = 1
+
+PROPERTIES
+    EventualCommit
+    EventualAgreement

specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg

@@ -0,0 +1,18 @@
+\* Safety model for the agreement layer, under adversarial replay.
+
+SPECIFICATION MCSpec
+
+CONSTANTS
+    Nodes   = {n1, n2}
+    MsgIDs  = {m1, m2}
+    MaxSlot = 2
+
+INVARIANTS
+    MCTypeInvariant
+    ProcessedAreCurrentSlot
+    CommittedIsUnion
+    MerkleAgreement
+    CommittedSupersetsProcessed
+    NoPhantomInCommitted
+    NoReorderAcrossCslot
+    PhaseProgressionValid

specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.cfg

@@ -0,0 +1,17 @@
+\* Per-node clocks under bounded skew, with Byzantine slot/origin spoofing.
+
+SPECIFICATION MCSpec
+
+CONSTANTS
+    Nodes   = {n1, n2}
+    MsgIDs  = {m1}
+    MaxSkew = 1
+    MaxSlot = 2
+
+INVARIANTS
+    MCTypeInvariant
+    BoundedSkew
+    ExactlyOncePerNode
+    CSlotLocalAdmission
+    PersistedReflectsReality
+    NoPhantomProcess

specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla

@@ -0,0 +1,34 @@
+---- MODULE MC_Vortex_DSE_CSlot_Skew ----
+(***************************************************************************)
+(* TLC harness for Vortex_DSE_CSlot_Skew.                                  *)
+(*                                                                          *)
+(* MaxSkew is a protocol parameter and stays in the specification: it is    *)
+(* the assumption the protocol relies on. MaxSlot is only a horizon for     *)
+(* model checking, so it lives here and bounds the actions directly.        *)
+(***************************************************************************)
+EXTENDS Vortex_DSE_CSlot_Skew
+
+CONSTANT MaxSlot
+
+Slots == 0..MaxSlot
+
+MCTick(n) ==
+    /\ node_slot[n] < MaxSlot
+    /\ SkewedTick(n)
+
+MCNext ==
+    \/ \E id \in MsgIDs, n \in Nodes : Submit(id, n)
+    \/ \E n \in Nodes, m \in network : Process(n, m)
+    \/ \E n \in Nodes : Crash(n)
+    \/ \E n \in Nodes : Rejoin(n)
+    \/ \E id \in MsgIDs, k \in Slots : ByzantineInject(id, k)
+    \/ \E n \in Nodes : MCTick(n)
+
+MCSpec == Init /\ [][MCNext]_vars
+
+MCTypeInvariant ==
+    /\ TypeInvariant
+    /\ node_slot \in [Nodes -> Slots]
+    /\ \A m \in network : m.cslot \in Slots
+
+====

specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.cfg

@@ -0,0 +1,17 @@
+\* Safety model for the strict (opt-in TTL) admission mode.
+
+SPECIFICATION MCSpec
+
+CONSTANTS
+    Nodes   = {n1, n2}
+    MsgIDs  = {m1, m2}
+    MaxSlot = 4
+
+INVARIANTS
+    MCTypeInvariant
+    ExactlyOncePerNode
+    CSlotStrictAdmission
+    PersistedReflectsReality
+    NoPhantomProcess
+    DecisionLocalityOnly
+    NoLateAdmission

specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla

@@ -0,0 +1,41 @@
+---- MODULE MC_Vortex_DSE_CSlot_TTL ----
+(***************************************************************************)
+(* TLC harness for Vortex_DSE_CSlot_TTL.                                   *)
+(*                                                                          *)
+(* As in MC_Vortex_DSE_CSlot, the slot horizon is a model-checking concern  *)
+(* and is imposed inside the actions rather than as a CONSTRAINT, so that   *)
+(* no successor state is discarded while temporal properties are checked.   *)
+(***************************************************************************)
+EXTENDS Vortex_DSE_CSlot_TTL
+
+CONSTANT MaxSlot
+
+Slots == 0..MaxSlot
+
+MCTick ==
+    /\ current_slot < MaxSlot
+    /\ Tick
+
+MCNext ==
+    \/ \E id \in MsgIDs, k \in Slots : Send(id, k)
+    \/ \E n \in Nodes, m \in network : Process(n, m)
+    \/ \E n \in Nodes : Crash(n)
+    \/ \E n \in Nodes : Rejoin(n)
+    \/ MCTick
+
+MCSpec == Init /\ [][MCNext]_vars
+
+MCFairness ==
+    /\ WF_vars(MCTick)
+    /\ \A n \in Nodes : WF_vars(Rejoin(n))
+
+MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness
+
+MCTickProgress == <>[](current_slot = MaxSlot)
+
+MCTypeInvariant ==
+    /\ TypeInvariant
+    /\ current_slot \in Slots
+    /\ \A m \in network : m.cslot \in Slots
+
+====

specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_admission.cfg

@@ -0,0 +1,13 @@
+\* A deliberate liveness failure. Under the strict gate a message whose slot
+\* has passed is refused for good, so eventual admission does not hold. This
+\* is what the bounded-memory mode costs, and it is the reason the strict
+\* rule is a concession rather than a stronger protocol.
+
+SPECIFICATION MCLiveSpec
+
+CONSTANTS
+    Nodes   = {n1, n2}
+    MsgIDs  = {m1}
+    MaxSlot = 1
+
+PROPERTY EventualAdmission

specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg

@@ -0,0 +1,12 @@
+\* Liveness model. Bounded through MCNext rather than a CONSTRAINT.
+
+SPECIFICATION MCLiveSpec
+
+CONSTANTS
+    Nodes   = {n1, n2}
+    MsgIDs  = {m1}
+    MaxSlot = 2
+
+PROPERTIES
+    MCTickProgress
+    EventualRejoin

specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg

@@ -0,0 +1,14 @@
+\* Liveness model. Bounded inside MCTick rather than by a state constraint,
+\* so no successor state is discarded while temporal properties are checked.
+
+SPECIFICATION MCLiveSpec
+
+CONSTANTS
+    Nodes   = {n1, n2}
+    MsgIDs  = {m1}
+    MaxSlot = 1
+
+PROPERTIES
+    MCTickProgress
+    EventualRejoin
+    EventualAdmission