Skip to main content

lemma_segment_cover_witness

ostd::specs::mm::embedding

Function lemma_segment_cover_witness 

Source 
pub proof fn lemma_segment_cover_witness(
    segments: Map<SegmentId, SegmentEntry>,
    paddr: Paddr,
) -> sid : SegmentId
Expand description
requires
segment_cover_count(segments, paddr) > 0,
ensures
segments.dom().contains(sid),
segments[sid].range.start <= paddr < segments[sid].range.end,

A positive segment-cover count exhibits a witnessing segment id whose range covers paddr. Used to lift segment_cover_count(..) > 0 into the structural covered ⟹ usage == Frame clause (which is keyed by a concrete (sid, paddr)), replacing the retired raw_count cache.