Update the |X86ISA|::|MM| field of a evex-byte1 bit structure.
(!evex-byte1->mm mm byte1) → new-byte1
Function:
(defun !evex-byte1->mm$inline (mm byte1) (declare (xargs :guard (and (2bits-p mm) (evex-byte1-p byte1)))) (mbe :logic (b* ((mm (mbe :logic (2bits-fix mm) :exec mm)) (byte1 (evex-byte1-fix byte1))) (part-install mm byte1 :width 2 :low 0)) :exec (the (unsigned-byte 8) (logior (the (unsigned-byte 8) (logand (the (unsigned-byte 8) byte1) (the (signed-byte 3) -4))) (the (unsigned-byte 2) mm)))))
Theorem:
(defthm evex-byte1-p-of-!evex-byte1->mm (b* ((new-byte1 (!evex-byte1->mm$inline mm byte1))) (evex-byte1-p new-byte1)) :rule-classes :rewrite)
Theorem:
(defthm !evex-byte1->mm$inline-of-2bits-fix-mm (equal (!evex-byte1->mm$inline (2bits-fix mm) byte1) (!evex-byte1->mm$inline mm byte1)))
Theorem:
(defthm !evex-byte1->mm$inline-2bits-equiv-congruence-on-mm (implies (2bits-equiv mm mm-equiv) (equal (!evex-byte1->mm$inline mm byte1) (!evex-byte1->mm$inline mm-equiv byte1))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->mm$inline-of-evex-byte1-fix-byte1 (equal (!evex-byte1->mm$inline mm (evex-byte1-fix byte1)) (!evex-byte1->mm$inline mm byte1)))
Theorem:
(defthm !evex-byte1->mm$inline-evex-byte1-equiv-congruence-on-byte1 (implies (evex-byte1-equiv byte1 byte1-equiv) (equal (!evex-byte1->mm$inline mm byte1) (!evex-byte1->mm$inline mm byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->mm-is-evex-byte1 (equal (!evex-byte1->mm mm byte1) (change-evex-byte1 byte1 :mm mm)))
Theorem:
(defthm evex-byte1->mm-of-!evex-byte1->mm (b* ((?new-byte1 (!evex-byte1->mm$inline mm byte1))) (equal (evex-byte1->mm new-byte1) (2bits-fix mm))))
Theorem:
(defthm !evex-byte1->mm-equiv-under-mask (b* ((?new-byte1 (!evex-byte1->mm$inline mm byte1))) (evex-byte1-equiv-under-mask new-byte1 byte1 -4)))