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().level == level
    &&& owner.level() == (INC_LEVELS - level - 1) as nat
    &&& owner.value().node().inv()
    &&& !owner.value().node().children_perm.value().all(|child: C::E| child.is_present())
    &&& forall |i: int| {
        0 <= i < NR_ENTRIES
            ==> {
                &&& #[trigger] owner.has_child(i)
                &&& owner.child(i).value().is_absent()
                &&& owner.child(i).value().inv()
                &&& owner.child(i).value().path == owner.value().path.push_tail(i)

            }
    }
    &&& forall |i: int| {
        0 <= i < NR_ENTRIES
            ==> owner
                .child(i)
                .value()
                .match_pte(
                    owner.value().node().children_perm.value()[i],
                    owner.child(i).value().parent_level,
                )
    }
    &&& forall |i: int| {
        0 <= i < NR_ENTRIES
            ==> owner.child(i).value().parent_level == owner.value().node().level
    }
    &&& forall |j: int| {
        0 <= j < NR_ENTRIES
            ==> #[trigger] owner.value().node().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.