Skip to main content

lemma_segment_cover_contains

ostd::specs::mm::embedding

Function lemma_segment_cover_contains 

Source 
pub proof fn lemma_segment_cover_contains(
    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, paddr) >= 1,

If sid ∈ segments and segments[sid].range covers paddr, then segment_cover_count >= 1 at paddr.