Skip to main content

lemma_segment_cover_shrink_front

ostd::specs::mm::embedding

Function lemma_segment_cover_shrink_front 

Source 
pub proof fn lemma_segment_cover_shrink_front(
    segments: Map<SegmentId, SegmentEntry>,
    sid: SegmentId,
    new_entry: SegmentEntry,
    paddr_check: Paddr,
)
Expand description
requires
segments.dom().contains(sid),
segments.dom().finite(),
segments[sid].range.start < segments[sid].range.end,
segments[sid].range.start % PAGE_SIZE == 0,
segments[sid].range.start + PAGE_SIZE <= MAX_PADDR,
new_entry.range.start == (segments[sid].range.start + PAGE_SIZE) as Paddr,
new_entry.range.end == segments[sid].range.end,
new_entry.range.start <= new_entry.range.end,
paddr_check % PAGE_SIZE == 0,
ensures
new_entry.range.start < new_entry.range.end
    ==> ({
        let new_segments = segments.remove(sid).insert(sid, new_entry);
        paddr_check == segments[sid].range.start
            ==> segment_cover_count(new_segments, paddr_check) + 1
                == segment_cover_count(segments, paddr_check)
    }),
new_entry.range.start < new_entry.range.end
    ==> ({
        let new_segments = segments.remove(sid).insert(sid, new_entry);
        paddr_check != segments[sid].range.start
            ==> segment_cover_count(new_segments, paddr_check)
                == segment_cover_count(segments, paddr_check)
    }),
new_entry.range.start >= new_entry.range.end
    ==> ({
        let new_segments = segments.remove(sid);
        paddr_check == segments[sid].range.start
            ==> segment_cover_count(new_segments, paddr_check) + 1
                == segment_cover_count(segments, paddr_check)
    }),
new_entry.range.start >= new_entry.range.end
    ==> ({
        let new_segments = segments.remove(sid);
        paddr_check != segments[sid].range.start
            ==> segment_cover_count(new_segments, paddr_check)
                == segment_cover_count(segments, paddr_check)
    }),

Next-pop helper. Segment::next pops the front frame off sid, shrinking its range from [start, end) to [start + PAGE_SIZE, end). The net effect on per-paddr segment_cover_count: it decrements by 1 only at the popped paddr == start; everywhere else it’s invariant.

Models the two cases (segment becomes empty vs not) via the two resulting map shapes: remove(sid) (when the new range is empty) or remove(sid).insert(sid, new_entry) (when the new range still has frames).