		Search-engine friendly clone of the ACL2 documentation.

Call-gate-descriptorbits

!call-gate-descriptorbits->selector

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

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

Definitions and Theorems

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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