		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex3-byte1

An 8-bit unsigned bitstruct type.

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

Fields

m-mmmm — 5bits: 00000: Reserved for future use (will #UD)
00001: implied 0F leading opcode byte 00010: implied 0F 38 leading opcode bytes 00011: implied 0F 3A leading opcode bytes 00100-11111: Reserved for future use (will #UD)
b — bit: REX.B in 1's complement (inverted) form
1 - Same as REX.B=0 (Ignored in 32-bit mode)
0 - Same as REX.B=1 (64-bit mode only)
x — bit: REX.X in 1's complement (inverted) form
1 - Same as REX.X=0 (must be 1 in 32-bit mode)
0 - Same as REX.X=1 (64-bit mode only)
In 32-bit modes, this bit must be set to 1, otherwise the instruction is LES or LDS.
r — bit: REX.R in 1's complement (inverted) form
1 - Same as REX.R=0 (must be 1 in 32-bit mode)
0 - Same as REX.R=1 (64-bit mode only)
In protected and compatibility modes the bit must be set to 1 otherwise the instruction is LES or LDS.

Definitions and Theorems

Function: vex3-byte1-p$inline

(defun vex3-byte1-p$inline (vex3byte1)
  (declare (xargs :guard t))
  (mbe :logic (unsigned-byte-p 8 vex3byte1)
       :exec (and (natp vex3byte1)
                  (< vex3byte1 256))))

Theorem: vex3-byte1-p-when-unsigned-byte-p

(defthm vex3-byte1-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 8 vex3byte1)
           (vex3-byte1-p vex3byte1)))

Theorem: unsigned-byte-p-when-vex3-byte1-p

(defthm unsigned-byte-p-when-vex3-byte1-p
  (implies (vex3-byte1-p vex3byte1)
           (unsigned-byte-p 8 vex3byte1)))

Theorem: vex3-byte1-p-compound-recognizer

(defthm vex3-byte1-p-compound-recognizer
  (implies (vex3-byte1-p vex3byte1)
           (natp vex3byte1))
  :rule-classes :compound-recognizer)

Function: vex3-byte1-fix$inline

(defun vex3-byte1-fix$inline (vex3byte1)
  (declare (xargs :guard (vex3-byte1-p vex3byte1)))
  (mbe :logic (loghead 8 vex3byte1)
       :exec vex3byte1))

Theorem: vex3-byte1-p-of-vex3-byte1-fix

(defthm vex3-byte1-p-of-vex3-byte1-fix
  (b* ((fty::fixed (vex3-byte1-fix$inline vex3byte1)))
    (vex3-byte1-p fty::fixed))
  :rule-classes :rewrite)

Theorem: vex3-byte1-fix-when-vex3-byte1-p

(defthm vex3-byte1-fix-when-vex3-byte1-p
  (implies (vex3-byte1-p vex3byte1)
           (equal (vex3-byte1-fix vex3byte1)
                  vex3byte1)))

Function: vex3-byte1-equiv$inline

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

Theorem: vex3-byte1-equiv-is-an-equivalence

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

Theorem: vex3-byte1-equiv-implies-equal-vex3-byte1-fix-1

