		Search-engine friendly clone of the ACL2 documentation.

Linear-memory-in-app-view

Wvm08

Signature
(wvm08 addr val x86) → (mv * x86)

Definitions and Theorems

Function: wvm08$inline

(defun wvm08$inline (addr val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) addr)
           (type (unsigned-byte 8) val))
  (mbe :logic
       (if (canonical-address-p addr)
           (let ((x86 (!memi (n48 addr) (n08 val) x86)))
             (mv nil x86))
         (mv 'wvm08 x86))
       :exec
       (let ((x86 (!memi (n48 addr) val x86)))
         (mv nil x86))))

Theorem: wvm08-no-error

(defthm wvm08-no-error
  (implies (canonical-address-p addr)
           (equal (mv-nth 0 (wvm08 addr val x86))
                  nil)))

Theorem: x86p-mv-nth-1-wvm08

(defthm x86p-mv-nth-1-wvm08
  (implies (x86p x86)
           (x86p (mv-nth 1 (wvm08 addr val x86))))
  :rule-classes (:rewrite :type-prescription))

Theorem: xr-wmv08-app-view

(defthm xr-wmv08-app-view
  (implies (not (equal fld :mem))
           (equal (xr fld
                      index (mv-nth 1 (wvm08 addr val x86)))
                  (xr fld index x86))))

Theorem: wvm08-xw-app-view

(defthm wvm08-xw-app-view
 (implies
      (not (equal fld :mem))
      (and (equal (mv-nth 0
                          (wvm08 addr val (xw fld index value x86)))
                  (mv-nth 0 (wvm08 addr val x86)))
           (equal (mv-nth 1
                          (wvm08 addr val (xw fld index value x86)))
                  (xw fld index value
                      (mv-nth 1 (wvm08 addr val x86)))))))