Function size_of_logic 

pub fn size_of_logic<T>() -> Int

size_of as a logic Int value.

The definition of size_of_logic guarantees at least the following, based on the documentation of size_of:

• (), bool, char, primitive integers and floats are known constants.
• For T: Sized, the pointer and reference types *const T, *mut T, &T, &mut T, Box<T>, Option<&T>, Option<&mut T>, and Option<Box<T>> have the same size as usize.
• [T; N] has size N * size_of_logic::<T>().

See also the Rust Reference section on Type Layout.

Stability of size_of_logic

Note that the size of usize, references, pointers… is platform-dependent: if you want to verify your code against a specific architecture, you need to use Creusot with the exact same architecture.

Additionally, for repr(Rust) types, the value of size_of/size_of_logic is not guaranteed to stay the same across compilations.

logic(open, inline)

dead

ensures

0 <= result