Ensure is_sized in global layout lemma

[ouuan]

This could be useful for satisfying the precondition of PointsToRaw::into_typed, saving a layout_for_type_is_valid/size_of.

Now users can write things like global size_of int == 1 to make ghost/unsized types is_sized, but that's another topic. We may need to constraint the types that can use global size_of, but it's not a problem to ensure is_sized here. Anyhow, assert(size_of::<int>() == 1) is already a mistake.

[ouuan]

Now users can write things like global size_of int == 1 to make ghost/unsized types is_sized, but that's another topic. We may need to constrain the types that can use global size_of, but it's not a problem to ensure is_sized here. Anyhow, assert(size_of::<int>() == 1) is already a mistake.

I just realized that incorrect global size_of will cause errors at compilation instead of verification. This leaves only the problem that global size_of int == 0 works and we can have is_sized::<int>(). Not a big problem IMO 🤔️