		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)))