		Search-engine friendly clone of the ACL2 documentation.

Setting-up-page-tables

Add-pdp-entry

Add a PDP entry that maps a 1GB page

Signature
(add-pdp-entry page-base-addr) → *

Definitions and Theorems

Function: add-pdp-entry

(defun
 add-pdp-entry (page-base-addr)
 (declare (type (unsigned-byte 22)
                page-base-addr))
 (let
  ((__function__ 'add-pdp-entry))
  (declare (ignorable __function__))
  (b*
     ((64-bit-entry
           (!ia32e-pdpte-1gb-pagebits->page page-base-addr 0))
      (64-bit-entry (!ia32e-pdpte-1gb-pagebits->p 1 64-bit-entry))
      (64-bit-entry (!ia32e-pdpte-1gb-pagebits->r/w 1 64-bit-entry))
      (64-bit-entry (!ia32e-pdpte-1gb-pagebits->u/s 1 64-bit-entry))
      (64-bit-entry (!ia32e-pdpte-1gb-pagebits->ps 1 64-bit-entry)))
     64-bit-entry)))

Theorem: n64p-add-pdp-entry

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