		Search-engine friendly clone of the ACL2 documentation.

Reasoning-about-memory-reads-and-writes

Wb

Signature
(wb n addr w value x86) → (mv * x86)
Arguments: n — Number of bytes to be written.
Guard (natp n).; addr — First linear address.
Guard (integerp addr).; w — Type of memory access.; value — Guard (natp value).

Definitions and Theorems

Function: wb

(defun wb (n addr w value x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :w) w))
  (declare (xargs :guard (and (natp n)
                              (integerp addr)
                              (natp value))))
  (declare (xargs :guard (canonical-address-p (+ -1 n addr))))
  (let ((__function__ 'wb))
    (declare (ignorable __function__))
    (if (app-view x86)
        (wb-1 n addr w value x86)
      (b* (((mv flgs p-addrs x86)
            (las-to-pas n addr :w x86))
           ((when flgs) (mv flgs x86))
           (x86 (write-to-physical-memory p-addrs value x86)))
        (mv nil x86)))))

Theorem: wb-no-writes-when-zp-n

(defthm wb-no-writes-when-zp-n
  (equal (mv-nth 1 (wb 0 addr val w x86))
         x86))

Theorem: wb-is-wb-1-for-app-view

(defthm wb-is-wb-1-for-app-view
  (implies (app-view x86)
           (equal (wb n addr w value x86)
                  (wb-1 n addr w value x86))))

Theorem: x86p-of-wb

(defthm x86p-of-wb
  (implies (x86p x86)
           (x86p (mv-nth 1 (wb n addr w value x86)))))

Theorem: wb-returns-no-error-app-view

(defthm wb-returns-no-error-app-view
  (implies (and (canonical-address-p addr)
                (canonical-address-p (+ -1 n addr))
                (app-view x86))
           (equal (mv-nth 0 (wb n addr w value x86))
                  nil)))