#|
 Copyright (C) 1985 by Warren A. Hunt, Jr.  All Rights Reserved.

 You may copy and distribute verbatim copies of this Nqthm-1992 event script as
 you receive it, in any medium, including embedding it verbatim in derivative
 works, provided that you conspicuously and appropriately publish on each copy
 a valid copyright notice "Copyright (C) 1985 by Warren A. Hunt, Jr.  All
 Rights Reserved."

 NO WARRANTY

 Warren A. Hunt, Jr. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Warren A. Hunt, Jr. BE LIABLE TO YOU FOR ANY DAMAGES, ANY
 LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
 DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
 NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
 SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
 SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

;;; -*- Mode: LISP; Base: 10; Syntax: Zetalisp -*-

;   The Mechanical Verification of the FM8501 Microprocessor

;                             by
;                       Warren A. Hunt, Jr.



(boot-strap)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                             lemmas about PLUS                                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(compile-uncompiled-defns "tmp")
(prove-lemma plus-1 (rewrite)
  (equal (plus 1 x) (add1 x)))

(prove-lemma plus-right-id (rewrite)
  (implies (not (numberp y))
           (equal (plus x y) (fix x))))

(prove-lemma plus-add1 (rewrite)
  (equal (plus x (add1 y))
         (if (numberp y)
             (add1 (plus x y))
             (add1 x))))

(prove-lemma commutativity2-of-plus (rewrite)
  (equal (plus x (plus y z))
         (plus y (plus x z))))

(prove-lemma commutativity-of-plus (rewrite)
  (equal (plus x y) (plus y x)))

(prove-lemma associativity-of-plus (rewrite)
  (equal (plus (plus x y) z)
         (plus x (plus y z))))

(prove-lemma plus-equal-0 (rewrite)
  (equal (equal (plus a b) 0)
         (and (zerop a) (zerop b))))

(prove-lemma plus-cancellation (rewrite)
  (equal (equal (plus a b) (plus a c))
         (equal (fix b) (fix c))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                             lemmas about TIMES                               ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(prove-lemma times-zero2 (rewrite)
  (implies (not (numberp y))
           (equal (times x y) 0)))

(prove-lemma distributivity-of-times-over-plus (rewrite)
  (equal (times x (plus y z))
         (plus (times x y) (times x z))))

(prove-lemma times-add1 (rewrite)
  (equal (times x (add1 y))
         (if (numberp y)
             (plus x (times x y))
             (fix x))))

(prove-lemma commutativity-of-times (rewrite)
  (equal (times x y) (times y x)))

(prove-lemma commutativity2-of-times (rewrite)
  (equal (times x (times y z))
         (times y (times x z))))

(prove-lemma associativity-of-times (rewrite)
  (equal (times (times x y) z)
         (times x (times y z))))

(prove-lemma equal-times-0 (rewrite)
  (equal (equal (times x y) 0)
         (or (zerop x) (zerop y))))

(prove-lemma times-1 (rewrite)
  (equal (times 1 x) (fix x)))

(prove-lemma equal-bools (rewrite)
  (implies (and (or (equal bool1 t) (equal bool1 f))
                (or (equal bool2 t) (equal bool2 f)))
           (equal (equal bool1 bool2)
                  (and (implies bool1 bool2)
                       (implies bool2 bool1)))))

(disable equal-bools)

(prove-lemma lessp-times (rewrite)
  (equal (lessp (times y x) (times x z))
         (and (not (zerop x))
              (lessp y z)))
  
  ((enable equal-bools)))

(prove-lemma times-2-not-1 (rewrite)
  (not (equal (times 2 x) 1)))

(prove-lemma lessp-crock1 (rewrite)
  (equal (lessp (plus z (times 2 v w)) w)
         (and (zerop v) (lessp z w))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                             lemmas about EXP                                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defn exp (i j)
  (if (zerop j)
      1
      (times i (exp i (sub1 j)))))

(prove-lemma exp-plus (rewrite)
  (equal (exp i (plus j k))
         (times (exp i j) (exp i k))))

(prove-lemma exp-of-0 (rewrite)
  (equal (exp 0 k) (if (zerop k) 1 0)))

(prove-lemma exp-of-1 (rewrite)
  (equal (exp 1 k) 1))

(prove-lemma exp-by-0 (rewrite)
  (equal (exp x 0) 1))

(prove-lemma exp-times (rewrite)
  (equal (exp (times i j) k)
         (times (exp i k) (exp j k))))

(prove-lemma exp-2-never-0 (rewrite)
  (lessp 0 (exp 2 i)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                           lemmas about DIFFERENCE                            ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(prove-lemma difference-elim (elim)
  (implies (and (numberp y) (not (lessp y x)))
           (equal (plus x (difference y x)) y)))

(prove-lemma difference-2 (rewrite)
  (equal (difference x 2)
         (sub1 (sub1 x))))

(prove-lemma difference-x-x (rewrite)
  (equal (difference x x) 0))

(prove-lemma difference-plus (rewrite)
  (equal (difference (plus j x) j)
         (fix x)))

(prove-lemma difference-plus-cancellation (rewrite)
  (equal (difference (plus a x) (plus a y))
         (difference x y)))

(prove-lemma pathological-difference (rewrite)
  (implies (lessp x y) (equal (difference x y) 0)))

(prove-lemma difference-crock1 (rewrite)
  (equal (difference (plus x (difference y z)) y)
         (if (lessp y z)
             (difference x y)
             (difference x z))))

(prove-lemma difference-difference (rewrite)
  (equal (difference (difference x y) z)
         (difference x (plus y z))))

(prove-lemma lessp-difference (rewrite)
  (equal (lessp (difference x y) x)
         (and (not (zerop x)) (not (zerop y)))))

(prove-lemma difference-add1 nil
  (equal (difference (add1 x) y)
         (if (lessp y (add1 x))
             (add1 (difference x y))
             0)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                       lemmas about QUOTIENT and REMAINDER                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(prove-lemma remainder-quotient (rewrite)
  (equal (plus (remainder x y)
               (times y (quotient x y)))
         (fix x)))

(prove-lemma remainder-by-1 (rewrite)
  (equal (remainder y 1) 0))

(prove-lemma remainder-by-nonnumber (rewrite)
  (implies (not (numberp x))
           (equal (remainder y x) (fix y))))

(prove-lemma lessp-remainder (rewrite generalize)
  (equal (lessp (remainder x y) y)
         (not (zerop y))))

(prove-lemma remainder-quotient-elim (elim)
  (implies (and (not (zerop y)) (numberp x))
           (equal (plus (remainder x y)
                        (times y (quotient x y)))
                  x)))

(prove-lemma remainder-x-x (rewrite)
  (equal (remainder x x) 0))

(prove-lemma remainder-plus (rewrite)
  (equal (remainder (plus j x) j)
         (remainder x j)))

(prove-lemma remainder-plus-times (rewrite)
  (equal (remainder (plus x (times i j)) j)
         (remainder x j)))

(prove-lemma remainder-plus-times-commuted (rewrite)
  (equal (remainder (plus x (times j i)) j)
         (remainder x j)))

(prove-lemma remainder-times (rewrite)
  (equal (remainder (times j i) j)
         0)
  ((use (remainder-plus-times (x 0)))
   (disable remainder-plus-times)))

(prove-lemma remainder-add1-times (rewrite)
  (equal (remainder (add1 (times j i)) j)
         (remainder 1 j))
  ((use (remainder-plus-times (x 1)))
   (disable remainder-plus-times)))

(prove-lemma quotient-plus-times (rewrite)
  (equal (quotient (plus x (times i j)) j)
         (if (zerop j)
             0
             (plus i (quotient x j)))))

(prove-lemma quotient-plus-times-commuted (rewrite)
  (equal (quotient (plus x (times j i)) j)
         (if (zerop j)
             0
             (plus i (quotient x j)))))

(prove-lemma quotient-times (rewrite)
  (equal (quotient (times j i) j)
         (if (zerop j) 0 (fix i)))
  ((use (quotient-plus-times (x 0)))
   (disable quotient-plus-times)))

(prove-lemma quotient-add1-times (rewrite)
  (equal (quotient (add1 (times j i)) j)
         (if (zerop j) 0 (plus i (quotient 1 j))))
  ((use (quotient-plus-times (x 1)))
   (disable quotient-plus-times)))

(disable times)

(prove-lemma times-distributes-over-remainder (rewrite)
  (equal (remainder (times x y) (times x z))
         (times x (remainder y z)))
  ((expand (remainder (times v x) (times x z)))))

(prove-lemma remainder-of-1 (rewrite)
  (equal (remainder 1 x)
         (if (equal x 1) 0 1))
  ((expand (remainder 1 x))))

(prove-lemma remainder-crock1 (rewrite)
  (implies (and (numberp x)
                (lessp x z)
                (numberp v)
                (numberp z)
                (not (equal z 0)))
           (equal (remainder (add1 (plus (times 2 x) (times 2 v z)))
                             (times 2 z))
                  (add1 (times 2 x))))
  
  ;HINT:
  
  ((use (remainder-plus-times (x (add1 (times 2 x)))
                              (i v)
                              (j (times 2 z))))
   (disable remainder-plus-times)))

(prove-lemma times-2-distributes-over-remainder-add1 (rewrite)
  (equal (remainder (add1 (times 2 y)) (times 2 z))
         (add1 (times 2 (remainder y z)))))

(prove-lemma remainder-crock2 (rewrite)
  (implies (lessp v (exp 2 (sub1 size)))
           (equal (remainder (plus (times 2 v)
                                   (times 2 w (exp 2 (sub1 size))))
                             (times 2 (exp 2 (sub1 size))))
                  (times 2 v)))
  
  ;HINT:
  ((use (remainder-plus-times (x (times 2 v))
                              (i w)
                              (j (times 2 (exp 2 (sub1 size))))))
   (disable remainder-plus-times)))

(prove-lemma remainder-crock3 (rewrite)
  (equal (remainder (plus x (difference y z)) y)
         (if (lessp (plus x (difference y z)) y)
             (plus x (difference y z))
             (if (lessp y z)
                 (remainder x y)
                 (remainder (difference x z) y)))))

(prove-lemma remainder-of-0 (rewrite)
  (equal (remainder 0 x) 0))

(prove-lemma remainder-crock4 (rewrite)
  (equal (remainder (add1 (plus x (difference y z))) y)
         (if (lessp (add1 (plus x (difference y z))) y)
             (add1 (plus x (difference y z)))
             (if (lessp y z)
                 (remainder (add1 x) y)
                 (if (lessp z (add1 x))
                     (remainder (add1 (difference x z)) y)
                     0))))
  
  ;HINT:
  ((use (remainder-crock3 (x (add1 x)))
        (difference-add1 (x x) (y z)))
   (disable remainder-crock3 difference lessp remainder)))

(prove-lemma quotient-2i-by-2 (rewrite)
  (and (equal (quotient (add1 (plus i i)) 2) (fix i))
       (equal (quotient (plus i i) 2) (fix i))))

(prove-lemma remainder-2i-by-2 (rewrite)
  (and (equal (remainder (add1 (plus i i)) 2) 1)
       (equal (remainder (plus i i) 2) 0)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                           boolean operations                                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defn xor (x y)
  (if x (if y f t) (if y t f)))

(defn b-not (x)
  (if x f t))

(defn b-nand (x y)
  (if x (if y f t) t))

(defn b-nor (x y)
  (if x f (if y f t)))

(defn b-and (x y)
  (and x y))

(defn b-or (x y)
  (or x y))

(defn b-xor (x y)
  (if x (if y f t) (if y t f)))

(defn b-equv (x y)
  (if x (if y t f) (if y f t)))

(defn boolp (x)
  (or (truep x) (falsep x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                          primitive bit vector operations                     ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(add-shell bitv btm bitvp
           ((bit (one-of truep falsep) false)
            (vec (one-of bitvp) btm)))

(prove-lemma boolp-bit (generalize)
  (boolp (bit x)))

(defn fix-bv (x)
  (if (bitvp x) x (btm)))

(defn carry (c)
  (if c 1 0))

(defn size (a)
  (if (bitvp a)
      (if (equal a (btm))
          0
          (add1 (size (vec a))))
      0))

(defn trunc (a n)
  (if (zerop n)
      (btm)
      (bitv (bit a) (trunc (vec a) (sub1 n)))))

(defn compl (x)
  (if (bitvp x)
      (if (equal x (btm))
          (btm)
          (bitv (not (bit x)) (compl (vec x))))
      (btm)))

; IT MAY BE POSSIBLE TO ELIMINATE THE C FLG.

(defn incr (c x)
  (if (bitvp x)
      (if (equal x (btm))
          (btm)
          (bitv (xor c (bit x))
                (incr (and c (bit x)) (vec x))))
      (btm)))

(defn bitn (x n)
  (if (zerop n)
      f
      (if (equal n 1)
          (bit x)
          (bitn (vec x) (sub1 n)))))

(defn btmp (a)
  (if (bitvp a) (equal a (btm)) t))

(defn all-zerosp (a)
  (if (bitvp a)
      (if (equal a (btm))
          t
          (and (not (bit a)) (all-zerosp (vec a))))
      t))

(defn all-onesp (a)
  (if (bitvp a)
      (if (equal a (btm))
          t
          (and (bit a) (all-onesp (vec a))))
      t))

(prove-lemma size-of-trunc (rewrite)
  (equal (size (trunc a n)) (fix n)))

(prove-lemma size-of-compl (rewrite)
  (equal (size (compl a)) (size a)))

(prove-lemma size-of-incr (rewrite)
  (equal (size (incr c a)) (size a)))

(prove-lemma incr-f-noop (rewrite)
  (equal (incr f a) (fix-bv a)))

(prove-lemma size-0 (rewrite)
  (equal (equal (size x) 0) (btmp x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Definitions about logical functions                               ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn v-not (a)                 ; Vector not
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (not (bit a))
                (v-not (vec a))))
      (btm)))

(defn v-or (a b)                ; Vector or
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (or (bit a) (bit b))
                (v-or (vec a) (vec b))))
      (btm)))

(defn v-and (a b)               ; Vector and
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (and (bit a) (bit b))
                (v-and (vec a) (vec b))))
      (btm)))

(defn v-xor (a b)               ; Vector exclusive or
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (xor (bit a) (bit b))
                (v-xor (vec a) (vec b))))
      (btm)))

(defn bv-not (a)                ; Bit vector not
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (b-not (bit a))
                (bv-not (vec a))))
      (btm)))

(defn bv-or (a b)               ; Bit vector or
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (b-or (bit a) (bit b))
                (bv-or (vec a) (vec b))))
      (btm)))

(defn bv-and (a b)              ; Bit vector and
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (b-and (bit a) (bit b))
                (bv-and (vec a) (vec b))))
      (btm)))

(defn bv-xor (a b)              ; Bit vector exclusive or
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (b-xor (bit a) (bit b))
                (bv-xor (vec a) (vec b))))
      (btm)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                 TC numbers and their operations                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn tcp (x)
  (or (numberp x)
      (and (negativep x)
           (not (zerop (negative-guts x))))))

(defn tc-in-rangep (x n)
  (if (zerop n)
      f
      (if (negativep x)
          (not (lessp (exp 2 (sub1 n))
                      (negative-guts x)))
          (lessp x (exp 2 (sub1 n))))))

(defn add (x y)
  (if (negativep x)
      (if (negativep y)
          (minus (plus (negative-guts x) (negative-guts y)))
          (if (lessp y (negative-guts x))
              (minus (difference (negative-guts x) y))
              (difference y (negative-guts x))))
      (if (negativep y)
          (if (lessp x (negative-guts y))
              (minus (difference (negative-guts y) x))
              (difference x (negative-guts y)))
          (plus x y))))

(prove-lemma commutativity2-of-add (rewrite)
  (equal (add x (add y z)) (add y (add x z))))

(prove-lemma commutativity-of-add (rewrite)
  (equal (add x y) (add y x)))

(prove-lemma associativity-of-add (rewrite)
  (equal (add (add x y) z) (add x (add y z)))
  
  ;HINT:
  ((disable add)))

(prove-lemma add-with-carry-of-negatives-is-negative nil
  (implies (and (tcp x)
                (tcp y)
                (negativep x)
                (negativep y))
           (negativep (add x (add y (carry c))))))

(prove-lemma add-with-carry-of-non-negatives-is-non-negative nil
  (implies (and (tcp x)
                (tcp y)
                (not (negativep x))
                (not (negativep y)))
           (not (negativep (add x (add y (carry c)))))))

(prove-lemma overflow-lemma1 (rewrite)
  (implies (and (tcp x)
                (tcp y)
                (tc-in-rangep x n)
                (tc-in-rangep y n)
                (negativep (add x (add y (carry c)))))
           (not (negativep (add x (add y (add (carry c) (exp 2 n))))))))

(prove-lemma overflow-lemma2 (rewrite)
  (implies (and (tcp x)
                (tcp y)
                (tc-in-rangep x n)
                (tc-in-rangep y n)
                (not (negativep (add x (add y (carry c))))))
           (negativep (add x (add y (add (carry c) (minus (exp 2 n))))))))

(prove-lemma opposite-signs-implies-tc-in-rangep (rewrite)
  (implies (and (tcp x)
                (tcp y)
                (tc-in-rangep x n)
                (tc-in-rangep y n)
                (negativep x)
                (not (negativep y)))
           (tc-in-rangep (add x (add y (carry c))) n)))

(prove-lemma opposite-signs-implies-tc-in-rangep-commuted (rewrite)
  (implies (and (tcp x)
                (tcp y)
                (tc-in-rangep x n)
                (tc-in-rangep y n)
                (negativep x)
                (not (negativep y)))
           (tc-in-rangep (add y (add x (carry c))) n))
  
  ;HINT:
  ((disable tcp add tc-in-rangep carry)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;             Mapping Functions between BV, NAT, and TC                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn nat-to-bv (n size)                ; Natural number to bit vector
  (if (zerop size)
      (btm)
      (bitv (if (zerop (remainder n 2)) f t)
            (nat-to-bv (quotient n 2)
                       (sub1 size)))))

(defn bv-to-nat (x)                     ; Bit vector to natural number
  (if (bitvp x)
      (if (equal x (btm))
          0
          (plus (if (bit x) 1 0)
                (times 2 (bv-to-nat (vec x))))) ;
      0))

(defn tc-to-bv (x size)                 ; Two's complement number to bit vector
  (if (negativep x)
      (incr t
            (compl (nat-to-bv (negative-guts x) size)))
      (nat-to-bv x size)))

(defn bv-to-tc (x)                      ; Bit vector to two's complement number
  (if (bitn x (size x))
      (minus (bv-to-nat (incr t (compl x))))
      (bv-to-nat x)))

(defn nat-to-tc (n size)                ; Natural number to two's complement number
  (if (lessp n (exp 2 (sub1 size)))
      n
      (minus (difference (exp 2 size) n))))

(defn tc-to-nat (n size)                ; Two's complement number to natural number
  (if (negativep n)
      (difference (exp 2 size)
                  (negative-guts n))
      n))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                   Elementary Properties of Mapping Functions                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(prove-lemma size-of-nat-to-bv (rewrite)
  (equal (size (nat-to-bv n size)) (fix size)))

(prove-lemma size-of-tc-to-bv (rewrite)
  (equal (size (tc-to-bv x size)) (fix size)))

(prove-lemma bv-to-nat-of-incr (rewrite)
  (equal (bv-to-nat (incr t a))
         (if (all-onesp a)
             0
             (add1 (bv-to-nat a)))))

(prove-lemma bitn-implies-compl-not-all-onesp (rewrite)
  (implies (bitn a i) (not (all-onesp (compl a)))))

(prove-lemma upper-bound-on-bv-to-nat (rewrite)
  (lessp (bv-to-nat a) (exp 2 (size a))))

(prove-lemma bv-to-nat-of-compl (rewrite)
  (equal (bv-to-nat (compl a))
         (difference (sub1 (exp 2 (size a))) (bv-to-nat a))))

(prove-lemma bv-to-nat-to-tc-lemma1 nil
  (implies (bitn a (size a))
           (equal (bv-to-nat (incr t (compl a)))
                  (difference (exp 2 (size a))
                              (bv-to-nat a)))))

(prove-lemma bv-to-nat-to-tc-lemma2 nil
  (equal (bitn a (size a))
         (if (zerop (size a))
             f
             (not (lessp (bv-to-nat a) (exp 2 (sub1 (size a))))))))

(prove-lemma bv-to-nat-of-trunc (rewrite)
  (equal (bv-to-nat (trunc a n)) (remainder (bv-to-nat a) (exp 2 n))))

(prove-lemma all-onesp-of-compl (rewrite)
  (equal (all-onesp (compl a))
         (equal (bv-to-nat a) 0)))

(prove-lemma tcp-bv-to-tc (rewrite)
  (tcp (bv-to-tc a)))

(prove-lemma upper-bound-on-non-negative-bv-to-nat (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm)))
                (not (bitn a (size a))))
           (lessp (bv-to-nat a) (exp 2 (sub1 (size a))))))

(prove-lemma lower-bound-on-negative-bv-to-nat (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm)))
                (bitn a (size a)))
           (not (lessp (bv-to-nat a) (exp 2 (sub1 (size a)))))))

(prove-lemma tc-in-rangep-of-bv-to-tc (rewrite)
  (implies (equal n (size a))
           (equal (tc-in-rangep (bv-to-tc a) n)
                  (and (bitvp a) (not (equal a (btm)))))))

(prove-lemma bitn-means-negativep (rewrite)
  (implies (equal n (size a))
           (equal (bitn a n)
                  (negativep (bv-to-tc a)))))

