		Search-engine friendly clone of the ACL2 documentation.

Structures

Evex-byte3

An 8-bit unsigned bitstruct type.

This is a bitstruct type introduced by defbitstruct, represented as a unsigned 8-bit integer.

Fields

aaa — 3bits: Embedded opmask register specifier.
v-prime — bit: High-16 NDS/VIDX register specifier -- combine with EVEX.vvvv or when VSIB present.
b — bit: Broadcast/RC/SAE Context.
vl/rc — 2bits: Vector length/RC (denoted as L'L in the Intel manuals).
z — bit: Zeroing/Merging.

Definitions and Theorems

Function: evex-byte3-p$inline

(defun evex-byte3-p$inline (x)
  (declare (xargs :guard t))
  (mbe :logic (unsigned-byte-p 8 x)
       :exec (and (natp x) (< x 256))))

Theorem: evex-byte3-p-when-unsigned-byte-p

(defthm evex-byte3-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 8 x)
           (evex-byte3-p x)))

Theorem: unsigned-byte-p-when-evex-byte3-p

(defthm unsigned-byte-p-when-evex-byte3-p
  (implies (evex-byte3-p x)
           (unsigned-byte-p 8 x)))

Theorem: evex-byte3-p-compound-recognizer

(defthm evex-byte3-p-compound-recognizer
  (implies (evex-byte3-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: evex-byte3-fix$inline

(defun evex-byte3-fix$inline (x)
  (declare (xargs :guard (evex-byte3-p x)))
  (mbe :logic (loghead 8 x) :exec x))

Theorem: evex-byte3-p-of-evex-byte3-fix

(defthm evex-byte3-p-of-evex-byte3-fix
  (b* ((fty::fixed (evex-byte3-fix$inline x)))
    (evex-byte3-p fty::fixed))
  :rule-classes :rewrite)

Theorem: evex-byte3-fix-when-evex-byte3-p

(defthm evex-byte3-fix-when-evex-byte3-p
  (implies (evex-byte3-p x)
           (equal (evex-byte3-fix x) x)))

Function: evex-byte3-equiv$inline

(defun evex-byte3-equiv$inline (x y)
  (declare (xargs :guard (and (evex-byte3-p x)
                              (evex-byte3-p y))))
  (equal (evex-byte3-fix x)
         (evex-byte3-fix y)))

Theorem: evex-byte3-equiv-is-an-equivalence

(defthm evex-byte3-equiv-is-an-equivalence
  (and (booleanp (evex-byte3-equiv x y))
       (evex-byte3-equiv x x)
       (implies (evex-byte3-equiv x y)
                (evex-byte3-equiv y x))
       (implies (and (evex-byte3-equiv x y)
                     (evex-byte3-equiv y z))
                (evex-byte3-equiv x z)))
  :rule-classes (:equivalence))

Theorem: evex-byte3-equiv-implies-equal-evex-byte3-fix-1

(defthm evex-byte3-equiv-implies-equal-evex-byte3-fix-1
  (implies (evex-byte3-equiv x x-equiv)
           (equal (evex-byte3-fix x)
                  (evex-byte3-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: evex-byte3-fix-under-evex-byte3-equiv

(defthm evex-byte3-fix-under-evex-byte3-equiv
  (evex-byte3-equiv (evex-byte3-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: evex-byte3$inline

(defun evex-byte3$inline (aaa v-prime b vl/rc z)
  (declare (xargs :guard (and (3bits-p aaa)
                              (bitp v-prime)
                              (bitp b)
                              (2bits-p vl/rc)
                              (bitp z))))
  (b* ((aaa (mbe :logic (3bits-fix aaa) :exec aaa))
       (v-prime (mbe :logic (bfix v-prime)
                     :exec v-prime))
       (b (mbe :logic (bfix b) :exec b))
       (vl/rc (mbe :logic (2bits-fix vl/rc)
                   :exec vl/rc))
       (z (mbe :logic (bfix z) :exec z)))
    (logapp 3 aaa
            (logapp 1 v-prime
                    (logapp 1 b (logapp 2 vl/rc z))))))

Theorem: evex-byte3-p-of-evex-byte3

(defthm evex-byte3-p-of-evex-byte3
  (b* ((evex-byte3 (evex-byte3$inline aaa v-prime b vl/rc z)))
    (evex-byte3-p evex-byte3))
  :rule-classes :rewrite)

Theorem: evex-byte3$inline-of-3bits-fix-aaa

(defthm evex-byte3$inline-of-3bits-fix-aaa
  (equal (evex-byte3$inline (3bits-fix aaa)
                            v-prime b vl/rc z)
         (evex-byte3$inline aaa v-prime b vl/rc z)))

Theorem: evex-byte3$inline-3bits-equiv-congruence-on-aaa

(defthm evex-byte3$inline-3bits-equiv-congruence-on-aaa
  (implies (3bits-equiv aaa aaa-equiv)
           (equal (evex-byte3$inline aaa v-prime b vl/rc z)
                  (evex-byte3$inline aaa-equiv v-prime b vl/rc z)))
  :rule-classes :congruence)

Theorem: evex-byte3$inline-of-bfix-v-prime

(defthm evex-byte3$inline-of-bfix-v-prime
  (equal (evex-byte3$inline aaa (bfix v-prime)
                            b vl/rc z)
         (evex-byte3$inline aaa v-prime b vl/rc z)))

Theorem: evex-byte3$inline-bit-equiv-congruence-on-v-prime

(defthm evex-byte3$inline-bit-equiv-congruence-on-v-prime
  (implies (bit-equiv v-prime v-prime-equiv)
           (equal (evex-byte3$inline aaa v-prime b vl/rc z)
                  (evex-byte3$inline aaa v-prime-equiv b vl/rc z)))
  :rule-classes :congruence)

Theorem: evex-byte3$inline-of-bfix-b

(defthm evex-byte3$inline-of-bfix-b
  (equal (evex-byte3$inline aaa v-prime (bfix b)
                            vl/rc z)
         (evex-byte3$inline aaa v-prime b vl/rc z)))

Theorem: evex-byte3$inline-bit-equiv-congruence-on-b

(defthm evex-byte3$inline-bit-equiv-congruence-on-b
  (implies (bit-equiv b b-equiv)
           (equal (evex-byte3$inline aaa v-prime b vl/rc z)
                  (evex-byte3$inline aaa v-prime b-equiv vl/rc z)))
  :rule-classes :congruence)

Theorem: evex-byte3$inline-of-2bits-fix-vl/rc

(defthm evex-byte3$inline-of-2bits-fix-vl/rc
  (equal (evex-byte3$inline aaa v-prime b (2bits-fix vl/rc)
                            z)
         (evex-byte3$inline aaa v-prime b vl/rc z)))

Theorem: evex-byte3$inline-2bits-equiv-congruence-on-vl/rc

(defthm evex-byte3$inline-2bits-equiv-congruence-on-vl/rc
  (implies (2bits-equiv vl/rc vl/rc-equiv)
           (equal (evex-byte3$inline aaa v-prime b vl/rc z)
                  (evex-byte3$inline aaa v-prime b vl/rc-equiv z)))
  :rule-classes :congruence)

Theorem: evex-byte3$inline-of-bfix-z

(defthm evex-byte3$inline-of-bfix-z
  (equal (evex-byte3$inline aaa v-prime b vl/rc (bfix z))
         (evex-byte3$inline aaa v-prime b vl/rc z)))

Theorem: evex-byte3$inline-bit-equiv-congruence-on-z

(defthm evex-byte3$inline-bit-equiv-congruence-on-z
  (implies (bit-equiv z z-equiv)
           (equal (evex-byte3$inline aaa v-prime b vl/rc z)
                  (evex-byte3$inline aaa v-prime b vl/rc z-equiv)))
  :rule-classes :congruence)

Function: evex-byte3-equiv-under-mask$inline

(defun evex-byte3-equiv-under-mask$inline (x x1 mask)
  (declare (xargs :guard (and (evex-byte3-p x)
                              (evex-byte3-p x1)
                              (integerp mask))))
  (fty::int-equiv-under-mask (evex-byte3-fix x)
                             (evex-byte3-fix x1)
                             mask))

Function: evex-byte3->aaa$inline

(defun evex-byte3->aaa$inline (x)
  (declare (xargs :guard (evex-byte3-p x)))
  (mbe :logic
       (let ((x (evex-byte3-fix x)))
         (part-select x :low 0 :width 3))
       :exec (the (unsigned-byte 3)
                  (logand (the (unsigned-byte 3) 7)
                          (the (unsigned-byte 8) x)))))

Theorem: 3bits-p-of-evex-byte3->aaa

(defthm 3bits-p-of-evex-byte3->aaa
  (b* ((aaa (evex-byte3->aaa$inline x)))
    (3bits-p aaa))
  :rule-classes :rewrite)

Theorem: evex-byte3->aaa$inline-of-evex-byte3-fix-x

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

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

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

Theorem: evex-byte3->aaa-of-evex-byte3

(defthm evex-byte3->aaa-of-evex-byte3
  (equal (evex-byte3->aaa (evex-byte3 aaa v-prime b vl/rc z))
         (3bits-fix aaa)))

Theorem: evex-byte3->aaa-of-write-with-mask

(defthm evex-byte3->aaa-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x evex-byte3-equiv-under-mask)
                (evex-byte3-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 7) 0))
           (equal (evex-byte3->aaa x)
                  (evex-byte3->aaa y))))

Function: evex-byte3->v-prime$inline

(defun evex-byte3->v-prime$inline (x)
 (declare (xargs :guard (evex-byte3-p x)))
 (mbe
     :logic
     (let ((x (evex-byte3-fix x)))
       (part-select x :low 3 :width 1))
     :exec (the (unsigned-byte 1)
                (logand (the (unsigned-byte 1) 1)
                        (the (unsigned-byte 5)
                             (ash (the (unsigned-byte 8) x) -3))))))

Theorem: bitp-of-evex-byte3->v-prime

(defthm bitp-of-evex-byte3->v-prime
  (b* ((v-prime (evex-byte3->v-prime$inline x)))
    (bitp v-prime))
  :rule-classes :rewrite)

Theorem: evex-byte3->v-prime$inline-of-evex-byte3-fix-x

(defthm evex-byte3->v-prime$inline-of-evex-byte3-fix-x
  (equal (evex-byte3->v-prime$inline (evex-byte3-fix x))
         (evex-byte3->v-prime$inline x)))

Theorem: evex-byte3->v-prime$inline-evex-byte3-equiv-congruence-on-x

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

Theorem: evex-byte3->v-prime-of-evex-byte3

(defthm evex-byte3->v-prime-of-evex-byte3
  (equal (evex-byte3->v-prime (evex-byte3 aaa v-prime b vl/rc z))
         (bfix v-prime)))

Theorem: evex-byte3->v-prime-of-write-with-mask

(defthm evex-byte3->v-prime-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x evex-byte3-equiv-under-mask)
                (evex-byte3-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 8) 0))
           (equal (evex-byte3->v-prime x)
                  (evex-byte3->v-prime y))))

Function: evex-byte3->b$inline

(defun evex-byte3->b$inline (x)
 (declare (xargs :guard (evex-byte3-p x)))
 (mbe
     :logic
     (let ((x (evex-byte3-fix x)))
       (part-select x :low 4 :width 1))
     :exec (the (unsigned-byte 1)
                (logand (the (unsigned-byte 1) 1)
                        (the (unsigned-byte 4)
                             (ash (the (unsigned-byte 8) x) -4))))))

Theorem: bitp-of-evex-byte3->b

(defthm bitp-of-evex-byte3->b
  (b* ((b (evex-byte3->b$inline x)))
    (bitp b))
  :rule-classes :rewrite)

Theorem: evex-byte3->b$inline-of-evex-byte3-fix-x

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

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

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

Theorem: evex-byte3->b-of-evex-byte3

(defthm evex-byte3->b-of-evex-byte3
  (equal (evex-byte3->b (evex-byte3 aaa v-prime b vl/rc z))
         (bfix b)))

Theorem: evex-byte3->b-of-write-with-mask

(defthm evex-byte3->b-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x evex-byte3-equiv-under-mask)
                (evex-byte3-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 16)
                       0))
           (equal (evex-byte3->b x)
                  (evex-byte3->b y))))