(defthm vex3-byte1-equiv-implies-equal-vex3-byte1-fix-1
  (implies (vex3-byte1-equiv x x-equiv)
           (equal (vex3-byte1-fix x)
                  (vex3-byte1-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: vex3-byte1-fix-under-vex3-byte1-equiv

(defthm vex3-byte1-fix-under-vex3-byte1-equiv
  (vex3-byte1-equiv (vex3-byte1-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: vex3-byte1$inline

(defun vex3-byte1$inline (m-mmmm b x r)
  (declare (xargs :guard (and (5bits-p m-mmmm)
                              (bitp b)
                              (bitp x)
                              (bitp r))))
  (b* ((m-mmmm (mbe :logic (5bits-fix m-mmmm)
                    :exec m-mmmm))
       (b (mbe :logic (bfix b) :exec b))
       (x (mbe :logic (bfix x) :exec x))
       (r (mbe :logic (bfix r) :exec r)))
    (logapp 5 m-mmmm (logapp 1 b (logapp 1 x r)))))

Theorem: vex3-byte1-p-of-vex3-byte1

(defthm vex3-byte1-p-of-vex3-byte1
  (b* ((vex3-byte1 (vex3-byte1$inline m-mmmm b x r)))
    (vex3-byte1-p vex3-byte1))
  :rule-classes :rewrite)

Theorem: vex3-byte1$inline-of-5bits-fix-m-mmmm

(defthm vex3-byte1$inline-of-5bits-fix-m-mmmm
  (equal (vex3-byte1$inline (5bits-fix m-mmmm)
                            b x r)
         (vex3-byte1$inline m-mmmm b x r)))

Theorem: vex3-byte1$inline-5bits-equiv-congruence-on-m-mmmm

(defthm vex3-byte1$inline-5bits-equiv-congruence-on-m-mmmm
  (implies (5bits-equiv m-mmmm m-mmmm-equiv)
           (equal (vex3-byte1$inline m-mmmm b x r)
                  (vex3-byte1$inline m-mmmm-equiv b x r)))
  :rule-classes :congruence)

Theorem: vex3-byte1$inline-of-bfix-b

(defthm vex3-byte1$inline-of-bfix-b
  (equal (vex3-byte1$inline m-mmmm (bfix b) x r)
         (vex3-byte1$inline m-mmmm b x r)))

Theorem: vex3-byte1$inline-bit-equiv-congruence-on-b

(defthm vex3-byte1$inline-bit-equiv-congruence-on-b
  (implies (bit-equiv b b-equiv)
           (equal (vex3-byte1$inline m-mmmm b x r)
                  (vex3-byte1$inline m-mmmm b-equiv x r)))
  :rule-classes :congruence)

Theorem: vex3-byte1$inline-of-bfix-x

(defthm vex3-byte1$inline-of-bfix-x
  (equal (vex3-byte1$inline m-mmmm b (bfix x) r)
         (vex3-byte1$inline m-mmmm b x r)))

Theorem: vex3-byte1$inline-bit-equiv-congruence-on-x

(defthm vex3-byte1$inline-bit-equiv-congruence-on-x
  (implies (bit-equiv x x-equiv)
           (equal (vex3-byte1$inline m-mmmm b x r)
                  (vex3-byte1$inline m-mmmm b x-equiv r)))
  :rule-classes :congruence)

Theorem: vex3-byte1$inline-of-bfix-r

(defthm vex3-byte1$inline-of-bfix-r
  (equal (vex3-byte1$inline m-mmmm b x (bfix r))
         (vex3-byte1$inline m-mmmm b x r)))

Theorem: vex3-byte1$inline-bit-equiv-congruence-on-r

(defthm vex3-byte1$inline-bit-equiv-congruence-on-r
  (implies (bit-equiv r r-equiv)
           (equal (vex3-byte1$inline m-mmmm b x r)
                  (vex3-byte1$inline m-mmmm b x r-equiv)))
  :rule-classes :congruence)

Function: vex3-byte1-equiv-under-mask$inline

(defun vex3-byte1-equiv-under-mask$inline
       (vex3byte1 vex3byte11 mask)
  (declare (xargs :guard (and (vex3-byte1-p vex3byte1)
                              (vex3-byte1-p vex3byte11)
                              (integerp mask))))
  (fty::int-equiv-under-mask (vex3-byte1-fix vex3byte1)
                             (vex3-byte1-fix vex3byte11)
                             mask))

Function: vex3-byte1->m-mmmm$inline

(defun vex3-byte1->m-mmmm$inline (vex3byte1)
  (declare (xargs :guard (vex3-byte1-p vex3byte1)))
  (mbe :logic
       (let ((vex3byte1 (vex3-byte1-fix vex3byte1)))
         (part-select vex3byte1 :low 0 :width 5))
       :exec (the (unsigned-byte 5)
                  (logand (the (unsigned-byte 5) 31)
                          (the (unsigned-byte 8) vex3byte1)))))

Theorem: 5bits-p-of-vex3-byte1->m-mmmm

(defthm 5bits-p-of-vex3-byte1->m-mmmm
  (b* ((m-mmmm (vex3-byte1->m-mmmm$inline vex3byte1)))
    (5bits-p m-mmmm))
  :rule-classes :rewrite)

Theorem: vex3-byte1->m-mmmm$inline-of-vex3-byte1-fix-vex3byte1

(defthm vex3-byte1->m-mmmm$inline-of-vex3-byte1-fix-vex3byte1
  (equal (vex3-byte1->m-mmmm$inline (vex3-byte1-fix vex3byte1))
         (vex3-byte1->m-mmmm$inline vex3byte1)))

Theorem: vex3-byte1->m-mmmm$inline-vex3-byte1-equiv-congruence-on-vex3byte1

(defthm
 vex3-byte1->m-mmmm$inline-vex3-byte1-equiv-congruence-on-vex3byte1
 (implies (vex3-byte1-equiv vex3byte1 vex3byte1-equiv)
          (equal (vex3-byte1->m-mmmm$inline vex3byte1)
                 (vex3-byte1->m-mmmm$inline vex3byte1-equiv)))
 :rule-classes :congruence)

Theorem: vex3-byte1->m-mmmm-of-vex3-byte1

(defthm vex3-byte1->m-mmmm-of-vex3-byte1
  (equal (vex3-byte1->m-mmmm (vex3-byte1 m-mmmm b x r))
         (5bits-fix m-mmmm)))

Theorem: vex3-byte1->m-mmmm-of-write-with-mask

(defthm vex3-byte1->m-mmmm-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     vex3byte1 vex3-byte1-equiv-under-mask)
                (vex3-byte1-equiv-under-mask vex3byte1 y fty::mask)
                (equal (logand (lognot fty::mask) 31)
                       0))
           (equal (vex3-byte1->m-mmmm vex3byte1)
                  (vex3-byte1->m-mmmm y))))

Function: vex3-byte1->b$inline

(defun vex3-byte1->b$inline (vex3byte1)
 (declare (xargs :guard (vex3-byte1-p vex3byte1)))
 (mbe :logic
      (let ((vex3byte1 (vex3-byte1-fix vex3byte1)))
        (part-select vex3byte1 :low 5 :width 1))
      :exec (the (unsigned-byte 1)
                 (logand (the (unsigned-byte 1) 1)
                         (the (unsigned-byte 3)
                              (ash (the (unsigned-byte 8) vex3byte1)
                                   -5))))))

Theorem: bitp-of-vex3-byte1->b

(defthm bitp-of-vex3-byte1->b
  (b* ((b (vex3-byte1->b$inline vex3byte1)))
    (bitp b))
  :rule-classes :rewrite)

Theorem: vex3-byte1->b$inline-of-vex3-byte1-fix-vex3byte1

(defthm vex3-byte1->b$inline-of-vex3-byte1-fix-vex3byte1
  (equal (vex3-byte1->b$inline (vex3-byte1-fix vex3byte1))
         (vex3-byte1->b$inline vex3byte1)))

Theorem: vex3-byte1->b$inline-vex3-byte1-equiv-congruence-on-vex3byte1

(defthm
      vex3-byte1->b$inline-vex3-byte1-equiv-congruence-on-vex3byte1
  (implies (vex3-byte1-equiv vex3byte1 vex3byte1-equiv)
           (equal (vex3-byte1->b$inline vex3byte1)
                  (vex3-byte1->b$inline vex3byte1-equiv)))
  :rule-classes :congruence)

Theorem: vex3-byte1->b-of-vex3-byte1

(defthm vex3-byte1->b-of-vex3-byte1
  (equal (vex3-byte1->b (vex3-byte1 m-mmmm b x r))
         (bfix b)))

Theorem: vex3-byte1->b-of-write-with-mask

(defthm vex3-byte1->b-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     vex3byte1 vex3-byte1-equiv-under-mask)
                (vex3-byte1-equiv-under-mask vex3byte1 y fty::mask)
                (equal (logand (lognot fty::mask) 32)
                       0))
           (equal (vex3-byte1->b vex3byte1)
                  (vex3-byte1->b y))))

Function: vex3-byte1->x$inline

(defun vex3-byte1->x$inline (vex3byte1)
 (declare (xargs :guard (vex3-byte1-p vex3byte1)))
 (mbe :logic
      (let ((vex3byte1 (vex3-byte1-fix vex3byte1)))
        (part-select vex3byte1 :low 6 :width 1))
      :exec (the (unsigned-byte 1)
                 (logand (the (unsigned-byte 1) 1)
                         (the (unsigned-byte 2)
                              (ash (the (unsigned-byte 8) vex3byte1)
                                   -6))))))

Theorem: bitp-of-vex3-byte1->x

(defthm bitp-of-vex3-byte1->x
  (b* ((x (vex3-byte1->x$inline vex3byte1)))
    (bitp x))
  :rule-classes :rewrite)

Theorem: vex3-byte1->x$inline-of-vex3-byte1-fix-vex3byte1

(defthm vex3-byte1->x$inline-of-vex3-byte1-fix-vex3byte1
  (equal (vex3-byte1->x$inline (vex3-byte1-fix vex3byte1))
         (vex3-byte1->x$inline vex3byte1)))

Theorem: vex3-byte1->x$inline-vex3-byte1-equiv-congruence-on-vex3byte1

(defthm
      vex3-byte1->x$inline-vex3-byte1-equiv-congruence-on-vex3byte1
  (implies (vex3-byte1-equiv vex3byte1 vex3byte1-equiv)
           (equal (vex3-byte1->x$inline vex3byte1)
                  (vex3-byte1->x$inline vex3byte1-equiv)))
  :rule-classes :congruence)

Theorem: vex3-byte1->x-of-vex3-byte1

(defthm vex3-byte1->x-of-vex3-byte1
  (equal (vex3-byte1->x (vex3-byte1 m-mmmm b x r))
         (bfix x)))

Theorem: vex3-byte1->x-of-write-with-mask

(defthm vex3-byte1->x-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     vex3byte1 vex3-byte1-equiv-under-mask)
                (vex3-byte1-equiv-under-mask vex3byte1 y fty::mask)
                (equal (logand (lognot fty::mask) 64)
                       0))
           (equal (vex3-byte1->x vex3byte1)
                  (vex3-byte1->x y))))

