From 96f16035d754d11b428d2a5f1db105c4ecda9ff1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 23 Jul 2024 12:40:14 +0000
Subject: [PATCH 01/17] Add harnesses for all public functions of `Layout`

Exercise all public member functions of `Layout` and assert properties
over the result. Some of those should, perhaps, become `ensures`
clauses.
---
 library/core/src/alloc/layout.rs | 199 +++++++++++++++++++++++++++++++
 1 file changed, 199 insertions(+)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index c63db5aa0aa2f..b5074a215645b 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -503,6 +503,22 @@ impl fmt::Display for LayoutError {
 mod verify {
     use super::*;
 
+    // pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError>
+    #[kani::proof_for_contract(Layout::from_size_align)]
+    pub fn check_from_size_align() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        if let Some(layout) = Layout::from_size_align(s, a) {
+            assert_eq!(layout.size(), s);
+            assert_eq!(layout.align(), a);
+            assert!(a > 0);
+            assert!(a.is_power_of_two());
+            assert!(s <= isize::MAX as usize - (a - 1));
+        }
+    }
+
+    // pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self
     #[kani::proof_for_contract(Layout::from_size_align_unchecked)]
     pub fn check_from_size_align_unchecked() {
         let s = kani::any::<usize>();
@@ -514,4 +530,187 @@ mod verify {
             assert_eq!(layout.align(), a);
         }
     }
+
+    // pub const fn size(&self) -> usize
+    #[kani::proof_for_contract(Layout::size)]
+    pub fn check_size() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            assert_eq!(layout.size(), s);
+        }
+    }
+
+    // pub const fn align(&self) -> usize
+    #[kani::proof_for_contract(Layout::align)]
+    pub fn check_align() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            assert!(layout.align().is_power_of_two());
+        }
+    }
+
+    // pub const fn new<T>() -> Self
+    #[kani::proof_for_contract(Layout::new<i32>)]
+    pub fn check_new_i32() {
+        let layout = Layout::new<i32>();
+        assert_eq!(layout.size(), 4);
+        assert!(layout.align().is_power_of_two());
+    }
+
+    // pub const fn for_value<T: ?Sized>(t: &T) -> Self
+    #[kani::proof_for_contract(Layout::for_value<i32>)]
+    pub fn check_for_value_i32() {
+        let array : [i32; 2] = [1, 2];
+        let layout = Layout::for_value<&i32>(&array[1 .. 1);
+        assert!(layout.align().is_power_of_two());
+    }
+
+    // pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self
+    #[kani::proof_for_contract(Layout::for_value_raw<i32>)]
+    pub fn check_for_value_raw_i32() {
+        unsafe {
+            let layout = Layout::for_value_raw<i32>(&[]);
+            assert!(layout.align().is_power_of_two());
+        }
+    }
+
+    // pub const fn dangling(&self) -> NonNull<u8>
+    #[kani::proof_for_contract(Layout::dangling)]
+    pub fn check_dangling() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            assert!(layout.dangling().is_aligned());
+        }
+    }
+
+    // pub fn align_to(&self, align: usize) -> Result<Self, LayoutError>
+    #[kani::proof_for_contract(Layout::align_to)]
+    pub fn check_align_to() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            let a2 = kani::any::<usize>();
+            if let Some(layout2) = layout.align_to(a2) {
+                assert!(layout2.align() > 0);
+                assert!(layout2.align().is_power_of_two());
+            }
+        }
+    }
+
+    // pub const fn padding_needed_for(&self, align: usize) -> usize
+    #[kani::proof_for_contract(Layout::padding_needed_for)]
+    pub fn check_padding_needed_for() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            let a2 = kani::any::<usize>();
+            if(a2.is_power_of_two() && a2 <= a) {
+                let p = layout.padding_needed_for(a2);
+                assert!(p <= a2);
+            }
+        }
+    }
+
+    // pub const fn pad_to_align(&self) -> Layout
+    #[kani::proof_for_contract(Layout::pad_to_align)]
+    pub fn check_pad_to_align() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            let layout2 = layout.pad_to_align();
+            assert_eq!(layout2.size() % a, 0);
+            assert_eq!(layout.size() + layout.padding_needed_for(layout.align()), layout2.size());
+        }
+    }
+
+    // pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError>
+    #[kani::proof_for_contract(Layout::repeat)]
+    pub fn check_repeat() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            let n = kani::any::<usize>();
+            if let Some((layout2, padding)) = layout.repeat(n) {
+                assert!(n == 0 || layout2.size() >= s);
+                assert!(n == 0 || padding < a);
+            }
+        }
+    }
+
+    // pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError>
+    #[kani::proof_for_contract(Layout::extend)]
+    pub fn check_extend() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            let s2 = kani::any::<usize>();
+            let a2 = kani::any::<usize>();
+            let layout2 = Layout::from_size_align_unchecked(s2, a2);
+            if let Some((layout3, offset)) = layout.extend(layout2) {
+                assert_eq!(layout3.align(), cmp::max(a, a2));
+                assert!(layout3.size() >= s + s2);
+                assert!(offset >= s);
+                assert!(offset <= layout3.size());
+            }
+        }
+    }
+
+    // pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError>
+    #[kani::proof_for_contract(Layout::repeat_packed)]
+    pub fn check_repeat_packed() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            let n = kani::any::<usize>();
+            if let Some(layout2) = layout.repeat_packed(n) {
+                assert!(n == 0 || layout2.size() >= s);
+            }
+        }
+    }
+
+    // pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError>
+    #[kani::proof_for_contract(Layout::extend_packed)]
+    pub fn check_extend_packed() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            let s2 = kani::any::<usize>();
+            let a2 = kani::any::<usize>();
+            let layout2 = Layout::from_size_align_unchecked(s2, a2);
+            if let Some(layout3) = layout.extend_packed(layout2) {
+                assert_eq!(layout3.align(), a);
+                assert_eq!(layout3.size(), s + s2);
+            }
+        }
+    }
+
+    // pub const fn array<T>(n: usize) -> Result<Self, LayoutError>
+    #[kani::proof_for_contract(Layout::array<i32>)]
+    pub fn check_array_i32() {
+        let layout = Layout::array<i32>();
+        assert!(layout.align().is_power_of_two());
+    }
 }