Function: evex-byte3->vl/rc$inline

(defun evex-byte3->vl/rc$inline (x)
 (declare (xargs :guard (evex-byte3-p x)))
 (mbe
     :logic
     (let ((x (evex-byte3-fix x)))
       (part-select x :low 5 :width 2))
     :exec (the (unsigned-byte 2)
                (logand (the (unsigned-byte 2) 3)
                        (the (unsigned-byte 3)
                             (ash (the (unsigned-byte 8) x) -5))))))

Theorem: 2bits-p-of-evex-byte3->vl/rc

(defthm 2bits-p-of-evex-byte3->vl/rc
  (b* ((vl/rc (evex-byte3->vl/rc$inline x)))
    (2bits-p vl/rc))
  :rule-classes :rewrite)

Theorem: evex-byte3->vl/rc$inline-of-evex-byte3-fix-x

(defthm evex-byte3->vl/rc$inline-of-evex-byte3-fix-x
  (equal (evex-byte3->vl/rc$inline (evex-byte3-fix x))
         (evex-byte3->vl/rc$inline x)))

Theorem: evex-byte3->vl/rc$inline-evex-byte3-equiv-congruence-on-x

(defthm evex-byte3->vl/rc$inline-evex-byte3-equiv-congruence-on-x
  (implies (evex-byte3-equiv x x-equiv)
           (equal (evex-byte3->vl/rc$inline x)
                  (evex-byte3->vl/rc$inline x-equiv)))
  :rule-classes :congruence)