Function: vex3-byte1->r$inline

(defun vex3-byte1->r$inline (vex3byte1)
 (declare (xargs :guard (vex3-byte1-p vex3byte1)))
 (mbe :logic
      (let ((vex3byte1 (vex3-byte1-fix vex3byte1)))
        (part-select vex3byte1 :low 7 :width 1))
      :exec (the (unsigned-byte 1)
                 (logand (the (unsigned-byte 1) 1)
                         (the (unsigned-byte 1)
                              (ash (the (unsigned-byte 8) vex3byte1)
                                   -7))))))

Theorem: bitp-of-vex3-byte1->r

(defthm bitp-of-vex3-byte1->r
  (b* ((r (vex3-byte1->r$inline vex3byte1)))
    (bitp r))
  :rule-classes :rewrite)

Theorem: vex3-byte1->r$inline-of-vex3-byte1-fix-vex3byte1

(defthm vex3-byte1->r$inline-of-vex3-byte1-fix-vex3byte1
  (equal (vex3-byte1->r$inline (vex3-byte1-fix vex3byte1))
         (vex3-byte1->r$inline vex3byte1)))

Theorem: vex3-byte1->r$inline-vex3-byte1-equiv-congruence-on-vex3byte1

(defthm
      vex3-byte1->r$inline-vex3-byte1-equiv-congruence-on-vex3byte1
  (implies (vex3-byte1-equiv vex3byte1 vex3byte1-equiv)
           (equal (vex3-byte1->r$inline vex3byte1)
                  (vex3-byte1->r$inline vex3byte1-equiv)))
  :rule-classes :congruence)

