Skip to main content

wf_mapping_set

ostd::specs::mm::page_table::mapping_set_lemmas

Function wf_mapping_set 

Source 
pub open spec fn wf_mapping_set(s: Set<Mapping>) -> bool
Expand description
{
    &&& s.finite()
    &&& forall |m: Mapping| s.contains(m) ==> m.inv()
    &&& forall |m: Mapping, n: Mapping| {
        s.contains(m) && s.contains(n) && m != n
            ==> m.va_range.end <= n.va_range.start || n.va_range.end <= m.va_range.start
    }

}

Well-formed mapping set: finite, all inv(), pairwise VA-disjoint.