From 617ba54478fc07c6560d2c6c86ccaeca2c950895 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 23 Jul 2024 14:57:13 +0000
Subject: [PATCH 02/17] Fix syntax errors

---
 library/core/src/alloc/layout.rs | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index b5074a215645b..2ce6d7357c02a 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -509,7 +509,7 @@ mod verify {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
 
-        if let Some(layout) = Layout::from_size_align(s, a) {
+        if let Ok(layout) = Layout::from_size_align(s, a) {
             assert_eq!(layout.size(), s);
             assert_eq!(layout.align(), a);
             assert!(a > 0);
@@ -558,7 +558,7 @@ mod verify {
     // pub const fn new<T>() -> Self
     #[kani::proof_for_contract(Layout::new<i32>)]
     pub fn check_new_i32() {
-        let layout = Layout::new<i32>();
+        let layout = Layout::new::<i32>();
         assert_eq!(layout.size(), 4);
         assert!(layout.align().is_power_of_two());
     }
@@ -567,7 +567,7 @@ mod verify {
     #[kani::proof_for_contract(Layout::for_value<i32>)]
     pub fn check_for_value_i32() {
         let array : [i32; 2] = [1, 2];
-        let layout = Layout::for_value<&i32>(&array[1 .. 1);
+        let layout = Layout::for_value::<[i32]>(&array[1 .. 1]);
         assert!(layout.align().is_power_of_two());
     }
 
@@ -575,7 +575,7 @@ mod verify {
     #[kani::proof_for_contract(Layout::for_value_raw<i32>)]
     pub fn check_for_value_raw_i32() {
         unsafe {
-            let layout = Layout::for_value_raw<i32>(&[]);
+            let layout = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
             assert!(layout.align().is_power_of_two());
         }
     }
@@ -601,7 +601,7 @@ mod verify {
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let a2 = kani::any::<usize>();
-            if let Some(layout2) = layout.align_to(a2) {
+            if let Ok(layout2) = layout.align_to(a2) {
                 assert!(layout2.align() > 0);
                 assert!(layout2.align().is_power_of_two());
             }
@@ -647,7 +647,7 @@ mod verify {
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let n = kani::any::<usize>();
-            if let Some((layout2, padding)) = layout.repeat(n) {
+            if let Ok((layout2, padding)) = layout.repeat(n) {
                 assert!(n == 0 || layout2.size() >= s);
                 assert!(n == 0 || padding < a);
             }
@@ -665,7 +665,7 @@ mod verify {
             let s2 = kani::any::<usize>();
             let a2 = kani::any::<usize>();
             let layout2 = Layout::from_size_align_unchecked(s2, a2);
-            if let Some((layout3, offset)) = layout.extend(layout2) {
+            if let Ok((layout3, offset)) = layout.extend(layout2) {
                 assert_eq!(layout3.align(), cmp::max(a, a2));
                 assert!(layout3.size() >= s + s2);
                 assert!(offset >= s);
@@ -683,7 +683,7 @@ mod verify {
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let n = kani::any::<usize>();
-            if let Some(layout2) = layout.repeat_packed(n) {
+            if let Ok(layout2) = layout.repeat_packed(n) {
                 assert!(n == 0 || layout2.size() >= s);
             }
         }
@@ -700,7 +700,7 @@ mod verify {
             let s2 = kani::any::<usize>();
             let a2 = kani::any::<usize>();
             let layout2 = Layout::from_size_align_unchecked(s2, a2);
-            if let Some(layout3) = layout.extend_packed(layout2) {
+            if let Ok(layout3) = layout.extend_packed(layout2) {
                 assert_eq!(layout3.align(), a);
                 assert_eq!(layout3.size(), s + s2);
             }
@@ -710,7 +710,10 @@ mod verify {
     // pub const fn array<T>(n: usize) -> Result<Self, LayoutError>
     #[kani::proof_for_contract(Layout::array<i32>)]
     pub fn check_array_i32() {
-        let layout = Layout::array<i32>();
-        assert!(layout.align().is_power_of_two());
+        let n = kani::any::<usize>();
+        if let Ok(layout) = Layout::array::<i32>(n) {
+            assert!(layout.size() >= n * 4);
+            assert!(layout.align().is_power_of_two());
+        }
     }
 }

From 6a6bd64f805e3a62e03881892aaafda4ed88485c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 26 Jul 2024 13:28:21 +0000
Subject: [PATCH 03/17] Add some ensures clauses

---
 library/core/src/alloc/layout.rs | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 2ce6d7357c02a..98e5feba26f7e 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -4,7 +4,7 @@
 // collections, resulting in having to optimize down excess IR multiple times.
 // Your performance intuition is useless. Run perf.
 
-use safety::requires;
+use safety::{ensures, requires};
 use crate::cmp;
 use crate::error::Error;
 use crate::fmt;
@@ -71,6 +71,7 @@ impl Layout {
     #[rustc_const_stable(feature = "const_alloc_layout_size_align", since = "1.50.0")]
     #[inline]
     #[rustc_allow_const_fn_unstable(ptr_alignment_type)]
+    #[ensures(|result| result.is_err() || align.is_power_of_two())]
     pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError> {
         if !align.is_power_of_two() {
             return Err(LayoutError);
@@ -145,6 +146,7 @@ impl Layout {
                   without modifying the layout"]
     #[inline]
     #[rustc_allow_const_fn_unstable(ptr_alignment_type)]
+    #[ensures(|result| result.is_power_of_two())]
     pub const fn align(&self) -> usize {
         self.align.as_usize()
     }
@@ -154,6 +156,7 @@ impl Layout {
     #[rustc_const_stable(feature = "alloc_layout_const_new", since = "1.42.0")]
     #[must_use]
     #[inline]
+    #[ensures(|result| result.align().is_power_of_two())]
     pub const fn new<T>() -> Self {
         let (size, align) = size_align::<T>();
         // SAFETY: if the type is instantiated, rustc already ensures that its
@@ -169,6 +172,7 @@ impl Layout {
     #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")]
     #[must_use]
     #[inline]
+    #[ensures(|result| result.align().is_power_of_two())]
     pub const fn for_value<T: ?Sized>(t: &T) -> Self {
         let (size, align) = (mem::size_of_val(t), mem::align_of_val(t));
         // SAFETY: see rationale in `new` for why this is using the unsafe variant
@@ -203,6 +207,7 @@ impl Layout {
     #[unstable(feature = "layout_for_ptr", issue = "69835")]
     #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")]
     #[must_use]
+    #[ensures(|result| result.align().is_power_of_two())]
     pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self {
         // SAFETY: we pass along the prerequisites of these functions to the caller
         let (size, align) = unsafe { (mem::size_of_val_raw(t), mem::align_of_val_raw(t)) };
@@ -220,6 +225,7 @@ impl Layout {
     #[rustc_const_unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[must_use]
     #[inline]
+    #[ensures(|result| result.is_aligned())]
     pub const fn dangling(&self) -> NonNull<u8> {
         // SAFETY: align is guaranteed to be non-zero
         unsafe { NonNull::new_unchecked(crate::ptr::without_provenance_mut::<u8>(self.align())) }
@@ -241,6 +247,7 @@ impl Layout {
     /// `align` violates the conditions listed in [`Layout::from_size_align`].
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[inline]
+    #[ensures(|result| result.is_err() || result.unwrap().is_aligned())]
     pub fn align_to(&self, align: usize) -> Result<Self, LayoutError> {
         Layout::from_size_align(self.size(), cmp::max(self.align(), align))
     }
@@ -532,7 +539,7 @@ mod verify {
     }
 
     // pub const fn size(&self) -> usize
-    #[kani::proof_for_contract(Layout::size)]
+    #[kani::proof]
     pub fn check_size() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();

From 08d6f5824b0cba3357e1da53dc7a26ee0fc18981 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 30 Jul 2024 11:07:16 +0000
Subject: [PATCH 04/17] Fix syntax errors, add ensures

---
 library/core/src/alloc/layout.rs | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 98e5feba26f7e..0e93040a5cb63 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -156,7 +156,6 @@ impl Layout {
     #[rustc_const_stable(feature = "alloc_layout_const_new", since = "1.42.0")]
     #[must_use]
     #[inline]
-    #[ensures(|result| result.align().is_power_of_two())]
     pub const fn new<T>() -> Self {
         let (size, align) = size_align::<T>();
         // SAFETY: if the type is instantiated, rustc already ensures that its
@@ -247,7 +246,7 @@ impl Layout {
     /// `align` violates the conditions listed in [`Layout::from_size_align`].
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[inline]
-    #[ensures(|result| result.is_err() || result.unwrap().is_aligned())]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() >= align)]
     pub fn align_to(&self, align: usize) -> Result<Self, LayoutError> {
         Layout::from_size_align(self.size(), cmp::max(self.align(), align))
     }
@@ -273,6 +272,7 @@ impl Layout {
     #[must_use = "this returns the padding needed, \
                   without modifying the `Layout`"]
     #[inline]
+    #[ensures(|result| *result <= align)]
     pub const fn padding_needed_for(&self, align: usize) -> usize {
         let len = self.size();
 
@@ -309,6 +309,7 @@ impl Layout {
     #[must_use = "this returns a new `Layout`, \
                   without modifying the original"]
     #[inline]
+    #[ensures(|result| result.size() % result.align() == 0)]
     pub const fn pad_to_align(&self) -> Layout {
         let pad = self.padding_needed_for(self.align());
         // This cannot overflow. Quoting from the invariant of Layout:
@@ -331,6 +332,7 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().1 % n == 0)]
     pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
         // This cannot overflow. Quoting from the invariant of Layout:
         // > `size`, when rounded up to the nearest multiple of `align`,
@@ -391,6 +393,7 @@ impl Layout {
     /// ```
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[inline]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().1 <= result.as_ref().unwrap().0.size())]
     pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> {
         let new_align = cmp::max(self.align, next.align);
         let pad = self.padding_needed_for(next.align());
@@ -417,6 +420,7 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() % n == 0)]
     pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
         let size = self.size().checked_mul(n).ok_or(LayoutError)?;
         // The safe constructor is called here to enforce the isize size limit.
@@ -431,6 +435,7 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() <= next.size())]
     pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError> {
         let new_size = self.size().checked_add(next.size()).ok_or(LayoutError)?;
         // The safe constructor is called here to enforce the isize size limit.
@@ -563,7 +568,7 @@ mod verify {
     }
 
     // pub const fn new<T>() -> Self
-    #[kani::proof_for_contract(Layout::new<i32>)]
+    #[kani::proof]
     pub fn check_new_i32() {
         let layout = Layout::new::<i32>();
         assert_eq!(layout.size(), 4);
@@ -571,7 +576,7 @@ mod verify {
     }
 
     // pub const fn for_value<T: ?Sized>(t: &T) -> Self
-    #[kani::proof_for_contract(Layout::for_value<i32>)]
+    #[kani::proof_for_contract(Layout::for_value)]
     pub fn check_for_value_i32() {
         let array : [i32; 2] = [1, 2];
         let layout = Layout::for_value::<[i32]>(&array[1 .. 1]);
@@ -579,7 +584,7 @@ mod verify {
     }
 
     // pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self
-    #[kani::proof_for_contract(Layout::for_value_raw<i32>)]
+    #[kani::proof_for_contract(Layout::for_value_raw)]
     pub fn check_for_value_raw_i32() {
         unsafe {
             let layout = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
@@ -654,9 +659,9 @@ mod verify {
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let n = kani::any::<usize>();
-            if let Ok((layout2, padding)) = layout.repeat(n) {
+            if let Ok((layout2, padded_size)) = layout.repeat(n) {
                 assert!(n == 0 || layout2.size() >= s);
-                assert!(n == 0 || padding < a);
+                assert_eq!(layout2.size(), n * padded_size);
             }
         }
     }
@@ -715,7 +720,7 @@ mod verify {
     }
 
     // pub const fn array<T>(n: usize) -> Result<Self, LayoutError>
-    #[kani::proof_for_contract(Layout::array<i32>)]
+    #[kani::proof]
     pub fn check_array_i32() {
         let n = kani::any::<usize>();
         if let Ok(layout) = Layout::array::<i32>(n) {

From 8c21272bdf5383d23ac117219e5520d13e681d01 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 8 Aug 2024 11:16:25 +0000
Subject: [PATCH 05/17] Add more ensures clauses

---
 library/core/src/alloc/layout.rs | 90 ++++++++++++--------------------
 1 file changed, 34 insertions(+), 56 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 0e93040a5cb63..ac49caf0a2cfe 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -72,6 +72,9 @@ impl Layout {
     #[inline]
     #[rustc_allow_const_fn_unstable(ptr_alignment_type)]
     #[ensures(|result| result.is_err() || align.is_power_of_two())]
+    #[ensures(|result| result.is_err() || size <= isize::MAX as usize - (align - 1))]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == size)]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == align)]
     pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError> {
         if !align.is_power_of_two() {
             return Err(LayoutError);
@@ -123,6 +126,8 @@ impl Layout {
     #[inline]
     #[rustc_allow_const_fn_unstable(ptr_alignment_type)]
     #[requires(Layout::from_size_align(size, align).is_ok())]
+    #[ensures(|result| result.size() == size)]
+    #[ensures(|result| result.align() == align)]
     pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
         // SAFETY: the caller is required to uphold the preconditions.
         unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
@@ -247,6 +252,7 @@ impl Layout {
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[inline]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() >= align)]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().align().is_power_of_two())]
     pub fn align_to(&self, align: usize) -> Result<Self, LayoutError> {
         Layout::from_size_align(self.size(), cmp::max(self.align(), align))
     }
@@ -309,7 +315,10 @@ impl Layout {
     #[must_use = "this returns a new `Layout`, \
                   without modifying the original"]
     #[inline]
+    #[ensures(|result| result.size() >= self.size())]
+    #[ensures(|result| result.align() == self.align())]
     #[ensures(|result| result.size() % result.align() == 0)]
+    #[ensures(|result| self.size() + self.padding_needed_for(self.align()) == result.size())]
     pub const fn pad_to_align(&self) -> Layout {
         let pad = self.padding_needed_for(self.align());
         // This cannot overflow. Quoting from the invariant of Layout:
@@ -332,7 +341,9 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    #[ensures(|result| result.is_err() || result.as_ref().unwrap().1 % n == 0)]
+    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().1 % n == 0)]
+    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size())]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]
     pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
         // This cannot overflow. Quoting from the invariant of Layout:
         // > `size`, when rounded up to the nearest multiple of `align`,
@@ -393,6 +404,9 @@ impl Layout {
     /// ```
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[inline]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.align() == cmp::max(self.align(), next.align()))]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() >= self.size() + next.size())]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().1 >= self.size())]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().1 <= result.as_ref().unwrap().0.size())]
     pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> {
         let new_align = cmp::max(self.align, next.align);
@@ -420,7 +434,8 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() % n == 0)]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size())]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
     pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
         let size = self.size().checked_mul(n).ok_or(LayoutError)?;
         // The safe constructor is called here to enforce the isize size limit.
@@ -435,7 +450,11 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
+    // the below is wrong but was written in a previous commit; keeping it for now to confirm that
+    // this is caught
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() <= next.size())]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == self.size() + next.size())]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
     pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError> {
         let new_size = self.size().checked_add(next.size()).ok_or(LayoutError)?;
         // The safe constructor is called here to enforce the isize size limit.
@@ -520,14 +539,7 @@ mod verify {
     pub fn check_from_size_align() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
-        if let Ok(layout) = Layout::from_size_align(s, a) {
-            assert_eq!(layout.size(), s);
-            assert_eq!(layout.align(), a);
-            assert!(a > 0);
-            assert!(a.is_power_of_two());
-            assert!(s <= isize::MAX as usize - (a - 1));
-        }
+        let _ = Layout::from_size_align(s, a);
     }
 
     // pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self
@@ -535,11 +547,8 @@ mod verify {
     pub fn check_from_size_align_unchecked() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            assert_eq!(layout.size(), s);
-            assert_eq!(layout.align(), a);
+            let _ = Layout::from_size_align_unchecked(s, a);
         }
     }
 
@@ -548,7 +557,6 @@ mod verify {
     pub fn check_size() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             assert_eq!(layout.size(), s);
@@ -560,10 +568,9 @@ mod verify {
     pub fn check_align() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
-            assert!(layout.align().is_power_of_two());
+            let _ = layout.align();
         }
     }
 
@@ -579,16 +586,14 @@ mod verify {
     #[kani::proof_for_contract(Layout::for_value)]
     pub fn check_for_value_i32() {
         let array : [i32; 2] = [1, 2];
-        let layout = Layout::for_value::<[i32]>(&array[1 .. 1]);
-        assert!(layout.align().is_power_of_two());
+        let _ = Layout::for_value::<[i32]>(&array[1 .. 1]);
     }
 
     // pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self
     #[kani::proof_for_contract(Layout::for_value_raw)]
     pub fn check_for_value_raw_i32() {
         unsafe {
-            let layout = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
-            assert!(layout.align().is_power_of_two());
+            let _ = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
         }
     }
 
@@ -597,10 +602,9 @@ mod verify {
     pub fn check_dangling() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
-            assert!(layout.dangling().is_aligned());
+            let _ = layout.dangling();
         }
     }
 
@@ -609,14 +613,10 @@ mod verify {
     pub fn check_align_to() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let a2 = kani::any::<usize>();
-            if let Ok(layout2) = layout.align_to(a2) {
-                assert!(layout2.align() > 0);
-                assert!(layout2.align().is_power_of_two());
-            }
+            let _ = layout.align_to(a2);
         }
     }
 
@@ -625,13 +625,11 @@ mod verify {
     pub fn check_padding_needed_for() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let a2 = kani::any::<usize>();
             if(a2.is_power_of_two() && a2 <= a) {
-                let p = layout.padding_needed_for(a2);
-                assert!(p <= a2);
+                let _ = layout.padding_needed_for(a2);
             }
         }
     }
@@ -641,12 +639,9 @@ mod verify {
     pub fn check_pad_to_align() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
-            let layout2 = layout.pad_to_align();
-            assert_eq!(layout2.size() % a, 0);
-            assert_eq!(layout.size() + layout.padding_needed_for(layout.align()), layout2.size());
+            let _ = layout.pad_to_align();
         }
     }
 
@@ -655,14 +650,10 @@ mod verify {
     pub fn check_repeat() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let n = kani::any::<usize>();
-            if let Ok((layout2, padded_size)) = layout.repeat(n) {
-                assert!(n == 0 || layout2.size() >= s);
-                assert_eq!(layout2.size(), n * padded_size);
-            }
+            let _ = layout.repeat(n);
         }
     }
 
@@ -671,18 +662,12 @@ mod verify {
     pub fn check_extend() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let s2 = kani::any::<usize>();
             let a2 = kani::any::<usize>();
             let layout2 = Layout::from_size_align_unchecked(s2, a2);
-            if let Ok((layout3, offset)) = layout.extend(layout2) {
-                assert_eq!(layout3.align(), cmp::max(a, a2));
-                assert!(layout3.size() >= s + s2);
-                assert!(offset >= s);
-                assert!(offset <= layout3.size());
-            }
+            let _ = layout.extend(layout2);
         }
     }
 
@@ -691,13 +676,10 @@ mod verify {
     pub fn check_repeat_packed() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let n = kani::any::<usize>();
-            if let Ok(layout2) = layout.repeat_packed(n) {
-                assert!(n == 0 || layout2.size() >= s);
-            }
+            let _ = layout.repeat_packed(n);
         }
     }
 
@@ -706,16 +688,12 @@ mod verify {
     pub fn check_extend_packed() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
-
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let s2 = kani::any::<usize>();
             let a2 = kani::any::<usize>();
             let layout2 = Layout::from_size_align_unchecked(s2, a2);
-            if let Ok(layout3) = layout.extend_packed(layout2) {
-                assert_eq!(layout3.align(), a);
-                assert_eq!(layout3.size(), s + s2);
-            }
+            let _ = layout.extend_packed(layout2);
         }
     }
 

From 0b62529f20c3ad5056a0589af7d0d03874d4d549 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 9 Aug 2024 11:17:47 +0000
Subject: [PATCH 06/17] Wrong clause was caught

---
 library/core/src/alloc/layout.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index ac49caf0a2cfe..6d8334a243aac 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -434,7 +434,10 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size())]
+    // the below multiplication might be too costly to prove at this time
+    // #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size())]
+    // use the weaker statement below for now
+    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().size() >= self.size())]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
     pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
         let size = self.size().checked_mul(n).ok_or(LayoutError)?;
@@ -450,9 +453,6 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    // the below is wrong but was written in a previous commit; keeping it for now to confirm that
-    // this is caught
-    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() <= next.size())]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == self.size() + next.size())]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
     pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError> {

From e331419795726fa5c6159bcb0aaef0de60004b9d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 9 Aug 2024 13:15:07 +0000
Subject: [PATCH 07/17] Avoid multiplication

---
 library/core/src/alloc/layout.rs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 6d8334a243aac..fa2a433d63cf5 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -343,7 +343,10 @@ impl Layout {
     #[inline]
     #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().1 % n == 0)]
     #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size())]
-    #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]
+    // the below multiplication might be too costly to prove at this time
+    // #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]
+    // use the weaker statement below for now
+    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= result.as_ref().unwrap().1)]
     pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
         // This cannot overflow. Quoting from the invariant of Layout:
         // > `size`, when rounded up to the nearest multiple of `align`,

From 45505edb9673ad794222ab624b9493326c90cfcd Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 9 Aug 2024 13:33:11 +0000
Subject: [PATCH 08/17] Add assumptions

---
 library/core/src/alloc/layout.rs | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index fa2a433d63cf5..20d47b29439ea 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -560,6 +560,7 @@ mod verify {
     pub fn check_size() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             assert_eq!(layout.size(), s);
@@ -605,6 +606,7 @@ mod verify {
     pub fn check_dangling() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let _ = layout.dangling();
@@ -616,6 +618,7 @@ mod verify {
     pub fn check_align_to() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let a2 = kani::any::<usize>();
@@ -628,6 +631,7 @@ mod verify {
     pub fn check_padding_needed_for() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let a2 = kani::any::<usize>();
@@ -642,6 +646,7 @@ mod verify {
     pub fn check_pad_to_align() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let _ = layout.pad_to_align();
@@ -653,6 +658,7 @@ mod verify {
     pub fn check_repeat() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let n = kani::any::<usize>();
@@ -665,10 +671,12 @@ mod verify {
     pub fn check_extend() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let s2 = kani::any::<usize>();
             let a2 = kani::any::<usize>();
+            kani::assume(Layout::from_size_align(s2, a2).is_ok());
             let layout2 = Layout::from_size_align_unchecked(s2, a2);
             let _ = layout.extend(layout2);
         }
@@ -679,6 +687,7 @@ mod verify {
     pub fn check_repeat_packed() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let n = kani::any::<usize>();
@@ -691,10 +700,12 @@ mod verify {
     pub fn check_extend_packed() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let s2 = kani::any::<usize>();
             let a2 = kani::any::<usize>();
+            kani::assume(Layout::from_size_align(s2, a2).is_ok());
             let layout2 = Layout::from_size_align_unchecked(s2, a2);
             let _ = layout.extend_packed(layout2);
         }

From 4156263046cb7eb01058131e2a6b2f91e42743e5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 9 Aug 2024 13:46:34 +0000
Subject: [PATCH 09/17] Fixed contracts

---
 library/core/src/alloc/layout.rs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 20d47b29439ea..53426be7e6010 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -341,7 +341,7 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().1 % n == 0)]
+    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0)]
     #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size())]
     // the below multiplication might be too costly to prove at this time
     // #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]
@@ -572,6 +572,7 @@ mod verify {
     pub fn check_align() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
+        kani::assume(Layout::from_size_align(s, a).is_ok());
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);
             let _ = layout.align();

From 5231a68fdd82747fcccf8171775489d37f274fd3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 9 Aug 2024 19:50:56 +0000
Subject: [PATCH 10/17] Try disabling one more clause

---
 library/core/src/alloc/layout.rs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 53426be7e6010..9104ab3356713 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -341,7 +341,8 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0)]
+    // the below modulo operation might be too costly to prove
+    // #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0)]
     #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size())]
     // the below multiplication might be too costly to prove at this time
     // #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]

From 8e0c75a6bfb8a3297ed652a182f0ba441958f530 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 20 Aug 2024 12:38:39 +0000
Subject: [PATCH 11/17] Use Arbitrary, add contracts

---
 library/core/src/alloc/layout.rs | 121 ++++++++++---------------------
 1 file changed, 40 insertions(+), 81 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 015aefe29d5cd..4d38c1728fda2 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -159,6 +159,9 @@ impl Layout {
     #[rustc_const_stable(feature = "alloc_layout_const_new", since = "1.42.0")]
     #[must_use]
     #[inline]
+    #[requires(mem::align_of::<T>().is_power_of_two())]
+    #[ensures(|result| result.size() == mem::size_of::<T>())]
+    #[ensures(|result| result.align() == mem::align_of::<T>())]
     pub const fn new<T>() -> Self {
         let (size, align) = size_align::<T>();
         // SAFETY: if the type is instantiated, rustc already ensures that its
@@ -472,6 +475,8 @@ impl Layout {
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")]
     #[inline]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * mem::size_of::<T>())]
+    #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == mem::align_of::<T>())]
     pub const fn array<T>(n: usize) -> Result<Self, LayoutError> {
         // Reduce the amount of code we need to monomorphize per `T`.
         return inner(mem::size_of::<T>(), Alignment::of::<T>(), n);
@@ -538,6 +543,13 @@ impl fmt::Display for LayoutError {
 mod verify {
     use super::*;
 
+    impl kani::Arbitrary for Layout {
+        fn any() -> Self {
+            let size = kani::any::<usize>();
+            unsafe { Layout { size, align: kani::any::<Alignment>() } }
+        }
+    }
+
     // pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError>
     #[kani::proof_for_contract(Layout::from_size_align)]
     pub fn check_from_size_align() {
@@ -571,21 +583,14 @@ mod verify {
     // pub const fn align(&self) -> usize
     #[kani::proof_for_contract(Layout::align)]
     pub fn check_align() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let _ = layout.align();
-        }
+        let layout = kani::any::<Layout>();
+        let _ = layout.align();
     }
 
     // pub const fn new<T>() -> Self
-    #[kani::proof]
+    #[kani::proof_for_contract(Layout::new)]
     pub fn check_new_i32() {
-        let layout = Layout::new::<i32>();
-        assert_eq!(layout.size(), 4);
-        assert!(layout.align().is_power_of_two());
+        let _ = Layout::new::<i32>();
     }
 
     // pub const fn for_value<T: ?Sized>(t: &T) -> Self
@@ -606,115 +611,69 @@ mod verify {
     // pub const fn dangling(&self) -> NonNull<u8>
     #[kani::proof_for_contract(Layout::dangling)]
     pub fn check_dangling() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let _ = layout.dangling();
-        }
+        let layout = kani::any::<Layout>();
+        let _ = layout.dangling();
     }
 
     // pub fn align_to(&self, align: usize) -> Result<Self, LayoutError>
     #[kani::proof_for_contract(Layout::align_to)]
     pub fn check_align_to() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let a2 = kani::any::<usize>();
-            let _ = layout.align_to(a2);
-        }
+        let layout = kani::any::<Layout>();
+        let a2 = kani::any::<usize>();
+        let _ = layout.align_to(a2);
     }
 
     // pub const fn padding_needed_for(&self, align: usize) -> usize
     #[kani::proof_for_contract(Layout::padding_needed_for)]
     pub fn check_padding_needed_for() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let a2 = kani::any::<usize>();
-            if(a2.is_power_of_two() && a2 <= a) {
-                let _ = layout.padding_needed_for(a2);
-            }
+        let layout = kani::any::<Layout>();
+        let a2 = kani::any::<usize>();
+        if(a2.is_power_of_two() && a2 <= layout.align()) {
+            let _ = layout.padding_needed_for(a2);
         }
     }
 
     // pub const fn pad_to_align(&self) -> Layout
     #[kani::proof_for_contract(Layout::pad_to_align)]
     pub fn check_pad_to_align() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let _ = layout.pad_to_align();
-        }
+        let layout = kani::any::<Layout>();
+        let _ = layout.pad_to_align();
     }
 
     // pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError>
     #[kani::proof_for_contract(Layout::repeat)]
     pub fn check_repeat() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let n = kani::any::<usize>();
-            let _ = layout.repeat(n);
-        }
+        let layout = kani::any::<Layout>();
+        let n = kani::any::<usize>();
+        let _ = layout.repeat(n);
     }
 
     // pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError>
     #[kani::proof_for_contract(Layout::extend)]
     pub fn check_extend() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let s2 = kani::any::<usize>();
-            let a2 = kani::any::<usize>();
-            kani::assume(Layout::from_size_align(s2, a2).is_ok());
-            let layout2 = Layout::from_size_align_unchecked(s2, a2);
-            let _ = layout.extend(layout2);
-        }
+        let layout = kani::any::<Layout>();
+        let layout2 = kani::any::<Layout>();
+        let _ = layout.extend(layout2);
     }
 
     // pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError>
     #[kani::proof_for_contract(Layout::repeat_packed)]
     pub fn check_repeat_packed() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let n = kani::any::<usize>();
-            let _ = layout.repeat_packed(n);
-        }
+        let layout = kani::any::<Layout>();
+        let n = kani::any::<usize>();
+        let _ = layout.repeat_packed(n);
     }
 
     // pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError>
     #[kani::proof_for_contract(Layout::extend_packed)]
     pub fn check_extend_packed() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        kani::assume(Layout::from_size_align(s, a).is_ok());
-        unsafe {
-            let layout = Layout::from_size_align_unchecked(s, a);
-            let s2 = kani::any::<usize>();
-            let a2 = kani::any::<usize>();
-            kani::assume(Layout::from_size_align(s2, a2).is_ok());
-            let layout2 = Layout::from_size_align_unchecked(s2, a2);
-            let _ = layout.extend_packed(layout2);
-        }
+        let layout = kani::any::<Layout>();
+        let layout2 = kani::any::<Layout>();
+        let _ = layout.extend_packed(layout2);
     }
 
     // pub const fn array<T>(n: usize) -> Result<Self, LayoutError>
-    #[kani::proof]
+    #[kani::proof_for_contract(Layout::array)]
     pub fn check_array_i32() {
         let n = kani::any::<usize>();
         if let Ok(layout) = Layout::array::<i32>(n) {

From 41635f04bc5da95378ceb7f09a7152071dd449c0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 20 Aug 2024 12:58:15 +0000
Subject: [PATCH 12/17] More on for_value, for_value_raw

---
 library/core/src/alloc/layout.rs | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 4d38c1728fda2..a947812b7d6fb 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -177,7 +177,8 @@ impl Layout {
     #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")]
     #[must_use]
     #[inline]
-    #[ensures(|result| result.align().is_power_of_two())]
+    #[requires(mem::align_of_val(t).is_power_of_two())]
+    #[ensures(|result| result.align() == mem::align_of_val(t))]
     pub const fn for_value<T: ?Sized>(t: &T) -> Self {
         let (size, align) = (mem::size_of_val(t), mem::align_of_val(t));
         // SAFETY: see rationale in `new` for why this is using the unsafe variant
@@ -596,15 +597,23 @@ mod verify {
     // pub const fn for_value<T: ?Sized>(t: &T) -> Self
     #[kani::proof_for_contract(Layout::for_value)]
     pub fn check_for_value_i32() {
+        let x = kani::any::<i32>();
+        let _ = Layout::for_value::<i32>(&x);
         let array : [i32; 2] = [1, 2];
         let _ = Layout::for_value::<[i32]>(&array[1 .. 1]);
+        // TODO: the case of a trait object as unsized tail is not yet covered
+        // TODO: the case of an extern type as unsized tail is not yet covered
     }
 
     // pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self
     #[kani::proof_for_contract(Layout::for_value_raw)]
     pub fn check_for_value_raw_i32() {
         unsafe {
+            let x = kani::any::<i32>();
+            let _ = Layout::for_value_raw::<i32>(&x as *const i32);
             let _ = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
+            // TODO: the case of a trait object as unsized tail is not yet covered
+            // TODO: the case of an extern type as unsized tail is not yet covered
         }
     }
 

From 10493b5d92529bab13d3f9f2312185c6e1595ed5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 20 Aug 2024 13:08:01 +0000
Subject: [PATCH 13/17] add size constraints

---
 library/core/src/alloc/layout.rs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index a947812b7d6fb..b23ed074c1c66 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -546,8 +546,9 @@ mod verify {
 
     impl kani::Arbitrary for Layout {
         fn any() -> Self {
-            let size = kani::any::<usize>();
-            unsafe { Layout { size, align: kani::any::<Alignment>() } }
+            let align = kani::any::<Alignment>();
+            let size = kani::any_where(|s: &usize| *s <= isize::MAX as usize - (align.as_usize() - 1));
+            unsafe { Layout { size, align } }
         }
     }
 

From c5345295114010af7d16977ac58c90b5538114b4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Wed, 21 Aug 2024 12:06:14 +0200
Subject: [PATCH 14/17] Update library/core/src/alloc/layout.rs

Co-authored-by: Celina G. Val <celinval@amazon.com>
---
 library/core/src/alloc/layout.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index b23ed074c1c66..f8830ec437fad 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -346,8 +346,8 @@ impl Layout {
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
     // the below modulo operation might be too costly to prove
-    // #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0)]
-    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size())]
+    #[cfg_attr(not(kani), ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0))]
+    #[cfg_attr(kani, ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size()))]
     // the below multiplication might be too costly to prove at this time
     // #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]
     // use the weaker statement below for now

From e1c598c0800d321cd002710a5cdc229b249ad766 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 21 Aug 2024 10:49:03 +0000
Subject: [PATCH 15/17] Cleanup contracts

---
 library/core/src/alloc/layout.rs | 40 +++++++++++++++++++++-----------
 1 file changed, 27 insertions(+), 13 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index f8830ec437fad..55aed720e5145 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -215,6 +215,9 @@ impl Layout {
     #[unstable(feature = "layout_for_ptr", issue = "69835")]
     #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")]
     #[must_use]
+    // TODO: we should try to capture the above constraints on T in a `requires` clause, and the
+    // metadata helpers from https://github.com/model-checking/verify-rust-std/pull/37 may be able
+    // to accomplish this.
     #[ensures(|result| result.align().is_power_of_two())]
     pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self {
         // SAFETY: we pass along the prerequisites of these functions to the caller
@@ -345,13 +348,20 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    // the below modulo operation might be too costly to prove
-    #[cfg_attr(not(kani), ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0))]
-    #[cfg_attr(kani, ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size()))]
-    // the below multiplication might be too costly to prove at this time
-    // #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]
-    // use the weaker statement below for now
-    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= result.as_ref().unwrap().1)]
+    // for Kani (v0.54.0), the below modulo operation is too costly to prove (running into the
+    // 6-hours timeout on GitHub); we use a weaker postcondition instead
+    #[cfg_attr(not(kani),
+        ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0))]
+    #[cfg_attr(kani,
+        ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size()))]
+    // for Kani (v0.54.0), the below multiplication is too costly to prove (running into the
+    // 6-hours timeout on GitHub); we use a weaker postcondition instead
+    #[cfg_attr(not(kani),
+        ensures(|result| result.is_err() ||
+            result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1))]
+    #[cfg_attr(kani,
+        ensures(|result| result.is_err() || n == 0 ||
+            result.as_ref().unwrap().0.size() >= result.as_ref().unwrap().1))]
     pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
         // This cannot overflow. Quoting from the invariant of Layout:
         // > `size`, when rounded up to the nearest multiple of `align`,