(disable bitn-means-negativep)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Relationship between TC and NAT addition                          ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(prove-lemma plus-to-add nil
  (implies (and (tcp x)
                (tcp y)
                (tc-in-rangep x n)
                (tc-in-rangep y n))
           (equal (nat-to-tc (remainder (plus (carry c)
                                              (tc-to-nat x n)
                                              (tc-to-nat y n))
                                        (exp 2 n))
                             n)
                  (if (tc-in-rangep (add x (add y (carry c)))
                                    n)
                      (add x (add y (carry c)))
                      (if (negativep (add x (add y (carry c))))
                          (add x (add y (add (carry c) (exp 2 n))))
                          (add x (add y (add (carry c) (minus (exp 2 n))))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;      Fundamental Relationships between the Mapping Functions                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(prove-lemma bv-to-nat-to-bv (rewrite)
  (implies (equal size (size a))
           (equal (nat-to-bv (bv-to-nat a) size)
                  (fix-bv a))))

(prove-lemma bv-to-nat-to-tc (rewrite)
  (equal (bv-to-tc a) (nat-to-tc (bv-to-nat a) (size a)))
  
  ;HINT:
  ((use (bv-to-nat-to-tc-lemma1)
        (bv-to-nat-to-tc-lemma2))))

(disable bv-to-nat-to-tc)

(prove-lemma nat-to-bv-to-nat (rewrite)
  (equal (bv-to-nat (nat-to-bv n size))
         (remainder n (exp 2 size))))

(prove-lemma tc-to-bv-to-nat (rewrite)
  (implies (and (tcp x)
                (tc-in-rangep x n))
           (equal (tc-to-nat x n) (bv-to-nat (tc-to-bv x n)))))

(disable tc-to-bv-to-nat)

(prove-lemma bv-to-tc-to-nat (rewrite)
  (implies (equal n (size a))
           (equal (tc-to-nat (bv-to-tc a) n)
                  (bv-to-nat a))))

(disable bv-to-tc-to-nat)

(prove-lemma incr-compl-nat-to-bv-0 (rewrite)   ; SHOULD BE MOVED TO TC NUMBER OPER
  (equal (incr t (compl (nat-to-bv 0 (size x))))
         (nat-to-bv 0 (size x))))

(prove-lemma bitn-on-implies-non-0 (rewrite)    ; SHOULD BE MOVED TO TC NUMBER OPER
  (implies (bitn a n) (not (equal (bv-to-nat a) 0))))

(prove-lemma bv-to-tc-to-bv (rewrite)
  (implies (equal size (size a))
           (equal (tc-to-bv (bv-to-tc a) size)
                  (fix-bv a)))
  ((disable bv-to-nat-of-incr bv-to-nat-of-compl)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                                   Bridge Lemmas                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma embed-in-nat-to-bv nil
  (implies (equal x y) (equal (nat-to-bv x n) (nat-to-bv y n))))

(prove-lemma embed-in-tc-to-bv nil
  (implies (equal x y) (equal (tc-to-bv x n) (tc-to-bv y n))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                                   BV-ADDER                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defn bv-adder (c a b)
  (if (bitvp a)
      (if (equal a (btm))
          (bitv c (btm))
          (bitv (b-xor c (b-xor (bit a) (bit b)))
                (bv-adder (b-or (b-and (bit a) (bit b))
                                (b-or (b-and (bit a) c)
                                      (b-and (bit b) c)))
                          (vec a)
                          (vec b))))
      (bitv c (btm))))

(defn bv-adder-output (c a b)
  (trunc (bv-adder c a b) (size a)))

(defn bv-adder-carry-out (c a b)
  (bitn (bv-adder c a b) (add1 (size a))))

(defn bv-adder-overflowp (c a b)
  (b-and (b-equv (bitn a (size a)) (bitn b (size b)))
         (b-xor (bitn a (size a))
                (bitn (bv-adder-output c a b)
                      (size a)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                    Fundamental Properties of BV-ADDER                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma size-of-bv-adder (rewrite)
  (equal (size (bv-adder c a b))
         (add1 (size a))))

(prove-lemma bv-to-nat-of-bv-adder (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-to-nat (bv-adder c a b))
                  (plus (bv-to-nat a)
                        (bv-to-nat b)
                        (carry c)))))

; From here on we use only the above two lemmas about BV-ADDER
; The definition of BV-ADDER is disabled and henceforth any adder
; with the two properties above would suffice.

(disable bv-adder)

(prove-lemma bv-adder-non-btm (rewrite)
  (not (equal (bv-adder c a b) (btm)))
  
  ;HINT:
  ((use (size-of-bv-adder))
   (disable size-of-bv-adder)))

(prove-lemma size-bv-adder-output (rewrite)
  (equal (size (bv-adder-output c a b))
         (size a)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                 NAT view of BV-ADDER                                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma nat-interpretation-of-bv-adder-output (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-to-nat (bv-adder-output c a b))
                  (if (lessp (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                             (exp 2 (size a)))
                      (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                      (remainder (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                                 (exp 2 (size a)))))))

(disable nat-interpretation-of-bv-adder-output)

(prove-lemma nat-bv-adder-output-seen-as-bit-vector (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-adder-output c a b)
                  (if (lessp (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                             (exp 2 (size a)))
                      (nat-to-bv (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                                 (size a))
                      (nat-to-bv
                        (remainder (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                                   (exp 2 (size a)))
                        (size a)))))
  ((use (embed-in-nat-to-bv
          (x (bv-to-nat (bv-adder-output c a b)))
          (y (if (lessp (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                        (exp 2 (size a)))
                 (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                 (remainder (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                              (exp 2 (size a)))))
          (n (size a)))
        (nat-interpretation-of-bv-adder-output))
   (disable boolp bv-adder-output carry)))

(disable nat-bv-adder-output-seen-as-bit-vector)

(prove-lemma nat-interpretation-of-bv-adder-carry-out (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-adder-carry-out c a b)
                  (not (lessp (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                              (exp 2 (size a))))))
  
  ;HINT:
  ((use (upper-bound-on-non-negative-bv-to-nat
         (a (bv-adder c a b)))
        (lower-bound-on-negative-bv-to-nat
         (a (bv-adder c a b))))
   (disable bitn carry upper-bound-on-non-negative-bv-to-nat
            lower-bound-on-negative-bv-to-nat)))

(disable nat-interpretation-of-bv-adder-carry-out)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                      TC view of BV-ADDER                                     ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(prove-lemma tc-interpretation-of-bv-adder-output-lemma1 (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-to-tc (trunc (bv-adder c a b)
                                   (size a)))
                  (nat-to-tc (remainder (plus (carry c)
                                              (bv-to-nat a)
                                              (bv-to-nat b))
                                        (exp 2 (size a)))
                             (size a))))
  
  ;HINT:
  ((enable bv-to-nat-to-tc)
   (disable bv-to-tc tc-to-bv nat-to-tc tc-to-nat exp)))

(prove-lemma tc-interpretation-of-bv-adder-output (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (not (equal a (btm)))
                (not (equal b (btm)))
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-to-tc (bv-adder-output c a b))
                  (if (tc-in-rangep (add (bv-to-tc a)
                                         (add (bv-to-tc b) (carry c)))
                                    (size a))
                      (add (bv-to-tc a) (add (bv-to-tc b) (carry c)))
                      (if (negativep (add (bv-to-tc a)
                                          (add (bv-to-tc b) (carry c))))
                          (add (bv-to-tc a)
                               (add (bv-to-tc b)
                                    (add (carry c) (exp 2 (size a)))))
                          (add (bv-to-tc a)
                               (add (bv-to-tc b)
                                    (add (carry c) (minus (exp 2 (size a))))))))))
  
  ;HINT:
  ((use (plus-to-add (x (bv-to-tc a))
                     (y (bv-to-tc b))
                     (n (size a))))
   (enable bv-to-tc-to-nat)
   (disable boolp bv-to-tc trunc bv-adder size
            tc-in-rangep add carry exp
            nat-to-tc tc-to-nat tcp)))

(disable tc-interpretation-of-bv-adder-output-lemma1)
(disable tc-interpretation-of-bv-adder-output)

(prove-lemma tc-bv-adder-output-seen-as-bit-vector-lemma1 (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (not (equal a (btm)))
                (not (equal b (btm)))
                (equal (size a) (size b))
                (boolp c))
           (equal (tc-to-bv (bv-to-tc (bv-adder-output c a b))
                            (size (bv-adder-output c a b)))
                  (tc-to-bv (if (tc-in-rangep (add (bv-to-tc a)
                                                   (add (bv-to-tc b) (carry c)))
                                              (size a))
                                (add (bv-to-tc a) (add (bv-to-tc b) (carry c)))
                                (if (negativep (add (bv-to-tc a)
                                                    (add (bv-to-tc b) (carry c))))
                                    (add (bv-to-tc a)
                                         (add (bv-to-tc b)
                                              (add (carry c) (exp 2 (size a)))))
                                    (add (bv-to-tc a)
                                         (add (bv-to-tc b)
                                              (add (carry c)
                                                   (minus (exp 2 (size a))))))))
                            (size a))))
  ((use (embed-in-tc-to-bv
          (x (bv-to-tc (bv-adder-output c a b)))
          (y (if (tc-in-rangep (add (bv-to-tc a)
                                    (add (bv-to-tc b) (carry c)))
                               (size a))
                 (add (bv-to-tc a) (add (bv-to-tc b) (carry c)))
                 (if (negativep (add (bv-to-tc a)
                                     (add (bv-to-tc b) (carry c))))
                     (add (bv-to-tc a)
                          (add (bv-to-tc b)
                               (add (carry c) (exp 2 (size a)))))
                     (add (bv-to-tc a)
                          (add (bv-to-tc b)
                               (add (carry c) (minus (exp 2 (size a)))))))))
          (n (size (bv-adder-output c a b))))
        (size-bv-adder-output))
   (enable tc-interpretation-of-bv-adder-output)
   (disable bv-adder-output bv-to-tc tc-to-bv tc-in-rangep
            carry add exp boolp size-bv-adder-output)
   (hands-off bv-adder-output add tc-in-rangep)))

(disable tc-bv-adder-output-seen-as-bit-vector-lemma1)

(prove-lemma tc-bv-adder-output-seen-as-bit-vector (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (not (equal a (btm)))
                (not (equal b (btm)))
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-adder-output c a b)
                  (tc-to-bv (if (tc-in-rangep (add (bv-to-tc a)
                                                   (add (bv-to-tc b) (carry c)))
                                              (size a))
                                (add (bv-to-tc a) (add (bv-to-tc b) (carry c)))
                                (if (negativep (add (bv-to-tc a)
                                                    (add (bv-to-tc b) (carry c))))
                                    (add (bv-to-tc a)
                                         (add (bv-to-tc b)
                                              (add (carry c) (exp 2 (size a)))))
                                    (add (bv-to-tc a)
                                         (add (bv-to-tc b)
                                              (add (carry c)
                                                   (minus (exp 2 (size a))))))))
                            (size a))))
  ((use (bv-to-tc-to-bv (a (bv-adder-output c a b))
                        (size (size (bv-adder-output c a b))))
        (tc-bv-adder-output-seen-as-bit-vector-lemma1))
   (disable bv-adder-output bv-to-tc tc-to-bv tc-in-rangep carry add exp boolp
            size-bv-adder-output bv-to-tc-to-bv)
   (hands-off bv-adder-output add tc-in-rangep tc-to-bv if)))

(disable tc-bv-adder-output-seen-as-bit-vector)

(prove-lemma tc-interpretation-of-bv-adder-overflowp (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c)
                (not (equal a (btm)))
                (not (equal b (btm))))
           (equal (bv-adder-overflowp c a b)
                  (not (tc-in-rangep (add (bv-to-tc a)
                                          (add (bv-to-tc b) (carry c)))
                                     (size a)))))
  
  ;HINT:
  ((use (add-with-carry-of-negatives-is-negative
         (x (bv-to-tc a))
         (y (bv-to-tc b))
         (n (size a)))
        (add-with-carry-of-non-negatives-is-non-negative
         (x (bv-to-tc a))
         (y (bv-to-tc b))
         (n (size a))))
   (enable bitn-means-negativep tc-interpretation-of-bv-adder-output)
   (disable tc-in-rangep add bv-to-tc size carry boolp
            bv-adder-output)))

(disable tc-interpretation-of-bv-adder-overflowp)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Definitions and lemmas about subtraction functions                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;(defn bv-subtracter (c a b)    ; B - A - C
;  (bv-adder (b-not c) 
;            (bv-not a)
;            b))

(defn bv-subtracter-output (c a b)
  (bv-adder-output (b-not c) (bv-not a) b))

(defn bv-subtracter-carry-out (c a b)
  (b-not (bv-adder-carry-out (b-not c) (bv-not a) b)))

(defn bv-subtracter-overflowp (c a b)
  (bv-adder-overflowp (b-not c)
                      (bv-not a)
                      b))


(prove-lemma bv-not-is-compl (rewrite)
  (equal (bv-not a) (compl a)))

(prove-lemma subtract-lemma1 (rewrite)
  (implies (equal (size b) (size a))
           (equal (lessp (difference (bv-to-nat b) (bv-to-nat a))
                         (exp 2 (size a)))
                  t)))

(prove-lemma subtract-lemma2 (rewrite)
  (implies (and (not (zerop b))
                (not (lessp (sub1 b) a)))
           (equal (lessp (plus b (difference (sub1 n) a))
                         n)
                  f)))

(prove-lemma subtract-lemma3 (rewrite)  
  (implies (and (not (zerop b))
                (not (lessp (sub1 b) a))
                (lessp a n))
           (equal (difference (plus b (difference (sub1 n) a)) n)
                  (difference (sub1 b) a))))

(prove-lemma subtract-lemma4 (rewrite)
  (implies (equal (size b) (size a))
           (equal (lessp (difference (sub1 (bv-to-nat b)) (bv-to-nat a))
                         (exp 2 (size a)))
                  t)))

(prove-lemma size-bv-subtracter-output (rewrite)
  (equal (size (bv-subtracter-output c a b))
         (size a)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                 NAT view of BV-SUBTRACTER                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma nat-interpretation-of-bv-subtracter-output (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-to-nat (bv-subtracter-output c a b))
                  (if (not (lessp (bv-to-nat b)
                                  (plus (bv-to-nat a) (carry c))))
                      (difference (bv-to-nat b)
                                  (plus (bv-to-nat a) (carry c)))
                      (difference (exp 2 (size a))
                                  (difference (plus (bv-to-nat a) (carry c))
                                              (bv-to-nat b)))))))

(disable nat-interpretation-of-bv-subtracter-output)

(prove-lemma nat-bv-subtracter-output-seen-as-bit-vector (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-subtracter-output c a b)
                  (if (not (lessp (bv-to-nat b)
                                  (plus (bv-to-nat a) (carry c))))
                      (nat-to-bv (difference (bv-to-nat b)
                                             (plus (bv-to-nat a) (carry c)))
                                 (size a))
                      (nat-to-bv (difference (exp 2 (size a))
                                             (difference (plus (bv-to-nat a)
                                                               (carry c))
                                                         (bv-to-nat b)))
                                 (size a)))))
  ((use (embed-in-nat-to-bv
          (x (bv-to-nat (bv-subtracter-output c a b)))
          (y (if (not (lessp (bv-to-nat b)
                             (plus (bv-to-nat a) (carry c))))
                 (difference (bv-to-nat b)
                             (plus (bv-to-nat a) (carry c)))
                 (difference (exp 2 (size a))
                             (difference (plus (bv-to-nat a)
                                               (carry c))
                                         (bv-to-nat b)))))
          (n (size a)))
        (nat-interpretation-of-bv-subtracter-output))
   (disable boolp bv-subtracter-output carry exp difference)))

(disable nat-bv-subtracter-output-seen-as-bit-vector)

(prove-lemma equal-lessp-hack (rewrite)
  (equal (equal (lessp x y) z)
         (if (lessp x y)
             (equal z t)
             (equal z f))))

(prove-lemma nat-interpretation-of-bv-subtracter-carry-out (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-subtracter-carry-out c a b)
                  (lessp (bv-to-nat b)
                         (plus (bv-to-nat a) (carry c)))))
  ((enable nat-to-bv-to-nat nat-interpretation-of-bv-adder-carry-out)
   (disable size-bv-subtracter-output)))

(disable nat-interpretation-of-bv-subtracter-carry-out)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                      TC view of BV-SUBTRACTER                                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn tc-minus (x)
  (if (negativep x)
      (negative-guts x)
      (if (zerop x) 0 (minus x))))

(prove-lemma tc-minus-add (rewrite)
  (equal (tc-minus (add x y)) (add (tc-minus x) (tc-minus y))))

(prove-lemma bitn-compl (rewrite)
  (implies (and (not (zerop n))
                (not (lessp (size a) n)))
           (equal (bitn (compl a) n) (not (bitn a n)))))

;(prove-lemma bitn-on-implies-non-0 (rewrite)
;  (implies (bitn a n) (not (equal (bv-to-nat a) 0))))

(prove-lemma equal-difference-0 (rewrite)
  (equal (equal (difference x y) 0)
         (not (lessp y x))))

(prove-lemma top-bit-off-implies-smaller (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm)))
                (not (bitn a (size a))))
           (lessp (bv-to-nat a) (sub1 (exp 2 (size a))))))

(prove-lemma tc-minus-bv-to-tc (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm))))
           (equal (tc-minus (bv-to-tc a))
                  (if (equal (bv-to-tc a) 0)
                      0
                      (add 1 (bv-to-tc (compl a)))))))

(defn tc-fix (x)
  (if (tcp x) x 0))

(prove-lemma tcp-add (rewrite)
  (and (implies (tcp x) (tcp (add x y)))
       (implies (tcp y) (tcp (add x y)))))

(prove-lemma add-0 (rewrite)
  (equal (add 0 x) (tc-fix x)))

(prove-lemma add-1-1 (rewrite)
  (equal (add 1 (add -1 x)) (tc-fix x)))

(prove-lemma bv-to-tc-compl-0 (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm)))
                (equal (bv-to-tc a) 0))
           (equal (bv-to-tc (compl a)) -1)))

(prove-lemma tc-minus-add-carry (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm))))
           (equal (tc-minus (add (bv-to-tc a) (carry c)))
                  (add (bv-to-tc (compl a)) (carry (not c)))))
  ((disable add bv-to-tc tc-minus tcp)))

(prove-lemma boolp-b-not (rewrite)
  (boolp (b-not x)))

(prove-lemma compl-not-btm (rewrite)
  (equal (equal (compl a) (btm))
         (or (not (bitvp a)) (equal a (btm)))))

(prove-lemma tc-interpretation-of-bv-subtracter-output (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (not (equal a (btm)))
                (not (equal b (btm)))
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-to-tc (bv-subtracter-output c a b))
                  (if (tc-in-rangep (add (bv-to-tc b)
                                         (tc-minus (add (bv-to-tc a)
                                                        (carry c))))
                                    (size a))
                      (add (bv-to-tc b) (tc-minus (add (bv-to-tc a)
                                                       (carry c))))
                      (if (negativep (add (bv-to-tc b)
                                          (tc-minus (add (bv-to-tc a)
                                                         (carry c)))))
                          (add (bv-to-tc b)
                               (add (exp 2 (size a))
                                    (tc-minus (add (bv-to-tc a)
                                                   (carry c)))))
                          (add (bv-to-tc b)
                               (add (minus (exp 2 (size a)))
                                    (tc-minus (add (bv-to-tc a)
                                                   (carry c)))))
                          ))))
  ((disable add carry boolp tc-minus bv-to-tc tc-in-rangep bv-adder-output
            tc-minus-add tc-minus-bv-to-tc)
   (enable tc-interpretation-of-bv-adder-output)))

(disable tc-interpretation-of-bv-subtracter-output)


(prove-lemma tc-bv-subtracter-output-seen-as-bit-vector-lemma1 (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (not (equal a (btm)))
                (not (equal b (btm)))
                (equal (size a) (size b))
                (boolp c))
           (equal (tc-to-bv (bv-to-tc (bv-subtracter-output c a b))
                            (size (bv-subtracter-output c a b)))
                  (tc-to-bv (if (tc-in-rangep (add (bv-to-tc b)
                                                   (tc-minus (add (bv-to-tc a)
                                                                  (carry c))))
                                              (size a))
                                (add (bv-to-tc b) (tc-minus (add (bv-to-tc a)
                                                                 (carry c))))
                                (if (negativep (add (bv-to-tc b)
                                                    (tc-minus (add (bv-to-tc a)
                                                              (carry c)))))
                                    (add (bv-to-tc b)
                                         (add (exp 2 (size a))
                                              (tc-minus (add (bv-to-tc a)
                                                             (carry c)))))
                                    (add (bv-to-tc b)
                                         (add (minus (exp 2 (size a)))
                                              (tc-minus (add (bv-to-tc a)
                                                             (carry c)))))))
                            (size a))))
  ((use (embed-in-tc-to-bv
          (x (bv-to-tc (bv-subtracter-output c a b)))
          (y (if (tc-in-rangep (add (bv-to-tc b)
                                                   (tc-minus (add (bv-to-tc a)
                                                                  (carry c))))
                                              (size a))
                                (add (bv-to-tc b) (tc-minus (add (bv-to-tc a)
                                                                 (carry c))))
                                (if (negativep (add (bv-to-tc b)
                                                    (tc-minus (add (bv-to-tc a)
                                                                   (carry c)))))
                                    (add (bv-to-tc b)
                                         (add (exp 2 (size a))
                                              (tc-minus (add (bv-to-tc a)
                                                             (carry c)))))
                                    (add (bv-to-tc b)
                                         (add (minus (exp 2 (size a)))
                                              (tc-minus (add (bv-to-tc a)
                                                             (carry c))))))))
          (n (size (bv-subtracter-output c a b))))
        (size-bv-subtracter-output))
   (enable tc-interpretation-of-bv-subtracter-output)
   (disable add carry boolp tc-minus bv-to-tc tc-in-rangep bv-adder-output
            tc-minus-add tc-minus-bv-to-tc)
   (hands-off bv-subtracter-output add tc-in-rangep)))

(disable tc-bv-subtracter-output-seen-as-bit-vector-lemma1)

(prove-lemma tc-bv-subtracter-output-seen-as-bit-vector (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (not (equal a (btm)))
                (not (equal b (btm)))
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-subtracter-output c a b)
                  (if (tc-in-rangep (add (bv-to-tc b)
                                         (tc-minus (add (bv-to-tc a)
                                                        (carry c))))
                                    (size a))
                      (tc-to-bv (add (bv-to-tc b) (tc-minus (add (bv-to-tc a)
                                                                 (carry c))))
                                (size a))
                      (if (negativep (add (bv-to-tc b)
                                          (tc-minus (add (bv-to-tc a)
                                                         (carry c)))))
                          (tc-to-bv (add (bv-to-tc b)
                                         (add (exp 2 (size a))
                                              (tc-minus (add (bv-to-tc a)
                                                             (carry c)))))
                                    (size a))
                          (tc-to-bv (add (bv-to-tc b)
                                         (add (minus (exp 2 (size a)))
                                              (tc-minus (add (bv-to-tc a)
                                                             (carry c)))))
                                    (size a))))))
  ((use (tc-bv-subtracter-output-seen-as-bit-vector-lemma1))
   (disable add carry boolp tc-minus bv-to-tc tc-in-rangep bv-subtracter-output
            tc-minus-add tc-minus-bv-to-tc tc-to-bv tc-minus-add-carry)))

(disable tc-bv-subtracter-output-seen-as-bit-vector)

(prove-lemma tc-interpretation-of-bv-subtracter-overflowp (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (not (equal a (btm)))
                (not (equal b (btm)))
                (equal (size a) (size b))
                (boolp c))
           (equal (bv-subtracter-overflowp c a b)
                  (not (tc-in-rangep (add (bv-to-tc b)
                                          (tc-minus (add (bv-to-tc a)
                                                         (carry c))))
                                     (size a)))))
  ((disable add carry boolp tc-minus bv-to-tc tc-in-rangep bv-adder-output
            tc-minus-add tc-minus-bv-to-tc)
   (enable tc-interpretation-of-bv-adder-overflowp)))

(disable tc-interpretation-of-bv-subtracter-overflowp)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Definitions and lemmas for shift and rotate functions             ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn v-append (a b)            ; Append two bit vectors
  (if (bitvp a)
      (if (equal a (btm))
          b
          (bitv (bit a)
                (v-append (vec a) b)))
      b))

(defn v-lsr (a)                 ; Vector logical shift right
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (v-append (vec a) (bitv f (btm))))
      (btm)))

(defn v-lsl (a)                 ; Vector logical shift left
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (v-append (bitv f (btm)) (trunc a (sub1 (size a)))))
      (btm)))

(defn v-asr (a)                 ; Vector arithmetic shift right
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (v-append (vec a) (bitv (bitn a (size a)) (btm))))
      (btm)))

(defn v-asl (a)                 ; Vector arithmetric shift left
  (v-lsl a))

(defn v-ror (a c)               ; Vector rotate right
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (v-append (vec a) (bitv c (btm))))
      (btm)))

(defn v-rol (a c)               ; Vector rotate left
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (v-append (bitv c (btm)) (trunc a (sub1 (size a)))))
      (btm)))

(defn bv-append (a b) (v-append a b))

(defn bv-lsr (a) (v-lsr a))

(defn bv-asr (a) (v-asr a))

(defn bv-ror (a c) (v-ror a c))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Natural and two's complement interpretation of shifters           ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma bv-to-nat-v-append (rewrite)
  (equal (bv-to-nat (v-append a b))
         (plus (bv-to-nat a) (times (bv-to-nat b) (exp 2 (size a))))))

(prove-lemma bv-lsr-divides-by-two-lemma (rewrite)
  (equal (v-lsr a)
         (nat-to-bv (quotient (bv-to-nat a) 2)
                    (size a))))

(defn mod2 (x)
  (if (negativep x)
      (minus (quotient (add1 (negative-guts x)) 2))
      (quotient x 2)))

(prove-lemma bitvp-v-append (rewrite)
  (equal (bitvp (v-append a b))
         (if (bitvp a)
             (or (not (equal a (btm))) (bitvp b))
             (bitvp b))))

(prove-lemma bitn-v-append (rewrite)
  (equal (bitn (v-append a b) n)
         (if (lessp (size a) n)
             (bitn b (difference n (size a)))
             (bitn a n))))

(prove-lemma size-v-append (rewrite)
  (equal (size (v-append a b)) (plus (size a) (size b))))

(prove-lemma difference-x-x-1 (rewrite)
  (equal (difference x (sub1 x))
         (if (zerop x) 0 1)))

(prove-lemma bv-to-nat-of-twos-compl (rewrite)
  (equal (bv-to-nat (incr t (compl a)))
         (if (equal (bv-to-nat a) 0)
             0
             (difference (exp 2 (size a)) (bv-to-nat a)))))

(prove-lemma difference-2x-x (rewrite)
  (equal (difference (times 2 y) (plus x y))
         (difference y x)))

(prove-lemma quotient-crock1 (rewrite)
  (equal (quotient (add1 (difference (times 2 y) (times 2 x))) 2)
         (difference y x)))

(prove-lemma add1-difference-sub1 (rewrite)
  (equal (add1 (difference (sub1 x) y))
         (if (lessp y x)
             (difference x y)
             1)))

(prove-lemma quotient-crock2 (rewrite)
  (equal (quotient (difference (times 2 y) (times 2 x)) 2)
         (difference y x)))

(prove-lemma bv-asr-divides-by-two (rewrite)
  (equal (bv-to-tc (bv-asr a))
         (mod2 (bv-to-tc a))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Definitions and lemmas about hardware if                          ;;
;;            and constructor for ALU result                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn b-if (c a b)              ; Binary if
 (b-nand (b-nand c a)
         (b-nand (b-not c) b)))

(defn bv-if (c a b)             ; Bit-vector if
  (if (bitvp a)
      (if (equal a (btm))
          (btm)
          (bitv (b-if c (bit a) (bit b))
                (bv-if c (vec a) (vec b))))
      (btm)))

(prove-lemma bv-if-works (rewrite)
  (equal (bv-if c a b)
         (if c (if (bitvp a) a (btm)) (trunc b (size a)))))

(add-shell bv-cv nil bv-cvp ((bv (one-of bitvp) btm)
                             (c  (one-of truep falsep) false)
                             (v  (one-of truep falsep) false)))

(defn bv-cv-if (c a b)          ; Bit-vector, carry, and overflow if
  (bv-cv (bv-if c (bv a) (bv b))
         (b-if  c (c a)  (c b))
         (b-if  c (v a)  (v b))))

(prove-lemma trunc-size (rewrite)
  (implies (and (bitvp b)
                (equal (size b) (size a)))
           (equal (trunc b (size a)) b))
  ((induct (bv-and a b))))

(prove-lemma bv-cv-if-works (rewrite)
  (implies (and (bv-cvp a)
                (bv-cvp b)
                (equal (size (bv a)) (size (bv b))))
           (and (equal (bv-cv-if t a b) a)
                (equal (bv-cv-if f a b) b))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            SIZE lemmas                                                       ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma size-bv-bv-cv-if (rewrite)
  (equal (size (bv (bv-cv-if c a b))) (size (bv a))))

; We rewrite "bv-not" to "v-not", etc., and so we need these size lemmas about
; the v-functions.

(prove-lemma size-v-not (rewrite)
  (equal (size (v-not a)) (size a)))

(prove-lemma size-v-and (rewrite)
  (equal (size (v-and a b)) (size a)))

(prove-lemma size-v-or (rewrite)
  (equal (size (v-or a b)) (size a)))

(prove-lemma size-v-xor (rewrite)
  (equal (size (v-xor a b)) (size a)))

(prove-lemma size-v-append-1 (rewrite)
  (equal (size
           (if (bitvp a)
               (if (equal a (btm))
                   (btm)
                   (v-append (vec a) (bitv x (btm))))
               (btm)))
         (size a)))

(prove-lemma size-v-append-2 (rewrite)
  (equal (size (v-append (vec a) (bitv x (btm))))
         (if (bitvp a)
             (if (equal a (btm))
                 1
                 (size a))
             1)))

;  We have already proved (SIZE (BV-ADDER-OUTPUT C A B)) = (SIZE A) and
;                         (SIZE (BV-SUBTRACTER-OUTPUT C A B)) = (SIZE A).

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            ALU definition                                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(disable bv-cv-if)

(defn bv-alu-cv (a b c op-code)
  (bv-cv-if (bitn op-code 4)
    (bv-cv-if (bitn op-code 3)
      (bv-cv-if (bitn op-code 2)
        (bv-cv-if (bitn op-code 1)
                  (bv-cv a                              ; Op-code 15 - move
                         f
                         f)
                  (bv-cv (bv-not a)                     ; Op-code 14 - not
                         f
                         f))
        (bv-cv-if (bitn op-code 1)
                  (bv-cv (bv-and a b)                   ; Op-code 13 - and
                         f
                         f)
                  (bv-cv (bv-or a b)                    ; Op-code 12 - or
                         f
                         f)))
      (bv-cv-if (bitn op-code 2)
        (bv-cv-if (bitn op-code 1)
                  (bv-cv (bv-xor a b)                   ; Op-code 11 - xor
                         f
                         f)
                  (bv-cv (bv-lsr a)                     ; Op-code 10 - lsr
                         (bitn a 1)
                         f))
        (bv-cv-if (bitn op-code 1)
                  (bv-cv (bv-asr a)                     ; Op-code 9 - asr
                         (bitn a 1)
                         f)
                  (bv-cv (bv-ror a c)                   ; Op-code 8 - ror
                         (if (zerop (size a))
                             c
                             (bitn a 1))
                         f))))
    (bv-cv-if (bitn op-code 3)
      (bv-cv-if (bitn op-code 2)
        (bv-cv-if (bitn op-code 1)
                  (bv-cv (bv-subtracter-output f a b)   ; Op-code 7 - sub
                         (bv-subtracter-carry-out f a b)        
                         (bv-subtracter-overflowp f a b))
                  (bv-cv (bv-subtracter-output c a b)   ; Op-code 6 - subb
                         (bv-subtracter-carry-out c a b)        
                         (bv-subtracter-overflowp c a b)))
        (bv-cv-if (bitn op-code 1)                      ; Op-code 5 - dec
                  (bv-cv (bv-subtracter-output t (nat-to-bv 0 (size a)) a)
                         (bv-subtracter-carry-out t (nat-to-bv 0 (size a)) a)
                         (bv-subtracter-overflowp t (nat-to-bv 0 (size a)) a))
                                                        ; Op-code 4 - neg
                  (bv-cv (bv-subtracter-output f a (nat-to-bv 0 (size a)))
                         (bv-subtracter-carry-out f a (nat-to-bv 0 (size a)))
                         (bv-subtracter-overflowp f a (nat-to-bv 0 (size a))))))
      (bv-cv-if (bitn op-code 2)
        (bv-cv-if (bitn op-code 1)
                  (bv-cv (bv-adder-output f a b)        ; Op-code 3 - add
                         (bv-adder-carry-out f a b)
                         (bv-adder-overflowp f a b))
                  (bv-cv (bv-adder-output c a b)        ; Op-code 2 - addc
                         (bv-adder-carry-out c a b)
                         (bv-adder-overflowp c a b)))
        (bv-cv-if (bitn op-code 1)                      ; Op-code 1 - inc
                  (bv-cv (bv-adder-output t a (nat-to-bv 0 (size a)))
                         (bv-adder-carry-out t a (nat-to-bv 0 (size a)))
                         (bv-adder-overflowp t a (nat-to-bv 0 (size a))))
                  (bv-cv a                              ; Op-code 0 - nop, move
                         f
                         f))))))

(prove-lemma v-not-is-compl (rewrite)
  (equal (v-not a) (compl a)))

(prove-lemma bv-and-is-v-and (rewrite)
  (equal (bv-and a b) (v-and a b)))

(prove-lemma bv-or-is-v-or (rewrite)
  (equal (bv-or a b) (v-or a b)))

(prove-lemma bv-xor-is-v-xor (rewrite)
  (equal (bv-xor a b) (v-xor a b)))

(prove-lemma bv-cv-if-reduce (rewrite)
  (equal (bv-cv-if c
                   (bv-cv x y z)
                   (bv-cv x y z))
         (bv-cv x y z))
  ((enable bv-cv-if)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           BV-ALU with theorem-prover "ifs".  This was done to speed the      ;;
;;           rewriting when proving the large lemmas that follow.               ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma bv-alu-cv-with-ifs (rewrite)
  (implies
    (and (bitvp a)
         (bitvp b)
         (equal (size a) (size b)))
    (equal
      (bv-alu-cv a b c op-code)
      (if (bitn op-code 4)
          (if (bitn op-code 3)
              (if (bitn op-code 2)
                  (if (bitn op-code 1)
                      (bv-cv a                  ; Op-code 15 - move
                             f
                             f)
                      (bv-cv (bv-not a)         ; Op-code 14 - not
                             f
                             f))
                  (if (bitn op-code 1)
                      (bv-cv (bv-and a b)       ; Op-code 13 - and
                             f
                             f)
                      (bv-cv (bv-or a b)        ; Op-code 12 - or
                             f
                             f)))
              (if (bitn op-code 2)
                  (if (bitn op-code 1)
                      (bv-cv (bv-xor a b)       ; Op-code 11 - xor
                             f
                             f)
                      (bv-cv (bv-lsr a)         ; Op-code 10 - lsr
                             (bitn a 1)
                             f))
                  (if (bitn op-code 1)
                      (bv-cv (bv-asr a)         ; Op-code 9 - asr
                             (bitn a 1)
                             f)
                      (bv-cv (bv-ror a c)       ; Op-code 8 - ror
                             (if (zerop (size a))
                                 c
                                 (bitn a 1))
                             f))))
          (if (bitn op-code 3)
              (if (bitn op-code 2)
                  (if (bitn op-code 1)
                      (bv-cv (bv-subtracter-output f a b)       ; Op-code 7 - sub
                             (bv-subtracter-carry-out f a b)    
                             (bv-subtracter-overflowp f a b))
                      (bv-cv (bv-subtracter-output c a b)       ; Op-code 6 - subb
                             (bv-subtracter-carry-out c a b)    
                             (bv-subtracter-overflowp c a b)))
                  (if (bitn op-code 1)          ; Op-code 5 - dec
                      (bv-cv (bv-subtracter-output t (nat-to-bv 0 (size a)) a)
                             (bv-subtracter-carry-out t (nat-to-bv 0 (size a)) a)
                             (bv-subtracter-overflowp t (nat-to-bv 0 (size a)) a))
                                                ; Op-code 4 - neg
                      (bv-cv (bv-subtracter-output f a (nat-to-bv 0 (size a)))
                             (bv-subtracter-carry-out f a (nat-to-bv 0 (size a)))
                             (bv-subtracter-overflowp f a (nat-to-bv 0 (size a))))))
              (if (bitn op-code 2)
                  (if (bitn op-code 1)
                      (bv-cv (bv-adder-output f a b)    ; Op-code 3 - add
                             (bv-adder-carry-out f a b)
                             (bv-adder-overflowp f a b))
                      (bv-cv (bv-adder-output c a b)    ; Op-code 2 - addc
                             (bv-adder-carry-out c a b)
                             (bv-adder-overflowp c a b)))
                  (if (bitn op-code 1)          ; Op-code 1 - inc
                      (bv-cv (bv-adder-output t a (nat-to-bv 0 (size a)))
                             (bv-adder-carry-out t a (nat-to-bv 0 (size a)))
                             (bv-adder-overflowp t a (nat-to-bv 0 (size a))))
                      (bv-cv a                  ; Op-code 0 - nop, move
                             f
                             f)))))))
  ((disable bv-adder-output bv-adder-carry-out bv-adder-overflowp
            bv-subtracter-output bv-subtracter-carry-out bv-subtracter-overflowp
            nat-to-bv-to-nat remainder-of-0 carry)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Boolean ALU help lemmas                                            ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma nat-to-bv-of-2i (rewrite)
  (implies (boolp c)
           (equal (nat-to-bv (plus (carry c) (plus i i)) n)
                  (if (zerop n)
                      (btm)
                      (bitv c (nat-to-bv i (sub1 n)))))))

(prove-lemma nat-to-bv-to-nat-wrong-size (rewrite)
  (equal (nat-to-bv (bv-to-nat a) n)
         (trunc a n)))

(prove-lemma nat-to-bv-ignores-remainder (rewrite)
  (equal (nat-to-bv (remainder i (exp 2 n)) n)
         (nat-to-bv i n)))

(disable nat-to-bv-ignores-remainder)

(prove-lemma bv-adder-as-shifter (rewrite)
  (implies (and (bitvp a) (boolp c))
           (equal (bv-adder c a a)
                  (nat-to-bv (plus (bv-to-nat a)
                                   (bv-to-nat a)
                                   (carry c))
                             (add1 (size a)))))
  ((use (embed-in-nat-to-bv (x (bv-to-nat (bv-adder c a a)))
                            (y (plus (bv-to-nat a)
                                     (bv-to-nat a)
                                     (carry c)))
                            (n (add1 (size a))))
        (bv-to-nat-of-bv-adder (b a)))
   (disable nat-to-bv-to-nat-wrong-size bv-to-nat-of-bv-adder)))

(prove-lemma bv-adder-output-used-as-asl (rewrite)
  (implies (and (bitvp a)
                (boolp c))
           (equal (bv-adder-output c a a)
                  (if (equal a (btm))
                      (btm)
                      (bitv c (trunc a (sub1 (size a))))))))
             
(disable bv-adder-output-used-as-asl)
             
(prove-lemma bitn-equiv-lessp (rewrite)
  (implies (bitvp a)
           (equal (bitn a (size a))
                  (not (lessp (bv-to-nat a) (exp 2 (sub1 (size a))))))))
             
(prove-lemma bv-adder-carry-out-used-as-asl (rewrite)
  (implies (and (bitvp a)
                (boolp c))
           (equal (bv-adder-carry-out c a a)
                  (if (zerop (size a))
                      c
                      (bitn a (size a))))))
             
(disable bv-adder-carry-out-used-as-asl)

(disable bv-adder-as-shifter)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Boolean operation of ALU                                           ;; 
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
             
             
(prove-lemma bv-alu-cv-correct-boolean nil
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))
           
           (and (equal (bv-alu-cv a b c (nat-to-bv 15 4))       ; Move
                       (bv-cv a f f))
                
                (equal (bv-alu-cv a b c (nat-to-bv 14 4))       ; Not
                       (bv-cv (v-not a) f f))
                
                (equal (bv-alu-cv a b c (nat-to-bv 13 4))       ; And
                       (bv-cv (v-and a b) f f))
                
                (equal (bv-alu-cv a b c (nat-to-bv 12 4))       ; Or
                       (bv-cv (v-or a b) f f))
                
                (equal (bv-alu-cv a b c (nat-to-bv 11 4))       ; Xor
                       (bv-cv (v-xor a b) f f))
                
                (equal (bv-alu-cv a b c (nat-to-bv 10 4))       ; Lsr
                       (bv-cv (v-lsr a)
                              (bitn a 1)
                              f))
                
                (equal (bv-alu-cv a b c (nat-to-bv 9 4))        ; Asr
                       (bv-cv (v-asr a)
                              (bitn a 1)
                              f))
                
                (equal (bv-alu-cv a b c (nat-to-bv 8 4))        ; Ror
                       (bv-cv (v-ror a c)
                              (if (zerop (size a))
                                  c
                                  (bitn a 1))
                              f))
                
                (implies (equal a b)            ; Lsl
                         (and (equal (bv (bv-alu-cv a b c (nat-to-bv 3 4)))
                                     (v-lsl a))
                              (equal (c (bv-alu-cv a b c (nat-to-bv 3 4)))
                                     (bitn a (size a)))))
                
                (implies (equal a b)            ; Asl
                         (and (equal (bv (bv-alu-cv a b c (nat-to-bv 3 4)))
                                     (v-asl a))
                              (equal (c (bv-alu-cv a b c (nat-to-bv 3 4)))
                                     (bitn a (size a)))))
                
                (implies (equal a b)            ; Rol
                         (and (equal (bv (bv-alu-cv a b c (nat-to-bv 2 4)))
                                     (v-rol a c))
                              (equal (c (bv-alu-cv a b c (nat-to-bv 2 4)))
                                     (if (zerop (size a))
                                         c
                                         (bitn a (size a))))))))
  ((disable bv-adder-output bv-adder-carry-out bv-adder-overflowp
            bv-subtracter-output bv-subtracter-carry-out bv-subtracter-overflowp)
   (enable bv-adder-output-used-as-asl bv-adder-carry-out-used-as-asl)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Natural number ALU help lemmas                                     ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

                
(prove-lemma v-append-quotient (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm))))
           (equal (nat-to-bv (quotient (bv-to-nat a) 2)
                             (size a))
                  (v-append (vec a)
                            (bitv f (btm))))))

