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 exec fn into_pte(self) -> res : C::E

with

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

requires

self.invariants(*old(owner), *old(regions)),

old(owner).in_scope,

ensures

owner.pte_invariants(res, *regions),

*regions == old(owner).into_pte_regions_spec(*old(regions)),

*owner == old(owner).into_pte_owner_spec(),

old(owner).node is Some
    ==> res
        == C::E::new_pt_spec(meta_to_frame(old(owner).node.unwrap().meta_perm.addr())),

Converts the child to a raw PTE value.

§Verified Properties

§Preconditions

Safety Invariants: all safety invariants must hold on the child.
Safety: the entry’s must be marked as a child, which implies that it has a raw_count of 0.

§Postconditions

Safety Invariants: the PTE’s safety invariants are preserved.
Safety: the entry’s raw count is incremented by 1.
Safety: No frame other than the target entry’s (if applicable) is impacted by the call.
Correctness: the PTE is equivalent to the original Child.

§Safety

The PTE safety invariants ensure that the raw pointer to the entry is tracked correctly so that we can guarantee the safety condition on from_pte.

Source

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

with

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

requires

old(entry_own).pte_invariants(pte, *old(regions)),

level == old(entry_own).parent_level,

ensures

res.invariants(*entry_own, *regions),

res == Child::<C>::from_pte_spec(pte, level, *regions),

*entry_own == old(entry_own).from_pte_owner_spec(),

*regions == entry_own.from_pte_regions_spec(*old(regions)),

Converts a PTE to a Child.

§Verified Properties

§Preconditions

Safety Invariants: the PTE’s safety invariants must hold.
Safety: level must match the original level of the child.

§Postconditions

Safety Invariants: the safety invariants are preserved.
Safety: the EntryOwner is aware that it is tracking an entry in Child form.
Safety: No frame other than the target entry’s (if applicable) is impacted by the call.
Correctness: the Child is equivalent to the original PTE.

§Safety

The PTE safety invariants require that the PTE was previously obtained using Self::into_pte (or another function that calls ManuallyDrop::new, which is sufficient for safety).

Source §

impl<C: PageTableConfig> Child<C>

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 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_spec( pte: C::E, level: PagingLevel, regions: MetaRegionOwners, ) -> Self

{
    if !pte.is_present() {
        Self::None
    } else if pte.is_last(level) {
        Self::Frame(pte.paddr(), level, pte.prop())
    } else {
        Self::PageTable(PageTableNode::from_raw_spec(pte.paddr()))
    }
}

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)) }

Source

pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool

{
    &&& owner.inv()
    &&& regions.inv()
    &&& self.wf(owner)
    &&& owner.relate_region(regions)
    &&& owner.in_scope

}

Trait Implementations§

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()
            &&& node.index() == frame_to_index(meta_to_frame(node.ptr.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 §