#|
This file corresponds to the paper

Mechanized Formal Reasoning about Programs and Computing Machines

by Robert S. Boyer and J Strother Moore



To certify this book, start ACL2, execute the following three forms,

(defpkg "SMALL-MACHINE"
  (union-eq
   (delete1-eq 'pc
	       (delete1-eq 'state *acl2-exports*))
   (append '(true-listp zp nfix fix len quotep defevaluator syntaxp)
           (delete1-eq 'pi
		       (delete1-eq 'step
				   *common-lisp-symbols-from-main-lisp-package*)))))

(certify-book "small-machine" 1)


Boyer and Moore

|#

(in-package "SMALL-MACHINE")

; We define all this in a different package because STEP (at least) is a
; function defined in the LISP package and ACL2 does not permit us to redefine
; it.

; Now we start the development of the small machine.

(defun statep (x)
  (and (true-listp x)
       (equal (len x) 5)))

(defun state (pc stk mem halt code) (list pc stk mem halt code))

(defun pc (s) (nth 0 s))
(defun stk (s) (nth 1 s))
(defun mem (s) (nth 2 s))
(defun halt (s) (nth 3 s))
(defun code (s) (nth 4 s))

(defmacro modify (s &key (pc '0 pcp)
                    (stk 'nil stkp)
                    (mem 'nil memp)
                    (halt 'nil haltp)
                    (code 'nil codep))
  `(state ,(if pcp pc `(pc ,s))
          ,(if stkp stk `(stk ,s))
          ,(if memp mem `(mem ,s))
          ,(if haltp halt `(halt ,s))
          ,(if codep code `(code ,s))))

(defmacro st (&rest args)
  `(modify nil ,@args))

; Utility Functions

(defun pc+1 (pc)
  (cons (car pc) (+ 1 (cdr pc))))

(defun put (n v mem)
  (if (zp n)
      (cons v (cdr mem))
      (cons (car mem) (put (1- n) v (cdr mem)))))

(defun fetch (pc code)
  (nth (cdr pc)
       (cdr (assoc (car pc) code))))

(defun current-instruction (s)
  (fetch (pc s) (code s)))

(defun opcode (ins) (nth 0 ins))
(defun a (ins) (nth 1 ins))
(defun b (ins) (nth 2 ins))

; The Semantics of Individual Instructions

; Move Instructions

(defun move (a b s)
  (modify s
          :pc (pc+1 (pc s))
          :mem (put a (nth b (mem s)) (mem s))))

(defun movi (a b s)
  (modify s
          :pc (pc+1 (pc s))
          :mem (put a b (mem s))))

; Arithmetic Instructions

(defun add (a b s)
  (modify s
          :pc (pc+1 (pc s))
          :mem (put a
                    (+ (nth a (mem s))
                       (nth b (mem s)))
                    (mem s))))

(defun subi (a b s)
  (modify s
          :pc (pc+1 (pc s))
          :mem (put a
                    (- (nth a (mem s)) b)
                    (mem s))))

; Jump Instructions

(defun jumpz (a b s)
  (modify s
          :pc (if (zp (nth a (mem s)))
                    (cons (car (pc s)) b)
                  (pc+1 (pc s)))))

(defun jump (a s)
  (modify s :pc (cons (car (pc s)) a)))

; Subroutine Call and Return

(defun call (a s)
  (modify s
          :pc (cons a 0)
          :stk (cons (pc+1 (pc s)) (stk s))))

(defun ret (s)
  (if (endp (stk s))
      (modify s :halt t)
      (modify s
              :pc (car (stk s))
              :stk (cdr (stk s)))))

; One can imagine adding new instructions.

; The Interpreter

(defun execute (ins s)
  (let ((op (opcode ins))
        (a (a ins))
        (b (b ins)))
    (case op
          (move  (move a b s))
          (movi  (movi a b s))
          (add   (add a b s))
          (subi  (subi a b s))
          (jumpz (jumpz a b s))
          (jump  (jump a s))
          (call  (call a s))
          (ret   (ret s))
          (otherwise s))))

(defun step (s)
  (if (halt s)
      s
      (execute (current-instruction s) s)))

(defun sm (s n)
  (if (zp n)
      s
      (sm (step s) (+ n -1))))