• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
        • Cpuid
        • Linear-memory
          • Reasoning-about-memory-reads-and-writes
          • Rml256
          • Wml512
          • Wml256
          • Rml512
          • 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
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Linear-memory

Rml512

Signature

(rml512 lin-addr r-x x86) → (mv * * x86)

Definitions and Theorems

Theorem: rb-and-rvm512

(defthm rb-and-rvm512
  (implies (and (app-view x86)
                (x86p x86)
                (canonical-address-p lin-addr)
                (canonical-address-p (+ 63 lin-addr)))
           (equal (rvm512 lin-addr x86)
                  (rb 64 lin-addr r-x x86))))

Theorem: unsigned-byte-p-512-of-merge-64-u8s-linear

(defthm unsigned-byte-p-512-of-merge-64-u8s-linear
 (implies
      (and (unsigned-byte-p 8 h31)
           (unsigned-byte-p 8 h30)
           (unsigned-byte-p 8 h29)
           (unsigned-byte-p 8 h28)
           (unsigned-byte-p 8 h27)
           (unsigned-byte-p 8 h26)
           (unsigned-byte-p 8 h25)
           (unsigned-byte-p 8 h24)
           (unsigned-byte-p 8 h23)
           (unsigned-byte-p 8 h22)
           (unsigned-byte-p 8 h21)
           (unsigned-byte-p 8 h20)
           (unsigned-byte-p 8 h19)
           (unsigned-byte-p 8 h18)
           (unsigned-byte-p 8 h17)
           (unsigned-byte-p 8 h16)
           (unsigned-byte-p 8 h15)
           (unsigned-byte-p 8 h14)
           (unsigned-byte-p 8 h13)
           (unsigned-byte-p 8 h12)
           (unsigned-byte-p 8 h11)
           (unsigned-byte-p 8 h10)
           (unsigned-byte-p 8 h9)
           (unsigned-byte-p 8 h8)
           (unsigned-byte-p 8 h7)
           (unsigned-byte-p 8 h6)
           (unsigned-byte-p 8 h5)
           (unsigned-byte-p 8 h4)
           (unsigned-byte-p 8 h3)
           (unsigned-byte-p 8 h2)
           (unsigned-byte-p 8 h1)
           (unsigned-byte-p 8 h0)
           (unsigned-byte-p 8 l31)
           (unsigned-byte-p 8 l30)
           (unsigned-byte-p 8 l29)
           (unsigned-byte-p 8 l28)
           (unsigned-byte-p 8 l27)
           (unsigned-byte-p 8 l26)
           (unsigned-byte-p 8 l25)
           (unsigned-byte-p 8 l24)
           (unsigned-byte-p 8 l23)
           (unsigned-byte-p 8 l22)
           (unsigned-byte-p 8 l21)
           (unsigned-byte-p 8 l20)
           (unsigned-byte-p 8 l19)
           (unsigned-byte-p 8 l18)
           (unsigned-byte-p 8 l17)
           (unsigned-byte-p 8 l16)
           (unsigned-byte-p 8 l15)
           (unsigned-byte-p 8 l14)
           (unsigned-byte-p 8 l13)
           (unsigned-byte-p 8 l12)
           (unsigned-byte-p 8 l11)
           (unsigned-byte-p 8 l10)
           (unsigned-byte-p 8 l9)
           (unsigned-byte-p 8 l8)
           (unsigned-byte-p 8 l7)
           (unsigned-byte-p 8 l6)
           (unsigned-byte-p 8 l5)
           (unsigned-byte-p 8 l4)
           (unsigned-byte-p 8 l3)
           (unsigned-byte-p 8 l2)
           (unsigned-byte-p 8 l1)
           (unsigned-byte-p 8 l0))
      (unsigned-byte-p
           512
           (merge-64-u8s h31 h30 h29 h28 h27 h26 h25 h24 h23 h22
                         h21 h20 h19 h18 h17 h16 h15 h14 h13 h12
                         h11 h10 h9 h8 h7 h6 h5 h4 h3 h2 h1 h0
                         l31 l30 l29 l28 l27 l26 l25 l24 l23 l22
                         l21 l20 l19 l18 l17 l16 l15 l14 l13 l12
                         l11 l10 l9 l8 l7 l6 l5 l4 l3 l2 l1 l0)))
 :rule-classes
 ((:linear
   :corollary
   (implies
    (and (unsigned-byte-p 8 h31)
         (unsigned-byte-p 8 h30)
         (unsigned-byte-p 8 h29)
         (unsigned-byte-p 8 h28)
         (unsigned-byte-p 8 h27)
         (unsigned-byte-p 8 h26)
         (unsigned-byte-p 8 h25)
         (unsigned-byte-p 8 h24)
         (unsigned-byte-p 8 h23)
         (unsigned-byte-p 8 h22)
         (unsigned-byte-p 8 h21)
         (unsigned-byte-p 8 h20)
         (unsigned-byte-p 8 h19)
         (unsigned-byte-p 8 h18)
         (unsigned-byte-p 8 h17)
         (unsigned-byte-p 8 h16)
         (unsigned-byte-p 8 h15)
         (unsigned-byte-p 8 h14)
         (unsigned-byte-p 8 h13)
         (unsigned-byte-p 8 h12)
         (unsigned-byte-p 8 h11)
         (unsigned-byte-p 8 h10)
         (unsigned-byte-p 8 h9)
         (unsigned-byte-p 8 h8)
         (unsigned-byte-p 8 h7)
         (unsigned-byte-p 8 h6)
         (unsigned-byte-p 8 h5)
         (unsigned-byte-p 8 h4)
         (unsigned-byte-p 8 h3)
         (unsigned-byte-p 8 h2)
         (unsigned-byte-p 8 h1)
         (unsigned-byte-p 8 h0)
         (unsigned-byte-p 8 l31)
         (unsigned-byte-p 8 l30)
         (unsigned-byte-p 8 l29)
         (unsigned-byte-p 8 l28)
         (unsigned-byte-p 8 l27)
         (unsigned-byte-p 8 l26)
         (unsigned-byte-p 8 l25)
         (unsigned-byte-p 8 l24)
         (unsigned-byte-p 8 l23)
         (unsigned-byte-p 8 l22)
         (unsigned-byte-p 8 l21)
         (unsigned-byte-p 8 l20)
         (unsigned-byte-p 8 l19)
         (unsigned-byte-p 8 l18)
         (unsigned-byte-p 8 l17)
         (unsigned-byte-p 8 l16)
         (unsigned-byte-p 8 l15)
         (unsigned-byte-p 8 l14)
         (unsigned-byte-p 8 l13)
         (unsigned-byte-p 8 l12)
         (unsigned-byte-p 8 l11)
         (unsigned-byte-p 8 l10)
         (unsigned-byte-p 8 l9)
         (unsigned-byte-p 8 l8)
         (unsigned-byte-p 8 l7)
         (unsigned-byte-p 8 l6)
         (unsigned-byte-p 8 l5)
         (unsigned-byte-p 8 l4)
         (unsigned-byte-p 8 l3)
         (unsigned-byte-p 8 l2)
         (unsigned-byte-p 8 l1)
         (unsigned-byte-p 8 l0))
    (and
     (<= 0
         (merge-64-u8s h31 h30 h29 h28 h27 h26 h25 h24 h23 h22
                       h21 h20 h19 h18 h17 h16 h15 h14 h13 h12
                       h11 h10 h9 h8 h7 h6 h5 h4 h3 h2 h1 h0
                       l31 l30 l29 l28 l27 l26 l25 l24 l23 l22
                       l21 l20 l19 l18 l17 l16 l15 l14 l13 l12
                       l11 l10 l9 l8 l7 l6 l5 l4 l3 l2 l1 l0))
     (<
      (merge-64-u8s h31 h30 h29 h28 h27 h26 h25 h24 h23 h22
                    h21 h20 h19 h18 h17 h16 h15 h14 h13 h12
                    h11 h10 h9 h8 h7 h6 h5 h4 h3 h2 h1 h0
                    l31 l30 l29 l28 l27 l26 l25 l24 l23 l22
                    l21 l20 l19 l18 l17 l16 l15 l14 l13 l12
                    l11 l10 l9 l8 l7 l6 l5 l4 l3 l2 l1 l0)
      13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096)))
   :hints
   (("Goal"
         :in-theory
         (disable bitops::unsigned-byte-p-512-of-merge-64-u8s))))))

