-
Notifications
You must be signed in to change notification settings - Fork 0
/
MC_ffg.tla
124 lines (101 loc) · 4.03 KB
/
MC_ffg.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
----------------------------- MODULE MC_ffg -----------------------------
EXTENDS FiniteSets
\* @type: Int;
MAX_BLOCK_SLOT == 5
\* @type: Set(Str);
BLOCK_BODIES == {"A", "B", "C", "D", "E"}
\* @type: Set(Str);
VALIDATORS == {"V1", "V2", "V3", "V4"}
N == 4
VARIABLES
\* @type: Set($block);
blocks,
\* @type: Set(<<$block,$block>>);
block_graph,
\* @type: Set(<<$block, $block>>);
block_graph_closure,
\* @type: Set($ffgVote);
ffg_votes,
\* @type: Set($vote);
votes,
\* @type: Set($checkpoint);
justified_checkpoints
INSTANCE ffg
ExistsJustifiedNonGenesisInv == Cardinality(justified_checkpoints) <= 1
ExistTwoFinalizedConflictingBlocks ==
LET disagreement == \E c1, c2 \in justified_checkpoints:
/\ IsFinalized(c1, votes, justified_checkpoints)
/\ IsFinalized(c2, votes, justified_checkpoints)
/\ AreConflictingBlocks(c1[1], c2[1])
IN ~disagreement
AccountableSafety ==
LET disagreement == \E c1, c2 \in justified_checkpoints:
/\ IsFinalized(c1, votes, justified_checkpoints)
/\ IsFinalized(c2, votes, justified_checkpoints)
/\ AreConflictingBlocks(c1[1], c2[1])
IN ~disagreement \/ Cardinality(SlashableNodes) * 3 >= N
Inv == ExistTwoFinalizedConflictingBlocks
\* `block_graph` forms a tree. Assumes RealClosureInv for brevity (to be used in conjunction)
GraphIsTreeInv ==
/\ \A <<child, parent>> \in block_graph: \A <<ochild, oparent>> \in block_graph:
\* 1 parent per child
child = ochild => parent = oparent
\* No cycles (RealClosureInv assumed for the formulation below)
/\ \A block1, block2 \in blocks:
\/ block1 = block2
\/ <<block1,block2>> \notin block_graph_closure
\/ <<block2,block1>> \notin block_graph_closure
\* Tree, not forest
/\ \A block \in blocks: <<block, GenesisBlock>> \in block_graph_closure
GraphWellFormedInv ==
/\ \A block \in blocks: IsValidBlock(block)
/\ \A <<child, parent>> \in block_graph:
/\ child \in blocks
/\ parent \in blocks
/\ child.slot > parent.slot
\* `block_graph_closure` is the closure of the relation `block_graph`
RealClosureInv ==
\* MUST contain
\* Would be trivially true for block_graph_closure = blocks^2
/\ \A block \in blocks: <<block, block>> \in block_graph_closure
/\ block_graph \subseteq block_graph_closure
/\ \A <<descendant, midpoint1>> \in block_graph_closure: \A <<midpoint2, ancestor>> \in block_graph_closure:
midpoint1 = midpoint2 => <<descendant, ancestor>> \in block_graph_closure
\* MAY contain
\* Would be trivially true for block_graph_closure = {}
/\ \A <<descendant, ancestor>> \in block_graph_closure:
\/ descendant = ancestor
\/ <<descendant, ancestor>> \in block_graph
\/ \E block \in blocks:
/\ <<descendant, block>> \in block_graph
/\ <<block, ancestor>> \in block_graph_closure
GraphInv ==
/\ GraphIsTreeInv
/\ GraphWellFormedInv
/\ RealClosureInv
JustifiedCheckpointsInv ==
/\ \A c \in justified_checkpoints:
/\ IsValidCheckpoint(c)
/\ IsJustified(c, votes, justified_checkpoints)
/\ LET allCheckpoints == {Checkpoint(block, i): block \in blocks, i \in CheckpointSlots}
IN \A c \in (allCheckpoints \ justified_checkpoints): ~IsJustified(c, votes, justified_checkpoints)
VotesWellFormedInv ==
/\ \A ffgVote \in ffg_votes: IsValidFFGVote(ffgVote)
/\ \A vote \in votes:
/\ vote.ffg_vote \in ffg_votes
/\ vote.validator \in VALIDATORS
VoteAndCheckpointInv ==
/\ JustifiedCheckpointsInv
/\ VotesWellFormedInv
InductiveInv == GraphInv /\ VoteAndCheckpointInv
Init0 ==
/\ ffg_votes = Gen(5)
/\ votes = Gen(5)
/\ justified_checkpoints = Gen(5)
/\ blocks = Gen(MAX_BLOCK_SLOT)
/\ block_graph = Gen(MAX_BLOCK_SLOT)
/\ block_graph_closure = Gen(MAX_BLOCK_SLOT * MAX_BLOCK_SLOT)
/\ InductiveInv
Next0 == Next
Inv0 == InductiveInv
=============================================================================