		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex->vvvv

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

Signature
(vex->vvvv vex-prefixes) → vvvv
Arguments: vex-prefixes — Guard (vex-prefixes-p vex-prefixes).
Returns: vvvv — Type (unsigned-byte-p 4 vvvv), given (vex-prefixes-byte0-p vex-prefixes).

Definitions and Theorems

Function: vex->vvvv$inline

(defun vex->vvvv$inline (vex-prefixes)
  (declare (xargs :guard (vex-prefixes-p vex-prefixes)))
  (declare (xargs :guard (vex-prefixes-byte0-p vex-prefixes)))
  (case (vex-prefixes->byte0 vex-prefixes)
    (197 (vex2-byte1->vvvv (vex-prefixes->byte1 vex-prefixes)))
    (196 (vex3-byte2->vvvv (vex-prefixes->byte2 vex-prefixes)))
    (otherwise -1)))

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

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