Skip to main content

mappings_disjoint_vaddrs

ostd::specs::mm::page_table

Function mappings_disjoint_vaddrs 

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

Distinct mappings in the set have disjoint virtual address ranges.