Skip to main content

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 + 1) as PagingLevel
    &&& owner.value.node.unwrap().level == level
    &&& 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
    }
    &&& forall |j: int| {
        0 <= j < NR_ENTRIES
            ==> #[trigger] owner.value.node.unwrap().children_perm.value()[j]
                == C::E::new_absent_spec()
    }

}

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

The level parameter is the NODE level (i.e., the PT level of the freshly-allocated PT itself). The entry-side parent_level is one above (level + 1). This convention is internally consistent with NodeOwner::inv (which requires 1 <= level <= NR_LEVELS) for any level in [1, NR_LEVELS-1], unlike the prior convention where alloc(1) was unsatisfiable.