@@ -442,10 +452,12 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    // the below multiplication might be too costly to prove at this time
-    // #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size())]
-    // use the weaker statement below for now
-    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().size() >= self.size())]
+    // for Kani (v0.54.0), the below multiplication is too costly to prove (running into the
+    // 6-hours timeout on GitHub); we use a weaker postcondition instead
+    #[cfg_attr(not(kani),
+        ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size()))]
+    #[cfg_attr(kani,
+        ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().size() >= self.size()))]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
     pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
         let size = self.size().checked_mul(n).ok_or(LayoutError)?;
@@ -602,7 +614,8 @@ mod verify {
         let _ = Layout::for_value::<i32>(&x);
         let array : [i32; 2] = [1, 2];
         let _ = Layout::for_value::<[i32]>(&array[1 .. 1]);
-        // TODO: the case of a trait object as unsized tail is not yet covered
+        let trait_ref: &dyn core::fmt::Debug = &x;
+        let _ = Layout::for_value::<dyn core::fmt::Debug>(trait_ref);
         // TODO: the case of an extern type as unsized tail is not yet covered
     }
 
@@ -613,7 +626,8 @@ mod verify {
             let x = kani::any::<i32>();
             let _ = Layout::for_value_raw::<i32>(&x as *const i32);
             let _ = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
-            // TODO: the case of a trait object as unsized tail is not yet covered
+            let trait_ref: &dyn core::fmt::Debug = &x;
+            let _ = Layout::for_value_raw::<dyn core::fmt::Debug>(trait_ref);
             // TODO: the case of an extern type as unsized tail is not yet covered
         }
     }

