• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Tlb
      • Booting-linux
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
        • Cpuid
        • Linear-memory
          • Reasoning-about-memory-reads-and-writes
            • Las-to-pas
            • Rb
            • Create-canonical-address-list
            • Rb-1
            • Read-from-physical-memory
            • Write-to-physical-memory
            • Wb
            • Wb-1
            • Canonical-address-listp
          • Rml256
          • Wml256
          • Rml128
          • Rml80
          • Program-location
          • Rml64
          • Wml128
          • Rml48
          • Rml32
          • Rml08
          • Rml16
          • Wml80
          • Byte-listp
          • Wml64
          • Wml08
          • Wml48
          • Parametric-memory-reads-and-writes
          • Combine-n-bytes
          • Wml32
          • Program-at
          • Wml16
          • Combine-bytes
          • Write-canonical-address-to-memory-user-exec
          • Write-canonical-address-to-memory
          • Wml-size
          • Rml-size
          • Riml64
          • Riml32
          • Riml16
          • Riml08
          • Wiml64
          • Wiml32
          • Wiml16
          • Wiml08
          • Wiml-size
          • Generate-xr-over-write-thms
          • Generate-write-fn-over-xw-thms
          • Generate-read-fn-over-xw-thms
          • Riml-size
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • Register-readers-and-writers
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Linear-memory

Reasoning-about-memory-reads-and-writes

Definitions of rb and wb

The functions rb (read bytes) and wb (write bytes) are used in reasoning about memory reads and writes. Functions like rml08, rml16, rml32, and rml64 are reduced to rb, and wml08, wml16, wml32, and wml64 to wb during reasoning.

Definitions and Theorems

Function: canonical-address-listp

