		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Call-gate-descriptorbits

AMD manual, Jun'23, Vol. 2, Figure 4-23.

This is a bitstruct type introduced by defbitstruct, represented as a unsigned 128-bit integer.

Fields

offset15-0 — 16bits
selector — 16bits
res1 — 8bits
type — 4bits
s — bit
dpl — 2bits
p — bit
offset31-16 — 16bits
offset63-32 — 32bits
res2 — 8bits
all-zeroes? — 5bits
res3 — 19bits

Definitions and Theorems

Function: call-gate-descriptorbits-p

(defun call-gate-descriptorbits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'call-gate-descriptorbits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 128 x)
         :exec (and (natp x)
                    (< x
                       340282366920938463463374607431768211456)))))

Theorem: call-gate-descriptorbits-p-when-unsigned-byte-p

(defthm call-gate-descriptorbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 128 x)
           (call-gate-descriptorbits-p x)))

Theorem: unsigned-byte-p-when-call-gate-descriptorbits-p

(defthm unsigned-byte-p-when-call-gate-descriptorbits-p
  (implies (call-gate-descriptorbits-p x)
           (unsigned-byte-p 128 x)))

Theorem: call-gate-descriptorbits-p-compound-recognizer

(defthm call-gate-descriptorbits-p-compound-recognizer
  (implies (call-gate-descriptorbits-p x)
           (natp x))
  :rule-classes :compound-recognizer)

Function: call-gate-descriptorbits-fix

