← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2011/krug-et-al/support/Symbolic/extended-partial-correctness.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2011/krug-et-al/support/Symbolic/extended-partial-correctness.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;;; RBK: Names such as next, run, and modify-main are much to valuable
 
4
;;; to be used here, so I changed them.  This was done blindly with
 
5
;;; emacs, so may be overly aggressive in some places
 
6
 
 
7
#||
 
8
 
 
9
 extended-partial-correctness.lisp
 
10
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
11
 
 
12
Author: Sandip Ray
 
13
Date: Fri Aug 11 14:49:55 2006
 
14
 
 
15
This book is a part of a two-book series to develop a generic theory that
 
16
allows us to compose partial correctness proofs efficiently.  Here I briefly
 
17
discuss the problem and the solution.
 
18
 
 
19
  [Uninteresting aside: I use mathematical notations rather than Lisp in the
 
20
   description below as much as possible since emacs gets confused about syntax
 
21
   highlighting if I use s-expressions in a comment that is delineated by a
 
22
   "block comment" rather than a "line comment".]
 
23
 
 
24
The Problem (and some Background)
 
25
---------------------------------
 
26
 
 
27
Recall that a partial correctness proof looks like the following: 
 
28
 
 
29
o   pre(s) /\ exists-exitpoint (s) => run(s,clock(s)) = modify(s)
 
30
 
 
31
Assume that we have proven this theorem about a subroutine Q, and we now are
 
32
interested in proving the correctness of some caller P of Q.  While verifying P
 
33
we want to of course not re-verify Q but reuse the work in its verification by
 
34
making use of the correctness theorem above.  More concretely, consider using
 
35
the cutpoint methodology (and the inductive assertions method) to prove the
 
36
correctness of P.  The crucial step in the method is to prove the following
 
37
theorem:
 
38
 
 
39
 
 
40
o  cut(s) /\ assert(s) /\ exists-cut (s) => assert(nextc(next(s)))
 
41
 
 
42
In defsimulate this was proven by just symbolically simulating the machine from
 
43
each cutpoint until the next cutpoint is reached.  But the process might cause
 
44
repeated symbolic simulation of an already verified subroutine Q.  We prefer
 
45
instead to invoke the correctness theorem of Q when symbolic simulation
 
46
encounters an invocation of Q.  That is, consider symbolically simulating the
 
47
machine starting from a cutpoint s of P.  When we encounter a state s'
 
48
involving an invocation of Q, we want to then look for the next cutpoint of s
 
49
from the state modify s.
 
50
 
 
51
It would have been nice if we could have proven a theorem of the form pre-Q(s)
 
52
=> nextc-p(s) = nextc-p(modify(s)).  Unfortunately, given the definition of
 
53
nextc (in partial-correctness.lisp and total-correctness.lisp) and the
 
54
correctness of Q above, this is not a theorem when Q is proven partially
 
55
correct.  The theorem is something like: 
 
56
 
 
57
o  pre-Q(s) /\ exists-exitpoint-Q (s) => nextc-p (s) = nextc-p (modify (s))  
 
58
 
 
59
But now we get into trouble.  We want to do the symbolic simulation in order to
 
60
prove the persistence of assertions over cutpoints.  In that context we know
 
61
exists-cut (s) for each cutpoint s of P (from the hypothesis of the theorem we
 
62
want to prove).  This hypothesis, together with some hypothesis of the
 
63
well-formedness of the subroutine Q, will be sufficient to derive
 
64
exists-exitpoint-Q (s) and hence apply the subroutine correctness theorem
 
65
above.  But we do not know exists-cut (s) for the state s that is poised at the
 
66
invocation of Q.  Rather, we know it only at the previous cutpoint before the
 
67
invocation.  Of course by "construction" we know that (a) the hypothesis was
 
68
there for a previous state, and (b) no cutpoint was encountered from that
 
69
previous state to the invocation point; therefore the hypothesis must be true
 
70
for the invocation point.  But to apply this argument we need either some
 
71
memoizing term simplifier that memoizes each of the intermediate symbolic
 
72
states (and the fact that exists-cutpoint holds for each of those), which of
 
73
course, ACL2 is not, or we must symbolically simulate the machine twice, once
 
74
for actually proving the inductive assertions and the other for advancing the
 
75
exists-cutpoint predicate, the second being a completely unnecessary one).  In
 
76
a previous version of these books, I had managed to get rid of the double
 
77
simulation by creating a number of cludges involving the use of hide.  But such
 
78
optimizations are purely ACL2-specific and no more than "dirty hacks".  The
 
79
challenge therefore is to solve the problem in a clean way.
 
80
 
 
81
|#
 
82
 
 
83
 
 
84
(include-book "misc/defp" :dir :system)
 
85
;;; RBK: try different ordinal books, to prevent problems with
 
86
;;; arithmetic-5 compatibility.
 
87
(include-book "ordinals/limits" :dir :system)
 
88
(in-theory (disable o< o+ o- o* o^))
 
89
(local (include-book "arithmetic/top-with-meta" :dir :system))
 
