Skip to main content

allocated_empty_node_grandchildren_none

ostd::specs::mm::page_table

Function allocated_empty_node_grandchildren_none 

Source 
pub open spec fn allocated_empty_node_grandchildren_none<C: PageTableConfig>(
    owner: OwnerSubtree<C>,
) -> bool
Expand description
{
    forall |i: int, j: int| {
        0 <= i < NR_ENTRIES && 0 <= j < NR_ENTRIES ==> #[trigger]
            owner.children[i].unwrap().children[j] is None
    }
}

Grandchildren of a freshly-allocated PT node are all None. The absent children come from OwnerSubtree::new_val_tracked (see vstd_extra::ghost_tree), which initializes children = Seq::new(N, |_| None). Kept as a separate predicate (rather than folded into allocated_empty_node_owner) to avoid SMT trigger pressure at every allocated_empty_node_owner reference; threaded through PageTableNode::alloc and alloc_if_none only where it’s actually needed.