pub const exec fn layout_for_type_is_valid<V>()Expand description
ensures
valid_layout(size_of::<V>() as usize, align_of::<V>() as usize),size_of::<V>() as usize as nat == size_of::<V>(),align_of::<V>() as usize as nat == align_of::<V>(),align_of::<V>() != 0,size_of::<V>() % align_of::<V>() == 0,Lemma to learn that the (size, alignment) of a type is a valid “layout”.
See valid_layout for the exact conditions.
Also exports that size is a multiple of alignment (Reference).
Note that, unusually for a lemma, this is an exec-mode function. (This is necessary to
ensure that the types are really compilable, as ghost code can reason about “virtual” types
that exceed these bounds.) Despite being exec-mode, it is a no-op.