(prove-lemma bit-interpretation-of-even-and-odd (rewrite)
  (equal (equal (remainder (bv-to-nat a) 2) 0)
         (not (bit a))))

(prove-lemma nat-to-bv-to-nat-hidden-to-accomodate-hands-off (rewrite)
  (equal (difference x
                     (bv-to-nat (nat-to-bv 0 n)))
         (fix x)))

(prove-lemma zero-not-less-than-anything (rewrite)
  (not (lessp (sub1 (bv-to-nat a))
              (bv-to-nat (nat-to-bv 0 (size a))))))

(prove-lemma nat-interpretation-of-inc-bit-vector (rewrite)
  (implies (bitvp a)
           (equal (bv-adder-output t a (nat-to-bv 0 (size a)))
                  (if (lessp (add1 (bv-to-nat a))
                             (exp 2 (size a)))
                      (nat-to-bv (add1 (bv-to-nat a)) (size a))
                      (nat-to-bv 0 (size a)))))
  ((disable pathological-difference boolp v-lsr
            bv-adder-output bv-adder-carry-out bv-adder-overflowp
            bv-subtracter-output bv-subtracter-carry-out bv-subtracter-overflowp)
   (enable nat-bv-adder-output-seen-as-bit-vector)))

(disable nat-interpretation-of-inc-bit-vector)

(prove-lemma nat-interpretation-of-inc-carry-out (rewrite)
  (implies (bitvp a)
           (equal (bv-adder-carry-out t a (nat-to-bv 0 (size a)))    ; Inc - carry
                  (not (lessp (add1 (bv-to-nat a))
                              (exp 2 (size a))))))
  ((disable pathological-difference boolp v-lsr
            bv-adder-output bv-adder-carry-out bv-adder-overflowp
            bv-subtracter-output bv-subtracter-carry-out bv-subtracter-overflowp)
   (enable nat-interpretation-of-bv-adder-carry-out)))

(disable nat-interpretation-of-inc-carry-out)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Natural number operation of ALU                                    ;; 
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma bv-alu-cv-correct-natural-number nil
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b))
                (boolp c))

           (and (equal (bv-alu-cv a b c (nat-to-bv 10 4))               ; Lsr
                       (bv-cv (nat-to-bv (quotient (bv-to-nat a) 2)
                                         (size a))
                              (not (zerop (remainder (bv-to-nat a) 2)))
                              f))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 7 4)))   ; Sub - bv
                       (if (not (lessp (bv-to-nat b)
                                       (bv-to-nat a)))
                           (nat-to-bv (difference (bv-to-nat b)
                                                  (bv-to-nat a))
                                      (size a))
                           (nat-to-bv (difference (exp 2 (size a))
                                       (difference (bv-to-nat a)
                                                   (bv-to-nat b)))
                                      (size a))))

                (equal (c (bv-alu-cv a b c (nat-to-bv 7 4)))    ; Sub - carry
                       (lessp (bv-to-nat b) (bv-to-nat a)))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 6 4)))   ; Subb - bv
                       (if (not (lessp (bv-to-nat b)
                                       (plus (bv-to-nat a) (carry c))))
                           (nat-to-bv (difference (bv-to-nat b)
                                                  (plus (bv-to-nat a) (carry c)))
                                      (size a))
                           (nat-to-bv (difference (exp 2 (size a))
                                                  (difference (plus (bv-to-nat a)
                                                                    (carry c))
                                                              (bv-to-nat b)))
                                      (size a))))

                (equal (c (bv-alu-cv a b c (nat-to-bv 6 4)))    ; Subb - carry
                       (lessp (bv-to-nat b)
                              (plus (bv-to-nat a) (carry c))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 5 4)))   ; Dec - bv
                       (if (zerop (bv-to-nat a))
                           (nat-to-bv (sub1 (exp 2 (size a)))
                                      (size a))
                           (nat-to-bv (sub1 (bv-to-nat a))
                                      (size a))))

                (equal (c (bv-alu-cv a b c (nat-to-bv 5 4)))    ; Dec - carry
                       (zerop (bv-to-nat a)))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 3 4)))   ; Add - bv
                       (if (lessp (plus (bv-to-nat a) (bv-to-nat b))
                                  (exp 2 (size a)))
                           (nat-to-bv (plus (bv-to-nat a) (bv-to-nat b))
                                      (size a))
                           (nat-to-bv
                             (remainder (plus (bv-to-nat a) (bv-to-nat b))
                                        (exp 2 (size a)))
                             (size a))))

                (equal (c (bv-alu-cv a b c (nat-to-bv 3 4)))    ; Add - carry
                       (not (lessp (plus (bv-to-nat a) (bv-to-nat b))
                                   (exp 2 (size a)))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 2 4)))   ; Addc - bv
                       (if (lessp (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                                  (exp 2 (size a)))
                           (nat-to-bv (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                                      (size a))
                           (nat-to-bv
                             (remainder (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                                        (exp 2 (size a)))
                             (size a))))

                (equal (c (bv-alu-cv a b c (nat-to-bv 2 4)))    ; Addc - carry
                       (not (lessp (plus (bv-to-nat a) (bv-to-nat b) (carry c))
                                   (exp 2 (size a)))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 1 4)))   ; Inc - bv
                       (if (lessp (add1 (bv-to-nat a))
                                  (exp 2 (size a)))
                           (nat-to-bv (add1 (bv-to-nat a)) (size a))
                           (nat-to-bv 0 (size a))))

                (equal (c (bv-alu-cv a b c (nat-to-bv 1 4)))    ; Inc - carry
                       (not (lessp (add1 (bv-to-nat a))
                                   (exp 2 (size a)))))))
  ((disable pathological-difference boolp v-lsr
            bv-adder-output bv-adder-carry-out bv-adder-overflowp
            bv-subtracter-output bv-subtracter-carry-out bv-subtracter-overflowp
            nat-to-bv-to-nat)
   (hands-off bv-to-nat nat-to-bv)
   (enable nat-interpretation-of-inc-carry-out
           nat-interpretation-of-inc-bit-vector
           nat-interpretation-of-bv-subtracter-carry-out
           nat-bv-subtracter-output-seen-as-bit-vector
           nat-interpretation-of-bv-adder-carry-out
           nat-bv-adder-output-seen-as-bit-vector)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Two's complement ALU help lemmas                                   ;; 
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma twos-complement-twos-complement (rewrite)
  (implies (bitvp a)
           (equal (incr t (compl (incr t (compl a))))
                  a)))

(prove-lemma tc-to-bv-to-tc-negative (rewrite)
  (implies (and (bitvp a)
                (equal (size a) n))
           (equal (tc-to-bv (bv-to-tc a) n)
                  a))
  ((disable bv-to-nat-of-twos-compl bitn-equiv-lessp bv-to-nat-of-incr
            bv-to-nat-of-compl all-onesp-of-compl bitn-on-implies-non-0)))

(prove-lemma v-asr-is-a-bitv (rewrite)
  (bitvp (v-asr a)))

(prove-lemma size-of-v-asr nil
  (equal (size (v-asr a))
         (size a)))

(prove-lemma bv-asr-divides-by-two-bridge (rewrite)
  (implies (bitvp a)
           (equal (tc-to-bv (mod2 (bv-to-tc a))
                            (size a))
                  (bv-asr a)))
  ((use (embed-in-tc-to-bv (x (bv-to-tc (bv-asr a)))
                           (y (mod2 (bv-to-tc a)))
                           (n (size a)))
        (bv-asr-divides-by-two)
        (size-of-v-asr))
   (disable bv-asr-divides-by-two tc-to-bv)
   (hands-off mod2 bv-to-tc v-asr)))

(prove-lemma bv-to-tc-to-bv-of-zero-is-zero (rewrite)
  (equal (bv-to-tc (tc-to-bv 0 n))
         0))

(prove-lemma tc-to-bv-is-not-btm-for-non-zero-size (rewrite)
  (implies (not (zerop n))
           (equal (equal (tc-to-bv 0 n)
                         (btm))
                  f)))

(prove-lemma nat-of-zero-is-tc-of-zero (rewrite)
  (equal (nat-to-bv 0 size)
         (tc-to-bv 0 size)))

(prove-lemma tc-fix-of-add (rewrite)
  (equal (tc-fix (add a b))
         (add (tc-fix a) b)))

(prove-lemma tc-to-bv-of-bitv-not-btm (rewrite)
  (implies (and (not (equal a (btm)))
                (bitvp a))
           (not (equal (tc-to-bv 0 (size a))
                              (btm)))))

(prove-lemma tc-interpretation-of-inc-bit-vector (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm))))
           (equal (bv-adder-output t a (nat-to-bv 0 (size a)))
                  (tc-to-bv
                    (if (tc-in-rangep (add (bv-to-tc a) 1)
                                      (size a))
                        (add (bv-to-tc a) 1)
                        (if (negativep (add (bv-to-tc a) 1))
                            (add (bv-to-tc a)
                                 (add 1
                                      (exp 2 (size a))))
                            (add (bv-to-tc a)
                                 (add 1
                                      (minus (exp 2 (size a)))))))
                    (size a))))
  ((disable bv-adder-output add tc-in-rangep negativep bv-to-tc tc-to-bv)
   (hands-off exp)
   (enable tc-bv-adder-output-seen-as-bit-vector)))

(disable tc-interpretation-of-inc-bit-vector)

(prove-lemma tc-interpretation-of-dec-bit-vector (rewrite)
  (implies (and (bitvp a)
                (not (equal a (btm))))
           (equal (bv-subtracter-output t (nat-to-bv 0 (size a)) a)
                  (tc-to-bv
                    (if (tc-in-rangep (add (bv-to-tc a) -1)
                                      (size a))
                        (add (bv-to-tc a) -1)
                        (if (negativep (add (bv-to-tc a) -1))
                            (add (bv-to-tc a)
                                 (add -1
                                      (exp 2 (size a))))
                            (add (bv-to-tc a)
                                 (add -1
                                      (minus (exp 2 (size a)))))))
                    (size a))))
  ((disable bv-subtracter-output add tc-in-rangep negativep bv-to-tc tc-to-bv)
   (hands-off exp)
   (enable tc-bv-subtracter-output-seen-as-bit-vector)))

(disable tc-interpretation-of-dec-bit-vector)

(prove-lemma tc-interpretation-of-inc-overflowp (rewrite)
  (implies (and (bitvp a) 
                (not (equal a (btm))))
           (equal (bv-adder-overflowp t a (nat-to-bv 0 (size a)))
                  (not (tc-in-rangep (add (bv-to-tc a) 1)
                                     (size a)))))
  ((disable bv-adder-overflowp add tc-in-rangep negativep bv-to-tc tc-to-bv)
   (hands-off exp)
   (enable tc-interpretation-of-bv-adder-overflowp)))
  
(disable tc-interpretation-of-inc-overflowp)

(prove-lemma tc-interpretation-of-dec-overflowp (rewrite)
  (implies (and (bitvp a) 
                (not (equal a (btm))))
           (equal (bv-subtracter-overflowp t (nat-to-bv 0 (size a)) a)
                  (not (tc-in-rangep (add (bv-to-tc a) -1)
                                     (size a)))))
  ((disable bv-subtracter-overflowp add tc-in-rangep negativep bv-to-tc tc-to-bv)
   (hands-off exp)
   (enable tc-interpretation-of-bv-subtracter-overflowp)))
  
(disable tc-interpretation-of-dec-overflowp)

(prove-lemma tc-interpretation-of-negation-output (rewrite)
  (implies (and (bitvp a) 
                (not (equal a (btm))))
           (equal (bv-subtracter-output f a (nat-to-bv 0 (size a)))
                  (tc-to-bv
                    (if (tc-in-rangep (tc-minus (bv-to-tc a))
                                      (size a))
                        (tc-minus (bv-to-tc a))
                        (if (negativep (tc-minus (bv-to-tc a)))
                            (add (exp 2 (size a))
                                 (tc-minus (bv-to-tc a)))
                            (add (minus (exp 2 (size a)))
                                 (tc-minus (bv-to-tc a)))))
                    (size a))))  
  ((disable bv-subtracter-output add tc-in-rangep negativep bv-to-tc tc-to-bv)
   (hands-off exp)
   (enable tc-bv-subtracter-output-seen-as-bit-vector)))

(disable tc-interpretation-of-negation-output)

(prove-lemma tc-interpretation-of-negation-overflowp (rewrite)
  (implies (and (bitvp a) 
                (not (equal a (btm))))
           (equal (bv-subtracter-overflowp f a (nat-to-bv 0 (size a)))
                  (not (tc-in-rangep (tc-minus (bv-to-tc a))
                                     (size a)))))
  ((disable bv-subtracter-overflowp add tc-in-rangep negativep bv-to-tc tc-to-bv)
   (hands-off exp)
   (enable tc-interpretation-of-bv-subtracter-overflowp)))

