|
| 1 | +----------------------------- MODULE BlockDag ----------------------------- |
| 2 | + |
| 3 | +(**************************************************************************************) |
| 4 | +(* In this specification we define notions on DAGs useful for DAG-based consensus *) |
| 5 | +(* protocols (which build DAGs of blocks) *) |
| 6 | +(**************************************************************************************) |
| 7 | + |
| 8 | +EXTENDS FiniteSets, Sequences, Integers, Utils, Digraph, TLC |
| 9 | + |
| 10 | +CONSTANTS |
| 11 | + N \* The set of all network nodes (not DAG nodes) |
| 12 | +, R \* The set of rounds |
| 13 | +, Leader(_) \* operator mapping each round to its leader |
| 14 | + |
| 15 | +(**************************************************************************************) |
| 16 | +(* For our purpose of checking safety and liveness, DAG vertices just consist of a *) |
| 17 | +(* node and a round. *) |
| 18 | +(**************************************************************************************) |
| 19 | +V == N \times R \* the set of possible DAG vertices |
| 20 | +Node(v) == v[1] |
| 21 | +Round(v) == IF v = <<>> THEN 0 ELSE v[2] \* accomodates <<>> as default value |
| 22 | + |
| 23 | +(**************************************************************************************) |
| 24 | +(* Next we define leader vertices: *) |
| 25 | +(**************************************************************************************) |
| 26 | +LeaderVertex(r) == IF r > 0 THEN <<Leader(r), r>> ELSE <<>> |
| 27 | +IsLeader(v) == LeaderVertex(Round(v)) = v |
| 28 | +Genesis == <<>> |
| 29 | +ASSUME IsLeader(Genesis) \* this should hold |
| 30 | + |
| 31 | +(**************************************************************************************) |
| 32 | +(* OrderSet(S) arbitrarily order the members of the set S. Note that, in TLA+, *) |
| 33 | +(* `CHOOSE' is deterministic but arbitrary choice, i.e. `CHOOSE e \in S : TRUE' is *) |
| 34 | +(* always the same `e' if `S' is the same *) |
| 35 | +(**************************************************************************************) |
| 36 | +RECURSIVE OrderSet(_) |
| 37 | +OrderSet(S) == IF S = {} THEN <<>> ELSE |
| 38 | + LET e == CHOOSE e \in S : TRUE |
| 39 | + IN Append(OrderSet(S \ {e}), e) |
| 40 | + |
| 41 | +(**************************************************************************************) |
| 42 | +(* PreviousLeader(dag, r) returns the leader vertex in dag whose round is the *) |
| 43 | +(* largest but smaller than r. We assume that dag contains at least the genesis *) |
| 44 | +(* vertex. *) |
| 45 | +(**************************************************************************************) |
| 46 | +PreviousLeader(dag, r) == CHOOSE l \in Vertices(dag) : |
| 47 | + /\ IsLeader(l) |
| 48 | + /\ Round(l) = Max({Round(l2) : l2 \in |
| 49 | + {l2 \in Vertices(dag) : IsLeader(l2) /\ Round(l2) < r}}) |
| 50 | + |
| 51 | +(**************************************************************************************) |
| 52 | +(* Linearize a DAG. In a real blockchain we should use a topological ordering, but, *) |
| 53 | +(* for the purpose of ensuring agreement, an arbitrary ordering (as provided by *) |
| 54 | +(* OrderSet) is fine. This assume a DAG where all paths end with the Genesis *) |
| 55 | +(* vertex. *) |
| 56 | +(**************************************************************************************) |
| 57 | +RECURSIVE Linearize(_, _) |
| 58 | +Linearize(dag, l) == IF Vertices(dag) = {<<>>} THEN <<>> ELSE |
| 59 | + LET dagOfL == SubDag(dag, {l}) |
| 60 | + prevL == PreviousLeader(dagOfL, Round(l)) |
| 61 | + dagOfPrev == SubDag(dag, {prevL}) |
| 62 | + remaining == Vertices(dagOfL) \ Vertices(dagOfPrev) |
| 63 | + IN Linearize(dagOfPrev, prevL) \o OrderSet(remaining \ {l}) \o <<l>> |
| 64 | + |
| 65 | +Compatible(s1, s2) == \* whether the sequence s1 is a prefix of the sequence s2, or vice versa |
| 66 | + \A i \in 1..Min({Len(s1), Len(s2)}) : s1[i] = s2[i] |
| 67 | +========================================================================= |
0 commit comments