		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Call-gate-descriptor-attributesbits

Subset of call-gate-descriptorBits.

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

Fields

type — 4bits
s — bit
dpl — 2bits
p — bit
unknownbits — 8bits

Definitions and Theorems

Function: call-gate-descriptor-attributesbits-p

(defun call-gate-descriptor-attributesbits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'call-gate-descriptor-attributesbits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 16 x)
         :exec (and (natp x) (< x 65536)))))

Theorem: call-gate-descriptor-attributesbits-p-when-unsigned-byte-p

(defthm call-gate-descriptor-attributesbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 16 x)
           (call-gate-descriptor-attributesbits-p x)))

Theorem: unsigned-byte-p-when-call-gate-descriptor-attributesbits-p

(defthm unsigned-byte-p-when-call-gate-descriptor-attributesbits-p
  (implies (call-gate-descriptor-attributesbits-p x)
           (unsigned-byte-p 16 x)))

Theorem: call-gate-descriptor-attributesbits-p-compound-recognizer

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

Function: call-gate-descriptor-attributesbits-fix

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

Theorem: call-gate-descriptor-attributesbits-p-of-call-gate-descriptor-attributesbits-fix

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

Theorem: call-gate-descriptor-attributesbits-fix-when-call-gate-descriptor-attributesbits-p

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

Function: call-gate-descriptor-attributesbits-equiv$inline

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

Theorem: call-gate-descriptor-attributesbits-equiv-is-an-equivalence

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

Theorem: call-gate-descriptor-attributesbits-equiv-implies-equal-call-gate-descriptor-attributesbits-fix-1

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

Theorem: call-gate-descriptor-attributesbits-fix-under-call-gate-descriptor-attributesbits-equiv

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

Function: call-gate-descriptor-attributesbits

