← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/support/setbits-proofs.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/support/support/setbits-proofs.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(defun natp (x)
 
4
  (declare (xargs :guard t))
 
5
  (and (integerp x)
 
6
       (<= 0 x)))
 
7
 
 
8
(defund bvecp (x k)
 
9
  (declare (xargs :guard (integerp k)))
 
10
  (and (integerp x)
 
11
       (<= 0 x)
 
12
       (< x (expt 2 k))))
 
13
 
 
14
(include-book "cat-def")
 
15
(local (include-book "../../arithmetic/top"))
 
16
(local (include-book "bits"))
 
17
(local (include-book "bitn"))
 
18
(local (include-book "bvecp"))
 
19
(local (include-book "cat"))
 
20
 
 
21
(defund bitn (x n)
 
22
  (declare (xargs :guard (and (natp x)
 
23
                              (natp n))
 
24
                  :verify-guards nil))
 
25
  (mbe :logic (bits x n n)
 
26
       :exec  (if (evenp (ash x (- n))) 0 1)))
 
27
 
 
28
#|
 
29
 
 
30
Currently we expect to leave setbits enabled so that it rewrites to cat, but there are some lemmas below which
 
31
might be useful if we choose to keep setbits disabled...
 
32
 
 
33
is this comment still valid? :
 
34
;it may happen that setbitn is called with an index which is a signal rather than a constant.
 
35
;in that case, we probably don't want it to expand to setbits. 
 
36
;thus, we always expect the indices in setbits calls to be constants
 
37
 
 
38
 
 
39
;Set bits I down to J of the W-bit value X to Y.
 
40
 
 
41
(setbits x w i j y) is only well-defined when the following predicate is true:
 
42
 
 
43
(and (natp w)
 
44
     (bvecp x w)
 
45
     (integerp i)
 
46
     (integerp j)
 
47
     (<= 0 j)
 
48
     (<= j i)
 
49
     (< i w)
 
50
     (bvecp y (+ 1 i (- j))))
 
51
 
 
52
|#
 
53
 
 
54
#| old:
 
55
(defund setbits (x w i j y)
 
56
  (declare (xargs :guard (and (rationalp x) (rationalp y)
 
57
                              (acl2-numberp i) (acl2-numberp j) (acl2-numberp w))))
 
58
  (if (not (natp w))
 
59
      0
 
60
    (cat (bits x (1- w) (+ 1 i))
 
61
         (+ -1 w (- i))
 
62
         (cat (bits y (+ i (- j)) 0)
 
63
              (+ 1 i (- j))
 
64
              (bits x (1- j) 0)
 
65
              j)
 
66
         (+ 1 i))))
 
67
|#
 
68
 
 
69
;Note: when j is 0, there is not lower part of x, but we have cat-with-n-0 to handle this case. 
 
70
(defund setbits (x w i j y)
 
71
  (declare (xargs :guard (and (natp x)
 
72
                              (natp y)
 
73
                              (integerp i)
 
74
                              (integerp j)
 
75
                              (<= 0 j)
 
76
                              (<= j i)
 
77
                              (integerp w)
 
78
                              (< i w))
 
79
                  :verify-guards nil))
 
80
  (mbe :logic (cat (bits x (1- w) (1+ i))
 
81
                   (+ -1 w (- i))
 
82
                   (cat (bits y (+ i (- j)) 0)
 
83
                        (+ 1 i (- j))
 
84
                        (bits x (1- j) 0)
 
85
                        j)
 
86
                   (1+ i))
 
87
       :exec  (cond ((int= j 0)
 
88
                     (cond ((int= (1+ i) w)
 
89
                            (bits y (+ i (- j)) 0))
 
90
                           (t
 
91
                            (cat (bits x (1- w) (1+ i))
 
92
                                 (+ -1 w (- i))
 
93
                                 (bits y (+ i (- j)) 0)
 
94
                                 (1+ i)))))
 
95
                    ((int= (1+ i) w)
 
96
                     (cat (bits y (+ i (- j)) 0)
 
97
                          (+ 1 i (- j))
 
98
                          (bits x (1- j) 0)
 
99
                          j))
 
100
                    (t
 
101
                     (cat (bits x (1- w) (1+ i))
 
102
                          (+ -1 w (- i))
 
103
                          (cat (bits y (+ i (- j)) 0)
 
104
                               (+ 1 i (- j))
 
105
                               (bits x (1- j) 0)
 
106
                               j)
 
107
                          (1+ i))))))
 