Theorem: vex3-byte1->r-of-vex3-byte1

(defthm vex3-byte1->r-of-vex3-byte1
  (equal (vex3-byte1->r (vex3-byte1 m-mmmm b x r))
         (bfix r)))

Theorem: vex3-byte1->r-of-write-with-mask

(defthm vex3-byte1->r-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     vex3byte1 vex3-byte1-equiv-under-mask)
                (vex3-byte1-equiv-under-mask vex3byte1 y fty::mask)
                (equal (logand (lognot fty::mask) 128)
                       0))
           (equal (vex3-byte1->r vex3byte1)
                  (vex3-byte1->r y))))

Theorem: vex3-byte1-fix-in-terms-of-vex3-byte1

(defthm vex3-byte1-fix-in-terms-of-vex3-byte1
  (equal (vex3-byte1-fix vex3byte1)
         (change-vex3-byte1 vex3byte1)))

Function: !vex3-byte1->m-mmmm$inline

(defun !vex3-byte1->m-mmmm$inline (m-mmmm vex3byte1)
 (declare (xargs :guard (and (5bits-p m-mmmm)
                             (vex3-byte1-p vex3byte1))))
 (mbe
   :logic
   (b* ((m-mmmm (mbe :logic (5bits-fix m-mmmm)
                     :exec m-mmmm))
        (vex3byte1 (vex3-byte1-fix vex3byte1)))
     (part-install m-mmmm vex3byte1
                   :width 5
                   :low 0))
   :exec (the (unsigned-byte 8)
              (logior (the (unsigned-byte 8)
                           (logand (the (unsigned-byte 8) vex3byte1)
                                   (the (signed-byte 6) -32)))
                      (the (unsigned-byte 5) m-mmmm)))))

