		Search-engine friendly clone of the ACL2 documentation.

Evex-prefixes

!evex-prefixes->byte3

Update the |X86ISA|::|BYTE3| field of a evex-prefixes bit structure.

Signature
(!evex-prefixes->byte3 byte3 x) → new-x
Arguments: byte3 — Guard (8bits-p byte3).; x — Guard (evex-prefixes-p x).
Returns: new-x — Type (evex-prefixes-p new-x).

Definitions and Theorems

Function: !evex-prefixes->byte3$inline

(defun !evex-prefixes->byte3$inline (byte3 x)
 (declare (xargs :guard (and (8bits-p byte3)
                             (evex-prefixes-p x))))
 (mbe :logic
      (b* ((byte3 (mbe :logic (8bits-fix byte3)
                       :exec byte3))
           (x (evex-prefixes-fix x)))
        (part-install byte3 x :width 8 :low 24))
      :exec
      (the (unsigned-byte 32)
           (logior (the (unsigned-byte 32)
                        (logand (the (unsigned-byte 32) x)
                                (the (signed-byte 33) -4278190081)))
                   (the (unsigned-byte 32)
                        (ash (the (unsigned-byte 8) byte3)
                             24))))))

Theorem: evex-prefixes-p-of-!evex-prefixes->byte3

(defthm evex-prefixes-p-of-!evex-prefixes->byte3
  (b* ((new-x (!evex-prefixes->byte3$inline byte3 x)))
    (evex-prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !evex-prefixes->byte3$inline-of-8bits-fix-byte3

(defthm !evex-prefixes->byte3$inline-of-8bits-fix-byte3
  (equal (!evex-prefixes->byte3$inline (8bits-fix byte3)
                                       x)
         (!evex-prefixes->byte3$inline byte3 x)))

Theorem: !evex-prefixes->byte3$inline-8bits-equiv-congruence-on-byte3

(defthm !evex-prefixes->byte3$inline-8bits-equiv-congruence-on-byte3
  (implies (8bits-equiv byte3 byte3-equiv)
           (equal (!evex-prefixes->byte3$inline byte3 x)
                  (!evex-prefixes->byte3$inline byte3-equiv x)))
  :rule-classes :congruence)

Theorem: !evex-prefixes->byte3$inline-of-evex-prefixes-fix-x

(defthm !evex-prefixes->byte3$inline-of-evex-prefixes-fix-x
  (equal (!evex-prefixes->byte3$inline byte3 (evex-prefixes-fix x))
         (!evex-prefixes->byte3$inline byte3 x)))

Theorem: !evex-prefixes->byte3$inline-evex-prefixes-equiv-congruence-on-x

(defthm
   !evex-prefixes->byte3$inline-evex-prefixes-equiv-congruence-on-x
  (implies (evex-prefixes-equiv x x-equiv)
           (equal (!evex-prefixes->byte3$inline byte3 x)
                  (!evex-prefixes->byte3$inline byte3 x-equiv)))
  :rule-classes :congruence)

Theorem: !evex-prefixes->byte3-is-evex-prefixes

(defthm !evex-prefixes->byte3-is-evex-prefixes
  (equal (!evex-prefixes->byte3 byte3 x)
         (change-evex-prefixes x :byte3 byte3)))

Theorem: evex-prefixes->byte3-of-!evex-prefixes->byte3

(defthm evex-prefixes->byte3-of-!evex-prefixes->byte3
  (b* ((?new-x (!evex-prefixes->byte3$inline byte3 x)))
    (equal (evex-prefixes->byte3 new-x)
           (8bits-fix byte3))))

Theorem: !evex-prefixes->byte3-equiv-under-mask

(defthm !evex-prefixes->byte3-equiv-under-mask
  (b* ((?new-x (!evex-prefixes->byte3$inline byte3 x)))
    (evex-prefixes-equiv-under-mask new-x x 16777215)))