		Search-engine friendly clone of the ACL2 documentation.

Evex-byte3

!evex-byte3->v-prime

Update the |X86ISA|::|V-PRIME| field of a evex-byte3 bit structure.

Signature
(!evex-byte3->v-prime v-prime x) → new-x
Arguments: v-prime — Guard (bitp v-prime).; x — Guard (evex-byte3-p x).
Returns: new-x — Type (evex-byte3-p new-x).

Definitions and Theorems

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)))