		Search-engine friendly clone of the ACL2 documentation.

Interrupt/trap-gate-descriptorbits

!interrupt/trap-gate-descriptorbits->all-zeros?

Update the |X86ISA|::|ALL-ZEROS?| field of a interrupt/trap-gate-descriptorbits bit structure.

Signature
(!interrupt/trap-gate-descriptorbits->all-zeros? all-zeros? x) → new-x
Arguments: all-zeros? — Guard (5bits-p all-zeros?).; x — Guard (interrupt/trap-gate-descriptorbits-p x).
Returns: new-x — Type (interrupt/trap-gate-descriptorbits-p new-x).

Definitions and Theorems

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