		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Segment-selectorbits

Intel manual, Mar'23, Vol. 3A, Figure 3-6.

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

Fields

rpl — 2bits
ti — bit
index — 13bits

Definitions and Theorems

Function: segment-selectorbits-p

(defun segment-selectorbits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'segment-selectorbits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 16 x)
         :exec (and (natp x) (< x 65536)))))

Theorem: segment-selectorbits-p-when-unsigned-byte-p

(defthm segment-selectorbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 16 x)
           (segment-selectorbits-p x)))

Theorem: unsigned-byte-p-when-segment-selectorbits-p

(defthm unsigned-byte-p-when-segment-selectorbits-p
  (implies (segment-selectorbits-p x)
           (unsigned-byte-p 16 x)))

Theorem: segment-selectorbits-p-compound-recognizer

(defthm segment-selectorbits-p-compound-recognizer
  (implies (segment-selectorbits-p x)
           (natp x))
  :rule-classes :compound-recognizer)

Function: segment-selectorbits-fix

(defun segment-selectorbits-fix (x)
  (declare (xargs :guard (segment-selectorbits-p x)))
  (let ((__function__ 'segment-selectorbits-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 16 x) :exec x)))

Theorem: segment-selectorbits-p-of-segment-selectorbits-fix

(defthm segment-selectorbits-p-of-segment-selectorbits-fix
  (b* ((fty::fixed (segment-selectorbits-fix x)))
    (segment-selectorbits-p fty::fixed))
  :rule-classes :rewrite)

Theorem: segment-selectorbits-fix-when-segment-selectorbits-p

(defthm segment-selectorbits-fix-when-segment-selectorbits-p
  (implies (segment-selectorbits-p x)
           (equal (segment-selectorbits-fix x) x)))

Function: segment-selectorbits-equiv$inline

(defun segment-selectorbits-equiv$inline (x y)
  (declare (xargs :guard (and (segment-selectorbits-p x)
                              (segment-selectorbits-p y))))
  (equal (segment-selectorbits-fix x)
         (segment-selectorbits-fix y)))

Theorem: segment-selectorbits-equiv-is-an-equivalence

(defthm segment-selectorbits-equiv-is-an-equivalence
  (and (booleanp (segment-selectorbits-equiv x y))
       (segment-selectorbits-equiv x x)
       (implies (segment-selectorbits-equiv x y)
                (segment-selectorbits-equiv y x))
       (implies (and (segment-selectorbits-equiv x y)
                     (segment-selectorbits-equiv y z))
                (segment-selectorbits-equiv x z)))
  :rule-classes (:equivalence))

Theorem: segment-selectorbits-equiv-implies-equal-segment-selectorbits-fix-1

(defthm
 segment-selectorbits-equiv-implies-equal-segment-selectorbits-fix-1
 (implies (segment-selectorbits-equiv x x-equiv)
          (equal (segment-selectorbits-fix x)
                 (segment-selectorbits-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: segment-selectorbits-fix-under-segment-selectorbits-equiv

(defthm segment-selectorbits-fix-under-segment-selectorbits-equiv
  (segment-selectorbits-equiv (segment-selectorbits-fix x)
                              x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: segment-selectorbits

(defun segment-selectorbits (rpl ti index)
  (declare (xargs :guard (and (2bits-p rpl)
                              (bitp ti)
                              (13bits-p index))))
  (let ((__function__ 'segment-selectorbits))
    (declare (ignorable __function__))
    (b* ((rpl (mbe :logic (2bits-fix rpl) :exec rpl))
         (ti (mbe :logic (bfix ti) :exec ti))
         (index (mbe :logic (13bits-fix index)
                     :exec index)))
      (logapp 2 rpl (logapp 1 ti index)))))

Theorem: segment-selectorbits-p-of-segment-selectorbits

(defthm segment-selectorbits-p-of-segment-selectorbits
  (b* ((segment-selectorbits (segment-selectorbits rpl ti index)))
    (segment-selectorbits-p segment-selectorbits))
  :rule-classes :rewrite)

Theorem: segment-selectorbits-of-2bits-fix-rpl

(defthm segment-selectorbits-of-2bits-fix-rpl
  (equal (segment-selectorbits (2bits-fix rpl)
                               ti index)
         (segment-selectorbits rpl ti index)))

Theorem: segment-selectorbits-2bits-equiv-congruence-on-rpl

(defthm segment-selectorbits-2bits-equiv-congruence-on-rpl
  (implies (2bits-equiv rpl rpl-equiv)
           (equal (segment-selectorbits rpl ti index)
                  (segment-selectorbits rpl-equiv ti index)))
  :rule-classes :congruence)

Theorem: segment-selectorbits-of-bfix-ti

(defthm segment-selectorbits-of-bfix-ti
  (equal (segment-selectorbits rpl (bfix ti)
                               index)
         (segment-selectorbits rpl ti index)))

Theorem: segment-selectorbits-bit-equiv-congruence-on-ti

(defthm segment-selectorbits-bit-equiv-congruence-on-ti
  (implies (bit-equiv ti ti-equiv)
           (equal (segment-selectorbits rpl ti index)
                  (segment-selectorbits rpl ti-equiv index)))
  :rule-classes :congruence)

Theorem: segment-selectorbits-of-13bits-fix-index

(defthm segment-selectorbits-of-13bits-fix-index
  (equal (segment-selectorbits rpl ti (13bits-fix index))
         (segment-selectorbits rpl ti index)))

Theorem: segment-selectorbits-13bits-equiv-congruence-on-index

(defthm segment-selectorbits-13bits-equiv-congruence-on-index
  (implies (13bits-equiv index index-equiv)
           (equal (segment-selectorbits rpl ti index)
                  (segment-selectorbits rpl ti index-equiv)))
  :rule-classes :congruence)

Function: segment-selectorbits-equiv-under-mask

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

Function: segment-selectorbits->rpl$inline

(defun segment-selectorbits->rpl$inline (x)
  (declare (xargs :guard (segment-selectorbits-p x)))
  (mbe :logic
       (let ((x (segment-selectorbits-fix x)))
         (part-select x :low 0 :width 2))
       :exec (the (unsigned-byte 2)
                  (logand (the (unsigned-byte 2) 3)
                          (the (unsigned-byte 16) x)))))

Theorem: 2bits-p-of-segment-selectorbits->rpl

(defthm 2bits-p-of-segment-selectorbits->rpl
  (b* ((rpl (segment-selectorbits->rpl$inline x)))
    (2bits-p rpl))
  :rule-classes :rewrite)

Theorem: segment-selectorbits->rpl$inline-of-segment-selectorbits-fix-x

(defthm
     segment-selectorbits->rpl$inline-of-segment-selectorbits-fix-x
 (equal
     (segment-selectorbits->rpl$inline (segment-selectorbits-fix x))
     (segment-selectorbits->rpl$inline x)))

Theorem: segment-selectorbits->rpl$inline-segment-selectorbits-equiv-congruence-on-x

(defthm
 segment-selectorbits->rpl$inline-segment-selectorbits-equiv-congruence-on-x
 (implies (segment-selectorbits-equiv x x-equiv)
          (equal (segment-selectorbits->rpl$inline x)
                 (segment-selectorbits->rpl$inline x-equiv)))
 :rule-classes :congruence)

Theorem: segment-selectorbits->rpl-of-segment-selectorbits

(defthm segment-selectorbits->rpl-of-segment-selectorbits
 (equal
     (segment-selectorbits->rpl (segment-selectorbits rpl ti index))
     (2bits-fix rpl)))

Theorem: segment-selectorbits->rpl-of-write-with-mask

(defthm segment-selectorbits->rpl-of-write-with-mask
 (implies (and (fty::bitstruct-read-over-write-hyps
                    x segment-selectorbits-equiv-under-mask)
               (segment-selectorbits-equiv-under-mask x y fty::mask)
               (equal (logand (lognot fty::mask) 3) 0))
          (equal (segment-selectorbits->rpl x)
                 (segment-selectorbits->rpl y))))

Function: segment-selectorbits->ti$inline

(defun segment-selectorbits->ti$inline (x)
 (declare (xargs :guard (segment-selectorbits-p x)))
 (mbe
    :logic
    (let ((x (segment-selectorbits-fix x)))
      (part-select x :low 2 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 14)
                            (ash (the (unsigned-byte 16) x) -2))))))

Theorem: bitp-of-segment-selectorbits->ti

(defthm bitp-of-segment-selectorbits->ti
  (b* ((ti (segment-selectorbits->ti$inline x)))
    (bitp ti))
  :rule-classes :rewrite)

Theorem: segment-selectorbits->ti$inline-of-segment-selectorbits-fix-x

(defthm
      segment-selectorbits->ti$inline-of-segment-selectorbits-fix-x
 (equal
      (segment-selectorbits->ti$inline (segment-selectorbits-fix x))
      (segment-selectorbits->ti$inline x)))

Theorem: segment-selectorbits->ti$inline-segment-selectorbits-equiv-congruence-on-x

(defthm
 segment-selectorbits->ti$inline-segment-selectorbits-equiv-congruence-on-x
 (implies (segment-selectorbits-equiv x x-equiv)
          (equal (segment-selectorbits->ti$inline x)
                 (segment-selectorbits->ti$inline x-equiv)))
 :rule-classes :congruence)

Theorem: segment-selectorbits->ti-of-segment-selectorbits

(defthm segment-selectorbits->ti-of-segment-selectorbits
 (equal
      (segment-selectorbits->ti (segment-selectorbits rpl ti index))
      (bfix ti)))

Theorem: segment-selectorbits->ti-of-write-with-mask

(defthm segment-selectorbits->ti-of-write-with-mask
 (implies (and (fty::bitstruct-read-over-write-hyps
                    x segment-selectorbits-equiv-under-mask)
               (segment-selectorbits-equiv-under-mask x y fty::mask)
               (equal (logand (lognot fty::mask) 4) 0))
          (equal (segment-selectorbits->ti x)
                 (segment-selectorbits->ti y))))

Function: segment-selectorbits->index$inline

(defun segment-selectorbits->index$inline (x)
 (declare (xargs :guard (segment-selectorbits-p x)))
 (mbe
    :logic
    (let ((x (segment-selectorbits-fix x)))
      (part-select x :low 3 :width 13))
    :exec (the (unsigned-byte 13)
               (logand (the (unsigned-byte 13) 8191)
                       (the (unsigned-byte 13)
                            (ash (the (unsigned-byte 16) x) -3))))))

Theorem: 13bits-p-of-segment-selectorbits->index

(defthm 13bits-p-of-segment-selectorbits->index
  (b* ((index (segment-selectorbits->index$inline x)))
    (13bits-p index))
  :rule-classes :rewrite)

Theorem: segment-selectorbits->index$inline-of-segment-selectorbits-fix-x

(defthm
   segment-selectorbits->index$inline-of-segment-selectorbits-fix-x
 (equal
   (segment-selectorbits->index$inline (segment-selectorbits-fix x))
   (segment-selectorbits->index$inline x)))

Theorem: segment-selectorbits->index$inline-segment-selectorbits-equiv-congruence-on-x

(defthm
 segment-selectorbits->index$inline-segment-selectorbits-equiv-congruence-on-x
 (implies (segment-selectorbits-equiv x x-equiv)
          (equal (segment-selectorbits->index$inline x)
                 (segment-selectorbits->index$inline x-equiv)))
 :rule-classes :congruence)

Theorem: segment-selectorbits->index-of-segment-selectorbits

(defthm segment-selectorbits->index-of-segment-selectorbits
 (equal
   (segment-selectorbits->index (segment-selectorbits rpl ti index))
   (13bits-fix index)))

Theorem: segment-selectorbits->index-of-write-with-mask

(defthm segment-selectorbits->index-of-write-with-mask
 (implies (and (fty::bitstruct-read-over-write-hyps
                    x segment-selectorbits-equiv-under-mask)
               (segment-selectorbits-equiv-under-mask x y fty::mask)
               (equal (logand (lognot fty::mask) 65528)
                      0))
          (equal (segment-selectorbits->index x)
                 (segment-selectorbits->index y))))

Theorem: segment-selectorbits-fix-in-terms-of-segment-selectorbits

(defthm segment-selectorbits-fix-in-terms-of-segment-selectorbits
  (equal (segment-selectorbits-fix x)
         (change-segment-selectorbits x)))

Function: !segment-selectorbits->rpl$inline

(defun !segment-selectorbits->rpl$inline (rpl x)
  (declare (xargs :guard (and (2bits-p rpl)
                              (segment-selectorbits-p x))))
  (mbe :logic
       (b* ((rpl (mbe :logic (2bits-fix rpl) :exec rpl))
            (x (segment-selectorbits-fix x)))
         (part-install rpl x :width 2 :low 0))
       :exec (the (unsigned-byte 16)
                  (logior (the (unsigned-byte 16)
                               (logand (the (unsigned-byte 16) x)
                                       (the (signed-byte 3) -4)))
                          (the (unsigned-byte 2) rpl)))))

Theorem: segment-selectorbits-p-of-!segment-selectorbits->rpl

(defthm segment-selectorbits-p-of-!segment-selectorbits->rpl
  (b* ((new-x (!segment-selectorbits->rpl$inline rpl x)))
    (segment-selectorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !segment-selectorbits->rpl$inline-of-2bits-fix-rpl

(defthm !segment-selectorbits->rpl$inline-of-2bits-fix-rpl
  (equal (!segment-selectorbits->rpl$inline (2bits-fix rpl)
                                            x)
         (!segment-selectorbits->rpl$inline rpl x)))

Theorem: !segment-selectorbits->rpl$inline-2bits-equiv-congruence-on-rpl

(defthm
    !segment-selectorbits->rpl$inline-2bits-equiv-congruence-on-rpl
  (implies (2bits-equiv rpl rpl-equiv)
           (equal (!segment-selectorbits->rpl$inline rpl x)
                  (!segment-selectorbits->rpl$inline rpl-equiv x)))
  :rule-classes :congruence)

Theorem: !segment-selectorbits->rpl$inline-of-segment-selectorbits-fix-x

(defthm
    !segment-selectorbits->rpl$inline-of-segment-selectorbits-fix-x
  (equal (!segment-selectorbits->rpl$inline
              rpl (segment-selectorbits-fix x))
         (!segment-selectorbits->rpl$inline rpl x)))

Theorem: !segment-selectorbits->rpl$inline-segment-selectorbits-equiv-congruence-on-x

(defthm
 !segment-selectorbits->rpl$inline-segment-selectorbits-equiv-congruence-on-x
 (implies (segment-selectorbits-equiv x x-equiv)
          (equal (!segment-selectorbits->rpl$inline rpl x)
                 (!segment-selectorbits->rpl$inline rpl x-equiv)))
 :rule-classes :congruence)

Theorem: !segment-selectorbits->rpl-is-segment-selectorbits

(defthm !segment-selectorbits->rpl-is-segment-selectorbits
  (equal (!segment-selectorbits->rpl rpl x)
         (change-segment-selectorbits x
                                      :rpl rpl)))

Theorem: segment-selectorbits->rpl-of-!segment-selectorbits->rpl

(defthm segment-selectorbits->rpl-of-!segment-selectorbits->rpl
  (b* ((?new-x (!segment-selectorbits->rpl$inline rpl x)))
    (equal (segment-selectorbits->rpl new-x)
           (2bits-fix rpl))))

Theorem: !segment-selectorbits->rpl-equiv-under-mask

(defthm !segment-selectorbits->rpl-equiv-under-mask
  (b* ((?new-x (!segment-selectorbits->rpl$inline rpl x)))
    (segment-selectorbits-equiv-under-mask new-x x -4)))

Function: !segment-selectorbits->ti$inline

(defun !segment-selectorbits->ti$inline (ti x)
 (declare (xargs :guard (and (bitp ti)
                             (segment-selectorbits-p x))))
 (mbe
     :logic
     (b* ((ti (mbe :logic (bfix ti) :exec ti))
          (x (segment-selectorbits-fix x)))
       (part-install ti x :width 1 :low 2))
     :exec (the (unsigned-byte 16)
                (logior (the (unsigned-byte 16)
                             (logand (the (unsigned-byte 16) x)
                                     (the (signed-byte 4) -5)))
                        (the (unsigned-byte 3)
                             (ash (the (unsigned-byte 1) ti) 2))))))

Theorem: segment-selectorbits-p-of-!segment-selectorbits->ti

(defthm segment-selectorbits-p-of-!segment-selectorbits->ti
  (b* ((new-x (!segment-selectorbits->ti$inline ti x)))
    (segment-selectorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !segment-selectorbits->ti$inline-of-bfix-ti

(defthm !segment-selectorbits->ti$inline-of-bfix-ti
  (equal (!segment-selectorbits->ti$inline (bfix ti)
                                           x)
         (!segment-selectorbits->ti$inline ti x)))

Theorem: !segment-selectorbits->ti$inline-bit-equiv-congruence-on-ti

(defthm !segment-selectorbits->ti$inline-bit-equiv-congruence-on-ti
  (implies (bit-equiv ti ti-equiv)
           (equal (!segment-selectorbits->ti$inline ti x)
                  (!segment-selectorbits->ti$inline ti-equiv x)))
  :rule-classes :congruence)

Theorem: !segment-selectorbits->ti$inline-of-segment-selectorbits-fix-x

(defthm
     !segment-selectorbits->ti$inline-of-segment-selectorbits-fix-x
 (equal
  (!segment-selectorbits->ti$inline ti (segment-selectorbits-fix x))
  (!segment-selectorbits->ti$inline ti x)))

Theorem: !segment-selectorbits->ti$inline-segment-selectorbits-equiv-congruence-on-x

(defthm
 !segment-selectorbits->ti$inline-segment-selectorbits-equiv-congruence-on-x
 (implies (segment-selectorbits-equiv x x-equiv)
          (equal (!segment-selectorbits->ti$inline ti x)
                 (!segment-selectorbits->ti$inline ti x-equiv)))
 :rule-classes :congruence)

Theorem: !segment-selectorbits->ti-is-segment-selectorbits

(defthm !segment-selectorbits->ti-is-segment-selectorbits
  (equal (!segment-selectorbits->ti ti x)
         (change-segment-selectorbits x :ti ti)))

Theorem: segment-selectorbits->ti-of-!segment-selectorbits->ti

(defthm segment-selectorbits->ti-of-!segment-selectorbits->ti
  (b* ((?new-x (!segment-selectorbits->ti$inline ti x)))
    (equal (segment-selectorbits->ti new-x)
           (bfix ti))))

Theorem: !segment-selectorbits->ti-equiv-under-mask

(defthm !segment-selectorbits->ti-equiv-under-mask
  (b* ((?new-x (!segment-selectorbits->ti$inline ti x)))
    (segment-selectorbits-equiv-under-mask new-x x -5)))

Function: !segment-selectorbits->index$inline

(defun !segment-selectorbits->index$inline (index x)
 (declare (xargs :guard (and (13bits-p index)
                             (segment-selectorbits-p x))))
 (mbe
     :logic
     (b* ((index (mbe :logic (13bits-fix index)
                      :exec index))
          (x (segment-selectorbits-fix x)))
       (part-install index x :width 13 :low 3))
     :exec (the (unsigned-byte 16)
                (logior (the (unsigned-byte 16)
                             (logand (the (unsigned-byte 16) x)
                                     (the (signed-byte 17) -65529)))
                        (the (unsigned-byte 16)
                             (ash (the (unsigned-byte 13) index)
                                  3))))))

Theorem: segment-selectorbits-p-of-!segment-selectorbits->index

(defthm segment-selectorbits-p-of-!segment-selectorbits->index
  (b* ((new-x (!segment-selectorbits->index$inline index x)))
    (segment-selectorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !segment-selectorbits->index$inline-of-13bits-fix-index

(defthm !segment-selectorbits->index$inline-of-13bits-fix-index
  (equal (!segment-selectorbits->index$inline (13bits-fix index)
                                              x)
         (!segment-selectorbits->index$inline index x)))

Theorem: !segment-selectorbits->index$inline-13bits-equiv-congruence-on-index

(defthm
 !segment-selectorbits->index$inline-13bits-equiv-congruence-on-index
 (implies
      (13bits-equiv index index-equiv)
      (equal (!segment-selectorbits->index$inline index x)
             (!segment-selectorbits->index$inline index-equiv x)))
 :rule-classes :congruence)

Theorem: !segment-selectorbits->index$inline-of-segment-selectorbits-fix-x

(defthm
  !segment-selectorbits->index$inline-of-segment-selectorbits-fix-x
  (equal (!segment-selectorbits->index$inline
              index (segment-selectorbits-fix x))
         (!segment-selectorbits->index$inline index x)))

Theorem: !segment-selectorbits->index$inline-segment-selectorbits-equiv-congruence-on-x

(defthm
 !segment-selectorbits->index$inline-segment-selectorbits-equiv-congruence-on-x
 (implies
      (segment-selectorbits-equiv x x-equiv)
      (equal (!segment-selectorbits->index$inline index x)
             (!segment-selectorbits->index$inline index x-equiv)))
 :rule-classes :congruence)

Theorem: !segment-selectorbits->index-is-segment-selectorbits

(defthm !segment-selectorbits->index-is-segment-selectorbits
  (equal (!segment-selectorbits->index index x)
         (change-segment-selectorbits x
                                      :index index)))

Theorem: segment-selectorbits->index-of-!segment-selectorbits->index

(defthm segment-selectorbits->index-of-!segment-selectorbits->index
  (b* ((?new-x (!segment-selectorbits->index$inline index x)))
    (equal (segment-selectorbits->index new-x)
           (13bits-fix index))))

Theorem: !segment-selectorbits->index-equiv-under-mask

(defthm !segment-selectorbits->index-equiv-under-mask
  (b* ((?new-x (!segment-selectorbits->index$inline index x)))
    (segment-selectorbits-equiv-under-mask new-x x 7)))

Function: segment-selectorbits-debug

(defun segment-selectorbits-debug (x)
  (declare (xargs :guard (segment-selectorbits-p x)))
  (let ((__function__ 'segment-selectorbits-debug))
    (declare (ignorable __function__))
    (b* (((segment-selectorbits x)))
      (cons (cons 'rpl x.rpl)
            (cons (cons 'ti x.ti)
                  (cons (cons 'index x.index) nil))))))

Subtopics

!segment-selectorbits->index: Update the |X86ISA|::|INDEX| field of a segment-selectorbits bit structure.
!segment-selectorbits->rpl: Update the |X86ISA|::|RPL| field of a segment-selectorbits bit structure.
!segment-selectorbits->ti: Update the |X86ISA|::|TI| field of a segment-selectorbits bit structure.
Segment-selectorbits-fix: Fixing function for segment-selectorbits bit structures.
Segment-selectorbits->index: Access the |X86ISA|::|INDEX| field of a segment-selectorbits bit structure.
Segment-selectorbits->ti: Access the |X86ISA|::|TI| field of a segment-selectorbits bit structure.
Segment-selectorbits->rpl: Access the |X86ISA|::|RPL| field of a segment-selectorbits bit structure.
Segment-selectorbits-p: Recognizer for segment-selectorbits bit structures.