Theorem: vex3-byte1-p-of-!vex3-byte1->m-mmmm

(defthm vex3-byte1-p-of-!vex3-byte1->m-mmmm
 (b* ((new-vex3byte1 (!vex3-byte1->m-mmmm$inline m-mmmm vex3byte1)))
   (vex3-byte1-p new-vex3byte1))
 :rule-classes :rewrite)

Theorem: !vex3-byte1->m-mmmm$inline-of-5bits-fix-m-mmmm

(defthm !vex3-byte1->m-mmmm$inline-of-5bits-fix-m-mmmm
  (equal (!vex3-byte1->m-mmmm$inline (5bits-fix m-mmmm)
                                     vex3byte1)
         (!vex3-byte1->m-mmmm$inline m-mmmm vex3byte1)))

Theorem: !vex3-byte1->m-mmmm$inline-5bits-equiv-congruence-on-m-mmmm

(defthm !vex3-byte1->m-mmmm$inline-5bits-equiv-congruence-on-m-mmmm
  (implies
       (5bits-equiv m-mmmm m-mmmm-equiv)
       (equal (!vex3-byte1->m-mmmm$inline m-mmmm vex3byte1)
              (!vex3-byte1->m-mmmm$inline m-mmmm-equiv vex3byte1)))
  :rule-classes :congruence)

Theorem: !vex3-byte1->m-mmmm$inline-of-vex3-byte1-fix-vex3byte1

(defthm !vex3-byte1->m-mmmm$inline-of-vex3-byte1-fix-vex3byte1
 (equal
      (!vex3-byte1->m-mmmm$inline m-mmmm (vex3-byte1-fix vex3byte1))
      (!vex3-byte1->m-mmmm$inline m-mmmm vex3byte1)))

Theorem: !vex3-byte1->m-mmmm$inline-vex3-byte1-equiv-congruence-on-vex3byte1

(defthm
 !vex3-byte1->m-mmmm$inline-vex3-byte1-equiv-congruence-on-vex3byte1
 (implies
      (vex3-byte1-equiv vex3byte1 vex3byte1-equiv)
      (equal (!vex3-byte1->m-mmmm$inline m-mmmm vex3byte1)
             (!vex3-byte1->m-mmmm$inline m-mmmm vex3byte1-equiv)))
 :rule-classes :congruence)

Theorem: !vex3-byte1->m-mmmm-is-vex3-byte1

