		Search-engine friendly clone of the ACL2 documentation.

Cr4bits

Cr4bits->pse

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

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

Definitions and Theorems

Function: cr4bits->pse$inline

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

Theorem: bitp-of-cr4bits->pse

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

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

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

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

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

Theorem: cr4bits->pse-of-cr4bits

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

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

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