Access the |X86ISA|::|MM| field of a evex-byte1 bit structure.
(evex-byte1->mm byte1) → mm
Function:
(defun evex-byte1->mm$inline (byte1) (declare (xargs :guard (evex-byte1-p byte1))) (mbe :logic (let ((byte1 (evex-byte1-fix byte1))) (part-select byte1 :low 0 :width 2)) :exec (the (unsigned-byte 2) (logand (the (unsigned-byte 2) 3) (the (unsigned-byte 8) byte1)))))
Theorem:
(defthm 2bits-p-of-evex-byte1->mm (b* ((mm (evex-byte1->mm$inline byte1))) (2bits-p mm)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte1->mm$inline-of-evex-byte1-fix-byte1 (equal (evex-byte1->mm$inline (evex-byte1-fix byte1)) (evex-byte1->mm$inline 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 byte1) (evex-byte1->mm$inline byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1->mm-of-evex-byte1 (equal (evex-byte1->mm (evex-byte1 mm res r-prime b x r)) (2bits-fix mm)))
Theorem:
(defthm evex-byte1->mm-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps byte1 evex-byte1-equiv-under-mask) (evex-byte1-equiv-under-mask byte1 y fty::mask) (equal (logand (lognot fty::mask) 3) 0)) (equal (evex-byte1->mm byte1) (evex-byte1->mm y))))