• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
        • System-level-marking-view-proof-utilities
          • Rb-alt
          • Unwind-x86-interpreter-in-marking-view
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • Program-at-alt
          • Rb-in-system-level-marking-view
          • Xlate-equiv-memory-and-rml08
          • Reasoning-about-page-tables
          • Las-to-pas-two-n-ind-hint
          • Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
          • Replace-element
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
        • Subset-p
        • Disjoint-p
        • Pos
        • Member-p
        • No-duplicates-p
        • Common-system-level-utils
        • Debugging-code-proofs
        • General-memory-utils
        • X86-row-wow-thms
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Testing-utilities
  • Math

• System-level-marking-view-proof-utilities

Rb-alt

Signature

(rb-alt n addr r-x x86) → *

Arguments

n — Number of bytes to be read.
    Guard (natp n).

addr — First linear address.
    Guard (integerp addr).

r-x — Type of memory access.

rb-alt is defined basically to read the program bytes from the memory. I don't intend to use it to read paging data structures.

Definitions and Theorems

Function: rb-alt

(defun rb-alt (n addr r-x x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (member :r :x) r-x))
 (declare (xargs :guard (and (natp n) (integerp addr))))
 (declare (xargs :non-executable t))
 (prog2$
  (acl2::throw-nonexec-error 'rb-alt
                             (list n addr r-x x86))
  (let ((__function__ 'rb-alt))
   (declare (ignorable __function__))
   (if
    (and
      (marking-view x86)
      (64-bit-modep x86)
      (not (app-view x86))
      (canonical-address-p addr)
      (canonical-address-p (+ -1 n addr))
      (not (mv-nth 0 (las-to-pas n addr r-x x86)))
      (disjoint-p
           (mv-nth 1 (las-to-pas n addr r-x x86))
           (open-qword-paddr-list
                (gather-all-paging-structure-qword-addresses x86))))
    (rb n addr r-x x86)
    (mv nil 0 x86)))))

Theorem: integerp-of-mv-nth-1-rb-alt

(defthm integerp-of-mv-nth-1-rb-alt
  (integerp (mv-nth 1 (rb-alt n addr r-x x86)))
  :rule-classes :type-prescription)

Theorem: natp-of-mv-nth-1-rb-alt

(defthm natp-of-mv-nth-1-rb-alt
  (implies (x86p x86)
           (natp (mv-nth 1 (rb-alt n addr r-x x86))))
  :rule-classes :type-prescription)

Theorem: x86p-of-mv-nth-2-rb-alt

(defthm x86p-of-mv-nth-2-rb-alt
  (implies (x86p x86)
           (x86p (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: rb-alt-no-reads-when-zp-n

(defthm rb-alt-no-reads-when-zp-n
  (equal (mv-nth 1 (rb-alt 0 addr r-x x86))
         0))

Theorem: xr-doc-mv-nth-2-rb-alt

(defthm xr-doc-mv-nth-2-rb-alt
  (equal (xr :doc index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :doc index x86)))

Theorem: xr-ms-mv-nth-2-rb-alt

(defthm xr-ms-mv-nth-2-rb-alt
  (equal (xr :ms index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :ms index x86)))

Theorem: xr-env-mv-nth-2-rb-alt

(defthm xr-env-mv-nth-2-rb-alt
  (equal (xr :env index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :env index x86)))

Theorem: xr-undef-mv-nth-2-rb-alt

(defthm xr-undef-mv-nth-2-rb-alt
  (equal (xr :undef index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :undef index x86)))

Theorem: xr-app-view-mv-nth-2-rb-alt

(defthm xr-app-view-mv-nth-2-rb-alt
  (equal (xr :app-view index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :app-view index x86)))

Theorem: xr-marking-view-mv-nth-2-rb-alt

(defthm xr-marking-view-mv-nth-2-rb-alt
  (equal (xr :marking-view index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :marking-view index x86)))

Theorem: xr-os-info-mv-nth-2-rb-alt

(defthm xr-os-info-mv-nth-2-rb-alt
  (equal (xr :os-info index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :os-info index x86)))

Theorem: xr-rgf-mv-nth-2-rb-alt

(defthm xr-rgf-mv-nth-2-rb-alt
  (equal (xr :rgf index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :rgf index x86)))

Theorem: xr-rip-mv-nth-2-rb-alt

(defthm xr-rip-mv-nth-2-rb-alt
  (equal (xr :rip index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :rip index x86)))

Theorem: xr-rflags-mv-nth-2-rb-alt

(defthm xr-rflags-mv-nth-2-rb-alt
  (equal (xr :rflags index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :rflags index x86)))

Theorem: xr-seg-visible-mv-nth-2-rb-alt

(defthm xr-seg-visible-mv-nth-2-rb-alt
  (equal (xr :seg-visible index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :seg-visible index x86)))

Theorem: xr-seg-hidden-base-mv-nth-2-rb-alt

(defthm xr-seg-hidden-base-mv-nth-2-rb-alt
  (equal (xr :seg-hidden-base index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :seg-hidden-base index x86)))

Theorem: xr-seg-hidden-limit-mv-nth-2-rb-alt

(defthm xr-seg-hidden-limit-mv-nth-2-rb-alt
  (equal (xr :seg-hidden-limit index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :seg-hidden-limit index x86)))

Theorem: xr-seg-hidden-attr-mv-nth-2-rb-alt

(defthm xr-seg-hidden-attr-mv-nth-2-rb-alt
  (equal (xr :seg-hidden-attr index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :seg-hidden-attr index x86)))

Theorem: xr-str-mv-nth-2-rb-alt

(defthm xr-str-mv-nth-2-rb-alt
  (equal (xr :str index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :str index x86)))

Theorem: xr-ssr-visible-mv-nth-2-rb-alt

(defthm xr-ssr-visible-mv-nth-2-rb-alt
  (equal (xr :ssr-visible index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :ssr-visible index x86)))

Theorem: xr-ssr-hidden-base-mv-nth-2-rb-alt

(defthm xr-ssr-hidden-base-mv-nth-2-rb-alt
  (equal (xr :ssr-hidden-base index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :ssr-hidden-base index x86)))

Theorem: xr-ssr-hidden-limit-mv-nth-2-rb-alt

(defthm xr-ssr-hidden-limit-mv-nth-2-rb-alt
  (equal (xr :ssr-hidden-limit index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :ssr-hidden-limit index x86)))

Theorem: xr-ssr-hidden-attr-mv-nth-2-rb-alt

(defthm xr-ssr-hidden-attr-mv-nth-2-rb-alt
  (equal (xr :ssr-hidden-attr index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :ssr-hidden-attr index x86)))

Theorem: xr-ctr-mv-nth-2-rb-alt

(defthm xr-ctr-mv-nth-2-rb-alt
  (equal (xr :ctr index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :ctr index x86)))

Theorem: xr-dbg-mv-nth-2-rb-alt

(defthm xr-dbg-mv-nth-2-rb-alt
  (equal (xr :dbg index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :dbg index x86)))

Theorem: xr-fp-data-mv-nth-2-rb-alt

(defthm xr-fp-data-mv-nth-2-rb-alt
  (equal (xr :fp-data index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :fp-data index x86)))

Theorem: xr-fp-ctrl-mv-nth-2-rb-alt

(defthm xr-fp-ctrl-mv-nth-2-rb-alt
  (equal (xr :fp-ctrl index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :fp-ctrl index x86)))

Theorem: xr-fp-status-mv-nth-2-rb-alt

(defthm xr-fp-status-mv-nth-2-rb-alt
  (equal (xr :fp-status index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :fp-status index x86)))

Theorem: xr-fp-tag-mv-nth-2-rb-alt

(defthm xr-fp-tag-mv-nth-2-rb-alt
  (equal (xr :fp-tag index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :fp-tag index x86)))

Theorem: xr-fp-last-inst-mv-nth-2-rb-alt

(defthm xr-fp-last-inst-mv-nth-2-rb-alt
  (equal (xr :fp-last-inst index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :fp-last-inst index x86)))

Theorem: xr-fp-last-data-mv-nth-2-rb-alt

(defthm xr-fp-last-data-mv-nth-2-rb-alt
  (equal (xr :fp-last-data index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :fp-last-data index x86)))

Theorem: xr-fp-opcode-mv-nth-2-rb-alt

(defthm xr-fp-opcode-mv-nth-2-rb-alt
  (equal (xr :fp-opcode index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :fp-opcode index x86)))

Theorem: xr-mxcsr-mv-nth-2-rb-alt

(defthm xr-mxcsr-mv-nth-2-rb-alt
  (equal (xr :mxcsr index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :mxcsr index x86)))

Theorem: xr-opmsk-mv-nth-2-rb-alt

(defthm xr-opmsk-mv-nth-2-rb-alt
  (equal (xr :opmsk index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :opmsk index x86)))

Theorem: xr-zmm-mv-nth-2-rb-alt

(defthm xr-zmm-mv-nth-2-rb-alt
  (equal (xr :zmm index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :zmm index x86)))

Theorem: xr-msr-mv-nth-2-rb-alt

(defthm xr-msr-mv-nth-2-rb-alt
  (equal (xr :msr index
             (mv-nth 2 (rb-alt n addr r-x x86)))
         (xr :msr index x86)))

Theorem: xr-fault-rb-alt-state-in-sys-view

(defthm xr-fault-rb-alt-state-in-sys-view
  (equal (xr :fault index
             (mv-nth 2 (rb-alt n lin-addr r-x x86)))
         (xr :fault index x86)))

Theorem: mv-nth-0-rb-alt-is-nil

(defthm mv-nth-0-rb-alt-is-nil
  (equal (mv-nth 0 (rb-alt n addr r-x x86))
         nil))

Theorem: mv-nth-0-rb-alt-xw-doc

(defthm mv-nth-0-rb-alt-xw-doc
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :doc index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-ms

(defthm mv-nth-0-rb-alt-xw-ms
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :ms index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-env

(defthm mv-nth-0-rb-alt-xw-env
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :env index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-undef

(defthm mv-nth-0-rb-alt-xw-undef
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :undef index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-os-info

(defthm mv-nth-0-rb-alt-xw-os-info
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :os-info index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-rgf

(defthm mv-nth-0-rb-alt-xw-rgf
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :rgf index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-rip

(defthm mv-nth-0-rb-alt-xw-rip
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :rip index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-str

(defthm mv-nth-0-rb-alt-xw-str
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :str index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-ssr-visible

(defthm mv-nth-0-rb-alt-xw-ssr-visible
  (equal (mv-nth 0
                 (rb-alt n addr
                         r-x (xw :ssr-visible index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-ssr-hidden-base

(defthm mv-nth-0-rb-alt-xw-ssr-hidden-base
  (equal (mv-nth 0
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-base index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-ssr-hidden-limit

(defthm mv-nth-0-rb-alt-xw-ssr-hidden-limit
  (equal (mv-nth 0
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-limit index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-ssr-hidden-attr

(defthm mv-nth-0-rb-alt-xw-ssr-hidden-attr
  (equal (mv-nth 0
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-attr index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-dbg

(defthm mv-nth-0-rb-alt-xw-dbg
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :dbg index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-fp-data

(defthm mv-nth-0-rb-alt-xw-fp-data
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :fp-data index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-fp-ctrl

(defthm mv-nth-0-rb-alt-xw-fp-ctrl
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :fp-ctrl index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-fp-status

(defthm mv-nth-0-rb-alt-xw-fp-status
  (equal (mv-nth 0
                 (rb-alt n
                         addr r-x (xw :fp-status index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-fp-tag

(defthm mv-nth-0-rb-alt-xw-fp-tag
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :fp-tag index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-fp-last-inst

(defthm mv-nth-0-rb-alt-xw-fp-last-inst
  (equal (mv-nth 0
                 (rb-alt n addr
                         r-x (xw :fp-last-inst index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-fp-last-data

(defthm mv-nth-0-rb-alt-xw-fp-last-data
  (equal (mv-nth 0
                 (rb-alt n addr
                         r-x (xw :fp-last-data index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-fp-opcode

(defthm mv-nth-0-rb-alt-xw-fp-opcode
  (equal (mv-nth 0
                 (rb-alt n
                         addr r-x (xw :fp-opcode index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-mxcsr

(defthm mv-nth-0-rb-alt-xw-mxcsr
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :mxcsr index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-opmsk

(defthm mv-nth-0-rb-alt-xw-opmsk
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :opmsk index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-xw-zmm

(defthm mv-nth-0-rb-alt-xw-zmm
  (equal (mv-nth 0
                 (rb-alt n addr r-x (xw :zmm index val x86)))
         (mv-nth 0
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-doc

(defthm mv-nth-1-rb-alt-xw-doc
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :doc index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-ms

(defthm mv-nth-1-rb-alt-xw-ms
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :ms index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-env

(defthm mv-nth-1-rb-alt-xw-env
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :env index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-undef

(defthm mv-nth-1-rb-alt-xw-undef
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :undef index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-os-info

(defthm mv-nth-1-rb-alt-xw-os-info
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :os-info index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-rgf

(defthm mv-nth-1-rb-alt-xw-rgf
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :rgf index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-rip

(defthm mv-nth-1-rb-alt-xw-rip
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :rip index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-str

(defthm mv-nth-1-rb-alt-xw-str
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :str index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-ssr-visible

(defthm mv-nth-1-rb-alt-xw-ssr-visible
  (equal (mv-nth 1
                 (rb-alt n addr
                         r-x (xw :ssr-visible index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-ssr-hidden-base

(defthm mv-nth-1-rb-alt-xw-ssr-hidden-base
  (equal (mv-nth 1
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-base index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-ssr-hidden-limit

(defthm mv-nth-1-rb-alt-xw-ssr-hidden-limit
  (equal (mv-nth 1
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-limit index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-ssr-hidden-attr

(defthm mv-nth-1-rb-alt-xw-ssr-hidden-attr
  (equal (mv-nth 1
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-attr index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-dbg

(defthm mv-nth-1-rb-alt-xw-dbg
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :dbg index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-fp-data

(defthm mv-nth-1-rb-alt-xw-fp-data
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :fp-data index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-fp-ctrl

(defthm mv-nth-1-rb-alt-xw-fp-ctrl
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :fp-ctrl index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-fp-status

(defthm mv-nth-1-rb-alt-xw-fp-status
  (equal (mv-nth 1
                 (rb-alt n
                         addr r-x (xw :fp-status index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-fp-tag

(defthm mv-nth-1-rb-alt-xw-fp-tag
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :fp-tag index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-fp-last-inst

(defthm mv-nth-1-rb-alt-xw-fp-last-inst
  (equal (mv-nth 1
                 (rb-alt n addr
                         r-x (xw :fp-last-inst index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-fp-last-data

(defthm mv-nth-1-rb-alt-xw-fp-last-data
  (equal (mv-nth 1
                 (rb-alt n addr
                         r-x (xw :fp-last-data index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-fp-opcode

(defthm mv-nth-1-rb-alt-xw-fp-opcode
  (equal (mv-nth 1
                 (rb-alt n
                         addr r-x (xw :fp-opcode index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-mxcsr

(defthm mv-nth-1-rb-alt-xw-mxcsr
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :mxcsr index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-opmsk

(defthm mv-nth-1-rb-alt-xw-opmsk
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :opmsk index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-1-rb-alt-xw-zmm

(defthm mv-nth-1-rb-alt-xw-zmm
  (equal (mv-nth 1
                 (rb-alt n addr r-x (xw :zmm index val x86)))
         (mv-nth 1
                 (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: rb-alt-xw-rflags-not-ac-values-in-sys-view

(defthm rb-alt-xw-rflags-not-ac-values-in-sys-view
 (implies
  (equal (rflagsbits->ac (double-rewrite value))
         (rflagsbits->ac (rflags x86)))
  (and
      (equal (mv-nth 0
                     (rb-alt n addr r-x (xw :rflags nil value x86)))
             (mv-nth 0 (rb-alt n addr r-x x86)))
      (equal (mv-nth 1
                     (rb-alt n addr r-x (xw :rflags nil value x86)))
             (mv-nth 1 (rb-alt n addr r-x x86))))))

Theorem: mv-nth-2-rb-alt-xw-doc

(defthm mv-nth-2-rb-alt-xw-doc
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :doc index val x86)))
         (xw :doc index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-ms

(defthm mv-nth-2-rb-alt-xw-ms
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :ms index val x86)))
         (xw :ms index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-env

(defthm mv-nth-2-rb-alt-xw-env
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :env index val x86)))
         (xw :env index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-undef

(defthm mv-nth-2-rb-alt-xw-undef
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :undef index val x86)))
         (xw :undef index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-os-info

(defthm mv-nth-2-rb-alt-xw-os-info
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :os-info index val x86)))
         (xw :os-info index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-rgf

(defthm mv-nth-2-rb-alt-xw-rgf
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :rgf index val x86)))
         (xw :rgf index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-rip

(defthm mv-nth-2-rb-alt-xw-rip
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :rip index val x86)))
         (xw :rip index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-str

(defthm mv-nth-2-rb-alt-xw-str
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :str index val x86)))
         (xw :str index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-ssr-visible

(defthm mv-nth-2-rb-alt-xw-ssr-visible
  (equal (mv-nth 2
                 (rb-alt n addr
                         r-x (xw :ssr-visible index val x86)))
         (xw :ssr-visible index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-ssr-hidden-base

(defthm mv-nth-2-rb-alt-xw-ssr-hidden-base
  (equal (mv-nth 2
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-base index val x86)))
         (xw :ssr-hidden-base index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-ssr-hidden-limit

(defthm mv-nth-2-rb-alt-xw-ssr-hidden-limit
  (equal (mv-nth 2
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-limit index val x86)))
         (xw :ssr-hidden-limit index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-ssr-hidden-attr

(defthm mv-nth-2-rb-alt-xw-ssr-hidden-attr
  (equal (mv-nth 2
                 (rb-alt n addr r-x
                         (xw :ssr-hidden-attr index val x86)))
         (xw :ssr-hidden-attr index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-dbg

(defthm mv-nth-2-rb-alt-xw-dbg
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :dbg index val x86)))
         (xw :dbg index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-fp-data

(defthm mv-nth-2-rb-alt-xw-fp-data
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :fp-data index val x86)))
         (xw :fp-data index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-fp-ctrl

(defthm mv-nth-2-rb-alt-xw-fp-ctrl
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :fp-ctrl index val x86)))
         (xw :fp-ctrl index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-fp-status

(defthm mv-nth-2-rb-alt-xw-fp-status
  (equal (mv-nth 2
                 (rb-alt n
                         addr r-x (xw :fp-status index val x86)))
         (xw :fp-status index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-fp-tag

(defthm mv-nth-2-rb-alt-xw-fp-tag
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :fp-tag index val x86)))
         (xw :fp-tag index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-fp-last-inst

(defthm mv-nth-2-rb-alt-xw-fp-last-inst
  (equal (mv-nth 2
                 (rb-alt n addr
                         r-x (xw :fp-last-inst index val x86)))
         (xw :fp-last-inst index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-fp-last-data

(defthm mv-nth-2-rb-alt-xw-fp-last-data
  (equal (mv-nth 2
                 (rb-alt n addr
                         r-x (xw :fp-last-data index val x86)))
         (xw :fp-last-data index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-fp-opcode

(defthm mv-nth-2-rb-alt-xw-fp-opcode
  (equal (mv-nth 2
                 (rb-alt n
                         addr r-x (xw :fp-opcode index val x86)))
         (xw :fp-opcode index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-mxcsr

(defthm mv-nth-2-rb-alt-xw-mxcsr
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :mxcsr index val x86)))
         (xw :mxcsr index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-opmsk

(defthm mv-nth-2-rb-alt-xw-opmsk
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :opmsk index val x86)))
         (xw :opmsk index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: mv-nth-2-rb-alt-xw-zmm

(defthm mv-nth-2-rb-alt-xw-zmm
  (equal (mv-nth 2
                 (rb-alt n addr r-x (xw :zmm index val x86)))
         (xw :zmm index val
             (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: rb-alt-xw-rflags-not-ac-state-in-sys-view

(defthm rb-alt-xw-rflags-not-ac-state-in-sys-view
 (implies
      (equal (rflagsbits->ac (double-rewrite value))
             (rflagsbits->ac (rflags x86)))
      (equal (mv-nth 2
                     (rb-alt n addr r-x (xw :rflags nil value x86)))
             (xw :rflags nil value
                 (mv-nth 2 (rb-alt n addr r-x x86))))))

Theorem: rb-alt-values-and-xw-rflags-in-sys-view

(defthm rb-alt-values-and-xw-rflags-in-sys-view
 (implies
  (and (equal (rflagsbits->ac (double-rewrite value))
              (rflagsbits->ac (rflags x86)))
       (x86p x86))
  (and
     (equal (mv-nth 0
                    (rb-alt n addrs r-x (xw :rflags nil value x86)))
            (mv-nth 0
                    (rb-alt n addrs r-x (double-rewrite x86))))
     (equal (mv-nth 1
                    (rb-alt n addrs r-x (xw :rflags nil value x86)))
            (mv-nth 1
                    (rb-alt n addrs r-x (double-rewrite x86)))))))

Theorem: rb-alt-and-xw-rflags-state-in-sys-view

(defthm rb-alt-and-xw-rflags-state-in-sys-view
  (implies (and (equal (rflagsbits->ac (double-rewrite value))
                       (rflagsbits->ac (rflags x86)))
                (x86p x86))
           (equal (mv-nth 2
                          (rb-alt n lin-addr
                                  r-x (xw :rflags nil value x86)))
                  (xw :rflags nil value
                      (mv-nth 2 (rb-alt n lin-addr r-x x86))))))

Theorem: xr-rflags-and-mv-nth-2-rb-alt

(defthm xr-rflags-and-mv-nth-2-rb-alt
  (equal (xr :rflags nil
             (mv-nth 2 (rb-alt n lin-addr r-x x86)))
         (xr :rflags nil x86)))

Theorem: alignment-checking-enabled-p-and-mv-nth-2-rb-alt

(defthm alignment-checking-enabled-p-and-mv-nth-2-rb-alt
  (equal (alignment-checking-enabled-p
              (mv-nth 2 (rb-alt n lin-addr r-x x86)))
         (alignment-checking-enabled-p x86)))

Theorem: mv-nth-2-rb-alt-in-system-level-marking-view

(defthm mv-nth-2-rb-alt-in-system-level-marking-view
 (implies
  (and
     (not (mv-nth 0
                  (las-to-pas n lin-addr r-x (double-rewrite x86))))
     (disjoint-p
          (mv-nth 1
                  (las-to-pas n lin-addr r-x (double-rewrite x86)))
          (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                      (double-rewrite x86))))
     (canonical-address-p lin-addr)
     (canonical-address-p (+ -1 n lin-addr))
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86)))
  (equal
       (mv-nth 2 (rb-alt n lin-addr r-x x86))
       (mv-nth 2
               (las-to-pas n lin-addr r-x (double-rewrite x86))))))

Theorem: rewrite-rb-to-rb-alt

(defthm rewrite-rb-to-rb-alt
 (implies
  (and
   (disjoint-p (mv-nth 1
                       (las-to-pas n addr r-x (double-rewrite x86)))
               (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                           (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas n addr r-x (double-rewrite x86))))
   (canonical-address-p addr)
   (canonical-address-p (+ -1 n addr))
   (marking-view x86)
   (not (app-view x86))
   (64-bit-modep (double-rewrite x86)))
  (equal (rb n addr r-x x86)
         (rb-alt n addr r-x (double-rewrite x86)))))

Theorem: mv-nth-0-rb-alt-and-xlate-equiv-memory-cong

(defthm mv-nth-0-rb-alt-and-xlate-equiv-memory-cong
  (implies (xlate-equiv-memory x86-1 x86-2)
           (equal (mv-nth 0 (rb-alt n addr r-x x86-1))
                  (mv-nth 0 (rb-alt n addr r-x x86-2))))
  :rule-classes :congruence)

Theorem: mv-nth-1-rb-alt-and-xlate-equiv-memory-cong

(defthm mv-nth-1-rb-alt-and-xlate-equiv-memory-cong
  (implies (xlate-equiv-memory x86-1 x86-2)
           (equal (mv-nth 1 (rb-alt n lin-addr r-w-x x86-1))
                  (mv-nth 1 (rb-alt n lin-addr r-w-x x86-2))))
  :rule-classes :congruence)

Theorem: mv-nth-2-rb-alt-and-xlate-equiv-memory

(defthm mv-nth-2-rb-alt-and-xlate-equiv-memory
  (and (xlate-equiv-memory (mv-nth 2 (rb-alt n addr r-x x86))
                           (double-rewrite x86))
       (xlate-equiv-memory x86
                           (mv-nth 2 (rb-alt n addr r-x x86)))))

Theorem: xlate-equiv-memory-and-two-mv-nth-2-rb-alt-cong

(defthm xlate-equiv-memory-and-two-mv-nth-2-rb-alt-cong
 (implies (xlate-equiv-memory x86-1 x86-2)
          (xlate-equiv-memory (mv-nth 2 (rb-alt n addr r-x x86-1))
                              (mv-nth 2 (rb-alt n addr r-x x86-2))))
 :rule-classes :congruence)

Theorem: many-reads-with-rb-alt-from-program-at-alt-in-marking-view

(defthm many-reads-with-rb-alt-from-program-at-alt-in-marking-view
 (implies (and (bind-free (find-program-at-info 'prog-addr
                                                'bytes
                                                mfc state)
                          (prog-addr bytes))
               (program-at-alt prog-addr bytes (double-rewrite x86))
               (<= prog-addr lin-addr)
               (< (+ n lin-addr)
                  (+ (len bytes) prog-addr))
               (integerp lin-addr)
               (posp n)
               (byte-listp bytes)
               (64-bit-modep (double-rewrite x86))
               (x86p x86))
          (equal (mv-nth 1 (rb-alt n lin-addr :x x86))
                 (combine-n-bytes (- lin-addr prog-addr)
                                  n bytes))))

Theorem: one-read-with-rb-alt-from-program-at-alt-in-marking-view

(defthm one-read-with-rb-alt-from-program-at-alt-in-marking-view
 (implies (and (bind-free (find-program-at-info 'prog-addr
                                                'bytes
                                                mfc state)
                          (prog-addr bytes))
               (program-at-alt prog-addr bytes (double-rewrite x86))
               (<= prog-addr lin-addr)
               (< lin-addr (+ (len bytes) prog-addr))
               (integerp lin-addr)
               (byte-listp bytes)
               (64-bit-modep (double-rewrite x86))
               (x86p x86))
          (equal (mv-nth 1 (rb-alt 1 lin-addr :x x86))
                 (nth (- lin-addr prog-addr) bytes))))

Theorem: rb-alt-wb-equal-in-sys-view

(defthm rb-alt-wb-equal-in-sys-view
 (implies
  (and
   (equal
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (mv-nth 1
                (las-to-pas n-w write-addr
                            :w (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))))
   (no-duplicates-p (mv-nth 1
                            (las-to-pas n-w write-addr
                                        :w (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (not (mv-nth 0
                (las-to-pas n-w write-addr
                            :w (double-rewrite x86))))
   (canonical-address-p (+ -1 n lin-addr))
   (canonical-address-p lin-addr)
   (unsigned-byte-p (ash n-w 3) value)
   (natp n-w)
   (64-bit-modep (double-rewrite x86))
   (not (app-view x86))
   (marking-view x86)
   (x86p x86))
  (and
   (equal
        (mv-nth 0
                (rb-alt n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
        nil)
   (equal
        (mv-nth 1
                (rb-alt n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
        value))))

Theorem: rb-alt-wb-disjoint-in-sys-view

(defthm rb-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 n lin-addr r-w-x (double-rewrite x86))))
   (disjoint-p
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (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))))
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (canonical-address-p (+ -1 n lin-addr))
   (canonical-address-p lin-addr)
   (canonical-address-p (+ -1 n-w write-addr))
   (canonical-address-p write-addr)
   (marking-view x86)
   (64-bit-modep (double-rewrite x86))
   (not (app-view x86)))
  (and
   (equal
        (mv-nth 0
                (rb-alt n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
        (mv-nth 0
                (rb-alt n lin-addr r-w-x (double-rewrite x86))))
   (equal
        (mv-nth 1
                (rb-alt n lin-addr r-w-x
                        (mv-nth 1 (wb n-w write-addr w value x86))))
        (mv-nth 1
                (rb-alt n lin-addr
                        r-w-x (double-rewrite x86)))))))

Theorem: no-errors-when-translating-program-bytes-in-marking-view-using-program-at-alt

(defthm
 no-errors-when-translating-program-bytes-in-marking-view-using-program-at-alt
 (implies (and (bind-free (find-program-at-info 'prog-addr
                                                'bytes
                                                mfc state)
                          (prog-addr bytes))
               (program-at-alt prog-addr bytes x86)
               (<= prog-addr addr)
               (<= (+ n addr)
                   (+ (len bytes) prog-addr))
               (canonical-address-p addr)
               (64-bit-modep (double-rewrite x86)))
          (equal (mv-nth 0 (las-to-pas n addr :x x86))
                 nil)))

Theorem: disjointness-of-program-bytes-from-paging-structures

(defthm disjointness-of-program-bytes-from-paging-structures
 (implies
     (and (bind-free (find-program-at-info 'prog-addr
                                           'bytes
                                           mfc state)
                     (prog-addr bytes))
          (program-at-alt prog-addr bytes (double-rewrite x86))
          (<= prog-addr lin-addr)
          (<= (+ n lin-addr)
              (+ (len bytes) prog-addr))
          (posp n)
          (integerp lin-addr)
          (64-bit-modep (double-rewrite x86)))
     (disjoint-p
          (mv-nth 1 (las-to-pas n lin-addr :x x86))
          (open-qword-paddr-list
               (gather-all-paging-structure-qword-addresses x86)))))

Theorem: disjointness-of-las-to-pas-from-write-to-physical-memory-subset-of-paging-structures

(defthm
 disjointness-of-las-to-pas-from-write-to-physical-memory-subset-of-paging-structures
 (implies
  (and (equal p-addrs (addr-range 8 index))
       (disjoint-p
            (mv-nth 1 (las-to-pas n lin-addr r-x x86))
            (open-qword-paddr-list
                 (gather-all-paging-structure-qword-addresses x86)))
       (equal (page-size (double-rewrite value))
              1)
       (physical-address-p index)
       (equal (loghead 3 index) 0)
       (unsigned-byte-p 64 value)
       (not (app-view x86)))
  (disjoint-p
       (mv-nth 1 (las-to-pas n lin-addr r-x x86))
       (open-qword-paddr-list
            (gather-all-paging-structure-qword-addresses
                 (write-to-physical-memory p-addrs value x86))))))

Theorem: disjointness-of-las-to-pas-from-wb-to-subset-of-paging-structures-general

(defthm
 disjointness-of-las-to-pas-from-wb-to-subset-of-paging-structures-general
 (implies
     (and (equal (gather-all-paging-structure-qword-addresses
                      (double-rewrite x86-2))
                 (gather-all-paging-structure-qword-addresses
                      (double-rewrite x86-1)))
          (equal (mv-nth 1
                         (las-to-pas n-1 lin-addr-1
                                     r-w-x (double-rewrite x86-1)))
                 (mv-nth 1
                         (las-to-pas n-1 lin-addr-1
                                     r-w-x (double-rewrite x86-2))))
          (equal (page-size (double-rewrite value))
                 1)
          (direct-map-p 8 entry-addr
                        :w (double-rewrite x86-2))
          (disjoint-p$
               (mv-nth 1
                       (las-to-pas n-1 lin-addr-1
                                   r-w-x (double-rewrite x86-1)))
               (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                           (double-rewrite x86-1))))
          (<= lin-addr-1 lin-addr-2)
          (< (+ n-2 lin-addr-2)
             (+ n-1 lin-addr-1))
          (not (mv-nth 0
                       (las-to-pas n-1 lin-addr-1
                                   r-w-x (double-rewrite x86-1))))
          (physical-address-p entry-addr)
          (equal (loghead 3 entry-addr) 0)
          (unsigned-byte-p 64 value)
          (64-bit-modep x86-1)
          (64-bit-modep (double-rewrite x86-2))
          (not (app-view x86-2))
          (posp n-1)
          (posp n-2)
          (integerp lin-addr-2))
     (disjoint-p
          (mv-nth 1
                  (las-to-pas n-2 lin-addr-2 r-w-x x86-1))
          (open-qword-paddr-list
               (gather-all-paging-structure-qword-addresses
                    (mv-nth 1 (wb 8 entry-addr w value x86-2)))))))

Function: find-program-at-alt-len-bytes-info

(defun find-program-at-alt-len-bytes-info
       (addr-var bytes-var mfc state)
  (declare (xargs :stobjs (state))
           (ignorable state))
  (b* ((call (acl2::find-call-lst 'program-at-alt
                                  (mfc-clause mfc)))
       (call (or call
                 (acl2::find-call-lst 'program-at
                                      (mfc-clause mfc))))
       ((when (not call)) nil))
    (cons (cons addr-var (nth 1 call))
          (cons (cons bytes-var
                      (cons 'quote
                            (cons (len (unquote (nth 2 call)))
                                  'nil)))
                'nil))))

Theorem: disjointness-of-las-to-pas-from-wb-to-subset-of-paging-structures

(defthm
  disjointness-of-las-to-pas-from-wb-to-subset-of-paging-structures
 (implies
     (and (bind-free (find-program-at-alt-len-bytes-info 'lin-addr-1
                                                         'n-1
                                                         mfc state)
                     (lin-addr-1 n-1))
          (equal (gather-all-paging-structure-qword-addresses
                      (double-rewrite x86-2))
                 (gather-all-paging-structure-qword-addresses
                      (double-rewrite x86-1)))
          (equal (mv-nth 1
                         (las-to-pas n-1 lin-addr-1
                                     :x (double-rewrite x86-1)))
                 (mv-nth 1
                         (las-to-pas n-1 lin-addr-1
                                     :x (double-rewrite x86-2))))
          (equal (page-size (double-rewrite value))
                 1)
          (direct-map-p 8 entry-addr
                        :w (double-rewrite x86-2))
          (disjoint-p$
               (mv-nth 1
                       (las-to-pas n-1 lin-addr-1
                                   :x (double-rewrite x86-1)))
               (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                           (double-rewrite x86-1))))
          (<= lin-addr-1 lin-addr-2)
          (< (+ n-2 lin-addr-2)
             (+ n-1 lin-addr-1))
          (not (mv-nth 0
                       (las-to-pas n-1 lin-addr-1
                                   :x (double-rewrite x86-1))))
          (physical-address-p entry-addr)
          (equal (loghead 3 entry-addr) 0)
          (unsigned-byte-p 64 value)
          (64-bit-modep x86-1)
          (64-bit-modep (double-rewrite x86-2))
          (not (app-view x86-2))
          (posp n-1)
          (posp n-2)
          (integerp lin-addr-2))
     (disjoint-p
          (mv-nth 1 (las-to-pas n-2 lin-addr-2 :x x86-1))
          (open-qword-paddr-list
               (gather-all-paging-structure-qword-addresses
                    (mv-nth 1 (wb 8 entry-addr w value x86-2)))))))

Theorem: disjointness-of-las-to-pas-from-wb-to-a-paging-entry

(defthm disjointness-of-las-to-pas-from-wb-to-a-paging-entry
 (implies
  (and
   (equal (gather-all-paging-structure-qword-addresses
               (double-rewrite x86-2))
          (gather-all-paging-structure-qword-addresses
               (double-rewrite x86-1)))
   (equal
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-1)))
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-2))))
   (equal (page-size (double-rewrite value))
          1)
   (direct-map-p 8 entry-addr
                 :w (double-rewrite x86-2))
   (disjoint-p
        (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (double-rewrite x86-1)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86-1))))
   (physical-address-p entry-addr)
   (equal (loghead 3 entry-addr) 0)
   (unsigned-byte-p 64 value)
   (64-bit-modep x86-1)
   (64-bit-modep (double-rewrite x86-2))
   (not (app-view x86-2)))
  (disjoint-p
       (mv-nth 1 (las-to-pas n lin-addr r-w-x x86-1))
       (open-qword-paddr-list
            (gather-all-paging-structure-qword-addresses
                 (mv-nth 1 (wb 8 entry-addr w value x86-2)))))))

Theorem: rb-alt-and-wb-to-paging-structures-disjoint

(defthm rb-alt-and-wb-to-paging-structures-disjoint
 (implies
  (and
   (direct-map-p 8 entry-addr
                 :w (double-rewrite x86))
   (equal (page-size (double-rewrite value))
          1)
   (disjoint-p
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86)))
        (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                    (double-rewrite x86))))
   (disjoint-p (mv-nth 1
                       (las-to-pas 8 entry-addr
                                   :w (double-rewrite x86)))
               (all-xlation-governing-entries-paddrs
                    n lin-addr (double-rewrite x86)))
   (disjoint-p
        (mv-nth 1
                (las-to-pas 8 entry-addr
                            :w (double-rewrite x86)))
        (mv-nth 1
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (physical-address-p entry-addr)
   (equal (loghead 3 entry-addr) 0)
   (unsigned-byte-p 64 value)
   (canonical-address-p entry-addr))
  (and
   (equal (mv-nth 0
                  (rb-alt n lin-addr r-w-x
                          (mv-nth 1 (wb 8 entry-addr w value x86))))
          (mv-nth 0
                  (rb-alt n lin-addr r-w-x (double-rewrite x86))))
   (equal (mv-nth 1
                  (rb-alt n lin-addr r-w-x
                          (mv-nth 1 (wb 8 entry-addr w value x86))))
          (mv-nth 1
                  (rb-alt n lin-addr
                          r-w-x (double-rewrite x86)))))))