; JVM Problem Set 3
; Copyright (C) 2004  J Strother Moore,
;               University of Texas at Austin

; This program is free software; you can redistribute it and/or 
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free 
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

; Written by: J Strother Moore
; email:      Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

; Modified by: John Cowles
; email:       cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
;=============================================================
; In this problem set you will be asked to elaborate the 
; operational semantics for the m0 virtual machine.  

; To do this problem set you should first copy it to a directory
; where you have write permission.  Connect to that directory and
; fire up ACL2 (so that the connected book directory is the
; directory where this file resides).  Then execute each of the
; events below, in the order indicated.

; When you get to a comment labeled ``Problem'' you will see some
; ``blanks'' (written ``***'') in the event.  You should edit
; your copy of this file, replacing ``***'' by one or more
; expressions as appropriate. Then execute the form and continue.

; When you are all done you can check your work by saving the
; edited file to your directory, then do

; ACL2 !>:ubt! 1

; to erase the ACL2 database and then

; ACL2 !>(ld "hw5.lisp" :ld-pre-eval-print t)

; to process every form in the edited file, printing each before
; evaluation.

; Note:  When ld terminates, either because of an error or because
; of successful completion, the current package will be restored 
; to what it was when ld was invoked.  That will probably be the
; ACL2 package and you will probably want it to be the M0 package,
; if you want to play with M0.  So when the ld is done, select the
; M0 package as current with:

; ACL2 !>(in-package "M0") 

; ---------------------------------------------------------------------------
; Prolog

; Think of the next two events as a prolog that just set the 
; stage: we'll be working in a symbol package in which certain
; symbols, e.g., PC, PROGRAM, PUSH, etc., are undefined.

