← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/trivial/basic-def.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/2000/manolios/pipeline/trivial/basic-def.lisp
 
1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
2
; Basic-def.lisp: 
 
3
; Copyright reserved by SRC
 
4
; Author  Jun Sawada, University of Texas at Austin
 
5
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;'
 
6
 
 
7
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
8
;; This file includes various underlying definition for ISA and
 
9
;; MA designs.
 
10
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
11
(in-package "ACL2")
 
12
 
 
13
(include-book "../../../../../data-structures/array1")
 
14
(include-book "../../../../../data-structures/deflist")
 
15
(include-book "../../../../../data-structures/list-defthms")
 
16
(include-book "../../../../../data-structures/structures")
 
17
(include-book "ihs")
 
18
 
 
19
(include-book "trivia")
 
20
(include-book "b-ops-aux")
 
21
 
 
22
(deflabel begin-basic-def)
 
23
 
 
24
(defconst *addr-size* 16)
 
25
(defconst *page-offset-size* 10)
 
26
 
 
27
(defconst *rname-size* 4)
 
28
(defconst *immediate-size* 8)
 
29
(defconst *opcode-size* 4)
 
30
(defconst *word-size* 16)
 
31
(defconst *max-word-value* (expt 2 *word-size*))
 
32
(defconst *num-regs* (expt 2 *rname-size*))
 
33
(defconst *num-mem-words* (expt 2 *addr-size*))
 
34
(defconst *num-page-words* (expt 2 *page-offset-size*))
 
35
(defconst *num-pages* (expt 2 (- *addr-size* *page-offset-size*)))
 
36
(defbytetype word *word-size* :unsigned)
 
37
(defbytetype addr  *addr-size* :unsigned)
 
38
(defbytetype rname *rname-size* :unsigned)
 
39
(defbytetype immediate *immediate-size* :unsigned)
 
40
(defbytetype opcd  *opcode-size* :unsigned)
 
41
 
 
42
(defthm word-p-type
 
43
    (implies (word-p word)
 
44
             (and (integerp word)
 
45
                  (>= word 0)
 
46
                  (< word *max-word-value*)))
 
47
  :hints (("Goal" :in-theory (enable word-p)))
 
48
  :rule-classes :forward-chaining)
 
49
 
 
50
(defthm rname-p-type
 
51
    (implies (rname-p rname)
 
52
             (and (integerp rname)
 
53
                  (>= rname 0)
 
54
                  (< rname *num-regs*)))
 
55
  :hints (("Goal" :in-theory (enable rname-p)))
 
56
  :rule-classes :forward-chaining)
 
57
 
 
58
(defthm addr-p-type
 
59
    (implies (addr-p ad)
 
60
             (and (integerp ad)
 
61
                  (>= ad  0)
 
62
                  (< ad *num-mem-words*)))
 
63
 :hints (("Goal" :in-theory (enable addr-p)))
 
64
  :rule-classes :forward-chaining)
 
65
 
 
66
(defthm addr-word-double-casting
 
67
    (equal (addr (word i)) (addr i))
 
68
  :hints (("goal" :in-theory (enable addr word))))
 
69
 
 
70
(defthm word-addr-double-casting
 
71
    (equal (word (addr i)) (word i))
 
72
  :hints (("goal" :in-theory (enable addr word))))
 
73
 
 
74
 
 
75
(defthm word-addr-p
 
76
    (implies (addr-p x) (equal (word x) x))
 
77
  :hints (("goal" :in-theory (enable addr-p word))))
 
78
 
 
79
(defthm addr-word-p
 
80
    (implies (word-p x) (equal (addr x) x))
 
81
  :hints (("goal" :in-theory (enable addr word-p))))
 
82
 
 
83
(in-theory (disable word-addr-p addr-word-p))
 
84
 
 
85
(defthm word-p-logand
 
86
    (implies (and (word-p val1) (word-p val2))
 
87
             (word-p (logand val1 val2)))
 
88
  :hints (("Goal" :in-theory (enable word-p))))
 
89
 
 
90
(defthm word-p-logxor
 
91
    (implies (and (word-p val1) (word-p val2))
 
92
             (word-p (logxor val1 val2)))
 
93
  :hints (("Goal" :in-theory (enable word-p))))
 
94
 
 
95
(defthm word-p-logior
 
96
    (implies (and (word-p val1) (word-p val2))
 
97
             (word-p (logior val1 val2)))
 
98
  :hints (("Goal" :in-theory (enable word-p))))
 
99
 
 
100
(defthm word-p-bv-eqv-iff-equal
 
101
    (implies (and (word-p wd0) (word-p wd1))
 
102
             (equal (b1p (bv-eqv *word-size* wd0 wd1)) (equal wd0 wd1)))
 
103
  :hints (("Goal" :in-theory (enable word-p))))
 
104
 
 
105
(defthm addr-p-bv-eqv-iff-equal
 
106
    (implies (and (addr-p wd0) (addr-p wd1))
 
107
             (equal (b1p (bv-eqv *addr-size* wd0 wd1)) (equal wd0 wd1)))
 
108
  :hints (("Goal" :in-theory (enable addr-p))))
 
109
 
 
110
(defthm rname-p-bv-eqv-iff-equal
 
111
    (implies (and (rname-p wd0) (rname-p wd1))
 
112
             (equal (b1p (bv-eqv *rname-size* wd0 wd1)) (equal wd0 wd1)))
 
113
  :hints (("Goal" :in-theory (enable rname-p))))
 
