← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2004/legato/support/nqthm/generic-theory-tail-recursion-mult.events

  • 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/2004/legato/support/nqthm/generic-theory-tail-recursion-mult.events
 
1
;;; This file contains a proof of the 6502 multiply program using the tail
 
2
;;; recursion generic theory.
 
3
 
 
4
(note-lib "modularithmetic-98")
 
5
(load "generic-theories.events")
 
6
 
 
7
;;; The following is a Floyd-Hoare correctness specification for the multiply
 
8
;;; program.
 
9
;;;
 
10
;;;      { F1=F1SAVE ^ F1<256 ^ F2<256 ^ LOW<256 }
 
11
;;;
 
12
;;;         LDX #8     load the X register immediate with the value 8
 
13
;;;         LDA #0     load the A register immediate with the value 0
 
14
;;; LOOP    ROR F1     rotate F1 right circular through the carry flag
 
15
;;;         BCC ZCOEF  branch on carry flag clear to ZCOEF
 
16
;;;         CLC        clear the carry flag
 
17
;;;         ADC F2     add with carry F2 to the contents of A
 
18
;;; ZCOEF   ROR A      rotate A right circular through the carry flag
 
19
;;;         ROR LOW    rotate LOW right circular through the carry flag
 
20
;;;         DEX        decrement the X register by 1
 
21
;;;         BNE LOOP   branch if X is non-zero to LOOP
 
22
;;;
 
23
;;;      { LOW + 256*A = F1SAVE*F2 }
 
24
 
 
25
;;; Provide semantics for the Mostek 6502 DEX instruction.  The remaining
 
26
;;; instructions have semantics built into the weakest precondition generation
 
27
;;; program.
 
28
 
 
29
(defn dec (x)
 
30
  (if (not (zerop x))
 
31
      (sub1 x)
 
32
    255))
 
33
 
 
34
;;; This is mechanically derived.
 
35
 
 
36
(DEFN WP-ZCOEF
 
37
       (F1 X C LOW A F1SAVE F2)
 
38
       (IF (EQUAL (DEC X) 0)
 
39
           (EQUAL
 
40
              (PLUS (TIMES (PLUS (TIMES 128 C) (QUOTIENT A 2)) 256)
 
41
                    (PLUS (TIMES 128 (REMAINDER A 2))
 
42
                          (QUOTIENT LOW 2)))
 
43
              (TIMES F1SAVE F2))
 
44
           (WP-ZCOEF
 
45
              (PLUS (TIMES 128 (REMAINDER LOW 2))
 
46
                    (QUOTIENT F1 2))
 
47
              (DEC X)
 
48
              (TIMES
 
49
                 (REMAINDER F1 2)
 
50
                 (QUOTIENT
 
51
                    (PLUS (PLUS (TIMES 128 C) (QUOTIENT A 2)) F2)
 
52
                    256))
 
53
              (PLUS (TIMES 128 (REMAINDER A 2))
 
54
                    (QUOTIENT LOW 2))
 
55
              (IF (EQUAL (REMAINDER F1 2) 0)
 
56
                  (PLUS (TIMES 128 C) (QUOTIENT A 2))
 
57
                  (REMAINDER
 
58
                   (PLUS (PLUS (TIMES 128 C) (QUOTIENT A 2))
 
59
                         F2)
 
60
                   256))
 
61
              F1SAVE
 
62
              F2))
 
63
       ((lessp (dec x)))) ; This hint is user added
 
64
 
 
65
;;; This is the weakest precondition at the beginning of the program.
 
66
 
 
67
(defn wp-zcoef-1 (f1 c low f2)
 
68
  (wp-zcoef
 
69
   (plus (times 128 c) (quotient f1 2))
 
70
   8
 
71
   0
 
72
   low
 
73
   (times (remainder f1 2) f2)
 
74
   f1
 
75
   f2))
 
76
 
 
77
;;; (exp i b) = b**i if b > 0, otherwise 0.
 
78
 
 
79
(defn exp (i b)
 
80
  (if (zerop b)
 
81
      0
 
82
    (if (zerop i)
 
83
        1
 
84
      (times b (exp (sub1 i) b)))))
 
