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
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
|
; AleoBFT Library
;
; Copyright (C) 2024 Provable Inc.
;
; License: See the LICENSE file distributed with this library.
;
; Authors: Alessandro Coglio (www.alessandrocoglio.info)
; Eric McCarthy (bendyarm on GitHub)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ALEOBFT-STAKE2")
(include-book "certificates")
(include-book "dags")
(include-book "committees")
(local (include-book "../library-extensions/oset-theorems"))
(local (include-book "kestrel/built-ins/disable" :dir :system))
(local (acl2::disable-most-builtin-logic-defuns))
(local (acl2::disable-builtin-rewrite-rules-for-defaults))
(set-induction-depth-limit 0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defxdoc+ successor-predecessor-intersection
:parents (correctness)
:short "Intersection of successors and predecessors."
:long
(xdoc::topstring
(xdoc::p
"This is the second key intersection argument
for the correctness of AleoBFT,
besides "
(xdoc::seetopic "quorum-intersection" "quorum intersection")
". However, this second argument is very different:
it has nothing to do with correct and faulty validators;
it only has to do with paths in DAGs.
When an anchor @($A$) at a round @($r$)
has enough voting stake from the successors at round @($r+1$),
then if there is a certificate @($C$) at round @($r+2$)
then there must be a certificate @($B$) at round @($r+1$)
that is both a successor (i.e. voter) of @($A$)
and a predecessor of @($C$).
This actually also applies across differnt DAGs:
@($A$) is in DAG 1,
@($C$) is in DAG 2,
and @($B$) is in both DAG 1 and DAG 2.
The case in which DAGs 1 and 2 are the same is a special case.")
(xdoc::p
"Here we prove the non-emptiness of the intersection,
and we introduce a function to pick
a common certificate from the intersection.
This is then used in further proofs.")
(xdoc::p
"Here we talk about successors and predecessors,
not specifically voters and anchors,
because the argument is more general."))
:order-subtopics t
:default-parent t)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defruled not-empty-successor-predecessor-author-intersection
:short "Non-empty intersection of successor and predecessor authors."
:long
(xdoc::topstring
(xdoc::p
"Here @('n') and @('f') are
the @($n$) and @($f$) mentioned in @(tsee max-faulty-for-total).
Here @('successors-vals') represents
the authors of the successors of @($A$),
while @('predecessors') represents
the authors of the predecessors of @($C$),
with reference to @(see successor-predecessor-intersection).")
(xdoc::p
"If (i) the total stake of successor and predecessor authors
is bounded by @('n'),
(ii) the total stake of the successor authors
is more than @('f'),
and (iii) the total stake of the predecessor authors
is at least @('n - f'),
then in order for the two sets to have no intersection
their total stake would have to be more than @('n'),
which contradicts the first hypothesis.
So there must be at least one in the intersection."))
(implies (and (address-setp successor-vals)
(address-setp predecessor-vals)
(<= (committee-members-stake (set::union successor-vals
predecessor-vals)
commtt)
n)
(> (committee-members-stake successor-vals commtt)
f)
(>= (committee-members-stake predecessor-vals commtt)
(- n f)))
(not (set::emptyp (set::intersect successor-vals
predecessor-vals))))
:enable committee-members-stake-of-intersect
:use (:instance committee-members-stake-0-to-emptyp-members
(members (set::intersect successor-vals predecessor-vals))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defruled successors+predecessors-same-round
:short "Successors and predecessors have all the same round."
:long
(xdoc::topstring
(xdoc::p
"This is used to establish
a hypothesis of @(tsee not-empty-successor-predecessor-intersection).
If (again with reference to @(see successor-predecessor-intersection))
@($A$) and @($C$) are two rounds apart,
then the successors of @($A$) and the predecessors of @($C$)
are all in the round between those two rounds."))
(implies (and (certificate-setp dag1)
(certificate-setp dag2)
(equal (certificate->round cert2)
(+ 2 (certificate->round cert1))))
(<= (set::cardinality
(certificate-set->round-set
(set::union (successors cert1 dag1)
(predecessors cert2 dag2))))
1))
:rule-classes :linear
:enable (set::cardinality
certificate-set->round-set-of-successors
certificate-set->round-set-of-predecessors
certificate-set->round-set-of-union))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defruled not-empty-successor-predecessor-intersection
:short "Non-empty intersection of successors and predecessors"
:long
(xdoc::topstring
(xdoc::p
"This lifts @(tsee not-empty-successor-predecessor-author-intersection)
from the authors,
over which stake is calculated,
to the certificates,
which are the ones whose non-empty intersection we need to show.
With reference to @(see successor-predecessor-intersection),
here @('cert1') is @($A$) and @('cert2') is @($C$);
we show that the successors of @($A$) and the predecessors of @($C$)
have a non-empty intersection.
The key theorem used in the proof is
@('certs-same-round-unequiv-intersect-when-authors-intersect')."))
(implies (and (certificate-setp dag1)
(certificate-setp dag2)
(certificate-set-unequivocalp dag1)
(certificate-set-unequivocalp dag2)
(certificate-sets-unequivocalp dag1 dag2)
(equal (certificate->round cert2)
(+ 2 (certificate->round cert1)))
(set::subset (certificate-set->author-set
(successors cert1 dag1))
(committee-members commtt))
(set::subset (certificate-set->author-set
(predecessors cert2 dag2))
(committee-members commtt))
(> (committee-members-stake
(certificate-set->author-set
(successors cert1 dag1))
commtt)
(committee-max-faulty-stake commtt))
(>= (committee-members-stake
(certificate-set->author-set
(predecessors cert2 dag2))
commtt)
(committee-quorum-stake commtt)))
(not (set::emptyp (set::intersect (successors cert1 dag1)
(predecessors cert2 dag2)))))
:enable (committee-quorum-stake
committee-total-stake
committee-members-stake-monotone
certificate-set-unequivocalp-of-union
certificate-set-unequivocalp-when-subset
certificate-sets-unequivocalp-when-subsets
successors+predecessors-same-round
certs-same-round-unequiv-intersect-when-authors-intersect)
:use (:instance not-empty-successor-predecessor-author-intersection
(successor-vals (certificate-set->author-set
(successors cert1 dag1)))
(predecessor-vals (certificate-set->author-set
(predecessors cert2 dag2)))
(n (committee-total-stake commtt))
(f (committee-max-faulty-stake commtt))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define pick-successor/predecessor ((dag1 certificate-setp)
(dag2 certificate-setp)
(cert1 certificatep)
(cert2 certificatep))
:guard (and (set::in cert1 dag1)
(set::in cert2 dag2)
(equal (certificate->round cert2)
(+ 2 (certificate->round cert1))))
:returns (cert? certificate-optionp)
:short "Pick a certificate in the successor-predecessor intersection."
:long
(xdoc::topstring
(xdoc::p
"We pick the first one, but the exact choice does not matter.
We show that, under the assumptions in
@(tsee not-empty-successor-predecessor-intersection),
this function returns a certificate that is
in the successors, in the predecessors, and in both DAGs."))
(b* ((common (set::intersect (successors cert1 dag1)
(predecessors cert2 dag2))))
(if (set::emptyp common)
nil
(set::head common)))
///
(defruled pick-successor/predecessor-in-successors
(implies (pick-successor/predecessor dag1 dag2 cert1 cert2)
(set::in (pick-successor/predecessor dag1 dag2 cert1 cert2)
(successors cert1 dag1)))
:enable set::head-of-intersect-member-when-not-emptyp)
(defruled pick-successor/predecessor-in-predecessors
(implies (pick-successor/predecessor dag1 dag2 cert1 cert2)
(set::in (pick-successor/predecessor dag1 dag2 cert1 cert2)
(predecessors cert2 dag2)))
:enable set::head-of-intersect-member-when-not-emptyp)
(defruled pick-successor/predecessor-in-dag1
(implies (and (certificate-setp dag1)
(pick-successor/predecessor dag1 dag2 cert1 cert2))
(set::in (pick-successor/predecessor dag1 dag2 cert1 cert2)
dag1))
:use (:instance successors-subset-of-dag (cert cert1) (dag dag1))
:enable (pick-successor/predecessor-in-successors
set::expensive-rules)
:disable (pick-successor/predecessor
successors-subset-of-dag))
(defruled pick-successor/predecessor-in-dag2
(implies (and (certificate-setp dag2)
(pick-successor/predecessor dag1 dag2 cert1 cert2))
(set::in (pick-successor/predecessor dag1 dag2 cert1 cert2)
dag2))
:use (:instance predecessors-subset-of-dag (cert cert2) (dag dag2))
:enable (pick-successor/predecessor-in-predecessors
set::expensive-rules)
:disable (pick-successor/predecessor
predecessors-subset-of-dag))
(defruled pick-successor/predecessor-not-nil
(implies (and (certificate-setp dag1)
(certificate-setp dag2)
(certificate-set-unequivocalp dag1)
(certificate-set-unequivocalp dag2)
(certificate-sets-unequivocalp dag1 dag2)
(equal (certificate->round cert2)
(+ 2 (certificate->round cert1)))
(set::subset (certificate-set->author-set
(successors cert1 dag1))
(committee-members commtt))
(set::subset (certificate-set->author-set
(predecessors cert2 dag2))
(committee-members commtt))
(> (committee-members-stake
(certificate-set->author-set
(successors cert1 dag1))
commtt)
(committee-max-faulty-stake commtt))
(>= (committee-members-stake
(certificate-set->author-set
(predecessors cert2 dag2))
commtt)
(committee-quorum-stake commtt)))
(pick-successor/predecessor dag1 dag2 cert1 cert2))
:use (not-empty-successor-predecessor-intersection
(:instance consp-when-certificatep
(x (pick-successor/predecessor dag1 dag2 cert1 cert2))))
:disable consp-when-certificatep))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defruled pick-successor/predecessor-properties
:short "Key properties of @(tsee pick-successor/predecessor)."
:long
(xdoc::topstring
(xdoc::p
"This combines and generalizes
the theorems proved in @(tsee pick-successor/predecessor),
by using stronger hypotheses on the DAGs
that imply the specific properties used in those previous theorems.
The hypotheses on the DAGs are all invariants, as proved elsewhere.
The key properties are that the picked certificate
is among the successors of @('cert1') in the first DAG,
among the precedessors of @('cert2') in the second DAG,
and also in both DAGs.")
(xdoc::p
"We prove four lemmas that serve to establish
hypotheses in the theorems in @(tsee pick-successor/predecessor)
from the more general hypothesis in this theorem."))
(implies (and (certificate-setp dag1)
(certificate-setp dag2)
(certificate-set-unequivocalp dag1)
(certificate-set-unequivocalp dag2)
(certificate-sets-unequivocalp dag1 dag2)
(set::in cert2 dag2)
(equal (certificate->round cert2)
(+ 2 (certificate->round cert1)))
(dag-has-committees-p dag1 blockchain1)
(dag-has-committees-p dag2 blockchain2)
(dag-in-committees-p dag1 blockchain1)
(dag-in-committees-p dag2 blockchain2)
(same-active-committees-p blockchain1 blockchain2)
(dag-predecessor-quorum-p dag2 blockchain2)
(> (committee-members-stake
(certificate-set->author-set (successors cert1 dag1))
(active-committee-at-round (1+ (certificate->round cert1))
blockchain1))
(committee-max-faulty-stake
(active-committee-at-round (1+ (certificate->round cert1))
blockchain1))))
(b* ((cert (pick-successor/predecessor dag1 dag2 cert1 cert2)))
(and (set::in cert (successors cert1 dag1))
(set::in cert (predecessors cert2 dag2))
(set::in cert dag1)
(set::in cert dag2))))
:use ((:instance pick-successor/predecessor-not-nil
(commtt (active-committee-at-round
(1+ (certificate->round cert1))
blockchain2)))
pick-successor/predecessor-in-successors
pick-successor/predecessor-in-predecessors
pick-successor/predecessor-in-dag1
pick-successor/predecessor-in-dag2
lemma1
lemma2
lemma3
lemma4)
:prep-lemmas
((defruled lemma1
(implies (and (certificate-setp dag1)
(dag-in-committees-p dag1 blockchain1))
(set::subset (certificate-set->author-set
(successors cert1 dag1))
(committee-members
(active-committee-at-round
(1+ (certificate->round cert1)) blockchain1))))
:use ((:instance round-in-committee-when-dag-in-committees-p
(dag dag1)
(blockchain blockchain1)
(round (1+ (certificate->round cert1))))
(:instance set::emptyp-subset-2
(x (successors cert1 dag1))
(y (certs-with-round (1+ (certificate->round cert1))
dag1))))
:enable (certificate-set->author-set-monotone
set::expensive-rules)
:disable set::emptyp-subset-2)
(defruled lemma2
(implies (and (certificate-setp dag2)
(dag-in-committees-p dag2 blockchain2)
(equal (certificate->round cert2)
(+ 2 (certificate->round cert1))))
(set::subset (certificate-set->author-set
(predecessors cert2 dag2))
(committee-members
(active-committee-at-round
(1- (certificate->round cert2)) blockchain2))))
:use ((:instance round-in-committee-when-dag-in-committees-p
(dag dag2)
(blockchain blockchain2)
(round (1- (certificate->round cert2))))
(:instance set::emptyp-subset-2
(x (predecessors cert2 dag2))
(y (certs-with-round (1- (certificate->round cert2))
dag2))))
:enable (certificate-set->author-set-monotone
set::expensive-rules)
:disable set::emptyp-subset-2)
(defruled lemma3
(implies (and (certificate-setp dag1)
(dag-has-committees-p dag1 blockchain1)
(dag-has-committees-p dag2 blockchain2)
(dag-in-committees-p dag1 blockchain1)
(dag-in-committees-p dag2 blockchain2)
(same-active-committees-p blockchain1 blockchain2)
(set::in cert2 dag2)
(equal (certificate->round cert2)
(+ 2 (certificate->round cert1)))
(> (committee-members-stake
(certificate-set->author-set (successors cert1 dag1))
(active-committee-at-round
(1+ (certificate->round cert1))
blockchain1))
(committee-max-faulty-stake
(active-committee-at-round
(1+ (certificate->round cert1))
blockchain1))))
(equal (active-committee-at-round
(1+ (certificate->round cert1)) blockchain1)
(active-committee-at-round
(1+ (certificate->round cert1)) blockchain2)))
:use ((:instance same-active-committees-p-necc
(round (1+ (certificate->round cert1)))
(blocks1 blockchain1)
(blocks2 blockchain2))
(:instance dag-has-committees-p-necc
(dag dag1)
(blockchain blockchain1)
(cert (set::head (successors cert1 dag1))))
(:instance dag-has-committees-p-necc
(dag dag2)
(blockchain blockchain2)
(cert cert2))
(:instance dag-in-committees-p-necc
(dag dag1)
(blockchain blockchain1)
(cert (set::head (successors cert1 dag1))))
(:instance dag-in-committees-p-necc
(dag dag2)
(blockchain blockchain2)
(cert cert2))
(:instance set::in-head
(x (successors cert1 dag1)))
(:instance active-committee-at-previous-round-when-at-round
(blocks blockchain2)
(round (certificate->round cert2)))
(:instance set::cardinality-zero-emptyp
(x (successors cert1 dag1))))
:enable (set::expensive-rules
certificate->round-of-element-of-successors)
:disable (set::in-head
set::cardinality-zero-emptyp))
(defruled lemma4
(implies (and (set::in cert2 dag2)
(equal (certificate->round cert2)
(+ 2 (certificate->round cert1)))
(dag-predecessor-quorum-p dag2 blockchain2))
(>= (committee-members-stake
(certificate-set->author-set
(predecessors cert2 dag2))
(active-committee-at-round (1+ (certificate->round cert1))
blockchain2))
(committee-quorum-stake
(active-committee-at-round (1+ (certificate->round cert1))
blockchain2))))
:use (:instance dag-predecessor-quorum-p-necc
(dag dag2)
(blockchain blockchain2)
(cert cert2)))))
|
