ostd::specs::mm::page_table::node::entry_owners

Struct EntryOwner

pub struct EntryOwner<C: PageTableConfig> {
    pub node: Option<NodeOwner<C>>,
    pub frame: Option<FrameEntryOwner>,
    pub locked: Option<Ghost<Seq<FrameView<C>>>>,
    pub absent: bool,
    pub path: TreePath<CONST_NR_ENTRIES>,
    pub parent_level: PagingLevel,
}

Fields§

§node: Option<NodeOwner<C>>§frame: Option<FrameEntryOwner>§locked: Option<Ghost<Seq<FrameView<C>>>>§absent: bool§path: TreePath<CONST_NR_ENTRIES>§parent_level: PagingLevel

Implementations§

Source §

impl<C: PageTableConfig> EntryOwner<C>

Source

pub open spec fn is_node(self) -> bool

{ self.node is Some }

Source

pub open spec fn is_frame(self) -> bool

{ self.frame is Some }

Source

pub open spec fn is_locked(self) -> bool

{ self.locked is Some }

Source

pub open spec fn is_absent(self) -> bool

{ self.absent }

Source

pub open spec fn new_absent_spec(parent_level: PagingLevel) -> Self

{
    EntryOwner {
        node: None,
        frame: None,
        locked: None,
        absent: true,
        path: TreePath::new(Seq::empty()),
        parent_level,
    }
}

Source

pub open spec fn new_frame_spec( paddr: Paddr, parent_level: PagingLevel, prop: PageProperty, ) -> Self

{
    EntryOwner {
        node: None,
        frame: Some(FrameEntryOwner {
            mapped_pa: paddr,
            size: page_size(parent_level),
            prop,
        }),
        locked: None,
        absent: false,
        path: TreePath::new(Seq::empty()),
        parent_level,
    }
}

Source

pub open spec fn new_node_spec(node: NodeOwner<C>) -> Self

{
    EntryOwner {
        node: Some(node),
        frame: None,
        locked: None,
        absent: false,
        path: TreePath::new(Seq::empty()),
        parent_level: (node.level + 1) as PagingLevel,
    }
}

Source

pub proof fn new_absent(parent_level: PagingLevel) -> tracked Self

Source

pub proof fn new_frame( paddr: Paddr, parent_level: PagingLevel, prop: PageProperty, ) -> tracked Self

Source

pub proof fn new_node(node: NodeOwner<C>) -> tracked Self

Source

pub open spec fn match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool

{
    &&& pte.paddr() % PAGE_SIZE() == 0
    &&& pte.paddr() < MAX_PADDR()
    &&& !pte.is_present() ==> { self.is_absent() }
    &&& pte.is_present() && !pte.is_last(parent_level)
        ==> {
            &&& self.is_node()
            &&& meta_to_frame(self.node.unwrap().meta_perm.addr()) == pte.paddr()

        }
    &&& pte.is_present() && pte.is_last(parent_level)
        ==> {
            &&& self.is_frame()
            &&& self.frame.unwrap().mapped_pa == pte.paddr()
            &&& self.frame.unwrap().prop == pte.prop()

        }

}

Trait Implementations§

Source §

impl<C: PageTableConfig> Inv for EntryOwner<C>

Source §

open spec fn inv(self) -> bool

{
    &&& self.node is Some
        ==> {
            &&& self.frame is None
            &&& self.locked is None
            &&& self.node.unwrap().inv()
            &&& !self.absent

        }
    &&& self.frame is Some
        ==> {
            &&& self.node is None
            &&& self.locked is None
            &&& !self.absent
            &&& self.frame.unwrap().mapped_pa % PAGE_SIZE() == 0
            &&& self.frame.unwrap().mapped_pa < MAX_PADDR()

        }
    &&& self.locked is Some
        ==> {
            &&& self.frame is None
            &&& self.node is None
            &&& !self.absent

        }

}

Source §

open spec fn default(lv: nat) -> Self

{
    Self {
        path: TreePath::new(Seq::empty()),
        parent_level: (INC_LEVELS() - lv + 1) as PagingLevel,
        node: None,
        frame: None,
        locked: None,
        absent: true,
    }
}

Source §

proof fn default_preserves_inv()

Source §

open spec fn la_inv(self, lv: nat) -> bool

{ self.is_node() ==> lv < L - 1 }

Source §

proof fn default_preserves_la_inv()

Source §

open spec fn rel_children(self, child: Option<Self>) -> bool

{
    if self.is_node() {
        &&& child is Some
        &&& child.unwrap().parent_level == self.node.unwrap().level

    } else {
        &&& child is None

    }
}

Source §

proof fn default_preserves_rel_children(self, lv: nat)

Source §

impl<C: PageTableConfig> View for EntryOwner<C>

Source §

open spec fn view(&self) -> <Self as View>::V

{
    if let Some(frame) = self.frame {
        EntryView::Leaf {
            leaf: LeafPageTableEntryView {
                map_va: vaddr(self.path) as int,
                map_to_pa: frame.mapped_pa as int,
                level: (self.path.len() + 1) as u8,
                prop: frame.prop,
                phantom: PhantomData,
            },
        }
    } else if let Some(node) = self.node {
        EntryView::Intermediate {
            node: IntermediatePageTableEntryView {
                map_va: vaddr(self.path) as int,
                map_to_pa: meta_to_frame(node.meta_perm.addr()) as int,
                level: (self.path.len() + 1) as u8,
                phantom: PhantomData,
            },
        }
    } else if let Some(view) = self.locked {
        EntryView::LockedSubtree {
            views: view@,
        }
    } else {
        EntryView::Absent
    }
}