85
 
 
86
;;; Generalize the register size in order to capture properties of the constants
 
87
;;; 128 and 256.
 
88
 
 
89
(defn wp-zcoef-g (f1 x c low a result f2 i)
 
90
       (if (equal (dec x) 0)
 
91
           (equal
 
92
              (plus (times (plus (times (exp (sub1 i) 2) c) (quotient a 2))
 
93
                           (exp i 2))
 
94
                    (plus (times (exp (sub1 i) 2) (remainder a 2))
 
95
                          (quotient low 2)))
 
96
              result)
 
97
           (wp-zcoef-g
 
98
              (plus (times (exp (sub1 i) 2) (remainder low 2))
 
99
                    (quotient f1 2))
 
100
              (dec x)
 
101
              (times
 
102
                 (remainder f1 2)
 
103
                 (quotient
 
104
                    (plus (plus (times (exp (sub1 i) 2) c) (quotient a 2)) f2)
 
105
                    (exp i 2)))
 
106
              (plus (times (exp (sub1 i) 2) (remainder a 2))
 
107
                    (quotient low 2))
 
108
              (if (equal (remainder f1 2) 0)
 
109
                  (plus (times (exp (sub1 i) 2) c) (quotient a 2))
 
110
                  (remainder
 
111
                   (plus (plus (times (exp (sub1 i) 2) c) (quotient a 2))
 
112
                         f2)
 
113
                   (exp i 2)))
 
114
              result
 
115
              f2
 
116
              i))
 
117
       ((lessp (dec x))))
 
118
 
 
119
;;; Our proof strategy is to successively transform wp-zcoef-1 into instances of more
 
120
;;; general functions.  This performs the first step.
 
121
 
 
122
(prove-lemma wp-zcoef-g-instance (rewrite)
 
123
             (equal (wp-zcoef f1 x c low a f1save f2)
 
124
                    (wp-zcoef-g f1 x c low a (times f1save f2) f2 8))
 
125
             ((hands-off plus times quotient remainder difference)
 
126
              (expand (wp-zcoef f1 0 c low a f1save f2)
 
127
                      (wp-zcoef-g f1 0 c low a (times f1save f2) f2 8))))
 
128
 
 
129
;;; Split the state into an "a" component that does the effective computation, and
 
130
;;; an "s" component that drives the computation.
 
131
 
 
132
;;; Package the "a" component into a long integer.
 
133
 
 
134
(defn c (a i) (quotient a (exp (times 2 i) 2)))             ; the carry flag
 
135
(defn a (a i) (remainder (quotient a (exp i 2)) (exp i 2))) ; the accumulator
 
136
(defn low (a i) (remainder a (exp i 2)))                    ; lower half of product
 
137
 
 
138
;;; Package the "s" component using lists.
 
139
 
 
140
(defn x (s) (car s))                                        ; x register counter
 
141
(defn f1 (s) (cadr s))                                      ; first factor
 
142
(defn f2 (s) (caddr s))                                     ; second factor
 
143
(defn result (s) (cadddr s))                                ; the result
 
144
(defn i (s) (caddddr s))                                    ; word size in bits
 
145
 
 
146
;;; Define the instantiation of h from the generic theory.  wp-zcoef-h performs a
 
147
;;; multiply in the standard way, except that it delivers twice the product.
 
148
 
 
149
(defn wp-zcoef-h (s)
 
150
  (if (equal (dec (x s)) 0)
 
151
      0
 
152
    (times 2 (plus (wp-zcoef-h
 
153
                    (list (dec (x s))
 
154
                          (quotient (f1 s) 2)
 
155
                          (f2 s)
 
156
                          (result s)
 
157
                          (i s)))
 
158
                   (if (equal (remainder (f1 s) 2) 0)
 
159
                       0
 
160
                     (f2 s)))))
 
161
  ((lessp (dec (x s)))))
 
162
 
 
163
;;; Define the instantiation of hs.  btm-s compute the bottom object under tau.
 