(defun canonical-address-listp (lst)
  (declare (xargs :guard t))
  (let ((__function__ 'canonical-address-listp))
    (declare (ignorable __function__))
    (if (equal lst nil)
        t
      (and (consp lst)
           (canonical-address-p (car lst))
           (canonical-address-listp (cdr lst))))))

Theorem: cdr-canonical-address-listp

(defthm cdr-canonical-address-listp
  (implies (canonical-address-listp x)
           (canonical-address-listp (cdr x))))

Function: create-canonical-address-list

(defun create-canonical-address-list (count addr)
  (declare (xargs :guard (natp count)))
  (let ((__function__ 'create-canonical-address-list))
    (declare (ignorable __function__))
    (if (or (zp count)
            (not (canonical-address-p addr)))
        nil
      (cons addr
            (create-canonical-address-list (1- count)
                                           (1+ addr))))))

Theorem: true-listp-create-canonical-address-list

(defthm true-listp-create-canonical-address-list
  (true-listp (create-canonical-address-list cnt lin-addr))
  :rule-classes (:rewrite :type-prescription))

Theorem: canonical-address-listp-create-canonical-address-list

(defthm canonical-address-listp-create-canonical-address-list
  (canonical-address-listp
       (create-canonical-address-list count addr))
  :rule-classes (:rewrite :type-prescription))

Theorem: create-canonical-address-list-1

(defthm create-canonical-address-list-1
  (implies (canonical-address-p x)
           (equal (create-canonical-address-list 1 x)
                  (list x))))

Theorem: len-of-create-canonical-address-list

(defthm len-of-create-canonical-address-list
  (implies (and (canonical-address-p (+ -1 addr count))
                (canonical-address-p addr)
                (natp count))
           (equal (len (create-canonical-address-list count addr))
                  count)))

Theorem: car-create-canonical-address-list

(defthm car-create-canonical-address-list
  (implies (and (canonical-address-p addr)
                (posp count))
           (equal (car (create-canonical-address-list count addr))
                  addr)))

Theorem: cdr-create-canonical-address-list

(defthm cdr-create-canonical-address-list
  (implies (and (canonical-address-p addr)
                (posp count))
           (equal (cdr (create-canonical-address-list count addr))
                  (create-canonical-address-list (1- count)
                                                 (1+ addr)))))

Theorem: consp-of-create-canonical-address-list

(defthm consp-of-create-canonical-address-list
  (implies (and (canonical-address-p addr)
                (natp count)
                (< 0 count))
           (consp (create-canonical-address-list count addr))))

Theorem: create-canonical-address-list-split

(defthm create-canonical-address-list-split
 (implies
     (and (canonical-address-p addr)
          (canonical-address-p (+ k addr))
          (natp j)
          (natp k))
     (equal (create-canonical-address-list (+ k j)
                                           addr)
            (append (create-canonical-address-list k addr)
                    (create-canonical-address-list j (+ k addr))))))

Function: rb-1

(defun rb-1 (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 :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'rb-1))
    (declare (ignorable __function__))
    (if (zp n)
        (mv nil 0 x86)
      (b* (((unless (canonical-address-p addr))
            (mv 'rb-1 0 x86))
           ((mv flg0 byte0 x86) (rvm08 addr x86))
           ((when flg0) (mv flg0 0 x86))
           ((mv rest-flg rest-bytes x86)
            (rb-1 (1- n) (1+ addr) r-x x86)))
        (mv rest-flg
            (logior byte0 (ash rest-bytes 8))
            x86)))))

Theorem: natp-of-rb-1.val

(defthm natp-of-rb-1.val
  (b* (((mv ?flg ?val ?new-x86)
        (rb-1 n addr r-x x86)))
    (natp val))
  :rule-classes :type-prescription)

Theorem: x86p-of-rb-1.new-x86

(defthm x86p-of-rb-1.new-x86
  (implies (x86p x86)
           (b* (((mv ?flg ?val ?new-x86)
                 (rb-1 n addr r-x x86)))
             (x86p new-x86)))
  :rule-classes :rewrite)

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

(defthm integerp-of-mv-nth-1-rb-1
  (b* (((mv ?flg ?val ?new-x86)
        (rb-1 n addr r-x x86)))
    (integerp val))
  :rule-classes :type-prescription)

Theorem: rb-1-returns-x86-app-view

(defthm rb-1-returns-x86-app-view
  (b* (((mv ?flg ?val ?new-x86)
        (rb-1 n addr r-x x86)))
    (implies (app-view x86)
             (equal new-x86 x86))))

Theorem: rb-1-returns-no-error-app-view

(defthm rb-1-returns-no-error-app-view
  (implies (and (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr))
                (app-view x86))
           (equal (mv-nth 0 (rb-1 n addr r-x x86))
                  nil)))

Theorem: size-of-rb-1

(defthm size-of-rb-1
 (implies (and (equal m (ash n 3)) (natp n))
          (unsigned-byte-p m (mv-nth 1 (rb-1 n addr r-x x86))))
 :rule-classes
 (:rewrite
  (:linear
    :corollary (implies (and (equal m (ash n 3)) (natp n))
                        (and (<= 0 (mv-nth 1 (rb-1 n addr r-x x86)))
                             (< (mv-nth 1 (rb-1 n addr r-x x86))
                                (expt 2 m))))
    :hints (("Goal" :in-theory (e/d* nil (rb-1)))))))

Function: las-to-pas

(defun las-to-pas (n lin-addr r-w-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :r :w :x) r-w-x))
  (declare (xargs :guard (and (natp n) (integerp lin-addr))))
  (declare (xargs :guard (not (app-view x86))))
  (let ((__function__ 'las-to-pas))
    (declare (ignorable __function__))
    (if (zp n)
        (mv nil nil x86)
      (b* (((unless (canonical-address-p lin-addr))
            (mv t nil x86))
           ((mv flg p-addr x86)
            (ia32e-la-to-pa lin-addr r-w-x x86))
           ((when flg) (mv flg nil x86))
           ((mv flgs p-addrs x86)
            (las-to-pas (1- n)
                        (1+ lin-addr)
                        r-w-x x86)))
        (mv flgs (if flgs nil (cons p-addr p-addrs))
            x86)))))

Theorem: true-listp-of-las-to-pas.p-addrs

(defthm true-listp-of-las-to-pas.p-addrs
  (b* (((mv ?flg ?p-addrs ?x86)
        (las-to-pas n lin-addr r-w-x x86)))
    (true-listp p-addrs))
  :rule-classes (:rewrite :type-prescription))

Theorem: x86p-of-las-to-pas.x86

(defthm x86p-of-las-to-pas.x86
  (implies (x86p x86)
           (b* (((mv ?flg ?p-addrs ?x86)
                 (las-to-pas n lin-addr r-w-x x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Theorem: consp-mv-nth-1-las-to-pas

(defthm consp-mv-nth-1-las-to-pas
  (implies (and (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
                (not (zp n)))
           (consp (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))
  :rule-classes (:rewrite :type-prescription))

Theorem: car-mv-nth-1-las-to-pas

(defthm car-mv-nth-1-las-to-pas
  (implies (and (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
                (not (zp n)))
           (equal (car (mv-nth 1 (las-to-pas n lin-addr r-w-x x86)))
                  (mv-nth 1
                          (ia32e-la-to-pa lin-addr r-w-x x86)))))

Theorem: physical-address-listp-mv-nth-1-las-to-pas

(defthm physical-address-listp-mv-nth-1-las-to-pas
  (physical-address-listp
       (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: las-to-pas-n=0

(defthm las-to-pas-n=0
  (and (equal (mv-nth 0 (las-to-pas 0 lin-addr r-w-x x86))
              nil)
       (equal (mv-nth 1 (las-to-pas 0 lin-addr r-w-x x86))
              nil)
       (equal (mv-nth 2 (las-to-pas 0 lin-addr r-w-x x86))
              x86)))

Theorem: xr-ms-mv-nth-2-las-to-pas

(defthm xr-ms-mv-nth-2-las-to-pas
  (equal (xr :ms index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :ms index x86)))

Theorem: xr-env-mv-nth-2-las-to-pas

(defthm xr-env-mv-nth-2-las-to-pas
  (equal (xr :env index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :env index x86)))

Theorem: xr-undef-mv-nth-2-las-to-pas

(defthm xr-undef-mv-nth-2-las-to-pas
  (equal (xr :undef index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :undef index x86)))

Theorem: xr-app-view-mv-nth-2-las-to-pas

(defthm xr-app-view-mv-nth-2-las-to-pas
  (equal (xr :app-view index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :app-view index x86)))

Theorem: xr-marking-view-mv-nth-2-las-to-pas

(defthm xr-marking-view-mv-nth-2-las-to-pas
  (equal (xr :marking-view index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :marking-view index x86)))

Theorem: xr-enable-peripherals-mv-nth-2-las-to-pas

(defthm xr-enable-peripherals-mv-nth-2-las-to-pas
  (equal (xr :enable-peripherals index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :enable-peripherals index x86)))

Theorem: xr-handle-exceptions-mv-nth-2-las-to-pas

(defthm xr-handle-exceptions-mv-nth-2-las-to-pas
  (equal (xr :handle-exceptions index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :handle-exceptions index x86)))

Theorem: xr-os-info-mv-nth-2-las-to-pas

(defthm xr-os-info-mv-nth-2-las-to-pas
  (equal (xr :os-info index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :os-info index x86)))

Theorem: xr-rgf-mv-nth-2-las-to-pas

(defthm xr-rgf-mv-nth-2-las-to-pas
  (equal (xr :rgf index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :rgf index x86)))

Theorem: xr-rip-mv-nth-2-las-to-pas

(defthm xr-rip-mv-nth-2-las-to-pas
  (equal (xr :rip index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :rip index x86)))

Theorem: xr-rflags-mv-nth-2-las-to-pas

(defthm xr-rflags-mv-nth-2-las-to-pas
  (equal (xr :rflags index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :rflags index x86)))

Theorem: xr-seg-visible-mv-nth-2-las-to-pas

(defthm xr-seg-visible-mv-nth-2-las-to-pas
  (equal (xr :seg-visible index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :seg-visible index x86)))

Theorem: xr-seg-hidden-base-mv-nth-2-las-to-pas

(defthm xr-seg-hidden-base-mv-nth-2-las-to-pas
  (equal (xr :seg-hidden-base index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :seg-hidden-base index x86)))

Theorem: xr-seg-hidden-limit-mv-nth-2-las-to-pas

(defthm xr-seg-hidden-limit-mv-nth-2-las-to-pas
  (equal (xr :seg-hidden-limit index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :seg-hidden-limit index x86)))

Theorem: xr-seg-hidden-attr-mv-nth-2-las-to-pas

(defthm xr-seg-hidden-attr-mv-nth-2-las-to-pas
  (equal (xr :seg-hidden-attr index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :seg-hidden-attr index x86)))

Theorem: xr-str-mv-nth-2-las-to-pas

(defthm xr-str-mv-nth-2-las-to-pas
  (equal (xr :str index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :str index x86)))

Theorem: xr-ssr-visible-mv-nth-2-las-to-pas

(defthm xr-ssr-visible-mv-nth-2-las-to-pas
  (equal (xr :ssr-visible index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :ssr-visible index x86)))

Theorem: xr-ssr-hidden-base-mv-nth-2-las-to-pas

(defthm xr-ssr-hidden-base-mv-nth-2-las-to-pas
  (equal (xr :ssr-hidden-base index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :ssr-hidden-base index x86)))

Theorem: xr-ssr-hidden-limit-mv-nth-2-las-to-pas

(defthm xr-ssr-hidden-limit-mv-nth-2-las-to-pas
  (equal (xr :ssr-hidden-limit index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :ssr-hidden-limit index x86)))

Theorem: xr-ssr-hidden-attr-mv-nth-2-las-to-pas

(defthm xr-ssr-hidden-attr-mv-nth-2-las-to-pas
  (equal (xr :ssr-hidden-attr index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :ssr-hidden-attr index x86)))

Theorem: xr-ctr-mv-nth-2-las-to-pas

(defthm xr-ctr-mv-nth-2-las-to-pas
  (equal (xr :ctr index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :ctr index x86)))

Theorem: xr-dbg-mv-nth-2-las-to-pas

(defthm xr-dbg-mv-nth-2-las-to-pas
  (equal (xr :dbg index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :dbg index x86)))

Theorem: xr-fp-data-mv-nth-2-las-to-pas

(defthm xr-fp-data-mv-nth-2-las-to-pas
  (equal (xr :fp-data index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :fp-data index x86)))

Theorem: xr-fp-ctrl-mv-nth-2-las-to-pas

(defthm xr-fp-ctrl-mv-nth-2-las-to-pas
  (equal (xr :fp-ctrl index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :fp-ctrl index x86)))

Theorem: xr-fp-status-mv-nth-2-las-to-pas

(defthm xr-fp-status-mv-nth-2-las-to-pas
  (equal (xr :fp-status index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :fp-status index x86)))

Theorem: xr-fp-tag-mv-nth-2-las-to-pas

(defthm xr-fp-tag-mv-nth-2-las-to-pas
  (equal (xr :fp-tag index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :fp-tag index x86)))

Theorem: xr-fp-last-inst-mv-nth-2-las-to-pas

(defthm xr-fp-last-inst-mv-nth-2-las-to-pas
  (equal (xr :fp-last-inst index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :fp-last-inst index x86)))

Theorem: xr-fp-last-data-mv-nth-2-las-to-pas

(defthm xr-fp-last-data-mv-nth-2-las-to-pas
  (equal (xr :fp-last-data index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :fp-last-data index x86)))

Theorem: xr-fp-opcode-mv-nth-2-las-to-pas

(defthm xr-fp-opcode-mv-nth-2-las-to-pas
  (equal (xr :fp-opcode index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :fp-opcode index x86)))

Theorem: xr-mxcsr-mv-nth-2-las-to-pas

(defthm xr-mxcsr-mv-nth-2-las-to-pas
  (equal (xr :mxcsr index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :mxcsr index x86)))

Theorem: xr-opmsk-mv-nth-2-las-to-pas

(defthm xr-opmsk-mv-nth-2-las-to-pas
  (equal (xr :opmsk index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :opmsk index x86)))

Theorem: xr-zmm-mv-nth-2-las-to-pas

(defthm xr-zmm-mv-nth-2-las-to-pas
  (equal (xr :zmm index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :zmm index x86)))

Theorem: xr-msr-mv-nth-2-las-to-pas

(defthm xr-msr-mv-nth-2-las-to-pas
  (equal (xr :msr index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :msr index x86)))

Theorem: xr-inhibit-interrupts-one-instruction-mv-nth-2-las-to-pas

(defthm xr-inhibit-interrupts-one-instruction-mv-nth-2-las-to-pas
  (equal (xr :inhibit-interrupts-one-instruction
             index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :inhibit-interrupts-one-instruction
             index x86)))

Theorem: xr-time-stamp-counter-mv-nth-2-las-to-pas

(defthm xr-time-stamp-counter-mv-nth-2-las-to-pas
  (equal (xr :time-stamp-counter index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :time-stamp-counter index x86)))

Theorem: xr-last-clock-event-mv-nth-2-las-to-pas

(defthm xr-last-clock-event-mv-nth-2-las-to-pas
  (equal (xr :last-clock-event index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :last-clock-event index x86)))

Theorem: xr-implicit-supervisor-access-mv-nth-2-las-to-pas

(defthm xr-implicit-supervisor-access-mv-nth-2-las-to-pas
  (equal (xr :implicit-supervisor-access index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :implicit-supervisor-access index x86)))

Theorem: xr-tty-in-mv-nth-2-las-to-pas

(defthm xr-tty-in-mv-nth-2-las-to-pas
  (equal (xr :tty-in index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :tty-in index x86)))

Theorem: xr-tty-out-mv-nth-2-las-to-pas

(defthm xr-tty-out-mv-nth-2-las-to-pas
  (equal (xr :tty-out index
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (xr :tty-out index x86)))

Theorem: xr-rflags-las-to-pas

(defthm xr-rflags-las-to-pas
 (implies
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (equal (xr :rflags nil
              (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
          (xr :rflags nil (double-rewrite x86)))))

Theorem: xr-fault-las-to-pas

(defthm xr-fault-las-to-pas
 (implies
   (not (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (equal (xr :fault nil
              (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
          (xr :fault nil (double-rewrite x86)))))

Theorem: mv-nth-0-las-to-pas-xw-ms

(defthm mv-nth-0-las-to-pas-xw-ms
  (equal (mv-nth 0
                 (las-to-pas n
                             lin-addr r-w-x (xw :ms index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-env

(defthm mv-nth-0-las-to-pas-xw-env
 (equal (mv-nth 0
                (las-to-pas n
                            lin-addr r-w-x (xw :env index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-undef

(defthm mv-nth-0-las-to-pas-xw-undef
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :undef index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-enable-peripherals

(defthm mv-nth-0-las-to-pas-xw-enable-peripherals
 (equal (mv-nth 0
                (las-to-pas n lin-addr r-w-x
                            (xw :enable-peripherals index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-handle-exceptions

(defthm mv-nth-0-las-to-pas-xw-handle-exceptions
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :handle-exceptions index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-os-info

(defthm mv-nth-0-las-to-pas-xw-os-info
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :os-info index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-rgf

(defthm mv-nth-0-las-to-pas-xw-rgf
 (equal (mv-nth 0
                (las-to-pas n
                            lin-addr r-w-x (xw :rgf index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-rip

(defthm mv-nth-0-las-to-pas-xw-rip
 (equal (mv-nth 0
                (las-to-pas n
                            lin-addr r-w-x (xw :rip index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-seg-hidden-base

(defthm mv-nth-0-las-to-pas-xw-seg-hidden-base
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-base index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-seg-hidden-limit

(defthm mv-nth-0-las-to-pas-xw-seg-hidden-limit
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-limit index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-seg-hidden-attr

(defthm mv-nth-0-las-to-pas-xw-seg-hidden-attr
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-attr index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-str

(defthm mv-nth-0-las-to-pas-xw-str
 (equal (mv-nth 0
                (las-to-pas n
                            lin-addr r-w-x (xw :str index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-ssr-visible

(defthm mv-nth-0-las-to-pas-xw-ssr-visible
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :ssr-visible index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-ssr-hidden-base

(defthm mv-nth-0-las-to-pas-xw-ssr-hidden-base
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-base index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-ssr-hidden-limit

(defthm mv-nth-0-las-to-pas-xw-ssr-hidden-limit
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-limit index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-ssr-hidden-attr

(defthm mv-nth-0-las-to-pas-xw-ssr-hidden-attr
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-attr index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-dbg

(defthm mv-nth-0-las-to-pas-xw-dbg
 (equal (mv-nth 0
                (las-to-pas n
                            lin-addr r-w-x (xw :dbg index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-fp-data

(defthm mv-nth-0-las-to-pas-xw-fp-data
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-data index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-fp-ctrl

(defthm mv-nth-0-las-to-pas-xw-fp-ctrl
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-ctrl index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-fp-status

(defthm mv-nth-0-las-to-pas-xw-fp-status
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-status index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-fp-tag

(defthm mv-nth-0-las-to-pas-xw-fp-tag
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-tag index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-fp-last-inst

(defthm mv-nth-0-las-to-pas-xw-fp-last-inst
 (equal (mv-nth 0
                (las-to-pas n lin-addr
                            r-w-x (xw :fp-last-inst index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-fp-last-data

(defthm mv-nth-0-las-to-pas-xw-fp-last-data
 (equal (mv-nth 0
                (las-to-pas n lin-addr
                            r-w-x (xw :fp-last-data index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-fp-opcode

(defthm mv-nth-0-las-to-pas-xw-fp-opcode
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-opcode index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-mxcsr

(defthm mv-nth-0-las-to-pas-xw-mxcsr
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :mxcsr index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-opmsk

(defthm mv-nth-0-las-to-pas-xw-opmsk
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :opmsk index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-zmm

(defthm mv-nth-0-las-to-pas-xw-zmm
 (equal (mv-nth 0
                (las-to-pas n
                            lin-addr r-w-x (xw :zmm index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-inhibit-interrupts-one-instruction

(defthm mv-nth-0-las-to-pas-xw-inhibit-interrupts-one-instruction
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :inhibit-interrupts-one-instruction
                                 index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-time-stamp-counter

(defthm mv-nth-0-las-to-pas-xw-time-stamp-counter
 (equal (mv-nth 0
                (las-to-pas n lin-addr r-w-x
                            (xw :time-stamp-counter index val x86)))
        (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-last-clock-event

(defthm mv-nth-0-las-to-pas-xw-last-clock-event
  (equal (mv-nth 0
                 (las-to-pas n lin-addr r-w-x
                             (xw :last-clock-event index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-tty-in

(defthm mv-nth-0-las-to-pas-xw-tty-in
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :tty-in index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-0-las-to-pas-xw-tty-out

(defthm mv-nth-0-las-to-pas-xw-tty-out
  (equal (mv-nth 0
                 (las-to-pas n lin-addr
                             r-w-x (xw :tty-out index val x86)))
         (mv-nth 0 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-ms

(defthm mv-nth-1-las-to-pas-xw-ms
  (equal (mv-nth 1
                 (las-to-pas n
                             lin-addr r-w-x (xw :ms index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-env

(defthm mv-nth-1-las-to-pas-xw-env
 (equal (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (xw :env index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-undef

(defthm mv-nth-1-las-to-pas-xw-undef
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :undef index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-enable-peripherals

(defthm mv-nth-1-las-to-pas-xw-enable-peripherals
 (equal (mv-nth 1
                (las-to-pas n lin-addr r-w-x
                            (xw :enable-peripherals index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-handle-exceptions

(defthm mv-nth-1-las-to-pas-xw-handle-exceptions
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :handle-exceptions index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-os-info

(defthm mv-nth-1-las-to-pas-xw-os-info
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :os-info index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-rgf

(defthm mv-nth-1-las-to-pas-xw-rgf
 (equal (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (xw :rgf index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-rip

(defthm mv-nth-1-las-to-pas-xw-rip
 (equal (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (xw :rip index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-seg-hidden-base

(defthm mv-nth-1-las-to-pas-xw-seg-hidden-base
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-base index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-seg-hidden-limit

(defthm mv-nth-1-las-to-pas-xw-seg-hidden-limit
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-limit index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-seg-hidden-attr

(defthm mv-nth-1-las-to-pas-xw-seg-hidden-attr
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-attr index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-str

(defthm mv-nth-1-las-to-pas-xw-str
 (equal (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (xw :str index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-ssr-visible

(defthm mv-nth-1-las-to-pas-xw-ssr-visible
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :ssr-visible index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-ssr-hidden-base

(defthm mv-nth-1-las-to-pas-xw-ssr-hidden-base
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-base index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-ssr-hidden-limit

(defthm mv-nth-1-las-to-pas-xw-ssr-hidden-limit
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-limit index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-ssr-hidden-attr

(defthm mv-nth-1-las-to-pas-xw-ssr-hidden-attr
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-attr index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-dbg

(defthm mv-nth-1-las-to-pas-xw-dbg
 (equal (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (xw :dbg index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-fp-data

(defthm mv-nth-1-las-to-pas-xw-fp-data
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-data index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-fp-ctrl

(defthm mv-nth-1-las-to-pas-xw-fp-ctrl
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-ctrl index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-fp-status

(defthm mv-nth-1-las-to-pas-xw-fp-status
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-status index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-fp-tag

(defthm mv-nth-1-las-to-pas-xw-fp-tag
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-tag index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-fp-last-inst

(defthm mv-nth-1-las-to-pas-xw-fp-last-inst
 (equal (mv-nth 1
                (las-to-pas n lin-addr
                            r-w-x (xw :fp-last-inst index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-fp-last-data

(defthm mv-nth-1-las-to-pas-xw-fp-last-data
 (equal (mv-nth 1
                (las-to-pas n lin-addr
                            r-w-x (xw :fp-last-data index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-fp-opcode

(defthm mv-nth-1-las-to-pas-xw-fp-opcode
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-opcode index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-mxcsr

(defthm mv-nth-1-las-to-pas-xw-mxcsr
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :mxcsr index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-opmsk

(defthm mv-nth-1-las-to-pas-xw-opmsk
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :opmsk index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-zmm

(defthm mv-nth-1-las-to-pas-xw-zmm
 (equal (mv-nth 1
                (las-to-pas n
                            lin-addr r-w-x (xw :zmm index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-inhibit-interrupts-one-instruction

(defthm mv-nth-1-las-to-pas-xw-inhibit-interrupts-one-instruction
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :inhibit-interrupts-one-instruction
                                 index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-time-stamp-counter

(defthm mv-nth-1-las-to-pas-xw-time-stamp-counter
 (equal (mv-nth 1
                (las-to-pas n lin-addr r-w-x
                            (xw :time-stamp-counter index val x86)))
        (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-last-clock-event

(defthm mv-nth-1-las-to-pas-xw-last-clock-event
  (equal (mv-nth 1
                 (las-to-pas n lin-addr r-w-x
                             (xw :last-clock-event index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-tty-in

(defthm mv-nth-1-las-to-pas-xw-tty-in
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :tty-in index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: mv-nth-1-las-to-pas-xw-tty-out

(defthm mv-nth-1-las-to-pas-xw-tty-out
  (equal (mv-nth 1
                 (las-to-pas n lin-addr
                             r-w-x (xw :tty-out index val x86)))
         (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

Theorem: 64-bit-modep-of-las-to-pas

(defthm 64-bit-modep-of-las-to-pas
  (equal (64-bit-modep (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-las-to-pas

(defthm x86-operation-mode-of-las-to-pas
 (equal
   (x86-operation-mode (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
   (x86-operation-mode x86)))

Theorem: mv-nth-2-las-to-pas-xw-ms

(defthm mv-nth-2-las-to-pas-xw-ms
  (equal (mv-nth 2
                 (las-to-pas n
                             lin-addr r-w-x (xw :ms index val x86)))
         (xw :ms index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-env

(defthm mv-nth-2-las-to-pas-xw-env
 (equal (mv-nth 2
                (las-to-pas n
                            lin-addr r-w-x (xw :env index val x86)))
        (xw :env index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-undef

(defthm mv-nth-2-las-to-pas-xw-undef
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :undef index val x86)))
         (xw :undef index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-enable-peripherals

(defthm mv-nth-2-las-to-pas-xw-enable-peripherals
 (equal (mv-nth 2
                (las-to-pas n lin-addr r-w-x
                            (xw :enable-peripherals index val x86)))
        (xw :enable-peripherals index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-handle-exceptions

(defthm mv-nth-2-las-to-pas-xw-handle-exceptions
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :handle-exceptions index val x86)))
         (xw :handle-exceptions index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-os-info

(defthm mv-nth-2-las-to-pas-xw-os-info
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :os-info index val x86)))
         (xw :os-info index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-rgf

(defthm mv-nth-2-las-to-pas-xw-rgf
 (equal (mv-nth 2
                (las-to-pas n
                            lin-addr r-w-x (xw :rgf index val x86)))
        (xw :rgf index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-rip

(defthm mv-nth-2-las-to-pas-xw-rip
 (equal (mv-nth 2
                (las-to-pas n
                            lin-addr r-w-x (xw :rip index val x86)))
        (xw :rip index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-seg-hidden-base

(defthm mv-nth-2-las-to-pas-xw-seg-hidden-base
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-base index val x86)))
         (xw :seg-hidden-base index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-seg-hidden-limit

(defthm mv-nth-2-las-to-pas-xw-seg-hidden-limit
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-limit index val x86)))
         (xw :seg-hidden-limit index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-seg-hidden-attr

(defthm mv-nth-2-las-to-pas-xw-seg-hidden-attr
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :seg-hidden-attr index val x86)))
         (xw :seg-hidden-attr index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-str

(defthm mv-nth-2-las-to-pas-xw-str
 (equal (mv-nth 2
                (las-to-pas n
                            lin-addr r-w-x (xw :str index val x86)))
        (xw :str index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-ssr-visible

(defthm mv-nth-2-las-to-pas-xw-ssr-visible
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :ssr-visible index val x86)))
         (xw :ssr-visible index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-ssr-hidden-base

(defthm mv-nth-2-las-to-pas-xw-ssr-hidden-base
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-base index val x86)))
         (xw :ssr-hidden-base index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-ssr-hidden-limit

(defthm mv-nth-2-las-to-pas-xw-ssr-hidden-limit
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-limit index val x86)))
         (xw :ssr-hidden-limit index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-ssr-hidden-attr

(defthm mv-nth-2-las-to-pas-xw-ssr-hidden-attr
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :ssr-hidden-attr index val x86)))
         (xw :ssr-hidden-attr index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-dbg

(defthm mv-nth-2-las-to-pas-xw-dbg
 (equal (mv-nth 2
                (las-to-pas n
                            lin-addr r-w-x (xw :dbg index val x86)))
        (xw :dbg index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-fp-data

(defthm mv-nth-2-las-to-pas-xw-fp-data
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-data index val x86)))
         (xw :fp-data index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-fp-ctrl

(defthm mv-nth-2-las-to-pas-xw-fp-ctrl
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-ctrl index val x86)))
         (xw :fp-ctrl index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-fp-status

(defthm mv-nth-2-las-to-pas-xw-fp-status
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-status index val x86)))
         (xw :fp-status index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-fp-tag

(defthm mv-nth-2-las-to-pas-xw-fp-tag
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-tag index val x86)))
         (xw :fp-tag index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-fp-last-inst

(defthm mv-nth-2-las-to-pas-xw-fp-last-inst
 (equal (mv-nth 2
                (las-to-pas n lin-addr
                            r-w-x (xw :fp-last-inst index val x86)))
        (xw :fp-last-inst index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-fp-last-data

(defthm mv-nth-2-las-to-pas-xw-fp-last-data
 (equal (mv-nth 2
                (las-to-pas n lin-addr
                            r-w-x (xw :fp-last-data index val x86)))
        (xw :fp-last-data index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-fp-opcode

(defthm mv-nth-2-las-to-pas-xw-fp-opcode
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :fp-opcode index val x86)))
         (xw :fp-opcode index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-mxcsr

(defthm mv-nth-2-las-to-pas-xw-mxcsr
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :mxcsr index val x86)))
         (xw :mxcsr index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-opmsk

(defthm mv-nth-2-las-to-pas-xw-opmsk
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :opmsk index val x86)))
         (xw :opmsk index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-zmm

(defthm mv-nth-2-las-to-pas-xw-zmm
 (equal (mv-nth 2
                (las-to-pas n
                            lin-addr r-w-x (xw :zmm index val x86)))
        (xw :zmm index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-inhibit-interrupts-one-instruction

(defthm mv-nth-2-las-to-pas-xw-inhibit-interrupts-one-instruction
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :inhibit-interrupts-one-instruction
                                 index val x86)))
         (xw :inhibit-interrupts-one-instruction
             index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-time-stamp-counter

(defthm mv-nth-2-las-to-pas-xw-time-stamp-counter
 (equal (mv-nth 2
                (las-to-pas n lin-addr r-w-x
                            (xw :time-stamp-counter index val x86)))
        (xw :time-stamp-counter index val
            (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-last-clock-event

(defthm mv-nth-2-las-to-pas-xw-last-clock-event
  (equal (mv-nth 2
                 (las-to-pas n lin-addr r-w-x
                             (xw :last-clock-event index val x86)))
         (xw :last-clock-event index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-tty-in

(defthm mv-nth-2-las-to-pas-xw-tty-in
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :tty-in index val x86)))
         (xw :tty-in index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: mv-nth-2-las-to-pas-xw-tty-out

(defthm mv-nth-2-las-to-pas-xw-tty-out
  (equal (mv-nth 2
                 (las-to-pas n lin-addr
                             r-w-x (xw :tty-out index val x86)))
         (xw :tty-out index val
             (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))))

Theorem: las-to-pas-xw-rflags-not-ac

(defthm las-to-pas-xw-rflags-not-ac
 (implies
  (equal (rflagsbits->ac value)
         (rflagsbits->ac (rflags (double-rewrite x86))))
  (and
   (equal
        (mv-nth 0
                (las-to-pas n lin-addr
                            r-w-x (xw :rflags nil value x86)))
        (mv-nth 0
                (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
   (equal (mv-nth 1
                  (las-to-pas n lin-addr
                              r-w-x (xw :rflags nil value x86)))
          (mv-nth 1
                  (las-to-pas n lin-addr
                              r-w-x (double-rewrite x86)))))))

Theorem: las-to-pas-xw-rflags-state-not-ac

(defthm las-to-pas-xw-rflags-state-not-ac
  (implies
       (equal (rflagsbits->ac value)
              (rflagsbits->ac (rflags x86)))
       (equal (mv-nth 2
                      (las-to-pas n lin-addr
                                  r-w-x (xw :rflags nil value x86)))
              (xw :rflags nil value
                  (mv-nth 2 (las-to-pas n lin-addr r-w-x x86))))))

Theorem: len-of-mv-nth-1-las-to-pas

(defthm len-of-mv-nth-1-las-to-pas
  (implies (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
           (equal (len (mv-nth 1 (las-to-pas n lin-addr r-w-x x86)))
                  (nfix n))))

Function: read-from-physical-memory

(defun read-from-physical-memory (p-addrs x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (physical-address-listp p-addrs)))
  (declare (xargs :guard (not (app-view x86))))
  (let ((__function__ 'read-from-physical-memory))
    (declare (ignorable __function__))
    (if (endp p-addrs)
        0
      (b* ((addr0 (car p-addrs))
           (byte0 (memi addr0 x86))
           (rest-bytes (read-from-physical-memory (cdr p-addrs)
                                                  x86)))
        (logior byte0 (ash rest-bytes 8))))))

Theorem: integerp-of-read-from-physical-memory

(defthm integerp-of-read-from-physical-memory
  (b* ((value (read-from-physical-memory p-addrs x86)))
    (integerp value))
  :rule-classes :type-prescription)

Theorem: size-of-read-from-physical-memory

(defthm size-of-read-from-physical-memory
 (implies (equal n (ash (len p-addrs) 3))
          (unsigned-byte-p n
                           (read-from-physical-memory p-addrs x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (implies (equal n (ash (len p-addrs) 3))
               (natp (read-from-physical-memory p-addrs x86)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies (equal n (ash (len p-addrs) 3))
            (and (<= 0
                     (read-from-physical-memory p-addrs x86))
                 (< (read-from-physical-memory p-addrs x86)
                    (expt 2 n))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: read-from-physical-memory-xw-rflags

(defthm read-from-physical-memory-xw-rflags
 (equal (read-from-physical-memory p-addrs (xw :rflags nil val x86))
        (read-from-physical-memory p-addrs x86)))

Theorem: read-from-physical-memory-xw-not-mem

(defthm read-from-physical-memory-xw-not-mem
 (implies
   (not (equal fld :mem))
   (equal (read-from-physical-memory p-addrs (xw fld index val x86))
          (read-from-physical-memory p-addrs x86))))

Function: rb

(defun rb (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 :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'rb))
    (declare (ignorable __function__))
    (if (app-view x86)
        (rb-1 n addr r-x x86)
      (b* (((mv flgs p-addrs x86)
            (las-to-pas n addr r-x x86))
           ((when flgs) (mv flgs 0 x86))
           (val (read-from-physical-memory p-addrs x86)))
        (mv nil val x86)))))

Theorem: integerp-of-rb.val

(defthm integerp-of-rb.val
  (b* (((mv ?flg ?val ?new-x86)
        (rb n addr r-x x86)))
    (integerp val))
  :rule-classes :type-prescription)

Theorem: x86p-of-rb.new-x86

(defthm x86p-of-rb.new-x86
  (implies (x86p x86)
           (b* (((mv ?flg ?val ?new-x86)
                 (rb n addr r-x x86)))
             (x86p new-x86)))
  :rule-classes :rewrite)

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

(defthm natp-of-mv-nth-1-rb
  (b* (((mv ?flg ?val ?new-x86)
        (rb n addr r-x x86)))
    (natp val))
  :rule-classes :type-prescription)

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

(defthm rb-no-reads-when-zp-n
  (b* (((mv ?flg ?val ?new-x86)
        (rb n addr r-x x86)))
    (implies (zp n) (equal val 0))))

Theorem: rb-is-rb-1-for-app-view

(defthm rb-is-rb-1-for-app-view
  (implies (app-view x86)
           (equal (rb n addr r-x x86)
                  (rb-1 n addr r-x x86))))

Theorem: rb-returns-no-error-app-view

(defthm rb-returns-no-error-app-view
  (implies (and (app-view x86)
                (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr)))
           (equal (mv-nth 0 (rb n addr r-x x86))
                  nil)))

Theorem: rb-returns-x86-app-view

(defthm rb-returns-x86-app-view
  (implies (app-view x86)
           (equal (mv-nth 2 (rb n addr r-x x86))
                  x86)))

Theorem: size-of-rb

(defthm size-of-rb
 (implies (and (equal m (ash n 3)) (natp n))
          (unsigned-byte-p m (mv-nth 1 (rb n addr r-x x86))))
 :rule-classes
 (:rewrite
  (:linear
      :corollary (implies (and (equal m (ash n 3)) (natp n))
                          (and (<= 0 (mv-nth 1 (rb n addr r-x x86)))
                               (< (mv-nth 1 (rb n addr r-x x86))
                                  (expt 2 m))))
      :hints (("Goal" :in-theory (e/d* nil (rb)))))))

Theorem: size-of-rb-in-app-view

(defthm size-of-rb-in-app-view
 (implies (and (app-view x86) (natp n))
          (unsigned-byte-p (ash n 3)
                           (mv-nth 1 (rb n addr r-x x86))))
 :rule-classes
 (:rewrite
  (:linear
      :corollary (implies (and (app-view x86) (natp n))
                          (and (<= 0 (mv-nth 1 (rb n addr r-x x86)))
                               (< (mv-nth 1 (rb n addr r-x x86))
                                  (expt 2 (ash n 3)))))
      :hints (("Goal" :in-theory (e/d* nil (rb)))))))

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

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

Theorem: 64-bit-modep-of-rb

(defthm 64-bit-modep-of-rb
  (equal (64-bit-modep (mv-nth 2 (rb n addr r-x x86)))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-rb

(defthm x86-operation-mode-of-rb
  (equal (x86-operation-mode (mv-nth 2 (rb n addr r-x x86)))
         (x86-operation-mode x86)))

Function: wb-1

(defun wb-1 (n addr w value x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :w) w))
  (declare (xargs :guard (and (natp n)
                              (integerp addr)
                              (natp value))))
  (declare (xargs :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'wb-1))
    (declare (ignorable __function__))
    (if (zp n)
        (mv nil x86)
      (b* (((unless (canonical-address-p addr))
            (mv t x86))
           ((mv flg0 x86)
            (wvm08 addr (loghead 8 value) x86))
           ((when flg0) (mv flg0 x86))
           ((mv rest-flg x86)
            (wb-1 (1- n)
                  (1+ addr)
                  w (logtail 8 value)
                  x86)))
        (mv rest-flg x86)))))

Theorem: wb-1-returns-x86p

(defthm wb-1-returns-x86p
  (implies (x86p x86)
           (x86p (mv-nth 1 (wb-1 n addr w value x86)))))

Theorem: wb-1-returns-no-error-app-view

(defthm wb-1-returns-no-error-app-view
  (implies (and (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr))
                (app-view x86))
           (equal (mv-nth 0 (wb-1 n addr w value x86))
                  nil)))

Function: write-to-physical-memory

(defun write-to-physical-memory (p-addrs value x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (and (physical-address-listp p-addrs)
                              (natp value))))
  (declare (xargs :guard (not (app-view x86))))
  (let ((__function__ 'write-to-physical-memory))
    (declare (ignorable __function__))
    (if (endp p-addrs)
        x86
      (b* ((addr0 (car p-addrs))
           (byte0 (loghead 8 value))
           (x86 (!memi addr0 byte0 x86)))
        (write-to-physical-memory (cdr p-addrs)
                                  (logtail 8 value)
                                  x86)))))

Theorem: x86p-write-to-physical-memory

(defthm x86p-write-to-physical-memory
  (implies (and (x86p x86)
                (physical-address-listp p-addrs))
           (x86p (write-to-physical-memory p-addrs value x86))))

Theorem: xr-not-mem-write-to-physical-memory

(defthm xr-not-mem-write-to-physical-memory
  (implies (not (equal fld :mem))
           (equal (xr fld index
                      (write-to-physical-memory p-addrs bytes x86))
                  (xr fld index x86))))

Theorem: write-to-physical-memory-xw-in-sys-view

(defthm write-to-physical-memory-xw-in-sys-view
 (implies
  (not (equal fld :mem))
  (equal
   (write-to-physical-memory p-addrs bytes (xw fld index value x86))
   (xw fld index value
       (write-to-physical-memory p-addrs bytes x86)))))

Theorem: 64-bit-modep-of-write-to-physical-memory

(defthm 64-bit-modep-of-write-to-physical-memory
  (equal (64-bit-modep (write-to-physical-memory p-addrs value x86))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-write-to-physical-memory

(defthm x86-operation-mode-of-write-to-physical-memory
 (equal
   (x86-operation-mode (write-to-physical-memory p-addrs value x86))
   (x86-operation-mode x86)))

Function: wb

(defun wb (n addr w value x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :w) w))
  (declare (xargs :guard (and (natp n)
                              (integerp addr)
                              (natp value))))
  (declare (xargs :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'wb))
    (declare (ignorable __function__))
    (if (app-view x86)
        (wb-1 n addr w value x86)
      (b* (((mv flgs p-addrs x86)
            (las-to-pas n addr :w x86))
           ((when flgs) (mv flgs x86))
           (x86 (write-to-physical-memory p-addrs value x86)))
        (mv nil x86)))))

Theorem: wb-no-writes-when-zp-n

(defthm wb-no-writes-when-zp-n
  (equal (mv-nth 1 (wb 0 addr val w x86))
         x86))

Theorem: wb-is-wb-1-for-app-view

(defthm wb-is-wb-1-for-app-view
  (implies (app-view x86)
           (equal (wb n addr w value x86)
                  (wb-1 n addr w value x86))))

Theorem: x86p-of-wb

(defthm x86p-of-wb
  (implies (x86p x86)
           (x86p (mv-nth 1 (wb n addr w value x86)))))

Theorem: wb-returns-no-error-app-view

(defthm wb-returns-no-error-app-view
  (implies (and (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr))
                (app-view x86))
           (equal (mv-nth 0 (wb n addr w value x86))
                  nil)))

Theorem: wb-by-wb-1-for-app-view-induction-rule

(defthm wb-by-wb-1-for-app-view-induction-rule
  t
  :rule-classes ((:induction :pattern (wb n addr w value x86)
                             :condition (app-view x86)
                             :scheme (wb-1 n addr w value x86))))

Theorem: xr-rb-state-in-app-view

(defthm xr-rb-state-in-app-view
  (implies (app-view x86)
           (equal (xr fld
                      index (mv-nth 2 (rb n addr r-x x86)))
                  (xr fld index x86))))

Theorem: rb-xw-values-in-app-view

(defthm rb-xw-values-in-app-view
  (implies
       (and (app-view x86)
            (not (equal fld :mem))
            (not (equal fld :app-view)))
       (and (equal (mv-nth 0
                           (rb n addr r-x (xw fld index value x86)))
                   (mv-nth 0 (rb n addr r-x x86)))
            (equal (mv-nth 1
                           (rb n addr r-x (xw fld index value x86)))
                   (mv-nth 1 (rb n addr r-x x86))))))

Theorem: rb-xw-state-in-app-view

(defthm rb-xw-state-in-app-view
  (implies (and (app-view x86)
                (not (equal fld :app-view)))
           (equal (mv-nth 2
                          (rb n addr r-x (xw fld index value x86)))
                  (xw fld index
                      value (mv-nth 2 (rb n addr r-x x86))))))

Theorem: xr-rb-1-state-in-sys-view

(defthm xr-rb-1-state-in-sys-view
  (implies (and (not (app-view x86))
                (not (equal fld :mem))
                (not (equal fld :fault)))
           (equal (xr fld
                      index (mv-nth 2 (rb-1 n addr r-x x86)))
                  (xr fld index x86))))

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

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

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

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

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

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

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

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

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

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

Theorem: xr-enable-peripherals-mv-nth-2-rb

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

Theorem: xr-handle-exceptions-mv-nth-2-rb

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: xr-inhibit-interrupts-one-instruction-mv-nth-2-rb

(defthm xr-inhibit-interrupts-one-instruction-mv-nth-2-rb
  (equal (xr :inhibit-interrupts-one-instruction
             index (mv-nth 2 (rb n addr r-x x86)))
         (xr :inhibit-interrupts-one-instruction
             index x86)))

Theorem: xr-time-stamp-counter-mv-nth-2-rb

(defthm xr-time-stamp-counter-mv-nth-2-rb
  (equal (xr :time-stamp-counter
             index (mv-nth 2 (rb n addr r-x x86)))
         (xr :time-stamp-counter index x86)))

Theorem: xr-last-clock-event-mv-nth-2-rb

(defthm xr-last-clock-event-mv-nth-2-rb
  (equal (xr :last-clock-event
             index (mv-nth 2 (rb n addr r-x x86)))
         (xr :last-clock-event index x86)))

Theorem: xr-implicit-supervisor-access-mv-nth-2-rb

(defthm xr-implicit-supervisor-access-mv-nth-2-rb
  (equal (xr :implicit-supervisor-access
             index (mv-nth 2 (rb n addr r-x x86)))
         (xr :implicit-supervisor-access index x86)))

Theorem: xr-tty-in-mv-nth-2-rb

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

Theorem: xr-tty-out-mv-nth-2-rb

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

Theorem: rb-1-xw-values-in-sys-view

(defthm rb-1-xw-values-in-sys-view
 (implies
     (and (not (app-view x86))
          (not (equal fld :mem))
          (not (equal fld :rflags))
          (not (equal fld :ctr))
          (not (equal fld :seg-visible))
          (not (equal fld :msr))
          (not (equal fld :fault))
          (not (equal fld :app-view))
          (not (equal fld :marking-view)))
     (and (equal (mv-nth 0
                         (rb-1 n addr r-x (xw fld index value x86)))
                 (mv-nth 0 (rb-1 n addr r-x x86)))
          (equal (mv-nth 1
                         (rb-1 n addr r-x (xw fld index value x86)))
                 (mv-nth 1 (rb-1 n addr r-x x86))))))

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

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

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

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

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

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

Theorem: mv-nth-0-rb-xw-enable-peripherals

(defthm mv-nth-0-rb-xw-enable-peripherals
  (equal (mv-nth 0
                 (rb n addr r-x
                     (xw :enable-peripherals index val x86)))
         (mv-nth 0 (rb n addr r-x x86))))

Theorem: mv-nth-0-rb-xw-handle-exceptions

(defthm mv-nth-0-rb-xw-handle-exceptions
  (equal (mv-nth 0
                 (rb n addr r-x
                     (xw :handle-exceptions index val x86)))
         (mv-nth 0 (rb n addr r-x x86))))

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

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

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

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

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

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

Theorem: mv-nth-0-rb-xw-seg-hidden-base

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

Theorem: mv-nth-0-rb-xw-seg-hidden-limit

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

Theorem: mv-nth-0-rb-xw-seg-hidden-attr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: mv-nth-0-rb-xw-inhibit-interrupts-one-instruction

(defthm mv-nth-0-rb-xw-inhibit-interrupts-one-instruction
  (equal (mv-nth 0
                 (rb n addr r-x
                     (xw :inhibit-interrupts-one-instruction
                         index val x86)))
         (mv-nth 0 (rb n addr r-x x86))))

Theorem: mv-nth-0-rb-xw-time-stamp-counter

(defthm mv-nth-0-rb-xw-time-stamp-counter
  (equal (mv-nth 0
                 (rb n addr r-x
                     (xw :time-stamp-counter index val x86)))
         (mv-nth 0 (rb n addr r-x x86))))

Theorem: mv-nth-0-rb-xw-last-clock-event

(defthm mv-nth-0-rb-xw-last-clock-event
  (equal (mv-nth 0
                 (rb n addr r-x
                     (xw :last-clock-event index val x86)))
         (mv-nth 0 (rb n addr r-x x86))))

Theorem: mv-nth-0-rb-xw-tty-in

(defthm mv-nth-0-rb-xw-tty-in
  (equal (mv-nth 0
                 (rb n addr r-x (xw :tty-in index val x86)))
         (mv-nth 0 (rb n addr r-x x86))))

Theorem: mv-nth-0-rb-xw-tty-out

(defthm mv-nth-0-rb-xw-tty-out
  (equal (mv-nth 0
                 (rb n addr r-x (xw :tty-out index val x86)))
         (mv-nth 0 (rb n addr r-x x86))))

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

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

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

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

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

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

Theorem: mv-nth-1-rb-xw-enable-peripherals

(defthm mv-nth-1-rb-xw-enable-peripherals
  (equal (mv-nth 1
                 (rb n addr r-x
                     (xw :enable-peripherals index val x86)))
         (mv-nth 1 (rb n addr r-x x86))))

Theorem: mv-nth-1-rb-xw-handle-exceptions

(defthm mv-nth-1-rb-xw-handle-exceptions
  (equal (mv-nth 1
                 (rb n addr r-x
                     (xw :handle-exceptions index val x86)))
         (mv-nth 1 (rb n addr r-x x86))))

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

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

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

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

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

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

Theorem: mv-nth-1-rb-xw-seg-hidden-base

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

Theorem: mv-nth-1-rb-xw-seg-hidden-limit

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

Theorem: mv-nth-1-rb-xw-seg-hidden-attr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: mv-nth-1-rb-xw-inhibit-interrupts-one-instruction

(defthm mv-nth-1-rb-xw-inhibit-interrupts-one-instruction
  (equal (mv-nth 1
                 (rb n addr r-x
                     (xw :inhibit-interrupts-one-instruction
                         index val x86)))
         (mv-nth 1 (rb n addr r-x x86))))

Theorem: mv-nth-1-rb-xw-time-stamp-counter

(defthm mv-nth-1-rb-xw-time-stamp-counter
  (equal (mv-nth 1
                 (rb n addr r-x
                     (xw :time-stamp-counter index val x86)))
         (mv-nth 1 (rb n addr r-x x86))))

Theorem: mv-nth-1-rb-xw-last-clock-event

(defthm mv-nth-1-rb-xw-last-clock-event
  (equal (mv-nth 1
                 (rb n addr r-x
                     (xw :last-clock-event index val x86)))
         (mv-nth 1 (rb n addr r-x x86))))

Theorem: mv-nth-1-rb-xw-tty-in

(defthm mv-nth-1-rb-xw-tty-in
  (equal (mv-nth 1
                 (rb n addr r-x (xw :tty-in index val x86)))
         (mv-nth 1 (rb n addr r-x x86))))

Theorem: mv-nth-1-rb-xw-tty-out

(defthm mv-nth-1-rb-xw-tty-out
  (equal (mv-nth 1
                 (rb n addr r-x (xw :tty-out index val x86)))
         (mv-nth 1 (rb n addr r-x x86))))

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

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

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

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

Theorem: rb-1-xw-state-in-sys-view

(defthm rb-1-xw-state-in-sys-view
 (implies (and (not (app-view x86))
               (not (equal fld :mem))
               (not (equal fld :rflags))
               (not (equal fld :ctr))
               (not (equal fld :seg-visible))
               (not (equal fld :msr))
               (not (equal fld :fault))
               (not (equal fld :app-view))
               (not (equal fld :marking-view)))
          (equal (mv-nth 2
                         (rb-1 n addr r-x (xw fld index value x86)))
                 (xw fld index value
                     (mv-nth 2 (rb-1 n addr r-x x86))))))

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

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

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

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

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

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

Theorem: mv-nth-2-rb-xw-enable-peripherals

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

Theorem: mv-nth-2-rb-xw-handle-exceptions

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

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

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

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

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

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

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

Theorem: mv-nth-2-rb-xw-seg-hidden-base

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

Theorem: mv-nth-2-rb-xw-seg-hidden-limit

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

Theorem: mv-nth-2-rb-xw-seg-hidden-attr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: mv-nth-2-rb-xw-inhibit-interrupts-one-instruction

(defthm mv-nth-2-rb-xw-inhibit-interrupts-one-instruction
  (equal (mv-nth 2
                 (rb n addr r-x
                     (xw :inhibit-interrupts-one-instruction
                         index val x86)))
         (xw :inhibit-interrupts-one-instruction
             index
             val (mv-nth 2 (rb n addr r-x x86)))))

Theorem: mv-nth-2-rb-xw-time-stamp-counter

(defthm mv-nth-2-rb-xw-time-stamp-counter
  (equal (mv-nth 2
                 (rb n addr r-x
                     (xw :time-stamp-counter index val x86)))
         (xw :time-stamp-counter index
             val (mv-nth 2 (rb n addr r-x x86)))))

Theorem: mv-nth-2-rb-xw-last-clock-event

(defthm mv-nth-2-rb-xw-last-clock-event
  (equal (mv-nth 2
                 (rb n addr r-x
                     (xw :last-clock-event index val x86)))
         (xw :last-clock-event index
             val (mv-nth 2 (rb n addr r-x x86)))))

Theorem: mv-nth-2-rb-xw-tty-in

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

Theorem: mv-nth-2-rb-xw-tty-out

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

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

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

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

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

Theorem: xr-wb-1-in-app-view

(defthm xr-wb-1-in-app-view
  (implies (and (app-view x86)
                (not (equal fld :mem)))
           (equal (xr fld index
                      (mv-nth 1 (wb-1 n addr w value x86)))
                  (xr fld index x86))))

Theorem: xr-wb-in-app-view

(defthm xr-wb-in-app-view
  (implies (and (app-view x86)
                (not (equal fld :mem)))
           (equal (xr fld index
                      (mv-nth 1 (wb n addr w value x86)))
                  (xr fld index x86))))

Theorem: wb-1-xw-in-app-view

(defthm wb-1-xw-in-app-view
 (implies
   (and (app-view x86)
        (not (equal fld :mem))
        (not (equal fld :app-view)))
   (and (equal (mv-nth 0
                       (wb-1 n addr w val (xw fld index value x86)))
               (mv-nth 0 (wb-1 n addr w val x86)))
        (equal (mv-nth 1
                       (wb-1 n addr w val (xw fld index value x86)))
               (xw fld index value
                   (mv-nth 1 (wb-1 n addr w val x86)))))))

Theorem: wb-xw-in-app-view

(defthm wb-xw-in-app-view
 (implies
     (and (app-view x86)
          (not (equal fld :mem))
          (not (equal fld :app-view)))
     (and (equal (mv-nth 0
                         (wb n addr w val (xw fld index value x86)))
                 (mv-nth 0 (wb n addr w val x86)))
          (equal (mv-nth 1
                         (wb n addr w val (xw fld index value x86)))
                 (xw fld index value
                     (mv-nth 1 (wb n addr w val x86)))))))

Theorem: xr-ms-mv-nth-1-wb

(defthm xr-ms-mv-nth-1-wb
  (equal (xr :ms index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :ms index x86)))

Theorem: xr-env-mv-nth-1-wb

(defthm xr-env-mv-nth-1-wb
  (equal (xr :env index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :env index x86)))

Theorem: xr-undef-mv-nth-1-wb

(defthm xr-undef-mv-nth-1-wb
  (equal (xr :undef index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :undef index x86)))

Theorem: xr-app-view-mv-nth-1-wb

(defthm xr-app-view-mv-nth-1-wb
  (equal (xr :app-view index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :app-view index x86)))

Theorem: xr-marking-view-mv-nth-1-wb

(defthm xr-marking-view-mv-nth-1-wb
  (equal (xr :marking-view index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :marking-view index x86)))

Theorem: xr-enable-peripherals-mv-nth-1-wb

(defthm xr-enable-peripherals-mv-nth-1-wb
  (equal (xr :enable-peripherals index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :enable-peripherals index x86)))

Theorem: xr-handle-exceptions-mv-nth-1-wb

(defthm xr-handle-exceptions-mv-nth-1-wb
  (equal (xr :handle-exceptions index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :handle-exceptions index x86)))

Theorem: xr-os-info-mv-nth-1-wb

(defthm xr-os-info-mv-nth-1-wb
  (equal (xr :os-info index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :os-info index x86)))

Theorem: xr-rgf-mv-nth-1-wb

(defthm xr-rgf-mv-nth-1-wb
  (equal (xr :rgf index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :rgf index x86)))

Theorem: xr-rip-mv-nth-1-wb

(defthm xr-rip-mv-nth-1-wb
  (equal (xr :rip index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :rip index x86)))

Theorem: xr-rflags-mv-nth-1-wb

(defthm xr-rflags-mv-nth-1-wb
  (equal (xr :rflags index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :rflags index x86)))

Theorem: xr-seg-visible-mv-nth-1-wb

(defthm xr-seg-visible-mv-nth-1-wb
  (equal (xr :seg-visible index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :seg-visible index x86)))

Theorem: xr-seg-hidden-base-mv-nth-1-wb

(defthm xr-seg-hidden-base-mv-nth-1-wb
  (equal (xr :seg-hidden-base index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :seg-hidden-base index x86)))

Theorem: xr-seg-hidden-limit-mv-nth-1-wb

(defthm xr-seg-hidden-limit-mv-nth-1-wb
  (equal (xr :seg-hidden-limit index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :seg-hidden-limit index x86)))

Theorem: xr-seg-hidden-attr-mv-nth-1-wb

(defthm xr-seg-hidden-attr-mv-nth-1-wb
  (equal (xr :seg-hidden-attr index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :seg-hidden-attr index x86)))

Theorem: xr-str-mv-nth-1-wb

(defthm xr-str-mv-nth-1-wb
  (equal (xr :str index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :str index x86)))

Theorem: xr-ssr-visible-mv-nth-1-wb

(defthm xr-ssr-visible-mv-nth-1-wb
  (equal (xr :ssr-visible index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :ssr-visible index x86)))

Theorem: xr-ssr-hidden-base-mv-nth-1-wb

(defthm xr-ssr-hidden-base-mv-nth-1-wb
  (equal (xr :ssr-hidden-base index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :ssr-hidden-base index x86)))

Theorem: xr-ssr-hidden-limit-mv-nth-1-wb

(defthm xr-ssr-hidden-limit-mv-nth-1-wb
  (equal (xr :ssr-hidden-limit index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :ssr-hidden-limit index x86)))

Theorem: xr-ssr-hidden-attr-mv-nth-1-wb

(defthm xr-ssr-hidden-attr-mv-nth-1-wb
  (equal (xr :ssr-hidden-attr index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :ssr-hidden-attr index x86)))

Theorem: xr-ctr-mv-nth-1-wb

(defthm xr-ctr-mv-nth-1-wb
  (equal (xr :ctr index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :ctr index x86)))

Theorem: xr-dbg-mv-nth-1-wb

(defthm xr-dbg-mv-nth-1-wb
  (equal (xr :dbg index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :dbg index x86)))

Theorem: xr-fp-data-mv-nth-1-wb

(defthm xr-fp-data-mv-nth-1-wb
  (equal (xr :fp-data index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :fp-data index x86)))

Theorem: xr-fp-ctrl-mv-nth-1-wb

(defthm xr-fp-ctrl-mv-nth-1-wb
  (equal (xr :fp-ctrl index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :fp-ctrl index x86)))

Theorem: xr-fp-status-mv-nth-1-wb

(defthm xr-fp-status-mv-nth-1-wb
  (equal (xr :fp-status index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :fp-status index x86)))

Theorem: xr-fp-tag-mv-nth-1-wb

(defthm xr-fp-tag-mv-nth-1-wb
  (equal (xr :fp-tag index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :fp-tag index x86)))

Theorem: xr-fp-last-inst-mv-nth-1-wb

(defthm xr-fp-last-inst-mv-nth-1-wb
  (equal (xr :fp-last-inst index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :fp-last-inst index x86)))

Theorem: xr-fp-last-data-mv-nth-1-wb

(defthm xr-fp-last-data-mv-nth-1-wb
  (equal (xr :fp-last-data index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :fp-last-data index x86)))

Theorem: xr-fp-opcode-mv-nth-1-wb

(defthm xr-fp-opcode-mv-nth-1-wb
  (equal (xr :fp-opcode index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :fp-opcode index x86)))

Theorem: xr-mxcsr-mv-nth-1-wb

(defthm xr-mxcsr-mv-nth-1-wb
  (equal (xr :mxcsr index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :mxcsr index x86)))

Theorem: xr-opmsk-mv-nth-1-wb

(defthm xr-opmsk-mv-nth-1-wb
  (equal (xr :opmsk index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :opmsk index x86)))

Theorem: xr-zmm-mv-nth-1-wb

(defthm xr-zmm-mv-nth-1-wb
  (equal (xr :zmm index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :zmm index x86)))

Theorem: xr-msr-mv-nth-1-wb

(defthm xr-msr-mv-nth-1-wb
  (equal (xr :msr index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :msr index x86)))

Theorem: xr-inhibit-interrupts-one-instruction-mv-nth-1-wb

(defthm xr-inhibit-interrupts-one-instruction-mv-nth-1-wb
  (equal (xr :inhibit-interrupts-one-instruction
             index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :inhibit-interrupts-one-instruction
             index x86)))

Theorem: xr-time-stamp-counter-mv-nth-1-wb

(defthm xr-time-stamp-counter-mv-nth-1-wb
  (equal (xr :time-stamp-counter index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :time-stamp-counter index x86)))

Theorem: xr-last-clock-event-mv-nth-1-wb

(defthm xr-last-clock-event-mv-nth-1-wb
  (equal (xr :last-clock-event index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :last-clock-event index x86)))

Theorem: xr-implicit-supervisor-access-mv-nth-1-wb

(defthm xr-implicit-supervisor-access-mv-nth-1-wb
  (equal (xr :implicit-supervisor-access index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :implicit-supervisor-access index x86)))

Theorem: xr-tty-in-mv-nth-1-wb

(defthm xr-tty-in-mv-nth-1-wb
  (equal (xr :tty-in index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :tty-in index x86)))

Theorem: xr-tty-out-mv-nth-1-wb

(defthm xr-tty-out-mv-nth-1-wb
  (equal (xr :tty-out index
             (mv-nth 1 (wb n addr w value x86)))
         (xr :tty-out index x86)))

Theorem: xr-fault-wb-in-system-level-marking-view

(defthm xr-fault-wb-in-system-level-marking-view
  (implies (not (mv-nth 0
                        (las-to-pas n addr
                                    :w (double-rewrite x86))))
           (equal (xr :fault
                      nil (mv-nth 1 (wb n addr w val x86)))
                  (xr :fault nil x86))))

Theorem: 64-bit-modep-of-mv-nth-1-of-wb

(defthm 64-bit-modep-of-mv-nth-1-of-wb
  (equal (64-bit-modep (mv-nth 1 (wb n addr w value x86)))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-mv-nth-1-of-wb

(defthm x86-operation-mode-of-mv-nth-1-of-wb
  (equal (x86-operation-mode (mv-nth 1 (wb n addr w value x86)))
         (x86-operation-mode x86)))

Theorem: mv-nth-0-wb-xw-ms

(defthm mv-nth-0-wb-xw-ms
  (equal (mv-nth 0
                 (wb n addr w value (xw :ms index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-env

(defthm mv-nth-0-wb-xw-env
  (equal (mv-nth 0
                 (wb n addr w value (xw :env index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-undef

(defthm mv-nth-0-wb-xw-undef
  (equal (mv-nth 0
                 (wb n
                     addr w value (xw :undef index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-enable-peripherals

(defthm mv-nth-0-wb-xw-enable-peripherals
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :enable-peripherals index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-handle-exceptions

(defthm mv-nth-0-wb-xw-handle-exceptions
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :handle-exceptions index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-os-info

(defthm mv-nth-0-wb-xw-os-info
  (equal (mv-nth 0
                 (wb n addr
                     w value (xw :os-info index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-rgf

(defthm mv-nth-0-wb-xw-rgf
  (equal (mv-nth 0
                 (wb n addr w value (xw :rgf index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-rip

(defthm mv-nth-0-wb-xw-rip
  (equal (mv-nth 0
                 (wb n addr w value (xw :rip index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-seg-hidden-base

(defthm mv-nth-0-wb-xw-seg-hidden-base
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :seg-hidden-base index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-seg-hidden-limit

(defthm mv-nth-0-wb-xw-seg-hidden-limit
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :seg-hidden-limit index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-seg-hidden-attr

(defthm mv-nth-0-wb-xw-seg-hidden-attr
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :seg-hidden-attr index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-str

(defthm mv-nth-0-wb-xw-str
  (equal (mv-nth 0
                 (wb n addr w value (xw :str index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-ssr-visible

(defthm mv-nth-0-wb-xw-ssr-visible
  (equal (mv-nth 0
                 (wb n addr w
                     value (xw :ssr-visible index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-ssr-hidden-base

(defthm mv-nth-0-wb-xw-ssr-hidden-base
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :ssr-hidden-base index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-ssr-hidden-limit

(defthm mv-nth-0-wb-xw-ssr-hidden-limit
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :ssr-hidden-limit index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-ssr-hidden-attr

(defthm mv-nth-0-wb-xw-ssr-hidden-attr
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :ssr-hidden-attr index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-dbg

(defthm mv-nth-0-wb-xw-dbg
  (equal (mv-nth 0
                 (wb n addr w value (xw :dbg index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-fp-data

(defthm mv-nth-0-wb-xw-fp-data
  (equal (mv-nth 0
                 (wb n addr
                     w value (xw :fp-data index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-fp-ctrl

(defthm mv-nth-0-wb-xw-fp-ctrl
  (equal (mv-nth 0
                 (wb n addr
                     w value (xw :fp-ctrl index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-fp-status

(defthm mv-nth-0-wb-xw-fp-status
  (equal (mv-nth 0
                 (wb n addr
                     w value (xw :fp-status index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-fp-tag

(defthm mv-nth-0-wb-xw-fp-tag
  (equal (mv-nth 0
                 (wb n addr
                     w value (xw :fp-tag index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-fp-last-inst

(defthm mv-nth-0-wb-xw-fp-last-inst
  (equal (mv-nth 0
                 (wb n addr w
                     value (xw :fp-last-inst index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-fp-last-data

(defthm mv-nth-0-wb-xw-fp-last-data
  (equal (mv-nth 0
                 (wb n addr w
                     value (xw :fp-last-data index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-fp-opcode

(defthm mv-nth-0-wb-xw-fp-opcode
  (equal (mv-nth 0
                 (wb n addr
                     w value (xw :fp-opcode index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-mxcsr

(defthm mv-nth-0-wb-xw-mxcsr
  (equal (mv-nth 0
                 (wb n
                     addr w value (xw :mxcsr index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-opmsk

(defthm mv-nth-0-wb-xw-opmsk
  (equal (mv-nth 0
                 (wb n
                     addr w value (xw :opmsk index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-zmm

(defthm mv-nth-0-wb-xw-zmm
  (equal (mv-nth 0
                 (wb n addr w value (xw :zmm index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-inhibit-interrupts-one-instruction

(defthm mv-nth-0-wb-xw-inhibit-interrupts-one-instruction
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :inhibit-interrupts-one-instruction
                         index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-time-stamp-counter

(defthm mv-nth-0-wb-xw-time-stamp-counter
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :time-stamp-counter index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-last-clock-event

(defthm mv-nth-0-wb-xw-last-clock-event
  (equal (mv-nth 0
                 (wb n addr w value
                     (xw :last-clock-event index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-tty-in

(defthm mv-nth-0-wb-xw-tty-in
  (equal (mv-nth 0
                 (wb n addr
                     w value (xw :tty-in index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-0-wb-xw-tty-out

(defthm mv-nth-0-wb-xw-tty-out
  (equal (mv-nth 0
                 (wb n addr
                     w value (xw :tty-out index val x86)))
         (mv-nth 0 (wb n addr w value x86))))

Theorem: mv-nth-1-wb-xw-ms

(defthm mv-nth-1-wb-xw-ms
  (equal (mv-nth 1
                 (wb n addr w value (xw :ms index val x86)))
         (xw :ms index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-env

(defthm mv-nth-1-wb-xw-env
  (equal (mv-nth 1
                 (wb n addr w value (xw :env index val x86)))
         (xw :env index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-undef

(defthm mv-nth-1-wb-xw-undef
  (equal (mv-nth 1
                 (wb n
                     addr w value (xw :undef index val x86)))
         (xw :undef index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-enable-peripherals

(defthm mv-nth-1-wb-xw-enable-peripherals
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :enable-peripherals index val x86)))
         (xw :enable-peripherals index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-handle-exceptions

(defthm mv-nth-1-wb-xw-handle-exceptions
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :handle-exceptions index val x86)))
         (xw :handle-exceptions index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-os-info

(defthm mv-nth-1-wb-xw-os-info
  (equal (mv-nth 1
                 (wb n addr
                     w value (xw :os-info index val x86)))
         (xw :os-info index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-rgf

(defthm mv-nth-1-wb-xw-rgf
  (equal (mv-nth 1
                 (wb n addr w value (xw :rgf index val x86)))
         (xw :rgf index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-rip

(defthm mv-nth-1-wb-xw-rip
  (equal (mv-nth 1
                 (wb n addr w value (xw :rip index val x86)))
         (xw :rip index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-seg-hidden-base

(defthm mv-nth-1-wb-xw-seg-hidden-base
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :seg-hidden-base index val x86)))
         (xw :seg-hidden-base index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-seg-hidden-limit

(defthm mv-nth-1-wb-xw-seg-hidden-limit
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :seg-hidden-limit index val x86)))
         (xw :seg-hidden-limit index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-seg-hidden-attr

(defthm mv-nth-1-wb-xw-seg-hidden-attr
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :seg-hidden-attr index val x86)))
         (xw :seg-hidden-attr index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-str

(defthm mv-nth-1-wb-xw-str
  (equal (mv-nth 1
                 (wb n addr w value (xw :str index val x86)))
         (xw :str index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-ssr-visible

(defthm mv-nth-1-wb-xw-ssr-visible
  (equal (mv-nth 1
                 (wb n addr w
                     value (xw :ssr-visible index val x86)))
         (xw :ssr-visible index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-ssr-hidden-base

(defthm mv-nth-1-wb-xw-ssr-hidden-base
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :ssr-hidden-base index val x86)))
         (xw :ssr-hidden-base index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-ssr-hidden-limit

(defthm mv-nth-1-wb-xw-ssr-hidden-limit
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :ssr-hidden-limit index val x86)))
         (xw :ssr-hidden-limit index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-ssr-hidden-attr

(defthm mv-nth-1-wb-xw-ssr-hidden-attr
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :ssr-hidden-attr index val x86)))
         (xw :ssr-hidden-attr index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-dbg

(defthm mv-nth-1-wb-xw-dbg
  (equal (mv-nth 1
                 (wb n addr w value (xw :dbg index val x86)))
         (xw :dbg index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-fp-data

(defthm mv-nth-1-wb-xw-fp-data
  (equal (mv-nth 1
                 (wb n addr
                     w value (xw :fp-data index val x86)))
         (xw :fp-data index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-fp-ctrl

(defthm mv-nth-1-wb-xw-fp-ctrl
  (equal (mv-nth 1
                 (wb n addr
                     w value (xw :fp-ctrl index val x86)))
         (xw :fp-ctrl index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-fp-status

(defthm mv-nth-1-wb-xw-fp-status
  (equal (mv-nth 1
                 (wb n addr
                     w value (xw :fp-status index val x86)))
         (xw :fp-status index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-fp-tag

(defthm mv-nth-1-wb-xw-fp-tag
  (equal (mv-nth 1
                 (wb n addr
                     w value (xw :fp-tag index val x86)))
         (xw :fp-tag index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-fp-last-inst

(defthm mv-nth-1-wb-xw-fp-last-inst
  (equal (mv-nth 1
                 (wb n addr w
                     value (xw :fp-last-inst index val x86)))
         (xw :fp-last-inst index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-fp-last-data

(defthm mv-nth-1-wb-xw-fp-last-data
  (equal (mv-nth 1
                 (wb n addr w
                     value (xw :fp-last-data index val x86)))
         (xw :fp-last-data index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-fp-opcode

(defthm mv-nth-1-wb-xw-fp-opcode
  (equal (mv-nth 1
                 (wb n addr
                     w value (xw :fp-opcode index val x86)))
         (xw :fp-opcode index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-mxcsr

(defthm mv-nth-1-wb-xw-mxcsr
  (equal (mv-nth 1
                 (wb n
                     addr w value (xw :mxcsr index val x86)))
         (xw :mxcsr index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-opmsk

(defthm mv-nth-1-wb-xw-opmsk
  (equal (mv-nth 1
                 (wb n
                     addr w value (xw :opmsk index val x86)))
         (xw :opmsk index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-zmm

(defthm mv-nth-1-wb-xw-zmm
  (equal (mv-nth 1
                 (wb n addr w value (xw :zmm index val x86)))
         (xw :zmm index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-inhibit-interrupts-one-instruction

(defthm mv-nth-1-wb-xw-inhibit-interrupts-one-instruction
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :inhibit-interrupts-one-instruction
                         index val x86)))
         (xw :inhibit-interrupts-one-instruction
             index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-time-stamp-counter

(defthm mv-nth-1-wb-xw-time-stamp-counter
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :time-stamp-counter index val x86)))
         (xw :time-stamp-counter index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-last-clock-event

(defthm mv-nth-1-wb-xw-last-clock-event
  (equal (mv-nth 1
                 (wb n addr w value
                     (xw :last-clock-event index val x86)))
         (xw :last-clock-event index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-tty-in

(defthm mv-nth-1-wb-xw-tty-in
  (equal (mv-nth 1
                 (wb n addr
                     w value (xw :tty-in index val x86)))
         (xw :tty-in index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: mv-nth-1-wb-xw-tty-out

(defthm mv-nth-1-wb-xw-tty-out
  (equal (mv-nth 1
                 (wb n addr
                     w value (xw :tty-out index val x86)))
         (xw :tty-out index val
             (mv-nth 1 (wb n addr w value x86)))))

Theorem: wb-xw-rflags-not-ac-in-sys-view

(defthm wb-xw-rflags-not-ac-in-sys-view
 (implies
     (equal (rflagsbits->ac value)
            (rflagsbits->ac (rflags x86)))
     (and (equal (mv-nth 0
                         (wb n
                             addr w val (xw :rflags nil value x86)))
                 (mv-nth 0
                         (wb n addr w val (double-rewrite x86))))
          (equal (mv-nth 1
                         (wb n
                             addr w val (xw :rflags nil value x86)))
                 (xw :rflags nil value
                     (mv-nth 1 (wb n addr w val x86)))))))

Theorem: xr-fault-wb-in-sys-view

(defthm xr-fault-wb-in-sys-view
  (implies (and (not (mv-nth 0 (las-to-pas n addr :w x86)))
                (not (marking-view x86)))
           (equal (xr :fault
                      nil (mv-nth 1 (wb n addr w val x86)))
                  (xr :fault nil x86))))

Theorem: split-rb-in-app-view

(defthm split-rb-in-app-view
  (implies
       (and (canonical-address-p (+ -1 i j lin-addr))
            (canonical-address-p lin-addr)
            (app-view x86)
            (natp i)
            (natp j))
       (equal (mv-nth 1 (rb (+ i j) lin-addr r-x x86))
              (b* ((low (mv-nth 1 (rb i lin-addr r-x x86)))
                   (high (mv-nth 1 (rb j (+ i lin-addr) r-x x86))))
                (logior low (ash high (ash i 3)))))))

Function: split-wb-induction-scheme

(defun split-wb-induction-scheme (i j lin-addr val x86)
 (declare (xargs :non-executable t))
 (prog2$ (acl2::throw-nonexec-error 'split-wb-induction-scheme
                                    (list i j lin-addr val x86))
         (cond ((or (not (natp i))
                    (not (natp j))
                    (zp (+ i j))
                    (zp i)
                    (not (canonical-address-p lin-addr))
                    (not (canonical-address-p (+ -1 i j lin-addr))))
                (mv i j lin-addr val x86))
               (t (split-wb-induction-scheme
                       (1- i)
                       j (1+ lin-addr)
                       (logtail 8 val)
                       (mv-nth 1
                               (wvm08 lin-addr (loghead 8 val)
                                      x86)))))))

Theorem: split-wb-in-app-view

(defthm split-wb-in-app-view
 (implies
  (and (canonical-address-p lin-addr)
       (canonical-address-p (+ -1 i j lin-addr))
       (unsigned-byte-p (ash (+ i j) 3) val)
       (app-view x86)
       (posp i)
       (natp j))
  (equal
    (mv-nth 1 (wb-1 (+ i j) lin-addr w val x86))
    (mv-nth 1
            (wb-1 j (+ i lin-addr)
                  w
                  (loghead (ash j 3)
                           (logtail (ash i 3) val))
                  (mv-nth 1
                          (wb-1 i lin-addr w (loghead (ash i 3) val)
                                x86)))))))

Subtopics

Las-to-pas

Rb

Create-canonical-address-list

Rb-1

Read-from-physical-memory

Write-to-physical-memory

Wb

Wb-1

Canonical-address-listp

Recognizer of a list of canonical addresses