← 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.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.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 "setbits-proofs"))
 
16
 
 
17
(defund bitn (x n)
 
18
  (declare (xargs :guard (and (natp x)
 
19
                              (natp n))
 
20
                  :verify-guards nil))
 
21
  (mbe :logic (bits x n n)
 
22
       :exec  (if (evenp (ash x (- n))) 0 1)))
 
23
 
 
24
#|
 
25
 
 
26
Currently we expect to leave setbits enabled so that it rewrites to cat, but there are some lemmas below which
 
27
might be useful if we choose to keep setbits disabled...
 
28
 
 
29
is this comment still valid? :
 
30
;it may happen that setbitn is called with an index which is a signal rather than a constant.
 
31
;in that case, we probably don't want it to expand to setbits. 
 
32
;thus, we always expect the indices in setbits calls to be constants
 
33
 
 
34
 
 
35
;Set bits I down to J of the W-bit value X to Y.
 
36
 
 
37
(setbits x w i j y) is only well-defined when the following predicate is true:
 
38
 
 
39
(and (natp w)
 
40
     (bvecp x w)
 
41
     (integerp i)
 
42
     (integerp j)
 
43
     (<= 0 j)
 
44
     (<= j i)
 
45
     (< i w)
 
46
     (bvecp y (+ 1 i (- j))))
 
47
 
 
48
|#
 
49
 
 
50
;Note: when j is 0, there is no lower part of x, but we have cat-with-n-0 to handle this case. 
 
51
(defund setbits (x w i j y)
 
52
  (declare (xargs :guard (and (natp x)
 
53
                              (natp y)
 
54
                              (integerp i)
 
55
                              (integerp j)
 
56
                              (<= 0 j)
 
57
                              (<= j i)
 
58
                              (integerp w)
 
59
                              (< i w))
 
60
                  :verify-guards nil))
 
61
  (mbe :logic (cat (bits x (1- w) (1+ i))
 
62
                   (+ -1 w (- i))
 
63
                   (cat (bits y (+ i (- j)) 0)
 
64
                        (+ 1 i (- j))
 
65
                        (bits x (1- j) 0)
 
66
                        j)
 
67
                   (1+ i))
 
68
       :exec  (cond ((int= j 0)
 
69
                     (cond ((int= (1+ i) w)
 
70
                            (bits y (+ i (- j)) 0))
 
71
                           (t
 
72
                            (cat (bits x (1- w) (1+ i))
 
73
                                 (+ -1 w (- i))
 
74
                                 (bits y (+ i (- j)) 0)
 
75
                                 (1+ i)))))
 
76
                    ((int= (1+ i) w)
 
77
                     (cat (bits y (+ i (- j)) 0)
 
78
                          (+ 1 i (- j))
 
79
                          (bits x (1- j) 0)
 
80
                          j))
 
81
                    (t
 
82
                     (cat (bits x (1- w) (1+ i))
 
83
                          (+ -1 w (- i))
 
84
                          (cat (bits y (+ i (- j)) 0)
 
85
                               (+ 1 i (- j))
 
86
                               (bits x (1- j) 0)
 
87
                               j)
 
88
                          (1+ i))))))
 
89
 
 
90
(defthm setbits-nonnegative-integer-type
 
91
  (and (integerp (setbits x w i j y))
 
92
       (<= 0 (setbits x w i j y)))
 
93
  :rule-classes (:type-prescription))
 
94
 
 
95
;this rule is no better than setbits-nonnegative-integer-type and might be worse:
 
96
(in-theory (disable (:type-prescription setbits)))
 
97
 
 
98
(defthm setbits-natp
 
99
  (natp (setbits x w i j y)))
 
100
 
 
101
;BOZO r-c?
 
102
;tighten?
 
103
(defthm setbits-upper-bound
 
104
  (< (setbits x w i j y) (expt 2 w)))
 
105
 
 
106
(defthm setbits-bvecp-simple
 
107
  (bvecp (setbits x w i j y) w))
 
108
 
 
109
(defthm setbits-bvecp
 
110
  (implies (and (<= w k) ;gen?
 
111
                (case-split (integerp k))
 
112
                )
 
113
           (bvecp (setbits x w i j y) k)))
 
114
 
 
115
(defthm setbits-does-nothing
 
116
  (implies (and (case-split (< i w))
 
117
                (case-split (<= j i))
 
118
                (case-split (integerp i))
 
119
                (case-split (integerp j))
 
120
                (case-split (<= 0 j))
 
121
                )
 
122
           (equal (setbits x w i j (bits x i j))
 
123
                  (bits x (1- w) 0))))
 
