PagingConstsTrait

ostd::mm

Trait PagingConstsTrait 

Source 
pub trait PagingConstsTrait: Debug + Sync {

Show 14 methods    // Required methods
    spec fn BASE_PAGE_SIZE_spec() -> usize;
    proof fn lemma_BASE_PAGE_SIZE_properties();
    exec fn BASE_PAGE_SIZE() -> res : usize;
    spec fn NR_LEVELS_spec() -> PagingLevel;
    exec fn NR_LEVELS() -> res : PagingLevel;
    spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel;
    exec fn HIGHEST_TRANSLATION_LEVEL() -> res : PagingLevel;
    spec fn PTE_SIZE_spec() -> usize;
    exec fn PTE_SIZE() -> res : usize;
    proof fn lemma_PTE_SIZE_properties();
    spec fn ADDRESS_WIDTH_spec() -> usize;
    exec fn ADDRESS_WIDTH() -> res : usize;
    spec fn VA_SIGN_EXT_spec() -> bool;
    exec fn VA_SIGN_EXT() -> bool;

}

Required Methods§

Source

spec fn BASE_PAGE_SIZE_spec() -> usize

Source

proof fn lemma_BASE_PAGE_SIZE_properties()

ensures
0 < Self::BASE_PAGE_SIZE_spec(),
is_pow2(Self::BASE_PAGE_SIZE_spec() as int),
Source

exec fn BASE_PAGE_SIZE() -> res : usize

ensures
res == Self::BASE_PAGE_SIZE_spec(),
0 < res,
is_pow2(res as int),

The smallest page size. This is also the page size at level 1 page tables.

Source

spec fn NR_LEVELS_spec() -> PagingLevel

Source

exec fn NR_LEVELS() -> res : PagingLevel

ensures
res == Self::NR_LEVELS_spec(),
res > 0,

The number of levels in the page table. The numbering of levels goes from deepest node to the root node. For example, the level 1 to 5 on AMD64 corresponds to Page Tables, Page Directory Tables, Page Directory Pointer Tables, Page-Map Level-4 Table, and Page-Map Level-5 Table, respectively.

Source

spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel

Source

exec fn HIGHEST_TRANSLATION_LEVEL() -> res : PagingLevel

ensures
res == Self::HIGHEST_TRANSLATION_LEVEL_spec(),

The highest level that a PTE can be directly used to translate a VA. This affects the the largest page size supported by the page table.

Source

spec fn PTE_SIZE_spec() -> usize

Source

exec fn PTE_SIZE() -> res : usize

ensures
res == Self::PTE_SIZE_spec(),
is_pow2(res as int),
0 < res <= Self::BASE_PAGE_SIZE(),

The size of a PTE.

Source

proof fn lemma_PTE_SIZE_properties()

ensures
0 < Self::PTE_SIZE_spec() <= Self::BASE_PAGE_SIZE(),
is_pow2(Self::PTE_SIZE_spec() as int),
Source

spec fn ADDRESS_WIDTH_spec() -> usize

Source

exec fn ADDRESS_WIDTH() -> res : usize

ensures
res == Self::ADDRESS_WIDTH_spec(),

The address width may be BASE_PAGE_SIZE.ilog2() + NR_LEVELS * IN_FRAME_INDEX_BITS. If it is shorter than that, the higher bits in the highest level are ignored.

Source

spec fn VA_SIGN_EXT_spec() -> bool

Whether virtual addresses are sign-extended.

The sign bit of a Vaddr is the bit at index PagingConstsTrait::ADDRESS_WIDTH - 1. If this constant is true, bits in Vaddr that are higher than the sign bit must be equal to the sign bit. If an address violates this rule, both the hardware and OSTD should reject it.

Otherwise, if this constant is false, higher bits must be zero.

Regardless of sign extension, Vaddr is always not signed upon calculation. That means, 0xffff_ffff_ffff_0000 < 0xffff_ffff_ffff_0001 is true.

Source

exec fn VA_SIGN_EXT() -> bool

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§