Returns a list of qword addresses of inferior paging
structures referred by the entries located at addresses
(gather-qword-addresses-corresponding-to-entries-aux superior-structure-paddrs x86) → list-of-addresses
Function:
(defun gather-qword-addresses-corresponding-to-entries-aux (superior-structure-paddrs x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard (and (not (app-view x86)) (qword-paddr-listp superior-structure-paddrs)))) (let ((__function__ 'gather-qword-addresses-corresponding-to-entries-aux)) (declare (ignorable __function__)) (if (endp superior-structure-paddrs) nil (b* ((superior-structure-paddr-1 (car superior-structure-paddrs)) (superior-structure-paddrs-rest (cdr superior-structure-paddrs)) (inferior-addresses (gather-qword-addresses-corresponding-to-1-entry superior-structure-paddr-1 x86)) ((when (not inferior-addresses)) (gather-qword-addresses-corresponding-to-entries-aux superior-structure-paddrs-rest x86))) (append inferior-addresses (gather-qword-addresses-corresponding-to-entries-aux superior-structure-paddrs-rest x86))))))
Theorem:
(defthm qword-paddr-listp-of-gather-qword-addresses-corresponding-to-entries-aux (b* ((list-of-addresses (gather-qword-addresses-corresponding-to-entries-aux superior-structure-paddrs x86))) (qword-paddr-listp list-of-addresses)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-gather-qword-addresses-corresponding-to-entries-aux (b* ((list-of-addresses (gather-qword-addresses-corresponding-to-entries-aux superior-structure-paddrs x86))) (true-listp list-of-addresses)) :rule-classes :rewrite)
Theorem:
(defthm mult-8-qword-paddr-listp-gather-qword-addresses-corresponding-to-entries-aux (implies (mult-8-qword-paddr-listp addrs) (mult-8-qword-paddr-listp (gather-qword-addresses-corresponding-to-entries-aux addrs x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-1-entry-and-entries-aux-subset-p (implies (member-p addr addrs) (subset-p (gather-qword-addresses-corresponding-to-1-entry addr x86) (gather-qword-addresses-corresponding-to-entries-aux addrs x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-entries-aux-subset-and-superset (implies (subset-p sub super) (subset-p (gather-qword-addresses-corresponding-to-entries-aux sub x86) (gather-qword-addresses-corresponding-to-entries-aux super x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-entries-aux-xw-fld!=mem (implies (and (not (equal fld :mem)) (not (equal fld :app-view))) (equal (gather-qword-addresses-corresponding-to-entries-aux addrs (xw fld index val x86)) (gather-qword-addresses-corresponding-to-entries-aux addrs x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-entries-aux-xw-fld=mem-disjoint (implies (and (not (member-p index (open-qword-paddr-list addrs))) (physical-address-p index)) (equal (gather-qword-addresses-corresponding-to-entries-aux addrs (xw :mem index val x86)) (gather-qword-addresses-corresponding-to-entries-aux addrs x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-entries-aux-wm-low-64-disjoint (implies (disjoint-p (addr-range 8 index) (open-qword-paddr-list addrs)) (equal (gather-qword-addresses-corresponding-to-entries-aux addrs (wm-low-64 index val x86)) (gather-qword-addresses-corresponding-to-entries-aux addrs x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-entries-aux-wm-low-64-superior-entry-addr (implies (and (member-p index addrs) (mult-8-qword-paddr-listp addrs) (no-duplicates-p addrs) (xlate-equiv-entries (double-rewrite val) (rm-low-64 index x86)) (unsigned-byte-p 64 val) (not (xr :app-view nil x86))) (equal (gather-qword-addresses-corresponding-to-entries-aux addrs (wm-low-64 index val x86)) (gather-qword-addresses-corresponding-to-entries-aux addrs x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-entries-aux-wm-low-64-with-different-x86-disjoint (implies (and (equal (gather-qword-addresses-corresponding-to-entries-aux addrs x86-equiv) (gather-qword-addresses-corresponding-to-entries-aux addrs x86)) (disjoint-p (addr-range 8 index) (open-qword-paddr-list addrs))) (equal (gather-qword-addresses-corresponding-to-entries-aux addrs (wm-low-64 index val x86-equiv)) (gather-qword-addresses-corresponding-to-entries-aux addrs x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-entries-aux-wm-low-64-with-different-x86 (implies (and (equal (gather-qword-addresses-corresponding-to-entries-aux addrs x86-equiv) (gather-qword-addresses-corresponding-to-entries-aux addrs x86)) (member-p index addrs) (mult-8-qword-paddr-listp addrs) (no-duplicates-p addrs) (xlate-equiv-entries (double-rewrite val) (rm-low-64 index x86-equiv)) (unsigned-byte-p 64 val) (not (xr :app-view nil x86-equiv))) (equal (gather-qword-addresses-corresponding-to-entries-aux addrs (wm-low-64 index val x86-equiv)) (gather-qword-addresses-corresponding-to-entries-aux addrs x86))))
Theorem:
(defthm gather-qword-addresses-corresponding-to-entries-aux-and-wm-low-64-subset-and-superset-general (implies (and (subset-p sub super) (equal (page-size value) 1) (mult-8-qword-paddr-listp super) (physical-address-p index) (equal (loghead 3 index) 0) (not (app-view x86)) (unsigned-byte-p 64 value)) (subset-p (gather-qword-addresses-corresponding-to-entries-aux sub (wm-low-64 index value x86)) (gather-qword-addresses-corresponding-to-entries-aux super x86))))