pub const exec fn layout_for_val_is_valid<V: ?Sized>(val: Tracked<&V>)Expand description
ensures
valid_layout(spec_size_of_val::<V>(val@) as usize, spec_align_of_val::<V>(val@) as usize),spec_size_of_val::<V>(val@) as usize as nat == spec_size_of_val::<V>(val@),spec_align_of_val::<V>(val@) as usize as nat == spec_align_of_val::<V>(val@),spec_align_of_val::<V>(val@) != 0,spec_size_of_val::<V>(val@) % spec_align_of_val::<V>(val@) == 0,Lemma to learn that the (size, alignment) of a (possibly not Sized) value 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.