		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Gdtr/idtrbits

AMD manual, Jun'23, Vol. 2, Figure 4-8.

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

Fields

base-addr — 64bits
limit — 16bits

Definitions and Theorems

Function: gdtr/idtrbits-p

(defun gdtr/idtrbits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'gdtr/idtrbits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 80 x)
         :exec (and (natp x)
                    (< x 1208925819614629174706176)))))

Theorem: gdtr/idtrbits-p-when-unsigned-byte-p

(defthm gdtr/idtrbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 80 x)
           (gdtr/idtrbits-p x)))

Theorem: unsigned-byte-p-when-gdtr/idtrbits-p

(defthm unsigned-byte-p-when-gdtr/idtrbits-p
  (implies (gdtr/idtrbits-p x)
           (unsigned-byte-p 80 x)))

Theorem: gdtr/idtrbits-p-compound-recognizer

(defthm gdtr/idtrbits-p-compound-recognizer
  (implies (gdtr/idtrbits-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: gdtr/idtrbits-fix

(defun gdtr/idtrbits-fix (x)
  (declare (xargs :guard (gdtr/idtrbits-p x)))
  (let ((__function__ 'gdtr/idtrbits-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 80 x) :exec x)))

Theorem: gdtr/idtrbits-p-of-gdtr/idtrbits-fix

(defthm gdtr/idtrbits-p-of-gdtr/idtrbits-fix
  (b* ((fty::fixed (gdtr/idtrbits-fix x)))
    (gdtr/idtrbits-p fty::fixed))
  :rule-classes :rewrite)

Theorem: gdtr/idtrbits-fix-when-gdtr/idtrbits-p

(defthm gdtr/idtrbits-fix-when-gdtr/idtrbits-p
  (implies (gdtr/idtrbits-p x)
           (equal (gdtr/idtrbits-fix x) x)))

Function: gdtr/idtrbits-equiv$inline

(defun gdtr/idtrbits-equiv$inline (x y)
  (declare (xargs :guard (and (gdtr/idtrbits-p x)
                              (gdtr/idtrbits-p y))))
  (equal (gdtr/idtrbits-fix x)
         (gdtr/idtrbits-fix y)))

Theorem: gdtr/idtrbits-equiv-is-an-equivalence

(defthm gdtr/idtrbits-equiv-is-an-equivalence
  (and (booleanp (gdtr/idtrbits-equiv x y))
       (gdtr/idtrbits-equiv x x)
       (implies (gdtr/idtrbits-equiv x y)
                (gdtr/idtrbits-equiv y x))
       (implies (and (gdtr/idtrbits-equiv x y)
                     (gdtr/idtrbits-equiv y z))
                (gdtr/idtrbits-equiv x z)))
  :rule-classes (:equivalence))

Theorem: gdtr/idtrbits-equiv-implies-equal-gdtr/idtrbits-fix-1

(defthm gdtr/idtrbits-equiv-implies-equal-gdtr/idtrbits-fix-1
  (implies (gdtr/idtrbits-equiv x x-equiv)
           (equal (gdtr/idtrbits-fix x)
                  (gdtr/idtrbits-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: gdtr/idtrbits-fix-under-gdtr/idtrbits-equiv

(defthm gdtr/idtrbits-fix-under-gdtr/idtrbits-equiv
  (gdtr/idtrbits-equiv (gdtr/idtrbits-fix x)
                       x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: gdtr/idtrbits

(defun gdtr/idtrbits (base-addr limit)
  (declare (xargs :guard (and (64bits-p base-addr)
                              (16bits-p limit))))
  (let ((__function__ 'gdtr/idtrbits))
    (declare (ignorable __function__))
    (b* ((base-addr (mbe :logic (64bits-fix base-addr)
                         :exec base-addr))
         (limit (mbe :logic (16bits-fix limit)
                     :exec limit)))
      (logapp 64 base-addr limit))))

Theorem: gdtr/idtrbits-p-of-gdtr/idtrbits

(defthm gdtr/idtrbits-p-of-gdtr/idtrbits
  (b* ((gdtr/idtrbits (gdtr/idtrbits base-addr limit)))
    (gdtr/idtrbits-p gdtr/idtrbits))
  :rule-classes :rewrite)

Theorem: gdtr/idtrbits-of-64bits-fix-base-addr

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

Theorem: gdtr/idtrbits-64bits-equiv-congruence-on-base-addr

(defthm gdtr/idtrbits-64bits-equiv-congruence-on-base-addr
  (implies (64bits-equiv base-addr base-addr-equiv)
           (equal (gdtr/idtrbits base-addr limit)
                  (gdtr/idtrbits base-addr-equiv limit)))
  :rule-classes :congruence)

Theorem: gdtr/idtrbits-of-16bits-fix-limit

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

Theorem: gdtr/idtrbits-16bits-equiv-congruence-on-limit

(defthm gdtr/idtrbits-16bits-equiv-congruence-on-limit
  (implies (16bits-equiv limit limit-equiv)
           (equal (gdtr/idtrbits base-addr limit)
                  (gdtr/idtrbits base-addr limit-equiv)))
  :rule-classes :congruence)

Function: gdtr/idtrbits-equiv-under-mask

(defun gdtr/idtrbits-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (gdtr/idtrbits-p x)
                              (gdtr/idtrbits-p x1)
                              (integerp mask))))
  (let ((__function__ 'gdtr/idtrbits-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (gdtr/idtrbits-fix x)
                               (gdtr/idtrbits-fix x1)
                               mask)))

Function: gdtr/idtrbits->base-addr$inline

(defun gdtr/idtrbits->base-addr$inline (x)
  (declare (xargs :guard (gdtr/idtrbits-p x)))
  (mbe :logic
       (let ((x (gdtr/idtrbits-fix x)))
         (part-select x :low 0 :width 64))
       :exec (the (unsigned-byte 64)
                  (logand (the (unsigned-byte 64)
                               18446744073709551615)
                          (the (unsigned-byte 80) x)))))

Theorem: 64bits-p-of-gdtr/idtrbits->base-addr

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

Theorem: gdtr/idtrbits->base-addr$inline-of-gdtr/idtrbits-fix-x

(defthm gdtr/idtrbits->base-addr$inline-of-gdtr/idtrbits-fix-x
  (equal (gdtr/idtrbits->base-addr$inline (gdtr/idtrbits-fix x))
         (gdtr/idtrbits->base-addr$inline x)))

Theorem: gdtr/idtrbits->base-addr$inline-gdtr/idtrbits-equiv-congruence-on-x

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

Theorem: gdtr/idtrbits->base-addr-of-gdtr/idtrbits

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

Theorem: gdtr/idtrbits->base-addr-of-write-with-mask

(defthm gdtr/idtrbits->base-addr-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)
                               18446744073709551615)
                       0))
           (equal (gdtr/idtrbits->base-addr x)
                  (gdtr/idtrbits->base-addr y))))

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

Theorem: gdtr/idtrbits-fix-in-terms-of-gdtr/idtrbits

(defthm gdtr/idtrbits-fix-in-terms-of-gdtr/idtrbits
  (equal (gdtr/idtrbits-fix x)
         (change-gdtr/idtrbits x)))

Function: !gdtr/idtrbits->base-addr$inline

(defun !gdtr/idtrbits->base-addr$inline (base-addr x)
  (declare (xargs :guard (and (64bits-p base-addr)
                              (gdtr/idtrbits-p x))))
  (mbe :logic
       (b* ((base-addr (mbe :logic (64bits-fix base-addr)
                            :exec base-addr))
            (x (gdtr/idtrbits-fix x)))
         (part-install base-addr x
                       :width 64
                       :low 0))
       :exec (the (unsigned-byte 80)
                  (logior (the (unsigned-byte 80)
                               (logand (the (unsigned-byte 80) x)
                                       (the (signed-byte 65)
                                            -18446744073709551616)))
                          (the (unsigned-byte 64) base-addr)))))

Theorem: gdtr/idtrbits-p-of-!gdtr/idtrbits->base-addr

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

Theorem: !gdtr/idtrbits->base-addr$inline-of-64bits-fix-base-addr

(defthm !gdtr/idtrbits->base-addr$inline-of-64bits-fix-base-addr
  (equal (!gdtr/idtrbits->base-addr$inline (64bits-fix base-addr)
                                           x)
         (!gdtr/idtrbits->base-addr$inline base-addr x)))

Theorem: !gdtr/idtrbits->base-addr$inline-64bits-equiv-congruence-on-base-addr

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

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

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

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

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

Theorem: !gdtr/idtrbits->base-addr-is-gdtr/idtrbits

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

Theorem: gdtr/idtrbits->base-addr-of-!gdtr/idtrbits->base-addr

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

Theorem: !gdtr/idtrbits->base-addr-equiv-under-mask

(defthm !gdtr/idtrbits->base-addr-equiv-under-mask
  (b* ((?new-x (!gdtr/idtrbits->base-addr$inline base-addr x)))
    (gdtr/idtrbits-equiv-under-mask new-x x -18446744073709551616)))

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

Function: gdtr/idtrbits-debug

(defun gdtr/idtrbits-debug (x)
  (declare (xargs :guard (gdtr/idtrbits-p x)))
  (let ((__function__ 'gdtr/idtrbits-debug))
    (declare (ignorable __function__))
    (b* (((gdtr/idtrbits x)))
      (cons (cons 'base-addr x.base-addr)
            (cons (cons 'limit x.limit) nil)))))

Subtopics

!gdtr/idtrbits->base-addr: Update the |X86ISA|::|BASE-ADDR| field of a gdtr/idtrbits bit structure.
!gdtr/idtrbits->limit: Update the |X86ISA|::|LIMIT| field of a gdtr/idtrbits bit structure.
Gdtr/idtrbits->base-addr: Access the |X86ISA|::|BASE-ADDR| field of a gdtr/idtrbits bit structure.
Gdtr/idtrbits->limit: Access the |X86ISA|::|LIMIT| field of a gdtr/idtrbits bit structure.
Gdtr/idtrbits-fix: Fixing function for gdtr/idtrbits bit structures.
Gdtr/idtrbits-p: Recognizer for gdtr/idtrbits bit structures.