164
 
 
165
(defn btm-s (s)
 
166
  (if (equal (dec (x s)) 0)
 
167
      s
 
168
    (btm-s (list (dec (x s))
 
169
                 (quotient (f1 s) 2)
 
170
                 (f2 s)
 
171
                 (result s)
 
172
                 (i s))))
 
173
  ((lessp (dec (x s)))))
 
174
 
 
175
;;; An alternative to the library rule remainder-plus-arg1 with fewer case splits.
 
176
 
 
177
(prove-lemma remainder-plus-arg1-alt (rewrite)
 
178
             (implies (equal (remainder a d) 0)
 
179
                      (and (equal (remainder (plus a b) d) (remainder b d))
 
180
                           (equal (remainder (plus b a) d) (remainder b d))
 
181
                           (equal (remainder (plus b a c) d)
 
182
                                  (remainder (plus b c) d))
 
183
                           (equal (remainder (plus b c a) d)
 
184
                                  (remainder (plus b c) d))))
 
185
             ((disable-theory if-normalization)
 
186
              (hands-off difference)
 
187
              (disable times-add1)))
 
188
 
 
189
;;; This simple fact is absent from modularithmetic-98.
 
190
 
 
191
(prove-lemma equal-even-odd (rewrite)
 
192
             (implies (equal (remainder a 2) (remainder b 2))
 
193
                      (and (not (equal a (add1 b)))
 
194
                           (not (equal (add1 b) a))))
 
195
             ((disable-theory if-normalization)
 
196
              (disable remainder-add1-arg2)))
 
197
 
 
198
 
 
199
;;; Define an induction hint which recurses on two copies of wp-zcoef-g.
 
200
 
 
201
(defn ind-2 (f1 x c low a f1p xp cp lowp ap f2 i)
 
202
  (if (equal (dec x) 0)
 
203
      0
 
204
    (ind-2
 
205
     (plus (times (exp (sub1 i) 2) (remainder low 2))
 
206
           (quotient f1 2))
 
207
     (dec x)
 
208
     (times
 
209
      (remainder f1 2)
 
210
      (quotient
 
211
       (plus (plus (times (exp (sub1 i) 2) c) (quotient a 2)) f2)
 
212
       (exp i 2)))
 
213
     (plus (times (exp (sub1 i) 2) (remainder a 2))
 
214
           (quotient low 2))
 
215
     (if (equal (remainder f1 2) 0)
 
216
         (plus (times (exp (sub1 i) 2) c) (quotient a 2))
 
217
       (remainder
 
218
        (plus (plus (times (exp (sub1 i) 2) c) (quotient a 2))
 
219
              f2)
 
220
        (exp i 2)))
 
221
     (plus (times (exp (sub1 i) 2) (remainder lowp 2))
 
222
           (quotient f1p 2))
 
223
     (dec xp)
 
224
     (times
 
225
      (remainder f1p 2)
 
226
      (quotient
 
227
       (plus (plus (times (exp (sub1 i) 2) cp) (quotient ap 2)) f2)
 
228
       (exp i 2)))
 
229
     (plus (times (exp (sub1 i) 2) (remainder ap 2))
 
230
           (quotient lowp 2))
 
231
     (if (equal (remainder f1p 2) 0)
 
232
         (plus (times (exp (sub1 i) 2) cp) (quotient ap 2))
 
233
       (remainder
 
234
        (plus (plus (times (exp (sub1 i) 2) cp) (quotient ap 2))
 
235
              f2)
 
236
        (exp i 2)))
 
237
     f2
 
238
     i))
 
239
  ((lessp (dec x))))
 
240
 
 
241
;;; Prove equality on wp-zcoef-g by backchaining on equality of its arguments.
 
