• 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
            • 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
              • Wml256
              • Rml256
              • Wml512
              • Rml512
              • Rml128
              • Rml80
              • Program-location
              • Rml64
              • Wml128
              • Rml48
              • Rml32
              • Rml08
              • Rml16
              • Wml80
              • Wml64
              • Wml08
              • Byte-listp
              • 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
              • Riml64
              • Wml-size
              • Rml-size
              • 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
    • Reasoning-about-memory-reads-and-writes

    Rb

    Signature
    (rb n addr r-x x86) → (mv flg val new-x86)
    Arguments
    n — Number of bytes to be read.
        Guard (natp n).
    addr — First linear address.
        Guard (integerp addr).
    r-x — Type of memory access.
    Returns
    val — Type (integerp val).
    new-x86 — Type (x86p new-x86), given (x86p x86).

    Definitions and Theorems

    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 flg p-addrs x86)
                (las-to-pas n addr r-x x86))
               ((when flg) (mv flg 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 '(unsigned-byte-p integer-range-p (:e expt)))))))

    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 '(unsigned-byte-p integer-range-p (:e expt)))))))

    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)))