		Search-engine friendly clone of the ACL2 documentation.

Sib-structures

Bitstruct definitions to store a SIB byte and its fields.

Definitions and Theorems

Function: sib-p$inline

(defun sib-p$inline (x)
  (declare (xargs :guard t))
  (mbe :logic (unsigned-byte-p 8 x)
       :exec (and (natp x) (< x 256))))

Theorem: sib-p-when-unsigned-byte-p

(defthm sib-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 8 x)
           (sib-p x)))

Theorem: unsigned-byte-p-when-sib-p

(defthm unsigned-byte-p-when-sib-p
  (implies (sib-p x)
           (unsigned-byte-p 8 x)))

Theorem: sib-p-compound-recognizer

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

Function: sib-fix$inline

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

Theorem: sib-p-of-sib-fix

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

Theorem: sib-fix-when-sib-p

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

Function: sib-equiv$inline

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

Theorem: sib-equiv-is-an-equivalence

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

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

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

Theorem: sib-fix-under-sib-equiv

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

Function: sib$inline

(defun sib$inline (base index scale)
  (declare (xargs :guard (and (3bits-p base)
                              (3bits-p index)
                              (2bits-p scale))))
  (b* ((base (mbe :logic (3bits-fix base)
                  :exec base))
       (index (mbe :logic (3bits-fix index)
                   :exec index))
       (scale (mbe :logic (2bits-fix scale)
                   :exec scale)))
    (logapp 3 base (logapp 3 index scale))))

Theorem: sib-p-of-sib

(defthm sib-p-of-sib
  (b* ((sib (sib$inline base index scale)))
    (sib-p sib))
  :rule-classes :rewrite)

Theorem: sib$inline-of-3bits-fix-base

(defthm sib$inline-of-3bits-fix-base
  (equal (sib$inline (3bits-fix base)
                     index scale)
         (sib$inline base index scale)))

Theorem: sib$inline-3bits-equiv-congruence-on-base

(defthm sib$inline-3bits-equiv-congruence-on-base
  (implies (3bits-equiv base base-equiv)
           (equal (sib$inline base index scale)
                  (sib$inline base-equiv index scale)))
  :rule-classes :congruence)

Theorem: sib$inline-of-3bits-fix-index

(defthm sib$inline-of-3bits-fix-index
  (equal (sib$inline base (3bits-fix index)
                     scale)
         (sib$inline base index scale)))

Theorem: sib$inline-3bits-equiv-congruence-on-index

(defthm sib$inline-3bits-equiv-congruence-on-index
  (implies (3bits-equiv index index-equiv)
           (equal (sib$inline base index scale)
                  (sib$inline base index-equiv scale)))
  :rule-classes :congruence)

Theorem: sib$inline-of-2bits-fix-scale

(defthm sib$inline-of-2bits-fix-scale
  (equal (sib$inline base index (2bits-fix scale))
         (sib$inline base index scale)))

Theorem: sib$inline-2bits-equiv-congruence-on-scale

(defthm sib$inline-2bits-equiv-congruence-on-scale
  (implies (2bits-equiv scale scale-equiv)
           (equal (sib$inline base index scale)
                  (sib$inline base index scale-equiv)))
  :rule-classes :congruence)

Function: sib-equiv-under-mask$inline

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

Function: sib->base$inline

(defun sib->base$inline (x)
  (declare (xargs :guard (sib-p x)))
  (mbe :logic
       (let ((x (sib-fix x)))
         (part-select x :low 0 :width 3))
       :exec (the (unsigned-byte 3)
                  (logand (the (unsigned-byte 3) 7)
                          (the (unsigned-byte 8) x)))))

Theorem: 3bits-p-of-sib->base

(defthm 3bits-p-of-sib->base
  (b* ((base (sib->base$inline x)))
    (3bits-p base))
  :rule-classes :rewrite)

Theorem: sib->base$inline-of-sib-fix-x

(defthm sib->base$inline-of-sib-fix-x
  (equal (sib->base$inline (sib-fix x))
         (sib->base$inline x)))

Theorem: sib->base$inline-sib-equiv-congruence-on-x

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

Theorem: sib->base-of-sib

(defthm sib->base-of-sib
  (equal (sib->base (sib base index scale))
         (3bits-fix base)))

Theorem: sib->base-of-write-with-mask

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

Function: sib->index$inline

(defun sib->index$inline (x)
 (declare (xargs :guard (sib-p x)))
 (mbe
     :logic
     (let ((x (sib-fix x)))
       (part-select x :low 3 :width 3))
     :exec (the (unsigned-byte 3)
                (logand (the (unsigned-byte 3) 7)
                        (the (unsigned-byte 5)
                             (ash (the (unsigned-byte 8) x) -3))))))

