Skip to main content

lemma_segment_cover_insert_outside

ostd::specs::mm::embedding

Function lemma_segment_cover_insert_outside 

Source 
pub proof fn lemma_segment_cover_insert_outside(
    segments: Map<SegmentId, SegmentEntry>,
    sid: SegmentId,
    entry: SegmentEntry,
    paddr: Paddr,
)
Expand description
requires
!segments.dom().contains(sid),
segments.dom().finite(),
!(entry.range.start <= paddr < entry.range.end),
ensures
segment_cover_count(segments.insert(sid, entry), paddr)
    == segment_cover_count(segments, paddr),

Inserting a fresh segment whose range DOES NOT cover paddr leaves segment_cover_count(_, paddr) unchanged.