		Search-engine friendly clone of the ACL2 documentation.

Rflagsbits

!rflagsbits->res5

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

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

Definitions and Theorems

Function: !rflagsbits->res5$inline

(defun !rflagsbits->res5$inline (res5 x)
 (declare (xargs :guard (and (10bits-p res5) (rflagsbits-p x))))
 (mbe :logic
      (b* ((res5 (mbe :logic (10bits-fix res5)
                      :exec res5))
           (x (rflagsbits-fix x)))
        (part-install res5 x :width 10 :low 22))
      :exec
      (the (unsigned-byte 32)
           (logior (the (unsigned-byte 32)
                        (logand (the (unsigned-byte 32) x)
                                (the (signed-byte 33) -4290772993)))
                   (the (unsigned-byte 32)
                        (ash (the (unsigned-byte 10) res5)
                             22))))))

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

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

Theorem: !rflagsbits->res5$inline-of-10bits-fix-res5

(defthm !rflagsbits->res5$inline-of-10bits-fix-res5
  (equal (!rflagsbits->res5$inline (10bits-fix res5)
                                   x)
         (!rflagsbits->res5$inline res5 x)))

Theorem: !rflagsbits->res5$inline-10bits-equiv-congruence-on-res5

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

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

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

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

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

Theorem: !rflagsbits->res5-is-rflagsbits

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

Theorem: rflagsbits->res5-of-!rflagsbits->res5

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

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

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