		Search-engine friendly clone of the ACL2 documentation.

Hidden-segment-registerbits

!hidden-segment-registerbits->attr

Update the |X86ISA|::|ATTR| field of a hidden-segment-registerbits bit structure.

Signature
(!hidden-segment-registerbits->attr attr x) → new-x
Arguments: attr — Guard (16bits-p attr).; x — Guard (hidden-segment-registerbits-p x).
Returns: new-x — Type (hidden-segment-registerbits-p new-x).

Definitions and Theorems

Function: !hidden-segment-registerbits->attr$inline

(defun !hidden-segment-registerbits->attr$inline (attr x)
 (declare (xargs :guard (and (16bits-p attr)
                             (hidden-segment-registerbits-p x))))
 (mbe
  :logic
  (b* ((attr (mbe :logic (16bits-fix attr)
                  :exec attr))
       (x (hidden-segment-registerbits-fix x)))
    (part-install attr x :width 16 :low 96))
  :exec
  (the
    (unsigned-byte 112)
    (logior (the (unsigned-byte 112)
                 (logand (the (unsigned-byte 112) x)
                         (the (signed-byte 113)
                              -5192217630372313364192902785269761)))
            (the (unsigned-byte 112)
                 (ash (the (unsigned-byte 16) attr)
                      96))))))

Theorem: hidden-segment-registerbits-p-of-!hidden-segment-registerbits->attr

(defthm
 hidden-segment-registerbits-p-of-!hidden-segment-registerbits->attr
 (b* ((new-x (!hidden-segment-registerbits->attr$inline attr x)))
   (hidden-segment-registerbits-p new-x))
 :rule-classes :rewrite)

Theorem: !hidden-segment-registerbits->attr$inline-of-16bits-fix-attr

(defthm !hidden-segment-registerbits->attr$inline-of-16bits-fix-attr
 (equal (!hidden-segment-registerbits->attr$inline (16bits-fix attr)
                                                   x)
        (!hidden-segment-registerbits->attr$inline attr x)))

Theorem: !hidden-segment-registerbits->attr$inline-16bits-equiv-congruence-on-attr

(defthm
 !hidden-segment-registerbits->attr$inline-16bits-equiv-congruence-on-attr
 (implies
   (16bits-equiv attr attr-equiv)
   (equal (!hidden-segment-registerbits->attr$inline attr x)
          (!hidden-segment-registerbits->attr$inline attr-equiv x)))
 :rule-classes :congruence)

Theorem: !hidden-segment-registerbits->attr$inline-of-hidden-segment-registerbits-fix-x

(defthm
 !hidden-segment-registerbits->attr$inline-of-hidden-segment-registerbits-fix-x
 (equal (!hidden-segment-registerbits->attr$inline
             attr
             (hidden-segment-registerbits-fix x))
        (!hidden-segment-registerbits->attr$inline attr x)))

Theorem: !hidden-segment-registerbits->attr$inline-hidden-segment-registerbits-equiv-congruence-on-x

(defthm
 !hidden-segment-registerbits->attr$inline-hidden-segment-registerbits-equiv-congruence-on-x
 (implies
   (hidden-segment-registerbits-equiv x x-equiv)
   (equal (!hidden-segment-registerbits->attr$inline attr x)
          (!hidden-segment-registerbits->attr$inline attr x-equiv)))
 :rule-classes :congruence)

Theorem: !hidden-segment-registerbits->attr-is-hidden-segment-registerbits

(defthm
  !hidden-segment-registerbits->attr-is-hidden-segment-registerbits
  (equal (!hidden-segment-registerbits->attr attr x)
         (change-hidden-segment-registerbits x
                                             :attr attr)))

Theorem: hidden-segment-registerbits->attr-of-!hidden-segment-registerbits->attr

(defthm
 hidden-segment-registerbits->attr-of-!hidden-segment-registerbits->attr
 (b* ((?new-x (!hidden-segment-registerbits->attr$inline attr x)))
   (equal (hidden-segment-registerbits->attr new-x)
          (16bits-fix attr))))

Theorem: !hidden-segment-registerbits->attr-equiv-under-mask

(defthm !hidden-segment-registerbits->attr-equiv-under-mask
  (b* ((?new-x (!hidden-segment-registerbits->attr$inline attr x)))
    (hidden-segment-registerbits-equiv-under-mask
         new-x x 79228162514264337593543950335)))