Function fresh_vm_io_id Copy item path

pub open spec fn fresh_vm_io_id<'a>(m: Map<VmIoId, VmIoEntry>) -> VmIoId

{ choose |id: VmIoId| !m.dom().contains(id) }