#|
This file corresponds to the paper

                Symbolic Simulation:  An ACL2 Approach
                                  by
                           J Strother Moore

It is also compatible with the paper

  Mechanized Formal Reasoning about Programs and Computing Machines
                                  by
                 Robert S. Boyer and J Strother Moore

The machine model here is Common Lisp compliant, whereas the model in
the latter paper above is not.  In order to make it compliant I had to
enforce the guard that memory contains integers.  This changed the
definition of put so that it puts 0's instead of nil's when asked to
put beyond the end of currently represented memory.  I also changed
the semantics of the instruction set a little (e.g., JUMPZ used to
jump if its tested argument was less than or equal to 0 and now it
jumps if the argument is equal to 0).  But every theorem mentioned in
the latter paper has an analogue here and no real violence was done to
the general method discussed in that paper.

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

:set-cbd "/...this directory.../"

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

(certify-book "small-machine" 1)

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.

; We start with the a description of the type system we will use.

(defun natp (n)
  (declare (xargs :guard t))
  (and (integerp n)
       (<= 0 n)))

(defun pcp (pc)
  (declare (xargs :guard t))
  (and (consp pc)
       (symbolp (car pc))
       (natp (cdr pc))))

(defun stkp (stk)
  (declare (xargs :guard t))
  (if (atom stk)
      (equal stk nil)
    (and (pcp (car stk))
         (stkp (cdr stk)))))

(defthm stkp-forward-to-true-listp
  (implies (stkp stk) (true-listp stk))
  :rule-classes :forward-chaining)

(defun memp (mem)
  (declare (xargs :guard t))
  (if (atom mem)
      (equal mem nil)
    (and (integerp (car mem))
         (memp (cdr mem)))))

(defthm memp-forward-to-true-listp
  (implies (memp mem) (true-listp mem))
  :rule-classes :forward-chaining)

(defun movep (a b)
  (declare (xargs :guard t))
  (and (natp a)
       (natp b)))

(defun movip (a b)
  (declare (xargs :guard t))
  (and (natp a)
       (natp b)))

(defun addp (a b)
  (declare (xargs :guard t))
  (and (natp a)
       (natp b)))

(defun subip (a b)
  (declare (xargs :guard t))
  (and (natp a)
       (natp b)))

(defun jumpzp (a b)
  (declare (xargs :guard t))
  (and (natp a)
       (natp b)))

(defun jumpp (a)
  (declare (xargs :guard t))
  (natp a))

(defun callp (a)
  (declare (xargs :guard t))
  (symbolp a))

(defun retp ()
  (declare (xargs :guard t))
  t)

(defun insp (ins)
  (declare (xargs :guard t))
  (and (consp ins)
       (symbolp (car ins))
       (true-listp (cdr ins))
       (let ((a (nth 1 ins))
             (b (nth 2 ins)))
         (case (car ins)
           (move  (movep a b))
           (movi  (movip a b))
           (add   (addp a b))
           (subi  (subip a b))
           (jumpz (jumpzp a b))
           (jump  (jumpp a))
           (call  (callp a))
           (ret   (retp))
           (otherwise nil)))))
         
(defun instructionsp (lst)
  (declare (xargs :guard t))
  (if (atom lst)
      (equal lst nil)
    (and (insp (car lst))
         (instructionsp (cdr lst)))))

(defthm instrunctionsp-forward-to-true-listp
  (implies (instructionsp lst)
           (true-listp lst))
  :rule-classes :forward-chaining)

(defun programp (prog)
  (declare (xargs :guard t))
  (and (consp prog)
       (symbolp (car prog))
       (instructionsp (cdr prog))))

(defun codep (code)
  (declare (xargs :guard t))
  (if (atom code)
      (equal code nil)
    (and (programp (car code))
         (codep (cdr code)))))

(defthm codep-forward-to-symbol-alistp
  (implies (codep code)
           (symbol-alistp code))
  :rule-classes :forward-chaining)

(defun pc (s)   (declare (xargs :guard (true-listp s))) (nth 0 s))
(defun stk (s)  (declare (xargs :guard (true-listp s))) (nth 1 s))
(defun mem (s)  (declare (xargs :guard (true-listp s))) (nth 2 s))
(defun halt (s) (declare (xargs :guard (true-listp s))) (nth 3 s))
(defun code (s) (declare (xargs :guard (true-listp s))) (nth 4 s))

(defun statep (x)
  (declare (xargs :guard t))
  (and (true-listp x)
       (equal (len x) 5)
       (pcp (pc x))
       (stkp (stk x))
       (memp (mem x))
       (codep (code x))))

(defun state (pc stk mem halt code)
  (declare (xargs :guard (and (pcp pc)
                              (stkp stk)
                              (memp mem)
                              (codep code))))
  (list pc stk mem halt code))

(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)
  (declare (xargs :guard (pcp pc)))
  (cons (car pc) (+ 1 (cdr pc))))

; If we knew n were a legal address, i.e., n < (len mem), in the guard
; for get below, we could remove the nfix.  The nfix is necessary if
; we want the invariant that get produces a nat.

; Unfortunately, to enforce the legal address requirement would
; require changing the definition of a legal instruction, since
; instructions can contain arbitrary addresses.  That would require
; passing into the insp predicate the memory size and proving theorems
; about how memory doesn't shrink.  Rather than do that, I have just
; accessed memory in a way that guarantees it always returns a nat.

(defun get (n mem)
  (declare (xargs :guard
                  (and (natp n)
                       (true-listp mem))))
  (if (zp n)
      (if (null mem) 0 (car mem))
    (get (- n 1) (cdr mem))))

