;;;  Copyright 2022 Intel Corporation All Rights Reserved.
;; Simple proofs of Sam Coward rules
;; Anna Slobodova 02/08/2022

(in-package "ACL2")


(include-book "centaur/bitops/ihsext-basics" :dir :System)
(local (include-book "arithmetic/top" :dir :system))
(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))
;; (local (include-book "std/strings/hexify" :dir :system))

(local (in-theory (disable unsigned-byte-p (tau-system))))

;;------- Commutativity
;; For any r: follows from commutativity of integers
(defthm bounded-commutativity-of-*
  (implies
   (and
    (integerp a)
    (integerp b))
   (equal
    (loghead r (* a b))
    (loghead r (* b a)))))

;; SOme lemmas that help us with further proofs

(local
 (defthm unsigned-byte-p-of-mul
  (implies
   (and
    (unsigned-byte-p p a)
    (unsigned-byte-p r b))
   (unsigned-byte-p (+ p r) (* a b)))
  :hints (("goal" :in-theory (enable unsigned-byte-p)
           :nonlinearp t))
  ))


;;  uses BITOPS::UNSIGNED-BYTE-P-INCR
(local
 (defthm loghead-inc
  (implies
   (and
    (unsigned-byte-p n x)
    (natp m)
    (<= n m))
   (equal
    (loghead m x)
    x))))

(local
 (defthm loghead-inc-of-mul
   (implies
    (and
     (force (unsigned-byte-p p a))
     (force (unsigned-byte-p r b))
     (natp p)
     (natp r)
     (natp u)
     (<= (+ p r) u))
    (equal
     (loghead u (* a b))
     (* a b)
     ))
   :hints (("goal" :in-theory (disable loghead-inc)
            :use ((:instance loghead-inc (m u) (n (+ p r)) (x (* a b))))
            ))
   ))


;;------------------ MULT ASSOCIATIVITY --------------

;; Our goal is to prove (under some conditions)
;; (equal
;;    (loghead v (* (loghead u (* a b)) c))
;;    (loghead v (* a (loghead q (* b c ))))) 
;; First let's simplify LHS:
;; consider two cases:
;;= (loghead v (* (loghead v (loghead u (* a b))) (loghead v c))) if (<= v u)
;;= (loghead v (* (* a b) c))                                     if (and (< u v)(<= (+ p r) u))
(local
 (encapsulate
   ()
   (local
    (defthm bounded-mult-associativity-LHS1
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp u)
        (<= v u))
       (equal
        (loghead v (* (loghead u (* a b)) c))
        (loghead v (* (loghead v (* a b)) (loghead v c)))))
      :hints (("goal"
               :in-theory (disable BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME
                                   BITOPS::LOGHEAD-OF-LOGHEAD-1)
               :use ((:instance BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME (n v) (x (loghead u (* a b))) (y c))
                     (:instance BITOPS::LOGHEAD-OF-LOGHEAD-1  (m v) (n u) (x (* a b))))))
      ))

   (local
    (defthm bounded-mult-associativity-LHS2
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp u)
        (<= v u))
       (equal
        (loghead v (* (loghead v (* a b)) (loghead v c)))
        (loghead v (* a b c))))))

   (local (in-theory (disable COMMUTATIVITY-OF-*)))
   (local
    (defthm bounded-mult-associativity-LHS3
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp u)
        (<= v u))
       (equal
        (loghead v (* (loghead u (* a b)) c))
        (loghead v (* a b c))))
      :hints (("goal" :cases ((<= v u)) ))
      ))
   
   (defthm bounded-mult-associativity-LHS4
     (implies
      (and
       (unsigned-byte-p p a)
       (unsigned-byte-p r b)
       (integerp c)
       (natp u) (natp v) (natp p) (natp r)
       (or
        (<= v u)
        (<= (+ p r) u)))
      (equal
       (loghead v (* (loghead u (* a b)) c))
       (loghead v (*  a b c)))))
   ))

