		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Interrupt/trap-gate-descriptorbits

AMD manual, Jun'23, Vol. 2, Figures 4-24 and 4-18.

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

Fields

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

Definitions and Theorems

Function: interrupt/trap-gate-descriptorbits-p

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

Theorem: interrupt/trap-gate-descriptorbits-p-when-unsigned-byte-p

(defthm interrupt/trap-gate-descriptorbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 128 x)
           (interrupt/trap-gate-descriptorbits-p x)))

Theorem: unsigned-byte-p-when-interrupt/trap-gate-descriptorbits-p

(defthm unsigned-byte-p-when-interrupt/trap-gate-descriptorbits-p
  (implies (interrupt/trap-gate-descriptorbits-p x)
           (unsigned-byte-p 128 x)))

Theorem: interrupt/trap-gate-descriptorbits-p-compound-recognizer

(defthm interrupt/trap-gate-descriptorbits-p-compound-recognizer
  (implies (interrupt/trap-gate-descriptorbits-p x)
           (natp x))
  :rule-classes :compound-recognizer)

Function: interrupt/trap-gate-descriptorbits-fix

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

Theorem: interrupt/trap-gate-descriptorbits-p-of-interrupt/trap-gate-descriptorbits-fix

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

Theorem: interrupt/trap-gate-descriptorbits-fix-when-interrupt/trap-gate-descriptorbits-p

(defthm
 interrupt/trap-gate-descriptorbits-fix-when-interrupt/trap-gate-descriptorbits-p
 (implies (interrupt/trap-gate-descriptorbits-p x)
          (equal (interrupt/trap-gate-descriptorbits-fix x)
                 x)))

Function: interrupt/trap-gate-descriptorbits-equiv$inline

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

Theorem: interrupt/trap-gate-descriptorbits-equiv-is-an-equivalence

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

Theorem: interrupt/trap-gate-descriptorbits-equiv-implies-equal-interrupt/trap-gate-descriptorbits-fix-1

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

Theorem: interrupt/trap-gate-descriptorbits-fix-under-interrupt/trap-gate-descriptorbits-equiv

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

Function: interrupt/trap-gate-descriptorbits

(defun interrupt/trap-gate-descriptorbits
       (offset15-0 selector
                   ist res1 type s dpl p offset31-16
                   offset63-32 res2 all-zeros? res3)
 (declare (xargs :guard (and (16bits-p offset15-0)
                             (16bits-p selector)
                             (3bits-p ist)
                             (5bits-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-zeros?)
                             (19bits-p res3))))
 (let ((__function__ 'interrupt/trap-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))
       (ist (mbe :logic (3bits-fix ist) :exec ist))
       (res1 (mbe :logic (5bits-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-zeros? (mbe :logic (5bits-fix all-zeros?)
                        :exec all-zeros?))
       (res3 (mbe :logic (19bits-fix res3)
                  :exec res3)))
   (logapp
    16 offset15-0
    (logapp
     16 selector
     (logapp
      3 ist
      (logapp
       5 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-zeros? res3)))))))))))))))

Theorem: interrupt/trap-gate-descriptorbits-p-of-interrupt/trap-gate-descriptorbits

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

Theorem: interrupt/trap-gate-descriptorbits-of-16bits-fix-offset15-0