(disable tc-interpretation-of-negation-overflowp)
(disable nat-of-zero-is-tc-of-zero)
(disable tc-fix-of-add)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Two's complement operation of ALU                                  ;; 
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

                
(prove-lemma alu-correct-twos-complement nil
  (implies (and (bitvp a)
                (not (equal a (btm)))
                (bitvp b)
                (not (equal b (btm)))
                (equal (size a) (size b))
                (boolp c))

           (and (equal (bv (bv-alu-cv a b c (nat-to-bv 9 4)))   ; Asr - bv
                       (tc-to-bv (mod2 (bv-to-tc a))
                                 (size a)))
                (equal (v (bv-alu-cv a b c (nat-to-bv 9 4)))    ; Asr - ovflow
                       f)

                (equal (bv (bv-alu-cv a b c (nat-to-bv 7 4)))   ; Sub - bv
                       (tc-to-bv
                         (if (tc-in-rangep (add (bv-to-tc b)
                                                (tc-minus (bv-to-tc a)))
                                           (size a))
                             (add (bv-to-tc b)
                                  (tc-minus (bv-to-tc a)))
                             (if (negativep (add (bv-to-tc b)
                                                 (tc-minus (bv-to-tc a))))
                                 (add (bv-to-tc b)
                                      (add (exp 2 (size a))
                                           (tc-minus (bv-to-tc a))))
                                 (add (bv-to-tc b)
                                      (add (minus (exp 2 (size a)))
                                           (tc-minus (bv-to-tc a))))))
                         (size a)))
                (equal (v (bv-alu-cv a b c (nat-to-bv 7 4)))    ; Sub - ovflow
                       (not (tc-in-rangep (add (bv-to-tc b)
                                               (tc-minus (bv-to-tc a)))
                                          (size a))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 6 4)))   ; Subb - bv
                       (tc-to-bv
                         (if (tc-in-rangep (add (bv-to-tc b)
                                                (tc-minus (add (bv-to-tc a)
                                                               (carry c))))
                                           (size a))
                             (add (bv-to-tc b) (tc-minus (add (bv-to-tc a)
                                                              (carry c))))
                             (if (negativep (add (bv-to-tc b)
                                                 (tc-minus (add (bv-to-tc a)
                                                                (carry c)))))
                                 (add (bv-to-tc b)
                                      (add (exp 2 (size a))
                                           (tc-minus (add (bv-to-tc a)
                                                          (carry c)))))
                                 (add (bv-to-tc b)
                                      (add (minus (exp 2 (size a)))
                                           (tc-minus (add (bv-to-tc a)
                                                          (carry c)))))))
                         (size a)))
                (equal (v (bv-alu-cv a b c (nat-to-bv 6 4)))    ; Subb - ovflow
                       (not (tc-in-rangep (add (bv-to-tc b)
                                               (tc-minus (add (bv-to-tc a)
                                                              (carry c))))
                                          (size a))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 5 4)))   ; Dec - bv
                  (tc-to-bv
                    (if (tc-in-rangep (add (bv-to-tc a) -1)
                                      (size a))
                        (add (bv-to-tc a) -1)
                        (if (negativep (add (bv-to-tc a) -1))
                            (add (bv-to-tc a)
                                 (add -1
                                      (exp 2 (size a))))
                            (add (bv-to-tc a)
                                 (add -1
                                      (minus (exp 2 (size a)))))))
                    (size a)))
                (equal (v (bv-alu-cv a b c (nat-to-bv 5 4)))    ; Dec - ovflow
                       (not (tc-in-rangep (add (bv-to-tc a) -1)
                                          (size a))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 4 4)))   ; Neg - bv
                       (tc-to-bv
                         (if (tc-in-rangep (tc-minus (bv-to-tc a))
                                           (size a))
                             (tc-minus (bv-to-tc a))
                             (if (negativep (tc-minus (bv-to-tc a)))
                                 (add (exp 2 (size a))
                                      (tc-minus (bv-to-tc a)))
                                 (add (minus (exp 2 (size a)))
                                      (tc-minus (bv-to-tc a)))))
                         (size a)))
                (equal (v (bv-alu-cv a b c (nat-to-bv 4 4)))    ; Neg - ovflow
                       (not (tc-in-rangep (tc-minus (bv-to-tc a))
                                          (size a))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 3 4)))   ; Add -  bv
                       (tc-to-bv
                         (if (tc-in-rangep (add (bv-to-tc a)
                                                (bv-to-tc b))
                                           (size a))
                             (add (bv-to-tc a) (bv-to-tc b))
                             (if (negativep (add (bv-to-tc a)
                                                 (bv-to-tc b)))
                                 (add (bv-to-tc a)
                                      (add (bv-to-tc b)
                                           (exp 2 (size a))))
                                 (add (bv-to-tc a)
                                      (add (bv-to-tc b)
                                           (minus (exp 2 (size a)))))))
                         (size a)))
                (equal (v (bv-alu-cv a b c (nat-to-bv 3 4)))    ; Add - ovflow
                       (not (tc-in-rangep (add (bv-to-tc a)
                                               (bv-to-tc b))
                                          (size a))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 2 4)))   ; Addc - bv
                       (tc-to-bv
                         (if (tc-in-rangep (add (bv-to-tc a)
                                                (add (bv-to-tc b)
                                                     (carry c)))
                                           (size a))
                             (add (bv-to-tc a) (add (bv-to-tc b)
                                                    (carry c)))
                             (if (negativep (add (bv-to-tc a)
                                                 (add (bv-to-tc b)
                                                      (carry c))))
                                 (add (bv-to-tc a)
                                      (add (bv-to-tc b)
                                           (add (carry c)
                                                (exp 2 (size a)))))
                                 (add (bv-to-tc a)
                                      (add (bv-to-tc b)
                                           (add (carry c)
                                                (minus (exp 2 (size a))))))))
                         (size a)))
                (equal (v (bv-alu-cv a b c (nat-to-bv 2 4)))    ; Addc - ovflow
                       (not (tc-in-rangep (add (bv-to-tc a)
                                               (add (bv-to-tc b) (carry c)))
                                          (size a))))

                (equal (bv (bv-alu-cv a b c (nat-to-bv 1 4)))   ; Inc - bv
                       (tc-to-bv
                         (if (tc-in-rangep (add (bv-to-tc a) 1)
                                           (size a))
                             (add (bv-to-tc a) 1)
                             (if (negativep (add (bv-to-tc a) 1))
                                 (add (bv-to-tc a)
                                      (add 1 (exp 2 (size a))))
                                 (add (bv-to-tc a)
                                      (add 1 (minus (exp 2 (size a)))))))
                         (size a)))
                (equal (v (bv-alu-cv a b c (nat-to-bv 1 4)))    ; Inc - ovflow
                       (not (tc-in-rangep (add (bv-to-tc a) 1)
                                          (size a))))))
  ((disable pathological-difference boolp v-lsr v-asr mod2
            bv-adder-output bv-adder-carry-out bv-adder-overflowp
            bv-subtracter-output bv-subtracter-carry-out bv-subtracter-overflowp
            nat-to-bv-to-nat add tc-in-rangep minus tc-to-bv)
   (hands-off nat-to-bv bv-to-nat bv-to-tc)
   (enable tc-interpretation-of-bv-subtracter-overflowp
           tc-bv-subtracter-output-seen-as-bit-vector
           tc-interpretation-of-bv-adder-overflowp
           tc-bv-adder-output-seen-as-bit-vector
           tc-interpretation-of-inc-bit-vector
           tc-interpretation-of-dec-bit-vector
           tc-interpretation-of-inc-overflowp
           tc-interpretation-of-dec-overflowp
           tc-interpretation-of-negation-output
           tc-interpretation-of-negation-overflowp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          This file contains definitions and lemmas concerning the            ;;
;;          hardware necessary to build "big-machine".                          ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Miscellaneous lemmas                                                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma size-bv-bv-alu-cv (rewrite)
  (equal (size (bv (bv-alu-cv a b c op-code)))
         (size a))
  ((disable bv-adder-output bv-adder-carry-out bv-adder-overflowp
            bv-subtracter-output bv-subtracter-carry-out bv-subtracter-overflowp
            nat-to-bv-to-nat remainder-of-0 carry)))

(disable bv-alu-cv)

(disable bv-alu-cv-with-ifs)

(defn fix-bool (x) (if x t f))

(defn properp (x)
  (if (nlistp x) (equal x nil) (properp (cdr x))))

(defn append (x y)
  (if (nlistp x)
      y
      (cons (car x) (append (cdr x) y))))

(prove-lemma assoc-of-append (rewrite)
  (equal (append (append a b) c) (append a (append b c))))

(prove-lemma length-0 (rewrite)
  (equal (equal (length x) 0) (nlistp x)))


(defn v-nat-dec (a)                             ; Word width decrement 
  (if (zerop (bv-to-nat a))
      (nat-to-bv (sub1 (exp 2 (size a)))
                 (size a))                      ; This is not needed for plus.
      (nat-to-bv (sub1 (bv-to-nat a))           ; (sub1 0) is zero and no wrap-
                 (size a))))                    ; around is received.

(defn v-nat-inc (a)                             ; Word width increment
  (nat-to-bv (add1 (bv-to-nat a)) (size a)))

(prove-lemma size-v-nat-dec (rewrite)
  (equal (size (v-nat-dec x))
         (size x)))

(prove-lemma size-v-nat-inc (rewrite)
  (equal (size (v-nat-inc x))
         (size x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Memory accessors                                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn nth (n lst)
  (if (zerop n)
      (car lst)
      (nth (sub1 n) (cdr lst))))

(defn v-nth (v-n lst)
  (nth (bv-to-nat v-n) lst))

(defn update-v (c cell value)
  (if (truep c)
      value
      cell))

(defn update-nth (c n lst value)
  (if (and (truep c)
           (listp lst))
      (if (zerop n)
          (cons value (cdr lst))
          (cons (car lst) (update-nth c (sub1 n) (cdr lst) value)))
      lst))

(defn update-v-nth (c v-n lst value)
  (update-nth c (bv-to-nat v-n) lst value))

(prove-lemma length-update-nth (rewrite)
  (equal (length (update-nth c n lst value))
         (length lst)))

(prove-lemma length-update-v-nth (rewrite)
  (equal (length (update-v-nth c n lst value))
         (length lst)))

(prove-lemma listp-update-nth (rewrite)
  (equal (listp (update-nth c n lst value))
         (listp lst)))

(prove-lemma listp-update-v-nth (rewrite)
  (equal (listp (update-v-nth c n lst value))
         (listp lst)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Zero and Negative flag interpretation lemmas                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn b-bv-nzerop (a)                           ; Not zerop vector test
  (if (bitvp a)
      (if (equal a (btm))
          f
          (b-or (bit a)
                (b-bv-nzerop (vec a))))
      f))

(defn b-bv-zerop (a)
  (b-not (b-bv-nzerop a)))

(defn v-zerop (a)
  (if (bitvp a)
      (if (equal a (btm))
          t
          (and (equal (bit a) f)
               (v-zerop (vec a))))
      t))

(prove-lemma b-bv-zerop-equal-v-zerop (rewrite)
  (equal (b-bv-zerop a)
         (v-zerop a)))


;  The following are the natural number and tc intepretation lemmas for
;  the zero flag.

(prove-lemma v-zerop-equal-bv-to-nat-zero (rewrite)
  (equal (v-zerop a)
         (zerop (bv-to-nat a))))

(prove-lemma v-zerop-equal-bv-to-tc-zero (rewrite)
  (equal (v-zerop a)
         (equal 0 (bv-to-tc a))))

(disable v-zerop-equal-bv-to-nat-zero)
(disable v-zerop-equal-bv-to-tc-zero)

;  The following is the tc interpretation lemma for the negative flag.

(prove-lemma n-flag-equals-negativep (rewrite)
  (equal (bitn a (size a))
         (negativep (bv-to-tc a))))

(disable n-flag-equals-negativep)



(defn bv-equal (a b)                            ; Vector equal test
  (if (bitvp a)
      (if (equal a (btm))
          t
          (b-and (b-equv (bit a) (bit b))
                 (bv-equal (vec a) (vec b))))
      f))

(prove-lemma bv-equal-is-equal (rewrite)
  (implies (and (bitvp a)
                (bitvp b)
                (equal (size a) (size b)))
           (equal (bv-equal a b)
                  (equal a b))))

(disable bv-equal-is-equal)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Assumptions made about the various registers                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn nxsz nil 4)                               ; width of micro address reg

(defn machine-size nil 16)                      ; Word width of micro-processor

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Register, RAMP, and ROMP recognizer                                 ;;
;;                                                                              ;;
;;          A ram and rom checker are presented below and is used to ensure     ;;
;;          that RAM and ROM (constant function) have certain properties.       ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defn sizep (register width)
  (equal (size register) width))

(defn every-member-sizep (lst n)
  (if (nlistp lst)
      t
      (and (sizep (car lst) n)
           (every-member-sizep (cdr lst) n))))

(defn ramp (ram width locations)
  (and (equal (length ram) locations)
       (every-member-sizep ram width)))

(defn romp (rom width locations)
  (and (equal (length rom) locations)
       (every-member-sizep rom width)))

(prove-lemma every-member-sizep-implies-size-nth (rewrite)
  (implies (and (lessp n (length lst))
                (every-member-sizep lst width))
           (equal (size (nth n lst)) width)))

(prove-lemma every-member-sizep-implies-size-nth-machine-size (rewrite)
  (implies (and (lessp n (length lst))
                (every-member-sizep lst (machine-size)))
           (equal (size (nth n lst)) (machine-size))))

(prove-lemma every-member-sizep-implies-size-nth-0 (rewrite)
  (implies (and (every-member-sizep lst width)
                (lessp 0 (length lst)))
           (equal (size (car lst)) width)))

(disable boolp)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Op-code accessors                                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn bv-op-code (i-reg)
  (bitv (bitn i-reg 13)
        (bitv (bitn i-reg 14)
              (bitv (bitn i-reg 15)
                    (bitv (bitn i-reg 16)
                          (btm))))))

(defn b-move-op (i-reg)
  (bitn i-reg 12))

(defn b-cc-set (i-reg)
  (bitn i-reg 11))

(defn b-direct-reg-b (i-reg)
  (b-nor (bitn i-reg 9)
         (bitn i-reg 10)))

(defn b-indirect-reg-b (i-reg)
  (b-and (bitn i-reg 9)
         (b-not (bitn i-reg 10))))

(defn b-indirect-reg-b-dec (i-reg)
  (b-and (b-not (bitn i-reg 9))
         (bitn i-reg 10)))

(defn b-indirect-reg-b-inc (i-reg)
  (b-and (bitn i-reg 9)
         (bitn i-reg 10)))

(defn bv-oprd-b (i-reg)
  (bitv (bitn i-reg 6)
        (bitv (bitn i-reg 7)
              (bitv (bitn i-reg 8)
                    (btm)))))

(defn b-direct-reg-a (i-reg)
  (b-nor (bitn i-reg 4)
         (bitn i-reg 5)))

(defn b-indirect-reg-a (i-reg)
  (b-and (bitn i-reg 4)
         (b-not (bitn i-reg 5))))

(defn b-indirect-reg-a-dec (i-reg)
  (b-and (b-not (bitn i-reg 4))
         (bitn i-reg 5)))

(defn b-indirect-reg-a-inc (i-reg)
  (b-and (bitn i-reg 4)
         (bitn i-reg 5)))

(defn bv-oprd-a (i-reg)
  (bitv (bitn i-reg 1)
        (bitv (bitn i-reg 2)
              (bitv (bitn i-reg 3)
                    (btm)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Sub-functions for FM8501                                            ;;
;;                                                                              ;;
;;          NOTE:  Many definitions below are presented in pairs.  A hardware   ;;
;;                 version is presented along with a version that is more       ;;
;;                 agreeable to the theorem-prover.  The second of these        ;;
;;                 paired definitions is has a "WITH-IFS" ending.  Not all      ;;
;;                 of the hardware functions have a "WITH-IFS" pair.            ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn bv-alu-op-code (i-reg)
  (bv-if (b-move-op i-reg)
         (nat-to-bv 0 4)
         (bv-op-code i-reg)))

(defn b-store-alu-result (c-flag v-flag z-flag n-flag i-reg)
  (b-or (b-or (b-not (b-move-op i-reg))
              (bitn (bv-op-code i-reg) 4))
        (b-or (b-or (b-or (b-and (b-not c-flag)
                                 (bv-equal (bv-op-code i-reg)
                                           (nat-to-bv 0 4)))
                          (b-and c-flag
                                 (bv-equal (bv-op-code i-reg)
                                           (nat-to-bv 1 4))))
                    (b-or (b-and (b-not v-flag)
                                 (bv-equal (bv-op-code i-reg)
                                           (nat-to-bv 2 4)))
                          (b-and v-flag
                                 (bv-equal (bv-op-code i-reg)
                                           (nat-to-bv 3 4)))))
              (b-or (b-or (b-and (b-not z-flag)
                                 (bv-equal (bv-op-code i-reg)
                                           (nat-to-bv 4 4)))
                          (b-and z-flag
                                 (bv-equal (bv-op-code i-reg)
                                           (nat-to-bv 5 4))))
                    (b-or (b-and (b-not n-flag)
                                 (bv-equal (bv-op-code i-reg)
                                           (nat-to-bv 6 4)))
                          (b-and n-flag
                                 (bv-equal (bv-op-code i-reg)
                                           (nat-to-bv 7 4))))))))

(defn b-store-alu-result-with-ifs (c-flag v-flag z-flag n-flag i-reg)
  (or (not (b-move-op i-reg))
      (bitn (bv-op-code i-reg) 4)
      (equal (bv-op-code i-reg)
             (nat-to-bv (if c-flag 1 0) 4))
      (equal (bv-op-code i-reg)
             (nat-to-bv (if v-flag 3 2) 4))
      (equal (bv-op-code i-reg)
             (nat-to-bv (if z-flag 5 4) 4))
      (equal (bv-op-code i-reg)
             (nat-to-bv (if n-flag 7 6) 4))))

(prove-lemma b-store-alu-result-ifs (rewrite)
  (equal (b-store-alu-result c-flag v-flag z-flag n-flag i-reg)
         (b-store-alu-result-with-ifs c-flag v-flag z-flag n-flag i-reg)))

(disable b-store-alu-result)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Micro-rom                                                           ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn make-micro-word (l)
 (if (nlistp l)
     (btm)
     (if (nlistp (cdr l))
         (nat-to-bv (car l) (nxsz))
         (bitv (if (equal (car l) 't) t f)
               (make-micro-word (cdr l))))))

(defn make-micro-rom (l)
  (if (nlistp l) nil (cons (make-micro-word (car l)) (make-micro-rom (cdr l)))))


(defn micro-store nil
;                      1 1 1 1 1 1 1 1
;    1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7
  (make-micro-rom '((f f f f f f f f f t f f f f f f 1)         ;0
                    
                    (f t f t f t f f f t f t f f f f 2)         ;1
                    (f f f t f f f f t f f f f f f f 3)         ;2
                    (f f f f f f f f f t f f f f t f 4)         ;3
                    
                    (f f f f t f f t f t f t f f f f 5)         ;4
                    (f f f f t f f f t f f f f f f f 6)         ;5
                    (f f f f t f f f f t t f f f f f 7)         ;6
                    
                    (f f f f f f f t f t f t f f f f 8)         ;7
                    (f f f f f f f f t f f f f f f f 9)         ;8
                    (f f f f f f f f f t f f t f f f 10)        ;9
                    
                    (f f f f f f f f f t f f f t f f 11)        ;10
                    (t f t f f f f f f f f f f f f t 12)        ;11
                    
                    (f f f f t f t f f t f f f f f f 13)        ;12
                    (f f f f f f t f f t f f f f f f 1)         ;13
                    
;  The remaining lines send us to state 0 if mar ever gets beyond 13.  This is
;  provably impossible after resetting; however, if struck by alpha radiation
;  this insures a reset.  It also makes some of the proofs easier because we
;  know that (next (micro-rom mar)) has size 4 provided mar has size 4.
                    
                    (f f f f f f f f f t f f f f f f 0)         ;14
                    (f f f f f f f f f t f f f f f f 0)         ;15
                    )))

(defn micro-rom (addr)
  (v-nth addr (micro-store)))


;  Accessors for data in the ROM named "micro-store".

(defn b-dout-incdec    (x) (bitn x 1))  ; Data out reg or address unit
(defn b-force-inc      (x) (bitn x 2))  ; Force increment for address
(defn b-en-no-store    (x) (bitn x 3))  ; Let "NO-STORE" effect sequencer
(defn b-ir-mem-ref     (x) (bitn x 4))  ; Memory reference for instruction
(defn b-oprda-oprdb    (x) (bitn x 5))  ; Select operand A or operand B
(defn b-pc-regnum      (x) (bitn x 6))  ; Select PC or register in file
(defn b-postinc        (x) (bitn x 7))  ; Post-increment address mode
(defn b-predec         (x) (bitn x 8))  ; Pre-decrement address mode
(defn b-rd             (x) (bitn x 9))  ; Read cycle
(defn b-seq            (x) (bitn x 10)) ; Sequence micro-address register
(defn b-we-a-reg       (x) (bitn x 11)) ; Write enable A register
(defn b-we-addr-out    (x) (bitn x 12)) ; Write enable address-out register
(defn b-we-b-reg       (x) (bitn x 13)) ; Write enable B register
(defn b-we-alu-result  (x) (bitn x 14)) ; WE DATA-OUT, CC-REG, NO-STORE
(defn b-we-ir          (x) (bitn x 15)) ; Write enable instruction register
(defn b-wr             (x) (bitn x 16)) ; Write cycle
(defn bv-next          (x) (bitv (bitn x 17)    ; Next micro address
                                 (bitv (bitn x 18)
                                       (bitv (bitn x 19)
                                             (bitv (bitn x 20)
                                                   (btm))))))

(defn right-bv-next-size (lst)
  (if (nlistp lst)
      t
      (and (equal (size (bv-next (car lst))) (nxsz))
           (right-bv-next-size (cdr lst)))))

(prove-lemma size-bv-next-micro-rom-lemma (rewrite)
  (equal (size (bv-next x)) 4))

(disable micro-rom)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Hardware variable and constant assumptions for FM8501.              ;;
;;                                                                              ;;
;;      The following definition describes the assumptions about the various    ;;
;;      registers (variables) and the ROM used in the construction of the       ;;
;;      FM8501 microprocessor.                                                  ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn standard-hyps (mar read write dtack reset no-store data-out
                         reg-file addr-out c-flag v-flag z-flag n-flag
                         a-reg b-reg i-reg visual-mem real-mem)
  (and (romp (micro-store) 20 (exp 2 (nxsz)))
       (sizep mar (nxsz))
       (boolp read)
       (boolp write)
       (boolp dtack)
       (boolp reset)
       (boolp no-store)
       (sizep data-out (machine-size))
       (ramp reg-file (machine-size) 8)
       (sizep addr-out (machine-size))
       (boolp c-flag)
       (boolp v-flag)
       (boolp z-flag)
       (boolp n-flag)
       (sizep a-reg (machine-size))
       (sizep b-reg (machine-size))
       (sizep i-reg (machine-size))
       (sizep visual-mem (machine-size))
       (ramp real-mem (machine-size) (exp 2 16))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Miscellanous lemmas                                                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma every-member-sizep-implies-bitvp (rewrite)
  (implies (and (every-member-sizep lst width)
                (lessp n (length lst))
                (not (zerop width)))
           (bitvp (nth n lst))))

(prove-lemma every-member-sizep-implies-bitvp-machine-size (rewrite)
  (implies (and (every-member-sizep lst (machine-size))
                (lessp n (length lst)))
           (bitvp (nth n lst))))

(prove-lemma sizep-implies-bitvp (rewrite)
  (implies (equal (size a) (add1 n))
           (bitvp a)))


;  The following lemma subsumes trunc-size.

(prove-lemma trunc-size-bridge (rewrite)
  (implies (and (bitvp a)
                (equal n (size a)))
           (equal (trunc a n) a)))

(prove-lemma b-if-works (rewrite)
  (implies (and (boolp c)
                (boolp a)
                (boolp b))
           (equal (b-if c a b) (if c a b)))
  ((enable boolp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Functions for composing the micro-processor                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn bv-reg-select (i-reg mar reset)
  (bv-if (b-or reset
               (b-pc-regnum (micro-rom mar)))
         (nat-to-bv 0 3)                        ; PC is register 0
         (bv-if (b-oprda-oprdb (micro-rom mar))
                (bv-oprd-a i-reg)
                (bv-oprd-b i-reg))))

(defn bv-reg-select-with-ifs (i-reg mar reset)
  (if (b-or reset
            (b-pc-regnum (micro-rom mar)))
      (nat-to-bv 0 3)                           ; PC is register 0
      (if (b-oprda-oprdb (micro-rom mar))
          (bv-oprd-a i-reg)
          (bv-oprd-b i-reg))))

(prove-lemma bv-reg-select-ifs (rewrite)
  (equal (bv-reg-select i-reg mar reset)
         (bv-reg-select-with-ifs i-reg mar reset)))


(defn b-oprd-mem-ref (mar i-reg)
  (b-if (b-oprda-oprdb (micro-rom mar))
        (b-not (b-direct-reg-a i-reg))
        (b-not (b-direct-reg-b i-reg))))

(defn b-oprd-mem-ref-with-ifs (mar i-reg)
  (if (b-oprda-oprdb (micro-rom mar))
        (b-not (b-direct-reg-a i-reg))
        (b-not (b-direct-reg-b i-reg))))

(prove-lemma b-oprd-mem-ref-ifs (rewrite)
  (equal (b-oprd-mem-ref mar i-reg)
         (b-oprd-mem-ref-with-ifs mar i-reg)))

(disable b-oprd-mem-ref)        ; This disable was not here when FM8501 proved.

;  Next micro-address

(defn mar (mar i-reg dtack reset no-store)
  (update-v (b-or (b-or reset
                        (b-or dtack
                              (b-seq (micro-rom mar))))
                  (b-or (b-and (b-en-no-store (micro-rom mar))
                               no-store)
                        (b-and (b-not (b-oprd-mem-ref mar i-reg))
                               (b-not (b-ir-mem-ref (micro-rom mar))))))
            mar
            (bv-if reset
                   (nat-to-bv 0 (nxsz))
                   (bv-next (micro-rom mar)))))

;  Read register

(defn read (mar i-reg)
  (b-and (b-or (b-oprd-mem-ref mar i-reg)
               (b-ir-mem-ref (micro-rom mar)))
         (b-rd (micro-rom mar))))

;  Write register

(defn write (mar i-reg no-store)
  (b-and (b-wr (micro-rom mar))
         (b-and (b-oprd-mem-ref mar i-reg)
                (b-not no-store))))

;  Data acknowledgement

(defn dtack (current-oracle-entry)
  (fix-bool (car current-oracle-entry)))

;  Reset function

(defn reset (current-oracle-entry)
  (fix-bool (cadr current-oracle-entry)))

;  No-store -- defines the flag which allows FM8501 to do conditional stores.

(defn no-store (no-store c-flag v-flag z-flag n-flag i-reg mar)
  (update-v (b-we-alu-result (micro-rom mar))
            no-store
            (b-not (b-store-alu-result c-flag v-flag z-flag n-flag i-reg))))


(defn no-store-with-ifs (no-store c-flag v-flag z-flag n-flag i-reg mar)
  (if (b-we-alu-result (micro-rom mar))
      (not (b-store-alu-result-with-ifs c-flag v-flag z-flag n-flag i-reg))
      no-store))

(prove-lemma no-store-ifs (rewrite)
  (equal (no-store no-store c-flag v-flag z-flag n-flag i-reg mar)
         (no-store-with-ifs no-store c-flag v-flag z-flag n-flag i-reg mar))
  ((disable b-store-alu-result-with-ifs)))

(disable no-store)

;  Bit-vector result of the ALU

(defn data-out (data-out a-reg b-reg c-flag i-reg mar)
  (update-v (b-we-alu-result (micro-rom mar))
            data-out
            (bv (bv-alu-cv a-reg b-reg c-flag (bv-alu-op-code i-reg)))))

(defn data-out-with-ifs (data-out a-reg b-reg c-flag i-reg mar)
  (if (b-we-alu-result (micro-rom mar))
      (bv (bv-alu-cv a-reg b-reg c-flag (bv-alu-op-code i-reg)))
      data-out))

(prove-lemma data-out-ifs (rewrite)
  (equal (data-out data-out a-reg b-reg c-flag i-reg mar)
         (data-out-with-ifs data-out a-reg b-reg c-flag i-reg mar)))

(disable data-out)

;  Calculates the next value of the register file.

(defn reg-file (reg-file data-out i-reg mar no-store reset)
  (update-v-nth (b-or (b-or reset
                            (b-force-inc (micro-rom mar)))
                      (b-or (b-or (b-pc-regnum (micro-rom mar))
                                  (b-and (b-wr (micro-rom mar))
                                         (b-and (b-not no-store)
                                                (b-direct-reg-b i-reg))))
                            (b-or (b-and (b-predec (micro-rom mar))
                                         (b-if (b-oprda-oprdb (micro-rom mar))
                                               (b-indirect-reg-a-dec i-reg)
                                               (b-indirect-reg-b-dec i-reg)))
                                  (b-and (b-postinc (micro-rom mar))
                                         (b-if (b-oprda-oprdb (micro-rom mar))
                                               (b-indirect-reg-a-inc i-reg)
                                               (b-indirect-reg-b-inc i-reg))))))
                (bv-reg-select i-reg mar reset)
                reg-file
                (bv-if (b-or (b-dout-incdec (micro-rom mar))
                             reset)
                       (bv-if reset
                              (nat-to-bv 0 (machine-size))
                              data-out)
                       (bv-if (b-or (b-force-inc (micro-rom mar))
                                    (b-if (b-oprda-oprdb (micro-rom mar))
                                          (b-indirect-reg-a-inc i-reg)
                                          (b-indirect-reg-b-inc i-reg)))
                              (bv-adder-output
                                t
                                (nat-to-bv 0 (machine-size))
                                (v-nth (bv-reg-select i-reg mar reset) reg-file))
                              (bv-subtracter-output
                                t
                                (nat-to-bv 0 (machine-size))
                                (v-nth (bv-reg-select i-reg mar reset)
                                       reg-file))))))

;  Defines the output address presented by FM8501.

(defn addr-out (addr-out reg-file i-reg mar reset)
  (update-v (b-we-addr-out (micro-rom mar))
            addr-out
            (bv-if (b-and (b-predec (micro-rom mar))
                          (b-if (b-oprda-oprdb (micro-rom mar))
                                (b-indirect-reg-a-dec i-reg)
                                (b-indirect-reg-b-dec i-reg)))
                   (bv-subtracter-output
                     t
                     (nat-to-bv 0 (machine-size))
                     (v-nth (bv-reg-select i-reg mar reset) reg-file))
                   (v-nth (bv-reg-select i-reg mar reset) reg-file))))

;  Carry flag

(defn c-flag (c-flag a-reg b-reg i-reg mar)
  (update-v (b-and (b-we-alu-result (micro-rom mar))
                   (b-cc-set i-reg))
            c-flag
            (c (bv-alu-cv a-reg b-reg c-flag (bv-alu-op-code i-reg)))))

(defn c-flag-with-ifs (c-flag a-reg b-reg i-reg mar)
  (if (b-and (b-we-alu-result (micro-rom mar))
             (b-cc-set i-reg))
      (c (bv-alu-cv a-reg b-reg c-flag (bv-alu-op-code i-reg)))
      c-flag))

(prove-lemma c-flag-ifs (rewrite)
  (equal (c-flag c-flag a-reg b-reg i-reg mar)
         (c-flag-with-ifs c-flag a-reg b-reg i-reg mar)))

(disable c-flag)

;  The overflow flag

(defn v-flag (v-flag a-reg b-reg c-flag i-reg mar)
  (update-v (b-and (b-we-alu-result (micro-rom mar))
                   (b-cc-set i-reg))
            v-flag
            (v (bv-alu-cv a-reg b-reg c-flag (bv-alu-op-code i-reg)))))

(defn v-flag-with-ifs (v-flag a-reg b-reg c-flag i-reg mar)
  (if (b-and (b-we-alu-result (micro-rom mar))
             (b-cc-set i-reg))
      (v (bv-alu-cv a-reg b-reg c-flag (bv-alu-op-code i-reg)))
      v-flag))

(prove-lemma v-flag-ifs (rewrite)
  (equal (v-flag v-flag a-reg b-reg c-flag i-reg mar)
         (v-flag-with-ifs v-flag a-reg b-reg c-flag i-reg mar)))

(disable v-flag)

;  The zero flag

(defn z-flag (z-flag a-reg b-reg c-flag i-reg mar)
  (update-v (b-and (b-we-alu-result (micro-rom mar))
                   (b-cc-set i-reg))
            z-flag
            (b-bv-zerop (bv (bv-alu-cv a-reg b-reg c-flag
                                       (bv-alu-op-code i-reg))))))

(defn z-flag-with-ifs (z-flag a-reg b-reg c-flag i-reg mar)
  (if (b-and (b-we-alu-result (micro-rom mar))
             (b-cc-set i-reg))
      (b-bv-zerop (bv (bv-alu-cv a-reg b-reg c-flag
                                 (bv-alu-op-code i-reg))))
      z-flag))

(prove-lemma z-flag-ifs (rewrite)
  (equal (z-flag z-flag a-reg b-reg c-flag i-reg mar)
         (z-flag-with-ifs z-flag a-reg b-reg c-flag i-reg mar)))

(disable z-flag)

;  Two's complement negative flag

(defn n-flag (n-flag a-reg b-reg c-flag i-reg mar)
  (update-v (b-and (b-we-alu-result (micro-rom mar))
                   (b-cc-set i-reg))
            n-flag
            (bitn (bv (bv-alu-cv a-reg b-reg c-flag (bv-alu-op-code i-reg)))
                  (machine-size))))

(defn n-flag-with-ifs (n-flag a-reg b-reg c-flag i-reg mar)
  (if (b-and (b-we-alu-result (micro-rom mar))
             (b-cc-set i-reg))
      (bitn (bv (bv-alu-cv a-reg b-reg c-flag (bv-alu-op-code i-reg)))
            (machine-size))
      n-flag))

(prove-lemma n-flag-ifs (rewrite)
  (equal (n-flag n-flag a-reg b-reg c-flag i-reg mar)
         (n-flag-with-ifs n-flag a-reg b-reg c-flag i-reg mar)))

(disable n-flag)

;  Operand A for the ALU

(defn a-reg (a-reg visual-mem reg-file i-reg mar reset)
  (update-v (b-we-a-reg (micro-rom mar))
            a-reg
            (bv-if (b-direct-reg-a i-reg)
                   (v-nth (bv-reg-select i-reg mar reset)
                          reg-file)
                   visual-mem)))

;  Operand B for the ALU

(defn b-reg (b-reg visual-mem reg-file i-reg mar reset)
  (update-v (b-we-b-reg (micro-rom mar))
            b-reg
            (bv-if (b-direct-reg-b i-reg)
                   (v-nth (bv-reg-select i-reg mar reset)
                          reg-file)
                   visual-mem)))

;  Fills the instruction register

(defn i-reg (i-reg visual-mem mar)
  (update-v (b-we-ir (micro-rom mar))
            i-reg
            visual-mem))

(defn i-reg-with-ifs (i-reg visual-mem mar)
  (if (b-we-ir (micro-rom mar))
      visual-mem
      i-reg))

(prove-lemma i-reg-ifs (rewrite)
  (equal (i-reg i-reg visual-mem mar)
         (i-reg-with-ifs i-reg visual-mem mar)))

(disable i-reg)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Memory process                                                      ;;
;;                                                                              ;;
;;          The memory process is interesting as it requires history to         ;;
;;          operate.  VISUAL-MEM is the description of how a memory that        ;;
;;          FM8501 reads is expected to act.  A "correct" memory value is       ;;
;;          only returned after the READ line has been on for two clock "ticks",;;
;;          the WRITE line is off, DTACK is on, RESET is off, and DATA-OUT      ;;
;;          and ADDR-OUT have been stable for two clock "ticks".  VISUAL-MEM    ;;
;;          embodies the assumptions made about reading memory.  REAL-MEM       ;;
;;          is a function that actually updates the memory.  Its assumptions    ;;
;;          are expressed similarily as VISUAL-MEM.  The WATCH-DOG allows       ;;
;;          one tick's worth of state to be kept concerning READ, WRITE,        ;;
;;          DTACK, DATA-OUT, and ADDR-OUT.                                      ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(add-shell watch-dog nil watch-dogp
           ((read-1          (none-of) false)
            (write-1         (none-of) false)
            (dtack-1-oracle  (none-of) false)
            (data-out-1      (one-of bitvp) btm)
            (addr-out-1      (one-of bitvp) btm)))


(dcl default-visual-mem-value ())       ; Default value from memory when memory
                                        ; has not been selected to return a value.

(defn visual-mem (real-mem read write addr-out
                  memory-watch-dog-history dtack-oracle reset-oracle)
  (trunc (if (and (and read (read-1 memory-watch-dog-history))
                  (and (not write) (not (write-1 memory-watch-dog-history)))
                  (equal addr-out (addr-out-1 memory-watch-dog-history))
                  (and dtack-oracle
                       (dtack-1-oracle memory-watch-dog-history))
                  (not reset-oracle))
             (v-nth addr-out real-mem)
             (default-visual-mem-value))
         (machine-size)))

(defn real-mem (real-mem read write addr-out data-out
                memory-watch-dog-history dtack-oracle reset-oracle)
  (update-v-nth (and (and write (write-1 memory-watch-dog-history))
                     (and (not read) (not (read-1 memory-watch-dog-history)))
                     (equal addr-out (addr-out-1 memory-watch-dog-history))
                     (and dtack-oracle
                          (not (dtack-1-oracle memory-watch-dog-history)))
                     (not reset-oracle))
                addr-out
                real-mem
                data-out))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          "big-machine" -- the definition of the microprocessor               ;;
;;                                                                              ;;
;;          This function is the definition of the FM8501 microprocessor.       ;;
;;          BIG-MACHINE executes as along as there are clock "ticks".  Clock    ;;
;;          "ticks" are characterized by there being elements left in the       ;;
;;          ORACLE.  Otherwise, this function just stops, effectively           ;;
;;          freezing the value of its variables (registers).                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn big-machine (mar read write dtack reset
                       no-store data-out
                       reg-file addr-out c-flag v-flag z-flag n-flag
                       a-reg b-reg i-reg
                       visual-mem real-mem
                       memory-watch-dog-history oracle)
  (if (nlistp oracle)
      (list mar read write dtack reset
            no-store data-out
            reg-file addr-out c-flag v-flag z-flag n-flag
            a-reg b-reg i-reg visual-mem real-mem memory-watch-dog-history)
      (big-machine (mar mar i-reg dtack reset no-store)
                   (read mar i-reg)
                   (write mar i-reg no-store)
                   (dtack (car oracle))
                   (reset (car oracle))
                   (no-store no-store c-flag v-flag z-flag n-flag i-reg mar)
                   (data-out data-out a-reg b-reg c-flag i-reg mar)
                   (reg-file reg-file data-out i-reg mar no-store reset)
                   (addr-out addr-out reg-file i-reg mar reset)
                   (c-flag c-flag a-reg b-reg i-reg mar)
                   (v-flag v-flag a-reg b-reg c-flag i-reg mar)
                   (z-flag z-flag a-reg b-reg c-flag i-reg mar)
                   (n-flag n-flag a-reg b-reg c-flag i-reg mar)
                   (a-reg a-reg visual-mem reg-file i-reg mar reset)
                   (b-reg b-reg visual-mem reg-file i-reg mar reset)
                   (i-reg i-reg visual-mem mar)
                   (visual-mem real-mem read write addr-out
                               memory-watch-dog-history
                               (dtack (car oracle)) (reset (car oracle)))
                   (real-mem real-mem read write addr-out data-out
                             memory-watch-dog-history
                             (dtack (car oracle)) (reset (car oracle)))
                   (watch-dog read write (dtack (car oracle)) data-out addr-out)
                   (cdr oracle)
                   )))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          "big-machine" operation on lists and empty lists                    ;;
;;                                                                              ;;
;;          The following two lemmas describe what BIG-MACHINE does when        ;;
;;          clock "ticks" are available or the clock has been exhausted.        ;;
;;          This information is easily available by looking at the definition   ;;
;;          BIG-MACHINE; however, these formulations make it easier for the     ;;
;;          theorem-prover to reason about BIG-MACHINE.                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma open-big-machine-on-nlistp (rewrite)
  (implies (not (listp oracle))
           (equal (big-machine mar read write dtack reset
                               no-store data-out
                               reg-file addr-out c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               memory-watch-dog-history oracle)
                  (list mar read write dtack reset
                        no-store data-out
                        reg-file addr-out c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg visual-mem real-mem
                        memory-watch-dog-history))))

(prove-lemma open-big-machine-on-listp (rewrite)
  (implies (listp oracle)
           (equal (big-machine mar read write dtack reset
                               no-store data-out
                               reg-file addr-out c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               memory-watch-dog-history oracle)
                  (big-machine
                    (mar mar i-reg dtack reset no-store)
                    (read mar i-reg)
                    (write mar i-reg no-store)
                    (dtack (car oracle))
                    (reset (car oracle))
                    (no-store-with-ifs no-store c-flag v-flag
                                       z-flag n-flag i-reg mar)
                    (data-out-with-ifs data-out a-reg b-reg c-flag i-reg mar)
                    (reg-file reg-file data-out i-reg mar no-store reset)
                    (addr-out addr-out reg-file i-reg mar reset)
                    (c-flag-with-ifs c-flag a-reg b-reg i-reg mar)
                    (v-flag-with-ifs v-flag a-reg b-reg c-flag i-reg mar)
                    (z-flag-with-ifs z-flag a-reg b-reg c-flag i-reg mar)
                    (n-flag-with-ifs n-flag a-reg b-reg c-flag i-reg mar)
                    (a-reg a-reg visual-mem reg-file i-reg mar reset)
                    (b-reg b-reg visual-mem reg-file i-reg mar reset)
                    (i-reg-with-ifs i-reg visual-mem mar)
                    (visual-mem real-mem read write addr-out
                                memory-watch-dog-history
                                (dtack (car oracle)) (reset (car oracle)))
                    (real-mem real-mem read write addr-out data-out
                              memory-watch-dog-history
                              (dtack (car oracle)) (reset (car oracle)))
                    (watch-dog read write (dtack (car oracle)) data-out addr-out)
                    (cdr oracle))))
  ((disable mar read write dtack reset no-store-with-ifs
            data-out-with-ifs reg-file addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs
            a-reg b-reg
            i-reg-with-ifs visual-mem real-mem)))

(disable big-machine)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          This file contains definitions and lemmas concerning the            ;;
;;          sequencing of big-machine.  The proofs for the correctness of       ;;
;;          the micro-code are given here.                                      ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Lemma used to tear apart "append"ed oracles                         ;;
;;          This is the fundamental lemma for sequencing big-machine.           ;;
;;          It permits us to express computations on a (append a b) in terms    ;;
;;          of a computation on b applied to the state produced by a.  We can   ;;
;;          then get results about long computations by composing them from     ;;
;;          simple ones.                                                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



(prove-lemma big-machine-append (rewrite)
  (implies (equal m (big-machine mar read write dtack reset
                                 no-store data-out reg-file addr-out
                                 c-flag v-flag z-flag n-flag
                                 a-reg b-reg i-reg
                                 visual-mem real-mem
                                 memory-watch-dog-history oracle1))
           (equal (big-machine mar read write dtack reset
                               no-store data-out
                               reg-file addr-out c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               memory-watch-dog-history (append oracle1 oracle2))
                  (big-machine (car m)
                               (cadr m)
                               (caddr m)
                               (cadddr m)
                               (caddddr m)
                               (cadddddr m)
                               (caddddddr m)
                               (cadddddddr m)
                               (caddddddddr m)
                               (cadddddddddr m)
                               (caddddddddddr m)
                               (cadddddddddddr m)
                               (caddddddddddddr m)
                               (cadddddddddddddr m)
                               (caddddddddddddddr m)
                               (cadddddddddddddddr m)
                               (caddddddddddddddddr m)
                               (cadddddddddddddddddr m)
                               (caddddddddddddddddddr m)
                               oracle2)))
  ((disable mar read write dtack reset no-store-with-ifs
            data-out-with-ifs reg-file addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs
            a-reg b-reg i-reg-with-ifs visual-mem real-mem)
   (induct (big-machine mar read write dtack reset 
                        no-store data-out
                        reg-file addr-out c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        visual-mem real-mem
                        memory-watch-dog-history oracle1))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Miscellaneous lemmas about inc/dec and updating                     ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma bv-incrementer-truncates-to-machine-size (rewrite)
  (implies (and (equal zero (nat-to-bv 0 (machine-size)))
                (bitvp bit-vec)
                (equal (size bit-vec) (machine-size)))
           (equal (bv-adder-output t zero bit-vec)
                  (v-nat-inc bit-vec)))
  ((hands-off bv-adder-output)
   (enable nat-to-bv-ignores-remainder)
   (use (nat-bv-adder-output-seen-as-bit-vector
          (a (nat-to-bv 0 (machine-size)))
          (b bit-vec)
          (c t)))))

(disable bv-incrementer-truncates-to-machine-size)

(prove-lemma bv-decrementer-truncates-to-machine-size-help (rewrite)
  (implies
    (and (not (lessp (bv-to-nat bit-vec) 1))
         (bitvp bit-vec)
         (equal (size bit-vec) 16)
         (not (equal (bv-to-nat bit-vec) 0)))
    (equal (nat-to-bv (difference (bv-to-nat bit-vec) 1)
                      16)
           (nat-to-bv (sub1 (bv-to-nat bit-vec))
                      16))))

(prove-lemma bv-decrementer-truncates-to-machine-size (rewrite)
  (implies (and (equal zero (nat-to-bv 0 (machine-size)))
                (bitvp bit-vec)
                (equal (size bit-vec) (machine-size)))
           (equal (bv-subtracter-output t zero bit-vec)
                  (v-nat-dec bit-vec)))
  ((hands-off bv-subtracter-output)
   (disable nat-to-bv bv-to-nat)
   (use (nat-bv-subtracter-output-seen-as-bit-vector
          (a (nat-to-bv 0 (machine-size)))
          (b bit-vec)
          (c t)))))

(disable bv-decrementer-truncates-to-machine-size-help)
(disable bv-decrementer-truncates-to-machine-size)

(prove-lemma trunc-size-1 (rewrite)
  (implies (equal n (size a))
           (equal (trunc a n)
                  (if (bitvp a) a (btm)))))

(prove-lemma size-v-nth (rewrite)
  (implies (and (equal (size a) 3)
                (equal (length reg-file) 8)
                (every-member-sizep reg-file (machine-size)))
           (equal (size (v-nth a reg-file))
                  (machine-size)))
  ((use (upper-bound-on-bv-to-nat (a a)))))

(prove-lemma update-update-nth (rewrite)
  (equal (update-nth c n (update-nth c n lst value2) value1)
         (update-nth c n lst value1)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Resetting "big-machine"                                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma mar-on-reset (rewrite)
  (equal (mar mar i-reg dtack t no-store)
         (nat-to-bv 0 (nxsz))))

(prove-lemma reg-file-on-reset (rewrite)
  (equal (reg-file reg-file data-out i-reg mar no-store t)
         (update-nth t 0 reg-file (nat-to-bv 0 (machine-size)))))

(prove-lemma listp-reg-file (rewrite)
  (equal (listp (reg-file reg-file data-out i-reg mar no-store reset))
         (listp reg-file)))

;  The following lemma describes the first three clock "ticks" after a
;  reset occurs.  The memory-address register (MAR) is set to zero, the
;  read and write outputs are set to "false", and the reset latch is set
;  to "true".  Since nothing is know about the WATCH-DOG-HISTORY, it is
;  not possible to characterize what the memory state is.  However, after
;  these three clock "ticks" everything is stable (unchanging) until reset
;  is turned off.

(prove-lemma reset-to-state-0 (rewrite)
  (implies (and (standard-hyps mar read write dtack reset no-store data-out
                          reg-file addr-out c-flag v-flag z-flag n-flag
                          a-reg b-reg i-reg visual-mem real-mem)
                (equal m (big-machine mar read write dtack reset
                                 no-store data-out
                                 reg-file addr-out c-flag v-flag z-flag n-flag
                                 a-reg b-reg i-reg
                                 visual-mem real-mem
                                 memory-watch-dog-history
                                 (list (list dt1 t) (list dt2 t) (list dt3 t)))))
           (and (equal (car m) (nat-to-bv 0 (nxsz)))
                (equal (cadr m) f)
                (equal (caddr m) f)
                (equal (caddddr m) t)
                (equal (nth 0 (cadddddddr m))
                       (nat-to-bv 0 (machine-size)))))
    ((disable mar no-store-with-ifs
            data-out-with-ifs reg-file addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg
            b-reg i-reg-with-ifs visual-mem real-mem length-update-nth)))

(disable reset-to-state-0)

(defn list-of-n-plus-1-dtack-off-reset-on (count)
  (if (zerop count)
      (list (list f t))
      (cons (list f t)
            (list-of-n-plus-1-dtack-off-reset-on (sub1 count)))))

(prove-lemma state-0-to-0-wait-help (rewrite)
  (implies (equal mar0 (nat-to-bv 0 (nxsz)))
           (equal (big-machine mar0 f f dtack t
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (cons (list dt-any t) oracle))
                  (big-machine mar0 f f (fix-bool dt-any) t
                               no-store data-out
                               (update-nth t 0 reg-file (nat-to-bv 0 (machine-size)))
                               addr-out c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               (trunc (default-visual-mem-value) (machine-size))
                               real-mem
                               (watch-dog f f (fix-bool dt-any) data-out addr-out)
                               oracle))))

(disable state-0-to-0-wait-help)

(defn state-0-to-0-induction (dtack data-out reg-file addr-out visual-mem
                                    watch-dog n)
  (if (zerop n)
      t
      (state-0-to-0-induction
        f
        data-out
        (update-nth t 0 reg-file (nat-to-bv 0 (machine-size)))
        addr-out
        (trunc (default-visual-mem-value) (machine-size))
        (watch-dog f f f data-out addr-out)
        (sub1 n))))
                       
(prove-lemma state-0-to-0-wait (rewrite)
  (implies (equal mar0 (nat-to-bv 0 (nxsz)))
           (equal (big-machine mar0 f f dtack t
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list-of-n-plus-1-dtack-off-reset-on n))
                  (list (nat-to-bv 0 (nxsz)) f f f t
                        no-store data-out
                        (update-nth t 0 reg-file (nat-to-bv 0 (machine-size)))
                        addr-out c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) (machine-size)) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable mar read write no-store-with-ifs
            data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output
            bv-subtracter-output b-store-alu-result
            append open-big-machine-on-listp
            update-nth nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-0-to-0-wait-help)
   (induct (state-0-to-0-induction dtack data-out reg-file addr-out visual-mem
                                   watch-dog-history n))))

(disable state-0-to-0-wait)


(prove-lemma state-0-to-1 (rewrite)
  (implies (equal mar0 (nat-to-bv 0 (nxsz)))
           (equal (big-machine mar0 f f dtack t
                               no-store data-out
                               reg-file
                               addr-out c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               memory-watch-dog-history
                               (list (list dt-any1 f) (list dt-any2 f)))
                  (list (nat-to-bv 1 (nxsz))
                        f f (fix-bool dt-any2) f no-store data-out
                        (update-nth t 0 reg-file (nat-to-bv 0 (machine-size)))
                        addr-out c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16)
                        real-mem
                        (watch-dog f f (fix-bool dt-any2) data-out addr-out))))
    ((disable bv-adder-output bv-subtracter-output b-store-alu-result)
     (hands-off bv-alu-cv)))

(disable state-0-to-1)

(defn state-0-to-0-wait-to-1-oracle (n)
  (append (list-of-n-plus-1-dtack-off-reset-on n)
          (list (list f f) (list f f))))

;  After the MAR has been set to zero, this lemma describes the steps taken by
;  FM8501 to prepare itself for executing instructions.

(prove-lemma state-0-to-0-wait-to-1 (rewrite)
  (implies (and (standard-hyps mar0 f f dtack t no-store data-out
                          reg-file addr-out c-flag v-flag z-flag n-flag
                          a-reg b-reg i-reg visual-mem real-mem)
                (equal mar0 (nat-to-bv 0 (nxsz))))
           (equal (big-machine mar0 f f dtack t
                               no-store data-out
                               reg-file
                               addr-out c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (state-0-to-0-wait-to-1-oracle n))
                  (list (nat-to-bv 1 (nxsz))
                        f f f f no-store data-out
                        (update-nth t 0 reg-file (nat-to-bv 0 (machine-size)))
                        addr-out c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable no-store-with-ifs data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output bv-subtracter-output
            b-store-alu-result append open-big-machine-on-listp update-nth
            nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-0-to-0-wait
           state-0-to-1)))

(disable state-0-to-0-wait-to-1)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          "big-machine" instruction loop -- micro-state by micro-state        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Fetch the instruction, and increment the PC                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; We are about to embark on a litany of lemmas that move us from one microcode
; state to another.  By inspection of the oracles used below one can deduce the
; timing diagrams.  For example, the lemma below moves us from microcode state 
; 1, where mar=1, and read, write, and reset are f, to microcode state 2, where
; mar=2, read, write, dtack and reset are f, the pc has been incremented,
; and addr-out contains the old pc.  To move from state 1 to 2, we need
; one clock tick with both dtack and reset f.

; We will similarly move through every state, some of which have several
; substates as we set lines, wait for acknowledgment, and then move.
; Once we get all the way through the microcode, we will append together
; the oracles to get an oracle that moves us all the way around from state 1
; to state 1.

; These lemmas make it perfectly clear what each state in the microcode does
; and how long each takes.

(prove-lemma state-1-to-2 (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar1 (nat-to-bv 1 (nxsz))))
           (equal (big-machine mar1 f f dtack f
                               no-store data-out
                               reg-file
                               addr-out c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               memory-watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 2 (nxsz))
                        f f f f no-store data-out
                        (update-nth t 0 reg-file (v-nat-inc (nth 0 reg-file)))
                        (nth 0 reg-file) c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16)
                        real-mem
                        (watch-dog f f f data-out addr-out))))
    ((disable bv-adder-output bv-subtracter-output b-store-alu-result)
     (hands-off bv-alu-cv)
     (enable bv-incrementer-truncates-to-machine-size)))

