pub enum ChildRef<'a, C: PageTableConfig> {
PageTable(PageTableNodeRef<'a, C>),
Frame(Paddr, PagingLevel, PageProperty),
None,
}Expand description
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§
Source§impl<'a, C: PageTableConfig> ChildRef<'a, C>
impl<'a, C: PageTableConfig> ChildRef<'a, C>
pub fn arrow_1(self) -> PagingLevel
pub fn arrow_2(self) -> PageProperty
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
Source§impl<C: PageTableConfig> ChildRef<'_, C>
impl<C: PageTableConfig> ChildRef<'_, C>
Sourcepub exec fn from_pte(pte: &C::E, level: PagingLevel) -> res : Self
pub exec fn from_pte(pte: &C::E, level: PagingLevel) -> res : Self
with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(entry_owner): Tracked<&EntryOwner<C>>,entry_owner.pte_invariants(*pte, *old(regions)),level == entry_owner.parent_level,res.invariants(*entry_owner, *regions),*regions =~= *old(regions),Converts a PTE to a reference to a child.
§Verified Properties
§Preconditions
- Safety Invariants: the
PTE’s safety invariants must hold. - Safety:
levelmust match the original level of the child.
§Postconditions
- Safety Invariants: the safety invariants are preserved.
- Correctness: the
ChildRefis equivalent to the originalPTE. - Safety: No frame other than the target entry’s (if applicable) is impacted by the call.
§Safety
- The
PTEsafety invariants require that thePTEwas previously obtained usingSelf::from_pte - The soundness of using the resulting
ChildRefas a reference follows fromFrameRefsafety.
Source§impl<C: PageTableConfig> ChildRef<'_, C>
impl<C: PageTableConfig> ChildRef<'_, C>
Sourcepub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool
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<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C>
impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C>
Source§open spec fn wf(self, owner: Self::Owner) -> bool
open spec fn wf(self, owner: Self::Owner) -> bool
{
match self {
Self::PageTable(node) => (
&&& owner.is_node()
&&& node.inner.0.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
),
Self::None => owner.is_absent(),
}
}Source§type Owner = EntryOwner<C>
type Owner = EntryOwner<C>
The owner of the concrete type.
The Owner must implement
Inv, indicating that it must
has a consistent state.Auto Trait Implementations§
impl<'a, C> Freeze for ChildRef<'a, C>
impl<'a, C> !RefUnwindSafe for ChildRef<'a, C>
impl<'a, C> Send for ChildRef<'a, C>
impl<'a, C> Sync for ChildRef<'a, C>
impl<'a, C> Unpin for ChildRef<'a, C>where
C: Unpin,
impl<'a, C> !UnwindSafe for ChildRef<'a, C>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more