(defun call-gate-descriptorbits-fix (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (let ((__function__ 'call-gate-descriptorbits-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 128 x) :exec x)))

Theorem: call-gate-descriptorbits-p-of-call-gate-descriptorbits-fix

(defthm call-gate-descriptorbits-p-of-call-gate-descriptorbits-fix
  (b* ((fty::fixed (call-gate-descriptorbits-fix x)))
    (call-gate-descriptorbits-p fty::fixed))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits-fix-when-call-gate-descriptorbits-p

(defthm call-gate-descriptorbits-fix-when-call-gate-descriptorbits-p
  (implies (call-gate-descriptorbits-p x)
           (equal (call-gate-descriptorbits-fix x)
                  x)))

Function: call-gate-descriptorbits-equiv$inline

(defun call-gate-descriptorbits-equiv$inline (x y)
  (declare (xargs :guard (and (call-gate-descriptorbits-p x)
                              (call-gate-descriptorbits-p y))))
  (equal (call-gate-descriptorbits-fix x)
         (call-gate-descriptorbits-fix y)))

Theorem: call-gate-descriptorbits-equiv-is-an-equivalence

(defthm call-gate-descriptorbits-equiv-is-an-equivalence
  (and (booleanp (call-gate-descriptorbits-equiv x y))
       (call-gate-descriptorbits-equiv x x)
       (implies (call-gate-descriptorbits-equiv x y)
                (call-gate-descriptorbits-equiv y x))
       (implies (and (call-gate-descriptorbits-equiv x y)
                     (call-gate-descriptorbits-equiv y z))
                (call-gate-descriptorbits-equiv x z)))
  :rule-classes (:equivalence))

Theorem: call-gate-descriptorbits-equiv-implies-equal-call-gate-descriptorbits-fix-1

(defthm
 call-gate-descriptorbits-equiv-implies-equal-call-gate-descriptorbits-fix-1
 (implies (call-gate-descriptorbits-equiv x x-equiv)
          (equal (call-gate-descriptorbits-fix x)
                 (call-gate-descriptorbits-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: call-gate-descriptorbits-fix-under-call-gate-descriptorbits-equiv

(defthm
  call-gate-descriptorbits-fix-under-call-gate-descriptorbits-equiv
  (call-gate-descriptorbits-equiv (call-gate-descriptorbits-fix x)
                                  x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: call-gate-descriptorbits

(defun call-gate-descriptorbits
       (offset15-0 selector res1 type s dpl p offset31-16
                   offset63-32 res2 all-zeroes? res3)
 (declare (xargs :guard (and (16bits-p offset15-0)
                             (16bits-p selector)
                             (8bits-p res1)
                             (4bits-p type)
                             (bitp s)
                             (2bits-p dpl)
                             (bitp p)
                             (16bits-p offset31-16)
                             (32bits-p offset63-32)
                             (8bits-p res2)
                             (5bits-p all-zeroes?)
                             (19bits-p res3))))
 (let ((__function__ 'call-gate-descriptorbits))
  (declare (ignorable __function__))
  (b* ((offset15-0 (mbe :logic (16bits-fix offset15-0)
                        :exec offset15-0))
       (selector (mbe :logic (16bits-fix selector)
                      :exec selector))
       (res1 (mbe :logic (8bits-fix res1)
                  :exec res1))
       (type (mbe :logic (4bits-fix type)
                  :exec type))
       (s (mbe :logic (bfix s) :exec s))
       (dpl (mbe :logic (2bits-fix dpl) :exec dpl))
       (p (mbe :logic (bfix p) :exec p))
       (offset31-16 (mbe :logic (16bits-fix offset31-16)
                         :exec offset31-16))
       (offset63-32 (mbe :logic (32bits-fix offset63-32)
                         :exec offset63-32))
       (res2 (mbe :logic (8bits-fix res2)
                  :exec res2))
       (all-zeroes? (mbe :logic (5bits-fix all-zeroes?)
                         :exec all-zeroes?))
       (res3 (mbe :logic (19bits-fix res3)
                  :exec res3)))
   (logapp
    16 offset15-0
    (logapp
     16 selector
     (logapp
      8 res1
      (logapp
       4 type
       (logapp
        1 s
        (logapp
         2 dpl
         (logapp
          1 p
          (logapp
            16 offset31-16
            (logapp 32 offset63-32
                    (logapp 8 res2
                            (logapp 5 all-zeroes? res3))))))))))))))

Theorem: call-gate-descriptorbits-p-of-call-gate-descriptorbits

(defthm call-gate-descriptorbits-p-of-call-gate-descriptorbits
 (b*
  ((call-gate-descriptorbits
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))
  (call-gate-descriptorbits-p call-gate-descriptorbits))
 :rule-classes :rewrite)

Theorem: call-gate-descriptorbits-of-16bits-fix-offset15-0

(defthm call-gate-descriptorbits-of-16bits-fix-offset15-0
 (equal
    (call-gate-descriptorbits (16bits-fix offset15-0)
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-16bits-equiv-congruence-on-offset15-0

(defthm
     call-gate-descriptorbits-16bits-equiv-congruence-on-offset15-0
 (implies
  (16bits-equiv offset15-0 offset15-0-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0-equiv
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-16bits-fix-selector

(defthm call-gate-descriptorbits-of-16bits-fix-selector
 (equal
    (call-gate-descriptorbits offset15-0 (16bits-fix selector)
                              res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-16bits-equiv-congruence-on-selector

(defthm call-gate-descriptorbits-16bits-equiv-congruence-on-selector
 (implies
  (16bits-equiv selector selector-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector-equiv
                              res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-8bits-fix-res1

(defthm call-gate-descriptorbits-of-8bits-fix-res1
 (equal
    (call-gate-descriptorbits offset15-0 selector (8bits-fix res1)
                              type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-8bits-equiv-congruence-on-res1

(defthm call-gate-descriptorbits-8bits-equiv-congruence-on-res1
 (implies
  (8bits-equiv res1 res1-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector
                              res1-equiv type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-4bits-fix-type

(defthm call-gate-descriptorbits-of-4bits-fix-type
 (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 (4bits-fix type)
                              s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-4bits-equiv-congruence-on-type

(defthm call-gate-descriptorbits-4bits-equiv-congruence-on-type
 (implies
  (4bits-equiv type type-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector
                              res1 type-equiv s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-bfix-s

(defthm call-gate-descriptorbits-of-bfix-s
 (equal
    (call-gate-descriptorbits offset15-0 selector res1 type (bfix s)
                              dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-bit-equiv-congruence-on-s

(defthm call-gate-descriptorbits-bit-equiv-congruence-on-s
 (implies
  (bit-equiv s s-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector
                              res1 type s-equiv dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-2bits-fix-dpl

(defthm call-gate-descriptorbits-of-2bits-fix-dpl
 (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s (2bits-fix dpl)
                              p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-2bits-equiv-congruence-on-dpl

(defthm call-gate-descriptorbits-2bits-equiv-congruence-on-dpl
 (implies
  (2bits-equiv dpl dpl-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector
                              res1 type s dpl-equiv p offset31-16
                              offset63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-bfix-p

(defthm call-gate-descriptorbits-of-bfix-p
 (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl (bfix p)
                              offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-bit-equiv-congruence-on-p

(defthm call-gate-descriptorbits-bit-equiv-congruence-on-p
 (implies
  (bit-equiv p p-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector
                              res1 type s dpl p-equiv offset31-16
                              offset63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-16bits-fix-offset31-16

(defthm call-gate-descriptorbits-of-16bits-fix-offset31-16
 (equal
    (call-gate-descriptorbits offset15-0 selector res1
                              type s dpl p (16bits-fix offset31-16)
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-16bits-equiv-congruence-on-offset31-16

(defthm
    call-gate-descriptorbits-16bits-equiv-congruence-on-offset31-16
 (implies
  (16bits-equiv offset31-16 offset31-16-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector
                              res1 type s dpl p offset31-16-equiv
                              offset63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-32bits-fix-offset63-32

(defthm call-gate-descriptorbits-of-32bits-fix-offset63-32
 (equal
    (call-gate-descriptorbits offset15-0 selector res1 type s dpl
                              p offset31-16 (32bits-fix offset63-32)
                              res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-32bits-equiv-congruence-on-offset63-32

(defthm
    call-gate-descriptorbits-32bits-equiv-congruence-on-offset63-32
 (implies
  (32bits-equiv offset63-32 offset63-32-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector res1 type
                              s dpl p offset31-16 offset63-32-equiv
                              res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-8bits-fix-res2

(defthm call-gate-descriptorbits-of-8bits-fix-res2
 (equal
  (call-gate-descriptorbits offset15-0 selector res1 type s dpl p
                            offset31-16 offset63-32 (8bits-fix res2)
                            all-zeroes? res3)
  (call-gate-descriptorbits offset15-0
                            selector res1 type s dpl p offset31-16
                            offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-8bits-equiv-congruence-on-res2

(defthm call-gate-descriptorbits-8bits-equiv-congruence-on-res2
 (implies
  (8bits-equiv res2 res2-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector res1
                              type s dpl p offset31-16 offset63-32
                              res2-equiv all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-5bits-fix-all-zeroes?

(defthm call-gate-descriptorbits-of-5bits-fix-all-zeroes?
 (equal
  (call-gate-descriptorbits offset15-0
                            selector res1 type s dpl p offset31-16
                            offset63-32 res2 (5bits-fix all-zeroes?)
                            res3)
  (call-gate-descriptorbits offset15-0
                            selector res1 type s dpl p offset31-16
                            offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-5bits-equiv-congruence-on-all-zeroes?

(defthm
     call-gate-descriptorbits-5bits-equiv-congruence-on-all-zeroes?
 (implies
  (5bits-equiv all-zeroes? all-zeroes?-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector res1
                              type s dpl p offset31-16 offset63-32
                              res2 all-zeroes?-equiv res3)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits-of-19bits-fix-res3

(defthm call-gate-descriptorbits-of-19bits-fix-res3
 (equal
    (call-gate-descriptorbits offset15-0 selector res1
                              type s dpl p offset31-16 offset63-32
                              res2 all-zeroes? (19bits-fix res3))
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)))

Theorem: call-gate-descriptorbits-19bits-equiv-congruence-on-res3

(defthm call-gate-descriptorbits-19bits-equiv-congruence-on-res3
 (implies
  (19bits-equiv res3 res3-equiv)
  (equal
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3)
    (call-gate-descriptorbits offset15-0 selector res1
                              type s dpl p offset31-16 offset63-32
                              res2 all-zeroes? res3-equiv)))
 :rule-classes :congruence)

Function: call-gate-descriptorbits-equiv-under-mask

(defun call-gate-descriptorbits-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (call-gate-descriptorbits-p x)
                              (call-gate-descriptorbits-p x1)
                              (integerp mask))))
  (let ((__function__ 'call-gate-descriptorbits-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (call-gate-descriptorbits-fix x)
                               (call-gate-descriptorbits-fix x1)
                               mask)))

Function: call-gate-descriptorbits->offset15-0$inline

(defun call-gate-descriptorbits->offset15-0$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 0 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 128) x)))))

Theorem: 16bits-p-of-call-gate-descriptorbits->offset15-0

(defthm 16bits-p-of-call-gate-descriptorbits->offset15-0
  (b* ((offset15-0 (call-gate-descriptorbits->offset15-0$inline x)))
    (16bits-p offset15-0))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->offset15-0$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->offset15-0$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->offset15-0$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->offset15-0$inline x)))

Theorem: call-gate-descriptorbits->offset15-0$inline-call-gate-descriptorbits-equiv-congruence-on-x

(defthm
 call-gate-descriptorbits->offset15-0$inline-call-gate-descriptorbits-equiv-congruence-on-x
 (implies
      (call-gate-descriptorbits-equiv x x-equiv)
      (equal (call-gate-descriptorbits->offset15-0$inline x)
             (call-gate-descriptorbits->offset15-0$inline x-equiv)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits->offset15-0-of-call-gate-descriptorbits

(defthm
   call-gate-descriptorbits->offset15-0-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->offset15-0
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (16bits-fix offset15-0)))

Theorem: call-gate-descriptorbits->offset15-0-of-write-with-mask

(defthm call-gate-descriptorbits->offset15-0-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask) 65535)
                  0))
      (equal (call-gate-descriptorbits->offset15-0 x)
             (call-gate-descriptorbits->offset15-0 y))))

Function: call-gate-descriptorbits->selector$inline

(defun call-gate-descriptorbits->selector$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 16 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 112)
                               (ash (the (unsigned-byte 128) x)
                                    -16))))))

Theorem: 16bits-p-of-call-gate-descriptorbits->selector

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

Theorem: call-gate-descriptorbits->selector$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->selector$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->selector$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->selector$inline x)))

Theorem: call-gate-descriptorbits->selector$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: call-gate-descriptorbits->selector-of-call-gate-descriptorbits

(defthm
     call-gate-descriptorbits->selector-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->selector
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (16bits-fix selector)))

Theorem: call-gate-descriptorbits->selector-of-write-with-mask

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

Function: call-gate-descriptorbits->res1$inline

(defun call-gate-descriptorbits->res1$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 32 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 96)
                               (ash (the (unsigned-byte 128) x)
                                    -32))))))

Theorem: 8bits-p-of-call-gate-descriptorbits->res1

(defthm 8bits-p-of-call-gate-descriptorbits->res1
  (b* ((res1 (call-gate-descriptorbits->res1$inline x)))
    (8bits-p res1))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->res1$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->res1$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->res1$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->res1$inline x)))

Theorem: call-gate-descriptorbits->res1$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: call-gate-descriptorbits->res1-of-call-gate-descriptorbits

(defthm call-gate-descriptorbits->res1-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->res1
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (8bits-fix res1)))

Theorem: call-gate-descriptorbits->res1-of-write-with-mask

(defthm call-gate-descriptorbits->res1-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          1095216660480)
                  0))
      (equal (call-gate-descriptorbits->res1 x)
             (call-gate-descriptorbits->res1 y))))

Function: call-gate-descriptorbits->type$inline

(defun call-gate-descriptorbits->type$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 40 :width 4))
       :exec (the (unsigned-byte 4)
                  (logand (the (unsigned-byte 4) 15)
                          (the (unsigned-byte 88)
                               (ash (the (unsigned-byte 128) x)
                                    -40))))))

Theorem: 4bits-p-of-call-gate-descriptorbits->type

(defthm 4bits-p-of-call-gate-descriptorbits->type
  (b* ((type (call-gate-descriptorbits->type$inline x)))
    (4bits-p type))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->type$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->type$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->type$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->type$inline x)))

Theorem: call-gate-descriptorbits->type$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: call-gate-descriptorbits->type-of-call-gate-descriptorbits

(defthm call-gate-descriptorbits->type-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->type
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (4bits-fix type)))

Theorem: call-gate-descriptorbits->type-of-write-with-mask

(defthm call-gate-descriptorbits->type-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          16492674416640)
                  0))
      (equal (call-gate-descriptorbits->type x)
             (call-gate-descriptorbits->type y))))

Function: call-gate-descriptorbits->s$inline

(defun call-gate-descriptorbits->s$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 44 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 84)
                               (ash (the (unsigned-byte 128) x)
                                    -44))))))

Theorem: bitp-of-call-gate-descriptorbits->s

(defthm bitp-of-call-gate-descriptorbits->s
  (b* ((s (call-gate-descriptorbits->s$inline x)))
    (bitp s))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->s$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->s$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->s$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->s$inline x)))

Theorem: call-gate-descriptorbits->s$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: call-gate-descriptorbits->s-of-call-gate-descriptorbits

(defthm call-gate-descriptorbits->s-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->s
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (bfix s)))

Theorem: call-gate-descriptorbits->s-of-write-with-mask

(defthm call-gate-descriptorbits->s-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          17592186044416)
                  0))
      (equal (call-gate-descriptorbits->s x)
             (call-gate-descriptorbits->s y))))

Function: call-gate-descriptorbits->dpl$inline

(defun call-gate-descriptorbits->dpl$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 45 :width 2))
       :exec (the (unsigned-byte 2)
                  (logand (the (unsigned-byte 2) 3)
                          (the (unsigned-byte 83)
                               (ash (the (unsigned-byte 128) x)
                                    -45))))))

Theorem: 2bits-p-of-call-gate-descriptorbits->dpl

(defthm 2bits-p-of-call-gate-descriptorbits->dpl
  (b* ((dpl (call-gate-descriptorbits->dpl$inline x)))
    (2bits-p dpl))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->dpl$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->dpl$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->dpl$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->dpl$inline x)))

Theorem: call-gate-descriptorbits->dpl$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: call-gate-descriptorbits->dpl-of-call-gate-descriptorbits

(defthm call-gate-descriptorbits->dpl-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->dpl
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (2bits-fix dpl)))

Theorem: call-gate-descriptorbits->dpl-of-write-with-mask

(defthm call-gate-descriptorbits->dpl-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          105553116266496)
                  0))
      (equal (call-gate-descriptorbits->dpl x)
             (call-gate-descriptorbits->dpl y))))

Function: call-gate-descriptorbits->p$inline

(defun call-gate-descriptorbits->p$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 47 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 81)
                               (ash (the (unsigned-byte 128) x)
                                    -47))))))

Theorem: bitp-of-call-gate-descriptorbits->p

(defthm bitp-of-call-gate-descriptorbits->p
  (b* ((p (call-gate-descriptorbits->p$inline x)))
    (bitp p))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->p$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->p$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->p$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->p$inline x)))

Theorem: call-gate-descriptorbits->p$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: call-gate-descriptorbits->p-of-call-gate-descriptorbits

(defthm call-gate-descriptorbits->p-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->p
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (bfix p)))

Theorem: call-gate-descriptorbits->p-of-write-with-mask

(defthm call-gate-descriptorbits->p-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          140737488355328)
                  0))
      (equal (call-gate-descriptorbits->p x)
             (call-gate-descriptorbits->p y))))

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

