← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/1999/simulator/tiny.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/1999/simulator/tiny.lisp
 
1
#| 
 
2
 
 
3
This file contains an interpreter for the "tiny" machine, an
 
4
experimental machine loosely based on Boyer's and Moore's small
 
5
machine, as described in "High-Speed Analyzable Simulators", Chapter 8
 
6
of the book "Computer-Aided Reasoning: ACL2 Case Studies".  We also
 
7
include a small benchmark program that calculates the remainder of two
 
8
integers.  This file is the latest in a series of experiments to build
 
9
a toy interpreter that can be analyzed and run fast using many
 
10
different methods of constructing fast interpreters.
 
11
 
 
12
Several of the changes made in Fall 1999 to reflect improvements in
 
13
ACL2, or highlight something in the chapter.  In particular, we
 
14
 
 
15
  - Added symbolic field names.
 
16
 
 
17
  - Updated the model to use STOBJ.  (STOBJ names were also
 
18
subsequently changed to comply with the name changes in the draft and
 
19
released versions of ACL2 2.4.)
 
20
 
 
21
  - Changed the definition of 32-bit add in order to avoid compiler
 
22
replacements altogether, as described in the chapter.
 
23
 
 
24
Dave Greve and Matt Wilding 
 
25
 
 
26
September 1999 
 
27
(updated January 2000)
 
28
 
 
29
|#
 
30
 
 
31
(in-package "ACL2")
 
32
(include-book "../../../arithmetic/top")
 
33
(include-book "../../../data-structures/list-defthms")
 
34
(include-book "../../../meta/meta")
 
35
(include-book "../../../ihs/logops-lemmas")
 
