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

    Write-to-physical-memory

    Signature
    (write-to-physical-memory p-addrs value x86) → x86
    Arguments
    p-addrs — Guard (physical-address-listp p-addrs).
    value — Guard (natp value).

    Definitions and Theorems

    Function: write-to-physical-memory

    (defun write-to-physical-memory (p-addrs value x86)
      (declare (xargs :stobjs (x86)))
      (declare (xargs :guard (and (physical-address-listp p-addrs)
                                  (natp value))))
      (declare (xargs :guard (not (app-view x86))))
      (let ((__function__ 'write-to-physical-memory))
        (declare (ignorable __function__))
        (if (endp p-addrs)
            x86
          (b* ((addr0 (car p-addrs))
               (byte0 (loghead 8 value))
               (x86 (!memi addr0 byte0 x86)))
            (write-to-physical-memory (cdr p-addrs)
                                      (logtail 8 value)
                                      x86)))))

    Theorem: x86p-write-to-physical-memory

    (defthm x86p-write-to-physical-memory
      (implies (and (x86p x86)
                    (physical-address-listp p-addrs))
               (x86p (write-to-physical-memory p-addrs value x86))))

    Theorem: xr-not-mem-write-to-physical-memory

    (defthm xr-not-mem-write-to-physical-memory
      (implies (not (equal fld :mem))
               (equal (xr fld index
                          (write-to-physical-memory p-addrs bytes x86))
                      (xr fld index x86))))

    Theorem: write-to-physical-memory-xw-in-sys-view

    (defthm write-to-physical-memory-xw-in-sys-view
     (implies
      (not (equal fld :mem))
      (equal
       (write-to-physical-memory p-addrs bytes (xw fld index value x86))
       (xw fld index value
           (write-to-physical-memory p-addrs bytes x86)))))

    Theorem: 64-bit-modep-of-write-to-physical-memory

    (defthm 64-bit-modep-of-write-to-physical-memory
      (equal (64-bit-modep (write-to-physical-memory p-addrs value x86))
             (64-bit-modep x86)))

    Theorem: x86-operation-mode-of-write-to-physical-memory

    (defthm x86-operation-mode-of-write-to-physical-memory
     (equal
       (x86-operation-mode (write-to-physical-memory p-addrs value x86))
       (x86-operation-mode x86)))