From 8fa4ac5e032ddb4f67aa7ecf03693876012152ae Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 21 Aug 2026 13:24:37 -0700 Subject: [PATCH] dag-consensus: state the assumptions of BlockDag and Sailfish Agreement and Liveness rest on premises the modules left implicit: that F is a subset of N, that Leader maps rounds to nodes, that rounds are positive integers, and that two quorums share a correct node. Stated one by one, they are premises TLAPS can cite. TLC ignores the assumptions of an instantiated module, so TLCSailfish1, TLCSailfish2 and BlockDagTest assume each of them again. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- specifications/dag-consensus/BlockDag.tla | 12 +++++- specifications/dag-consensus/BlockDagTest.tla | 5 +++ specifications/dag-consensus/Sailfish.tla | 43 ++++++++++++++++++- specifications/dag-consensus/TLCSailfish1.tla | 16 +++++++ specifications/dag-consensus/TLCSailfish2.tla | 16 +++++++ 5 files changed, 90 insertions(+), 2 deletions(-) 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)