		Search-engine friendly clone of the ACL2 documentation.

Cr4bits

Cr4bits->fsgsbase

Access the |X86ISA|::|FSGSBASE| field of a cr4bits bit structure.

Signature
(cr4bits->fsgsbase x) → fsgsbase
Arguments: x — Guard (cr4bits-p x).
Returns: fsgsbase — Type (bitp fsgsbase).

Definitions and Theorems

Function: cr4bits->fsgsbase$inline

(defun cr4bits->fsgsbase$inline (x)
  (declare (xargs :guard (cr4bits-p x)))
  (mbe :logic
       (let ((x (cr4bits-fix x)))
         (part-select x :low 16 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 10)
                               (ash (the (unsigned-byte 26) x)
                                    -16))))))

Theorem: bitp-of-cr4bits->fsgsbase

(defthm bitp-of-cr4bits->fsgsbase
  (b* ((fsgsbase (cr4bits->fsgsbase$inline x)))
    (bitp fsgsbase))
  :rule-classes :rewrite)

Theorem: cr4bits->fsgsbase$inline-of-cr4bits-fix-x

(defthm cr4bits->fsgsbase$inline-of-cr4bits-fix-x
  (equal (cr4bits->fsgsbase$inline (cr4bits-fix x))
         (cr4bits->fsgsbase$inline x)))

Theorem: cr4bits->fsgsbase$inline-cr4bits-equiv-congruence-on-x

(defthm cr4bits->fsgsbase$inline-cr4bits-equiv-congruence-on-x
  (implies (cr4bits-equiv x x-equiv)
           (equal (cr4bits->fsgsbase$inline x)
                  (cr4bits->fsgsbase$inline x-equiv)))
  :rule-classes :congruence)

Theorem: cr4bits->fsgsbase-of-cr4bits

(defthm cr4bits->fsgsbase-of-cr4bits
  (equal (cr4bits->fsgsbase
              (cr4bits vme pvi tsd
                       de pse pae mce pge pce osfxsr osxmmexcpt
                       umip la57 vmxe smxe res1 fsgsbase pcide
                       osxsave kl smep smap pke cet pks uintr))
         (bfix fsgsbase)))

Theorem: cr4bits->fsgsbase-of-write-with-mask

(defthm cr4bits->fsgsbase-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x cr4bits-equiv-under-mask)
    (cr4bits-equiv-under-mask x y fty::mask)
    (equal (logand (lognot fty::mask) 65536)
           0))
  (equal (cr4bits->fsgsbase x)
         (cr4bits->fsgsbase y))))