;; Now let's simplify RHS (again consider two cases)
;;(loghead v (* a (loghead q (* b c))))
;;= (loghead v (* (loghead v a) (loghead v (* b c))))             if (<= v q)
;;= (loghead v (* a (loghead (+ r s) (* b c))))                   if (< q v) (<= (+ r s) q)
;;       =(loghead v (* a (loghead v (* b c))))
;;          =(loghead v (* a (* b c)))
(local
 (encapsulate
   () 
   (local
    (defthm bounded-mult-associativity-RHS1
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp v)
        (natp q)
        (<= v q))
       (equal
        (loghead v (* a (loghead q (* b c))))
        (loghead v (* (loghead v a ) (loghead v (* b c))))))
      :hints (("goal"
               :in-theory (disable BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME
                                   BITOPS::LOGHEAD-OF-LOGHEAD-1)
               :use ((:instance BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME (n v) (x  a) (y (loghead q (* b c))))
                     (:instance BITOPS::LOGHEAD-OF-LOGHEAD-1  (m v) (n q) (x (* b c))))))
      ))
   (local
    (defthm bounded-mult-associativity-RHS2
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp v)
        (natp q)
        (<= v q))
       (equal
        (loghead v (* (loghead v a ) (loghead v (* b c))))
        (loghead v (* a b c))))))

   (local
    (defthm bounded-mult-associativity-RHS3
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp v)
        (natp q)
        (<= v q))
       (equal
        (loghead v (* a (loghead q (* b c))))
        (loghead v (* a b c))))))

   (defthm bounded-associativity-RHS4
     (implies
      (and
       (unsigned-byte-p r b)
       (unsigned-byte-p s c)
       (integerp a)
       (natp q) (natp v) (natp r) (natp s)
       (or
        (<= v q)
        (<= (+ r s) q)))
      (equal
       (loghead v (* a (loghead q (* b c))))
       (loghead v (* a b c)))))
   ))
(defthm bounded-mult-associativity
  (implies
   (and
    (unsigned-byte-p p a)
    (unsigned-byte-p r b)
    (unsigned-byte-p s c)
    (natp p)(natp r) (natp s)(natp u) 
    (natp v)(natp q)
    (and
     (or
      (<= v q)
      (<= (+ r s) q))
     (or
      (<= v u)
      (<= (+ p r) u))))
   (equal
    (loghead v (* (loghead u (* a b)) c))
    (loghead v (* a (loghead q (* b c )))))
   ))

;;---------- ADD ASSOCIATIVITY LEFT OUT
#||

(defthm bounded-add-associativity
  (implies
   (and
    (unsigned-byte-p p a)
    (unsigned-byte-p r b)
    (unsigned-byte-p s c)
    (and
     (or (<= v q) (< (max r s) q))
     (or (<= v u) (< (max p r) u))))
   (equal
    (loghead v (+ (loghead u (+ a b)) c))
    (loghead v (+ a (loghead q (+ b c)))))))

||#
;;------------- DISTRIBUTE
;; We want to prove (under some conditions)
(local
 (encapsulate
   ()
   ;; (loghead r (* a (loghead q (+ b c))))
   ;; (loghead r (* (loghead r a) (loghead r (loghead q (+ b c)))))
   ;; (loghead r (* (loghead r a) (loghead r (+ b c))))
   ;; (loghead r (* (loghead r a) (loghead r (+ (loghead r b) (loghead r c)))))

   (local
    (defthm distribute-mult-over-add-LHS1
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp q)
        (<= r q))
       (equal
        (loghead r (* a (loghead q (+ b c))))
        (loghead r (* (loghead r a) (loghead r (+ b c))))
        ))
      :hints (("goal"
               :in-theory (disable BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME
                                   BITOPS::LOGHEAD-OF-LOGHEAD-1
                                   )
               :use ((:instance BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME (n r) (x a) (y (loghead q (+ b c))))
                     (:instance BITOPS::LOGHEAD-OF-LOGHEAD-1  (m r) (n q) (x (+ b c))) 
                     )
               ))))     
   (local
    (defthm distribute-mult-over-add-LHS2
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp q)
        (<= r q))
       (equal
        (loghead r (* (loghead r a) (loghead r (+ b c))))
        (loghead r (* a (+ b c)))
        ))))
   
   (defthm distribute-mult-over-add-LHS3
     (implies
      (and
       (integerp a)
       (integerp b)
       (integerp c)
       (natp q)
       (<= r q))
      (equal
       (loghead r (* a (loghead q (+ b c))))
       (loghead r (* a (+ b c)))
       )))
   ))

