Function lemma_mapping_set_cardinality_bound

pub proof fn lemma_mapping_set_cardinality_bound(s: Set<Mapping>, bound: usize)

Expand description

requires

wf_mapping_set(s),

forall |m: Mapping| {
    #[trigger] s.contains(m) ==> 0 <= m.va_range.start && m.va_range.end <= bound as int
},

ensures

s.len() <= bound / PAGE_SIZE,

Main lemma: A well-formed mapping set has cardinality at most bound / PAGE_SIZE, where bound is its largest element.

lemma_mapping_set_cardinality_bound