		Search-engine friendly clone of the ACL2 documentation.

Reasoning-about-memory-reads-and-writes

Wb-1

Signature
(wb-1 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: write.; value — Guard (natp value).

Definitions and Theorems

Function: wb-1

(defun wb-1 (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-1))
    (declare (ignorable __function__))
    (if (zp n)
        (mv nil x86)
      (b* (((unless (canonical-address-p addr))
            (mv t x86))
           ((mv flg0 x86)
            (wvm08 addr (loghead 8 value) x86))
           ((when flg0) (mv flg0 x86))
           ((mv rest-flg x86)
            (wb-1 (1- n)
                  (1+ addr)
                  w (logtail 8 value)
                  x86)))
        (mv rest-flg x86)))))

Theorem: wb-1-returns-x86p

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

Theorem: wb-1-returns-no-error

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