(program-at-alt prog-addr bytes x86) → *
Function:
(defun program-at-alt (prog-addr bytes x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard (and (canonical-address-p prog-addr) (byte-listp bytes)))) (declare (xargs :non-executable t)) (prog2$ (acl2::throw-nonexec-error 'program-at-alt (list prog-addr bytes x86)) (let ((__function__ 'program-at-alt)) (declare (ignorable __function__)) (if (and (marking-view x86) (64-bit-modep x86) (not (app-view x86)) (canonical-address-p prog-addr) (canonical-address-p (+ -1 (len bytes) prog-addr)) (disjoint-p$ (mv-nth 1 (las-to-pas (len bytes) prog-addr :x x86)) (open-qword-paddr-list (gather-all-paging-structure-qword-addresses x86)))) (program-at prog-addr bytes x86) nil))))
Theorem:
(defthm program-at-alt-implies-program-addresses-properties (implies (program-at-alt prog-addr bytes (double-rewrite x86)) (and (marking-view x86) (not (app-view x86)) (canonical-address-p prog-addr) (canonical-address-p (+ -1 (len bytes) prog-addr)) (disjoint-p$ (mv-nth 1 (las-to-pas (len bytes) prog-addr :x x86)) (open-qword-paddr-list (gather-all-paging-structure-qword-addresses x86))) (program-at prog-addr bytes x86))))
Theorem:
(defthm rewrite-program-at-to-program-at-alt (implies (forced-and (disjoint-p$ (mv-nth 1 (las-to-pas (len bytes) prog-addr :x (double-rewrite x86))) (open-qword-paddr-list (gather-all-paging-structure-qword-addresses (double-rewrite x86)))) (canonical-address-p prog-addr) (canonical-address-p (+ -1 (len bytes) prog-addr)) (marking-view x86) (not (app-view x86)) (64-bit-modep (double-rewrite x86))) (equal (program-at prog-addr bytes x86) (program-at-alt prog-addr bytes (double-rewrite x86)))))
Theorem:
(defthm program-at-alt-and-xlate-equiv-memory-cong (implies (xlate-equiv-memory x86-1 x86-2) (equal (program-at-alt prog-addr bytes x86-1) (program-at-alt prog-addr bytes x86-2))) :rule-classes :congruence)
Theorem:
(defthm program-at-alt-wb-disjoint-in-sys-view (implies (and (disjoint-p$ (mv-nth 1 (las-to-pas n-w write-addr :w (double-rewrite x86))) (mv-nth 1 (las-to-pas (len bytes) prog-addr :x (double-rewrite x86)))) (disjoint-p$ (mv-nth 1 (las-to-pas n-w write-addr :w (double-rewrite x86))) (open-qword-paddr-list (gather-all-paging-structure-qword-addresses (double-rewrite x86)))) (canonical-address-p (+ -1 n-w write-addr)) (canonical-address-p write-addr)) (equal (program-at-alt prog-addr bytes (mv-nth 1 (wb n-w write-addr w value x86))) (program-at-alt prog-addr bytes (double-rewrite x86)))))
Theorem:
(defthm program-at-alt-xw-doc (equal (program-at-alt prog-addr bytes (xw :doc index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-ms (equal (program-at-alt prog-addr bytes (xw :ms index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-env (equal (program-at-alt prog-addr bytes (xw :env index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-undef (equal (program-at-alt prog-addr bytes (xw :undef index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-os-info (equal (program-at-alt prog-addr bytes (xw :os-info index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-rgf (equal (program-at-alt prog-addr bytes (xw :rgf index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-rip (equal (program-at-alt prog-addr bytes (xw :rip index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-str (equal (program-at-alt prog-addr bytes (xw :str index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-ssr-visible (equal (program-at-alt prog-addr bytes (xw :ssr-visible index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-ssr-hidden-base (equal (program-at-alt prog-addr bytes (xw :ssr-hidden-base index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-ssr-hidden-limit (equal (program-at-alt prog-addr bytes (xw :ssr-hidden-limit index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-ssr-hidden-attr (equal (program-at-alt prog-addr bytes (xw :ssr-hidden-attr index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-dbg (equal (program-at-alt prog-addr bytes (xw :dbg index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-fp-data (equal (program-at-alt prog-addr bytes (xw :fp-data index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-fp-ctrl (equal (program-at-alt prog-addr bytes (xw :fp-ctrl index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-fp-status (equal (program-at-alt prog-addr bytes (xw :fp-status index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-fp-tag (equal (program-at-alt prog-addr bytes (xw :fp-tag index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-fp-last-inst (equal (program-at-alt prog-addr bytes (xw :fp-last-inst index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-fp-last-data (equal (program-at-alt prog-addr bytes (xw :fp-last-data index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-fp-opcode (equal (program-at-alt prog-addr bytes (xw :fp-opcode index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-mxcsr (equal (program-at-alt prog-addr bytes (xw :mxcsr index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-opmsk (equal (program-at-alt prog-addr bytes (xw :opmsk index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-zmm (equal (program-at-alt prog-addr bytes (xw :zmm index val x86)) (program-at-alt prog-addr bytes (double-rewrite x86))))
Theorem:
(defthm program-at-alt-xw-rflags (implies (and (equal (rflagsbits->ac value) (rflagsbits->ac (xr :rflags nil (double-rewrite x86)))) (not (app-view x86)) (x86p x86)) (equal (program-at-alt l-addrs bytes (xw :rflags nil value x86)) (program-at-alt l-addrs bytes (double-rewrite x86)))))
Theorem:
(defthm program-at-alt-after-mv-nth-2-rb (implies (not (mv-nth 0 (las-to-pas n lin-addr r-x (double-rewrite x86)))) (equal (program-at-alt prog-addr bytes (mv-nth 2 (rb n lin-addr r-x x86))) (program-at-alt prog-addr bytes (double-rewrite x86)))))