(defun call-gate-descriptor-attributesbits
       (type s dpl p unknownbits)
  (declare (xargs :guard (and (4bits-p type)
                              (bitp s)
                              (2bits-p dpl)
                              (bitp p)
                              (8bits-p unknownbits))))
  (let ((__function__ 'call-gate-descriptor-attributesbits))
    (declare (ignorable __function__))
    (b* ((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))
         (unknownbits (mbe :logic (8bits-fix unknownbits)
                           :exec unknownbits)))
      (logapp 4 type
              (logapp 1 s
                      (logapp 2 dpl (logapp 1 p unknownbits)))))))

Theorem: call-gate-descriptor-attributesbits-p-of-call-gate-descriptor-attributesbits

(defthm
 call-gate-descriptor-attributesbits-p-of-call-gate-descriptor-attributesbits
 (b*
  ((call-gate-descriptor-attributesbits
    (call-gate-descriptor-attributesbits type s dpl p unknownbits)))
  (call-gate-descriptor-attributesbits-p
       call-gate-descriptor-attributesbits))
 :rule-classes :rewrite)

Theorem: call-gate-descriptor-attributesbits-of-4bits-fix-type

(defthm call-gate-descriptor-attributesbits-of-4bits-fix-type
 (equal
    (call-gate-descriptor-attributesbits (4bits-fix type)
                                         s dpl p unknownbits)
    (call-gate-descriptor-attributesbits type s dpl p unknownbits)))

Theorem: call-gate-descriptor-attributesbits-4bits-equiv-congruence-on-type

(defthm
 call-gate-descriptor-attributesbits-4bits-equiv-congruence-on-type
 (implies
  (4bits-equiv type type-equiv)
  (equal
      (call-gate-descriptor-attributesbits type s dpl p unknownbits)
      (call-gate-descriptor-attributesbits
           type-equiv s dpl p unknownbits)))
 :rule-classes :congruence)

Theorem: call-gate-descriptor-attributesbits-of-bfix-s

(defthm call-gate-descriptor-attributesbits-of-bfix-s
 (equal
    (call-gate-descriptor-attributesbits type (bfix s)
                                         dpl p unknownbits)
    (call-gate-descriptor-attributesbits type s dpl p unknownbits)))

Theorem: call-gate-descriptor-attributesbits-bit-equiv-congruence-on-s

(defthm
      call-gate-descriptor-attributesbits-bit-equiv-congruence-on-s
 (implies
  (bit-equiv s s-equiv)
  (equal
      (call-gate-descriptor-attributesbits type s dpl p unknownbits)
      (call-gate-descriptor-attributesbits
           type s-equiv dpl p unknownbits)))
 :rule-classes :congruence)

Theorem: call-gate-descriptor-attributesbits-of-2bits-fix-dpl

(defthm call-gate-descriptor-attributesbits-of-2bits-fix-dpl
 (equal
    (call-gate-descriptor-attributesbits type s (2bits-fix dpl)
                                         p unknownbits)
    (call-gate-descriptor-attributesbits type s dpl p unknownbits)))

Theorem: call-gate-descriptor-attributesbits-2bits-equiv-congruence-on-dpl

(defthm
  call-gate-descriptor-attributesbits-2bits-equiv-congruence-on-dpl
 (implies
  (2bits-equiv dpl dpl-equiv)
  (equal
      (call-gate-descriptor-attributesbits type s dpl p unknownbits)
      (call-gate-descriptor-attributesbits
           type s dpl-equiv p unknownbits)))
 :rule-classes :congruence)

Theorem: call-gate-descriptor-attributesbits-of-bfix-p

(defthm call-gate-descriptor-attributesbits-of-bfix-p
 (equal
    (call-gate-descriptor-attributesbits type s dpl (bfix p)
                                         unknownbits)
    (call-gate-descriptor-attributesbits type s dpl p unknownbits)))

Theorem: call-gate-descriptor-attributesbits-bit-equiv-congruence-on-p

(defthm
      call-gate-descriptor-attributesbits-bit-equiv-congruence-on-p
 (implies
  (bit-equiv p p-equiv)
  (equal
      (call-gate-descriptor-attributesbits type s dpl p unknownbits)
      (call-gate-descriptor-attributesbits
           type s dpl p-equiv unknownbits)))
 :rule-classes :congruence)

Theorem: call-gate-descriptor-attributesbits-of-8bits-fix-unknownbits

(defthm call-gate-descriptor-attributesbits-of-8bits-fix-unknownbits
 (equal
    (call-gate-descriptor-attributesbits
         type s dpl p (8bits-fix unknownbits))
    (call-gate-descriptor-attributesbits type s dpl p unknownbits)))

Theorem: call-gate-descriptor-attributesbits-8bits-equiv-congruence-on-unknownbits

(defthm
 call-gate-descriptor-attributesbits-8bits-equiv-congruence-on-unknownbits
 (implies
  (8bits-equiv unknownbits unknownbits-equiv)
  (equal
      (call-gate-descriptor-attributesbits type s dpl p unknownbits)
      (call-gate-descriptor-attributesbits
           type s dpl p unknownbits-equiv)))
 :rule-classes :congruence)

Function: call-gate-descriptor-attributesbits-equiv-under-mask

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

Function: call-gate-descriptor-attributesbits->type$inline

(defun call-gate-descriptor-attributesbits->type$inline (x)
  (declare (xargs :guard (call-gate-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (call-gate-descriptor-attributesbits-fix x)))
         (part-select x :low 0 :width 4))
       :exec (the (unsigned-byte 4)
                  (logand (the (unsigned-byte 4) 15)
                          (the (unsigned-byte 16) x)))))

Theorem: 4bits-p-of-call-gate-descriptor-attributesbits->type

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

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

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

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

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

Theorem: call-gate-descriptor-attributesbits->type-of-call-gate-descriptor-attributesbits

(defthm
 call-gate-descriptor-attributesbits->type-of-call-gate-descriptor-attributesbits
 (equal
  (call-gate-descriptor-attributesbits->type
     (call-gate-descriptor-attributesbits type s dpl p unknownbits))
  (4bits-fix type)))

Theorem: call-gate-descriptor-attributesbits->type-of-write-with-mask

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

Function: call-gate-descriptor-attributesbits->s$inline