(defthm !vex3-byte1->m-mmmm-is-vex3-byte1
  (equal (!vex3-byte1->m-mmmm m-mmmm vex3byte1)
         (change-vex3-byte1 vex3byte1
                            :m-mmmm m-mmmm)))

Theorem: vex3-byte1->m-mmmm-of-!vex3-byte1->m-mmmm

(defthm vex3-byte1->m-mmmm-of-!vex3-byte1->m-mmmm
  (b*
    ((?new-vex3byte1 (!vex3-byte1->m-mmmm$inline m-mmmm vex3byte1)))
    (equal (vex3-byte1->m-mmmm new-vex3byte1)
           (5bits-fix m-mmmm))))

Theorem: !vex3-byte1->m-mmmm-equiv-under-mask

(defthm !vex3-byte1->m-mmmm-equiv-under-mask
  (b*
    ((?new-vex3byte1 (!vex3-byte1->m-mmmm$inline m-mmmm vex3byte1)))
    (vex3-byte1-equiv-under-mask new-vex3byte1 vex3byte1 -32)))

Function: !vex3-byte1->b$inline

(defun !vex3-byte1->b$inline (b vex3byte1)
 (declare (xargs :guard (and (bitp b)
                             (vex3-byte1-p vex3byte1))))
 (mbe
   :logic
   (b* ((b (mbe :logic (bfix b) :exec b))
        (vex3byte1 (vex3-byte1-fix vex3byte1)))
     (part-install b vex3byte1
                   :width 1
                   :low 5))
   :exec (the (unsigned-byte 8)
              (logior (the (unsigned-byte 8)
                           (logand (the (unsigned-byte 8) vex3byte1)
                                   (the (signed-byte 7) -33)))
                      (the (unsigned-byte 6)
                           (ash (the (unsigned-byte 1) b) 5))))))

Theorem: vex3-byte1-p-of-!vex3-byte1->b

(defthm vex3-byte1-p-of-!vex3-byte1->b
  (b* ((new-vex3byte1 (!vex3-byte1->b$inline b vex3byte1)))
    (vex3-byte1-p new-vex3byte1))
  :rule-classes :rewrite)

Theorem: !vex3-byte1->b$inline-of-bfix-b

(defthm !vex3-byte1->b$inline-of-bfix-b
  (equal (!vex3-byte1->b$inline (bfix b)
                                vex3byte1)
         (!vex3-byte1->b$inline b vex3byte1)))

Theorem: !vex3-byte1->b$inline-bit-equiv-congruence-on-b

(defthm !vex3-byte1->b$inline-bit-equiv-congruence-on-b
  (implies (bit-equiv b b-equiv)
           (equal (!vex3-byte1->b$inline b vex3byte1)
                  (!vex3-byte1->b$inline b-equiv vex3byte1)))
  :rule-classes :congruence)

Theorem: !vex3-byte1->b$inline-of-vex3-byte1-fix-vex3byte1

(defthm !vex3-byte1->b$inline-of-vex3-byte1-fix-vex3byte1
  (equal (!vex3-byte1->b$inline b (vex3-byte1-fix vex3byte1))
         (!vex3-byte1->b$inline b vex3byte1)))

Theorem: !vex3-byte1->b$inline-vex3-byte1-equiv-congruence-on-vex3byte1

(defthm
     !vex3-byte1->b$inline-vex3-byte1-equiv-congruence-on-vex3byte1
  (implies (vex3-byte1-equiv vex3byte1 vex3byte1-equiv)
           (equal (!vex3-byte1->b$inline b vex3byte1)
                  (!vex3-byte1->b$inline b vex3byte1-equiv)))
  :rule-classes :congruence)

Theorem: !vex3-byte1->b-is-vex3-byte1

(defthm !vex3-byte1->b-is-vex3-byte1
  (equal (!vex3-byte1->b b vex3byte1)
         (change-vex3-byte1 vex3byte1 :b b)))

Theorem: vex3-byte1->b-of-!vex3-byte1->b

(defthm vex3-byte1->b-of-!vex3-byte1->b
  (b* ((?new-vex3byte1 (!vex3-byte1->b$inline b vex3byte1)))
    (equal (vex3-byte1->b new-vex3byte1)
           (bfix b))))