(disable state-1-to-2)


(prove-lemma state-2-to-3-init (rewrite)
  (implies (equal mar2 (nat-to-bv 2 (nxsz)))
           (equal (big-machine mar2 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 2 (nxsz))
                        t f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result)
   (hands-off bv-alu-cv)))

(defn list-of-n-plus-1-dtack-reset-off (count)
  (if (zerop count)
      (list (list f f))
      (cons (list f f)
            (list-of-n-plus-1-dtack-reset-off (sub1 count)))))

(prove-lemma state-2-to-2-wait-help (rewrite)
  (implies (equal mar2 (nat-to-bv 2 (nxsz)))
           (equal (big-machine mar2 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (cons (list f f) oracle))
                  (big-machine mar2 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               (trunc (default-visual-mem-value) (machine-size))
                               real-mem
                               (watch-dog t f f data-out addr-out)
                               oracle))))

(defn state-2-to-2-induction (dtack data-out addr-out visual-mem
                                    watch-dog-history n)
  (if (zerop n)
      t
      (state-2-to-2-induction
        f
        data-out
        addr-out
        (trunc (default-visual-mem-value) (machine-size))
        (watch-dog t f f data-out addr-out)
        (sub1 n))))

(prove-lemma state-2-to-3-wait (rewrite)
  (implies (equal mar2 (nat-to-bv 2 (nxsz)))
           (equal (big-machine mar2 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list-of-n-plus-1-dtack-reset-off n))
                  (list (nat-to-bv 2 (nxsz))
                        t f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog t f f data-out addr-out))))
  ((disable no-store-with-ifs data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output bv-subtracter-output
            b-store-alu-result append open-big-machine-on-listp update-nth
            nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (induct (state-2-to-2-induction dtack data-out addr-out visual-mem
                                   watch-dog-history
                                   n))))

(disable state-2-to-3-wait)

(prove-lemma upper-bound-bridge (rewrite)
  (implies (equal n (exp 2 (size a)))
           (lessp (bv-to-nat a) n)))

(prove-lemma state-2-to-3-step3 (rewrite)
  (implies (and (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (sizep addr-out (machine-size))
                (equal mar2 (nat-to-bv 2 (nxsz)))
                (equal visual-mem (v-nth addr-out real-mem)))
           (equal (big-machine mar2 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f f data-out addr-out)
                               (list (list t f) (list t f)))
                  (list (nat-to-bv 3 (nxsz))
                        t f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (v-nth addr-out real-mem) real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result)
   (hands-off bv-alu-cv)))

(disable state-2-to-3-step3)

(prove-lemma state-3-to-4 (rewrite)
  (implies (and (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (sizep addr-out (machine-size))
                (equal mar3 (nat-to-bv 3 (nxsz)))
                (equal visual-mem (v-nth addr-out real-mem)))
           (equal (big-machine mar3 t f t f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f t data-out addr-out)
                               (list (list t f)))
                  (list (nat-to-bv 4 (nxsz))
                        f f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg (v-nth addr-out real-mem)
                        (v-nth addr-out real-mem) real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result)
   (hands-off bv-alu-cv)))

(disable state-3-to-4)

;  This proof is required because it is impossible to keep "APPEND"
;  from opening up on constants.  The opening does not allow 
;  "BIG-MACHINE-APPEND" to apply because the 'append' will have
;  disappeared before it get a chance to apply.

(prove-lemma state-2-to-3-step3-to-4 (rewrite)
  (implies (and (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (sizep addr-out (machine-size))
                (equal mar2 (nat-to-bv 2 (nxsz))))
           (equal (big-machine mar2 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f f data-out addr-out)
                               (list (list t f) (list t f) (list t f)))
                  (list (nat-to-bv 4 (nxsz))
                        f f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg (v-nth addr-out real-mem)
                        (v-nth addr-out real-mem) real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            big-machine-append)
   (hands-off bv-alu-cv)))

(disable state-2-to-3-step3-to-4)

(defn fetch-ir-oracle (n)
  (append (list (list f f))
          (append (list (list f f))
                  (append (list-of-n-plus-1-dtack-reset-off n)
                          (list (list t f) (list t f) (list t f))))))

(prove-lemma state-1-to-4 (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (sizep addr-out (machine-size))
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (equal mar1 (nat-to-bv 1 (nxsz))))
           (equal (big-machine mar1 f f f f
                               no-store data-out
                               reg-file
                               addr-out c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               memory-watch-dog-history
                               (fetch-ir-oracle n))
                  (list (nat-to-bv 4 (nxsz))
                        f f t f no-store data-out
                        (update-nth t 0 reg-file (v-nat-inc (nth 0 reg-file)))
                        (nth 0 reg-file) c-flag v-flag z-flag n-flag
                        a-reg b-reg (v-nth (nth 0 reg-file) real-mem)
                        (v-nth (nth 0 reg-file) real-mem) real-mem
                        (watch-dog t f t data-out (nth 0 reg-file)))))
    ((disable mar read write no-store-with-ifs
              data-out-with-ifs addr-out c-flag-with-ifs
              v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
              i-reg-with-ifs visual-mem real-mem bv-adder-output
              bv-subtracter-output b-store-alu-result
              append open-big-machine-on-listp
              update-nth nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
     (hands-off bv-alu-cv)
     (enable state-1-to-2
             state-2-to-3-init
             state-2-to-3-wait
             state-2-to-3-step3-to-4
             )))

(disable state-1-to-4)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Some size lemmas                                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma size-bv-reg-select (rewrite)
  (equal (size (bv-reg-select i-reg mar reset)) 3))

(prove-lemma size-bv-oprd-a (rewrite)
  (equal (size (bv-oprd-a i-reg)) 3))

(prove-lemma size-bv-oprd-b (rewrite)
  (equal (size (bv-oprd-b i-reg)) 3))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Fetch operand A, doing pre-decrement if necessary                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn fetch-oprd-a-reg-file (i-reg reg-file)
  (update-v-nth (b-indirect-reg-a-dec i-reg)
                (bv-oprd-a i-reg)
                reg-file
                (v-nat-dec (v-nth (bv-oprd-a i-reg)
                                  reg-file))))

(prove-lemma every-member-sizep-update-nth (rewrite)
  (implies (and (equal (size x) width)
                (every-member-sizep lst width))
           (every-member-sizep (update-nth bool n lst x) width)))

;  Both of the following two lemmas are needed, as we sometimes have RAMP enabled.

(prove-lemma ramp-fetch-oprd-a-reg-file (rewrite)
  (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8))
           (and (equal (length (fetch-oprd-a-reg-file i-reg reg-file)) 8)
                (every-member-sizep (fetch-oprd-a-reg-file i-reg reg-file) m)))
  ((disable update-nth bv-oprd-a)))

(prove-lemma ramp-fetch-oprd-a-reg-file-2 (rewrite)
  (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8))
           (ramp (fetch-oprd-a-reg-file i-reg reg-file) m 8))
  ((disable update-nth bv-oprd-a)))

(defn fetch-oprd-a-addr-out (i-reg reg-file)
  (if (b-indirect-reg-a-dec i-reg)
      (v-nat-dec (v-nth (bv-oprd-a i-reg) reg-file))
      (v-nth (bv-oprd-a i-reg) reg-file)))

(prove-lemma sizep-fetch-oprd-a-addr-out (rewrite)
  (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8))
           (equal (size (fetch-oprd-a-addr-out i-reg reg-file)) m))
  ((disable bv-oprd-a)))

(prove-lemma state-4-to-5 (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar4 (nat-to-bv 4 (nxsz))))
           (equal (big-machine mar4 f f t f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog
                               (list (list f f)))
                  (list (nat-to-bv 5 (nxsz))
                        f f f f no-store data-out
                        (fetch-oprd-a-reg-file i-reg reg-file)
                        (fetch-oprd-a-addr-out i-reg reg-file)
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            v-nat-dec v-nat-inc fix-bool bv-oprd-a)
   (hands-off bv-alu-cv)
   (enable bv-decrementer-truncates-to-machine-size
           bv-incrementer-truncates-to-machine-size)))

(disable state-4-to-5)

;  The next two prove-lemmas are of type nil -- we never use them as
;  rewrite rules.  Ideally we would like to append together the two clocks
;  for state-5-to-6-reg and state-6-to-7-reg.  But the two clocks are both
;  constant so the append computes and big-machine-append will not apply.
;  So we will actually prove state-4-to-5-to-6-to-7-reg as one rewrite rule.
;  But for the sake of exposition, we prove individual lemmas about each
;  state transition.

