← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2006/hunt-reeber/support/acl2.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/2006/hunt-reeber/support/acl2.lisp
 
1
 
 
2
(in-package "ACL2")
 
3
 
 
4
;; This file contains the examples from our paper that we
 
5
;; were able to prove using Brute force through the ACL2
 
6
;; simplifier.  Recursive calls are unrolled and ifs are
 
7
;; turned into case splits.
 
8
 
 
9
;; For a description of the example and a description of
 
10
;; how this relates to our SAT system see our workshop paper,
 
11
;; A SAT-Based Procedure for Verifying Finite State Machines in ACL2.
 
12
 
 
13
(defun n-bleq (n x y)
 
14
  (if (zp n)
 
15
      t
 
16
    (and (iff (car x) (car y))
 
17
         (n-bleq (1- n) (cdr x) (cdr y)))))
 
18
 
 
19
(defun xor3 (x y z)
 
20
  (xor x (xor y z)))
 
21
 
 
22
(defun maj3 (x y z)
 
23
  (if x (or y z)
 
24
    (and y z)))
 
25
 
 
26
;; Returns a n+1 length sum of the first
 
27
;; n bits of a and b (plus the carray).
 
28
(defun v-adder (n c a b)
 
29
  (if (zp n)
 
30
      (list c)
 
31
    (cons (xor3 c (car a) (car b))
 
32
          (v-adder (1- n) 
 
33
                   (maj3 c (car a) (car b))
 
34
                   (cdr a) (cdr b)))))
 
35
 
 
36
(defthm v-adder-rewrite 
 
37
  (equal
 
38
   (v-adder n c a b)
 
39
   (if (zp n)
 
40
       (list c)
 
41
     (cons (xor3 c (car a) (car b))
 
42
           (v-adder (1- n) 
 
43
                    (maj3 c (car a) (car b))
 
44
                    (cdr a) (cdr b))))))
 
45
 
 
46
(defthm n-bleq-rewrite
 
47
  (equal 
 
48
   (n-bleq n x y)
 
49
   (if (zp n)
 
50
       t
 
51
     (and (iff (car x) (car y))
 
52
          (n-bleq (1- n) (cdr x) (cdr y))))))
 
53
 
 
54
 
 
55
;; ;; 4 Bit Adder Associativity
 
56
;; (defthm 4-adder-assoc
 
57
;;   (n-bleq 4 (v-adder 4 nil (v-adder 4 nil a b) c)
 
58
;;           (v-adder 4 nil a (v-adder 4 nil b c))))))
 
59
 
 
60
;; ;; 32 bit adder associativity
 
61
;; (defthm 32-adder-assoc
 
62
;;   (n-bleq 32 (v-adder 32 nil (v-adder 32 nil a b) c)
 
63
;;           (v-adder 32 nil a (v-adder 32 nil b c))))
 
64
 
 
65
;; ;; 200 Bit adder associativity
 
66
;; (defthm 200-adder-assoc
 
67
;;   (n-bleq 200 (v-adder 200 nil (v-adder 200 nil a b) c)
 
68
;;           (v-adder 200 nil a (v-adder 200 nil b c))))
 
69
 
 
70
 
 
71
(defun nth-cdr (n x)
 
72
  (if (zp n)
 
73
      x
 
74
    (nth-cdr (1- n) (cdr x))))
 
75
 
 
76
(defun nth-sublist (n lst)
 
77
  (if (zp n)
 
78
      nil
 
79
    (cons (car lst) (nth-sublist (1- n) (cdr lst)))))
 
80
 
 
81
(defun append-n (n x y)
 
82
  (if (zp n)
 
83
      y
 
84
    (cons (car x) (append-n (1- n) (cdr x) y))))
 
85
 
 
86
(defun n-nills (n)
 
87
  (if (zp n)
 
88
      nil
 
89
    (cons nil (n-nills (1- n)))))
 
90
 
 
91
(defun rev-n (n x ans)
 
92
  (if (zp n)
 
93
      ans
 
94
    (rev-n (1- n) (cdr x) (cons (car x) ans))))
 
95
 
 
96
(defun mux-n-help (n in rsel)
 
97
  (if (zp n)
 
98
      (car in)
 
99
    (if (car rsel)
 
100
        (mux-n-help (1- n) (nth-cdr (expt 2 (1- n)) in) (cdr rsel))
 
101
      (mux-n-help (1- n) in (cdr rsel)))))
 
