• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
            • Linear-memory-in-app-view
              • Canonical-address-p
              • Rvm512
              • Rvm32
              • Rvm256
              • Wvm32
              • Rvm128
              • Rvm80
              • Rvm64
                • Rvm48
                • Wvm512
                • Wvm64
                • Wvm48
                • Wvm256
                • Wvm128
                • Rvm16
                • Wvm80
                • Wvm16
                • Rvm08
                • Wvm08
            • 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-in-app-view

    Rvm64

    Signature
    (rvm64 addr x86) → (mv * * x86)

    Definitions and Theorems

    Function: rvm64$inline

    (defun rvm64$inline (addr x86)
      (declare (xargs :stobjs (x86)))
      (declare (type (signed-byte 48) addr))
      (if
       (mbt (canonical-address-p addr))
       (let* ((4+addr (the (signed-byte 49)
                           (+ 4 (the (signed-byte 48) addr))))
              (7+addr (the (signed-byte 49)
                           (+ 7 (the (signed-byte 48) addr)))))
         (if (mbe :logic (canonical-address-p 7+addr)
                  :exec (< (the (signed-byte 49) 7+addr)
                           140737488355328))
             (b* (((mv flg0 (the (unsigned-byte 32) dword0)
                       x86)
                   (rvm32 addr x86))
                  ((mv flg1 (the (unsigned-byte 32) dword1)
                       x86)
                   (rvm32 4+addr x86))
                  ((the (unsigned-byte 64) qword)
                   (the (unsigned-byte 64)
                        (logior (the (unsigned-byte 64) (ash dword1 32))
                                dword0))))
               (mbe :logic
                    (if (or flg0 flg1)
                        (mv 'rvm64 0 x86)
                      (mv nil qword x86))
                    :exec (mv nil qword x86)))
           (mv 'rvm64 0 x86)))
       (mv 'rvm64 0 x86)))

    Theorem: rvm64-no-error

    (defthm rvm64-no-error
      (implies (and (canonical-address-p addr)
                    (canonical-address-p (+ 7 addr)))
               (equal (mv-nth 0 (rvm64 addr x86))
                      nil)))

    Theorem: n64p-mv-nth-1-rvm64

    (defthm n64p-mv-nth-1-rvm64
     (unsigned-byte-p 64 (mv-nth 1 (rvm64 addr x86)))
     :rule-classes
     (:rewrite
      (:type-prescription
          :corollary (natp (mv-nth 1 (rvm64 addr x86)))
          :hints
          (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
      (:linear
       :corollary (and (<= 0 (mv-nth 1 (rvm64 addr x86)))
                       (< (mv-nth 1 (rvm64 addr x86))
                          18446744073709551616))
       :hints
       (("Goal"
            :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

    Theorem: x86p-mv-nth-2-rvm64-unchanged

    (defthm x86p-mv-nth-2-rvm64-unchanged
      (equal (mv-nth 2 (rvm64 addr x86)) x86))

    Theorem: xr-rvm64

    (defthm xr-rvm64
      (equal (xr fld index (mv-nth 2 (rvm64 addr x86)))
             (xr fld index x86)))

    Theorem: rvm64-xw-values

    (defthm rvm64-xw-values
      (implies
           (not (equal fld :mem))
           (and (equal (mv-nth 0 (rvm64 addr (xw fld index value x86)))
                       (mv-nth 0 (rvm64 addr x86)))
                (equal (mv-nth 1 (rvm64 addr (xw fld index value x86)))
                       (mv-nth 1 (rvm64 addr x86))))))