• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
            • Modr/m-structures
            • Vex-prefixes-layout-structures
            • Sib-structures
            • Legacy-prefixes-layout-structure
            • Evex-prefixes-layout-structures
            • Cr8bits
            • Opcode-maps-structures
            • Segmentation-bitstructs
              • System-segment-descriptorbits
              • Data-segment-descriptorbits
              • Code-segment-descriptorbits
              • Interrupt/trap-gate-descriptorbits
              • Call-gate-descriptorbits
              • Data-segment-descriptor-attributesbits
              • Code-segment-descriptor-attributesbits
              • System-segment-descriptor-attributesbits
              • Interrupt/trap-gate-descriptor-attributesbits
              • Call-gate-descriptor-attributesbits
              • Segment-selectorbits
                • !segment-selectorbits->index
                • !segment-selectorbits->rpl
                • !segment-selectorbits->ti
                • Segment-selectorbits-fix
                • Segment-selectorbits->index
                • Segment-selectorbits->ti
                • Segment-selectorbits->rpl
                  • Segment-selectorbits-p
                • Hidden-segment-registerbits
                • Gdtr/idtrbits
                • Interrupt/trap-gate-descriptor-attributesbits-equiv-under-mask
                • System-segment-descriptorbits-debug
                • System-segment-descriptor-attributesbits-equiv-under-mask
                • Interrupt/trap-gate-descriptorbits-equiv-under-mask
                • Data-segment-descriptor-attributesbits-equiv-under-mask
                • Code-segment-descriptor-attributesbits-equiv-under-mask
                • Call-gate-descriptor-attributesbits-equiv-under-mask
                • System-segment-descriptorbits-equiv-under-mask
                • Interrupt/trap-gate-descriptorbits-debug
                • Hidden-segment-registerbits-equiv-under-mask
                • Data-segment-descriptorbits-equiv-under-mask
                • Data-segment-descriptorbits-debug
                • Data-segment-descriptor-attributesbits-debug
                • Code-segment-descriptorbits-equiv-under-mask
                • Code-segment-descriptorbits-debug
                • Code-segment-descriptor-attributesbits-debug
                • Call-gate-descriptorbits-equiv-under-mask
                • System-segment-descriptor-attributesbits-debug
                • Segment-selectorbits-equiv-under-mask
                • Interrupt/trap-gate-descriptor-attributesbits-debug
                • Call-gate-descriptorbits-debug
                • Gdtr/idtrbits-equiv-under-mask
                • Call-gate-descriptor-attributesbits-debug
                • Segment-selectorbits-debug
                • Hidden-segment-registerbits-debug
                • Gdtr/idtrbits-debug
              • 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
    • Segment-selectorbits

    Segment-selectorbits->rpl

    Access the |X86ISA|::|RPL| field of a segment-selectorbits bit structure.

    Signature
    (segment-selectorbits->rpl x) → rpl
    Arguments
    x — Guard (segment-selectorbits-p x).
    Returns
    rpl — Type (2bits-p rpl).

    Definitions and Theorems

    Function: segment-selectorbits->rpl$inline

    (defun segment-selectorbits->rpl$inline (x)
      (declare (xargs :guard (segment-selectorbits-p x)))
      (mbe :logic
           (let ((x (segment-selectorbits-fix x)))
             (part-select x :low 0 :width 2))
           :exec (the (unsigned-byte 2)
                      (logand (the (unsigned-byte 2) 3)
                              (the (unsigned-byte 16) x)))))

    Theorem: 2bits-p-of-segment-selectorbits->rpl

    (defthm 2bits-p-of-segment-selectorbits->rpl
      (b* ((rpl (segment-selectorbits->rpl$inline x)))
        (2bits-p rpl))
      :rule-classes :rewrite)

    Theorem: segment-selectorbits->rpl$inline-of-segment-selectorbits-fix-x

    (defthm
         segment-selectorbits->rpl$inline-of-segment-selectorbits-fix-x
     (equal
         (segment-selectorbits->rpl$inline (segment-selectorbits-fix x))
         (segment-selectorbits->rpl$inline x)))

    Theorem: segment-selectorbits->rpl$inline-segment-selectorbits-equiv-congruence-on-x

    (defthm
     segment-selectorbits->rpl$inline-segment-selectorbits-equiv-congruence-on-x
     (implies (segment-selectorbits-equiv x x-equiv)
              (equal (segment-selectorbits->rpl$inline x)
                     (segment-selectorbits->rpl$inline x-equiv)))
     :rule-classes :congruence)

    Theorem: segment-selectorbits->rpl-of-segment-selectorbits

    (defthm segment-selectorbits->rpl-of-segment-selectorbits
     (equal
         (segment-selectorbits->rpl (segment-selectorbits rpl ti index))
         (2bits-fix rpl)))

    Theorem: segment-selectorbits->rpl-of-write-with-mask

    (defthm segment-selectorbits->rpl-of-write-with-mask
     (implies (and (fty::bitstruct-read-over-write-hyps
                        x segment-selectorbits-equiv-under-mask)
                   (segment-selectorbits-equiv-under-mask x y fty::mask)
                   (equal (logand (lognot fty::mask) 3) 0))
              (equal (segment-selectorbits->rpl x)
                     (segment-selectorbits->rpl y))))