		Search-engine friendly clone of the ACL2 documentation.

Mxcsrbits

Mxcsrbits->reserved

Access the |X86ISA|::|RESERVED| field of a mxcsrbits bit structure.

Signature
(mxcsrbits->reserved x) → reserved
Arguments: x — Guard (mxcsrbits-p x).
Returns: reserved — Type (16bits-p reserved).

Definitions and Theorems

Function: mxcsrbits->reserved$inline

(defun mxcsrbits->reserved$inline (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (mbe :logic
       (let ((x (mxcsrbits-fix x)))
         (part-select x :low 16 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 16)
                               (ash (the (unsigned-byte 32) x)
                                    -16))))))

Theorem: 16bits-p-of-mxcsrbits->reserved

(defthm 16bits-p-of-mxcsrbits->reserved
  (b* ((reserved (mxcsrbits->reserved$inline x)))
    (16bits-p reserved))
  :rule-classes :rewrite)

Theorem: mxcsrbits->reserved$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->reserved$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->reserved$inline (mxcsrbits-fix x))
         (mxcsrbits->reserved$inline x)))

Theorem: mxcsrbits->reserved$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->reserved$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->reserved$inline x)
                  (mxcsrbits->reserved$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->reserved-of-mxcsrbits

(defthm mxcsrbits->reserved-of-mxcsrbits
  (equal (mxcsrbits->reserved
              (mxcsrbits ie de ze oe ue pe
                         daz im dm zm om um pm rc ftz reserved))
         (16bits-fix reserved)))

Theorem: mxcsrbits->reserved-of-write-with-mask

(defthm mxcsrbits->reserved-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 4294901760)
                       0))
           (equal (mxcsrbits->reserved x)
                  (mxcsrbits->reserved y))))