• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
        • Structures
          • Rflagsbits
          • Cr4bits
          • Xcr0bits
          • Cr0bits
          • Prefixes
          • Ia32_eferbits
          • Evex-byte1
          • Cr3bits
          • Evex-byte3
          • Vex3-byte2
          • Vex3-byte1
          • Vex2-byte1
          • Evex-prefixes
          • Evex-byte2
          • Vex-prefixes
          • Sib
            • !sib->scale
            • !sib->index
            • !sib->base
            • Sib-p
            • Sib->scale
            • Sib->index
            • Sib->base
            • Sib-fix
          • Modr/m-structures
          • Vex-prefixes-layout-structures
          • Sib-structures
          • Legacy-prefixes-layout-structure
          • Evex-prefixes-layout-structures
          • Cr8bits
          • Opcode-maps-structures
          • Segmentation-bitstructs
          • 8bits
          • 2bits
          • 4bits
          • 16bits
          • Paging-bitstructs
          • 3bits
          • 11bits
          • 40bits
          • 5bits
          • 32bits
          • 19bits
          • 10bits
          • 7bits
          • 64bits
          • 54bits
          • 45bits
          • 36bits
          • 31bits
          • 24bits
          • 22bits
          • 17bits
          • 13bits
          • 12bits
          • 6bits
          • Vex->x
          • Vex->b
          • Vex-prefixes-map-p
          • Vex-prefixes-byte0-p
          • Vex->w
          • Vex->vvvv
          • Vex->r
          • Fp-bitstructs
          • Cr4bits-debug
          • Vex->pp
          • Vex->l
          • Rflagsbits-debug
          • Evex->v-prime
          • Evex->z
          • Evex->w
          • Evex->vvvv
          • Evex->vl/rc
          • Evex->pp
          • Evex->aaa
          • Xcr0bits-debug
          • Vex3-byte1-equiv-under-mask
          • Vex3-byte2-equiv-under-mask
          • Vex2-byte1-equiv-under-mask
          • Vex-prefixes-equiv-under-mask
          • Rflagsbits-equiv-under-mask
          • Ia32_eferbits-equiv-under-mask
          • Evex-prefixes-equiv-under-mask
          • Evex-byte3-equiv-under-mask
          • Evex-byte2-equiv-under-mask
          • Evex-byte1-equiv-under-mask
          • Cr0bits-debug
          • Xcr0bits-equiv-under-mask
          • Sib-equiv-under-mask
          • Prefixes-equiv-under-mask
          • Cr8bits-equiv-under-mask
          • Cr4bits-equiv-under-mask
          • Cr3bits-equiv-under-mask
          • Cr0bits-equiv-under-mask
          • Vex3-byte1-debug
          • Prefixes-debug
          • Ia32_eferbits-debug
          • Evex-byte1-debug
          • Vex3-byte2-debug
          • Vex2-byte1-debug
          • Vex-prefixes-debug
          • Evex-prefixes-debug
          • Evex-byte3-debug
          • Evex-byte2-debug
          • Cr3bits-debug
          • Sib-debug
          • Cr8bits-debug
        • Utilities
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Structures

Sib

An 8-bit unsigned bitstruct type.

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

Fields

base — 3bits

index — 3bits

scale — 2bits

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)))))

Subtopics

!sib->scale

Update the |X86ISA|::|SCALE| field of a sib bit structure.

!sib->index

Update the |X86ISA|::|INDEX| field of a sib bit structure.

!sib->base

Update the |X86ISA|::|BASE| field of a sib bit structure.

Sib-p

Recognizer for sib bit structures.

Sib->scale

Access the |X86ISA|::|SCALE| field of a sib bit structure.

Sib->index

Access the |X86ISA|::|INDEX| field of a sib bit structure.

Sib->base

Access the |X86ISA|::|BASE| field of a sib bit structure.

Sib-fix

Fixing function for sib bit structures.