diff --git a/README.md b/README.md index 8aa16616..3ae95272 100644 --- a/README.md +++ b/README.md @@ -98,60 +98,61 @@ Here is a list of specs included in this repository which are validated by the C | [Chameneos, a Concurrency Game](specifications/Chameneos) | Mariusz Ryndzionek | | | | ✔ | | | [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | | | [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | | -| [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | | -| [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | | -| [B-trees](specifications/btree) | Lorin Hochstein | | | | ✔ | | +| [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | | +| [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | | +| [B-trees](specifications/btree) | Lorin Hochstein | | | | ✔ | | | [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | | [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 Here is a list of specs stored in locations outside this repository or not validated by the CI, such as submodules. Since these specs are not covered by CI testing it is possible they contain errors, the reported details are incorrect, or they are no longer available. Ideally these will be moved into this repo over time. -| Spec | Details | Author(s) | Beginner | TLAPS Proof | TLC Model | PlusCal | Apalache | -| --------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------- | :------: | :---------: | :-------: | :-----: | :------: | -| [Blocking Queue](https://github.com/lemmy/BlockingQueue) | BlockingQueue | Markus Kuppe | ✔ | ✔ | ✔ | (✔) | | -| IEEE 802.16 WiMAX Protocols | 2006, [paper](https://users.cs.northwestern.edu/~ychen/Papers/npsec06.pdf), [specs](http://list.cs.northwestern.edu/802.16/) | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, Hai Zhou | | | | | | -| On the diversity of asynchronous communication | 2016, [paper](https://dl.acm.org/doi/10.1007/s00165-016-0379-x), [specs](http://hurault.perso.enseeiht.fr/asynchronousCommunication/) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | | | | | -| [Caesar](specifications/Caesar) | Multi-leader generalized consensus protocol (Arun et al., 2017) | Giuliano Losa | | | ✔ | ✔ | | -| [CASPaxos](specifications/CASPaxos) | An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) | Tobias Schottdorf | | | ✔ | | | -| [DataPort](specifications/DataPort) | Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) | Geoffrey Biggs, Noriaki Ando | | | | | | -| [egalitarian-paxos](specifications/egalitarian-paxos) | Leaderless replication protocol based on Paxos (Moraru et al., 2013) | Iulian Moraru | | | ✔ | | | -| [fastpaxos](specifications/fastpaxos) | An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) | Leslie Lamport | | | | | | -| [fpaxos](specifications/fpaxos) | A variant of Paxos with flexible quorums (Howard et al., 2017) | Heidi Howard | | | ✔ | | | -| [HLC](specifications/HLC) | Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) | Murat Demirbas | | | ✔ | ✔ | | -| [L1](specifications/L1) | Data center network L1 switch protocol, only PDF files (Thacker) | Tom Rodeheffer | | | | | | -| [leaderless](specifications/leaderless) | Leaderless generalized-consensus algorithms (Losa, 2016) | Giuliano Losa | | | ✔ | ✔ | | -| [losa_ap](specifications/losa_ap) | The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) | Giuliano Losa | | | ✔ | ✔ | | -| [losa_rda](specifications/losa_rda) | Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) | Giuliano Losa | | | | | | -| [m2paxos](specifications/m2paxos) | Multi-leader consensus protocols (Peluso et al., 2016) | Giuliano Losa | | | ✔ | | | -| [mongo-repl-tla](specifications/mongo-repl-tla) | A simplified part of Raft in MongoDB (Ongaro, 2014) | Siyuan Zhou | | | ✔ | | | -| [MultiPaxos](specifications/MultiPaxos) | The abstract specification of Generalized Paxos (Lamport, 2004) | Giuliano Losa | | | ✔ | | | -| [naiad](specifications/naiad) | Naiad clock protocol, only PDF files (Murray et al., 2013) | Tom Rodeheffer | | | ✔ | | | -| [nfc04](specifications/nfc04) | Non-functional properties of component-based software systems (Zschaler, 2010) | Steffen Zschaler | | | ✔ | | | -| [raft](specifications/raft) | Raft consensus algorithm (Ongaro, 2014) | Diego Ongaro | | | ✔ | | | -| [SnapshotIsolation](specifications/SnapshotIsolation) | Serializable snapshot isolation (Cahill et al., 2010) | Michael J. Cahill, Uwe Röhm, Alan D. Fekete | | | ✔ | | | -| [SyncConsensus](specifications/SyncConsensus) | Synchronized round consensus algorithm (Demirbas) | Murat Demirbas | | | ✔ | ✔ | | -| [Termination](specifications/Termination) | Channel-counting algorithm (Kumar, 1985) | Giuliano Losa | | ✔ | ✔ | ✔ | ✔ | -| [Tla-tortoise-hare](specifications/Tla-tortoise-hare) | Robert Floyd's cycle detection algorithm | Lorin Hochstein | | | ✔ | ✔ | | -| [VoldemortKV](specifications/VoldemortKV) | Voldemort distributed key value store | Murat Demirbas | | | ✔ | ✔ | | -| [Tencent-Paxos](specifications/TencentPaxos) | PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017) | Xingchen Yi, Hengfeng Wei | | ✔ | ✔ | | | -| [Paxos](https://github.com/neoschizomer/Paxos) | Paxos | | | | ✔ | | | -| [Lock-Free Set](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla) | PlusCal spec of a lock-Free set used by TLC | Markus Kuppe | | | ✔ | ✔ | | -| [ParallelRaft](specifications/ParalleRaft) | A variant of Raft | Xiaosong Gu, Hengfeng Wei, Yu Huang | | | ✔ | | | -| [CRDT-Bug](https://github.com/Alexander-N/tla-specs/tree/main/crdt-bug) | CRDT algorithm with defect and fixed version | Alexander Niederbühl | | | ✔ | | | -| [asyncio-lock](https://github.com/Alexander-N/tla-specs/tree/main/asyncio-lock) | Bugs from old versions of Python's asyncio lock | Alexander Niederbühl | | | ✔ | | | -| [Raft (with cluster changes)](https://github.com/dranov/raft-tla) | Raft with cluster changes, and a version with Apalache type annotations but no cluster changes | George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts | | | ✔ | | ✔ | -| [MET for CRDT-Redis](https://github.com/elem-azar-unis/CRDT-Redis/tree/master/MET/TLA) | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | | ✔ | ✔ | | -| [Parallel increment](https://github.com/Cjen1/tla_increment) | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | | ✔ | | | -| [The Streamlet consensus algorithm](https://github.com/nano-o/streamlet) | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | | ✔ | ✔ | | -| [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 | ✔ | | | ✔ | | | +| Spec | Details | Author(s) | Beginner | TLAPS Proof | TLC Model | PlusCal | Apalache | | +| --------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------- | :------: | :---------: | :-------: | :-----: | :------: | --- | +| [Blocking Queue](https://github.com/lemmy/BlockingQueue) | BlockingQueue | Markus Kuppe | ✔ | ✔ | ✔ | (✔) | | | +| IEEE 802.16 WiMAX Protocols | 2006, [paper](https://users.cs.northwestern.edu/~ychen/Papers/npsec06.pdf), [specs](http://list.cs.northwestern.edu/802.16/) | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, Hai Zhou | | | | | | | +| On the diversity of asynchronous communication | 2016, [paper](https://dl.acm.org/doi/10.1007/s00165-016-0379-x), [specs](http://hurault.perso.enseeiht.fr/asynchronousCommunication/) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | | | | | | +| [Caesar](specifications/Caesar) | Multi-leader generalized consensus protocol (Arun et al., 2017) | Giuliano Losa | | | ✔ | ✔ | | | +| [CASPaxos](specifications/CASPaxos) | An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) | Tobias Schottdorf | | | ✔ | | | | +| [DataPort](specifications/DataPort) | Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) | Geoffrey Biggs, Noriaki Ando | | | | | | | +| [egalitarian-paxos](specifications/egalitarian-paxos) | Leaderless replication protocol based on Paxos (Moraru et al., 2013) | Iulian Moraru | | | ✔ | | | | +| [fastpaxos](specifications/fastpaxos) | An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) | Leslie Lamport | | | | | | | +| [fpaxos](specifications/fpaxos) | A variant of Paxos with flexible quorums (Howard et al., 2017) | Heidi Howard | | | ✔ | | | | +| [HLC](specifications/HLC) | Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) | Murat Demirbas | | | ✔ | ✔ | | | +| [L1](specifications/L1) | Data center network L1 switch protocol, only PDF files (Thacker) | Tom Rodeheffer | | | | | | | +| [leaderless](specifications/leaderless) | Leaderless generalized-consensus algorithms (Losa, 2016) | Giuliano Losa | | | ✔ | ✔ | | | +| [losa_ap](specifications/losa_ap) | The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) | Giuliano Losa | | | ✔ | ✔ | | | +| [losa_rda](specifications/losa_rda) | Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) | Giuliano Losa | | | | | | | +| [m2paxos](specifications/m2paxos) | Multi-leader consensus protocols (Peluso et al., 2016) | Giuliano Losa | | | ✔ | | | | +| [mongo-repl-tla](specifications/mongo-repl-tla) | A simplified part of Raft in MongoDB (Ongaro, 2014) | Siyuan Zhou | | | ✔ | | | | +| [MultiPaxos](specifications/MultiPaxos) | The abstract specification of Generalized Paxos (Lamport, 2004) | Giuliano Losa | | | ✔ | | | | +| [naiad](specifications/naiad) | Naiad clock protocol, only PDF files (Murray et al., 2013) | Tom Rodeheffer | | | ✔ | | | | +| [nfc04](specifications/nfc04) | Non-functional properties of component-based software systems (Zschaler, 2010) | Steffen Zschaler | | | ✔ | | | | +| [raft](specifications/raft) | Raft consensus algorithm (Ongaro, 2014) | Diego Ongaro | | | ✔ | | | | +| [SnapshotIsolation](specifications/SnapshotIsolation) | Serializable snapshot isolation (Cahill et al., 2010) | Michael J. Cahill, Uwe Röhm, Alan D. Fekete | | | ✔ | | | | +| [SyncConsensus](specifications/SyncConsensus) | Synchronized round consensus algorithm (Demirbas) | Murat Demirbas | | | ✔ | ✔ | | | +| [Termination](specifications/Termination) | Channel-counting algorithm (Kumar, 1985) | Giuliano Losa | | ✔ | ✔ | ✔ | ✔ | | +| [Tla-tortoise-hare](specifications/Tla-tortoise-hare) | Robert Floyd's cycle detection algorithm | Lorin Hochstein | | | ✔ | ✔ | | | +| [VoldemortKV](specifications/VoldemortKV) | Voldemort distributed key value store | Murat Demirbas | | | ✔ | ✔ | | | +| [Tencent-Paxos](specifications/TencentPaxos) | PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017) | Xingchen Yi, Hengfeng Wei | | ✔ | ✔ | | | | +| [Paxos](https://github.com/neoschizomer/Paxos) | Paxos | | | | ✔ | | | | +| [Lock-Free Set](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla) | PlusCal spec of a lock-Free set used by TLC | Markus Kuppe | | | ✔ | ✔ | | | +| [ParallelRaft](specifications/ParalleRaft) | A variant of Raft | Xiaosong Gu, Hengfeng Wei, Yu Huang | | | ✔ | | | | +| [CRDT-Bug](https://github.com/Alexander-N/tla-specs/tree/main/crdt-bug) | CRDT algorithm with defect and fixed version | Alexander Niederbühl | | | ✔ | | | | +| [asyncio-lock](https://github.com/Alexander-N/tla-specs/tree/main/asyncio-lock) | Bugs from old versions of Python's asyncio lock | Alexander Niederbühl | | | ✔ | | | | +| [Raft (with cluster changes)](https://github.com/dranov/raft-tla) | Raft with cluster changes, and a version with Apalache type annotations but no cluster changes | George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts | | | ✔ | | ✔ | | +| [MET for CRDT-Redis](https://github.com/elem-azar-unis/CRDT-Redis/tree/master/MET/TLA) | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | | ✔ | ✔ | | | +| [Parallel increment](https://github.com/Cjen1/tla_increment) | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | | ✔ | | | | +| [The Streamlet consensus algorithm](https://github.com/nano-o/streamlet) | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | | ✔ | ✔ | | | +| [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](https://github.com/lucformalmethodscourse/microwave-tla) | Spec of a microwave oven | Konstantin Läufer, George K. Thiruvathukal | ✔ | | | ✔ | | | ## Contributing a Spec diff --git a/specifications/dag-consensus/BlockDag.tla b/specifications/dag-consensus/BlockDag.tla new file mode 100644 index 00000000..b71bdc12 --- /dev/null +++ b/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 <> 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 <> + +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] +========================================================================= diff --git a/specifications/dag-consensus/BlockDagTest.cfg b/specifications/dag-consensus/BlockDagTest.cfg new file mode 100644 index 00000000..e69de29b diff --git a/specifications/dag-consensus/BlockDagTest.tla b/specifications/dag-consensus/BlockDagTest.tla new file mode 100644 index 00000000..dcdb35cb --- /dev/null +++ b/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}, + {<>, <>, + <>, <>, <>, + <>, <>, <>} >> + +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>>>> + +========================================================================= diff --git a/specifications/dag-consensus/Digraph.tla b/specifications/dag-consensus/Digraph.tla new file mode 100644 index 00000000..26fe1dbe --- /dev/null +++ b/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 = <> + /\ \A e \in Edges(digraph) : + /\ e = <> + /\ {e[1],e[2]} \subseteq Vertices(digraph) + +Children(digraph, v) == + {c \in Vertices(digraph) : <> \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 : <> \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 <> + +========================================================================== diff --git a/specifications/dag-consensus/README.md b/specifications/dag-consensus/README.md new file mode 100644 index 00000000..2b5a4c0f --- /dev/null +++ b/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`. diff --git a/specifications/dag-consensus/Sailfish.tla b/specifications/dag-consensus/Sailfish.tla new file mode 100644 index 00000000..03169ab3 --- /dev/null +++ b/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 == <> + 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 {<>}; + es := es \cup {<<<>, 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 = <>) { + vs := vs \cup {newV}; + es := es \cup {<> : 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 : <> \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 = <>) { + when newV \notin vs; \* no equivocation + if (r = 1) { + vs := vs \cup {newV}; + es := es \cup {<>} + } + 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 {<> : 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 == <> +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 {<>}) + /\ es' = (es \cup {<<<>, 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 == <> IN + /\ vs' = (vs \cup {newV}) + /\ es' = (es \cup {<> : pv \in deliveredVertices}) + /\ IF r > 2 + THEN /\ LET votesForLeader == {pv \in deliveredVertices : <> \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 == <> IN + /\ newV \notin vs + /\ IF r = 1 + THEN /\ vs' = (vs \cup {newV}) + /\ es' = (es \cup {<>}) + 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 {<> : 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]} \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) + +=========================================================================== diff --git a/specifications/dag-consensus/TLCSailfish1.cfg b/specifications/dag-consensus/TLCSailfish1.cfg new file mode 100644 index 00000000..e44e6ace --- /dev/null +++ b/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 diff --git a/specifications/dag-consensus/TLCSailfish1.tla b/specifications/dag-consensus/TLCSailfish1.tla new file mode 100644 index 00000000..98b9ecdb --- /dev/null +++ b/specifications/dag-consensus/TLCSailfish1.tla @@ -0,0 +1,56 @@ +----------------------------- MODULE TLCSailfish1 ----------------------------- + +(**************************************************************************************) +(* In this configuartion, we have 3 nodes among which one is Byzantine. Quorums *) +(* are chosen such that every two quorums have a correct node in common, and each *) +(* blocking set intersects all quorums and contains a correct node. This allows to *) +(* exercise the protocol with some Byzantine behavior while limiting state-space *) +(* explosion. *) +(**************************************************************************************) + +EXTENDS Integers, FiniteSets + +VARIABLES vs, es, round, log + +CONSTANTS + n1,n2,n3 + +N == {n1,n2,n3} +F == {n1} +R == 1..5 +IsQuorum(Q) == Q \in {{n1,n3},{n2,n3},{n1,n2,n3}} +IsBlocking(B) == B \in {{n3},{n1,n3},{n2,n3},{n1,n2,n3}} +LeaderSchedule == <> +Leader(r) == LeaderSchedule[((r-1) % Cardinality(N))+1] +GST == 3 + +INSTANCE Sailfish + +(**************************************************************************************) +(* Next we define a constraint to stop the model-checker. *) +(**************************************************************************************) +StateConstraint == \A n \in N \ F : round[n] \in 0..Max(R) + +Done == \A n \in N \ F : round[n] = Max(R) +Terminate == Done /\ UNCHANGED <> +TerminatingSpec == Init /\ [][Next \/ Terminate]_<> + +(**************************************************************************************) +(* Finally, we give some properties we expect to be violated (useful to get the *) +(* model-checker to print interesting executions). *) +(**************************************************************************************) + +Falsy1 == \neg ( + \A n \in N \ F : round[n] = Max(R) +) + +Falsy2 == \neg ( + \E n \in N \ F : Len(log[n]) > 1 +) + +\* can be used to stop the model-checker when the leader vertex of round 2 is committed +Falsy3 == \neg ( + \E n \in N \ F : \E i \in DOMAIN log[n] : log[n][i] = <> +) + +=========================================================================== diff --git a/specifications/dag-consensus/TLCSailfish2.cfg b/specifications/dag-consensus/TLCSailfish2.cfg new file mode 100644 index 00000000..b029d477 --- /dev/null +++ b/specifications/dag-consensus/TLCSailfish2.cfg @@ -0,0 +1,13 @@ +SPECIFICATION TerminatingSpec + +CONSTANTS + n1 = n1 + n2 = n2 + n3 = n3 + n4 = n4 + +INVARIANT TypeOK +INVARIANT Agreement +INVARIANT Liveness + +CONSTRAINT StateConstraint diff --git a/specifications/dag-consensus/TLCSailfish2.tla b/specifications/dag-consensus/TLCSailfish2.tla new file mode 100644 index 00000000..24c64617 --- /dev/null +++ b/specifications/dag-consensus/TLCSailfish2.tla @@ -0,0 +1,33 @@ +----------------------------- MODULE TLCSailfish2 ----------------------------- + +(**************************************************************************************) +(* In this configuartion, we have 4 nodes among which one is Byzantine, every set *) +(* of 3 nodes (i.e. n-f nodes) is a quorum, and every set of 2 nodes (i.e. f+1 *) +(* nodes) is a blocking set. *) +(**************************************************************************************) + +EXTENDS Integers, FiniteSets + +VARIABLES vs, es, round, log + +CONSTANTS + n1,n2,n3,n4 + +N == {n1,n2,n3,n4} +F == {n1} +R == 1..5 +IsQuorum(Q) == Cardinality(Q) >= 3 +IsBlocking(B) == Cardinality(B) >= 2 +LeaderSchedule == <> +Leader(r) == LeaderSchedule[((r-1) % Cardinality(N))+1] +GST == 6 + +INSTANCE Sailfish + +StateConstraint == \A n \in N \ F : round[n] \in 0..Max(R) + +Done == \A n \in N \ F : round[n] = Max(R) +Terminate == Done /\ UNCHANGED <> +TerminatingSpec == Init /\ [][Next \/ Terminate]_<> + +=========================================================================== diff --git a/specifications/dag-consensus/Utils.tla b/specifications/dag-consensus/Utils.tla new file mode 100644 index 00000000..2596af59 --- /dev/null +++ b/specifications/dag-consensus/Utils.tla @@ -0,0 +1,8 @@ +------------- MODULE Utils --------------- + +EXTENDS Integers + +Max(S) == CHOOSE x \in S : \A y \in S : y <= x +Min(S) == CHOOSE x \in S : \A y \in S : x <= y + +========================================== diff --git a/specifications/dag-consensus/manifest.json b/specifications/dag-consensus/manifest.json new file mode 100644 index 00000000..ddbeb34e --- /dev/null +++ b/specifications/dag-consensus/manifest.json @@ -0,0 +1,68 @@ +{ + "sources": ["https://github.com/nano-o/dag-consensus"], + "authors": ["Giuliano Losa"], + "tags": [], + "modules": [ + { + "path": "specifications/dag-consensus/BlockDag.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/dag-consensus/BlockDagTest.tla", + "features": [], + "models": [ + { + "path": "specifications/dag-consensus/BlockDagTest.cfg", + "runtime": "00:00:10", + "mode": "exhaustive search", + "result": "success" + } + ] + }, + { + "path": "specifications/dag-consensus/Digraph.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/dag-consensus/Sailfish.tla", + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/dag-consensus/TLCSailfish1.tla", + "features": [], + "models": [ + { + "path": "specifications/dag-consensus/TLCSailfish1.cfg", + "runtime": "00:00:10", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 109604, + "totalStates": 314144, + "stateDepth": 16 + } + ] + }, + { + "path": "specifications/dag-consensus/TLCSailfish2.tla", + "features": [], + "models": [ + { + "path": "specifications/dag-consensus/TLCSailfish2.cfg", + "runtime": "unknown", + "mode": "exhaustive search", + "result": "success" + } + ] + }, + { + "path": "specifications/dag-consensus/Utils.tla", + "features": [], + "models": [] + } + ] +}