← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/projects/codewalker/m1-version-3.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/projects/codewalker/m1-version-3.lisp
 
1
; Copyright (C) 2014, ForrestHunt, Inc.
 
2
; Written by J Moore
 
3
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
 
4
 
 
5
#||
 
6
Like m1-version-1 but uses stobjs.
 
7
 
 
8
I totally ignore the guard question.
 
9
 
 
10
See the README file on this directory for an overview of this work.
 
11
 
 
12
(defpkg "M1"
 
13
  (set-difference-eq (union-eq *acl2-exports*
 
14
                               *common-lisp-symbols-from-main-lisp-package*)
 
15
                     '(push pop pc program step
 
16
                            ; nth update-nth nth-update-nth  ; <--- stobjs use built-ins
 
17
                            )))
 
18
(certify-book "m1-version-3" 1)
 
19
||#
 
20
 
 
21
(in-package "M1")
 
22
 
 
23
; -----------------------------------------------------------------
 
24
; Stack Manipulation
 
25
 
 
26
(defun push (x y)
 
27
  (cons x y))
 
28
 
 
29
(defun top (stack)
 
30
  (car stack))
 
31
 
 
32
(defun pop (stack)
 
33
  (cdr stack))
 
34
 
 
35
; -----------------------------------------------------------------
 
36
 
 
37
; State Manipulation:
 
38
 
 
39
(set-verify-guards-eagerness 0)
 
40
 
 
41
; I name the components with the prefix "ugly-" because I don't want
 
42
; to see them in proofs!  I'm going to define a more uniform interface. 
 
43
 
 
44
(defstobj s ugly-pc ugly-locals ugly-stack ugly-program)
 
45
 
 
46
; Basic read/write operations on state: for each field f of a stobj, defstobj
 
47
; provides two functions, f and update-f, for accessing and updating the field
 
48
; value.  Now think about how messy it is to normalize a random mix of update
 
49
; expressions, e.g., (update-h a (update-g b (update-h c (update-f d st)))).
 
50
; So I define a pair of read/write functions that can hit each field of the
 
51
; stobj, then I prove the normalization rules, then I disable these basic
 
52
; functions.  Finally, I use the basic functions to define the field-specific
 
53
; update-f versions.  I define how to write to the cd field even though it is
 
54
; never needed.  I did this to provide a uniform interface: to access or change
 
55
; a field, use rd or wr.
 
56
 
 
57
(defun wr (key v s)
 
58
  (declare (xargs :stobjs (s)))
 
59
  (case key
 
60
    (:pc (update-ugly-pc v s))
 
61
    (:locals (update-ugly-locals v s))
 
62
    (:stack (update-ugly-stack v s))
 
63
    (:program (update-ugly-program v s))
 
64
    (otherwise s)))
 
65
 
 
66
(defun rd (key s)
 
67
  (declare (xargs :stobjs (s)))
 
68
  (case key
 
69
    (:pc (ugly-pc s))
 
70
    (:locals (ugly-locals s))
 
71
    (:stack (ugly-stack s))
 
72
    (:program (ugly-program s))
 
73
    (otherwise 0)))
 
74
 
 
75
(defthm sp-wr
 
76
  (implies (sp s)
 
77
           (sp (wr loc val s))))
 
78
 
 
79
(in-theory (disable sp))
 