Theorem: evex-byte3->vl/rc-of-evex-byte3

(defthm evex-byte3->vl/rc-of-evex-byte3
  (equal (evex-byte3->vl/rc (evex-byte3 aaa v-prime b vl/rc z))
         (2bits-fix vl/rc)))

Theorem: evex-byte3->vl/rc-of-write-with-mask

(defthm evex-byte3->vl/rc-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x evex-byte3-equiv-under-mask)
                (evex-byte3-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 96)
                       0))
           (equal (evex-byte3->vl/rc x)
                  (evex-byte3->vl/rc y))))

Function: evex-byte3->z$inline

(defun evex-byte3->z$inline (x)
 (declare (xargs :guard (evex-byte3-p x)))
 (mbe
     :logic
     (let ((x (evex-byte3-fix x)))
       (part-select x :low 7 :width 1))
     :exec (the (unsigned-byte 1)
                (logand (the (unsigned-byte 1) 1)
                        (the (unsigned-byte 1)
                             (ash (the (unsigned-byte 8) x) -7))))))

Theorem: bitp-of-evex-byte3->z

(defthm bitp-of-evex-byte3->z
  (b* ((z (evex-byte3->z$inline x)))
    (bitp z))
  :rule-classes :rewrite)

Theorem: evex-byte3->z$inline-of-evex-byte3-fix-x

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

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

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

