-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSCP.ivy
175 lines (136 loc) · 6.91 KB
/
SCP.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
#lang ivy1.7
# SCP with explicit slices
include order
type node
relation well_behaved(N:node)
relation intertwined(N:node)
type nset # node sets
relation member(N:node, Q:nset)
relation nset_subseteq(Q1:nset, Q2:nset)
type slice
relation slice_of(N:node, S:slice)
relation slice_member(N:node, S:slice)
relation slice_subseteq_nset(S:slice, Q:nset)
relation is_quorum(Q:nset) # defined below in terms of slices
instance value : bounded_sequence(nat)
instance round : bounded_sequence(nat)
type ballot = struct {
n:round,
x:value
}
# type statement = {abort, commit}
type statement
individual commit:statement
individual abort:statement
trusted isolate commit_abort_iso = {
property commit ~= abort
property X = commit | X = abort
}
isolate fbas_axiomatization = {
# quorum intersection:
axiom (exists N1 . intertwined(N1) & is_quorum(Q1) & member(N1,Q1)) & (exists N2 . intertwined(N2) & is_quorum(Q2) & member(N2,Q2)) -> exists N3 . well_behaved(N3) & member(N3,Q1) & member(N3,Q2)
axiom ~(intertwined(N) & ~well_behaved(N))
axiom slice_of(N,S) & well_behaved(N) -> slice_member(N,S) # assumed in Isabelle/HOL
axiom well_behaved(N) -> exists S . slice_of(N,S) # assumed in Isabelle/HOL
# two shorthands:
definition slice_subseteq_nset(S,Q) = forall N . slice_member(N,S) -> member(N,Q)
definition nset_subseteq(Q1,Q2) = forall N . member(N,Q1) -> member(N,Q2)
definition is_quorum(Q:nset) = forall N . member(N,Q) & well_behaved(N) -> exists S . slice_of(N,S) & (forall N . slice_member(N,S) -> member(N,Q)) # here we get a QA cycle between slice and node with the axiom that says that every well-behaved node has a slice
}
isolate ballot_order = {
definition (B1 < B2) = (n(B1) < n(B2)) | (n(B1) = n(B2) & x(B1) < x(B2))
definition (B1:ballot <= B2) = (B1 < B2 | B1 = B2)
instantiate totally_ordered(ballot)
} with value, round
isolate simple_ballot_protocol = {
relation vote(N:node, B:ballot, S:statement)
relation accept(N:node, B:ballot, S:statement)
relation confirm(N:node, B:ballot, S:statement)
trusted isolate skip_slices = {
# lemma asserting that it is safe to omit the slices of a node reporting a commit from the quorum computation
# proved in Isabelle/HOL
action lemma(v:node, q:nset, b:ballot, s:statement) = {
require well_behaved(v);
require (exists N . well_behaved(N) & confirm(N,B,commit)) -> exists Q . (exists N . well_behaved(N) & member(N,Q)) & is_quorum(Q) & (forall N . well_behaved(N) & member(N,Q) -> accept(N,B,commit));
require member(N,q) -> ((accept(N,b,s) & exists S . slice_of(N,S) & slice_subseteq_nset(S,q)) | confirm(N,b,s));
ensure exists Q . member(v,Q) & is_quorum(Q) & (forall N . member(N,Q) -> accept(N,b,s))
}
}
# ghost vars (do not affect non-ghost vars):
individual confirmed_commit:bool
individual the_b:ballot
## Invariants
# note that invariants do not say anything about ill-behaved nodes; therefore we do not bother to model their behavior
invariant [safety] ~(intertwined(N1) & intertwined(N2) & confirm(N1,B1,commit) & confirm(N2,B2,commit) & x(B1) ~= x(B2))
private { # together with safety, the following invariants form an inductive invariant
# the main invariant:
invariant (exists N . intertwined(N) & accept(N,B2,commit)) & B1 < B2 & x(B1) ~= x(B2) -> (
(exists N . intertwined(N) & confirm(N,B1,abort)) | (confirmed_commit & the_b <= B1 & x(the_b) = x(B2)) )
invariant confirmed_commit -> (exists N . intertwined(N) & confirm(N,the_b,commit))
invariant intertwined(N) & confirm(N,B,commit) -> confirmed_commit & the_b <= B
invariant ~(well_behaved(N) & accept(N,B,S1) & accept(N,B,S2) & S1 ~= S2)
invariant ~(intertwined(N1) & intertwined(N2) & confirm(N1,B1,S1) & confirm(N2,B1,S2) & S1 ~= S2)
invariant (exists N . well_behaved(N) & confirm(N,B,commit)) -> exists Q . (exists N . well_behaved(N) & member(N,Q)) & is_quorum(Q) & forall N . well_behaved(N) & member(N,Q) -> accept(N,B,commit)
invariant (exists N1 . intertwined(N1) & confirm(N1,B1,S1)) -> exists Q . is_quorum(Q) & (exists N3 . intertwined(N3) & member(N3,Q)) & forall N2 . well_behaved(N2) & member(N2,Q) -> accept(N2,B1,S1)
}
after init {
vote(N,B,S) := false;
accept(N,B,S) := false;
confirm(N,B,S) := false;
confirmed_commit := false;
}
relation condition_accept(N:node, B:ballot, S:statement)
# note that the second conjunct has no effect on safety
definition condition_accept(V:node, B:ballot, S:statement) =
(forall S2 . ~accept(V,B,S2)) & (
(exists Q . is_quorum(Q) & member(V,Q) & forall N . member(N,Q) -> (vote(N,B,S) | accept(N,B,S))) )
relation condition_vote(N:node, B:ballot, S:statement)
definition condition_vote(V:node, B:ballot, S:statement) =
forall S2 . ~(vote(V,B,S2) & S ~= S2)
relation condition_confirm(Q:nset, N:node, B:ballot, S:statement)
definition condition_confirm(q:nset, v:node, b:ballot, s:statement) =
member(v,q) & ((s = abort & is_quorum(q) & forall N . member(N,q) -> accept(N,b,s)) | (s = commit & (forall N . member(N,q) -> ((accept(N,b,s) & exists S . slice_of(N,S) & slice_subseteq_nset(S,q)) | confirm(N,b,s)))))
# QA cycle involving slice and node: made it a macro.
## Basic actions
# note that votes have no effect on safety
action vote_abort(n:node, b:ballot) = {
# require condition_vote(n,b,abort);
vote(n,b,abort) := true;
}
# note that votes have no effect on safety
action vote_commit(n:node, b:ballot) = {
# require B < b & x(B) ~= x(b) -> confirm(n,B,abort);
# require condition_vote(n,b,commit);
vote(n,b,commit) := true;
}
action do_accept(v:node, b:ballot, s:statement) = {
require condition_accept(v,b,s);
# the following should be an invariant due to phasing:
require B < b & x(B) ~= x(b) & s = commit -> confirm(v,B,abort);
accept(v,b,s) := true;
}
action do_confirm(q:nset, v:node, b:ballot, s:statement) = {
require condition_confirm(q,v,b,s);
# ghost call:
if (well_behaved(v) & s = commit) {
call skip_slices.lemma(v, q, b, s);
};
confirm(v,b,s) := true;
# ghost update:
if (intertwined(v) & s = commit & (~confirmed_commit | (confirmed_commit & b < the_b))) {
confirmed_commit := true;
the_b := b;
}
}
action accept_after_confirm(v:node, b:ballot, cb:ballot) = {
require confirm(v, cb, commit);
require cb < b & cb.x = b.x;
require ~accept(v,b,abort);
accept(v,b,commit) := true;
}
export vote_abort
export vote_commit
export do_accept
export do_confirm
export accept_after_confirm
} with value, round, ballot_order, fbas_axiomatization, commit_abort_iso, simple_ballot_protocol.skip_slices