Function axiom_cpu_count_bounds 

pub broadcast proof fn axiom_cpu_count_bounds()

ensures

1 <= cpu_count() <= u32::MAX,

The count is a positive value that fits a u32 (the exec reads static NUM_CPUS: u32), hence also a usize; the u32 bound is what lets a CpuSet bitset fit in its backing SmallVec without overflowing isize::MAX.