		Search-engine friendly clone of the ACL2 documentation.

Gdtr/idtrbits

Gdtr/idtrbits->limit

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

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

Definitions and Theorems

Function: gdtr/idtrbits->limit$inline

(defun gdtr/idtrbits->limit$inline (x)
  (declare (xargs :guard (gdtr/idtrbits-p x)))
  (mbe :logic
       (let ((x (gdtr/idtrbits-fix x)))
         (part-select x :low 64 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 16)
                               (ash (the (unsigned-byte 80) x)
                                    -64))))))

Theorem: 16bits-p-of-gdtr/idtrbits->limit

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

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 (gdtr/idtrbits-fix x))
         (gdtr/idtrbits->limit$inline 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 x)
                  (gdtr/idtrbits->limit$inline x-equiv)))
  :rule-classes :congruence)

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

(defthm gdtr/idtrbits->limit-of-gdtr/idtrbits
  (equal (gdtr/idtrbits->limit (gdtr/idtrbits base-addr limit))
         (16bits-fix limit)))

Theorem: gdtr/idtrbits->limit-of-write-with-mask

(defthm gdtr/idtrbits->limit-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x gdtr/idtrbits-equiv-under-mask)
                (gdtr/idtrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask)
                               1208907372870555465154560)
                       0))
           (equal (gdtr/idtrbits->limit x)
                  (gdtr/idtrbits->limit y))))