(defun put (n v mem)
  (declare (xargs :guard (and (natp n)
                              (true-listp mem))))
  (if (zp n)
      (cons v (cdr mem))
    (cons (if (null mem) 0 (car mem))
          (put (1- n) v (cdr mem)))))

(defun fetch (pc code)
  (declare (xargs :guard (and (pcp pc)
                              (codep code))))
  (nth (cdr pc)
       (cdr (assoc-eq (car pc) code))))

(defun current-instruction (s)
  (declare (xargs :guard (statep s)))
  (fetch (pc s) (code s)))

; It is convenient if we define opcode, a and b, below, so that they
; can operate on non-instructions.  This way, we don't have to prove
; that the pc always points to an instruction and that calls always
; name procedures defined in the code.  We dealt with issues like this
; in Piton, where we guaranteed we never "fell off" the end of a
; program, etc.  But it requires making the notion of a legal
; instruction sensitive to the entire code segment.

(defun opcode (ins)
  (declare (xargs :guard (true-listp ins)))
  (nth 0 ins))

(defun a (ins)
  (declare (xargs :guard (true-listp ins)))
  (nth 1 ins))

(defun b (ins)
  (declare (xargs :guard (true-listp ins)))
  (nth 2 ins))

; A Few Important Guard Lemmas



(defthm memp-put
  (implies (and (force (integerp v))
                (force (memp mem)))
           (memp (put n v mem))))
                
(defthm integerp-get
  (implies (force (memp mem))
           (integerp (get n mem)))
  :rule-classes :type-prescription)

; The Semantics of Individual Instructions

; Move Instructions

(defun move (a b s)
  (declare (xargs :guard (and (movep a b)
                              (statep s))))
  (modify s
          :pc (pc+1 (pc s))
          :mem (put a (get b (mem s)) (mem s))))

(defthm statep-move
  (implies (and (statep s)
                (movep a b))
           (statep (move a b s))))

(defun movi (a b s)
  (declare (xargs :guard (and (movip a b)
                              (statep s))))
  (modify s
          :pc (pc+1 (pc s))
          :mem (put a b (mem s))))

(defthm statep-movip
  (implies (and (movip a b)
                (statep s))
           (statep (movi a b s))))

; Arithmetic Instructions

(defun add (a b s)
  (declare (xargs :guard (and (addp a b)
                              (statep s))))
  (modify s
          :pc (pc+1 (pc s))
          :mem (put a
                    (+ (get a (mem s))
                       (get b (mem s)))
                    (mem s))))

(defthm statep-add
  (implies (and (addp a b)
                (statep s))
           (statep (add a b s))))

(defun subi (a b s)
  (declare (xargs :guard (and (subip a b)
                              (statep s))))

; This instructions decrements the contents of mem location a by b.
; We have to insure that the new contents is still a natural number.
; We could do this in one of two ways.  We could test that and raise
; an exception at runtime if it is not, or we could test it and coerce
; it to zero at runtime.  We choose the latter.  Note that both
; alternatives involve runtime tests.

; We could put this test into the guard.  It would then be
; ``syntactically'' illegal to execute a subi instruction on certain
; states.  This would impossibly complicate guard verification.  How,
; for example, would we prove that run satisfied it guards?  We would
; have to characterize those states that could run without a subi
; guard violation.  Our decision to insist that memory contains
; naturals but then to provide an operation that does not always
; produce naturals is akin to the provision of a div instruction in a
; machine.  Something must be done about division by 0 and the only
; "sane" thing to do involves a runtime test that the divisor is not 0
; and some sort of defined behavior when it is not.

  (modify s
          :pc (pc+1 (pc s))
          :mem (put a
                    (- (get a (mem s)) b)
                    (mem s))))

(defthm statep-subi
  (implies (and (subip a b)
                (statep s))
           (statep (subi a b s))))

; Jump Instructions

(defun jumpz (a b s)
  (declare (xargs :guard (and (jumpzp a b)
                              (statep s))))
  (modify s
          :pc (if (zerop (get a (mem s)))
                  (cons (car (pc s)) b)
                (pc+1 (pc s)))))

(defthm statep-jumpz
  (implies (and (jumpzp a b)
                (statep s))
           (statep (jumpz a b s))))

(defun jump (a s)
  (declare (xargs :guard (and (jumpp a)
                              (statep s))))
  (modify s :pc (cons (car (pc s)) a)))

(defthm statep-jump
  (implies (and (jumpp a)
                (statep s))
           (statep (jump a s))))

; Subroutine Call and Return

(defun call (a s)
  (declare (xargs :guard (and (callp a)
                              (statep s))))
  (modify s
          :pc (cons a 0)
          :stk (cons (pc+1 (pc s)) (stk s))))

(defthm statep-call
  (implies (and (callp a)
                (statep s))
           (statep (call a s))))

(defun ret (s)
  (declare (xargs :guard (and (retp)
                              (statep s))))
  (if (endp (stk s))
      (modify s :halt t)
      (modify s
              :pc (car (stk s))
              :stk (cdr (stk s)))))

(defthm statep-ret
  (implies (statep s)
           (statep (ret s))))

; One can imagine adding new instructions.

(deftheory instruction-semantics
  '(movep move
    movip movi
    addp  add
    subip subi
    jumpzp jumpz
    jumpp jump
    callp call
    retp ret))
  

; The Interpreter

