Function vstd::layout::layout_of_primitives

source · 
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.