Function segment_cover_count 

pub open spec fn segment_cover_count(
    segments: Map<SegmentId, SegmentEntry>,
    paddr: Paddr,
) -> nat

{
    segments
        .dom()
        .filter(|sid: SegmentId| {
            segments[sid].range.start <= paddr && paddr < segments[sid].range.end
        })
        .len()
}

Number of outstanding Segment handles covering the frame slot at paddr.