(ia32e-la-to-pa lin-addr r-w-x x86) → (mv * * x86)
Function:
(defun ia32e-la-to-pa (lin-addr r-w-x x86) (declare (xargs :stobjs (x86))) (declare (type (signed-byte 48) lin-addr) (type (member :r :w :x) r-w-x)) (declare (xargs :guard (and (not (app-view x86)) (canonical-address-p lin-addr)))) (let ((__function__ 'ia32e-la-to-pa)) (declare (ignorable __function__)) (if (mbt (not (app-view x86))) (b* ((lin-addr (mbe :logic (logext 48 (loghead 48 lin-addr)) :exec lin-addr)) (cr0 (n32 (ctri *cr0* x86))) (cr4 (n22 (ctri *cr4* x86))) (cpl (the (unsigned-byte 2) (cpl x86))) (ia32-efer (n12 (msri *ia32_efer-idx* x86))) (wp (cr0bits->wp cr0)) (smep (cr4bits->smep cr4)) (smap (cr4bits->smap cr4)) (ac (rflagsbits->ac (rflags x86))) (nxe (ia32_eferbits->nxe ia32-efer)) (cr3 (ctri *cr3* x86)) (pml4-table-base-addr (mbe :logic (ash (cr3bits->pdb cr3) 12) :exec (the (unsigned-byte 52) (ash (the (unsigned-byte 40) (cr3bits->pdb cr3)) 12))))) (ia32e-la-to-pa-pml4-table lin-addr pml4-table-base-addr wp smep smap ac nxe r-w-x cpl x86)) (mv t 0 x86))))
Theorem:
(defthm n52p-mv-nth-1-ia32e-la-to-pa (unsigned-byte-p *physical-address-size* (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86))) :hints (("Goal" :in-theory (e/d (unsigned-byte-p) (force (force) not))))) (:linear :corollary (and (<= 0 (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86))) (< (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86)) (expt 2 *physical-address-size*))) :hints (("Goal" :in-theory (e/d (unsigned-byte-p) (force (force))))))))
Theorem:
(defthm x86p-mv-nth-2-ia32e-la-to-pa (implies (x86p x86) (x86p (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86)))))
Theorem:
(defthm xr-ia32e-la-to-pa (implies (and (not (equal fld :mem)) (not (equal fld :fault))) (equal (xr fld index (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86))) (xr fld index x86))))
Theorem:
(defthm xr-fault-ia32e-la-to-pa (implies (not (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x x86))) (equal (xr :fault index (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86))) (xr :fault index x86))))
Theorem:
(defthm xr-and-ia32e-la-to-pa-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 lin-addr r-w-x x86))) (xr fld index x86))))
Theorem:
(defthm ia32e-la-to-pa-xw-values (implies (and (not (equal fld :mem)) (not (equal fld :rflags)) (not (equal fld :fault)) (not (equal fld :ctr)) (not (equal fld :msr)) (not (equal fld :seg-visible)) (not (equal fld :app-view))) (and (equal (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x (xw fld index value x86))) (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x x86))) (equal (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x (xw fld index value x86))) (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86))))))
Theorem:
(defthm ia32e-la-to-pa-xw-rflags-not-ac (implies (equal (rflagsbits->ac value) (rflagsbits->ac (rflags x86))) (and (equal (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x (xw :rflags nil value x86))) (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x x86))) (equal (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x (xw :rflags nil value x86))) (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86))))))
Theorem:
(defthm ia32e-la-to-pa-xw-state (implies (and (not (equal fld :mem)) (not (equal fld :rflags)) (not (equal fld :fault)) (not (equal fld :ctr)) (not (equal fld :msr)) (not (equal fld :seg-visible)) (not (equal fld :app-view)) (not (equal fld :marking-view))) (equal (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x (xw fld index value x86))) (xw fld index value (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86))))))
Theorem:
(defthm ia32e-la-to-pa-xw-rflags-state-not-ac (implies (equal (rflagsbits->ac value) (rflagsbits->ac (rflags x86))) (equal (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x (xw :rflags nil value x86))) (xw :rflags nil value (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86))))))
Theorem:
(defthm mv-nth-2-ia32e-la-to-pa-system-level-non-marking-view (implies (and (not (marking-view x86)) (not (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x x86)))) (equal (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86)) x86)))
Theorem:
(defthm 64-bit-modep-of-ia32e-la-to-pa (equal (64-bit-modep (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86))) (64-bit-modep x86)))
Theorem:
(defthm x86-operation-mode-of-ia32e-la-to-pa (equal (x86-operation-mode (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86))) (x86-operation-mode x86)))