Trait PageTableConfig

Source

pub unsafe trait PageTableConfig:
    Clone
    + Debug
    + Send
    + Sync
    + 'static {
    type E: PageTableEntryTrait;
    type C: PagingConstsTrait;
    type Item: RCClone;

Show 21 methods    // Required methods
    spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize>;
    exec fn TOP_LEVEL_INDEX_RANGE() -> Range<usize>;
    exec fn TOP_LEVEL_CAN_UNMAP() -> bool;
    spec fn item_into_raw_spec(
        item: Self::Item,
    ) -> (Paddr, PagingLevel, PageProperty);
    exec fn item_into_raw(item: Self::Item) -> res : (Paddr, PagingLevel, PageProperty);
    spec fn item_from_raw_spec(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> Self::Item;
    unsafe fn item_from_raw(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> Self::Item;
    spec fn tracked(item: Self::Item) -> bool;
    spec fn item_well_formed(item: Self::Item) -> bool;
    proof fn item_from_raw_well_formed(
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    );
    proof fn clone_ensures_concrete(
        item: Self::Item,
        pa: Paddr,
        old_regions: MetaRegionOwners,
        new_regions: MetaRegionOwners,
        res: Self::Item,
    );
    proof fn item_roundtrip(
        item: Self::Item,
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    );
    proof fn clone_requires_concrete(
        item: Self::Item,
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
        regions: MetaRegionOwners,
    );
    proof fn lemma_page_table_config_constant_requirements();
    proof fn lemma_pte_size_eq_size_of();
    proof fn lemma_pte_walk_fills_page();
    proof fn lemma_pte_align_divides_size();

    // Provided methods
    open spec fn LEADING_BITS_spec() -> usize { ... }
    fn TOP_LEVEL_CAN_UNMAP_spec() -> bool { ... }
    fn LOCKED_END_BOUND_spec() -> int { ... }
    fn lemma_page_table_config_constant_properties() { ... }
}

Expand description

The configurations of a page table.

It abstracts away both the usage and the architecture specifics from the general page table implementation. For examples:

the managed virtual address range;
the trackedness of physical mappings;
the PTE layout;
the number of page table levels, etc.

§Safety

The implementor must ensure that the item_into_raw and item_from_raw are implemented correctly so that:

item_into_raw consumes the ownership of the item;
if the provided raw form matches the item that was consumed by item_into_raw, item_from_raw restores the exact item that was consumed by item_into_raw.

Required Associated Types§

Source

type Item: RCClone

The item that can be mapped into the virtual memory space using the page table.

Usually, this item is a [crate::mm::Frame], which we call a “tracked” frame. The page table can also do “untracked” mappings that only maps to certain physical addresses without tracking the ownership of the mapped physical frame. The user of the page table APIs can choose by defining this type and the corresponding methods item_into_raw and item_from_raw.

Required Methods§

Source

spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize>

Source

exec fn TOP_LEVEL_INDEX_RANGE() -> Range<usize>

returns

Self::TOP_LEVEL_INDEX_RANGE(),

The index range at the top level (C::NR_LEVELS()) page table.

When configured with this value, the PageTable instance will only be allowed to manage the virtual address range that is covered by this range. The range can be smaller than the actual allowed range specified by the hardware MMU (limited by C::ADDRESS_WIDTH).

Source

exec fn TOP_LEVEL_CAN_UNMAP() -> bool

returns

Self::TOP_LEVEL_CAN_UNMAP(),

If we can remove the top-level page table entries.

This is for the kernel page table, whose second-top-level page tables need 'static lifetime to be shared with user page tables. Other page tables do not need to set this to false.

Source

spec fn item_into_raw_spec(item: Self::Item) -> (Paddr, PagingLevel, PageProperty)

Consumes the item and returns the physical address, the paging level, and the page property.

The ownership of the item will be consumed, i.e., the item will be forgotten after this function is called.

Source

exec fn item_into_raw(item: Self::Item) -> res : (Paddr, PagingLevel, PageProperty)

ensures

1 <= res.1 <= NR_LEVELS,

res == Self::item_into_raw_spec(item),

res.0 % PAGE_SIZE == 0,

res.0 < MAX_PADDR,

res.0 % page_size(res.1) == 0,

res.0 + page_size(res.1) <= MAX_PADDR,

Source

spec fn item_from_raw_spec( paddr: Paddr, level: PagingLevel, prop: PageProperty, ) -> Self::Item

Restores the item from the physical address and the paging level.

There could be transformations after PageTableConfig::item_into_raw and before PageTableConfig::item_from_raw, which include:

splitting and coalescing the items, for example, splitting one item into 512 level - 1 items with and contiguous physical addresses;
protecting the items, for example, changing the page property.

Splitting and coalescing maintains ownership rules, i.e., if one physical address is within the range of one item, after splitting/ coalescing, there should be exactly one item that contains the address.

§Safety

The caller must ensure that:

the physical address and the paging level represent a page table item or part of it (as described above);
either the ownership of the item is properly transferred to the return value, or the return value is wrapped in a core::mem::ManuallyDrop that won’t outlive the original item.

A concrete trait implementation may require the caller to ensure that

the [super::PageFlags::AVAIL1] flag is the same as that returned from PageTableConfig::item_into_raw.

Source

unsafe exec fn item_from_raw( paddr: Paddr, level: PagingLevel, prop: PageProperty, ) -> Self::Item

returns

Self::item_from_raw_spec(paddr, level, prop),

Source

spec fn tracked(item: Self::Item) -> bool

Whether cloning this item bumps a slot’s refcount. For ref-counted items (e.g. MappedItem::Tracked), true; for items where clone is a no-op (e.g. MappedItem::Untracked for kernel MMIO frames), false.

Source

spec fn item_well_formed(item: Self::Item) -> bool

Per-config predicate that captures the structural well-formedness an item reconstructed via item_from_raw_spec must satisfy. Typically: the Frame::inv() of the tracked-frame component (if any).

KernelPtConfig defines this as match item { Tracked(f, _) => f.inv(), Untracked => true }. UserPtConfig defines it as item.frame.inv().

Source

proof fn item_from_raw_well_formed(pa: Paddr, level: PagingLevel, prop: PageProperty)

requires

has_safe_slot(pa),

ensures

Self::item_well_formed(Self::item_from_raw_spec(pa, level, prop)),

The item produced by item_from_raw_spec is structurally well-formed (see item_well_formed).

Source

proof fn clone_ensures_concrete( item: Self::Item, pa: Paddr, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, res: Self::Item, )

requires

item.clone_ensures(old_regions, new_regions, res),

Self::item_into_raw_spec(item).0 == pa,

res == item,

new_regions.inv(),

new_regions.slots =~= old_regions.slots,

new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom(),

ensures

forall |i: usize| {
    i != frame_to_index(pa)
        ==> (#[trigger] new_regions.slot_owners[i] == old_regions.slot_owners[i])
},

Self::tracked(item)
    ==> {
        &&& new_regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value()
            == old_regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value()
                + 1
        &&& new_regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.id()
            == old_regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.id()
        &&& new_regions.slot_owners[frame_to_index(pa)].inner_perms.storage
            == old_regions.slot_owners[frame_to_index(pa)].inner_perms.storage
        &&& new_regions.slot_owners[frame_to_index(pa)].inner_perms.vtable_ptr
            == old_regions.slot_owners[frame_to_index(pa)].inner_perms.vtable_ptr
        &&& new_regions.slot_owners[frame_to_index(pa)].inner_perms.in_list
            == old_regions.slot_owners[frame_to_index(pa)].inner_perms.in_list
        &&& new_regions.slot_owners[frame_to_index(pa)].paths_in_pt
            == old_regions.slot_owners[frame_to_index(pa)].paths_in_pt
        &&& new_regions.slot_owners[frame_to_index(pa)].slot_vaddr
            == old_regions.slot_owners[frame_to_index(pa)].slot_vaddr
        &&& new_regions.slot_owners[frame_to_index(pa)].usage
            == old_regions.slot_owners[frame_to_index(pa)].usage

    },

!Self::tracked(item)
    ==> new_regions.slot_owners[frame_to_index(pa)]
        == old_regions.slot_owners[frame_to_index(pa)],

Self::tracked(item)
    ==> new_regions.frame_obligations
        == old_regions.frame_obligations.insert(frame_to_index(pa)),

!Self::tracked(item) ==> new_regions.frame_obligations == old_regions.frame_obligations,

Proves that clone_ensures for Self::Item implies concrete per-field properties on MetaRegionOwners. Each PageTableConfig implementor proves this by unfolding its MappedItem::clone_ensures → Frame::clone_ensures. Proves that after clone, the slot at frame_to_index(pa) has the expected per-field properties. Implementors unfold their MappedItem::clone_ensures to Frame::clone_ensures and connect pa to the frame’s internal pointer address.

Source

proof fn item_roundtrip( item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty, )

ensures

Self::item_into_raw_spec(item) == (paddr, level, prop)
    <==> Self::item_from_raw_spec(paddr, level, prop) == item,

Source

proof fn clone_requires_concrete( item: Self::Item, pa: Paddr, level: PagingLevel, prop: PageProperty, regions: MetaRegionOwners, )

requires

regions.inv(),

Self::item_from_raw_spec(pa, level, prop) == item,

has_safe_slot(pa),

regions.slots.contains_key(frame_to_index(pa)),

regions.slot_owners.contains_key(frame_to_index(pa)),

Self::tracked(item)
    ==> regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value() > 0,

Self::tracked(item)
    ==> regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value()
        != REF_COUNT_UNUSED,

Self::tracked(item)
    ==> (regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value()
        < REF_COUNT_MAX || may_panic()),

ensures

item.clone_requires(regions),

Proves item.clone_requires(regions) from the concrete frame-slot facts delivered by metaregion_sound plus the non-saturation bound propagated from Cursor::query. Implementors unfold their MappedItem::clone_requires to Frame::clone_requires and connect pa to the frame’s internal pointer address.

Source

proof fn lemma_page_table_config_constant_requirements()

ensures

Self::TOP_LEVEL_INDEX_RANGE().start < Self::TOP_LEVEL_INDEX_RANGE().end,

Self::TOP_LEVEL_INDEX_RANGE().end
    <= pow2(
        (Self::C::ADDRESS_WIDTH()
            - pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS())) as nat,
    ),

Self::TOP_LEVEL_INDEX_RANGE().end
    * pow2(pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS()) as nat) <= usize::MAX,

