		Search-engine friendly clone of the ACL2 documentation.

Evex-byte1

!evex-byte1->res

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

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

Definitions and Theorems

Function: !evex-byte1->res$inline

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

Theorem: evex-byte1-p-of-!evex-byte1->res

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

Theorem: !evex-byte1->res$inline-of-bfix-res

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

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

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

Theorem: !evex-byte1->res$inline-of-evex-byte1-fix-byte1

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

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

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

Theorem: !evex-byte1->res-is-evex-byte1

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

Theorem: evex-byte1->res-of-!evex-byte1->res

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

Theorem: !evex-byte1->res-equiv-under-mask

(defthm !evex-byte1->res-equiv-under-mask
  (b* ((?new-byte1 (!evex-byte1->res$inline res byte1)))
    (evex-byte1-equiv-under-mask new-byte1 byte1 -9)))