(prove-lemma state-5-to-6-reg nil
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar5 (nat-to-bv 5 (nxsz)))
                (b-direct-reg-a i-reg))
           (equal (big-machine mar5 f f dt-any f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 6 (nxsz))
                        f f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-a-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(prove-lemma state-6-to-7-reg nil
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar6 (nat-to-bv 6 (nxsz)))
                (b-direct-reg-a i-reg))
           (equal (big-machine mar6 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 7 (nxsz))
                        f f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        (v-nth (bv-oprd-a i-reg) reg-file) b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            bv-oprd-a b-indirect-reg-a-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(prove-lemma state-5-to-6-mem-init (rewrite)
  (implies (and (equal mar5 (nat-to-bv 5 (nxsz)))
                (not (b-direct-reg-a i-reg)))
           (equal (big-machine mar5 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               memory-watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 5 (nxsz))
                        t f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-a-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(disable state-5-to-6-mem-init)


(prove-lemma state-5-to-6-mem-help (rewrite)
  (implies (and (equal mar5 (nat-to-bv 5 (nxsz)))
                (not (b-direct-reg-a i-reg)))
           (equal (big-machine mar5 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (cons (list f f) oracle))
                  (big-machine mar5 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               (trunc (default-visual-mem-value) (machine-size))
                               real-mem
                               (watch-dog t f f data-out addr-out)
                               oracle))))

(disable state-5-to-6-mem-help)


(prove-lemma state-5-to-6-mem-wait (rewrite)
  (implies (and (equal mar5 (nat-to-bv 5 (nxsz)))
                (not (b-direct-reg-a i-reg)))
           (equal (big-machine mar5 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list-of-n-plus-1-dtack-reset-off n))
                  (list (nat-to-bv 5 (nxsz))
                        t f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog t f f data-out addr-out))))
  ((disable no-store-with-ifs data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output bv-subtracter-output
            b-store-alu-result append open-big-machine-on-listp update-nth
            nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-5-to-6-mem-help)
   (induct (state-2-to-2-induction dtack data-out addr-out visual-mem   ;
                                   watch-dog-history
                                   n))))

(disable state-5-to-6-mem-wait)


; The next two lemmas we never use as rewrite rules, for the same reasons
; explained above.

(prove-lemma state-5-to-6-mem-dtack nil
  (implies (and (equal mar5 (nat-to-bv 5 (nxsz)))
                (ramp reg-file (machine-size) 8)
                (sizep addr-out (machine-size))
                (not (b-direct-reg-a i-reg)))
           (equal (big-machine mar5 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f f data-out addr-out)
                               (list (list t f) (list t f)))
                  (list (nat-to-bv 6 (nxsz))
                        t f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (v-nth addr-out real-mem) (machine-size))
                        real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-a-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(prove-lemma state-6-to-7-mem nil
  (implies (and (equal mar6 (nat-to-bv 6 (nxsz)))
                (ramp reg-file (machine-size) 8)
                (sizep visual-mem (machine-size))
                (sizep addr-out (machine-size))
                (not (b-direct-reg-a i-reg)))
           (equal (big-machine mar6 t f t f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f t data-out addr-out)
                               (list (list t f)))
                  (list (nat-to-bv 7 (nxsz))
                        f f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        visual-mem b-reg i-reg
                        (trunc (v-nth addr-out real-mem) (machine-size))
                        real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-a-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))


; We now piece together states 4, 5, 6, and 7 for the reg case:

(prove-lemma state-4-to-5-to-6-to-7-reg (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar4 (nat-to-bv 4 (nxsz)))
                (b-direct-reg-a i-reg))
           (equal (big-machine mar4 f f t f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog
                               (list (list f f) (list f f) (list f f)))
                  (list (nat-to-bv 7 (nxsz))
                        f f f f no-store data-out
                        (fetch-oprd-a-reg-file i-reg reg-file)
                        (fetch-oprd-a-addr-out i-reg reg-file)
                        c-flag v-flag z-flag n-flag
                        (v-nth (bv-oprd-a i-reg)
                               (fetch-oprd-a-reg-file i-reg reg-file))
                        b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out
                                   (fetch-oprd-a-addr-out i-reg reg-file)))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            v-nat-dec v-nat-inc fix-bool bv-oprd-a)
   (hands-off bv-alu-cv)
   (enable bv-decrementer-truncates-to-machine-size
           bv-incrementer-truncates-to-machine-size)))

(disable state-4-to-5-to-6-to-7-reg)


; and now we do the same thing for 5, 6, and 7 in the mem case:

(prove-lemma state-5-to-6-to-7-mem-dtack (rewrite)
  (implies (and (equal mar5 (nat-to-bv 5 (nxsz)))
                (ramp reg-file (machine-size) 8)
                (sizep addr-out (machine-size))
                (not (b-direct-reg-a i-reg)))
           (equal (big-machine mar5 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f f data-out addr-out)
                               (list (list t f) (list t f) (list t f)))
                  (list (nat-to-bv 7 (nxsz))
                        f f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        (trunc (v-nth addr-out real-mem) (machine-size)) b-reg i-reg
                        (trunc (v-nth addr-out real-mem) (machine-size))
                        real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-a-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(disable state-5-to-6-to-7-mem-dtack)


; Finally, we do the entire transition from state 4 to state 7.  We first
; define the oracle necessary to drive the machine through the sequence.

(defn fetch-oprd-a-oracle (i-reg n)
  (if (b-direct-reg-a i-reg)
      (list (list f f) (list f f) (list f f))
      (append (list (list f f))
              (append (list (list f f))
                      (append (list-of-n-plus-1-dtack-reset-off n)
                              (list (list t f) (list t f) (list t f)))))))

(prove-lemma every-member-sizep-update-nth-machine-size (rewrite)
  (implies (and (equal (size x) 16)
                (every-member-sizep lst 16))
           (every-member-sizep (update-nth bool n lst x) 16)))

(disable every-member-sizep-update-nth)


(prove-lemma state-4-to-7 (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (sizep addr-out (machine-size))
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (equal mar4 (nat-to-bv 4 (nxsz))))
           (equal (big-machine mar4 f f t f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog
                               (fetch-oprd-a-oracle i-reg n))
                  (list (nat-to-bv 7 (nxsz))
                        f f (not (b-direct-reg-a i-reg)) f
                        no-store data-out
                        (fetch-oprd-a-reg-file i-reg reg-file)
                        (fetch-oprd-a-addr-out i-reg reg-file)
                        c-flag v-flag z-flag n-flag
                        (if (b-direct-reg-a i-reg)
                            (v-nth (bv-oprd-a i-reg)
                                   (fetch-oprd-a-reg-file i-reg reg-file))
                            (v-nth (fetch-oprd-a-addr-out i-reg reg-file)
                                   real-mem))
                        b-reg i-reg
                        (if (b-direct-reg-a i-reg)
                            (trunc (default-visual-mem-value) 16)
                            (v-nth (fetch-oprd-a-addr-out i-reg reg-file)
                                   real-mem))
                        real-mem
                        (watch-dog (not (b-direct-reg-a i-reg))
                                   f
                                   (not (b-direct-reg-a i-reg))
                                   data-out
                                   (fetch-oprd-a-addr-out i-reg reg-file)))))
  ((disable fetch-oprd-a-reg-file fetch-oprd-a-addr-out
            mar read write no-store-with-ifs
            data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output
            bv-subtracter-output b-store-alu-result
            append open-big-machine-on-listp
            update-nth nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
     (hands-off bv-alu-cv)
     (enable state-4-to-5
             state-4-to-5-to-6-to-7-reg
             state-5-to-6-mem-init
             state-5-to-6-mem-wait
             state-5-to-6-to-7-mem-dtack)))

(disable state-4-to-7)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Fetch operand B, doing pre-decrement if necessary                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



(defn fetch-oprd-b-reg-file (i-reg reg-file)
  (update-v-nth (b-indirect-reg-b-dec i-reg)
                (bv-oprd-b i-reg)
                reg-file
                (v-nat-dec (v-nth (bv-oprd-b i-reg)
                                  reg-file))))

; Both of the following lemmas are needed, as RAMP is enabled sometimes

(prove-lemma ramp-fetch-oprd-b-reg-file (rewrite)
  (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8))
           (and (equal (length (fetch-oprd-b-reg-file i-reg reg-file)) 8)
                (every-member-sizep (fetch-oprd-b-reg-file i-reg reg-file) m)))
  ((disable update-nth bv-oprd-b)))

(prove-lemma ramp-fetch-oprd-b-reg-file-2 (rewrite)
  (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8))
           (ramp (fetch-oprd-b-reg-file i-reg reg-file) m 8))
  ((disable update-nth bv-oprd-b)))

(defn fetch-oprd-b-addr-out (i-reg reg-file)
  (if (b-indirect-reg-b-dec i-reg)
      (v-nat-dec (v-nth (bv-oprd-b i-reg) reg-file))
      (v-nth (bv-oprd-b i-reg) reg-file)))

(prove-lemma sizep-fetch-oprd-b-addr-out (rewrite)
  (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8))
           (equal (size (fetch-oprd-b-addr-out i-reg reg-file)) m))
  ((disable bv-oprd-b)))

(prove-lemma state-7-to-8 (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar7 (nat-to-bv 7 (nxsz))))
           (equal (big-machine mar7 f f dtack f
                       no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog
                               (list (list f f)))
                  (list (nat-to-bv 8 (nxsz))
                        f f f f no-store data-out
                        (fetch-oprd-b-reg-file i-reg reg-file)
                        (fetch-oprd-b-addr-out i-reg reg-file)
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            v-nat-dec v-nat-inc fix-bool bv-oprd-b)
   (hands-off bv-alu-cv)
   (enable bv-decrementer-truncates-to-machine-size
           bv-incrementer-truncates-to-machine-size)))

(disable state-7-to-8)

; The next two lemmas are never used as rewrite rules.

(prove-lemma state-8-to-9-reg nil
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar8 (nat-to-bv 8 (nxsz)))
                (b-direct-reg-b i-reg))
           (equal (big-machine mar8 f f dt-any f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 9 (nxsz))
                        f f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-b-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(prove-lemma state-9-to-10-reg nil
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar9 (nat-to-bv 9 (nxsz)))
                (b-direct-reg-b i-reg))
           (equal (big-machine mar9 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 10 (nxsz))
                        f f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg (v-nth (bv-oprd-b i-reg) reg-file) i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            bv-oprd-b b-indirect-reg-b-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))


(prove-lemma state-8-to-9-mem-init (rewrite)
  (implies (and (equal mar8 (nat-to-bv 8 (nxsz)))
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar8 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               memory-watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 8 (nxsz))
                        t f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-b-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(disable state-8-to-9-mem-init)


(prove-lemma state-8-to-9-mem-help (rewrite)
  (implies (and (equal mar8 (nat-to-bv 8 (nxsz)))
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar8 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (cons (list f f) oracle))
                  (big-machine mar8 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               (trunc (default-visual-mem-value) (machine-size))
                               real-mem
                               (watch-dog t f f data-out addr-out)
                               oracle))))

(disable state-8-to-9-mem-help)


(prove-lemma state-8-to-9-mem-wait (rewrite)
  (implies (and (equal mar8 (nat-to-bv 8 (nxsz)))
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar8 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list-of-n-plus-1-dtack-reset-off n))
                  (list (nat-to-bv 8 (nxsz))
                        t f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog t f f data-out addr-out))))
  ((disable no-store-with-ifs data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output bv-subtracter-output
            b-store-alu-result append open-big-machine-on-listp update-nth
            nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-8-to-9-mem-help)
   (induct (state-2-to-2-induction dtack data-out addr-out visual-mem
                                   watch-dog-history
                                   n))))

(disable state-8-to-9-mem-wait)


; the next two are never used as rewrites.

(prove-lemma state-8-to-9-mem-dtack nil
  (implies (and (equal mar8 (nat-to-bv 8 (nxsz)))
                (ramp reg-file (machine-size) 8)
                (sizep addr-out (machine-size))
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar8 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f f data-out addr-out)
                               (list (list t f) (list t f)))
                  (list (nat-to-bv 9 (nxsz))
                        t f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (v-nth addr-out real-mem) (machine-size))
                        real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-a-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))


(prove-lemma state-9-to-10-mem nil
  (implies (and (equal mar9 (nat-to-bv 9 (nxsz)))
                (ramp reg-file (machine-size) 8)
                (sizep visual-mem (machine-size))
                (sizep addr-out (machine-size))
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar9 t f t f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f t data-out addr-out)
                               (list (list t f)))
                  (list (nat-to-bv 10 (nxsz))
                        f f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg visual-mem i-reg
                        (trunc (v-nth addr-out real-mem) (machine-size))
                        real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-b-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

; We now piece together states 7, 8, 9, and 10 for the reg case:

(prove-lemma state-7-to-8-to-9-to-10-reg (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar7 (nat-to-bv 7 (nxsz)))
                (b-direct-reg-b i-reg))
           (equal (big-machine mar7 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog
                               (list (list f f) (list f f) (list f f)))
                  (list (nat-to-bv 10 (nxsz))
                        f f f f no-store data-out
                        (fetch-oprd-b-reg-file i-reg reg-file)
                        (fetch-oprd-b-addr-out i-reg reg-file)
                        c-flag v-flag z-flag n-flag
                        a-reg
                        (v-nth (bv-oprd-b i-reg)
                               (fetch-oprd-b-reg-file i-reg reg-file))
                        i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out
                                   (fetch-oprd-b-addr-out i-reg reg-file)))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            v-nat-dec v-nat-inc fix-bool bv-oprd-a)
   (hands-off bv-alu-cv)
   (enable bv-decrementer-truncates-to-machine-size
           bv-incrementer-truncates-to-machine-size)))

(disable state-7-to-8-to-9-to-10-reg)


; and now we do the same thing for 8, 9 and 10 in the mem case.

(prove-lemma state-8-to-9-to-10-mem-dtack (rewrite)
  (implies (and (equal mar8 (nat-to-bv 8 (nxsz)))
                (ramp reg-file (machine-size) 8)
                (sizep addr-out (machine-size))
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar8 t f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog t f f data-out addr-out)
                               (list (list t f) (list t f) (list t f)))
                  (list (nat-to-bv 10 (nxsz))
                        f f t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg
                        (trunc (v-nth addr-out real-mem) (machine-size))
                        i-reg
                        (trunc (v-nth addr-out real-mem) (machine-size))
                        real-mem
                        (watch-dog t f t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-a-dec v-nat-dec v-nat-inc bv-oprd-b)
   (hands-off bv-alu-cv)))

(disable state-5-to-6-to-7-mem-dtack)


; Finally, we do the entire transition from state 7 to state 10.  We first
; define the oracle necessary to drive the machine through the sequence.

(defn fetch-oprd-b-oracle (i-reg n)
  (if (b-direct-reg-b i-reg)
      (list (list f f) (list f f) (list f f))
      (append (list (list f f))
              (append (list (list f f))
                      (append (list-of-n-plus-1-dtack-reset-off n)
                              (list (list t f) (list t f) (list t f)))))))


(prove-lemma state-7-to-10 (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (sizep addr-out (machine-size))
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (equal mar7 (nat-to-bv 7 (nxsz))))
           (equal (big-machine mar7 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog
                               (fetch-oprd-b-oracle i-reg n))
                  (list (nat-to-bv 10 (nxsz))
                        f f
                        (not (b-direct-reg-b i-reg))
                        f
                        no-store data-out
                        (fetch-oprd-b-reg-file i-reg reg-file)
                        (fetch-oprd-b-addr-out i-reg reg-file)
                        c-flag v-flag z-flag n-flag
                        a-reg
                        (if (b-direct-reg-b i-reg)
                            (v-nth (bv-oprd-b i-reg)
                                   (fetch-oprd-b-reg-file i-reg reg-file))
                            (v-nth (fetch-oprd-b-addr-out i-reg reg-file)
                                   real-mem))
                        i-reg
                        (if (b-direct-reg-b i-reg)
                            (trunc (default-visual-mem-value) 16)
                            (v-nth (fetch-oprd-b-addr-out i-reg reg-file)
                                   real-mem))
                        real-mem
                        (watch-dog (not (b-direct-reg-b i-reg))
                                   f
                                   (not (b-direct-reg-b i-reg))
                                   data-out
                                   (fetch-oprd-b-addr-out i-reg reg-file)))))
  ((disable fetch-oprd-b-reg-file fetch-oprd-b-addr-out
            mar read write no-store-with-ifs
            data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output
            bv-subtracter-output b-store-alu-result
            append open-big-machine-on-listp
            update-nth nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-7-to-8
           state-7-to-8-to-9-to-10-reg
           state-8-to-9-mem-init
           state-8-to-9-mem-wait
           state-8-to-9-to-10-mem-dtack)))

(disable state-7-to-10)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                   ALU, results to memory or register                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn alu-c-flag (i-reg a-reg b-reg c-flag)
  (if (b-cc-set i-reg)
      (c (bv-alu-cv a-reg b-reg c-flag
                    (bv-alu-op-code i-reg)))
      c-flag))

(defn alu-v-flag (i-reg a-reg b-reg c-flag v-flag)
  (if (b-cc-set i-reg)
      (v (bv-alu-cv a-reg b-reg c-flag
                    (bv-alu-op-code i-reg)))
      v-flag))

(defn alu-z-flag (i-reg a-reg b-reg c-flag z-flag)
  (if (b-cc-set i-reg)
      (b-bv-zerop (bv (bv-alu-cv a-reg b-reg c-flag
                                 (bv-alu-op-code i-reg))))
      z-flag))

(defn alu-n-flag (i-reg a-reg b-reg c-flag n-flag)
  (if (b-cc-set i-reg)
      (bitn (bv (bv-alu-cv a-reg b-reg c-flag
                           (bv-alu-op-code i-reg)))
            (machine-size))
      n-flag))

(prove-lemma boolp-alu-c-flag (rewrite)
  (implies (boolp c-flag)
           (boolp (alu-c-flag i-reg a-reg b-reg c-flag)))
  ((enable boolp)))

(prove-lemma boolp-alu-v-flag (rewrite)
  (implies (boolp v-flag)
           (boolp (alu-v-flag i-reg a-reg b-reg c-flag v-flag)))
  ((enable boolp)))

(prove-lemma boolp-alu-z-flag (rewrite)
  (implies (boolp z-flag)
           (boolp (alu-z-flag i-reg a-reg b-reg c-flag z-flag)))
  ((enable boolp)))

(prove-lemma boolp-alu-n-flag (rewrite)
  (implies (boolp n-flag)
           (boolp (alu-n-flag i-reg a-reg b-reg c-flag n-flag)))
  ((enable boolp)))

(prove-lemma state-10-to-11 (rewrite)
  (implies (and (equal mar10 (nat-to-bv 10 (nxsz)))
                (boolp no-store)
                (boolp c-flag)
                (boolp v-flag)
                (boolp n-flag)
                (boolp z-flag)
                (sizep data-out (machine-size)))
           (equal (big-machine mar10 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 11 (nxsz))
                        f f f f
                        (not (b-store-alu-result c-flag v-flag z-flag n-flag i-reg))
                        (bv (bv-alu-cv a-reg b-reg c-flag
                                       (bv-alu-op-code i-reg)))
                        reg-file addr-out
                        (alu-c-flag i-reg a-reg b-reg c-flag)
                        (alu-v-flag i-reg a-reg b-reg c-flag v-flag)
                        (alu-z-flag i-reg a-reg b-reg c-flag z-flag)
                        (alu-n-flag i-reg a-reg b-reg c-flag n-flag)
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            bv-oprd-b b-indirect-reg-b-dec v-nat-dec v-nat-inc bv-alu-op-code
            b-store-alu-result-with-ifs b-bv-zerop)
   (hands-off bv-alu-cv)))

(disable state-10-to-11)
(disable alu-c-flag)
(disable alu-v-flag)
(disable alu-z-flag)
(disable alu-n-flag)

(prove-lemma state-11-to-12-reg nil
  (implies (and (ramp reg-file (machine-size) 8)
                (sizep data-out (machine-size))
                (equal mar11 (nat-to-bv 11 (nxsz)))
                (b-direct-reg-b i-reg))
           (equal (big-machine mar11 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 12 (nxsz))
                        f f f f no-store data-out
                        (update-v-nth (not no-store)
                                      (bv-oprd-b i-reg)
                                      reg-file
                                      data-out)
                        addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-b-dec v-nat-dec v-nat-inc bv-oprd-b)
   (hands-off bv-alu-cv)))

(prove-lemma state-11-to-12-mem-no-store nil
  (implies (and (equal mar11 (nat-to-bv 11 (nxsz)))
                (equal no-store t)
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar11 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 12 (nxsz))
                        f f f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16)
                        real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-b-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))


(prove-lemma state-11-to-12-mem-init-store (rewrite)
  (implies (and (equal mar11 (nat-to-bv 11 (nxsz)))
                (equal no-store f)
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar11 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 11 (nxsz))
                        f t f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16)
                        real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-b-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(disable state-11-to-12-mem-init-store)


(prove-lemma state-11-to-12-mem-help (rewrite)
  (implies (and (equal mar11 (nat-to-bv 11 (nxsz)))
                (equal no-store f)
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar11 f t f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (cons (list f f) oracle))
                  (big-machine mar11 f t f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               (trunc (default-visual-mem-value) (machine-size))
                               real-mem
                               (watch-dog f t f data-out addr-out)
                               oracle))))

(disable state-11-to-12-mem-help)

(defn state-11-to-11-induction (dtack data-out addr-out visual-mem
                                      watch-dog-history n)
  (if (zerop n)
      t
      (state-11-to-11-induction
        f
        data-out
        addr-out
        (trunc (default-visual-mem-value) (machine-size))
        (watch-dog f t f data-out addr-out)
        (sub1 n))))

(prove-lemma state-11-to-12-mem-wait-store (rewrite)
  (implies (and (equal mar11 (nat-to-bv 11 (nxsz)))
                (equal no-store f)
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar11 f t f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list-of-n-plus-1-dtack-reset-off n))
                  (list (nat-to-bv 11 (nxsz))
                        f t f f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f t f data-out addr-out))))
  ((disable no-store-with-ifs data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output bv-subtracter-output
            b-store-alu-result append open-big-machine-on-listp update-nth
            nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-11-to-12-mem-help)
   (induct (state-11-to-11-induction dtack data-out addr-out visual-mem
                                     watch-dog-history
                                     n))))

(disable state-11-to-12-mem-wait-store)


(prove-lemma state-11-to-12-mem-dtack-store (rewrite)
  (implies (and (sizep addr-out (machine-size))
                (equal mar11 (nat-to-bv 11 (nxsz)))
                (equal no-store f)
                (not (b-direct-reg-b i-reg)))
           (equal (big-machine mar11 f t f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog f t f data-out addr-out)
                               (list (list t f) (list t f)))
                  (list (nat-to-bv 12 (nxsz))
                        f t t f no-store data-out
                        reg-file addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16)
                        (update-v-nth t addr-out real-mem data-out)
                        (watch-dog f t t data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            b-indirect-reg-b-dec v-nat-dec v-nat-inc)
   (hands-off bv-alu-cv)))

(disable state-11-to-12-mem-dtack-store)

(prove-lemma state-10-to-12-reg (rewrite)
  (implies (and (equal mar10 (nat-to-bv 10 (nxsz)))
                (boolp no-store)
                (boolp c-flag)
                (boolp v-flag)
                (boolp n-flag)
                (boolp z-flag)
                (sizep data-out (machine-size))
                (sizep a-reg (machine-size))
                (ramp reg-file (machine-size) 8)
                (b-direct-reg-b i-reg))
           (equal (big-machine mar10 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f) (list f f)))
                  (list (nat-to-bv 12 (nxsz))
                        f f f f
                        (not (b-store-alu-result c-flag v-flag z-flag n-flag i-reg))
                        (bv (bv-alu-cv a-reg b-reg c-flag
                                       (bv-alu-op-code i-reg)))
                        (update-v-nth
                          (b-store-alu-result c-flag v-flag z-flag n-flag i-reg)
                          (bv-oprd-b i-reg)
                          reg-file
                          (bv (bv-alu-cv a-reg b-reg c-flag
                                         (bv-alu-op-code i-reg))))
                        addr-out
                        (alu-c-flag i-reg a-reg b-reg c-flag)
                        (alu-v-flag i-reg a-reg b-reg c-flag v-flag)
                        (alu-z-flag i-reg a-reg b-reg c-flag z-flag)
                        (alu-n-flag i-reg a-reg b-reg c-flag n-flag)
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f
                                   (bv (bv-alu-cv a-reg b-reg c-flag
                                                  (bv-alu-op-code i-reg)))
                                   addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            bv-oprd-b b-indirect-reg-b-dec v-nat-dec v-nat-inc bv-alu-op-code
            b-store-alu-result-with-ifs b-bv-zerop)
   (enable alu-c-flag alu-v-flag alu-z-flag alu-n-flag)
   (hands-off bv-alu-cv)))

(disable state-10-to-12-reg)

(prove-lemma state-10-to-12-mem-no-store (rewrite)
  (implies (and (equal mar10 (nat-to-bv 10 (nxsz)))
                (boolp c-flag)
                (boolp v-flag)
                (boolp n-flag)
                (boolp z-flag)
                (sizep data-out (machine-size))
                (sizep a-reg (machine-size))
                (not (b-direct-reg-b i-reg))
                (not (b-store-alu-result c-flag v-flag z-flag n-flag i-reg)))
           (equal (big-machine mar10 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f) (list f f)))
                  (list (nat-to-bv 12 (nxsz))
                        f f f f 
                        (not (b-store-alu-result c-flag v-flag z-flag n-flag i-reg))
                        (bv (bv-alu-cv a-reg b-reg c-flag
                                       (bv-alu-op-code i-reg)))
                        reg-file addr-out
                        (alu-c-flag i-reg a-reg b-reg c-flag)
                        (alu-v-flag i-reg a-reg b-reg c-flag v-flag)
                        (alu-z-flag i-reg a-reg b-reg c-flag z-flag)
                        (alu-n-flag i-reg a-reg b-reg c-flag n-flag)
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16)
                        real-mem
                        (watch-dog f f f
                                   (bv (bv-alu-cv a-reg b-reg c-flag
                                                  (bv-alu-op-code i-reg)))
                                   addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            bv-oprd-b b-indirect-reg-b-dec v-nat-dec v-nat-inc bv-alu-op-code
            b-store-alu-result-with-ifs b-bv-zerop)
   (enable alu-c-flag alu-v-flag alu-z-flag alu-n-flag)
   (hands-off bv-alu-cv)))

(disable state-10-to-12-mem-no-store)

(prove-lemma state-10-to-12-mem-store (rewrite)
  (implies (and (equal mar10 (nat-to-bv 10 (nxsz)))
                (boolp no-store)
                (boolp c-flag)
                (boolp v-flag)
                (boolp n-flag)
                (boolp z-flag)
                (sizep data-out (machine-size))
                (sizep addr-out (machine-size))
                (sizep a-reg (machine-size))
                (not (b-direct-reg-b i-reg))
                (b-store-alu-result c-flag v-flag z-flag n-flag i-reg))
           (equal (big-machine mar10 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (append (list (list f f))
                                       (append (list (list f f))
                                               (append
                                                 (list-of-n-plus-1-dtack-reset-off n)
                                                 (list (list t f) (list t f))))))
                  (list (nat-to-bv 12 (nxsz))
                        f t t f
                        (not (b-store-alu-result c-flag v-flag z-flag n-flag i-reg))
                        (bv (bv-alu-cv a-reg b-reg c-flag
                                       (bv-alu-op-code i-reg)))
                        reg-file addr-out
                        (alu-c-flag i-reg a-reg b-reg c-flag)
                        (alu-v-flag i-reg a-reg b-reg c-flag v-flag)
                        (alu-z-flag i-reg a-reg b-reg c-flag z-flag)
                        (alu-n-flag i-reg a-reg b-reg c-flag n-flag)
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16)
                        (update-v-nth t addr-out real-mem
                                      (bv (bv-alu-cv a-reg b-reg c-flag
                                                     (bv-alu-op-code i-reg))))
                        (watch-dog
                          f t t
                          (bv (bv-alu-cv a-reg b-reg c-flag
                                         (bv-alu-op-code i-reg)))
                          addr-out))))
  ((disable ramp
            b-direct-reg-b bv-alu-op-code
            mar read write no-store-with-ifs
            data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output
            bv-subtracter-output b-store-alu-result
            b-store-alu-result-with-ifs
            append open-big-machine-on-listp
            update-nth nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-10-to-11
           state-11-to-12-mem-init-store
           state-11-to-12-mem-wait-store
           state-11-to-12-mem-dtack-store)))

(disable state-10-to-12-mem-store)  

(defn alu-oracle (i-reg c-flag v-flag z-flag n-flag n)
   (if (b-direct-reg-b i-reg)
       (list (list f f) (list f f))
       (if (b-store-alu-result c-flag v-flag z-flag n-flag i-reg)
           (append (list (list f f))
                   (append (list (list f f))
                           (append (list-of-n-plus-1-dtack-reset-off n)
                                   (list (list t f) (list t f)))))
           (list (list f f) (list f f)))))

(prove-lemma update-nth-f (rewrite)
  (equal (update-nth f n lst val) lst))

(defn mem-store-flag (i-reg c-flag v-flag z-flag n-flag)
  (if (b-direct-reg-b i-reg)
      f
      (b-store-alu-result c-flag v-flag z-flag n-flag i-reg)))

(prove-lemma state-10-to-12 (rewrite)
  (implies (and (boolp no-store)
                (boolp c-flag)
                (boolp v-flag)
                (boolp n-flag)
                (boolp z-flag)
                (sizep data-out (machine-size))
                (sizep a-reg (machine-size))
                (sizep addr-out (machine-size))
                (ramp reg-file (machine-size) 8)
                (equal mar10 (nat-to-bv 10 (nxsz))))
           (equal (big-machine mar10 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (alu-oracle i-reg c-flag v-flag z-flag n-flag n))
                      (list (nat-to-bv 12 (nxsz))
                            f
                            (mem-store-flag i-reg c-flag v-flag z-flag n-flag)
                            (mem-store-flag i-reg c-flag v-flag z-flag n-flag)
                            f
                            (not (b-store-alu-result c-flag v-flag z-flag n-flag i-reg))
                            (bv (bv-alu-cv a-reg b-reg c-flag
                                           (bv-alu-op-code i-reg)))
                            (update-v-nth
                                  (and (b-direct-reg-b i-reg)
                                       (b-store-alu-result
                                         c-flag v-flag z-flag n-flag i-reg))
                                  (bv-oprd-b i-reg)
                                  reg-file
                                  (bv (bv-alu-cv a-reg b-reg c-flag
                                                 (bv-alu-op-code i-reg))))
                            addr-out
                            (alu-c-flag i-reg a-reg b-reg c-flag)
                            (alu-v-flag i-reg a-reg b-reg c-flag v-flag)
                            (alu-z-flag i-reg a-reg b-reg c-flag z-flag)
                            (alu-n-flag i-reg a-reg b-reg c-flag n-flag)
                            a-reg b-reg i-reg
                            (trunc (default-visual-mem-value) 16)
                            (update-v-nth (and (not (b-direct-reg-b i-reg))
                                               (b-store-alu-result
                                                 c-flag v-flag z-flag n-flag i-reg))
                                          addr-out real-mem
                                          (bv (bv-alu-cv a-reg b-reg c-flag
                                                         (bv-alu-op-code i-reg))))
                            (watch-dog
                              f
                              (mem-store-flag i-reg c-flag v-flag z-flag n-flag)
                              (mem-store-flag i-reg c-flag v-flag z-flag n-flag)
                              (bv (bv-alu-cv a-reg b-reg c-flag
                                             (bv-alu-op-code i-reg)))
                              addr-out))))
  ((disable ramp
            b-direct-reg-b bv-alu-op-code
            mar read write no-store-with-ifs
            data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output
            bv-subtracter-output b-store-alu-result b-store-alu-result-with-ifs
            append open-big-machine-on-listp big-machine-append
            update-nth nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-10-to-12-reg
           state-10-to-12-mem-no-store
           state-10-to-12-mem-store)))