242
 
 
243
(prove-lemma equal-wp-zcoef-g (rewrite)
 
244
             (implies (and (equal (remainder f1 (exp (sub1 x) 2))
 
245
                                  (remainder f1p (exp (sub1 x) 2)))
 
246
                           (equal x xp)
 
247
                           (equal (plus (times c (exp i 2)) a)
 
248
                                  (plus (times cp (exp i 2)) ap))
 
249
                           (equal low lowp)
 
250
                           (not (lessp i x))
 
251
                           (not (zerop x)))
 
252
                      (equal (equal (wp-zcoef-g f1 x c low a result f2 i)
 
253
                                    (wp-zcoef-g f1p xp cp lowp ap result f2 i))
 
254
                             t))
 
255
             ((disable-theory if-normalization)
 
256
              (hands-off difference)
 
257
              (induct (ind-2 f1 x c low a f1p xp cp lowp ap f2 i))
 
258
              (expand (exp (sub1 xp) 2))
 
259
              (disable remainder-add1-arg2
 
260
                       quotient-add1-arg2
 
261
                       quotient-plus-arg1
 
262
                       remainder-plus-arg1
 
263
                       remainder-plus-arg1-simple
 
264
                       times
 
265
                       times-add1
 
266
                       sub1-times
 
267
                       sub1-plus
 
268
                       sub1-remainder
 
269
                       sub1-quotient
 
270
                       remainder-times-arg1
 
271
                       remainder-difference-arg1
 
272
                       equal-add1
 
273
                       remainder-minus-one-as-0
 
274
                       equal-transpose-meta
 
275
                       quotient-is-unique
 
276
                       lessp-quotient-arg2-linear
 
277
                       lessp-quotient
 
278
                       plus-is-0
 
279
                       remainder-add1-arg1
 
280
                       equal-quotient-0
 
281
                       quotient-times-arg1-simple
 
282
                       quotient-add1-arg1
 
283
                       )))
 
284
 
 
285
;;; An alternative to the library quotient-plus-arg1 with fewer case splits.
 
286
 
 
287
(prove-lemma quotient-plus-arg1-alt (rewrite)
 
288
             (implies (equal (remainder a d) 0)
 
289
                      (and (equal (quotient (plus a b) d)
 
290
                                  (plus (quotient a d) (quotient b d)))
 
291
                           (equal (quotient (plus b a) d)
 
292
                                  (plus (quotient a d) (quotient b d)))
 
293
                           (equal (quotient (plus b a c) d)
 
294
                                  (plus (quotient a d) (quotient (plus b c) d)))
 
295
                           (equal (quotient (plus b c a) d)
 
296
                                  (plus (quotient a d) (quotient (plus b c) d)))))
 
297
             ((disable-theory if-normalization)
 
298
              (hands-off difference)
 
299
              (disable lessp-transpose-meta
 
300
                       equal-transpose-meta
 
301
                       equal-even-odd
 
302
                       remainder-difference-arg1
 
303
                       remainder-plus-arg1)))
 
304
 
 
305
;;; A Knuth-Bendix style rule for remainder-times-arg2.
 
306
 
 
307
(prove-lemma remainder-times-arg2-kb (rewrite)
 
308
             (equal (plus (remainder a b)
 
309
                          (times b (remainder (quotient a b) c)))
 
310
                    (plus (remainder a c)
 
311
                          (times c (remainder (quotient a c) b))))
 
312
             ((use (remainder-times-arg2 (a a) (zb b) (zc c))
 
313
                   (remainder-times-arg2 (a a) (zb c) (zc b)))
 
314
              (disable remainder-times-arg2
 
315
                       times
 
316
                       quotient
 
317
                       remainder)))
 
318
 
 
319
;;; A Knuth-Bendix style rule for quotient-times-arg2.
 
320
 
 
321
(prove-lemma remainder-times-arg2-close-kb (rewrite)
 
322
             (equal (plus (remainder (quotient a b) c)
 
323
                          (times c (quotient (quotient a c) b)))
 
324
                    (quotient a b)))
 
325
 
 
326
;;; More properties of exp.
 
327
 
 
328
(prove-lemma exp-plus-arg1 (rewrite)
 
329
             (equal (exp (plus i j) b) (times (exp i b) (exp j b))))
 
330
 
 
331
(prove-lemma remainder-exp-exp (rewrite)
 
332
  (implies (not (lessp i j))
 
333
           (equal (remainder (exp i 2) (exp j 2)) 0))
 
334
  ((disable times
 
335
            times-add1)))
 
