Skip to main content

rebase_freshly_allocated_children_at

ostd::specs::mm::page_table

Function rebase_freshly_allocated_children_at 

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

        }
},

Recursive worker for rebase_freshly_allocated_children. Rebases owner.children[i..NR_ENTRIES] and leaves owner.children[0..i] untouched. Verus disallows while in proof code, so the loop is expressed as tail recursion on i.