114
 
 
115
(defthm immediate-p-bv-eqv-iff-equal
 
116
    (implies (and (immediate-p wd0) (immediate-p wd1))
 
117
             (equal (b1p (bv-eqv *immediate-size* wd0 wd1)) (equal wd0 wd1)))
 
118
  :hints (("Goal" :in-theory (enable immediate-p))))
 
119
 
 
120
(defthm opcd-p-bv-eqv-iff-equal
 
121
    (implies (and (opcd-p wd0) (opcd-p wd1))
 
122
             (equal (b1p (bv-eqv *opcode-size* wd0 wd1)) (equal wd0 wd1)))
 
123
  :hints (("Goal" :in-theory (enable opcd-p))))
 
124
 
 
125
 
 
126
(deflist word-listp (l)
 
127
  (declare (xargs :guard t))
 
128
  word-p)
 
129
 
 
130
(defun fixlen-word-listp (n lst)
 
131
  "test if list is a array of n words."
 
132
  (declare (xargs :guard (and (integerp n) (<= 0 n))))
 
133
  (and (word-listp lst) (equal (len lst) n)))
 
134
 
 
135
(defthm fixlen-word-true-listp
 
136
    (implies (fixlen-word-listp n x)
 
137
             (true-listp x))
 
138
  :rule-classes :forward-chaining)
 
139
 
 
140
(in-theory (disable fixlen-word-listp))
 
141
 
 
142
; Register file is a fixed lenghth true list of words.
 
143
(defun regs-p (regs)
 
144
  (declare (xargs :guard t))
 
145
  (fixlen-word-listp *num-regs* regs))
 
146
 
 
147
(defthm regs-p-true-listp
 
148
    (implies (regs-p x)
 
149
             (true-listp x))
 
150
  :rule-classes :forward-chaining)
 
151
 
 
152
 
 
153
(defun read-reg (num regs)
 
154
  (declare (xargs :guard (and (rname-p num) (regs-p regs))))
 
155
  (nth num regs))
 
156
 
 
157
(defun write-reg (val num regs)
 
158
  (declare (xargs :guard (and (word-p val) (rname-p num) (regs-p regs))))
 
159
  (update-nth num val regs))
 
160
 
 
161
(defthm regs-p-write-reg
 
162
    (implies (and (word-p word)
 
163
                  (rname-p rname)
 
164
                  (regs-p regs))
 
165
             (regs-p (write-reg word rname regs)))
 
166
  :hints (("Goal" :in-theory (enable regs-p fixlen-word-listp
 
167
                                     rname-p UNSIGNED-BYTE-P
 
168
                                     len-update-nth))))
 
169
 
 
170
(local
 
171
(defthm nth-content-word-listp
 
172
    (implies (and (integerp n)
 
173
                  (<= 0 n)
 
174
                  (word-listp lst)
 
175
                  (< n (len lst)))
 
176
             (and (integerp (nth n lst))
 
177
                  (acl2-numberp (nth n lst))))
 
178
  :hints (("Goal" :use ((:instance word-listp-nth (n0 n) (l lst)))
 
179
                  :in-theory (disable word-listp-nth)))))
 
180
 
 
181
 
 
182
(defthm numberp-read-reg
 
183
    (implies (and (regs-p regs)
 
184
                  (rname-p rname))
 
185
             (and (integerp (read-reg rname regs))
 
186
                  (acl2-numberp (read-reg rname regs))))
 
187
  :hints (("Goal" :in-theory (enable rname-p regs-p fixlen-word-listp)))
 
188
  :rule-classes
 
189
  ((:type-prescription) (:rewrite)))
 
190
 
 
191
(defthm word-p-read-reg
 
192
    (implies (and (regs-p regs)
 
193
                  (rname-p rname))
 
194
             (word-p (read-reg rname regs)))
 
195
  :hints (("Goal" :in-theory (enable rname-p regs-p fixlen-word-listp)))
 
196
  :rule-classes
 
197
  ((:rewrite)
 
198
   (:type-prescription :corollary
 
199
             (implies (and (regs-p regs) (rname-p rname))
 
200
                      (integerp (read-reg rname regs)))
 
201
             :hints (("goal" :in-theory (enable word-p unsigned-byte-p))))))
 
202
 
 
203
(defthm read-reg-write-reg
 
204
    (implies (and (rname-p rn1)
 
205
                  (rname-p rn2)
 
206
                  (regs-p regs))
 
207
             (equal (read-reg rn1 (write-reg val rn2 regs))
 
208
                    (if (equal rn1 rn2) val (read-reg rn1 regs))))
 
209
  :hints (("Goal" :in-theory (enable read-reg write-reg regs-p
 
210
                                     nth-update-nth))))
 
211
 
 
212
(in-theory (disable regs-p write-reg read-reg))
 
213
 
 
214
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
215
;; Here we define the memory system.
 
216
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
217
(defconst *no-access* 0)
 
218
(defconst *read-only* 1)
 
219
(defconst *read-write* 2)
 
220
 
 
221
;;  Definition of Address Transformer
 
222
;;  page-num Address --> Page number 
 
223
;;  page-offset Address --> Page Offset
 
224
(defun page-num (addr)
 
225
  (declare (xargs :guard (addr-p addr)))
 
226
  (floor addr *num-page-words*))
 
227
 
 
228
(defun page-offset (addr)
 
229
  (declare (xargs :guard (addr-p addr)))
 
230
  (mod addr *num-page-words*))
 
231
 
 
232
(defthm page-num-type
 
233
    (implies (addr-p addr)
 
234
             (and (integerp (page-num addr))
 
235
                  (<= 0 (page-num addr))))
 
236
  :rule-classes :type-prescription)
 