(defun call-gate-descriptorbits->offset31-16$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 48 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 80)
                               (ash (the (unsigned-byte 128) x)
                                    -48))))))

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

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

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
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->offset31-16$inline 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 x)
            (call-gate-descriptorbits->offset31-16$inline x-equiv)))
 :rule-classes :congruence)

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

(defthm
  call-gate-descriptorbits->offset31-16-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->offset31-16
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (16bits-fix offset31-16)))

Theorem: call-gate-descriptorbits->offset31-16-of-write-with-mask

(defthm call-gate-descriptorbits->offset31-16-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          18446462598732840960)
                  0))
      (equal (call-gate-descriptorbits->offset31-16 x)
             (call-gate-descriptorbits->offset31-16 y))))

Function: call-gate-descriptorbits->offset63-32$inline

(defun call-gate-descriptorbits->offset63-32$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 64 :width 32))
       :exec (the (unsigned-byte 32)
                  (logand (the (unsigned-byte 32) 4294967295)
                          (the (unsigned-byte 64)
                               (ash (the (unsigned-byte 128) x)
                                    -64))))))

Theorem: 32bits-p-of-call-gate-descriptorbits->offset63-32

(defthm 32bits-p-of-call-gate-descriptorbits->offset63-32
  (b*
    ((offset63-32 (call-gate-descriptorbits->offset63-32$inline x)))
    (32bits-p offset63-32))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->offset63-32$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->offset63-32$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->offset63-32$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->offset63-32$inline x)))