90
 
 
91
(encapsulate 
 
92
 (((epc-next *) => *)
 
93
  ((epc-in-sub *) => *)
 
94
  ((epc-pre-sub *) => *)
 
95
  ((epc-modify-sub *) => *)
 
96
  ((epc-pre-main *) => *)
 
97
  ((epc-cutpoint-main *) => *)
 
98
  ((epc-in-main *) => *)
 
99
  ((epc-modify-main *) => *)
 
100
  ((epc-assertion-main * *) => *))
 
101
 
 
102
 
 
103
 (local (defun epc-next (s) s))
 
104
 (defun epc-run (s n) (if (zp n) s (epc-run (epc-next s) (1- n))))
 
105
 
 
106
 (local (defun epc-in-sub (s) (declare (ignore s)) nil))
 
107
 (local (defun epc-pre-sub (s) (declare (ignore s)) nil))
 
108
 (local (defun epc-modify-sub (s) s))
 
109
 (defun-sk epc-exists-exitpoint-sub (s) (exists n (not (epc-in-sub (epc-run s n)))))
 
110
  
 
111
 (defp epc-steps-to-exitpoint-tail-sub (s i)
 
112
   (if (not (epc-in-sub s))
 
113
       i 
 
114
     (epc-steps-to-exitpoint-tail-sub (epc-next s) (1+ i))))
 
115
 
 
116
 (defun epc-steps-to-exitpoint-sub (s)
 
117
   (let ((steps (epc-steps-to-exitpoint-tail-sub s 0)))
 
118
     (if (not (epc-in-sub (epc-run s steps)))
 
119
         steps 
 
120
       (omega))))
 
121
 
 
122
 (defun epc-next-exitpoint-sub (s) (epc-run s (epc-steps-to-exitpoint-sub s)))
 
123
 
 
124
 (defthm |correctness of epc-sub|
 
125
   (implies (and (epc-pre-sub s)
 
126
                 (epc-exists-exitpoint-sub s))
 
127
            (equal (epc-next-exitpoint-sub s)
 
128
                   (epc-modify-sub s))))
 
129
 
 
130
 (local (defun epc-pre-main (s) (declare (ignore s)) nil))
 
131
 (local (defun epc-in-main (s) (declare (ignore s)) t))
 
132
 (local (defun epc-cutpoint-main (s) (declare (ignore s)) nil))
 
133
 (local (defun epc-assertion-main (s0 s) (declare (ignore s0 s)) nil))
 
134
 (local (defun epc-modify-main (s) s))
 
135
 
 
136
 (defp epc-next-epc-cutpoint-main (s)
 
137
   (if (or (epc-cutpoint-main s) 
 
138
           (not (epc-in-main s)))
 
139
       s
 
140
     (epc-next-epc-cutpoint-main (if (epc-pre-sub s) (epc-modify-sub s) (epc-next s)))))
 
141
 
 
142
 (defun-sk exists-epc-next-cutpoint (s) (exists n (epc-cutpoint-main (epc-run s n))))
 
143
 
 
144
 (defthm |no main cutpoint in epc-sub|
 
145
   (implies (epc-in-sub s)
 
146
            (not (epc-cutpoint-main s))))
 
147
 
 
148
 (defthm |epc-in-main implies in epc-sub|
 
149
   (implies (epc-in-sub s)
 
150
            (epc-in-main s)))
 
151
 
 
152
 (defthm |epc-pre-sub is epc-in-sub|
 
153
   (implies (epc-pre-sub s) (epc-in-sub s)))
 
154
 
 
155
 
 
156
 ;; Here we add all the other constraints on assertions.  
 
157
 
 
158
 (defthm |epc-assertion implies cutpoint|
 
159
   (implies (epc-assertion-main s0 s)
 
160
            (or (epc-cutpoint-main s)
 
161
                (not (epc-in-main s))))
 
162
   :rule-classes :forward-chaining)
 
163
 
 
164
 (defthm |epc-pre main implies assertion|
 
165
   (implies (epc-pre-main s)
 
166
            (epc-assertion-main s s)))
 
167
 
 
168
 (defthm |epc-assertion main implies post|
 
169
   (implies (and (epc-assertion-main s0 s)
 
170
                 (not (epc-in-main s)))
 
171
            (equal s (epc-modify-main s0)))
 
172
   :rule-classes nil)
 
173
 
 
174
 (defthm |epc-assertions for cutpoint definition|
 
175
   (implies (and (epc-assertion-main s0 s)
 
176
                 (epc-in-main s)
 
177
                 (not (epc-in-main (epc-run s n))))
 
178
            (epc-assertion-main s0 (epc-next-epc-cutpoint-main (epc-next s)))))
 
179
)
 
180
 
 
181
(local
 
182
 (defthm |definition of epc-next cutpoint|
 
183
   (equal (epc-next-epc-cutpoint-main s)
 
184
          (if (epc-pre-sub s)
 
185
              (epc-next-epc-cutpoint-main (epc-modify-sub s))
 
186
            (if (or (epc-cutpoint-main s)
 
187
                    (not (epc-in-main s)))
 
188
                s
 
189
              (epc-next-epc-cutpoint-main (epc-next s)))))
 
190
  :rule-classes :definition))
 
191
 
 
192
 
 
193
;; OK, so we need to prove that from the above we can prove the same
 
194
;; assertions-invariant theorem for the epc-next-cutpoint definition that we are
 
195
;; used to in partial correctness.  That will let us reuse the
 
196
;; partial-correctness result.
 
197
 
 
198
;; [ Maybe it is worth thinking whether we want to just use the above definition
 
199
;;   of epc-next-cutpoints for proving partial correctness theorem in the generic
 
200
;;   theory.  The reason why I do not do that is because the above definition only
 
201
;;   works for partial correctness, not total correctness.  Why?  Because for
 
202
;;   total correctness we need to know that the epc-next-cutpoint is a reachable
 
203
;;   state, and we do not have the extra hypothesis that some cutpoint is
 
204
;;   reachable.  But suppose no cutpoint is actually reachable from state s.  The
 
205
;;   above definition of epc-next-cutpoint may still produce a cutpoint (the
 
206
;;   definition is tail-recursive and we do not know what the definition produces
 
207
;;   when no cutpoint is reachable) and the cutpoint-measure of that cutpoint
 
208
;;   might even decrease, but that does not guarantee total correctness (since no
 
209
;;   cutpoint is reachable from a state, and hence no exitpoint).  And I just
 
210
;;   preferred to have the same "golden" definition of epc-next-cutpoint rather than
 
211
;;   two different ones.  So I just use this definition as a proof rule in order
 
212
;;   to compositionally prove partial correctness or more precisely, the original
 
213
;;   assertion-invariant theorem. ]
 
214
 
 
215
;; OK so we first introduce the original cutpoint definition.
 
216
 
 
217
(local (defstub default-aux-epc-state () => *))
 
218
 
 
219
(local 
 
220
 (defp o-steps-to-cutpoint-tail-main (s i)
 
221
   (if (or (epc-cutpoint-main s) 
 
222
           (not (epc-in-main s)))
 
223
       i 
 
224
     (o-steps-to-cutpoint-tail-main (epc-next s) (1+ i)))))
 
