		Search-engine friendly clone of the ACL2 documentation.

Segment-selectorbits

!segment-selectorbits->ti

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

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

Definitions and Theorems

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