• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Tlb
      • Booting-linux
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • 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
              • 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
      • To-do
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Gather-paging-structures

Gather-pml4-table-qword-addresses

Signature

(gather-pml4-table-qword-addresses x86) → list-of-addresses

Returns

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

Definitions and Theorems

Function: gather-pml4-table-qword-addresses

(defun gather-pml4-table-qword-addresses (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'gather-pml4-table-qword-addresses))
    (declare (ignorable __function__))
    (b* ((cr3 (ctri *cr3* x86))
         (pml4-table-base-addr (ash (cr3bits->pdb cr3) 12)))
      (create-qword-address-list 512 pml4-table-base-addr))))

Theorem: qword-paddr-listp-of-gather-pml4-table-qword-addresses

(defthm qword-paddr-listp-of-gather-pml4-table-qword-addresses
  (b* ((list-of-addresses (gather-pml4-table-qword-addresses x86)))
    (qword-paddr-listp list-of-addresses))
  :rule-classes :rewrite)

Theorem: true-listp-of-gather-pml4-table-qword-addresses

(defthm true-listp-of-gather-pml4-table-qword-addresses
  (b* ((list-of-addresses (gather-pml4-table-qword-addresses x86)))
    (true-listp list-of-addresses))
  :rule-classes :rewrite)

Theorem: consp-gather-pml4-table-qword-addresses

(defthm consp-gather-pml4-table-qword-addresses
  (consp (gather-pml4-table-qword-addresses x86))
  :rule-classes (:type-prescription :rewrite))

Theorem: mult-8-qword-paddr-listp-gather-pml4-table-qword-addresses

(defthm mult-8-qword-paddr-listp-gather-pml4-table-qword-addresses
 (mult-8-qword-paddr-listp (gather-pml4-table-qword-addresses x86)))

Theorem: no-duplicates-p-gather-pml4-table-qword-addresses

(defthm no-duplicates-p-gather-pml4-table-qword-addresses
  (no-duplicates-p (gather-pml4-table-qword-addresses x86)))

Theorem: gather-pml4-table-qword-addresses-xw-fld!=ctr

(defthm gather-pml4-table-qword-addresses-xw-fld!=ctr
 (implies
   (not (equal fld :ctr))
   (equal (gather-pml4-table-qword-addresses (xw fld index val x86))
          (gather-pml4-table-qword-addresses x86))))

Theorem: gather-pml4-table-qword-addresses-wm-low-64

(defthm gather-pml4-table-qword-addresses-wm-low-64
  (equal
       (gather-pml4-table-qword-addresses (wm-low-64 index val x86))
       (gather-pml4-table-qword-addresses x86)))

Theorem: gather-pml4-table-qword-addresses-xw-fld=ctr

(defthm gather-pml4-table-qword-addresses-xw-fld=ctr
 (implies
   (and (equal fld :ctr)
        (not (equal index *cr3*)))
   (equal (gather-pml4-table-qword-addresses (xw fld index val x86))
          (gather-pml4-table-qword-addresses x86))))