Theorem: call-gate-descriptorbits->offset63-32$inline-call-gate-descriptorbits-equiv-congruence-on-x

(defthm
 call-gate-descriptorbits->offset63-32$inline-call-gate-descriptorbits-equiv-congruence-on-x
 (implies
     (call-gate-descriptorbits-equiv x x-equiv)
     (equal (call-gate-descriptorbits->offset63-32$inline x)
            (call-gate-descriptorbits->offset63-32$inline x-equiv)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits->offset63-32-of-call-gate-descriptorbits

(defthm
  call-gate-descriptorbits->offset63-32-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->offset63-32
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (32bits-fix offset63-32)))

Theorem: call-gate-descriptorbits->offset63-32-of-write-with-mask

(defthm call-gate-descriptorbits->offset63-32-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          79228162495817593519834398720)
                  0))
      (equal (call-gate-descriptorbits->offset63-32 x)
             (call-gate-descriptorbits->offset63-32 y))))

Function: call-gate-descriptorbits->res2$inline

(defun call-gate-descriptorbits->res2$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 96 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 32)
                               (ash (the (unsigned-byte 128) x)
                                    -96))))))

Theorem: 8bits-p-of-call-gate-descriptorbits->res2

(defthm 8bits-p-of-call-gate-descriptorbits->res2
  (b* ((res2 (call-gate-descriptorbits->res2$inline x)))
    (8bits-p res2))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->res2$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->res2$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->res2$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->res2$inline x)))

Theorem: call-gate-descriptorbits->res2$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: call-gate-descriptorbits->res2-of-call-gate-descriptorbits

(defthm call-gate-descriptorbits->res2-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->res2
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (8bits-fix res2)))

Theorem: call-gate-descriptorbits->res2-of-write-with-mask

(defthm call-gate-descriptorbits->res2-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          20203181441137406086353707335680)
                  0))
      (equal (call-gate-descriptorbits->res2 x)
             (call-gate-descriptorbits->res2 y))))

Function: call-gate-descriptorbits->all-zeroes?$inline

(defun call-gate-descriptorbits->all-zeroes?$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 104 :width 5))
       :exec (the (unsigned-byte 5)
                  (logand (the (unsigned-byte 5) 31)
                          (the (unsigned-byte 24)
                               (ash (the (unsigned-byte 128) x)
                                    -104))))))

Theorem: 5bits-p-of-call-gate-descriptorbits->all-zeroes?

(defthm 5bits-p-of-call-gate-descriptorbits->all-zeroes?
  (b*
    ((all-zeroes? (call-gate-descriptorbits->all-zeroes?$inline x)))
    (5bits-p all-zeroes?))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->all-zeroes?$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->all-zeroes?$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->all-zeroes?$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->all-zeroes?$inline x)))

Theorem: call-gate-descriptorbits->all-zeroes?$inline-call-gate-descriptorbits-equiv-congruence-on-x

(defthm
 call-gate-descriptorbits->all-zeroes?$inline-call-gate-descriptorbits-equiv-congruence-on-x
 (implies
     (call-gate-descriptorbits-equiv x x-equiv)
     (equal (call-gate-descriptorbits->all-zeroes?$inline x)
            (call-gate-descriptorbits->all-zeroes?$inline x-equiv)))
 :rule-classes :congruence)

Theorem: call-gate-descriptorbits->all-zeroes?-of-call-gate-descriptorbits

(defthm
  call-gate-descriptorbits->all-zeroes?-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->all-zeroes?
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (5bits-fix all-zeroes?)))

