diff --git a/specifications/dag-consensus/BlockDag.tla b/specifications/dag-consensus/BlockDag.tla index b71bdc12..a35e5e77 100644 --- a/specifications/dag-consensus/BlockDag.tla +++ b/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 <> 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+, *) diff --git a/specifications/dag-consensus/BlockDagTest.tla b/specifications/dag-consensus/BlockDagTest.tla index dcdb35cb..cb2b3f2b 100644 --- a/specifications/dag-consensus/BlockDagTest.tla +++ b/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>> diff --git a/specifications/dag-consensus/Sailfish.tla b/specifications/dag-consensus/Sailfish.tla index 03169ab3..5d8c6453 100644 --- a/specifications/dag-consensus/Sailfish.tla +++ b/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 diff --git a/specifications/dag-consensus/TLCSailfish1.tla b/specifications/dag-consensus/TLCSailfish1.tla index 98b9ecdb..487ea787 100644 --- a/specifications/dag-consensus/TLCSailfish1.tla +++ b/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. *) (**************************************************************************************) diff --git a/specifications/dag-consensus/TLCSailfish2.tla b/specifications/dag-consensus/TLCSailfish2.tla index 24c64617..7033330a 100644 --- a/specifications/dag-consensus/TLCSailfish2.tla +++ b/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)