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).children[j].unwrap();
            let c_new = (#[trigger] final(owner).children[j]).unwrap();
            &&& final(owner).children[j] is Some
            &&& c_new.value
                == EntryOwner {
                    path: new_path.push_tail(j as usize),
                    ..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.