(local
 (encapsulate
   ()
   (local
    (defthm distribute-mult-over-add-RHS1
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp u)
        (natp v)
        (<= r u)
        (<= r v))
       (equal
        (loghead r (+ (loghead u (* a b)) (loghead v (* a c))))
        (loghead r (+ (loghead r (* a b)) (loghead r (* a c))))
        ))
      :hints (("goal"
               :in-theory (disable BITOPS::LOGHEAD-OF-+-OF-LOGHEAD-SAME
                                   BITOPS::LOGHEAD-OF-LOGHEAD-1
                                   )
               :use ((:instance BITOPS::LOGHEAD-OF-+-OF-LOGHEAD-SAME (n r) (x (loghead u (* a b))) (y (loghead v (* a c))))
                     (:instance BITOPS::LOGHEAD-OF-LOGHEAD-1  (m r) (n u) (x (* a b)))
                     (:instance BITOPS::LOGHEAD-OF-LOGHEAD-1  (m r) (n v) (x (* a c))) 
                     )
               )))
    )

   (local
    (defthm distribute-mult-over-add-RHS2
      (implies
       (and
        (integerp a)
        (integerp b)
        (integerp c)
        (natp u)
        (natp v)
        (<= r u)
        (<= r v))
       (equal
        (loghead r (+ (loghead r (* a b)) (loghead r (* a c))))
        (loghead r (+ (* a b) (* a c)))
        ))))

   (defthm distribute-mult-over-add-RHS3
     (implies
      (and
       (integerp a)
       (integerp b)
       (integerp c)
       (natp u)
       (natp v)
       (<= r u)
       (<= r v))
      (equal
       (loghead r (+ (loghead u (* a b)) (loghead v (* a c))))
       (loghead r (+ (* a b) (* a c)))
       )))
   ))
   
(defthm distribute-mult-over-add
  (implies
   (and
    (integerp a)
    (integerp b)
    (integerp c)
    (natp q) (natp u) (natp v)
    (<= r q) (<= r u) (<= r v))
   (equal
    (loghead r (* a (loghead q (+ b c))))
    (loghead r (+ (loghead u (* a b)) (loghead v (* a c))))))
  :hints (("goal"
           :in-theory (disable   distribute-mult-over-add-LHS3  )
           :use ( distribute-mult-over-add-LHS3)
           ))
  )
   

;;------------- Sum Same
(encapsulate
  ()

  (local
   (defthm lemma1
     (implies
      (integerp a)
      (equal (+ a a) (* 2 a)))))

  (defthm bounded-sum-same
    (implies
     (integerp a)
     (equal
      (loghead q (+ a a))
      (loghead q (* 2 a)))))
  )
;;--------------- Add Zero
(defthm bounded-add-zero
  (implies
   (and
    (integerp a)
    (integerp b)
    (natp p)
    (equal (mod b (expt 2 p)) 0))
   (equal
    (loghead p (+ a b))
    (loghead p a)))
  :hints (("goal" :in-theory (enable loghead)))
  )

;;------------- Sub to Neg
;; no rules are created from this theorem
(defthm sub-to-neg
  (implies
   (and
    (integerp a)
    (integerp b))
   (equal
    (loghead r (- a b))
    (loghead r (+ a (- b)))))
  :rule-classes nil
  )
  
;;----------- Mult by One
(defthm mult-by-one
  (implies
   (and
    (integerp a)
    (integerp b)
    (natp p)
    (equal (mod b (expt 2 p)) 1))
   (equal
    (loghead p (* a b))
    (loghead p a)))
   :hints (("goal" :in-theory (enable loghead)))
   )
;;------------ Mult by Two
(defthm bounded-mult-by-two
  (implies
   (integerp a)
   (equal
    (loghead r (* a 2))
    (loghead r (ash a 1))))
  :hints(("goal" :in-theory (Enable ash)))
  )

;;------------ Merge Left Shift
;; -- more general
(defthm merge-left-shift
  (implies
   (and
    (integerp a)
    (natp b)
    (natp c))
   (equal
    (ash (ash a b) c)
    (ash a (+ b c))))
  :hints (("goal" :in-theory (enable ash)))
  )
;;----------- Merg Right Shift
;; -- mode general
(defthm merge-right-shift
  (implies
   (and
    (integerp a)
    (natp b)
    (natp c))
   (equal
    (ash (ash a (- b)) (- c))
    (ash a (- (+ b c))))))

;;---------- Redundant Sel
(defthm redundant-sel
  (equal
   (if b a a)
   a)
  :rule-classes nil)

;; not true: (r=10, p=2, a=3=b011,~a=b110, -a=-3=b101, r=3)
;; (defthm bounded-not-neg
;;   (implies
;;    (and
;;     (unsigned-byte-p p a)
;;     (natp p))
;;    (equal
;;     (loghead r (+ 1 (loghead p (lognot a))))
;;     (loghead r (- a))))
;;   :hints (("goal" :in-theory (Enable lognot)))
;;   )