108
 
 
109
 
 
110
 
 
111
#| old defn
 
112
(defun setbits (x i j y)
 
113
  (ocat (ocat (ash x (- (1+ i)))
 
114
            y
 
115
            (1+ (- i j)))
 
116
       (bits x (1- j) 0)
 
117
       j))
 
118
|#
 
119
 
 
120
(defthm setbits-nonnegative-integer-type
 
121
  (and (integerp (setbits x w i j y))
 
122
       (<= 0 (setbits x w i j y)))
 
123
  :hints (("Goal" :in-theory (enable setbits)))
 
124
  :rule-classes (:type-prescription)
 
125
  )
 
126
 
 
127
;this rule is no better than setbits-nonnegative-integer-type and might be worse:
 
128
(in-theory (disable (:type-prescription setbits)))
 
129
 
 
130
(defthm setbits-natp
 
131
  (natp (setbits x w i j y)))
 
132
 
 
133
;BOZO r-c?
 
134
(defthm setbits-upper-bound
 
135
  (< (setbits x w i j y) (expt 2 w))
 
136
  :hints (("Goal" :in-theory (enable setbits cat-upper-bound))))
 
137
 
 
138
(defthm setbits-bvecp-simple
 
139
  (bvecp (setbits x w i j y) w)
 
140
  :hints (("goal" :in-theory (enable bvecp))))
 
141
 
 
142
(defthm setbits-bvecp
 
143
  (implies (and (<= w k)
 
144
                (case-split (integerp k))
 
145
                )
 
146
           (bvecp (setbits x w i j y) k))
 
147
  :hints (("goal" :use setbits-bvecp-simple
 
148
           :in-theory (disable setbits-bvecp-simple))))
 
149
 
 
150
(defthm setbits-does-nothing
 
151
  (implies (and (case-split (< i w))
 
152
                (case-split (<= j i))
 
153
                (case-split (integerp i))
 
154
                (case-split (integerp j))
 
155
                (case-split (<= 0 j))
 
156
                )
 
157
           (equal (setbits x w i j (bits x i j))
 
158
                  (bits x (1- w) 0)))
 
159
  :hints (("Goal" :in-theory (enable setbits))))
 
160
 
 
161
 
 
162
#| old, prove the two match for bvecps
 
163
(defun oldsetbits (x i j y)
 
164
  (ocat (ocat (ash x (- (1+ i)))
 
165
            y
 
166
            (1+ (- i j)))
 
167
       (bits x (1- j) 0)
 
168
       j))
 
169
 
 
170
;we had this before
 
171
(defthm oldsetbits-rewrite-1
 
172
    (implies (and (bvecp x n)
 
173
                  (natp n)
 
174
                  (> n 0)
 
175
                  (natp i)
 
176
                  (natp j)
 
177
                  (<= j i)
 
178
                  (bvecp y (1+ (- i j))))
 
179
             (equal (oldsetbits x i j y)
 
180
                    (ocat (ocat (bits x (1- n) (1+ i))
 
181
                              y
 
182
                              (1+ (- i j)))
 
183
                         (bits x (1- j) 0)
 
184
                         j))))
 
185
 
 
186
(defthm setbits-match
 
187
  (implies (and (bvecp x n)
 
188
                (natp n)
 
189
                (> n 0)
 
190
                (natp w)
 
191
                (<= n w)
 
192
                (bvecp y (1+ (- i j)))
 
193
                (natp i)
 
194
                (natp j)
 
195
                (<= j i))
 
196
           (equal (oldsetbits x i j y)
 
197
                  (setbits x w i j y)))
 
198
  :otf-flg t
 
199
  :hints (("Goal" :in-theory (enable setbits oldsetbits bits-does-nothing
 
200
                                     natp))))
 
201
 
 
202
|#
 
203
 
 
204
;taking bits from the lower third
 
205
;slow proof with may cases!
 
206
(defthm bits-setbits-1
 
207
  (implies (and (< k j)
 
208
                (case-split (<= 0 w))
 
209
                (case-split (< i w))
 
210
                (case-split (<= 0 l))
 
211
                (case-split (<= j i)) ;drop?
 
212
                (case-split (integerp w))
 
213
                (case-split (integerp i))
 
214
                (case-split (integerp j))
 
215
                )
 
216
           (equal (bits (setbits x w i j y) k l)
 
217
                  (bits x k l)))
 
218
  :hints (("Goal" :in-theory (enable setbits))))
 
219
 
 
220
;taking bits from the middle third
 
221
;slow proof with may cases!
 
