Function lemma_segment_cover_remove_outside

pub proof fn lemma_segment_cover_remove_outside(
    segments: Map<SegmentId, SegmentEntry>,
    sid: SegmentId,
    paddr: Paddr,
)

Expand description

requires

segments.dom().contains(sid),

segments.dom().finite(),

!(segments[sid].range.start <= paddr < segments[sid].range.end),

ensures

segment_cover_count(segments.remove(sid), paddr) == segment_cover_count(segments, paddr),

Removing an existing segment whose range does NOT cover paddr leaves segment_cover_count at paddr unchanged.

lemma_segment_cover_remove_outside