		Search-engine friendly clone of the ACL2 documentation.

Cr4bits

Cr4bits->smap

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

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

Definitions and Theorems

Function: cr4bits->smap$inline

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

Theorem: bitp-of-cr4bits->smap

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

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

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

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

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

Theorem: cr4bits->smap-of-cr4bits

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

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

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