225
 
 
226
(local
 
227
 (defun o-steps-to-epc-cutpoint-main (s)
 
228
   (let ((steps (o-steps-to-cutpoint-tail-main s 0)))
 
229
     (if (or (epc-cutpoint-main (epc-run s steps))
 
230
             (not (epc-in-main (epc-run s steps))))
 
231
         steps
 
232
       (omega)))))
 
233
 
 
234
 ;; (epc-next-state-cutpoint s) is simply the closest cutpoint reachable from s.
 
235
 
 
236
(local
 
237
 (defun o-epc-next-epc-cutpoint-main (s)
 
238
   (let ((steps (o-steps-to-epc-cutpoint-main s)))
 
239
     (if (natp steps)
 
240
         (epc-run s steps)
 
241
       (default-aux-epc-state)))))
 
242
 
 
243
;; OK we need to deal with both forms of epc-next-cutpoint definition.  To do this,
 
244
;; I first prove the standard theorem about epc-steps-to-exitpoint-sub.
 
245
 
 
246
(local 
 
247
 (defun cutpoint-induction (k steps s)
 
248
   (if (zp k) (list k steps s)
 
249
     (cutpoint-induction (1- k) (1+ steps) (epc-next s)))))
 
250
 
 
251
(local
 
252
 (encapsulate
 
253
  ()
 
254
 
 
255
  (local
 
256
   (defthmd steps-to-exitpoint-tail-inv
 
257
     (implies (and (not (epc-in-sub (epc-run s k)))
 
258
                   (natp steps))
 
259
              (let* ((result  (epc-steps-to-exitpoint-tail-sub s steps))
 
260
                     (exitpoint-steps (- result steps)))
 
261
                (and (natp result)
 
262
                     (natp exitpoint-steps)
 
263
                     (implies (natp k)
 
264
                              (<= exitpoint-steps k))
 
265
                     (not (epc-in-sub (epc-run s exitpoint-steps))))))
 
266
     :hints (("Goal" 
 
267
              :in-theory (enable natp)
 
268
              :induct (cutpoint-induction k steps s)))))
 
269
  
 
270
 (defthm steps-to-exitpoint-is-ordinal
 
271
  (implies (not (natp (epc-steps-to-exitpoint-sub s)))
 
272
           (equal (epc-steps-to-exitpoint-sub s) (omega)))
 
273
  :rule-classes :forward-chaining)
 
274
 
 
275
 ;; Notice that most of the theorems I deal with has a free variable in the
 
276
 ;; hypothesis. This is unfortunate but necessary.  As a result I presume that
 
277
 ;; most of the theorems will not be proved by ACL2 automatically but often
 
278
 ;; require :use hints.  This is the reason for the proliferation of such hints
 
279
 ;; in this book.
 
280
 
 
281
 (defthm steps-to-exitpoint-is-natp
 
282
   (implies (not (epc-in-sub (epc-run s k)))
 
283
            (natp (epc-steps-to-exitpoint-sub s)))
 
284
  :rule-classes (:rewrite :forward-chaining :type-prescription)
 
285
  :hints (("Goal"
 
286
           :use ((:instance steps-to-exitpoint-tail-inv
 
287
                            (steps 0))))))
 
288
 
 
289
 (defthm steps-to-exitpoint-provide-exitpoint
 
290
   (implies (not (epc-in-sub (epc-run s k)))
 
291
            (not (epc-in-sub (epc-run s (epc-steps-to-exitpoint-sub s)))))
 
292
   :hints (("Goal"
 
293
            :use ((:instance steps-to-exitpoint-tail-inv
 
294
                             (steps 0))))))
 
295
 
 
296
 (defthm steps-to-exitpoint-is-minimal
 
297
  (implies (and (not (epc-in-sub (epc-run s k)))
 
298
                (natp k))
 
299
           (<= (epc-steps-to-exitpoint-sub s)
 
300
               k))
 
301
  :rule-classes :linear
 
302
  :hints (("Goal"
 
303
           :use ((:instance steps-to-exitpoint-tail-inv
 
304
                            (steps 0))))))))
 
305
 
 
306
(local
 
307
 (in-theory (disable epc-steps-to-exitpoint-sub)))
 
308
 
 
309
 
 
310
;; The key thing that I am going to prove is that if some cutpoint is reachable
 
311
;; from s, then epc-next-epc-cutpoint-main is the same as o-epc-next-epc-cutpoint-main.  That
 
312
;; will imply the theorem since we know some cutpoint is reachable from s as
 
313
;; the hypothesis of our desired theorem.  Now to prove this above fact, what
 
314
;; I'll do is essentially say that if some cutpoint is reachable then both
 
315
;; definitions give the minimum reachable cutpoint from s.  As such from
 
316
;; minimality they must be equal.  So the trick is to relate the new definition
 
317
;; of epc-next-cutpoint with some form of definition of steps-to-cutpoint. 
 
318
 
 
319
;; This is a feedback lemma (that is, proven after I saw ACL2 could not reduce
 
320
;; o< to <).  This lemma should really be in the ordinal books, and is one of
 
321
;; the most obvious application of ordinals.
 
322
 
 
323
(local
 
324
 (defthm natp-implies-o<=<
 
325
   (implies (and (natp x)
 
326
                 (natp y))
 
327
            (equal (o< x y)
 
328
                   (< x y)))
 
329
   :hints (("Goal"
 
330
            :in-theory (enable o<)))))
 
331
 
 
332
;; We now prove that exitsteps indeed takes you to an exitpoint of the
 
333
;; subroutine.  This might have been better to be put in the encapsulation,
 
334
;; with the other properties, but it is so trivial that it does not matter.
 
335
 
 
336
(local
 
337
 (defthmd exitsteps-natp-implies-not-in
 
338
   (implies (natp (epc-steps-to-exitpoint-sub s))
 
339
            (not (epc-in-sub (epc-run s (epc-steps-to-exitpoint-sub s)))))
 
340
  :hints (("Goal"
 
341
           :in-theory (e/d (epc-steps-to-exitpoint-sub)
 
342
                           (epc-steps-to-exitpoint-tail-sub$def))))))
 
