• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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
        • Read-channel-into-memory
        • 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
        • Read-channel-into-byte-list
        • Init-zero-page
        • Linux-load
        • Read-file-into-memory
        • Read-file-into-byte-list
        • Init-sys-view
        • Load-elf-sections
        • Chars-to-c-str
        • String-to-c-str
        • Pack-u64
        • Pack-u32
        • Concrete-simulation-examples
        • Gdt-entry
      • 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
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Setting-up-page-tables

Construct-pml4-table

Construct a PML4 table, one entry at a time, each of which references a Page-Directory-Pointer Table.

Signature

(construct-pml4-table entry-number entry-addr pdpt-base-addr acc) 
  → 
*

A PML4 table comprises 512 64-bit entries.

Definitions and Theorems

Function: construct-pml4-table

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

Theorem: true-listp-construct-pml4-table

(defthm true-listp-construct-pml4-table
 (implies
  (true-listp acc)
  (true-listp (construct-pml4-table entry-number
                                    entry-addr pdpt-base-addr acc)))
 :rule-classes :type-prescription)

Theorem: consp-construct-pml4-table-helper

(defthm consp-construct-pml4-table-helper
 (implies
  (and (unsigned-byte-p 40 (+ 1 pdpt-base-addr))
       (unsigned-byte-p 52 (+ 8 entry-addr)))
  (consp (construct-pml4-table 511 entry-addr pdpt-base-addr acc))))

Theorem: consp-construct-pml4-table

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

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

(defthm physical-addr-qword-alistp-construct-pml4-table-helper
 (implies
    (and (natp entry-addr)
         (unsigned-byte-p 40 pdpt-base-addr)
         (physical-addr-qword-alistp acc))
    (physical-addr-qword-alistp
         (construct-pml4-table 511 entry-addr pdpt-base-addr acc))))

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

(defthm physical-addr-qword-alistp-construct-pml4-table
  (implies
       (and (unsigned-byte-p 40 pdpt-base-addr)
            (unsigned-byte-p 52 entry-addr)
            (physical-addr-qword-alistp acc))
       (physical-addr-qword-alistp
            (construct-pml4-table entry-number
                                  entry-addr pdpt-base-addr acc)))
  :rule-classes :type-prescription)