Self::LEADING_BITS_spec() != 0usize
    ==> (Self::C::VA_SIGN_EXT()
        && ((Self::TOP_LEVEL_INDEX_RANGE().start
            * pow2(pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS()) as nat))
            / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1),

(Self::C::VA_SIGN_EXT()
    && (((Self::TOP_LEVEL_INDEX_RANGE().start
        * pow2(pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS()) as nat))
        / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1))
    ==> {
        &&& 48 <= Self::C::ADDRESS_WIDTH()
        &&& Self::LEADING_BITS_spec() * 0x1_0000_0000_0000int
            == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat)

    },

Self::LEADING_BITS_spec() < 0x1_0000_usize,

pow2(
    (Self::C::ADDRESS_WIDTH() - pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS()))
        as nat,
) == NR_ENTRIES,

The requirements of the page table configuration constants so that the memory management system can work correctly.

NOTE: The postcondition is designed to be minimal, to actually be used in proofs, call lemma_page_table_config_constant_properties instead to get all the properties that are derived from the requirements.

FIXME： General architecture support. Move properties only relevant to paging constants to PagingConstsTrait.

Source

proof fn lemma_pte_size_eq_size_of()

ensures

core::mem::size_of::<Self::E>() == Self::C::PTE_SIZE_spec(),

