(xlation-governing-entries-paddrs lin-addr x86) → *
Function:
(defun xlation-governing-entries-paddrs (lin-addr x86) (declare (xargs :stobjs (x86))) (declare (type (signed-byte 48) lin-addr)) (declare (xargs :guard (not (app-view x86)))) (let ((__function__ 'xlation-governing-entries-paddrs)) (declare (ignorable __function__)) (if (mbt (not (app-view x86))) (b* ((cr3 (ctri *cr3* x86)) (pml4-base-addr (ash (cr3bits->pdb cr3) 12))) (xlation-governing-entries-paddrs-for-pml4-table lin-addr pml4-base-addr x86)) nil)))
Theorem:
(defthm xlation-governing-entries-paddrs-and-xw-not-mem (implies (and (not (equal fld :mem)) (not (equal fld :ctr)) (not (equal fld :app-view))) (equal (xlation-governing-entries-paddrs lin-addr (xw fld index value x86)) (xlation-governing-entries-paddrs lin-addr (double-rewrite x86)))))
Theorem:
(defthm xlation-governing-entries-paddrs-and-xw-mem-not-member (implies (not (member-p index (xlation-governing-entries-paddrs lin-addr (double-rewrite x86)))) (equal (xlation-governing-entries-paddrs lin-addr (xw :mem index value x86)) (xlation-governing-entries-paddrs lin-addr (double-rewrite x86)))))
Theorem:
(defthm ia32e-la-to-pa-values-and-xw-mem-not-member (implies (and (not (member-p index (xlation-governing-entries-paddrs lin-addr (double-rewrite x86)))) (canonical-address-p lin-addr)) (and (equal (mv-nth 0 (ia32e-la-to-pa-without-tlb lin-addr r-w-x (xw :mem index value x86))) (mv-nth 0 (ia32e-la-to-pa-without-tlb lin-addr r-w-x (double-rewrite x86)))) (equal (mv-nth 1 (ia32e-la-to-pa-without-tlb lin-addr r-w-x (xw :mem index value x86))) (mv-nth 1 (ia32e-la-to-pa-without-tlb lin-addr r-w-x (double-rewrite x86)))))))
Theorem:
(defthm xlation-governing-entries-paddrs-and-write-to-physical-memory-disjoint (implies (and (disjoint-p (xlation-governing-entries-paddrs lin-addr (double-rewrite x86)) p-addrs) (physical-address-listp p-addrs)) (equal (xlation-governing-entries-paddrs lin-addr (write-to-physical-memory p-addrs bytes x86)) (xlation-governing-entries-paddrs lin-addr (double-rewrite x86)))))