#||
Like m1 but uses a stobj for the state.
I totally ignore the guard question.
(defpkg "M1"
(set-difference-eq (union-eq *acl2-exports*
*common-lisp-symbols-from-main-lisp-package*)
'(push pop pc program step
; nth update-nth nth-update-nth ; <--- stobjs use built-ins
)))
(certify-book "m1-with-stobj" 1)
||#
(in-package "M1")
; -----------------------------------------------------------------
; Stack Manipulation
(defun push (x y)
(cons x y))
(defun top (stack)
(car stack))
(defun pop (stack)
(cdr stack))
; -----------------------------------------------------------------
; State Manipulation:
(set-verify-guards-eagerness 0)
; I name the components with the prefix "ugly-" because I don't want to see
; them in proofs! I'm going to define a more uniform interface. If I see
; ``ugly-'' in a proof, something is wrong!
(defstobj s ugly-pc ugly-locals ugly-stack ugly-program)
; Basic read/write operations on state: for each field f of a stobj, defstobj
; provides two functions, f and update-f, for accessing and updating the field
; value. Now think about how messy it is to normalize a random mix of update
; expressions, e.g., (update-h a (update-g b (update-h c (update-f d st)))).
; One needs a quadradic number of rules to commute the updates into some canonical order:
; (update-g a (update-f b s)) = (update-f b (update-g a s))
; (update-h a (update-f b s)) = (update-f b (update-h a s))
; (update-i a (update-f b s)) = (update-f b (update-i a s))
; ...
; (update-h a (update-g b s)) = (update-g b (update-h a s))
; (update-i a (update-g b s)) = (update-g b (update-i a s))
; ...
; So I define a pair of read/write functions that can hit any field of the
; stobj, then I prove the normalization rules, then I disable these basic
; functions. Finally, I use the basic functions to define the field-specific
; update-f versions. I define how to write to the cd field even though it is
; never needed. I did this to provide a uniform interface: to access or change
; a field, use rd or wr.
(defun wr (key v s)
(declare (xargs :stobjs (s)))
(case key
(:pc (update-ugly-pc v s))
(:locals (update-ugly-locals v s))
(:stack (update-ugly-stack v s))
(:program (update-ugly-program v s))
(otherwise s)))
(defun rd (key s)
(declare (xargs :stobjs (s)))
(case key
(:pc (ugly-pc s))
(:locals (ugly-locals s))
(:stack (ugly-stack s))
(:program (ugly-program s))
(otherwise 0)))
(defthm sp-wr
(implies (sp s)
(sp (wr loc val s))))
(in-theory (disable sp))
(defun keyp (k) (member k '(:pc :locals :stack :program)))
(defthm rd-wr
(equal (rd key1 (wr key2 v s))
(if (and (equal key1 key2)
(keyp key1))
v
(rd key1 s))))
(defthm update-nth-update-nth-diff
(implies (and (natp i) (natp j) (not (equal i j)))
(equal (update-nth i v (update-nth j w list))
(update-nth j w (update-nth i v list))))
:rule-classes ((:rewrite :loop-stopper ((i j update-nth)))))
(defthm update-nth-update-nth-same
(equal (update-nth i v (update-nth i w list))
(update-nth i v list)))
(defthm update-nth-redundant
(implies (and (natp i)
(< i (len x))
(equal (nth i x) v))
(equal (update-nth i v x) x)))
(defthm wr-wr-diff
(implies (and (keyp key1)
(keyp key2)
(not (equal key1 key2)))
(equal (wr key1 v1 (wr key2 v2 s))
(wr key2 v2 (wr key1 v1 s))))
:hints (("Goal" :in-theory (disable nth update-nth)))
:rule-classes ((:rewrite :loop-stopper ((key1 key2 wr)))))
(defthm wr-wr-same
(implies (keyp key1)
(equal (wr key1 v1 (wr key1 v2 s))
(wr key1 v1 s))))
(defthm wr-redundant
(implies (and (sp s)
(equal (rd key s) v))
(equal (wr key v s) s))
:hints (("Goal" :in-theory (enable sp))))
(in-theory (disable rd wr))
; The following functions are just handy abbreviations to use in the semantics
; of the instructions. I expect them always to be expanded into rd/wr terms.
; They could be macros.
(defun pc (s)
(declare (xargs :stobjs (s)))
(rd :pc s))
(defun !pc (v s)
(declare (xargs :stobjs (s)))
(wr :pc v s))
; There is no need to define lo and !lo since we always change indexed
; positions, not the whole field.
(defun loi (i s)
(declare (xargs :stobjs (s)))
(nth i (rd :locals s)))
(defun !loi (i v s)
(declare (xargs :stobjs (s)))
(wr :locals (update-nth i v (rd :locals s)) s))
(defun stack (s)
(declare (xargs :stobjs (s)))
(rd :stack s))
(defun !stack (v s)
(declare (xargs :stobjs (s)))
(wr :stack v s))
; There is no need to define !program.
(defun program (s)
(declare (xargs :stobjs (s)))
(rd :program s))
(defun next-inst (s)
(declare (xargs :stobjs (s)))
(nth (pc s) (program s)))
; -----------------------------------------------------------------
; Instruction Accessors
(defun op-code (inst)
(nth 0 inst))
(defun arg1 (inst)
(nth 1 inst))
; -----------------------------------------------------------------
; The M1 Machine
; Now we define the semantics of each instruction. These functions are called
; ``semantic functions.''
; Each opcode will be given semantics with an ACL2 function that takes an
; instruction (with the given opcode) and a state and returns the state
; produced by executing the instruction. For example, the ILOAD instruction,
; which looks like this (ILOAD k), where k is the index of the local variable
; to be loaded, is given semantics by the function execute-ILOAD. Execute-ILOAD is
; the ``semantic function'' for ILOAD.
; Our expectation when (execute-ILOAD inst s) is called is that s is a ``good''
; M1 state, that inst is the next instruction in s, and that inst is an ILOAD
; instruction. If all that is true, we can run execute-ILOAD without error,
; i.e., without worrying whether the instruction is well-formed, whether the
; local variable of that index exists, whether incrementing the pc pushes it
; outside the bounds of the program, etc. Because we have analogous
; expectations on the semantic function for each opcode, we wrap up these
; expectations into a single predicate:
; Semantics of (ILOAD k): increment the pc and push onto the stack the value of
; the kth local. Aside: We will know, by guard verification, that the new pc
; is legal and that the value pushed is a rational number. As a rule, I will
; not comment here on everything we know by guard verification, I'm just trying
; to give you a sense of the implications of our expectations.
(defun execute-ILOAD (inst s)
(declare (xargs :stobjs (s)))
(let* ((s (!stack (push (loi (arg1 inst) s) (stack s))
s))
(s (!pc (+ 1 (pc s)) s)))
s))
; Semantics of (ICONST k): increment the pc and push k onto the stack.
(defun execute-ICONST (inst s)
(declare (xargs :stobjs (s)))
(let* ((s (!stack (push (arg1 inst) (stack s))
s))
(s (!pc (+ 1 (pc s)) s)))
s))
; Semantics of (IADD): increment the pc, pop two items off the stack and push
; their sum. Aside: We will know, by guard verification, that there are at
; least two items on the stack and that they are both rational numbers.
(defun execute-IADD (inst s)
(declare (xargs :stobjs (s))
(ignore inst))
(let ((u (top (stack s)))
(v (top (pop (stack s))))
(stack1 (pop (pop (stack s)))))
(let* ((s (!stack (push (+ v u) stack1) s))
(s (!pc (+ 1 (pc s)) s)))
s)))
; Semantics of (ISUB): increment the pc, pop two items off the stack and push
; their difference.
(defun execute-ISUB (inst s)
(declare (xargs :stobjs (s))
(ignore inst))
(let ((u (top (stack s)))
(v (top (pop (stack s))))
(stack1 (pop (pop (stack s)))))
(let* ((s (!stack (push (- v u) stack1) s))
(s (!pc (+ 1 (pc s)) s)))
s)))
; Semantics of (IMUL): increment the ic, pop two items off the stack and push
; their product.
(defun execute-IMUL (inst s)
(declare (xargs :stobjs (s))
(ignore inst))
(let ((u (top (stack s)))
(v (top (pop (stack s))))
(stack1 (pop (pop (stack s)))))
(let* ((s (!stack (push (* v u) stack1) s))
(s (!pc (+ 1 (pc s)) s)))
s)))
; Semantics of (ISTORE k): increment the ic, pop one item off the stack, and
; store it as the value of local variable k.
(defun execute-ISTORE (inst s)
(declare (xargs :stobjs (s)))
(let ((u (top (stack s)))
(stack1 (pop (stack s))))
(let* ((s (!stack stack1 s))
(s (!loi (arg1 inst) u s))
(s (!pc (+ 1 (pc s)) s)))
s)))
; Semantics of (GOTO k): increment the pc by k. Aside: We will know, by guard
; verification, that the new pc is legal.
(defun execute-GOTO (inst s)
(declare (xargs :stobjs (s)))
(let* ((s (!pc (+ (arg1 inst) (pc s)) s)))
s))
; Semantics of (IFEQ k): pop one item off the stack and increment the pc k if
; that item is 0 and by 1 if if is non-0. Aside: We will know, by guard
; verification, that the new pc is legal.
(defun execute-IFEQ (inst s)
(declare (xargs :stobjs (s)))
(let ((u (top (stack s)))
(stack1 (pop (stack s))))
(let* ((s (!stack stack1 s))
(s (!pc (if (equal u 0)
(+ (arg1 inst) (pc s))
(+ 1 (pc s)))
s)))
s)))
(defun do-inst (inst s)
(declare (xargs :stobjs (s)))
(if (equal (op-code inst) 'ILOAD)
(execute-ILOAD inst s)
(if (equal (op-code inst) 'ICONST)
(execute-ICONST inst s)
(if (equal (op-code inst) 'IADD)
(execute-IADD inst s)
(if (equal (op-code inst) 'ISUB)
(execute-ISUB inst s)
(if (equal (op-code inst) 'IMUL)
(execute-IMUL inst s)
(if (equal (op-code inst) 'ISTORE)
(execute-ISTORE inst s)
(if (equal (op-code inst) 'GOTO)
(execute-GOTO inst s)
(if (equal (op-code inst) 'IFEQ)
(execute-IFEQ inst s)
s)))))))))
; This is the single-step function: it executes the next instruction in a
; state. Aside: We will know, by guard verification, that the resulting state
; is a good state.
(defun step (s)
(declare (xargs :stobjs (s)))
(do-inst (next-inst s) s))
(defun m1 (s n)
(declare (xargs :stobjs (s)))
(if (zp n)
s
(let* ((s (step s)))
(m1 s (- n 1)))))
(defun haltedp (s)
(declare (xargs :stobjs (s)))
(equal (next-inst s) '(HALT)))
; =================================================================
; Lemmas for Proving M1 Code
; Arithmetic
(include-book "arithmetic-5/top" :dir :system)
; Stacks
(defthm top-push
(equal (top (push x y)) x))
(defthm pop-push
(equal (pop (push x y)) y))
(defun popn (n stk)
(if (zp n)
stk
(popn (- n 1) (pop stk))))
(defmacro push* (&rest lst)
(if (endp lst)
nil
(if (endp (cdr lst))
(car lst)
`(push ,(car lst) (push* ,@(cdr lst))))))
(defthm len-push
(equal (len (push x y))
(+ 1 (len y))))
; Abstract Data Type Stuff
(defthm constant-stacks
(and
; These next two are needed because some push expressions evaluate to
; list constants, e.g., (push 1 (push 2 nil)) becomes '(1 2) and '(1
; 2) pattern-matches with (cons x s) but not with (push x s).
(equal (top (cons x s)) x)
(equal (pop (cons x s)) s))
:hints (("Goal" :in-theory (enable top pop))))
(in-theory (disable push (:executable-counterpart push) top pop))
; Step Stuff
(defthm step-opener
(implies (consp (next-inst s))
(equal (step s)
(do-inst (next-inst s) s)))
:hints (("Goal" :in-theory (enable step))))
(in-theory (disable step))
; Schedules and Run
(defun binary-clk+ (i j)
(+ (nfix i) (nfix j)))
(defthm clk+-associative
(equal (binary-clk+ (binary-clk+ i j) k)
(binary-clk+ i (binary-clk+ j k))))
(defmacro clk+ (&rest argst)
(if (endp argst)
0
(if (endp (cdr argst))
(car argst)
`(binary-clk+ ,(car argst)
(clk+ ,@(cdr argst))))))
(defthm m1-clk+
(equal (m1 s (clk+ i j))
(m1 (m1 s i) j)))
(in-theory (disable binary-clk+))
(defthm m1-opener
(and (equal (m1 s 0) s)
(implies (natp i)
(equal (m1 s (+ 1 i))
(m1 (step s) i)))))
(in-theory (disable m1))
; Nth and update-nth
; Len and the Locals
; In our code proofs we need this theorem to prove that certain initial states
; satisfy the good-statep predicate.
(defthm equal-len-0
(equal (equal (len x) 0)
(not (consp x))))