336
 
 
337
(prove-lemma quotient-exp-2 (rewrite)
 
338
             (equal (quotient (exp i 2) 2)
 
339
                    (if (zerop i)
 
340
                        0
 
341
                      (exp (sub1 i) 2))))
 
342
 
 
343
;;; Use the generic tail recursion theory.
 
344
 
 
345
(functionally-instantiate wp-zcoef-g=h nil
 
346
 (implies (and (not (zerop (x s)))
 
347
               (not (lessp (i s) (x s)))
 
348
               (numberp (f2 s))
 
349
               (lessp (f2 s) (exp (i s) 2)))
 
350
          (equal (wp-zcoef-g
 
351
                  (f1 s)
 
352
                  (x s)
 
353
                  (c a (i s))
 
354
                  (low a (i s))
 
355
                  (a a (i s))
 
356
                  (result s)
 
357
                  (f2 s)
 
358
                  (i s))
 
359
                 (if (equal (dec (x s)) 0)
 
360
                     (equal
 
361
                      (plus
 
362
                       (times (plus (times (exp (sub1 (i s)) 2) (c a (i s)))
 
363
                                    (quotient (a a (i s)) 2))
 
364
                              (exp (i s) 2))
 
365
                       (plus (times (exp (sub1 (i s)) 2)
 
366
                                    (remainder (a a (i s)) 2))
 
367
                             (quotient (low a (i s)) 2)))
 
368
                      (result s))
 
369
                   (let ((a (if (equal (dec (x s)) 0)
 
370
                                a
 
371
                              (quotient (plus a (times (exp (i s) 2)
 
372
                                                       (wp-zcoef-h s)))
 
373
                                        (exp (sub1 (x s)) 2))))
 
374
                         (s (btm-s s)))
 
375
                     (equal
 
376
                      (plus
 
377
                       (times (plus (times (exp (sub1 (i s)) 2) (c a (i s)))
 
378
                                    (quotient (a a (i s)) 2))
 
379
                              (exp (i s) 2))
 
380
                       (plus (times (exp (sub1 (i s)) 2)
 
381
                                    (remainder (a a (i s)) 2))
 
382
                             (quotient (low a (i s)) 2)))
 
383
                      (result s))))))
 
384
 g=h
 
385
 ((bb (lambda (s) (equal (dec (x s)) 0)))
 
386
  (qt (lambda (a s) (equal
 
387
                     (plus
 
388
                      (times (plus (times (exp (sub1 (i s)) 2) (c a (i s)))
 
389
                                   (quotient (a a (i s)) 2))
 
390
                             (exp (i s) 2))
 
391
                      (plus (times (exp (sub1 (i s)) 2)
 
392
                                   (remainder (a a (i s)) 2))
 
393
                            (quotient (low a (i s)) 2)))
 
394
                     (result s))))
 
395
  (g (lambda (a s) (wp-zcoef-g (f1 s)
 
396
                               (x s)
 
397
                               (c a (i s))
 
398
                               (low a (i s))
 
399
                               (a a (i s))
 
400
                               (result s)
 
401
                               (f2 s)
 
402
                               (i s))))
 
403
  (measure-g (lambda (s) (dec (x s))))
 
404
  (tau (lambda (s) (list (dec (x s))
 
405
                         (quotient (f1 s) 2)
 
406
                         (f2 s)
 
407
                         (result s)
 
408
                         (i s))))
 
409
  (rho (lambda (a s)
 
410
         (if (equal (remainder (f1 s) 2) 0)
 
411
             (quotient a 2)
 
412
           (plus (quotient a 2)
 
413
                 (times (f2 s) (exp (i s) 2))))))
 
414
  (rhoh (lambda (a s) (if (equal (remainder (f1 s) 2) 0)
 
415
                          (times 2 a)
 
416
                        (times 2 (plus a (f2 s))))))
 
417
  (h (lambda (s) (wp-zcoef-h s)))
 
418
  (rt (lambda (a s) (and (not (zerop (x s)))
 
419
                         (not (lessp (i s) (x s)))
 
420
                         (numberp (f2 s))
 
421
                         (lessp (f2 s) (exp (i s) 2)))))
 
422
  (id (lambda () 0))
 
423
  (op (lambda (a x s) (if (equal (dec (x s)) 0)
 
424
                          a
 
425
                        (quotient (plus a (times (exp (i s) 2) x))
 
426
                                  (exp (sub1 (x s)) 2)))))
 
427
  (hs (lambda (s) (btm-s s))))
 
428
 ((disable-theory if-normalization)
 
429
  (hands-off difference)
 
430
  (expand (times 2 x)
 
431
          (times 2 z))
 
432
  (disable quotient-add1-arg2
 
433
           remainder-add1-arg2
 
434
           remainder-plus-arg1
 
435
           remainder-plus-arg1-simple
 
436
           quotient-plus-arg1
 
437
           remainder-difference-arg1
 
438
           times-add1
 
439
           times
 
440
           equal-add1
 
441
           equal-transpose-meta
 
442
           lessp-transpose-meta
 
443
           lessp-2
 
444
           quotient-plus-arg2
 
445
           lessp-quotient-arg2-linear
 
446
           remainder-add1-arg1
 
447
           sub1-remainder
 
448
           sub1-quotient
 
449
           sub1-times
 
450
           sub1-plus
 
451
           quotient-remainder
 
452
           remainder-minus-one-as-0
 
453
           lessp-quotient
 
454
           lessp-odometer-simple
 
455
           equal-odometer-simple
 
456
           plus-is-0
 
457
           no-divisors-of-zero
 
458
           )))
 