From 80134173fcf9df05e247c08409f5b8d820464e47 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 16 Sep 2024 09:13:11 +0000
Subject: [PATCH 16/17] Try to use Invariant

---
 library/core/src/alloc/layout.rs | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 72c5f7fe3f60b..dd29054b6fe5f 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -166,7 +166,6 @@ impl Layout {
                   without modifying the layout"]
     #[inline]
     #[rustc_allow_const_fn_unstable(ptr_alignment_type)]
-    #[ensures(|result| result.is_power_of_two())]
     pub const fn align(&self) -> usize {
         self.align.as_usize()
     }
@@ -176,7 +175,6 @@ impl Layout {
     #[rustc_const_stable(feature = "alloc_layout_const_new", since = "1.42.0")]
     #[must_use]
     #[inline]
-    #[requires(mem::align_of::<T>().is_power_of_two())]
     #[ensures(|result| result.size() == mem::size_of::<T>())]
     #[ensures(|result| result.align() == mem::align_of::<T>())]
     pub const fn new<T>() -> Self {
@@ -235,7 +233,8 @@ impl Layout {
     // TODO: we should try to capture the above constraints on T in a `requires` clause, and the
     // metadata helpers from https://github.com/model-checking/verify-rust-std/pull/37 may be able
     // to accomplish this.
-    #[ensures(|result| result.align().is_power_of_two())]
+    #[cfg_attr(not(kani), ensures(|result| result.align().is_power_of_two()))]
+    #[cfg_attr(kani, ensures(|result| result.is_safe()))]
     pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self {
         // SAFETY: we pass along the prerequisites of these functions to the caller
         let (size, align) = unsafe { (mem::size_of_val_raw(t), mem::align_of_val_raw(t)) };
@@ -581,6 +580,12 @@ mod verify {
         }
     }
 
+    impl kani::Invariant for Layout {
+        fn is_safe(&self) -> bool {
+            self.align.as_usize().is_power_of_two()
+        }
+    }
+
     // pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError>
     #[kani::proof_for_contract(Layout::from_size_align)]
     pub fn check_from_size_align() {
@@ -612,10 +617,10 @@ mod verify {
     }
 
     // pub const fn align(&self) -> usize
-    #[kani::proof_for_contract(Layout::align)]
+    #[kani::proof]
     pub fn check_align() {
         let layout = kani::any::<Layout>();
-        let _ = layout.align();
+        assert!(layout.align().is_power_of_two());
     }
 
     // pub const fn new<T>() -> Self

From 2e44a57329d766a401367eb7b37e97375297cf37 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 2 Oct 2024 19:13:29 +0000
Subject: [PATCH 17/17] Revert "Try to use Invariant"

This reverts commit 80134173fcf9df05e247c08409f5b8d820464e47.
---
 library/core/src/alloc/layout.rs | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index dd29054b6fe5f..666c5be7c29b5 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -233,8 +233,7 @@ impl Layout {
     // TODO: we should try to capture the above constraints on T in a `requires` clause, and the
     // metadata helpers from https://github.com/model-checking/verify-rust-std/pull/37 may be able
     // to accomplish this.
-    #[cfg_attr(not(kani), ensures(|result| result.align().is_power_of_two()))]
-    #[cfg_attr(kani, ensures(|result| result.is_safe()))]
+    #[ensures(|result| result.align().is_power_of_two())]
     pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self {
         // SAFETY: we pass along the prerequisites of these functions to the caller
         let (size, align) = unsafe { (mem::size_of_val_raw(t), mem::align_of_val_raw(t)) };
@@ -580,12 +579,6 @@ mod verify {
         }
     }
 
-    impl kani::Invariant for Layout {
-        fn is_safe(&self) -> bool {
-            self.align.as_usize().is_power_of_two()
-        }
-    }
-
     // pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError>
     #[kani::proof_for_contract(Layout::from_size_align)]
     pub fn check_from_size_align() {