Access the |X86ISA|::|R-PRIME| field of a evex-byte1 bit structure.
(evex-byte1->r-prime byte1) → r-prime
Function:
(defun evex-byte1->r-prime$inline (byte1) (declare (xargs :guard (evex-byte1-p byte1))) (mbe :logic (let ((byte1 (evex-byte1-fix byte1))) (part-select byte1 :low 4 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 4) (ash (the (unsigned-byte 8) byte1) -4))))))
Theorem:
(defthm bitp-of-evex-byte1->r-prime (b* ((r-prime (evex-byte1->r-prime$inline byte1))) (bitp r-prime)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte1->r-prime$inline-of-evex-byte1-fix-byte1 (equal (evex-byte1->r-prime$inline (evex-byte1-fix byte1)) (evex-byte1->r-prime$inline byte1)))
Theorem:
(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 byte1) (evex-byte1->r-prime$inline byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1->r-prime-of-evex-byte1 (equal (evex-byte1->r-prime (evex-byte1 mmm res r-prime b x r)) (bfix r-prime)))
Theorem:
(defthm evex-byte1->r-prime-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) 16) 0)) (equal (evex-byte1->r-prime byte1) (evex-byte1->r-prime y))))