102
 
 
103
(defun mux-n (n in sel)
 
104
  (mux-n-help n in (rev-n n sel nil)))
 
105
 
 
106
(defun mux-n-w-help (n w in)
 
107
  (if (zp n)
 
108
      nil
 
109
    (cons (car in) (mux-n-w-help (1- n) w (nth-cdr w in)))))
 
110
 
 
111
(defun mux-n-w1 (nw sn w in sel)
 
112
  (if (zp nw)
 
113
      nil
 
114
    (cons (mux-n sn (mux-n-w-help (expt 2 sn) w in) sel)
 
115
          (mux-n-w1 (1- nw) sn w (cdr in) sel))))
 
116
 
 
117
(defun mux-n-w (n w in sel)
 
118
  (mux-n-w1 w n w in sel))
 
119
 
 
120
(defun shift-mux-help (n w reg)
 
121
  (if (zp n)
 
122
      nil
 
123
    (append-n w reg (shift-mux-help (1- n) w (cons nil reg)))))
 
124
 
 
125
(defun shifter (sn rn rshift reg)
 
126
  (if (zp sn)
 
127
      reg
 
128
    (mux-n-w sn rn (shift-mux-help (expt 2 sn) rn reg) rshift)))
 
129
 
 
130
(defthm append-n-rewrite
 
131
  (equal
 
132
   (append-n n x y)
 
133
   (if (zp n)
 
134
       y
 
135
     (cons (car x) (append-n (1- n) (cdr x) y)))))
 
136
 
 
137
(defthm nth-cdr-rewrite
 
138
  (equal
 
139
   (nth-cdr n x)
 
140
   (if (zp n)
 
141
       x
 
142
     (nth-cdr (1- n) (cdr x)))))
 
143
 
 
144
(defthm nth-sublist-rewrite
 
145
  (equal
 
146
   (nth-sublist n lst)
 
147
   (if (zp n)
 
148
       nil
 
149
     (cons (car lst) (nth-sublist (1- n) (cdr lst))))))
 
150
 
 
151
(defthm n-nills-rewrite 
 
152
  (equal 
 
153
   (n-nills n)
 
154
   (if (zp n)
 
155
       nil
 
156
     (cons nil (n-nills (1- n))))))
 
157
 
 
158
(defthm rev-n-rewrite 
 
159
  (equal 
 
160
   (rev-n n x ans)
 
161
   (if (zp n)
 
162
       ans
 
163
     (rev-n (1- n) (cdr x) (cons (car x) ans)))))
 
164
 
 
165
(defthm mux-n-help-rewrite
 
166
  (equal
 
167
   (mux-n-help n in rsel)
 
168
   (if (zp n)
 
169
       (car in)
 
170
     (if (car rsel)
 
171
         (mux-n-help (1- n) (nth-cdr (expt 2 (1- n)) in) (cdr rsel))
 
172
       (mux-n-help (1- n) in (cdr rsel)))))
 
173
  :hints (("Goal" :in-theory (disable nth-cdr-rewrite))))
 
174
 
 
175
(defthm mux-n-w-help-rewrite
 
176
  (equal
 
177
   (mux-n-w-help n w in)
 
178
   (if (zp n)
 
179
       nil
 
180
     (cons (car in) (mux-n-w-help (1- n) w (nth-cdr w in)))))
 
181
  :hints (("Goal" :in-theory (disable nth-cdr-rewrite))))
 
182
 
 
183
(defthm mux-n-w1-rewrite
 
184
  (equal
 
185
   (mux-n-w1 nw sn w in sel)
 
186
   (if (zp nw)
 
187
       nil
 
188
     (cons (mux-n sn (mux-n-w-help (expt 2 sn) w in) sel)
 
189
           (mux-n-w1 (1- nw) sn w (cdr in) sel))))
 
190
    :hints (("Goal" :in-theory (disable mux-n-w-help-rewrite mux-n-w-help mux-n mux-n-help-rewrite))))
 
191
 
 
192
(defthm shift-mux-help-rewrite
 
193
  (equal 
 
194
   (shift-mux-help n w reg)
 
195
   (if (zp n)
 
196
       nil
 
197
     (append-n w reg (shift-mux-help (1- n) w (cons nil reg)))))
 
198
  :hints (("Goal" :in-theory (disable append-n-rewrite))))
 
