		Search-engine friendly clone of the ACL2 documentation.

Segment-selectorbits

Segment-selectorbits->ti

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

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

Definitions and Theorems

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