• 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
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
        • 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
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Gather-paging-structures

Xlation-governing-entries-paddrs-for-page-table

Signature

(xlation-governing-entries-paddrs-for-page-table 
     lin-addr page-table-base-addr x86) 
 
  → 
*

Definitions and Theorems

Function: xlation-governing-entries-paddrs-for-page-table

(defun xlation-governing-entries-paddrs-for-page-table
       (lin-addr page-table-base-addr x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) lin-addr)
           (type (unsigned-byte 52)
                 page-table-base-addr))
  (declare
       (xargs :guard (and (not (app-view x86))
                          (canonical-address-p lin-addr)
                          (equal (loghead 12 page-table-base-addr)
                                 0))))
  (let
   ((__function__ 'xlation-governing-entries-paddrs-for-page-table))
   (declare (ignorable __function__))
   (b* ((page-table-entry-addr
             (page-table-entry-addr lin-addr page-table-base-addr)))
     (addr-range 8 page-table-entry-addr))))

Theorem: xlation-governing-entries-paddrs-for-page-table-and-xw-not-mem

(defthm
     xlation-governing-entries-paddrs-for-page-table-and-xw-not-mem
  (implies (and (not (equal fld :mem))
                (not (equal fld :app-view)))
           (equal (xlation-governing-entries-paddrs-for-page-table
                       lin-addr
                       base-addr (xw fld index value x86))
                  (xlation-governing-entries-paddrs-for-page-table
                       lin-addr
                       base-addr (double-rewrite x86)))))

Theorem: xlation-governing-entries-paddrs-for-page-table-and-xw-mem-not-member

(defthm
 xlation-governing-entries-paddrs-for-page-table-and-xw-mem-not-member
 (implies (not (member-p index
                         (xlation-governing-entries-paddrs-for-page-table
                              lin-addr
                              base-addr (double-rewrite x86))))
          (equal (xlation-governing-entries-paddrs-for-page-table
                      lin-addr
                      base-addr (xw :mem index value x86))
                 (xlation-governing-entries-paddrs-for-page-table
                      lin-addr
                      base-addr (double-rewrite x86)))))

Theorem: ia32e-la-to-pa-page-table-values-and-xw-mem-not-member

(defthm ia32e-la-to-pa-page-table-values-and-xw-mem-not-member
 (implies
     (and (not (member-p index
                         (xlation-governing-entries-paddrs-for-page-table
                              lin-addr
                              base-addr (double-rewrite x86))))
          (physical-address-p base-addr)
          (equal (loghead 12 base-addr) 0)
          (canonical-address-p lin-addr))
     (and (equal (mv-nth 0
                         (ia32e-la-to-pa-page-table
                              lin-addr base-addr
                              u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl (xw :mem index value x86)))
                 (mv-nth 0
                         (ia32e-la-to-pa-page-table
                              lin-addr base-addr
                              u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl (double-rewrite x86))))
          (equal (mv-nth 1
                         (ia32e-la-to-pa-page-table
                              lin-addr base-addr
                              u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl (xw :mem index value x86)))
                 (mv-nth 1
                         (ia32e-la-to-pa-page-table
                              lin-addr base-addr
                              u/s-acc r/w-acc x/d-acc wp smep
                              smap ac nxe implicit-supervisor-access
                              r-w-x cpl (double-rewrite x86)))))))