#|
 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-