• 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
        • X86isa-state
        • Syscalls
        • Cpuid
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • App-view
        • Top-level-memory
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • Register-readers-and-writers
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
          • Ia32e-paging
            • Paging-entry-no-page-fault-p
            • Ia32e-la-to-pa-without-tlb-internal
            • Ia32e-la-to-pa-page-directory
            • Ia32e-la-to-pa-page-dir-ptr-table
            • Ia32e-la-to-pa-page-table
            • Ia32e-la-to-pa-pml4-table
            • Ia32e-la-to-pa-without-tlb
            • Ia32e-la-to-pa
            • Same-page
            • Page-fault-exception
            • Page-dir-ptr-table-entry-addr
            • Page-directory-entry-addr
            • Page-table-entry-addr
            • La-to-pa
            • Paging-entry-no-page-fault-p-did-fault?
            • Pml4-table-entry-addr
            • Same-page-offset
            • Page-user-supervisor
            • Page-execute-disable
            • Set-dirty-bit
            • Set-accessed-bit
            • Page-read-write
            • Page-present
            • Page-fault-err-no
            • Accessed-bit
            • Page-size
            • Find-similar-paging-entries-from-page-present-equality-aux
            • Dirty-bit
            • Good-lin-addr-p
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Ia32e-paging

Page-directory-entry-addr

Signature

(page-directory-entry-addr lin-addr base-addr) → *

Definitions and Theorems

Function: page-directory-entry-addr$inline

(defun page-directory-entry-addr$inline (lin-addr base-addr)
  (declare (type (signed-byte 48) lin-addr)
           (type (unsigned-byte 52) base-addr))
  (declare (xargs :guard (equal (loghead 12 base-addr) 0)))
  (if
   (mbt (and (unsigned-byte-p *physical-address-size* base-addr)
             (equal (loghead 12 base-addr) 0)))
   (mbe :logic (part-install (part-select lin-addr :low 21 :high 29)
                             base-addr
                             :low 3
                             :high 11)
        :exec
        (the (unsigned-byte 52)
             (logior (the (unsigned-byte 52)
                          (logand base-addr (lognot 4088)))
                     (the (unsigned-byte 12)
                          (ash (the (unsigned-byte 9)
                                    (logand 511 (ash lin-addr -21)))
                               3)))))
   0))

Theorem: natp-page-directory-entry-addr

(defthm natp-page-directory-entry-addr
  (natp (page-directory-entry-addr lin-addr base-addr))
  :rule-classes (:rewrite :type-prescription))

Theorem: *physical-address-size*p-page-directory-entry-addr

(defthm *physical-address-size*p-page-directory-entry-addr
 (unsigned-byte-p *physical-address-size*
                  (page-directory-entry-addr lin-addr base-addr))
 :rule-classes
 (:rewrite
  (:linear
   :corollary
   (and (<= 0
            (page-directory-entry-addr lin-addr base-addr))
        (< (page-directory-entry-addr lin-addr base-addr)
           (expt 2 *physical-address-size*)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: page-directory-entry-addr-is-a-multiple-of-8

(defthm page-directory-entry-addr-is-a-multiple-of-8
  (equal (loghead 3
                  (page-directory-entry-addr lin-addr base-addr))
         0))

Theorem: adding-7-to-page-directory-entry-addr

(defthm adding-7-to-page-directory-entry-addr
 (unsigned-byte-p
      *physical-address-size*
      (+ 7
         (page-directory-entry-addr lin-addr base-addr)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (natp (+ 7
               (page-directory-entry-addr lin-addr base-addr)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (+ 7
               (page-directory-entry-addr lin-addr base-addr)))
        (< (+ 7
              (page-directory-entry-addr lin-addr base-addr))
           (expt 2 *physical-address-size*)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: page-directory-entry-addr-equal-if-same-page

(defthm page-directory-entry-addr-equal-if-same-page
  (implies (same-page lin-addr lin-addr-2)
           (equal (page-directory-entry-addr lin-addr base-addr)
                  (page-directory-entry-addr lin-addr-2 base-addr)))
  :rule-classes :congruence)