From fe4ba8899568e0493433ca8be9562e9e17903902 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 20 Aug 2024 11:53:44 +0000
Subject: [PATCH] Add contract to of<T>

---
 library/core/src/ptr/alignment.rs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
index 36063989a350c..d51f2ef7edff3 100644
--- a/library/core/src/ptr/alignment.rs
+++ b/library/core/src/ptr/alignment.rs
@@ -48,6 +48,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[requires(mem::align_of::<T>().is_power_of_two())]
+    #[ensures(|result| result.as_usize().is_power_of_two())]
     pub const fn of<T>() -> Self {
         // SAFETY: rustc ensures that type alignment is always a power of two.
         unsafe { Alignment::new_unchecked(mem::align_of::<T>()) }
@@ -396,10 +398,9 @@ mod verify {
     }
 
     // pub const fn of<T>() -> Self
-    #[kani::proof]
+    #[kani::proof_for_contract(Alignment::of)]
     pub fn check_of_i32() {
-        let alignment = Alignment::of::<i32>();
-        assert!(alignment.as_usize().is_power_of_two());
+        let _ = Alignment::of::<i32>();
     }
 
     // pub const fn new(align: usize) -> Option<Self>