343
 
 
344
;; Notice that the above theorem does not take care of the 0 case, for a subtle
 
345
;; reason.  The subtle reason is that when (epc-steps-to-exitpoint-sub s) is 0, we
 
346
;; want the epc-run term to collapse to s, and that does not unify.  So we add
 
347
;; another lemma.
 
348
 
 
349
(local
 
350
 (defthm exitsteps-0-implies-not-in
 
351
   (implies (equal 0 (epc-steps-to-exitpoint-sub s))
 
352
            (not (epc-in-sub s)))
 
353
   :hints (("Goal"
 
354
            :use exitsteps-natp-implies-not-in))))
 
355
 
 
356
;; Now we define the induction function for compositional reasoning.  The
 
357
;; induction here is just a generalization of cutpoint-induction.  In
 
358
;; particular, we just add another case in which the control is poised to be at
 
359
;; the entry-point of the subroutine.  Notice that the induction function is
 
360
;; not easy to admit. 
 
361
 
 
362
(local
 
363
 (defun comp-cutpoint-induction (s k)
 
364
   (declare 
 
365
    (xargs 
 
366
     :measure (nfix k)
 
367
     :hints (("Subgoal 1.1"
 
368
              :in-theory (disable |epc-pre-sub is epc-in-sub| 
 
369
                                  steps-to-exitpoint-is-natp)
 
370
              :use ((:instance |epc-pre-sub is epc-in-sub|)
 
371
                    (:instance steps-to-exitpoint-is-natp
 
372
                               (k (epc-exists-exitpoint-sub-witness s))))))))
 
373
                   
 
374
  (if (zp k) (list s k)
 
375
    (if (and (epc-pre-sub s) (epc-exists-exitpoint-sub s))
 
376
        (comp-cutpoint-induction (epc-modify-sub s) 
 
377
                            (- k (epc-steps-to-exitpoint-sub s)))
 
378
      (comp-cutpoint-induction (epc-next s) (1- k))))))
 
379
  
 
380
 
 
381
;; The epc-next important concept is that of no-cutpoint.  This says that there is
 
382
;; no cutpoint in less than n steps from s.  This definition is used to define
 
383
;; the first reachable cutpoint from s (if one exists).
 
384
 
 
385
(local
 
386
 (defun no-cutpoint (s n)
 
387
   (if (zp n) t
 
388
     (let* ((n (1- n)))
 
389
       (and (not (or (epc-cutpoint-main (epc-run s n))
 
390
                     (not (epc-in-main (epc-run s n)))))
 
391
            (no-cutpoint s n))))))
 
392
 
 
393
;; Now we prove that no-cutpoint indeed implies there is no cutpoint. 
 
394
 
 
395
(local
 
396
 (defthm no-cutpoint-implies-not-cutpoint
 
397
   (implies (and (no-cutpoint s n)
 
398
                 (natp n)
 
399
                 (natp k)
 
400
                 (< k n))
 
401
            (and (epc-in-main (epc-run s k))
 
402
                 (not (epc-cutpoint-main (epc-run s k)))))
 
403
   :hints (("Goal"
 
404
            :induct (no-cutpoint s n)
 
405
            :do-not-induct t))))
 
406
 
 
407
 
 
408
;; Now for the converse of the theorem above.  We have to prove that if there
 
409
;; is no cutpoint reachable in less than n steps then no-cutpoint holds.  We do
 
410
;; that by the standard trick of defining the witnessing cutpoint if
 
411
;; no-cutpoint does not hold.  This is a standard and (I believe) well
 
412
;; documented trick with ACL2.
 
413
 
 
414
(local 
 
415
 (defun no-cutpoint-witness (s n)
 
416
   (if (zp n) 0
 
417
     (if (or (epc-cutpoint-main (epc-run s n))
 
418
             (not (epc-in-main (epc-run s n))))
 
419
         n
 
420
       (no-cutpoint-witness s (1- n))))))
 
421
 
 
422
;; After defining the witness function we now need to prove these epc-next couple
 
423
;; of theorems.  These theorems are obvious ones, and easily provable by
 
424
;; induction.
 
425
 
 
426
(local
 
427
 (defthm cutpoint-implies-no-cut-2
 
428
   (implies (and (not (epc-cutpoint-main (epc-run s (no-cutpoint-witness s n))))
 
429
                 (epc-in-main (epc-run s (no-cutpoint-witness s n))))
 
430
            (no-cutpoint s n))))
 
431
 
 
432
(local
 
433
 (defthm no-cutpoint-witness-is-<=-n
 
434
   (implies (natp n)
 
435
            (<= (no-cutpoint-witness s n) n))
 
436
   :rule-classes :linear))
 
437
 
 
438
;; OK now we prove that if we epc-run for a number of steps k <
 
439
;; (epc-steps-to-exitpoint-sub s) then we cannot hit a epc-cutpoint-main. This is
 
440
;; because there is no epc-cutpoint-main as long as we are epc-in-main.
 
441
 
 
442
(local
 
443
 (defthm not-cutpoint-epc-pre-sub 
 
444
   (implies (and (natp k)
 
445
                 (< k (epc-steps-to-exitpoint-sub s)))
 
446
            (and (not (epc-cutpoint-main (epc-run s k)))
 
447
                 (epc-in-main (epc-run s k))))
 
448
   :hints (("Goal"
 
449
            :in-theory (disable |no main cutpoint in epc-sub|)
 
450
            :use ((:instance |no main cutpoint in epc-sub|
 
451
                             (s (epc-run s k)))
 
452
                  (:instance |epc-in-main implies in epc-sub|
 
453
                             (s (epc-run s k))))))))
 
454
 
 
455
;; We can then use this theorem to prove that (no-cutpoint s k) holds for each
 
456
;; k <= (epc-steps-to-exitpoint-sub s).  Notice that we get <= here instead of <
 
457
;; since we count from 1 less.
 
458
 
 
459
(local
 
460
 (defthm no-cutpoint-epc-pre-sub
 
461
   (implies (and (natp k)
 
462
                 (<= k (epc-steps-to-exitpoint-sub s)))
 
463
            (no-cutpoint s k))))
 