Theorem: evex-byte3->z-of-evex-byte3

(defthm evex-byte3->z-of-evex-byte3
  (equal (evex-byte3->z (evex-byte3 aaa v-prime b vl/rc z))
         (bfix z)))

Theorem: evex-byte3->z-of-write-with-mask

(defthm evex-byte3->z-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x evex-byte3-equiv-under-mask)
                (evex-byte3-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 128)
                       0))
           (equal (evex-byte3->z x)
                  (evex-byte3->z y))))

Theorem: evex-byte3-fix-in-terms-of-evex-byte3

(defthm evex-byte3-fix-in-terms-of-evex-byte3
  (equal (evex-byte3-fix x)
         (change-evex-byte3 x)))

Function: !evex-byte3->aaa$inline

(defun !evex-byte3->aaa$inline (aaa x)
  (declare (xargs :guard (and (3bits-p aaa) (evex-byte3-p x))))
  (mbe :logic
       (b* ((aaa (mbe :logic (3bits-fix aaa) :exec aaa))
            (x (evex-byte3-fix x)))
         (part-install aaa x :width 3 :low 0))
       :exec (the (unsigned-byte 8)
                  (logior (the (unsigned-byte 8)
                               (logand (the (unsigned-byte 8) x)
                                       (the (signed-byte 4) -8)))
                          (the (unsigned-byte 3) aaa)))))

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

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

Theorem: !evex-byte3->aaa$inline-of-3bits-fix-aaa

(defthm !evex-byte3->aaa$inline-of-3bits-fix-aaa
  (equal (!evex-byte3->aaa$inline (3bits-fix aaa)
                                  x)
         (!evex-byte3->aaa$inline aaa x)))

Theorem: !evex-byte3->aaa$inline-3bits-equiv-congruence-on-aaa

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

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

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

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

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

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

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

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

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

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

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

Function: !evex-byte3->v-prime$inline

