Skip to main content

rebase_freshly_allocated_children

ostd::specs::mm::page_table

Function rebase_freshly_allocated_children 

Source 
pub proof fn rebase_freshly_allocated_children<C: PageTableConfig>(tracked 
    owner: &mut OwnerSubtree<C>,
    new_path: TreePath<NR_ENTRIES>,
)
Expand description
requires
old(owner).children.len() == NR_ENTRIES,
new_path.inv(),
forall |i: int| 0 <= i < NR_ENTRIES ==> (#[trigger] old(owner).children[i]) is Some,
ensures
final(owner).value == old(owner).value,
final(owner).level == old(owner).level,
final(owner).children.len() == NR_ENTRIES,
forall |i: int| {
    0 <= i < NR_ENTRIES
        ==> {
            let c_old = old(owner).children[i].unwrap();
            let c_new = (#[trigger] final(owner).children[i]).unwrap();
            &&& final(owner).children[i] is Some
            &&& c_new.value
                == EntryOwner {
                    path: new_path.push_tail(i as usize),
                    ..c_old.value
                }
            &&& c_new.level == c_old.level
            &&& c_new.children == c_old.children

        }
},

Rebases the children of a freshly-allocated PT node onto a new path.

PageTableNode::alloc produces an allocated_empty_node_owner whose value.path == empty, so its children’s paths are empty.push_tail(i) == [i]. When alloc_if_none plugs that subtree into the cursor at a non-empty path, it rewrites the parent’s path but leaves children with stale [i] paths. This helper walks the children seq and rewrites each child’s value.path to new_path.push_tail(i), producing a subtree whose pt_edge_at(_, i) clauses can be discharged.