		Search-engine friendly clone of the ACL2 documentation.

Setting-up-page-tables

Construct-pdp-tables

Construct PDP tables, where each table has entries that map a 1GB page

Signature
(construct-pdp-tables table-number pdpt-base-addr acc) → *

PML4 tables contain 512 64-bit entries, and in our current setup, each of those 512 entries point to a PDP table. Thus, we need to construct 512 PDP tables. In our current setup, each PDPTE maps a 1GB page.

Definitions and Theorems

Function: construct-pdp-tables

(defun
 construct-pdp-tables
 (table-number pdpt-base-addr acc)
 (declare (type (unsigned-byte 10) table-number)
          (type (unsigned-byte 40)
                pdpt-base-addr))
 (declare (xargs :guard (alistp acc)))
 (let
  ((__function__ 'construct-pdp-tables))
  (declare (ignorable __function__))
  (cond
     ((not (and (natp table-number)
                (unsigned-byte-p 22 (* 512 table-number))
                (unsigned-byte-p 40 (+ 1 pdpt-base-addr))
                (unsigned-byte-p 10 (+ 1 table-number))
                (unsigned-byte-p 22 (+ 1 (* 512 table-number)))
                (unsigned-byte-p 52 (+ 8 (ash pdpt-base-addr 12)))))
      acc)
     ((< table-number 512)
      (b* ((table (construct-pdp-table 0 (ash pdpt-base-addr 12)
                                       (* 512 table-number)
                                       nil))
           (acc (cons table acc)))
          (construct-pdp-tables (+ 1 table-number)
                                (+ 1 pdpt-base-addr)
                                acc)))
     (t acc))))

Theorem: physical-addr-qword-alist-listp-construct-pdp-tables

(defthm
  physical-addr-qword-alist-listp-construct-pdp-tables
  (implies
       (and (physical-addr-qword-alist-listp acc)
            (unsigned-byte-p 40 pdpt-base-addr))
       (physical-addr-qword-alist-listp
            (construct-pdp-tables table-number pdpt-base-addr acc)))
  :rule-classes (:type-prescription :rewrite))