459
 
 
460
;;; Since the bottom object under tau was defined recursively this is needed.
 
461
 
 
462
(prove-lemma btm-s-destruct (rewrite)
 
463
  (implies (and (not (zerop (x s)))
 
464
                (not (lessp (i s) (x s))))
 
465
           (and (equal (car (btm-s s)) 1)
 
466
                (equal (cadr (btm-s s))
 
467
                       (if (equal (dec (x s)) 0)
 
468
                           (f1 s)
 
469
                         (quotient (f1 s) (exp (sub1 (x s)) 2))))
 
470
                (equal (caddr (btm-s s)) (f2 s))
 
471
                (equal (cadddr (btm-s s)) (result s))
 
472
                (equal (caddddr (btm-s s)) (i s))))
 
473
  ((disable-theory if-normalization)
 
474
   (hands-off difference)
 
475
   (disable quotient-add1-arg2
 
476
            remainder-add1-arg2
 
477
            quotient-sub1-arg1
 
478
            times
 
479
            times-add1)))
 
480
 
 
481
;;; Another Knuth-Bendex style rule for quotient-times-arg2.
 
482
 
 
483
(prove-lemma quotient-times-arg2-permutative (rewrite)
 
484
             (implies (equal (remainder c b) 0)
 
485
                      (and (equal (quotient (quotient (plus a c) d) b)
 
486
                                  (quotient (plus (quotient a b)
 
487
                                                  (quotient c b))
 
488
                                            d))
 
489
                           (equal (quotient (quotient (quotient (plus a c) d) e) b)
 
490
                                  (quotient
 
491
                                   (quotient (plus (quotient a b)
 
492
                                                   (quotient c b))
 
493
                                             d)
 
494
                                   e))))
 
495
             ((disable-theory if-normalization)
 
496
              (hands-off difference)
 
497
              (use (quotient-times-arg2-kb
 
498
                    (a (plus a c)) (b d) (c b))
 
499
                   (quotient-times-arg2-kb
 
500
                    (a (quotient (plus a c) d)) (b e) (c b))
 
501
                   (quotient-times-arg2-kb
 
502
                    (a a) (b b) (c d))
 
503
                   (quotient-times-arg2-kb
 
504
                    (a c) (b b) (c d))
 
505
                   (quotient-plus-arg1 (a a) (b c) (c b)))
 
506
              (disable quotient-times-arg2-kb
 
507
                       quotient-plus-arg1
 
508
                       remainder
 
509
                       quotient
 
510
                       plus
 
511
                       lessp-times-single-linear
 
512
                       lessp-quotient-arg2-linear
 
513
                       quotient-plus-arg2
 
514
                       lessp-quotient
 
515
                       lessp-transpose-meta
 
516
                       equal-transpose-meta
 
517
                       quotient-add1-arg1
 
518
                       equal-even-odd
 
519
                       sub1-plus
 
520
                       remainder-add1-arg2
 
521
                       )))
 
