Add documentation on type sizes

source/docs/guide/src/SUMMARY.md

@@ -147,6 +147,7 @@
 - [Misc. Rust features]()
   - [Statics](./static.md)
   - [char](./char.md)
+  - [Type layout](./type-layout.md)
 - [Command line]()
   - [--record](./reference-flag-record.md)
 - [Planned future work]()

source/docs/guide/src/integers.md

@@ -27,16 +27,6 @@ a `u8` value is an integer constrained to be greater than or equal to `0` and le
 {{#include ../../../rust_verify/example/guide/integers.rs:test_u8}}
 ```
 
-(The bounds of `usize` and `isize` are platform dependent.
-By default, Verus assumes that these types may be either 32 bits or 64 bits wide,
-but this can be configured with the directive:
-
-```rust
-global size_of usize == 8;
-```
-
-(This would set the size of `usize` to 8 bytes, and add a static assertion to check it matches the target.)
-
 # Using integer types in specifications
 
 Since there are 14 different integer types (counting `int`, `nat`, `u8`...`usize`, and `i8`...`isize`),

source/docs/guide/src/type-layout.md

@@ -0,0 +1,35 @@
+# Type layout
+
+Verus does not have direct access information about [type layout](https://doc.rust-lang.org/reference/type-layout.html) during verification. The layout of most types is undefined by default (with the exception of `usize`/`isize`; see below). The `global size_of` and `global layout` directives may be used to set the size and/or alignment of a type and add static assertions to check that the provided layout matches the layout used by the Rust compiler. Note that checking these assertions requires the `--compile` Verus flag as these assertions are checked by the Rust compiler.
+
+For example:
+
+```rust
+{{#include ../../../rust_verify/example/guide/sized.rs:sized_foo}}
+```
+
+The size of `Foo` is 16, rather than 12, because the C representation adds four bytes of padding to ensure that field `b` has the correct alignment.
+
+To set both the size and alignment of `Foo`, use the following directive:
+```rust
+{{#include ../../../rust_verify/example/guide/sized.rs:layout_foo}}
+```
+
+The layout of a type is dependent on its representation. The default `Rust` representation [does not guarantee that the same type always compiles to the same layout](https://doc.rust-lang.org/reference/type-layout.html#size-and-alignment). If it is important that a type's size remains the same across compilations, [other representations](https://doc.rust-lang.org/reference/type-layout.html#representations) (e.g., `repr(C)`) should be used.
+
+Once set using these directives, the size and/or alignment of a type can be accessed with `core::mem::size_of::<T>()`/`core::mem::align_of::<T>()` in both ghost and `exec` code. For example:
+
+```rust
+{{#include ../../../rust_verify/example/guide/sized.rs:sized_check}}
+```
+
+## Platform-dependent sizes
+
+The width of `usize` and `isize` is platform-dependent. By default, Verus assumes that these types may be either 32 bits or 64 bits wide, but this can be configured with the directive:
+
+```rust
+global size_of usize == 8;
+```
+
+This would set the size of `usize` to 8 bytes and add a static assertion to check that it matches the target. 
+

source/rust_verify/example/guide/sized.rs

@@ -0,0 +1,38 @@
+#[allow(unused_imports)]
+use builtin::*;
+#[allow(unused_imports)]
+use builtin_macros::*;
+
+verus! {
+    // ANCHOR: sized_foo 
+    #[repr(C)]
+    struct Foo {
+        a: u32,
+        b: u64,
+    }
+
+    global size_of Foo == 16;
+    // ANCHOR_END: sized_foo
+
+    /*
+    // ANCHOR: layout_foo
+    global layout Foo is size == 16, align == 8;
+    // ANCHOR_END: layout_foo
+    */
+
+    /*
+    // ANCHOR: sized_check
+    #[repr(C)]
+    struct Bar {
+        c: u32,
+        d: u64
+    }
+
+    fn check_size() {
+        assert(core::mem::size_of::<Foo>() == 16); // succeeds; Foo's size was set above
+        assert(core::mem::size_of::<Bar>() == 16); // fails; the size of Bar has not been set
+    }
+    */
+
+    // ANCHOR_END: sized_check
+}