Skip to main content

lemma_handle_count_remove

ostd::specs::mm::embedding

Function lemma_handle_count_remove 

Source 
pub proof fn lemma_handle_count_remove(
    frames: Map<FrameId, FrameEntry>,
    fid: FrameId,
    idx: usize,
)
Expand description
requires
frames.dom().contains(fid),
frames.dom().finite(),
ensures
handle_count(frames.remove(fid), idx)
    == handle_count(frames, idx)
        - (if frame_to_index(frames[fid].paddr) == idx { 1nat } else { 0nat }),

Handle-count delta under [Map::remove]: -1 at the removed entry’s slot if it was the only one present (or generally -1 if the entry at fid mapped to idx), unchanged elsewhere.