From 4c762f7b75a737716bcfcd50c0e3d2a7eed79fba Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Mon, 19 Jan 2026 08:37:35 -0800 Subject: [PATCH 1/2] microwave spec: fix link in table Signed-off-by: Giuliano Losa --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 8aa16616..657ae5a5 100644 --- a/README.md +++ b/README.md @@ -151,7 +151,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 From 4134be00fe91258f67fba606591467b2945fba7b Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Mon, 19 Jan 2026 08:41:09 -0800 Subject: [PATCH 2/2] add dag-consensus Signed-off-by: Giuliano Losa --- README.md | 1 + specifications/dag-consensus/BlockDag.tla | 67 ++++++ specifications/dag-consensus/BlockDagTest.cfg | 0 specifications/dag-consensus/BlockDagTest.tla | 50 +++++ specifications/dag-consensus/Digraph.tla | 35 +++ specifications/dag-consensus/README.md | 23 ++ specifications/dag-consensus/Sailfish.tla | 200 ++++++++++++++++++ specifications/dag-consensus/TLCSailfish1.cfg | 13 ++ specifications/dag-consensus/TLCSailfish1.tla | 56 +++++ specifications/dag-consensus/TLCSailfish2.cfg | 13 ++ specifications/dag-consensus/TLCSailfish2.tla | 33 +++ specifications/dag-consensus/Utils.tla | 8 + specifications/dag-consensus/manifest.json | 68 ++++++ 13 files changed, 567 insertions(+) create mode 100644 specifications/dag-consensus/BlockDag.tla create mode 100644 specifications/dag-consensus/BlockDagTest.cfg create mode 100644 specifications/dag-consensus/BlockDagTest.tla create mode 100644 specifications/dag-consensus/Digraph.tla create mode 100644 specifications/dag-consensus/README.md create mode 100644 specifications/dag-consensus/Sailfish.tla create mode 100644 specifications/dag-consensus/TLCSailfish1.cfg create mode 100644 specifications/dag-consensus/TLCSailfish1.tla create mode 100644 specifications/dag-consensus/TLCSailfish2.cfg create mode 100644 specifications/dag-consensus/TLCSailfish2.tla create mode 100644 specifications/dag-consensus/Utils.tla create mode 100644 specifications/dag-consensus/manifest.json diff --git a/README.md b/README.md index 657ae5a5..2241260d 100644 --- a/README.md +++ b/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 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": [] + } + ] +}