-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSCP2.ivy
201 lines (173 loc) · 11.7 KB
/
SCP2.ivy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
#lang ivy1.7
# Nomination and federated-voting are black-boxes whose properties are assumed
include order
object protocol = {
type node
relation well_behaved(N:node)
relation intact(N:node)
axiom ~(intact(N) & ~well_behaved(N))
instance value : bounded_sequence(nat)
instance ballot : bounded_sequence(nat)
relation vote_prepare(N:node, B:ballot, V:value)
relation confirmed_prepared(N:node, B:ballot, V:value)
relation vote_commit(N:node, B:ballot, V:value)
relation confirmed_committed(N:node, B:ballot, V:value)
relation nomination_output(N:node, V:value)
relation started(N:node, B:ballot)
relation left_ballot(N:node, B:ballot)
relation voted_prepared(N:node, B:ballot) # projection of vote_prepare?
invariant [safety] ~(intact(N1) & intact(N2) & confirmed_committed(N1,B1,V1) & confirmed_committed(N2,B2,V2) & V1 ~= V2)
invariant ~(vote_commit(N1,B1,V) & intact(N1) & ~confirmed_prepared(N1,B1,V))
invariant ~(intact(N1) & intact(N2) & confirmed_committed(N1,B1,V1) & B1 <= B2 & V1 ~= V2 & confirmed_prepared(N2,B2,V2))
#invariant intact(N1) & intact(N2) & confirmed_committed(N1,B1,V1) & B1 <= B2 & V1 ~= V2 -> ~confirmed_prepared(N2,B2,V2)
invariant ~(intact(N1) & confirmed_committed(N1,B,V) & forall N2 . intact(N2) -> ~vote_commit(N2,B,V))
invariant ~(left_ballot(N,B) & B2 < B & ~left_ballot(N,B2))
invariant ~(intact(N) & started(N,B) & B0 < B & ~left_ballot(N,B0))
after init {
vote_prepare(N,B,V) := false;
confirmed_prepared(N,B,V) := false;
vote_commit(N,B,V) := false;
confirmed_committed(N,B,V) := false;
nomination_output(N,X) := false;
left_ballot(N,B) := false;
started(N,B) := false;
voted_prepared(N,B) := false;
# there are finitely many nodes:
l2s_d(N:node) := true;
}
## Basic actions
action byz_action = {
vote_prepare(N,B,X) := *;
assume ~(well_behaved(N) & (vote_prepare(N,B,X) ~= old vote_prepare(N,B,X)));
vote_commit(N,B,X) := *;
assume ~(well_behaved(N) & (vote_commit(N,B,X) ~= old vote_commit(N,B,X)));
confirmed_prepared(N,B,V) := *;
assume ~(well_behaved(N) & (confirmed_prepared(N,B,X) ~= old confirmed_prepared(N,B,X)));
confirmed_committed(N,B,V) := *;
assume ~(well_behaved(N) & (confirmed_committed(N,B,X) ~= old confirmed_committed(N,B,X)));
}
action change_ballot(n:node, b:ballot) = {
assume ~left_ballot(n,b);
left_ballot(n,B) := B < b;
started(n,b) := true;
# vote to commit stuff that has already been prepared
vote_commit(n,b,V) := confirmed_prepared(n,b,V);
}
action nomination_update(n:node, v:value) = {
nomination_output(n, V) := V = v
}
action prepare(n:node, b:ballot, bmax:ballot, vmax:value) = {
assume ~left_ballot(n,b);
assume started(n,b);
assume ~vote_prepare(n,b,V);
# use the highest confirmed prepared value or, if none exists, the nomination output:
assume
((forall B,V . B < b -> ~confirmed_prepared(n,B,V)) & nomination_output(n,vmax))
| (bmax < b & confirmed_prepared(n,bmax,vmax) & (forall B,V . B < b & confirmed_prepared(n,B,V) -> (B < bmax | (B = bmax & V <= vmax))));
vote_prepare(n, b, vmax) := true;
voted_prepared(n,b) := true;
}
action confirm_commit(n:node, b:ballot, v:value) = {
# assumptions come from the specification of federated voting:
assume exists N . intact(N) & vote_commit(N,b,v);
assume intact(N) & b <= B & V ~= v -> ~confirmed_prepared(N,B,V);
confirmed_committed(n,b,v) := true;
}
action confirm_prepare(n:node, b:ballot, v:value) = {
# assumptions come from the specification of federated voting:
assume exists N . intact(N) & vote_prepare(N,b,v);
assume intact(N) & B <= b & V ~= v -> ~confirmed_committed(N,B,V);
confirmed_prepared(n,b,v) := true;
if (~left_ballot(n,b) & started(n,b)) {
vote_commit(n, b, v) := true;
}
}
export change_ballot
export confirm_commit
export byz_action
export nomination_update
export confirm_prepare
export prepare
isolate safety_proof = protocol with ballot
isolate liveness = {
individual b0:ballot # the good ballot
individual n0:node # the node that never confirms v0 or v1
individual v0:value # nomination output at b0
individual v1:value # highest prepared at b0
individual n1:node # node that prepares v1
individual b1:ballot # corresponding ballot
# relation prepared(B:ballot, V:value)
# definition prepared(B:ballot, V:value) = B < b0 & (exists N . intact(N) & confirmed_prepared(N,B,V))
# relation highest_prepared(B:ballot, V:value)
# definition highest_prepared(B,V) = prepared(B,V)
# & (forall V2,B2 . prepared(B2,V2) -> (B2 < B | (B2 = B & V2 <= V)))
object spec = {
temporal property (
# if all intact nodes vote to prepare B,V then eventually all intact nodes confirm B,V as prepared
(forall B,V,N1 . intact(N1) -> globally ((forall N2 . intact(N2) -> vote_prepare(N2,B,V)) -> eventually confirmed_prepared(N1,B,V))) &
# b0 eventually starts:
(forall N . intact(N) -> eventually started(N,b0)) &
# intact nodes eventually vote to prepare something in b0:
(forall N . intact(N) -> eventually voted_prepared(N,b0)) &
# ballot b0 never ends (this is how we model that b0 is long enough):
(forall N . intact(N) -> globally ~left_ballot(N,b0)) &
# v0 is nominated by all intact at b0:
(forall N . intact(N) -> (globally (started(N,b0) -> nomination_output(N,v0)))) &
# v0 is the unanimous nomination output at b0:
(forall N1,N2,V1,V2 . globally (intact(N1) & intact(N2) & started(N1,b0) & started(N2,b0) & nomination_output(N1,V1) & nomination_output(N2,V2) -> V1 = V2)) &
# all intact nodes have confirmed the same things when entering b0:
(forall B,N1,N2,V . B < b0 & intact(N1) & intact(N2) -> globally (started(N1,b0) & started(N2,b0) & confirmed_prepared(N1,B,V) -> confirmed_prepared(N2,B,V))) &
# no old confirmations happen during b0:
(forall N . globally intact(N) & started(N,b0) & B < b0 & ~confirmed_prepared(N,B,V) -> globally ~confirmed_prepared(N,B,V)) &
# witnesses:
## if there is a highest confirmed prepared value below b0, then it is v1 at ballot b1:
(forall N,B,V . globally B < b0 & intact(N) & started(N,b0) & confirmed_prepared(N,B,V) -> (b1 < b0 & intact(n1) & started(n1,b0) & confirmed_prepared(n1,b1,v1) & (B < b1 | (B = b1 & V2 <= v1)))) &
## if there is a node that never confirms v0 or v1 at b0, then this node is n0:
(forall N . (intact(N) & globally ~(confirmed_committed(N,b0,v1) | confirmed_committed(N,b0,v0))) -> (intact(n0) & globally ~(confirmed_committed(n0,b0,v1) | confirmed_committed(n0,b0,v0))))
)
-> forall N . intact(N) -> exists B,V . eventually confirmed_committed(N,B,V)
}
object impl = {
# basic temporal info (this follow directly from the assumptions):
invariant intact(N1) -> globally ((forall N2 . intact(N2) -> vote_prepare(N2,B,V)) -> eventually confirmed_prepared(N1,B,V))
invariant intact(N) -> eventually started(N,b0)
invariant intact(N) -> eventually voted_prepared(N,b0)
invariant intact(N) -> globally ~left_ballot(N,b0)
invariant intact(N) -> (globally (started(N,b0) -> nomination_output(N,v0)))
invariant globally (intact(N1) & intact(N2) & started(N1,b0) & started(N2,b0) & nomination_output(N1,V1) & nomination_output(N2,V2) -> V1 = V2)
invariant B < b0 & intact(N1) & intact(N2) -> globally (started(N1,b0) & started(N2,b0) & confirmed_prepared(N1,B,V) -> confirmed_prepared(N2,B,V))
invariant forall N . globally intact(N) & started(N,b0) & B < b0 & ~confirmed_prepared(N,B,V) -> globally ~confirmed_prepared(N,B,V)
invariant forall N,B,V . globally B < b0 & intact(N) & started(N,b0) & confirmed_prepared(N,B,V) -> (b1 < b0 & intact(n1) & started(n1,b0) & confirmed_prepared(n1,b1,v1) & (B < b1 | (B = b1 & V2 <= v1)))
invariant (intact(N) & globally ~(confirmed_committed(N,b0,v1) | confirmed_committed(N,b0,v0))) -> (intact(n0) & globally ~(confirmed_committed(n0,b0,v1) | confirmed_committed(n0,b0,v0)))
# the initial footprint
invariant l2s_d(N:node) & l2s_d(b0) & l2s_d(v0) & l2s_d(n0) & l2s_d(b1) & l2s_d(v1) & l2s_d(n1)
# intact nodes vote to prepare v0 xor v1 at b0 by the freeze point
invariant intact(N) & ~($l2s_w N . started(N,b0))(N) -> started(N,b0)
invariant intact(N) -> ~left_ballot(N,b0)
invariant intact(N) & started(N,b0) -> nomination_output(N,v0)
invariant intact(N) & started(N,b0) & nomination_output(N,V) -> V=v0
invariant intact(N) & B < b0 & intact(N2) & started(N,b0) & started(N2,b0) & confirmed_prepared(N,B,V) -> confirmed_prepared(N2,B,V)
# (b1,v1) is the highest confirmed prepared value among intact nodes:
invariant intact(N) & started(N,b0) & B < b0 & confirmed_prepared(N,B,V) -> (B < b1 | (B = b1 & V2 <= v1)) & intact(n1) & b1 < b0 & confirmed_prepared(n1,b1,v1)
invariant intact(N) & voted_prepared(N,B) -> started(N,B)
invariant intact(N) & vote_prepare(N,B,V) & vote_prepare(N,B,V2) -> V = V2
invariant intact(N) & vote_prepare(N,b0,V) -> (vote_prepare(N,b0,v0) | vote_prepare(N,b0,v1))
invariant intact(N) & vote_prepare(N,B,V) -> voted_prepared(N,B)
invariant intact(N) & voted_prepared(N,b0) & B < b0 & confirmed_prepared(N,B,V) -> vote_prepare(N,b0,v1)
invariant intact(N1) & intact(N2) & B < b0 & started(N2,b0) & confirmed_prepared(N2,B,V) & voted_prepared(N1,b0) -> vote_prepare(N1,b0,v1)
invariant ~(intact(N) & (v0 ~= v1) & vote_prepare(N,b0,v1) & ~(b1 < b0 & confirmed_prepared(N,b1,v1)))
invariant ~(intact(N) & (v0 ~= v1) & vote_prepare(N,b0,v0) & intact(N2) & started(N2,b0) & confirmed_prepared(N2,B,V) & B < b0)
invariant intact(N1) & intact(N2) & vote_prepare(N1,b0,V1) & vote_prepare(N2,b0,V2) -> V1 = V2
invariant l2s_waiting & intact(N) & ~($l2s_w N . voted_prepared(N,b0))(N) -> voted_prepared(N,b0)
invariant intact(N) & voted_prepared(N,b0) -> (vote_prepare(N,b0,v0) | vote_prepare(N,b0,v1))
# invariant l2s_waiting -> ( (forall N . intact(N) & ~($l2s_w N,B,V . confirmed_prepared(N,B,V))(N,b0,v0) -> confirmed_prepared(N,b0,v0)) | (forall N . intact(N) & ~($l2s_w N,B,V . confirmed_prepared(N,B,V))(N,b0,v1) -> confirmed_prepared(N,b0,v1))
)
# invariant ~l2s_waiting & intact(N) -> (vote_prepare(N,b0,v0) | vote_prepare(N,b0,v1))
# After the save point, we wait for confirmed_prepared(N,b0,V) where V=v1 or V=v0
# invariant l2s_saved -> (($l2s_s N . intact(N))(N) <-> intact(N))
# invariant ~l2s_waiting -> l2s_a(N:node) & l2s_a(b0) & l2s_a(v0) & l2s_a(n0) & l2s_a(b1) & l2s_a(v1) & l2s_a(n1)
# invariant l2s_saved & B=b0 & intact(N) -> ((V = v0 & ~($l2s_w N,B,V . confirmed_prepared(N,B,V))(N,B,V) -> (confirmed_prepared(N,B,V) | (globally ~confirmed_prepared(N,B,V)))) | (V = v1 & ~($l2s_w N,B,V . confirmed_prepared(N,B,V))(N,B,V) -> (confirmed_prepared(N,B,V) | (globally ~confirmed_prepared(N,B,V)))))
# invariant intact(N) & confirmed_prepared(N,B,V) & ~left_ballot(N,B) & started(N,B) -> vote_commit(N,B,V)
}
} with this, ballot, value
}