(defun call-gate-descriptor-attributesbits->s$inline (x)
 (declare (xargs :guard (call-gate-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (call-gate-descriptor-attributesbits-fix x)))
      (part-select x :low 4 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 12)
                            (ash (the (unsigned-byte 16) x) -4))))))

Theorem: bitp-of-call-gate-descriptor-attributesbits->s

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

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

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

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

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

Theorem: call-gate-descriptor-attributesbits->s-of-call-gate-descriptor-attributesbits

(defthm
 call-gate-descriptor-attributesbits->s-of-call-gate-descriptor-attributesbits
 (equal
  (call-gate-descriptor-attributesbits->s
     (call-gate-descriptor-attributesbits type s dpl p unknownbits))
  (bfix s)))

Theorem: call-gate-descriptor-attributesbits->s-of-write-with-mask

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

Function: call-gate-descriptor-attributesbits->dpl$inline

(defun call-gate-descriptor-attributesbits->dpl$inline (x)
 (declare (xargs :guard (call-gate-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (call-gate-descriptor-attributesbits-fix x)))
      (part-select x :low 5 :width 2))
    :exec (the (unsigned-byte 2)
               (logand (the (unsigned-byte 2) 3)
                       (the (unsigned-byte 11)
                            (ash (the (unsigned-byte 16) x) -5))))))

Theorem: 2bits-p-of-call-gate-descriptor-attributesbits->dpl

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

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

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

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

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

Theorem: call-gate-descriptor-attributesbits->dpl-of-call-gate-descriptor-attributesbits

(defthm
 call-gate-descriptor-attributesbits->dpl-of-call-gate-descriptor-attributesbits
 (equal
  (call-gate-descriptor-attributesbits->dpl
     (call-gate-descriptor-attributesbits type s dpl p unknownbits))
  (2bits-fix dpl)))

Theorem: call-gate-descriptor-attributesbits->dpl-of-write-with-mask

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

Function: call-gate-descriptor-attributesbits->p$inline

(defun call-gate-descriptor-attributesbits->p$inline (x)
 (declare (xargs :guard (call-gate-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (call-gate-descriptor-attributesbits-fix x)))
      (part-select x :low 7 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 9)
                            (ash (the (unsigned-byte 16) x) -7))))))

Theorem: bitp-of-call-gate-descriptor-attributesbits->p

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

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

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

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

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

Theorem: call-gate-descriptor-attributesbits->p-of-call-gate-descriptor-attributesbits

(defthm
 call-gate-descriptor-attributesbits->p-of-call-gate-descriptor-attributesbits
 (equal
  (call-gate-descriptor-attributesbits->p
     (call-gate-descriptor-attributesbits type s dpl p unknownbits))
  (bfix p)))

Theorem: call-gate-descriptor-attributesbits->p-of-write-with-mask

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

Function: call-gate-descriptor-attributesbits->unknownbits$inline

(defun call-gate-descriptor-attributesbits->unknownbits$inline (x)
 (declare (xargs :guard (call-gate-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (call-gate-descriptor-attributesbits-fix x)))
      (part-select x :low 8 :width 8))
    :exec (the (unsigned-byte 8)
               (logand (the (unsigned-byte 8) 255)
                       (the (unsigned-byte 8)
                            (ash (the (unsigned-byte 16) x) -8))))))

Theorem: 8bits-p-of-call-gate-descriptor-attributesbits->unknownbits

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

Theorem: call-gate-descriptor-attributesbits->unknownbits$inline-of-call-gate-descriptor-attributesbits-fix-x

(defthm
 call-gate-descriptor-attributesbits->unknownbits$inline-of-call-gate-descriptor-attributesbits-fix-x
 (equal
      (call-gate-descriptor-attributesbits->unknownbits$inline
           (call-gate-descriptor-attributesbits-fix x))
      (call-gate-descriptor-attributesbits->unknownbits$inline x)))

Theorem: call-gate-descriptor-attributesbits->unknownbits$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 call-gate-descriptor-attributesbits->unknownbits$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (call-gate-descriptor-attributesbits-equiv x x-equiv)
  (equal (call-gate-descriptor-attributesbits->unknownbits$inline x)
         (call-gate-descriptor-attributesbits->unknownbits$inline
              x-equiv)))
 :rule-classes :congruence)

