[layout] Move Kani proofs from crate root

src/layout.rs

@@ -1429,3 +1429,244 @@ mod tests {
         validate_against_rust!(4, 16, 4);
     }
 }
+
+#[cfg(kani)]
+mod proofs {
+    use core::alloc::Layout;
+
+    use super::*;
+
+    impl kani::Arbitrary for DstLayout {
+        fn any() -> Self {
+            let align: NonZeroUsize = kani::any();
+            let size_info: SizeInfo = kani::any();
+
+            kani::assume(align.is_power_of_two());
+            kani::assume(align < DstLayout::THEORETICAL_MAX_ALIGN);
+
+            // For testing purposes, we most care about instantiations of
+            // `DstLayout` that can correspond to actual Rust types. We use
+            // `Layout` to verify that our `DstLayout` satisfies the validity
+            // conditions of Rust layouts.
+            kani::assume(
+                match size_info {
+                    SizeInfo::Sized { size } => Layout::from_size_align(size, align.get()),
+                    SizeInfo::SliceDst(TrailingSliceLayout { offset, elem_size: _ }) => {
+                        // `SliceDst`` cannot encode an exact size, but we know
+                        // it is at least `offset` bytes.
+                        Layout::from_size_align(offset, align.get())
+                    }
+                }
+                .is_ok(),
+            );
+
+            Self { align: align, size_info: size_info }
+        }
+    }
+
+    impl kani::Arbitrary for SizeInfo {
+        fn any() -> Self {
+            let is_sized: bool = kani::any();
+
+            match is_sized {
+                true => {
+                    let size: usize = kani::any();
+
+                    kani::assume(size <= isize::MAX as _);
+
+                    SizeInfo::Sized { size }
+                }
+                false => SizeInfo::SliceDst(kani::any()),
+            }
+        }
+    }
+
+    impl kani::Arbitrary for TrailingSliceLayout {
+        fn any() -> Self {
+            let elem_size: usize = kani::any();
+            let offset: usize = kani::any();
+
+            kani::assume(elem_size < isize::MAX as _);
+            kani::assume(offset < isize::MAX as _);
+
+            TrailingSliceLayout { elem_size, offset }
+        }
+    }
+
+    #[kani::proof]
+    fn prove_dst_layout_extend() {
+        use crate::util::{max, min, padding_needed_for};
+
+        let base: DstLayout = kani::any();
+        let field: DstLayout = kani::any();
+        let packed: Option<NonZeroUsize> = kani::any();
+
+        if let Some(max_align) = packed {
+            kani::assume(max_align.is_power_of_two());
+            kani::assume(base.align <= max_align);
+        }
+
+        // The base can only be extended if it's sized.
+        kani::assume(matches!(base.size_info, SizeInfo::Sized { .. }));
+        let base_size = if let SizeInfo::Sized { size } = base.size_info {
+            size
+        } else {
+            unreachable!();
+        };
+
+        // Under the above conditions, `DstLayout::extend` will not panic.
+        let composite = base.extend(field, packed);
+
+        // The field's alignment is clamped by `max_align` (i.e., the
+        // `packed` attribute, if any) [1].
+        //
+        // [1] Per https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers:
+        //
+        //   The alignments of each field, for the purpose of positioning
+        //   fields, is the smaller of the specified alignment and the
+        //   alignment of the field's type.
+        let field_align = min(field.align, packed.unwrap_or(DstLayout::THEORETICAL_MAX_ALIGN));
+
+        // The struct's alignment is the maximum of its previous alignment and
+        // `field_align`.
+        assert_eq!(composite.align, max(base.align, field_align));
+
+        // Compute the minimum amount of inter-field padding needed to
+        // satisfy the field's alignment, and offset of the trailing field.
+        // [1]
+        //
+        // [1] Per https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers:
+        //
+        //   Inter-field padding is guaranteed to be the minimum required in
+        //   order to satisfy each field's (possibly altered) alignment.
+        let padding = padding_needed_for(base_size, field_align);
+        let offset = base_size + padding;
+
+        // For testing purposes, we'll also construct `alloc::Layout`
+        // stand-ins for `DstLayout`, and show that `extend` behaves
+        // comparably on both types.
+        let base_analog = Layout::from_size_align(base_size, base.align.get()).unwrap();
+
+        match field.size_info {
+            SizeInfo::Sized { size: field_size } => {
+                if let SizeInfo::Sized { size: composite_size } = composite.size_info {
+                    // If the trailing field is sized, the resulting layout will
+                    // be sized. Its size will be the sum of the preceding
+                    // layout, the size of the new field, and the size of
+                    // inter-field padding between the two.
+                    assert_eq!(composite_size, offset + field_size);
+
+                    let field_analog =
+                        Layout::from_size_align(field_size, field_align.get()).unwrap();
+
+                    if let Ok((actual_composite, actual_offset)) = base_analog.extend(field_analog)
+                    {
+                        assert_eq!(actual_offset, offset);
+                        assert_eq!(actual_composite.size(), composite_size);
+                        assert_eq!(actual_composite.align(), composite.align.get());
+                    } else {
+                        // An error here reflects that composite of `base`
+                        // and `field` cannot correspond to a real Rust type
+                        // fragment, because such a fragment would violate
+                        // the basic invariants of a valid Rust layout. At
+                        // the time of writing, `DstLayout` is a little more
+                        // permissive than `Layout`, so we don't assert
+                        // anything in this branch (e.g., unreachability).
+                    }
+                } else {
+                    panic!("The composite of two sized layouts must be sized.")
+                }
+            }
+            SizeInfo::SliceDst(TrailingSliceLayout {
+                offset: field_offset,
+                elem_size: field_elem_size,
+            }) => {
+                if let SizeInfo::SliceDst(TrailingSliceLayout {
+                    offset: composite_offset,
+                    elem_size: composite_elem_size,
+                }) = composite.size_info
+                {
+                    // The offset of the trailing slice component is the sum
+                    // of the offset of the trailing field and the trailing
+                    // slice offset within that field.
+                    assert_eq!(composite_offset, offset + field_offset);
+                    // The elem size is unchanged.
+                    assert_eq!(composite_elem_size, field_elem_size);
+
+                    let field_analog =
+                        Layout::from_size_align(field_offset, field_align.get()).unwrap();
+
+                    if let Ok((actual_composite, actual_offset)) = base_analog.extend(field_analog)
+                    {
+                        assert_eq!(actual_offset, offset);
+                        assert_eq!(actual_composite.size(), composite_offset);
+                        assert_eq!(actual_composite.align(), composite.align.get());
+                    } else {
+                        // An error here reflects that composite of `base`
+                        // and `field` cannot correspond to a real Rust type
+                        // fragment, because such a fragment would violate
+                        // the basic invariants of a valid Rust layout. At
+                        // the time of writing, `DstLayout` is a little more
+                        // permissive than `Layout`, so we don't assert
+                        // anything in this branch (e.g., unreachability).
+                    }
+                } else {
+                    panic!("The extension of a layout with a DST must result in a DST.")
+                }
+            }
+        }
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    fn prove_dst_layout_extend_dst_panics() {
+        let base: DstLayout = kani::any();
+        let field: DstLayout = kani::any();
+        let packed: Option<NonZeroUsize> = kani::any();
+
+        if let Some(max_align) = packed {
+            kani::assume(max_align.is_power_of_two());
+            kani::assume(base.align <= max_align);
+        }
+
+        kani::assume(matches!(base.size_info, SizeInfo::SliceDst(..)));
+
+        let _ = base.extend(field, packed);
+    }
+
+    #[kani::proof]
+    fn prove_dst_layout_pad_to_align() {
+        use crate::util::padding_needed_for;
+
+        let layout: DstLayout = kani::any();
+
+        let padded: DstLayout = layout.pad_to_align();
+
+        // Calling `pad_to_align` does not alter the `DstLayout`'s alignment.
+        assert_eq!(padded.align, layout.align);
+
+        if let SizeInfo::Sized { size: unpadded_size } = layout.size_info {
+            if let SizeInfo::Sized { size: padded_size } = padded.size_info {
+                // If the layout is sized, it will remain sized after padding is
+                // added. Its sum will be its unpadded size and the size of the
+                // trailing padding needed to satisfy its alignment
+                // requirements.
+                let padding = padding_needed_for(unpadded_size, layout.align);
+                assert_eq!(padded_size, unpadded_size + padding);
+
+                // Prove that calling `DstLayout::pad_to_align` behaves
+                // identically to `Layout::pad_to_align`.
+                let layout_analog =
+                    Layout::from_size_align(unpadded_size, layout.align.get()).unwrap();
+                let padded_analog = layout_analog.pad_to_align();
+                assert_eq!(padded_analog.align(), layout.align.get());
+                assert_eq!(padded_analog.size(), padded_size);
+            } else {
+                panic!("The padding of a sized layout must result in a sized layout.")
+            }
+        } else {
+            // If the layout is a DST, padding cannot be statically added.
+            assert_eq!(padded.size_info, layout.size_info);
+        }
+    }
+}