Skip to main content

lemma_view_in_vaddr_range

ostd::specs::mm::page_table::cursor::owners

Function lemma_view_in_vaddr_range 

Source 
pub proof fn lemma_view_in_vaddr_range<'rcu, C: PageTableConfig>(
    owner: &CursorOwner<'rcu, C>,
)
Expand description
requires
owner.inv(),
ensures
forall |m: Mapping| {
    owner.view_mappings().contains(m)
        ==> {
            &&& vaddr_range_spec::<C>()@.start <= m.va_range.start
            &&& m.va_range.end <= vaddr_range_spec::<C>()@.end + 1

        }
},

Every mapping in a cursor’s view has its VA range within the page table’s managed range.