		Search-engine friendly clone of the ACL2 documentation.

Segment-selectorbits

!segment-selectorbits->rpl

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

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

Definitions and Theorems

Function: !segment-selectorbits->rpl$inline

(defun !segment-selectorbits->rpl$inline (rpl x)
  (declare (xargs :guard (and (2bits-p rpl)
                              (segment-selectorbits-p x))))
  (mbe :logic
       (b* ((rpl (mbe :logic (2bits-fix rpl) :exec rpl))
            (x (segment-selectorbits-fix x)))
         (part-install rpl x :width 2 :low 0))
       :exec (the (unsigned-byte 16)
                  (logior (the (unsigned-byte 16)
                               (logand (the (unsigned-byte 16) x)
                                       (the (signed-byte 3) -4)))
                          (the (unsigned-byte 2) rpl)))))

Theorem: segment-selectorbits-p-of-!segment-selectorbits->rpl

(defthm segment-selectorbits-p-of-!segment-selectorbits->rpl
  (b* ((new-x (!segment-selectorbits->rpl$inline rpl x)))
    (segment-selectorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !segment-selectorbits->rpl$inline-of-2bits-fix-rpl

(defthm !segment-selectorbits->rpl$inline-of-2bits-fix-rpl
  (equal (!segment-selectorbits->rpl$inline (2bits-fix rpl)
                                            x)
         (!segment-selectorbits->rpl$inline rpl x)))

Theorem: !segment-selectorbits->rpl$inline-2bits-equiv-congruence-on-rpl

(defthm
    !segment-selectorbits->rpl$inline-2bits-equiv-congruence-on-rpl
  (implies (2bits-equiv rpl rpl-equiv)
           (equal (!segment-selectorbits->rpl$inline rpl x)
                  (!segment-selectorbits->rpl$inline rpl-equiv x)))
  :rule-classes :congruence)

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
              rpl (segment-selectorbits-fix x))
         (!segment-selectorbits->rpl$inline rpl 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 rpl x)
                 (!segment-selectorbits->rpl$inline rpl x-equiv)))
 :rule-classes :congruence)

Theorem: !segment-selectorbits->rpl-is-segment-selectorbits

(defthm !segment-selectorbits->rpl-is-segment-selectorbits
  (equal (!segment-selectorbits->rpl rpl x)
         (change-segment-selectorbits x
                                      :rpl rpl)))

Theorem: segment-selectorbits->rpl-of-!segment-selectorbits->rpl

(defthm segment-selectorbits->rpl-of-!segment-selectorbits->rpl
  (b* ((?new-x (!segment-selectorbits->rpl$inline rpl x)))
    (equal (segment-selectorbits->rpl new-x)
           (2bits-fix rpl))))

Theorem: !segment-selectorbits->rpl-equiv-under-mask

(defthm !segment-selectorbits->rpl-equiv-under-mask
  (b* ((?new-x (!segment-selectorbits->rpl$inline rpl x)))
    (segment-selectorbits-equiv-under-mask new-x x -4)))