124
 
 
125
;taking bits from the lower third
 
126
(defthm bits-setbits-1
 
127
  (implies (and (< k j)
 
128
                (case-split (<= 0 w))
 
129
                (case-split (< i w))
 
130
                (case-split (<= 0 l))
 
131
                (case-split (<= j i)) ;drop?
 
132
                (case-split (integerp w))
 
133
                (case-split (integerp i))
 
134
                (case-split (integerp j))
 
135
                )
 
136
           (equal (bits (setbits x w i j y) k l)
 
137
                  (bits x k l)))
 
138
  :hints (("Goal" :in-theory (enable setbits))))
 
139
 
 
140
;taking bits from the middle third
 
141
;gen?
 
142
(defthm bits-setbits-2
 
143
  (implies (and (<= k i)
 
144
                (<= j l)
 
145
                (case-split (integerp i))
 
146
                (case-split (<= 0 j))
 
147
                (case-split (integerp j))
 
148
                (case-split (acl2-numberp k));            (case-split (integerp k))
 
149
                (case-split (acl2-numberp l)) ;   (case-split (integerp l))
 
150
                (case-split (integerp w))
 
151
                (case-split (<= 0 w))
 
152
                (case-split (< i w))
 
153
                )
 
154
           (equal (bits (setbits x w i j y) k l)
 
155
                  (bits y (- k j) (- l j))))
 
156
  :hints (("Goal" :in-theory (enable setbits natp))))
 
157
 
 
158
;taking bits from the upper third
 
159
(defthm bits-setbits-3
 
160
  (implies (and (< i l)
 
161
                (case-split (< i w))
 
162
                (case-split (< k w)) ;handle this?
 
163
                (case-split (<= j i))
 
164
                (case-split (<= 0 l))
 
165
                (case-split (<= 0 j))
 
166
                (case-split (<= 0 w))
 
167
                (case-split (integerp l))
 
168
                (case-split (integerp w))
 
169
                (case-split (integerp i))
 
170
                (case-split (integerp j))
 
171
                (case-split (integerp k))
 
172
                )
 
173
           (equal (bits (setbits x w i j y) k l)
 
174
                  (bits x k l)))
 
175
  :hints (("Goal" :in-theory (enable setbits natp))))
 
176
 
 
177
(defthm setbits-with-w-0
 
178
  (equal (setbits x 0 i j y)
 
179
         0))
 
180
 
 
181
;add case-splits to the bitn-setbits rules?
 
182
;why can't i prove this from bits-setbits?
 
183
(defthm bitn-setbits-1
 
184
  (implies (and (< k j) ;case 1
 
185
                (< i w)
 
186
                (<= 0 i)
 
187
                (<= 0 j) 
 
188
                (<= 0 k)
 
189
                (<= j i)
 
190
                (integerp k)
 
191
                (integerp w)
 
192
                (integerp i)
 
193
                (integerp j)
 
194
                )
 
195
           (equal (bitn (setbits x w i j y) k)
 
196
                  (bitn x k))))
 
197
 
 
198
(defthm bitn-setbits-2
 
199
  (implies (and(<= k i) ;;case-2
 
200
               (<= j k) ;;case-2
 
201
               (<= 0 i)
 
202
               (<= 0 j) 
 
203
               (< i w)
 
204
               (integerp k)
 
205
               (integerp w)
 
206
               (integerp i)
 
207
               (integerp j)
 
208
               )
 
209
           (equal (bitn (setbits x w i j y) k)
 
210
                  (bitn y (- k j)))))
 
211
 
 
212
(defthm bitn-setbits-3
 
213
  (implies (and (< i k) ;;case-3
 
214
                (< k w) ;;case-3
 
215
;                (< i w)
 
216
                (<= 0 i)
 
217
                (<= 0 j) 
 
218
                (<= j i)
 
219
                (integerp i)
 
220
                (integerp j)
 
221
                (integerp k)
 
222
                (integerp w))
 
223
           (equal (bitn (setbits x w i j y) k)
 
224
                  (bitn x k))))
 
225
 
 
226
;taking a slice of each of the lower two thirds.
 
227
(defthm bits-setbits-4
 
228
  (implies (and (<= k i) ;;case-4
 
229
                (<= j k) ;;case-4
 
230
                (< l j) ;;case-4
 
231
                (< i w)
 
232
                (<= 0 j)
 
233
                (<= 0 l)
 
234
                (integerp i)
 
235
                (integerp j)
 
236
                (integerp w) 
 
237
                (acl2-numberp l) ;(integerp l)
 
238
                )
 
239
           (equal (bits (setbits x w i j y) k l)
 
240
                  (cat (bits y (- k j) 0)
 
241
                       (+ 1 k (- j))
 
242
                       (bits x (1- j) l)
 
243
                       (- j l))))
 
244
  :hints (("Goal" :in-theory (enable setbits))))
 
