Enum ChildRef 

pub enum ChildRef<'a, C: PageTableConfig> {
    PageTable(PageTableNodeRef<'a, C>),
    Frame(Paddr, PagingLevel, PageProperty),
    None,
}

A reference to the child of a page table node.

Verification Design

If the child is itself a page table node, it is represented by a PageTableNodeRef, because a reference to it must be treated as a potentially shared reference of the appropriate lifetime. By contrast, a mapped frame can be referenced by just carrying its values, and an absent one is just a simple tag.

Variants

PageTable(PageTableNodeRef<'a, 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<'a, C: PageTableConfig> ChildRef<'a, C>

pub fn arrow_2(self) -> PageProperty

pub fn arrow_1(self) -> PagingLevel

pub fn arrow_PageTable_0(self) -> PageTableNodeRef<'a, 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> ChildRef<'_, C>

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

with

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

requires

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

level == entry_owner.parent_level,

ensures

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

final(regions).slot_owners == old(regions).slot_owners,

forall |k: int| {
    old(regions).slots.contains_key(k) ==> #[trigger]
        final(regions).slots.contains_key(k)
},

forall |k: int| {
    old(regions).slots.contains_key(k)
        ==> old(regions).slots[k] == #[trigger] final(regions).slots[k]
},

Converts a PTE to a reference 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.
• Correctness: the ChildRef is equivalent to the original PTE.
• Safety: No frame other than the target entry’s (if applicable) is impacted by the call.

Safety

• The PTE safety invariants require that the PTE was previously obtained using Self::from_pte
• The soundness of using the resulting ChildRef as a reference follows from FrameRef safety.

impl<C: PageTableConfig> ChildRef<'_, C>

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

{
    &&& owner.inv()
    &&& regions.inv()
    &&& self.wf(owner)
    &&& owner.metaregion_sound(regions)

}

Trait Implementations

impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C>

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

{
    match self {
        Self::PageTable(node) => (
            &&& owner.is_node()
            &&& node.inner@.ptr.addr() == owner.node().slot_vaddr()
            &&& node.inner@.ptr_inv()
            &&& node.inner@
                .external_meta_wf(owner.node().frame_permission.resource(), ())

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

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