222
(defthm bits-setbits-2
 
223
  (implies (and (<= k i)
 
224
                (<= j l)
 
225
                (case-split (integerp i))
 
226
                (case-split (<= 0 j))
 
227
                (case-split (integerp j))
 
228
                (case-split (acl2-numberp k));            (case-split (integerp k))
 
229
                (case-split (acl2-numberp l)) ;   (case-split (integerp l))
 
230
                (case-split (integerp w))
 
231
                (case-split (<= 0 w))
 
232
                (case-split (< i w))
 
233
                )
 
234
           (equal (bits (setbits x w i j y) k l)
 
235
                  (bits y (- k j) (- l j))))
 
236
  :hints (("Goal" :in-theory (enable setbits natp))))
 
237
 
 
238
;taking bits from the upper third
 
239
(defthm bits-setbits-3
 
240
  (implies (and (< i l)
 
241
                (case-split (< i w))
 
242
                (case-split (< k w)) ;handle this?
 
243
                (case-split (<= j i))
 
244
                (case-split (<= 0 l))
 
245
                (case-split (<= 0 j))
 
246
                (case-split (<= 0 w))
 
247
                (case-split (integerp l))
 
248
                (case-split (integerp w))
 
249
                (case-split (integerp i))
 
250
                (case-split (integerp j))
 
251
                (case-split (integerp k))
 
252
                )
 
253
           (equal (bits (setbits x w i j y) k l)
 
254
                  (bits x k l)))
 
255
  :hints (("Goal" :in-theory (enable setbits natp))))
 
256
 
 
257
 
 
258
(defthm setbits-with-0-width
 
259
  (equal (setbits x 0 i j y)
 
260
         0)
 
261
  :hints (("Goal" :cases ((integerp j))
 
262
           :in-theory (enable setbits))))
 
263
 
 
264
;add case-splits?
 
265
;why can't i prove this from bits-setbits?
 
266
(defthm bitn-setbits-1
 
267
  (implies (and (< k j) ;case 1
 
268
                (< i w)
 
269
                (<= 0 i)
 
270
                (<= 0 j) 
 
271
                (<= 0 k)
 
272
                (<= j i)
 
273
                (integerp k)
 
274
                (integerp w)
 
275
                (integerp i)
 
276
                (integerp j)
 
277
                )
 
278
           (equal (bitn (setbits x w i j y) k)
 
279
                  (bitn x k)))
 
280
  :hints (("Goal" :in-theory (enable setbits)))
 
281
  )
 
282
 
 
283
(defthm bitn-setbits-2
 
284
  (implies (and(<= k i) ;;case-2
 
285
               (<= j k) ;;case-2
 
286
               (<= 0 i)
 
287
               (<= 0 j) 
 
288
               (< i w)
 
289
               (integerp k)
 
290
               (integerp w)
 
291
               (integerp i)
 
292
               (integerp j)
 
293
               )
 
294
           (equal (bitn (setbits x w i j y) k)
 
295
                  (bitn y (- k j))))
 
296
  :hints (("Goal" :in-theory (enable setbits)))
 
297
  )
 
298
 
 
299
(defthm bitn-setbits-3
 
300
  (implies (and (< i k) ;;case-3
 
301
                (< k w) ;;case-3
 
302
;                (< i w)
 
303
                (<= 0 i)
 
304
                (<= 0 j) 
 
305
                (<= j i)
 
306
                (integerp i)
 
307
                (integerp j)
 
308
                (integerp k)
 
309
                (integerp w))
 
310
           (equal (bitn (setbits x w i j y) k)
 
311
                  (bitn x k)))
 
312
  :hints (("Goal" :in-theory (enable setbits)))
 
313
  )
 
314
 
 
315
 
 
316
;taking a slice of each of the lower two thirds.
 
317
(defthm bits-setbits-4
 
318
  (implies (and (<= k i) ;;case-4
 
319
                (<= j k) ;;case-4
 
320
                (< l j) ;;case-4
 
321
                (< i w)
 
322
                (<= 0 j)
 
323
                (<= 0 l)
 
324
                (integerp i)
 
325
                (integerp j)
 
326
                (integerp w) 
 
327
                (acl2-numberp l) ;(integerp l)
 
328
                )
 
329
           (equal (bits (setbits x w i j y) k l)
 
330
                  (cat (bits y (- k j) 0)
 
331
                       (+ 1 k (- j))
 
332
                       (bits x (1- j) l)
 
333
                       (- j l))))
 
334
  :hints (("Goal" :in-theory (enable setbits))))
 