Layout identity: the PTE type’s Rust size_of matches the config’s PTE_SIZE_spec. Concrete impls satisfy this via their global layout declaration. Exposed for generic code that calls core::mem::size_of::<Self::E>().

Source

proof fn lemma_pte_walk_fills_page()

ensures

NR_ENTRIES * core::mem::size_of::<Self::E>() == PAGE_SIZE,

A full PT-node’s worth of PTEs fills exactly one base page.

Source

proof fn lemma_pte_align_divides_size()

ensures

core::mem::size_of::<Self::E>() % core::mem::align_of::<Self::E>() == 0,

core::mem::align_of::<Self::E>() > 0,

align_of::<E>() divides size_of::<E>(). True for any sized Rust type (the alignment divides the size by the layout rules), but Verus’s size_of/align_of are uninterpreted so we expose it as a proof obligation. Used by PT-node on_drop to prove cursor alignment is preserved across read_once iterations.

Provided Methods§

Source

open spec fn LEADING_BITS_spec() -> usize

{ 0 }

VERIFICATION only: The leading bits [48, 64) of every virtual address managed by this config.

Concretely, a mapping m in this page table has m.va_range.start / 2^48 == LEADING_BITS_spec(). For non-sign-extended configurations (e.g. UserPtConfig) this is 0. For x86-64 kernel PT it is 0xffff (sign-extended high half). The type is wide enough to carry arbitrary bit patterns, so the model can accommodate future configurations that place their managed range at a non-canonical fixed offset.

Combined with TOP_LEVEL_INDEX_RANGE_spec, this fully determines the managed VA range, computed as vaddr_range_bounds_spec::<Self>. Callers that previously used VADDR_RANGE_spec() should use vaddr_range_bounds_spec::<C>() directly — the inclusive (start, end_inclusive) form avoids the end == usize::MAX + 1 overflow that plagues Range<Vaddr> for sign-extended kernel configurations.

