QBFT Blockchain Consensus Protocol Specification v1

EEA Specification

This Version
https://entethalliance.org/specs/qbft/v1/
Latest Release Version
https://entethalliance.org/specs/qbft/
Latest editor's draft:
https://entethalliance.github.io/client-spec/qbft_spec.html
Author:
(ConsenSys)

Copyright © 2021-2023 Enterprise Ethereum Alliance.

Abstract

This document provides the specification of the Byzantine-fault-tolerant (BFT) blockchain consensus protocol QBFT. QBFT provides the following features:

Status of This Document

This section describes the status of this document at the time of its publication. Newer documents may supersede this document.

This Specification is copyright © 2021-2023 Enterprise Ethereum Alliance Incorporated (EEA). It is made available under the terms of the Apache License version 2.0. [Apache2], and unless required by applicable law or agreed to in writing, this specification is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

This the QBFT Blockchain Consensus Algorithm Specification version 1. This version of the specification does not address at least the following issues:

Please send any comments to the EEA at https://entethalliance.org/contact/.

1. Specification

The specification of QBFT is written using the verification-aware language [Dafny] and comprises the following files: 1.1 node.dfy, 1.2 node_auxiliary_functions.dfy, 1.3 types.dfy and 1.4 lemmas.dfy.

Overall, the specification is constructed following the [TLA]-style approach of using boolean-valued functions (predicates) over old and new states to specify state transition systems, and it uses existential quantifiers to hide the variables that should not appear in the final specification. Specifically,

1.1 node.dfy

This file is the main corpus of the QBFT specification and it includes the following items:

Download this as Dafny

1
/**
2
 * Copyright © 2021 EEA Inc. 
3
 *
4
 * This document is available under the terms of the Apache 2.0 License
5
 * (http://www.apache.org/licenses/LICENSE-2.0.html)
6
 */
7
include "types.dfy"
8
include "node_auxiliary_functions.dfy"
9
include "lemmas.dfy"
10
 
