layout and alignment invariants

library/core/src/alloc/layout.rs

@@ -4,10 +4,11 @@
 // collections, resulting in having to optimize down excess IR multiple times.
 // Your performance intuition is useless. Run perf.
 
-use safety::requires;
+use safety::{invariant, requires};
 use crate::error::Error;
 use crate::ptr::{Alignment, NonNull};
 use crate::{assert_unsafe_precondition, cmp, fmt, mem};
+use crate::ub_checks::Invariant;
 
 #[cfg(kani)]
 use crate::kani;
@@ -39,6 +40,7 @@ const fn size_align<T>() -> (usize, usize) {
 #[stable(feature = "alloc_layout", since = "1.28.0")]
 #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
 #[lang = "alloc_layout"]
+#[invariant(self.align.is_safe())]
 pub struct Layout {
     // size of the requested block of memory, measured in bytes.
     size: usize,
@@ -529,6 +531,7 @@ mod verify {
             let layout = Layout::from_size_align_unchecked(s, a);
             assert_eq!(layout.size(), s);
             assert_eq!(layout.align(), a);
+            assert!(layout.is_safe());
         }
     }
 }

library/core/src/ptr/alignment.rs

@@ -1,6 +1,6 @@
-use safety::{ensures, requires};
+use safety::{ensures, invariant, requires};
 use crate::num::NonZero;
-use crate::ub_checks::assert_unsafe_precondition;
+use crate::ub_checks::{assert_unsafe_precondition, Invariant};
 use crate::{cmp, fmt, hash, mem, num};
 
 #[cfg(kani)]
@@ -14,6 +14,7 @@ use crate::kani;
 #[unstable(feature = "ptr_alignment_type", issue = "102070")]
 #[derive(Copy, Clone, PartialEq, Eq)]
 #[repr(transparent)]
+#[invariant(self.as_usize().is_power_of_two())]
 pub struct Alignment(AlignmentEnum);
 
 // Alignment is `repr(usize)`, but via extra steps.
@@ -391,7 +392,9 @@ mod verify {
     impl kani::Arbitrary for Alignment {
         fn any() -> Self {
             let align = kani::any_where(|a: &usize| a.is_power_of_two());
-            unsafe { mem::transmute::<usize, Alignment>(align) }
+            let ret = unsafe { mem::transmute::<usize, Alignment>(align) };
+            kani::assert(ret.is_safe(), "Alignment is safe");
+            ret
         }
     }