		Search-engine friendly clone of the ACL2 documentation.

Setting-up-page-tables

Load-qwords-into-physical-memory

Load 64-bit entries into the physical memory

Signature
(load-qwords-into-physical-memory addr-qword-lst x86) → x86
Arguments: addr-qword-lst — Required to be a physical-addr-qword-alistp.
Returns: x86 — Type (x86p x86), given the guard.

Definitions and Theorems

Function: load-qwords-into-physical-memory

(defun load-qwords-into-physical-memory (addr-qword-lst x86)
 (declare (xargs :stobjs (x86)))
 (declare
   (xargs :guard (and (not (app-view x86))
                      (physical-addr-qword-alistp addr-qword-lst))))
 (let ((__function__ 'load-qwords-into-physical-memory))
   (declare (ignorable __function__))
   (cond ((endp addr-qword-lst) x86)
         (t (b* ((addr (caar addr-qword-lst))
                 (qword (cdar addr-qword-lst))
                 (x86 (wm-low-64 addr qword x86)))
              (load-qwords-into-physical-memory (cdr addr-qword-lst)
                                                x86))))))

Theorem: x86p-of-load-qwords-into-physical-memory

(defthm x86p-of-load-qwords-into-physical-memory
 (implies
   (and (x86p x86)
        (not (app-view x86))
        (physical-addr-qword-alistp addr-qword-lst))
   (b* ((x86 (load-qwords-into-physical-memory addr-qword-lst x86)))
     (x86p x86)))
 :rule-classes :rewrite)

Theorem: app-view-unchanged-after-load-qwords-into-physical-memory

(defthm app-view-unchanged-after-load-qwords-into-physical-memory
  (equal (xr :app-view nil
             (load-qwords-into-physical-memory addr-qword-lst x86))
         (xr :app-view nil x86)))