Theorem: !vex3-byte1->b-equiv-under-mask

(defthm !vex3-byte1->b-equiv-under-mask
  (b* ((?new-vex3byte1 (!vex3-byte1->b$inline b vex3byte1)))
    (vex3-byte1-equiv-under-mask new-vex3byte1 vex3byte1 -33)))

Function: !vex3-byte1->x$inline

(defun !vex3-byte1->x$inline (x vex3byte1)
 (declare (xargs :guard (and (bitp x)
                             (vex3-byte1-p vex3byte1))))
 (mbe
   :logic
   (b* ((x (mbe :logic (bfix x) :exec x))
        (vex3byte1 (vex3-byte1-fix vex3byte1)))
     (part-install x vex3byte1
                   :width 1
                   :low 6))
   :exec (the (unsigned-byte 8)
              (logior (the (unsigned-byte 8)
                           (logand (the (unsigned-byte 8) vex3byte1)
                                   (the (signed-byte 8) -65)))
                      (the (unsigned-byte 7)
                           (ash (the (unsigned-byte 1) x) 6))))))

Theorem: vex3-byte1-p-of-!vex3-byte1->x

(defthm vex3-byte1-p-of-!vex3-byte1->x
  (b* ((new-vex3byte1 (!vex3-byte1->x$inline x vex3byte1)))
    (vex3-byte1-p new-vex3byte1))
  :rule-classes :rewrite)

Theorem: !vex3-byte1->x$inline-of-bfix-x

(defthm !vex3-byte1->x$inline-of-bfix-x
  (equal (!vex3-byte1->x$inline (bfix x)
                                vex3byte1)
         (!vex3-byte1->x$inline x vex3byte1)))

Theorem: !vex3-byte1->x$inline-bit-equiv-congruence-on-x

(defthm !vex3-byte1->x$inline-bit-equiv-congruence-on-x
  (implies (bit-equiv x x-equiv)
           (equal (!vex3-byte1->x$inline x vex3byte1)
                  (!vex3-byte1->x$inline x-equiv vex3byte1)))
  :rule-classes :congruence)

Theorem: !vex3-byte1->x$inline-of-vex3-byte1-fix-vex3byte1

(defthm !vex3-byte1->x$inline-of-vex3-byte1-fix-vex3byte1
  (equal (!vex3-byte1->x$inline x (vex3-byte1-fix vex3byte1))
         (!vex3-byte1->x$inline x vex3byte1)))

Theorem: !vex3-byte1->x$inline-vex3-byte1-equiv-congruence-on-vex3byte1

(defthm
     !vex3-byte1->x$inline-vex3-byte1-equiv-congruence-on-vex3byte1
  (implies (vex3-byte1-equiv vex3byte1 vex3byte1-equiv)
           (equal (!vex3-byte1->x$inline x vex3byte1)
                  (!vex3-byte1->x$inline x vex3byte1-equiv)))
  :rule-classes :congruence)

Theorem: !vex3-byte1->x-is-vex3-byte1

(defthm !vex3-byte1->x-is-vex3-byte1
  (equal (!vex3-byte1->x x vex3byte1)
         (change-vex3-byte1 vex3byte1 :x x)))

Theorem: vex3-byte1->x-of-!vex3-byte1->x

(defthm vex3-byte1->x-of-!vex3-byte1->x
  (b* ((?new-vex3byte1 (!vex3-byte1->x$inline x vex3byte1)))
    (equal (vex3-byte1->x new-vex3byte1)
           (bfix x))))

Theorem: !vex3-byte1->x-equiv-under-mask

(defthm !vex3-byte1->x-equiv-under-mask
  (b* ((?new-vex3byte1 (!vex3-byte1->x$inline x vex3byte1)))
    (vex3-byte1-equiv-under-mask new-vex3byte1 vex3byte1 -65)))

Function: !vex3-byte1->r$inline

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

Theorem: vex3-byte1-p-of-!vex3-byte1->r

