		Search-engine friendly clone of the ACL2 documentation.

Segment-selectorbits

Segment-selectorbits->index

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

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

Definitions and Theorems

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