Enum Child

Source

pub enum Child<C: PageTableConfig> {
    PageTable(PageTableNode<C>),
    Frame(Paddr, PagingLevel, PageProperty),
    None,
}

Expand description

A page table entry that owns the child of a page table node if present.

Variants§

§

PageTable(PageTableNode<C>)

A child page table node.

§

Frame(Paddr, PagingLevel, PageProperty)

Physical address of a mapped physical frame.

It is associated with the virtual page property and the level of the mapping node, which decides the size of the frame.

§

None

Implementations§

Source §

pub open spec fn get_node(self) -> Option<PageTableNode<C>>

{
    match self {
        Self::PageTable(node) => Some(node),
        _ => None,
    }
}

Source

pub open spec fn get_frame_tuple(self) -> Option<(Paddr, PagingLevel, PageProperty)>

{
    match self {
        Self::Frame(paddr, level, prop) => Some((paddr, level, prop)),
        _ => None,
    }
}

Source

pub exec fn is_none(&self) -> b : bool

Returns whether the child is not present.

Source §

impl<C: PageTableConfig> Child<C>

Source

pub exec fn into_pte(self) -> res : C::E

with

Tracked(owner): Tracked <& EntryOwner <C>>,
Tracked(regions): Tracked <& mut MetaRegionOwners>,

requires

owner.inv(),

old(regions).inv(),

self.wf(*owner),

ensures

regions.inv(),

res.paddr() % PAGE_SIZE() == 0,

res.paddr() < MAX_PADDR(),

owner.match_pte(res, owner.parent_level),

Source

pub exec fn from_pte(pte: C::E, level: PagingLevel) -> res : Self

with

Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(entry_own): Tracked <& EntryOwner <C>>,

requires

pte.paddr() % PAGE_SIZE() == 0,

pte.paddr() < MAX_PADDR(),

old(regions).inv(),

entry_own.inv(),

entry_own.is_node() ==> entry_own.node.unwrap().relate_region(*old(regions)),

ensures

regions.inv(),

res.wf(*entry_own),

!pte.is_present() ==> res == Child::<C>::None,

pte.is_present() && pte.is_last(level)
    ==> res == Child::<C>::from_pte_frame_spec(pte, level),

pte.is_present() && !pte.is_last(level)
    ==> res == Child::<C>::from_pte_pt_spec(pte.paddr(), *regions),

entry_own.is_node() ==> entry_own.node.unwrap().relate_region(*regions),

§Safety

The provided PTE must be the output of Self::into_pte, and the PTE:

must not be used to created a Child twice;
must not be referenced by a living ChildRef.

The level must match the original level of the child.

Source §

impl<C: PageTableConfig> Child<C>

Source

pub open spec fn into_pte_pt_spec(self, slot_own: MetaSlotOwner) -> C::E

{ C::E::new_pt_spec(meta_to_frame(slot_own.self_addr)) }

Source

pub open spec fn into_pte_frame_spec( self, tuple: (Paddr, PagingLevel, PageProperty), ) -> C::E

{
    let (paddr, level, prop) = tuple;
    C::E::new_page_spec(paddr, level, prop)
}

Source

pub open spec fn into_pte_none_spec(self) -> C::E

{ C::E::new_absent_spec() }

Source

pub open spec fn from_pte_frame_spec(pte: C::E, level: PagingLevel) -> Self

{ Self::Frame(pte.paddr(), level, pte.prop()) }

Source

pub open spec fn from_pte_pt_spec(paddr: Paddr, regions: MetaRegionOwners) -> Self

{ Self::PageTable(PageTableNode::from_raw_spec(paddr)) }

Trait Implementations§

Source §

impl<'a, C: PageTableConfig> Inv for Child<C>

Source §

open spec fn inv(self) -> bool

{ true }

Source §

impl<C: PageTableConfig> OwnerOf for Child<C>

Source §

open spec fn wf(self, owner: Self::Owner) -> bool

{
    match self {
        Self::PageTable(node) => (
            &&& owner.is_node()
            &&& node.ptr.addr() == owner.node.unwrap().meta_perm.addr()

        ),
        Self::Frame(paddr, level, prop) => (
            &&& owner.is_frame()
            &&& owner.frame.unwrap().mapped_pa == paddr
            &&& owner.frame.unwrap().prop == prop
            &&& level == owner.parent_level

        ),
        Self::None => owner.is_absent(),
    }
}

Source §