11
module L1_Spec
12
{
13
    import opened L1_SpecTypes
14
    import opened L1_AuxiliaryFunctionsAndLemmas
15
    import opened L1_Lemmas     
16
 
17
 
18
    /** =======================================================================
19
     * QBFT SPECIFICATION
20
     ========================================================================*/      
21
    /**
22
     *
23
     * This function provides the overall specification of the QBFT protocol.
24
     *
25
     * @param configuration The system configuration
26
     * @param id The QBFT node id.
27
     * @param qbftNodeBehaviour QBFT Behaviour
28
     *
29
     * @returns `true` if and only if `qbftNodeBehaviour` is a valid QBFT behaviour
30
     *          for a QBFT node with id `id` deployed in a system with configuration
31
     *          `configuration.
32
     * 
33
     */   
34
    predicate IsValidQbftBehaviour(
35
        configuration: Configuration,
36
        id: Address,
37
        qbftNodeBehaviour: QbftNodeBehaviour
38
    )
39
    {
40
        exists nt: iseq<NodeState> ::
41
            && NodeInit(nt[0], configuration, id)
42
            && qbftNodeBehaviour.initialBlockchain == nt[0].blockchain
43
            && (forall i:nat ::
44
                    IsValidQbftBehaviourStep(qbftNodeBehaviour, nt ,i)
45
            )
46
    }    
47
 
48
    /**
49
     * This function defines the conditions of validity for a single QBFT
50
     * behaviour step
51
     *
52
     * @param qbftNodeBehaviour QBFT Behaviour including the step for which to
53
     *                          verify validity.
54
     * @param nt Infinite sequence of QBFT states associated with the behaviour
55
     *           `qbftNodeBehaviour`.
56
     * @param i Index of the step for which to verify validity
57
     *
58
     * @returns `true` if and only if the `i`-th step in `qbftNodeBehaviour`
59
     *          corresponds to a valid transition between state `nt[i]` and
60
     *          state `nt[i+1]`.
61
     */
62
    predicate IsValidQbftBehaviourStep(
63
        qbftNodeBehaviour: QbftNodeBehaviour,
64
        nt: iseq<NodeState>,
65
        i: nat
66
    )
67
    {
68
        var step := qbftNodeBehaviour.steps[i];
69
        && validNodeState(nt[i])
70
        && NodeNext(nt[i], step.messagesReceived, nt[i+1], step.messagesToSend)
71
        && step.newBlockchain == nt[i+1].blockchain        
72
    }    
73
 
74
    /** =======================================================================
75
     * QBFT NODE STATE TRANSITION AND MESSAGE TRANSMISSION SPECIFICATION
76
     ========================================================================*/    
77
    /**
78
     * Initial State Specification.
79
     *
80
     * This predicate specifies the set of allowed initial states for a QBFT
81
     * node.
82
     *
83
     * @param state A QBFT node state.
84
     * @param c A QBFT network configuration.
85
     * @param id A QBFT node identifier.
86
     *
87
     * @returns `true` if and only if `state` is a valid initial QBFT state for
88
     *          a node with id `id` deployed in a QBFT network with
89
     *          configuration `c`. 
90
     */
91
    predicate NodeInit(state:NodeState, c:Configuration, id:Address)
92
    {
93
        && state.blockchain == [c.genesisBlock]
94
        && |validators([c.genesisBlock])| > 0
95
        && state.round == 0
96
        && state.localTime == 0
97
        && state.id == id
98
        && state.configuration == c
99
        && state.messagesReceived == {} 
100
        && state.proposalAcceptedForCurrentRound == None
101
        && state.lastPreparedBlock == None
102
        && state.lastPreparedRound == None
103
        && state.timeLastRoundStart == 0
104
    }
105
 
106
    /**
107
     * Next State and Message Transmission Specification.
108
     *
109
     * This predicate specifies how the state of a QBFT node should evolve and
110
     * which messages should be transmitted every time that its system clock
111
     * ticks.
112
     *
113
     * @param current Current, or old, QBFT node state.
114
     * @param inQbftMessages The of messages received when the node clock ticks.
115
     * @param next Next state QBFT node state.
116
     * @param outQbftMessages Set of messages with recipient to be sent by the
117
     *                        QBFT node.
118
     *
119
     * @returns `true` if and only if a QBFT node with state `current` that
120
     *          receives the set of messages `inQbftMessages` on the next tick
121
     *          of its local clock can transition to state `next` and send the
122
     *          set of messages with recipient `outQbftMessages`.
123
     */
124
    predicate NodeNext(
125
        current:NodeState, 
126
        inQbftMessages: set<QbftMessage>, 
127
        next:NodeState,
128
        outQbftMessages: set<QbftMessageWithRecipient>
129
        )
130
    requires validNodeState(current)   
131
    {
132
        var newMessagesReceived := current.messagesReceived + inQbftMessages;
133
 
134
        var currentWithNewMessagesReceived :=
135
            current.(
136
                messagesReceived := newMessagesReceived,
137
                localTime := current.localTime + 1
138
            );
139
    
140
        // `next` and `outQbftMessages` must be the result result of the
141
        // composition of as many `NodeNextSubStep` predicates as possible until
142
        // only stuttering actions are possible, i.e. until `NodeNextSubStep` is
143
        // `true` only if the state provided for the `next` parameter matches
144
        // the state provided for the `current` parameter and the
145
        // `outQbftMessages` parameter corresponds to the empty set.
146
        exists s:seq<NodeState>, o:seq<set<QbftMessageWithRecipient>> ::
147
            && |s| >= 2
148
            && |o| == |s| - 1
149
            && s[0] == currentWithNewMessagesReceived
150
            && s[|s|-1] == next
151
            && (forall i | 0 <= i < |s| - 1 ::
152
                && validNodeState(s[i])  
153
                && NodeNextSubStep(s[i], s[i+1], o[i])
154
            )          
155
            && (forall afterNext, messages | afterNext != s[|s|-1] :: 
156
                !(
157
                    && validNodeState(s[|s|-1])
158
                    && NodeNextSubStep(s[|s|-1], afterNext, messages)
159
                )
160
            )
161
            && outQbftMessages == setUnionOnSeq(o)
162
    }
163
 
164
    /**
165
     * Single Step State and Message Transmission Specification
166
     *
167
     * This predicate specifies how the state of a QBFT node should evolve and
168
     * which messages should be transmitted for any single event, like the
169
     * reception of a message of a specific type or the expiry of a specific
170
     * timer, that may occur when its local clock ticks. The predicate assumes
171
     * that `current.messagesReceived` corresponds to the set of all and only
172
     * messages received so far by the node. 
173
     *
174
     *
175
     * @param current Current, or old, QBFT node state.
176
     * @param next Next state QBFT node state.
177
     * @param outQbftMessages Set of messages with recipient to be sent by the
178
     * QBFT node.
179
     *
180
     * @returns `true` if and only if a QBFT node with state `current` that has
181
     *          received the set of messages `current.messagesReceived` can
182
     *          transition to state `next` and send the set of messages with
183
     *          recipient `outQbftMessages` when its local clock ticks.
184
     */
185
    predicate NodeNextSubStep(
186
        current:NodeState, 
187
        next: NodeState,
188
 
189
        outQbftMessages: set<QbftMessageWithRecipient>
190
    )
191
    requires validNodeState(current)       
192
    {
193
        || (
194
            && current.id in validators(current.blockchain)
195
            && (
196
                || UponBlockTimeout(current, next, outQbftMessages)
197
                || UponProposal(current, next, outQbftMessages)
198
                || UponPrepare(current, next, outQbftMessages)
199
                || UponCommit(current, next, outQbftMessages)
200
                || UponRoundChange(current, next, outQbftMessages)
201
                || UponRoundTimeout(current, next, outQbftMessages)
202
            )
203
        )
204
        || UponNewBlock(current, next, outQbftMessages)
205
        || (
206
            && next == current
207
            && outQbftMessages == {}
208
        )   
209
    }    
210
 
211
    /** =======================================================================
212
     * QBFT SINGLE EVENT STATE TRANSITION AND MESSAGE TRANSMISSION SPECIFICATION
213
     *
214
     * Each of the Upon<EventName> predicates in the remainder of this file
215
     * specifies how the state of a QBFT node should evolve and which messages
216
     * should be transmitted when the event <EventName> occurs the next local
217
     * clock tick.
218
     *
219
     * An <EventName> that end in `Timeout` indicates the expiry of a time, all
220
     * other event <EventName>s indicate the reception of a specific QBFT
221
     * message, i.e. `UponProposal` is the predicate associate with the
222
     * reception of a Proposal message.
223
     *
224
     * All Upon<EventName> predicates have the same parameters and the same
225
     * return value. Namely, 
226
     * @param current Current, or old, QBFT node state.
227
     * @param next Next state QBFT node state.
228
     * @param outQbftMessages Set of messages with recipient to be sent by the
229
     *                        QBFT node.
230
     *
231
     * @returns `true` if and only if a QBFT node with state `current` that has
232
     *          received the set of messages `current.messagesReceived` can
233
     *          transition to state `next` and send the set of messages with
234
     *          recipient `outQbftMessages` when event <EventName> occurs on its
235
     *          next local clock tick.
236
     ========================================================================*/  
237
 
238
    predicate UponBlockTimeout(
239
        current:NodeState,
240
        next: NodeState,
241
 
242
        outQbftMessages: set<QbftMessageWithRecipient>
243
        )
244
    requires validNodeState(current)      
245
    {
246
        if  && current.round == 0
247
            && proposer(0,current.blockchain) == current.id
248
            && current.localTime >= 
249
                current.blockchain[|current.blockchain|-1].header.timestamp + 
250
                current.configuration.blockTime 
251
        then
252
            var block := getNewBlock(current, 0);
253
 
254
            var proposal :=
255
                Proposal(
256
                    signProposal(
257
                        UnsignedProposal(
258
                            |current.blockchain|,
259
                            0,
260
                            digest(block)),
261
                        current.id),
262
                    block,
263
                    {},
264
                    {});
265
            
266
            && outQbftMessages ==
267
                Multicast(
268
                    validators(current.blockchain),
269
                    proposal
270
                )
271
 
272
            && next == current.(
273
                            messagesReceived := current.messagesReceived + {proposal}
274
                        )
275
        else
276
            false
277
 
278
    }  
279
 
280
    predicate UponProposal(
281
        current:NodeState, 
282
        next: NodeState,
283
 
284
        outQbftMessages: set<QbftMessageWithRecipient>)
285
    requires validNodeState(current)
286
    {
287
        if  exists m | m in current.messagesReceived :: isValidProposal(m, current)
288
        then
289
            var m :|    && m in current.messagesReceived
290
                        && isValidProposal(m, current);
291
 
292
            var newRound := m.proposalPayload.unsignedPayload.round;
293
            
294
            var prepare := 
295
                Prepare(
296
                    signPrepare(
297
                        UnsignedPrepare(
298
                            |current.blockchain|,
299
                            newRound,
300
                            digest(m.proposedBlock)),
301
                        current.id
302
                        )
303
                );
304
 
305
            && outQbftMessages ==
306
                    Multicast(
307
                        validators(current.blockchain),
308
                        prepare
309
                    )
310
 
311
            && next == current.(
312
                            round := newRound,
313
                            proposalAcceptedForCurrentRound := Optional(m),
314
                            timeLastRoundStart :=
315
                                if m.proposalPayload.unsignedPayload.round > current.round then
316
                                    current.localTime
317
                                else
318
                                    current.timeLastRoundStart  ,
319
                            messagesReceived := current.messagesReceived + {prepare}                 
320
                        )
321
 
322
        else
323
            false
324
    }   
325
 
326
    predicate UponPrepare(
327
        current:NodeState,
328
        next: NodeState,
329
 
330
        outQbftMessages: set<QbftMessageWithRecipient>
331
        )
332
    requires validNodeState(current)
333
    {
334
        if  && exists QofP:: 
335
                    && optionIsPresent(current.proposalAcceptedForCurrentRound)
336
 
337
                    &&  isNonStrictSubSetOf(
338
                        QofP,
339
                        validPreparesForHeightRoundAndDigest(
340
                            current.messagesReceived,
341
                            |current.blockchain|,
342
                            current.round,
343
                            digest(optionGet(current.proposalAcceptedForCurrentRound).proposedBlock),
344
                            validators(current.blockchain)
345
                        )
346
                    )
347
                    && |QofP| >= quorum(|validators(current.blockchain)|) 
348
 
349
            && !exists m :: && m in current.messagesReceived
350
                            && m.Commit?
351
                            && var uPayload := m.commitPayload.unsignedPayload;
352
                            && uPayload.height == |current.blockchain|
353
                            && uPayload.round == current.round
354
                            && recoverSignedCommitAuthor(m.commitPayload) == current.id
355
        then          
356
            var proposedBlock := optionGet(current.proposalAcceptedForCurrentRound).proposedBlock;
357
 
358
            var commit := 
359
                Commit(
360
                    signCommit(
361
                        UnsignedCommit(
362
                            |current.blockchain|,
363
                            current.round,
364
                            signHash(hashBlockForCommitSeal(proposedBlock), current.id),
365
                            digest(proposedBlock)),
366
                            current.id
367
                        )
368
                    );
369
 
370
            && outQbftMessages == 
371
                Multicast(
372
                    validators(current.blockchain),
373
                    commit
374
                )
375
 
376
            && next == current.(
377
                            lastPreparedBlock := Optional(proposedBlock),
378
                            lastPreparedRound := Optional(current.round),
379
                            messagesReceived := current.messagesReceived + {commit}
380
                        )
381
                     
382
        else
383
            false 
384
    }
385
 
386
    function getCommitSealsFromCommitMessages(
387
        msgs: set<QbftMessage>
388
    ): set<Signature>
389
    requires forall m | m in msgs :: m.Commit?
390
    {
391
        set m:QbftMessage | m in msgs :: m.commitPayload.unsignedPayload.commitSeal
392
    }
393
 
394
    predicate UponCommit(
395
        current:NodeState,
396
        next: NodeState,
397
 
398
        outQbftMessages: set<QbftMessageWithRecipient>
399
        )
400
    requires validNodeState(current)
401
    {
402
        if current.proposalAcceptedForCurrentRound.Optional? then
403
            var allValidCommitsForCurrentHeightAndRound := 
404
                validCommitsForHeightRoundAndDigest(
405
                    current.messagesReceived,
406
                    |current.blockchain|,
407
                    current.round,
408
                    current.proposalAcceptedForCurrentRound.value.proposedBlock,
409
                    validators(current.blockchain));
410
 
411
            if  exists QofC:: 
412
                    && isNonStrictSubSetOf(QofC, allValidCommitsForCurrentHeightAndRound)
413
                    && |QofC| >= quorum(|validators(current.blockchain)|) 
414
            then  
415
                // The following statement is required only to let the varifier
416
                // prove the existence of the var QofC below
417
                lemmaIfSubSetOfGreaterSizeExistsThenSmallSubsetExists(allValidCommitsForCurrentHeightAndRound, quorum(|validators(current.blockchain)|));
418
 
419
                var QofC:|
420
                    && isNonStrictSubSetOf(QofC, allValidCommitsForCurrentHeightAndRound)
421
                    && |QofC| == quorum(|validators(current.blockchain)|);
422
 
423
                var proposedBlock:Block := current.proposalAcceptedForCurrentRound.value.proposedBlock;
424
 
425
                var blockWithAddedCommitSeals :=  
426
                    proposedBlock.(
427
                        header := proposedBlock.header.(
428
                            commitSeals := getCommitSealsFromCommitMessages(QofC)
429
                        )
430
                    );            
431
 
432
                var newBlock := NewBlock( blockWithAddedCommitSeals);
433
 
434
                && outQbftMessages == 
435
                    Multicast(
436
                        current.configuration.nodes,
437
                        newBlock
438
                    )
439
 
440
                && next == current.(
441
                                blockchain := current.blockchain + [proposedBlock],
442
                                round := 0,
443
                                proposalAcceptedForCurrentRound := Optional.None,
444
                                lastPreparedBlock := Optional.None,
445
                                lastPreparedRound := Optional.None,
446
                                timeLastRoundStart := current.localTime,
447
                                messagesReceived := current.messagesReceived + {newBlock}
448
                            )
449
                        
450
            else
451
                false 
452
        else
453
            false
454
    }    
455
 
456
    predicate UponNewBlock(
457
        current:NodeState,
458
        next: NodeState,
459
 
460
        outQbftMessages: set<QbftMessageWithRecipient>
461
        )
462
    requires validNodeState(current)
463
    {
464
        if exists m | m in current.messagesReceived :: validNewBlockMessage(current.blockchain,m)
465
        then
466
            var m :| m in current.messagesReceived && validNewBlockMessage(current.blockchain,m);
467
 
468
            && next == current.(
469
                            blockchain := current.blockchain + [m.block],
470
                            round := 0,
471
                            proposalAcceptedForCurrentRound := Optional.None,
472
                            lastPreparedBlock := Optional.None,
473
                            lastPreparedRound := Optional.None,
474
                            timeLastRoundStart := current.localTime                            
475
                        )
476
 
477
            && outQbftMessages == {}
478
        else
479
            false
480
    } 
481
 
482
    predicate UponRoundTimeout(
483
        current:NodeState, 
484
        next: NodeState,
485
 
486
        outQbftMessages: set<QbftMessageWithRecipient>
487
        )
488
    requires validNodeState(current)
489
    {
490
        if  current.localTime >= current.timeLastRoundStart + roundTimeout(current.round)
491
        then
492
            var newRound := current.round + 1;
493
            var roundChange := createRoundChange(current, newRound);
494
 
495
            && outQbftMessages ==
496
                Multicast(
497
                    validators(current.blockchain),
498
                    roundChange
499
                )
500
 
501
            && next == current.(
502
                            round := newRound,
503
                            proposalAcceptedForCurrentRound := Optional.None,
504
                            messagesReceived := current.messagesReceived + {roundChange}
505
                        )
506
        else
507
            false
508
    }
509
 
510
    predicate UponRoundChange(
511
        current:NodeState, 
512
        next: NodeState,
513
 
514
        outQbftMessages: set<QbftMessageWithRecipient>)
515
    requires validNodeState(current)
516
    {
517
        if  hasReceivedProposalJustificationForLeadingRound(current)
518
        then
519
            var roundChanges,
520
                prepares,
521
                newRound:nat,
522
                block
523
                :|
524
                    isProposalJustificationForLeadingRound(roundChanges, prepares, newRound, block, current);
525
 
526
            var proposal :=
527
                Proposal(
528
                    signProposal(
529
                        UnsignedProposal(
530
                            |current.blockchain|,
531
                            newRound,
532
                            digest(block)),
533
                        current.id),
534
                    block,
535
                    extractSignedRoundChanges(roundChanges),
536
                    extractSignedPrepares(prepares));
537
 
538
            && outQbftMessages ==
539
                Multicast(
540
                    validators(current.blockchain),
541
                    proposal
542
                )
543
 
544
            && next ==  current.(
545
                            round := newRound,
546
                            proposalAcceptedForCurrentRound := Optional.None,
547
                            timeLastRoundStart :=
548
                                if newRound > current.round then
549
                                    current.localTime
550
                                else
551
                                    current.timeLastRoundStart,
552
                            messagesReceived := current.messagesReceived + {proposal}
553
                        )
554
 
555
        else if 
556
            exists Frc:set<SignedRoundChange> ::
557
                && isNonStrictSubSetOf(Frc, receivedSignedRoundChangesForCurrentHeightAndFutureRounds(current))
558
                && |getSetOfRoundChangeSenders(Frc)| >= f(|validators(current.blockchain)|) + 1
559
        then
560
            // The following lemma is not really part of the specification.
561
            // It is only required to prove that the set `Frc` below exists.
562
            lemmaToProveExistenceOfSetFrc(
563
                receivedSignedRoundChangesForCurrentHeightAndFutureRounds(current), 
564
                f(|validators(current.blockchain)|) + 1 );                
565
            
566
            var Frc:set<SignedRoundChange> :| 
567
                && isNonStrictSubSetOf(Frc, receivedSignedRoundChangesForCurrentHeightAndFutureRounds(current))
568
                && |getSetOfRoundChangeSenders(Frc)| == f(|validators(current.blockchain)|) + 1;
569
 
570
            var newRound := minSet(set rcm | rcm in Frc :: rcm.unsignedPayload.round);
571
 
572
 
573
            var roundChange := createRoundChange(current, newRound);
574
 
575
            && outQbftMessages ==
576
                Multicast(
577
                    validators(current.blockchain),
578
                    roundChange
579
                )
580
 
581
            && next == current.(
582
                            round := newRound,
583
                            proposalAcceptedForCurrentRound := Optional.None,
584
                            messagesReceived := current.messagesReceived + {roundChange}
585
                        )
586
        else
587
            false
588
 
589
    } 
590
}
591

