Struct UserPtConfig 

pub struct UserPtConfig {}

The configuration for user page tables.

Trait Implementations

impl Clone for UserPtConfig

fn clone(&self) -> UserPtConfig

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for UserPtConfig

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PageTableConfig for UserPtConfig

open spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize>

{ 0..256 }

open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> b : bool

{ true }

exec fn TOP_LEVEL_INDEX_RANGE() -> Range<usize>

exec fn TOP_LEVEL_CAN_UNMAP() -> b : bool

open spec fn perm_well_formed_with_region( pa: Paddr, perm: Tracked<Option<Self::Perm>>, regions: MetaRegionOwners, ) -> bool

{
    perm@ is Some
        ==> {
            let idx = crate::specs::mm::frame::mapping::frame_to_index(pa);
            let frame_perm = perm@->0;
            &&& frame_perm.0 == regions.slots[idx]
            &&& frame_perm.1.frac() == 1
            &&& frame_perm.1.id() == regions.slot_owners[idx].metadata_perm.id()
            &&& MetaSlot::perms_related(*frame_perm.0, frame_perm.1.resource())

        }
}

proof fn lemma_none_perm_well_formed(pa: Paddr, regions: MetaRegionOwners)

open spec fn item_into_raw_spec( item: Self::Item, ) -> (Paddr, PagingLevel, PageProperty, Tracked<Option<Self::Perm>>)

{
    (
        item.frame.start_paddr_spec(),
        1,
        item.prop,
        Tracked(
            Some((item.frame.tracked_slot_perm@, item.frame.tracked_metadata_perm@->0)),
        ),
    )
}

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

open spec fn item_from_raw_spec( paddr: Paddr, _level: PagingLevel, prop: PageProperty, perm: Tracked<Option<Self::Perm>>, ) -> Self::Item

{
    MappedItem {
        frame: UFrame {
            ptr: vstd::simple_pptr::PPtr(
                crate::mm::frame::meta::mapping::frame_to_meta(paddr),
                PhantomData,
            ),
            _marker: PhantomData,
            #[cfg(verus_keep_ghost_body)]
            tracked_slot_perm: Tracked((perm@->0).0),
            #[cfg(verus_keep_ghost_body)]
            tracked_metadata_perm: Tracked(Some((perm@->0).1)),
        },
        prop,
    }
}

unsafe exec fn item_from_raw( paddr: Paddr, level: PagingLevel, prop: PageProperty, Tracked(perm): Tracked<Option<Self::Perm>>, ) -> Self::Item

proof fn lemma_item_into_raw_roundtrip( pa: Paddr, level: PagingLevel, prop: PageProperty, perm: Tracked<Option<Self::Perm>>, )

proof fn lemma_item_from_raw_roundtrip( item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty, perm: Tracked<Option<Self::Perm>>, )

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

{ item.frame.inv() }

open spec fn raw_item_well_formed( item: (Paddr, PagingLevel, PageProperty, Tracked<Option<Self::Perm>>), ) -> bool

{
    let (pa, level, _prop, perm) = item;
    &&& level == 1
    &&& perm@ is Some
    &&& (perm@->0).0.addr() == crate::mm::frame::meta::mapping::frame_to_meta(pa)
    &&& (perm@->0).0.is_init()
    &&& (perm@->0).1.frac() == 1
    &&& MetaSlot::perms_related(*(perm@->0).0, (perm@->0).1.resource())

}

proof fn lemma_perm_well_formed_with_region_preserved( pa: Paddr, perm: Tracked<Option<Self::Perm>>, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, )

proof fn lemma_raw_item_well_formed_preserved( pa: Paddr, level: PagingLevel, old_prop: PageProperty, new_prop: PageProperty, perm: Tracked<Option<Self::Perm>>, )

proof fn lemma_raw_item_well_formed_split( pa: Paddr, level: PagingLevel, prop: PageProperty, child_pa: Paddr, child_idx: usize, perm: Tracked<Option<Self::Perm>>, )

proof fn lemma_huge_raw_item_untracked( pa: Paddr, level: PagingLevel, prop: PageProperty, perm: Tracked<Option<Self::Perm>>, )

proof fn lemma_item_from_raw_well_formed( pa: Paddr, level: PagingLevel, prop: PageProperty, perm: Tracked<Option<Self::Perm>>, )

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

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

proof fn lemma_page_table_config_constant_requirements()

type E = PageTableEntry

The type of the page table entry.

type C = PagingConsts

The paging constants.

type Item = MappedItem

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

type Perm = (&'static PointsTo<MetaSlot>, Count<MetadataPerm, REF_COUNT_MAX_USIZE>)

Verification-only type of the permission carried by a tracked item. An untracked item carries None in its raw representation.

fn LEADING_BITS_spec() -> usize

fn LOCKED_END_BOUND_spec() -> int

fn lemma_page_table_config_constant_properties()