		Search-engine friendly clone of the ACL2 documentation.

Structures

Prefixes

An 52-bit unsigned bitstruct type.

This is a bitstruct type introduced by defbitstruct, represented as a unsigned 52-bit integer.

Fields

num — 4bits: Number of Prefix Bytes
lck — 8bits: Lock Prefix
rep — 8bits: Repeat Prefix
seg — 8bits: Segment Override Prefix
opr — 8bits: Operand-Size Override Prefix
adr — 8bits: Address-Size Override Prefix
nxt — 8bits: First non-prefix instruction byte

Definitions and Theorems

Function: prefixes-p$inline

(defun prefixes-p$inline (x)
  (declare (xargs :guard t))
  (mbe :logic (unsigned-byte-p 52 x)
       :exec (and (natp x) (< x 4503599627370496))))

Theorem: prefixes-p-when-unsigned-byte-p

(defthm prefixes-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 52 x)
           (prefixes-p x)))

Theorem: unsigned-byte-p-when-prefixes-p

(defthm unsigned-byte-p-when-prefixes-p
  (implies (prefixes-p x)
           (unsigned-byte-p 52 x)))

Theorem: prefixes-p-compound-recognizer

(defthm prefixes-p-compound-recognizer
  (implies (prefixes-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: prefixes-fix$inline

(defun prefixes-fix$inline (x)
  (declare (xargs :guard (prefixes-p x)))
  (mbe :logic (loghead 52 x) :exec x))

Theorem: prefixes-p-of-prefixes-fix

(defthm prefixes-p-of-prefixes-fix
  (b* ((fty::fixed (prefixes-fix$inline x)))
    (prefixes-p fty::fixed))
  :rule-classes :rewrite)

Theorem: prefixes-fix-when-prefixes-p

(defthm prefixes-fix-when-prefixes-p
  (implies (prefixes-p x)
           (equal (prefixes-fix x) x)))

Function: prefixes-equiv$inline

(defun prefixes-equiv$inline (x y)
  (declare (xargs :guard (and (prefixes-p x) (prefixes-p y))))
  (equal (prefixes-fix x)
         (prefixes-fix y)))

Theorem: prefixes-equiv-is-an-equivalence

(defthm prefixes-equiv-is-an-equivalence
  (and (booleanp (prefixes-equiv x y))
       (prefixes-equiv x x)
       (implies (prefixes-equiv x y)
                (prefixes-equiv y x))
       (implies (and (prefixes-equiv x y)
                     (prefixes-equiv y z))
                (prefixes-equiv x z)))
  :rule-classes (:equivalence))

Theorem: prefixes-equiv-implies-equal-prefixes-fix-1

(defthm prefixes-equiv-implies-equal-prefixes-fix-1
  (implies (prefixes-equiv x x-equiv)
           (equal (prefixes-fix x)
                  (prefixes-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: prefixes-fix-under-prefixes-equiv

(defthm prefixes-fix-under-prefixes-equiv
  (prefixes-equiv (prefixes-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: prefixes$inline

(defun prefixes$inline (num lck rep seg opr adr nxt)
 (declare (xargs :guard (and (4bits-p num)
                             (8bits-p lck)
                             (8bits-p rep)
                             (8bits-p seg)
                             (8bits-p opr)
                             (8bits-p adr)
                             (8bits-p nxt))))
 (b* ((num (mbe :logic (4bits-fix num) :exec num))
      (lck (mbe :logic (8bits-fix lck) :exec lck))
      (rep (mbe :logic (8bits-fix rep) :exec rep))
      (seg (mbe :logic (8bits-fix seg) :exec seg))
      (opr (mbe :logic (8bits-fix opr) :exec opr))
      (adr (mbe :logic (8bits-fix adr) :exec adr))
      (nxt (mbe :logic (8bits-fix nxt) :exec nxt)))
  (logapp
     4 num
     (logapp 8 lck
             (logapp 8 rep
                     (logapp 8 seg
                             (logapp 8 opr (logapp 8 adr nxt))))))))

Theorem: prefixes-p-of-prefixes

(defthm prefixes-p-of-prefixes
  (b* ((prefixes (prefixes$inline num lck rep seg opr adr nxt)))
    (prefixes-p prefixes))
  :rule-classes :rewrite)

Theorem: prefixes$inline-of-4bits-fix-num

(defthm prefixes$inline-of-4bits-fix-num
  (equal (prefixes$inline (4bits-fix num)
                          lck rep seg opr adr nxt)
         (prefixes$inline num lck rep seg opr adr nxt)))

Theorem: prefixes$inline-4bits-equiv-congruence-on-num

(defthm prefixes$inline-4bits-equiv-congruence-on-num
  (implies
       (4bits-equiv num num-equiv)
       (equal (prefixes$inline num lck rep seg opr adr nxt)
              (prefixes$inline num-equiv lck rep seg opr adr nxt)))
  :rule-classes :congruence)

Theorem: prefixes$inline-of-8bits-fix-lck

(defthm prefixes$inline-of-8bits-fix-lck
  (equal (prefixes$inline num (8bits-fix lck)
                          rep seg opr adr nxt)
         (prefixes$inline num lck rep seg opr adr nxt)))

Theorem: prefixes$inline-8bits-equiv-congruence-on-lck

(defthm prefixes$inline-8bits-equiv-congruence-on-lck
  (implies
       (8bits-equiv lck lck-equiv)
       (equal (prefixes$inline num lck rep seg opr adr nxt)
              (prefixes$inline num lck-equiv rep seg opr adr nxt)))
  :rule-classes :congruence)

Theorem: prefixes$inline-of-8bits-fix-rep

(defthm prefixes$inline-of-8bits-fix-rep
  (equal (prefixes$inline num lck (8bits-fix rep)
                          seg opr adr nxt)
         (prefixes$inline num lck rep seg opr adr nxt)))

Theorem: prefixes$inline-8bits-equiv-congruence-on-rep

(defthm prefixes$inline-8bits-equiv-congruence-on-rep
  (implies
       (8bits-equiv rep rep-equiv)
       (equal (prefixes$inline num lck rep seg opr adr nxt)
              (prefixes$inline num lck rep-equiv seg opr adr nxt)))
  :rule-classes :congruence)

Theorem: prefixes$inline-of-8bits-fix-seg

(defthm prefixes$inline-of-8bits-fix-seg
  (equal (prefixes$inline num lck rep (8bits-fix seg)
                          opr adr nxt)
         (prefixes$inline num lck rep seg opr adr nxt)))

Theorem: prefixes$inline-8bits-equiv-congruence-on-seg

(defthm prefixes$inline-8bits-equiv-congruence-on-seg
  (implies
       (8bits-equiv seg seg-equiv)
       (equal (prefixes$inline num lck rep seg opr adr nxt)
              (prefixes$inline num lck rep seg-equiv opr adr nxt)))
  :rule-classes :congruence)

Theorem: prefixes$inline-of-8bits-fix-opr

(defthm prefixes$inline-of-8bits-fix-opr
  (equal (prefixes$inline num lck rep seg (8bits-fix opr)
                          adr nxt)
         (prefixes$inline num lck rep seg opr adr nxt)))

Theorem: prefixes$inline-8bits-equiv-congruence-on-opr

(defthm prefixes$inline-8bits-equiv-congruence-on-opr
  (implies
       (8bits-equiv opr opr-equiv)
       (equal (prefixes$inline num lck rep seg opr adr nxt)
              (prefixes$inline num lck rep seg opr-equiv adr nxt)))
  :rule-classes :congruence)

Theorem: prefixes$inline-of-8bits-fix-adr

(defthm prefixes$inline-of-8bits-fix-adr
  (equal (prefixes$inline num lck rep seg opr (8bits-fix adr)
                          nxt)
         (prefixes$inline num lck rep seg opr adr nxt)))

Theorem: prefixes$inline-8bits-equiv-congruence-on-adr

(defthm prefixes$inline-8bits-equiv-congruence-on-adr
  (implies
       (8bits-equiv adr adr-equiv)
       (equal (prefixes$inline num lck rep seg opr adr nxt)
              (prefixes$inline num lck rep seg opr adr-equiv nxt)))
  :rule-classes :congruence)

Theorem: prefixes$inline-of-8bits-fix-nxt

(defthm prefixes$inline-of-8bits-fix-nxt
  (equal (prefixes$inline num lck rep seg opr adr (8bits-fix nxt))
         (prefixes$inline num lck rep seg opr adr nxt)))

Theorem: prefixes$inline-8bits-equiv-congruence-on-nxt

(defthm prefixes$inline-8bits-equiv-congruence-on-nxt
  (implies
       (8bits-equiv nxt nxt-equiv)
       (equal (prefixes$inline num lck rep seg opr adr nxt)
              (prefixes$inline num lck rep seg opr adr nxt-equiv)))
  :rule-classes :congruence)

Function: prefixes-equiv-under-mask$inline

(defun prefixes-equiv-under-mask$inline (x x1 mask)
  (declare (xargs :guard (and (prefixes-p x)
                              (prefixes-p x1)
                              (integerp mask))))
  (fty::int-equiv-under-mask (prefixes-fix x)
                             (prefixes-fix x1)
                             mask))

Function: prefixes->num$inline

(defun prefixes->num$inline (x)
  (declare (xargs :guard (prefixes-p x)))
  (mbe :logic
       (let ((x (prefixes-fix x)))
         (part-select x :low 0 :width 4))
       :exec (the (unsigned-byte 4)
                  (logand (the (unsigned-byte 4) 15)
                          (the (unsigned-byte 52) x)))))

Theorem: 4bits-p-of-prefixes->num

(defthm 4bits-p-of-prefixes->num
  (b* ((num (prefixes->num$inline x)))
    (4bits-p num))
  :rule-classes :rewrite)

Theorem: prefixes->num$inline-of-prefixes-fix-x

(defthm prefixes->num$inline-of-prefixes-fix-x
  (equal (prefixes->num$inline (prefixes-fix x))
         (prefixes->num$inline x)))

Theorem: prefixes->num$inline-prefixes-equiv-congruence-on-x

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

Theorem: prefixes->num-of-prefixes

(defthm prefixes->num-of-prefixes
  (equal (prefixes->num (prefixes num lck rep seg opr adr nxt))
         (4bits-fix num)))

Theorem: prefixes->num-of-write-with-mask

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

Function: prefixes->lck$inline

(defun prefixes->lck$inline (x)
 (declare (xargs :guard (prefixes-p x)))
 (mbe
    :logic
    (let ((x (prefixes-fix x)))
      (part-select x :low 4 :width 8))
    :exec (the (unsigned-byte 8)
               (logand (the (unsigned-byte 8) 255)
                       (the (unsigned-byte 48)
                            (ash (the (unsigned-byte 52) x) -4))))))

Theorem: 8bits-p-of-prefixes->lck

(defthm 8bits-p-of-prefixes->lck
  (b* ((lck (prefixes->lck$inline x)))
    (8bits-p lck))
  :rule-classes :rewrite)

Theorem: prefixes->lck$inline-of-prefixes-fix-x

(defthm prefixes->lck$inline-of-prefixes-fix-x
  (equal (prefixes->lck$inline (prefixes-fix x))
         (prefixes->lck$inline x)))

Theorem: prefixes->lck$inline-prefixes-equiv-congruence-on-x

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

Theorem: prefixes->lck-of-prefixes

(defthm prefixes->lck-of-prefixes
  (equal (prefixes->lck (prefixes num lck rep seg opr adr nxt))
         (8bits-fix lck)))

Theorem: prefixes->lck-of-write-with-mask

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

Function: prefixes->rep$inline

(defun prefixes->rep$inline (x)
  (declare (xargs :guard (prefixes-p x)))
  (mbe :logic
       (let ((x (prefixes-fix x)))
         (part-select x :low 12 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 40)
                               (ash (the (unsigned-byte 52) x)
                                    -12))))))

Theorem: 8bits-p-of-prefixes->rep

(defthm 8bits-p-of-prefixes->rep
  (b* ((rep (prefixes->rep$inline x)))
    (8bits-p rep))
  :rule-classes :rewrite)

Theorem: prefixes->rep$inline-of-prefixes-fix-x

(defthm prefixes->rep$inline-of-prefixes-fix-x
  (equal (prefixes->rep$inline (prefixes-fix x))
         (prefixes->rep$inline x)))

Theorem: prefixes->rep$inline-prefixes-equiv-congruence-on-x

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

Theorem: prefixes->rep-of-prefixes

(defthm prefixes->rep-of-prefixes
  (equal (prefixes->rep (prefixes num lck rep seg opr adr nxt))
         (8bits-fix rep)))

Theorem: prefixes->rep-of-write-with-mask

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

Function: prefixes->seg$inline

(defun prefixes->seg$inline (x)
  (declare (xargs :guard (prefixes-p x)))
  (mbe :logic
       (let ((x (prefixes-fix x)))
         (part-select x :low 20 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 32)
                               (ash (the (unsigned-byte 52) x)
                                    -20))))))

Theorem: 8bits-p-of-prefixes->seg

(defthm 8bits-p-of-prefixes->seg
  (b* ((seg (prefixes->seg$inline x)))
    (8bits-p seg))
  :rule-classes :rewrite)

Theorem: prefixes->seg$inline-of-prefixes-fix-x

(defthm prefixes->seg$inline-of-prefixes-fix-x
  (equal (prefixes->seg$inline (prefixes-fix x))
         (prefixes->seg$inline x)))

Theorem: prefixes->seg$inline-prefixes-equiv-congruence-on-x

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

Theorem: prefixes->seg-of-prefixes

(defthm prefixes->seg-of-prefixes
  (equal (prefixes->seg (prefixes num lck rep seg opr adr nxt))
         (8bits-fix seg)))

Theorem: prefixes->seg-of-write-with-mask

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

Function: prefixes->opr$inline

(defun prefixes->opr$inline (x)
  (declare (xargs :guard (prefixes-p x)))
  (mbe :logic
       (let ((x (prefixes-fix x)))
         (part-select x :low 28 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 24)
                               (ash (the (unsigned-byte 52) x)
                                    -28))))))

Theorem: 8bits-p-of-prefixes->opr

(defthm 8bits-p-of-prefixes->opr
  (b* ((opr (prefixes->opr$inline x)))
    (8bits-p opr))
  :rule-classes :rewrite)

Theorem: prefixes->opr$inline-of-prefixes-fix-x

(defthm prefixes->opr$inline-of-prefixes-fix-x
  (equal (prefixes->opr$inline (prefixes-fix x))
         (prefixes->opr$inline x)))

Theorem: prefixes->opr$inline-prefixes-equiv-congruence-on-x

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

Theorem: prefixes->opr-of-prefixes

(defthm prefixes->opr-of-prefixes
  (equal (prefixes->opr (prefixes num lck rep seg opr adr nxt))
         (8bits-fix opr)))

Theorem: prefixes->opr-of-write-with-mask

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

Function: prefixes->adr$inline

(defun prefixes->adr$inline (x)
  (declare (xargs :guard (prefixes-p x)))
  (mbe :logic
       (let ((x (prefixes-fix x)))
         (part-select x :low 36 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 16)
                               (ash (the (unsigned-byte 52) x)
                                    -36))))))

Theorem: 8bits-p-of-prefixes->adr

(defthm 8bits-p-of-prefixes->adr
  (b* ((adr (prefixes->adr$inline x)))
    (8bits-p adr))
  :rule-classes :rewrite)

Theorem: prefixes->adr$inline-of-prefixes-fix-x

(defthm prefixes->adr$inline-of-prefixes-fix-x
  (equal (prefixes->adr$inline (prefixes-fix x))
         (prefixes->adr$inline x)))

Theorem: prefixes->adr$inline-prefixes-equiv-congruence-on-x

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

Theorem: prefixes->adr-of-prefixes

(defthm prefixes->adr-of-prefixes
  (equal (prefixes->adr (prefixes num lck rep seg opr adr nxt))
         (8bits-fix adr)))

Theorem: prefixes->adr-of-write-with-mask

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

Function: prefixes->nxt$inline

(defun prefixes->nxt$inline (x)
  (declare (xargs :guard (prefixes-p x)))
  (mbe :logic
       (let ((x (prefixes-fix x)))
         (part-select x :low 44 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 8)
                               (ash (the (unsigned-byte 52) x)
                                    -44))))))

