Function all_cpus 

pub exec fn all_cpus() -> ret : impl Iterator<Item = CpuId>

ensures

IteratorSpec::obeys_prophetic_iter_laws(&ret),

IteratorSpec::decrease(&ret) is Some,

IteratorSpec::remaining(&ret).len() == cpu_count(),

IteratorSpec::produces(&ret).len() == cpu_count(),

forall |i: int| {
    0 <= i < IteratorSpec::remaining(&ret).len() && IteratorSpec::produces(&ret)[i]
        ==> #[trigger] IteratorSpec::remaining(&ret)[i]@ == i
},

Returns an iterator over all CPUs.

Verified Properties

If iteration completes, CPU IDs are yielded exactly once in ascending order.