Theorem: call-gate-descriptor-attributesbits->unknownbits-of-call-gate-descriptor-attributesbits

(defthm
 call-gate-descriptor-attributesbits->unknownbits-of-call-gate-descriptor-attributesbits
 (equal
  (call-gate-descriptor-attributesbits->unknownbits
     (call-gate-descriptor-attributesbits type s dpl p unknownbits))
  (8bits-fix unknownbits)))

Theorem: call-gate-descriptor-attributesbits->unknownbits-of-write-with-mask

(defthm
 call-gate-descriptor-attributesbits->unknownbits-of-write-with-mask
 (implies
     (and (fty::bitstruct-read-over-write-hyps
               x
               call-gate-descriptor-attributesbits-equiv-under-mask)
          (call-gate-descriptor-attributesbits-equiv-under-mask
               x y fty::mask)
          (equal (logand (lognot fty::mask) 65280)
                 0))
     (equal (call-gate-descriptor-attributesbits->unknownbits x)
            (call-gate-descriptor-attributesbits->unknownbits y))))

Theorem: call-gate-descriptor-attributesbits-fix-in-terms-of-call-gate-descriptor-attributesbits

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

Function: !call-gate-descriptor-attributesbits->type$inline

(defun !call-gate-descriptor-attributesbits->type$inline (type x)
 (declare
     (xargs :guard (and (4bits-p type)
                        (call-gate-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((type (mbe :logic (4bits-fix type)
                      :exec type))
           (x (call-gate-descriptor-attributesbits-fix x)))
        (part-install type x :width 4 :low 0))
      :exec (the (unsigned-byte 16)
                 (logior (the (unsigned-byte 16)
                              (logand (the (unsigned-byte 16) x)
                                      (the (signed-byte 5) -16)))
                         (the (unsigned-byte 4) type)))))

Theorem: call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->type

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

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

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

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

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

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

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

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

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

Theorem: !call-gate-descriptor-attributesbits->type-is-call-gate-descriptor-attributesbits

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

Theorem: call-gate-descriptor-attributesbits->type-of-!call-gate-descriptor-attributesbits->type

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

Theorem: !call-gate-descriptor-attributesbits->type-equiv-under-mask

(defthm !call-gate-descriptor-attributesbits->type-equiv-under-mask
 (b*
  ((?new-x
        (!call-gate-descriptor-attributesbits->type$inline type x)))
  (call-gate-descriptor-attributesbits-equiv-under-mask
       new-x x -16)))

Function: !call-gate-descriptor-attributesbits->s$inline

(defun !call-gate-descriptor-attributesbits->s$inline (s x)
 (declare
     (xargs :guard (and (bitp s)
                        (call-gate-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((s (mbe :logic (bfix s) :exec s))
           (x (call-gate-descriptor-attributesbits-fix x)))
        (part-install s x :width 1 :low 4))
      :exec (the (unsigned-byte 16)
                 (logior (the (unsigned-byte 16)
                              (logand (the (unsigned-byte 16) x)
                                      (the (signed-byte 6) -17)))
                         (the (unsigned-byte 5)
                              (ash (the (unsigned-byte 1) s) 4))))))

Theorem: call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->s

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

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

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

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

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

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

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

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

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

Theorem: !call-gate-descriptor-attributesbits->s-is-call-gate-descriptor-attributesbits

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

Theorem: call-gate-descriptor-attributesbits->s-of-!call-gate-descriptor-attributesbits->s

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

Theorem: !call-gate-descriptor-attributesbits->s-equiv-under-mask

(defthm !call-gate-descriptor-attributesbits->s-equiv-under-mask
 (b* ((?new-x (!call-gate-descriptor-attributesbits->s$inline s x)))
   (call-gate-descriptor-attributesbits-equiv-under-mask
        new-x x -17)))

Function: !call-gate-descriptor-attributesbits->dpl$inline

(defun !call-gate-descriptor-attributesbits->dpl$inline (dpl x)
 (declare
     (xargs :guard (and (2bits-p dpl)
                        (call-gate-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl))
         (x (call-gate-descriptor-attributesbits-fix x)))
      (part-install dpl x :width 2 :low 5))
    :exec (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16)
                            (logand (the (unsigned-byte 16) x)
                                    (the (signed-byte 8) -97)))
                       (the (unsigned-byte 7)
                            (ash (the (unsigned-byte 2) dpl) 5))))))

