Access the |X86ISA|::|VL/RC| field of a evex-byte3 bit structure.
(evex-byte3->vl/rc x) → vl/rc
Function:
(defun evex-byte3->vl/rc$inline (x) (declare (xargs :guard (evex-byte3-p x))) (mbe :logic (let ((x (evex-byte3-fix x))) (part-select x :low 5 :width 2)) :exec (the (unsigned-byte 2) (logand (the (unsigned-byte 2) 3) (the (unsigned-byte 3) (ash (the (unsigned-byte 8) x) -5))))))
Theorem:
(defthm 2bits-p-of-evex-byte3->vl/rc (b* ((vl/rc (evex-byte3->vl/rc$inline x))) (2bits-p vl/rc)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte3->vl/rc$inline-of-evex-byte3-fix-x (equal (evex-byte3->vl/rc$inline (evex-byte3-fix x)) (evex-byte3->vl/rc$inline x)))
Theorem:
(defthm evex-byte3->vl/rc$inline-evex-byte3-equiv-congruence-on-x (implies (evex-byte3-equiv x x-equiv) (equal (evex-byte3->vl/rc$inline x) (evex-byte3->vl/rc$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm evex-byte3->vl/rc-of-evex-byte3 (equal (evex-byte3->vl/rc (evex-byte3 aaa v-prime b vl/rc z)) (2bits-fix vl/rc)))
Theorem:
(defthm evex-byte3->vl/rc-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x evex-byte3-equiv-under-mask) (evex-byte3-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 96) 0)) (equal (evex-byte3->vl/rc x) (evex-byte3->vl/rc y))))