-
Notifications
You must be signed in to change notification settings - Fork 2
/
HotStuff.txt
133 lines (111 loc) · 3.67 KB
/
HotStuff.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
type BlockId
type Block = struct {
parent: BlockId,
height: uint,
justify: BlockId,
}
function Hash(Block): BlockId
const blocks: [BlockId]Block
axiom forall id: BlockId. Hash(blocks[id]) == id
const h: uint // number of honest replicas
const f: uint // number of faulty replicas
axiom h > 2f
const root: BlockId // root of block tree
axiom blocks[root].height == 0 && blocks[root].parent == root && blocks[root].justify == root
type HonestReplicaId = 1..h // ids of honest replicas
//// global model variables
// all collected votes sent by honest replicas
// initial value: lambda id: BlockId. {}
var voteStore: [BlockId][HonestReplicaId]bool
// id of the latest globally-committed block
// initial value: root
var committed: BlockId
//// per-replica state
// monotonically increasing height of the last voted block
// initial value: 0
var vheight: uint
// id of the locked block
// initial value: root
var lockedBlockId: BlockId
// id of the latest locally-committed block
// initial value: root
var locallyCommitted: BlockId
// primitive function that evaluates as follows:
// if id' can reach id by following parent link 0 or more times, then set of all nodes along the path (id' and id inclusive)
// otherwise, empty set
function Between(id': BlockId, id: BlockId) : [BlockId]bool
function Reaches(id': BlockId, id: BlockId): bool {
Between(id', id) != {}
}
function Extends(newProposalId: BlockId, lockedBlockId: BlockId) : bool {
Reaches(newProposalId, lockedBlockId) &&
(forall id in Between(newProposalId, lockedBlockId).
id == lockedBlockId || blocks[id].height == blocks[blocks[id].parent].height + 1)
}
function Consistent(id': BlockId, id: BlockId) : bool {
Reaches(id', id) || Reaches(id, id')
}
//// start things off
procedure Main() {
var r: HonestReplicaId
var newBlockId: BlockId
async OnReceiveProposal(r, newBlockId)
if * {
async Main()
}
}
//// top-level event handler at a replica to update vheight and "send" vote
procedure OnReceiveProposal(r: HonestReplicaId, newBlockId: BlockId)
reads voteStore, vheight, lockedBlockId
writes voteStore, vheight, lockedBlockId
{
var newBlock: Block
var numEquivocators: uint;
assume numEquivocators <= f;
newBlock := blocks[newBlockId]
if card(voteStore[newBlock.justify]) + numEquivocators < h {
return
}
if newBlock.height > vheight[r] &&
(Extends(newBlockId, lockedBlockId[r]) ||
blocks[newBlock.justify].height > blocks[lockedBlockId[r]].height) {
vheight[r] := newBlock.height
voteStore[newBlockId][r] := true
}
Update(r, newBlock.justify)
}
//// update lockedBlockId and make the async call to commit the 3-chain head
procedure Update(r: HonestReplicaId, id'': BlockId)
reads lockedBlockId
writes lockedBlockId
{
var id', id: BlockId
var b'', b', b: Block
b'' := blocks[id'']
id' := b''.justify
b' := blocks[id']
id := b'.justify
b := blocks[id]
if b'.height > blocks[lockedBlockId[r]].height {
lockedBlockId[r] := id'
}
if b''.parent == id' && b'.parent == id {
async Commit(r, id)
}
}
//// internal event handler at a replica to update locallyCommitted and committed
//// and assert consensus safety
procedure Commit(r: HonestReplicaId, id: BlockId)
reads locallyCommitted, committed
writes locallyCommitted, committed
{
// the fact stated below is preserved by the body of Commit
// (forall x: HonestReplicaId. Reaches(committed, locallyCommitted[x]))
assert Consistent(id, committed)
if Reaches(id, locallyCommitted[r]) {
locallyCommitted[r] := id
}
if Reaches(id, committed) {
committed := id
}
}