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)

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