• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
        • Dynamic-instrumentation
        • Initialize-x86-state
        • Binary-file-load-fn
        • Setting-up-page-tables
          • Construct-pml4-table
          • Construct-pdp-table
          • Load-qwords-into-physical-memory-list
          • Construct-pdp-tables
          • Load-qwords-into-physical-memory
          • Construct-page-tables
          • Physical-addr-qword-alistp
          • Add-pml4-entry
          • Add-pdp-entry
          • Physical-addr-qword-alist-listp
        • Init-sys-view
        • Load-elf-sections
        • Concrete-simulation-examples
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Setting-up-page-tables

Construct-pdp-table

Construct a PDP table, one entry at a time, each of which map a 1GB page

Signature

(construct-pdp-table entry-number entry-addr page-base-addr acc) 
  → 
*

A PDP table comprises 512 64-bit entries.

Definitions and Theorems

Function: construct-pdp-table

(defun
 construct-pdp-table
 (entry-number entry-addr page-base-addr acc)
 (declare (type (unsigned-byte 10) entry-number)
          (type (unsigned-byte 52) entry-addr)
          (type (unsigned-byte 22)
                page-base-addr))
 (declare (xargs :guard (alistp acc)))
 (let
   ((__function__ 'construct-pdp-table))
   (declare (ignorable __function__))
   (cond ((or (not (integerp entry-number))
              (< entry-number 0)
              (not (unsigned-byte-p 22 (1+ page-base-addr)))
              (not (unsigned-byte-p 10 (1+ entry-number)))
              (not (unsigned-byte-p 52 (+ 8 entry-addr))))
          acc)
         ((< entry-number 512)
          (construct-pdp-table (+ 1 entry-number)
                               (+ 8 entry-addr)
                               (+ 1 page-base-addr)
                               (acons entry-addr
                                      (add-pdp-entry page-base-addr)
                                      acc)))
         (t acc))))

Theorem: true-listp-construct-pdp-table

(defthm
 true-listp-construct-pdp-table
 (implies
  (true-listp acc)
  (true-listp (construct-pdp-table entry-number
                                   entry-addr page-base-addr acc))))

Theorem: consp-construct-pdp-table-helper

(defthm
 consp-construct-pdp-table-helper
 (implies
   (and (unsigned-byte-p 52 (+ 8 entry-addr))
        (unsigned-byte-p 22 (+ 1 page-base-addr)))
   (consp (construct-pdp-table 511 entry-addr page-base-addr acc))))

Theorem: consp-construct-pdp-table

(defthm
   consp-construct-pdp-table
   (implies
        (and (< entry-number 512)
             (unsigned-byte-p 10 entry-number)
             (unsigned-byte-p 10 (+ 1 entry-number))
             (unsigned-byte-p 52 (+ 8 entry-addr))
             (unsigned-byte-p 22 (+ 1 page-base-addr)))
        (consp (construct-pdp-table entry-number
                                    entry-addr page-base-addr acc)))
   :rule-classes (:type-prescription :rewrite))

Theorem: physical-addr-qword-alistp-construct-pdp-table-helper

(defthm
 physical-addr-qword-alistp-construct-pdp-table-helper
 (implies
     (and (natp entry-addr)
          (physical-addr-qword-alistp acc)
          (unsigned-byte-p 22 page-base-addr))
     (physical-addr-qword-alistp
          (construct-pdp-table 511 entry-addr page-base-addr acc))))

Theorem: physical-addr-qword-alistp-construct-pdp-table

(defthm
 physical-addr-qword-alistp-construct-pdp-table
 (implies (and (natp entry-addr)
               (physical-addr-qword-alistp acc)
               (unsigned-byte-p 22 page-base-addr))
          (physical-addr-qword-alistp
               (construct-pdp-table entry-number
                                    entry-addr page-base-addr acc)))
 :rule-classes (:type-prescription :rewrite))