(ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86) → (mv * * x86)
Function:
(defun ia32e-la-to-pa-pml4-table (lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86) (declare (xargs :stobjs (x86))) (declare (type (signed-byte 48) lin-addr) (type (unsigned-byte 52) base-addr) (type (unsigned-byte 1) wp) (type (unsigned-byte 1) smep) (type (unsigned-byte 1) smap) (type (unsigned-byte 1) ac) (type (unsigned-byte 1) nxe) (type (unsigned-byte 1) implicit-supervisor-access) (type (member :r :w :x) r-w-x) (type (unsigned-byte 2) cpl)) (declare (xargs :guard (and (not (app-view x86)) (canonical-address-p lin-addr) (equal (loghead 12 base-addr) 0) (or (not (equal implicit-supervisor-access 1)) (< cpl 3))))) (let ((__function__ 'ia32e-la-to-pa-pml4-table)) (declare (ignorable __function__)) (if (mbt (not (app-view x86))) (b* ((lin-addr (mbe :logic (logext 48 (loghead 48 lin-addr)) :exec lin-addr)) (base-addr (mbe :logic (part-install 0 (loghead *physical-address-size* base-addr) :low 0 :width 12) :exec base-addr)) (p-entry-addr (the (unsigned-byte 52) (pml4-table-entry-addr lin-addr base-addr))) (entry (the (unsigned-byte 64) (rm-low-64 p-entry-addr x86))) (u/s-all (mbe :logic (page-user-supervisor entry) :exec (ia32e-page-tablesbits->u/s entry))) (r/w-all (mbe :logic (page-read-write entry) :exec (ia32e-page-tablesbits->r/w entry))) (x/d-all (mbe :logic (page-execute-disable entry) :exec (ia32e-page-tablesbits->xd entry))) (marking-view? (marking-view x86)) ((mv fault-flg val x86) (paging-entry-no-page-fault-p 3 lin-addr entry u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) ((when fault-flg) (b* ((x86 (if (and marking-view? (equal (mbe :logic (page-present entry) :exec (ia32e-page-tablesbits->p entry)) 1)) (b* ((accessed (mbe :logic (accessed-bit entry) :exec (ia32e-page-tablesbits->a entry))) ((unless (equal accessed 0)) x86)) (wm-low-64 p-entry-addr (set-accessed-bit entry) x86)) x86))) (mv 'page-fault val x86))) (page-dir-ptr-table-base-addr (ash (ia32e-pml4ebits->pdpt entry) 12)) ((mv flag (the (unsigned-byte 52) p-addr) x86) (ia32e-la-to-pa-page-dir-ptr-table lin-addr page-dir-ptr-table-base-addr u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (entry (rm-low-64 p-entry-addr x86)) (x86 (if marking-view? (b* ((accessed (mbe :logic (accessed-bit entry) :exec (ia32e-page-tablesbits->a entry))) ((unless (equal accessed 0)) x86)) (wm-low-64 p-entry-addr (set-accessed-bit entry) x86)) x86)) ((when flag) (mv flag 0 x86))) (mv nil p-addr x86)) (mv t 0 x86))))
Theorem:
(defthm n52p-mv-nth-1-ia32e-la-to-pa-pml4-table (unsigned-byte-p *physical-address-size* (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) :hints (("Goal" :in-theory (e/d (unsigned-byte-p) (not))))) (:linear :corollary (and (<= 0 (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (< (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (expt 2 *physical-address-size*))) :hints (("Goal" :in-theory (e/d (unsigned-byte-p) nil))))))
Theorem:
(defthm x86p-mv-nth-2-ia32e-la-to-pa-pml4-table (implies (x86p x86) (x86p (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))))
Theorem:
(defthm xr-ia32e-la-to-pa-pml4-table (implies (and (not (equal fld :mem)) (not (equal fld :fault))) (equal (xr fld index (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr fld index x86))))
Theorem:
(defthm xr-fault-ia32e-la-to-pa-pml4-table (implies (not (mv-nth 0 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (equal (xr :fault index (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr :fault index x86))))
Theorem:
(defthm xr-and-ia32e-la-to-pa-pml4-table-in-non-marking-view (implies (and (not (marking-view x86)) (not (equal fld :fault))) (equal (xr fld index (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr fld index x86))))
Theorem:
(defthm ia32e-la-to-pa-pml4-table-xw-values (implies (and (not (equal fld :mem)) (not (equal fld :app-view))) (and (equal (mv-nth 0 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw fld index value x86))) (mv-nth 0 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (equal (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw fld index value x86))) (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm ia32e-la-to-pa-pml4-table-xw-state (implies (and (not (equal fld :mem)) (not (equal fld :fault)) (not (equal fld :app-view)) (not (equal fld :marking-view))) (equal (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw fld index value x86))) (xw fld index value (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm mv-nth-2-ia32e-la-to-pa-pml4-table-system-level-non-marking-view (implies (and (not (marking-view x86)) (not (mv-nth 0 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) (equal (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) x86)))
Theorem:
(defthm 64-bit-modep-of-ia32e-la-to-pa-pml4-table (equal (64-bit-modep (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (64-bit-modep x86)))
Theorem:
(defthm x86-operation-mode-of-ia32e-la-to-pa-pml4-table (equal (x86-operation-mode (mv-nth 2 (ia32e-la-to-pa-pml4-table lin-addr ase-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (x86-operation-mode x86)))
Theorem:
(defthm ia32e-la-to-pa-pml4-table-same-page-offset (implies (not (mv-nth 0 (ia32e-la-to-pa-pml4-table lin-addr ase-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (same-page-offset (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr ase-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) lin-addr)))
Theorem:
(defthm ia32e-la-to-pa-pml4-table-flg-same-if-virt-addr-same-page (implies (same-page lin-addr lin-addr-2) (equal (mv-nth 0 (ia32e-la-to-pa-pml4-table lin-addr ase-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (mv-nth 0 (ia32e-la-to-pa-pml4-table lin-addr-2 ase-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) :rule-classes :congruence)
Theorem:
(defthm ia32e-la-to-pa-pml4-table-phys-addr-same-if-virt-addr-same-page (implies (same-page lin-addr lin-addr-2) (same-page (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr ase-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (mv-nth 1 (ia32e-la-to-pa-pml4-table lin-addr-2 ase-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) :rule-classes :congruence)