464
 
 
465
 
 
466
(local
 
467
 (defthm epc-cutpoint-main-implies-epc-next-cutpoint-s
 
468
   (implies (or (epc-cutpoint-main s)
 
469
                (not (epc-in-main s)))
 
470
            (equal (epc-next-epc-cutpoint-main s)
 
471
                   s))
 
472
   :hints (("Goal"
 
473
            :use ((:instance |definition of epc-next cutpoint|))))))
 
474
 
 
475
 
 
476
;; Now we get to a couple of hack lemmas that can be safely ignored.  First we
 
477
;; do not want to deal with (epc-next s) in the context of no-cutpoint.  So we
 
478
;; rewrite that term. 
 
479
 
 
480
(local
 
481
 (defthm epc-next-no-cutpoint
 
482
   (implies (and (not (epc-cutpoint-main s))
 
483
                 (epc-in-main s)
 
484
                 (natp n))
 
485
            (equal (no-cutpoint (epc-next s) n)
 
486
                   (no-cutpoint s (1+ n))))))
 
487
 
 
488
(local
 
489
 (in-theory (disable epc-exists-exitpoint-sub-suff 
 
490
                     epc-exists-exitpoint-sub)))
 
491
 
 
492
;; We also prove that if a cutpoint holds then no-cutpoint is nil.  This is
 
493
;; just orienting the rewriting.
 
494
 
 
495
(local
 
496
 (defthmd cutpoint-implies-not-nocut
 
497
   (implies (and (or (epc-cutpoint-main s)
 
498
                     (not (epc-in-main s)))
 
499
                 (natp n)
 
500
                 (> n 0))
 
501
            (equal (no-cutpoint s n) nil))))
 
502
 
 
503
 
 
504
 
 
505
(local
 
506
 (defthm cutpoint-implies-exists-exitpoint
 
507
   (implies (or (epc-cutpoint-main (epc-run s n))
 
508
                (not (epc-in-main (epc-run s n))))
 
509
            (epc-exists-exitpoint-sub s))
 
510
   :hints (("Goal"
 
511
            :in-theory (disable epc-exists-exitpoint-sub-suff)
 
512
            :use ((:instance epc-exists-exitpoint-sub-suff))))))
 
513
 
 
514
 
 
515
;; The reader might be surprised to see the epc-run-fnn (although they might have
 
516
;; seen this in some of the previous books designed by me).  The problem is
 
517
;; that epc-run has been defined within the encapsulate and therefore its induction
 
518
;; schemes are not exported.  For details about this issue, see :DOC
 
519
;; subversive-recursions.  So we define a new recursive epc-run-fnn, prove it is
 
520
;; equal to epc-run, and then use it when we need induction.
 
521
                              
 
522
 
 
523
(local
 
524
 (defun epc-run-fnn (s n)
 
525
   (if (zp n) s (epc-run-fnn (epc-next s) (1- n)))))
 
526
 
 
527
;; The trigger is the obvious one, it rewrites epc-run to epc-run-fnn when we need it.
 
528
 
 
529
(local
 
530
 (defthmd epc-run-fnn-trigger
 
531
   (equal (epc-run s n)
 
532
          (epc-run-fnn s n))))
 
533
 
 
534
;; And this allows us to prove theorems about epc-run by induction, via proving
 
535
;; them about epc-run-fnn.
 
536
 
 
537
(local
 
538
 (defthm epc-run-plus-reduction
 
539
   (implies (and (natp m)
 
540
                 (natp n))
 
541
            (equal (epc-run (epc-run s m) n)
 
542
                  (epc-run s (+ m n))))
 
543
   :hints (("Goal"
 
544
            :in-theory (enable epc-run-fnn-trigger)))))
 
545
 
 
546
 
 
547
;; Now we get back, obviously, to no-cutpoint.  We prove that we can use
 
548
;; no-cutpoint with +.  Of course the way we prove it is that we prove the
 
549
;; theorem for (not (cutpoint ...)) and then lift the result for no-cutpoint.
 
550
 
 
551
 
 
552
(local
 
553
 (defthmd not-cutpoint-plus-reduction
 
554
   (implies (and (no-cutpoint s k)
 
555
                 (natp k)
 
556
                 (natp n)
 
557
                 (no-cutpoint (epc-run s k) n)
 
558
                 (< l (+ k n))
 
559
                 (natp l))
 
560
            (and (not (epc-cutpoint-main (epc-run s l)))
 
561
                 (epc-in-main (epc-run s l))))
 
562
   :hints (("Goal"
 
563
            :cases ((< l k)))
 
564
           ("Subgoal 2"
 
565
            :use ((:instance no-cutpoint-implies-not-cutpoint
 
566
                             (s (epc-run s k))
 
567
                             (k (- l k))))))))
 
568
 
 
569
 
 
570
(local
 
571
 (defthm no-cutpoint-plus-reduction
 
572
   (implies (and (no-cutpoint s k)
 
573
                 (natp k)
 
574
                 (natp n)
 
575
                 (no-cutpoint (epc-run s k) n)
 
576
                 (<= l (+ k n))
 
577
                 (natp l))
 
578
            (no-cutpoint s l))
 
579
   :hints (("Goal"
 
580
            :cases ((zp l)))
 
581
           ("Subgoal 2"
 
582
            :use ((:instance not-cutpoint-plus-reduction
 
583
                             (l (no-cutpoint-witness s (1- l)))))))))
 
584
 
 
585
 
 
586
;; Now we prove that if no-cutpoint holds for s and n then it also holds for
 
587
;; (epc-run s k) for n-k steps. 
 
588
 
 
589
(local
 
590
 (defthmd no-cutpoint-epc-run-reduction
 
591
   (implies (and (no-cutpoint s n)
 
592
                 (natp n)
 
593
                 (natp k)
 
594
                 (<= k n))
 
595
            (no-cutpoint (epc-run s k) (- n k)))))
 
596
 
 
597
;; Therefore we know that if we are standing at a epc-pre-sub state then from the
 
598
;; epc-next-exitpoint, which is to say epc-modify-sub state it should be true from
 
599
;; n-steps steps, where n is the number of steps for the first cutpoint from s.
 
