Enum Child 

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

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

impl<C: PageTableConfig> Child<C>

pub fn arrow_1(self) -> PagingLevel

pub fn arrow_2(self) -> PageProperty

pub fn arrow_PageTable_0(self) -> PageTableNode<C>

pub fn arrow_Frame_0(self) -> Paddr

pub fn arrow_Frame_1(self) -> PagingLevel

pub fn arrow_Frame_2(self) -> PageProperty

impl<C: PageTableConfig> Child<C>

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

with

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

requires

old(owner).inv_base(),

self.wf(*old(owner)),

self matches Child::Frame(paddr, level, prop) ==> C::E::new_page_req(paddr, level, prop),

ensures

final(owner).inv(),

final(owner).match_pte(res, final(owner).parent_level),

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

old(owner).is_node()
    ==> res == C::E::new_pt_spec(meta_to_frame(old(owner).node().slot_vaddr())),

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.

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

with

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

requires

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

level == old(entry_own).parent_level,

ensures

res.invariants(*final(entry_own), *regions),

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

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

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

impl<C: PageTableConfig> Child<C>

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(),
                regions
                    .slots[crate::specs::mm::frame::mapping::frame_to_index(
                    pte.paddr(),
                )],
                None,
            ),
        )
    }
}

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

{
    &&& owner.inv_base()
    &&& regions.inv()
    &&& self.wf(owner)
    &&& match self {
        Self::Frame(paddr, level, prop) => C::E::new_page_req(paddr, level, prop),
        _ => true,
    }
    &&& owner.metaregion_sound(regions)

}

Trait Implementations

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

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

{
    match self {
        Self::PageTable(node) => (
            &&& owner.is_node()
            &&& node.ptr.addr() == owner.node().slot_vaddr()
            &&& node.index() == meta_to_index(node.ptr.addr())
            &&& node.ptr_inv()

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

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

type Owner = EntryOwner<C>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.