Skip to main content

mappings_disjoint_paddrs

ostd::specs::mm::page_table

Function mappings_disjoint_paddrs 

Source 
pub open spec fn mappings_disjoint_paddrs(mappings: Set<Mapping>) -> bool
Expand description
{
    forall |m: Mapping, n: Mapping| {
        mappings.contains(m) && mappings.contains(n) && m != n
            ==> Mapping::disjoint_paddrs(m, n)
    }
}

Distinct mappings in the set have disjoint physical address ranges.