		Search-engine friendly clone of the ACL2 documentation.

Xlate-equiv-structures

Xlate-equiv-entries-at-qword-addresses

Signature
(xlate-equiv-entries-at-qword-addresses list-of-addresses-1 list-of-addresses-2 x86-1 x86-2) → *

Definitions and Theorems

Function: xlate-equiv-entries-at-qword-addresses

(defun xlate-equiv-entries-at-qword-addresses
       (list-of-addresses-1 list-of-addresses-2 x86-1 x86-2)
 (declare (xargs :guard (and (qword-paddr-listp list-of-addresses-1)
                             (qword-paddr-listp list-of-addresses-2)
                             (equal (len list-of-addresses-1)
                                    (len list-of-addresses-2))
                             (x86p x86-1)
                             (x86p x86-2))
                 :non-executable t))
 (prog2$
  (acl2::throw-nonexec-error 'xlate-equiv-entries-at-qword-addresses
                             (list list-of-addresses-1
                                   list-of-addresses-2 x86-1 x86-2))
  (let ((__function__ 'xlate-equiv-entries-at-qword-addresses))
    (declare (ignorable __function__))
    (if
      (equal (xr :app-view nil x86-1) nil)
      (if (equal (xr :app-view nil x86-2) nil)
          (if (endp list-of-addresses-1)
              t
            (b* ((addr-1 (car list-of-addresses-1))
                 (addr-2 (car list-of-addresses-2))
                 (qword-1 (rm-low-64 addr-1 x86-1))
                 (qword-2 (rm-low-64 addr-2 x86-2))
                 ((when (not (xlate-equiv-entries qword-1 qword-2)))
                  nil))
              (xlate-equiv-entries-at-qword-addresses
                   (cdr list-of-addresses-1)
                   (cdr list-of-addresses-2)
                   x86-1 x86-2)))
        nil)
      (equal (xr :app-view nil x86-2)
             (xr :app-view nil x86-1))))))

Theorem: booleanp-of-xlate-equiv-entries-at-qword-addresses

(defthm booleanp-of-xlate-equiv-entries-at-qword-addresses
 (booleanp (xlate-equiv-entries-at-qword-addresses addrs addrs x y))
 :rule-classes :type-prescription)

Theorem: xlate-equiv-entries-at-qword-addresses-reflexive

(defthm xlate-equiv-entries-at-qword-addresses-reflexive
  (implies (qword-paddr-listp a)
           (xlate-equiv-entries-at-qword-addresses a a x x)))

Theorem: xlate-equiv-entries-at-qword-addresses-commutative

(defthm xlate-equiv-entries-at-qword-addresses-commutative
 (implies (equal (len a) (len b))
          (equal (xlate-equiv-entries-at-qword-addresses a b x y)
                 (xlate-equiv-entries-at-qword-addresses b a y x))))

Theorem: xlate-equiv-entries-at-qword-addresses-transitive

(defthm xlate-equiv-entries-at-qword-addresses-transitive
  (implies (and (equal (len a) (len b))
                (equal (len b) (len c))
                (xlate-equiv-entries-at-qword-addresses a b x y)
                (xlate-equiv-entries-at-qword-addresses b c y z))
           (xlate-equiv-entries-at-qword-addresses a c x z)))

Theorem: xlate-equiv-entries-at-qword-addresses-with-xw-fld!=mem

(defthm xlate-equiv-entries-at-qword-addresses-with-xw-fld!=mem
  (implies (and (not (equal fld :mem))
                (not (equal fld :app-view)))
           (equal (xlate-equiv-entries-at-qword-addresses
                       addrs-1
                       addrs-2 x86-1 (xw fld index val x86-2))
                  (xlate-equiv-entries-at-qword-addresses
                       addrs-1 addrs-2 x86-1 x86-2))))

Theorem: xlate-equiv-entries-at-qword-addresses-implies-xlate-equiv-entries

(defthm
 xlate-equiv-entries-at-qword-addresses-implies-xlate-equiv-entries
 (implies
  (and
    (xlate-equiv-entries-at-qword-addresses addrs addrs x86-1 x86-2)
    (member-p index addrs)
    (not (xr :app-view nil x86-1)))
  (xlate-equiv-entries (rm-low-64 index x86-1)
                       (rm-low-64 index x86-2))))

Theorem: xlate-equiv-entries-at-qword-addresses-with-xw-mem-disjoint

(defthm xlate-equiv-entries-at-qword-addresses-with-xw-mem-disjoint
  (implies (disjoint-p (list index)
                       (open-qword-paddr-list addrs))
           (equal (xlate-equiv-entries-at-qword-addresses
                       addrs
                       addrs x86-1 (xw :mem index val x86-2))
                  (xlate-equiv-entries-at-qword-addresses
                       addrs addrs x86-1 x86-2))))

Theorem: xlate-equiv-entries-at-qword-addresses-with-wm-low-64-disjoint

(defthm
     xlate-equiv-entries-at-qword-addresses-with-wm-low-64-disjoint
  (implies (disjoint-p (addr-range 8 index)
                       (open-qword-paddr-list addrs))
           (equal (xlate-equiv-entries-at-qword-addresses
                       addrs
                       addrs x86-1 (wm-low-64 index val x86-2))
                  (xlate-equiv-entries-at-qword-addresses
                       addrs addrs x86-1 x86-2))))

Theorem: xlate-equiv-entries-at-qword-addresses-with-wm-low-64-entry-addr

(defthm
   xlate-equiv-entries-at-qword-addresses-with-wm-low-64-entry-addr
 (implies
  (and
   (mult-8-qword-paddr-listp addrs)
   (no-duplicates-p addrs)
   (member-p index addrs)
   (xlate-equiv-entries (double-rewrite val)
                        (rm-low-64 index x86-1))
   (unsigned-byte-p 64 val)
   (xlate-equiv-entries-at-qword-addresses addrs addrs x86-1 x86-2))
  (xlate-equiv-entries-at-qword-addresses
       addrs addrs
       x86-1 (wm-low-64 index val x86-2))))

Theorem: xlate-equiv-entries-at-qword-addresses-with-wm-low-64-different-x86

(defthm
 xlate-equiv-entries-at-qword-addresses-with-wm-low-64-different-x86
 (implies (and (mult-8-qword-paddr-listp addrs)
               (no-duplicates-p addrs)
               (member-p index addrs)
               (xlate-equiv-entries (double-rewrite val)
                                    (rm-low-64 index x86-2))
               (unsigned-byte-p 64 val))
          (equal (xlate-equiv-entries-at-qword-addresses
                      addrs
                      addrs x86-1 (wm-low-64 index val x86-2))
                 (xlate-equiv-entries-at-qword-addresses
                      addrs addrs x86-1 x86-2))))