(xlate-equiv-entries-at-qword-addresses list-of-addresses-1 list-of-addresses-2 x86-1 x86-2) → *
Function:
(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:
(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:
(defthm xlate-equiv-entries-at-qword-addresses-reflexive (implies (qword-paddr-listp a) (xlate-equiv-entries-at-qword-addresses a a x x)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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))))