Theorem: call-gate-descriptorbits->all-zeroes?-of-write-with-mask

(defthm call-gate-descriptorbits->all-zeroes?-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          628754697713201783142364789866496)
                  0))
      (equal (call-gate-descriptorbits->all-zeroes? x)
             (call-gate-descriptorbits->all-zeroes? y))))

Function: call-gate-descriptorbits->res3$inline

(defun call-gate-descriptorbits->res3$inline (x)
  (declare (xargs :guard (call-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptorbits-fix x)))
         (part-select x :low 109 :width 19))
       :exec (the (unsigned-byte 19)
                  (logand (the (unsigned-byte 19) 524287)
                          (the (unsigned-byte 19)
                               (ash (the (unsigned-byte 128) x)
                                    -109))))))

Theorem: 19bits-p-of-call-gate-descriptorbits->res3

(defthm 19bits-p-of-call-gate-descriptorbits->res3
  (b* ((res3 (call-gate-descriptorbits->res3$inline x)))
    (19bits-p res3))
  :rule-classes :rewrite)

Theorem: call-gate-descriptorbits->res3$inline-of-call-gate-descriptorbits-fix-x

(defthm
 call-gate-descriptorbits->res3$inline-of-call-gate-descriptorbits-fix-x
 (equal (call-gate-descriptorbits->res3$inline
             (call-gate-descriptorbits-fix x))
        (call-gate-descriptorbits->res3$inline x)))

Theorem: call-gate-descriptorbits->res3$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: call-gate-descriptorbits->res3-of-call-gate-descriptorbits

(defthm call-gate-descriptorbits->res3-of-call-gate-descriptorbits
 (equal
  (call-gate-descriptorbits->res3
    (call-gate-descriptorbits offset15-0
                              selector res1 type s dpl p offset31-16
                              offset63-32 res2 all-zeroes? res3))
  (19bits-fix res3)))

Theorem: call-gate-descriptorbits->res3-of-write-with-mask

(defthm call-gate-descriptorbits->res3-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                call-gate-descriptorbits-equiv-under-mask)
           (call-gate-descriptorbits-equiv-under-mask x y fty::mask)
           (equal (logand (lognot fty::mask)
                          340281717883831146609921041119727058944)
                  0))
      (equal (call-gate-descriptorbits->res3 x)
             (call-gate-descriptorbits->res3 y))))

Theorem: call-gate-descriptorbits-fix-in-terms-of-call-gate-descriptorbits

(defthm
  call-gate-descriptorbits-fix-in-terms-of-call-gate-descriptorbits
  (equal (call-gate-descriptorbits-fix x)
         (change-call-gate-descriptorbits x)))

Function: !call-gate-descriptorbits->offset15-0$inline

