		Search-engine friendly clone of the ACL2 documentation.

Gather-paging-structures

Gather-qword-addresses-corresponding-to-1-entry

Signature
(gather-qword-addresses-corresponding-to-1-entry superior-structure-paddr x86) → list-of-addresses
Arguments: superior-structure-paddr — Guard (natp superior-structure-paddr).
Returns: list-of-addresses — Type (qword-paddr-listp list-of-addresses).

This function returns all qword addresses of the inferior paging structure referred to by a paging entry at address superior-structure-paddr.

Definitions and Theorems

Function: gather-qword-addresses-corresponding-to-1-entry

(defun gather-qword-addresses-corresponding-to-1-entry
       (superior-structure-paddr x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (natp superior-structure-paddr)))
 (declare
  (xargs :guard
         (and (not (app-view x86))
              (physical-address-p superior-structure-paddr)
              (physical-address-p (+ 7 superior-structure-paddr)))))
 (let
  ((__function__ 'gather-qword-addresses-corresponding-to-1-entry))
  (declare (ignorable __function__))
  (b* ((superior-structure-entry
            (rm-low-64 superior-structure-paddr x86)))
    (if
     (and (equal (page-size superior-structure-entry)
                 0))
     (b*
      ((this-structure-base-addr (ash (ia32e-page-tablesbits->reference-addr
                                           superior-structure-entry)
                                      12)))
      (create-qword-address-list 512 this-structure-base-addr))
     nil))))

Theorem: qword-paddr-listp-of-gather-qword-addresses-corresponding-to-1-entry

(defthm
 qword-paddr-listp-of-gather-qword-addresses-corresponding-to-1-entry
 (b* ((list-of-addresses (gather-qword-addresses-corresponding-to-1-entry
                              superior-structure-paddr x86)))
   (qword-paddr-listp list-of-addresses))
 :rule-classes :rewrite)

Theorem: true-listp-of-gather-qword-addresses-corresponding-to-1-entry

(defthm
      true-listp-of-gather-qword-addresses-corresponding-to-1-entry
  (b* ((list-of-addresses (gather-qword-addresses-corresponding-to-1-entry
                               superior-structure-paddr x86)))
    (true-listp list-of-addresses))
  :rule-classes :rewrite)

Theorem: mult-8-qword-paddr-listp-gather-qword-addresses-corresponding-to-1-entry

(defthm
 mult-8-qword-paddr-listp-gather-qword-addresses-corresponding-to-1-entry
 (mult-8-qword-paddr-listp
      (gather-qword-addresses-corresponding-to-1-entry entry x86)))

Theorem: no-duplicates-p-gather-qword-addresses-corresponding-to-1-entry

(defthm
    no-duplicates-p-gather-qword-addresses-corresponding-to-1-entry
  (no-duplicates-p
       (gather-qword-addresses-corresponding-to-1-entry entry x86)))

Theorem: gather-qword-addresses-corresponding-to-1-entry-xw-fld!=mem

(defthm gather-qword-addresses-corresponding-to-1-entry-xw-fld!=mem
 (implies
   (and (not (equal fld :mem))
        (not (equal fld :app-view)))
   (equal (gather-qword-addresses-corresponding-to-1-entry
               n (xw fld index val x86))
          (gather-qword-addresses-corresponding-to-1-entry n x86))))

Theorem: gather-qword-addresses-corresponding-to-1-entry-xw-fld=mem-disjoint

(defthm
 gather-qword-addresses-corresponding-to-1-entry-xw-fld=mem-disjoint
 (implies
  (disjoint-p (addr-range 1 index)
              (addr-range 8 addr))
  (equal
       (gather-qword-addresses-corresponding-to-1-entry
            addr (xw :mem index val x86))
       (gather-qword-addresses-corresponding-to-1-entry addr x86))))

Theorem: gather-qword-addresses-corresponding-to-1-entry-wm-low-64-disjoint

(defthm
 gather-qword-addresses-corresponding-to-1-entry-wm-low-64-disjoint
 (implies
  (disjoint-p (addr-range 8 index)
              (addr-range 8 addr))
  (equal
       (gather-qword-addresses-corresponding-to-1-entry
            addr (wm-low-64 index val x86))
       (gather-qword-addresses-corresponding-to-1-entry addr x86))))

Theorem: gather-qword-addresses-corresponding-to-1-entry-wm-low-64-superior-entry-addr

(defthm
 gather-qword-addresses-corresponding-to-1-entry-wm-low-64-superior-entry-addr
 (implies
  (and (equal index addr)
       (xlate-equiv-entries (double-rewrite val)
                            (rm-low-64 addr x86))
       (unsigned-byte-p 64 val)
       (not (xr :app-view nil x86)))
  (equal
       (gather-qword-addresses-corresponding-to-1-entry
            addr (wm-low-64 index val x86))
       (gather-qword-addresses-corresponding-to-1-entry addr x86))))

Theorem: gather-qword-addresses-corresponding-to-1-entry-with-different-x86-entries

(defthm
 gather-qword-addresses-corresponding-to-1-entry-with-different-x86-entries
 (implies
  (xlate-equiv-entries (rm-low-64 addr x86-equiv)
                       (rm-low-64 addr x86))
  (equal
    (gather-qword-addresses-corresponding-to-1-entry addr x86-equiv)
    (gather-qword-addresses-corresponding-to-1-entry addr x86))))

Theorem: gather-qword-addresses-corresponding-to-1-entry-wm-low-64-with-different-x86-disjoint

(defthm
 gather-qword-addresses-corresponding-to-1-entry-wm-low-64-with-different-x86-disjoint
 (implies
  (and
   (disjoint-p (addr-range 8 index)
               (addr-range 8 addr))
   (equal
    (gather-qword-addresses-corresponding-to-1-entry addr x86-equiv)
    (gather-qword-addresses-corresponding-to-1-entry addr x86)))
  (equal
       (gather-qword-addresses-corresponding-to-1-entry
            addr (wm-low-64 index val x86-equiv))
       (gather-qword-addresses-corresponding-to-1-entry addr x86))))

Theorem: gather-qword-addresses-corresponding-to-1-entry-wm-low-64-with-different-x86

(defthm
 gather-qword-addresses-corresponding-to-1-entry-wm-low-64-with-different-x86
 (implies
  (and (xlate-equiv-entries (double-rewrite val)
                            (rm-low-64 addr x86))
       (unsigned-byte-p 64 val)
       (not (xr :app-view nil x86-equiv)))
  (equal
       (gather-qword-addresses-corresponding-to-1-entry
            addr (wm-low-64 addr val x86-equiv))
       (gather-qword-addresses-corresponding-to-1-entry addr x86))))

Theorem: gather-qword-addresses-corresponding-to-1-entry-subset-p-with-wm-low-64

(defthm
 gather-qword-addresses-corresponding-to-1-entry-subset-p-with-wm-low-64
 (implies
  (and (equal (page-size value) 1)
       (physical-address-p index)
       (equal (loghead 3 index) 0)
       (physical-address-p addr)
       (equal (loghead 3 addr) 0)
       (unsigned-byte-p 64 value)
       (not (app-view x86)))
  (subset-p
       (gather-qword-addresses-corresponding-to-1-entry
            addr (wm-low-64 index value x86))
       (gather-qword-addresses-corresponding-to-1-entry addr x86))))