		Search-engine friendly clone of the ACL2 documentation.

Cr4bits

Cr4bits->umip

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

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

Definitions and Theorems

Function: cr4bits->umip$inline

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

Theorem: bitp-of-cr4bits->umip

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

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

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

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

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

Theorem: cr4bits->umip-of-cr4bits

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

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

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