Theorem: call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->dpl

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

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

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

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

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

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

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

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

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

Theorem: !call-gate-descriptor-attributesbits->dpl-is-call-gate-descriptor-attributesbits

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

Theorem: call-gate-descriptor-attributesbits->dpl-of-!call-gate-descriptor-attributesbits->dpl

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

Theorem: !call-gate-descriptor-attributesbits->dpl-equiv-under-mask

(defthm !call-gate-descriptor-attributesbits->dpl-equiv-under-mask
  (b*
    ((?new-x
          (!call-gate-descriptor-attributesbits->dpl$inline dpl x)))
    (call-gate-descriptor-attributesbits-equiv-under-mask
         new-x x -97)))

Function: !call-gate-descriptor-attributesbits->p$inline

(defun !call-gate-descriptor-attributesbits->p$inline (p x)
 (declare
     (xargs :guard (and (bitp p)
                        (call-gate-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((p (mbe :logic (bfix p) :exec p))
           (x (call-gate-descriptor-attributesbits-fix x)))
        (part-install p x :width 1 :low 7))
      :exec (the (unsigned-byte 16)
                 (logior (the (unsigned-byte 16)
                              (logand (the (unsigned-byte 16) x)
                                      (the (signed-byte 9) -129)))
                         (the (unsigned-byte 8)
                              (ash (the (unsigned-byte 1) p) 7))))))

Theorem: call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->p

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

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

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

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

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

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

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

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

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

Theorem: !call-gate-descriptor-attributesbits->p-is-call-gate-descriptor-attributesbits

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

Theorem: call-gate-descriptor-attributesbits->p-of-!call-gate-descriptor-attributesbits->p

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

Theorem: !call-gate-descriptor-attributesbits->p-equiv-under-mask

(defthm !call-gate-descriptor-attributesbits->p-equiv-under-mask
 (b* ((?new-x (!call-gate-descriptor-attributesbits->p$inline p x)))
   (call-gate-descriptor-attributesbits-equiv-under-mask
        new-x x -129)))

Function: !call-gate-descriptor-attributesbits->unknownbits$inline

(defun !call-gate-descriptor-attributesbits->unknownbits$inline
       (unknownbits x)
 (declare
     (xargs :guard (and (8bits-p unknownbits)
                        (call-gate-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((unknownbits (mbe :logic (8bits-fix unknownbits)
                           :exec unknownbits))
         (x (call-gate-descriptor-attributesbits-fix x)))
      (part-install unknownbits x
                    :width 8
                    :low 8))
    :exec (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16)
                            (logand (the (unsigned-byte 16) x)
                                    (the (signed-byte 17) -65281)))
                       (the (unsigned-byte 16)
                            (ash (the (unsigned-byte 8) unknownbits)
                                 8))))))

Theorem: call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->unknownbits

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

Theorem: !call-gate-descriptor-attributesbits->unknownbits$inline-of-8bits-fix-unknownbits

(defthm
 !call-gate-descriptor-attributesbits->unknownbits$inline-of-8bits-fix-unknownbits
 (equal (!call-gate-descriptor-attributesbits->unknownbits$inline
             (8bits-fix unknownbits)
             x)
        (!call-gate-descriptor-attributesbits->unknownbits$inline
             unknownbits x)))

Theorem: !call-gate-descriptor-attributesbits->unknownbits$inline-8bits-equiv-congruence-on-unknownbits

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

Theorem: !call-gate-descriptor-attributesbits->unknownbits$inline-of-call-gate-descriptor-attributesbits-fix-x

(defthm
 !call-gate-descriptor-attributesbits->unknownbits$inline-of-call-gate-descriptor-attributesbits-fix-x
 (equal (!call-gate-descriptor-attributesbits->unknownbits$inline
             unknownbits
             (call-gate-descriptor-attributesbits-fix x))
        (!call-gate-descriptor-attributesbits->unknownbits$inline
             unknownbits x)))

Theorem: !call-gate-descriptor-attributesbits->unknownbits$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !call-gate-descriptor-attributesbits->unknownbits$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x
 (implies (call-gate-descriptor-attributesbits-equiv x x-equiv)
          (equal (!call-gate-descriptor-attributesbits->unknownbits$inline
                      unknownbits x)
                 (!call-gate-descriptor-attributesbits->unknownbits$inline
                      unknownbits x-equiv)))
 :rule-classes :congruence)