245
 
 
246
;taking a slice of each of the upper two thirds.
 
247
(defthm bits-setbits-5
 
248
    (implies (and (< i k)  ;case-5
 
249
                  (<= l i) ;case-5
 
250
                  (<= j l) ;case-5
 
251
                  (< k w)  ;case-5 ;BOZO drop stuff like this?
 
252
                  (<= 0 j)
 
253
                  (integerp i)
 
254
                  (integerp j)
 
255
                  (integerp w)
 
256
                  (acl2-numberp l) ;(integerp l)
 
257
                  )
 
258
             (equal (bits (setbits x w i j y) k l)
 
259
                    (cat (bits x k (1+ i))
 
260
                         (+ k (- i))
 
261
                         (bits y (- i j) (- l j))
 
262
                         (1+ (- i l))))))
 
263
 
 
264
;taking a slice of each of the thirds.
 
265
;make one huge bits-setbits lemma?
 
266
(defthm bits-setbits-6
 
267
  (implies (and (< i k) ;;case-6
 
268
                (< l j) ;;case-6
 
269
                (<= j i)
 
270
                (< k w)
 
271
                (<= 0 l)
 
272
                (integerp i)
 
273
                (integerp j)
 
274
                (acl2-numberp l) ; (integerp l)
 
275
                (integerp w)
 
276
                )
 
277
           (equal (bits (setbits x w i j y) k l)
 
278
                  (cat (bits x k (1+ i))
 
279
                       (+ k (- i))
 
280
                       (cat (bits y (+ i (- j)) 0)
 
281
                            (1+ (- i j))
 
282
                            (bits x (1- j) l)
 
283
                            (- j l))
 
284
                       (+ 1 i (- l))))))
 
285
 
 
286
;prove that if (not (natp w)) setbits = 0 .
 
287
 
 
288
;are our setbits-combine rules sufficient to cover all of the cases?
 
289
 
 
290
;combining these adjacent ranges [i..j][k..l]
 
291
(defthm setbits-combine
 
292
  (implies (and (equal j (+ k 1))
 
293
                (case-split (<= j i))
 
294
                (case-split (<= l k))
 
295
                (case-split (natp w))
 
296
                (case-split (natp i))
 
297
                (case-split (natp j))
 
298
                (case-split (natp k))
 
299
                (case-split (natp l))
 
300
                )
 
301
  (equal (setbits (setbits x w k l y1) w i j y2)
 
302
         (setbits x w i l (cat y2
 
303
                                (+ 1 i (- j))
 
304
                                y1
 
305
                                (+ 1 k (- l))
 
306
                                )))))
 
307
 
 
308
(defthm setbits-combine-2
 
309
  (implies (and (equal j (+ k 1))
 
310
                (case-split (< i w))
 
311
                (case-split (<= j i))
 
312
                (case-split (<= l k))
 
313
                (case-split (natp w))
 
314
                (case-split (natp i))
 
315
                (case-split (natp j))
 
316
                (case-split (natp k))
 
317
                (case-split (natp l))
 
318
                )
 
319
  (equal (setbits (setbits x w i j y2) w k l y1)
 
320
         (setbits x w i l (cat y2
 
321
                                (+ 1 i (- j))
 
322
                                y1
 
323
                                (+ 1 k (- l))
 
324
                                )))))
 
325
 
 
326
(defthm setbits-combine-3
 
327
  (implies (and (equal j (+ k 1))
 
328
                (case-split (< i w))
 
329
                (case-split (<= j i))
 
330
                (case-split (<= l k))
 
331
                (case-split (natp w))
 
332
                (case-split (natp i))
 
333
                (case-split (natp j))
 
334
                (case-split (natp k))
 
335
                (case-split (natp l)))
 
336
           (equal (setbits (setbits x w i j y2) w k l y1)
 
337
                  (setbits x w i l
 
338
                           (cat y2 (+ 1 i (- j))
 
339
                                 y1 (+ 1 k (- l)))))))
 
340
 
 
341
 
 
342
(defthm setbits-all
 
343
  (implies (and (equal i (1- w))
 
344
                (case-split (bvecp y w))
 
345
                )
 
346
  (equal (setbits x w i 0 y)
 
347
         y)))
 
348