(defun !evex-byte3->v-prime$inline (v-prime x)
  (declare (xargs :guard (and (bitp v-prime) (evex-byte3-p x))))
  (mbe :logic
       (b* ((v-prime (mbe :logic (bfix v-prime)
                          :exec v-prime))
            (x (evex-byte3-fix x)))
         (part-install v-prime x
                       :width 1
                       :low 3))
       :exec (the (unsigned-byte 8)
                  (logior (the (unsigned-byte 8)
                               (logand (the (unsigned-byte 8) x)
                                       (the (signed-byte 5) -9)))
                          (the (unsigned-byte 4)
                               (ash (the (unsigned-byte 1) v-prime)
                                    3))))))

Theorem: evex-byte3-p-of-!evex-byte3->v-prime

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

Theorem: !evex-byte3->v-prime$inline-of-bfix-v-prime

(defthm !evex-byte3->v-prime$inline-of-bfix-v-prime
  (equal (!evex-byte3->v-prime$inline (bfix v-prime)
                                      x)
         (!evex-byte3->v-prime$inline v-prime x)))

Theorem: !evex-byte3->v-prime$inline-bit-equiv-congruence-on-v-prime

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

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

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

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

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

Theorem: !evex-byte3->v-prime-is-evex-byte3

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

Theorem: evex-byte3->v-prime-of-!evex-byte3->v-prime

(defthm evex-byte3->v-prime-of-!evex-byte3->v-prime
  (b* ((?new-x (!evex-byte3->v-prime$inline v-prime x)))
    (equal (evex-byte3->v-prime new-x)
           (bfix v-prime))))

Theorem: !evex-byte3->v-prime-equiv-under-mask

(defthm !evex-byte3->v-prime-equiv-under-mask
  (b* ((?new-x (!evex-byte3->v-prime$inline v-prime x)))
    (evex-byte3-equiv-under-mask new-x x -9)))

Function: !evex-byte3->b$inline

(defun !evex-byte3->b$inline (b x)
 (declare (xargs :guard (and (bitp b) (evex-byte3-p x))))
 (mbe :logic
      (b* ((b (mbe :logic (bfix b) :exec b))
           (x (evex-byte3-fix x)))
        (part-install b x :width 1 :low 4))
      :exec (the (unsigned-byte 8)
                 (logior (the (unsigned-byte 8)
                              (logand (the (unsigned-byte 8) x)
                                      (the (signed-byte 6) -17)))
                         (the (unsigned-byte 5)
                              (ash (the (unsigned-byte 1) b) 4))))))

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

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

Theorem: !evex-byte3->b$inline-of-bfix-b

(defthm !evex-byte3->b$inline-of-bfix-b
  (equal (!evex-byte3->b$inline (bfix b) x)
         (!evex-byte3->b$inline b x)))

Theorem: !evex-byte3->b$inline-bit-equiv-congruence-on-b

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

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

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

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

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

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

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

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

(defthm evex-byte3->b-of-!evex-byte3->b
  (b* ((?new-x (!evex-byte3->b$inline b x)))
    (equal (evex-byte3->b new-x) (bfix b))))

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

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

Function: !evex-byte3->vl/rc$inline

(defun !evex-byte3->vl/rc$inline (vl/rc x)
  (declare (xargs :guard (and (2bits-p vl/rc) (evex-byte3-p x))))
  (mbe :logic
       (b* ((vl/rc (mbe :logic (2bits-fix vl/rc)
                        :exec vl/rc))
            (x (evex-byte3-fix x)))
         (part-install vl/rc x :width 2 :low 5))
       :exec (the (unsigned-byte 8)
                  (logior (the (unsigned-byte 8)
                               (logand (the (unsigned-byte 8) x)
                                       (the (signed-byte 8) -97)))
                          (the (unsigned-byte 7)
                               (ash (the (unsigned-byte 2) vl/rc)
                                    5))))))

Theorem: evex-byte3-p-of-!evex-byte3->vl/rc

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

Theorem: !evex-byte3->vl/rc$inline-of-2bits-fix-vl/rc

(defthm !evex-byte3->vl/rc$inline-of-2bits-fix-vl/rc
  (equal (!evex-byte3->vl/rc$inline (2bits-fix vl/rc)
                                    x)
         (!evex-byte3->vl/rc$inline vl/rc x)))

Theorem: !evex-byte3->vl/rc$inline-2bits-equiv-congruence-on-vl/rc

(defthm !evex-byte3->vl/rc$inline-2bits-equiv-congruence-on-vl/rc
  (implies (2bits-equiv vl/rc vl/rc-equiv)
           (equal (!evex-byte3->vl/rc$inline vl/rc x)
                  (!evex-byte3->vl/rc$inline vl/rc-equiv x)))
  :rule-classes :congruence)

