		Search-engine friendly clone of the ACL2 documentation.

Evex-byte1

!evex-byte1->r-prime

Update the |X86ISA|::|R-PRIME| field of a evex-byte1 bit structure.

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

Definitions and Theorems

Function: !evex-byte1->r-prime$inline

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

Theorem: evex-byte1-p-of-!evex-byte1->r-prime

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

Theorem: !evex-byte1->r-prime$inline-of-bfix-r-prime

(defthm !evex-byte1->r-prime$inline-of-bfix-r-prime
  (equal (!evex-byte1->r-prime$inline (bfix r-prime)
                                      byte1)
         (!evex-byte1->r-prime$inline r-prime byte1)))

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

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

Theorem: !evex-byte1->r-prime$inline-of-evex-byte1-fix-byte1

(defthm !evex-byte1->r-prime$inline-of-evex-byte1-fix-byte1
 (equal (!evex-byte1->r-prime$inline r-prime (evex-byte1-fix byte1))
        (!evex-byte1->r-prime$inline r-prime byte1)))

Theorem: !evex-byte1->r-prime$inline-evex-byte1-equiv-congruence-on-byte1

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

Theorem: !evex-byte1->r-prime-is-evex-byte1

(defthm !evex-byte1->r-prime-is-evex-byte1
  (equal (!evex-byte1->r-prime r-prime byte1)
         (change-evex-byte1 byte1
                            :r-prime r-prime)))

Theorem: evex-byte1->r-prime-of-!evex-byte1->r-prime

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

Theorem: !evex-byte1->r-prime-equiv-under-mask

(defthm !evex-byte1->r-prime-equiv-under-mask
  (b* ((?new-byte1 (!evex-byte1->r-prime$inline r-prime byte1)))
    (evex-byte1-equiv-under-mask new-byte1 byte1 -17)))