(disable state-10-to-12)

(disable mem-store-flag)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                  Post-increment operations                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma state-12-to-13 nil
  (implies (and (ramp reg-file (machine-size) 8)
                (or (truep mem-store-flag)
                    (falsep mem-store-flag))
                (equal mar12 (nat-to-bv 12 (nxsz))))
           (equal (big-machine mar12 f
                               mem-store-flag
                               mem-store-flag
                               f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog f mem-store-flag mem-store-flag
                                          data-out addr-out)
                               (list (list mem-store-flag f)))
                  (list (nat-to-bv 13 (nxsz))
                        f f mem-store-flag f no-store data-out
                        (update-v-nth (b-indirect-reg-a-inc i-reg)
                                      (bv-oprd-a i-reg)
                                      reg-file
                                      (v-nat-inc (v-nth (bv-oprd-a i-reg)
                                                        reg-file)))
                        addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f mem-store-flag mem-store-flag data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            v-nat-dec v-nat-inc fix-bool bv-oprd-a)
   (hands-off bv-alu-cv)
   (enable bv-decrementer-truncates-to-machine-size
           bv-incrementer-truncates-to-machine-size)))


(prove-lemma state-13-to-1 nil
  (implies (and (ramp reg-file (machine-size) 8)
                (equal mar13 (nat-to-bv 13 (nxsz))))
           (equal (big-machine mar13 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (list (list f f)))
                  (list (nat-to-bv 1 (nxsz))
                        f f f f no-store data-out
                        (update-v-nth (b-indirect-reg-b-inc i-reg)
                                      (bv-oprd-b i-reg)
                                      reg-file
                                      (v-nat-inc (v-nth (bv-oprd-b i-reg)
                                                        reg-file)))
                        addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            v-nat-dec v-nat-inc fix-bool bv-oprd-b)
   (hands-off bv-alu-cv)
   (enable bv-decrementer-truncates-to-machine-size
           bv-incrementer-truncates-to-machine-size)))

(defn reg-file-post-inc (i-reg reg-file)
  (update-v-nth (b-indirect-reg-b-inc i-reg)
                (bv-oprd-b i-reg)
                (update-v-nth (b-indirect-reg-a-inc i-reg)
                              (bv-oprd-a i-reg)
                              reg-file
                              (v-nat-inc (v-nth (bv-oprd-a i-reg)
                                                reg-file)))
                (v-nat-inc (v-nth (bv-oprd-b i-reg)
                                  (update-v-nth (b-indirect-reg-a-inc i-reg)
                                                (bv-oprd-a i-reg)
                                                reg-file
                                                (v-nat-inc (v-nth (bv-oprd-a i-reg)
                                                                  reg-file)))))))

(prove-lemma state-12-to-1 (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (or (truep mem-store-flag)
                    (falsep mem-store-flag))
                (equal mar12 (nat-to-bv 12 (nxsz))))
           (equal (big-machine mar12 f
                               mem-store-flag
                               mem-store-flag
                               f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               (watch-dog f mem-store-flag mem-store-flag
                                          data-out addr-out)
                               (list (list mem-store-flag f) (list f f)))
                  (list (nat-to-bv 1 (nxsz))
                        f f f f no-store data-out
                        (reg-file-post-inc i-reg reg-file)
                        addr-out
                        c-flag v-flag z-flag n-flag
                        a-reg b-reg i-reg
                        (trunc (default-visual-mem-value) 16) real-mem
                        (watch-dog f f f data-out addr-out))))
  ((disable bv-adder-output bv-subtracter-output b-store-alu-result
            v-nat-dec v-nat-inc fix-bool bv-oprd-a bv-oprd-b b-oprd-mem-ref-with-ifs)
   (hands-off bv-alu-cv)
   (enable bv-decrementer-truncates-to-machine-size
           bv-incrementer-truncates-to-machine-size)))

(disable state-12-to-1)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                  Pasting together the steps                                  ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; In state-4-to-7 we rewrite to something of the form (list ... (if a b c) ...).
; When applying big-machine-append the variable M is bound to the rewritten version
; of this form.  But the rewriter moves the if's out, producing 
; (if a (list ... b ...) (list ... c ...)).  We then, in simplifying the rhs of
; big-machine-append, rewrite (cadr M) to get the new read.  We want it to rewrite to
; f but in fact it rewrites to (cadr (if a (list mar7 f ...) (list mar7 f ...))).
; Then, state-7-to-10 doesn't unify.  So we prove the following two facts.
; Because of these, we don't really care whether our state steppers return
; lists with if's inside or outside.

(prove-lemma car-if (rewrite)
  (equal (car (if a b c)) (if a (car b) (car c))))

(prove-lemma cdr-if (rewrite)
  (equal (cdr (if a b c)) (if a (cdr b) (cdr c))))

(defn reg-file-after-a-b (reg-file real-mem)
  (fetch-oprd-b-reg-file
    (v-nth (nth 0 reg-file) real-mem)
    (fetch-oprd-a-reg-file (v-nth (nth 0 reg-file) real-mem)
                           (update-nth t 0 reg-file (v-nat-inc (nth 0 reg-file))))))

(defn addr-out-after-a-b (reg-file real-mem)
  (fetch-oprd-b-addr-out
    (v-nth (nth 0 reg-file) real-mem)
    (fetch-oprd-a-reg-file (v-nth (nth 0 reg-file) real-mem)
                           (update-nth t 0 reg-file (v-nat-inc (nth 0 reg-file))))))


(defn a-reg-after-a-b (reg-file real-mem)
  (if (b-direct-reg-a (v-nth (nth 0 reg-file) real-mem))
      (v-nth (bv-oprd-a (v-nth (nth 0 reg-file) real-mem))
             (fetch-oprd-a-reg-file
               (v-nth (nth 0 reg-file) real-mem)
               (update-nth t 0 reg-file (v-nat-inc (nth 0 reg-file)))))
      (v-nth (fetch-oprd-a-addr-out
               (v-nth (nth 0 reg-file) real-mem)
               (update-nth t 0 reg-file (v-nat-inc (nth 0 reg-file))))
             real-mem)))

(defn b-reg-after-a-b (reg-file real-mem)
  (if (b-direct-reg-b (v-nth (nth 0 reg-file) real-mem))
      (v-nth (bv-oprd-b (v-nth (nth 0 reg-file) real-mem))
             (fetch-oprd-b-reg-file
               (v-nth (nth 0 reg-file) real-mem)
               (fetch-oprd-a-reg-file (v-nth (nth 0 reg-file) real-mem)
                                      (update-nth t 0 reg-file
                                                  (v-nat-inc (nth 0 reg-file))))))
      (v-nth (fetch-oprd-b-addr-out
               (v-nth (nth 0 reg-file) real-mem)
               (fetch-oprd-a-reg-file (v-nth (nth 0 reg-file) real-mem)
                                      (update-nth t 0 reg-file
                                                  (v-nat-inc (nth 0 reg-file)))))
             real-mem)))

(defn visual-mem-after-a-b (reg-file real-mem)
  (if (b-direct-reg-b (v-nth (nth 0 reg-file) real-mem))
      (trunc (default-visual-mem-value) 16)
      (v-nth (fetch-oprd-b-addr-out
               (v-nth (nth 0 reg-file) real-mem)
               (fetch-oprd-a-reg-file (v-nth (nth 0 reg-file) real-mem)
                                      (update-nth t 0 reg-file
                                                  (v-nat-inc (nth 0 reg-file)))))
             real-mem)))

(defn dtack-after-a-b (reg-file real-mem)
  (not (b-direct-reg-b (v-nth (nth 0 reg-file) real-mem))))

(defn a-b-oracle (reg-file real-mem i n m)
  (append (fetch-ir-oracle i)
          (append (fetch-oprd-a-oracle (v-nth (nth 0 reg-file) real-mem) n)
                  (fetch-oprd-b-oracle (v-nth (nth 0 reg-file) real-mem) m))))

(prove-lemma state-1-to-10 (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (sizep addr-out (machine-size))
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (equal mar1 (nat-to-bv 1 (nxsz))))
           (equal (big-machine mar1 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog
                               (a-b-oracle reg-file real-mem i n m))
                  (list (nat-to-bv 10 (nxsz))
                        f f
                        (dtack-after-a-b reg-file real-mem)
                        f
                        no-store data-out
                        (reg-file-after-a-b reg-file real-mem)
                        (addr-out-after-a-b reg-file real-mem)
                        c-flag v-flag z-flag n-flag
                        (a-reg-after-a-b reg-file real-mem)
                        (b-reg-after-a-b reg-file real-mem)
                        (v-nth (nth 0 reg-file) real-mem)
                        (visual-mem-after-a-b reg-file real-mem)
                        real-mem
                        (watch-dog (dtack-after-a-b reg-file real-mem)
                                   f
                                   (dtack-after-a-b reg-file real-mem)
                                   data-out
                                   (addr-out-after-a-b reg-file real-mem)))))
  ((disable fetch-oprd-a-reg-file fetch-oprd-a-addr-out
            fetch-oprd-b-reg-file fetch-oprd-b-addr-out
            fetch-ir-oracle fetch-oprd-a-oracle fetch-oprd-b-oracle
            b-direct-reg-a b-direct-reg-b
            mar read write no-store-with-ifs
            data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output
            bv-subtracter-output b-store-alu-result
            append open-big-machine-on-listp
            update-nth nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-1-to-4 state-4-to-7 state-7-to-10)))


(defn reg-file-alu (i-reg c-flag v-flag z-flag n-flag reg-file a-reg b-reg)
  (update-v-nth (and (b-direct-reg-b i-reg)
                     (b-store-alu-result
                       c-flag v-flag z-flag n-flag i-reg))
                (bv-oprd-b i-reg)
                reg-file
                (bv (bv-alu-cv a-reg b-reg c-flag
                               (bv-alu-op-code i-reg)))))

(defn reg-file-from-alu-thru-post-inc (i-reg c-flag v-flag z-flag n-flag
                                             reg-file a-reg b-reg)
  (update-v-nth
    (b-indirect-reg-b-inc i-reg)
    (bv-oprd-b i-reg)
    (update-v-nth
      (b-indirect-reg-a-inc i-reg)
      (bv-oprd-a i-reg)
      (reg-file-alu i-reg c-flag v-flag z-flag n-flag reg-file a-reg b-reg)
      (v-nat-inc (v-nth (bv-oprd-a i-reg)
                        (reg-file-alu i-reg c-flag v-flag z-flag n-flag
                                      reg-file a-reg b-reg))))
    (v-nat-inc
      (v-nth (bv-oprd-b i-reg)
             (update-v-nth
               (b-indirect-reg-a-inc i-reg)
               (bv-oprd-a i-reg)
               (reg-file-alu i-reg c-flag v-flag z-flag n-flag reg-file a-reg b-reg)
               (v-nat-inc
                 (v-nth (bv-oprd-a i-reg)
                        (reg-file-alu i-reg c-flag v-flag z-flag n-flag reg-file
                                      a-reg b-reg))))))))

(defn real-mem-thru-post-inc (i-reg c-flag v-flag z-flag n-flag
                                    addr-out real-mem a-reg b-reg)
 (update-v-nth (and (not (b-direct-reg-b i-reg))
                    (b-store-alu-result
                      c-flag v-flag z-flag n-flag i-reg))
               addr-out real-mem
               (bv (bv-alu-cv a-reg b-reg c-flag
                              (bv-alu-op-code i-reg)))))

(defn alu-post-inc-oracle (i-reg c-flag v-flag z-flag n-flag n)
  (append (alu-oracle i-reg c-flag v-flag z-flag n-flag n)
              (list (list (mem-store-flag i-reg c-flag v-flag z-flag n-flag)
                          f)
                    (list f f))))

(prove-lemma ramp-if (rewrite)
  (equal (ramp (if c a b) i j) (if c (ramp a i j) (ramp b i j))))

(prove-lemma ramp-update-nth (rewrite)
  (implies (and (ramp reg-file width number)
                (sizep value width)
                (boolp boolean)
                (not (lessp number place)))
           (ramp (update-nth boolean place reg-file value)
                 width
                 number)))

(prove-lemma state-10-to-1 (rewrite)
  (implies (and (boolp no-store)
                (boolp c-flag)
                (boolp v-flag)
                (boolp n-flag)
                (boolp z-flag)
                (sizep data-out (machine-size))
                (sizep a-reg (machine-size))
                (sizep addr-out (machine-size))
                (ramp reg-file (machine-size) 8)
                (equal mar10 (nat-to-bv 10 (nxsz))))
           (equal (big-machine mar10 f f dtack f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog-history
                               (alu-post-inc-oracle i-reg c-flag v-flag z-flag n-flag n))
                      (list (nat-to-bv 1 (nxsz))
                            f f f f
                            (not (b-store-alu-result c-flag v-flag z-flag n-flag i-reg))
                            (bv (bv-alu-cv a-reg b-reg c-flag
                                           (bv-alu-op-code i-reg)))
                            (reg-file-from-alu-thru-post-inc i-reg c-flag v-flag z-flag
                                                             n-flag reg-file a-reg b-reg)
                            addr-out
                            (alu-c-flag i-reg a-reg b-reg c-flag)
                            (alu-v-flag i-reg a-reg b-reg c-flag v-flag)
                            (alu-z-flag i-reg a-reg b-reg c-flag z-flag)
                            (alu-n-flag i-reg a-reg b-reg c-flag n-flag)
                            a-reg b-reg i-reg
                            (trunc (default-visual-mem-value) 16)
                            (real-mem-thru-post-inc i-reg c-flag v-flag z-flag n-flag
                                                    addr-out real-mem a-reg b-reg)
                            (watch-dog f f f
                                       (bv (bv-alu-cv a-reg b-reg c-flag
                                                      (bv-alu-op-code i-reg)))
                                       addr-out))))
  ((disable alu-oracle alu-c-flag alu-v-flag alu-z-flag alu-n-flag ramp
            b-direct-reg-b bv-alu-op-code 
            mar read write no-store-with-ifs
            data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output
            bv-subtracter-output b-store-alu-result b-store-alu-result-with-ifs
            append open-big-machine-on-listp bv-oprd-a bv-oprd-b 
            update-nth nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-10-to-12 state-12-to-1)))

(disable state-10-to-1)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            The lemmas that follow culminate in lemma STATE-1-to-1            ;;
;;            which is a statement of what FM8501 does upon executing           ;;
;;            an instruction.  FM8501 executes one memory based instruction     ;;
;;            by starting in a state where the MAR is "1", executing some       ;;
;;            of micro-states eventually taking it back to a place where        ;;
;;            MAR is equal to "1".                                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma sizep-a-reg-after-a-b (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (size (a-reg-after-a-b reg-file real-mem))
                  (machine-size)))
  ((disable b-direct-reg-a bv-oprd-a fetch-oprd-a-addr-out update-nth nth)))


(prove-lemma sizep-addr-out-after-a-b (rewrite)
  (implies (ramp reg-file (machine-size) 8)
           (equal (size (addr-out-after-a-b reg-file real-mem))
                  (machine-size)))
  ((disable fetch-oprd-a-reg-file b-indirect-reg-a-dec v-nth bv-oprd-b
            b-indirect-reg-b-dec fetch-oprd-b-addr-out v-nat-dec)))

(prove-lemma ramp-reg-file-after-a-b (rewrite)
  (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8))
           (ramp (reg-file-after-a-b reg-file real-mem) m 8))
  ((disable fetch-oprd-a-reg-file b-indirect-reg-a-dec v-nth bv-oprd-b
            update-nth b-indirect-reg-b-dec fetch-oprd-b-addr-out v-nat-dec)))



(defn state-1-to-1-oracle (reg-file real-mem c-flag v-flag z-flag n-flag
                           ir-wait a-wait b-wait store-wait)
  (append (a-b-oracle reg-file real-mem ir-wait a-wait b-wait)
          (alu-post-inc-oracle (v-nth (nth 0 reg-file) real-mem)
                               c-flag v-flag
                               z-flag n-flag
                               store-wait)))

(prove-lemma state-1-to-1 (rewrite)
  (implies (and (boolp no-store)
                (boolp c-flag)
                (boolp v-flag)
                (boolp n-flag)
                (boolp z-flag)
                (ramp reg-file (machine-size) 8)
                (sizep data-out (machine-size))
                (sizep addr-out (machine-size))
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (equal mar1 (nat-to-bv 1 (nxsz))))
           (equal (big-machine mar1 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem
                               watch-dog
                               (state-1-to-1-oracle reg-file real-mem
                                                    c-flag v-flag z-flag n-flag
                                                    ir-wait a-wait b-wait store-wait))
                  (list (nat-to-bv 1 (nxsz))
                        f f f f
                        (not (b-store-alu-result c-flag v-flag z-flag n-flag
                                                 (v-nth (nth 0 reg-file) real-mem)))
                        (bv (bv-alu-cv (a-reg-after-a-b reg-file real-mem)
                                       (b-reg-after-a-b reg-file real-mem)
                                       c-flag
                                       (bv-alu-op-code
                                         (v-nth (nth 0 reg-file) real-mem))))
                        (reg-file-from-alu-thru-post-inc
                          (v-nth (nth 0 reg-file) real-mem)
                          c-flag v-flag z-flag
                          n-flag
                          (reg-file-after-a-b reg-file real-mem)
                          (a-reg-after-a-b reg-file real-mem)
                          (b-reg-after-a-b reg-file real-mem))
                        (addr-out-after-a-b reg-file real-mem) 
                        (alu-c-flag (v-nth (nth 0 reg-file) real-mem)
                                    (a-reg-after-a-b reg-file real-mem)
                                    (b-reg-after-a-b reg-file real-mem)
                                    c-flag)
                        (alu-v-flag (v-nth (nth 0 reg-file) real-mem)
                                    (a-reg-after-a-b reg-file real-mem)
                                    (b-reg-after-a-b reg-file real-mem)
                                    c-flag v-flag)
                        (alu-z-flag (v-nth (nth 0 reg-file) real-mem)
                                    (a-reg-after-a-b reg-file real-mem)
                                    (b-reg-after-a-b reg-file real-mem)
                                    c-flag z-flag)
                        (alu-n-flag (v-nth (nth 0 reg-file) real-mem)
                                    (a-reg-after-a-b reg-file real-mem)
                                    (b-reg-after-a-b reg-file real-mem)
                                    c-flag n-flag)
                        (a-reg-after-a-b reg-file real-mem)
                        (b-reg-after-a-b reg-file real-mem)
                        (v-nth (nth 0 reg-file) real-mem)
                        (trunc (default-visual-mem-value) 16)
                        (real-mem-thru-post-inc
                          (v-nth (nth 0 reg-file) real-mem)
                          c-flag v-flag z-flag n-flag
                          (addr-out-after-a-b reg-file real-mem)
                          real-mem
                          (a-reg-after-a-b reg-file real-mem)
                          (b-reg-after-a-b reg-file real-mem))
                        (watch-dog f f f
                                   (bv (bv-alu-cv
                                         (a-reg-after-a-b reg-file real-mem)
                                         (b-reg-after-a-b reg-file real-mem)
                                         c-flag
                                         (bv-alu-op-code
                                           (v-nth (nth 0 reg-file) real-mem))))
                                   (addr-out-after-a-b reg-file real-mem)))))
  ((disable reg-file-from-alu-thru-post-inc real-mem-thru-post-inc
            reg-file-after-a-b addr-out-after-a-b a-reg-after-a-b b-reg-after-a-b
            a-b-oracle alu-post-inc-oracle
            alu-c-flag alu-v-flag alu-z-flag alu-n-flag ramp
            bv-alu-op-code 
            b-store-alu-result-with-ifs bv-oprd-a bv-oprd-b v-nth
            fetch-oprd-a-reg-file fetch-oprd-a-addr-out
            fetch-oprd-b-reg-file fetch-oprd-b-addr-out
            fetch-ir-oracle fetch-oprd-a-oracle fetch-oprd-b-oracle
            b-direct-reg-a b-direct-reg-b
            mar read write no-store-with-ifs
            data-out-with-ifs addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output
            bv-subtracter-output b-store-alu-result
            append open-big-machine-on-listp
            update-nth nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat)
   (hands-off bv-alu-cv)
   (enable state-1-to-10 state-10-to-1)))

(disable state-1-to-1)


