		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex->w

Get the W field of vex-prefixes; cognizant of the two- or three-byte VEX prefixes form.

Signature
(vex->w vex-prefixes) → w
Returns: w — Type (unsigned-byte-p 1 w), given (vex-prefixes-byte0-p vex-prefixes).

Definitions and Theorems

Function: vex->w$inline

(defun vex->w$inline (vex-prefixes)
  (declare (type (unsigned-byte 24) vex-prefixes))
  (declare (xargs :guard (vex-prefixes-byte0-p vex-prefixes)))
  (case (vex-prefixes->byte0 vex-prefixes)
    (196 (vex3-byte2->w (vex-prefixes->byte2 vex-prefixes)))
    (otherwise 0)))

Theorem: return-type-of-vex->w

(defthm return-type-of-vex->w
  (implies (vex-prefixes-byte0-p vex-prefixes)
           (b* ((w (vex->w$inline vex-prefixes)))
             (unsigned-byte-p 1 w)))
  :rule-classes :rewrite)

Theorem: if-not-vex3-byte0-then-vex-w=0

(defthm if-not-vex3-byte0-then-vex-w=0
  (b* nil
    (implies (not (equal (vex-prefixes->byte0 vex-prefixes)
                         196))
             (equal (vex->w vex-prefixes) 0))))