Add a PDP entry that maps a 1GB page.
(add-pdp-entry page-base-addr) → *
Function:
(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:
(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)))))))