-
Notifications
You must be signed in to change notification settings - Fork 0
/
MC_ffg.tla
223 lines (190 loc) · 9.56 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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
----------------------------- MODULE MC_ffg -----------------------------
(*
* Main TLA+ module for model-checking with Apalache
*
* Jure Kukovec, 2024.
*
* Subject to Apache 2.0. See `LICENSE.md`.
*)
EXTENDS FiniteSets
Nodes == { "A", "B", "C", "D" }
\* Model-checking: Maximum slot (inclusive) that Apalache folds over when traversing ancestors.
\* Let `genesis <- b1 <- ... <- bn` be the longest chain from genesis in `view_votes`. Then `MAX_SLOT` MUST be at least `n`.
MAX_SLOT == 4
\* Model-checking: Maximum number of votes in `view_votes`.
MAX_VOTES == 12
\* ========== Dummy implementations of stubs ==========
\* SRC: https://github.com/saltiniroberto/ssf/blob/7ea6e18093d9da3154b4e396dd435549f687e6b9/high_level/common/stubs.pyi#L6
\*
\* Model-checking: We assume the block_body type is the string (hash) already.
\*
\* @type: ($block) => $hash;
BLOCK_HASH(b) == b.body
\* SRC: https://github.com/saltiniroberto/ssf/blob/7ea6e18093d9da3154b4e396dd435549f687e6b9/high_level/common/stubs.pyi#L9
\*
\* Model-checking: We assume that all vote signatures are valid.
\*
\* @type: ($signedVoteMessage) => Bool;
VERIFY_VOTE_SIGNATURE(vote) == TRUE
\* SRC: https://github.com/saltiniroberto/ssf/blob/7ea6e18093d9da3154b4e396dd435549f687e6b9/high_level/common/stubs.pyi#L18
\*
\* Stake associated with each validator in a given slot.
\*
\* Model-checking: We assume uniform voting power.
\*
\* @type: ($block, Int, $commonNodeState) => $validatorBalances;
GET_VALIDATOR_SET_FOR_SLOT(block, slot, node_state) == [node \in Nodes |-> 100]
\* ====================================================
VARIABLES
\* @type: $commonNodeState;
single_node_state,
\* A precomputed map from (descendant) blocks to their ancestors.
\* @type: $block -> Set($block);
PRECOMPUTED__IS_ANCESTOR_DESCENDANT_RELATIONSHIP,
\* A precomputed set of all justified checkpoints.
\* @type: Set($checkpoint);
PRECOMPUTED__IS_JUSTIFIED_CHECKPOINT
INSTANCE ffg WITH
MAX_SLOT <- MAX_SLOT,
BLOCK_HASH <- BLOCK_HASH,
VERIFY_VOTE_SIGNATURE <- VERIFY_VOTE_SIGNATURE,
GET_VALIDATOR_SET_FOR_SLOT <- GET_VALIDATOR_SET_FOR_SLOT
\* ========== Shape-requirements for state-variable fields ==========
\* Readable names for block hashes (introduced as fresh constants by Apalache). `BlockHashes` must satisfy |BlockHashes| >= |DOMAIN view_blocks|
BlockHashes == { BLOCK_HASH(GenesisBlock), "BLOCK1", "BLOCK2", "BLOCK3", "BLOCK4", "BLOCK5", "BLOCK6", "BLOCK7", "BLOCK8", "BLOCK9", "BLOCK10" }
\* @type: ($checkpoint, $commonNodeState) => Bool;
IsValidCheckpoint(c, node_state) ==
/\ c.block_hash \in DOMAIN node_state.view_blocks
/\ \/ c = genesis_checkpoint(node_state)
\/ \* Section 3.Checkpoints: "Importantly, the slot c for the checkpoint occurs after the slot B.p where the block was proposed"
/\ c.block_slot >= 0
/\ c.chkp_slot > c.block_slot
/\ c.chkp_slot <= MAX_SLOT
\* @type: ($voteMessage, $commonNodeState) => Bool;
IsValidVoteMessage(msg, node_state) ==
/\ msg.slot >= 0
/\ msg.slot <= MAX_SLOT
\* A message can only reference checkpoints that have already happened
\* QUESTION TO REVIEWERS: strict > ?
/\ msg.slot >= msg.ffg_source.chkp_slot
/\ msg.slot >= msg.ffg_target.chkp_slot
/\ IsValidCheckpoint(msg.ffg_source, node_state)
/\ IsValidCheckpoint(msg.ffg_target, node_state)
\* Section 3.Votes: "... C1 and C2 are checkpoints with C1.c < C2.c and C1.B <- C2.B"
/\ msg.ffg_source.chkp_slot < msg.ffg_target.chkp_slot
\* TODO: MAJOR source of slowdown as MAX_SLOT increases, investigate further
/\ PRECOMPUTED__is_ancestor_descendant_relationship(
get_block_from_hash(msg.ffg_source.block_hash, node_state),
get_block_from_hash(msg.ffg_target.block_hash, node_state),
node_state
)
\* @type: ($signedVoteMessage, $commonNodeState) => Bool;
IsValidSigedVoteMessage(msg, node_state) ==
/\ IsValidVoteMessage(msg.message, node_state)
/\ VERIFY_VOTE_SIGNATURE(msg)
/\ msg.sender \in Nodes
\* @type: ($block, $commonNodeState) => Bool;
IsValidBlock(block, node_state) ==
/\ block.parent_hash \in (DOMAIN node_state.view_blocks \union { GenesisBlock.parent_hash })
/\ block.slot >= 0
/\ block.slot <= MAX_SLOT
/\ \A voteMsg \in block.votes: IsValidSigedVoteMessage(voteMsg, node_state)
/\ LET parent == get_block_from_hash(block.parent_hash, node_state)
IN parent.slot < block.slot \* Parent has lower slot #
/\ block.body /= ""
\* @type: ($proposeMessage, $commonNodeState) => Bool;
IsValidProposeMessage(msg, node_state) ==
/\ IsValidBlock(msg.block, node_state)
/\ \A i \in Indices(msg.proposer_view): IsValidSigedVoteMessage(At(msg.proposer_view, i), node_state)
\* @type: ($signedProposeMessage, $commonNodeState) => Bool;
IsValidSignedProposeMessage(msg, node_state) ==
/\ IsValidProposeMessage(msg.message, node_state)
\* there's no equivalent to verify_vote_signature for propose messages
\* QUESTION TO REVIEWERS: strict > ?
\* @type: ($configuration, $commonNodeState) => Bool;
IsValidConfiguration(cfg, node_state) ==
/\ cfg.delta >= 0
/\ cfg.genesis = GenesisBlock
/\ cfg.eta >= 1
/\ cfg.k >= 0
\* @type: ($hash -> $block, $commonNodeState) => Bool;
IsValidBlockView(view_blocks, node_state) ==
\* Assign readable names to block hashes introduced as fresh constants by Apalache
/\ DOMAIN node_state.view_blocks \subseteq BlockHashes
\* The genesis block is always in the block view, it's parent hash never
/\ BLOCK_HASH(GenesisBlock) \in DOMAIN view_blocks
/\ view_blocks[BLOCK_HASH(GenesisBlock)] = GenesisBlock
/\ GenesisBlock.parent_hash \notin DOMAIN view_blocks
\* Each block must have a unique hash: H(B1) = H(B2) <=> B1 = B2
/\ \A hash1,hash2 \in DOMAIN view_blocks:
hash1 = hash2 <=> view_blocks[hash1] = view_blocks[hash2]
\* @type: ($commonNodeState) => Bool;
IsValidNodeState(node_state) ==
/\ IsValidConfiguration(node_state.configuration, node_state)
/\ node_state.identity \in Nodes
/\ node_state.current_slot >= 0
/\ node_state.current_slot <= MAX_SLOT
/\ IsValidBlockView(node_state.view_blocks, node_state)
/\ \A msg \in node_state.view_votes: IsValidSigedVoteMessage(msg, node_state)
/\ IsValidBlock(node_state.chava, node_state)
\* ==================================================================
\* State machine
\* ==================================================================
\* The following variables encode precomputed sets, to avoid emitting nested folds
Precompute ==
LET all_blocks == get_all_blocks(single_node_state) IN
/\ PRECOMPUTED__IS_ANCESTOR_DESCENDANT_RELATIONSHIP =
[ descendant \in all_blocks |-> {
ancestor \in all_blocks:
is_ancestor_descendant_relationship(ancestor, descendant, single_node_state)
}]
/\ LET initialTargetMap == [
checkpoint \in get_set_FFG_targets(single_node_state.view_votes) |->
VotesInSupportAssumingJustifiedSource(checkpoint, single_node_state)
]
IN PRECOMPUTED__IS_JUSTIFIED_CHECKPOINT =
AllJustifiedCheckpoints(initialTargetMap, single_node_state, MAX_SLOT)
\* Start in some arbitrary state
Init ==
LET
config == Gen(1)
id == Gen(1)
current_slot == MAX_SLOT
view_blocks == Gen(MAX_SLOT + 1) \* MAX_SLOT "regular" blocks + 1 for genesis (at slot 0)
view_votes == Gen(MAX_VOTES)
chava == Gen(1)
IN
/\ single_node_state = [ configuration |-> config, identity |-> id, current_slot |-> current_slot, view_blocks |-> view_blocks, view_votes |-> view_votes, chava |-> chava ]
/\ Precompute
/\ IsValidNodeState(single_node_state)
Next == UNCHANGED <<single_node_state, PRECOMPUTED__IS_ANCESTOR_DESCENDANT_RELATIONSHIP, PRECOMPUTED__IS_JUSTIFIED_CHECKPOINT>>
\* ==================================================================
\* Invariants
\* ==================================================================
\* Consistency checks on parameters
ConsistentParameters == Cardinality(BlockHashes) >= Cardinality(DOMAIN single_node_state.view_blocks)
\* Theorem 1 (Accountable safety). The finalized chain chFin_i is accountably safe, i.e.,
\* two conflicting finalized blocks imply that at least n/3 adversarial validators can be
\* detected to have violated either [slashing condition] E1 or E2.
AccountableSafety ==
LET finalized_checkpoints == get_finalized_checkpoints(single_node_state)
finalized_blocks == {
get_block_from_hash(checkpoint.block_hash, single_node_state):
checkpoint \in finalized_checkpoints
}
there_are_conflicting_finalized_blocks ==
\E block1, block2 \in finalized_blocks:
are_conflicting(block1, block2, single_node_state)
slashable_nodes == get_slashable_nodes(single_node_state.view_votes)
IN there_are_conflicting_finalized_blocks =>
(Cardinality(slashable_nodes) * 3 >= Cardinality(Nodes))
Inv ==
/\ ConsistentParameters
/\ AccountableSafety
\* The ebb-and-flow protocol property stipulates that at every step, two chains are maintained,
\* the finalized chain, which is safe, and the available chain, which is live, s.t. the finalized
\* chain is a prefix of the available chain.
FinalizedChainIsPrefixOfAvailableChain ==
LET lastFinBLock == get_block_from_hash(get_greatest_finalized_checkpoint(single_node_state).block_hash, single_node_state)
IN is_ancestor_descendant_relationship(lastFinBLock, single_node_state.chava, single_node_state)
=============================================================================