237
 
 
238
(defthm page-num-bound
 
239
    (implies (addr-p addr)
 
240
             (< (page-num addr) *num-pages*))
 
241
  :hints (("Goal" :in-theory (enable addr-p unsigned-byte-p)))
 
242
  :rule-classes :linear)
 
243
 
 
244
(defthm page-offset-type
 
245
    (implies (addr-p addr)
 
246
             (and (integerp (page-offset addr))
 
247
                  (<= 0 (page-offset addr))))
 
248
  :rule-classes :type-prescription)
 
249
 
 
250
(defthm page-offset-bound
 
251
    (implies (addr-p addr)
 
252
             (< (page-offset addr) *num-page-words*))
 
253
  :rule-classes :linear)
 
254
             
 
255
(in-theory (disable page-num page-offset))
 
256
;;  End of Address Transformer
 
257
 
 
258
 
 
259
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
260
; Definition of Memory Object
 
261
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
262
; Check if page is an array representing a page.
 
263
; Addr does not affect the value, but if the correct page tag is given,
 
264
; execution is faster.
 
265
(defun word-array-p (array)
 
266
  (declare (xargs :guard (alistp array)
 
267
                  :verify-guards nil))
 
268
  (cond ((endp array) t)
 
269
        ((equal (caar array) ':header) (word-array-p (cdr array)))
 
270
        (t (and (word-p (cdar array))
 
271
                (word-array-p (cdr array))))))
 
272
 
 
273
(verify-guards word-array-p
 
274
               :hints (("Goal" :in-theory (enable alistp))))
 
275
 
 
276
(defun page-array-p (tag page-array)
 
277
  (declare (xargs :guard t))
 
278
  (and (array1p tag page-array)
 
279
       (equal (car (dimensions tag page-array)) *num-page-words*)
 
280
       (word-p (default tag page-array))
 
281
       (word-array-p page-array)))
 
282
 
 
283
(defstructure page
 
284
  (tag (:assert (symbolp tag) :rewrite))
 
285
  (mode (:assert (integerp mode) :rewrite))
 
286
  (array (:assert (page-array-p tag array) :rewrite))
 
287
  (:options :guards))
 
288
 
 
289
(defun mem-array-p (array)
 
290
  (declare (xargs :guard (alistp array)
 
291
                  :verify-guards nil))
 
292
  (cond ((endp array) t)
 
293
        ((equal (caar array) ':header) (mem-array-p (cdr array)))
 
294
        (t (and (let ((page (cdar array)))
 
295
                  (if (integerp page)
 
296
                      (or (equal page *no-access*) (equal page *read-only*)
 
297
                          (equal page *read-write*))
 
298
                      (page-p page)))
 
299
                (mem-array-p (cdr array))))))
 
300
 
 
301
(verify-guards mem-array-p :hints (("Goal" :in-theory (enable alistp))))
 
302
 
 
303
(defun mem-p (mem)
 
304
  (declare (xargs :guard t))
 
305
  (and (array1p 'mem mem)
 
306
       (equal (car (dimensions 'mem mem)) *num-pages*)
 
307
       (equal (default 'mem mem) *no-access*)
 
308
       (mem-array-p mem)))
 
309
 
 
310
(in-theory (disable word-array-p page-array-p mem-array-p mem-p))
 
311
 
 
312
(defthm page-p-type
 
313
    (implies (page-p p)
 
314
             (consp p))
 
315
  :hints (("Goal" :in-theory (enable page-p)))
 
316
  :rule-classes :compound-recognizer)
 
317
 
 
318
 
 
319
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
320
;  Definition of Read-mem 
 
321
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
322
(defmacro get-page (n mem)
 
323
  `(aref1 'mem ,mem ,n))
 
324
 
 
325
(defmacro set-page (page n mem)
 
326
  `(aset1 'mem ,mem ,n ,page))
 
327
 
 
328
(defun read-page (offset page)
 
329
  (declare (xargs :guard (and (page-p page)
 
330
                              (integerp offset) (<= 0 offset)
 
331
                              (< offset *num-page-words*))
 
332
                  :verify-guards nil))
 
333
  (aref1 (page-tag page) (page-array page) offset))
 
334
 
 
335
 
 
336
(defun read-mem (addr mem)
 
337
  (declare (xargs :guard (and (addr-p addr) (mem-p mem))
 
338
                  :verify-guards nil))
 
339
  (let ((page (get-page (page-num addr) mem)))
 
340
    (if (integerp page)
 
341
        0
 
342
        (read-page (page-offset addr) page))))
 
343
 
 
344
;(verify-guards get-page
 
345
; :hints (("Goal" :in-theory (enable mem-p))))
 
346
 
 
347
(verify-guards read-page
 
348
  :hints (("Goal" :in-theory (enable page-p page-array-p))))
 
349
 
 
350
(encapsulate nil
 
351
(local 
 
352
 (defthm page-p-assoc-mem-array
 
353
     (implies (and (mem-array-p mem)
 
354
                   (integerp pn)
 
355
                   (assoc pn mem)
 
356
                   (not (integerp (cdr (assoc pn mem)))))
 
357
              (page-p (cdr (assoc pn mem))))
 
358
   :hints (("Goal" :in-theory (enable assoc mem-array-p)))))
 
359
 
 
360
(local 
 
361
 (defthm integerp-default-in-mem-array
 
362
     (implies (mem-p mem)
 
363
              (integerp (default 'mem mem)))
 
364
   :hints (("Goal" :in-theory (enable mem-p)))))
 
365
 
 
366
(defthm page-p-get-page
 
367
    (implies (and (mem-p mem)
 
368
                  (integerp pn)
 
369
                  (not (integerp (get-page pn mem))))
 
370
             (page-p (get-page pn mem)))
 
371
  :hints (("Goal" :in-theory (enable aref1 mem-p))))
 
372
)
 
373
 
 
374
(local   
 
375
 (defthm word-p-assoc-word-array
 
376
     (implies (and (word-array-p wa)
 
377
                   (integerp pn)
 
378
                   (assoc pn wa))
 
379
              (word-p (cdr (assoc pn wa))))
 
380
   :hints (("Goal" :in-theory (enable word-array-p assoc)))))
 
381
 
 
382
(encapsulate nil
 
383
(defthm word-p-read-page
 
384
    (implies (and (page-p page)
 
385
                  (integerp offset))
 
386
             (word-p (read-page offset page)))
 
387
  :hints (("Goal" :in-theory (enable page-p aref1 page-array-p))))
 
388
)
 
389
 
 
390
(in-theory (disable read-page read-mem))
 
391
(verify-guards read-mem
 
392
               :hints (("goal" :in-theory (enable mem-p))))
 
393
 
 
394
(defthm word-p-read-mem
 
395
    (implies (and (mem-p mem)
 
396
                  (addr-p addr))
 
397
             (word-p (read-mem addr mem)))
 
398
  :hints (("Goal" :in-theory (enable read-mem)))
 
399
  :rule-classes
 
400
  ((:rewrite)
 
401
   (:type-prescription :corollary
 
402
                       (implies (and (mem-p mem) (addr-p addr))
 
403
                                (and (integerp (read-mem addr mem))
 
404
                                     (>= (read-mem addr mem) 0))))
 
405
   (:rewrite :corollary
 
406
             (implies (and (mem-p mem) (addr-p addr))
 
407
                      (acl2-numberp (read-mem addr mem))))))
 
408
 
 
409
   
 
410
 
 
411
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
412
; Definition of Write-Mem
 
413
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
414
; Page tag is calculated for fast array access. 
 
415
; The tag for the <n>'th page is given by page<n>.
 
416
(defun gen-page-tag (page-num)
 
417
  (declare (xargs :guard (and (integerp page-num)
 
418
                              (>= page-num 0))
 
419
                  :verify-guards nil))
 
420
  (pack-intern 'mem
 
421
       (coerce (append (coerce (symbol-name 'page) 'list)
 
422
                       (explode-nonnegative-integer page-num 10 nil))
 
423
               'string)))
 
424
 
 
425
(encapsulate nil
 
426
(local
 
427
 (defthm character-listp-explode-nonnegative-integer-help
 
428
     (implies (and (integerp n) (>= n 0)
 
429
                   (character-listp x))
 
430
              (character-listp (explode-nonnegative-integer n print-base x)))
 
431
   :hints (("goal" :in-theory (enable explode-nonnegative-integer
 
432
                                      character-listp)))))
 
433
 
 
434
(local
 
435
 (defthm character-listp-explode-nonnegative-integer
 
436
     (implies (and (integerp n) (>= n 0))
 
437
              (character-listp (explode-nonnegative-integer n print-base nil)))))
 
438
 
 
439
; Renamed by Matt K. after Version 4.3, since a similar :type-prescription
 
440
; lemma is now provided by the ACL2 system.  Perhaps it could be deleted now.
 
441
(local
 
442
 (defthm true-listp-explode-nonnegative-integer-rewrite
 
443
     (implies (true-listp x)
 
444
              (true-listp (explode-nonnegative-integer n print-base x)))))
 
445
       
 
446
(verify-guards gen-page-tag
 
447
     :hints (("goal" :in-theory (enable U::coerce-string-designator-list
 
448
                                        U::STRING-DESIGNATOR-LISTP
 
449
                                        character-listp
 
450
                                        binary-append))))
 
451
)
 
452
 
 
453
(defun init-page (page-num mode)
 
454
  (declare (xargs :guard (and (integerp page-num) (<= 0 page-num)
 
455
                              (integerp mode))
 
456
                  :verify-guards nil))
 
457
  (let ((name (gen-page-tag page-num)))
 
458
    (page name
 
459
          mode
 
460
          (compress1 name `((:header :name ,name
 
461
                             :dimensions (,*num-page-words*)
 
462
                             :default 0
 
463
                             :maximum-length 4096))))))
 
464
 
 
465
(verify-guards init-page
 
466
 :hints (("Goal" :in-theory (enable array1p alistp
 
467
                                    keyword-value-listp
 
468
                                    assoc-eq
 
469
                                    assoc-keyword
 
470
                                    bounded-integer-alistp))))
 
471
 
 
472
(defun write-page (val offset page)
 
473
  (declare (xargs :guard (and (word-p val)
 
474
                              (integerp offset) (<= 0 offset)
 
475
                              (< offset *num-page-words*)
 
476
                              (page-p page))
 
477
                  :verify-guards nil))
 
478
  (update-page page
 
479
               :array (aset1 (page-tag page) (page-array page) offset val)))
 
480
 
 
481
(defun write-mem (val addr mem)
 
482
  (declare (xargs :guard (and (word-p val) (addr-p addr) (mem-p mem))
 
483
                  :verify-guards nil))
 
484
  (let ((page (get-page (page-num addr) mem)))
 
485
    (if (integerp page)
 
486
        (let ((p (init-page (page-num addr) page)))
 
487
          (set-page (write-page val (page-offset addr) p)
 
488
                    (page-num addr)
 
489
                    mem))
 
490
        (set-page (write-page val (page-offset addr) page)
 
491
                  (page-num addr)
 
492
                  mem))))
 
493
 
 
494
(verify-guards write-page
 
495
  :hints (("Goal" :in-theory (enable page-p page-array-p)))) 
 
496
 
 
497
(in-theory (disable  write-mem init-page gen-page-tag write-page))
 
498
 
 
499
 
 
500
(defthm page-p-init-page
 
501
    (implies (integerp mode)
 
502
             (page-p (init-page pn mode)))
 
503
  :hints (("goal" :in-theory (enable page-p init-page page-array-p
 
504
                                     default dimensions
 
505
                                     header array1p word-array-p))))
 
506
 
 
507
(verify-guards write-mem
 
508
  :hints (("Goal" :in-theory (enable mem-p ))))
 
509
 
 
510
(local
 
511
(defthm word-array-p-compress11
 
512
    (implies (and (array1p tag array)
 
513
                  (word-array-p array)
 
514
                  (integerp i))
 
515
             (word-array-p (compress11 tag array i dim default)))
 
516
  :hints (("Goal" :in-theory (enable word-array-p)))))
 
517
 
 
518
 
 
519
; Added by Matt K. for Version 3.1, 7/1/06, to support proof of
 
520
; compress1-assoc-property-0 in light of addition of reverse-sorted and
 
521
; unsorted ACL2 arrays:
 
522
(local
 
523
 (defthm word-array-p-revappend
 
524
   (equal (word-array-p (revappend x y))
 
525
          (and (word-array-p x)
 
526
               (word-array-p y)))
 
527
   :hints (("Goal" :in-theory (enable word-array-p)
 
528
            :induct (revappend x y)))))
 
529
 
 
530
(defthm word-array-p-compress1
 
531
    (implies (and (array1p tag array)
 
532
                  (word-array-p array))
 
533
             (word-array-p (compress1 tag array)))
 
534
  :hints (("Goal" :in-theory (enable compress1 word-array-p))))
 
535
 
 
536
(defthm word-array-p-aset1
 
537
    (implies (and (array1p tag page-array)
 
538
                  (word-array-p page-array)
 
539
                  (integerp index)
 
540
                  (>= index 0)
 
541
                  (> (car (dimensions tag page-array)) index)
 
542
                  (word-p val))
 
543
             (word-array-p (aset1 tag page-array index val)))
 
544
  :hints (("goal" :in-theory (enable aset1 word-array-p ARRAY1P-CONS))))
 
545
 
 
546
(defthm page-array-p-aref1
 
547
    (implies (and (page-array-p tag page-array)
 
548
                  (word-p val)
 
549
                  (integerp offset)
 
550
                  (>= offset 0)
 
551
                  (> *num-page-words* offset))
 
552
             (page-array-p tag (aset1 tag page-array offset val)))
 
553
  :hints (("Goal" :in-theory (enable page-array-p))))
 
554
 
 
555
 
 
556
(defthm page-p-write-page
 
557
    (implies (and (word-p val)
 
558
                  (integerp offset)
 
559
                  (>= offset 0)
 
560
                  (> *num-page-words* offset)
 
561
                  (page-p page))
 
562
             (page-p (write-page val offset page)))
 
563
  :hints (("Goal" :in-theory (enable write-page))))
 
564
 
 
565
(local   
 
566
 (defthm valid-integer-assoc-mem-array
 
567
     (implies (and (mem-array-p ma) 
 
568
                   (integerp pn)
 
569
                   (assoc pn ma)
 
570
                   (integerp (cdr (assoc pn ma)))
 
571
                   (not (equal (cdr (assoc pn ma)) 0))
 
572
                   (not (equal (cdr (assoc pn ma)) 1)))
 
573
              (equal (cdr (assoc pn ma)) 2))
 
574
   :hints (("Goal" :in-theory (enable mem-array-p assoc)))))
 
575
 
 
576
(local   
 
577
 (defthm page-p-assoc-mem-array
 
578
     (implies (and (mem-array-p ma) 
 
579
                   (integerp pn)
 
580
                   (assoc pn ma)
 
581
                   (not (integerp (cdr (assoc pn ma)))))
 
582
              (page-p (cdr (assoc pn ma))))
 
583
   :hints (("Goal" :in-theory (enable mem-array-p assoc)))))
 
584
 
 
585
 
 
586
(local
 
587
(defthm mem-array-p-compress11
 
588
    (implies (and (array1p tag array)
 
589
                  (mem-array-p array)
 
590
                  (integerp i))
 
591
             (mem-array-p (compress11 tag array i dim default)))
 
592
  :hints (("Goal" :in-theory (enable mem-array-p compress1)))))
 
593
 
 
594
; Added by Matt K. for Version 3.1, 7/1/06, to support proof of
 
595
; compress1-assoc-property-0 in light of addition of reverse-sorted and
 
596
; unsorted ACL2 arrays:
 
597
(local
 
598
 (defthm mem-array-p-revappend
 
599
   (equal (mem-array-p (revappend x y))
 
600
          (and (mem-array-p x)
 
601
               (mem-array-p y)))
 
602
   :hints (("Goal" :in-theory (enable mem-array-p)
 
603
            :induct (revappend x y)))))
 
604
 
 
605
(defthm mem-array-p-compress1
 
606
    (implies (and (array1p tag array)
 
607
                  (mem-array-p array))
 
608
             (mem-array-p (compress1 tag array)))
 
609
  :hints (("Goal" :in-theory (enable mem-array-p compress1))))
 
610
 
 
611
 
 
612
 
 
613
(defthm mem-array-p-aset1
 
614
    (implies (and (array1p tag mem-array)
 
615
                  (mem-array-p mem-array)
 
616
                  (or (page-p page)
 
617
                      (equal page *no-access*)
 
618
                      (equal page *read-only*)
 
619
                      (equal page *read-write*))
 
620
                  (integerp pn)
 
621
                  (>= pn 0)
 
622
                  (> (car (dimensions tag mem-array)) pn))
 
623
             (mem-array-p (aset1 tag mem-array pn page)))
 
624
  :hints (("Goal" :in-theory (enable mem-array-p aset1))))
 
625
 
 
626
 
 
627
(defthm mem-p-write-mem
 
628
    (implies (and (word-p val)
 
629
                  (addr-p addr)
 
630
                  (mem-p mem))
 
631
             (mem-p (write-mem val addr mem)))
 
632
  :hints (("goal" :in-theory (enable mem-p write-mem))))
 
633
 
 
634
(defthm page-num-offset-extionsionality
 
635
     (implies (and (addr-p addr1)
 
636
                   (addr-p addr2)
 
637
                   (equal (page-num addr1) (page-num addr2))
 
638
                   (equal (page-offset addr1) (page-offset addr2)))
 
639
              (equal addr1 addr2))
 
640
  :hints (("Goal" :in-theory (enable addr-p page-num page-offset)))
 
641
   :rule-classes
 
642
   ((:rewrite :corollary
 
643
              (implies (and (addr-p addr1)
 
644
                            (addr-p addr2)
 
645
                            (equal (page-num addr1) (page-num addr2))
 
646
                            (not (equal addr1 addr2)))
 
647
                       (equal (equal (page-offset addr1) (page-offset addr2))
 
648
                              nil)))))
 
649
 
 
650
(defthm read-page-init-page
 
651
    (implies (integerp offset)
 
652
             (equal (read-page offset (init-page pn mode)) 0))
 
653
  :hints (("Goal" :in-theory (enable init-page read-page aref1
 
654
                                     default header))))
 
655
 
 
656
 
 
657
(defthm read-page-write-page
 
658
    (implies (and (page-p page)
 
659
                  (integerp offset1)
 
660
                  (>= offset1 0)
 
661
                  (> *num-page-words* offset1)
 
662
                  (integerp offset2)
 
663
                  (>= offset2 0)
 
664
                  (> *num-page-words* offset2))
 
665
             (equal (read-page offset1 (write-page val offset2 page))
 
666
                    (if (equal offset1 offset2)
 
667
                        val
 
668
                        (read-page offset1 page))))
 
669
  :hints (("Goal" :in-theory (enable page-p read-page write-page
 
670
                                     page-array-p))))
 
671
 
 
672
 
 
673
(defthm read-mem-write-mem
 
674
    (implies (and (addr-p ad1)
 
675
                  (addr-p ad2)
 
676
                  (mem-p mem))
 
677
             (equal (read-mem ad1 (write-mem val ad2 mem))
 
678
                    (if (equal ad1 ad2) val (read-mem ad1 mem))))
 
679
  :hints (("Goal" :in-theory (enable read-mem write-mem
 
680
                                     mem-p))))
 
681
 
 
682
 
 
683
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
684
; Definition of Protection Check.
 
685
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
686
(defun readable-addr-p (ad mem)
 
687
  (declare (xargs :guard (and (addr-p ad) (mem-p mem))
 
688
                  :verify-guards nil))
 
689
  (let ((page (get-page (page-num ad) mem)))
 
690
    (if (integerp page)
 
691
        (or (equal page *read-only*)
 
692
            (equal page *read-write*))
 
693
        (or (equal (page-mode page) *read-only*)
 
694
            (equal (page-mode page) *read-write*)))))
 
695
 
 
696
(verify-guards  readable-addr-p
 
697
 :hints (("Goal" :in-theory (enable mem-p))))
 
698
 
 
699
(defun readable-addr? (ad mem)
 
700
  (declare (xargs :guard (and (addr-p ad) (mem-p mem))))
 
701
  (if (readable-addr-p ad mem) 1 0))
 
702
 
 
703
(defthm bitp-readable-addr (bitp (readable-addr? ad mem)))
 
704
 
 
705
(defun writable-addr-p (ad mem)
 
706
  (declare (xargs :guard (and (addr-p ad) (mem-p mem))
 
707
                  :verify-guards nil))
 
708
  (let ((page (get-page (page-num ad) mem)))
 
709
    (if (integerp page)
 
710
        (equal page *read-write*)
 
711
        (equal (page-mode page) *read-write*))))
 
712
 
 
713
(verify-guards  writable-addr-p
 
714
 :hints (("Goal" :in-theory (enable mem-p))))
 
715
 
 
716
(defun writable-addr? (ad mem)
 
717
  (declare (xargs :guard (and (addr-p ad) (mem-p mem))))
 
718
  (if (writable-addr-p ad mem) 1 0))
 
719
 
 
720
(defthm bitp-writable-addr (bitp (writable-addr? ad mem)))
 
721
 
 
722
(defun set-page-mode (mode pn mem)
 
723
  (declare (xargs :guard (and (integerp mode)
 
724
                              (integerp pn) (<= 0 pn) (< pn *num-pages*)
 
725
                              (mem-p mem))
 
726
                  :verify-guards nil))
 
727
  (let ((page (get-page pn mem)))
 
728
    (if (integerp page)
 
729
        (set-page mode pn mem)
 
730
        (set-page (update-page page :mode mode) pn mem))))
 
731
 
 
732
(verify-guards set-page-mode
 
733
        :hints (("Goal" :in-theory (enable mem-p))))      
 
734
 
 
735
(defthm mem-p-set-page-mode
 
736
    (implies (and (mem-p mem)
 
737
                  (integerp mode)
 
738
                  (or (equal mode *no-access*)
 
739
                      (equal mode *read-only*)
 
740
                      (equal mode *read-write*))
 
741
                  (integerp pn) (<= 0 pn) (< pn *num-pages*))
 
742
             (mem-p (set-page-mode mode pn mem)))
 
743
  :hints (("Goal" :in-theory (enable mem-p))))
 
744
 
 
745
(defthm page-mode-init-page
 
746
    (equal (page-mode (init-page page-num mode)) mode)
 
747
  :hints (("Goal" :in-theory (enable init-page))))
 
748
 
 
749
(defthm page-mode-write-page
 
750
    (equal (page-mode (write-page val offset page))
 
751
           (page-mode page))
 
752
  :hints (("Goal" :in-theory (enable write-page))))
 
753
 
 
754
(defthm readable-addr-p-set-page-mode
 
755
    (implies (and (integerp mode)
 
756
                  (addr-p addr)
 
757
                  (integerp pn1) (<= 0 pn1) (< pn1 *num-pages*)
 
758
                  (mem-p mem))
 
759
             (equal (readable-addr-p addr (set-page-mode mode pn1 mem))
 
760
                    (if (equal (page-num addr) pn1)
 
761
                        (or (equal mode *read-only*) (equal mode *read-write*))
 
762
                        (readable-addr-p addr mem))))
 
763
  :hints (("Goal" :in-theory (enable set-page-mode mem-p
 
764
                                     readable-addr-p))))
 
765
 
 
766
 
 
767
(defthm readable-addr-set-page-mode
 
768
    (implies (and (integerp mode)
 
769
                  (addr-p addr)
 
770
                  (integerp pn1) (<= 0 pn1) (< pn1 *num-pages*)
 
771
                  (mem-p mem))
 
772
             (equal (readable-addr? addr (set-page-mode mode pn1 mem))
 
773
                    (if (equal (page-num addr) pn1)
 
774
                        (if (or (equal mode *read-only*)
 
775
                                (equal mode *read-write*))
 
776
                            1 0)
 
777
                        (readable-addr? addr mem))))
 
778
  :hints (("Goal" :in-theory (e/d (readable-addr?) (readable-addr-p
 
779
                                                    SET-PAGE-MODE)))))
 
780
 
 
781
(defthm writable-addr-p-set-page-mode
 
782
    (implies (and (integerp mode)
 
783
                  (addr-p addr)
 
784
                  (integerp pn1) (<= 0 pn1) (< pn1 *num-pages*)
 
785
                  (mem-p mem))
 
786
             (equal (writable-addr-p addr (set-page-mode mode pn1 mem))
 
787
                    (if (equal (page-num addr) pn1)
 
788
                        (equal mode *read-write*)
 
789
                        (writable-addr-p addr mem))))
 
790
  :hints (("Goal" :in-theory (enable set-page-mode mem-p
 
791
                                     writable-addr-p))))
 
792
 
 
793
(defthm writable-addr-set-page-mode
 
794
    (implies (and (integerp mode)
 
795
                  (addr-p addr)
 
796
                  (integerp pn1) (<= 0 pn1) (< pn1 *num-pages*)
 
797
                  (mem-p mem))
 
798
             (equal (writable-addr? addr (set-page-mode mode pn1 mem))
 
799
                    (if (equal (page-num addr) pn1)
 
800
                        (if (equal mode *read-write*) 1 0)
 
801
                        (writable-addr? addr mem))))
 
802
  :hints (("Goal" :in-theory (e/d (writable-addr?)
 
803
                                  (writable-addr-p SET-PAGE-MODE)))))
 
804
 
 
805
(defthm readable-addr-p-write-mem
 
806
    (implies (and (addr-p addr) (addr-p addr2) (word-p val) (mem-p mem))
 
807
             (equal (readable-addr-p addr (write-mem val addr2 mem))
 
808
                    (readable-addr-p addr mem)))
 
809
  :hints (("Goal" :in-theory (enable readable-addr-p write-mem mem-p))))
 
810
 
 
811
(defthm readable-addr-write-mem
 
812
    (implies (and (addr-p addr) (addr-p addr2) (word-p val) (mem-p mem))
 
813
             (equal (readable-addr? addr (write-mem val addr2 mem))
 
814
                    (readable-addr? addr mem)))
 
815
  :hints (("Goal" :in-theory (enable readable-addr?))))
 
816
 
 
817
(defthm writable-addr-p-write-mem
 
818
    (implies (and (addr-p addr) (addr-p addr2) (word-p val) (mem-p mem))
 
819
             (equal (writable-addr-p addr (write-mem val addr2 mem))
 
820
                    (writable-addr-p addr mem)))
 
821
  :hints (("Goal" :in-theory (enable writable-addr-p write-mem mem-p))))
 
822
 
 
823
(defthm writable-addr-write-mem
 
824
    (implies (and (addr-p addr) (addr-p addr2) (word-p val) (mem-p mem))
 
825
             (equal (writable-addr? addr (write-mem val addr2 mem))
 
826
                    (writable-addr? addr mem)))
 
827
  :hints (("Goal" :in-theory (enable writable-addr?))))
 
828
 
 
829
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
830
; Initialize Memory
 
831
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
832
(defconst *init-mem*
 
833
    (compress1 'mem (list `(:header :name mem
 
834
                            :dimensions (,*num-pages*)
 
835
                            :default ,*no-access*
 
836
                            :maximum-length 2048))))
 
837
 
 
838
(defthm mem-p-init-mem
 
839
    (mem-p *init-mem*))
 
840
 
 
841
(deflist mem-alist-p (l)
 
842
  (declare (xargs :guard t))
 
843
  (lambda (l) (and (consp l) (addr-p (car l)) (word-p (cdr l)))))
 
844
 
 
845
(defun load-mem-alist (alist mem)
 
846
  (declare (xargs :guard (and (mem-alist-p alist) (mem-p mem))))
 
847
  (if (endp alist)
 
848
      mem
 
849
      (load-mem-alist (cdr alist) (write-mem (cdar alist) (caar alist) mem))))
 
850
 
 
851
(defthm mem-p-load-mem-alist
 
852
    (implies (and (mem-alist-p alist)
 
853
                  (mem-p mem))
 
854
             (mem-p (load-mem-alist alist mem))))
 
855
    
 
856
(in-theory (disable page-p page-array-p word-array-p mem-p))
 
857
(in-theory (disable read-reg))
 
858
(in-theory (disable write-reg))
 
859
(in-theory (disable read-mem))
 
860
(in-theory (disable write-mem))
 
861
(in-theory (disable writable-addr-p readable-addr-p
 
862
                    writable-addr? readable-addr? set-page-mode))
 
863
 
 
864
(defword* word-layout ((op-field 4 12)
 
865
                      (rc-field *rname-size* 8)
 
866
                      (ra-field *rname-size* 4)
 
867
                      (rb-field *rname-size* 0)
 
868
                      (im-field *immediate-size* 0))
 
869
  :conc-name ||)
 
870
 
 
871
 
 
872
(defthm opcd-p-opcode
 
873
    (opcd-p (op-field inst))
 
874
  :hints (("Goal" :in-theory (enable opcd-p))))
 
875
 
 
876
(defthm rname-p-rc-field
 
877
    (rname-p (rc-field inst))
 
878
  :hints (("Goal" :in-theory (enable rname-p))))
 
879
 
 
880
(defthm rname-p-ra-field
 
881
    (rname-p (ra-field inst))
 
882
  :hints (("Goal" :in-theory (enable rname-p))))
 
883
 
 
884
(defthm rname-p-rb-field
 
885
    (rname-p (rb-field inst))
 
886
  :hints (("Goal" :in-theory (enable rname-p))))
 
887
 
 
888
 
 
889
(defthm immediate-p-immediate-field
 
890
    (immediate-p (im-field inst))
 
891
  :hints (("Goal" :in-theory (enable immediate-p))))
 
892
 
 
893
 
 
894
(defthm word-p-immediate-field
 
895
    (word-p (im-field inst))
 
896
  :hints (("Goal" :in-theory (enable word-p))))
 
897
 
 
898
(defthm word-IM-field
 
899
    (equal (word (IM-field i)) (IM-field i))
 
900
  :hints (("goal" :in-theory (enable word))))
 
901
 
 
902
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
903
;  Definition of Special registers
 
904
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
905
(defconst *num-sregs* 2)
 
906
 
 
907
(defstructure sregs
 
908
  (su (:assert (bitp su) :rewrite ))
 
909
  (sr0 (:assert (word-p sr0) :rewrite))
 
910
  (sr1 (:assert (word-p sr1) :rewrite))
 
911
  (:options :guards))
 
912
 
 
913
(defun srname-p (rname)
 
914
  (declare (xargs :guard t))
 
915
  (and (rname-p rname) (< rname *num-sregs*)))
 
916
 
 
917
(defthm srname-p-type
 
918
    (implies (srname-p rname)
 
919
             (and (integerp rname)
 
920
                  (>= rname 0)
 
921
                  (< rname *num-sregs*)))
 
922
  :hints (("Goal" :in-theory (enable rname-p srname-p)))
 
923
  :rule-classes :forward-chaining)
 
924
 
 
925
(defun read-sreg (id sregs)
 
926
  (declare (xargs :guard (and (rname-p id) (sregs-p sregs))))
 
927
  (if (equal id 0) (sregs-sr0 sregs)
 
928
      (if (equal id 1) (sregs-sr1 sregs)
 
929
          0)))
 
930
 
 
931
(defun write-sreg (val id sregs)
 
932
  (declare (xargs :guard (and (word-p val) (rname-p id) (sregs-p sregs))))
 
933
  (if (equal id 0) (sregs (sregs-su sregs) val (sregs-sr1 sregs))
 
934
      (if (equal id 1) (sregs (sregs-su sregs) (sregs-sr0 sregs) val)
 
935
          sregs)))
 
936
 
 
937
(defthm word-p-read-sreg
 
938
    (implies (and (rname-p id) (sregs-p sregs))
 
939
             (word-p (read-sreg id sregs))))
 
940
 
 
941
(defthm numberp-read-sreg
 
942
    (implies (and (sregs-p sregs)
 
943
                  (rname-p rname))
 
944
             (and (integerp (read-sreg rname sregs))
 
945
                  (acl2-numberp (read-sreg rname sregs))))
 
946
  :hints (("Goal" :in-theory (enable rname-p sregs-p fixlen-word-listp)))
 
947
  :rule-classes
 
948
  ((:type-prescription) (:rewrite)))
 
949
 
 
950
(defthm sregs-p-write-sreg
 
951
    (implies (and (word-p val) (rname-p id) (sregs-p sregs))
 
952
             (sregs-p (write-sreg val id sregs))))
 
953
 
 
954
(defthm read-sreg-write-sreg
 
955
    (implies (and (srname-p rn1)
 
956
                  (srname-p rn2)
 
957
                  (sregs-p sregs))
 
958
             (equal (read-sreg rn1 (write-sreg val rn2 sregs))
 
959
                    (if (equal rn1 rn2) val (read-sreg rn1 sregs))))
 
960
  :hints (("Goal" :in-theory (enable read-sreg write-sreg sregs-p
 
961
                                     srname-p))))
 
962
 
 
963
(in-theory (disable read-sreg write-sreg srname-p))