Function handle_count 

pub open spec fn handle_count(frames: Map<FrameId, FrameEntry>, idx: int) -> nat

{ frames.dom().filter(|fid: FrameId| frame_to_index(frames[fid].paddr) == idx).len() }

Number of outstanding Frame handles whose paddr maps to slot idx.