State the assumptions of BlockDag and Sailfish

specifications/dag-consensus/BlockDag.tla

@@ -12,6 +12,16 @@ CONSTANTS
 ,   R \* The set of rounds
 ,   Leader(_) \* operator mapping each round to its leader
 
+(**************************************************************************************)
+(* Round 0 is reserved for the genesis vertex, so it must not be a round of the       *)
+(* protocol.  Rounds being integers also bounds the set whose Max PreviousLeader      *)
+(* takes by 0..r-1, and it is what makes the recursion of Linearize well-founded.     *)
+(**************************************************************************************)
+
+ASSUME RoundsArePositiveIntegers == R \subseteq Nat \ {0}
+
+ASSUME LeadersAreNodes == \A r \in R : Leader(r) \in N
+
 (**************************************************************************************)
 (* For our purpose of checking safety and liveness, DAG vertices just consist of a   *)
 (* node and a round.                                                                  *)
@@ -26,7 +36,7 @@ Round(v) == IF v = <<>> THEN 0 ELSE v[2] \* accomodates <<>> as default value
 LeaderVertex(r) == IF r > 0 THEN <<Leader(r), r>> ELSE <<>>
 IsLeader(v) == LeaderVertex(Round(v)) = v
 Genesis == <<>>
-ASSUME IsLeader(Genesis) \* this should hold
+ASSUME GenesisIsALeaderVertex == IsLeader(Genesis) \* this should hold
 
 (**************************************************************************************)
 (* OrderSet(S) arbitrarily order the members of the set S.  Note that, in TLA+,       *)

specifications/dag-consensus/BlockDagTest.tla

@@ -15,6 +15,11 @@ Leader(r) == CASE
 
 INSTANCE BlockDag WITH N <- N, R <- R, Leader <- Leader
 
+\* TLC does not check the assumptions of an instantiated module, so assume them again:
+ASSUME RoundsArePositiveIntegers
+ASSUME LeadersAreNodes
+ASSUME GenesisIsALeaderVertex
+
 v11 == <<1, 1>> \* leader
 v21 == <<2, 1>>
 v12 == <<1, 2>>

specifications/dag-consensus/Sailfish.tla

@@ -17,7 +17,48 @@ CONSTANTS
 ,   Leader(_) \* operator mapping each round to its leader
 ,   GST \* the first round in which the system is synchronous
 
-ASSUME \E n \in R : R = 1..n \* rounds start at 1; 0 is used as default placeholder
+(**************************************************************************************)
+(* Explicitly state the properties of the constants that the protocol relies on.    *)
+(* They are all satisfied by the canonical instantiation, in which N has n > 3f       *)
+(* members, F has at most f members, the quorums are the sets of at least n-f nodes,  *)
+(* and the blocking sets are the sets of at least f+1 nodes.  Beware that TLC does    *)
+(* not check the assumptions of an instantiated module; the TLC-specific modules      *)
+(* therefore assume each of them again, by name.                                      *)
+(**************************************************************************************)
+
+\* Quorums and blocking sets are defined by counting nodes, which presupposes that
+\* there are finitely many of them:
+ASSUME NodesAreFinite == IsFiniteSet(N)
+
+ASSUME ByzantineNodesAreNodes == F \subseteq N
+
+ASSUME SomeNodeIsCorrect == N \ F # {}
+
+\* Rounds are contiguous, since a node entering round r reasons about r-1 and r-2:
+ASSUME RoundsStartAtOne == \E n \in R : R = 1..n
+
+\* GST need not be a member of R; if it is not, then the system never becomes
+\* synchronous in the rounds under consideration:
+ASSUME GSTIsARoundNumber == GST \in Nat
+
+\* Since only correct nodes are guaranteed to follow the protocol, the correct nodes
+\* have to form a quorum, or else no round could ever be entered:
+ASSUME CorrectNodesFormQuorum == IsQuorum(N \ F)
+
+\* Any two quorums have a correct node in common; this is what prevents two correct
+\* nodes from committing conflicting leader vertices:
+ASSUME QuorumsIntersectInCorrectNode ==
+    \A Q1,Q2 \in SUBSET N : IsQuorum(Q1) /\ IsQuorum(Q2) => (Q1 \cap Q2) \ F # {}
+
+\* Removing the Byzantine nodes from a quorum leaves a blocking set:
+ASSUME QuorumMinusByzantineIsBlocking ==
+    \A Q \in SUBSET N : IsQuorum(Q) => IsBlocking(Q \ F)
+
+ASSUME BlockingSetsContainCorrectNode ==
+    \A B \in SUBSET N : IsBlocking(B) => B \ F # {}
+
+ASSUME BlockingSetsIntersectQuorums ==
+    \A B,Q \in SUBSET N : IsBlocking(B) /\ IsQuorum(Q) => B \cap Q # {}
 
 INSTANCE BlockDag \* Import definitions related to DAGs of blocks
 

specifications/dag-consensus/TLCSailfish1.tla

@@ -26,6 +26,22 @@ GST == 3
 
 INSTANCE Sailfish
 
+(**************************************************************************************)
+(* TLC does not check the assumptions of an instantiated module, so we assume them    *)
+(* again here to have them checked against the parameters defined above.              *)
+(**************************************************************************************)
+ASSUME NodesAreFinite
+ASSUME ByzantineNodesAreNodes
+ASSUME SomeNodeIsCorrect
+ASSUME RoundsStartAtOne
+ASSUME LeadersAreNodes
+ASSUME GSTIsARoundNumber
+ASSUME CorrectNodesFormQuorum
+ASSUME QuorumsIntersectInCorrectNode
+ASSUME QuorumMinusByzantineIsBlocking
+ASSUME BlockingSetsContainCorrectNode
+ASSUME BlockingSetsIntersectQuorums
+
 (**************************************************************************************)
 (* Next we define a constraint to stop the model-checker.                             *)
 (**************************************************************************************)

specifications/dag-consensus/TLCSailfish2.tla

@@ -24,6 +24,22 @@ GST == 6
 
 INSTANCE Sailfish
 
+(**************************************************************************************)
+(* TLC does not check the assumptions of an instantiated module, so we assume them    *)
+(* again here to have them checked against the parameters defined above.              *)
+(**************************************************************************************)
+ASSUME NodesAreFinite
+ASSUME ByzantineNodesAreNodes
+ASSUME SomeNodeIsCorrect
+ASSUME RoundsStartAtOne
+ASSUME LeadersAreNodes
+ASSUME GSTIsARoundNumber
+ASSUME CorrectNodesFormQuorum
+ASSUME QuorumsIntersectInCorrectNode
+ASSUME QuorumMinusByzantineIsBlocking
+ASSUME BlockingSetsContainCorrectNode
+ASSUME BlockingSetsIntersectQuorums
+
 StateConstraint == \A n \in N \ F : round[n] \in 0..Max(R)
 
 Done == \A n \in N \ F : round[n] = Max(R)