(ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86) → (mv * * x86)
Function:
(defun ia32e-la-to-pa-page-table (lin-addr base-addr u/s-acc r/w-acc x/d-acc 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) u/s-acc) (type (unsigned-byte 1) r/w-acc) (type (unsigned-byte 1) x/d-acc) (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-page-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) (page-table-entry-addr lin-addr base-addr))) (entry (the (unsigned-byte 64) (rm-low-64 p-entry-addr x86))) ((mv fault-flg val x86) (paging-entry-no-page-fault-p 0 lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (marking-view? (marking-view x86)) ((mv updated? updated-entry) (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)))) (if (equal accessed 0) (mv t (mbe :logic (set-accessed-bit entry) :exec (!ia32e-page-tablesbits->a 1 entry))) (mv nil entry))) (mv nil entry))) ((when fault-flg) (b* ((x86 (if updated? (wm-low-64 p-entry-addr updated-entry x86) x86))) (mv 'page-fault val x86))) ((mv updated? updated-entry) (if marking-view? (b* ((dirty (mbe :logic (dirty-bit entry) :exec (ia32e-page-tablesbits->d entry)))) (if (and (equal dirty 0) (equal r-w-x :w)) (mv t (mbe :logic (set-dirty-bit updated-entry) :exec (!ia32e-page-tablesbits->d 1 updated-entry))) (mv updated? updated-entry))) (mv nil updated-entry))) (x86 (if updated? (wm-low-64 p-entry-addr updated-entry x86) x86))) (mv nil (mbe :logic (part-install (part-select lin-addr :low 0 :high 11) (ash (ia32e-pte-4k-pagebits->page entry) 12) :low 0 :high 11) :exec (the (unsigned-byte 52) (logior (the (unsigned-byte 52) (logand (the (unsigned-byte 52) (ash (the (unsigned-byte 40) (ia32e-pte-4k-pagebits->page entry)) 12)) -4096)) (the (unsigned-byte 12) (logand 4095 lin-addr))))) x86)) (mv t 0 x86))))
Theorem:
(defthm n52p-mv-nth-1-ia32e-la-to-pa-page-table (unsigned-byte-p *physical-address-size* (mv-nth 1 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc 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-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (< (mv-nth 1 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc 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-page-table (implies (x86p x86) (x86p (mv-nth 2 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))))
Theorem:
(defthm xr-ia32e-la-to-pa-page-table (implies (and (not (equal fld :mem)) (not (equal fld :fault))) (equal (xr fld index (mv-nth 2 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc 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-page-table (implies (not (mv-nth 0 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (equal (xr :fault index (mv-nth 2 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr :fault index x86))))
Theorem:
(defthm xr-ia32e-la-to-pa-page-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-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr fld index x86))))
Theorem:
(defthm ia32e-la-to-pa-page-table-xw-values (implies (and (not (equal fld :mem)) (not (equal fld :app-view))) (and (equal (mv-nth 0 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw fld index value x86))) (mv-nth 0 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (equal (mv-nth 1 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw fld index value x86))) (mv-nth 1 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm ia32e-la-to-pa-page-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-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc 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-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm mv-nth-2-ia32e-la-to-pa-page-table-system-level-non-marking-view (implies (and (not (marking-view x86)) (not (mv-nth 0 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) (equal (mv-nth 2 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) x86)))
Theorem:
(defthm 64-bit-modep-of-ia32e-la-to-pa-page-table (equal (64-bit-modep (mv-nth 2 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc 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-page-table (equal (x86-operation-mode (mv-nth 2 (ia32e-la-to-pa-page-table lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (x86-operation-mode x86)))
Theorem:
(defthm ia32e-la-to-pa-page-table-same-page-offset (implies (not (mv-nth 0 (ia32e-la-to-pa-page-table lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (same-page-offset (mv-nth 1 (ia32e-la-to-pa-page-table lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) lin-addr)))
Theorem:
(defthm ia32e-la-to-pa-page-table-flg-same-if-virt-addr-same-page (implies (same-page lin-addr lin-addr-2) (equal (mv-nth 0 (ia32e-la-to-pa-page-table lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (mv-nth 0 (ia32e-la-to-pa-page-table lin-addr-2 entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) :rule-classes :congruence)
Theorem:
(defthm ia32e-la-to-pa-page-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-page-table lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (mv-nth 1 (ia32e-la-to-pa-page-table lin-addr-2 entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) :rule-classes :congruence)