(prove-lemma nth-update-nth (rewrite)           ; A helping lemma
  (equal (nth i (update-nth c j lst x))
         (if (and (truep c)
                  (equal (fix i) (fix j))
                  (lessp j (length lst)))
             x
             (nth i lst))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Software specification of FM8501.                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Helping definitions for the specification of the software           ;;
;;          machine.  Function SOFT is the actual definition defining           ;;
;;          the operation of the FM8501.                                        ;;
;;                                                                              ;;
;;          When programming the FM8501 the user see eight general purpose      ;;
;;          registers (register file), four flag bits (carry, overflow,         ;;
;;          negative, and zero), and the memory.  Instruction execution         ;;
;;          is accomplished by reading the memory value pointed to by the       ;;
;;          program counter (register 0), and interpreting this memory word     ;;
;;          as an instruction to be executed.  The execution of an instruction  ;;
;;          may modify all visable registers.  The flag registers may be        ;;
;;          updated only once per instruction.  The memory may be updated       ;;
;;          only once per instruction.  The register file may be updated a      ;;
;;          maximum of four times in six opportunities.  The first update to    ;;
;;          the register file, which always occurs, is the incrementing of      ;;
;;          the program counter.  Next comes the possible pre-decrement         ;;
;;          operation of both operands.  The result of the ALU may be next      ;;
;;          stored into the register file.  Lastly, there may be two            ;;
;;          post-increment operations.  An operand cannot be both               ;;
;;          pre-decremented and post-incremented.                               ;;
;;                                                                              ;;
;;          The functions below generate the next state for the memory and      ;;
;;          the register file given an instruction.  These are grouped          ;;
;;          together into an interpreter called SOFT.  SOFT executed one        ;;
;;          instruction per recursive call.                                     ;;
;;                                                                              ;;
;;          The next state for the register file (REG-FILE) is created by       ;;
;;          the composition of several functions.  Each function describes      ;;
;;          the state of the register file at some point through the execution  ;;
;;          of an instruction.  Below are described the operation of the        ;;
;;          functions that update the register file.  All of these functions    ;;
;;          return a complete register file, which they may or may not of       ;;
;;          updated.                                                            ;;
;;                                                                              ;;
;;          reg-file-after-pc-increment --                                      ;;
;;               increments the PC (register 0)                                 ;;
;;                                                                              ;;
;;          reg-file-after-oprd-a-pre-decrement --                              ;;
;;               performs a pre-decrement operation for operand A if required,  ;;
;;               and included is the reg-file-after-pc-increment operation      ;;
;;                                                                              ;;
;;          reg-file-after-oprd-b-pre-decrement --                              ;;
;;               performs a pre-decrement operation for operand B if required,  ;;
;;               and included is the reg-file-after-oprd-a-pre-decrement        ;;
;;               operation                                                      ;;
;;                                                                              ;;
;;          reg-file-after-alu-write --                                         ;;
;;               writes the output of the ALU to the reg-file if required,      ;;
;;               and included is the reg-file-after-oprd-b-pre-decrement        ;;
;;               operation                                                      ;;
;;                                                                              ;;
;;          reg-file-after-oprd-a-post-increment --                             ;;
;;               performs a post-increment operation for operand A if required, ;;
;;               and included is the reg-file-after-alu-write operation         ;;
;;                                                                              ;;
;;          reg-file-after-oprd-b-post-increment --                             ;;
;;               performs a post-increment operation for operand B if required, ;;
;;               and included is the reg-file-after-oprd-a-post-increment       ;;
;;               operation                                                      ;;
;;                                                                              ;;
;;          The ALU requires three operands so its result can be calculated.    ;;
;;          The C-FLAG is readily available, but the A and B value for the      ;;
;;          ALU must be generated under instruction control.  The A value is    ;;
;;          fetched either from the register file or the memory, but not until  ;;
;;          both the PC has been incremented and the operand A pre-decrement    ;;
;;          performed.  The function A-VALUE-FOR-ALU-AFTER-OPRD-A-PRE-DECREMENT ;;
;;          generates the appropriate value.  The B value for the ALU is        ;;
;;          fetched from either the register file or memory, but not until the  ;;
;;          PC has been incremented and the possible operand A pre-decrement    ;;
;;          and operand B pre-decrement operations performed.  The function     ;;
;;          B-VALUE-FOR-ALU-AFTER-OPRD-B-PRE-DECREMENT generates the correct    ;;
;;          operand B value.                                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;  This function increments the Program Counter (PC) by one.  The PC is
;  stored in register 0 in the register file.

(defn reg-file-after-pc-increment (reg-file)
  (update-nth t 0 reg-file (v-nat-inc (nth 0 reg-file))))


;  This function extracts the current instruction from memory.

(defn current-instruction (reg-file real-mem)
  (v-nth (nth 0 reg-file) real-mem))


;  The result of this function are the contents of the register file after
;  the possible pre-decrement for operand A and the increment of PC.

(defn reg-file-after-oprd-a-pre-decrement (reg-file real-mem)
  (update-v-nth (b-indirect-reg-a-dec (current-instruction reg-file real-mem))
                (bv-oprd-a (current-instruction reg-file real-mem))
                (reg-file-after-pc-increment reg-file)
                (v-nat-dec (v-nth (bv-oprd-a (current-instruction reg-file real-mem))
                                  (reg-file-after-pc-increment reg-file)))))


;  The result of this function are the contents of the register file after
;  the possible pre-decrement for operand B, the possible pre-decrement for
;  operand A and the increment of PC.

(defn reg-file-after-oprd-b-pre-decrement (reg-file real-mem)
  (update-v-nth (b-indirect-reg-b-dec (current-instruction reg-file real-mem))
                (bv-oprd-b (current-instruction reg-file real-mem))
                (reg-file-after-oprd-a-pre-decrement reg-file real-mem)
                (v-nat-dec
                  (v-nth (bv-oprd-b (current-instruction reg-file real-mem))
                         (reg-file-after-oprd-a-pre-decrement reg-file real-mem)))))


;  This function returns operand A for use in the ALU after the PC has been
;  incremented and the possible operand A pre-decrement has occured.

(defn a-value-for-alu-after-oprd-a-pre-decrement (reg-file real-mem)
  (if (b-direct-reg-a (current-instruction reg-file real-mem))
      (v-nth (bv-oprd-a (current-instruction reg-file real-mem))
             (reg-file-after-pc-increment reg-file))
      (if (b-indirect-reg-a-dec (current-instruction reg-file real-mem))
          (v-nth (v-nat-dec (v-nth (bv-oprd-a (current-instruction reg-file real-mem))
                                   (reg-file-after-pc-increment reg-file)))
                 real-mem)
          (v-nth (v-nth (bv-oprd-a (current-instruction reg-file real-mem))
                                   (reg-file-after-pc-increment reg-file))
                 real-mem))))


;  This function returns operand B for use in the ALU after the PC has been
;  incremented, the possible operand A pre-decrement has occured, and the
;  possible operand B pre-decrement has occured.

(defn b-value-for-alu-after-oprd-b-pre-decrement (reg-file real-mem)
  (if (b-direct-reg-b (current-instruction reg-file real-mem))
      (v-nth (bv-oprd-b (current-instruction reg-file real-mem))
             (reg-file-after-oprd-a-pre-decrement reg-file real-mem))
      (if (b-indirect-reg-b-dec (current-instruction reg-file real-mem))
          (v-nth (v-nat-dec
                   (v-nth (bv-oprd-b (current-instruction reg-file real-mem))
                          (reg-file-after-oprd-a-pre-decrement reg-file real-mem)))
                 real-mem)
          (v-nth (v-nth (bv-oprd-b (current-instruction reg-file real-mem))
                        (reg-file-after-oprd-a-pre-decrement reg-file real-mem))
                 real-mem))))

;  This function returns the result of the ALU on operand A, operand B, and
;  the carry flag.

(defn bv-alu-cv-results (reg-file real-mem c-flag)
  (bv-alu-cv (a-value-for-alu-after-oprd-a-pre-decrement reg-file real-mem)
             (b-value-for-alu-after-oprd-b-pre-decrement reg-file real-mem)
             c-flag
             (bv-alu-op-code (current-instruction reg-file real-mem))))

;  This function returns the result of a possible storing of the ALU result
;  into the register file.  Note that this function takes into account the
;  possible changes that may have been inflicted on the register file by some
;  pre-decrement operations and the PC increment.

(defn reg-file-after-alu-write (reg-file real-mem c-flag v-flag z-flag n-flag)
  (update-v-nth (and (b-store-alu-result-with-ifs
                       c-flag v-flag z-flag n-flag
                       (current-instruction reg-file real-mem))
                     (b-direct-reg-b (current-instruction reg-file real-mem)))
                (bv-oprd-b (current-instruction reg-file real-mem))
                (reg-file-after-oprd-b-pre-decrement reg-file real-mem)
                (bv (bv-alu-cv-results reg-file real-mem c-flag))))

;  This function returns the result of a possible storing of the ALU result
;  into the memory.

(defn real-mem-after-alu-write (reg-file real-mem c-flag v-flag z-flag n-flag)
  (update-v-nth (and (b-store-alu-result-with-ifs
                       c-flag v-flag z-flag n-flag
                       (current-instruction reg-file real-mem))
                     (not (b-direct-reg-b (current-instruction reg-file real-mem))))
                (v-nth (bv-oprd-b (current-instruction reg-file real-mem))
                       (reg-file-after-oprd-b-pre-decrement reg-file real-mem))
                real-mem
                (bv (bv-alu-cv-results reg-file real-mem c-flag))))


;  This function returns the result of a possible post-increment of operand A
;  after the possible storing of the ALU result, the pre-decrements of A and B,
;  and the PC increment.

(defn reg-file-after-oprd-a-post-increment
      (reg-file real-mem c-flag v-flag z-flag n-flag)
  (update-v-nth (b-indirect-reg-a-inc (current-instruction reg-file real-mem))
                (bv-oprd-a (current-instruction reg-file real-mem))
                (reg-file-after-alu-write reg-file real-mem
                                          c-flag v-flag z-flag n-flag)          
                (v-nat-inc (v-nth (bv-oprd-a (current-instruction reg-file real-mem))
                                  (reg-file-after-alu-write
                                    reg-file real-mem
                                    c-flag v-flag z-flag n-flag)))))


;  This function returns the result of a possible post-increment of operand B
;  after the possible post-increment of A, the storing of the ALU result, etc.

(defn reg-file-after-oprd-b-post-increment
      (reg-file real-mem c-flag v-flag z-flag n-flag)
  (update-v-nth (b-indirect-reg-b-inc (current-instruction reg-file real-mem))
                (bv-oprd-b (current-instruction reg-file real-mem))
                (reg-file-after-oprd-a-post-increment reg-file real-mem
                                       c-flag v-flag z-flag n-flag)
                (v-nat-inc
                  (v-nth (bv-oprd-b (current-instruction reg-file real-mem))
                         (reg-file-after-oprd-a-post-increment reg-file real-mem
                                                               c-flag v-flag
                                                               z-flag n-flag)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Function SOFT is the programmer's interpreter for FM8501.           ;;
;;          This function completely defines the effect of all instructions     ;;
;;          on the programmer visable state.                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;  This function returns the result of executing n instructions, where
;  n is the length of lst.

(defn soft (reg-file real-mem c-flag v-flag z-flag n-flag lst)
  (if (nlistp lst)
      (list reg-file real-mem c-flag v-flag z-flag n-flag)
      (soft (reg-file-after-oprd-b-post-increment reg-file real-mem
                                                  c-flag v-flag z-flag n-flag)
            (real-mem-after-alu-write reg-file real-mem c-flag v-flag z-flag n-flag)
            (update-v (b-cc-set (current-instruction reg-file real-mem))
                      c-flag
                      (c (bv-alu-cv-results reg-file real-mem c-flag)))
            (update-v (b-cc-set (current-instruction reg-file real-mem))
                      v-flag
                      (v (bv-alu-cv-results reg-file real-mem c-flag)))
            (update-v (b-cc-set (current-instruction reg-file real-mem))
                      z-flag
                      (zerop
                        (bv-to-nat
                          (bv (bv-alu-cv-results reg-file real-mem c-flag)))))
            (update-v (b-cc-set (current-instruction reg-file real-mem))
                      n-flag
                      (negativep
                        (bv-to-tc
                          (bv (bv-alu-cv-results reg-file real-mem c-flag)))))
            (cdr lst))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Function SOFT-RESET specifies what the programmer sees after        ;;
;;          reset has occured.  Note that SOFT-RESET calls the function         ;;
;;          SOFT.  After a reset, the software instruction interpreter is       ;;
;;          is the function SOFT.                                               ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn soft-reset (reg-file real-mem c-flag v-flag z-flag n-flag
                           oracle)
  (if (nlistp oracle)
      (list reg-file real-mem c-flag v-flag z-flag n-flag)
      (soft (update-nth t 0 reg-file (nat-to-bv 0 (machine-size)))
            real-mem
            c-flag
            v-flag
            z-flag
            n-flag
            (cdr oracle))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          This file contains the events leading up to and including           ;;
;;          the proof that an abstraction, containing the programmer            ;;
;;          visable registers, of BIG-MACHINE is equivalent to SOFT.            ;;
;;          This equivalence is the main result of this work; this result       ;;
;;          proves the correctness of a large piece of hardware with            ;;
;;          respect to a high-level description.                                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Help lemmas for proving the correctness of "soft-machine"           ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma a-reg-after-a-b-is-a-value-for-alu-after-oprd-a-pre-decrement (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (a-reg-after-a-b reg-file real-mem)
                  (a-value-for-alu-after-oprd-a-pre-decrement reg-file real-mem)))
  ((disable nth bv-oprd-a update-nth v-nat-dec v-nat-inc)))

(prove-lemma b-reg-after-a-b-is-b-value-for-alu-after-oprd-b-pre-decrement (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (b-reg-after-a-b reg-file real-mem)
                  (b-value-for-alu-after-oprd-b-pre-decrement reg-file real-mem)))
  ((disable nth bv-oprd-a bv-oprd-b update-nth v-nat-dec v-nat-inc)))

(prove-lemma hard-c-flag-is-soft-c-flag (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (boolp c-flag))
           (equal (alu-c-flag (nth (bv-to-nat (nth 0 reg-file)) real-mem)
                              (a-value-for-alu-after-oprd-a-pre-decrement
                                reg-file real-mem)
                              (b-value-for-alu-after-oprd-b-pre-decrement
                                reg-file real-mem)
                              c-flag)
                  (update-v (b-cc-set (current-instruction reg-file real-mem))
                            c-flag
                            (c (bv-alu-cv-results reg-file real-mem c-flag)))))
  ((enable alu-c-flag)
   (disable nth b-reg-after-a-b a-reg-after-a-b
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement)
   (hands-off bv-alu-cv)))

(prove-lemma hard-v-flag-is-soft-v-flag (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (boolp v-flag))
           (equal (alu-v-flag (nth (bv-to-nat (nth 0 reg-file)) real-mem)
                              (a-value-for-alu-after-oprd-a-pre-decrement
                                reg-file real-mem)
                              (b-value-for-alu-after-oprd-b-pre-decrement
                                reg-file real-mem)
                              c-flag v-flag)
                  (update-v (b-cc-set (current-instruction reg-file real-mem))
                            v-flag
                            (v (bv-alu-cv-results reg-file real-mem c-flag)))))
  ((enable alu-v-flag)
   (disable nth b-reg-after-a-b a-reg-after-a-b
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement)
   (hands-off bv-alu-cv)))

(prove-lemma hard-z-flag-is-soft-z-flag (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (boolp z-flag))
           (equal (alu-z-flag (nth (bv-to-nat (nth 0 reg-file)) real-mem)
                              (a-value-for-alu-after-oprd-a-pre-decrement
                                reg-file real-mem)
                              (b-value-for-alu-after-oprd-b-pre-decrement
                                reg-file real-mem)
                              c-flag z-flag)
                  (update-v (b-cc-set (current-instruction reg-file real-mem))
                            z-flag
                            (zerop
                              (bv-to-nat
                                (bv (bv-alu-cv-results reg-file real-mem c-flag)))))))
  ((enable alu-z-flag v-zerop-equal-bv-to-nat-zero)
   (disable nth a-reg-after-a-b b-reg-after-a-b
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement)
   (hands-off bv-alu-cv)))

(prove-lemma sizep-a-value-for-alu-after-oprd-a-pre-decrement (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (size (a-value-for-alu-after-oprd-a-pre-decrement reg-file real-mem))
                  (machine-size)))
  ((disable nth update-nth bv-oprd-a bv-oprd-b v-nat-dec v-nat-inc)))

(prove-lemma hard-n-flag-is-soft-n-flag (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size)))
                (boolp n-flag))
           (equal (alu-n-flag (nth (bv-to-nat (nth 0 reg-file)) real-mem)
                              (a-value-for-alu-after-oprd-a-pre-decrement
                                reg-file real-mem)
                              (b-value-for-alu-after-oprd-b-pre-decrement
                                reg-file real-mem)
                              c-flag n-flag)
                  (update-v (b-cc-set (current-instruction reg-file real-mem))
                            n-flag
                            (negativep
                              (bv-to-tc
                                (bv (bv-alu-cv-results reg-file real-mem c-flag)))))))
  ((enable alu-n-flag n-flag-equals-negativep)
   (disable nth a-reg-after-a-b b-reg-after-a-b
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement
            bv-to-nat-of-twos-compl bv-to-nat-of-incr all-onesp-of-compl
            bitn-on-implies-non-0 ramp)
   (hands-off bv-alu-cv)))

(prove-lemma addr-out-after-a-b-is-v-nth-of-reg-file-after-oprd-b-pre-decrement
             (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (addr-out-after-a-b reg-file real-mem)
                  (v-nth (bv-oprd-b (current-instruction reg-file real-mem))
                         (reg-file-after-oprd-b-pre-decrement reg-file real-mem))))
  ((disable nth update-nth b-indirect-reg-a-dec b-indirect-reg-b-dec
            v-nat-inc v-nat-dec bv-to-nat)
   (hands-off bv-alu-cv)))

(prove-lemma hard-real-mem-is-soft-real-mem (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (real-mem-thru-post-inc
                    (nth (bv-to-nat (nth 0 reg-file)) real-mem)
                    c-flag v-flag z-flag n-flag
                    (nth (bv-to-nat
                           (bv-oprd-b
                             (current-instruction reg-file
                                                  real-mem)))
                         (reg-file-after-oprd-b-pre-decrement reg-file real-mem))
                    real-mem
                    (a-value-for-alu-after-oprd-a-pre-decrement reg-file real-mem)
                    (b-value-for-alu-after-oprd-b-pre-decrement reg-file real-mem))
                  (real-mem-after-alu-write reg-file real-mem
                                            c-flag v-flag z-flag n-flag)))
  ((disable a-reg-after-a-b b-reg-after-a-b
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement
            nth update-nth b-store-alu-result b-store-alu-result-with-ifs
            addr-out-after-a-b reg-file-after-oprd-b-pre-decrement bv-oprd-a bv-oprd-b)
   (hands-off bv-alu-cv)))


(prove-lemma reg-file-after-a-b-is-reg-file-after-oprd-b-pre-decrement (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (reg-file-after-a-b reg-file real-mem)
                  (reg-file-after-oprd-b-pre-decrement reg-file real-mem)))
  ((disable a-reg-after-a-b b-reg-after-a-b
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement
            nth update-nth b-store-alu-result b-store-alu-result-with-ifs
            addr-out-after-a-b bv-oprd-a bv-oprd-b
            v-nat-inc v-nat-dec nat-to-bv bv-to-nat
            b-indirect-reg-a-inc b-direct-reg-a b-indirect-reg-a-dec b-indirect-reg-a
            b-indirect-reg-b-inc b-direct-reg-b b-indirect-reg-b-dec b-indirect-reg-b
            bv-alu-op-code)
   (hands-off bv-alu-cv)))

(prove-lemma hard-reg-file-is-soft-reg-file (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (reg-file-from-alu-thru-post-inc
                    (nth (bv-to-nat (nth 0 reg-file)) real-mem)
                    c-flag v-flag z-flag
                    n-flag
                    (reg-file-after-oprd-b-pre-decrement reg-file real-mem)
                    (a-value-for-alu-after-oprd-a-pre-decrement reg-file real-mem)
                    (b-value-for-alu-after-oprd-b-pre-decrement reg-file real-mem))
                  (reg-file-after-oprd-b-post-increment
                    reg-file real-mem c-flag v-flag z-flag n-flag)))
  ((disable reg-file-after-oprd-b-pre-decrement
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement
            a-reg-after-a-b b-reg-after-a-b
            nth update-nth b-store-alu-result b-store-alu-result-with-ifs
            addr-out-after-a-b bv-oprd-a bv-oprd-b
            v-nat-inc v-nat-dec nat-to-bv bv-to-nat
            b-indirect-reg-a-inc b-direct-reg-a b-indirect-reg-a-dec b-indirect-reg-a
            b-indirect-reg-b-inc b-direct-reg-b b-indirect-reg-b-dec b-indirect-reg-b
            bv-alu-op-code reg-file-after-a-b reg-file-after-oprd-b-pre-decrement)
   (hands-off bv-alu-cv)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Oracle generation function for BIG-MACHINE given the oracle         ;;
;;          for SOFT.  The SOFT machine oracle is a list, each element of       ;;
;;          the list contains four arbitrary values.  This values are "fixed"   ;;
;;          into numbers and used to construct a BIG-MACHINE oracle.  These     ;;
;;          four-tuples describe the possible delay when BIG-MACHINE accesses   ;;
;;          memory.  The values are the number of waits to be inserted in       ;;
;;          memory accesses.  The four-tuples meaning is as follows:            ;;
;;                                                                              ;;
;;          (ir-wait fetch-oprd-a-wait fetch-oprd-b-wait store-oprd-b-wait)     ;;
;;                                                                              ;;
;;          ir-wait -- number of wait states for fetching an instruction        ;;
;;          fetch-oprd-a-wait -- number of wait states for fetching OPERAND-A   ;;
;;          fetch-oprd-b-wait -- number of wait states for fetching OPERAND-B   ;;
;;          store-oprd-b-wait -- number of wait states for storing OPERAND-B    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn oracle (reg-file real-mem c-flag v-flag z-flag n-flag lst)
  (if (nlistp lst)
      nil
      (append (state-1-to-1-oracle reg-file real-mem
                                   c-flag v-flag z-flag n-flag
                                   (car (car lst)) (cadr (car lst))
                                   (caddr (car lst)) (cadddr (car lst)))
              (oracle
                (reg-file-after-oprd-b-post-increment
                  reg-file real-mem c-flag v-flag z-flag n-flag)
                (real-mem-after-alu-write reg-file real-mem c-flag v-flag z-flag n-flag)
                (update-v (b-cc-set (current-instruction reg-file real-mem))
                          c-flag
                          (c (bv-alu-cv-results reg-file real-mem c-flag)))
                (update-v (b-cc-set (current-instruction reg-file real-mem))
                          v-flag
                          (v (bv-alu-cv-results reg-file real-mem c-flag)))
                (update-v (b-cc-set (current-instruction reg-file real-mem))
                          z-flag
                          (zerop
                            (bv-to-nat
                              (bv (bv-alu-cv-results reg-file real-mem c-flag)))))
                (update-v (b-cc-set (current-instruction reg-file real-mem))
                          n-flag
                          (negativep
                            (bv-to-tc
                              (bv (bv-alu-cv-results reg-file real-mem c-flag)))))
                (cdr lst)))))


(defn big-machine-induction
      (no-store data-out reg-file addr-out c-flag v-flag z-flag n-flag
                a-reg b-reg i-reg visual-mem real-mem watch-dog lst)
  (if (nlistp lst)
      t
      (big-machine-induction
        (not (b-store-alu-result c-flag v-flag z-flag n-flag
                                 (v-nth (nth 0 reg-file) real-mem)))
        (bv (bv-alu-cv (a-reg-after-a-b reg-file real-mem)
                       (b-reg-after-a-b reg-file real-mem)
                       c-flag
                       (bv-alu-op-code
                         (v-nth (nth 0 reg-file) real-mem))))
        (reg-file-from-alu-thru-post-inc
          (v-nth (nth 0 reg-file) real-mem)
          c-flag v-flag z-flag
          n-flag
          (reg-file-after-a-b reg-file real-mem)
          (a-reg-after-a-b reg-file real-mem)
          (b-reg-after-a-b reg-file real-mem))
        (addr-out-after-a-b reg-file real-mem) 
        (alu-c-flag (v-nth (nth 0 reg-file) real-mem)
                    (a-reg-after-a-b reg-file real-mem)
                    (b-reg-after-a-b reg-file real-mem)
                    c-flag)
        (alu-v-flag (v-nth (nth 0 reg-file) real-mem)
                    (a-reg-after-a-b reg-file real-mem)
                    (b-reg-after-a-b reg-file real-mem)
                    c-flag v-flag)
        (alu-z-flag (v-nth (nth 0 reg-file) real-mem)
                    (a-reg-after-a-b reg-file real-mem)
                    (b-reg-after-a-b reg-file real-mem)
                    c-flag z-flag)
        (alu-n-flag (v-nth (nth 0 reg-file) real-mem)
                    (a-reg-after-a-b reg-file real-mem)
                    (b-reg-after-a-b reg-file real-mem)
                    c-flag n-flag)
        (a-reg-after-a-b reg-file real-mem)
        (b-reg-after-a-b reg-file real-mem)
        (v-nth (nth 0 reg-file) real-mem)
        (trunc (default-visual-mem-value) 16)
        (real-mem-thru-post-inc
          (v-nth (nth 0 reg-file) real-mem)
          c-flag v-flag z-flag n-flag
          (addr-out-after-a-b reg-file real-mem)
          real-mem
          (a-reg-after-a-b reg-file real-mem)
          (b-reg-after-a-b reg-file real-mem))
        
        (watch-dog f f f
                   (bv (bv-alu-cv
                         (a-reg-after-a-b reg-file real-mem)
                         (b-reg-after-a-b reg-file real-mem)
                         c-flag
                         (bv-alu-op-code
                           (v-nth (nth 0 reg-file) real-mem))))
                   (addr-out-after-a-b reg-file real-mem))
        (cdr lst))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Abstraction for looking at certian registers in BIG-MACHINE.        ;;
;;          Specifically, the definition below allows us to view the registers  ;;
;;          REG-FILE, REAL-MEM, C-FLAG, V-FLAG, Z-FLAG, and N-FLAG, which       ;;
;;          are the registers used in SOFT machine.                             ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn abstract (m)
  (list (cadddddddr m)                  ; reg-file
        (cadddddddddddddddddr m)        ; real-mem
        (cadddddddddr m)                ; c-flag
        (caddddddddddr m)               ; v-flag
        (cadddddddddddr m)              ; z-flag
        (caddddddddddddr m)))           ; n-flag

(prove-lemma abstract-list (rewrite)
  (equal (equal (abstract (list mar read write dtack reset
                                no-store data-out
                                reg-file addr-out
                                c-flag v-flag z-flag n-flag
                                a-reg b-reg i-reg
                                visual-mem real-mem
                                watch-dog))
                (list reg-file real-mem c-flag v-flag z-flag n-flag))
         t))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          The following lemmas ensure SOFT machine does not change the        ;;
;;          size of any registers.                                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(prove-lemma ramp-reg-file-after-oprd-a-pre-decrement (rewrite)
 (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (and (every-member-sizep
                  (reg-file-after-oprd-a-pre-decrement reg-file real-mem) m)
                (equal (length (reg-file-after-oprd-a-pre-decrement reg-file real-mem))
                       8)))
  ((disable bv-to-nat update-nth nth bv-oprd-a bv-oprd-b
            b-indirect-reg-b-inc current-instruction v-nat-inc v-nat-dec
            b-indirect-reg-a-inc b-store-alu-result-with-ifs b-direct-reg-b
            bv-alu-cv-results
            b-indirect-reg-b-dec b-indirect-reg-a-dec)))

(prove-lemma ramp-reg-file-after-oprd-b-pre-decrement (rewrite)
 (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (and (every-member-sizep
                  (reg-file-after-oprd-b-pre-decrement reg-file real-mem) m)
                (equal (length (reg-file-after-oprd-b-pre-decrement reg-file real-mem))
                       8)))
  ((disable bv-to-nat update-nth nth bv-oprd-a bv-oprd-b
            b-indirect-reg-b-inc current-instruction v-nat-inc v-nat-dec
            b-indirect-reg-a-inc b-store-alu-result-with-ifs b-direct-reg-b
            bv-alu-cv-results
            b-indirect-reg-b-dec b-indirect-reg-a-dec)))
 

(prove-lemma size-bv-alu-cv-results (rewrite)
  (equal (size (bv (bv-alu-cv-results reg-file real-mem c-flag)))
         (size (a-value-for-alu-after-oprd-a-pre-decrement reg-file real-mem)))
  ((disable bv-alu-cv bv-alu-op-code
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement)))

(prove-lemma ramp-reg-file-after-oprd-b-post-increment (rewrite)
  (implies (and (equal m (machine-size))
                (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (ramp (reg-file-after-oprd-b-post-increment reg-file real-mem
                                        c-flag v-flag z-flag n-flag)
                 m 8))
  ((enable every-member-sizep-update-nth)
   (disable reg-file-after-oprd-b-pre-decrement
            bv-to-nat update-nth nth bv-oprd-a bv-oprd-b
            b-indirect-reg-b-inc current-instruction v-nat-inc v-nat-dec
            b-indirect-reg-a-inc b-store-alu-result-with-ifs b-direct-reg-b
            bv-alu-cv-results
            b-indirect-reg-b-dec b-indirect-reg-a-dec
            a-value-for-alu-after-oprd-a-pre-decrement)))



(prove-lemma sizep-b-value-for-alu-after-oprd-b-pre-decrement (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (equal (size (b-value-for-alu-after-oprd-b-pre-decrement
                          reg-file real-mem))
                  (machine-size)))
  ((disable fetch-oprd-b-reg-file fetch-oprd-a-reg-file
            update-nth nth bv-oprd-b
            fetch-oprd-a-addr-out fetch-oprd-b-addr-out
            v-nat-dec v-nat-inc bv-to-nat 
            reg-file-after-oprd-a-pre-decrement bv-oprd-a
            current-instruction)))

(prove-lemma ramp-real-mem-after-alu-write (rewrite)
  (implies (and (equal m (machine-size))
                (equal x (exp 2 (machine-size)))
                (ramp reg-file (machine-size) 8)
                (ramp real-mem (machine-size) (exp 2 (machine-size))))
           (ramp (real-mem-after-alu-write reg-file real-mem
                                           c-flag v-flag z-flag n-flag)
                 m x))
  ((disable a-reg-after-a-b b-reg-after-a-b
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement
            nth update-nth b-store-alu-result b-store-alu-result-with-ifs
            addr-out-after-a-b reg-file-after-oprd-b-pre-decrement
            bv-oprd-a bv-oprd-b)
   (hands-off bv-alu-cv)))

(prove-lemma size-nth (rewrite)
  (implies (and (ramp lst 16 n)
                (lessp i n))
           (equal (size (nth i lst)) 16)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          The proof of equivalence between the hardware definition of         ;;
;;          FM8501 and the software definition of FM8501.  This lemma proves    ;;
;;          that BIG-MACHINE executes instructions in the same way as the       ;;
;;          interpreter SOFT.                                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;       


(prove-lemma big-machine-is-soft-machine (rewrite)
  (implies (and (equal mar1 (nat-to-bv 1 (nxsz)))
                (standard-hyps mar1 f f f f
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem))
           (equal (abstract
                    (big-machine mar1 f f f f
                                 no-store data-out
                                 reg-file addr-out
                                 c-flag v-flag z-flag n-flag
                                 a-reg b-reg i-reg
                                 visual-mem real-mem
                                 watch-dog
                                 (oracle reg-file real-mem
                                         c-flag v-flag z-flag n-flag
                                         lst)))
                  (soft reg-file real-mem c-flag v-flag z-flag n-flag lst)))
  ((disable ramp boolp abstract
            nat-to-bv v-nat-inc v-nat-dec update-nth nth
            reg-file-after-oprd-a-pre-decrement reg-file-after-oprd-b-pre-decrement
            b-store-alu-result
            a-value-for-alu-after-oprd-a-pre-decrement
            b-value-for-alu-after-oprd-b-pre-decrement
            b-store-alu-result-ifs bv-oprd-a bv-oprd-b
            bv-alu-cv a-reg-after-a-b b-reg-after-a-b
            bv-alu-op-code nth reg-file-from-alu-thru-post-inc
            reg-file-after-a-b addr-out-after-a-b alu-c-flag alu-v-flag
            alu-z-flag alu-n-flag real-mem-thru-post-inc 
            reg-file-after-oprd-b-post-increment real-mem-after-alu-write
            update-v b-cc-set current-instruction bv-alu-cv-results
            zerop bv-to-nat bv-to-tc
            append state-1-to-1-oracle
            open-big-machine-on-listp)
   (enable state-1-to-1)
   (expand (oracle reg-file real-mem
                   c-flag v-flag z-flag n-flag
                   lst)
           (soft reg-file real-mem c-flag v-flag z-flag n-flag lst))
   (induct (big-machine-induction
             no-store data-out
             reg-file addr-out
             c-flag v-flag z-flag n-flag
             a-reg b-reg i-reg
             visual-mem real-mem
             watch-dog
             lst))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          The following events are concerning with the programmer's view      ;;
;;          of FM8501 during a reset operation.                                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defn oracle-reset (reg-file real-mem c-flag v-flag z-flag n-flag lst)
  (if (nlistp lst)
      nil
      (append (state-0-to-0-wait-to-1-oracle (car (car lst)))
              (oracle (update-nth t 0 reg-file (nat-to-bv 0 (machine-size)))
                      real-mem c-flag v-flag z-flag n-flag
                      (cdr lst)))))

(prove-lemma ramp-reg-file-after-reset (rewrite)
  (implies (and (ramp reg-file (machine-size) 8)
                (equal m (machine-size)))
           (ramp (update-nth t 0 reg-file (nat-to-bv 0 m)) m 8)))

(prove-lemma sizep-trunc-at-machine-size (rewrite)
  (implies (equal m (machine-size))
           (sizep (trunc x m) m)))


;  Proof that reseting FM8501 sets register 0 to zero.

(prove-lemma soft-reset-works (rewrite)
  (implies (and (equal mar0 (nat-to-bv 0 (nxsz)))
                (standard-hyps mar0 f f dtack t
                               no-store data-out
                               reg-file addr-out
                               c-flag v-flag z-flag n-flag
                               a-reg b-reg i-reg
                               visual-mem real-mem))
           (equal (abstract
                    (big-machine mar0 f f dtack t
                                 no-store data-out
                                 reg-file addr-out
                                 c-flag v-flag z-flag n-flag
                                 a-reg b-reg i-reg
                                 visual-mem real-mem
                                 memory-watch-dog-history
                                 (oracle-reset reg-file real-mem
                                               c-flag v-flag z-flag n-flag
                                               lst)))
                  (soft-reset reg-file real-mem c-flag v-flag z-flag n-flag
                              lst)))
  ((disable mar no-store-with-ifs data-out-with-ifs reg-file addr-out c-flag-with-ifs
            v-flag-with-ifs z-flag-with-ifs n-flag-with-ifs a-reg b-reg
            i-reg-with-ifs visual-mem real-mem bv-adder-output bv-subtracter-output
            b-store-alu-result append open-big-machine-on-listp update-nth
            update-v-nth nth v-nth v-nat-inc v-nat-dec nat-to-bv bv-to-nat nat-to-bv
            state-0-to-0-wait-to-1-oracle oracle soft
            ramp sizep boolp abstract)
   (hands-off bv-alu-cv)
   (enable state-0-to-0-wait-to-1)
   (expand (oracle-reset reg-file real-mem
                         c-flag v-flag z-flag n-flag
                         lst)
           (soft-reset reg-file real-mem c-flag v-flag z-flag n-flag lst))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Flag interpretation lemmas                                          ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(disable bv-alu-cv-results)

(prove-lemma bit-vector-interpretation-of-z-flag (rewrite)
  (equal (zerop
           (bv-to-nat
             (bv (bv-alu-cv-results reg-file real-mem c-flag))))
         (v-zerop (bv (bv-alu-cv-results reg-file real-mem c-flag))))
  ((enable v-zerop-equal-bv-to-nat-zero)))

(prove-lemma integer-interpretation-of-z-flag (rewrite)
  (equal (zerop
           (bv-to-nat
             (bv (bv-alu-cv-results reg-file real-mem c-flag))))
         (equal 0 (bv-to-tc
                    (bv (bv-alu-cv-results reg-file real-mem c-flag)))))
  ((enable v-zerop-equal-bv-to-tc-zero)))



(prove-lemma bit-vector-interpretation-of-n-flag (rewrite)
  (equal (negativep
           (bv-to-tc
             (bv (bv-alu-cv-results reg-file real-mem c-flag))))
         (bitn (bv (bv-alu-cv-results reg-file real-mem c-flag))
               (size (bv (bv-alu-cv-results reg-file real-mem c-flag)))))
  ((disable size-bv-alu-cv-results)
   (enable n-flag-equals-negativep)))