Add README

3 files changed, 673 insertions, 0 deletions

diff --git a/README.org b/README.org
new file mode 100644
index 0000000..702319a
--- /dev/null
+++ b/README.org
@@ -0,0 +1,4 @@
+#+title: BitEQ
+#+author: Yann Herklotz
+
+Reasoning about bit equality
diff --git a/resources/rewrite table.pdf b/resources/rewrite table.pdf
new file mode 100644
index 0000000..ca33197
--- /dev/null
+++ b/resources/rewrite table.pdf
diff --git a/resources/samc.lisp b/resources/samc.lisp
new file mode 100644
index 0000000..dc0ea20
--- /dev/null
+++ b/resources/samc.lisp
@@ -0,0 +1,669 @@
+;;;  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)))
+  )
+