(ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86) → (mv * * x86)
Function:
(defun ia32e-la-to-pa-without-tlb-internal (lin-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 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) (or (not (equal implicit-supervisor-access 1)) (< cpl 3))))) (let ((__function__ 'ia32e-la-to-pa-without-tlb-internal)) (declare (ignorable __function__)) (if (mbt (not (app-view x86))) (b* ((lin-addr (mbe :logic (logext 48 (loghead 48 lin-addr)) :exec lin-addr)) (r-w-x (mbe :logic (if (member r-w-x '(:r :w :x)) r-w-x :r) :exec r-w-x)) (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)))) ((mv flg phys-addr x86) (ia32e-la-to-pa-pml4-table lin-addr pml4-table-base-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) ((when flg) (mv t 0 x86))) (mv flg phys-addr x86)) (mv t 0 x86))))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-in-non-app-view (implies (xr :app-view nil x86) (equal (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86) (mv t 0 x86))))
Theorem:
(defthm n52p-mv-nth-1-ia32e-la-to-pa-without-tlb-internal (unsigned-byte-p *physical-address-size* (mv-nth 1 (ia32e-la-to-pa-without-tlb-internal lin-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-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) :hints (("Goal" :in-theory (e/d (unsigned-byte-p) (force (force) not))))) (:linear :corollary (and (<= 0 (mv-nth 1 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (< (mv-nth 1 (ia32e-la-to-pa-without-tlb-internal lin-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) (force (force))))))))
Theorem:
(defthm x86p-mv-nth-2-ia32e-la-to-pa-without-tlb-internal (implies (x86p x86) (x86p (mv-nth 2 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))))
Theorem:
(defthm xr-ia32e-la-to-pa-without-tlb-internal (implies (and (not (equal fld :mem)) (not (equal fld :fault))) (equal (xr fld index (mv-nth 2 (ia32e-la-to-pa-without-tlb-internal lin-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-without-tlb-internal (implies (not (mv-nth 0 (ia32e-la-to-pa-without-tlb-internal lin-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-without-tlb-internal lin-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-without-tlb-internal-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-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr fld index x86))))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-xw-values (implies (and (not (equal fld :mem)) (not (equal fld :rflags)) (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-without-tlb-internal lin-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-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (equal (mv-nth 1 (ia32e-la-to-pa-without-tlb-internal lin-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-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-xw-rflags-not-ac (implies (equal (rflagsbits->ac value) (rflagsbits->ac (rflags x86))) (and (equal (mv-nth 0 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw :rflags nil value x86))) (mv-nth 0 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (equal (mv-nth 1 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw :rflags nil value x86))) (mv-nth 1 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-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-without-tlb-internal lin-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-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-xw-rflags-state-not-ac (implies (equal (rflagsbits->ac value) (rflagsbits->ac (rflags x86))) (equal (mv-nth 2 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw :rflags nil value x86))) (xw :rflags nil value (mv-nth 2 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-same-page-offset (implies (not (mv-nth 0 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (same-page-offset (mv-nth 1 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) lin-addr)))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-flg-same-if-virt-addr-same-page (implies (same-page lin-addr lin-addr-2) (equal (mv-nth 0 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (mv-nth 0 (ia32e-la-to-pa-without-tlb-internal lin-addr-2 wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) :rule-classes :congruence)
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-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-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (mv-nth 1 (ia32e-la-to-pa-without-tlb-internal lin-addr-2 wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) :rule-classes :congruence)
Theorem:
(defthm mv-nth-2-ia32e-la-to-pa-without-tlb-internal-system-level-non-marking-view (implies (and (not (marking-view x86)) (not (mv-nth 0 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) (equal (mv-nth 2 (ia32e-la-to-pa-without-tlb-internal lin-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-without-tlb-internal (equal (64-bit-modep (mv-nth 2 (ia32e-la-to-pa-without-tlb-internal lin-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-without-tlb-internal (equal (x86-operation-mode (mv-nth 2 (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (x86-operation-mode x86)))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-fixes-address (equal (ia32e-la-to-pa-without-tlb-internal (logext 48 lin-addr) wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86) (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))
Theorem:
(defthm ia32e-la-to-pa-without-tlb-internal-fixes-perm (implies (not (member-p r-w-x '(:r :w :x))) (equal (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86) (ia32e-la-to-pa-without-tlb-internal lin-addr wp smep smap ac nxe implicit-supervisor-access :r cpl x86))))