Add "dag-based consensus"

specifications/dag-consensus/BlockDag.tla

@@ -0,0 +1,67 @@
+----------------------------- MODULE BlockDag -----------------------------
+
+(**************************************************************************************)
+(* In this specification we define notions on DAGs useful for DAG-based consensus     *)
+(* protocols (which build DAGs of blocks)                                             *)
+(**************************************************************************************)
+
+EXTENDS FiniteSets, Sequences, Integers, Utils, Digraph, TLC
+
+CONSTANTS
+    N \* The set of all network nodes (not DAG nodes)
+,   R \* The set of rounds
+,   Leader(_) \* operator mapping each round to its leader
+
+(**************************************************************************************)
+(* For our purpose of checking safety and liveness, DAG vertices just consist of a   *)
+(* node and a round.                                                                  *)
+(**************************************************************************************)
+V == N \times R \* the set of possible DAG vertices
+Node(v) == v[1]
+Round(v) == IF v = <<>> THEN 0 ELSE v[2] \* accomodates <<>> as default value
+
+(**************************************************************************************)
+(* Next we define leader vertices:                                                    *)
+(**************************************************************************************)
+LeaderVertex(r) == IF r > 0 THEN <<Leader(r), r>> ELSE <<>>
+IsLeader(v) == LeaderVertex(Round(v)) = v
+Genesis == <<>>
+ASSUME IsLeader(Genesis) \* this should hold
+
+(**************************************************************************************)
+(* OrderSet(S) arbitrarily order the members of the set S.  Note that, in TLA+,       *)
+(* `CHOOSE' is deterministic but arbitrary choice, i.e. `CHOOSE e \in S : TRUE' is    *)
+(* always the same `e' if `S' is the same                                             *)
+(**************************************************************************************)
+RECURSIVE OrderSet(_)
+OrderSet(S) == IF S = {} THEN <<>> ELSE
+    LET e == CHOOSE e \in S : TRUE
+    IN  Append(OrderSet(S \ {e}), e)
+
+(**************************************************************************************)
+(* PreviousLeader(dag, r) returns the leader vertex in dag whose round is the         *)
+(* largest but smaller than r.  We assume that dag contains at least the genesis      *)
+(* vertex.                                                                            *)
+(**************************************************************************************)
+PreviousLeader(dag, r) == CHOOSE l \in Vertices(dag) : 
+    /\  IsLeader(l)
+    /\  Round(l) = Max({Round(l2) : l2 \in 
+            {l2 \in Vertices(dag) : IsLeader(l2) /\ Round(l2) < r}})
+
+(**************************************************************************************)
+(* Linearize a DAG. In a real blockchain we should use a topological ordering, but,   *)
+(* for the purpose of ensuring agreement, an arbitrary ordering (as provided by       *)
+(* OrderSet) is fine. This assume a DAG where all paths end with the Genesis          *)
+(* vertex.                                                                            *)
+(**************************************************************************************)
+RECURSIVE Linearize(_, _)
+Linearize(dag, l) == IF Vertices(dag) = {<<>>} THEN <<>> ELSE
+    LET dagOfL == SubDag(dag, {l})
+        prevL == PreviousLeader(dagOfL, Round(l))
+        dagOfPrev == SubDag(dag, {prevL})
+        remaining == Vertices(dagOfL) \ Vertices(dagOfPrev)
+    IN  Linearize(dagOfPrev, prevL) \o OrderSet(remaining \ {l}) \o <<l>>
+
+Compatible(s1, s2) == \* whether the sequence s1 is a prefix of the sequence s2, or vice versa
+    \A i \in 1..Min({Len(s1), Len(s2)}) : s1[i] = s2[i]
+=========================================================================

specifications/dag-consensus/BlockDagTest.tla

@@ -0,0 +1,50 @@
+----------------------------- MODULE BlockDagTest -----------------------------
+
+(**************************************************************************************)
+(* Tests for BlockDag operators using small concrete DAGs.                            *)
+(**************************************************************************************)
+
+EXTENDS FiniteSets, Sequences, Integers, TLC
+
+N == {1, 2}
+R == 1..3
+Leader(r) == CASE
+    r = 1 -> 1
+[]  r = 2 -> 2
+[]  r = 3 -> 1
+
+INSTANCE BlockDag WITH N <- N, R <- R, Leader <- Leader
+
+v11 == <<1, 1>> \* leader
+v21 == <<2, 1>>
+v12 == <<1, 2>>
+v22 == <<2, 2>> \* leader
+v13 == <<1, 3>> \* leader
+v23 == <<2, 3>>
+
+ASSUME TestNodeRound == Node(v12) = 1 /\ Round(v12) = 2
+
+ASSUME TestLeaderVertice ==
+    /\ LeaderVertex(1) = v11
+    /\ LeaderVertex(2) = v22
+    /\ LeaderVertex(3) = v13
+
+ASSUME TestOrderSetPermutation ==
+    LET SeqToSet(seq) == {seq[i] : i \in DOMAIN seq}
+        IsPermutation(seq, s) == SeqToSet(seq) = s /\ Len(seq) = Cardinality(s)
+    IN  IsPermutation(OrderSet({v11, v21}), {v11, v21})
+
+dag1 ==
+    << {Genesis, v11, v21, v12, v22, v13, v23},
+       {<<v11, Genesis>>, <<v21, Genesis>>, 
+            <<v12, v21>>, <<v22, v11>>, <<v13, v22>>,
+            <<v13, v21>>, <<v13, v12>>, <<v23, v22>>} >>
+
+ASSUME TestPreviousLeader1 == PreviousLeader(dag1, 3) = v22
+ASSUME TestPreviousLeader2 == PreviousLeader(dag1, 2) = v11 
+ASSUME TestPreviousLeaderBase == PreviousLeader(dag1, 1) = <<>> 
+
+ASSUME TestLinearize == Linearize(dag1, v13) =
+    <<<<1, 1>>, <<2, 2>>>> \o OrderSet({<<2, 1>>, <<1, 2>>}) \o <<<<1, 3>>>>
+
+=========================================================================

specifications/dag-consensus/Digraph.tla

@@ -0,0 +1,35 @@
+----------------------------- MODULE Digraph -----------------------------
+
+(**************************************************************************************)
+(* A digraph is a pair consisting of a set of vertices and a set of edges             *)
+(**************************************************************************************)
+
+Vertices(digraph) == digraph[1]
+Edges(digraph) == digraph[2]
+
+IsDigraph(digraph) ==
+    /\  digraph = <<Vertices(digraph), Edges(digraph)>>
+    /\  \A e \in Edges(digraph) :
+        /\  e = <<e[1],e[2]>>
+        /\  {e[1],e[2]} \subseteq Vertices(digraph)
+
+Children(digraph, v) ==
+    {c \in Vertices(digraph) : <<v, c>> \in Edges(digraph)}
+
+(**************************************************************************************)
+(* Descendants(dag, vs) is the set of vertices reachable from any vertex in vs       *)
+(**************************************************************************************)
+RECURSIVE Descendants(_, _)
+Descendants(dag, vs) == IF vs = {} THEN {} ELSE
+    LET children == {c \in Vertices(dag) : \E v \in vs : <<v,c>> \in Edges(dag)} IN
+        children \cup Descendants(dag, children)
+
+(**************************************************************************************)
+(* The sub-dag reachable from the set of vertices vs:                                 *)
+(**************************************************************************************)
+SubDag(dag, vs) ==
+    LET vs2 == Descendants(dag, vs) \cup vs
+        es2 == {e \in Edges(dag) : e[1] \in vs2} \* implies e[2] \in vs2
+    IN  <<vs2, es2>>
+
+==========================================================================

specifications/dag-consensus/README.md

@@ -0,0 +1,23 @@
+# Formal specifications of DAG-based consensus protocols
+
+Copied from [nano-o/dag-consensus](https://github.com/nano-o/dag-consensus).
+
+## Block DAGs
+
+[BlockDag.tla](./BlockDag.tla) defines block DAGs and how DAG-based consensus protocols linearize them.
+This specification should be reusable for other DAG-based consensus protocols.
+To run some basic tests, run `make block-dag-test`.
+
+## Sailfish
+
+[Sailfish.tla](./Sailfish.tla) contains a high-level formal specification modeling both the Sailfish and Sailfish++ protocols (at the level of abstraction of the specification, the differences between the protocols are not visible).
+
+Sailfish is described in the paper ["Sailfish: Towards Improving the Latency of DAG-based BFT"](https://eprint.iacr.org/2024/472), S&P 2025, and Sailfish++ appears in the paper ["Optimistic, Signature-Free Reliable Broadcast and Its Applications"](https://arxiv.org/abs/2505.02761), CCS 2025.
+
+To run TLC on the specification, first translate the PlusCal part to TLA+ with `make trans TLA_SPEC=Sailfish.tla` and then run `make run-tlc TLA_SPEC=TLCSailfish1.tla`. The specification `TLCSailfish1.tla` and the associated config file `TLCSailfish1.cfg` fix a concrete system size, model-checking bounds, and the properties to check (typing invariant, agreement, and liveness).
+
+Have a look at the Makefile to tweak TLC options.
+
+Notes:
+- `make trans` rewrites the TLA+ module in place after PlusCal translation.
+- The Makefile expects `java` and `wget` to be available to download/run `tla2tools.jar`.

specifications/dag-consensus/Sailfish.tla

@@ -0,0 +1,200 @@
+----------------------------- MODULE Sailfish -----------------------------
+
+(**************************************************************************************)
+(* This is a high-level specification of the Sailfish and Sailfish++ (also called     *)
+(* signature-free Sailfish) algorithms.  At the level of abstraction of this          *)
+(* specification, the differences between the two algorithms are not visible.         *)
+(**************************************************************************************)
+
+EXTENDS Integers, FiniteSets, Sequences
+
+CONSTANTS
+    N \* The set of all nodes
+,   F \* The set of Byzantine nodes
+,   R \* The set of rounds
+,   IsQuorum(_) \* Whether a set is a quorum (i.e. cardinality >= n-f)
+,   IsBlocking(_) \* Whether a set is a blocking set (i.e. cardinality >= f+1)
+,   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
+
+INSTANCE BlockDag \* Import definitions related to DAGs of blocks
+
+(**************************************************************************************)
+(* Now we specify the algorithm in the PlusCal language.                              *)
+(**************************************************************************************)
+(*--algorithm Sailfish {
+    variables
+        vs = {Genesis}, \* the vertices of the DAG
+        es = {}; \* the edges of the DAG
+    define {
+        dag == <<vs, es>>
+        NoLeaderVoteQuorum(r, vertices, add) ==
+            LET NoLeaderVote == {v \in vertices : LeaderVertex(r-1) \notin Children(dag, v)}
+            IN  IsQuorum({Node(v) : v \in NoLeaderVote} \cup add)
+    }
+    process (correctNode \in N \ F)
+        variables
+            round = 0, \* current round; 0 means the node has not started execution
+            log = <<>>; \* delivered log
+    {
+l0:     while (TRUE) {
+            if (round = 0) { \* start the first round r=1
+                round := 1;
+                vs := vs \cup {<<self, 1>>};
+                es := es \cup {<<<<self, 1>>, Genesis>>}
+            }
+            else { \* start a round r>1
+                with (r \in {r \in R : r > round})
+                with (deliveredVertices \in SUBSET {v \in vs : Round(v) = r-1}) {
+                    \* we enter a round only if we have a quorum of vertices:
+                    await IsQuorum({Node(v) : v \in deliveredVertices});
+                    \* if this is after GST, we must have all correct vertices:
+                    await r >= GST => (N \ F) \subseteq {Node(v) : v \in deliveredVertices};
+                    \* enter round r:
+                    round := r;
+                    \* if the r-1 leader does not reference the r-2 leader,
+                    \* then we must be sure the r-2 leader cannot commit:
+                    await LeaderVertex(r-1) \in deliveredVertices =>
+                            \/ LeaderVertex(r-2) \in Children(dag, LeaderVertex(r-1))
+                            \/ NoLeaderVoteQuorum(r-1, deliveredVertices, {});
+                    \* if we are the leader, then we must include the r-1 leader or
+                    \* have evidence it cannot commit:
+                    if (Leader(r) = self)
+                        await   \/ LeaderVertex(r-1) \in deliveredVertices
+                                \/ NoLeaderVoteQuorum(r, {v \in vs : Round(v) = r}, {self});
+                    \* create a new vertex:
+                    with (newV = <<self, r>>) {
+                        vs := vs \cup {newV};
+                        es := es \cup {<<newV, pv>> : pv \in deliveredVertices};
+                    };
+                    \* commit if there is a quorum of votes for the leader of r-2:
+                    if (r > 2)
+                        with (votesForLeader = {pv \in deliveredVertices : <<pv, LeaderVertex(r-2)>> \in es})
+                        if (IsQuorum({Node(pv) : pv \in votesForLeader}))
+                            log := Linearize(dag, LeaderVertex(r-2))
+                }
+            }
+        }
+    }
+(**************************************************************************************)
+(*     Next comes our model of Byzantine nodes. Because the real protocol             *)
+(*     disseminates DAG vertices using reliable broadcast, Byzantine nodes cannot     *)
+(*     equivocate and cannot deviate much from the protocol (lest their messages      *)
+(*     be ignored).                                                                   *)
+(**************************************************************************************)
+    process (byzantineNode \in F)
+    {
+l0:     while (TRUE) {
+            with (r \in R)
+            with (newV = <<self, r>>) {
+                when newV \notin vs; \* no equivocation
+                if (r = 1) {
+                    vs := vs \cup {newV};
+                    es := es \cup {<<newV, Genesis>>}
+                }
+                else
+                with (delivered \in SUBSET {v \in vs : Round(v) = r-1}) {
+                    await IsQuorum({Node(v) : v \in delivered}); \* ignored otherwise
+                    vs := vs \cup {newV};
+                    es := es \cup {<<newV, pv>> : pv \in delivered}
+                }
+            }
+        }
+    }
+}*)
+\* BEGIN TRANSLATION (chksum(pcal) = "c16dfa43" /\ chksum(tla) = "9cdbd4f5")
+\* Label l0 of process correctNode at line 42 col 9 changed to l0_
+VARIABLES vs, es
+
+(* define statement *)
+dag == <<vs, es>>
+NoLeaderVoteQuorum(r, vertices, add) ==
+    LET NoLeaderVote == {v \in vertices : LeaderVertex(r-1) \notin Children(dag, v)}
+    IN  IsQuorum({Node(v) : v \in NoLeaderVote} \cup add)
+
+VARIABLES round, log
+
+vars == << vs, es, round, log >>
+
+ProcSet == (N \ F) \cup (F)
+
+Init == (* Global variables *)
+        /\ vs = {Genesis}
+        /\ es = {}
+        (* Process correctNode *)
+        /\ round = [self \in N \ F |-> 0]
+        /\ log = [self \in N \ F |-> <<>>]
+
+correctNode(self) == IF round[self] = 0
+                        THEN /\ round' = [round EXCEPT ![self] = 1]
+                             /\ vs' = (vs \cup {<<self, 1>>})
+                             /\ es' = (es \cup {<<<<self, 1>>, Genesis>>})
+                             /\ log' = log
+                        ELSE /\ \E r \in {r \in R : r > round[self]}:
+                                  \E deliveredVertices \in SUBSET {v \in vs : Round(v) = r-1}:
+                                    /\ IsQuorum({Node(v) : v \in deliveredVertices})
+                                    /\ r >= GST => (N \ F) \subseteq {Node(v) : v \in deliveredVertices}
+                                    /\ round' = [round EXCEPT ![self] = r]
+                                    /\ LeaderVertex(r-1) \in deliveredVertices =>
+                                         \/ LeaderVertex(r-2) \in Children(dag, LeaderVertex(r-1))
+                                         \/ NoLeaderVoteQuorum(r-1, deliveredVertices, {})
+                                    /\ IF Leader(r) = self
+                                          THEN /\ \/ LeaderVertex(r-1) \in deliveredVertices
+                                                  \/ NoLeaderVoteQuorum(r, {v \in vs : Round(v) = r}, {self})
+                                          ELSE /\ TRUE
+                                    /\ LET newV == <<self, r>> IN
+                                         /\ vs' = (vs \cup {newV})
+                                         /\ es' = (es \cup {<<newV, pv>> : pv \in deliveredVertices})
+                                    /\ IF r > 2
+                                          THEN /\ LET votesForLeader == {pv \in deliveredVertices : <<pv, LeaderVertex(r-2)>> \in es'} IN
+                                                    IF IsQuorum({Node(pv) : pv \in votesForLeader})
+                                                       THEN /\ log' = [log EXCEPT ![self] = Linearize(dag, LeaderVertex(r-2))]
+                                                       ELSE /\ TRUE
+                                                            /\ log' = log
+                                          ELSE /\ TRUE
+                                               /\ log' = log
+
+byzantineNode(self) == /\ \E r \in R:
+                            LET newV == <<self, r>> IN
+                              /\ newV \notin vs
+                              /\ IF r = 1
+                                    THEN /\ vs' = (vs \cup {newV})
+                                         /\ es' = (es \cup {<<newV, Genesis>>})
+                                    ELSE /\ \E delivered \in SUBSET {v \in vs : Round(v) = r-1}:
+                                              /\ IsQuorum({Node(v) : v \in delivered})
+                                              /\ vs' = (vs \cup {newV})
+                                              /\ es' = (es \cup {<<newV, pv>> : pv \in delivered})
+                       /\ UNCHANGED << round, log >>
+
+Next == (\E self \in N \ F: correctNode(self))
+           \/ (\E self \in F: byzantineNode(self))
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION 
+
+(**************************************************************************************)
+(* Basic type invariant:                                                              *)
+(**************************************************************************************)
+TypeOK ==
+    /\  \A v \in vs \ {<<>>} : 
+        /\  Node(v) \in N /\ Round(v) \in Nat \ {0}
+        /\  \A c \in Children(dag, v) : Round(c) = Round(v) - 1
+    /\  \A e \in es :
+            /\  e = <<e[1],e[2]>>
+            /\  {e[1], e[2]} \subseteq vs
+    /\  \A n \in N \ F : round[n] \in Nat
+
+(**************************************************************************************)
+(* Next we define the safety and liveness properties                                  *)
+(**************************************************************************************)
+
+Agreement == \A n1,n2 \in N \ F : Compatible(log[n1], log[n2])
+
+Liveness == \A r \in R : r >= GST /\ Leader(r) \notin F =>
+    \A n \in N \ F : round[n] >= r+2 =>
+        \E i \in DOMAIN log[n] : log[n][i] = LeaderVertex(r)
+
+===========================================================================

specifications/dag-consensus/TLCSailfish1.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION TerminatingSpec
+
+CONSTANTS
+    n1 = n1
+    n2 = n2
+    n3 = n3
+
+INVARIANT TypeOK
+INVARIANT Agreement
+INVARIANT Liveness
+\* INVARIANT Falsy3
+
+CONSTRAINT StateConstraint