		Search-engine friendly clone of the ACL2 documentation.

Gdtr/idtrbits

!gdtr/idtrbits->limit

Update the |X86ISA|::|LIMIT| field of a gdtr/idtrbits bit structure.

Signature
(!gdtr/idtrbits->limit limit x) → new-x
Arguments: limit — Guard (16bits-p limit).; x — Guard (gdtr/idtrbits-p x).
Returns: new-x — Type (gdtr/idtrbits-p new-x).

Definitions and Theorems

Function: !gdtr/idtrbits->limit$inline

(defun !gdtr/idtrbits->limit$inline (limit x)
 (declare (xargs :guard (and (16bits-p limit)
                             (gdtr/idtrbits-p x))))
 (mbe
  :logic
  (b* ((limit (mbe :logic (16bits-fix limit)
                   :exec limit))
       (x (gdtr/idtrbits-fix x)))
    (part-install limit x
                  :width 16
                  :low 64))
  :exec (the (unsigned-byte 80)
             (logior (the (unsigned-byte 80)
                          (logand (the (unsigned-byte 80) x)
                                  (the (signed-byte 81)
                                       -1208907372870555465154561)))
                     (the (unsigned-byte 80)
                          (ash (the (unsigned-byte 16) limit)
                               64))))))

Theorem: gdtr/idtrbits-p-of-!gdtr/idtrbits->limit

(defthm gdtr/idtrbits-p-of-!gdtr/idtrbits->limit
  (b* ((new-x (!gdtr/idtrbits->limit$inline limit x)))
    (gdtr/idtrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !gdtr/idtrbits->limit$inline-of-16bits-fix-limit

(defthm !gdtr/idtrbits->limit$inline-of-16bits-fix-limit
  (equal (!gdtr/idtrbits->limit$inline (16bits-fix limit)
                                       x)
         (!gdtr/idtrbits->limit$inline limit x)))

Theorem: !gdtr/idtrbits->limit$inline-16bits-equiv-congruence-on-limit

(defthm
      !gdtr/idtrbits->limit$inline-16bits-equiv-congruence-on-limit
  (implies (16bits-equiv limit limit-equiv)
           (equal (!gdtr/idtrbits->limit$inline limit x)
                  (!gdtr/idtrbits->limit$inline limit-equiv x)))
  :rule-classes :congruence)

Theorem: !gdtr/idtrbits->limit$inline-of-gdtr/idtrbits-fix-x

(defthm !gdtr/idtrbits->limit$inline-of-gdtr/idtrbits-fix-x
  (equal (!gdtr/idtrbits->limit$inline limit (gdtr/idtrbits-fix x))
         (!gdtr/idtrbits->limit$inline limit x)))

Theorem: !gdtr/idtrbits->limit$inline-gdtr/idtrbits-equiv-congruence-on-x

(defthm
   !gdtr/idtrbits->limit$inline-gdtr/idtrbits-equiv-congruence-on-x
  (implies (gdtr/idtrbits-equiv x x-equiv)
           (equal (!gdtr/idtrbits->limit$inline limit x)
                  (!gdtr/idtrbits->limit$inline limit x-equiv)))
  :rule-classes :congruence)

Theorem: !gdtr/idtrbits->limit-is-gdtr/idtrbits

(defthm !gdtr/idtrbits->limit-is-gdtr/idtrbits
  (equal (!gdtr/idtrbits->limit limit x)
         (change-gdtr/idtrbits x :limit limit)))

Theorem: gdtr/idtrbits->limit-of-!gdtr/idtrbits->limit

(defthm gdtr/idtrbits->limit-of-!gdtr/idtrbits->limit
  (b* ((?new-x (!gdtr/idtrbits->limit$inline limit x)))
    (equal (gdtr/idtrbits->limit new-x)
           (16bits-fix limit))))

Theorem: !gdtr/idtrbits->limit-equiv-under-mask

(defthm !gdtr/idtrbits->limit-equiv-under-mask
  (b* ((?new-x (!gdtr/idtrbits->limit$inline limit x)))
    (gdtr/idtrbits-equiv-under-mask new-x x 18446744073709551615)))