Skip to main content

lemma_segment_cover_insert_inside

ostd::specs::mm::embedding

Function lemma_segment_cover_insert_inside 

Source 
pub proof fn lemma_segment_cover_insert_inside(
    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) + 1,

Inserting a fresh segment whose range DOES cover paddr bumps segment_cover_count by 1.