ostd::specs::mm::page_table

Function fresh_node_tree_predicate_map

pub proof fn fresh_node_tree_predicate_map<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.children[i] is Some,

forall |i: int, j: int| {
    0 <= i < NR_ENTRIES && 0 <= j < NR_ENTRIES ==> #[trigger]
        node.children[i].unwrap().children[j] is None
},

forall |i: int| {
    0 <= i < NR_ENTRIES ==> #[trigger]
        f(node.children[i].unwrap().value, path.push_tail(i as usize))
},

ensures

node.tree_predicate_map(path, f),

tree_predicate_map for a freshly-allocated node grafted into the cursor: every child is a new_val-shaped node (all grandchildren None), so each child’s tree_predicate_map reduces to f at that child (new_val_tree_predicate_map). 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).

fresh_node_tree_predicate_map

Function fresh_node_tree_predicate_map Copy item path

Function fresh_node_tree_predicate_map