Skip to main content

lemma_segment_cover_split

ostd::specs::mm::embedding

Function lemma_segment_cover_split 

Source 
pub proof fn lemma_segment_cover_split(
    segments: Map<SegmentId, SegmentEntry>,
    sid: SegmentId,
    new_left: SegmentId,
    new_right: SegmentId,
    entry_left: SegmentEntry,
    entry_right: SegmentEntry,
    paddr: Paddr,
)
Expand description
requires
segments.dom().contains(sid),
segments.dom().finite(),
new_left != sid,
new_right != sid,
new_left != new_right,
!segments.remove(sid).dom().contains(new_left),
!segments.remove(sid).dom().contains(new_right),
entry_left.range.start == segments[sid].range.start,
entry_left.range.end == entry_right.range.start,
entry_right.range.end == segments[sid].range.end,
entry_left.range.start < entry_left.range.end,
entry_right.range.start < entry_right.range.end,
ensures
segment_cover_count(
    segments.remove(sid).insert(new_left, entry_left).insert(new_right, entry_right),
    paddr,
) == segment_cover_count(segments, paddr),

Split helper. Partitioning a segment’s range at mid and replacing the original sid with two fresh entries covering [start, mid) and [mid, end) leaves segment_cover_count invariant at every paddr. Any paddr covered by the original is covered by exactly one half; uncovered paddrs stay uncovered.