Function: rml512

(defun rml512 (lin-addr r-x x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (signed-byte 48) lin-addr)
          (type (member :r :x) r-x))
 (declare (xargs :guard (canonical-address-p lin-addr)))
 (let ((__function__ 'rml512))
  (declare (ignorable __function__))
  (if
   (mbt (canonical-address-p lin-addr))
   (let*
       ((63+lin-addr (the (signed-byte 49)
                          (+ 63 (the (signed-byte 48) lin-addr)))))
    (if
     (mbe :logic (canonical-address-p 63+lin-addr)
          :exec (< (the (signed-byte 49) 63+lin-addr)
                   140737488355328))
     (if (app-view x86)
         (mbe :logic (rb 64 lin-addr r-x x86)
              :exec (rvm512 lin-addr x86))
      (b*
       (((mv flag (the (unsigned-byte 52) p-addr0)
             x86)
         (la-to-pa lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 49) 1+lin-addr)
         (+ 1 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr1)
             x86)
         (la-to-pa 1+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 50) 2+lin-addr)
         (+ 2 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr2)
             x86)
         (la-to-pa 2+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 51) 3+lin-addr)
         (+ 3 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr3)
             x86)
         (la-to-pa 3+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 52) 4+lin-addr)
         (+ 4 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr4)
             x86)
         (la-to-pa 4+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 53) 5+lin-addr)
         (+ 5 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr5)
             x86)
         (la-to-pa 5+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 54) 6+lin-addr)
         (+ 6 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr6)
             x86)
         (la-to-pa 6+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 55) 7+lin-addr)
         (+ 7 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr7)
             x86)
         (la-to-pa 7+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 56) 8+lin-addr)
         (+ 8 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr8)
             x86)
         (la-to-pa 8+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 57) 9+lin-addr)
         (+ 9 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr9)
             x86)
         (la-to-pa 9+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 58) 10+lin-addr)
         (+ 10 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr10)
             x86)
         (la-to-pa 10+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 59) 11+lin-addr)
         (+ 11 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr11)
             x86)
         (la-to-pa 11+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 60) 12+lin-addr)
         (+ 12 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr12)
             x86)
         (la-to-pa 12+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 61) 13+lin-addr)
         (+ 13 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr13)
             x86)
         (la-to-pa 13+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 62) 14+lin-addr)
         (+ 14 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr14)
             x86)
         (la-to-pa 14+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 63) 15+lin-addr)
         (+ 15 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr15)
             x86)
         (la-to-pa 15+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 63) 16+lin-addr)
         (+ 16 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr16)
             x86)
         (la-to-pa 16+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 65) 17+lin-addr)
         (+ 17 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr17)
             x86)
         (la-to-pa 17+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 66) 18+lin-addr)
         (+ 18 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr18)
             x86)
         (la-to-pa 18+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 67) 19+lin-addr)
         (+ 19 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr19)
             x86)
         (la-to-pa 19+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 68) 20+lin-addr)
         (+ 20 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr20)
             x86)
         (la-to-pa 20+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 69) 21+lin-addr)
         (+ 21 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr21)
             x86)
         (la-to-pa 21+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 70) 22+lin-addr)
         (+ 22 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr22)
             x86)
         (la-to-pa 22+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 71) 23+lin-addr)
         (+ 23 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr23)
             x86)
         (la-to-pa 23+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 72) 24+lin-addr)
         (+ 24 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr24)
             x86)
         (la-to-pa 24+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 73) 25+lin-addr)
         (+ 25 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr25)
             x86)
         (la-to-pa 25+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 74) 26+lin-addr)
         (+ 26 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr26)
             x86)
         (la-to-pa 26+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 75) 27+lin-addr)
         (+ 27 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr27)
             x86)
         (la-to-pa 27+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 76) 28+lin-addr)
         (+ 28 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr28)
             x86)
         (la-to-pa 28+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 77) 29+lin-addr)
         (+ 29 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr29)
             x86)
         (la-to-pa 29+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 78) 30+lin-addr)
         (+ 30 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr30)
             x86)
         (la-to-pa 30+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 79) 31+lin-addr)
         (+ 31 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr31)
             x86)
         (la-to-pa 31+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 80) 32+lin-addr)
         (+ 32 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr32)
             x86)
         (la-to-pa 32+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 81) 33+lin-addr)
         (+ 33 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr33)
             x86)
         (la-to-pa 33+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 82) 34+lin-addr)
         (+ 34 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr34)
             x86)
         (la-to-pa 34+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 83) 35+lin-addr)
         (+ 35 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr35)
             x86)
         (la-to-pa 35+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 84) 36+lin-addr)
         (+ 36 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr36)
             x86)
         (la-to-pa 36+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 85) 37+lin-addr)
         (+ 37 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr37)
             x86)
         (la-to-pa 37+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 86) 38+lin-addr)
         (+ 38 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr38)
             x86)
         (la-to-pa 38+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 87) 39+lin-addr)
         (+ 39 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr39)
             x86)
         (la-to-pa 39+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 88) 40+lin-addr)
         (+ 40 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr40)
             x86)
         (la-to-pa 40+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 89) 41+lin-addr)
         (+ 41 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr41)
             x86)
         (la-to-pa 41+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 90) 42+lin-addr)
         (+ 42 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr42)
             x86)
         (la-to-pa 42+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 91) 43+lin-addr)
         (+ 43 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr43)
             x86)
         (la-to-pa 43+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 92) 44+lin-addr)
         (+ 44 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr44)
             x86)
         (la-to-pa 44+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 93) 45+lin-addr)
         (+ 45 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr45)
             x86)
         (la-to-pa 45+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 94) 46+lin-addr)
         (+ 46 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr46)
             x86)
         (la-to-pa 46+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 95) 47+lin-addr)
         (+ 47 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr47)
             x86)
         (la-to-pa 47+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 96) 48+lin-addr)
         (+ 48 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr48)
             x86)
         (la-to-pa 48+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 97) 49+lin-addr)
         (+ 49 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr49)
             x86)
         (la-to-pa 49+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 98) 50+lin-addr)
         (+ 50 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr50)
             x86)
         (la-to-pa 50+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 99) 51+lin-addr)
         (+ 51 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr51)
             x86)
         (la-to-pa 51+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 100) 52+lin-addr)
         (+ 52 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr52)
             x86)
         (la-to-pa 52+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 101) 53+lin-addr)
         (+ 53 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr53)
             x86)
         (la-to-pa 53+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 102) 54+lin-addr)
         (+ 54 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr54)
             x86)
         (la-to-pa 54+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 103) 55+lin-addr)
         (+ 55 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr55)
             x86)
         (la-to-pa 55+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 104) 56+lin-addr)
         (+ 56 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr56)
             x86)
         (la-to-pa 56+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 105) 57+lin-addr)
         (+ 57 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr57)
             x86)
         (la-to-pa 57+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 106) 58+lin-addr)
         (+ 58 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr58)
             x86)
         (la-to-pa 58+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 107) 59+lin-addr)
         (+ 59 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr59)
             x86)
         (la-to-pa 59+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 108) 60+lin-addr)
         (+ 60 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr60)
             x86)
         (la-to-pa 60+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 109) 61+lin-addr)
         (+ 61 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr61)
             x86)
         (la-to-pa 61+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 110) 62+lin-addr)
         (+ 62 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr62)
             x86)
         (la-to-pa 62+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        ((the (signed-byte 111) 63+lin-addr)
         (+ 63 lin-addr))
        ((mv flag (the (unsigned-byte 52) p-addr63)
             x86)
         (la-to-pa 63+lin-addr r-x x86))
        ((when flag) (mv flag 0 x86))
        (byte0 (memi p-addr0 x86))
        (byte1 (memi p-addr1 x86))
        (byte2 (memi p-addr2 x86))
        (byte3 (memi p-addr3 x86))
        (byte4 (memi p-addr4 x86))
        (byte5 (memi p-addr5 x86))
        (byte6 (memi p-addr6 x86))
        (byte7 (memi p-addr7 x86))
        (byte8 (memi p-addr8 x86))
        (byte9 (memi p-addr9 x86))
        (byte10 (memi p-addr10 x86))
        (byte11 (memi p-addr11 x86))
        (byte12 (memi p-addr12 x86))
        (byte13 (memi p-addr13 x86))
        (byte14 (memi p-addr14 x86))
        (byte15 (memi p-addr15 x86))
        (byte16 (memi p-addr16 x86))
        (byte17 (memi p-addr17 x86))
        (byte18 (memi p-addr18 x86))
        (byte19 (memi p-addr19 x86))
        (byte20 (memi p-addr20 x86))
        (byte21 (memi p-addr21 x86))
        (byte22 (memi p-addr22 x86))
        (byte23 (memi p-addr23 x86))
        (byte24 (memi p-addr24 x86))
        (byte25 (memi p-addr25 x86))
        (byte26 (memi p-addr26 x86))
        (byte27 (memi p-addr27 x86))
        (byte28 (memi p-addr28 x86))
        (byte29 (memi p-addr29 x86))
        (byte30 (memi p-addr30 x86))
        (byte31 (memi p-addr31 x86))
        (byte32 (memi p-addr32 x86))
        (byte33 (memi p-addr33 x86))
        (byte34 (memi p-addr34 x86))
        (byte35 (memi p-addr35 x86))
        (byte36 (memi p-addr36 x86))
        (byte37 (memi p-addr37 x86))
        (byte38 (memi p-addr38 x86))
        (byte39 (memi p-addr39 x86))
        (byte40 (memi p-addr40 x86))
        (byte41 (memi p-addr41 x86))
        (byte42 (memi p-addr42 x86))
        (byte43 (memi p-addr43 x86))
        (byte44 (memi p-addr44 x86))
        (byte45 (memi p-addr45 x86))
        (byte46 (memi p-addr46 x86))
        (byte47 (memi p-addr47 x86))
        (byte48 (memi p-addr48 x86))
        (byte49 (memi p-addr49 x86))
        (byte50 (memi p-addr50 x86))
        (byte51 (memi p-addr51 x86))
        (byte52 (memi p-addr52 x86))
        (byte53 (memi p-addr53 x86))
        (byte54 (memi p-addr54 x86))
        (byte55 (memi p-addr55 x86))
        (byte56 (memi p-addr56 x86))
        (byte57 (memi p-addr57 x86))
        (byte58 (memi p-addr58 x86))
        (byte59 (memi p-addr59 x86))
        (byte60 (memi p-addr60 x86))
        (byte61 (memi p-addr61 x86))
        (byte62 (memi p-addr62 x86))
        (byte63 (memi p-addr63 x86))
        (xxword
          (the (unsigned-byte 512)
               (merge-64-u8s byte63 byte62
                             byte61 byte60 byte59 byte58 byte57
                             byte56 byte55 byte54 byte53 byte52
                             byte51 byte50 byte49 byte48 byte47
                             byte46 byte45 byte44 byte43 byte42
                             byte41 byte40 byte39 byte38 byte37
                             byte36 byte35 byte34 byte33 byte32
                             byte31 byte30 byte29 byte28 byte27
                             byte26 byte25 byte24 byte23 byte22
                             byte21 byte20 byte19 byte18 byte17
                             byte16 byte15 byte14 byte13 byte12
                             byte11 byte10 byte9 byte8 byte7 byte6
                             byte5 byte4 byte3 byte2 byte1 byte0))))
       (mv nil xxword x86)))
     (mv 'rml512 0 x86)))
   (mv 'rml512 0 x86))))

Theorem: n512p-mv-nth-1-rml512

(defthm n512p-mv-nth-1-rml512
 (unsigned-byte-p 512
                  (mv-nth 1 (rml512 lin-addr r-x x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (mv-nth 1 (rml512 lin-addr r-x x86)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and
    (<= 0 (mv-nth 1 (rml512 lin-addr r-x x86)))
    (<
     (mv-nth 1 (rml512 lin-addr r-x x86))
     13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: x86p-rml512

(defthm x86p-rml512
  (implies (force (x86p x86))
           (x86p (mv-nth 2 (rml512 lin-addr r-x x86))))
  :rule-classes (:rewrite :type-prescription))

Theorem: rml512-value-when-error

(defthm rml512-value-when-error
  (implies (mv-nth 0 (rml512 lin-addr r-x x86))
           (equal (mv-nth 1 (rml512 lin-addr r-x x86))
                  0)))

Theorem: rml512-x86-unmodified-in-app-view

(defthm rml512-x86-unmodified-in-app-view
  (implies (app-view x86)
           (equal (mv-nth 2 (rml512 lin-addr r-x x86))
                  x86)))

Theorem: xr-rml512-state-sys-view

(defthm xr-rml512-state-sys-view
  (implies (and (not (equal fld :mem))
                (not (equal fld :fault))
                (not (equal fld :tlb)))
           (equal (xr fld index
                      (mv-nth 2 (rml512 lin-addr r-x x86)))
                  (xr fld index x86))))

Theorem: rml512-xw-app-view

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

Theorem: rml512-xw-sys-view

(defthm rml512-xw-sys-view
 (implies
  (and (not (app-view x86))
       (not (equal fld :fault))
       (not (equal fld :seg-visible))
       (not (equal fld :seg-hidden-base))
       (not (equal fld :seg-hidden-limit))
       (not (equal fld :seg-hidden-attr))
       (not (equal fld :mem))
       (not (equal fld :ctr))
       (not (equal fld :msr))
       (not (equal fld :rflags))
       (not (equal fld :app-view))
       (not (equal fld :marking-view))
       (not (equal fld :tlb))
       (not (equal fld :implicit-supervisor-access))
       (member-equal fld *x86-field-names-as-keywords*))
  (and
      (equal (mv-nth 0
                     (rml512 lin-addr r-x (xw fld index value x86)))
             (mv-nth 0 (rml512 lin-addr r-x x86)))
      (equal (mv-nth 1
                     (rml512 lin-addr r-x (xw fld index value x86)))
             (mv-nth 1 (rml512 lin-addr r-x x86)))
      (equal (mv-nth 2
                     (rml512 lin-addr r-x (xw fld index value x86)))
             (xw fld index value
                 (mv-nth 2 (rml512 lin-addr r-x x86)))))))

Theorem: rml512-xw-sys-view-rflags-not-ac

(defthm rml512-xw-sys-view-rflags-not-ac
  (implies
       (and (not (app-view x86))
            (equal (rflagsbits->ac value)
                   (rflagsbits->ac (rflags x86))))
       (and (equal (mv-nth 0
                           (rml512 lin-addr
                                   r-x (xw :rflags nil value x86)))
                   (mv-nth 0 (rml512 lin-addr r-x x86)))
            (equal (mv-nth 1
                           (rml512 lin-addr
                                   r-x (xw :rflags nil value x86)))
                   (mv-nth 1 (rml512 lin-addr r-x x86)))
            (equal (mv-nth 2
                           (rml512 lin-addr
                                   r-x (xw :rflags nil value x86)))
                   (xw :rflags nil value
                       (mv-nth 2 (rml512 lin-addr r-x x86)))))))