• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Introduction
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
        • Implemented-opcodes
        • Proof-utilities
        • To-do
        • Concrete-simulation-examples
        • Model-validation
        • Utils
          • Structures
            • Rflagsbits
            • Cr4bits
            • Cr0bits
            • Xcr0bits
            • 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
            • 8bits
            • 2bits
            • 4bits
            • 16bits
            • Paging-bitstructs
              • Ia32e-pdpte-1gb-pagebits
              • Ia32e-pde-2mb-pagebits
              • Ia32e-pte-4k-pagebits
              • Ia32e-pml4ebits
                • Ia32e-pml4ebits-p
                • !ia32e-pml4ebits->res3
                • !ia32e-pml4ebits->pdpt
                • !ia32e-pml4ebits->res2
                • !ia32e-pml4ebits->res1
                • !ia32e-pml4ebits->u/s
                • !ia32e-pml4ebits->r/w
                  • !ia32e-pml4ebits->pwt
                  • !ia32e-pml4ebits->pcd
                  • !ia32e-pml4ebits->xd
                  • !ia32e-pml4ebits->ps
                  • !ia32e-pml4ebits->p
                  • !ia32e-pml4ebits->a
                  • Ia32e-pml4ebits-fix
                  • Ia32e-pml4ebits->xd
                  • Ia32e-pml4ebits->res3
                  • Ia32e-pml4ebits->res2
                  • Ia32e-pml4ebits->pdpt
                  • Ia32e-pml4ebits->u/s
                  • Ia32e-pml4ebits->r/w
                  • Ia32e-pml4ebits->res1
                  • Ia32e-pml4ebits->pwt
                  • Ia32e-pml4ebits->ps
                  • Ia32e-pml4ebits->pcd
                  • Ia32e-pml4ebits->a
                  • Ia32e-pml4ebits->p
                • Ia32e-pdpte-pg-dirbits
                • Ia32e-pde-pg-tablebits
                • Ia32e-page-tablesbits
                • Ia32e-pdpte-pg-dirbits-equiv-under-mask
                • Ia32e-pdpte-1gb-pagebits-equiv-under-mask
                • Ia32e-pdpte-1gb-pagebits-debug
                • Ia32e-pde-pg-tablebits-equiv-under-mask
                • Ia32e-pde-2mb-pagebits-equiv-under-mask
                • Ia32e-pte-4k-pagebits-equiv-under-mask
                • Ia32e-pte-4k-pagebits-debug
                • Ia32e-pml4ebits-equiv-under-mask
                • Ia32e-pde-2mb-pagebits-debug
                • Ia32e-page-tablesbits-equiv-under-mask
                • Ia32e-pml4ebits-debug
                • Ia32e-pdpte-pg-dirbits-debug
                • Ia32e-pde-pg-tablebits-debug
                • Ia32e-page-tablesbits-debug
              • 3bits
              • 11bits
              • 40bits
              • 5bits
              • 32bits
              • 19bits
              • 10bits
              • 64bits
              • 7bits
              • 54bits
              • 31bits
              • 24bits
              • 22bits
              • 17bits
              • 13bits
              • 12bits
              • 6bits
              • Vex-prefixes-map-p
              • Vex-prefixes-byte0-p
              • Vex->w
              • Vex->vvvv
              • Fp-bitstructs
              • Vex->pp
              • Vex->l
              • Rflagsbits-debug
              • Evex->vl/rc
              • Evex->v-prime
              • Evex->aaa
              • Cr4bits-debug
              • Evex->z
              • Evex->w
              • Evex->vvvv
              • Evex->pp
              • Vex3-byte1-equiv-under-mask
              • Xcr0bits-equiv-under-mask
              • Xcr0bits-debug
              • Vex3-byte2-equiv-under-mask
              • Vex2-byte1-equiv-under-mask
              • Vex-prefixes-equiv-under-mask
              • Rflagsbits-equiv-under-mask
              • Prefixes-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
              • Cr8bits-equiv-under-mask
              • Cr4bits-equiv-under-mask
              • Cr3bits-equiv-under-mask
              • Cr0bits-equiv-under-mask
              • Cr0bits-debug
              • Sib-equiv-under-mask
              • Vex3-byte1-debug
              • Prefixes-debug
              • Ia32_eferbits-debug
              • Evex-prefixes-debug
              • Evex-byte3-debug
              • Evex-byte1-debug
              • Vex3-byte2-debug
              • Vex2-byte1-debug
              • Vex-prefixes-debug
              • Sib-debug
              • Evex-byte2-debug
              • Cr3bits-debug
              • Cr8bits-debug
            • Utilities
          • Debugging-code-proofs
        • Execloader
        • Axe
      • Testing-utilities
      • Math
    • Ia32e-pml4ebits

    !ia32e-pml4ebits->r/w

    Update the |X86ISA|::|R/W| field of a ia32e-pml4ebits bit structure.

    Signature
    (!ia32e-pml4ebits->r/w r/w x) → new-x
    Arguments
    r/w — Guard (bitp r/w).
    x — Guard (ia32e-pml4ebits-p x).
    Returns
    new-x — Type (ia32e-pml4ebits-p new-x).

    Definitions and Theorems

    Function: !ia32e-pml4ebits->r/w$inline

    (defun
     !ia32e-pml4ebits->r/w$inline (r/w x)
     (declare (xargs :guard (and (bitp r/w) (ia32e-pml4ebits-p x))))
     (mbe
        :logic (b* ((r/w (mbe :logic (bfix r/w) :exec r/w))
                    (x (ia32e-pml4ebits-fix x)))
                   (part-install r/w x :width 1 :low 1))
        :exec (the (unsigned-byte 64)
                   (logior (the (unsigned-byte 64)
                                (logand (the (unsigned-byte 64) x)
                                        (the (signed-byte 3) -3)))
                           (the (unsigned-byte 2)
                                (ash (the (unsigned-byte 1) r/w) 1))))))

    Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->r/w

    (defthm ia32e-pml4ebits-p-of-!ia32e-pml4ebits->r/w
            (b* ((new-x (!ia32e-pml4ebits->r/w$inline r/w x)))
                (ia32e-pml4ebits-p new-x))
            :rule-classes :rewrite)

    Theorem: !ia32e-pml4ebits->r/w$inline-of-bfix-r/w

    (defthm !ia32e-pml4ebits->r/w$inline-of-bfix-r/w
            (equal (!ia32e-pml4ebits->r/w$inline (bfix r/w)
                                                 x)
                   (!ia32e-pml4ebits->r/w$inline r/w x)))

    Theorem: !ia32e-pml4ebits->r/w$inline-bit-equiv-congruence-on-r/w

    (defthm !ia32e-pml4ebits->r/w$inline-bit-equiv-congruence-on-r/w
            (implies (bit-equiv r/w r/w-equiv)
                     (equal (!ia32e-pml4ebits->r/w$inline r/w x)
                            (!ia32e-pml4ebits->r/w$inline r/w-equiv x)))
            :rule-classes :congruence)

    Theorem: !ia32e-pml4ebits->r/w$inline-of-ia32e-pml4ebits-fix-x

    (defthm
       !ia32e-pml4ebits->r/w$inline-of-ia32e-pml4ebits-fix-x
       (equal (!ia32e-pml4ebits->r/w$inline r/w (ia32e-pml4ebits-fix x))
              (!ia32e-pml4ebits->r/w$inline r/w x)))

    Theorem: !ia32e-pml4ebits->r/w$inline-ia32e-pml4ebits-equiv-congruence-on-x

    (defthm
      !ia32e-pml4ebits->r/w$inline-ia32e-pml4ebits-equiv-congruence-on-x
      (implies (ia32e-pml4ebits-equiv x x-equiv)
               (equal (!ia32e-pml4ebits->r/w$inline r/w x)
                      (!ia32e-pml4ebits->r/w$inline r/w x-equiv)))
      :rule-classes :congruence)

    Theorem: !ia32e-pml4ebits->r/w-is-ia32e-pml4ebits

    (defthm !ia32e-pml4ebits->r/w-is-ia32e-pml4ebits
            (equal (!ia32e-pml4ebits->r/w r/w x)
                   (change-ia32e-pml4ebits x :r/w r/w)))

    Theorem: ia32e-pml4ebits->r/w-of-!ia32e-pml4ebits->r/w

    (defthm ia32e-pml4ebits->r/w-of-!ia32e-pml4ebits->r/w
            (b* ((?new-x (!ia32e-pml4ebits->r/w$inline r/w x)))
                (equal (ia32e-pml4ebits->r/w new-x)
                       (bfix r/w))))

    Theorem: !ia32e-pml4ebits->r/w-equiv-under-mask

    (defthm !ia32e-pml4ebits->r/w-equiv-under-mask
            (b* ((?new-x (!ia32e-pml4ebits->r/w$inline r/w x)))
                (ia32e-pml4ebits-equiv-under-mask new-x x -3)))