;; (defthm bounded-neg-not
;;   (implies
;;    (and
;;     (natp p)
;;     (natp r)
;;     (<= r p)
;;     (unsigned-byte-p p a)
;;     )
;;    (equal
;;     (loghead r (+ 1 (loghead p (lognot a))))
;;     (loghead r (- a))))
;;   :hints (("goal" :in-theory (Enable lognot)))
;;   )


;;---------- Not over Con
;;-- more general --
;; (logapp s b a) will concatenate a and low s bits of b
(defthm not-over-con
  (implies
   (and 
    (unsigned-byte-p q a) 
    (unsigned-byte-p s b)
    )
 (equal
  (loghead (+ s q) (lognot (logapp s b a)))
  (loghead (+ s q) (logapp s (lognot b) (lognot a)))))
  :hints (("goal" :in-theory (enable logapp lognot loghead expt mod unsigned-byte-p)
           :nonlinearp t)) 
)

;;-------------- Mult Constant
(defthm mult-constant
  (implies
   (and (integerp x) (integerp c))
   (equal
    (+ (* 2 (* (logtail 1 c) x)) (* (loghead 1 c) x))
    (* c x)))
  :hints (("goal" :nonlinearp t
           :in-theory (Enable loghead logtail)
           ))
  )

;;------------- One to Two Mult
(defthm mult-to-two
  (implies
   (integerp x)
   (equal
    (- (* 2 x) x)
    x)))

;;------------ Left Shift Add
(defthm left-shift-add
  (implies
   (and
    (natp c)
    (integerp a)
    (integerp b))
   (equal
    (ash (+ a b) c)
    (+ (ash a c) (ash b c))))
  :hints (("goal" :in-theory (Enable ash)))
  )

;;------------- Right Shift Add
(defthm add-right-shift
  (implies
   (and
    (integerp a)
    (integerp b)
    (natp c))
   (equal
    (ash (+ (ash a c) b) (- c))
    (+ a (ash b (- c)))))
  :hints (("goal" :in-theory (Enable ash)))
  )

;;-------------- Left Shift Mul
(defthm left-shift-mult
  (implies
   (and
    (integerp a)
    (integerp b)
    (natp c))
   (equal
    (ash (* a b) c)
    (* (ash a c) b)))
   :hints (("goal" :in-theory (Enable ash)))
   )

;;-------------- Sel Add
;; (defthm bounded-sel-add
;;   (implies
;;    (and
;;     (unsigned-byte-p p a)
;;     (unsigned-byte-p q b)
;;     (unsigned-byte-p p c)
;;     (unsigned-byte-p q d)
;;     )
;;    (equal
;;     (loghead r (if e (+ a b) (+ c d)))
;;     (loghead r (+ (if e a c) (if e b d))))))
;;
;;-- more general ---
;; In acl2, (if e x y) will evaluate to y only if e=NIL, otherwise it evaluates to x 
(defthm sel-add
  (implies
   (and
    (integerp a)
    (integerp b)
    (integerp c)
    (integerp d)
    )
   (equal
    (if e (+ a b) (+ c d))
    (+ (if e a c) (if e b d)))))

;;-------- Sel Add Zero
;; this is jsut a case of the previous one.
(defthm sel-add-zero
  (implies
   (and
    (integerp a)
    (integerp b)
    (integerp c))
   (equal
    (if e (+ a b) c)
    (+ (if e a c) (if e b 0)))))


;;------- Mov Sel Zero
;; (defthm mov-sel-zero
;;   (implies
;;    (and
;;     (integerp a)
;;     (integerp c))
;;    (equal
;;     (loghead r (* (if b 0 a) c))
;;     (loghead r (* a (if b 0 c))))))
;;
;;--- More general--
(defthm mov-sel-zero
  (implies
   (and
    (integerp a)
    (integerp c))
   (equal
    (* (if b 0 a) c)
    (* a (if b 0 c)))))


;;------------- Concat to Add
;; (str::hexify (logapp 16 #uxCDEF #uxAB))
;;more general
(defthm bounded-concat-to-add
  (implies
   (and
    (integerp a)
    (unsigned-byte-p q b)
    (natp q))
   (equal
    (logapp q b a)
    (+ (ash a q) b)))
  :hints (("goal" :in-theory (enable ash logapp unsigned-byte-p)))
  )