• 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-table-entry-addr

Signature

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

Definitions and Theorems

Function: page-table-entry-addr$inline

(defun page-table-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 12 :high 20)
                          base-addr
                          :low 3
                          :high 11)
     :exec (the (unsigned-byte 52)
                (logior (logand base-addr (lognot (ash 511 3)))
                        (ash (the (unsigned-byte 9)
                                  (logand 511
                                          (the (signed-byte 36)
                                               (ash lin-addr -12))))
                             3))))
  0))

Theorem: natp-page-table-entry-addr

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

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

(defthm *physical-address-size*p-page-table-entry-addr
 (unsigned-byte-p *physical-address-size*
                  (page-table-entry-addr lin-addr base-addr))
 :rule-classes
 (:rewrite
  (:linear
   :corollary (and (<= 0
                       (page-table-entry-addr lin-addr base-addr))
                   (< (page-table-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-table-entry-addr-is-a-multiple-of-8

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

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

(defthm adding-7-to-page-table-entry-addr
 (unsigned-byte-p *physical-address-size*
                  (+ 7
                     (page-table-entry-addr lin-addr base-addr)))
 :rule-classes
 (:rewrite
  (:type-prescription
    :corollary (natp (+ 7
                        (page-table-entry-addr lin-addr base-addr)))
    :hints
    (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (+ 7
               (page-table-entry-addr lin-addr base-addr)))
        (< (+ 7
              (page-table-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-table-entry-addr-equal-if-same-page

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