(defthm interrupt/trap-gate-descriptorbits-of-16bits-fix-offset15-0
  (equal (interrupt/trap-gate-descriptorbits
              (16bits-fix offset15-0)
              selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-16bits-equiv-congruence-on-offset15-0

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

Theorem: interrupt/trap-gate-descriptorbits-of-16bits-fix-selector

(defthm interrupt/trap-gate-descriptorbits-of-16bits-fix-selector
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0 (16bits-fix selector)
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-16bits-equiv-congruence-on-selector

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

Theorem: interrupt/trap-gate-descriptorbits-of-3bits-fix-ist

(defthm interrupt/trap-gate-descriptorbits-of-3bits-fix-ist
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0 selector (3bits-fix ist)
              res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-3bits-equiv-congruence-on-ist

(defthm
   interrupt/trap-gate-descriptorbits-3bits-equiv-congruence-on-ist
  (implies (3bits-equiv ist ist-equiv)
           (equal (interrupt/trap-gate-descriptorbits
                       offset15-0 selector
                       ist res1 type s dpl p offset31-16
                       offset63-32 res2 all-zeros? res3)
                  (interrupt/trap-gate-descriptorbits
                       offset15-0 selector
                       ist-equiv res1 type s dpl p offset31-16
                       offset63-32 res2 all-zeros? res3)))
  :rule-classes :congruence)

Theorem: interrupt/trap-gate-descriptorbits-of-5bits-fix-res1

(defthm interrupt/trap-gate-descriptorbits-of-5bits-fix-res1
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0 selector ist (5bits-fix res1)
              type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-5bits-equiv-congruence-on-res1

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

Theorem: interrupt/trap-gate-descriptorbits-of-4bits-fix-type

(defthm interrupt/trap-gate-descriptorbits-of-4bits-fix-type
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0
              selector ist res1 (4bits-fix type)
              s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-4bits-equiv-congruence-on-type

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

Theorem: interrupt/trap-gate-descriptorbits-of-bfix-s

(defthm interrupt/trap-gate-descriptorbits-of-bfix-s
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0
              selector ist res1 type (bfix s)
              dpl p offset31-16
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-bit-equiv-congruence-on-s

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

Theorem: interrupt/trap-gate-descriptorbits-of-2bits-fix-dpl

(defthm interrupt/trap-gate-descriptorbits-of-2bits-fix-dpl
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0
              selector ist res1 type s (2bits-fix dpl)
              p offset31-16
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-2bits-equiv-congruence-on-dpl

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

Theorem: interrupt/trap-gate-descriptorbits-of-bfix-p

(defthm interrupt/trap-gate-descriptorbits-of-bfix-p
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0
              selector ist res1 type s dpl (bfix p)
              offset31-16
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-bit-equiv-congruence-on-p

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

Theorem: interrupt/trap-gate-descriptorbits-of-16bits-fix-offset31-16

(defthm interrupt/trap-gate-descriptorbits-of-16bits-fix-offset31-16
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0 selector ist res1
              type s dpl p (16bits-fix offset31-16)
              offset63-32 res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-16bits-equiv-congruence-on-offset31-16

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

Theorem: interrupt/trap-gate-descriptorbits-of-32bits-fix-offset63-32

(defthm interrupt/trap-gate-descriptorbits-of-32bits-fix-offset63-32
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0 selector ist res1 type s dpl
              p offset31-16 (32bits-fix offset63-32)
              res2 all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-32bits-equiv-congruence-on-offset63-32

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

Theorem: interrupt/trap-gate-descriptorbits-of-8bits-fix-res2

(defthm interrupt/trap-gate-descriptorbits-of-8bits-fix-res2
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0
              selector ist res1 type s dpl p
              offset31-16 offset63-32 (8bits-fix res2)
              all-zeros? res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-8bits-equiv-congruence-on-res2

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

Theorem: interrupt/trap-gate-descriptorbits-of-5bits-fix-all-zeros?

(defthm interrupt/trap-gate-descriptorbits-of-5bits-fix-all-zeros?
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 (5bits-fix all-zeros?)
              res3)
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-5bits-equiv-congruence-on-all-zeros?

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

Theorem: interrupt/trap-gate-descriptorbits-of-19bits-fix-res3

(defthm interrupt/trap-gate-descriptorbits-of-19bits-fix-res3
  (equal (interrupt/trap-gate-descriptorbits
              offset15-0 selector ist res1
              type s dpl p offset31-16 offset63-32
              res2 all-zeros? (19bits-fix res3))
         (interrupt/trap-gate-descriptorbits
              offset15-0 selector
              ist res1 type s dpl p offset31-16
              offset63-32 res2 all-zeros? res3)))

Theorem: interrupt/trap-gate-descriptorbits-19bits-equiv-congruence-on-res3

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

Function: interrupt/trap-gate-descriptorbits-equiv-under-mask

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

Function: interrupt/trap-gate-descriptorbits->offset15-0$inline

(defun interrupt/trap-gate-descriptorbits->offset15-0$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->offset15-0

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

Theorem: interrupt/trap-gate-descriptorbits->offset15-0$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->offset15-0$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->offset15-0$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->offset15-0$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->offset15-0$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->offset15-0-of-interrupt/trap-gate-descriptorbits

(defthm
 interrupt/trap-gate-descriptorbits->offset15-0-of-interrupt/trap-gate-descriptorbits
 (equal (interrupt/trap-gate-descriptorbits->offset15-0
             (interrupt/trap-gate-descriptorbits
                  offset15-0 selector
                  ist res1 type s dpl p offset31-16
                  offset63-32 res2 all-zeros? res3))
        (16bits-fix offset15-0)))

Theorem: interrupt/trap-gate-descriptorbits->offset15-0-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->selector$inline

(defun interrupt/trap-gate-descriptorbits->selector$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->selector

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

Theorem: interrupt/trap-gate-descriptorbits->selector$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->selector$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->selector$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->selector$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->selector$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->selector-of-interrupt/trap-gate-descriptorbits

(defthm
 interrupt/trap-gate-descriptorbits->selector-of-interrupt/trap-gate-descriptorbits
 (equal (interrupt/trap-gate-descriptorbits->selector
             (interrupt/trap-gate-descriptorbits
                  offset15-0 selector
                  ist res1 type s dpl p offset31-16
                  offset63-32 res2 all-zeros? res3))
        (16bits-fix selector)))

Theorem: interrupt/trap-gate-descriptorbits->selector-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->ist$inline

(defun interrupt/trap-gate-descriptorbits->ist$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-gate-descriptorbits-fix x)))
         (part-select x :low 32 :width 3))
       :exec (the (unsigned-byte 3)
                  (logand (the (unsigned-byte 3) 7)
                          (the (unsigned-byte 96)
                               (ash (the (unsigned-byte 128) x)
                                    -32))))))

Theorem: 3bits-p-of-interrupt/trap-gate-descriptorbits->ist

(defthm 3bits-p-of-interrupt/trap-gate-descriptorbits->ist
  (b* ((ist (interrupt/trap-gate-descriptorbits->ist$inline x)))
    (3bits-p ist))
  :rule-classes :rewrite)

Theorem: interrupt/trap-gate-descriptorbits->ist$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->ist$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->ist$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->ist$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->ist$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

(defthm
 interrupt/trap-gate-descriptorbits->ist$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x
 (implies
   (interrupt/trap-gate-descriptorbits-equiv x x-equiv)
   (equal (interrupt/trap-gate-descriptorbits->ist$inline x)
          (interrupt/trap-gate-descriptorbits->ist$inline x-equiv)))
 :rule-classes :congruence)

Theorem: interrupt/trap-gate-descriptorbits->ist-of-interrupt/trap-gate-descriptorbits

(defthm
 interrupt/trap-gate-descriptorbits->ist-of-interrupt/trap-gate-descriptorbits
 (equal (interrupt/trap-gate-descriptorbits->ist
             (interrupt/trap-gate-descriptorbits
                  offset15-0 selector
                  ist res1 type s dpl p offset31-16
                  offset63-32 res2 all-zeros? res3))
        (3bits-fix ist)))

Theorem: interrupt/trap-gate-descriptorbits->ist-of-write-with-mask

(defthm interrupt/trap-gate-descriptorbits->ist-of-write-with-mask
 (implies
      (and (fty::bitstruct-read-over-write-hyps
                x
                interrupt/trap-gate-descriptorbits-equiv-under-mask)
           (interrupt/trap-gate-descriptorbits-equiv-under-mask
                x y fty::mask)
           (equal (logand (lognot fty::mask) 30064771072)
                  0))
      (equal (interrupt/trap-gate-descriptorbits->ist x)
             (interrupt/trap-gate-descriptorbits->ist y))))

Function: interrupt/trap-gate-descriptorbits->res1$inline

(defun interrupt/trap-gate-descriptorbits->res1$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-gate-descriptorbits-fix x)))
         (part-select x :low 35 :width 5))
       :exec (the (unsigned-byte 5)
                  (logand (the (unsigned-byte 5) 31)
                          (the (unsigned-byte 93)
                               (ash (the (unsigned-byte 128) x)
                                    -35))))))

Theorem: 5bits-p-of-interrupt/trap-gate-descriptorbits->res1

(defthm 5bits-p-of-interrupt/trap-gate-descriptorbits->res1
  (b* ((res1 (interrupt/trap-gate-descriptorbits->res1$inline x)))
    (5bits-p res1))
  :rule-classes :rewrite)

Theorem: interrupt/trap-gate-descriptorbits->res1$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->res1$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->res1$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->res1$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->res1$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->res1-of-interrupt/trap-gate-descriptorbits

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

Theorem: interrupt/trap-gate-descriptorbits->res1-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->type$inline

(defun interrupt/trap-gate-descriptorbits->type$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->type

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

Theorem: interrupt/trap-gate-descriptorbits->type$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->type$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->type$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->type$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->type$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->type-of-interrupt/trap-gate-descriptorbits

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

Theorem: interrupt/trap-gate-descriptorbits->type-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->s$inline

(defun interrupt/trap-gate-descriptorbits->s$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->s

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

Theorem: interrupt/trap-gate-descriptorbits->s$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->s$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->s$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->s$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->s$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->s-of-interrupt/trap-gate-descriptorbits

(defthm
 interrupt/trap-gate-descriptorbits->s-of-interrupt/trap-gate-descriptorbits
 (equal (interrupt/trap-gate-descriptorbits->s
             (interrupt/trap-gate-descriptorbits
                  offset15-0 selector
                  ist res1 type s dpl p offset31-16
                  offset63-32 res2 all-zeros? res3))
        (bfix s)))

Theorem: interrupt/trap-gate-descriptorbits->s-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->dpl$inline

(defun interrupt/trap-gate-descriptorbits->dpl$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->dpl

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

Theorem: interrupt/trap-gate-descriptorbits->dpl$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->dpl$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->dpl$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->dpl$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->dpl$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->dpl-of-interrupt/trap-gate-descriptorbits

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

Theorem: interrupt/trap-gate-descriptorbits->dpl-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->p$inline

(defun interrupt/trap-gate-descriptorbits->p$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->p

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

Theorem: interrupt/trap-gate-descriptorbits->p$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->p$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->p$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->p$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->p$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->p-of-interrupt/trap-gate-descriptorbits

(defthm
 interrupt/trap-gate-descriptorbits->p-of-interrupt/trap-gate-descriptorbits
 (equal (interrupt/trap-gate-descriptorbits->p
             (interrupt/trap-gate-descriptorbits
                  offset15-0 selector
                  ist res1 type s dpl p offset31-16
                  offset63-32 res2 all-zeros? res3))
        (bfix p)))

Theorem: interrupt/trap-gate-descriptorbits->p-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->offset31-16$inline

(defun interrupt/trap-gate-descriptorbits->offset31-16$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->offset31-16

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

Theorem: interrupt/trap-gate-descriptorbits->offset31-16$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->offset31-16$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->offset31-16$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->offset31-16$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->offset31-16$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->offset31-16-of-interrupt/trap-gate-descriptorbits

(defthm
 interrupt/trap-gate-descriptorbits->offset31-16-of-interrupt/trap-gate-descriptorbits
 (equal (interrupt/trap-gate-descriptorbits->offset31-16
             (interrupt/trap-gate-descriptorbits
                  offset15-0 selector
                  ist res1 type s dpl p offset31-16
                  offset63-32 res2 all-zeros? res3))
        (16bits-fix offset31-16)))

Theorem: interrupt/trap-gate-descriptorbits->offset31-16-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->offset63-32$inline

(defun interrupt/trap-gate-descriptorbits->offset63-32$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->offset63-32

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

Theorem: interrupt/trap-gate-descriptorbits->offset63-32$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->offset63-32$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->offset63-32$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->offset63-32$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->offset63-32$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->offset63-32-of-interrupt/trap-gate-descriptorbits

(defthm
 interrupt/trap-gate-descriptorbits->offset63-32-of-interrupt/trap-gate-descriptorbits
 (equal (interrupt/trap-gate-descriptorbits->offset63-32
             (interrupt/trap-gate-descriptorbits
                  offset15-0 selector
                  ist res1 type s dpl p offset31-16
                  offset63-32 res2 all-zeros? res3))
        (32bits-fix offset63-32)))

Theorem: interrupt/trap-gate-descriptorbits->offset63-32-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->res2$inline

(defun interrupt/trap-gate-descriptorbits->res2$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->res2

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

Theorem: interrupt/trap-gate-descriptorbits->res2$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->res2$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->res2$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->res2$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->res2$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->res2-of-interrupt/trap-gate-descriptorbits

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

Theorem: interrupt/trap-gate-descriptorbits->res2-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->all-zeros?$inline

(defun interrupt/trap-gate-descriptorbits->all-zeros?$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->all-zeros?

(defthm 5bits-p-of-interrupt/trap-gate-descriptorbits->all-zeros?
  (b*
   ((all-zeros?
         (interrupt/trap-gate-descriptorbits->all-zeros?$inline x)))
   (5bits-p all-zeros?))
  :rule-classes :rewrite)

Theorem: interrupt/trap-gate-descriptorbits->all-zeros?$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->all-zeros?$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->all-zeros?$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->all-zeros?$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->all-zeros?$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

(defthm
 interrupt/trap-gate-descriptorbits->all-zeros?$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x
 (implies
  (interrupt/trap-gate-descriptorbits-equiv x x-equiv)
  (equal
   (interrupt/trap-gate-descriptorbits->all-zeros?$inline x)
   (interrupt/trap-gate-descriptorbits->all-zeros?$inline x-equiv)))
 :rule-classes :congruence)

Theorem: interrupt/trap-gate-descriptorbits->all-zeros?-of-interrupt/trap-gate-descriptorbits

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

Theorem: interrupt/trap-gate-descriptorbits->all-zeros?-of-write-with-mask

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

Function: interrupt/trap-gate-descriptorbits->res3$inline

(defun interrupt/trap-gate-descriptorbits->res3$inline (x)
  (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
  (mbe :logic
       (let ((x (interrupt/trap-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-interrupt/trap-gate-descriptorbits->res3

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

Theorem: interrupt/trap-gate-descriptorbits->res3$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 interrupt/trap-gate-descriptorbits->res3$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (interrupt/trap-gate-descriptorbits->res3$inline
             (interrupt/trap-gate-descriptorbits-fix x))
        (interrupt/trap-gate-descriptorbits->res3$inline x)))

Theorem: interrupt/trap-gate-descriptorbits->res3$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: interrupt/trap-gate-descriptorbits->res3-of-interrupt/trap-gate-descriptorbits

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

Theorem: interrupt/trap-gate-descriptorbits->res3-of-write-with-mask

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

Theorem: interrupt/trap-gate-descriptorbits-fix-in-terms-of-interrupt/trap-gate-descriptorbits

(defthm
 interrupt/trap-gate-descriptorbits-fix-in-terms-of-interrupt/trap-gate-descriptorbits
 (equal (interrupt/trap-gate-descriptorbits-fix x)
        (change-interrupt/trap-gate-descriptorbits x)))

Function: !interrupt/trap-gate-descriptorbits->offset15-0$inline

(defun !interrupt/trap-gate-descriptorbits->offset15-0$inline
       (offset15-0 x)
 (declare
      (xargs :guard (and (16bits-p offset15-0)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((offset15-0 (mbe :logic (16bits-fix offset15-0)
                           :exec offset15-0))
          (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->offset15-0

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

Theorem: !interrupt/trap-gate-descriptorbits->offset15-0$inline-of-16bits-fix-offset15-0

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

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

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

Theorem: !interrupt/trap-gate-descriptorbits->offset15-0$inline-of-interrupt/trap-gate-descriptorbits-fix-x

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

Theorem: !interrupt/trap-gate-descriptorbits->offset15-0$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->offset15-0-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->offset15-0-is-interrupt/trap-gate-descriptorbits
 (equal
      (!interrupt/trap-gate-descriptorbits->offset15-0 offset15-0 x)
      (change-interrupt/trap-gate-descriptorbits
           x
           :offset15-0 offset15-0)))

Theorem: interrupt/trap-gate-descriptorbits->offset15-0-of-!interrupt/trap-gate-descriptorbits->offset15-0

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

Theorem: !interrupt/trap-gate-descriptorbits->offset15-0-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->selector$inline

(defun !interrupt/trap-gate-descriptorbits->selector$inline
       (selector x)
 (declare
      (xargs :guard (and (16bits-p selector)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe :logic
      (b* ((selector (mbe :logic (16bits-fix selector)
                          :exec selector))
           (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->selector

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

Theorem: !interrupt/trap-gate-descriptorbits->selector$inline-of-16bits-fix-selector

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

Theorem: !interrupt/trap-gate-descriptorbits->selector$inline-16bits-equiv-congruence-on-selector

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

Theorem: !interrupt/trap-gate-descriptorbits->selector$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->selector$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->selector$inline
             selector
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->selector$inline
             selector x)))

Theorem: !interrupt/trap-gate-descriptorbits->selector$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->selector-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->selector-is-interrupt/trap-gate-descriptorbits
 (equal
    (!interrupt/trap-gate-descriptorbits->selector selector x)
    (change-interrupt/trap-gate-descriptorbits x
                                               :selector selector)))

Theorem: interrupt/trap-gate-descriptorbits->selector-of-!interrupt/trap-gate-descriptorbits->selector

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

Theorem: !interrupt/trap-gate-descriptorbits->selector-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->ist$inline

(defun !interrupt/trap-gate-descriptorbits->ist$inline (ist x)
 (declare
      (xargs :guard (and (3bits-p ist)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((ist (mbe :logic (3bits-fix ist) :exec ist))
          (x (interrupt/trap-gate-descriptorbits-fix x)))
       (part-install ist x :width 3 :low 32))
     :exec
     (the (unsigned-byte 128)
          (logior (the (unsigned-byte 128)
                       (logand (the (unsigned-byte 128) x)
                               (the (signed-byte 36) -30064771073)))
                  (the (unsigned-byte 35)
                       (ash (the (unsigned-byte 3) ist)
                            32))))))

Theorem: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->ist

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

Theorem: !interrupt/trap-gate-descriptorbits->ist$inline-of-3bits-fix-ist

(defthm
   !interrupt/trap-gate-descriptorbits->ist$inline-of-3bits-fix-ist
 (equal
    (!interrupt/trap-gate-descriptorbits->ist$inline (3bits-fix ist)
                                                     x)
    (!interrupt/trap-gate-descriptorbits->ist$inline ist x)))

Theorem: !interrupt/trap-gate-descriptorbits->ist$inline-3bits-equiv-congruence-on-ist

(defthm
 !interrupt/trap-gate-descriptorbits->ist$inline-3bits-equiv-congruence-on-ist
 (implies
  (3bits-equiv ist ist-equiv)
  (equal
     (!interrupt/trap-gate-descriptorbits->ist$inline ist x)
     (!interrupt/trap-gate-descriptorbits->ist$inline ist-equiv x)))
 :rule-classes :congruence)

Theorem: !interrupt/trap-gate-descriptorbits->ist$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->ist$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->ist$inline
             ist
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->ist$inline ist x)))

Theorem: !interrupt/trap-gate-descriptorbits->ist$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

(defthm
 !interrupt/trap-gate-descriptorbits->ist$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x
 (implies
  (interrupt/trap-gate-descriptorbits-equiv x x-equiv)
  (equal
     (!interrupt/trap-gate-descriptorbits->ist$inline ist x)
     (!interrupt/trap-gate-descriptorbits->ist$inline ist x-equiv)))
 :rule-classes :congruence)

Theorem: !interrupt/trap-gate-descriptorbits->ist-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->ist-is-interrupt/trap-gate-descriptorbits
 (equal (!interrupt/trap-gate-descriptorbits->ist ist x)
        (change-interrupt/trap-gate-descriptorbits x
                                                   :ist ist)))

Theorem: interrupt/trap-gate-descriptorbits->ist-of-!interrupt/trap-gate-descriptorbits->ist

(defthm
 interrupt/trap-gate-descriptorbits->ist-of-!interrupt/trap-gate-descriptorbits->ist
 (b*
  ((?new-x (!interrupt/trap-gate-descriptorbits->ist$inline ist x)))
  (equal (interrupt/trap-gate-descriptorbits->ist new-x)
         (3bits-fix ist))))

Theorem: !interrupt/trap-gate-descriptorbits->ist-equiv-under-mask

(defthm !interrupt/trap-gate-descriptorbits->ist-equiv-under-mask
 (b*
  ((?new-x (!interrupt/trap-gate-descriptorbits->ist$inline ist x)))
  (interrupt/trap-gate-descriptorbits-equiv-under-mask
       new-x x -30064771073)))

Function: !interrupt/trap-gate-descriptorbits->res1$inline

(defun !interrupt/trap-gate-descriptorbits->res1$inline (res1 x)
 (declare
      (xargs :guard (and (5bits-p res1)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((res1 (mbe :logic (5bits-fix res1)
                   :exec res1))
        (x (interrupt/trap-gate-descriptorbits-fix x)))
     (part-install res1 x :width 5 :low 35))
   :exec
   (the (unsigned-byte 128)
        (logior (the (unsigned-byte 128)
                     (logand (the (unsigned-byte 128) x)
                             (the (signed-byte 41) -1065151889409)))
                (the (unsigned-byte 40)
                     (ash (the (unsigned-byte 5) res1)
                          35))))))

Theorem: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->res1

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

Theorem: !interrupt/trap-gate-descriptorbits->res1$inline-of-5bits-fix-res1

(defthm
 !interrupt/trap-gate-descriptorbits->res1$inline-of-5bits-fix-res1
 (equal
  (!interrupt/trap-gate-descriptorbits->res1$inline (5bits-fix res1)
                                                    x)
  (!interrupt/trap-gate-descriptorbits->res1$inline res1 x)))

Theorem: !interrupt/trap-gate-descriptorbits->res1$inline-5bits-equiv-congruence-on-res1

(defthm
 !interrupt/trap-gate-descriptorbits->res1$inline-5bits-equiv-congruence-on-res1
 (implies
  (5bits-equiv res1 res1-equiv)
  (equal
   (!interrupt/trap-gate-descriptorbits->res1$inline res1 x)
   (!interrupt/trap-gate-descriptorbits->res1$inline res1-equiv x)))
 :rule-classes :congruence)

Theorem: !interrupt/trap-gate-descriptorbits->res1$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->res1$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->res1$inline
             res1
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->res1$inline res1 x)))

Theorem: !interrupt/trap-gate-descriptorbits->res1$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->res1-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->res1-is-interrupt/trap-gate-descriptorbits
 (equal (!interrupt/trap-gate-descriptorbits->res1 res1 x)
        (change-interrupt/trap-gate-descriptorbits x
                                                   :res1 res1)))

Theorem: interrupt/trap-gate-descriptorbits->res1-of-!interrupt/trap-gate-descriptorbits->res1

(defthm
 interrupt/trap-gate-descriptorbits->res1-of-!interrupt/trap-gate-descriptorbits->res1
 (b*
  ((?new-x
        (!interrupt/trap-gate-descriptorbits->res1$inline res1 x)))
  (equal (interrupt/trap-gate-descriptorbits->res1 new-x)
         (5bits-fix res1))))

Theorem: !interrupt/trap-gate-descriptorbits->res1-equiv-under-mask

(defthm !interrupt/trap-gate-descriptorbits->res1-equiv-under-mask
  (b*
   ((?new-x
         (!interrupt/trap-gate-descriptorbits->res1$inline res1 x)))
   (interrupt/trap-gate-descriptorbits-equiv-under-mask
        new-x x -1065151889409)))

Function: !interrupt/trap-gate-descriptorbits->type$inline

(defun !interrupt/trap-gate-descriptorbits->type$inline (type x)
 (declare
      (xargs :guard (and (4bits-p type)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((type (mbe :logic (4bits-fix type)
                  :exec type))
       (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->type

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

Theorem: !interrupt/trap-gate-descriptorbits->type$inline-of-4bits-fix-type

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

Theorem: !interrupt/trap-gate-descriptorbits->type$inline-4bits-equiv-congruence-on-type

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

Theorem: !interrupt/trap-gate-descriptorbits->type$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->type$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->type$inline
             type
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->type$inline type x)))

Theorem: !interrupt/trap-gate-descriptorbits->type$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->type-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->type-is-interrupt/trap-gate-descriptorbits
 (equal (!interrupt/trap-gate-descriptorbits->type type x)
        (change-interrupt/trap-gate-descriptorbits x
                                                   :type type)))

Theorem: interrupt/trap-gate-descriptorbits->type-of-!interrupt/trap-gate-descriptorbits->type

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

Theorem: !interrupt/trap-gate-descriptorbits->type-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->s$inline

(defun !interrupt/trap-gate-descriptorbits->s$inline (s x)
 (declare
      (xargs :guard (and (bitp s)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((s (mbe :logic (bfix s) :exec s))
       (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->s

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

Theorem: !interrupt/trap-gate-descriptorbits->s$inline-of-bfix-s

(defthm !interrupt/trap-gate-descriptorbits->s$inline-of-bfix-s
  (equal (!interrupt/trap-gate-descriptorbits->s$inline (bfix s)
                                                        x)
         (!interrupt/trap-gate-descriptorbits->s$inline s x)))

Theorem: !interrupt/trap-gate-descriptorbits->s$inline-bit-equiv-congruence-on-s

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

Theorem: !interrupt/trap-gate-descriptorbits->s$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->s$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->s$inline
             s
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->s$inline s x)))

Theorem: !interrupt/trap-gate-descriptorbits->s$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->s-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->s-is-interrupt/trap-gate-descriptorbits
 (equal (!interrupt/trap-gate-descriptorbits->s s x)
        (change-interrupt/trap-gate-descriptorbits x
                                                   :s s)))

Theorem: interrupt/trap-gate-descriptorbits->s-of-!interrupt/trap-gate-descriptorbits->s

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

Theorem: !interrupt/trap-gate-descriptorbits->s-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->dpl$inline

(defun !interrupt/trap-gate-descriptorbits->dpl$inline (dpl x)
 (declare
      (xargs :guard (and (2bits-p dpl)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe :logic
      (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl))
           (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->dpl

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

Theorem: !interrupt/trap-gate-descriptorbits->dpl$inline-of-2bits-fix-dpl

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

Theorem: !interrupt/trap-gate-descriptorbits->dpl$inline-2bits-equiv-congruence-on-dpl

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

Theorem: !interrupt/trap-gate-descriptorbits->dpl$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->dpl$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->dpl$inline
             dpl
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->dpl$inline dpl x)))

Theorem: !interrupt/trap-gate-descriptorbits->dpl$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->dpl-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->dpl-is-interrupt/trap-gate-descriptorbits
 (equal (!interrupt/trap-gate-descriptorbits->dpl dpl x)
        (change-interrupt/trap-gate-descriptorbits x
                                                   :dpl dpl)))

Theorem: interrupt/trap-gate-descriptorbits->dpl-of-!interrupt/trap-gate-descriptorbits->dpl

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

Theorem: !interrupt/trap-gate-descriptorbits->dpl-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->p$inline

(defun !interrupt/trap-gate-descriptorbits->p$inline (p x)
 (declare
      (xargs :guard (and (bitp p)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((p (mbe :logic (bfix p) :exec p))
          (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->p

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

Theorem: !interrupt/trap-gate-descriptorbits->p$inline-of-bfix-p

(defthm !interrupt/trap-gate-descriptorbits->p$inline-of-bfix-p
  (equal (!interrupt/trap-gate-descriptorbits->p$inline (bfix p)
                                                        x)
         (!interrupt/trap-gate-descriptorbits->p$inline p x)))

Theorem: !interrupt/trap-gate-descriptorbits->p$inline-bit-equiv-congruence-on-p

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

Theorem: !interrupt/trap-gate-descriptorbits->p$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->p$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->p$inline
             p
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->p$inline p x)))

Theorem: !interrupt/trap-gate-descriptorbits->p$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->p-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->p-is-interrupt/trap-gate-descriptorbits
 (equal (!interrupt/trap-gate-descriptorbits->p p x)
        (change-interrupt/trap-gate-descriptorbits x
                                                   :p p)))

Theorem: interrupt/trap-gate-descriptorbits->p-of-!interrupt/trap-gate-descriptorbits->p

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

Theorem: !interrupt/trap-gate-descriptorbits->p-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->offset31-16$inline

(defun !interrupt/trap-gate-descriptorbits->offset31-16$inline
       (offset31-16 x)
 (declare
      (xargs :guard (and (16bits-p offset31-16)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((offset31-16 (mbe :logic (16bits-fix offset31-16)
                          :exec offset31-16))
        (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->offset31-16

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

Theorem: !interrupt/trap-gate-descriptorbits->offset31-16$inline-of-16bits-fix-offset31-16

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

Theorem: !interrupt/trap-gate-descriptorbits->offset31-16$inline-16bits-equiv-congruence-on-offset31-16

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

Theorem: !interrupt/trap-gate-descriptorbits->offset31-16$inline-of-interrupt/trap-gate-descriptorbits-fix-x

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

Theorem: !interrupt/trap-gate-descriptorbits->offset31-16$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->offset31-16-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->offset31-16-is-interrupt/trap-gate-descriptorbits
 (equal
    (!interrupt/trap-gate-descriptorbits->offset31-16 offset31-16 x)
    (change-interrupt/trap-gate-descriptorbits
         x
         :offset31-16 offset31-16)))

Theorem: interrupt/trap-gate-descriptorbits->offset31-16-of-!interrupt/trap-gate-descriptorbits->offset31-16

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

Theorem: !interrupt/trap-gate-descriptorbits->offset31-16-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->offset63-32$inline

(defun !interrupt/trap-gate-descriptorbits->offset63-32$inline
       (offset63-32 x)
 (declare
      (xargs :guard (and (32bits-p offset63-32)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
    :logic
    (b* ((offset63-32 (mbe :logic (32bits-fix offset63-32)
                           :exec offset63-32))
         (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->offset63-32

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

Theorem: !interrupt/trap-gate-descriptorbits->offset63-32$inline-of-32bits-fix-offset63-32

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

Theorem: !interrupt/trap-gate-descriptorbits->offset63-32$inline-32bits-equiv-congruence-on-offset63-32

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

Theorem: !interrupt/trap-gate-descriptorbits->offset63-32$inline-of-interrupt/trap-gate-descriptorbits-fix-x

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

Theorem: !interrupt/trap-gate-descriptorbits->offset63-32$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->offset63-32-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->offset63-32-is-interrupt/trap-gate-descriptorbits
 (equal
    (!interrupt/trap-gate-descriptorbits->offset63-32 offset63-32 x)
    (change-interrupt/trap-gate-descriptorbits
         x
         :offset63-32 offset63-32)))

Theorem: interrupt/trap-gate-descriptorbits->offset63-32-of-!interrupt/trap-gate-descriptorbits->offset63-32

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

Theorem: !interrupt/trap-gate-descriptorbits->offset63-32-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->res2$inline

(defun !interrupt/trap-gate-descriptorbits->res2$inline (res2 x)
 (declare
      (xargs :guard (and (8bits-p res2)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((res2 (mbe :logic (8bits-fix res2)
                  :exec res2))
       (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->res2

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

Theorem: !interrupt/trap-gate-descriptorbits->res2$inline-of-8bits-fix-res2

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

Theorem: !interrupt/trap-gate-descriptorbits->res2$inline-8bits-equiv-congruence-on-res2

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

Theorem: !interrupt/trap-gate-descriptorbits->res2$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->res2$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->res2$inline
             res2
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->res2$inline res2 x)))

Theorem: !interrupt/trap-gate-descriptorbits->res2$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->res2-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->res2-is-interrupt/trap-gate-descriptorbits
 (equal (!interrupt/trap-gate-descriptorbits->res2 res2 x)
        (change-interrupt/trap-gate-descriptorbits x
                                                   :res2 res2)))

Theorem: interrupt/trap-gate-descriptorbits->res2-of-!interrupt/trap-gate-descriptorbits->res2

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

Theorem: !interrupt/trap-gate-descriptorbits->res2-equiv-under-mask

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

Function: !interrupt/trap-gate-descriptorbits->all-zeros?$inline

(defun !interrupt/trap-gate-descriptorbits->all-zeros?$inline
       (all-zeros? x)
 (declare
      (xargs :guard (and (5bits-p all-zeros?)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((all-zeros? (mbe :logic (5bits-fix all-zeros?)
                        :exec all-zeros?))
       (x (interrupt/trap-gate-descriptorbits-fix x)))
    (part-install all-zeros? 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-zeros?)
                       104))))))

Theorem: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->all-zeros?

(defthm
 interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->all-zeros?
 (b* ((new-x (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
                  all-zeros? x)))
   (interrupt/trap-gate-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !interrupt/trap-gate-descriptorbits->all-zeros?$inline-of-5bits-fix-all-zeros?

(defthm
 !interrupt/trap-gate-descriptorbits->all-zeros?$inline-of-5bits-fix-all-zeros?
 (equal (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
             (5bits-fix all-zeros?)
             x)
        (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
             all-zeros? x)))

Theorem: !interrupt/trap-gate-descriptorbits->all-zeros?$inline-5bits-equiv-congruence-on-all-zeros?

(defthm
 !interrupt/trap-gate-descriptorbits->all-zeros?$inline-5bits-equiv-congruence-on-all-zeros?
 (implies (5bits-equiv all-zeros? all-zeros?-equiv)
          (equal (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
                      all-zeros? x)
                 (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
                      all-zeros?-equiv x)))
 :rule-classes :congruence)

Theorem: !interrupt/trap-gate-descriptorbits->all-zeros?$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->all-zeros?$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
             all-zeros?
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
             all-zeros? x)))

Theorem: !interrupt/trap-gate-descriptorbits->all-zeros?$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

(defthm
 !interrupt/trap-gate-descriptorbits->all-zeros?$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x
 (implies (interrupt/trap-gate-descriptorbits-equiv x x-equiv)
          (equal (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
                      all-zeros? x)
                 (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
                      all-zeros? x-equiv)))
 :rule-classes :congruence)

Theorem: !interrupt/trap-gate-descriptorbits->all-zeros?-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->all-zeros?-is-interrupt/trap-gate-descriptorbits
 (equal
      (!interrupt/trap-gate-descriptorbits->all-zeros? all-zeros? x)
      (change-interrupt/trap-gate-descriptorbits
           x
           :all-zeros? all-zeros?)))

Theorem: interrupt/trap-gate-descriptorbits->all-zeros?-of-!interrupt/trap-gate-descriptorbits->all-zeros?

(defthm
 interrupt/trap-gate-descriptorbits->all-zeros?-of-!interrupt/trap-gate-descriptorbits->all-zeros?
 (b* ((?new-x (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
                   all-zeros? x)))
   (equal (interrupt/trap-gate-descriptorbits->all-zeros? new-x)
          (5bits-fix all-zeros?))))

Theorem: !interrupt/trap-gate-descriptorbits->all-zeros?-equiv-under-mask

(defthm
   !interrupt/trap-gate-descriptorbits->all-zeros?-equiv-under-mask
  (b* ((?new-x (!interrupt/trap-gate-descriptorbits->all-zeros?$inline
                    all-zeros? x)))
    (interrupt/trap-gate-descriptorbits-equiv-under-mask
         new-x
         x -628754697713201783142364789866497)))

Function: !interrupt/trap-gate-descriptorbits->res3$inline

(defun !interrupt/trap-gate-descriptorbits->res3$inline (res3 x)
 (declare
      (xargs :guard (and (19bits-p res3)
                         (interrupt/trap-gate-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((res3 (mbe :logic (19bits-fix res3)
                  :exec res3))
       (x (interrupt/trap-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: interrupt/trap-gate-descriptorbits-p-of-!interrupt/trap-gate-descriptorbits->res3

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

Theorem: !interrupt/trap-gate-descriptorbits->res3$inline-of-19bits-fix-res3

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

Theorem: !interrupt/trap-gate-descriptorbits->res3$inline-19bits-equiv-congruence-on-res3

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

Theorem: !interrupt/trap-gate-descriptorbits->res3$inline-of-interrupt/trap-gate-descriptorbits-fix-x

(defthm
 !interrupt/trap-gate-descriptorbits->res3$inline-of-interrupt/trap-gate-descriptorbits-fix-x
 (equal (!interrupt/trap-gate-descriptorbits->res3$inline
             res3
             (interrupt/trap-gate-descriptorbits-fix x))
        (!interrupt/trap-gate-descriptorbits->res3$inline res3 x)))

Theorem: !interrupt/trap-gate-descriptorbits->res3$inline-interrupt/trap-gate-descriptorbits-equiv-congruence-on-x

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

Theorem: !interrupt/trap-gate-descriptorbits->res3-is-interrupt/trap-gate-descriptorbits

(defthm
 !interrupt/trap-gate-descriptorbits->res3-is-interrupt/trap-gate-descriptorbits
 (equal (!interrupt/trap-gate-descriptorbits->res3 res3 x)
        (change-interrupt/trap-gate-descriptorbits x
                                                   :res3 res3)))

Theorem: interrupt/trap-gate-descriptorbits->res3-of-!interrupt/trap-gate-descriptorbits->res3

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

Theorem: !interrupt/trap-gate-descriptorbits->res3-equiv-under-mask

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

Function: interrupt/trap-gate-descriptorbits-debug

(defun interrupt/trap-gate-descriptorbits-debug (x)
 (declare (xargs :guard (interrupt/trap-gate-descriptorbits-p x)))
 (let ((__function__ 'interrupt/trap-gate-descriptorbits-debug))
  (declare (ignorable __function__))
  (b* (((interrupt/trap-gate-descriptorbits x)))
   (cons
    (cons 'offset15-0 x.offset15-0)
    (cons
     (cons 'selector x.selector)
     (cons
      (cons 'ist x.ist)
      (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-zeros? x.all-zeros?)
                                     (cons (cons 'res3 x.res3)
                                           nil))))))))))))))))

Subtopics

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