		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Wml-size

Signature
(wml-size nbytes addr val x86) → (mv * x86)

Definitions and Theorems

Function: wml-size$inline

(defun wml-size$inline (nbytes addr val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member 1 2 4 6 8 10 16 32)
                 nbytes)
           (type (signed-byte 48) addr)
           (type (integer 0 *) val))
  (declare (xargs :guard
                  (case nbytes
                    (1 (n08p val))
                    (2 (n16p val))
                    (4 (n32p val))
                    (6 (n48p val))
                    (8 (n64p val))
                    (10 (n80p val))
                    (16 (n128p val))
                    (32 (n256p val)))))
  (case nbytes
    (1 (wml08 addr val x86))
    (2 (wml16 addr val x86))
    (4 (wml32 addr val x86))
    (6 (wml48 addr val x86))
    (8 (wml64 addr val x86))
    (10 (wml80 addr val x86))
    (16 (wml128 addr val x86))
    (32 (wml256 addr val x86))
    (otherwise
         (if (mbe :logic (canonical-address-p (+ -1 nbytes addr))
                  :exec (< (+ nbytes addr) 140737488355327))
             (wb nbytes addr :w val x86)
           (mv 'wml-size x86)))))

Theorem: x86p-wml-size

(defthm x86p-wml-size
  (implies (force (x86p x86))
           (x86p (mv-nth 1 (wml-size nbytes lin-addr val x86)))))