Theorem: 8bits-p-of-prefixes->nxt

(defthm 8bits-p-of-prefixes->nxt
  (b* ((nxt (prefixes->nxt$inline x)))
    (8bits-p nxt))
  :rule-classes :rewrite)

Theorem: prefixes->nxt$inline-of-prefixes-fix-x

(defthm prefixes->nxt$inline-of-prefixes-fix-x
  (equal (prefixes->nxt$inline (prefixes-fix x))
         (prefixes->nxt$inline x)))

Theorem: prefixes->nxt$inline-prefixes-equiv-congruence-on-x

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

Theorem: prefixes->nxt-of-prefixes

(defthm prefixes->nxt-of-prefixes
  (equal (prefixes->nxt (prefixes num lck rep seg opr adr nxt))
         (8bits-fix nxt)))

Theorem: prefixes->nxt-of-write-with-mask

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

Theorem: prefixes-fix-in-terms-of-prefixes

(defthm prefixes-fix-in-terms-of-prefixes
  (equal (prefixes-fix x)
         (change-prefixes x)))

Function: !prefixes->num$inline

(defun !prefixes->num$inline (num x)
  (declare (xargs :guard (and (4bits-p num) (prefixes-p x))))
  (mbe :logic
       (b* ((num (mbe :logic (4bits-fix num) :exec num))
            (x (prefixes-fix x)))
         (part-install num x :width 4 :low 0))
       :exec (the (unsigned-byte 52)
                  (logior (the (unsigned-byte 52)
                               (logand (the (unsigned-byte 52) x)
                                       (the (signed-byte 5) -16)))
                          (the (unsigned-byte 4) num)))))