Theorem: 3bits-p-of-sib->index

(defthm 3bits-p-of-sib->index
  (b* ((index (sib->index$inline x)))
    (3bits-p index))
  :rule-classes :rewrite)

Theorem: sib->index$inline-of-sib-fix-x

(defthm sib->index$inline-of-sib-fix-x
  (equal (sib->index$inline (sib-fix x))
         (sib->index$inline x)))

Theorem: sib->index$inline-sib-equiv-congruence-on-x

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

Theorem: sib->index-of-sib

(defthm sib->index-of-sib
  (equal (sib->index (sib base index scale))
         (3bits-fix index)))

Theorem: sib->index-of-write-with-mask

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

Function: sib->scale$inline

(defun sib->scale$inline (x)
 (declare (xargs :guard (sib-p x)))
 (mbe
     :logic
     (let ((x (sib-fix x)))
       (part-select x :low 6 :width 2))
     :exec (the (unsigned-byte 2)
                (logand (the (unsigned-byte 2) 3)
                        (the (unsigned-byte 2)
                             (ash (the (unsigned-byte 8) x) -6))))))

Theorem: 2bits-p-of-sib->scale

(defthm 2bits-p-of-sib->scale
  (b* ((scale (sib->scale$inline x)))
    (2bits-p scale))
  :rule-classes :rewrite)

Theorem: sib->scale$inline-of-sib-fix-x

(defthm sib->scale$inline-of-sib-fix-x
  (equal (sib->scale$inline (sib-fix x))
         (sib->scale$inline x)))

Theorem: sib->scale$inline-sib-equiv-congruence-on-x

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

Theorem: sib->scale-of-sib

(defthm sib->scale-of-sib
  (equal (sib->scale (sib base index scale))
         (2bits-fix scale)))

Theorem: sib->scale-of-write-with-mask

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

Theorem: sib-fix-in-terms-of-sib

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

Function: !sib->base$inline

(defun !sib->base$inline (base x)
  (declare (xargs :guard (and (3bits-p base) (sib-p x))))
  (mbe :logic
       (b* ((base (mbe :logic (3bits-fix base)
                       :exec base))
            (x (sib-fix x)))
         (part-install base x :width 3 :low 0))
       :exec (the (unsigned-byte 8)
                  (logior (the (unsigned-byte 8)
                               (logand (the (unsigned-byte 8) x)
                                       (the (signed-byte 4) -8)))
                          (the (unsigned-byte 3) base)))))

Theorem: sib-p-of-!sib->base

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

Theorem: !sib->base$inline-of-3bits-fix-base

(defthm !sib->base$inline-of-3bits-fix-base
  (equal (!sib->base$inline (3bits-fix base) x)
         (!sib->base$inline base x)))

Theorem: !sib->base$inline-3bits-equiv-congruence-on-base

(defthm !sib->base$inline-3bits-equiv-congruence-on-base
  (implies (3bits-equiv base base-equiv)
           (equal (!sib->base$inline base x)
                  (!sib->base$inline base-equiv x)))
  :rule-classes :congruence)

Theorem: !sib->base$inline-of-sib-fix-x

(defthm !sib->base$inline-of-sib-fix-x
  (equal (!sib->base$inline base (sib-fix x))
         (!sib->base$inline base x)))

Theorem: !sib->base$inline-sib-equiv-congruence-on-x

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

Theorem: !sib->base-is-sib

(defthm !sib->base-is-sib
  (equal (!sib->base base x)
         (change-sib x :base base)))

Theorem: sib->base-of-!sib->base

(defthm sib->base-of-!sib->base
  (b* ((?new-x (!sib->base$inline base x)))
    (equal (sib->base new-x)
           (3bits-fix base))))

Theorem: !sib->base-equiv-under-mask

(defthm !sib->base-equiv-under-mask
  (b* ((?new-x (!sib->base$inline base x)))
    (sib-equiv-under-mask new-x x -8)))

Function: !sib->index$inline

(defun !sib->index$inline (index x)
  (declare (xargs :guard (and (3bits-p index) (sib-p x))))
  (mbe :logic
       (b* ((index (mbe :logic (3bits-fix index)
                        :exec index))
            (x (sib-fix x)))
         (part-install index x :width 3 :low 3))
       :exec (the (unsigned-byte 8)
                  (logior (the (unsigned-byte 8)
                               (logand (the (unsigned-byte 8) x)
                                       (the (signed-byte 7) -57)))
                          (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 3) index)
                                    3))))))

