		Search-engine friendly clone of the ACL2 documentation.

Gdtr/idtrbits

!gdtr/idtrbits->base-addr

Update the |X86ISA|::|BASE-ADDR| field of a gdtr/idtrbits bit structure.

Signature
(!gdtr/idtrbits->base-addr base-addr x) → new-x
Arguments: base-addr — Guard (64bits-p base-addr).; x — Guard (gdtr/idtrbits-p x).
Returns: new-x — Type (gdtr/idtrbits-p new-x).

Definitions and Theorems

Function: !gdtr/idtrbits->base-addr$inline

(defun !gdtr/idtrbits->base-addr$inline (base-addr x)
  (declare (xargs :guard (and (64bits-p base-addr)
                              (gdtr/idtrbits-p x))))
  (mbe :logic
       (b* ((base-addr (mbe :logic (64bits-fix base-addr)
                            :exec base-addr))
            (x (gdtr/idtrbits-fix x)))
         (part-install base-addr x
                       :width 64
                       :low 0))
       :exec (the (unsigned-byte 80)
                  (logior (the (unsigned-byte 80)
                               (logand (the (unsigned-byte 80) x)
                                       (the (signed-byte 65)
                                            -18446744073709551616)))
                          (the (unsigned-byte 64) base-addr)))))

Theorem: gdtr/idtrbits-p-of-!gdtr/idtrbits->base-addr

(defthm gdtr/idtrbits-p-of-!gdtr/idtrbits->base-addr
  (b* ((new-x (!gdtr/idtrbits->base-addr$inline base-addr x)))
    (gdtr/idtrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !gdtr/idtrbits->base-addr$inline-of-64bits-fix-base-addr

(defthm !gdtr/idtrbits->base-addr$inline-of-64bits-fix-base-addr
  (equal (!gdtr/idtrbits->base-addr$inline (64bits-fix base-addr)
                                           x)
         (!gdtr/idtrbits->base-addr$inline base-addr x)))

Theorem: !gdtr/idtrbits->base-addr$inline-64bits-equiv-congruence-on-base-addr

(defthm
 !gdtr/idtrbits->base-addr$inline-64bits-equiv-congruence-on-base-addr
 (implies
      (64bits-equiv base-addr base-addr-equiv)
      (equal (!gdtr/idtrbits->base-addr$inline base-addr x)
             (!gdtr/idtrbits->base-addr$inline base-addr-equiv x)))
 :rule-classes :congruence)

Theorem: !gdtr/idtrbits->base-addr$inline-of-gdtr/idtrbits-fix-x

(defthm !gdtr/idtrbits->base-addr$inline-of-gdtr/idtrbits-fix-x
 (equal
  (!gdtr/idtrbits->base-addr$inline base-addr (gdtr/idtrbits-fix x))
  (!gdtr/idtrbits->base-addr$inline base-addr x)))

Theorem: !gdtr/idtrbits->base-addr$inline-gdtr/idtrbits-equiv-congruence-on-x

(defthm
 !gdtr/idtrbits->base-addr$inline-gdtr/idtrbits-equiv-congruence-on-x
 (implies
      (gdtr/idtrbits-equiv x x-equiv)
      (equal (!gdtr/idtrbits->base-addr$inline base-addr x)
             (!gdtr/idtrbits->base-addr$inline base-addr x-equiv)))
 :rule-classes :congruence)

Theorem: !gdtr/idtrbits->base-addr-is-gdtr/idtrbits

(defthm !gdtr/idtrbits->base-addr-is-gdtr/idtrbits
  (equal (!gdtr/idtrbits->base-addr base-addr x)
         (change-gdtr/idtrbits x
                               :base-addr base-addr)))

Theorem: gdtr/idtrbits->base-addr-of-!gdtr/idtrbits->base-addr

(defthm gdtr/idtrbits->base-addr-of-!gdtr/idtrbits->base-addr
  (b* ((?new-x (!gdtr/idtrbits->base-addr$inline base-addr x)))
    (equal (gdtr/idtrbits->base-addr new-x)
           (64bits-fix base-addr))))

Theorem: !gdtr/idtrbits->base-addr-equiv-under-mask

(defthm !gdtr/idtrbits->base-addr-equiv-under-mask
  (b* ((?new-x (!gdtr/idtrbits->base-addr$inline base-addr x)))
    (gdtr/idtrbits-equiv-under-mask new-x x -18446744073709551616)))