Skip to main content

handle_count

ostd::specs::mm::embedding

Function handle_count 

Source 
pub open spec fn handle_count(frames: Map<FrameId, FrameEntry>, idx: usize) -> nat
Expand description
{ frames.dom().filter(|fid: FrameId| frame_to_index(frames[fid].paddr) == idx).len() }

Number of outstanding Frame handles whose paddr maps to slot idx — i.e. the #handles(idx) term of the exact reference-count accounting ref_count(idx) == #handles(idx) + paths_in_pt(idx).len() (Stage 5 / full #4). Well-defined as a nat only when frames.dom() is finite, which VmStore::inv maintains.