600
 
 
601
(local
 
602
 (defthmd pre-implies-no-cutpoint-s
 
603
   (implies (and (no-cutpoint s n)
 
604
                 (natp n)
 
605
                 (or (epc-cutpoint-main (epc-run s n))
 
606
                     (not (epc-in-main (epc-run s n))))
 
607
                 (epc-pre-sub s))
 
608
            (no-cutpoint (epc-modify-sub s) (- n (epc-steps-to-exitpoint-sub s))))
 
609
   :hints (("Goal"
 
610
            :in-theory (disable |correctness of epc-sub|)
 
611
            :use ((:instance |correctness of epc-sub|)
 
612
                  (:instance no-cutpoint-epc-run-reduction
 
613
                             (k (epc-steps-to-exitpoint-sub s))))))))
 
614
 
 
615
 
 
616
 
 
617
;; Thus we also know that by virtue of epc-run-plus-reduction we can prove that
 
618
;; (epc-run s n) is equal to (epc-run (epc-modify-sub s) (n - steps)).  
 
619
 
 
620
(local           
 
621
 (defthm pre-implies-epc-run-plus
 
622
   (implies (and (epc-pre-sub s)
 
623
                 (natp n)
 
624
                 (or (epc-cutpoint-main (epc-run s n))
 
625
                     (not (epc-in-main (epc-run s n)))))
 
626
            (equal (epc-run (epc-modify-sub s) (- n (epc-steps-to-exitpoint-sub s)))
 
627
                   (epc-run s n)))
 
628
   :hints (("Goal"
 
629
            :in-theory (disable |correctness of epc-sub|
 
630
                                epc-run-plus-reduction
 
631
                                steps-to-exitpoint-is-minimal
 
632
                                steps-to-exitpoint-is-natp)
 
633
            :use ((:instance epc-run-plus-reduction
 
634
                             (n (- n (epc-steps-to-exitpoint-sub s)))
 
635
                             (m (epc-steps-to-exitpoint-sub s)))
 
636
                  (:instance |correctness of epc-sub|)
 
637
                  (:instance epc-exists-exitpoint-sub-suff)
 
638
                  (:instance steps-to-exitpoint-is-natp
 
639
                             (k n))
 
640
                  (:instance steps-to-exitpoint-is-minimal
 
641
                             (k n)))))))
 
642
 
 
643
(local
 
644
 (defthm alternative-epc-next-cutpoint-property
 
645
   (implies (and (or (epc-cutpoint-main (epc-run s n))
 
646
                     (not (epc-in-main (epc-run s n))))
 
647
                 (no-cutpoint s n))
 
648
            (equal (epc-next-epc-cutpoint-main s)
 
649
                   (epc-run s n)))
 
650
   :hints (("Goal"
 
651
            :induct (comp-cutpoint-induction s n))
 
652
           ("Subgoal *1/3"
 
653
            :use ((:instance cutpoint-implies-not-nocut
 
654
                             (n (1- n)))))
 
655
           ("Subgoal *1/2"
 
656
            :use ((:instance pre-implies-no-cutpoint-s))))))
 
657
 
 
658
 
 
659
;; OK so I have just proved that if n is the first cutpoint from s, then
 
660
;; epc-next-cutpoint-returns state after n steps.  Now we consider the traditional
 
661
;; steps-to-cutpoint and prove that it returns the same thing.  But we will
 
662
;; start with the definition of the traditional epc-next-cutpoint first.
 
663
 
 
664
(local
 
665
 (encapsulate 
 
666
  ()
 
667
  
 
668
  (local
 
669
   (defthmd steps-to-cutpoint-tail-inv
 
670
     (implies (and (or (epc-cutpoint-main (epc-run s k))
 
671
                       (not (epc-in-main (epc-run s k))))
 
672
                   (natp steps))
 
673
              (let* ((result  (o-steps-to-cutpoint-tail-main s steps))
 
674
                     (cutpoint-steps (- result steps)))
 
675
                (and (natp result)
 
676
                     (natp cutpoint-steps)
 
677
                     (implies (natp k)
 
678
                              (<= cutpoint-steps k))
 
679
                     (or (epc-cutpoint-main (epc-run s cutpoint-steps))
 
680
                         (not (epc-in-main (epc-run s cutpoint-steps)))))))
 
681
     :rule-classes :forward-chaining
 
682
     :hints (("Goal" 
 
683
              :in-theory (enable natp)
 
684
              :induct (cutpoint-induction k steps s)))))
 
685
  
 
686
  (defthm steps-to-cutpoint-is-ordinal
 
687
    (implies (not (natp (o-steps-to-epc-cutpoint-main s)))
 
688
             (equal (o-steps-to-epc-cutpoint-main s) (omega)))
 
689
    :rule-classes :forward-chaining)
 
690
  
 
691
  (defthm steps-to-cutpoint-is-natp
 
692
    (implies (or (epc-cutpoint-main (epc-run s k))
 
693
                 (not (epc-in-main (epc-run s k))))
 
694
             (natp (o-steps-to-epc-cutpoint-main s)))
 
695
    :rule-classes (:rewrite :forward-chaining :type-prescription)
 
696
    :hints (("Goal"
 
697
             :use ((:instance steps-to-cutpoint-tail-inv
 
698
                              (steps 0))))))
 
699
  
 
700
  (defthm steps-to-cutpoint-provide-cutpoint
 
701
    (implies (or (epc-cutpoint-main (epc-run s k))
 
702
                 (not (epc-in-main (epc-run s k))))
 
703
             (or (epc-cutpoint-main (epc-run s (o-steps-to-epc-cutpoint-main s)))
 
704
                 (not (epc-in-main (epc-run s (o-steps-to-epc-cutpoint-main s))))))
 
705
    :rule-classes :forward-chaining
 
706
    :hints (("Goal"
 
707
             :use ((:instance steps-to-cutpoint-tail-inv
 
708
                              (steps 0))))))
 
709
  
 
710
  (defthm steps-to-cutpoint-is-minimal
 
711
    (implies (and (or (epc-cutpoint-main (epc-run s k))
 
712
                      (not (epc-in-main (epc-run s k))))
 
713
                  (natp k))
 
714
             (<= (o-steps-to-epc-cutpoint-main s)
 
715
                 k))
 
716
    :rule-classes :linear
 
717
    :hints (("Goal"
 
718
             :use ((:instance steps-to-cutpoint-tail-inv
 
719
                              (steps 0))))))))
 
