Skip to main content

lemma_handle_count_insert_fresh

ostd::specs::mm::embedding

Function lemma_handle_count_insert_fresh 

Source 
pub proof fn lemma_handle_count_insert_fresh(
    frames: Map<FrameId, FrameEntry>,
    id: FrameId,
    entry: FrameEntry,
    idx: usize,
)
Expand description
requires
!frames.dom().contains(id),
frames.dom().finite(),
ensures
handle_count(frames.insert(id, entry), idx)
    == handle_count(frames, idx)
        + (if frame_to_index(entry.paddr) == idx { 1nat } else { 0nat }),

Handle-count delta under [Map::insert] at a fresh id: +1 at the inserted entry’s slot, unchanged elsewhere. Discharges the Set / filter arithmetic once so the per-step accounting proofs need only invoke it.