• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
        • System-level-marking-view-proof-utilities
          • Rb-alt
          • Unwind-x86-interpreter-in-marking-view
          • Program-at-alt
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • Rb-in-system-level-marking-view
          • Xlate-equiv-memory-and-rml08
          • Reasoning-about-page-tables
            • Create-qword-address-list
            • Mult-8-qword-paddr-listp
            • Gather-paging-structures
              • Gather-all-paging-structure-qword-addresses
                • Gather-qword-addresses-corresponding-to-entries
                  • Gather-qword-addresses-corresponding-to-entries-aux
              • All-mem-except-paging-structures-equal
              • Gather-qword-addresses-corresponding-to-1-entry
              • Xlation-governing-entries-paddrs
              • Xlate-equiv-structures
              • Xlation-governing-entries-paddrs-for-page-dir-ptr-table
              • Xlation-governing-entries-paddrs-for-page-directory
              • All-xlation-governing-entries-paddrs
              • Xlation-governing-entries-paddrs-for-pml4-table
              • Xlation-governing-entries-paddrs-for-page-table
              • Gather-pml4-table-qword-addresses
              • Xlate-equiv-memory
              • Open-qword-paddr-list
            • Qword-paddr-listp
            • Find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux
            • Find-first-arg-of-disjoint-p$-candidates
            • Paging-basics
          • Las-to-pas-two-n-ind-hint
          • Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
          • Replace-element
          • Phys-mem-values-same
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
        • Subset-p
        • Disjoint-p
        • Pos
        • Member-p
        • No-duplicates-p
        • Common-system-level-utils
        • Debugging-code-proofs
        • General-memory-utils
        • X86-row-wow-thms
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Gather-qword-addresses-corresponding-to-entries

Gather-qword-addresses-corresponding-to-entries-aux

Returns a list of qword addresses of inferior paging structures referred by the entries located at addresses superior-structure-paddrs of a given superior structure

Signature

(gather-qword-addresses-corresponding-to-entries-aux 
     superior-structure-paddrs x86) 
 
  → 
list-of-addresses

Returns

list-of-addresses — Type (qword-paddr-listp list-of-addresses).

Definitions and Theorems

Function: gather-qword-addresses-corresponding-to-entries-aux

(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: qword-paddr-listp-of-gather-qword-addresses-corresponding-to-entries-aux

(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: true-listp-of-gather-qword-addresses-corresponding-to-entries-aux

(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: mult-8-qword-paddr-listp-gather-qword-addresses-corresponding-to-entries-aux

(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: gather-qword-addresses-corresponding-to-1-entry-and-entries-aux-subset-p

(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: gather-qword-addresses-corresponding-to-entries-aux-subset-and-superset

(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: gather-qword-addresses-corresponding-to-entries-aux-xw-fld!=mem

(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: gather-qword-addresses-corresponding-to-entries-aux-xw-fld=mem-disjoint

(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: gather-qword-addresses-corresponding-to-entries-aux-wm-low-64-disjoint

(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: gather-qword-addresses-corresponding-to-entries-aux-wm-low-64-superior-entry-addr

(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: gather-qword-addresses-corresponding-to-entries-aux-wm-low-64-with-different-x86-disjoint

(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: gather-qword-addresses-corresponding-to-entries-aux-wm-low-64-with-different-x86

(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: gather-qword-addresses-corresponding-to-entries-aux-and-wm-low-64-subset-and-superset-general

(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))))