pub broadcast proof fn layout_of_primitives()Expand description
ensures
size_of::<bool>() == 1,size_of::<char>() == 4,size_of::<u8>() == size_of::<i8>() == 1,size_of::<u16>() == size_of::<i16>() == 2,size_of::<u32>() == size_of::<i32>() == 4,size_of::<u64>() == size_of::<i64>() == 8,size_of::<u128>() == size_of::<i128>() == 16,size_of::<usize>() == size_of::<isize>(),size_of::<usize>() * 8 == usize::BITS,Size of primitives (Reference).
Note that alignment may be platform specific; if you need to use alignment, use Verus’s global directive.