		Search-engine friendly clone of the ACL2 documentation.

Setting-up-page-tables

Add-pml4-entry

Add a PML4 entry that references a Page-Directory-Pointer Table

Signature
(add-pml4-entry pdpt-base-addr) → *

Definitions and Theorems

Function: add-pml4-entry

(defun
  add-pml4-entry (pdpt-base-addr)
  (declare (type (unsigned-byte 40)
                 pdpt-base-addr))
  (let ((__function__ 'add-pml4-entry))
       (declare (ignorable __function__))
       (b* ((64-bit-entry (!ia32e-pml4ebits->pdpt pdpt-base-addr 0))
            (64-bit-entry (!ia32e-pml4ebits->p 1 64-bit-entry))
            (64-bit-entry (!ia32e-pml4ebits->r/w 1 64-bit-entry))
            (64-bit-entry (!ia32e-pml4ebits->u/s 1 64-bit-entry)))
           64-bit-entry)))

Theorem: n64p-add-pml4-entry

(defthm
 n64p-add-pml4-entry
 (unsigned-byte-p 64 (add-pml4-entry pdpt-base-addr))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (add-pml4-entry pdpt-base-addr))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (add-pml4-entry pdpt-base-addr))
                   (< (add-pml4-entry pdpt-base-addr)
                      18446744073709551616))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))