Function lemma_segment_cover_remove_inside

pub proof fn lemma_segment_cover_remove_inside(
    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) - 1) as nat,

Removing an existing segment whose range covers paddr decreases segment_cover_count at paddr by exactly 1.

lemma_segment_cover_remove_inside