Theorem: !evex-byte3->vl/rc$inline-of-evex-byte3-fix-x

(defthm !evex-byte3->vl/rc$inline-of-evex-byte3-fix-x
  (equal (!evex-byte3->vl/rc$inline vl/rc (evex-byte3-fix x))
         (!evex-byte3->vl/rc$inline vl/rc x)))

Theorem: !evex-byte3->vl/rc$inline-evex-byte3-equiv-congruence-on-x

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

Theorem: !evex-byte3->vl/rc-is-evex-byte3

(defthm !evex-byte3->vl/rc-is-evex-byte3
  (equal (!evex-byte3->vl/rc vl/rc x)
         (change-evex-byte3 x :vl/rc vl/rc)))

Theorem: evex-byte3->vl/rc-of-!evex-byte3->vl/rc

(defthm evex-byte3->vl/rc-of-!evex-byte3->vl/rc
  (b* ((?new-x (!evex-byte3->vl/rc$inline vl/rc x)))
    (equal (evex-byte3->vl/rc new-x)
           (2bits-fix vl/rc))))

Theorem: !evex-byte3->vl/rc-equiv-under-mask

(defthm !evex-byte3->vl/rc-equiv-under-mask
  (b* ((?new-x (!evex-byte3->vl/rc$inline vl/rc x)))
    (evex-byte3-equiv-under-mask new-x x -97)))

Function: !evex-byte3->z$inline

(defun !evex-byte3->z$inline (z x)
 (declare (xargs :guard (and (bitp z) (evex-byte3-p x))))
 (mbe :logic
      (b* ((z (mbe :logic (bfix z) :exec z))
           (x (evex-byte3-fix x)))
        (part-install z x :width 1 :low 7))
      :exec (the (unsigned-byte 8)
                 (logior (the (unsigned-byte 8)
                              (logand (the (unsigned-byte 8) x)
                                      (the (signed-byte 9) -129)))
                         (the (unsigned-byte 8)
                              (ash (the (unsigned-byte 1) z) 7))))))

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

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

Theorem: !evex-byte3->z$inline-of-bfix-z

(defthm !evex-byte3->z$inline-of-bfix-z
  (equal (!evex-byte3->z$inline (bfix z) x)
         (!evex-byte3->z$inline z x)))

Theorem: !evex-byte3->z$inline-bit-equiv-congruence-on-z

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

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

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

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

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

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

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

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

(defthm evex-byte3->z-of-!evex-byte3->z
  (b* ((?new-x (!evex-byte3->z$inline z x)))
    (equal (evex-byte3->z new-x) (bfix z))))

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

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

Function: evex-byte3-debug$inline

(defun evex-byte3-debug$inline (x)
  (declare (xargs :guard (evex-byte3-p x)))
  (b* (((evex-byte3 x)))
    (cons (cons 'aaa x.aaa)
          (cons (cons 'v-prime x.v-prime)
                (cons (cons 'b x.b)
                      (cons (cons 'vl/rc x.vl/rc)
                            (cons (cons 'z x.z) nil)))))))

Subtopics

!evex-byte3->v-prime: Update the |X86ISA|::|V-PRIME| field of a evex-byte3 bit structure.
!evex-byte3->vl/rc: Update the |X86ISA|::|VL/RC| field of a evex-byte3 bit structure.
!evex-byte3->aaa: Update the |X86ISA|::|AAA| field of a evex-byte3 bit structure.
!evex-byte3->z: Update the |ACL2|::|Z| field of a evex-byte3 bit structure.
!evex-byte3->b: Update the |ACL2|::|B| field of a evex-byte3 bit structure.
Evex-byte3-p: Recognizer for evex-byte3 bit structures.
Evex-byte3->v-prime: Access the |X86ISA|::|V-PRIME| field of a evex-byte3 bit structure.
Evex-byte3->vl/rc: Access the |X86ISA|::|VL/RC| field of a evex-byte3 bit structure.
Evex-byte3-fix: Fixing function for evex-byte3 bit structures.
Evex-byte3->z: Access the |ACL2|::|Z| field of a evex-byte3 bit structure.
Evex-byte3->b: Access the |ACL2|::|B| field of a evex-byte3 bit structure.
Evex-byte3->aaa: Access the |X86ISA|::|AAA| field of a evex-byte3 bit structure.