An 8-bit unsigned bitstruct type.
This is a bitstruct type introduced by defbitstruct, represented as a unsigned 8-bit integer.
Function:
(defun evex-byte1-p$inline (byte1) (declare (xargs :guard t)) (mbe :logic (unsigned-byte-p 8 byte1) :exec (and (natp byte1) (< byte1 256))))
Theorem:
(defthm evex-byte1-p-when-unsigned-byte-p (implies (unsigned-byte-p 8 byte1) (evex-byte1-p byte1)))
Theorem:
(defthm unsigned-byte-p-when-evex-byte1-p (implies (evex-byte1-p byte1) (unsigned-byte-p 8 byte1)))
Theorem:
(defthm evex-byte1-p-compound-recognizer (implies (evex-byte1-p byte1) (natp byte1)) :rule-classes :compound-recognizer)
Function:
(defun evex-byte1-fix$inline (byte1) (declare (xargs :guard (evex-byte1-p byte1))) (mbe :logic (loghead 8 byte1) :exec byte1))
Theorem:
(defthm evex-byte1-p-of-evex-byte1-fix (b* ((fty::fixed (evex-byte1-fix$inline byte1))) (evex-byte1-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte1-fix-when-evex-byte1-p (implies (evex-byte1-p byte1) (equal (evex-byte1-fix byte1) byte1)))
Function:
(defun evex-byte1-equiv$inline (x y) (declare (xargs :guard (and (evex-byte1-p x) (evex-byte1-p y)))) (equal (evex-byte1-fix x) (evex-byte1-fix y)))
Theorem:
(defthm evex-byte1-equiv-is-an-equivalence (and (booleanp (evex-byte1-equiv x y)) (evex-byte1-equiv x x) (implies (evex-byte1-equiv x y) (evex-byte1-equiv y x)) (implies (and (evex-byte1-equiv x y) (evex-byte1-equiv y z)) (evex-byte1-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm evex-byte1-equiv-implies-equal-evex-byte1-fix-1 (implies (evex-byte1-equiv x x-equiv) (equal (evex-byte1-fix x) (evex-byte1-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm evex-byte1-fix-under-evex-byte1-equiv (evex-byte1-equiv (evex-byte1-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Function:
(defun evex-byte1$inline (mm res r-prime b x r) (declare (xargs :guard (and (2bits-p mm) (2bits-p res) (bitp r-prime) (bitp b) (bitp x) (bitp r)))) (b* ((mm (mbe :logic (2bits-fix mm) :exec mm)) (res (mbe :logic (2bits-fix res) :exec res)) (r-prime (mbe :logic (bfix r-prime) :exec r-prime)) (b (mbe :logic (bfix b) :exec b)) (x (mbe :logic (bfix x) :exec x)) (r (mbe :logic (bfix r) :exec r))) (logapp 2 mm (logapp 2 res (logapp 1 r-prime (logapp 1 b (logapp 1 x r)))))))
Theorem:
(defthm evex-byte1-p-of-evex-byte1 (b* ((evex-byte1 (evex-byte1$inline mm res r-prime b x r))) (evex-byte1-p evex-byte1)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte1$inline-of-2bits-fix-mm (equal (evex-byte1$inline (2bits-fix mm) res r-prime b x r) (evex-byte1$inline mm res r-prime b x r)))
Theorem:
(defthm evex-byte1$inline-2bits-equiv-congruence-on-mm (implies (2bits-equiv mm mm-equiv) (equal (evex-byte1$inline mm res r-prime b x r) (evex-byte1$inline mm-equiv res r-prime b x r))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1$inline-of-2bits-fix-res (equal (evex-byte1$inline mm (2bits-fix res) r-prime b x r) (evex-byte1$inline mm res r-prime b x r)))
Theorem:
(defthm evex-byte1$inline-2bits-equiv-congruence-on-res (implies (2bits-equiv res res-equiv) (equal (evex-byte1$inline mm res r-prime b x r) (evex-byte1$inline mm res-equiv r-prime b x r))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1$inline-of-bfix-r-prime (equal (evex-byte1$inline mm res (bfix r-prime) b x r) (evex-byte1$inline mm res r-prime b x r)))
Theorem:
(defthm evex-byte1$inline-bit-equiv-congruence-on-r-prime (implies (bit-equiv r-prime r-prime-equiv) (equal (evex-byte1$inline mm res r-prime b x r) (evex-byte1$inline mm res r-prime-equiv b x r))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1$inline-of-bfix-b (equal (evex-byte1$inline mm res r-prime (bfix b) x r) (evex-byte1$inline mm res r-prime b x r)))
Theorem:
(defthm evex-byte1$inline-bit-equiv-congruence-on-b (implies (bit-equiv b b-equiv) (equal (evex-byte1$inline mm res r-prime b x r) (evex-byte1$inline mm res r-prime b-equiv x r))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1$inline-of-bfix-x (equal (evex-byte1$inline mm res r-prime b (bfix x) r) (evex-byte1$inline mm res r-prime b x r)))
Theorem:
(defthm evex-byte1$inline-bit-equiv-congruence-on-x (implies (bit-equiv x x-equiv) (equal (evex-byte1$inline mm res r-prime b x r) (evex-byte1$inline mm res r-prime b x-equiv r))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1$inline-of-bfix-r (equal (evex-byte1$inline mm res r-prime b x (bfix r)) (evex-byte1$inline mm res r-prime b x r)))
Theorem:
(defthm evex-byte1$inline-bit-equiv-congruence-on-r (implies (bit-equiv r r-equiv) (equal (evex-byte1$inline mm res r-prime b x r) (evex-byte1$inline mm res r-prime b x r-equiv))) :rule-classes :congruence)
Function:
(defun evex-byte1-equiv-under-mask$inline (byte1 byte11 mask) (declare (xargs :guard (and (evex-byte1-p byte1) (evex-byte1-p byte11) (integerp mask)))) (fty::int-equiv-under-mask (evex-byte1-fix byte1) (evex-byte1-fix byte11) mask))
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))))
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))))
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 mm 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))))
Function:
(defun evex-byte1->b$inline (byte1) (declare (xargs :guard (evex-byte1-p byte1))) (mbe :logic (let ((byte1 (evex-byte1-fix byte1))) (part-select byte1 :low 5 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 3) (ash (the (unsigned-byte 8) byte1) -5))))))
Theorem:
(defthm bitp-of-evex-byte1->b (b* ((b (evex-byte1->b$inline byte1))) (bitp b)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte1->b$inline-of-evex-byte1-fix-byte1 (equal (evex-byte1->b$inline (evex-byte1-fix byte1)) (evex-byte1->b$inline byte1)))
Theorem:
(defthm evex-byte1->b$inline-evex-byte1-equiv-congruence-on-byte1 (implies (evex-byte1-equiv byte1 byte1-equiv) (equal (evex-byte1->b$inline byte1) (evex-byte1->b$inline byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1->b-of-evex-byte1 (equal (evex-byte1->b (evex-byte1 mm res r-prime b x r)) (bfix b)))
Theorem:
(defthm evex-byte1->b-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) 32) 0)) (equal (evex-byte1->b byte1) (evex-byte1->b y))))
Function:
(defun evex-byte1->x$inline (byte1) (declare (xargs :guard (evex-byte1-p byte1))) (mbe :logic (let ((byte1 (evex-byte1-fix byte1))) (part-select byte1 :low 6 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 2) (ash (the (unsigned-byte 8) byte1) -6))))))
Theorem:
(defthm bitp-of-evex-byte1->x (b* ((x (evex-byte1->x$inline byte1))) (bitp x)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte1->x$inline-of-evex-byte1-fix-byte1 (equal (evex-byte1->x$inline (evex-byte1-fix byte1)) (evex-byte1->x$inline byte1)))
Theorem:
(defthm evex-byte1->x$inline-evex-byte1-equiv-congruence-on-byte1 (implies (evex-byte1-equiv byte1 byte1-equiv) (equal (evex-byte1->x$inline byte1) (evex-byte1->x$inline byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1->x-of-evex-byte1 (equal (evex-byte1->x (evex-byte1 mm res r-prime b x r)) (bfix x)))
Theorem:
(defthm evex-byte1->x-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) 64) 0)) (equal (evex-byte1->x byte1) (evex-byte1->x y))))
Function:
(defun evex-byte1->r$inline (byte1) (declare (xargs :guard (evex-byte1-p byte1))) (mbe :logic (let ((byte1 (evex-byte1-fix byte1))) (part-select byte1 :low 7 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 1) (ash (the (unsigned-byte 8) byte1) -7))))))
Theorem:
(defthm bitp-of-evex-byte1->r (b* ((r (evex-byte1->r$inline byte1))) (bitp r)) :rule-classes :rewrite)
Theorem:
(defthm evex-byte1->r$inline-of-evex-byte1-fix-byte1 (equal (evex-byte1->r$inline (evex-byte1-fix byte1)) (evex-byte1->r$inline byte1)))
Theorem:
(defthm evex-byte1->r$inline-evex-byte1-equiv-congruence-on-byte1 (implies (evex-byte1-equiv byte1 byte1-equiv) (equal (evex-byte1->r$inline byte1) (evex-byte1->r$inline byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm evex-byte1->r-of-evex-byte1 (equal (evex-byte1->r (evex-byte1 mm res r-prime b x r)) (bfix r)))
Theorem:
(defthm evex-byte1->r-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) 128) 0)) (equal (evex-byte1->r byte1) (evex-byte1->r y))))
Theorem:
(defthm evex-byte1-fix-in-terms-of-evex-byte1 (equal (evex-byte1-fix byte1) (change-evex-byte1 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)))
Function:
(defun !evex-byte1->res$inline (res byte1) (declare (xargs :guard (and (2bits-p res) (evex-byte1-p byte1)))) (mbe :logic (b* ((res (mbe :logic (2bits-fix res) :exec res)) (byte1 (evex-byte1-fix byte1))) (part-install res byte1 :width 2 :low 2)) :exec (the (unsigned-byte 8) (logior (the (unsigned-byte 8) (logand (the (unsigned-byte 8) byte1) (the (signed-byte 5) -13))) (the (unsigned-byte 4) (ash (the (unsigned-byte 2) res) 2))))))
Theorem:
(defthm evex-byte1-p-of-!evex-byte1->res (b* ((new-byte1 (!evex-byte1->res$inline res byte1))) (evex-byte1-p new-byte1)) :rule-classes :rewrite)
Theorem:
(defthm !evex-byte1->res$inline-of-2bits-fix-res (equal (!evex-byte1->res$inline (2bits-fix res) byte1) (!evex-byte1->res$inline res byte1)))
Theorem:
(defthm !evex-byte1->res$inline-2bits-equiv-congruence-on-res (implies (2bits-equiv res res-equiv) (equal (!evex-byte1->res$inline res byte1) (!evex-byte1->res$inline res-equiv byte1))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->res$inline-of-evex-byte1-fix-byte1 (equal (!evex-byte1->res$inline res (evex-byte1-fix byte1)) (!evex-byte1->res$inline res 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 res byte1) (!evex-byte1->res$inline res byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->res-is-evex-byte1 (equal (!evex-byte1->res res byte1) (change-evex-byte1 byte1 :res res)))
Theorem:
(defthm evex-byte1->res-of-!evex-byte1->res (b* ((?new-byte1 (!evex-byte1->res$inline res byte1))) (equal (evex-byte1->res new-byte1) (2bits-fix res))))
Theorem:
(defthm !evex-byte1->res-equiv-under-mask (b* ((?new-byte1 (!evex-byte1->res$inline res byte1))) (evex-byte1-equiv-under-mask new-byte1 byte1 -13)))
Function:
(defun !evex-byte1->r-prime$inline (r-prime byte1) (declare (xargs :guard (and (bitp r-prime) (evex-byte1-p byte1)))) (mbe :logic (b* ((r-prime (mbe :logic (bfix r-prime) :exec r-prime)) (byte1 (evex-byte1-fix byte1))) (part-install r-prime byte1 :width 1 :low 4)) :exec (the (unsigned-byte 8) (logior (the (unsigned-byte 8) (logand (the (unsigned-byte 8) byte1) (the (signed-byte 6) -17))) (the (unsigned-byte 5) (ash (the (unsigned-byte 1) r-prime) 4))))))
Theorem:
(defthm evex-byte1-p-of-!evex-byte1->r-prime (b* ((new-byte1 (!evex-byte1->r-prime$inline r-prime byte1))) (evex-byte1-p new-byte1)) :rule-classes :rewrite)
Theorem:
(defthm !evex-byte1->r-prime$inline-of-bfix-r-prime (equal (!evex-byte1->r-prime$inline (bfix r-prime) byte1) (!evex-byte1->r-prime$inline r-prime byte1)))
Theorem:
(defthm !evex-byte1->r-prime$inline-bit-equiv-congruence-on-r-prime (implies (bit-equiv r-prime r-prime-equiv) (equal (!evex-byte1->r-prime$inline r-prime byte1) (!evex-byte1->r-prime$inline r-prime-equiv byte1))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->r-prime$inline-of-evex-byte1-fix-byte1 (equal (!evex-byte1->r-prime$inline r-prime (evex-byte1-fix byte1)) (!evex-byte1->r-prime$inline r-prime 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 r-prime byte1) (!evex-byte1->r-prime$inline r-prime byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->r-prime-is-evex-byte1 (equal (!evex-byte1->r-prime r-prime byte1) (change-evex-byte1 byte1 :r-prime r-prime)))
Theorem:
(defthm evex-byte1->r-prime-of-!evex-byte1->r-prime (b* ((?new-byte1 (!evex-byte1->r-prime$inline r-prime byte1))) (equal (evex-byte1->r-prime new-byte1) (bfix r-prime))))
Theorem:
(defthm !evex-byte1->r-prime-equiv-under-mask (b* ((?new-byte1 (!evex-byte1->r-prime$inline r-prime byte1))) (evex-byte1-equiv-under-mask new-byte1 byte1 -17)))
Function:
(defun !evex-byte1->b$inline (b byte1) (declare (xargs :guard (and (bitp b) (evex-byte1-p byte1)))) (mbe :logic (b* ((b (mbe :logic (bfix b) :exec b)) (byte1 (evex-byte1-fix byte1))) (part-install b byte1 :width 1 :low 5)) :exec (the (unsigned-byte 8) (logior (the (unsigned-byte 8) (logand (the (unsigned-byte 8) byte1) (the (signed-byte 7) -33))) (the (unsigned-byte 6) (ash (the (unsigned-byte 1) b) 5))))))
Theorem:
(defthm evex-byte1-p-of-!evex-byte1->b (b* ((new-byte1 (!evex-byte1->b$inline b byte1))) (evex-byte1-p new-byte1)) :rule-classes :rewrite)
Theorem:
(defthm !evex-byte1->b$inline-of-bfix-b (equal (!evex-byte1->b$inline (bfix b) byte1) (!evex-byte1->b$inline b byte1)))
Theorem:
(defthm !evex-byte1->b$inline-bit-equiv-congruence-on-b (implies (bit-equiv b b-equiv) (equal (!evex-byte1->b$inline b byte1) (!evex-byte1->b$inline b-equiv byte1))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->b$inline-of-evex-byte1-fix-byte1 (equal (!evex-byte1->b$inline b (evex-byte1-fix byte1)) (!evex-byte1->b$inline b byte1)))
Theorem:
(defthm !evex-byte1->b$inline-evex-byte1-equiv-congruence-on-byte1 (implies (evex-byte1-equiv byte1 byte1-equiv) (equal (!evex-byte1->b$inline b byte1) (!evex-byte1->b$inline b byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->b-is-evex-byte1 (equal (!evex-byte1->b b byte1) (change-evex-byte1 byte1 :b b)))
Theorem:
(defthm evex-byte1->b-of-!evex-byte1->b (b* ((?new-byte1 (!evex-byte1->b$inline b byte1))) (equal (evex-byte1->b new-byte1) (bfix b))))
Theorem:
(defthm !evex-byte1->b-equiv-under-mask (b* ((?new-byte1 (!evex-byte1->b$inline b byte1))) (evex-byte1-equiv-under-mask new-byte1 byte1 -33)))
Function:
(defun !evex-byte1->x$inline (x byte1) (declare (xargs :guard (and (bitp x) (evex-byte1-p byte1)))) (mbe :logic (b* ((x (mbe :logic (bfix x) :exec x)) (byte1 (evex-byte1-fix byte1))) (part-install x byte1 :width 1 :low 6)) :exec (the (unsigned-byte 8) (logior (the (unsigned-byte 8) (logand (the (unsigned-byte 8) byte1) (the (signed-byte 8) -65))) (the (unsigned-byte 7) (ash (the (unsigned-byte 1) x) 6))))))
Theorem:
(defthm evex-byte1-p-of-!evex-byte1->x (b* ((new-byte1 (!evex-byte1->x$inline x byte1))) (evex-byte1-p new-byte1)) :rule-classes :rewrite)
Theorem:
(defthm !evex-byte1->x$inline-of-bfix-x (equal (!evex-byte1->x$inline (bfix x) byte1) (!evex-byte1->x$inline x byte1)))
Theorem:
(defthm !evex-byte1->x$inline-bit-equiv-congruence-on-x (implies (bit-equiv x x-equiv) (equal (!evex-byte1->x$inline x byte1) (!evex-byte1->x$inline x-equiv byte1))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->x$inline-of-evex-byte1-fix-byte1 (equal (!evex-byte1->x$inline x (evex-byte1-fix byte1)) (!evex-byte1->x$inline x byte1)))
Theorem:
(defthm !evex-byte1->x$inline-evex-byte1-equiv-congruence-on-byte1 (implies (evex-byte1-equiv byte1 byte1-equiv) (equal (!evex-byte1->x$inline x byte1) (!evex-byte1->x$inline x byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->x-is-evex-byte1 (equal (!evex-byte1->x x byte1) (change-evex-byte1 byte1 :x x)))
Theorem:
(defthm evex-byte1->x-of-!evex-byte1->x (b* ((?new-byte1 (!evex-byte1->x$inline x byte1))) (equal (evex-byte1->x new-byte1) (bfix x))))
Theorem:
(defthm !evex-byte1->x-equiv-under-mask (b* ((?new-byte1 (!evex-byte1->x$inline x byte1))) (evex-byte1-equiv-under-mask new-byte1 byte1 -65)))
Function:
(defun !evex-byte1->r$inline (r byte1) (declare (xargs :guard (and (bitp r) (evex-byte1-p byte1)))) (mbe :logic (b* ((r (mbe :logic (bfix r) :exec r)) (byte1 (evex-byte1-fix byte1))) (part-install r byte1 :width 1 :low 7)) :exec (the (unsigned-byte 8) (logior (the (unsigned-byte 8) (logand (the (unsigned-byte 8) byte1) (the (signed-byte 9) -129))) (the (unsigned-byte 8) (ash (the (unsigned-byte 1) r) 7))))))
Theorem:
(defthm evex-byte1-p-of-!evex-byte1->r (b* ((new-byte1 (!evex-byte1->r$inline r byte1))) (evex-byte1-p new-byte1)) :rule-classes :rewrite)
Theorem:
(defthm !evex-byte1->r$inline-of-bfix-r (equal (!evex-byte1->r$inline (bfix r) byte1) (!evex-byte1->r$inline r byte1)))
Theorem:
(defthm !evex-byte1->r$inline-bit-equiv-congruence-on-r (implies (bit-equiv r r-equiv) (equal (!evex-byte1->r$inline r byte1) (!evex-byte1->r$inline r-equiv byte1))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->r$inline-of-evex-byte1-fix-byte1 (equal (!evex-byte1->r$inline r (evex-byte1-fix byte1)) (!evex-byte1->r$inline r byte1)))
Theorem:
(defthm !evex-byte1->r$inline-evex-byte1-equiv-congruence-on-byte1 (implies (evex-byte1-equiv byte1 byte1-equiv) (equal (!evex-byte1->r$inline r byte1) (!evex-byte1->r$inline r byte1-equiv))) :rule-classes :congruence)
Theorem:
(defthm !evex-byte1->r-is-evex-byte1 (equal (!evex-byte1->r r byte1) (change-evex-byte1 byte1 :r r)))
Theorem:
(defthm evex-byte1->r-of-!evex-byte1->r (b* ((?new-byte1 (!evex-byte1->r$inline r byte1))) (equal (evex-byte1->r new-byte1) (bfix r))))
Theorem:
(defthm !evex-byte1->r-equiv-under-mask (b* ((?new-byte1 (!evex-byte1->r$inline r byte1))) (evex-byte1-equiv-under-mask new-byte1 byte1 127)))
Function:
(defun evex-byte1-debug$inline (byte1) (declare (xargs :guard (evex-byte1-p byte1))) (b* (((evex-byte1 byte1))) (cons (cons 'mm byte1.mm) (cons (cons 'res byte1.res) (cons (cons 'r-prime byte1.r-prime) (cons (cons 'b byte1.b) (cons (cons 'x byte1.x) (cons (cons 'r byte1.r) nil))))))))