Function cpu_count 

pub uninterp spec fn cpu_count() -> int

The trusted value of the system CPU count. The exec reads NUM_CPUS, a u32 initialized to 1 and set once at boot (never decreased, no hot-plug), so it is a stable constant; Verus cannot mention an exec static in a spec, so this uninterp is the explicit specification boundary (mirrors io_port’s num_cpus-style pattern).