pub broadcast proof fn lemma_cpu_id_model(cpu_id: CpuId)Expand description
ensures
cpu_id.as_usize() == cpu_id@,(cpu_id.as_usize() as u32) == cpu_id@,as_usize and its u32 re-encoding equal the numeric view of a CpuId.