(defpkg "M0"
  (set-difference-equal
   (union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP
                           QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<)
             (union-eq *acl2-exports*
                       *common-lisp-symbols-from-main-lisp-package*))
   '(PC PROGRAM PUSH POP REVERSE STEP ++)))

(in-package "M0")

; ---------------------------------------------------------------------------
; Abstract Machine 0

; Utilities

(defun push (obj stack) (cons obj stack))
(defun top (stack) (car stack))
(defun pop (stack) (cdr stack))

(defun bound? (x alist) (assoc-equal x alist))

(defun bind (x y alist)
  (cond ((endp alist) (list (cons x y)))
        ((equal x (car (car alist)))
         (cons (cons x y) (cdr alist)))
        (t (cons (car alist) (bind x y (cdr alist))))))

(defun binding (x alist) (cdr (assoc-equal x alist)))

(defun op-code (inst) (car inst))
(defun arg1 (inst) (car (cdr inst)))
(defun arg2 (inst) (car (cdr (cdr inst))))
(defun arg3 (inst) (car (cdr (cdr (cdr inst)))))

; The Core of M0

(defun make-state (pc locals stack program)
  (list pc locals stack program))
(defun pc (s) (car s))
(defun locals (s) (cadr s))
(defun stack (s) (caddr s))
(defun program (s) (cadddr s))
(defun next-inst (s) (nth (pc s) (program s)))

(defun suppliedp (key args)
  (cond ((endp args) nil)
        ((equal key (car args)) t)
        (t (suppliedp key (cdr args)))))

(defun actual (key args)
  (cond ((endp args) nil)
        ((equal key (car args)) (cadr args))
        (t (actual key (cdr args)))))

(defmacro modify (s &rest args)
  (list 'make-state
        (if (suppliedp :pc args)
            (actual :pc args)
          (list 'pc s))
        (if (suppliedp :locals args)
            (actual :locals args)
          (list 'locals s))
        (if (suppliedp :stack args)
            (actual :stack args)
          (list 'stack s))
        (if (suppliedp :program args)
            (actual :program args)
          (list 'program s))))

; We now informally specify and then define each m0 instruction.

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (PUSH c)
; Push the constant c onto the operand stack.

(defun execute-PUSH (inst s)
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (arg1 inst) (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
; Informal Spec: (POP)
; Pop the top item off the operand stack and discard it.

; Problem 3.1
(defun execute-POP (inst s)
  (declare (ignore inst))
  ***)

; Note: When you define an ACL2 function that ignores one of its
; arguments you must declare that you are doing it intentionally.
; That is the purpose of the DECLARE form above.  Why does 
; execute-POP ignore inst?  The reason is that, by convention 
; here, we know that inst is an instruction whose opcode is POP.
; Since the POP instruction contains no additional fields, there 
; is nothing else we need from it.

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (LOAD v)
; Push the contents stored in local variable v onto the operand 
; stack.

(defun execute-LOAD (inst s)
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (binding (arg1 inst)
                                (locals s))
                       (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (STORE v)
; Pop the top item off the operand stack and store it into the
; local variable v.

; Problem 3.2
(defun execute-STORE (inst s)
  ***)

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
; Informal Spec: (DUP)
; Duplicate the top item on the stack.

; Problem 3.3
(defun execute-DUP (inst s)
  ***)

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (ADD)
; Pop the top two items off the stack and push their sum.

(defun execute-ADD (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (+ (top (pop (stack s)))
                          (top (stack s)))
                       (pop (pop (stack s))))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (SUB)
; Pop the top two items off the stack and push their difference.
; (The top item should be subtracted from the one below it.)

; Problem 3.4
(defun execute-SUB (inst s)
  ***)

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (MUL)
; Pop the top two items off the stack and push their product.

; Problem 3.5
(defun execute-MUL (inst s)
  ***)

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (GOTO delta)
; Jump to the instruction delta steps from the current 
; instruction. Here one step = one instruction.

; Problem 3.6
(defun execute-GOTO (inst s)
  ***)

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (IFEQ delta)
; Pop the top item off the stack and if it is 0, jump to the 
; instruction delta steps from the current instruction; otherwise,
; step to the next instruction.

; Problem 3.7
(defun execute-IFEQ (inst s)
  ***)

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (IFNE delta)
; Pop the top item off the stack and if it is not 0, jump to the
; instruction delta steps from the current instruction; otherwise,
; step to the next instruction.

; Problem 3.8
(defun execute-IFNE (inst s)
  ***)

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (IFGT delta)
; Pop the top item off the stack and if it is greater than 0, jump
; to the instruction delta steps from the current instruction;
; otherwise, step to the next instruction.

; Problem 3.9
(defun execute-IFGT (inst s)
  ***)

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (IFLE delta)
; Pop the top item off the stack and if it is less than or equal
; to 0, jump to the instruction delta steps from the current
; instruction; otherwise, step to the next instruction.

; Problem 3.10
(defun execute-IFLE (inst s)
  ***)

; ---------------------------------------------------------------

; Now we wrap it all up by defining the m0 step function and the
; top-level interpreter.

(defun do-inst (inst s)
  (case (op-code inst)
    (PUSH   (execute-PUSH  inst s))
    (POP    (execute-POP   inst s))
    (LOAD   (execute-LOAD  inst s))
    (STORE  (execute-STORE inst s))
    (DUP    (execute-DUP   inst s))
    (ADD    (execute-ADD   inst s))
    (SUB    (execute-SUB   inst s))
    (MUL    (execute-MUL   inst s))
    (GOTO   (execute-GOTO  inst s))
    (IFEQ   (execute-IFEQ  inst s))
    (IFNE   (execute-IFNE  inst s))
    (IFGT   (execute-IFGT  inst s))
    (IFLE   (execute-IFLE  inst s))
    (otherwise s)))

; Notice that there is no instruction with op-code HALT.  But
; what is (do-inst '(HALT) s)?  The answer: s!  That is, every
; undefined op-code is a no-op, and a no-op is the same as a halt
; instruction in the sense that execution never gets past it.

(defun step (s)
  (do-inst (next-inst s) s))

; So here is the operational semantics for the m0 virtual machine.

(defun run (s n)
  (if (zp n)
      s
    (run (step s) (- n 1))))

; Note: n gives the number of instrutions to execute.

; ---------------------------------------------------------------------------
; Some Simple Programming Problems

; The following event defines the constant *simple* to be an m0
; program.

(defconst *simple-program*
  '((LOAD x)
    (LOAD y)
    (ADD)
    (STORE z)
    (HALT)))

; Convention: It is my convention to put a (HALT) instruction at
; the end of every m0 program I write, simply to make it clear 
; that I'm done when I get there.  When I step the machine through
; a program I always have the choice: do I count the final HALT 
; instruction or not?  I make the convention not to count it. The
; reason is that executing the HALT is a no-op, i.e., there is no
; way to tell whether I executed it or not.  Thus, if I decided 
; to include the execution of the HALT, then I might as well 
; decide to execute the HALT twenty-seven times.  So I decided I
; will arrange to take execution to the HALT but not to
; execute it.

#|----------------------------------------------------------
Observe the results when the following is executed in ACL2.

(modify nil
	:pc      0
	:program *simple-program*
	:locals  (list (cons 'x 10)(cons 'y 11)(cons 'z 12))
	:stack   nil)

(run (modify nil
	     :pc      0
	     :program *simple-program*
	     :locals  (list (cons 'x 10)(cons 'y 11)(cons 'z 12))
	     :stack   nil)
     1)

(run (modify nil
	     :pc      0
	     :program *simple-program*
	     :locals  (list (cons 'x 10)(cons 'y 11)(cons 'z 12))
	     :stack   nil)
     2)

(run (modify nil
	     :pc      0
	     :program *simple-program*
	     :locals  (list (cons 'x 10)(cons 'y 11)(cons 'z 12))
	     :stack   nil)
     3)

(run (modify nil
	     :pc      0
	     :program *simple-program*
	     :locals  (list (cons 'x 10)(cons 'y 11)(cons 'z 12))
	     :stack   nil)
     4)

(run (modify nil
	     :pc      0
	     :program *simple-program*
	     :locals  (list (cons 'x 10)(cons 'y 11)(cons 'z 12))
	     :stack   nil)
     5)
----------------------------------------------------------------
|#
; The next theorem tells ACL2 whenever the number of instrutions
; to execute is given as an actual positive integer constant,
; then use the definition of run to execute m0 one step.

(defthm
  run-pos-constant-steps
  (implies (and (syntaxp (quotep n))
		(integerp n)
		(> n 0))
	   (equal (run s n)
		  (run (step s)(- n 1)))))

; Problem 3.11
; Fill in the blanks below to make the following a theorem.  This
; theorem may be thought of as a specification for the program
; *simple-program*, that characterizes what it does and how long
; it takes.

(defthm simple-program-is-correct
  (equal (run (modify nil
                      :pc      0
                      :program *simple-program*
                      :locals  (list (cons 'x i)
				     (cons 'y j)
				     (cons 'z k))
                      :stack   stk)
	       ***)
         (modify nil
                 :pc      ***
                 :program *simple-program*
                 :locals  ***
                 :stack   ***)))

; Problem 3.12
; Define the constant *sum-squares-program* to be an m0 program
; that sums the squares of the two local variables, A and B, and
; leaves the result on top of the stack.  The program should have
; no other effect on the state.  See Problem 3.13 for a formal
; specification.

(defconst *sum-squares-program*
  '(***))

(defun sq (x) (* x x))

; Problem 3.13
; Fill in the blanks below with the number of steps it takes to
; execute your *sum-squares-program* so that the following is a
; theorem.

(defthm sum-squares-program-is-correct
  (equal (run (modify nil
                      :pc      0
                      :program *sum-squares-program*
                      :locals  locals
                      :stack   stk)
	      ***)
         (modify nil
                 :pc      ***
                 :program *sum-squares-program*
                 :locals  locals
                 :stack   (push (+ (sq (binding 'A locals))
                                   (sq (binding 'B locals)))
                                stk))))

; Problem 3.14
; Define *fact-program* to be an m0 program that computes the
; factorial of the local variable, n, provided its value is a
; natural number, and leaves the result on the stack. 
; The program should have only one local.

(defconst *fact-program*
  '(***))

; Problem 3.15
; Count how many instructions it takes to execute your 
; *fact-program* on 5 and then fill in the blank below with that
; constant to see whether your program computes 120 in that many
; steps.

(defthm fact-program-on-5
  (equal (top (stack (run (modify nil
                                  :pc      0
                                  :program *fact-program*
                                  :locals  (list (cons 'n 5))
                                  :stack   nil)
			  ***)))
         120))