335
 
 
336
;taking a slice of each of the upper two thirds.
 
337
(defthm bits-setbits-5
 
338
    (implies (and (< i k)  ;case-5
 
339
                  (<= l i) ;case-5
 
340
                  (<= j l) ;case-5
 
341
                  (< k w)  ;case-5 ;BOZO drop stuff like this?
 
342
                  (<= 0 j)
 
343
                  (integerp i)
 
344
                  (integerp j)
 
345
                  (integerp w)
 
346
                  (acl2-numberp l) ;(integerp l)
 
347
                  )
 
348
             (equal (bits (setbits x w i j y) k l)
 
349
                    (cat (bits x k (1+ i))
 
350
                         (+ k (- i))
 
351
                         (bits y (- i j) (- l j))
 
352
                         (1+ (- i l)))))
 
353
    :hints (("Goal" :in-theory (enable setbits))))
 
354
 
 
355
;taking a slice of each of the thirds.
 
356
;make one huge bits-setbits lemma?
 
357
(defthm bits-setbits-6
 
358
  (implies (and (< i k) ;;case-6
 
359
                (< l j) ;;case-6
 
360
                (<= j i)
 
361
                (< k w)
 
362
                (<= 0 l)
 
363
                (integerp i)
 
364
                (integerp j)
 
365
                (acl2-numberp l) ; (integerp l)
 
366
                (integerp w)
 
367
                )
 
368
           (equal (bits (setbits x w i j y) k l)
 
369
                  (cat (bits x k (1+ i))
 
370
                       (+ k (- i))
 
371
                       (cat (bits y (+ i (- j)) 0)
 
372
                            (1+ (- i j))
 
373
                            (bits x (1- j) l)
 
374
                            (- j l))
 
375
                       (+ 1 i (- l)))))
 
376
  :hints (("Goal" :in-theory (enable setbits))))
 
377
 
 
378
;prove that if (not (natp w)) setbits = 0 .
 
379
 
 
380
;combining these adjacent ranges [i..j][k..l]
 
381
(defthm setbits-combine
 
382
  (implies (and (equal j (+ k 1))
 
383
                (case-split (<= j i))
 
384
                (case-split (<= l k))
 
385
                (case-split (natp w))
 
386
                (case-split (natp i))
 
387
                (case-split (natp j))
 
388
                (case-split (natp k))
 
389
                (case-split (natp l))
 
390
                )
 
391
  (equal (setbits (setbits x w k l y1) w i j y2)
 
392
         (setbits x w i l (cat y2
 
393
                                (+ 1 i (- j))
 
394
                                y1
 
395
                                (+ 1 k (- l))
 
396
                                ))))
 
397
  :hints (("goal" :in-theory (enable setbits))))
 
398
 
 
399
(defthm setbits-combine-2
 
400
  (implies (and (equal j (+ k 1))
 
401
                (case-split (< i w))
 
402
                (case-split (<= j i))
 
403
                (case-split (<= l k))
 
404
                (case-split (natp w))
 
405
                (case-split (natp i))
 
406
                (case-split (natp j))
 
407
                (case-split (natp k))
 
408
                (case-split (natp l))
 
409
                )
 
410
  (equal (setbits (setbits x w i j y2) w k l y1)
 
411
         (setbits x w i l (cat y2
 
412
                                (+ 1 i (- j))
 
413
                                y1
 
414
                                (+ 1 k (- l))
 
415
                                ))))
 
416
  :hints (("goal" :in-theory (enable setbits))))
 
417
 
 
418
(defthm setbits-combine-3
 
419
  (implies (and (equal j (+ k 1))
 
420
                (case-split (< i w))
 
421
                (case-split (<= j i))
 
422
                (case-split (<= l k))
 
423
                (case-split (natp w))
 
424
                (case-split (natp i))
 
425
                (case-split (natp j))
 
426
                (case-split (natp k))
 
427
                (case-split (natp l)))
 
428
           (equal (setbits (setbits x w i j y2) w k l y1)
 
429
                  (setbits x w i l
 
430
                           (cat y2 (+ 1 i (- j))
 
431
                                 y1 (+ 1 k (- l)))))))
 
432
 
 
433
 
 
434
(defthm setbits-all
 
435
  (implies (and (equal i (1- w))
 
436
                (case-split (bvecp y w))
 
437
                )
 
438
  (equal (setbits x w i 0 y)
 
439
         y))
 
440
  :hints (("goal" :in-theory (enable setbits))))
 
441