(defun execute (ins s)
  (declare (xargs :guard (and (or (null ins)
                                  (insp ins))
                              (statep s))
                  :guard-hints
                  (("Goal"
                    :in-theory
                    (set-difference-theories
                     (current-theory :here)
                     (cons '(:definition statep)
                           (theory 'instruction-semantics)))))))
  (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))))

(defthm statep-execute
  (implies (and (statep s)
                (force (or (null ins)
                           (insp ins))))
           (statep (execute ins s)))
  :hints 
  (("Goal"
    :in-theory
    (set-difference-theories
     (current-theory :here)
     (cons '(:definition statep)
           (theory 'instruction-semantics))))))


(defthm instructionsp-assoc-eq
  (implies (codep code)
           (instructionsp (cdr (assoc-eq x code)))))

(defthm insp-nth-instructionsp
  (implies (and (instructionsp lst)
                (nth i lst))
           (insp (nth i lst)))
  :hints (("Goal" :in-theory (disable insp))))

(defthm ins-current-instruction
  (implies (and (force (statep s))
                (current-instruction s))
           (insp (current-instruction s)))
  :hints (("Goal" :in-theory (disable insp))))

(defun step (s)
  (declare (xargs :guard (statep s)
                  :guard-hints 
                  (("Goal"
                    :in-theory (disable insp current-instruction)))))

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

(defthm statep-step
  (implies (statep s)
           (statep (step s)))
  :hints (("Goal" :in-theory (disable insp
                                      current-instruction
                                      statep
                                      execute))))

(defun sm (s n)
  (declare (xargs :guard
                  (and (statep s) (natp n))
                  :guard-hints (("Goal" :in-theory (disable statep step)))))
  (if (zp n)
      s
      (sm (step s) (+ n -1))))

; This concludes our formal definition of the intepreter.

; Now we develop the symbolic computation lemmas.

; We start with arithmetic.  We need some arithmetic simplification.

; In earlier versions of this book we used a subsidary book to hide
; the dumb arithmetic.  But that meant sending two files and having
; more complicated certification instructions.  So now we just start
; with an aside.  Here are some lemmas that suffice for our examples.
; The acl2:: prefixes are an ugly consequence of us putting this into
; the "SMALL-MACHINE" package.  In a separate book, with (in-package
; "ACL2"), these are prettier.

(defthm constant-fold-+
  (implies (syntaxp (and (quotep x) (quotep y)))
           (equal (+ x (+ y z)) (+ (+ x y) z))))

(defthm commutativity2-of-+
  (equal (+ x y z) (+ y x z))
  :hints (("Goal" :use ((:instance acl2::associativity-of-+
                                   (acl2::x y)
                                   (acl2::y x)
                                   (acl2::z z))
                        (:instance acl2::associativity-of-+
                                   (acl2::x x)
                                   (acl2::y y)
                                   (acl2::z z))
                        (:instance acl2::commutativity-of-+
                                   (acl2::x x)
                                   (acl2::y y)))
           :in-theory (disable acl2::associativity-of-+
                               acl2::commutativity-of-+))))

(defthm commutativity2-of-*
  (equal (* x y z) (* y x z))
  :hints (("Goal" :use ((:instance acl2::associativity-of-*
                                   (acl2::x y)
                                   (acl2::y x)
                                   (acl2::z z))
                        (:instance acl2::associativity-of-*
                                   (acl2::x x)
                                   (acl2::y y)
                                   (acl2::z z))
                        (:instance acl2::commutativity-of-*
                                   (acl2::x x)
                                   (acl2::y y)))
           :in-theory (disable acl2::associativity-of-*
                               acl2::commutativity-of-*))))

(defthm plus-right-id
  (equal (+ x 0) (fix x)))

(defthm *-0 (equal (* 0 x) 0))

(defthm +-cancellation1
  (equal (+ i j (* -1 i) k)
         (+ j k)))

(defthm 5+len-x=5
  (equal (equal (+ 5 (len x)) 5)
         (atom x)))

; End of the arithmetic "book".

; We will disable the state manipulation primitives so we don't see excessive
; car/cdr nests.  But that means we need to prove the standard lemmas for
; abstract data types...

(defthm statep-state
  (implies (and (pcp pc)
                (stkp stk)
                (memp mem)
                (codep code))
           (statep (state pc stk mem halt code))))

(defthm accessors
  (and (equal (pc (state pc stk mem halt code)) pc)
       (equal (stk (state pc stk mem halt code)) stk)
       (equal (mem (state pc stk mem halt code)) mem)
       (equal (halt (state pc stk mem halt code)) halt)
       (equal (code (state pc stk mem halt code)) code)
       (equal (len (state pc stk mem halt code)) 5)))

(defthm types-of-accessors
  (implies (statep s)
           (and (pcp (pc s))
                (symbolp (car (pc s)))
                (integerp (cdr (pc s)))
                (<= 0 (cdr (pc s)))
                (stkp (stk s))
                (memp (mem s))
                (codep (code s))))
  
  :rule-classes
  ((:rewrite 
    :corollary
    (implies (statep s)
             (and
              ; (consp (pc s))
              ; (symbolp (car (pc s)))
              ; (integerp (cdr (pc s)))
              ; (<= 0 (cdr (pc s)))
              (stkp (stk s))
              ; (true-listp (mem s))
              (codep (code s)))))
   (:type-prescription
    :corollary
    (implies (statep s)
             (consp (pc s))))
   (:type-prescription
    :corollary
    (implies (statep s)
             (symbolp (car (pc s)))))
   (:type-prescription
    :corollary
    (implies (statep s)
             (integerp (cdr (pc s)))))
   (:type-prescription
    :corollary
    (implies (statep s)
             (<= 0 (cdr (pc s)))))
   (:type-prescription
    :corollary
    (implies (statep s)
             (memp (mem s))))))

(encapsulate
 nil
 (local
  (defthm nth-expander
    (and
     (equal (nth 0 x) (car x))
     (implies (and (integerp i)
                   (<= 0 i)
                   (syntaxp (quotep i)))
              (equal (nth (+ 1 i) x)
                     (nth i (cdr x)))))))
 (defthm accessors-elim
   (implies (statep s)
            (equal (state (pc s) (stk s) (mem s) (halt s) (code s)) s))
   :rule-classes :elim))

(in-theory (disable statep state pc stk mem halt code))



(defthm step-opener
  (and (implies (halt s) (equal (step s) s))
       (implies (consp (current-instruction s))
                (equal (step s)
                       (if (halt s)
                           s
                           (execute (current-instruction s) s)))))
  :hints (("Goal" :in-theory (disable execute))))

(in-theory (disable step))

(defun cplus (i j)
  (+ (nfix i) (nfix j)))

(defun nat-recursion (i)
  (if (zp i) 0 (+ 1 (nat-recursion (- i 1)))))

(defthm cplus-alt-def
  (equal (cplus i j)
         (if (zp i)
             (nfix j)
           (+ 1 (cplus (1- i) j))))
  :rule-classes ((:definition :clique (cplus)
                              :controller-alist ((cplus t nil)))
                 (:induction :corollary t
                             :pattern (cplus i j)
                             :scheme (nat-recursion i))))

(defun ctimes (i j)
  (* (nfix i) (nfix j)))

(encapsulate nil
             (local (defthm lemma
                      (implies (and (<= 0 j)
                                    (integerp i)
                                    (<= 1 i))
                               (<= j (* i j)))
                      :rule-classes :linear
                      :hints (("Goal" :induct (nat-recursion i)))))

             (defthm ctimes-alt-def
               (equal (ctimes i j)
                      (if (zp i) 0 (cplus j (ctimes (1- i) j))))
               :rule-classes ((:definition :clique (ctimes)
                                           :controller-alist ((ctimes t nil)))
                              (:induction :corollary t
                                          :pattern (ctimes i j)
                                          :scheme (nat-recursion i)))))


(in-theory (disable cplus ctimes))

(defthm sm-cplus
  (implies (and (natp i) (natp j))
	   (equal (sm s (cplus i j))
		  (sm (sm s i) j)))
  :hints (("Goal" :in-theory (enable cplus))))

; Sometimes we get sm expressions such as (sm s (+ 4 (cplus ...))).  The
; following lemma produces (sm (sm s 4) (cplus ...)).

(defthm sm-+
  (implies (and (natp i) (natp j))
	   (equal (sm s (+ i j))
		  (sm (sm s i) j)))
  :hints (("Goal" :use sm-cplus
                  :in-theory (enable cplus))))

; Then we finally hit the (sm s 4) repeatedly with the following lemma to
; step s 4 times.

(defthm sm-opener
  (and (equal (sm s 0) s)
       (implies (natp i)
                (equal (sm s (+ 1 i))
                       (sm (step s) i)))))

(in-theory (disable sm))

; Here is the memory expression management stuff.

(defthm put-cons
  (and (equal (put 0 x (cons y mem)) (cons x mem))
       (implies (and (integerp i)
                     (<= 0 i)
                     (syntaxp (quotep i)))
                (equal (put (+ 1 i) x (cons y mem))
                       (cons y (put i x mem))))))

(defthm get-put
  (implies (and (natp i)
                (natp j))
           (equal (get i (put j val mem))
                  (cond ((equal i j) val) (t (get i mem))))))

(defthm put-put-0
  (implies (and (natp i)
                (< i (len mem))
                (equal (get i mem) val))
           (equal (put i val mem) mem)))

(defthm put-put-1
  (equal (put i val2 (put i val1 mem))
         (put i val2 mem)))

(defun put-put-simplifier (term)
  (cond ((and (consp term)
              (eq (car term) 'put)
              (quotep (cadr term))
              (integerp (cadr (cadr term)))
              (<= 0 (cadr (cadr term)))
              (consp (cadddr term))
              (eq (car (cadddr term)) 'put)
              (quotep (cadr (cadddr term)))
              (integerp (cadr (cadr (cadddr term))))
              (<= 0 (cadr (cadr (cadddr term))))
              (> (cadr (cadr term))
                 (cadr (cadr (cadddr term)))))
         (list 'put (cadr (cadddr term)) (caddr (cadddr term))
               (list 'put (cadr term) (caddr term)
                     (cadddr (cadddr term)))))
        (t term)))
  
(defevaluator put-eval put-eval-lst ((put i val mem)))

(defthm put-put-2
  (implies (and (natp i)
                (natp j)
                (not (equal i j)))
           (equal (put i vali (put j valj mem))
                  (put j valj (put i vali mem)))))

(defthm put-put-simplifier-correct
  (equal (put-eval term a)
         (put-eval (put-put-simplifier term) a))
  :rule-classes ((:meta :trigger-fns (put))))

(in-theory (disable put-put-2))

(defthm len-put
  (implies (and (natp i)
                (< i (len mem)))
           (equal (len (put i val mem)) (len mem))))


(in-theory (disable nth put get))

; Now we move to our first example program.  We will define a program
; that multiplies two naturals by successive addition.  We will then
; prove it correct.

; The program we have in mind is:

; (times (movi 2 0)
;        (jumpz 0 5)
;        (add 2 1)
;        (subi 0 1)
;        (jump 1)
;        (ret))

; Observe that the program multiplies the contents of location 0 by the
; contents of location 1 and leaves the result in location 2.  At the end,
; location 0 is 0 and location 1 is unchanged.  If we start at a (call times)
; this program requires 2+4i+2 instructions, where i is the initial contents of
; location 0.

; We start by defining the constant that is this program:

(defun times-program nil
;         instruction   pc     comment
  '(times (movi 2 0)   ; 0  mem[2] <- 0
          (jumpz 0 5)  ; 1  if mem[0]=0, go to 5
          (add 2 1)    ; 2  mem[2] <- mem[1] + mem[2]
          (subi 0 1)   ; 3  mem[0] <- mem[0] - 1
          (jump 1)     ; 4  go to 1
          (ret)))      ; 5  return to caller

; Here is a state that computes 7*11.

(defun demo-state nil
  (st :pc   '(times . 0)
      :stk   nil
      :mem  '(7 11 3 4 5)
      :halt nil
      :code (list (times-program))))

; And a trivial theorem to prove it:

(defthm demo-theorem
  (equal (sm (demo-state) 31)
         (st :pc   '(times . 5)
             :stk  nil
             :mem  '(0 11 77 4 5)
             :halt t
             :code (list (times-program)))))

; The clock function for times:

(defun times-clock (i)
  (cplus 2 (cplus (ctimes i 4) 2)))

; The mem function for times.  Times-fn-mem takes a state and yields a memory.
; This way it also encodes the induction.

(defun times-fn-mem (s)
  (declare (xargs :measure (acl2-count (get 0 (mem s)))
                  :hints (("Goal" :in-theory (enable statep)))))
  (if (statep s)
      (let ((m0 (get 0 (mem s)))
            (m1 (get 1 (mem s)))
            (m2 (get 2 (mem s))))
        (if (zp m0)
            (mem s)
          (times-fn-mem
           (modify s
                   :mem
                   (put 0 (+ m0 -1)
                        (put 2 (+ m1 m2) (mem s)))))))
    s))

; In some sense, the following mathematical fact completely captures
; the correctness of the program:

(defthm times-fn-mem-is-times
  (implies (and (statep s)
                (< 2 (len (mem s)))
                (equal m0 (get 0 (mem s)))
                (equal m1 (get 1 (mem s)))
                (equal m2 (get 2 (mem s)))
                (natp m0))
           (equal (times-fn-mem s)
                  (put 0 0
                   (put 2 (+ m2 (* m0 m1)) (mem s)))))
  :hints (("Goal" :in-theory (disable accessors-elim))))

; The hint above is required simply to let us state the lemma the way we show
; in the paper.  If we substituted the get expressions for the mi's,
; eliminating the three variables m0, m1, and m2, then this theorem would go
; right through:  we try elim, it doesn't work, and we back off and do
; an induction on the input formula.  But with the variables in place:  we try
; elim, it doesn't work, and we back off and do an induction on the
; input formula.  But it doesn't work since the mi don't participate in the
; induction scheme.  If we don't try the elim first, we substitute the vars
; away and induct on the result.

; There is something subtle happening below.  We prove the theorem in one form
; and store it in another.  We mention this in the paper.  In the stored
; version, the lhs of the conclusion is (sm s (ctimes i 4)).  In the proved
; version, it is (sm s (ctimes (get 0 (mem s)) 4)).  The proved version goes
; through induction (the i in the stored version requires accomodation in the
; induction), while the i in the stored version allows the rule to apply not
; just to sm applications on the very same s used to compute the clock but on
; any s whose mem[0] is the one used to compute the clock.

(defthm times-correct-lemma
  (implies (and (statep s)
                (< 2 (len (mem s)))
                (natp (get 0 (mem s)))
                (equal (pc s) '(times . 1))
                (equal (assoc-eq 'times (code s)) (times-program))
                (not (halt s)))
           (equal (sm s (ctimes (get 0 (mem s)) 4))
                  (modify s :mem (times-fn-mem s))))
  :rule-classes
  ((:rewrite
    :corollary
    (implies (and (statep s)
                  (< 2 (len (mem s)))
                  (equal i (get 0 (mem s)))
                  (natp i)
                  (equal (pc s) '(times . 1))
                  (equal (assoc-eq 'times (code s)) (times-program))
                  (not (halt s)))
             (equal (sm s (ctimes i 4))
                    (modify s :mem (times-fn-mem s)))))))

(defthm times-correct
  (implies (and (statep s0)
                (< 2 (len (mem s0)))
                (equal i (get 0 (mem s0)))
                (equal j (get 1 (mem s0)))
                (<= 0 i)
                (equal (current-instruction s0) '(call times))
                (equal (assoc-eq 'times (code s0)) (times-program))
                (not (halt s0)))
           (equal (sm s0 (times-clock i))
                  (modify s0
                          :pc (pc+1 (pc s0))
                          :mem (put 0 0
                                (put 2 (* i j) (mem s0)))))))

; We disable the clock function so that subsequent programs can
; use it without its expansion messing up their algebraic
; form.

(in-theory (disable times-clock))

; We now consider the role of subroutine call and return in this
; language.  To illustrate it we'll implement exponentiation, which
; will CALL our TIMES program.  The proof of the correctness of the
; exponentiation program will rely on the correctness of TIMES, not on
; re-analysis of the code for TIMES.

; The mathematical function we wish to implement is (expt i j), where
; i and j are naturals.

; The program we have in mind is:

(defun expt-program nil
  '(expt (move 3 0)   ; 0  mem[3] <- mem[0] (save args)
         (move 4 1)   ; 1  mem[4] <- mem[1]
         (movi 1 1)   ; 2  mem[1] <- 1      (initialize ans)
         (jumpz 4 9)  ; 3  if mem[4]=0, go to 9
         (move 0 3)   ; 4  mem[0] <- mem[3] (prepare for times)
         (call times) ; 5  mem[2] <- mem[0] * mem[1]
         (move 1 2)   ; 6  mem[1] <- mem[2]
         (subi 4 1)   ; 7  mem[4] <- mem[4]-1
         (jump 3)     ; 8  go to 3
         (ret)))      ; 9  return

; This program computes (expt mem[0] mem[1]) and leaves the result in mem[1].
; Because we use times (which requires repeatedly loading mem[0] and mem[1] to
; pass in its parameters) and because times smashes mem[2] with its result, we
; will use mem[3] and mem[4] as our "locals."  We will use mem[1] as our
; running answer, which starts at 1.  After moving mem[0] and mem[1] to mem[3]
; and mem[4] respectively and initializing our running answer to 1, we just
; multiply mem[3] by mem[1] (mem[4] times), moving the product back into mem[1]
; after each multiplication.

; A recursive description of the loop (pc 3 through 8) in this
; algorithm is:

(defun expt-fn-mem (s)
  (declare (xargs :measure (acl2-count (get 4 (mem s)))))
  (let ((m1 (get 1 (mem s)))
        (m3 (get 3 (mem s)))
        (m4 (get 4 (mem s))))
    (if (zp m4)
        (mem s)
        (expt-fn-mem
         (modify s
                 :mem
                 (put 0 0
                  (put 1 (* m3 m1)
                   (put 2 (* m3 m1)
                    (put 4 (- m4 1) (mem s))))))))))
  
; Pretty weird.

; We show the derived function has the desired generalized effect on memory.

(defthm expt-fn-mem-is-expt
  (implies (and (statep s)
                (< 4 (len (mem s)))
                (equal m1 (get 1 (mem s)))
                (equal m3 (get 3 (mem s)))
                (equal m4 (get 4 (mem s))))
           (equal (expt-fn-mem s)
                  (if (zp m4)
                      (mem s)
                      (put 0 0
                       (put 1 (* m1 (expt m3 m4))
                        (put 2 (* m1 (expt m3 m4))
                         (put 4 0 (mem s))))))))
  :hints (("Goal" :in-theory (disable accessors-elim))))

; Here is the clock function for expt.  Again we use an algebraically
; odd form simply to gain instant access to the desired sm-plus
; decomposition.  The "4" nths us past the CALL and the first 3
; initialization instructions; the times exptression takes us around
; the expt loop j times, and the final "2" nths us out through the RET.
; Note that as we go around the loop we make explicit reference to
; TIMES-CLOCK to explain the CALL of TIMES.

(defun expt-clock (i j)
  (cplus 4
         (cplus (ctimes j (cplus 2 (cplus (times-clock i) 3)))
                2)))

; Now we prove the "loop invariant" for the EXPT program.  We simply
; tell the system to induct according to expt-fn.  We could "trick" it
; into doing that by using expt-fn in place of the (times (expt r3 r4)
; r1) expressions, but that is devious and doesn't always work.

(defthm expt-correct-lemma
  (implies (and (statep s)
                (< 4 (len (mem s)))
                (<= 0 (get 3 (mem s)))
                (equal (pc s) '(expt . 3))
                (equal (assoc-eq 'expt (code s)) (expt-program))
                (equal (assoc-eq 'times (code s)) (times-program))
                (not (halt s)))
           (equal (sm s
                      (ctimes (get 4 (mem s))
                              (cplus 2
                                     (cplus (times-clock (get 3 (mem s)))
                                            3))))
                  (modify s :mem (expt-fn-mem s))))
  :rule-classes
  ((:rewrite
    :corollary
    (implies (and (statep s)
                  (< 4 (len (mem s)))
                  (equal m3 (get 3 (mem s)))
                  (equal m4 (get 4 (mem s)))
                  (natp m3)
                  (equal (pc s) '(expt . 3))
                  (equal (assoc-eq 'expt (code s)) (expt-program))
                  (equal (assoc-eq 'times (code s)) (times-program))
                  (not (halt s)))
             (equal (sm s
                        (ctimes m4
                                (cplus 2 (cplus (times-clock m3) 3))))
                    (modify s
                            :mem (expt-fn-mem s)))))))

; The theorem prover is now set up to prove that expt is correct
; without further assistance.  (But you must not underestimate how
; clever this assistance has been to make this possible!)

(defthm expt-correct
  (implies (and (statep s0)
                (< 4 (len (mem s0)))
                (equal i (get 0 (mem s0)))
                (equal j (get 1 (mem s0)))
                (<= 0 i)
                (<= 0 j)
                (equal (current-instruction s0) '(call expt))
                (equal (assoc-eq 'expt (code s0)) (expt-program))
                (equal (assoc-eq 'times (code s0)) (times-program))
                (not (halt s0)))
           (equal (sm s0 (expt-clock i j))
                  (modify s0 
                          :pc (pc+1 (pc s0))
                          :mem
                          (if (zp j)
                              (put 1 (expt i j)
                               (put 3 i
                                (put 4 0 (mem s0))))
                              (put 0 0
                               (put 1 (expt i j)
                                (put 2 (expt i j)
                                 (put 3 i
                                  (put 4 0 (mem s0)))))))))))

; Symbolic Simulation Examples:

; The examples shown below were added for the symbolic simulation paper.

(defun pi nil
  '(TIMES (MOVI 2 0)
          (JUMPZ 0 5)
          (ADD 2 1)
          (SUBI 0 1)
          (JUMP 1)
          (RET)))

(defun alpha ()
  (st :pc   '(TIMES . 0)
      :stk  nil
      :mem  (list 7 11 3 4 5)
      :halt nil
      :code `(,(pi))))
  
(defun beta (i j x y z)
  (st :pc   '(TIMES . 0)
      :stk  nil
      :mem  (list i j x y z)
      :halt nil
      :code `(,(pi))))

(defthm get-list
  (and (equal (get 0 (cons u v)) u)
       (implies (and (natp n)
                     (syntaxp (quotep n)))
                (equal (get (+ 1 n) (cons u v))
                       (get n v))))
  :hints (("Goal" :in-theory (enable get))))

; The following rule probably lets us symbolically simulate faster, but
; I haven't conducted any tests to confirm this.

(defthm get-list-5
  (and (equal (get 4 (list i j x y z)) z)
       (equal (get 3 (list i j x y z)) y)
       (equal (get 2 (list i j x y z)) x)
       (equal (get 1 (list i j x y z)) j)
       (equal (get 0 (list i j x y z)) i)))

(defmacro ints (&rest args)
  (cond ((endp args)
         t)
        ((endp (cdr args))
         `(integerp ,(car args)))
        (t `(and (integerp ,(car args)) (ints ,@(cdr args))))))

; In the paper, examples of symbolic simulation are given as
; non-theorems involving the variable symbol v.  But I can't put such
; non-theorems into a certified book.  So I have replaced v by the
; desired final state.  These examples therefore do not necessarily
; represent symbolic simulation.  (For example, they could be proved
; by transforming the right-hand side into the left (!) rather than
; vice versa.  But if you replace the right-hand side states below by
; the new variable v you will see failed proofs in which v is to be
; proved equal to the right-hand sides given here.

(defthm example-symsim-1
 (implies (and (ints i j x y z)
               (< 0 i))
          (equal (sm (beta i j x y z) 4)
                 (ST :pc   '(TIMES . 4)
                     :stk  NIL
                     :mem  (LIST (+ -1 I) J J Y Z)
                     :halt NIL
                     :code `(,(pi)))))
 :rule-classes nil)

(defthm example-symsim-2
  (implies (and (ints i j x y z)
                (< 1 i))
           (equal (sm (beta i j x y z) (+ 4 4)) 
                  (st :pc   '(TIMES . 4)
                      :stk   nil
                      :mem  (list (+ -2 i) j (+ j j) y z)
                      :halt nil
                      :code `(,(pi)))))
 :rule-classes nil)

(defthm example-symsim-2-split
  (implies (and (ints i j x y z)
                (< 0 i))
           (equal (sm (beta i j x y z) (+ 4 4)) 
                  (if (equal i 1)
                      (st :pc   '(TIMES . 5)
                          :stk   nil
                          :mem  (list 0 j j y z)
                          :halt t
                          :code `(,(pi)))
                    (st :pc   '(TIMES . 4)
                        :stk   nil
                        :mem  (list (+ -2 i) j (+ j j) y z)
                        :halt nil
                        :code `(,(pi))))))
 :rule-classes nil)

; The following MAIN program mutiplies i times j then adds z to that
; and subtracts 1.

(defthm example-symsim-times
  (implies (and (ints i j x y z)
                (<= 0 i))
           (equal (sm (st :pc '(MAIN . 0)
                          :stk nil
                          :mem (list i j x y z)
                          :halt nil
                          :code `(,(pi)
                                  (MAIN (CALL TIMES)
                                        (ADD 4 2)
                                        (SUBI 4 1))))
                      (cplus (times-clock i) 2))
                  (st :pc '(MAIN . 3)
                      :stk nil
                      :mem (list 0 j (* i j) y (+ (* i j) z -1))
                      :halt nil
                      :code `(,(pi)
                              (MAIN (CALL TIMES)
                                    (ADD 4 2)
                                    (SUBI 4 1))))))
  :rule-classes nil)

; The following two rules are useful if we are do do runs that involve
; products like (* 1000 j).  The symbolic simulation of TIMES on such
; input would produce answers like (+ J J J ... J).  Rather than
; tolerate such large nests we normalize them into the form used in
; the paper.

(defthm j+j
  (equal (+ j j) (* 2 j)))

(defthm j+nj
  (equal (+ j (* n j))
         (* (+ n 1) j)))

; Effective End of the Book

#|

; Everything below this point is commented out.

; Performance

; The performance figures quoted in the paper were obtained with
; experiments that involved modifying ACL2.  However, I give some
; illustrative theorems whose proof times are supportive of some of
; the numbers given.

; It is impossible to put these events into the book because they
; cannot be executed successfully until after the book has been
; compiled.  If they were part of the book proper then the attempt at
; certification would cause a stack overflow.  But if this book has
; been certified and then included, with 

(include-book "small-machine")

(in-package "SMALL-MACHINE")

, into an ACL2 session, the following theorems can
; be proved.

(defthm big-simulation-run
  (equal (get 2
              (mem
               (sm (st :pc   '(MAIN . 0)
                       :stk  nil
                       :mem  (list 0 0 0 0 0)
                       :halt nil
                       :code (list (pi)
                                   '(MAIN (MOVI 0 10000)
                                          (MOVI 1 1000)
                                          (CALL TIMES)
                                          (RET))))
                   40007)))
         10000000))

; Time:  0.63 seconds (prove: 0.61, print: 0.00, other: 0.02)

; The paper reports 0.53 because that is what I got when I ran the (sm
; (st ...) 400007) in raw Lisp and used the Common Lisp function
; lisp::time to time it.  

; It is not easy to get the times for a non-compliant run from the
; sources distributed here.  If you simply re-certified this book but
; with a directive in place to prevent guard verification, e.g.,
; (set-verify-guards-eagerness 0), you would NOT achieve the desired
; results.  There are two reasons.  First, the guards would still be
; in place in the source code and that would cause us to check them at
; runtime on every entry of every function.  So it would be much
; slower than running code in which the guards had simply been
; stripped out of user functions (but for which we still do runtime
; checks of Lisp primitives).  Second, we do not generally compile
; non-compliant code.

; To perform the test reported in the paper I made a copy of this
; book, up through the definition of pi.  Then I stripped out all
; declarations.  Then I certified the resulting unguarded code.  Then
; I included that code into an ACL2 session and executed the ACL2
; command :comp t to compile all uncompiled functions in the image.
; Finally, I did the same lisp::time experiment above in raw Lisp but
; instead of calling sm (which is the assumed-compliant compiled code)
; I called acl2_*1*_small-machine::sm, which is our compiled version
; of the code which checks all guards (for which, here, there are only
; guards on the primitives).

; Here is a symbolic execution task similar to the one measured in the
; paper, without any hint and then with a hint.

(defthm 1000*j-no-hint
  (implies (ints j x y z)
           (equal (sm (st :pc '(MAIN . 0)
                          :stk nil
                          :mem (list 1000 j x y z)
                          :halt nil
                          :code `(,(pi)
                                  (MAIN (CALL TIMES)
                                        (RET))))
                      (cplus (times-clock 1000) 1) ; 4005
                      )
                  (STATE '(MAIN . 1)
                         NIL
                         (LIST 0 J (* 1000 J) Y Z)
                         T
                         '((TIMES (MOVI 2 0)
                                  (JUMPZ 0 5)
                                  (ADD 2 1)
                                  (SUBI 0 1)
                                  (JUMP 1)
                                  (RET))
                           (MAIN (CALL TIMES) (RET))))))
  :rule-classes nil)

; Time:  53.40 seconds (prove: 53.37, print: 0.01, other: 0.02)

(defthm 1000*j-hint
  (implies (ints j x y z)
           (equal (sm (st :pc '(MAIN . 0)
                          :stk nil
                          :mem (list 1000 j x y z)
                          :halt nil
                          :code `(,(pi)
                                  (MAIN (CALL TIMES)
                                        (RET))))
                      (cplus (times-clock 1000) 1) ; 4005
                      )
                  (STATE '(MAIN . 1)
                         NIL
                         (LIST 0 J (* 1000 J) Y Z)
                         T
                         '((TIMES (MOVI 2 0)
                                  (JUMPZ 0 5)
                                  (ADD 2 1)
                                  (SUBI 0 1)
                                  (JUMP 1)
                                  (RET))
                           (MAIN (CALL TIMES) (RET))))))
  :rule-classes nil
  :hints (("Goal"
           :in-theory
           '((:EXECUTABLE-COUNTERPART PI)
             (:EXECUTABLE-COUNTERPART TIMES-CLOCK)
             (:EXECUTABLE-COUNTERPART CPLUS)
             (:DEFINITION IMPLIES)
;            (:FAKE-RUNE-FOR-TYPE-SET NIL)     <- this cannot be in a theory
             (:REWRITE SM-OPENER)
             (:DEFINITION RET)
             (:EXECUTABLE-COUNTERPART CDR)
             (:REWRITE ACL2::COMMUTATIVITY-OF-+)
             (:REWRITE J+NJ)
             (:REWRITE J+J)
             (:DEFINITION JUMP)
             (:DEFINITION SUBI)
             (:EXECUTABLE-COUNTERPART ACL2::BINARY-+)
             (:EXECUTABLE-COUNTERPART ACL2::UNARY--)
             (:DEFINITION ADD)
             (:REWRITE ACL2::UNICITY-OF-0)
             (:DEFINITION FIX)
             (:DEFINITION JUMPZ)
             (:REWRITE GET-LIST-5)
             (:DEFINITION MOVI)
             (:REWRITE PUT-CONS)
             (:EXECUTABLE-COUNTERPART CAR)
             (:EXECUTABLE-COUNTERPART EQ)
             (:EXECUTABLE-COUNTERPART IF)
             (:DEFINITION SYNTAXP)
             (:REWRITE STEP-OPENER)
             (:DEFINITION EXECUTE)
             (:DEFINITION CALL)
             (:EXECUTABLE-COUNTERPART PC+1)
             (:EXECUTABLE-COUNTERPART CONS)
             (:EXECUTABLE-COUNTERPART EQUAL)
             (:EXECUTABLE-COUNTERPART B)
             (:EXECUTABLE-COUNTERPART A)
             (:EXECUTABLE-COUNTERPART OPCODE)
             (:EXECUTABLE-COUNTERPART CONSP)
             (:DEFINITION CURRENT-INSTRUCTION)
             (:EXECUTABLE-COUNTERPART FETCH)
             (:REWRITE ACCESSORS)
             (:EXECUTABLE-COUNTERPART NATP)))))

; Time:  20.72 seconds (prove: 20.66, print: 0.02, other: 0.04)

|#