		Search-engine friendly clone of the ACL2 documentation.

Rflagsbits

!rflagsbits->iopl

Update the |X86ISA|::|IOPL| field of a rflagsbits bit structure.

Signature
(!rflagsbits->iopl iopl x) → new-x
Arguments: iopl — Guard (2bits-p iopl).; x — Guard (rflagsbits-p x).
Returns: new-x — Type (rflagsbits-p new-x).

Definitions and Theorems

Function: !rflagsbits->iopl$inline

(defun !rflagsbits->iopl$inline (iopl x)
 (declare (xargs :guard (and (2bits-p iopl) (rflagsbits-p x))))
 (mbe
     :logic
     (b* ((iopl (mbe :logic (2bits-fix iopl)
                     :exec iopl))
          (x (rflagsbits-fix x)))
       (part-install iopl x :width 2 :low 12))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 15) -12289)))
                        (the (unsigned-byte 14)
                             (ash (the (unsigned-byte 2) iopl)
                                  12))))))

Theorem: rflagsbits-p-of-!rflagsbits->iopl

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

Theorem: !rflagsbits->iopl$inline-of-2bits-fix-iopl

(defthm !rflagsbits->iopl$inline-of-2bits-fix-iopl
  (equal (!rflagsbits->iopl$inline (2bits-fix iopl)
                                   x)
         (!rflagsbits->iopl$inline iopl x)))

Theorem: !rflagsbits->iopl$inline-2bits-equiv-congruence-on-iopl

(defthm !rflagsbits->iopl$inline-2bits-equiv-congruence-on-iopl
  (implies (2bits-equiv iopl iopl-equiv)
           (equal (!rflagsbits->iopl$inline iopl x)
                  (!rflagsbits->iopl$inline iopl-equiv x)))
  :rule-classes :congruence)

Theorem: !rflagsbits->iopl$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->iopl$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->iopl$inline iopl (rflagsbits-fix x))
         (!rflagsbits->iopl$inline iopl x)))

Theorem: !rflagsbits->iopl$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->iopl-is-rflagsbits

(defthm !rflagsbits->iopl-is-rflagsbits
  (equal (!rflagsbits->iopl iopl x)
         (change-rflagsbits x :iopl iopl)))

Theorem: rflagsbits->iopl-of-!rflagsbits->iopl

(defthm rflagsbits->iopl-of-!rflagsbits->iopl
  (b* ((?new-x (!rflagsbits->iopl$inline iopl x)))
    (equal (rflagsbits->iopl new-x)
           (2bits-fix iopl))))

Theorem: !rflagsbits->iopl-equiv-under-mask

(defthm !rflagsbits->iopl-equiv-under-mask
  (b* ((?new-x (!rflagsbits->iopl$inline iopl x)))
    (rflagsbits-equiv-under-mask new-x x -12289)))