		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Wiml64

Signature
(wiml64 lin-addr val x86) → (mv * x86)

Definitions and Theorems

Function: wiml64

(defun wiml64 (lin-addr val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) lin-addr)
           (type (signed-byte 64) val))
  (declare (xargs :split-types t
                  :guard (and (canonical-address-p lin-addr)
                              (signed-byte-p 64 val))))
  (let ((__function__ 'wiml64))
    (declare (ignorable __function__))
    (wml64 lin-addr
           (the (unsigned-byte 64) (n64 val))
           x86)))

Theorem: x86p-wiml64

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