Theorem: sib-p-of-!sib->index

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

Theorem: !sib->index$inline-of-3bits-fix-index

(defthm !sib->index$inline-of-3bits-fix-index
  (equal (!sib->index$inline (3bits-fix index) x)
         (!sib->index$inline index x)))

Theorem: !sib->index$inline-3bits-equiv-congruence-on-index

(defthm !sib->index$inline-3bits-equiv-congruence-on-index
  (implies (3bits-equiv index index-equiv)
           (equal (!sib->index$inline index x)
                  (!sib->index$inline index-equiv x)))
  :rule-classes :congruence)

Theorem: !sib->index$inline-of-sib-fix-x

(defthm !sib->index$inline-of-sib-fix-x
  (equal (!sib->index$inline index (sib-fix x))
         (!sib->index$inline index x)))

Theorem: !sib->index$inline-sib-equiv-congruence-on-x

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

Theorem: !sib->index-is-sib

(defthm !sib->index-is-sib
  (equal (!sib->index index x)
         (change-sib x :index index)))

Theorem: sib->index-of-!sib->index

(defthm sib->index-of-!sib->index
  (b* ((?new-x (!sib->index$inline index x)))
    (equal (sib->index new-x)
           (3bits-fix index))))

Theorem: !sib->index-equiv-under-mask

(defthm !sib->index-equiv-under-mask
  (b* ((?new-x (!sib->index$inline index x)))
    (sib-equiv-under-mask new-x x -57)))

Function: !sib->scale$inline

(defun !sib->scale$inline (scale x)
  (declare (xargs :guard (and (2bits-p scale) (sib-p x))))
  (mbe :logic
       (b* ((scale (mbe :logic (2bits-fix scale)
                        :exec scale))
            (x (sib-fix x)))
         (part-install scale x :width 2 :low 6))
       :exec (the (unsigned-byte 8)
                  (logior (the (unsigned-byte 8)
                               (logand (the (unsigned-byte 8) x)
                                       (the (signed-byte 9) -193)))
                          (the (unsigned-byte 8)
                               (ash (the (unsigned-byte 2) scale)
                                    6))))))

Theorem: sib-p-of-!sib->scale

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

Theorem: !sib->scale$inline-of-2bits-fix-scale

(defthm !sib->scale$inline-of-2bits-fix-scale
  (equal (!sib->scale$inline (2bits-fix scale) x)
         (!sib->scale$inline scale x)))

Theorem: !sib->scale$inline-2bits-equiv-congruence-on-scale

(defthm !sib->scale$inline-2bits-equiv-congruence-on-scale
  (implies (2bits-equiv scale scale-equiv)
           (equal (!sib->scale$inline scale x)
                  (!sib->scale$inline scale-equiv x)))
  :rule-classes :congruence)

Theorem: !sib->scale$inline-of-sib-fix-x

(defthm !sib->scale$inline-of-sib-fix-x
  (equal (!sib->scale$inline scale (sib-fix x))
         (!sib->scale$inline scale x)))

Theorem: !sib->scale$inline-sib-equiv-congruence-on-x

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

Theorem: !sib->scale-is-sib

(defthm !sib->scale-is-sib
  (equal (!sib->scale scale x)
         (change-sib x :scale scale)))

Theorem: sib->scale-of-!sib->scale

(defthm sib->scale-of-!sib->scale
  (b* ((?new-x (!sib->scale$inline scale x)))
    (equal (sib->scale new-x)
           (2bits-fix scale))))

Theorem: !sib->scale-equiv-under-mask

(defthm !sib->scale-equiv-under-mask
  (b* ((?new-x (!sib->scale$inline scale x)))
    (sib-equiv-under-mask new-x x 63)))

Function: sib-debug$inline

(defun sib-debug$inline (x)
  (declare (xargs :guard (sib-p x)))
  (b* (((sib x)))
    (cons (cons 'base x.base)
          (cons (cons 'index x.index)
                (cons (cons 'scale x.scale) nil)))))

Theorem: return-type-of-sib->base-linear

(defthm return-type-of-sib->base-linear
  (< (sib->base sib) 8)
  :rule-classes :linear)

Theorem: return-type-of-sib->index-linear

(defthm return-type-of-sib->index-linear
  (< (sib->index sib) 8)
  :rule-classes :linear)

Theorem: return-type-of-sib->scale-linear

(defthm return-type-of-sib->scale-linear
  (< (sib->scale sib) 4)
  :rule-classes :linear)