		Search-engine friendly clone of the ACL2 documentation.

System-segment-descriptor-attributesbits

!system-segment-descriptor-attributesbits->dpl

Update the |X86ISA|::|DPL| field of a system-segment-descriptor-attributesbits bit structure.

Signature
(!system-segment-descriptor-attributesbits->dpl dpl x) → new-x
Arguments: dpl — Guard (2bits-p dpl).; x — Guard (system-segment-descriptor-attributesbits-p x).
Returns: new-x — Type (system-segment-descriptor-attributesbits-p new-x).

Definitions and Theorems

Function: !system-segment-descriptor-attributesbits->dpl$inline

(defun !system-segment-descriptor-attributesbits->dpl$inline (dpl x)
 (declare
  (xargs
       :guard (and (2bits-p dpl)
                   (system-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl))
         (x (system-segment-descriptor-attributesbits-fix x)))
      (part-install dpl x :width 2 :low 5))
    :exec (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16)
                            (logand (the (unsigned-byte 16) x)
                                    (the (signed-byte 8) -97)))
                       (the (unsigned-byte 7)
                            (ash (the (unsigned-byte 2) dpl) 5))))))

Theorem: system-segment-descriptor-attributesbits-p-of-!system-segment-descriptor-attributesbits->dpl

(defthm
 system-segment-descriptor-attributesbits-p-of-!system-segment-descriptor-attributesbits->dpl
 (b*
  ((new-x
     (!system-segment-descriptor-attributesbits->dpl$inline dpl x)))
  (system-segment-descriptor-attributesbits-p new-x))
 :rule-classes :rewrite)

Theorem: !system-segment-descriptor-attributesbits->dpl$inline-of-2bits-fix-dpl

(defthm
 !system-segment-descriptor-attributesbits->dpl$inline-of-2bits-fix-dpl
 (equal
     (!system-segment-descriptor-attributesbits->dpl$inline
          (2bits-fix dpl)
          x)
     (!system-segment-descriptor-attributesbits->dpl$inline dpl x)))

Theorem: !system-segment-descriptor-attributesbits->dpl$inline-2bits-equiv-congruence-on-dpl

(defthm
 !system-segment-descriptor-attributesbits->dpl$inline-2bits-equiv-congruence-on-dpl
 (implies
  (2bits-equiv dpl dpl-equiv)
  (equal
       (!system-segment-descriptor-attributesbits->dpl$inline dpl x)
       (!system-segment-descriptor-attributesbits->dpl$inline
            dpl-equiv x)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptor-attributesbits->dpl$inline-of-system-segment-descriptor-attributesbits-fix-x

(defthm
 !system-segment-descriptor-attributesbits->dpl$inline-of-system-segment-descriptor-attributesbits-fix-x
 (equal
     (!system-segment-descriptor-attributesbits->dpl$inline
          dpl
          (system-segment-descriptor-attributesbits-fix x))
     (!system-segment-descriptor-attributesbits->dpl$inline dpl x)))

Theorem: !system-segment-descriptor-attributesbits->dpl$inline-system-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !system-segment-descriptor-attributesbits->dpl$inline-system-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (system-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
       (!system-segment-descriptor-attributesbits->dpl$inline dpl x)
       (!system-segment-descriptor-attributesbits->dpl$inline
            dpl x-equiv)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptor-attributesbits->dpl-is-system-segment-descriptor-attributesbits

(defthm
 !system-segment-descriptor-attributesbits->dpl-is-system-segment-descriptor-attributesbits
 (equal (!system-segment-descriptor-attributesbits->dpl dpl x)
        (change-system-segment-descriptor-attributesbits x
                                                         :dpl dpl)))

Theorem: system-segment-descriptor-attributesbits->dpl-of-!system-segment-descriptor-attributesbits->dpl

(defthm
 system-segment-descriptor-attributesbits->dpl-of-!system-segment-descriptor-attributesbits->dpl
 (b*
  ((?new-x
     (!system-segment-descriptor-attributesbits->dpl$inline dpl x)))
  (equal (system-segment-descriptor-attributesbits->dpl new-x)
         (2bits-fix dpl))))

Theorem: !system-segment-descriptor-attributesbits->dpl-equiv-under-mask

(defthm
    !system-segment-descriptor-attributesbits->dpl-equiv-under-mask
 (b*
  ((?new-x
     (!system-segment-descriptor-attributesbits->dpl$inline dpl x)))
  (system-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -97)))