(defun !call-gate-descriptorbits->offset15-0$inline (offset15-0 x)
 (declare (xargs :guard (and (16bits-p offset15-0)
                             (call-gate-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((offset15-0 (mbe :logic (16bits-fix offset15-0)
                           :exec offset15-0))
          (x (call-gate-descriptorbits-fix x)))
       (part-install offset15-0 x
                     :width 16
                     :low 0))
     :exec (the (unsigned-byte 128)
                (logior (the (unsigned-byte 128)
                             (logand (the (unsigned-byte 128) x)
                                     (the (signed-byte 17) -65536)))
                        (the (unsigned-byte 16) offset15-0)))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->offset15-0

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

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

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

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

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

Theorem: !call-gate-descriptorbits->offset15-0$inline-of-call-gate-descriptorbits-fix-x

(defthm
 !call-gate-descriptorbits->offset15-0$inline-of-call-gate-descriptorbits-fix-x
 (equal
      (!call-gate-descriptorbits->offset15-0$inline
           offset15-0
           (call-gate-descriptorbits-fix x))
      (!call-gate-descriptorbits->offset15-0$inline offset15-0 x)))

Theorem: !call-gate-descriptorbits->offset15-0$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !call-gate-descriptorbits->offset15-0-is-call-gate-descriptorbits

(defthm
  !call-gate-descriptorbits->offset15-0-is-call-gate-descriptorbits
  (equal (!call-gate-descriptorbits->offset15-0 offset15-0 x)
         (change-call-gate-descriptorbits x
                                          :offset15-0 offset15-0)))

Theorem: call-gate-descriptorbits->offset15-0-of-!call-gate-descriptorbits->offset15-0

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

Theorem: !call-gate-descriptorbits->offset15-0-equiv-under-mask

(defthm !call-gate-descriptorbits->offset15-0-equiv-under-mask
 (b*
  ((?new-x
       (!call-gate-descriptorbits->offset15-0$inline offset15-0 x)))
  (call-gate-descriptorbits-equiv-under-mask new-x x -65536)))

Function: !call-gate-descriptorbits->selector$inline

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

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->selector

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

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

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

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

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

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

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

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

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

Theorem: !call-gate-descriptorbits->selector-is-call-gate-descriptorbits

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

Theorem: call-gate-descriptorbits->selector-of-!call-gate-descriptorbits->selector

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

Theorem: !call-gate-descriptorbits->selector-equiv-under-mask

(defthm !call-gate-descriptorbits->selector-equiv-under-mask
 (b*
  ((?new-x (!call-gate-descriptorbits->selector$inline selector x)))
  (call-gate-descriptorbits-equiv-under-mask new-x x -4294901761)))

Function: !call-gate-descriptorbits->res1$inline

(defun !call-gate-descriptorbits->res1$inline (res1 x)
 (declare (xargs :guard (and (8bits-p res1)
                             (call-gate-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((res1 (mbe :logic (8bits-fix res1)
                   :exec res1))
        (x (call-gate-descriptorbits-fix x)))
     (part-install res1 x :width 8 :low 32))
   :exec
   (the (unsigned-byte 128)
        (logior (the (unsigned-byte 128)
                     (logand (the (unsigned-byte 128) x)
                             (the (signed-byte 41) -1095216660481)))
                (the (unsigned-byte 40)
                     (ash (the (unsigned-byte 8) res1)
                          32))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->res1

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

Theorem: !call-gate-descriptorbits->res1$inline-of-8bits-fix-res1

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

Theorem: !call-gate-descriptorbits->res1$inline-8bits-equiv-congruence-on-res1

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

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

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

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

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

Theorem: !call-gate-descriptorbits->res1-is-call-gate-descriptorbits

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

Theorem: call-gate-descriptorbits->res1-of-!call-gate-descriptorbits->res1

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

Theorem: !call-gate-descriptorbits->res1-equiv-under-mask

(defthm !call-gate-descriptorbits->res1-equiv-under-mask
  (b* ((?new-x (!call-gate-descriptorbits->res1$inline res1 x)))
    (call-gate-descriptorbits-equiv-under-mask
         new-x x -1095216660481)))

Function: !call-gate-descriptorbits->type$inline

(defun !call-gate-descriptorbits->type$inline (type x)
 (declare (xargs :guard (and (4bits-p type)
                             (call-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((type (mbe :logic (4bits-fix type)
                  :exec type))
       (x (call-gate-descriptorbits-fix x)))
    (part-install type x :width 4 :low 40))
  :exec
  (the (unsigned-byte 128)
       (logior (the (unsigned-byte 128)
                    (logand (the (unsigned-byte 128) x)
                            (the (signed-byte 45) -16492674416641)))
               (the (unsigned-byte 44)
                    (ash (the (unsigned-byte 4) type)
                         40))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->type

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

Theorem: !call-gate-descriptorbits->type$inline-of-4bits-fix-type

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

Theorem: !call-gate-descriptorbits->type$inline-4bits-equiv-congruence-on-type

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

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

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

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

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

Theorem: !call-gate-descriptorbits->type-is-call-gate-descriptorbits

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

Theorem: call-gate-descriptorbits->type-of-!call-gate-descriptorbits->type

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

Theorem: !call-gate-descriptorbits->type-equiv-under-mask

(defthm !call-gate-descriptorbits->type-equiv-under-mask
  (b* ((?new-x (!call-gate-descriptorbits->type$inline type x)))
    (call-gate-descriptorbits-equiv-under-mask
         new-x x -16492674416641)))

Function: !call-gate-descriptorbits->s$inline

(defun !call-gate-descriptorbits->s$inline (s x)
 (declare (xargs :guard (and (bitp s)
                             (call-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((s (mbe :logic (bfix s) :exec s))
       (x (call-gate-descriptorbits-fix x)))
    (part-install s x :width 1 :low 44))
  :exec
  (the (unsigned-byte 128)
       (logior (the (unsigned-byte 128)
                    (logand (the (unsigned-byte 128) x)
                            (the (signed-byte 46) -17592186044417)))
               (the (unsigned-byte 45)
                    (ash (the (unsigned-byte 1) s) 44))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->s

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

Theorem: !call-gate-descriptorbits->s$inline-of-bfix-s

(defthm !call-gate-descriptorbits->s$inline-of-bfix-s
  (equal (!call-gate-descriptorbits->s$inline (bfix s)
                                              x)
         (!call-gate-descriptorbits->s$inline s x)))

Theorem: !call-gate-descriptorbits->s$inline-bit-equiv-congruence-on-s

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

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

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

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

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

Theorem: !call-gate-descriptorbits->s-is-call-gate-descriptorbits

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

Theorem: call-gate-descriptorbits->s-of-!call-gate-descriptorbits->s

(defthm call-gate-descriptorbits->s-of-!call-gate-descriptorbits->s
  (b* ((?new-x (!call-gate-descriptorbits->s$inline s x)))
    (equal (call-gate-descriptorbits->s new-x)
           (bfix s))))

Theorem: !call-gate-descriptorbits->s-equiv-under-mask

(defthm !call-gate-descriptorbits->s-equiv-under-mask
  (b* ((?new-x (!call-gate-descriptorbits->s$inline s x)))
    (call-gate-descriptorbits-equiv-under-mask
         new-x x -17592186044417)))

Function: !call-gate-descriptorbits->dpl$inline

(defun !call-gate-descriptorbits->dpl$inline (dpl x)
  (declare (xargs :guard (and (2bits-p dpl)
                              (call-gate-descriptorbits-p x))))
  (mbe :logic
       (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl))
            (x (call-gate-descriptorbits-fix x)))
         (part-install dpl x :width 2 :low 45))
       :exec (the (unsigned-byte 128)
                  (logior (the (unsigned-byte 128)
                               (logand (the (unsigned-byte 128) x)
                                       (the (signed-byte 48)
                                            -105553116266497)))
                          (the (unsigned-byte 47)
                               (ash (the (unsigned-byte 2) dpl)
                                    45))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->dpl

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

Theorem: !call-gate-descriptorbits->dpl$inline-of-2bits-fix-dpl

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

Theorem: !call-gate-descriptorbits->dpl$inline-2bits-equiv-congruence-on-dpl

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

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

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

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

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

Theorem: !call-gate-descriptorbits->dpl-is-call-gate-descriptorbits

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

Theorem: call-gate-descriptorbits->dpl-of-!call-gate-descriptorbits->dpl

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

Theorem: !call-gate-descriptorbits->dpl-equiv-under-mask

(defthm !call-gate-descriptorbits->dpl-equiv-under-mask
  (b* ((?new-x (!call-gate-descriptorbits->dpl$inline dpl x)))
    (call-gate-descriptorbits-equiv-under-mask
         new-x x -105553116266497)))

Function: !call-gate-descriptorbits->p$inline

(defun !call-gate-descriptorbits->p$inline (p x)
 (declare (xargs :guard (and (bitp p)
                             (call-gate-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((p (mbe :logic (bfix p) :exec p))
          (x (call-gate-descriptorbits-fix x)))
       (part-install p x :width 1 :low 47))
     :exec (the (unsigned-byte 128)
                (logior (the (unsigned-byte 128)
                             (logand (the (unsigned-byte 128) x)
                                     (the (signed-byte 49)
                                          -140737488355329)))
                        (the (unsigned-byte 48)
                             (ash (the (unsigned-byte 1) p) 47))))))

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

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

Theorem: !call-gate-descriptorbits->p$inline-of-bfix-p

(defthm !call-gate-descriptorbits->p$inline-of-bfix-p
  (equal (!call-gate-descriptorbits->p$inline (bfix p)
                                              x)
         (!call-gate-descriptorbits->p$inline p x)))

Theorem: !call-gate-descriptorbits->p$inline-bit-equiv-congruence-on-p

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

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

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

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

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

Theorem: !call-gate-descriptorbits->p-is-call-gate-descriptorbits

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

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

(defthm call-gate-descriptorbits->p-of-!call-gate-descriptorbits->p
  (b* ((?new-x (!call-gate-descriptorbits->p$inline p x)))
    (equal (call-gate-descriptorbits->p new-x)
           (bfix p))))

Theorem: !call-gate-descriptorbits->p-equiv-under-mask

(defthm !call-gate-descriptorbits->p-equiv-under-mask
  (b* ((?new-x (!call-gate-descriptorbits->p$inline p x)))
    (call-gate-descriptorbits-equiv-under-mask
         new-x x -140737488355329)))

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)))

Function: !call-gate-descriptorbits->offset63-32$inline

(defun !call-gate-descriptorbits->offset63-32$inline (offset63-32 x)
 (declare (xargs :guard (and (32bits-p offset63-32)
                             (call-gate-descriptorbits-p x))))
 (mbe
    :logic
    (b* ((offset63-32 (mbe :logic (32bits-fix offset63-32)
                           :exec offset63-32))
         (x (call-gate-descriptorbits-fix x)))
      (part-install offset63-32 x
                    :width 32
                    :low 64))
    :exec
    (the (unsigned-byte 128)
         (logior (the (unsigned-byte 128)
                      (logand (the (unsigned-byte 128) x)
                              (the (signed-byte 97)
                                   -79228162495817593519834398721)))
                 (the (unsigned-byte 96)
                      (ash (the (unsigned-byte 32) offset63-32)
                           64))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->offset63-32

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

Theorem: !call-gate-descriptorbits->offset63-32$inline-of-32bits-fix-offset63-32

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

Theorem: !call-gate-descriptorbits->offset63-32$inline-32bits-equiv-congruence-on-offset63-32

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

Theorem: !call-gate-descriptorbits->offset63-32$inline-of-call-gate-descriptorbits-fix-x

(defthm
 !call-gate-descriptorbits->offset63-32$inline-of-call-gate-descriptorbits-fix-x
 (equal
     (!call-gate-descriptorbits->offset63-32$inline
          offset63-32
          (call-gate-descriptorbits-fix x))
     (!call-gate-descriptorbits->offset63-32$inline offset63-32 x)))

Theorem: !call-gate-descriptorbits->offset63-32$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !call-gate-descriptorbits->offset63-32-is-call-gate-descriptorbits

(defthm
 !call-gate-descriptorbits->offset63-32-is-call-gate-descriptorbits
 (equal (!call-gate-descriptorbits->offset63-32 offset63-32 x)
        (change-call-gate-descriptorbits x
                                         :offset63-32 offset63-32)))

Theorem: call-gate-descriptorbits->offset63-32-of-!call-gate-descriptorbits->offset63-32

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

Theorem: !call-gate-descriptorbits->offset63-32-equiv-under-mask

(defthm !call-gate-descriptorbits->offset63-32-equiv-under-mask
 (b*
  ((?new-x
     (!call-gate-descriptorbits->offset63-32$inline offset63-32 x)))
  (call-gate-descriptorbits-equiv-under-mask
       new-x
       x -79228162495817593519834398721)))

Function: !call-gate-descriptorbits->res2$inline

(defun !call-gate-descriptorbits->res2$inline (res2 x)
 (declare (xargs :guard (and (8bits-p res2)
                             (call-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((res2 (mbe :logic (8bits-fix res2)
                  :exec res2))
       (x (call-gate-descriptorbits-fix x)))
    (part-install res2 x :width 8 :low 96))
  :exec
  (the
      (unsigned-byte 128)
      (logior (the (unsigned-byte 128)
                   (logand (the (unsigned-byte 128) x)
                           (the (signed-byte 105)
                                -20203181441137406086353707335681)))
              (the (unsigned-byte 104)
                   (ash (the (unsigned-byte 8) res2)
                        96))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->res2

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

Theorem: !call-gate-descriptorbits->res2$inline-of-8bits-fix-res2

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

Theorem: !call-gate-descriptorbits->res2$inline-8bits-equiv-congruence-on-res2

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

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

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

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

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

Theorem: !call-gate-descriptorbits->res2-is-call-gate-descriptorbits

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

Theorem: call-gate-descriptorbits->res2-of-!call-gate-descriptorbits->res2

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

Theorem: !call-gate-descriptorbits->res2-equiv-under-mask

(defthm !call-gate-descriptorbits->res2-equiv-under-mask
  (b* ((?new-x (!call-gate-descriptorbits->res2$inline res2 x)))
    (call-gate-descriptorbits-equiv-under-mask
         new-x
         x -20203181441137406086353707335681)))

Function: !call-gate-descriptorbits->all-zeroes?$inline

(defun !call-gate-descriptorbits->all-zeroes?$inline (all-zeroes? x)
 (declare (xargs :guard (and (5bits-p all-zeroes?)
                             (call-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((all-zeroes? (mbe :logic (5bits-fix all-zeroes?)
                         :exec all-zeroes?))
       (x (call-gate-descriptorbits-fix x)))
    (part-install all-zeroes? x
                  :width 5
                  :low 104))
  :exec
  (the
     (unsigned-byte 128)
     (logior (the (unsigned-byte 128)
                  (logand (the (unsigned-byte 128) x)
                          (the (signed-byte 110)
                               -628754697713201783142364789866497)))
             (the (unsigned-byte 109)
                  (ash (the (unsigned-byte 5) all-zeroes?)
                       104))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->all-zeroes?

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

Theorem: !call-gate-descriptorbits->all-zeroes?$inline-of-5bits-fix-all-zeroes?

(defthm
 !call-gate-descriptorbits->all-zeroes?$inline-of-5bits-fix-all-zeroes?
 (equal
     (!call-gate-descriptorbits->all-zeroes?$inline
          (5bits-fix all-zeroes?)
          x)
     (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x)))

Theorem: !call-gate-descriptorbits->all-zeroes?$inline-5bits-equiv-congruence-on-all-zeroes?

(defthm
 !call-gate-descriptorbits->all-zeroes?$inline-5bits-equiv-congruence-on-all-zeroes?
 (implies
  (5bits-equiv all-zeroes? all-zeroes?-equiv)
  (equal
       (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x)
       (!call-gate-descriptorbits->all-zeroes?$inline
            all-zeroes?-equiv x)))
 :rule-classes :congruence)

Theorem: !call-gate-descriptorbits->all-zeroes?$inline-of-call-gate-descriptorbits-fix-x

(defthm
 !call-gate-descriptorbits->all-zeroes?$inline-of-call-gate-descriptorbits-fix-x
 (equal
     (!call-gate-descriptorbits->all-zeroes?$inline
          all-zeroes?
          (call-gate-descriptorbits-fix x))
     (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x)))

Theorem: !call-gate-descriptorbits->all-zeroes?$inline-call-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !call-gate-descriptorbits->all-zeroes?-is-call-gate-descriptorbits

(defthm
 !call-gate-descriptorbits->all-zeroes?-is-call-gate-descriptorbits
 (equal (!call-gate-descriptorbits->all-zeroes? all-zeroes? x)
        (change-call-gate-descriptorbits x
                                         :all-zeroes? all-zeroes?)))

Theorem: call-gate-descriptorbits->all-zeroes?-of-!call-gate-descriptorbits->all-zeroes?

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

Theorem: !call-gate-descriptorbits->all-zeroes?-equiv-under-mask

(defthm !call-gate-descriptorbits->all-zeroes?-equiv-under-mask
 (b*
  ((?new-x
     (!call-gate-descriptorbits->all-zeroes?$inline all-zeroes? x)))
  (call-gate-descriptorbits-equiv-under-mask
       new-x
       x -628754697713201783142364789866497)))

Function: !call-gate-descriptorbits->res3$inline

(defun !call-gate-descriptorbits->res3$inline (res3 x)
 (declare (xargs :guard (and (19bits-p res3)
                             (call-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((res3 (mbe :logic (19bits-fix res3)
                  :exec res3))
       (x (call-gate-descriptorbits-fix x)))
    (part-install res3 x
                  :width 19
                  :low 109))
  :exec
  (the
   (unsigned-byte 128)
   (logior
       (the (unsigned-byte 128)
            (logand (the (unsigned-byte 128) x)
                    (the (signed-byte 129)
                         -340281717883831146609921041119727058945)))
       (the (unsigned-byte 128)
            (ash (the (unsigned-byte 19) res3)
                 109))))))

Theorem: call-gate-descriptorbits-p-of-!call-gate-descriptorbits->res3

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

Theorem: !call-gate-descriptorbits->res3$inline-of-19bits-fix-res3

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

Theorem: !call-gate-descriptorbits->res3$inline-19bits-equiv-congruence-on-res3

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

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

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

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

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

Theorem: !call-gate-descriptorbits->res3-is-call-gate-descriptorbits

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

Theorem: call-gate-descriptorbits->res3-of-!call-gate-descriptorbits->res3

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

Theorem: !call-gate-descriptorbits->res3-equiv-under-mask

(defthm !call-gate-descriptorbits->res3-equiv-under-mask
  (b* ((?new-x (!call-gate-descriptorbits->res3$inline res3 x)))
    (call-gate-descriptorbits-equiv-under-mask
         new-x
         x 649037107316853453566312041152511)))

Function: call-gate-descriptorbits-debug

(defun call-gate-descriptorbits-debug (x)
 (declare (xargs :guard (call-gate-descriptorbits-p x)))
 (let ((__function__ 'call-gate-descriptorbits-debug))
  (declare (ignorable __function__))
  (b* (((call-gate-descriptorbits x)))
   (cons
    (cons 'offset15-0 x.offset15-0)
    (cons
     (cons 'selector x.selector)
     (cons
      (cons 'res1 x.res1)
      (cons
       (cons 'type x.type)
       (cons
        (cons 's x.s)
        (cons
         (cons 'dpl x.dpl)
         (cons
           (cons 'p x.p)
           (cons (cons 'offset31-16 x.offset31-16)
                 (cons (cons 'offset63-32 x.offset63-32)
                       (cons (cons 'res2 x.res2)
                             (cons (cons 'all-zeroes? x.all-zeroes?)
                                   (cons (cons 'res3 x.res3)
                                         nil)))))))))))))))

Subtopics

Call-gate-descriptorbits-p: Recognizer for call-gate-descriptorbits bit structures.
!call-gate-descriptorbits->offset63-32: Update the |X86ISA|::|OFFSET63-32| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->offset31-16: Update the |X86ISA|::|OFFSET31-16| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->all-zeroes?: Update the |X86ISA|::|ALL-ZEROES?| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->offset15-0: Update the |X86ISA|::|OFFSET15-0| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->selector: Update the |X86ISA|::|SELECTOR| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->res3: Update the |X86ISA|::|RES3| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->type: Update the |COMMON-LISP|::|TYPE| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->res2: Update the |X86ISA|::|RES2| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->res1: Update the |X86ISA|::|RES1| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->dpl: Update the |X86ISA|::|DPL| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->s: Update the |X86ISA|::|S| field of a call-gate-descriptorbits bit structure.
!call-gate-descriptorbits->p: Update the |ACL2|::|P| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->offset63-32: Access the |X86ISA|::|OFFSET63-32| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->offset31-16: Access the |X86ISA|::|OFFSET31-16| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->all-zeroes?: Access the |X86ISA|::|ALL-ZEROES?| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->selector: Access the |X86ISA|::|SELECTOR| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->offset15-0: Access the |X86ISA|::|OFFSET15-0| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits-fix: Fixing function for call-gate-descriptorbits bit structures.
Call-gate-descriptorbits->type: Access the |COMMON-LISP|::|TYPE| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->res3: Access the |X86ISA|::|RES3| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->res2: Access the |X86ISA|::|RES2| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->res1: Access the |X86ISA|::|RES1| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->s: Access the |X86ISA|::|S| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->dpl: Access the |X86ISA|::|DPL| field of a call-gate-descriptorbits bit structure.
Call-gate-descriptorbits->p: Access the |ACL2|::|P| field of a call-gate-descriptorbits bit structure.