allocated_empty_node_owner

ostd::specs::mm::page_table

Function allocated_empty_node_owner 

Source 
pub open spec fn allocated_empty_node_owner<C: PageTableConfig>(
    owner: OwnerSubtree<C>,
    level: PagingLevel,
) -> bool
Expand description
{
    &&& owner.inv()
    &&& owner.value.is_node()
    &&& owner.value.path == TreePath::<NR_ENTRIES>::new(Seq::empty())
    &&& owner.value.parent_level == level
    &&& owner.value.node.unwrap().level == level - 1
    &&& owner.value.node.unwrap().inv()
    &&& !owner
        .value
        .node
        .unwrap()
        .children_perm
        .value()
        .all(|child: C::E| child.is_present())
    &&& forall |i: int| {
        0 <= i < NR_ENTRIES
            ==> {
                &&& owner.children[i] is Some
                &&& owner.children[i].unwrap().value.is_absent()
                &&& !owner.children[i].unwrap().value.in_scope
                &&& owner.children[i].unwrap().value.inv()
                &&& owner.children[i].unwrap().value.path
                    == owner.value.path.push_tail(i as usize)

            }
    }
    &&& forall |i: int| {
        0 <= i < NR_ENTRIES
            ==> owner
                .children[i]
                .unwrap()
                .value
                .match_pte(
                    owner.value.node.unwrap().children_perm.value()[i],
                    owner.children[i].unwrap().value.parent_level,
                )
    }
    &&& forall |i: int| {
        0 <= i < NR_ENTRIES
            ==> owner.children[i].unwrap().value.parent_level
                == owner.value.node.unwrap().level
    }

}

Specifies that owner is the ghost owner of a newly allocated empty page table node at the given level. Captures the structural post-conditions of PageTableNode::alloc.