Type Alias OwnerSubtree 

pub type OwnerSubtree<C> = Node<EntryOwner<C>, CONST_NR_ENTRIES, CONST_INC_LEVELS>;

OwnerSubtree is a tree Node (from vstd_extra::ghost_tree) containing EntryOwners. It lives in a tree of maximum depth 5. Page table nodes can be at levels 0-3, and their entries are their children at the next level down. This means that level 4, the lowest level, can only contain frame entries as it consists of the entries of level 1 page tables.

Level correspondences: tree level 0 ==> path length 0 ==> level 4 page table tree level 1 ==> path length 1 ==> level 3 page table (the level 4 page table does not map frames directly) tree level 2 ==> path length 2 ==> level 2 page table or frame mapped by level 3 table tree level 3 ==> path length 3 ==> level 1 page table or frame mapped by level 2 table tree level 4 ==> path length 4 ==> frame mapped by level 1 table

Aliased Type

pub struct OwnerSubtree<C> {
    pub value: EntryOwner<C>,
    pub level: nat,
    pub children: Seq<Option<Node<EntryOwner<C>, 512, 5>>>,
}

Fields

value: EntryOwner<C>

level: nat

children: Seq<Option<Node<EntryOwner<C>, 512, 5>>>