522
 
 
523
(prove-lemma remainder-exp-2 (rewrite)
 
524
             (equal (remainder (exp i 2) 2)
 
525
                    (if (zerop i)
 
526
                        1
 
527
                      0))
 
528
             ((expand (exp i 2))))
 
529
 
 
530
(prove-lemma equal-exp-0 (rewrite)
 
531
             (equal (equal (exp i b) 0)
 
532
                    (zerop b)))
 
533
 
 
534
;;; Avoids an expand hint.
 
535
 
 
536
(prove-lemma quotient-is-0 (rewrite)
 
537
             (implies (lessp a b) (equal (quotient a b) 0)))
 
538
 
 
539
;;; Convert generic theory back to flat state space.
 
540
 
 
541
(prove-lemma wp-zcoef-g=h-flat (rewrite)
 
542
 (implies (and (not (zerop i))
 
543
               (numberp f2)
 
544
               (lessp f2 (exp i 2))
 
545
               (numberp a)
 
546
               (lessp a (exp i 2))
 
547
               (numberp low)
 
548
               (lessp low (exp i 2)))
 
549
          (equal (wp-zcoef-g f1 i 0 low a result f2 i)
 
550
                 (if (equal (dec i) 0)
 
551
                     (equal a result)
 
552
                   (equal
 
553
                    (plus a
 
554
                          (wp-zcoef-h (list i f1 f2 result i)))
 
555
                    result))))
 
556
 ((disable-theory if-normalization)
 
557
  (use (wp-zcoef-g=h
 
558
        (a (plus low (times (exp i 2) a)))
 
559
        (s (list i f1 f2 result i))))
 
560
  (hands-off difference)
 
561
  (expand (times 2 i))
 
562
  (disable quotient-add1-arg2
 
563
           remainder-add1-arg2
 
564
           remainder-plus-arg1
 
565
           remainder-plus-arg1-simple
 
566
           quotient-plus-arg1
 
567
           remainder-difference-arg1
 
568
           times-add1
 
569
           times
 
570
           wp-zcoef-g
 
571
           wp-zcoef-h
 
572
           sub1-times
 
573
           sub1-plus
 
574
           sub1-remainder
 
575
           sub1-quotient
 
576
           quotient-times-arg1
 
577
           lessp-transpose-meta
 
578
           lessp-quotient-arg2-linear)))
 
579
 
 
580
;;; Prove the primitive recursive version multiplies.
 
581
 
 
582
(prove-lemma wp-zcoef-h-multiplies (rewrite)
 
583
  (implies (and (not (zerop (x s)))
 
584
                (not (lessp (i s) (x s))))
 
585
           (equal (wp-zcoef-h s)
 
586
                  (times 2 (f2 s) (remainder (f1 s) (exp (sub1 (x s)) 2)))))
 
587
  ((disable-theory if-normalization)
 
588
   (disable quotient-add1-arg2
 
589
            remainder-add1-arg2
 
590
            quotient-sub1-arg1
 
591
            times
 
592
            times-add1
 
593
            difference-add1
 
594
            sub1-quotient
 
595
            remainder-difference-arg1
 
596
            sub1-times)))
 
597
 
 
598
;;; Final program correctness proof.
 
599
 
 
600
(prove-lemma wp-zcoef-is-correct (rewrite)
 
601
 (implies (and (numberp f2)
 
602
               (lessp f2 256)
 
603
               (numberp f1)
 
604
               (lessp f1 256)
 
605
               (numberp low)
 
606
               (lessp low 256))
 
607
          (wp-zcoef-1 f1 c low f2))
 
608
 ((disable-theory if-normalization)
 
609
  (hands-off difference)
 
610
  (disable times
 
611
           times-add1
 
612
           quotient-add1-arg2
 
613
           remainder-add1-arg2
 
614
           equal-add1)))