Apply the TLA+ review guidelines

Four things in the review guidelines were not being followed.

Constants now carry named assumptions. All four specifications declared
Nodes and MsgIDs with nothing constraining them, and Skew's MaxSkew with
nothing saying it is a natural number. The guidelines call this crucial
for TLAPS, and these modules do carry proofs.

Type invariants are back to the var \in S form: network \subseteq
MsgRecord rather than a quantifier over its elements. MsgRecord ranges
over Nat and so cannot be enumerated, which is why the MC module carries
its own bounded MCTypeInvariant for TLC.

Strong fairness on Process is now justified by measurement rather than
assertion. Weak fairness was tried, as the guidelines ask: the liveness
model reports a temporal-property violation under it, because a crash
intermittently disables Process. The module says so.

The horizon stays inside MCTick rather than moving to a state
CONSTRAINT, which the guidelines otherwise prefer. A constraint was
tried first and does not work here: TLC evaluates invariants on the
state that crosses the boundary before the constraint discards it, so
with MaxSlot = 2 a Tick reaches current_slot = 3 and any invariant
mentioning the horizon fails there. The reason is recorded in the module
header rather than left as an unexplained deviation.

Seven TLC models, all completing in under five seconds. The three TLAPS
modules discharge 191, 128 and 32 obligations and exit 0 under
tlapm --strict.

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com>

Author: vasilisnasopoulos

specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg

@@ -1,5 +1,5 @@
-\* Safety model. The horizon lives in MCNext, so no state constraint is
-\* needed: the reachable state graph is already finite.
+\* Safety model. The horizon is imposed inside MCTick; see the module
+\* header for why a state constraint does not work here.
 
 SPECIFICATION MCSpec
 
@@ -13,3 +13,5 @@ INVARIANT NoFutureAdmission
 INVARIANT ExactlyOncePerNode
 INVARIANT NoPhantomProcess
 INVARIANT DecisionLocalityOnly
+
+

specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla

@@ -2,22 +2,33 @@
 (***************************************************************************)
 (* TLC harness for Vortex_DSE_CSlot.                                       *)
 (*                                                                          *)
-(* The specification itself has no slot horizon: Tick is unbounded and      *)
-(* DuplicateInject may forge any slot in Nat. The horizon is a             *)
-(* model-checking concern and lives here.                                   *)
+(* 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 the actions rather than as a CONSTRAINT, so the    *)
-(* state graph is genuinely finite rather than merely truncated. That      *)
-(* matters for the liveness model: under a state constraint TLC discards   *)
-(* successor states, which can mask or invent violations of temporal       *)
-(* properties.                                                              *)
+(* 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
@@ -33,6 +44,21 @@ MCNext ==
 
 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))
@@ -45,10 +71,4 @@ MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness
 \* counter stays there rather than merely visiting it.
 MCTickProgress == <>[](current_slot = MaxSlot)
 
-\* Everything reachable in this model lies within the horizon.
-MCTypeInvariant ==
-    /\ TypeInvariant
-    /\ current_slot \in Slots
-    /\ \A m \in network : m.cslot \in Slots
-
 ====

specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg

@@ -1,5 +1,5 @@
-\* Liveness model. Bounded through MCNext rather than a CONSTRAINT, so no
-\* successor states are discarded while temporal properties are checked.
+\* Liveness model. Bounded inside MCTick rather than by a state constraint,
+\* so no successor state is discarded while temporal properties are checked.
 
 SPECIFICATION MCLiveSpec
 

specifications/VortexDSE/Vortex_DSE_CSlot.tla

@@ -36,6 +36,9 @@ CONSTANTS
     \* @type: Set(Str);
     MsgIDs           \* finite set of distinct message identifiers
 
+ASSUME NodesAssumption  == IsFiniteSet(Nodes)  /\ Nodes  # {}
+ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs)
+
 \* Node liveness states, named rather than written as bare strings.
 Up   == "up"
 Down == "down"
@@ -141,7 +144,7 @@ Spec == Init /\ [][Next]_vars
 
 TypeInvariant ==
     /\ current_slot \in Nat
-    /\ \A m \in network : m.id \in MsgIDs /\ m.cslot \in Nat
+    /\ network      \subseteq MsgRecord
     /\ processed    \in [Nodes -> SUBSET MsgIDs]
     /\ persisted    \in [Nodes -> SUBSET MsgIDs]
     /\ node_state   \in [Nodes -> {Up, Down}]

specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla

@@ -74,6 +74,9 @@ CONSTANTS
     \* @type: Set(Str);
     MsgIDs           \* finite set of distinct message identifiers
 
+ASSUME NodesAssumption  == IsFiniteSet(Nodes)  /\ Nodes  # {}
+ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs)
+
 \* AE phase names, rather than bare strings.
 Open      == "open"
 Frozen    == "frozen"

specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla

@@ -22,6 +22,10 @@ EXTENDS Naturals, FiniteSets
 
 CONSTANTS Nodes, MsgIDs, MaxSkew
 
+ASSUME NodesAssumption  == IsFiniteSet(Nodes)  /\ Nodes  # {}
+ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs)
+ASSUME MaxSkewAssumption == MaxSkew \in Nat
+
 \* Node liveness states, named rather than written as bare strings.
 Up   == "up"
 Down == "down"

specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla

@@ -31,6 +31,9 @@ CONSTANTS
     \* @type: Set(Str);
     MsgIDs           \* finite set of distinct message identifiers
 
+ASSUME NodesAssumption  == IsFiniteSet(Nodes)  /\ Nodes  # {}
+ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs)
+
 \* Node liveness states, named rather than written as bare strings.
 Up   == "up"
 Down == "down"