Theorem: !call-gate-descriptor-attributesbits->unknownbits-is-call-gate-descriptor-attributesbits

(defthm
 !call-gate-descriptor-attributesbits->unknownbits-is-call-gate-descriptor-attributesbits
 (equal
   (!call-gate-descriptor-attributesbits->unknownbits unknownbits x)
   (change-call-gate-descriptor-attributesbits
        x
        :unknownbits unknownbits)))

Theorem: call-gate-descriptor-attributesbits->unknownbits-of-!call-gate-descriptor-attributesbits->unknownbits

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

Theorem: !call-gate-descriptor-attributesbits->unknownbits-equiv-under-mask

(defthm
 !call-gate-descriptor-attributesbits->unknownbits-equiv-under-mask
 (b* ((?new-x (!call-gate-descriptor-attributesbits->unknownbits$inline
                   unknownbits x)))
   (call-gate-descriptor-attributesbits-equiv-under-mask
        new-x x 255)))

Function: call-gate-descriptor-attributesbits-debug

(defun call-gate-descriptor-attributesbits-debug (x)
 (declare (xargs :guard (call-gate-descriptor-attributesbits-p x)))
 (let ((__function__ 'call-gate-descriptor-attributesbits-debug))
   (declare (ignorable __function__))
   (b* (((call-gate-descriptor-attributesbits x)))
     (cons (cons 'type x.type)
           (cons (cons 's x.s)
                 (cons (cons 'dpl x.dpl)
                       (cons (cons 'p x.p)
                             (cons (cons 'unknownbits x.unknownbits)
                                   nil))))))))

Subtopics

!call-gate-descriptor-attributesbits->unknownbits: Update the |X86ISA|::|UNKNOWNBITS| field of a call-gate-descriptor-attributesbits bit structure.
!call-gate-descriptor-attributesbits->type: Update the |COMMON-LISP|::|TYPE| field of a call-gate-descriptor-attributesbits bit structure.
!call-gate-descriptor-attributesbits->dpl: Update the |X86ISA|::|DPL| field of a call-gate-descriptor-attributesbits bit structure.
!call-gate-descriptor-attributesbits->s: Update the |X86ISA|::|S| field of a call-gate-descriptor-attributesbits bit structure.
!call-gate-descriptor-attributesbits->p: Update the |ACL2|::|P| field of a call-gate-descriptor-attributesbits bit structure.
Call-gate-descriptor-attributesbits-fix: Fixing function for call-gate-descriptor-attributesbits bit structures.
Call-gate-descriptor-attributesbits->unknownbits: Access the |X86ISA|::|UNKNOWNBITS| field of a call-gate-descriptor-attributesbits bit structure.
Call-gate-descriptor-attributesbits->type: Access the |COMMON-LISP|::|TYPE| field of a call-gate-descriptor-attributesbits bit structure.
Call-gate-descriptor-attributesbits->dpl: Access the |X86ISA|::|DPL| field of a call-gate-descriptor-attributesbits bit structure.
Call-gate-descriptor-attributesbits-p: Recognizer for call-gate-descriptor-attributesbits bit structures.
Call-gate-descriptor-attributesbits->s: Access the |X86ISA|::|S| field of a call-gate-descriptor-attributesbits bit structure.
Call-gate-descriptor-attributesbits->p: Access the |ACL2|::|P| field of a call-gate-descriptor-attributesbits bit structure.