#|
This file corresponds to the paper

Mechanized Formal Reasoning about Programs and Computing Machines

Robert S. Boyer and J Strother Moore



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)
           (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))))

; 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
  (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)))

(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 natp (x)
  (and (integerp x)
       (<= 0 x)))

(defun cplus (i j)
  (if (zp i)
      (nfix j)
      (+ 1 (cplus (1- i) j))))

(defun ctimes (i j)
  (if (zp i) 0 (cplus j (ctimes (1- i) j))))

(defthm cplus-revealed
  (implies (and (natp i) (natp j))
           (equal (cplus i j) (+ i j))))

(defthm ctimes-revealed
  (implies (and (natp i) (natp j))
           (equal (ctimes i j) (* i j))))

(in-theory (disable cplus-revealed ctimes-revealed))

(defthm sm-cplus
  (implies (and (natp i) (natp j))
	   (equal (sm s (cplus i j))
		  (sm (sm s i) j))))

; 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-revealed))))

; 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 nth-put
  (implies (and (natp i)
                (natp j))
           (equal (nth i (put j val mem))
                  (cond ((equal i j) val) (t (nth i mem))))))

(defthm put-put-0
  (implies (and (natp i)
                (< i (len mem))
                (equal (nth 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))

; 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 (nth 0 (mem s)))))
  (let ((m0 (nth 0 (mem s)))
        (m1 (nth 1 (mem s)))
        (m2 (nth 2 (mem s))))
    (if (zp m0)
        (mem s)
        (times-fn-mem
         (modify s
                 :mem
                 (put 0 (+ m0 -1)
                  (put 2 (+ m1 m2) (mem s))))))))

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

(defthm times-fn-mem-is-times
  (implies (and (< 2 (len (mem s)))
                (equal m0 (nth 0 (mem s)))
                (equal m1 (nth 1 (mem s)))
                (equal m2 (nth 2 (mem s)))
                (natp m0)
                (natp m1)
                (natp m2))
           (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 nth 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 (nth 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 (nth 0 (mem s)))
                (equal (pc s) '(times . 1))
                (equal (assoc 'times (code s)) (times-program))
                (not (halt s)))
           (equal (sm s (ctimes (nth 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 (nth 0 (mem s)))
                  (natp i)
                  (equal (pc s) '(times . 1))
                  (equal (assoc '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 (nth 0 (mem s0)))
                (equal j (nth 1 (mem s0)))
                (natp i)
                (natp j)
                (equal (current-instruction s0) '(call times))
                (equal (assoc '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 (nth 4 (mem s)))))
  (let ((m1 (nth 1 (mem s)))
        (m3 (nth 3 (mem s)))
        (m4 (nth 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 (< 4 (len (mem s)))
                (equal m1 (nth 1 (mem s)))
                (equal m3 (nth 3 (mem s)))
                (equal m4 (nth 4 (mem s)))
                (natp m1)
                (natp m3)
                (natp m4))
           (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)))
                (natp (nth 1 (mem s)))
                (natp (nth 3 (mem s)))
                (natp (nth 4 (mem s)))
                (equal (pc s) '(expt . 3))
                (equal (assoc 'expt (code s)) (expt-program))
                (equal (assoc 'times (code s)) (times-program))
                (not (halt s)))
           (equal (sm s
                      (ctimes (nth 4 (mem s))
                              (cplus 2
                                     (cplus (times-clock (nth 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 (nth 3 (mem s)))
                  (equal m4 (nth 4 (mem s)))
                  (natp (nth 1 (mem s)))
                  (natp m3)
                  (natp m4)
                  (equal (pc s) '(expt . 3))
                  (equal (assoc 'expt (code s)) (expt-program))
                  (equal (assoc '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 (nth 0 (mem s0)))
                (equal j (nth 1 (mem s0)))
                (natp i)
                (natp j)
                (equal (current-instruction s0) '(call expt))
                (equal (assoc 'expt (code s0)) (expt-program))
                (equal (assoc '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 following theorems are provable.  But more importantly, if you
; replace the states in the right-hand sides of the conclusions with
; some bogus variable name, e.g., ???, then the simplifier produces
; the goal to prove that ??? is equal to the replaced state.  Because
; ACL2 does not have a way for me to put a simplification problem in a
; certified book, I have had to phrase these simplifications as
; theorems.

(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 ()
  (st :pc   '(TIMES . 5)
      :stk  nil
      :mem  (list 0 11 77 4 5)
      :halt t
      :code `(,(pi))))

(defthm example-sim
  (equal (sm (alpha) 31) (beta))
  :rule-classes nil)

(defun gamma (i j x y z)
  (st :pc   '(TIMES . 0)
      :stk  nil
      :mem  (list i j x y z)
      :halt nil
      :code `(,(pi))))

(defthm alpha-is-gamma
        (equal (alpha) (gamma 7 11 3 4 5))
        :rule-classes nil)

(defthm example-symsim-1
 (implies (and (natp i)
               (natp j)
               (< 0 i))
          (equal (sm (gamma 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 (natp i)
                (< 1 i)
                (natp j))
           (equal (sm (gamma 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-3
  (implies (and (natp i)
                (< 2 i)
                (natp j))
           (equal (sm (gamma i j x y z) (+ 4 4 4)) 
                  (st :pc   '(TIMES . 4)
                      :stk   nil
                      :mem  (list (+ -3 i) j (+ j j j) y z)
                      :halt nil
                      :code `(,(pi)))))
 :rule-classes nil)

(defthm example-symsim-7
  (implies (natp j)
           (equal (sm (gamma 7 j x y z) (* 7 4)) 
                  (st :pc   '(TIMES . 4)
                      :stk   nil
                      :mem  (list 0 j (+ j j j j j j j) y z)
                      :halt nil
                      :code `(,(pi)))))
 :rule-classes nil)

(defthm example-symsim-7-terminated
  (implies (natp j)
           (equal (sm (gamma 7 j x y z) (+ (* 7 4) 1 1 1)) 
                  (st :pc   '(TIMES . 5)
                      :stk   nil
                      :mem  (list 0 j (+ j j j j j j j) y z)
                      :halt t
                      :code `(,(pi)))))
 :rule-classes nil)

(defthm example-symsim-2-split
  (implies (and (natp i)
                (< 0 i)
                (natp j))
           (equal (sm (gamma 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)

(defthm example-symsim-times
  (implies (and (natp i)
                (natp j)
                (natp z))
           (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 (+ -1 z (* i j)))
                      :halt nil
                      :code `(,(pi)
                              (MAIN (CALL TIMES)
                                    (ADD 4 2)
                                    (SUBI 4 1))))))
  :rule-classes nil)