Skip to main content

fresh_node_subtree_satisfies

ostd::specs::mm::page_table

Function fresh_node_subtree_satisfies 

Source 
pub proof fn fresh_node_subtree_satisfies<C: PageTableConfig>(
    node: OwnerSubtree<C>,
    path: TreePath<NR_ENTRIES>,
    f: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>,
)
Expand description
requires
node.inv(),
node.level() < INC_LEVELS - 1,
f(node.value(), path),
forall |i: int| 0 <= i < NR_ENTRIES ==> #[trigger] node.has_child(i),
forall |i: int, j: int| {
    0 <= i < NR_ENTRIES && 0 <= j < NR_ENTRIES ==> !#[trigger] node.child(i).has_child(j)
},
forall |i: int| {
    0 <= i < NR_ENTRIES ==> #[trigger] f(node.child(i).value(), path.push_tail(i))
},
ensures
node.subtree_satisfies(path, f),

subtree_satisfies for a freshly-allocated node grafted into the cursor: every child is a new_val-shaped node (all grandchildren None), so each child’s subtree_satisfies reduces to f at that child (lemma_new_val_subtree_satisfies). Combined with f at the root node, this discharges the whole one-level subtree. Used by alloc_if_none for the node_unlocked_except / metaregion_sound_pred / path_tracked_pred predicates over the fresh node (all of which hold trivially at the absent children).