Source

open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool

{ true }

Source

open spec fn LOCKED_END_BOUND_spec() -> int

{ 0x1_0000_0000_0000_0000int }

VERIFICATION only: Upper bound on locked_range().end for cursors of this config.

May be tighter than the structural vaddr_range_bounds_spec().1 + 1 when the actual sources of cursor ranges (e.g. the kvirt allocator for KernelPtConfig) draw from a sub-window of the configured VA range. KernelPtConfig overrides this to FRAME_METADATA_BASE_VADDR, which the kvirt_alloc_range_bounds axiom enforces. This bound is what allows the cursor’s move_forward proof to discharge prefix.idx[NR_LEVELS - 1] + 1 < NR_ENTRIES at the top-level boundary — the structural bound only gives <= NR_ENTRIES for configurations whose TOP_LEVEL_INDEX_RANGE.end == NR_ENTRIES.

Default: usize::MAX + 1 (no tightening over the structural bound).

Source

proof fn lemma_page_table_config_constant_properties()

ensures

Self::TOP_LEVEL_INDEX_RANGE().end <= NR_ENTRIES,

Self::TOP_LEVEL_INDEX_RANGE().start < Self::TOP_LEVEL_INDEX_RANGE().end,

Self::TOP_LEVEL_INDEX_RANGE().end
    <= pow2(
        (Self::C::ADDRESS_WIDTH()
            - pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS())) as nat,
    ),

Self::TOP_LEVEL_INDEX_RANGE().end
    * pow2(pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS()) as nat) <= usize::MAX,

Self::LEADING_BITS_spec() != 0usize
    ==> (Self::C::VA_SIGN_EXT()
        && ((Self::TOP_LEVEL_INDEX_RANGE().start
            * pow2(pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS()) as nat))
            / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1),

(Self::C::VA_SIGN_EXT()
    && (((Self::TOP_LEVEL_INDEX_RANGE().start
        * pow2(pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS()) as nat))
        / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1))
    ==> {
        &&& 48 <= Self::C::ADDRESS_WIDTH()
        &&& Self::LEADING_BITS_spec() * 0x1_0000_0000_0000int
            == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat)

    },

Self::LEADING_BITS_spec() < 0x1_0000_usize,

pow2(
    (Self::C::ADDRESS_WIDTH() - pte_index_bit_offset::<Self::C>(Self::C::NR_LEVELS()))
        as nat,
) == NR_ENTRIES,

NOTE: Implementations of PageTableConfig do not need to implement this lemma, the proof is automatically inherited from the default implementation.

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§

Source §

Trait PageTableConfig Copy item path

§Safety

Required Associated Types§

type E: PageTableEntryTrait

type C: PagingConstsTrait

type Item: RCClone

Required Methods§

spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize>

exec fn TOP_LEVEL_INDEX_RANGE() -> Range<usize>

exec fn TOP_LEVEL_CAN_UNMAP() -> bool

spec fn item_into_raw_spec(item: Self::Item) -> (Paddr, PagingLevel, PageProperty)

exec fn item_into_raw(item: Self::Item) -> res : (Paddr, PagingLevel, PageProperty)

spec fn item_from_raw_spec( paddr: Paddr, level: PagingLevel, prop: PageProperty, ) -> Self::Item

§Safety

unsafe exec fn item_from_raw( paddr: Paddr, level: PagingLevel, prop: PageProperty, ) -> Self::Item

spec fn tracked(item: Self::Item) -> bool

spec fn item_well_formed(item: Self::Item) -> bool

proof fn item_from_raw_well_formed(pa: Paddr, level: PagingLevel, prop: PageProperty)

proof fn clone_ensures_concrete( item: Self::Item, pa: Paddr, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, res: Self::Item, )

proof fn item_roundtrip( item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty, )

proof fn clone_requires_concrete( item: Self::Item, pa: Paddr, level: PagingLevel, prop: PageProperty, regions: MetaRegionOwners, )

proof fn lemma_page_table_config_constant_requirements()

proof fn lemma_pte_size_eq_size_of()

proof fn lemma_pte_walk_fills_page()

proof fn lemma_pte_align_divides_size()

Provided Methods§

open spec fn LEADING_BITS_spec() -> usize

open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool

open spec fn LOCKED_END_BOUND_spec() -> int

proof fn lemma_page_table_config_constant_properties()

Dyn Compatibility§

Implementors§

impl PageTableConfig for UserPtConfig

type E = PageTableEntry

type C = PagingConsts

type Item = MappedItem

Trait PageTableConfig