		Search-engine friendly clone of the ACL2 documentation.

Cr4bits

Cr4bits->de

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

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

Definitions and Theorems

Function: cr4bits->de$inline

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

Theorem: bitp-of-cr4bits->de

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

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

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

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

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

Theorem: cr4bits->de-of-cr4bits

(defthm cr4bits->de-of-cr4bits
 (equal
      (cr4bits->de (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 de)))

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

(defthm cr4bits->de-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) 8) 0))
  (equal (cr4bits->de x)
         (cr4bits->de y))))