36
 
 
37
(disable-theory (theory 'logops-functions))
 
38
 
 
39
(set-verify-guards-eagerness 2) 
 
40
 
 
41
(defstobj st
 
42
          (progc :type (unsigned-byte 10) :initially 0)
 
43
          (mem :type (array (signed-byte 32) (1024)) :initially 0)
 
44
          (dtos :type (unsigned-byte 10) :initially 0)
 
45
          (ctos :type (unsigned-byte 10) :initially 0))
 
46
 
 
47
;; We define symbolic names for the location of the stobj fields for
 
48
;; use in theorems.
 
49
 
 
50
(defmacro progcloc () 0)
 
51
(defmacro memloc ()   1)
 
52
(defmacro dtosloc ()  2)
 
53
(defmacro ctosloc ()  3)
 
54
 
 
55
;; Some proof speedup lemmas
 
56
;; Changed after Version 6.1 by Matt Kaufmann to replace obsolete the-error by
 
57
;; the-check.
 
58
(defthm the-check-noop
 
59
  (equal (the-check g x y) y))
 
60
 
 
61
(defthm nth-update-nth-const
 
62
  (implies
 
63
   (and
 
64
    (syntaxp (quotep n1))
 
65
    (syntaxp (quotep n2)))
 
66
   (equal (nth n1 (update-nth n2 v l))
 
67
          (if (equal (nfix n1) (nfix n2)) v (nth n1 l))))
 
68
  :rule-classes ((:rewrite :loop-stopper nil)))
 
69
 
 
70
(in-theory (disable the-check nth update-nth))
 
71
 
 
72
;; Some macros for convenient expression of declarations
 
73
(defmacro Int32 (x) `(the   (signed-byte 32) ,x))
 
74
(defmacro Nat10 (x) `(the (unsigned-byte 10) ,x))
 
75
(defmacro MAX_INT<32>   ()  2147483647)
 
76
(defmacro MIN_INT<32>   () -2147483648)
 
77
(defmacro MIN_INT<32>+1   () -2147483647)
 
78
(defmacro MAX_NAT<10>   ()  1023)
 
79
(defmacro MAX_NAT-1<10> ()  1022)
 
80
 
 
81
(defmacro fix|10| (x)
 
82
  `(Nat10 (logand (MAX_NAT<10>) ,x)))
 
83
 
 
84
(defmacro max<32> (x y)
 
85
  `(Int32 (max ,x ,y)))
 
86
 
 
87
(defmacro +<32> (x y)
 
88
  `(Int32 (+ ,x ,y)))
 
89
 
 
90
;; We introduce a speedy add function for 32-bit quantities, then a
 
91
;; not-so-speedy 32-bit add function that uses IHS library function
 
92
;; about which much has been previously proved.  We show their
 
93
;; equivalence to make use of the proofs in the IHS library.
 
94
 
 
95
;; The plus<32> guard proof require 3 minutes on an Ultra 10, a long
 
96
;; time for a little theorem.
 
97
 
 
98
(defun plus<32> (a b)
 
99
  (declare (type (signed-byte 32) a)
 
100
           (type (signed-byte 32) b)
 
101
           ;; Added by Matt K. for v2-7:
 
102
           (xargs :guard-hints (("Goal" :in-theory (enable signed-byte-p)))))
 
103
  (Int32 
 
104
   (if (< a 0)
 
105
       (if (>= b 0) (+<32> a b)
 
106
         (let ((psum (+<32> (+<32> (+<32> a (MAX_INT<32>)) 1) b)))
 
107
           (declare (type (signed-byte 32) psum))
 
108
           (if (< psum 0)
 
109
               (+<32> (+<32> (MAX_INT<32>) psum) 1)
 
110
             (+<32> psum (MIN_INT<32>)))))
 
111
     (if (< b 0) (+<32> a b)
 
112
       (let ((psum (+<32> (+<32> a (MIN_INT<32>)) b)))
 
113
         (declare (type (signed-byte 32) psum))
 
114
         (if (>= psum 0)
 
115
             (+<32> (MIN_INT<32>) psum)
 
116
           (+<32> (+<32> psum (MAX_INT<32>)) 1)))))))
 
117
 
 
118
(defun +bv32 (x y)
 
119
   (declare (type (signed-byte 32) x y))
 
120
   (logext 32 (+ x y)))
 
121
 
 
122
(defthm plus<32>-works
 
123
  (implies
 
124
   (and
 
125
    (signed-byte-p 32 a)
 
126
    (signed-byte-p 32 b))
 
127
  (equal
 
128
   (plus<32> a b)
 
129
   (+bv32 a b)))
 
130
  :hints (("goal" :use ((:instance logext-+-logext (size 32) (i (+ a b)) (j (- (expt 2 32))))
 
131
                        (:instance logext-+-logext (size 32) (i (+ a b)) (j (expt 2 32))))
 
132
           :in-theory (set-difference-theories (enable signed-byte-p) '(logext-+-logext)))))
 
133
 
 
134
(defthm integerp-means-rationalp
 
135
  (implies (integerp x) (rationalp x))
 
136
  :rule-classes nil)
 
137
 
 
138
(defthm integerp-plus
 
139
  (implies
 
140
   (and (integerp a) (integerp b))
 
141
   (integerp (+ a b)))
 
142
  :rule-classes nil)
 
143
 
 
144
;; Handy facts about 32-bit addition
 
145
(defthm +bv32-representable-as-32-bits
 
146
  (and
 
147
   (integerp (+bv32 a b))
 
148
   (rationalp (+bv32 a b))
 
149
   (< (+bv32 a b) 2147483648) ; modified by Matt K. for v2-7
 
150
   (>= (+bv32 a b) -2147483648))
 
151
  :hints (("goal" 
 
152
           :in-theory (set-difference-theories (enable signed-byte-p) '(signed-byte-p-logext))
 
153
           :use
 
154
           ((:instance integerp-means-rationalp
 
155
                       (x (+bv32 a b)))
 
156
            (:instance signed-byte-p-logext (size 32) (size1 32) (i (+ a b)))
 
157
            (:instance integerp-plus
 
158
                       (a (LOGAND A 4294967295))
 
159
                       (b (LOGAND B 4294967295)))))))
 
160
 
 
161
(in-theory (disable plus<32> +bv32))
 
162
(in-theory (enable signed-byte-p))
 
163
 
 
164
;; Macros for convenient arithmetic 
 
165
(defmacro +|10| (x y)
 
166
  `(Nat10 (logand (+<32> ,x ,y) (MAX_NAT<10>))))
 
167
 
 
168
(defmacro add<32> (x y)
 
169
  `(Int32 (plus<32> ,x ,y)))
 
170
 
 
171
(defmacro negate_32 (x)
 
172
  `(let ((x ,x))
 
173
     (declare (type (signed-byte 32) x))
 
174
     (Int32 (if (= x (MIN_INT<32>)) (MIN_INT<32>) (Int32 (- x))))))
 
175
 
 
176
(defun sub<32> (x y)
 
177
  (declare (type (signed-byte 32) x)
 
178
           (type (signed-byte 32) y))
 
179
  (add<32> x (negate_32 y)))
 
180
 
 
181
 
 
182
(defthm integerp-minus
 
183
  (implies
 
184
   (integerp x)
 
185
   (integerp (- x))))
 
186
 
 
187
; Modified for Version 2.6 and further for v2-7 by Matt Kaufmann:
 
188
(defthm update-nth-memp
 
189
  (implies
 
190
   (and
 
191
    (memp mem)
 
192
    (< n (len mem))
 
193
    (integerp n)
 
194
    (>= n 0))
 
195
   (equal (memp (update-nth n val mem))
 
196
          (and
 
197
           (<= (- (expt 2 31)) val)
 
198
           (< val (expt 2 31)) ; modified by Matt K. for v2-7
 
199
           (integerp val))))
 
200
  :hints (("goal" :in-theory (enable update-nth))))
 
201
 
 
202
; Modified by Matt Kaufmann for ACL2 Version 2.6.
 
203
(defthm arb-memory-proof 
 
204
  (implies
 
205
   (and
 
206
    (memp mem)
 
207
    (< n2 (len mem))
 
208
    (<= 0 n2))
 
209
   (and
 
210
    (<= (nth n2 mem) (MAX_INT<32>))
 
211
    (<= (MIN_INT<32>) (nth n2 mem))
 
212
    (integerp (nth n2 mem))))
 
213
  :hints (("goal" :in-theory (enable nth)))
 
214
  :rule-classes nil)
 
215
 
 
216
;; an element of memory is a 32-bit quantity.  Really.
 
217
; Modified by Matt Kaufmann for ACL2 Version 2.6.
 
218
(defthm arb-memory
 
219
  (implies
 
220
   (and
 
221
    (memp mem)
 
222
    (< n2 (len mem))
 
223
    (<= 0 n2))
 
224
   (and
 
225
    (<= (nth n2 mem) (MAX_INT<32>))
 
226
    (< (nth n2 mem) 2147483648)
 
227
    (not (< 2147483648 (NTH n2 mem))) ; needed later on.
 
228
    (<= (MIN_INT<32>) (nth n2 mem))
 
229
    (implies (not (equal (min_int<32>) (nth n2 mem))) 
 
230
             (< (MIN_INT<32>) (nth n2 mem)))
 
231
    (integerp (nth n2 mem))
 
232
    (rationalp (nth n2 mem))
 
233
    (acl2-numberp (nth n2 mem))))
 
234
  :hints (("goal" :use arb-memory-proof)))
 
235
 
 
236
; Always move the negation to the constant
 
237
(defthm less-neg-const
 
238
  (implies
 
239
   (syntaxp (quotep y))
 
240
   (and
 
241
    (iff (< (- x) y) (> x (- y)))
 
242
    (iff (< y (- x)) (> (- y) x))
 
243
    (iff (<= (- x) y) (>= x (- y)))
 
244
    (iff (<= y (- x)) (>= (- y) x))))
 
245
  :rule-classes ((:rewrite :loop-stopper nil)))
 
246
 
 
247
; Added by Matt K. for v2-7 to help with some guard proofs.
 
248
(in-theory (enable unsigned-byte-p))
 
249
 
 
250
;; Push a value onto the user stack.
 
251
(defun pushus (val st)
 
252
  (declare (type (signed-byte 32) val)
 
253
           (xargs :stobjs (st)
 
254
                  :guard (stp st)))
 
255
  (let ((dtos (dtos st)))
 
256
    (declare (type (unsigned-byte 10) dtos))
 
257
    (let ((st (update-memi dtos (Int32 val) st)))
 
258
      (update-dtos (+|10| dtos -1) st))))
 
259
 
 
260
;; Pop a value off the user stack.
 
261
(defun popus (address st)
 
262
  (declare (type (unsigned-byte 10) address)
 
263
           (xargs :stobjs (st)
 
264
                  :guard (stp st)))
 
265
  (let ((ndtos (+|10| (dtos st) 1)))
 
266
    (declare (type (unsigned-byte 10) ndtos))
 
267
    (let ((st (update-memi address (memi ndtos st) st)))
 
268
      (update-dtos ndtos st))))
 
269
 
 
270
;; Push a value on the call stack.
 
271
(defun pushcs (val st)
 
272
  (declare (type (signed-byte 32) val)
 
273
           (xargs :stobjs (st)
 
274
                  :guard (stp st)))
 
275
  (let ((ctos (ctos st)))
 
276
    (declare (type (unsigned-byte 10) ctos))
 
277
    (let ((st (update-memi ctos (Int32 val) st)))
 
278
     (update-ctos (+|10| ctos -1) st))))
 
279
 
 
280
;; Pop a value off the call stack
 
281
(defun popcs (address st)
 
282
  (declare (type (unsigned-byte 10) address)
 
283
           (xargs :stobjs (st)
 
284
                  :guard (stp st)))
 
285
  (let ((nctos (+|10| (ctos st) 1)))
 
286
    (declare (type (unsigned-byte 10) nctos))
 
287
    (let ((st (update-memi address (memi nctos st) st)))
 
288
      (update-dtos nctos st))))
 
289
 
 
290
;; Define the TINY instructions by defining the effect of executing
 
291
;; the current instruction.
 
292
(defun next (st)
 
293
  (declare (xargs :stobjs (st)
 
294
                  :guard (stp st)
 
295
                  :guard-hints (("goal" :in-theory
 
296
                                 (disable hard-error pushus popus pushcs)))))
 
297
  (let ((progc (progc st))
 
298
        (dtos  (dtos st))
 
299
        (ctos  (ctos st)))
 
300
    (declare (type (unsigned-byte 10) progc dtos ctos))
 
301
 
 
302
    (let ((ins (memi progc st)))
 
303
      (declare (type (signed-byte 32) ins))
 
304
 
 
305
      (case ins
 
306
        ; pop
 
307
        (0 (let ((st (update-progc (+|10| progc 2) st)))
 
308
            (popus (fix|10| (memi (+|10| progc 1) st)) st)))
 
309
 
 
310
        ; pushs
 
311
        (1 (let ((st (update-progc (+|10| progc 2) st)))
 
312
            (pushus (memi (fix|10| (memi (+|10| progc 1) st)) st) st)))
 
313
 
 
314
        ; pushsi
 
315
        (2 (let ((st (update-progc (+|10| progc 2) st)))
 
316
            (pushus (memi (+|10| progc 1) st) st)))
 
317
 
 
318
        ; add
 
319
        (3 (let ((st (update-progc (+|10| progc 1) st)))
 
320
             (let ((st (update-dtos (+|10| dtos 2) st)))
 
321
               (pushus (add<32> (Int32 (memi (+|10| dtos 1) st))
 
322
                                (Int32 (memi (+|10| dtos 2) st)))
 
323
                       st))))
 
324
 
 
325
        ; jump
 
326
        (4 (update-progc (fix|10| (memi (+|10| progc 1) st)) st))
 
327
 
 
328
        ; jumpz
 
329
        (5 (let ((nprogc (if (= (memi (+|10| dtos 1) st) 0)
 
330
                             (fix|10| (memi (+|10| progc 1) st))
 
331
                           (+|10| progc 2))))
 
332
             (declare (type (unsigned-byte 10) nprogc))
 
333
             (let ((st (update-progc nprogc st)))
 
334
               (update-dtos (+|10| dtos 1) st))))
 
335
 
 
336
        ; call
 
337
        (6 (let ((nadd (fix|10| (memi (+|10| progc 1) st))))
 
338
             (declare (type (unsigned-byte 10) nadd))
 
339
             (let ((st (update-progc nadd st)))
 
340
              (pushcs (+|10| progc 2) st))))
 
341
 
 
342
        ; return
 
343
        (7 (let ((nadd (fix|10| (memi (+|10| ctos 1) st))))
 
344
             (declare (type (unsigned-byte 10) nadd))
 
345
             (let ((st (update-progc nadd st)))
 
346
              (update-ctos (+|10| ctos 1) st))))
 
347
 
 
348
        ; sub
 
349
        (8 (let ((st (update-progc (+|10| progc 1) st)))
 
350
             (let ((st (update-dtos (+|10| dtos 2) st)))
 
351
               (pushus (max<32> 0 (sub<32> (memi (+|10| dtos 2) st)
 
352
                                           (memi (+|10| dtos 1) st)))
 
353
                       st))))
 
354
 
 
355
        ; dup
 
356
        (9 (let ((st (update-progc (+|10| progc 1) st)))
 
357
            (pushus (memi (+|10| dtos 1) st) st)))
 
358
 
 
359
        ; halt
 
360
        (otherwise st)))))
 
361
 
 
362
(defthm stp-next
 
363
  (implies
 
364
   (stp st)
 
365
   (stp (next st))))
 
366
 
 
367
(defun tiny (st n)
 
368
  (declare (xargs :stobjs (st)
 
369
                  :guard (stp st)
 
370
                  :guard-hints (("goal" :in-theory (disable next stp))))
 
371
           (type (signed-byte 32) n))
 
372
  (if (or (not (integerp (Int32 n))) (<= (Int32 n) (Int32 0)))   ; ifix inefficient
 
373
      st
 
374
    (let ((st (next st)))
 
375
      (tiny st (Int32 (1- (Int32 n)))))))
 
376
 
 
377
 
 
378
;;;;;
 
379
;; Functions for creating Tiny state
 
380
 
 
381
;; Note: recursive functions involving s.t. objects must have a base
 
382
;; case listed first.  Presumably ACL2 has this restriction in order
 
383
;; to allow ACL2 a simpler approach for determining whether a function
 
384
;; returns all the s.t. objects it needs to return, since every base
 
385
;; case must return every potentially-modified s.t. object.
 
386
 
 
387
(defun load-memory-block (address list st)
 
388
  (declare (xargs :stobjs (st)
 
389
                  :guard (stp st)
 
390
                  :verify-guards nil))
 
391
  (if (not (consp list)) st
 
392
      (let ((st (update-memi address (car list) st)))
 
393
        (load-memory-block (+|10| address 1) (cdr list) st))))
 
394
  
 
395
(defun load-memory (assoc st)
 
396
  (declare (xargs :stobjs (st)
 
397
                  :verify-guards nil))
 
398
  (if (not (consp assoc)) st
 
399
    (let ((st (load-memory-block (caar assoc) (cdar assoc) st)))
 
400
      (load-memory (cdr assoc) st))))
 
401
 
 
402
(defun load-tiny (pc memlist st)
 
403
  (declare (xargs :stobjs (st)
 
404
                  :verify-guards nil))
 
405
  (let ((st (update-progc pc st)))
 
406
    (let ((st (update-dtos 900 st)))
 
407
      (let ((st (update-ctos 1000 st)))
 
408
        (load-memory memlist st)))))
 
409
 
 
410
(defun encode (op)
 
411
  (declare (xargs :verify-guards nil))
 
412
  (case op
 
413
    ('pop 0)
 
414
    ('pushs 1)
 
415
    ('pushsi 2)
 
416
    ('add 3)
 
417
    ('jump 4)
 
418
    ('jumpz 5)
 
419
    ('call 6)
 
420
    ('ret 7)
 
421
    ('sub 8)
 
422
    ('dup 9)
 
423
    ('halt 10)))
 
424
 
 
425
(defun assemble (code)
 
426
  (declare (xargs :verify-guards nil))
 
427
  (if (consp code)
 
428
      (cons
 
429
       (if (integerp (car code)) (car code) (encode (car code)))
 
430
       (assemble (cdr code)))
 
431
    nil))
 
432
 
 
433
(defconst *mod-caller-prog* (assemble '(pushsi 0 pushsi 1 add pushsi 100 call 20 jump 6)))
 
434
 
 
435
(defconst *mod-prog* (assemble '(pop 19   ;20
 
436
                                 pop 18
 
437
                                 pushs 18 ;24
 
438
                                 pushs 19
 
439
                                 sub
 
440
                                 dup
 
441
                                 jumpz 36
 
442
                                 pop 18
 
443
                                 jump 24
 
444
                                 pushs 19 ;36
 
445
                                 pushs 18
 
446
                                 sub
 
447
                                 jumpz 45
 
448
                                 jump 49
 
449
                                 pushsi 0 ;45 
 
450
                                 pop 18
 
451
                                 pop 19   ;49
 
452
                                 pushs 18
 
453
                                 ret
 
454
                                 )))
 
455
 
 
456
(defun run-example-tiny-state (n st)
 
457
  (declare (xargs :verify-guards nil :stobjs (st)))
 
458
  (let ((st (load-tiny 4 (list (cons 4 *mod-caller-prog*) (cons 20 *mod-prog*)) st)))
 
459
    (tiny st n)))
 
460
 
 
461
#|  
 
462
ACL2 !>:q
 
463
 
 
464
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
 
465
ACL2>(time (run-example-tiny-state 10000000 st))
 
466
real time : 12.000 secs
 
467
run time  : 12.010 secs
 
468
(#(9)
 
469
 #(0 0 0 0 2 0 2 1 3 2 100 6 20 4 6 0 0 0 50 0 0 19 0 18 1 18 1 19 8 9
 
470
   5 36 0 18 4 24 1 19 1 18 8 5 45 4 49 2 0 0 18 0 19 1 18 7 0 0 0 0 0
 
471
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
472
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
473
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
474
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
475
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
476
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
477
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
478
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
479
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
480
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
481
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
482
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
483
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
484
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
485
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
486
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
487
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
488
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
489
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
490
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
491
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
492
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
493
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
494
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
495
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 50 1 51 0 0 0 0 0 0 0
 
496
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
497
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
 
498
   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 13 0 0 0 0 0 0 0 0 0
 
499
   0 0 0 0 0 0 0 0 0 0 0 0 0 0)
 
500
 #(899) #(1000))
 
501
 
 
502
ACL2>
 
503
 
 
504
|#
 
505
 
 
506
;;;;;
 
507
;;;;;  Proof about the benchmark program
 
508
;;;;;
 
509
 
 
510
;;; The proof begins with many preliminaries that help us reason about
 
511
;;; programs of this type.
 
512
 
 
513
;;; We are not interested in guard-proofs about functions we 
 
514
;;; use for specification and proof
 
515
(set-verify-guards-eagerness 0) 
 
516
 
 
517
;; Is "program" loaded at "location" in Tiny state?
 
518
(defun program-loaded (st program location)
 
519
  (declare (xargs :stobjs (st)))
 
520
  (if (consp program) 
 
521
      (and
 
522
       (equal (memi location st) (car program))
 
523
       (program-loaded st (cdr program) (1+ location)))
 
524
    t))
 
525
 
 
526
(defthm prog-lookup
 
527
  (implies
 
528
   (and
 
529
    (syntaxp (quotep n))
 
530
    (program-loaded st prog loc)
 
531
    (integerp loc)
 
532
    (<= loc (nfix n))
 
533
    (< (nfix n) (+ loc (len prog))))
 
534
   (equal (nth n (nth (memloc) st))
 
535
          (nth (- n loc) prog)))
 
536
  :hints (("goal" :in-theory (enable len nth))))
 
537
 
 
538
(in-theory (disable program-loaded))
 
539
 
 
540
(defthm +bv32-simple
 
541
  (implies
 
542
   (and
 
543
    (integerp x) (integerp y)
 
544
    (< x (expt 2 30)) ; modified by Matt K. for v2-7
 
545
    (>= x (- (expt 2 30)))
 
546
    (< y (expt 2 30)) ; modified by Matt K. for v2-7
 
547
    (>= y (- (expt 2 30))))
 
548
   (equal (+bv32 x y) (+ x y)))
 
549
  :hints (("goal" :in-theory (enable +bv32 signed-byte-p))))
 
550
 
 
551
(defthm +bv32-simple2
 
552
  (implies
 
553
   (and
 
554
    (integerp x) (integerp y)
 
555
    (< x (expt 2 31)) ; modified by Matt K. for v2-7
 
556
    (>= x 0)
 
557
    (< y (expt 2 31)) ; modified by Matt K. for v2-7
 
558
    (>= y 0))
 
559
   (equal (+bv32 x (- y)) (+ x (- y))))
 
560
  :hints (("goal" :in-theory (enable +bv32 signed-byte-p))))
 
561
  
 
562
(defthm logand-1023-hack
 
563
  (implies
 
564
   (and
 
565
    (<= 0 x)
 
566
    (<= x 1023)
 
567
    (integerp x))
 
568
   (equal (logand x 1023) x))
 
569
  :hints (("goal" :in-theory (enable unsigned-byte-p))))
 
570
 
 
571
(defthm +bv32-0
 
572
  (implies
 
573
   (and
 
574
    (integerp x)
 
575
    (< x (expt 2 31)) ; modified by Matt K. for v2-7
 
576
    (<= (- (expt 2 31)) x))
 
577
   (equal (+bv32 x 0) x))
 
578
  :hints (("goal" :in-theory  (enable +bv32 signed-byte-p))))
 
579
 
 
580
(defthm tiny-straightline
 
581
  (implies
 
582
   (syntaxp (quotep n))
 
583
   (equal (tiny st n) 
 
584
          (if (zp n) st (tiny (next st) (1- n)))))
 
585
  :hints (("goal" :in-theory (disable next))))
 
586
 
 
587
(defun c+ (x y) (+ (nfix x) (nfix y)))
 
588
 
 
589
(defthm tiny-c+
 
590
  (equal (tiny s (c+ x y))
 
591
         (tiny (tiny s x) y))
 
592
  :hints (("goal" :induct (tiny s x)
 
593
           :in-theory (set-difference-theories (enable tiny) '(next)))))
 
594
 
 
595
(in-theory (disable c+))
 
596
 
 
597
(defthm integerp-max
 
598
  (implies
 
599
   (and (integerp a) (integerp b))
 
600
   (integerp (max a b))))
 
601
 
 
602
(defthm max-less
 
603
  (and
 
604
   (equal
 
605
    (< (max a b) c)
 
606
    (and (< a c) (< b c)))
 
607
   (equal
 
608
    (< c (max a b))
 
609
    (or (< c a) (< c b)))))
 
610
 
 
611
(defthm equal-max-x-x
 
612
  (implies
 
613
   (and (integerp b) (integerp a))
 
614
  (and
 
615
   (equal (equal (max a b) a) (<= b a))
 
616
   (equal (equal (max b a) a) (<= b a))))
 
617
  :hints (("goal" :in-theory (enable max))))
 
618
 
 
619
(in-theory (disable max))
 
620
 
 
621
(defthm equal-plus-x-x
 
622
  (implies
 
623
   (and (integerp b) (integerp a))
 
624
   (equal (equal (+ a b) b) (equal a 0))))
 
625
 
 
626
(defthm integerp-unary--
 
627
  (implies
 
628
   (integerp x)
 
629
   (integerp (unary-- x))))
 
630
 
 
631
(defthm integerp-+
 
632
  (implies
 
633
   (and
 
634
    (integerp x)
 
635
    (integerp y))
 
636
   (integerp (+ x y))))
 
637
 
 
638
(in-theory (disable tiny))
 
639
 
 
640
(defthm less-minus-hack
 
641
  (implies
 
642
   (and
 
643
    (integerp a)
 
644
    (integerp b)
 
645
    (< 0 a)
 
646
    (<= 0 b))
 
647
   (not (< a (- b)))))
 
648
 
 
649
(defthm lessp-minus-hack3
 
650
 (implies
 
651
  (and
 
652
   (<= a n)
 
653
   (<= b n)
 
654
   (< 0 b)
 
655
   (integerp a)
 
656
   (integerp b)
 
657
   (integerp n))
 
658
  (equal (< n (+ (- b) a)) nil)))
 
659
 
 
660
(defthm lessp-minus-hack4
 
661
 (implies
 
662
  (and
 
663
   (<= a n)
 
664
   (<= b n)
 
665
   (<= 0 b)
 
666
   (integerp a)
 
667
   (integerp b)
 
668
   (integerp n))
 
669
  (<= (+ a (- b)) n)))
 
670
 
 
671
(defthm max-0-a-b
 
672
  (and
 
673
   (implies (<= a b) (equal (max 0 (+ a (- b))) 0))
 
674
   (implies (>= a b) (equal (max 0 (+ a (- b))) (+ a (- b)))))
 
675
  :hints (("goal" :in-theory (enable max))))
 
676
 
 
677
(defthm max-open
 
678
  (implies
 
679
   (and
 
680
    (<= a b)
 
681
    (integerp a) (integerp b))
 
682
   (equal (max a b) b)))
 
683
 
 
684
;; Try to backchain on nth-update-nth before casesplitting
 
685
(defthm nth-update-nth2
 
686
   (equal
 
687
    (nth n1 (update-nth n2 v l))
 
688
    (if (equal (nfix n1) (nfix n2))
 
689
        v
 
690
      (nth n1 l)))
 
691
  :hints (("goal" :in-theory (enable update-nth nth))))
 
692
 
 
693
(defthm nth-update-nth-1
 
694
  (implies
 
695
    (not (equal (nfix n1) (nfix n2)))
 
696
   (equal
 
697
    (nth n1 (update-nth n2 v l))
 
698
    (nth n1 l))))
 
699
 
 
700
(defthm nth-update-nth-2
 
701
  (implies
 
702
    (equal (nfix n1) (nfix n2))
 
703
   (equal
 
704
    (nth n1 (update-nth n2 v l))
 
705
    v)))
 
706
 
 
707
(defun repeat (n v)
 
708
  (if (zp n)
 
709
      nil
 
710
    (cons v (repeat (1- n) v))))
 
711
 
 
712
(defthm update-nth-nil
 
713
  (equal (update-nth i v nil)
 
714
         (append (repeat i nil) (list v)))
 
715
  :hints (("goal" :in-theory (enable update-nth))))
 
716
 
 
717
(defthm update-nth-nth-noop-helper
 
718
  (implies
 
719
   (and (<= 0 n) (< n (len l)))
 
720
   (equal (update-nth n (nth n l) l) l))
 
721
  :hints (("goal" :in-theory (enable nth update-nth))))
 
722
 
 
723
(defthm update-nth-nth-noop
 
724
  (implies
 
725
   (and (<= 0 n) (< n (len l1)) (equal (nth n l1) (nth n l2)))
 
726
   (equal (update-nth n (nth n l2) l1) l1)))
 
727
 
 
728
;; order update-nth terms based on update field value
 
729
(defthm update-nth-update-nth-diff
 
730
  (implies
 
731
   (not (equal (nfix i1) (nfix i2)))
 
732
   (equal (update-nth i1 v1 (update-nth i2 v2 l))
 
733
          (update-nth i2 v2 (update-nth i1 v1 l))))
 
734
  :hints (("goal" :in-theory (enable update-nth)))
 
735
  :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))
 
736
 
 
737
(defthm update-nth-update-nth-same
 
738
  (equal (update-nth i v1 (update-nth i v2 l))
 
739
         (update-nth i v1 l))
 
740
  :hints (("goal" :in-theory (enable update-nth))))
 
741
 
 
742
(defthm len-repeat
 
743
  (equal (len (repeat i v)) (nfix i)))
 
744
 
 
745
(defthm len-update-nth-better
 
746
  (equal (len (update-nth i v l)) (max (1+ (nfix i)) (len l)))
 
747
  :hints (("goal" :in-theory (enable update-nth max))))
 
748
 
 
749
(defthm car-update-nth
 
750
  (equal (car (update-nth i v l)) (if (zp i) v (car l)))
 
751
  :hints (("goal" :in-theory (enable update-nth))))  
 
752
 
 
753
(defthm len-pushus
 
754
  (implies
 
755
   (equal (len st) 4)
 
756
   (equal (len (pushus val st)) 4))
 
757
  :hints (("goal" :in-theory (disable logand-with-mask))))
 
758
 
 
759
(defthm cancel-plus-hack
 
760
  (implies
 
761
   (and (integerp x) (integerp y))
 
762
   (equal (equal (+ y x) y) (equal (fix x) 0))))
 
763
 
 
764
(defthm car-append
 
765
  (equal (car (append x y))
 
766
         (if (consp x) (car x) (car y))))
 
767
 
 
768
(defthm cdr-append
 
769
  (equal (cdr (append x y))
 
770
         (if (consp x) (append (cdr x) y) (cdr y))))
 
771
 
 
772
(defthm equal-plus-0
 
773
  (implies
 
774
   (and (integerp a) (integerp b) (<= 0 a) (<= 0 b))
 
775
   (equal (equal 0 (+ a b)) (and (equal a 0) (equal b 0)))))
 
776
 
 
777
(defthm cancel-hack
 
778
  (implies
 
779
   (rationalp x)
 
780
   (equal (< (+ x y) (+ x z)) (< y z)))
 
781
  :rule-classes nil)
 
782
 
 
783
(defthm less-quoted-hack
 
784
  (implies
 
785
   (and
 
786
    (rationalp x)
 
787
    (syntaxp (quotep a))
 
788
    (syntaxp (quotep b))
 
789
    (rationalp b))
 
790
   (equal (< a (+ b x)) (< (- a b) x)))
 
791
  :hints (("goal" :use ((:instance cancel-hack (x (- b)) (y a) (z (+ b x))))
 
792
           :in-theory (disable CANCEL_PLUS-LESSP-CORRECT))))
 
793
 
 
794
(defthm less-quoted-hack2
 
795
  (implies
 
796
   (and
 
797
    (rationalp x)
 
798
    (syntaxp (quotep a))
 
799
    (syntaxp (quotep b))
 
800
    (rationalp b))
 
801
   (equal (< (+ b x) a) (< x (- a b))))
 
802
  :hints (("goal" :use ((:instance cancel-hack (x (- b)) (z a) (y (+ b x))))
 
803
           :in-theory (disable CANCEL_PLUS-LESSP-CORRECT))))
 
804
 
 
805
(defthm lessp-hack-of-hacks
 
806
  (implies
 
807
   (and
 
808
    (not (< i1 i2))
 
809
    (<= i3 i2))
 
810
   (equal (< i1 i3) nil)))
 
811
 
 
812
(defthm equal-nat-neg-0
 
813
  (implies
 
814
   (and
 
815
   (integerp n1)
 
816
   (integerp n2)
 
817
   (<= 0 n1)
 
818
   (<= 0 n2))
 
819
   (and
 
820
    (equal (equal (+ n1 (- n2)) 0) (equal n1 n2))
 
821
    (equal (equal (+ (- n2) n1) 0) (equal n1 n2)))))
 
822
 
 
823
(defthm car-nthcdr
 
824
  (equal (car (nthcdr n l)) (nth n l))
 
825
  :hints (("goal" :in-theory (enable nth))))
 
826
 
 
827
(in-theory (disable next logand floor len update-nth max))
 
828
 
 
829
(in-theory (enable +bv32))
 
830
 
 
831
;; From J's library
 
832
(defthm iff-equal
 
833
   (implies (and (iff x y)
 
834
                 (booleanp x)
 
835
                 (booleanp y))
 
836
            (equal x y))
 
837
   :rule-classes nil)
 
838
 
 
839
(defthm lessp-unary---hack
 
840
  (implies
 
841
   (and
 
842
    (syntaxp (quotep n2))
 
843
    (integerp n1) (integerp n2))
 
844
   (equal
 
845
    (< (unary-- n1) n2)
 
846
    (< (unary-- n2) n1)))
 
847
  :hints (("goal" :use (:instance iff-equal (x (< (unary-- n1) n2)) (y (< (unary-- n2) n1))))))
 
848
 
 
849
;; We start proving facts about the benchmark 
 
850
 
 
851
;; Effect of running loop once (taken from theorem prover output)
 
852
(defun mod-loop-once-effect (st)
 
853
  (update-nth (progcloc) 24
 
854
           (update-nth (memloc)
 
855
                    (update-nth 18
 
856
                             (+ (nth 18 (nth (memloc) st))
 
857
                                (- (nth 19 (nth (memloc) st))))
 
858
                             (update-nth (nth (dtosloc) st)
 
859
                                      (+ (nth 18 (nth (memloc) st))
 
860
                                         (- (nth 19 (nth (memloc) st))))
 
861
                                      (update-nth (+ -1 (nth (dtosloc) st))
 
862
                                               (+ (nth 18 (nth (memloc) st))
 
863
                                                  (- (nth 19 (nth (memloc) st))))
 
864
                                               (nth (memloc) st))))
 
865
                    (update-nth (dtosloc) (nth (dtosloc) st) st))))
 
866
 
 
867
(in-theory (disable update-nth-update-nth))
 
868
(in-theory (enable len))
 
869
 
 
870
(defthm mod-loop-repeat
 
871
  (implies
 
872
   (and
 
873
    (stp st)
 
874
    (< (dtos st) 1000) (>= (dtos st) 100)
 
875
    (equal (progc st) 24)
 
876
    (program-loaded st *mod-prog* 20)
 
877
    (<= 0 (memi 19 st))
 
878
    (<= 0 (memi 18 st))
 
879
    (< (memi 19 st) (memi 18 st))
 
880
    (not (= (memi 19 st) (memi 18 st)))) ;;redundant, but simplifies proof
 
881
   (equal (tiny st 7)
 
882
          (mod-loop-once-effect st)))
 
883
  :hints (("goal''" :in-theory (enable next signed-byte-p len))))
 
884
 
 
885
;; Effect of loop when it ends with no adjust needed (expression taken
 
886
;;from theorem prover output)
 
887
(defthm mod-loop-end1
 
888
  (implies
 
889
   (and
 
890
    (stp st)
 
891
    (< (dtos st) 1000) (>= (dtos st) 100)
 
892
    (<= (ctos st) 1020) (> (ctos st) 1010)
 
893
    (equal (progc st) 24)
 
894
    (program-loaded st *mod-prog* 20)
 
895
    (<= 0 (memi 19 st))
 
896
    (< 0 (memi 18 st))
 
897
    (> (memi 19 st) (memi 18 st))
 
898
    (not (= (memi 19 st) (memi 18 st)))) ;;redundant
 
899
   (equal (tiny st 13)
 
900
          (update-nth (progcloc)
 
901
             (logand (nth (+ 1 (nth (ctosloc) st)) (nth (memloc) st))
 
902
                     1023)
 
903
             (update-nth (memloc)
 
904
                      (update-nth 19 0
 
905
                               (update-nth (nth (dtosloc) st)
 
906
                                        (nth 18 (nth (memloc) st))
 
907
                                        (update-nth (+ -1 (nth (dtosloc) st))
 
908
                                                 (+ (- (nth 18 (nth (memloc) st)))
 
909
                                                    (nth 19 (nth (memloc) st)))
 
910
                                                 (update-nth (+ -2 (nth (dtosloc) st))
 
911
                                                          (nth 18 (nth (memloc) st))
 
912
                                                          (nth (memloc) st)))))
 
913
                      (update-nth (dtosloc) (+ -1 (nth (dtosloc) st))
 
914
                               (update-nth (ctosloc) (+ 1 (nth (ctosloc) st)) st))))))
 
915
  :hints (("goal''" :in-theory (enable next signed-byte-p))))
 
916
 
 
917
;; Effect of loop when it ends with an adjust needed (expression taken
 
918
;;from theorem prover output)
 
919
(defthm mod-loop-end2
 
920
  (implies
 
921
   (and
 
922
    (stp st)
 
923
    (< (dtos st) 1000) (>= (dtos st) 100)
 
924
    (<= (ctos st) 1020) (> (ctos st) 1010)
 
925
    (equal (progc st) 24)
 
926
    (program-loaded st *mod-prog* 20)
 
927
    (<= 0 (memi 19 st))
 
928
    (< 0 (memi 18 st))
 
929
    (= (memi 19 st) (memi 18 st)))
 
930
   (equal (tiny st 14)
 
931
          (update-nth
 
932
           (progcloc)
 
933
           (logand (nth (+ 1 (nth (ctosloc) st)) (nth (memloc) st))
 
934
                   1023)
 
935
           (update-nth (memloc)
 
936
                    (update-nth 18 0
 
937
                             (update-nth 19 0
 
938
                                      (update-nth (nth (dtosloc) st)
 
939
                                               0
 
940
                                               (update-nth (+ -1 (nth (dtosloc) st))
 
941
                                                        0
 
942
                                                        (update-nth (+ -2 (nth (dtosloc) st))
 
943
                                                                 (nth 18 (nth (memloc) st))
 
944
                                                                 (nth (memloc) st))))))
 
945
                    (update-nth (dtosloc) (+ -1 (nth (dtosloc) st))
 
946
                             (update-nth (ctosloc) (+ 1 (nth (ctosloc) st)) st))))))
 
947
  :hints (("goal''" :in-theory (enable next signed-byte-p))))
 
948
 
 
949
;; number of instructions needed to execute loop for values x and y.
 
950
(defun modloop-clock-helper (x y)
 
951
  (if (or (not (integerp x)) (not (integerp y)) (>= 0 y) (<= x y))
 
952
      (if (equal x y) 14 13)
 
953
    (c+ 7 (modloop-clock-helper (- x y) y))))
 
954
 
 
955
(defun modloop-clock (st)
 
956
  (declare (xargs :stobjs (st)))
 
957
  (let ((x (memi 18 st)) (y (memi 19 st)))
 
958
    (modloop-clock-helper x y)))
 
959
 
 
960
(defun remainder-prog-result (n p)
 
961
  (if (or (zp p) (zp n) (< n p))
 
962
      (nfix n)
 
963
    (remainder-prog-result (- n p) p)))
 
964
 
 
965
(set-irrelevant-formals-ok :warn)
 
966
 
 
967
(defun mod-loop-repeat-induct (x y s)
 
968
  (if (or (not (integerp x)) (not (integerp y)) (>= 0 y) (<= x y))
 
969
      t
 
970
    (mod-loop-repeat-induct (- x y) y (mod-loop-once-effect s))))
 
971
 
 
972
(defthm less-+-1024-hack
 
973
  (implies
 
974
   (and
 
975
    (integerp n)
 
976
    (integerp p))
 
977
   (iff (< (+ p n) 1024) (< n (+ (- p) 1024)))))
 
978
 
 
979
; Modified by Matt Kaufmann for ACL2 Version 2.6.
 
980
(defthm memp-update-nth
 
981
  (implies
 
982
   (and
 
983
    (memp l)
 
984
    (integerp a)
 
985
    (<= 0 a)
 
986
    (< a (len l)))
 
987
   (equal (memp (update-nth a v l))
 
988
          (AND (INTEGERP v) (<= -2147483648 v) (<= v 2147483647))))
 
989
  :hints (("goal" :in-theory (enable update-nth))))
 
990
 
 
991
(defthm lessp-minus-hack5
 
992
  (implies
 
993
   (and
 
994
    (not (> b (- n)))
 
995
    (<= 0 a)
 
996
    (integerp a)
 
997
    (integerp b)
 
998
    (integerp c))
 
999
   (not (< (+ a (- b)) n))))
 
1000
 
 
1001
(in-theory (enable max))
 
1002
 
 
1003
(defun sub1-add1-cdr (n1 n2 l)
 
1004
  (if (consp l)
 
1005
      (sub1-add1-cdr (1- n1) (1+ n2) (cdr l))
 
1006
    t))
 
1007
 
 
1008
(defthm update-nth-equal
 
1009
  (implies
 
1010
   (and
 
1011
    (< n (len l))
 
1012
    (<= 0 n) (integerp n))
 
1013
   (equal (update-nth n (nth n l) l) l))
 
1014
  :hints (("goal" :in-theory (enable nth update-nth len))))
 
1015
 
 
1016
(defthm program-loaded-irrelevant
 
1017
  (implies
 
1018
   (not (equal n 1))
 
1019
   (equal (program-loaded (update-nth n v st) prog loc)
 
1020
          (program-loaded st prog loc)))
 
1021
  :hints (("goal" :in-theory (enable update-nth program-loaded))))
 
1022
 
 
1023
 
 
1024
;; such a screwy rule.  It's inelegant because program-loaded is a function
 
1025
;; of state.
 
1026
(defthm program-loaded-cons
 
1027
  (implies
 
1028
   (and
 
1029
    (or (< n loc) (< (+ (len prog) loc) n) (equal val (nth n mem)))
 
1030
    (integerp n) (<= 0 n) (integerp loc) (<= 0 loc)
 
1031
    (program-loaded (update-nth 1 mem st) prog loc))
 
1032
   (program-loaded (update-nth 1 (update-nth n val mem) st) prog loc))
 
1033
  :hints (("goal" :in-theory (enable program-loaded update-nth nth len))))
 
1034
 
 
1035
(defthm lessp-hack1
 
1036
  (implies
 
1037
   (and
 
1038
    (<= a b)
 
1039
    (< c a))
 
1040
   (equal (< c b) t)))
 
1041
 
 
1042
(defthm mod-loop-calculates-mod
 
1043
  (implies
 
1044
   (and
 
1045
    (stp st)
 
1046
    (< (dtos st) 1000) (>= (dtos st) 100)
 
1047
    (<= (ctos st) 1020) (> (ctos st) 1010)
 
1048
    (equal (progc st) 24)
 
1049
    (program-loaded st *mod-prog* 20)
 
1050
    (equal a (memi 18 st))
 
1051
    (equal b (memi 19 st))
 
1052
    (< 0 a) (< 0 b)
 
1053
    (equal s2 (tiny st (modloop-clock-helper a b))))
 
1054
   (equal (memi (1+ (dtos s2)) s2) (remainder-prog-result a b)))
 
1055
  :rule-classes nil
 
1056
  :hints (("goal" :in-theory (set-difference-theories
 
1057
                              (enable stp len)
 
1058
                              '(tiny-straightline))
 
1059
                              :induct (mod-loop-repeat-induct a b st))
 
1060
          ("Subgoal *1/1.1'" :expand (REMAINDER-PROG-RESULT (NTH 18 (NTH 1 ST))
 
1061
                       (NTH 19 (NTH 1 ST))))))
 
1062
 
 
1063
(defun remclock (st)
 
1064
  (declare (xargs :stobjs (st)))
 
1065
  (modloop-clock-helper (memi 18 st) (memi 19 st)))
 
1066
 
 
1067
(defun good-initial-remainder-state (st)
 
1068
  (declare (xargs :stobjs (st)))
 
1069
   (and
 
1070
    (stp st)
 
1071
    (< (dtos st) 1000) (>= (dtos st) 100)
 
1072
    (<= (ctos st) 1020) (> (ctos st) 1010)
 
1073
    (equal (progc st) 24)
 
1074
    (program-loaded st *mod-prog* 20)
 
1075
    (< 0 (memi 18 st))
 
1076
    (< 0 (memi 19 st))))
 
1077
 
 
1078
(defthm remainder-correct
 
1079
  (let ((s2 (tiny st (remclock st))))
 
1080
  (implies
 
1081
    (good-initial-remainder-state st)
 
1082
    (equal (memi (1+ (dtos s2)) s2)
 
1083
           (remainder-prog-result (memi 18 st) (memi 19 st)))))
 
1084
  :rule-classes nil
 
1085
  :hints (("goal"
 
1086
           :use ((:instance mod-loop-calculates-mod
 
1087
                            (s2 (tiny st (modloop-clock-helper (memi 18 st) (memi 19 st))))
 
1088
                            (a (memi 18 st))
 
1089
                            (b (memi 19 st))))
 
1090
           :in-theory (disable tiny-straightline))))
 
1091
 
 
1092
;;; Show that our recursive version of remainder is identical to mod.
 
1093
;;; Fortunately, Bishop Brock's been here before.
 
1094
 
 
1095
(include-book "../../../ihs/quotient-remainder-lemmas")
 
1096
 
 
1097
(defthm remainder-is-mod
 
1098
  (implies
 
1099
   (and
 
1100
    (integerp x)
 
1101
    (<= 0 x)
 
1102
    (integerp y)
 
1103
    (<= 0 y))
 
1104
   (equal (remainder-prog-result x y) (mod x y))))
 
1105
 
 
1106
(defthm mod-correct
 
1107
  (let ((s2 (tiny st (remclock st))))
 
1108
  (implies
 
1109
    (good-initial-remainder-state st)
 
1110
    (equal (memi (1+ (dtos s2)) s2)
 
1111
           (mod (memi 18 st) (memi 19 st)))))
 
1112
  :rule-classes nil
 
1113
  :hints (("goal" :use ((:instance remainder-correct)))))
 
1114