Access the |X86ISA|::|RES| field of a evex-byte1 bit structure.
(evex-byte1->res byte1) → res
Function:
(defun evex-byte1->res$inline (byte1) (declare (xargs :guard (evex-byte1-p byte1))) (mbe :logic (let ((byte1 (evex-byte1-fix byte1))) (part-select byte1 :low 2 :width 2)) :exec (the (unsigned-byte 2) (logand (the (unsigned-byte 2) 3) (the (unsigned-byte 6) (ash (the (unsigned-byte 8) byte1) -2))))))
Theorem:
(defthm 2bits-p-of-evex-byte1->res (b* ((res (evex-byte1->res$inline byte1))) (2bits-p res)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte1->res$inline-of-evex-byte1-fix-byte1 (equal (evex-byte1->res$inline (evex-byte1-fix byte1)) (evex-byte1->res$inline byte1)))
Theorem:
(defthm evex-byte1->res$inline-evex-byte1-equiv-congruence-on-byte1 (implies (evex-byte1-equiv byte1 byte1-equiv) (equal (evex-byte1->res$inline byte1) (evex-byte1->res$inline byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1->res-of-evex-byte1 (equal (evex-byte1->res (evex-byte1 mm res r-prime b x r)) (2bits-fix res)))
Theorem:
(defthm evex-byte1->res-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) 12) 0)) (equal (evex-byte1->res byte1) (evex-byte1->res y))))