		Search-engine friendly clone of the ACL2 documentation.

Segment-selectorbits

!segment-selectorbits->index

Update the |X86ISA|::|INDEX| field of a segment-selectorbits bit structure.

Signature
(!segment-selectorbits->index index x) → new-x
Arguments: index — Guard (13bits-p index).; x — Guard (segment-selectorbits-p x).
Returns: new-x — Type (segment-selectorbits-p new-x).

Definitions and Theorems

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