		Search-engine friendly clone of the ACL2 documentation.

Call-gate-descriptorbits

!call-gate-descriptorbits->offset31-16

Update the |X86ISA|::|OFFSET31-16| field of a call-gate-descriptorbits bit structure.

Signature
(!call-gate-descriptorbits->offset31-16 offset31-16 x) → new-x
Arguments: offset31-16 — Guard (16bits-p offset31-16).; x — Guard (call-gate-descriptorbits-p x).
Returns: new-x — Type (call-gate-descriptorbits-p new-x).

Definitions and Theorems

Function: !call-gate-descriptorbits->offset31-16$inline

(defun !call-gate-descriptorbits->offset31-16$inline (offset31-16 x)
 (declare (xargs :guard (and (16bits-p offset31-16)
                             (call-gate-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((offset31-16 (mbe :logic (16bits-fix offset31-16)
                          :exec offset31-16))
        (x (call-gate-descriptorbits-fix x)))
     (part-install offset31-16 x
                   :width 16
                   :low 48))
   :exec (the (unsigned-byte 128)
              (logior (the (unsigned-byte 128)
                           (logand (the (unsigned-byte 128) x)
                                   (the (signed-byte 65)
                                        -18446462598732840961)))
                      (the (unsigned-byte 64)
                           (ash (the (unsigned-byte 16) offset31-16)
                                48))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->offset31-16

(defthm
 call-gate-descriptorbits-p-of-!call-gate-descriptorbits->offset31-16
 (b*
  ((new-x
     (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)))
  (call-gate-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !call-gate-descriptorbits->offset31-16$inline-of-16bits-fix-offset31-16

(defthm
 !call-gate-descriptorbits->offset31-16$inline-of-16bits-fix-offset31-16
 (equal
     (!call-gate-descriptorbits->offset31-16$inline
          (16bits-fix offset31-16)
          x)
     (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)))

Theorem: !call-gate-descriptorbits->offset31-16$inline-16bits-equiv-congruence-on-offset31-16

(defthm
 !call-gate-descriptorbits->offset31-16$inline-16bits-equiv-congruence-on-offset31-16
 (implies
  (16bits-equiv offset31-16 offset31-16-equiv)
  (equal
       (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)
       (!call-gate-descriptorbits->offset31-16$inline
            offset31-16-equiv x)))
 :rule-classes :congruence)

Theorem: !call-gate-descriptorbits->offset31-16$inline-of-call-gate-descriptorbits-fix-x

(defthm
 !call-gate-descriptorbits->offset31-16$inline-of-call-gate-descriptorbits-fix-x
 (equal
     (!call-gate-descriptorbits->offset31-16$inline
          offset31-16
          (call-gate-descriptorbits-fix x))
     (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)))

Theorem: !call-gate-descriptorbits->offset31-16$inline-call-gate-descriptorbits-equiv-congruence-on-x

(defthm
 !call-gate-descriptorbits->offset31-16$inline-call-gate-descriptorbits-equiv-congruence-on-x
 (implies
  (call-gate-descriptorbits-equiv x x-equiv)
  (equal
       (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)
       (!call-gate-descriptorbits->offset31-16$inline
            offset31-16 x-equiv)))
 :rule-classes :congruence)

Theorem: !call-gate-descriptorbits->offset31-16-is-call-gate-descriptorbits

(defthm
 !call-gate-descriptorbits->offset31-16-is-call-gate-descriptorbits
 (equal (!call-gate-descriptorbits->offset31-16 offset31-16 x)
        (change-call-gate-descriptorbits x
                                         :offset31-16 offset31-16)))

Theorem: call-gate-descriptorbits->offset31-16-of-!call-gate-descriptorbits->offset31-16

(defthm
 call-gate-descriptorbits->offset31-16-of-!call-gate-descriptorbits->offset31-16
 (b*
  ((?new-x
     (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)))
  (equal (call-gate-descriptorbits->offset31-16 new-x)
         (16bits-fix offset31-16))))

Theorem: !call-gate-descriptorbits->offset31-16-equiv-under-mask

(defthm !call-gate-descriptorbits->offset31-16-equiv-under-mask
 (b*
  ((?new-x
     (!call-gate-descriptorbits->offset31-16$inline offset31-16 x)))
  (call-gate-descriptorbits-equiv-under-mask
       new-x x -18446462598732840961)))