		Search-engine friendly clone of the ACL2 documentation.

Segment-selectorbits

Segment-selectorbits->rpl

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

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

Definitions and Theorems

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