Refine size_of_logic

[dianegolfouse]

• Have more types satisfy size_of::<T>() > 0, based on discussion with the Rust team, and in particular this change to the reference that seems close to be accepted: Fields must fit in the type, even for repr(Rust) rust-lang/reference#2166:

  This PR guarantees that for all repr(Rust) structs, unions, and inhabited enum variants, each field must fit in the type. [...]
  The guarantee implies that (u8, !) can never be a ZST, fully closing that door.

• Restrict computation of size_of_logic::<T>() to types where the size is known to be fixed across compilation targets.

[jhjourdan]

I appreciate your efforts in making Creusot proofs portable, but I think this is, unfortunately, doomed to failure.

Indeed, we already depend on the architecture in many places:

• The model of usize depends on the architecture, and we are not going to make it generic, because then many proofs will fail.
• Typechecking sometimes evaluate const values, and size_of is const (hence, typechecking is target-dependent, which you may find ugly, but this is the way it is)
• There are already quite a few instances of #[cfg_attr(target_pointer_width = "16", ...)] in creusot-std

So let's use the value computed by Rustc for size_of when it succeeds doing so, even if the result is not portable.

[dianegolfouse]

I unfortunately agree about platform independance, this is probably a lost battle; and we can say "verify with Creusot on each architecture you want to release on".
However there is still an issue with types whose layout is not guaranteed: I am not really comfortable saying that a type has a given size, when the next compiler version might change this...
Actually, I'm not even sure that size_of is stable on a given compiler version.

[jhjourdan]

I unfortunately agree about platform independence, this is probably a lost battle; and we can say "verify with Creusot on each architecture you want to release on". However there is still an issue with types whose layout is not guaranteed: I am not really comfortable saying that a type has a given size, when the next compiler version might change this...

I agree this is a problem, but again, typechecking (including trait resolution) depends on const evaluation, so this is a lost battle. We may open an issue about that, but basically this means that Creusot is really sound only if the code is linked with the exact same version of Rustc that is used for compilation.

Actually, I'm not even sure that size_of is stable on a given compiler version.

I would really be surprised if that would not be the case (of course, we are assuming same compiler version with the same configuration)!

[dianegolfouse]

After our discussion, I agree: I opened #2186 to track this, and slightly changed the doc of size_of_logic, but the computation of size_of_logic stays as it was.

[jhjourdan]

LGTM!