pub open spec fn fresh_vm_space_id<'a>(m: Map<VmSpaceId, VmSpaceOwner>) -> VmSpaceIdExpand description
{ choose |id: VmSpaceId| !m.dom().contains(id) }Picks an id not currently in m.dom(). Since the key type is int, an
unused id always exists.
pub open spec fn fresh_vm_space_id<'a>(m: Map<VmSpaceId, VmSpaceOwner>) -> VmSpaceId{ choose |id: VmSpaceId| !m.dom().contains(id) }Picks an id not currently in m.dom(). Since the key type is int, an
unused id always exists.