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
|
(in-package "ACL2")
#|
final-theorems.lisp
~~~~~~~~~~~~~~~~~~~
In this book, we simply summarize all the final theorems that we have
proved in other books for the bakery. All the theorems should go thru
and say "redundant" in ACL2. I simply have this book, to make the task
easy for the reader of the proof. When all is said and done, these
will be the facts that we claim about the bakery algorithm.
|#
(include-book "labels")
(include-book "stutter1-match")
(include-book "stutter2")
(include-book "initial-state")
(include-book "inv-persists")
(include-book "inv-sufficient")
;; Labels of implementation and specification are equal
(DEFTHM labels-equal-b-c->>
(implies (inv-b-c st)
(equal (label (rep-b-c st))
(label st)))
:rule-classes nil)
(DEFTHM fair-labels-equal-b-c->>
(implies (fair-inv-b-c st)
(equal (label (rep-b-c st))
(label st)))
:rule-classes nil)
;; A step of the implementation is a step of the specification upto
;; stuttering:
(DEFTHM >>-stutter1-b-c
(implies (and (suff-b-c st in)
(not (commit-b-c st in)))
(equal (rep-b-c (bake+ st in))
(rep-b-c st)))
:rule-classes nil)
(DEFTHM >>-fair-stutter1-b-c
(implies (and (fair-suff-b-c st X)
(not (commit-b-c st (fair-select (env st) X))))
(equal (rep-b-c (fair-bake+ st X))
(rep-b-c st)))
:rule-classes nil)
(DEFTHM >>-stutter1-c-s
(implies (and (suff-c-s st in)
(not (commit-c-s st in)))
(equal (rep-c-s (cent st in))
(rep-c-s st)))
:rule-classes nil)
(DEFTHM >>-match-b-c
(implies (and (suff-b-c st in)
(commit-b-c st in))
(equal (rep-b-c (bake+ st in))
(cent (rep-b-c st) (pick-b-c st in))))
:rule-classes nil)
(DEFTHM >>-fair-match-b-c
(implies (and (fair-suff-b-c st X)
(commit-b-c st (fair-select (env st) X)))
(equal (rep-b-c (fair-bake+ st X))
(cent (rep-b-c st)
(fair-pick-b-c st X))))
:rule-classes nil)
(DEFTHM match-c-s
(implies (and (suff-c-s st in)
(legal st in)
(commit-c-s st in))
(equal (rep-c-s (cent st in))
(spec (rep-c-s st) in)))
:rule-classes nil)
;; Stuttering is finite:
(DEFTHM well-founded-b-c->>
(msrp (rank-b-c st))
:rule-classes nil)
(DEFTHM >>-stutter2-b-c
(implies (and (fair-suff-b-c st X)
(not (commit-b-c st (fair-select (env st) X))))
(msr< (rank-b-c (fair-bake+ st X))
(rank-b-c st)))
:rule-classes nil)
;; There exists at least one state in which the invariant inv holds
(DEFTHM inv-b-c-initial-state->>
(inv-b-c (initial-state-b))
:rule-classes nil)
(DEFTHM fair-inv-b-c-initial-state->>
(fair-inv-b-c (initial-state-b))
:rule-classes nil)
(DEFTHM inv-c-s-rep-initial-state->>
(inv-c-s (rep-c-s (initial-state-b)))
:rule-classes nil)
;; "inv" is an invariant:
(DEFTHM inv-b-c-persists->>
(implies (inv-b-c st)
(inv-b-c (bake+ st in)))
:rule-classes nil)
(DEFTHM fair-inv-b-c-persists->>
(implies (fair-inv-b-c st)
(fair-inv-b-c (fair-bake+ st X)))
:rule-classes nil)
(DEFTHM inv-c-s-persists->>
(implies (and (inv-c-s st)
(legal st in))
(inv-c-s (cent st in)))
:rule-classes nil)
;; "inv" is sufficient:
(DEFTHM inv-b-c-sufficient->>
(implies (inv-b-c st)
(suff-b-c st in))
:rule-classes nil)
(DEFTHM fair-inv-b-c-sufficient->>
(implies (fair-inv-b-c st)
(fair-suff-b-c st X))
:rule-classes nil)
(DEFTHM inv-c-s-sufficient
(implies (and (inv-c-s st)
(legal st in))
(suff-c-s st in))
:rule-classes nil)
|
