Skip to main content

lemma_count_present_upto_update

ostd::specs::mm::page_table::node::owners

Function lemma_count_present_upto_update 

Source 
pub proof fn lemma_count_present_upto_update<E: PageTableEntryTrait>(
    s: Seq<E>,
    n: int,
    idx: int,
    pte: E,
)
Expand description
requires
0 <= idx < n <= s.len(),
ensures
count_present_upto(s.update(idx, pte), n)
    == count_present_upto(s, n) - (if s[idx].is_present() { 1int } else { 0int })
        + (if pte.is_present() { 1int } else { 0int }),

Updating slot idx (with idx < n) shifts the count by the change in that slot’s present-indicator.