1.2 node_auxiliary_functions.dfy

This files defines the functions used in 1.1 node.dfy.

Download this as Dafny

1
/**
2
 * Copyright © 2021 EEA Inc. 
3
 *
4
 * This document is available under the terms of the Apache 2.0 License
5
 * (http://www.apache.org/licenses/LICENSE-2.0.html)
6
 */
7
include "types.dfy"
8
include "lemmas.dfy"
9
 
10
module L1_AuxiliaryFunctionsAndLemmas
11
{
12
    import opened L1_SpecTypes
13
 
14
    /** =======================================================================
15
     * CRYPTOGRAPHIC PRIMITIVES
16
     *
17
     * This section contains the declarations of the various cryptographic
18
     * primitives used throughout the specification along with `lemma`s listing
19
     * the minimum set of properties that each of them must satisfy.
20
     *
21
     * - The functions `sign<MessageType>(msg, author)` evaluate to a
22
     *   <MessageType> message signed by `author` with content `msg`.
23
     *
24
     * - The function `recoverSigned<MessagetType>Author(msg)` evaluate to the
25
     *   signer of the <MessageType> message `msg`.
26
     *
27
     * - The lemmas `lemmaSigned<MessageType>` list the minimum set of
28
     *   properties that any implementations of the `sign<MessageType>` and
29
     *   `recoverSigned<MessagetType>Author` functions used in the
30
     *   implementation of the QBFT specification must satisfy.
31
     *
32
     * - NOTE: In addition to the various properties of the formally stated in
33
     *   this specification, the `sign<MessageType>` and
34
     *   `recoverSigned<MessagetType>Author` functions must also ensure that the
35
     *   signatures cannot be forged by Byzantine nodes. This property can be
36
     *   formally expressed by providing a formal model of the systems
37
     *   (networks) that the QBFT protocol is intended to be deployed on. In the
38
     *   future, the QBFT specification may be extended to include such model.
39
     *
40
     ========================================================================*/  
41
 
42
    /**
43
     * @returns The digest of the block `block`.
44
     */
45
    function digest(block:Block):Hash
46
 
47
    /**
48
     * This lemma lists the minimum set of properties that any implementation of
49
     * the `digest` function used in the implementation of the QBFT
50
     * specification must satisfy.
51
     */
52
    lemma {:axiom} lemmaDigest()
53
    ensures forall b1, b2 :: digest(b1) == digest(b2) ==> b1 == b2     
54
 
55
    
56
    function signProposal(msg:UnsignedProposal, author: Address): SignedProposal  
57
    function recoverSignedProposalAuthor(msg:SignedProposal): Address     
58
    lemma {:axiom} lemmaSignedProposal()
59
    ensures forall m,a :: recoverSignedProposalAuthor(signProposal(m,a)) == a
60
    ensures forall m1,m2,a1,a2 :: (m1 != m2 || a1 != a2) ==> signProposal(m1,a1) != signProposal(m2,a2)
61
    ensures forall m: SignedProposal :: signProposal(m.unsignedPayload,recoverSignedProposalAuthor(m)) == m
62
    ensures forall m,a :: signProposal(m,a).unsignedPayload == m 
63
 
64
    function signPrepare(msg:UnsignedPrepare, author: Address): SignedPrepare
65
    function recoverSignedPrepareAuthor(msg:SignedPrepare): Address    
66
    lemma {:axiom} lemmaSignedPrepare()
67
    ensures forall m,a :: recoverSignedPrepareAuthor(signPrepare(m,a)) == a
68
    ensures forall m1,m2,a1,a2 :: (m1 != m2 || a1 != a2) ==> signPrepare(m1,a1) != signPrepare(m2,a2)
69
    ensures forall m: SignedPrepare :: signPrepare(m.unsignedPayload,recoverSignedPrepareAuthor(m)) == m
70
    ensures forall m,a :: signPrepare(m,a).unsignedPayload == m
71
    
72
    function signCommit(msg:UnsignedCommit, author: Address): SignedCommit
73
    function recoverSignedCommitAuthor(msg:SignedCommit): Address    
74
    lemma {:axiom} lemmaSignedCommit()
75
    ensures forall m,a :: recoverSignedCommitAuthor(signCommit(m,a)) == a
76
    ensures forall m1,m2,a1,a2 :: (m1 != m2 || a1 != a2) ==> signCommit(m1,a1) != signCommit(m2,a2)
77
    ensures forall m: SignedCommit :: signCommit(m.unsignedPayload,recoverSignedCommitAuthor(m)) == m
78
    ensures forall m,a :: signCommit(m,a).unsignedPayload == m   
79
 
80
    function signRoundChange(msg:UnsignedRoundChange, author: Address): SignedRoundChange
81
    function recoverSignedRoundChangeAuthor(msg:SignedRoundChange): Address    
82
    lemma {:axiom} lemmaSignedRoundChange()
83
    ensures forall m,a :: recoverSignedRoundChangeAuthor(signRoundChange(m,a)) == a
84
    ensures forall m1,m2,a1,a2 :: (m1 != m2 || a1 != a2) ==> signRoundChange(m1,a1) != signRoundChange(m2,a2)
85
    ensures forall m: SignedRoundChange :: signRoundChange(m.unsignedPayload,recoverSignedRoundChangeAuthor(m)) == m
86
    ensures forall m,a :: signRoundChange(m,a).unsignedPayload == m
87
 
88
    function signHash(hash:Hash, author: Address): Signature
89
    function recoverSignedHashAuthor(hash:Hash, signature: Signature): Address   
90
    lemma {:axiom} lemmaSignedHash()
91
    ensures forall h,a :: recoverSignedHashAuthor(h, signHash(h,a)) == a
92
    ensures forall h1,h2,a1,a2 :: (h1 != h2 || a1 != a2) ==> signHash(h1,a1) != signHash(h2,a2)
93
    ensures forall h,s :: signHash(h,recoverSignedHashAuthor(h,s)) == s     
94
 
95
    /** =======================================================================
96
     * UNDEFINED FUNCTIONS
97
     *
98
     * This section includes those functions for which no actual definition is
99
     * provided as that is beyond the scope of this specification. 
100
     ========================================================================*/  
101
 
102
    /**
103
     * @return `true` if and only if `block` is a valid `RawBlock` for the
104
     *         `RawBlockchain` `blockchain`. 
105
     *
106
     * @note This predicate is expected to check that `block` is valid from an
107
     *       blockchain application level perspective. This contrasts with the
108
     *       predicate `ValidNewBlock` defined below which checks that a block
109
     *       is valid from a consensus protocol perspective.
110
     */
111
    predicate validateRawEthereumBlock(blockchain:RawBlockchain, block:RawBlock)   
112
 
113
    /**
114
     * @return The set of nodes, or validators, responsible for deciding on the
115
     *         block to be appended to the `RawBlockchain` `rb`.
116
     */
117
    function validatorsOnRawBlockchain(rb: RawBlockchain): seq<Address>  
118
 
119
    /**
120
     * @returns The minimum value in set `S`.
121
     */
122
    function minSet(S:set<nat>): nat
123
    ensures minSet(S) in S 
124
    ensures forall e | e in S :: e >= minSet(S)    
125
 
126
    function getNewBlock(nodeState:NodeState, round:nat): Block
127
    ensures && getNewBlock(nodeState,round).header.roundNumber == round
128
            && |validators(nodeState.blockchain + [getNewBlock(nodeState,round)])| > 0
129
            && getNewBlock(nodeState,round).header.height == |nodeState.blockchain|
130
 
131
    /** =======================================================================
132
     * GENERAL FUNCTIONS
133
     *
134
     * This section defines those functions that, while used as part of the QBFT
135
     * specification, are general in nature
136
     ========================================================================*/
137
 
138
    /**
139
     * @return `true` if and only if the `Optional` value `o` is not empty.
140
     */
141
    predicate optionIsPresent<T>(o:Optional<T>)
142
    {
143
        o.Optional?
144
    }
145
 
146
    /**
147
     * @returns The value carried by the `Optional` value `o'.
148
     * 
149
     * @requires The `Optional` value `o` is not empty.
150
     */
151
    function optionGet<T>(o:Optional<T>): T
152
    requires optionIsPresent(o)
153
    {
154
        o.value
155
    } 
156
 
157
    /**
158
     * @returns The union of all sets included in `sets`.
159
     */
160
    function setUnion<T(!new)>(sets:set<set<T>>):set<T>
161
    ensures forall e :: ((exists s | s in sets :: e in s) <==> e in setUnion(sets))
162
    {
163
        if sets == {} then
164
            {}
165
        else
166
            var s :| s in sets;
167
            s + setUnion(sets - {s})
168
    } 
169
 
170
    /**
171
     * @returns The union of all sets included in `sets`.
172
     */
173
    function setUnionOnSeq<T>(sets:seq<set<T>>):set<T>
174
    {
175
        if sets == [] then
176
            {}
177
        else
178
            sets[0] + setUnionOnSeq(sets[1..])
179
    }             
180
 
181
    /**
182
     * @returns 2 ^ `exp`.
183
     */
184
    function powerOf2(exp:nat):nat
185
    {
186
        if exp == 0 then
187
            1
188
        else
189
            2 * powerOf2(exp-1)
190
    }
191
 
192
    /**
193
     * Function wrapping the Dafny set inclusion operator `<=` to make the spec more 
194
     * readable by people who are not much familiar with Dafny who may not be aware of
195
     * the semantic of the `<=` operator when applied to sets.
196
     *
197
     * @returns true iff `subSet` is a non-strict subset of `setIncludingTheSubset`
198
     */
199
    predicate isNonStrictSubSetOf<T>(subSet: set<T>, setIncludingTheSubset: set<T>)
200
    {
201
        subSet <= setIncludingTheSubset
202
    }     
203
 
204
    /** =======================================================================
205
     * QBFT GENERAL FUNCTIONS
206
     *
207
     * This section defines those functions that are specific to the QBFT
208
     * protocol and that are used throughout the specification
209
     ========================================================================*/  
210
     
211
    /**
212
     * @returns A `RawBlock` equivalent to `Block` `b`.
213
     */
214
    function fromBlockToRawBlock(
215
        b: Block
216
    ) : RawBlock
217
    {
218
       RawBlock(
219
           RawBlockHeader(
220
               b.header.proposer,
221
               b.header.height,
222
               b.header.timestamp
223
           ),
224
           b.body,
225
           b.transactions
226
       ) 
227
    }
228
 
229
    /**
230
     * @returns A `RawBlockchain` equivalent to `Blockchain` `bc`.
231
     */
232
    function fromBlockchainToRawBlockchain(bc:Blockchain): RawBlockchain
233
    {
234
        seq(|bc|, (i: nat) requires i < |bc| => fromBlockToRawBlock(bc[i]))
235
    }
236
 
237
    /**
238
     * @return The set of nodes, or validators, responsible for deciding on the
239
     *         block to be appended to the `Blockchain` `blockchain`.
240
     *
241
     * @note The definition of this function models the requirement that any two
242
     *       `Blockchain`s that have the same length where each block in one
243
     *       blockchain is identical to the block in the other blockchain at the
244
     *       same position except for the field `commitSeals` evaluate to the
245
     *       same set of validators. 
246
     */
247
    function validators(blockchain:Blockchain): seq<Address>
248
    {
249
        validatorsOnRawBlockchain(fromBlockchainToRawBlockchain(blockchain))
250
    }    
251
 
252
    /**
253
     * @return `true` if and only if `block` is a valid `Block` for the
254
     *         `Blockchain` `blockchain`. 
255
     *
256
     * @note The definition of this function models the requirement that the
257
     *       field `commitSeals` of `Block`s does not account when evaluating
258
     *       block validity from a blockchain application level perspective.
259
     */
260
    predicate validateEthereumBlock(blockchain:Blockchain, block:Block)   
261
    {
262
        validateRawEthereumBlock(fromBlockchainToRawBlockchain(blockchain), fromBlockToRawBlock(block))
263
    }
264
 
265
    /**
266
     * @returns The maximum number of Byzantine validators allowed in a network
267
     *          of `setSize` validators
268
     */
269
    function f(setSize:nat):nat
270
    {
271
        if setSize == 0 then
272
            0
273
        else
274
            (setSize - 1) / 3
275
    }
276
 
277
    /**
278
     * @returns The minimum size that any two subsets of validators for a
279
     *          network with `setSize` validators must have to guarantee that
280
     *          their intersection includes at least one honest validator under
281
     *          the assumption that no more than `f(setSeize)` validators are
282
     *          Byzantine.
283
     */
284
    function quorum(setSize:nat):nat
285
    {
286
        (setSize*2 - 1) / 3 + 1
287
    }    
288
 
289
    /**
290
     * @returns The round timeout for round number `round`.
291
     */
292
    function roundTimeout(round:nat):nat
293
    {
294
        powerOf2(round)
295
    }    
296
 
297
 
298
    /**
299
     * @returns `block` with `roundNumber` set to `newRound`
300
     */
301
    function replaceRoundInBlock(block: Block, newRound: nat): Block
302
    {
303
        block.(
304
            header := block.header.(
305
                roundNumber := newRound
306
            )
307
        )
308
    }          
309
 
310
    /**
311
     * @returns The hash of a block identical to `block` except for the field
312
     *          `commitSeals` which is set to the empty set.
313
     */
314
    function hashBlockForCommitSeal(block:Block): Hash
315
    {
316
        digest(
317
            block.(
318
                header:= block.header.(
319
                    commitSeals := {})
320
            )
321
        )
322
    }
323
 
324
    /**
325
     * @returns The identifier of the validator that should propose the block to
326
     *          be appended to `blockchain` via a Proposal message for round
327
     *          `ibftRound`.
328
     */
329
    function proposer(ibftRound:nat, blockchain:Blockchain): Address
330
    requires |blockchain|  > 0
331
    requires |blockchain|  > 1 ==> blockchain[|blockchain|-1].header.proposer in validators(blockchain[..|blockchain|-1])
332
    requires |validators(blockchain)| > 0
333
    {
334
        var roundZeroIndex: nat :=
335
            if |blockchain| == 1 then
336
                0
337
            else
338
                var previousBlockIndex':nat :| 
339
                && previousBlockIndex' < |validators(blockchain[..|blockchain|-1])|
340
                && validators(blockchain[..|blockchain|-1])[previousBlockIndex'] == blockchain[|blockchain|-1].header.proposer;
341
 
342
                previousBlockIndex' + 1
343
            ;
344
 
345
        validators(blockchain)[
346
            (roundZeroIndex + ibftRound) % |validators(blockchain)|
347
        ]
348
    }
349
 
350
    /**
351
     * @returns A set of `QbftMessageWithRecipient` with the field `message` set
352
     *          to the parameter `m` and the field `recipient` set to the
353
     *          parameter `recipient.
354
     *
355
     * @note This function is used in the specification to moel message
356
     *       multicast.
357
     */
358
    function Multicast(recipients:seq<Address>, m:QbftMessage): set<QbftMessageWithRecipient>
359
    {
360
        set r | r in recipients :: QbftMessageWithRecipient(m,r)
361
    }  
362
 
363
    /**
364
     * @returns An `Optional` datatype representing the digest of the `Optional`
365
     *          `block` parameter.
366
     */
367
    function digestOptionalBlock(block: Optional<Block>): Optional<Hash>
368
    {
369
        if optionIsPresent(block) then
370
            Optional(digest(optionGet(block)))
371
        else
372
            Optional.None
373
    }    
374
 
375
    /** =======================================================================
376
     * PROPOSAL AND ROUND-CHANGE FUNCTIONS
377
     *
378
     * This section defines those functions that are used in the definition of
379
     * the `UponProposal` and `UponRoundChange` predicates.
380
     ========================================================================*/   
381
    /**
382
     * @returns The set of all Prepare messages included in `current.messagesReceived`.
383
     */
384
    function receivedPrepares(current:NodeState): set<QbftMessage>
385
    {
386
        set m | 
387
            && m in current.messagesReceived
388
            && m.Prepare?            
389
    }   
390
 
391
    function extractSignedPreparesEx(messages:set<QbftMessage>): set<SignedPrepare>
392
    {
393
        (set m | && m in messages
394
                && m.Prepare?
395
            ::
396
                m.preparePayload)
397
        +
398
        setUnion(
399
            set m | && m in messages
400
                    && (
401
                        || m.Proposal?
402
                        || m.RoundChange?
403
                    )
404
                ::
405
                    m.roundChangeJustification
406
        )      
407
    }          
408
 
409
    /**
410
     * @returns The set of signed Prepare payloads included in the set of
411
     *          Prepare messages `messages`.
412
     */
413
    // TBD: Remove precondition?
414
    function extractSignedPrepares(messages:set<QbftMessage>): set<SignedPrepare>
415
    requires forall m | m in messages :: m.Prepare?
416
    {
417
        set m | m in messages
418
            ::
419
                m.preparePayload 
420
    }    
421
    
422
    /**
423
     * @returns The set of all RoundChange messages included in `current.messagesReceived`.
424
     */
425
    function receivedRoundChanges(current:NodeState): set<QbftMessage>
426
    {
427
        set m | 
428
            && m in current.messagesReceived
429
            && m.RoundChange?
430
            
431
    }    
432
    
433
    /**
434
     * @returns The set of signed RoundChange payloads included in messages in
435
     *          `current.messagesReceived` that have round higher than
436
     *          `current.round`.
437
     */
438
    function receivedSignedRoundChangesForCurrentHeightAndFutureRounds(current:NodeState): set<SignedRoundChange>
439
    {
440
        set m | 
441
            && m in current.messagesReceived
442
            && m.RoundChange?
443
            && var uPayload := m.roundChangePayload.unsignedPayload;
444
            && uPayload.height == |current.blockchain|
445
            && uPayload.round > current.round         
446
            ::
447
                m.roundChangePayload
448
            
449
    }    
450
 
451
    /**
452
     * @returns The set of signed RoundChange payloads included in the set of
453
     *          RoundChange messages `messages`.
454
     */
455
    function extractSignedRoundChanges(messages:set<QbftMessage>): set<SignedRoundChange>
456
    requires forall m | m in messages :: m.RoundChange?
457
    {
458
        set m | m in messages
459
            ::
460
                m.roundChangePayload
461
    }       
462
 
463
     /**
464
      * @returns The set of all node identifiers that have signed one or more
465
      *          RoundChange messages in `roundChanges`.
466
      */
467
    function getSetOfRoundChangeSenders(roundChanges: set<SignedRoundChange>): set<Address>
468
    {
469
        set m | m in roundChanges :: recoverSignedRoundChangeAuthor(m)
470
    }    
471
    
472
    /**
473
     * @returns The set of all blocks included in the set of RoundChange messages `messages`.
474
     */
475
    function receivedBlocksInRoundChanges(messages:set<QbftMessage>): set<Block>
476
    requires forall m | m in messages :: m.RoundChange?
477
    {
478
        set m   | 
479
                    && m in messages
480
                    && optionIsPresent(m.proposedBlockForNextRound)
481
                ::
482
                    optionGet(m.proposedBlockForNextRound)
483
 
484
    }     
485
 
486
    /**
487
     * @returns `true` if and only if `block` is a valid block for a Proposal
488
     *          message for round `round`  that does not carry any RoundChange
489
     *          Justification under the assumption that the current blockchain is
490
     *          `blockchain`.
491
     */
492
    predicate validateNonPreparedBlock(
493
        block: Block,
494
        blockchain: Blockchain,
495
        round: nat
496
    )
497
    requires StateBlockchainInvariant(blockchain)
498
    {
499
        && validateEthereumBlock(blockchain, block)
500
        && block.header.proposer == proposer(round, blockchain)
501
        && |validators(blockchain  + [block])| > 0
502
    }
503
 
504
    /**
505
     * @returns `true` if and only if `sPayload` is a valid signed RoundChange
506
     *          payload for height `height`, round `round` under the assumption
507
     *          that the current set of validators is `validators`.
508
     */
509
    predicate validRoundChange(
510
        sPayload: SignedRoundChange, 
511
        height: nat, 
512
        round: nat,
513
        validators: seq<Address>)
514
    {
515
        var uPayload := sPayload.unsignedPayload;
516
 
517
        && uPayload.height == height
518
        && uPayload.round == round
519
        && (if  && !optionIsPresent(uPayload.preparedRound)
520
                && !optionIsPresent(uPayload.preparedValue)
521
            then
522
                true
523
            else if && optionIsPresent(uPayload.preparedRound)
524
                    && optionIsPresent(uPayload.preparedValue)
525
            then
526
                    optionGet(uPayload.preparedRound) < round
527
            else
528
                false)
529
        && recoverSignedRoundChangeAuthor(sPayload) in validators
530
    }
531
 
532
    /**
533
     * @returns `true` if and only if `sPayload` is one of the signed
534
     *          RoundChange payloads with the highest round in the set
535
     *          `roundChanges`.
536
     */
537
    predicate isHighestPrepared(sPayload:SignedRoundChange, roundChanges:set<SignedRoundChange>)
538
    {
539
        &&  optionIsPresent(sPayload.unsignedPayload.preparedRound)
540
        &&  optionIsPresent(sPayload.unsignedPayload.preparedValue)
541
        &&  forall m | m in roundChanges ::
542
                optionIsPresent(m.unsignedPayload.preparedRound) ==>
543
                    optionGet(m.unsignedPayload.preparedRound) <= optionGet(sPayload.unsignedPayload.preparedRound)
544
                
545
    }
546
 
547
    /**
548
     * @returns `true` if and only if `roundChanges` and `prepares` are,
549
     *          respectively, valid Proposal and RoundChange justifications for
550
     *          a Proposal message for height `height`, round `round` including
551
     *          block `block` undef the following assumptions: (i) the only
552
     *          possible set of blocks that a node can justify is
553
     *          `setOfAvailableBlocks`, (ii) the validation function to be used
554
     *          in the case that `prepares` is empty is `validateBlock`, (iii)
555
     *          the leader for `round` is `roundLeader` and (iv) the current set
556
     *          of validators is `validators`.
557
     */
558
    predicate isProposalJustification( 
559
        roundChanges:set<SignedRoundChange>, 
560
        prepares:set<SignedPrepare>,   
561
        setOfAvailableBlocks: set<Block>,      
562
        height: nat,
563
        round: nat,
564
        block: Block,
565
        validateBlock: Block -> bool,
566
        roundLeader: Address,
567
        validators:seq<Address>)
568
    {
569
        if round == 0 then 
570
            && validateBlock(block)
571
            && block.header.roundNumber == 0
572
            && block.header.height == height
573
            && block.header.proposer == roundLeader
574
        else
575
            && |getSetOfRoundChangeSenders(roundChanges)| >= quorum(|validators|)
576
            && (forall m | m in roundChanges :: validRoundChange(m,height,round,validators))
577
            &&  if (forall m | m in roundChanges :: && !optionIsPresent(m.unsignedPayload.preparedRound)
578
                                                    && !optionIsPresent(m.unsignedPayload.preparedValue))
579
                then
580
                    && validateBlock(block)
581
                    && block.header.roundNumber == round
582
                    && block.header.height == height
583
                    && block.header.proposer == roundLeader
584
                else
585
                    && block in setOfAvailableBlocks
586
                    && block.header.roundNumber == round
587
                    && block.header.height == height
588
                    && |prepares| >= quorum(|validators|)
589
                    && exists rcm | rcm in roundChanges ::
590
                        && isHighestPrepared(rcm,roundChanges)
591
                        && var proposedBlockWithOldRound := 
592
                                replaceRoundInBlock(
593
                                    block,
594
                                    optionGet(rcm.unsignedPayload.preparedRound)
595
                                );                        
596
                        && optionGet(rcm.unsignedPayload.preparedValue) == digest(proposedBlockWithOldRound)
597
                        && (forall pm | pm in prepares :: 
598
                                            validSignedPrepareForHeightRoundAndDigest(
599
                                                pm,
600
                                                height,
601
                                                optionGet(rcm.unsignedPayload.preparedRound),
602
                                                optionGet(rcm.unsignedPayload.preparedValue),
603
                                                validators
604
                                            ))
605
    }
606
 
607
    /**
608
     * @returns `true` if and only if `m` is a valid Proposal message for a QBFT node with state `current.
609
     */
610
    predicate isValidProposal(m:QbftMessage, current:NodeState)
611
    requires validNodeState(current)
612
    {
613
        && m.Proposal?
614
        && var roundLeader := proposer(m.proposalPayload.unsignedPayload.round,current.blockchain);        
615
        && m.proposalPayload.unsignedPayload.height == |current.blockchain|
616
        && recoverSignedProposalAuthor(m.proposalPayload) == roundLeader
617
        && isProposalJustification(
618
            m.proposalJustification,
619
            m.roundChangeJustification,
620
            {m.proposedBlock},
621
            |current.blockchain|,
622
            m.proposalPayload.unsignedPayload.round,
623
            m.proposedBlock,
624
            b => validateNonPreparedBlock(b,current.blockchain,m.proposalPayload.unsignedPayload.round),
625
            roundLeader,
626
            validators(current.blockchain)
627
        )
628
        // NOTE: This check is not required by the QBFT paper as the message structure is a bit different
629
        && digest(m.proposedBlock) == m.proposalPayload.unsignedPayload.digest
630
        && (
631
            || m.proposalPayload.unsignedPayload.round > current.round
632
            || (
633
                && !optionIsPresent(current.proposalAcceptedForCurrentRound)
634
                && m.proposalPayload.unsignedPayload.round == current.round
635
            )
636
        )
637
    }    
638
 
639
    /**
640
     * @returns `true` if and only if `roundChanges` and `prepares` are,
641
     *          respectively, valid Proposal and RoundChange justifications for
642
     *          a Proposal message with round `newRound` including block `block`
643
     *          under the assumption that the current QBFT node state is
644
     *          `current`.
645
     */
646
    predicate isReceivedProposalJustification(
647
        roundChanges: set<QbftMessage>,
648
        prepares: set<QbftMessage>,  
649
        newRound: nat,
650
        block: Block,
651
        current:NodeState)
652
    requires validNodeState(current)
653
    {
654
        && isNonStrictSubSetOf(roundChanges, receivedRoundChanges(current))
655
        && (forall m | m in prepares :: m.Prepare?)
656
        && isNonStrictSubSetOf(extractSignedPrepares(prepares), extractSignedPreparesEx(current.messagesReceived))
657
        && isProposalJustification(
658
            extractSignedRoundChanges(roundChanges),
659
            extractSignedPrepares(prepares),
660
            receivedBlocksInRoundChanges(roundChanges),
661
            |current.blockchain|,
662
            newRound,
663
            block, 
664
            b => && b == getNewBlock(current, newRound),
665
            proposer(newRound,current.blockchain),
666
            validators(current.blockchain))
667
    }     
668
 
669
    /**
670
     * @returns `true` if and only if a QBFT node with state `current` has
671
     *          received a valid Proposal Justification for a round where the QBFT node 
672
     *          is the leader.
673
     */
674
    predicate hasReceivedProposalJustificationForLeadingRound(current: NodeState)
675
    requires validNodeState(current)
676
    {
677
        exists  
678
            roundChanges: set<QbftMessage>,
679
            prepares: set<QbftMessage>,
680
            newRound: nat,
681
            block: Block
682
        ::
683
            && isProposalJustificationForLeadingRound(roundChanges, prepares, newRound, block, current)          
684
    }  
685
 
686
    /**
687
     * @returns `true` if and only if a QBFT node with state `current` has
688
     *          received a valid Proposal Justification for `newRound` where the
689
     *          QBFT node is the leader in `newRound` and, either `newRound` is
690
     *          strictly higher than the current round or it is equal to the
691
     *          current round and no proposal has been accepted for the current
692
     *          round 
693
     */
694
    predicate isProposalJustificationForLeadingRound(
695
        roundChanges: set<QbftMessage>,
696
        prepares: set<QbftMessage>,
697
        newRound: nat,
698
        block: Block,
699
        current: NodeState     
700
    )
701
    requires validNodeState(current)
702
    {
703
        && isReceivedProposalJustification(roundChanges, prepares, newRound, block, current)
704
        && proposer(newRound, current.blockchain) == current.id
705
        && (
706
            || newRound > current.round
707
            || (
708
                && !optionIsPresent(current.proposalAcceptedForCurrentRound)
709
                && newRound == current.round
710
            )
711
        )               
712
    }      
713
      
714
    /**
715
     * @returns The RoundChange Justification that a QBFT node with state
716
     *          `current` has received since adopting its current blockchain, or
717
     *          the empty set if no Round Change Justification has been received
718
     *          since.
719
     */
720
    function getRoundChangeJustification(current:NodeState): set<SignedPrepare>
721
    requires validNodeState(current)
722
    {
723
        if !optionIsPresent(current.lastPreparedBlock) then
724
            {}
725
        else
726
            var QofP: set<QbftMessage> :| 
727
                && isNonStrictSubSetOf(
728
                    QofP,
729
                    validPreparesForHeightRoundAndDigest(
730
                        current.messagesReceived,
731
                        |current.blockchain|,
732
                        optionGet(current.lastPreparedRound),
733
                        digest(optionGet(current.lastPreparedBlock)),
734
                        validators(current.blockchain)
735
                    )
736
                )
737
                && |QofP| >= quorum(|validators(current.blockchain)|);
738
            
739
            set m | m in QofP :: m.preparePayload
740
    } 
741
 
742
    /**
743
     * @returns The RoundChange message that a QBFT node with state `current`
744
     *          would send to move to round `newRound`.
745
     */
746
    function createRoundChange(
747
        current: NodeState,
748
        newRound:nat
749
        ):
750
        QbftMessage
751
    requires validNodeState(current)
752
    {
753
        RoundChange(
754
            signRoundChange(
755
                UnsignedRoundChange(
756
                    |current.blockchain|,
757
                    newRound,
758
                    digestOptionalBlock(current.lastPreparedBlock),
759
                    current.lastPreparedRound),
760
            current.id),
761
            current.lastPreparedBlock,
762
            getRoundChangeJustification(current)
763
        )
764
    }    
765
 
766
    /** =======================================================================
767
     * PREPARE VALIDATION FUNCTIONS
768
     *
769
     * This section defines those functions that are used to determine whether a
770
     * Prepare message is valid.
771
     ========================================================================*/  
772
    /**
773
     * @returns `true` if and only if `sPayload` is a valid signed Prepare
774
     *          payload for height `height`, round `round`, block digest
775
     *          `digest` under the assumption that the set of validators is
776
     *          `validators'.
777
     */
778
    predicate validSignedPrepareForHeightRoundAndDigest(
779
        sPayload: SignedPrepare, 
780
        height:nat, 
781
        round:nat, 
782
        digest:Hash,
783
        validators: seq<Address>
784
        )
785
    {
786
        var uPayload := sPayload.unsignedPayload;
787
        && uPayload.height == height
788
        && uPayload.round == round
789
        && uPayload.digest == digest
790
        && recoverSignedPrepareAuthor(sPayload) in validators
791
    }
792
 
793
    /**
794
     * @returns The set of all valid Prepare messages for height `height, round
795
     *          `round`, block digest `digest` that are included in the set
796
     *          `messagesReceived` under the assumption that the set of
797
     *          validators is `validators`.
798
     */
799
    function validPreparesForHeightRoundAndDigest(
800
        messagesReceived: set<QbftMessage>, 
801
        height:nat, 
802
        round:nat, 
803
        digest:Hash,
804
        validators: seq<Address>
805
        ): set<QbftMessage>
806
    {
807
 
808
        set m  |    && m in messagesReceived
809
                    && m.Prepare?
810
                    && validSignedPrepareForHeightRoundAndDigest(
811
                        m.preparePayload,
812
                        height,
813
                        round,
814
                        digest,
815
                        validators
816
                    )
817
    }  
818
 
819
    /** =======================================================================
820
     * COMMIT VALIDATION FUNCTIONS
821
     *
822
     * This section defines those functions that are used to determine whether a
823
     * Commit message is valid.
824
     ========================================================================*/  
825
    /**
826
     * @returns `true` if and only if `sPayload` is a valid signed Commit
827
     *          payload for height `height`, round `round`, block
828
     *          `proposedBlock` under the assumption that the set of validators
829
     *          is `validators'.
830
     */
831
    predicate validateCommit(commit:SignedCommit, height:nat, round:nat, proposedBlock:Block, validators:seq<Address>)
832
    {
833
        var uPayload := commit.unsignedPayload;
834
 
835
        && uPayload.height == height
836
        && uPayload.round == round
837
        && uPayload.digest == digest(proposedBlock)
838
        && recoverSignedHashAuthor(hashBlockForCommitSeal(proposedBlock), uPayload.commitSeal) == recoverSignedCommitAuthor(commit)
839
        && recoverSignedCommitAuthor(commit) in validators
840
    }    
841
 
842
    /**
843
     * @returns The set of all valid Commit messages for height `height, round
844
     *          `round`, block `proposedBlock` that are included in the set
845
     *          `messagesReceived` under the assumption that the set of
846
     *          validators is `validators`.
847
     */    
848
    function validCommitsForHeightRoundAndDigest(
849
        messagesReceived: set<QbftMessage>, 
850
        height:nat, 
851
        round:nat, 
852
        proposedBlock:Block,
853
        validators: seq<Address>
854
        ): set<QbftMessage>
855
    {
856
 
857
        set m  |    && m in messagesReceived
858
                    && m.Commit?
859
                    && validateCommit(
860
                        m.commitPayload,
861
                        height,
862
                        round,
863
                        proposedBlock,
864
                        validators
865
                    )
866
    }    
867
 
868
    /** =======================================================================
869
     * NEW-BLOCK VALIDATION FUNCTIONS
870
     *
871
     * This section defines those functions that are used to determine whether a
872
     * NewBlock message is valid.
873
     ========================================================================*/  
874
    /**
875
     * @returns `true` if and only if block `block` carries a valid set of
876
     *          commit seals that justify appending it to blockchain
877
     *          `blockchain`.
878
     */
879
    predicate ValidNewBlock(blockchain:Blockchain, block: Block)
880
    {
881
        && block.header.height == |blockchain|
882
        && |block.header.commitSeals| >= quorum(|validators(blockchain)|)
883
        && (forall s | s in block.header.commitSeals :: recoverSignedHashAuthor(hashBlockForCommitSeal(block),s) in validators(blockchain))
884
    } 
885
 
886
    /**
887
     * @return `true` if and only if `msg` is a NewBlock message including a
888
     *         block that carries a valid set of commit seals that justify
889
     *         appending it to blockchain `blockchain`.
890
     */
891
    predicate validNewBlockMessage(blockchain: Blockchain, msg:QbftMessage)
892
    {
893
        && msg.NewBlock?
894
        && ValidNewBlock(blockchain, msg.block)
895
    }                
896
 
897
    /** =======================================================================
898
     * NON-SPECIFICATION FUNCTIONS
899
     *
900
     * This section defines those functions that are used in the specification
901
     * but that are used for verification purposes and not specification
902
     * purposes.
903
     ========================================================================*/  
904
    predicate validNodeState(nodeState: NodeState)
905
    {
906
        && (optionIsPresent(nodeState.proposalAcceptedForCurrentRound) ==> optionGet(nodeState.proposalAcceptedForCurrentRound).Proposal?)
907
        && (!optionIsPresent(nodeState.lastPreparedRound) <==> !optionIsPresent(nodeState.lastPreparedBlock))
908
        && (optionIsPresent(nodeState.lastPreparedRound) ==>
909
                exists QofP ::
910
                    && isNonStrictSubSetOf(
911
                            QofP,
912
                            validPreparesForHeightRoundAndDigest(
913
                                nodeState.messagesReceived,
914
                                |nodeState.blockchain|,
915
                                optionGet(nodeState.lastPreparedRound),
916
                                digest(optionGet(nodeState.lastPreparedBlock)),
917
                                validators(nodeState.blockchain)
918
                        )
919
                    )
920
                    && |QofP| >= quorum(|validators(nodeState.blockchain)|) 
921
            )   
922
        && StateBlockchainInvariant(nodeState.blockchain)       
923
    }
924
 
925
    predicate StateBlockchainInvariant(blockchain: Blockchain)
926
    {
927
        && |blockchain|  > 0
928
        && (|blockchain|  > 1 ==> blockchain[|blockchain|-1].header.proposer in validators(blockchain[..|blockchain|-1]))
929
        && |validators(blockchain)| > 0  
930
    }             
931
}

1.3 types.dfy

This file defines all the types used throughout the specification.

Download this as Dafny

1
 /**
2
 * Copyright © 2021 EEA Inc. 
3
 *
4
 * This document is available under the terms of the Apache 2.0 License
5
 * (http://www.apache.org/licenses/LICENSE-2.0.html)
6
 */
7
module L1_SpecTypes
8
{
9
    /** =======================================================================
10
     * UNDEFINED TYPES
11
     *
12
     * This section includes the declarations of those types that are left
13
     * undefined in this specification.
14
     ========================================================================*/
15
    type {:extern "Address"} Address(==,!new)
16
 
17
    type {:extern "BlockBody"} BlockBody(==,!new)
18
 
19
    type {:extern "Transaction"} Transaction(==,!new)
20
 
21
    type {:extern "Hash"} Hash(==,!new)
22
 
23
    type {:extern "Signature"} Signature(==,!new)
24
 
25
    /** =======================================================================
26
     * BLOCKCHAIN TYPES
27
     *
28
     * This section includes the declaration of the types that are related to
29
     * sequences of blocks.
30
     * 
31
     * - The only difference between `Block` and `RawBlock` is that the header
32
     *   of a `RawBlock` does not include the field `commitSeals`.
33
     ========================================================================*/
34
    type Blockchain = seq<Block>
35
 
36
    datatype BlockHeader = BlockHeader (
37
        proposer: Address, 
38
        roundNumber: nat,
39
        commitSeals: set<Signature>,
40
        height:nat,
41
        timestamp: nat
42
    )
43
 
44
    datatype Block = Block (
45
        header: BlockHeader,
46
        body: BlockBody,
47
        transactions: seq<Transaction>
48
    )
49
 
50
    type RawBlockchain = seq<RawBlock>     
51
 
52
    datatype RawBlockHeader = RawBlockHeader (
53
        proposer: Address,
54
        height:nat,
55
        timestamp: nat
56
    ) 
57
 
58
    datatype RawBlock = RawBlock (
59
        header: RawBlockHeader,
60
        body: BlockBody,
61
        transactions: seq<Transaction>
62
    )     
63
 
64
    /** =======================================================================
65
     * MESSAGE TYPES
66
     *
67
     * This section includes the declaration of those types that are used to
68
     * define the various QBFT messages.
69
     *
70
     * - `Unsigned*` types represent messages without signature.
71
     * - `Signed*` types represent messages carrying a signature.
72
     * - `QbtMessage` is the datatype representing any QBFT message.
73
     * - `QbtMessageWithRecipient` is the datatype used to indicate which node
74
     *   a message should be sent to.
75
     *
76
     ========================================================================*/
77
    datatype UnsignedProposal = UnsignedProposal (
78
        height:nat, 
79
        round:nat, 
80
        digest: Hash
81
    )
82
 
83
    datatype UnsignedPrepare = UnsignedPrepare (
84
        height:nat, 
85
        round:nat, 
86
        digest:Hash
87
    )
88
 
89
    datatype UnsignedCommit = UnsignedCommit (
90
        height:nat, 
91
        round:nat, 
92
        commitSeal: Signature,
93
        digest:Hash
94
    )
95
 
96
    datatype UnsignedRoundChange = UnsignedRoundChange (
97
        height:nat, 
98
        round:nat, 
99
        preparedValue: Optional<Hash>, 
100
        preparedRound: Optional<nat>
101
    )
102
 
103
    datatype SignedProposal = SignedProposal (
104
        unsignedPayload: UnsignedProposal,
105
        signature: Signature
106
    )
107
 
108
    datatype SignedPrepare = SignedPrepare(
109
        unsignedPayload: UnsignedPrepare,
110
        signature: Signature
111
    )
112
 
113
    datatype SignedCommit = SignedCommit(
114
        unsignedPayload: UnsignedCommit,
115
        signature: Signature
116
    )
117
 
118
    datatype SignedRoundChange = SignedRoundChange(
119
        unsignedPayload: UnsignedRoundChange,
120
        signature: Signature
121
    )
122
 
123
    datatype QbftMessage =
124
        | Proposal(
125
            proposalPayload: SignedProposal,
126
            proposedBlock:Block, 
127
            proposalJustification: set<SignedRoundChange>,
128
            roundChangeJustification: set<SignedPrepare>
129
        )
130
        | Prepare(
131
            preparePayload: SignedPrepare
132
        )
133
        | Commit(
134
            commitPayload: SignedCommit
135
        )
136
        | RoundChange(
137
            roundChangePayload: SignedRoundChange,
138
            proposedBlockForNextRound: Optional<Block>,
139
            roundChangeJustification: set<SignedPrepare>
140
        )
141
        | NewBlock(
142
            block: Block
143
        )
144
 
145
    datatype QbftMessageWithRecipient = QbftMessageWithRecipient(
146
        message: QbftMessage,
147
        recipient: Address
148
    )    
149
 
150
    /** =======================================================================
151
     * STATE TYPES
152
     *
153
     * This section includes the declaration of the types that are used in the
154
     * representation of the state of a QBFT node.
155
     *
156
     ========================================================================*/
157
 
158
    /**
159
     * This type groups the configuration parameters for a QBFT network.
160
     */
161
    datatype Configuration = Configuration(
162
        nodes: seq<Address>, // Ordered set of the ids of all the nodes
163
        genesisBlock : Block,
164
        blockTime: nat
165
    )
166
 
167
    /**
168
     * This type represents the state associated with any QBFT node.
169
     */
170
    datatype NodeState = NodeState (
171
        blockchain: Blockchain,
172
        round: nat,
173
        localTime: nat,
174
        id: Address,
175
        configuration: Configuration,
176
        messagesReceived: set<QbftMessage>,
177
        proposalAcceptedForCurrentRound: Optional<QbftMessage>,
178
        lastPreparedBlock: Optional<Block>,
179
        lastPreparedRound: Optional<nat>,
180
        timeLastRoundStart: nat
181
    )
182
 
183
    /** =======================================================================
184
     * GENERAL TYPES
185
     *
186
     * This section includes the declaration of the types that have general
187
     * usage.
188
     *
189
     ========================================================================*/
190
    /**
191
     * This type is used to represent a single value that may be not present.
192
     */
193
    datatype Optional<T> = Optional(value:T) | None     
194
 
195
    type iseq<T> = x: imap<nat, T> | forall i: nat :: i in x.Keys witness *     
196
 
197
    /** =======================================================================
198
     * BEHAVIOUR TYPES
199
     *
200
     * This section includes the declaration of the types that are used to 
201
     * describe QBFT node behaviours.
202
     *
203
     ========================================================================*/    
204
 
205
    /**
206
     * This type represents a step of a QBFT node behaviour.
207
     * 
208
     * On a step, a node receives the set of messages `messageReceived` and in 
209
     * response it sends the set of messages `messagesToSend` and set its
210
     * blockchain to `newBlockchain`.
211
     */
212
    datatype QbftSpecificationStep = QbftSpecificationStep(
213
        messagesReceived: set<QbftMessage>,
214
        newBlockchain: Blockchain,
215
        messagesToSend: set<QbftMessageWithRecipient>
216
    )
217
 
218
    /**
219
     * This type represents a QBFT node behaviour.
220
     * 
221
     * `initialBlockchain` is the blockchain exposed by the QBFT node
222
     * at the very beginning and `steps` is the infinite sequence of steps composing
223
     * the behaviour of the QBFT node.
224
     */
225
    datatype QbftNodeBehaviour = QbftNodeBehaviour(
226
        initialBlockchain: Blockchain,
227
        steps: iseq<QbftSpecificationStep>
228
    )     
229
}

1.4 lemmas.dfy

This file does not provide any specification. It just contains lemmas that are used in the UponCommit and UponRoundChange predicates in 1.1 node.dfy when declaring sets via such-that assignment (:|) as the verifier is not able to automatically prove the existence of such sets.

Show the code.
Download this as Dafny 
1
/**
2
 * Copyright © 2021-2022 EEA Inc. 
3
 *
4
 * This document is available under the terms of the Apache 2.0 License
5
 * (http://www.apache.org/licenses/LICENSE-2.0.html)
6
 *
7
 * This file does provide any specification. It just contains lemmas that are
8
 * used in the `UponCommit` and `UponRoundChange` predicates in `node.dfy` when
9
 * declaring sets via such-that assignment (`:|`) as the verifier is not able to
10
 * automatically prove the existence of such sets.
11
 */
12
include "types.dfy"
13
include "node_auxiliary_functions.dfy"
14
 
15
module L1_Lemmas
16
{
17
    import opened L1_SpecTypes
18
    import opened L1_AuxiliaryFunctionsAndLemmas
19
 
20
    lemma lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsHelper1<T,T2>(s:set<T>, s2: set<T2>, f:T -> T2)
21
    requires s2 == set m | m in s :: f(m)
22
    ensures |s2| <= |s|
23
    {
24
        if s != {}
25
        {
26
            var e :| e in s;
27
            var news := s - {e};
28
            var news2 := set m | m in news :: f(m);
29
            lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsHelper1(news, news2,f);
30
 
31
            if f(e) in news2
32
            {
33
                assert s2 == news2;
34
            }
35
            else
36
            {
37
                assert |news2| < |s|;
38
                assert f(e) in s2;
39
                assert s2 == news2 + {f(e)};
40
                assert |s2| == |news2| + 1;
41
            }
42
        }
43
    }        
44
 
45
    lemma lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsHelper2<T,T2>(a:set<T>, b:set<T>, c:set<T2>, d:set<T2>, f:T -> T2)
46
    requires b < a
47
    requires |a| == |b| + 1
48
    requires c == set m | m in a :: f(m)
49
    requires d == set m | m in b :: f(m)
50
    ensures |d| == |c| || |c| == |d| + 1
51
    {
52
        var diff := a - b;
53
        assert |diff| == 1;
54
        var e :| e in diff;
55
        assert |diff-{e}| == 0;
56
        // assert d - {e} == {};
57
        assert diff == {e};
58
        assert b + {e} == a;
59
 
60
        if f(e) in d 
61
        {
62
            assert d == c;
63
            assert |d| == |c|;
64
        }
65
        else
66
        {
67
            assert c == d + {f(e)};
68
        }        
69
    }         
70
 
71
    lemma lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsHelper3<T,T2>(sM: set<T>, s1:set<T>, f:set<T> -> set<T2>, v:nat) returns (s2:set<T>)
72
    requires |f(s1)| >= v
73
    requires s1 <= sM
74
    requires forall a :: |f(a)| <= |a|
75
    requires forall a,b | b < a && |a| == |b| + 1  :: |f(a)| == |f(b)| || |f(a)| == |f(b)| + 1
76
    ensures s2  <= s1
77
    ensures |f(s2)| == v
78
    {
79
        if s1 == {} 
80
        {
81
            s2 := s1;
82
        }
83
        else if |f(s1)| == v 
84
        {
85
            s2 := s1;
86
        }
87
        else
88
        {
89
            var e :| e in s1;
90
            var news := s1 - {e};
91
            assert |news| == |s1| - 1;
92
 
93
            var s2r := lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsHelper3(sM,news,f,v);
94
            s2 := s2r;
95
        }
96
    }
97
 
98
    lemma lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsGeneric<T, T2>(
99
        s1: set<T>,
100
        fSetMap: set<T> -> set<T2>,
101
        fElMap: T -> T2,
102
        v: nat
103
    )
104
    requires exists s1' :: s1' <= s1 && |fSetMap(s1')| >= v
105
    // requires fSetMap == ((s: set<T>) => set m | m in s :: fElMap(m))
106
    requires forall s1' :: fSetMap(s1') == set m | m in s1' :: fElMap(m)
107
    ensures exists s2 :: s2 <= s1 && |fSetMap(s2)| == v  
108
    {
109
        forall a 
110
        ensures |fSetMap(a)| <= |a|
111
        {
112
            lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsHelper1(a, fSetMap(a), fElMap);
113
        }        
114
 
115
        forall a,b | b < a && |a| == |b| + 1 
116
        ensures |fSetMap(a)| == |fSetMap(b)| || |fSetMap(a)| == |fSetMap(b)| + 1
117
        {
118
            lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsHelper2(a,b,fSetMap(a),fSetMap(b),fElMap);
119
        }             
120
 
121
        var s1' :| s1' <= s1 && |fSetMap(s1')| >= v;
122
        var s2 := lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsHelper3(s1, s1', fSetMap, v);             
123
    }  
124
 
125
    lemma lemmaToProveExistenceOfSetFrc(
126
        signedRoundChangesReceived: set<SignedRoundChange>,
127
        v: nat
128
    )
129
    requires exists s1 :: s1 <= signedRoundChangesReceived && |getSetOfRoundChangeSenders(s1)| >= v
130
    ensures exists s3 :: s3 <= signedRoundChangesReceived && |getSetOfRoundChangeSenders(s3)| == v  
131
    {
132
        lemmaIfMappedSubSetOfGreaterSizeExistsThenMappedSmallSubsetExistsGeneric(signedRoundChangesReceived, getSetOfRoundChangeSenders, recoverSignedRoundChangeAuthor, v);           
133
    }  
134
 
135
    lemma lemmaIfSubSetOfGreaterSizeExistsThenSmallSubsetExistsHelper<T>(s1:set<T>, s2:set<T>, sz1:nat) returns (s3:set<T>)
136
    requires s1 <= s2    
137
    requires |s1| >= sz1
138
    ensures s3 <= s2
139
    ensures |s3| == sz1
140
    {
141
        if |s1| == sz1
142
        {
143
            s3 := s1;
144
        }
145
        else
146
        {
147
            var e :| e in s1;
148
            var s1Sub := s1 - {e};
149
            s3 := lemmaIfSubSetOfGreaterSizeExistsThenSmallSubsetExistsHelper(s1Sub,s2,sz1);
150
        }
151
    }
152
 
153
    lemma lemmaIfSubSetOfGreaterSizeExistsThenSmallSubsetExists<T>(s2:set<T>, sz1:nat)
154
    requires exists s1 ::   && s1 <= s2    
155
                            && |s1| >= sz1
156
    ensures exists s3 ::    && s3 <= s2
157
                            && |s3| == sz1    
158
    {
159
        var s1 :| && s1 <= s2    
160
                            && |s1| >= sz1;
161
        var s3 := lemmaIfSubSetOfGreaterSizeExistsThenSmallSubsetExistsHelper(s1,s2,sz1);
162
    }
163
    
164
}

A. Additional Information

A.1 Defined Terms

The following is a list of terms defined in this Specification.

A.2 Acknowledgments

The EEA acknowledges and thanks the many people who contributed to the development of this version of the specification. Please advise us of any errors or omissions.

Enterprise Ethereum is built on top of Ethereum, and we are grateful to the entire community who develops Ethereum, for their work and their ongoing collaboration to helps us maintain as much compatibility as possible with the Ethereum ecosystem.

B. References

B.1 Informative references

[Apache2]
Apache license version 2.0. The Apache Software Foundation. URL: http://www.apache.org/licenses/LICENSE-2.0
[Dafny]
Dafny Reference Manual. K. Rustan M. Leino; Richard L. Ford; David R. Cok. Microsoft. URL: https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef
[IBFT-Moniz]
The Istanbul BFT Consensus Algorithm. Henrique Moniz. CoRR. URL: https://arxiv.org/abs/2002.03613
[TLA]
The temporal logic of actions. L. Lamport. ACM Transactions on Programming Languages and Systems. URL: https://dl.acm.org/doi/10.1145/177492.177726