199
 
 
200
;; ;; 32x6 Shift-0
 
201
;; (defthm 32x6-shift-0
 
202
;;  (implies 
 
203
;;   (car (nth-cdr 5 shift0))
 
204
;;   (n-bleq 32 
 
205
;;           (shifter 6 32 shift0 reg)
 
206
;;           (n-nills 32))))
 
207
 
 
208
 
 
209
;; ;; 64x7 Shift-0
 
210
;; (defthm 64x7-shift-0
 
211
;;  (implies 
 
212
;;   (car (nth-cdr 6 shift0))
 
213
;;   (n-bleq 64 (shifter 7 64 shift0 reg)
 
214
;;           (n-nills 64))))
 
215
 
 
216
;; ;; 32x4 Add-shift
 
217
;; (defthm 32x4-add-shift
 
218
;;  (n-bleq 32 
 
219
;;          (shifter 4 32 shift0 (shifter 4 32 shift1 reg))
 
220
;;          (shifter 5 32 (v-adder 4 nil shift0 shift1) reg)))
 
221
 
 
222
;; ;; 64x6 Add-shift
 
223
;; (defthm 64x6-add-shift
 
224
;;  (n-bleq 64 
 
225
;;          (shifter 6 64 shift0 (shifter 6 64 shift1 reg))
 
226
;;          (shifter 7 64 (v-adder 6 nil shift0 shift1) reg)))
 
227
 
 
228
(defun increment (n x)
 
229
  (if (zp n)
 
230
      nil
 
231
    (if (car x)
 
232
        (cons nil (increment (1- n) (cdr x)))
 
233
      (cons t (cdr x)))))
 
234
 
 
235
(defthm increment-rewrite
 
236
  (implies 
 
237
   (and (syntaxp (quotep n))
 
238
        (not (zp n)))
 
239
   (equal (increment n x)
 
240
          (if (car x)
 
241
              (cons nil (increment (1- n) (cdr x)))
 
242
            (cons t (cdr x))))))
 
243
 
 
244
(defthm increment-rewrite0
 
245
  (equal (increment 0 x)
 
246
         nil))
 
247
 
 
248
(defun next_digit_counter_state (x)
 
249
  (if (n-bleq 4 x '(t nil nil t))
 
250
      (list '(nil nil nil nil) t)
 
251
    (list (increment 4 x) nil)))
 
252
 
 
253
(defun next_counter_state (n x)
 
254
  (let* ((curr_d_out (next_digit_counter_state (car x)))
 
255
         (curr_d_val (car curr_d_out))
 
256
         (curr_d_reset (cadr curr_d_out)))
 
257
    (if (zp n)
 
258
        nil
 
259
      (if curr_d_reset
 
260
          (cons curr_d_val (next_counter_state (1- n) (cdr x)))
 
261
        (cons curr_d_val (cdr x))))))
 
262
 
 
263
 
 
264
(defun valid_digit (a)
 
265
  (let ((a1 (cadr a))
 
266
        (a2 (caddr a))
 
267
        (a3 (cadddr a)))
 
268
    (not (and a3 (or a2 a1)))))
 
269
 
 
270
(defun valid_digits (n x)
 
271
  (if (zp n)
 
272
      (not (consp x))
 
273
    (and (valid_digit (car x))
 
274
         (valid_digits (1- n) (cdr x)))))
 
275
 
 
276
(defthm valid_digits-rewrite
 
277
  (implies 
 
278
   (and (syntaxp (quotep n))
 
279
        (not (zp n)))
 
280
  (equal
 
281
   (valid_digits n x)
 
282
   (and (valid_digit (car x))
 
283
        (valid_digits (1- n) (cdr x))))))
 
284
 
 
285
(defthm valid_digits-rewrite0
 
286
  (equal (valid_digits 0 x)
 
287
         (not (consp x))))
 
288
 
 
289
;; 100 Digit Counter Invariant
 
290
;; (defthm 100-digit-counter-inv
 
291
;;  (implies
 
292
;;   (valid_digits 100 x)
 
293
;;   (valid_digits 100 (next_counter_state 100 x))))
 
294