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

Parametric-memory-reads-and-writes

Functions to read/write 8/16/32/64/128/256 bits into the memory.

Definitions and Theorems

Function: rml-size$inline

(defun rml-size$inline (nbytes addr r-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member 1 2 4 6 8 10 16 32)
                 nbytes)
           (type (signed-byte 48) addr)
           (type (member :r :x) r-x))
  (declare (xargs :guard (natp nbytes)))
  (case nbytes
    (1 (rml08 addr r-x x86))
    (2 (rml16 addr r-x x86))
    (4 (rml32 addr r-x x86))
    (6 (rml48 addr r-x x86))
    (8 (rml64 addr r-x x86))
    (10 (rml80 addr r-x x86))
    (16 (rml128 addr r-x x86))
    (32 (rml256 addr r-x x86))
    (otherwise
         (if (mbe :logic (canonical-address-p (+ -1 nbytes addr))
                  :exec (< (+ -1 nbytes addr) 140737488355328))
             (rb nbytes addr r-x x86)
           (mv 'rml-size 0 x86)))))

Theorem: x86p-of-mv-nth-2-of-rml-size

(defthm x86p-of-mv-nth-2-of-rml-size
  (implies (force (x86p x86))
           (x86p (mv-nth 2 (rml-size bytes lin-addr r-x x86)))))

Function: riml-size$inline

(defun riml-size$inline (nbytes addr r-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member 1 2 4 8) nbytes)
           (type (signed-byte 48) addr)
           (type (member :r :x) r-x))
  (case nbytes
    (1 (riml08 addr r-x x86))
    (2 (riml16 addr r-x x86))
    (4 (riml32 addr r-x x86))
    (8 (riml64 addr r-x x86))
    (otherwise (mv 'riml-size nbytes x86))))

Function: wml-size$inline

(defun wml-size$inline (nbytes addr val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member 1 2 4 6 8 10 16 32)
                 nbytes)
           (type (signed-byte 48) addr)
           (type (integer 0 *) val))
  (declare (xargs :guard
                  (case nbytes
                    (1 (n08p val))
                    (2 (n16p val))
                    (4 (n32p val))
                    (6 (n48p val))
                    (8 (n64p val))
                    (10 (n80p val))
                    (16 (n128p val))
                    (32 (n256p val)))))
  (case nbytes
    (1 (wml08 addr val x86))
    (2 (wml16 addr val x86))
    (4 (wml32 addr val x86))
    (6 (wml48 addr val x86))
    (8 (wml64 addr val x86))
    (10 (wml80 addr val x86))
    (16 (wml128 addr val x86))
    (32 (wml256 addr val x86))
    (otherwise
         (if (mbe :logic (canonical-address-p (+ -1 nbytes addr))
                  :exec (< (+ nbytes addr) 140737488355327))
             (wb nbytes addr :w val x86)
           (mv 'wml-size x86)))))

Theorem: x86p-wml-size

(defthm x86p-wml-size
  (implies (force (x86p x86))
           (x86p (mv-nth 1 (wml-size nbytes lin-addr val x86)))))

Function: wiml-size$inline

(defun wiml-size$inline (nbytes addr val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member 1 2 4 8) nbytes)
           (type (signed-byte 48) addr)
           (type integer val))
  (declare (xargs :guard
                  (case nbytes
                    (1 (i08p val))
                    (2 (i16p val))
                    (4 (i32p val))
                    (8 (i64p val)))))
  (case nbytes
    (1 (wiml08 addr val x86))
    (2 (wiml16 addr val x86))
    (4 (wiml32 addr val x86))
    (8 (wiml64 addr val x86))
    (otherwise (mv 'wiml-size x86))))