Theorem: prefixes-p-of-!prefixes->num

(defthm prefixes-p-of-!prefixes->num
  (b* ((new-x (!prefixes->num$inline num x)))
    (prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !prefixes->num$inline-of-4bits-fix-num

(defthm !prefixes->num$inline-of-4bits-fix-num
  (equal (!prefixes->num$inline (4bits-fix num)
                                x)
         (!prefixes->num$inline num x)))

Theorem: !prefixes->num$inline-4bits-equiv-congruence-on-num

(defthm !prefixes->num$inline-4bits-equiv-congruence-on-num
  (implies (4bits-equiv num num-equiv)
           (equal (!prefixes->num$inline num x)
                  (!prefixes->num$inline num-equiv x)))
  :rule-classes :congruence)

Theorem: !prefixes->num$inline-of-prefixes-fix-x

(defthm !prefixes->num$inline-of-prefixes-fix-x
  (equal (!prefixes->num$inline num (prefixes-fix x))
         (!prefixes->num$inline num x)))

Theorem: !prefixes->num$inline-prefixes-equiv-congruence-on-x

(defthm !prefixes->num$inline-prefixes-equiv-congruence-on-x
  (implies (prefixes-equiv x x-equiv)
           (equal (!prefixes->num$inline num x)
                  (!prefixes->num$inline num x-equiv)))
  :rule-classes :congruence)

Theorem: !prefixes->num-is-prefixes

(defthm !prefixes->num-is-prefixes
  (equal (!prefixes->num num x)
         (change-prefixes x :num num)))

Theorem: prefixes->num-of-!prefixes->num

(defthm prefixes->num-of-!prefixes->num
  (b* ((?new-x (!prefixes->num$inline num x)))
    (equal (prefixes->num new-x)
           (4bits-fix num))))

Theorem: !prefixes->num-equiv-under-mask

(defthm !prefixes->num-equiv-under-mask
  (b* ((?new-x (!prefixes->num$inline num x)))
    (prefixes-equiv-under-mask new-x x -16)))

Function: !prefixes->lck$inline

(defun !prefixes->lck$inline (lck x)
 (declare (xargs :guard (and (8bits-p lck) (prefixes-p x))))
 (mbe
    :logic
    (b* ((lck (mbe :logic (8bits-fix lck) :exec lck))
         (x (prefixes-fix x)))
      (part-install lck x :width 8 :low 4))
    :exec (the (unsigned-byte 52)
               (logior (the (unsigned-byte 52)
                            (logand (the (unsigned-byte 52) x)
                                    (the (signed-byte 13) -4081)))
                       (the (unsigned-byte 12)
                            (ash (the (unsigned-byte 8) lck) 4))))))

Theorem: prefixes-p-of-!prefixes->lck

(defthm prefixes-p-of-!prefixes->lck
  (b* ((new-x (!prefixes->lck$inline lck x)))
    (prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !prefixes->lck$inline-of-8bits-fix-lck

(defthm !prefixes->lck$inline-of-8bits-fix-lck
  (equal (!prefixes->lck$inline (8bits-fix lck)
                                x)
         (!prefixes->lck$inline lck x)))

Theorem: !prefixes->lck$inline-8bits-equiv-congruence-on-lck

(defthm !prefixes->lck$inline-8bits-equiv-congruence-on-lck
  (implies (8bits-equiv lck lck-equiv)
           (equal (!prefixes->lck$inline lck x)
                  (!prefixes->lck$inline lck-equiv x)))
  :rule-classes :congruence)

Theorem: !prefixes->lck$inline-of-prefixes-fix-x

(defthm !prefixes->lck$inline-of-prefixes-fix-x
  (equal (!prefixes->lck$inline lck (prefixes-fix x))
         (!prefixes->lck$inline lck x)))

Theorem: !prefixes->lck$inline-prefixes-equiv-congruence-on-x

(defthm !prefixes->lck$inline-prefixes-equiv-congruence-on-x
  (implies (prefixes-equiv x x-equiv)
           (equal (!prefixes->lck$inline lck x)
                  (!prefixes->lck$inline lck x-equiv)))
  :rule-classes :congruence)

Theorem: !prefixes->lck-is-prefixes

(defthm !prefixes->lck-is-prefixes
  (equal (!prefixes->lck lck x)
         (change-prefixes x :lck lck)))

Theorem: prefixes->lck-of-!prefixes->lck

(defthm prefixes->lck-of-!prefixes->lck
  (b* ((?new-x (!prefixes->lck$inline lck x)))
    (equal (prefixes->lck new-x)
           (8bits-fix lck))))

Theorem: !prefixes->lck-equiv-under-mask

(defthm !prefixes->lck-equiv-under-mask
  (b* ((?new-x (!prefixes->lck$inline lck x)))
    (prefixes-equiv-under-mask new-x x -4081)))

Function: !prefixes->rep$inline

(defun !prefixes->rep$inline (rep x)
 (declare (xargs :guard (and (8bits-p rep) (prefixes-p x))))
 (mbe
   :logic
   (b* ((rep (mbe :logic (8bits-fix rep) :exec rep))
        (x (prefixes-fix x)))
     (part-install rep x :width 8 :low 12))
   :exec (the (unsigned-byte 52)
              (logior (the (unsigned-byte 52)
                           (logand (the (unsigned-byte 52) x)
                                   (the (signed-byte 21) -1044481)))
                      (the (unsigned-byte 20)
                           (ash (the (unsigned-byte 8) rep)
                                12))))))

Theorem: prefixes-p-of-!prefixes->rep

(defthm prefixes-p-of-!prefixes->rep
  (b* ((new-x (!prefixes->rep$inline rep x)))
    (prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !prefixes->rep$inline-of-8bits-fix-rep

(defthm !prefixes->rep$inline-of-8bits-fix-rep
  (equal (!prefixes->rep$inline (8bits-fix rep)
                                x)
         (!prefixes->rep$inline rep x)))

Theorem: !prefixes->rep$inline-8bits-equiv-congruence-on-rep

(defthm !prefixes->rep$inline-8bits-equiv-congruence-on-rep
  (implies (8bits-equiv rep rep-equiv)
           (equal (!prefixes->rep$inline rep x)
                  (!prefixes->rep$inline rep-equiv x)))
  :rule-classes :congruence)

Theorem: !prefixes->rep$inline-of-prefixes-fix-x

(defthm !prefixes->rep$inline-of-prefixes-fix-x
  (equal (!prefixes->rep$inline rep (prefixes-fix x))
         (!prefixes->rep$inline rep x)))

Theorem: !prefixes->rep$inline-prefixes-equiv-congruence-on-x

(defthm !prefixes->rep$inline-prefixes-equiv-congruence-on-x
  (implies (prefixes-equiv x x-equiv)
           (equal (!prefixes->rep$inline rep x)
                  (!prefixes->rep$inline rep x-equiv)))
  :rule-classes :congruence)

Theorem: !prefixes->rep-is-prefixes

(defthm !prefixes->rep-is-prefixes
  (equal (!prefixes->rep rep x)
         (change-prefixes x :rep rep)))

Theorem: prefixes->rep-of-!prefixes->rep

(defthm prefixes->rep-of-!prefixes->rep
  (b* ((?new-x (!prefixes->rep$inline rep x)))
    (equal (prefixes->rep new-x)
           (8bits-fix rep))))

Theorem: !prefixes->rep-equiv-under-mask

(defthm !prefixes->rep-equiv-under-mask
  (b* ((?new-x (!prefixes->rep$inline rep x)))
    (prefixes-equiv-under-mask new-x x -1044481)))

Function: !prefixes->seg$inline

(defun !prefixes->seg$inline (seg x)
  (declare (xargs :guard (and (8bits-p seg) (prefixes-p x))))
  (mbe :logic
       (b* ((seg (mbe :logic (8bits-fix seg) :exec seg))
            (x (prefixes-fix x)))
         (part-install seg x :width 8 :low 20))
       :exec
       (the (unsigned-byte 52)
            (logior (the (unsigned-byte 52)
                         (logand (the (unsigned-byte 52) x)
                                 (the (signed-byte 29) -267386881)))
                    (the (unsigned-byte 28)
                         (ash (the (unsigned-byte 8) seg)
                              20))))))

Theorem: prefixes-p-of-!prefixes->seg

(defthm prefixes-p-of-!prefixes->seg
  (b* ((new-x (!prefixes->seg$inline seg x)))
    (prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !prefixes->seg$inline-of-8bits-fix-seg

(defthm !prefixes->seg$inline-of-8bits-fix-seg
  (equal (!prefixes->seg$inline (8bits-fix seg)
                                x)
         (!prefixes->seg$inline seg x)))

Theorem: !prefixes->seg$inline-8bits-equiv-congruence-on-seg

(defthm !prefixes->seg$inline-8bits-equiv-congruence-on-seg
  (implies (8bits-equiv seg seg-equiv)
           (equal (!prefixes->seg$inline seg x)
                  (!prefixes->seg$inline seg-equiv x)))
  :rule-classes :congruence)

Theorem: !prefixes->seg$inline-of-prefixes-fix-x

(defthm !prefixes->seg$inline-of-prefixes-fix-x
  (equal (!prefixes->seg$inline seg (prefixes-fix x))
         (!prefixes->seg$inline seg x)))

Theorem: !prefixes->seg$inline-prefixes-equiv-congruence-on-x

(defthm !prefixes->seg$inline-prefixes-equiv-congruence-on-x
  (implies (prefixes-equiv x x-equiv)
           (equal (!prefixes->seg$inline seg x)
                  (!prefixes->seg$inline seg x-equiv)))
  :rule-classes :congruence)

Theorem: !prefixes->seg-is-prefixes

(defthm !prefixes->seg-is-prefixes
  (equal (!prefixes->seg seg x)
         (change-prefixes x :seg seg)))

Theorem: prefixes->seg-of-!prefixes->seg

(defthm prefixes->seg-of-!prefixes->seg
  (b* ((?new-x (!prefixes->seg$inline seg x)))
    (equal (prefixes->seg new-x)
           (8bits-fix seg))))

Theorem: !prefixes->seg-equiv-under-mask

(defthm !prefixes->seg-equiv-under-mask
  (b* ((?new-x (!prefixes->seg$inline seg x)))
    (prefixes-equiv-under-mask new-x x -267386881)))

Function: !prefixes->opr$inline

(defun !prefixes->opr$inline (opr x)
 (declare (xargs :guard (and (8bits-p opr) (prefixes-p x))))
 (mbe
     :logic
     (b* ((opr (mbe :logic (8bits-fix opr) :exec opr))
          (x (prefixes-fix x)))
       (part-install opr x :width 8 :low 28))
     :exec
     (the (unsigned-byte 52)
          (logior (the (unsigned-byte 52)
                       (logand (the (unsigned-byte 52) x)
                               (the (signed-byte 37) -68451041281)))
                  (the (unsigned-byte 36)
                       (ash (the (unsigned-byte 8) opr)
                            28))))))

Theorem: prefixes-p-of-!prefixes->opr

(defthm prefixes-p-of-!prefixes->opr
  (b* ((new-x (!prefixes->opr$inline opr x)))
    (prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !prefixes->opr$inline-of-8bits-fix-opr

(defthm !prefixes->opr$inline-of-8bits-fix-opr
  (equal (!prefixes->opr$inline (8bits-fix opr)
                                x)
         (!prefixes->opr$inline opr x)))

Theorem: !prefixes->opr$inline-8bits-equiv-congruence-on-opr

(defthm !prefixes->opr$inline-8bits-equiv-congruence-on-opr
  (implies (8bits-equiv opr opr-equiv)
           (equal (!prefixes->opr$inline opr x)
                  (!prefixes->opr$inline opr-equiv x)))
  :rule-classes :congruence)

Theorem: !prefixes->opr$inline-of-prefixes-fix-x

(defthm !prefixes->opr$inline-of-prefixes-fix-x
  (equal (!prefixes->opr$inline opr (prefixes-fix x))
         (!prefixes->opr$inline opr x)))

Theorem: !prefixes->opr$inline-prefixes-equiv-congruence-on-x

(defthm !prefixes->opr$inline-prefixes-equiv-congruence-on-x
  (implies (prefixes-equiv x x-equiv)
           (equal (!prefixes->opr$inline opr x)
                  (!prefixes->opr$inline opr x-equiv)))
  :rule-classes :congruence)

Theorem: !prefixes->opr-is-prefixes

(defthm !prefixes->opr-is-prefixes
  (equal (!prefixes->opr opr x)
         (change-prefixes x :opr opr)))

Theorem: prefixes->opr-of-!prefixes->opr

(defthm prefixes->opr-of-!prefixes->opr
  (b* ((?new-x (!prefixes->opr$inline opr x)))
    (equal (prefixes->opr new-x)
           (8bits-fix opr))))

Theorem: !prefixes->opr-equiv-under-mask

(defthm !prefixes->opr-equiv-under-mask
  (b* ((?new-x (!prefixes->opr$inline opr x)))
    (prefixes-equiv-under-mask new-x x -68451041281)))

Function: !prefixes->adr$inline

(defun !prefixes->adr$inline (adr x)
 (declare (xargs :guard (and (8bits-p adr) (prefixes-p x))))
 (mbe
  :logic
  (b* ((adr (mbe :logic (8bits-fix adr) :exec adr))
       (x (prefixes-fix x)))
    (part-install adr x :width 8 :low 36))
  :exec
  (the (unsigned-byte 52)
       (logior (the (unsigned-byte 52)
                    (logand (the (unsigned-byte 52) x)
                            (the (signed-byte 45) -17523466567681)))
               (the (unsigned-byte 44)
                    (ash (the (unsigned-byte 8) adr)
                         36))))))

Theorem: prefixes-p-of-!prefixes->adr

(defthm prefixes-p-of-!prefixes->adr
  (b* ((new-x (!prefixes->adr$inline adr x)))
    (prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !prefixes->adr$inline-of-8bits-fix-adr

(defthm !prefixes->adr$inline-of-8bits-fix-adr
  (equal (!prefixes->adr$inline (8bits-fix adr)
                                x)
         (!prefixes->adr$inline adr x)))

Theorem: !prefixes->adr$inline-8bits-equiv-congruence-on-adr

(defthm !prefixes->adr$inline-8bits-equiv-congruence-on-adr
  (implies (8bits-equiv adr adr-equiv)
           (equal (!prefixes->adr$inline adr x)
                  (!prefixes->adr$inline adr-equiv x)))
  :rule-classes :congruence)

Theorem: !prefixes->adr$inline-of-prefixes-fix-x

(defthm !prefixes->adr$inline-of-prefixes-fix-x
  (equal (!prefixes->adr$inline adr (prefixes-fix x))
         (!prefixes->adr$inline adr x)))

Theorem: !prefixes->adr$inline-prefixes-equiv-congruence-on-x

(defthm !prefixes->adr$inline-prefixes-equiv-congruence-on-x
  (implies (prefixes-equiv x x-equiv)
           (equal (!prefixes->adr$inline adr x)
                  (!prefixes->adr$inline adr x-equiv)))
  :rule-classes :congruence)

Theorem: !prefixes->adr-is-prefixes

(defthm !prefixes->adr-is-prefixes
  (equal (!prefixes->adr adr x)
         (change-prefixes x :adr adr)))

Theorem: prefixes->adr-of-!prefixes->adr

(defthm prefixes->adr-of-!prefixes->adr
  (b* ((?new-x (!prefixes->adr$inline adr x)))
    (equal (prefixes->adr new-x)
           (8bits-fix adr))))

Theorem: !prefixes->adr-equiv-under-mask

(defthm !prefixes->adr-equiv-under-mask
  (b* ((?new-x (!prefixes->adr$inline adr x)))
    (prefixes-equiv-under-mask new-x x -17523466567681)))

Function: !prefixes->nxt$inline

(defun !prefixes->nxt$inline (nxt x)
  (declare (xargs :guard (and (8bits-p nxt) (prefixes-p x))))
  (mbe :logic
       (b* ((nxt (mbe :logic (8bits-fix nxt) :exec nxt))
            (x (prefixes-fix x)))
         (part-install nxt x :width 8 :low 44))
       :exec (the (unsigned-byte 52)
                  (logior (the (unsigned-byte 52)
                               (logand (the (unsigned-byte 52) x)
                                       (the (signed-byte 53)
                                            -4486007441326081)))
                          (the (unsigned-byte 52)
                               (ash (the (unsigned-byte 8) nxt)
                                    44))))))

Theorem: prefixes-p-of-!prefixes->nxt

(defthm prefixes-p-of-!prefixes->nxt
  (b* ((new-x (!prefixes->nxt$inline nxt x)))
    (prefixes-p new-x))
  :rule-classes :rewrite)

Theorem: !prefixes->nxt$inline-of-8bits-fix-nxt

(defthm !prefixes->nxt$inline-of-8bits-fix-nxt
  (equal (!prefixes->nxt$inline (8bits-fix nxt)
                                x)
         (!prefixes->nxt$inline nxt x)))

Theorem: !prefixes->nxt$inline-8bits-equiv-congruence-on-nxt

(defthm !prefixes->nxt$inline-8bits-equiv-congruence-on-nxt
  (implies (8bits-equiv nxt nxt-equiv)
           (equal (!prefixes->nxt$inline nxt x)
                  (!prefixes->nxt$inline nxt-equiv x)))
  :rule-classes :congruence)

Theorem: !prefixes->nxt$inline-of-prefixes-fix-x

(defthm !prefixes->nxt$inline-of-prefixes-fix-x
  (equal (!prefixes->nxt$inline nxt (prefixes-fix x))
         (!prefixes->nxt$inline nxt x)))

Theorem: !prefixes->nxt$inline-prefixes-equiv-congruence-on-x

(defthm !prefixes->nxt$inline-prefixes-equiv-congruence-on-x
  (implies (prefixes-equiv x x-equiv)
           (equal (!prefixes->nxt$inline nxt x)
                  (!prefixes->nxt$inline nxt x-equiv)))
  :rule-classes :congruence)

Theorem: !prefixes->nxt-is-prefixes

(defthm !prefixes->nxt-is-prefixes
  (equal (!prefixes->nxt nxt x)
         (change-prefixes x :nxt nxt)))

Theorem: prefixes->nxt-of-!prefixes->nxt

(defthm prefixes->nxt-of-!prefixes->nxt
  (b* ((?new-x (!prefixes->nxt$inline nxt x)))
    (equal (prefixes->nxt new-x)
           (8bits-fix nxt))))

Theorem: !prefixes->nxt-equiv-under-mask

(defthm !prefixes->nxt-equiv-under-mask
  (b* ((?new-x (!prefixes->nxt$inline nxt x)))
    (prefixes-equiv-under-mask new-x x 17592186044415)))

Function: prefixes-debug$inline

(defun prefixes-debug$inline (x)
 (declare (xargs :guard (prefixes-p x)))
 (b* (((prefixes x)))
  (cons
   (cons 'num x.num)
   (cons
        (cons 'lck x.lck)
        (cons (cons 'rep x.rep)
              (cons (cons 'seg x.seg)
                    (cons (cons 'opr x.opr)
                          (cons (cons 'adr x.adr)
                                (cons (cons 'nxt x.nxt) nil)))))))))

Subtopics

Prefixes-p: Recognizer for prefixes bit structures.
!prefixes->seg: Update the |X86ISA|::|SEG| field of a prefixes bit structure.
!prefixes->rep: Update the |X86ISA|::|REP| field of a prefixes bit structure.
!prefixes->nxt: Update the |X86ISA|::|NXT| field of a prefixes bit structure.
!prefixes->opr: Update the |X86ISA|::|OPR| field of a prefixes bit structure.
!prefixes->num: Update the |X86ISA|::|NUM| field of a prefixes bit structure.
!prefixes->lck: Update the |X86ISA|::|LCK| field of a prefixes bit structure.
!prefixes->adr: Update the |X86ISA|::|ADR| field of a prefixes bit structure.
Prefixes->seg: Access the |X86ISA|::|SEG| field of a prefixes bit structure.
Prefixes->rep: Access the |X86ISA|::|REP| field of a prefixes bit structure.
Prefixes->opr: Access the |X86ISA|::|OPR| field of a prefixes bit structure.
Prefixes->nxt: Access the |X86ISA|::|NXT| field of a prefixes bit structure.
Prefixes->lck: Access the |X86ISA|::|LCK| field of a prefixes bit structure.
Prefixes->adr: Access the |X86ISA|::|ADR| field of a prefixes bit structure.
Prefixes-fix: Fixing function for prefixes bit structures.
Prefixes->num: Access the |X86ISA|::|NUM| field of a prefixes bit structure.