• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • 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
          • 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
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Linear-memory

Rml256

Signature

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

Definitions and Theorems

Theorem: rb-and-rvm256

(defthm rb-and-rvm256
  (implies (and (app-view x86)
                (x86p x86)
                (canonical-address-p lin-addr)
                (canonical-address-p (+ 31 lin-addr)))
           (equal (rvm256 lin-addr x86)
                  (rb 32 lin-addr r-x x86))))

Theorem: unsigned-byte-p-256-of-merge-32-u8s-linear

(defthm unsigned-byte-p-256-of-merge-32-u8s-linear
 (implies
      (and (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 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
           256
           (merge-32-u8s h15 h14 h13 h12 h11 h10 h9 h8
                         h7 h6 h5 h4 h3 h2 h1 h0 l15 l14 l13 l12
                         l11 l10 l9 l8 l7 l6 l5 l4 l3 l2 l1 l0)))
 :rule-classes
 (:rewrite
  (:linear
   :corollary
   (implies
    (and (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 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-32-u8s h15 h14 h13 h12 h11 h10 h9 h8
                       h7 h6 h5 h4 h3 h2 h1 h0 l15 l14 l13 l12
                       l11 l10 l9 l8 l7 l6 l5 l4 l3 l2 l1 l0))
     (<
      (merge-32-u8s h15 h14 h13 h12 h11 h10 h9 h8
                    h7 h6 h5 h4 h3 h2 h1 h0 l15 l14 l13 l12
                    l11 l10 l9 l8 l7 l6 l5 l4 l3 l2 l1 l0)
      115792089237316195423570985008687907853269984665640564039457584007913129639936)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: rml256

(defun rml256 (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__ 'rml256))
  (declare (ignorable __function__))
  (if
   (mbt (canonical-address-p lin-addr))
   (let*
       ((31+lin-addr (the (signed-byte 49)
                          (+ 31 (the (signed-byte 48) lin-addr)))))
    (if
     (mbe :logic (canonical-address-p 31+lin-addr)
          :exec (< (the (signed-byte 49) 31+lin-addr)
                   140737488355328))
     (if (app-view x86)
         (mbe :logic (rb 32 lin-addr r-x x86)
              :exec (rvm256 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))
        (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))
        (xword
          (the (unsigned-byte 256)
               (merge-32-u8s 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 xword x86)))
     (mv 'rml256 0 x86)))
   (mv 'rml256 0 x86))))

Theorem: n256p-mv-nth-1-rml256

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

Theorem: x86p-rml256

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

Theorem: rml256-value-when-error

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

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

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

Theorem: xr-rml256-state-sys-view

(defthm xr-rml256-state-sys-view
  (implies (and (not (app-view x86))
                (not (equal fld :mem))
                (not (equal fld :fault))
                (not (equal fld :tlb))
                (member-equal fld *x86-field-names-as-keywords*))
           (equal (xr fld index
                      (mv-nth 2 (rml256 lin-addr r-x x86)))
                  (xr fld index x86))))

Theorem: rml256-xw-app-view

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

Theorem: rml256-xw-sys-view

(defthm rml256-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
                     (rml256 lin-addr r-x (xw fld index value x86)))
             (mv-nth 0 (rml256 lin-addr r-x x86)))
      (equal (mv-nth 1
                     (rml256 lin-addr r-x (xw fld index value x86)))
             (mv-nth 1 (rml256 lin-addr r-x x86)))
      (equal (mv-nth 2
                     (rml256 lin-addr r-x (xw fld index value x86)))
             (xw fld index value
                 (mv-nth 2 (rml256 lin-addr r-x x86)))))))

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

(defthm rml256-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
                           (rml256 lin-addr
                                   r-x (xw :rflags nil value x86)))
                   (mv-nth 0 (rml256 lin-addr r-x x86)))
            (equal (mv-nth 1
                           (rml256 lin-addr
                                   r-x (xw :rflags nil value x86)))
                   (mv-nth 1 (rml256 lin-addr r-x x86)))
            (equal (mv-nth 2
                           (rml256 lin-addr
                                   r-x (xw :rflags nil value x86)))
                   (xw :rflags nil value
                       (mv-nth 2 (rml256 lin-addr r-x x86)))))))