(all-mem-except-paging-structures-equal-aux i paging-qword-addresses x86-1 x86-2) → *
Function:
(defun all-mem-except-paging-structures-equal-aux (i paging-qword-addresses x86-1 x86-2) (declare (xargs :non-executable t :guard (and (natp i) (<= i *mem-size-in-bytes*) (mult-8-qword-paddr-listp paging-qword-addresses) (x86p x86-1) (x86p x86-2)))) (prog2$ (acl2::throw-nonexec-error 'all-mem-except-paging-structures-equal-aux (list i paging-qword-addresses x86-1 x86-2)) (let ((__function__ 'all-mem-except-paging-structures-equal-aux)) (declare (ignorable __function__)) (if (zp i) (if (disjoint-p (list i) (open-qword-paddr-list paging-qword-addresses)) (equal (xr :mem i x86-1) (xr :mem i x86-2)) t) (if (disjoint-p (list (1- i)) (open-qword-paddr-list paging-qword-addresses)) (and (equal (xr :mem (1- i) x86-1) (xr :mem (1- i) x86-2)) (all-mem-except-paging-structures-equal-aux (1- i) paging-qword-addresses x86-1 x86-2)) (all-mem-except-paging-structures-equal-aux (1- i) paging-qword-addresses x86-1 x86-2))))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-xr-mem-from-rest-of-memory (implies (and (all-mem-except-paging-structures-equal-aux i addrs x86-1 x86-2) (disjoint-p (list j) (open-qword-paddr-list addrs)) (natp i) (natp j) (< j i)) (equal (xr :mem j x86-1) (xr :mem j x86-2))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-rm-low-32-from-rest-of-memory (implies (and (all-mem-except-paging-structures-equal-aux i addrs x86-1 x86-2) (disjoint-p (addr-range 4 j) (open-qword-paddr-list addrs)) (natp i) (natp j) (< (+ 3 j) i) (not (app-view x86-1)) (not (app-view x86-2))) (equal (rm-low-32 j x86-1) (rm-low-32 j x86-2))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-rm-low-64-from-rest-of-memory (implies (and (all-mem-except-paging-structures-equal-aux i addrs x86-1 x86-2) (disjoint-p (addr-range 8 j) (open-qword-paddr-list addrs)) (natp i) (natp j) (< (+ 7 j) i) (not (app-view x86-1)) (not (app-view x86-2))) (equal (rm-low-64 j x86-1) (rm-low-64 j x86-2))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-is-reflexive (all-mem-except-paging-structures-equal-aux i addrs x x))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-is-commutative (implies (all-mem-except-paging-structures-equal-aux i addrs x y) (all-mem-except-paging-structures-equal-aux i addrs y x)))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-is-transitive (implies (and (all-mem-except-paging-structures-equal-aux i addrs x y) (all-mem-except-paging-structures-equal-aux i addrs y z)) (all-mem-except-paging-structures-equal-aux i addrs x z)))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-xw-1 (implies (not (equal fld :mem)) (equal (all-mem-except-paging-structures-equal-aux i addrs (xw fld index val x) y) (all-mem-except-paging-structures-equal-aux i addrs x y))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-xw-2 (implies (not (equal fld :mem)) (equal (all-mem-except-paging-structures-equal-aux i addrs x (xw fld index val y)) (all-mem-except-paging-structures-equal-aux i addrs x y))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-xw-mem (implies (all-mem-except-paging-structures-equal-aux i addrs x y) (all-mem-except-paging-structures-equal-aux i addrs (xw :mem index val x) (xw :mem index val y))))
Theorem:
(defthm xr-mem-wm-low-64 (implies (not (member-p index (addr-range 8 addr))) (equal (xr :mem index (wm-low-64 addr val x86)) (xr :mem index x86))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-wm-low-64-paging-entry (implies (member-p index addrs) (equal (all-mem-except-paging-structures-equal-aux i addrs (wm-low-64 index val x) y) (all-mem-except-paging-structures-equal-aux i addrs x y))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-wm-low-64 (implies (and (all-mem-except-paging-structures-equal-aux i addrs x y) (not (xr :app-view nil x)) (not (xr :app-view nil y))) (all-mem-except-paging-structures-equal-aux i addrs (wm-low-64 index val x) (wm-low-64 index val y))))
Theorem:
(defthm all-mem-except-paging-structures-equal-aux-and-xw-mem-commute-writes (implies (not (equal index-1 index-2)) (all-mem-except-paging-structures-equal-aux i addrs (xw :mem index-1 val-1 (xw :mem index-2 val-2 x)) (xw :mem index-2 val-2 (xw :mem index-1 val-1 x)))))