		Search-engine friendly clone of the ACL2 documentation.

Prefixes

!prefixes->opr

Update the |X86ISA|::|OPR| field of a prefixes bit structure.

Signature
(!prefixes->opr opr x) → new-x
Arguments: opr — Guard (8bits-p opr).; x — Guard (prefixes-p x).
Returns: new-x — Type (prefixes-p new-x).

Definitions and Theorems

Function: !prefixes->opr$inline

(defun !prefixes->opr$inline (opr x)
 (declare (xargs :guard (and (8bits-p opr) (prefixes-p x))))
 (mbe
     :logic
     (b* ((opr (mbe :logic (8bits-fix opr) :exec opr))
          (x (prefixes-fix x)))
       (part-install opr x :width 8 :low 28))
     :exec
     (the (unsigned-byte 52)
          (logior (the (unsigned-byte 52)
                       (logand (the (unsigned-byte 52) x)
                               (the (signed-byte 37) -68451041281)))
                  (the (unsigned-byte 36)
                       (ash (the (unsigned-byte 8) opr)
                            28))))))

Theorem: prefixes-p-of-!prefixes->opr

(defthm prefixes-p-of-!prefixes->opr
  (b* ((new-x (!prefixes->opr$inline opr x)))
    (prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !prefixes->opr$inline-of-8bits-fix-opr

(defthm !prefixes->opr$inline-of-8bits-fix-opr
  (equal (!prefixes->opr$inline (8bits-fix opr)
                                x)
         (!prefixes->opr$inline opr x)))

Theorem: !prefixes->opr$inline-8bits-equiv-congruence-on-opr

(defthm !prefixes->opr$inline-8bits-equiv-congruence-on-opr
  (implies (8bits-equiv opr opr-equiv)
           (equal (!prefixes->opr$inline opr x)
                  (!prefixes->opr$inline opr-equiv x)))
  :rule-classes :congruence)

Theorem: !prefixes->opr$inline-of-prefixes-fix-x

(defthm !prefixes->opr$inline-of-prefixes-fix-x
  (equal (!prefixes->opr$inline opr (prefixes-fix x))
         (!prefixes->opr$inline opr x)))

Theorem: !prefixes->opr$inline-prefixes-equiv-congruence-on-x

(defthm !prefixes->opr$inline-prefixes-equiv-congruence-on-x
  (implies (prefixes-equiv x x-equiv)
           (equal (!prefixes->opr$inline opr x)
                  (!prefixes->opr$inline opr x-equiv)))
  :rule-classes :congruence)

Theorem: !prefixes->opr-is-prefixes

(defthm !prefixes->opr-is-prefixes
  (equal (!prefixes->opr opr x)
         (change-prefixes x :opr opr)))

Theorem: prefixes->opr-of-!prefixes->opr

(defthm prefixes->opr-of-!prefixes->opr
  (b* ((?new-x (!prefixes->opr$inline opr x)))
    (equal (prefixes->opr new-x)
           (8bits-fix opr))))

Theorem: !prefixes->opr-equiv-under-mask

(defthm !prefixes->opr-equiv-under-mask
  (b* ((?new-x (!prefixes->opr$inline opr x)))
    (prefixes-equiv-under-mask new-x x -68451041281)))