Add "dag-based consensus"

README.md

@@ -105,6 +105,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder           |          |             |         |           |          |
 | [Buffered Random Access File](specifications/braf)                                                  | Calvin Loncaric                                     |          |             |         |     ✔     |          |
 | [Disruptor](specifications/Disruptor)                                                               | Nicholas Schultz-Møller                             |          |             |         |     ✔     |          |
+| [DAG-based Consensus](specifications/dag-consensus)                                                 | Giuliano Losa                                       |          |             |    ✔    |     ✔     |          |
 
 
 ## Other Examples
@@ -151,7 +152,7 @@ Ideally these will be moved into this repo over time.
 | [Petri Nets](https://github.com/elh/petri-tlaplus)                                                                                | Instantiable Petri Nets with liveness properties                                                                                          | Eugene Huang                                                               |          |             |     ✔     |         |          |
 | [CRDT](https://github.com/JYwellin/CRDT-TLA)                                                                                      | Specifying and Verifying CRDT Protocols                                                                                                   | Ye Ji, Hengfeng Wei                                                        |          |             |     ✔     |         |          |
 | [Azure Cosmos DB](https://github.com/tlaplus/azure-cosmos-tla)                                                                    | Consistency models provided by Azure Cosmos DB                                                                                            | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe            |          |             |     ✔     |    ✔    |          |
-| [Simple Microwave Oven](specifications/microwave)                                                                                 | Spec of a microwave oven                                                                                                                  | Konstantin Läufer, George K. Thiruvathukal                        |    ✔    |         |             |     ✔     |         |          |
+| [Simple Microwave Oven](https://github.com/lucformalmethodscourse/microwave-tla)                                                                                 | Spec of a microwave oven                                                                                                                  | Konstantin Läufer, George K. Thiruvathukal                                 |    ✔     |             |           |    ✔    |          |   |
 
 ## Contributing a Spec
 

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`.