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
|
; 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 "simultaneous-induction")
(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+ unequivocal-dag
:parents (correctness)
:short "Invariant that DAGs are unequivocal:
proof that it holds in every reachable state."
:long
(xdoc::topstring
(xdoc::p
"This completes @(see unequivocal-dags-def-and-init)
and @(see unequivocal-dags-next)
by showing that the invariant holds in every reachable state."))
:order-subtopics t
:default-parent t)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defsection unequivocal-dags-certificates-p-always
:short "The invariant holds in every state
reachable from an initial state via a sequence of events."
(defruled unequivocal-dags-certificates-p-when-reachable
(implies (and (system-initp systate)
(events-possiblep events systate)
(all-system-committees-fault-tolerant-p systate events))
(unequivocal-dags-p (events-next events systate)))))
|