80
 
 
81
(defun keyp (k) (member k '(:pc :locals :stack :program)))
 
82
 
 
83
(defthm rd-wr
 
84
  (equal (rd key1 (wr key2 v s))
 
85
         (if (and (equal key1 key2)
 
86
                  (keyp key1))
 
87
             v
 
88
             (rd key1 s))))
 
89
 
 
90
(defthm update-nth-update-nth-diff
 
91
  (implies (and (natp i) (natp j) (not (equal i j)))
 
92
           (equal (update-nth i v (update-nth j w list))
 
93
                  (update-nth j w (update-nth i v list))))
 
94
  :rule-classes ((:rewrite :loop-stopper ((i j update-nth)))))
 
95
 
 
96
(defthm update-nth-update-nth-same
 
97
  (equal (update-nth i v (update-nth i w list))
 
98
         (update-nth i v list)))
 
99
 
 
100
(defthm update-nth-redundant
 
101
  (implies (and (natp i)
 
102
                (< i (len x))
 
103
                (equal (nth i x) v))
 
104
           (equal (update-nth i v x) x)))
 
105
 
 
106
(defthm wr-wr-diff
 
107
  (implies (and (keyp key1)
 
108
                (keyp key2)
 
109
                (not (equal key1 key2)))
 
110
           (equal (wr key1 v1 (wr key2 v2 s))
 
111
                  (wr key2 v2 (wr key1 v1 s))))
 
112
  :hints (("Goal" :in-theory (disable nth update-nth)))
 
113
  :rule-classes ((:rewrite :loop-stopper ((key1 key2 wr)))))
 
114
 
 
115
(defthm wr-wr-same
 
116
  (implies (keyp key1)
 
117
           (equal (wr key1 v1 (wr key1 v2 s))
 
118
                  (wr key1 v1 s))))
 
119
 
 
120
(defthm wr-redundant
 
121
  (implies (and (sp s)                     ; <---- added and deleted below!
 
122
                (equal (rd key s) v)
 
123
;               (equal (len s) 4)          ; <----
 
124
                )
 
125
           (equal (wr key v s) s))
 
126
  :hints (("Goal" :in-theory (enable sp))))  ; <---
 
127
 
 
128
;(defthm len-wr
 
129
;  (implies (equal (len s) 4)
 
130
;           (equal (len (wr key v s)) 4)))
 
131
 
 
132
(in-theory (disable rd wr))
 
133
 
 
134
; The following functions are just handy abbreviations to use in the semantics
 
135
; of the instructions.  I expect them always to be expanded into rd/wr terms.
 
136
; They could be macros.
 
137
 
 
138
(defun pc (s)
 
139
  (declare (xargs :stobjs (s)))
 
140
  (rd :pc s))
 
141
 
 
142
(defun !pc (v s)
 
143
  (declare (xargs :stobjs (s)))
 
144
  (wr :pc v s))
 
145
 
 
146
; There is no need to define lo and !lo since we always change indexed
 
147
; positions, not the whole field.
 
148
 
 
149
(defun loi (i s)
 
150
  (declare (xargs :stobjs (s)))
 
151
  (nth i (rd :locals s)))
 
152
 
 
153
(defun !loi (i v s)
 
154
  (declare (xargs :stobjs (s)))
 
155
  (wr :locals (update-nth i v (rd :locals s)) s))
 
156
 
 
157
(defun stack (s)
 
158
  (declare (xargs :stobjs (s)))
 
159
  (rd :stack s))
 
160
 
 
161
(defun !stack (v s)
 
162
  (declare (xargs :stobjs (s)))
 
163
  (wr :stack v s))
 
164
 
 
165
; There is no need to define !program.
 
166
 
 
167
(defun program (s)
 
168
  (declare (xargs :stobjs (s)))
 
169
  (rd :program s))
 
170
 
 
171
(defun next-inst (s)
 
172
  (declare (xargs :stobjs (s)))
 
173
  (nth (pc s) (program s)))
 
174
 
 
175
; -----------------------------------------------------------------
 
176
; Instruction Accessors
 
177
 
 
178
(defun op-code (inst)
 
179
  (nth 0 inst))
 
180
 
 
181
(defun arg1 (inst)
 
182
  (nth 1 inst))
 
183
 
 
184
; -----------------------------------------------------------------
 
185
 
 
186
; The M1 Machine
 
187
 
 
188
; Now we define the semantics of each instruction.  These functions are called
 
189
; ``semantic functions.''
 
190
 
 
191
; Each opcode will be given semantics with an ACL2 function that takes an
 
192
; instruction (with the given opcode) and a state and returns the state
 
193
; produced by executing the instruction.  For example, the ILOAD instruction,
 
194
; which looks like this (ILOAD k), where k is the index of the local variable
 
195
; to be loaded, is given semantics by the function execute-ILOAD.  Execute-ILOAD is
 
196
; the ``semantic function'' for ILOAD.
 
197
 
 
198
; Our expectation when (execute-ILOAD inst s) is called is that s is a ``good''
 
199
; M1 state, that inst is the next instruction in s, and that inst is an ILOAD
 
200
; instruction.  If all that is true, we can run execute-ILOAD without error,
 
201
; i.e., without worrying whether the instruction is well-formed, whether the
 
202
; local variable of that index exists, whether incrementing the pc pushes it
 
203
; outside the bounds of the program, etc.  Because we have analogous
 
204
; expectations on the semantic function for each opcode, we wrap up these
 
205
; expectations into a single predicate:
 
206
 
 
207
; Semantics of (ILOAD k): increment the pc and push onto the stack the value of
 
208
; the kth local.  Aside: We will know, by guard verification, that the new pc
 
209
; is legal and that the value pushed is a rational number.  As a rule, I will
 
210
; not comment here on everything we know by guard verification, I'm just trying
 
211
; to give you a sense of the implications of our expectations.
 
212
 
 
213
(defun execute-ILOAD (inst s)
 
214
  (declare (xargs :stobjs (s)))
 
215
  (let* ((s (!stack (push (loi (arg1 inst) s) (stack s))
 
216
                    s))
 
217
         (s (!pc (+ 1 (pc s)) s)))
 
218
    s))
 
219
 
 
220
; Semantics of (ICONST k):  increment the pc and push k onto the stack.
 
221
 
 
222
(defun execute-ICONST (inst s)
 
223
  (declare (xargs :stobjs (s)))
 
224
  (let* ((s (!stack (push (arg1 inst) (stack s))
 
225
                    s))
 
226
         (s (!pc (+ 1 (pc s)) s)))
 
227
    s))
 
228
 
 
229
; Semantics of (IADD): increment the pc, pop two items off the stack and push
 
230
; their sum.  Aside: We will know, by guard verification, that there are at
 
231
; least two items on the stack and that they are both rational numbers.
 
232
 
 
233
(defun execute-IADD (inst s)
 
234
  (declare (xargs :stobjs (s))
 
235
           (ignore inst))
 
236
  (let ((u (top (stack s)))
 
237
        (v (top (pop (stack s))))
 
238
        (stack1 (pop (pop (stack s)))))
 
239
    (let* ((s (!stack (push (+ v u) stack1) s))
 
240
           (s (!pc (+ 1 (pc s)) s)))
 
241
      s)))
 
242
 
 
243
; Semantics of (ISUB): increment the pc, pop two items off the stack and push
 
244
; their difference.
 
245
 
 
246
(defun execute-ISUB (inst s)
 
247
  (declare (xargs :stobjs (s))
 
248
           (ignore inst))
 
249
  (let ((u (top (stack s)))
 
250
        (v (top (pop (stack s))))
 
251
        (stack1 (pop (pop (stack s)))))
 
252
    (let* ((s (!stack (push (- v u) stack1) s))
 
253
           (s (!pc (+ 1 (pc s)) s)))
 
254
      s)))
 
255
 
 
256
; Semantics of (IMUL): increment the ic, pop two items off the stack and push
 
257
; their product.
 
258
 
 
259
(defun execute-IMUL (inst s)
 
260
  (declare (xargs :stobjs (s))
 
261
           (ignore inst))
 
262
  (let ((u (top (stack s)))
 
263
        (v (top (pop (stack s))))
 
264
        (stack1 (pop (pop (stack s)))))
 
265
    (let* ((s (!stack (push (* v u) stack1) s))
 
266
           (s (!pc (+ 1 (pc s)) s)))
 
267
      s)))
 
268
 
 
269
; Semantics of (ISTORE k): increment the ic, pop one item off the stack, and
 
270
; store it as the value of local variable k.
 
271
 
 
272
(defun execute-ISTORE (inst s)
 
273
  (declare (xargs :stobjs (s)))
 
274
  (let ((u (top (stack s)))
 
275
        (stack1 (pop (stack s))))
 
276
    (let* ((s (!stack stack1 s))
 
277
           (s (!loi (arg1 inst) u s))
 
278
           (s (!pc (+ 1 (pc s)) s)))
 
279
      s)))
 
280
 
 
281
; Semantics of (GOTO k): increment the pc by k.  Aside: We will know, by guard
 
282
; verification, that the new pc is legal.
 
283
 
 
284
(defun execute-GOTO (inst s)
 
285
  (declare (xargs :stobjs (s)))
 
286
  (let* ((s (!pc (+ (arg1 inst) (pc s)) s)))
 
287
    s))
 
288
 
 
289
; Semantics of (IFEQ k): pop one item off the stack and increment the pc k if
 
290
; that item is 0 and by 1 if if is non-0.  Aside: We will know, by guard
 
291
; verification, that the new pc is legal.
 
292
 
 
293
(defun execute-IFEQ (inst s)
 
294
  (declare (xargs :stobjs (s)))
 
295
  (let ((u (top (stack s)))
 
296
        (stack1 (pop (stack s))))
 
297
    (let* ((s (!stack stack1 s))
 
298
           (s (!pc (if (equal u 0)
 
299
                       (+ (arg1 inst) (pc s))
 
300
                       (+ 1 (pc s)))
 
301
                   s)))
 
302
      s)))
 
303
 
 
304
(defun do-inst (inst s)
 
305
  (declare (xargs :stobjs (s)))
 
306
  (if (equal (op-code inst) 'ILOAD)
 
307
      (execute-ILOAD  inst s)
 
308
      (if (equal (op-code inst) 'ICONST)
 
309
          (execute-ICONST  inst s)
 
310
          (if (equal (op-code inst) 'IADD)
 
311
              (execute-IADD   inst s)
 
312
              (if (equal (op-code inst) 'ISUB)
 
313
                  (execute-ISUB   inst s)
 
314
                  (if (equal (op-code inst) 'IMUL)
 
315
                      (execute-IMUL   inst s)
 
316
                      (if (equal (op-code inst) 'ISTORE)
 
317
                          (execute-ISTORE  inst s)
 
318
                          (if (equal (op-code inst) 'GOTO)
 
319
                              (execute-GOTO   inst s)
 
320
                              (if (equal (op-code inst) 'IFEQ)
 
321
                                  (execute-IFEQ   inst s)
 
322
                                  s)))))))))
 
323
 
 
324
; This is the single-step function: it executes the next instruction in a
 
325
; state.  Aside: We will know, by guard verification, that the resulting state
 
326
; is a good state.
 
327
 
 
328
(defun step (s)
 
329
  (declare (xargs :stobjs (s)))
 
330
  (do-inst (next-inst s) s))
 
331
 
 
332
(defun m1 (s n)
 
333
  (declare (xargs :stobjs (s)))
 
334
  (if (zp n)
 
335
      s
 
336
      (let* ((s (step s)))
 
337
        (m1 s (- n 1)))))
 
338
 
 
339
(defun haltedp (s)
 
340
  (declare (xargs :stobjs (s)))
 
341
  (equal (next-inst s) '(HALT)))
 
342
 
 
343
; =================================================================
 
344
; Lemmas for Proving M1 Code
 
345
 
 
346
; Arithmetic
 
347
 
 
348
(include-book "arithmetic-5/top" :dir :system)
 
349
 
 
350
; Stacks
 
351
 
 
352
(defthm top-push
 
353
  (equal (top (push x y)) x))
 
354
 
 
355
(defthm pop-push
 
356
  (equal (pop (push x y)) y))
 
357
 
 
358
(defun popn (n stk)
 
359
  (if (zp n)
 
360
      stk
 
361
    (popn (- n 1) (pop stk))))
 
362
 
 
363
(defmacro push* (&rest lst)
 
364
  (if (endp lst)
 
365
      nil
 
366
      (if (endp (cdr lst))
 
367
          (car lst)
 
368
          `(push ,(car lst) (push* ,@(cdr lst))))))
 
369
 
 
370
(defthm len-push
 
371
  (equal (len (push x y))
 
372
         (+ 1 (len y))))
 
373
 
 
374
; Abstract Data Type Stuff
 
375
 
 
376
(defthm constant-stacks
 
377
  (and
 
378
 
 
379
; These next two are needed because some push expressions evaluate to
 
380
; list constants, e.g., (push 1 (push 2 nil)) becomes '(1 2) and '(1
 
381
; 2) pattern-matches with (cons x s) but not with (push x s).
 
382
 
 
383
       (equal (top (cons x s)) x)
 
384
       (equal (pop (cons x s)) s))
 
385
  :hints (("Goal" :in-theory (enable top pop))))
 
386
 
 
387
 
 
388
(in-theory (disable push (:executable-counterpart push) top pop))
 
389
 
 
390
; Step Stuff
 
391
 
 
392
(defthm step-opener
 
393
  (implies (consp (next-inst s))
 
394
           (equal (step s)
 
395
                  (do-inst (next-inst s) s)))
 
396
 
 
397
  :hints (("Goal" :in-theory (enable step))))
 
398
 
 
399
(in-theory (disable step))
 
400
 
 
401
; Schedules and Run
 
402
 
 
403
(defun binary-clk+ (i j)
 
404
  (+ (nfix i) (nfix j)))
 
405
 
 
406
(defthm clk+-associative
 
407
  (equal (binary-clk+ (binary-clk+ i j) k)
 
408
         (binary-clk+ i (binary-clk+ j k))))
 
409
 
 
410
(defmacro clk+ (&rest argst)
 
411
  (if (endp argst)
 
412
      0
 
413
      (if (endp (cdr argst))
 
414
          (car argst)
 
415
          `(binary-clk+ ,(car argst)
 
416
                         (clk+ ,@(cdr argst))))))
 
417
 
 
418
(defthm m1-clk+
 
419
  (equal (m1 s (clk+ i j))
 
420
         (m1 (m1 s i) j)))
 
421
 
 
422
(in-theory (disable binary-clk+))
 
423
 
 
424
(defthm m1-opener
 
425
  (and (equal (m1 s 0) s)
 
426
       (implies (natp i)
 
427
                (equal (m1 s (+ 1 i))
 
428
                       (m1 (step s) i)))))
 
429
 
 
430
(in-theory (disable m1))
 
431
 
 
432
; Nth and update-nth
 
433
 
 
434
 
 
435
 
 
436
 
 
437
; Len and the Locals
 
438
 
 
439
; In our code proofs we need this theorem to prove that certain initial states
 
440
; satisfy the good-statep predicate.
 
441
 
 
442
(defthm equal-len-0
 
443
  (equal (equal (len x) 0)
 
444
         (not (consp x))))