(defthm vex3-byte1-p-of-!vex3-byte1->r
  (b* ((new-vex3byte1 (!vex3-byte1->r$inline r vex3byte1)))
    (vex3-byte1-p new-vex3byte1))
  :rule-classes :rewrite)

Theorem: !vex3-byte1->r$inline-of-bfix-r

(defthm !vex3-byte1->r$inline-of-bfix-r
  (equal (!vex3-byte1->r$inline (bfix r)
                                vex3byte1)
         (!vex3-byte1->r$inline r vex3byte1)))

Theorem: !vex3-byte1->r$inline-bit-equiv-congruence-on-r

(defthm !vex3-byte1->r$inline-bit-equiv-congruence-on-r
  (implies (bit-equiv r r-equiv)
           (equal (!vex3-byte1->r$inline r vex3byte1)
                  (!vex3-byte1->r$inline r-equiv vex3byte1)))
  :rule-classes :congruence)

Theorem: !vex3-byte1->r$inline-of-vex3-byte1-fix-vex3byte1

(defthm !vex3-byte1->r$inline-of-vex3-byte1-fix-vex3byte1
  (equal (!vex3-byte1->r$inline r (vex3-byte1-fix vex3byte1))
         (!vex3-byte1->r$inline r vex3byte1)))

Theorem: !vex3-byte1->r$inline-vex3-byte1-equiv-congruence-on-vex3byte1

(defthm
     !vex3-byte1->r$inline-vex3-byte1-equiv-congruence-on-vex3byte1
  (implies (vex3-byte1-equiv vex3byte1 vex3byte1-equiv)
           (equal (!vex3-byte1->r$inline r vex3byte1)
                  (!vex3-byte1->r$inline r vex3byte1-equiv)))
  :rule-classes :congruence)

Theorem: !vex3-byte1->r-is-vex3-byte1

(defthm !vex3-byte1->r-is-vex3-byte1
  (equal (!vex3-byte1->r r vex3byte1)
         (change-vex3-byte1 vex3byte1 :r r)))

Theorem: vex3-byte1->r-of-!vex3-byte1->r

(defthm vex3-byte1->r-of-!vex3-byte1->r
  (b* ((?new-vex3byte1 (!vex3-byte1->r$inline r vex3byte1)))
    (equal (vex3-byte1->r new-vex3byte1)
           (bfix r))))

Theorem: !vex3-byte1->r-equiv-under-mask

(defthm !vex3-byte1->r-equiv-under-mask
  (b* ((?new-vex3byte1 (!vex3-byte1->r$inline r vex3byte1)))
    (vex3-byte1-equiv-under-mask new-vex3byte1 vex3byte1 127)))

Function: vex3-byte1-debug$inline

(defun vex3-byte1-debug$inline (vex3byte1)
  (declare (xargs :guard (vex3-byte1-p vex3byte1)))
  (b* (((vex3-byte1 vex3byte1)))
    (cons (cons 'm-mmmm vex3byte1.m-mmmm)
          (cons (cons 'b vex3byte1.b)
                (cons (cons 'x vex3byte1.x)
                      (cons (cons 'r vex3byte1.r) nil))))))

Subtopics

!vex3-byte1->m-mmmm: Update the |X86ISA|::|M-MMMM| field of a vex3-byte1 bit structure.
!vex3-byte1->x: Update the |ACL2|::|X| field of a vex3-byte1 bit structure.
!vex3-byte1->r: Update the |ACL2|::|R| field of a vex3-byte1 bit structure.
!vex3-byte1->b: Update the |ACL2|::|B| field of a vex3-byte1 bit structure.
Vex3-byte1-p: Recognizer for vex3-byte1 bit structures.
Vex3-byte1->m-mmmm: Access the |X86ISA|::|M-MMMM| field of a vex3-byte1 bit structure.
Vex3-byte1->x: Access the |ACL2|::|X| field of a vex3-byte1 bit structure.
Vex3-byte1->r: Access the |ACL2|::|R| field of a vex3-byte1 bit structure.
Vex3-byte1->b: Access the |ACL2|::|B| field of a vex3-byte1 bit structure.
Vex3-byte1-fix: Fixing function for vex3-byte1 bit structures.