• 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
      • Booting-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
          • 8bits
          • 2bits
          • 4bits
          • 16bits
          • Paging-bitstructs
            • Ia32e-pdpte-1gb-pagebits
            • Ia32e-pde-2mb-pagebits
            • Ia32e-pte-4k-pagebits
            • Ia32e-pml4ebits
            • Ia32e-pdpte-pg-dirbits
            • Ia32e-pde-pg-tablebits
            • Ia32e-page-tablesbits
            • Ia32e-pdpte-1gb-pagebits-equiv-under-mask
            • Ia32e-pdpte-1gb-pagebits-debug
            • Ia32e-pte-4k-pagebits-equiv-under-mask
            • Ia32e-pte-4k-pagebits-debug
            • Ia32e-pml4ebits-equiv-under-mask
            • Ia32e-pdpte-pg-dirbits-equiv-under-mask
            • Ia32e-pde-pg-tablebits-equiv-under-mask
            • Ia32e-pde-2mb-pagebits-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
          • 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

Paging-bitstructs

Bitstructs related to the paging data structures

Source: Intel Manual, Dec'23, Vol. 3A, Tables 4-14 through 4-19, Figure 4-11)

Subtopics

Ia32e-pdpte-1gb-pagebits

An 64-bit unsigned bitstruct type.

Ia32e-pde-2mb-pagebits

An 64-bit unsigned bitstruct type.

Ia32e-pte-4k-pagebits

An 64-bit unsigned bitstruct type.

Ia32e-pml4ebits

An 64-bit unsigned bitstruct type.

Ia32e-pdpte-pg-dirbits

An 64-bit unsigned bitstruct type.

Ia32e-pde-pg-tablebits

An 64-bit unsigned bitstruct type.

Ia32e-page-tablesbits

An 64-bit unsigned bitstruct type.

Ia32e-pdpte-1gb-pagebits-equiv-under-mask

Ia32e-pdpte-1gb-pagebits-debug

Ia32e-pte-4k-pagebits-equiv-under-mask

Ia32e-pte-4k-pagebits-debug

Ia32e-pml4ebits-equiv-under-mask

Ia32e-pdpte-pg-dirbits-equiv-under-mask

Ia32e-pde-pg-tablebits-equiv-under-mask

Ia32e-pde-2mb-pagebits-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