-
Notifications
You must be signed in to change notification settings - Fork 201
/
ReachableProofs.tla
215 lines (208 loc) · 12.5 KB
/
ReachableProofs.tla
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
-------------------------- MODULE ReachableProofs --------------------------
(***************************************************************************)
(* This module contains the TLAPS checked proofs of partial correctness of *)
(* the algorithm in module Reachable, based on the invariants Inv1, Inv2, *)
(* and Inv3 defined in that module. The proofs here are pretty simple *)
(* because the difficult parts involve proving general results about *)
(* reachability that are independent of the algorithm. Those results are *)
(* stated and proved in module ReachabilityProofs and are used by the *)
(* proofs in this module. *)
(* *)
(* You might be sufficiently motivated to make sure the algorithm is *)
(* correct to want a machine-checked proof that is, but not motivated *)
(* enough to write machine-checked proofs of the properties of directed *)
(* graphs that the proof uses. If that's the case, or you're curious *)
(* about why it might be the case, read module ReachabilityTest. *)
(* *)
(* After writing the proof, it occurred to me that it might be easier to *)
(* replace invariants Inv2 and Inv3 by the single invariant *)
(* *)
(* Inv23 == Reachable = ReachableFrom(marked \cup vroot) *)
(* *)
(* Inv23 is obviously true initially and its invariance is maintained by *)
(* this general result about marked graphs *)
(* *)
(* \A S \in SUBSET Nodes : *)
(* \A n \in S : reachableFrom(S) = reachableFrom(S \cup Succ[n]) *)
(* *)
(* since marked \cup vroot is changed only by adding successors of nodes *)
(* in vroot to it. Partial correctness is true because when vroot = {}, *)
(* we have *)
(* *)
(* Inv1 => \A n \in marked : Succ[n] \subseteq marked *)
(* Inv23 <=> Reachable = ReachableFrom(marked) *)
(* *)
(* and the following is true for any directed graph: *)
(* *)
(* \A S \in SUBSET Nodes: *)
(* (\A n \in S : Succ[n] \subseteq S) => (S = reachableFrom(S)) *)
(* *)
(* As an exercise, you can try rewriting the proof of partial correctness *)
(* of the algorithm using only the invariants Inv1 and Inv23, using the *)
(* necessary results about reachability. When you've finished doing that, *)
(* you can try proving those reachability results. *)
(***************************************************************************)
EXTENDS Reachable, ReachabilityProofs, TLAPS
(***************************************************************************)
(* Note that there is no need to write a separate proof that TypeOK is *)
(* invariant, since its invariance is implied by the invariance of Inv1. *)
(***************************************************************************)
THEOREM Thm1 == Spec => []Inv1
(*************************************************************************)
(* The three level <1> steps and its QED step's proof are the same for *)
(* any inductive invariance proof. Step <1>2 is the only one that TLAPS *)
(* couldn't prove with a BY proof. *)
(*************************************************************************)
<1>1. Init => Inv1
BY RootAssump DEF Init, Inv1, TypeOK
<1>2. Inv1 /\ [Next]_vars => Inv1'
(***********************************************************************)
(* The steps of this level <2> proof are the standard way of proving *)
(* the formula <1>2; they were generated by the Toolbox's Decompose *)
(* Proof Command. The algorithm is simple enough that TLAPS can prove *)
(* steps <2>1 and <2>2, which are the only nontrivial ones, with BY *)
(* proofs. *)
(***********************************************************************)
<2> SUFFICES ASSUME Inv1,
[Next]_vars
PROVE Inv1'
OBVIOUS
<2>1. CASE a
BY <2>1, SuccAssump DEF Inv1, TypeOK, a
<2>2. CASE UNCHANGED vars
BY <2>2 DEF Inv1, TypeOK, vars
<2>3. QED
BY <2>1, <2>2 DEF Next, Terminating
<1>3. QED
BY <1>1, <1>2, PTL DEF Spec
THEOREM Thm2 == Spec => [](TypeOK /\ Inv2)
(*************************************************************************)
(* This theorem is a trivial consequence of a general fact about *)
(* reachability in a directed graph, which is called Reachable1 and *)
(* proved in Module ReachabilityProofs, *)
(*************************************************************************)
<1>1. Inv1 => TypeOK /\ Inv2
BY Reachable1 DEF Inv1, Inv2, TypeOK
<1> QED
BY <1>1, Thm1, PTL
(***************************************************************************)
(* The best way to read the proof of the following theorem is *)
(* hierarchically. Read all the steps of a proof at a given level, then *)
(* read separately the proof of each of those steps, starting with the *)
(* proof of the QED step. Start by executing the Hide Current Subtree *)
(* command on the theorem, then use the little + and - icons beside the *)
(* theorem and each proof step to show and hide its proof. *)
(***************************************************************************)
THEOREM Thm3 == Spec => []Inv3
(*************************************************************************)
(* Observe the level <1> proof and the proof of its QED step to see how *)
(* the invariance of TypeOK and Inv2 are used in the proof of invariance *)
(* of Inv3. *)
(*************************************************************************)
<1>1. Init => Inv3
BY RootAssump DEF Init, Inv3, TypeOK, Reachable
<1>2. TypeOK /\ TypeOK' /\ Inv2 /\ Inv2' /\ Inv3 /\ [Next]_vars => Inv3'
(***********************************************************************)
(* The SUFFICES step and its proof, the QED step and its proof, and *)
(* the CASE steps <2>2 and <2>3 were generated by the Toolbox's *)
(* Decompose Proof command. *)
(***********************************************************************)
<2> SUFFICES ASSUME TypeOK,
TypeOK',
Inv2,
Inv2',
Inv3,
[Next]_vars
PROVE Inv3'
OBVIOUS
(***********************************************************************)
(* Step <2>1 is obviously true because Reachable and ReachableFrom are *)
(* constants. It helps TLAPS to give it these results explicitly so *)
(* it doesn't have to figure them out when it needs them. *)
(***********************************************************************)
<2>1. /\ Reachable' = Reachable
/\ ReachableFrom(vroot)' = ReachableFrom(vroot')
/\ ReachableFrom(marked \cup vroot)' = ReachableFrom(marked' \cup vroot')
OBVIOUS
<2>2. CASE a
(*********************************************************************)
(* `a' is a simple enough formula so there's no need to hide its *)
(* definition when it's not needed. *)
(*********************************************************************)
<3> USE <2>2 DEF a
(*********************************************************************)
(* Splitting the proof into these two cases is an obvious way to *)
(* write the proof--especially since TLAPS is not very good at *)
(* figuring out by itself when it should do a proof by a case split. *)
(*********************************************************************)
<3>1. CASE vroot = {}
BY <2>1, <3>1 DEF Inv3, TypeOK
<3>2. CASE vroot # {}
(*******************************************************************)
(* The way to use a fact of the form \E x \in S : P(x) is to pick *)
(* an x in S satisfying P(x). *)
(*******************************************************************)
<4>1. PICK v \in vroot :
IF v \notin marked
THEN /\ marked' = (marked \cup {v})
/\ vroot' = vroot \cup Succ[v]
ELSE /\ vroot' = vroot \ {v}
/\ UNCHANGED marked
BY <3>2
(*******************************************************************)
(* Again, the obvious way to use a fact of the form *)
(* *)
(* IF P THEN ... ELSE ... *)
(* *)
(* is by splitting the proof into the two cases P and ~P. *)
(*******************************************************************)
<4>2. CASE v \notin marked
(*****************************************************************)
(* This case follows immediately from the general reachability *)
(* result Reachable2 from module ReachabilityProofs. *)
(*****************************************************************)
<5>1. /\ ReachableFrom(vroot') = ReachableFrom(vroot)
/\ v \in ReachableFrom(vroot)
BY <4>1, <4>2, Reachable2 DEF TypeOK
<5>2. QED
BY <5>1, <4>1, <4>2, <5>1, <2>1 DEF Inv3
<4>3. CASE v \in marked
(*****************************************************************)
(* This case is obvious. *)
(*****************************************************************)
<5>1. marked' \cup vroot' = marked \cup vroot
BY <4>1, <4>3
<5>2. QED
BY <5>1, <2>1 DEF Inv2, Inv3
<4>4. QED
BY <4>2, <4>3
<3>3. QED
BY <3>1, <3>2
<2>3. CASE UNCHANGED vars
(*********************************************************************)
(* As is almost all invariance proofs, this case is trivial. *)
(*********************************************************************)
BY <2>1, <2>3 DEF Inv3, TypeOK, vars
<2>4. QED
BY <2>2, <2>3 DEF Next, Terminating
<1>3. QED
BY <1>1, <1>2, Thm2, PTL DEF Spec
THEOREM Spec => []((pc = "Done") => (marked = Reachable))
(*************************************************************************)
(* This theorem follows easily from the invariance of Inv1 and Inv3 and *)
(* the trivial result Reachable3 of module ReachabilityProofs that *)
(* Reachable({}) equals {}. That result was put in module *)
(* ReachabilityProofs so all the reasoning about the algorithm depends *)
(* only on properties of ReachableFrom, and doesn't depend on how *)
(* ReachableFrom is defined. *)
(*************************************************************************)
<1>1. Inv1 => ((pc = "Done") => (vroot = {}))
BY DEF Inv1, TypeOK
<1>2. Inv3 /\ (vroot = {}) => (marked = Reachable)
BY Reachable3 DEF Inv3
<1>3. QED
BY <1>1, <1>2, Thm1, Thm3, PTL
=============================================================================
\* Modification History
\* Last modified Sun Apr 14 16:24:32 PDT 2019 by lamport
\* Created Thu Apr 11 18:41:11 PDT 2019 by lamport