-
Notifications
You must be signed in to change notification settings - Fork 14
/
StateTransition.dfy
434 lines (389 loc) · 18.1 KB
/
StateTransition.dfy
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
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
/*
* Copyright 2020 ConsenSys AG.
*
* Licensed under the Apache License, Version 2.0 (the "License"); you may
* not use this file except in compliance with the License. You may obtain
* a copy of the License at http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software dis-
* tributed under the License is distributed on an "AS IS" BASIS, WITHOUT
* WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
* License for the specific language governing permissions and limitations
* under the License.
*/
include "../utils/Eth2Types.dfy"
include "../utils/Helpers.dfy"
include "../ssz/Constants.dfy"
include "BeaconChain.dfy"
/**
* State transition function for the Beacon Chain.
*/
module StateTransition {
// Import some constants and types
import opened Eth2Types
import opened Constants
import opened BeaconChain
import opened Helpers
/** The default zeroed Bytes32. */
const SEQ_EMPTY_32_BYTES := timeSeq<byte>(0,32)
/**
* The default (empty) Bytes32
*/
const EMPTY_BYTES32 : Bytes32 := Bytes(SEQ_EMPTY_32_BYTES)
/** The historical roots type. */
const EMPTY_HIST_ROOTS := timeSeq<Bytes32>(EMPTY_BYTES32, SLOTS_PER_HISTORICAL_ROOT as int)
type VectorOfHistRoots = x : seq<Bytes32> | |x| == SLOTS_PER_HISTORICAL_ROOT as int
witness EMPTY_HIST_ROOTS
/**
* Compute Root/Hash/Bytes32 for different types.
*
* @todo Use the hash_tree_root from Merkle.
*/
function method hash_tree_root<T(==)>(t : T) : Bytes32
ensures hash_tree_root(t) != EMPTY_BYTES32
/** Collision free hash function.
* This does not seem to affect the proofs so far, so
* this lemma is commented out.
**/
// lemma {:axiom} foo<T(==)>(t1: T, t2: T)
// ensures t1 == t2 <==> hash_tree_root(t1) == hash_tree_root(t2)
/**
* @link{https://notes.ethereum.org/@djrtwo/Bkn3zpwxB?type=view}
* The beacon chain’s state (BeaconState) is the core object around
* which the specification is built. The BeaconState encapsulates
* all of the information pertaining to:
* - who the validators are,
* - in what state each of them is in,
* - which chain in the block tree this state belongs to, and
* - a hash-reference to the Ethereum 1 chain.
* Beginning with the genesis state, the post state of a block is
* considered valid if it passes all of the guards within the state
* transition function. Thus, the precondition of a block is
* recursively defined as being a valid postcondition of running
* the state transition function on the previous block and its state
* all the way back to the genesis state.
*
* @param slot Time is divided into “slots” of fixed length
* at which actions occur and state transitions
* happen. This field tracks the slot of the
* containing state, not necessarily the slot
* according to the local wall clock
* @param latest_block_header The latest block header seen in the chain
* defining this state. This blockheader has
* During the slot transition
* of the block, the header is stored without the
* real state root but instead with a stub of Root
* () (empty 0x00 bytes). At the start of the next
* slot transition before anything has been
* modified within state, the state root is
* calculated and added to the
* latest_block_header. This is done to eliminate
* the circular dependency of the state root
* being embedded in the block header
* @param block_roots Per-slot store of the recent block roots.
* The block root for a slot is added at the start
* of the next slot to avoid the circular
* dependency due to the state root being embedded
* in the block. For slots that are skipped (no
* block in the chain for the given slot), the
* most recent block root in the chain prior to
* the current slot is stored for the skipped
* slot. When validators attest to a given slot,
* they use this store of block roots as an
* information source to cast their vote.
* @param state_roots Per-slot store of the recent state roots.
* The state root for a slot is stored at the
* start of the next slot to avoid a circular
* dependency
*/
datatype BeaconState = BeaconState(
slot: Slot,
latest_block_header: BeaconBlockHeader,
block_roots: VectorOfHistRoots,
state_roots: VectorOfHistRoots
)
/**
* Whether a block is valid in a given state.
*
* @param s A beacon state.
* @param b A block.
*
* @returns true iff `b` can be successfully added to the state `s`.
*/
predicate isValid(s : BeaconState, b : BeaconBlockHeader)
{
s.slot < b.slot
// Fast forward s to b.slot and check `b` can be attached to the
// resulting state's latest_block_header.
&& b.parent_root ==
hash_tree_root(
forwardStateToSlot(resolveStateRoot(s),
b.slot
).latest_block_header)
&& b.state_root == hash_tree_root(
addBlockToState(
forwardStateToSlot(resolveStateRoot(s), b.slot),
b
)
)
}
/**
* Compute the state obtained after adding a block.
*/
method stateTransition(s: BeaconState, b: BeaconBlockHeader) returns (s' : BeaconState)
// make sure the last state was one right after addition of new block
requires isValid(s, b)
/** The next state latest_block_header is same as b except for state_root that is 0. */
ensures s'.latest_block_header == b.(state_root := EMPTY_BYTES32)
/** s' slot is now adjusted to the slot of b. */
ensures s'.slot == b.slot
/** s' parent_root is the hash of the state obtained by resolving/forwarding s to
the slot of b. */
ensures s'.latest_block_header.parent_root ==
hash_tree_root(
forwardStateToSlot(resolveStateRoot(s), b.slot)
.latest_block_header
)
{
// finalise slots before b.slot.
var s1 := processSlots(s, b.slot);
// Process block and compute the new state.
s' := processBlock(s1, b);
// Verify state root (from eth2.0 specs)
// A proof that this assert statement is never violated when isValid() is true.
// if validate_result:
assert (b.state_root == hash_tree_root(s'));
}
/**
* Advance current state to a given slot.
*
* This mainly consists in advancing the slot number to
* a target future `slot` number and updating/recording the history of intermediate
* states (and block headers).
* Under normal circumstances, where a block is received at each slot,
* this involves only one iteration of the loop.
* Otherwise, the first iteration of the loop `finalises` the block header
* of the previous slot before recortding it,
* and subsequent rounds advance the slot number and record the history of states
* and blocks for each slot.
*
* @param s A state
* @param slot The slot to advance to. This is usually the slot of newly
* proposed block.
* @returns The state obtained after advancing the history to slot.
*
* @note The specs have the the first processSlot integrated
* in the while loop. However, because s.slot < slot,
* the while bdoy must be executed at least one time.
* To simplify the proof, we have taken this first iteration
* outside of the loop. It does not change the semantics
* but enables us to use the state obtained after the first
* iteration the loop and prove it is the same as
* resolveStateRoot(s);
*
*/
method processSlots(s: BeaconState, slot: Slot) returns (s' : BeaconState)
requires s.slot < slot // update in 0.12.0 (was <= before)
ensures s' == forwardStateToSlot( resolveStateRoot(s), slot)
ensures s.latest_block_header.parent_root == s'.latest_block_header.parent_root
// Termination ranking function
decreases slot - s.slot
{
// Start from the current state and update it with processSlot.
// First iteration of the loop in process_slots (Eth2)
s' := processSlot(s);
s':= s'.(slot := s'.slot + 1) ;
// The following asserts are not needed for the proof but provided for readability.
assert(s' == resolveStateRoot(s));
// s'.block header state_root should now be resolved
assert(s'.latest_block_header.state_root != EMPTY_BYTES32);
// Now fast forward to slot
// Next iterations of process_slot (Eth2)
while (s'.slot < slot)
invariant s'.slot <= slot
invariant s'.latest_block_header.state_root != EMPTY_BYTES32
invariant s' == forwardStateToSlot(resolveStateRoot(s), s'.slot) // Inv1
decreases slot - s'.slot
{
s':= processSlot(s');
// s'.slot is now processed: history updated and block header resolved
// The state's slot is processed and we can advance to the next slot.
s':= s'.(slot := s'.slot + 1) ;
}
}
/**
* Cache data for a slot.
*
* This function also finalises the block header of the last block
* so that it records the hash of the state `s`.
*
* @param s A state.
* @returns A new state where `s` has been added/cached to the history and
* the block header tracks the hash of the most recent received
* block.
*
* @note This function method could be a method (as per the Eth2 specs).
* However, this requires to expose the properties of the computation
* as methods are not inlined.
* @note Matches eth2.0 specs, need to uncomment update of state/block_roots.
*
* @todo Make this a method to have a def closer to Eth2 implementation.
*/
method processSlot(s: BeaconState) returns (s' : BeaconState)
requires s.slot as nat + 1 < 0x10000000000000000 as nat
ensures s.latest_block_header.state_root == EMPTY_BYTES32 ==>
s' == resolveStateRoot(s).(slot := s.slot)
ensures s.latest_block_header.state_root != EMPTY_BYTES32 ==>
s' == nextSlot(s).(slot := s.slot)
ensures s.latest_block_header.parent_root == s'.latest_block_header.parent_root
{
s' := s;
// Cache state root
// Record the hash of the previous state in the history.
var previous_state_root := hash_tree_root(s);
s' := s'.(state_roots := s'.state_roots[(s'.slot % SLOTS_PER_HISTORICAL_ROOT) as int := previous_state_root]);
// Cache latest block header state root
if (s'.latest_block_header.state_root == EMPTY_BYTES32) {
s' := s'.(latest_block_header := s'.latest_block_header.(state_root := previous_state_root));
}
// Cache block root
var previous_block_root := hash_tree_root(s'.latest_block_header);
s' := s'.(block_roots := s'.block_roots[(s.slot % SLOTS_PER_HISTORICAL_ROOT) as int := previous_block_root]);
}
/**
* Verify that a block is valid.
*
* @note Matches eth2.0 specs, need to implement randao, eth1, operations.
*/
method processBlock(s: BeaconState, b: BeaconBlockHeader) returns (s' : BeaconState)
requires b.slot == s.slot
requires b.parent_root == hash_tree_root(s.latest_block_header)
ensures s' == addBlockToState(s, b)
{
// Start by creating a block header from the ther actual block.
s' := processBlockHeader(s, b);
// process_randao(s, b.body)
// process_eth1_data(s, b.body)
// process_operations(s, b.body)
}
/**
* Check whether a block is valid and prepare and initialise new state
* with a corresponding block header.
*
* @note Matches eth2.0 specs except proposer slashing verification
*/
method processBlockHeader(s: BeaconState, b: BeaconBlockHeader) returns (s' : BeaconState)
// Verify that the slots match
requires b.slot == s.slot
// Verify that the parent matches
requires b.parent_root == hash_tree_root(s.latest_block_header)
ensures s' == addBlockToState(s, b)
{
s':= s.(
latest_block_header := BeaconBlockHeader(
b.slot,
b.parent_root,
EMPTY_BYTES32
)
);
}
// Specifications of finalisation of a state and forward to future slot.
/**
* Result of processing a block.
*
* @param s A state.
* @param b A block to add to the state `s`.
* @returns The state `s` updated to point to `b` with state_root set to 0.
*/
function addBlockToState(s: BeaconState, b: BeaconBlockHeader) : BeaconState
// Verify that the slots match
requires b.slot == s.slot
// Verify that the parent matches
requires b.parent_root == hash_tree_root(s.latest_block_header)
{
s.(
latest_block_header := BeaconBlockHeader(
b.slot,
b.parent_root,
EMPTY_BYTES32
)
)
}
/**
* Complete the current slot.
*
* @param s A beacon state.
* @returns A new state `s' such that:
* 1. a new latest_block_header' state_root set to the hash_tree_root(s)
* 2. the hash_tree_root(s) archived in the s'.state_roots for the slot
* 3. the hash_tree_root of the new_block_header is archived
* in s'.block_roots
*/
function resolveStateRoot(s: BeaconState): BeaconState
// Make sure s.slot does not overflow
requires s.slot as nat + 1 < 0x10000000000000000 as nat
// parent_root of the state block header is preserved
ensures s.latest_block_header.parent_root == resolveStateRoot(s).latest_block_header.parent_root
{
var new_latest_block_header :=
if (s.latest_block_header.state_root == EMPTY_BYTES32 ) then
s.latest_block_header.(state_root := hash_tree_root(s))
else
s.latest_block_header
;
BeaconState(
// slot unchanged
s.slot + 1,
new_latest_block_header,
// add new block_header root to block_roots history.
s.block_roots[(s.slot % SLOTS_PER_HISTORICAL_ROOT) as int := hash_tree_root(new_latest_block_header)],
// add previous state root to state_roots history
s.state_roots[(s.slot % SLOTS_PER_HISTORICAL_ROOT) as int := hash_tree_root(s)]
)
}
/**
* Finalise a state and forward to slot in the future.
*
* @param s A state
* @param slot A slot.
* @returns A new state obtained by archiving roots and incrementing slot.
* slot.
*/
function forwardStateToSlot(s: BeaconState, slot: Slot) : BeaconState
requires s.slot <= slot
ensures forwardStateToSlot(s, slot).slot == slot
ensures forwardStateToSlot(s, slot).latest_block_header == s.latest_block_header
// termination ranking function
decreases slot - s.slot
{
if (s.slot == slot) then
s
else
nextSlot(forwardStateToSlot(s, slot - 1))
}
/**
* Advance a state by one slot.
*
* @param s A beacon state.
* @returns The successor state for `slot + 1`.
*
* @note This function increment the slot number and archives
* the previous state_root and block_root, and copy verbatim the
* latest_block_header.
*/
function nextSlot(s : BeaconState) : BeaconState
// Make sure s.slot does not overflow
requires s.slot as nat + 1 < 0x10000000000000000 as nat
{
// Add header root to history of block_roots
var new_block_roots := s.block_roots[(s.slot % SLOTS_PER_HISTORICAL_ROOT) as int := hash_tree_root(s.latest_block_header)];
// Add state root to history of state roots
var new_state_roots := s.state_roots[(s.slot % SLOTS_PER_HISTORICAL_ROOT) as int := hash_tree_root(s)];
// Increment slot and copy latest_block_header
s.(
slot := s.slot + 1,
block_roots := new_block_roots,
state_roots := new_state_roots
)
}
}