sum_page_sizes_spec

ostd::mm::kspace::kvirt_area

Function sum_page_sizes_spec 

Source 
pub open spec fn sum_page_sizes_spec(elems: Seq<(Paddr, u8)>, from: int, to: int) -> nat
Expand description
{
    if from >= to {
        0nat
    } else {
        page_size(elems[from].1) as nat + sum_page_sizes_spec(elems, from + 1, to)
    }
}

Total size (in bytes) of the pages elems[from..to].