720
 
 
721
(local (in-theory (disable o-steps-to-epc-cutpoint-main)))
 
722
 
 
723
;; From this I can prove that if some cutpoint is reachable then
 
724
;; o-epc-next-epc-cutpoint-main takes us to the first reachable cutpoint.  My strategy
 
725
;; now is that I will prove the result rather for the new cutpoint definition
 
726
;; than for the old one.  The reason is that it is much easier to reason in
 
727
;; abstract about steps-to-cutpoint than about epc-next-cutpoint and therefore we
 
728
;; must move from epc-next-cutpoint to steps-to-cutpoint in order to simplify the
 
729
;; proofs.
 
730
 
 
731
(local
 
732
 (defthm not-cutpoint-until-steps-to-cutpoint
 
733
   (implies (and (natp l)
 
734
                 (or (epc-cutpoint-main (epc-run s k))
 
735
                     (not (epc-in-main (epc-run s k))))
 
736
                 (< l (o-steps-to-epc-cutpoint-main s)))
 
737
            (and (not (epc-cutpoint-main (epc-run s l)))
 
738
                 (epc-in-main (epc-run s l))))
 
739
    :hints (("Goal"
 
740
             :use ((:instance steps-to-cutpoint-is-minimal
 
741
                              (k l)))))))
 
742
 
 
743
(local (in-theory (disable o-steps-to-epc-cutpoint-main)))
 
744
 
 
745
(local
 
746
 (defthm no-cutpoint-until-steps-to-cutpoint-aux
 
747
   (implies (and (natp l)
 
748
                 (or (epc-cutpoint-main (epc-run s k))
 
749
                     (not (epc-in-main (epc-run s k))))
 
750
                 (<= l (o-steps-to-epc-cutpoint-main s)))
 
751
             (no-cutpoint s l))
 
752
   :hints (("Goal"
 
753
            :induct (no-cutpoint s l))
 
754
           ("Subgoal *1/2"
 
755
            :in-theory (disable not-cutpoint-until-steps-to-cutpoint)
 
756
            :use ((:instance not-cutpoint-until-steps-to-cutpoint
 
757
                             (l (1- l))))))))
 
758
 
 
759
;; So we have essentially proven that for any l <= steps-to-cutpoint,
 
760
;; no-cutpoint holds for l steps.  We can then instantiate l with
 
761
;; steps-to-cutpoint itself and clean this up.  Note that we have already
 
762
;; proven that steps-to-cutpoint is a natp when a cutpoint is reachable from s.
 
763
 
 
764
(local 
 
765
 (defthmd cutpoint-implies-no-cutpoint-steps
 
766
   (implies (or (epc-cutpoint-main (epc-run s k))
 
767
                (not (epc-in-main (epc-run s k))))
 
768
            (no-cutpoint s (o-steps-to-epc-cutpoint-main s)))
 
769
   :otf-flg t
 
770
   :hints (("Goal"
 
771
            :in-theory (disable steps-to-cutpoint-is-natp
 
772
                                cutpoint-implies-no-cut-2
 
773
                                not-cutpoint-until-steps-to-cutpoint
 
774
                                no-cutpoint-until-steps-to-cutpoint-aux)
 
775
            :use ((:instance steps-to-cutpoint-is-natp)
 
776
                  (:instance no-cutpoint-until-steps-to-cutpoint-aux
 
777
                             (l (o-steps-to-epc-cutpoint-main s))))))))
 
778
 
 
779
;; Therefore we should know that (epc-next-cutpoint s) is equal to (epc-run s
 
780
;; (o-steps-to-cutpoint s)).
 
781
 
 
782
(local
 
783
 (defthm epc-next-cutpoint-is-epc-run-of-steps
 
784
   (implies (or (epc-cutpoint-main (epc-run s k))
 
785
                (not (epc-in-main (epc-run s k))))
 
786
            (equal (epc-next-epc-cutpoint-main s)
 
787
                   (epc-run s (o-steps-to-epc-cutpoint-main s))))
 
788
   :hints (("Goal"
 
789
            :in-theory (disable alternative-epc-next-cutpoint-property)
 
790
            :use ((:instance cutpoint-implies-no-cutpoint-steps)
 
791
                  (:instance steps-to-cutpoint-provide-cutpoint)
 
792
                  (:instance alternative-epc-next-cutpoint-property
 
793
                             (n (o-steps-to-epc-cutpoint-main s))))))))
 
794
 
 
795
;; Now we only have to prove that if there is a cutpoint which is not an
 
796
;; exitpoint then there is a cutpoint reachable from (epc-next s)
 
797
 
 
798
(local
 
799
 (defthm epc-next-has-a-cutpoint
 
800
   (implies (and (epc-in-main s)
 
801
                 (not (epc-in-main (epc-run s k))))
 
802
            (or (epc-cutpoint-main (epc-run (epc-next s) (1- k)))
 
803
                (not (epc-in-main (epc-run (epc-next s) (1- k))))))
 
804
   :rule-classes nil
 
805
   :hints (("Goal"
 
806
            :expand (epc-run s k)))))
 
807
                
 
808
 
 
809
;; Now we can just prove that the epc-next-cutpoint  of (epc-next s) under the proper
 
810
;; condition is just the same as its traditional definition.
 
811
 
 
812
(local
 
813
 (defthm epc-next-cutpoint-matches
 
814
   (implies (and (epc-in-main s)
 
815
                 (not (epc-in-main (epc-run s k))))
 
816
            (equal (epc-run (epc-next s) (o-steps-to-epc-cutpoint-main (epc-next s)))
 
817
                   (epc-next-epc-cutpoint-main (epc-next s))))
 
818
   :hints (("Goal"
 
819
            :in-theory (disable epc-next-cutpoint-is-epc-run-of-steps)
 
820
            :use ((:instance epc-next-cutpoint-is-epc-run-of-steps
 
821
                             (s (epc-next s))
 
822
                             (k (1- k))))))))
 
