		Search-engine friendly clone of the ACL2 documentation.

System-segment-descriptorbits

!system-segment-descriptorbits->base23-16

Update the |X86ISA|::|BASE23-16| field of a system-segment-descriptorbits bit structure.

Signature
(!system-segment-descriptorbits->base23-16 base23-16 x) → new-x
Arguments: base23-16 — Guard (8bits-p base23-16).; x — Guard (system-segment-descriptorbits-p x).
Returns: new-x — Type (system-segment-descriptorbits-p new-x).

Definitions and Theorems

Function: !system-segment-descriptorbits->base23-16$inline

(defun !system-segment-descriptorbits->base23-16$inline
       (base23-16 x)
 (declare (xargs :guard (and (8bits-p base23-16)
                             (system-segment-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((base23-16 (mbe :logic (8bits-fix base23-16)
                        :exec base23-16))
        (x (system-segment-descriptorbits-fix x)))
     (part-install base23-16 x
                   :width 8
                   :low 32))
   :exec
   (the (unsigned-byte 128)
        (logior (the (unsigned-byte 128)
                     (logand (the (unsigned-byte 128) x)
                             (the (signed-byte 41) -1095216660481)))
                (the (unsigned-byte 40)
                     (ash (the (unsigned-byte 8) base23-16)
                          32))))))

Theorem: system-segment-descriptorbits-p-of-!system-segment-descriptorbits->base23-16

(defthm
 system-segment-descriptorbits-p-of-!system-segment-descriptorbits->base23-16
 (b*
  ((new-x
    (!system-segment-descriptorbits->base23-16$inline base23-16 x)))
  (system-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !system-segment-descriptorbits->base23-16$inline-of-8bits-fix-base23-16

(defthm
 !system-segment-descriptorbits->base23-16$inline-of-8bits-fix-base23-16
 (equal
    (!system-segment-descriptorbits->base23-16$inline
         (8bits-fix base23-16)
         x)
    (!system-segment-descriptorbits->base23-16$inline base23-16 x)))

Theorem: !system-segment-descriptorbits->base23-16$inline-8bits-equiv-congruence-on-base23-16

(defthm
 !system-segment-descriptorbits->base23-16$inline-8bits-equiv-congruence-on-base23-16
 (implies
  (8bits-equiv base23-16 base23-16-equiv)
  (equal
      (!system-segment-descriptorbits->base23-16$inline base23-16 x)
      (!system-segment-descriptorbits->base23-16$inline
           base23-16-equiv x)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptorbits->base23-16$inline-of-system-segment-descriptorbits-fix-x

(defthm
 !system-segment-descriptorbits->base23-16$inline-of-system-segment-descriptorbits-fix-x
 (equal
    (!system-segment-descriptorbits->base23-16$inline
         base23-16
         (system-segment-descriptorbits-fix x))
    (!system-segment-descriptorbits->base23-16$inline base23-16 x)))

Theorem: !system-segment-descriptorbits->base23-16$inline-system-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !system-segment-descriptorbits->base23-16$inline-system-segment-descriptorbits-equiv-congruence-on-x
 (implies
  (system-segment-descriptorbits-equiv x x-equiv)
  (equal
      (!system-segment-descriptorbits->base23-16$inline base23-16 x)
      (!system-segment-descriptorbits->base23-16$inline
           base23-16 x-equiv)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptorbits->base23-16-is-system-segment-descriptorbits

(defthm
 !system-segment-descriptorbits->base23-16-is-system-segment-descriptorbits
 (equal
      (!system-segment-descriptorbits->base23-16 base23-16 x)
      (change-system-segment-descriptorbits x
                                            :base23-16 base23-16)))

Theorem: system-segment-descriptorbits->base23-16-of-!system-segment-descriptorbits->base23-16

(defthm
 system-segment-descriptorbits->base23-16-of-!system-segment-descriptorbits->base23-16
 (b*
  ((?new-x
    (!system-segment-descriptorbits->base23-16$inline base23-16 x)))
  (equal (system-segment-descriptorbits->base23-16 new-x)
         (8bits-fix base23-16))))

Theorem: !system-segment-descriptorbits->base23-16-equiv-under-mask

(defthm !system-segment-descriptorbits->base23-16-equiv-under-mask
 (b*
  ((?new-x
    (!system-segment-descriptorbits->base23-16$inline base23-16 x)))
  (system-segment-descriptorbits-equiv-under-mask
       new-x x -1095216660481)))