fix x86 book for merge change

acl2 · Aug 11, 2016 · 48f303e · 48f303e
1 parent d58032e
commit 48f303e
Showing 1 changed file with 39 additions and 6 deletions.
diff --git a/books/projects/x86isa/machine/x86-top-level-memory.lisp b/books/projects/x86isa/machine/x86-top-level-memory.lisp
@@ -3507,27 +3507,60 @@ memory.</li>
                      (ash y 8)))
       :hints (("goal" :in-theory (enable ash-logior)))))
 
+   (local
+    (defthmd logior-ash-to-logapp
+      (implies (unsigned-byte-p w x)
+               (equal (logior x (ash y w))
+                      (logapp w x y)))
+      :hints(("Goal" :in-theory (e/d* (ihsext-inductions
+                                        ihsext-recursive-redefs)
+                                      (unsigned-byte-p))))))
+
+   (local
+    (defthmd logior-ash-to-logapp-2
+      (implies (unsigned-byte-p w x)
+               (equal (logior x (ash y w) z)
+                      (logior (logapp w x y) z)))
+      :hints (("goal" :use ((:instance (:theorem (implies (equal a b)
+                                                          (equal (logior a c)
+                                                                 (logior b c))))
+                             (a (logior (ash y w) x))
+                             (b (logapp w x y))))
+               :in-theory (e/d (logior-ash-to-logapp))))))
+
+
+   (local (defthm logior-0
+            (equal (logior x 0) (ifix x))))
+
    (defthmd combine-bytes-as-merge-16-u8s
      (implies
-      (and (natp b0)  (natp b1)  (natp b2)  (natp b3)
-           (natp b4)  (natp b5)  (natp b6)  (natp b7)
-           (natp b8)  (natp b9)  (natp b10) (natp b11)
-           (natp b12) (natp b13) (natp b14) (natp b15))
+      (and (unsigned-byte-p 8 b0)  (unsigned-byte-p 8 b1)  (unsigned-byte-p 8 b2)  (unsigned-byte-p 8 b3)
+           (unsigned-byte-p 8 b4)  (unsigned-byte-p 8 b5)  (unsigned-byte-p 8 b6)  (unsigned-byte-p 8 b7)
+           (unsigned-byte-p 8 b8)  (unsigned-byte-p 8 b9)  (unsigned-byte-p 8 b10) (unsigned-byte-p 8 b11)
+           (unsigned-byte-p 8 b12) (unsigned-byte-p 8 b13) (unsigned-byte-p 8 b14) (unsigned-byte-p 8 b15))
       (equal
        (combine-bytes
         (list
          b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15))
        (bitops::merge-16-u8s
         b15 b14 b13 b12 b11 b10 b9 b8 b7 b6 b5 b4 b3 b2 b1 b0)))
-     :hints (("goal" :in-theory (enable ash-logior-8 merge-16-u8s))))
+     :hints (("goal" :in-theory (e/d (ash-logior-8 merge-16-u8s
+                                                   logior-ash-to-logapp)
+                                     (unsigned-byte-p
+                                      acl2::commutativity-of-logior)))))
 
    (defthmd natp-memi
      (implies (and (x86p x86))
               (natp (memi p-addr x86))))
 
    (defthmd memi<256
      (implies (and (x86p x86))
-              (< (memi p-addr x86) 256))))
+              (< (memi p-addr x86) 256)))
+
+   (defthm unsigned-byte-p-of-memi
+     (implies (x86p x86)
+              (unsigned-byte-p 8 (memi p-addr x86)))
+     :hints(("Goal" :in-theory (enable memi<256)))))
 
   (if (mbt (canonical-address-p lin-addr))