823
 
 
824
 
 
825
;; Now we can of course just prove the final theorem since we know from the
 
826
;; encapsulation that assertion is inductive over the new definition of
 
827
;; epc-next-cutpoint.
 
828
 
 
829
(local
 
830
 (defthm |new cutpoint definition matches old|
 
831
   (implies (and (epc-assertion-main s0 s)
 
832
                 (epc-in-main s)
 
833
                 (not (epc-in-main (epc-run s n))))
 
834
            (epc-assertion-main s0 (o-epc-next-epc-cutpoint-main (epc-next s))))
 
835
   :hints (("Subgoal 1"
 
836
            :in-theory (disable steps-to-cutpoint-is-natp)
 
837
            :use ((:instance steps-to-cutpoint-is-natp
 
838
                             (k (1- n))
 
839
                             (s (epc-next s))))))))
 
840
 
 
841
(local (include-book "vanilla-partial-correctness"))
 
842
          
 
843
(defp epc-exitsteps-main-tail (s i)
 
844
  (if (not (epc-in-main s)) i
 
845
    (epc-exitsteps-main-tail (epc-next s) (1+ i))))
 
846
      
 
847
(defun epc-exitsteps-main (s)
 
848
  (let ((steps (epc-exitsteps-main-tail s 0)))
 
849
    (if (not (epc-in-main (epc-run s steps)))
 
850
        steps 
 
851
      (omega))))
 
852
 
 
853
(defun-sk epc-exists-exitpoint-main (s)
 
854
  (exists n (not (epc-in-main (epc-run s n)))))
 
855
 
 
856
 
 
857
(defun epc-next-exitpoint-main (s)
 
858
  (epc-run s (epc-exitsteps-main s)))
 
859
 
 
860
  
 
861
(local (in-theory (theory 'minimal-theory)))
 
862
 
 
863
(local
 
864
 (defthmd composition-partial-aux
 
865
  (implies (and (epc-pre-main s)
 
866
                (equal s s0)
 
867
                (epc-exists-exitpoint-main s))
 
868
           (and (not (epc-in-main (epc-next-exitpoint-main s)))
 
869
                (equal (epc-next-exitpoint-main s)
 
870
                       (epc-modify-main s))))
 
871
  :otf-flg t
 
872
  :hints (("Goal"
 
873
           :do-not-induct t
 
874
           :use ((:instance 
 
875
                  (:functional-instance 
 
876
                   |partial correctness|
 
877
                   (cutpoint 
 
878
                    (lambda (s) (or (epc-cutpoint-main s) (not (epc-in-main s)))))
 
879
                   (assertion (lambda (s) (epc-assertion-main s0 s)))
 
880
                   (pre (lambda (s) (and (epc-pre-main s) (equal s0 s))))
 
881
                   (exitpoint (lambda (s) (not (epc-in-main s))))
 
882
                   (next-exitpoint (lambda (s) (epc-next-exitpoint-main s)))
 
883
                   (exists-exitpoint (lambda (s) (epc-exists-exitpoint-main s)))
 
884
                   (steps-to-exitpoint (lambda (s) (epc-exitsteps-main s)))
 
885
                   (steps-to-exitpoint-tail epc-exitsteps-main-tail)
 
886
                   (steps-to-cutpoint 
 
887
                    (lambda (s) (o-steps-to-epc-cutpoint-main s)))
 
888
                   (steps-to-cutpoint-tail 
 
889
                    (lambda (s i) (o-steps-to-cutpoint-tail-main s i)))
 
890
                   (next-state-cutpoint 
 
891
                    (lambda (s) (o-epc-next-epc-cutpoint-main s)))
 
892
                   (post (lambda (s) (equal s (epc-modify-main s0))))
 
893
                   (default-state default-aux-epc-state)
 
894
                   (run-fn epc-run)
 
895
                   (exists-exitpoint-witness epc-exists-exitpoint-main-witness)
 
896
                   (next-state epc-next)))))
 
897
          ("Subgoal 14"
 
898
           :in-theory (enable epc-run))
 
899
         ("Subgoal 13"
 
900
          :use ((:instance |new cutpoint definition matches old|)))
 
901
          ("Subgoal 12"
 
902
           :use ((:instance o-steps-to-cutpoint-tail-main$def)))
 
903
          ("Subgoal 11"
 
904
          :use ((:instance |epc-assertion main implies post|)))
 
905
          ("Subgoal 10"
 
906
           :use ((:instance |epc-pre main implies assertion|)
 
907
                 (:instance |epc-assertion implies cutpoint|)))
 
908
          ("Subgoal 9"
 
909
           :use ((:instance |epc-pre main implies assertion|)))
 
910
          ("Subgoal 7"
 
911
           :use ((:instance (:definition o-epc-next-epc-cutpoint-main))))
 
912
          ("Subgoal 6"
 
913
           :use ((:instance (:definition o-steps-to-epc-cutpoint-main))))
 
914
          ("Subgoal 5"
 
915
           :use ((:instance (:definition epc-next-exitpoint-main))))
 
916
          ("Subgoal 4"
 
917
           :use ((:instance (:definition epc-exitsteps-main))))
 
918
          ("Subgoal 3"
 
919
           :use ((:instance epc-exitsteps-main-tail$def)))
 
920
         ("Subgoal 2"
 
921
          :use ((:instance epc-exists-exitpoint-main-suff)))
 
922
         ("Subgoal 1"
 
923
          :use ((:instance (:definition epc-exists-exitpoint-main)))))))
 
924
 
 
925
(DEFTHM |epc composite partial correctness|
 
926
  (implies (and (epc-pre-main s)
 
927
                (epc-exists-exitpoint-main s))
 
928
           (and (equal (epc-in-main (epc-next-exitpoint-main s)) nil)
 
929
                (equal (epc-next-exitpoint-main s)
 
930
                       (epc-modify-main s))))
 
931
  :hints (("Goal"
 
932
           :use ((:instance composition-partial-aux (s0 s))))))
 
933
 
 
 
b'\\ No newline at end of file'