From 1ae4c6d4958e43bda11562e832d9a28b930ba7a6 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Tue, 10 Sep 2024 17:11:15 -0700
Subject: [PATCH 01/42] Add Kani proofs of unchecked_add for all integer types

---
 .../core/tests/num/kani-proofs/i128-proofs.rs | 23 +++++++++++++++++++
 .../core/tests/num/kani-proofs/i16-proofs.rs  | 23 +++++++++++++++++++
 .../core/tests/num/kani-proofs/i32-proofs.rs  | 23 +++++++++++++++++++
 .../core/tests/num/kani-proofs/i64-proofs.rs  | 23 +++++++++++++++++++
 .../core/tests/num/kani-proofs/i8-proofs.rs   | 23 +++++++++++++++++++
 .../core/tests/num/kani-proofs/u128-proofs.rs | 21 +++++++++++++++++
 .../core/tests/num/kani-proofs/u16-proofs.rs  | 21 +++++++++++++++++
 .../core/tests/num/kani-proofs/u32-proofs.rs  | 21 +++++++++++++++++
 .../core/tests/num/kani-proofs/u64-proofs.rs  | 21 +++++++++++++++++
 .../core/tests/num/kani-proofs/u8-proofs.rs   | 21 +++++++++++++++++
 10 files changed, 220 insertions(+)
 create mode 100644 library/core/tests/num/kani-proofs/i128-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/i16-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/i32-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/i64-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/i8-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/u128-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/u16-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/u32-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/u64-proofs.rs
 create mode 100644 library/core/tests/num/kani-proofs/u8-proofs.rs

diff --git a/library/core/tests/num/kani-proofs/i128-proofs.rs b/library/core/tests/num/kani-proofs/i128-proofs.rs
new file mode 100644
index 0000000000000..279d8f26ff947
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/i128-proofs.rs
@@ -0,0 +1,23 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_i128_unchecked_add() {
+       let num1: i128 = kani::any::<i128>();
+       let num2: i128 = kani::any::<i128>();
+
+       // Safety preconditions:
+       // - Positive number addition won't overflow
+       // - Negative number addition won't underflow
+       // Addition of two integers with different signs never overflows
+       // Undefined behavior occurs when overflow or underflow happens
+       kani::assume((num1 > 0 && num2 > 0 && num1 < i128::MAX - num2)
+                    || (num1 < 0 && num2 < 0 && num1 > i128::MIN - num2));
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/i16-proofs.rs b/library/core/tests/num/kani-proofs/i16-proofs.rs
new file mode 100644
index 0000000000000..d946148d78976
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/i16-proofs.rs
@@ -0,0 +1,23 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_i16_unchecked_add() {
+       let num1: i16 = kani::any::<i16>();
+       let num2: i16 = kani::any::<i16>();
+
+       // Safety preconditions:
+       // - Positive number addition won't overflow
+       // - Negative number addition won't underflow
+       // Addition of two integers with different signs never overflows
+       // Undefined behavior occurs when overflow or underflow happens
+       kani::assume((num1 > 0 && num2 > 0 && num1 < i16::MAX - num2)
+                    || (num1 < 0 && num2 < 0 && num1 > i16::MIN - num2));
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/i32-proofs.rs b/library/core/tests/num/kani-proofs/i32-proofs.rs
new file mode 100644
index 0000000000000..bb2d542dbc38f
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/i32-proofs.rs
@@ -0,0 +1,23 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_i32_unchecked_add() {
+       let num1: i32 = kani::any::<i32>();
+       let num2: i32 = kani::any::<i32>();
+
+       // Safety preconditions:
+       // - Positive number addition won't overflow
+       // - Negative number addition won't underflow
+       // Addition of two integers with different signs never overflows
+       // Undefined behavior occurs when overflow or underflow happens
+       kani::assume((num1 > 0 && num2 > 0 && num1 < i32::MAX - num2)
+                    || (num1 < 0 && num2 < 0 && num1 > i32::MIN - num2));
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/i64-proofs.rs b/library/core/tests/num/kani-proofs/i64-proofs.rs
new file mode 100644
index 0000000000000..822bac06eb733
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/i64-proofs.rs
@@ -0,0 +1,23 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_i64_unchecked_add() {
+       let num1: i64 = kani::any::<i64>();
+       let num2: i64 = kani::any::<i64>();
+
+       // Safety preconditions:
+       // - Positive number addition won't overflow
+       // - Negative number addition won't underflow
+       // Addition of two integers with different signs never overflows
+       // Undefined behavior occurs when overflow or underflow happens
+       kani::assume((num1 > 0 && num2 > 0 && num1 < i64::MAX - num2)
+                    || (num1 < 0 && num2 < 0 && num1 > i64::MIN - num2));
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs
new file mode 100644
index 0000000000000..edc3522f42be3
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/i8-proofs.rs
@@ -0,0 +1,23 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_i8_unchecked_add() {
+       let num1: i8 = kani::any::<i8>();
+       let num2: i8 = kani::any::<i8>();
+
+       // Safety preconditions:
+       // - Positive number addition won't overflow
+       // - Negative number addition won't underflow
+       // Addition of two integers with different signs never overflows
+       // Undefined behavior occurs when overflow or underflow happens
+       kani::assume((num1 > 0 && num2 > 0 && num1 < i8::MAX - num2)
+                    || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2));
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/u128-proofs.rs b/library/core/tests/num/kani-proofs/u128-proofs.rs
new file mode 100644
index 0000000000000..98d781ec024b5
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/u128-proofs.rs
@@ -0,0 +1,21 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_u128_unchecked_add() {
+       let num1: u128 = kani::any::<u128>();
+       let num2: u128 = kani::any::<u128>();
+
+       // Safety preconditions:
+       // - Addition won't overflow
+       // Unsigned integers are always positive, so underflow won't happen
+       // Undefined behavior occurs when overflow happens
+       kani::assume(num1 < u128::MAX - num2);
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/u16-proofs.rs b/library/core/tests/num/kani-proofs/u16-proofs.rs
new file mode 100644
index 0000000000000..9dfff81d1abbb
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/u16-proofs.rs
@@ -0,0 +1,21 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_u16_unchecked_add() {
+       let num1: u16 = kani::any::<u16>();
+       let num2: u16 = kani::any::<u16>();
+
+       // Safety preconditions:
+       // - Addition won't overflow
+       // Unsigned integers are always positive, so underflow won't happen
+       // Undefined behavior occurs when overflow happens
+       kani::assume(num1 < u16::MAX - num2);
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/u32-proofs.rs b/library/core/tests/num/kani-proofs/u32-proofs.rs
new file mode 100644
index 0000000000000..0d13bdcd2dce0
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/u32-proofs.rs
@@ -0,0 +1,21 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_u32_unchecked_add() {
+       let num1: u32 = kani::any::<u32>();
+       let num2: u32 = kani::any::<u32>();
+
+       // Safety preconditions:
+       // - Addition won't overflow
+       // Unsigned integers are always positive, so underflow won't happen
+       // Undefined behavior occurs when overflow happens
+       kani::assume(num1 < u32::MAX - num2);
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/u64-proofs.rs b/library/core/tests/num/kani-proofs/u64-proofs.rs
new file mode 100644
index 0000000000000..405468c96e0ba
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/u64-proofs.rs
@@ -0,0 +1,21 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_u64_unchecked_add() {
+       let num1: u64 = kani::any::<u64>();
+       let num2: u64 = kani::any::<u64>();
+
+       // Safety preconditions:
+       // - Addition won't overflow
+       // Unsigned integers are always positive, so underflow won't happen
+       // Undefined behavior occurs when overflow happens
+       kani::assume(num1 < u64::MAX - num2);
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file
diff --git a/library/core/tests/num/kani-proofs/u8-proofs.rs b/library/core/tests/num/kani-proofs/u8-proofs.rs
new file mode 100644
index 0000000000000..89826fc292c4b
--- /dev/null
+++ b/library/core/tests/num/kani-proofs/u8-proofs.rs
@@ -0,0 +1,21 @@
+#[cfg(kani)]
+mod verification {
+   // use super::*;
+
+   #[kani::proof]
+   fn verify_u8_unchecked_add() {
+       let num1: u8 = kani::any::<u8>();
+       let num2: u8 = kani::any::<u8>();
+
+       // Safety preconditions:
+       // - Addition won't overflow
+       // Unsigned integers are always positive, so underflow won't happen
+       // Undefined behavior occurs when overflow happens
+       kani::assume(num1 < u8::MAX - num2);
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+            assert_eq!(Some(result), num1.checked_add(num2));
+        }
+   }
+}
\ No newline at end of file

From b553678c11aec836a9cc0aba1db0cc473a70fc03 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Tue, 10 Sep 2024 21:07:15 -0700
Subject: [PATCH 02/42] Format proof files & Add verification function
 templates

---
 .../core/tests/num/kani-proofs/i128-proofs.rs | 55 ++++++++++++++-----
 .../core/tests/num/kani-proofs/i16-proofs.rs  | 55 ++++++++++++++-----
 .../core/tests/num/kani-proofs/i32-proofs.rs  | 55 ++++++++++++++-----
 .../core/tests/num/kani-proofs/i64-proofs.rs  | 55 ++++++++++++++-----
 .../core/tests/num/kani-proofs/i8-proofs.rs   | 55 ++++++++++++++-----
 .../core/tests/num/kani-proofs/u128-proofs.rs | 49 +++++++++++++----
 .../core/tests/num/kani-proofs/u16-proofs.rs  | 49 +++++++++++++----
 .../core/tests/num/kani-proofs/u32-proofs.rs  | 49 +++++++++++++----
 .../core/tests/num/kani-proofs/u64-proofs.rs  | 49 +++++++++++++----
 .../core/tests/num/kani-proofs/u8-proofs.rs   | 49 +++++++++++++----
 10 files changed, 390 insertions(+), 130 deletions(-)

diff --git a/library/core/tests/num/kani-proofs/i128-proofs.rs b/library/core/tests/num/kani-proofs/i128-proofs.rs
index 279d8f26ff947..4ac03ec8714fe 100644
--- a/library/core/tests/num/kani-proofs/i128-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i128-proofs.rs
@@ -1,23 +1,50 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_i128_unchecked_add() {
-       let num1: i128 = kani::any::<i128>();
-       let num2: i128 = kani::any::<i128>();
+    #[kani::proof]
+    fn verify_i128_unchecked_add() {
+        let num1: i128 = kani::any::<i128>();
+        let num2: i128 = kani::any::<i128>();
 
-       // Safety preconditions:
-       // - Positive number addition won't overflow
-       // - Negative number addition won't underflow
-       // Addition of two integers with different signs never overflows
-       // Undefined behavior occurs when overflow or underflow happens
-       kani::assume((num1 > 0 && num2 > 0 && num1 < i128::MAX - num2)
-                    || (num1 < 0 && num2 < 0 && num1 > i128::MIN - num2));
+        // Safety preconditions:
+        // - Positive number addition won't overflow
+        // - Negative number addition won't underflow
+        // Addition of two integers with different signs never overflows
+        // Undefined behavior occurs when overflow or underflow happens
+        kani::assume(
+            (num1 > 0 && num2 > 0 && num1 < i128::MAX - num2)
+                || (num1 < 0 && num2 < 0 && num1 > i128::MIN - num2),
+        );
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_i128_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i128_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i128_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i128_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i128_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/i16-proofs.rs b/library/core/tests/num/kani-proofs/i16-proofs.rs
index d946148d78976..f57591f6b8e07 100644
--- a/library/core/tests/num/kani-proofs/i16-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i16-proofs.rs
@@ -1,23 +1,50 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_i16_unchecked_add() {
-       let num1: i16 = kani::any::<i16>();
-       let num2: i16 = kani::any::<i16>();
+    #[kani::proof]
+    fn verify_i16_unchecked_add() {
+        let num1: i16 = kani::any::<i16>();
+        let num2: i16 = kani::any::<i16>();
 
-       // Safety preconditions:
-       // - Positive number addition won't overflow
-       // - Negative number addition won't underflow
-       // Addition of two integers with different signs never overflows
-       // Undefined behavior occurs when overflow or underflow happens
-       kani::assume((num1 > 0 && num2 > 0 && num1 < i16::MAX - num2)
-                    || (num1 < 0 && num2 < 0 && num1 > i16::MIN - num2));
+        // Safety preconditions:
+        // - Positive number addition won't overflow
+        // - Negative number addition won't underflow
+        // Addition of two integers with different signs never overflows
+        // Undefined behavior occurs when overflow or underflow happens
+        kani::assume(
+            (num1 > 0 && num2 > 0 && num1 < i16::MAX - num2)
+                || (num1 < 0 && num2 < 0 && num1 > i16::MIN - num2),
+        );
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_i16_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i16_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i16_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i16_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i16_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/i32-proofs.rs b/library/core/tests/num/kani-proofs/i32-proofs.rs
index bb2d542dbc38f..0c8cca6a8d9c0 100644
--- a/library/core/tests/num/kani-proofs/i32-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i32-proofs.rs
@@ -1,23 +1,50 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_i32_unchecked_add() {
-       let num1: i32 = kani::any::<i32>();
-       let num2: i32 = kani::any::<i32>();
+    #[kani::proof]
+    fn verify_i32_unchecked_add() {
+        let num1: i32 = kani::any::<i32>();
+        let num2: i32 = kani::any::<i32>();
 
-       // Safety preconditions:
-       // - Positive number addition won't overflow
-       // - Negative number addition won't underflow
-       // Addition of two integers with different signs never overflows
-       // Undefined behavior occurs when overflow or underflow happens
-       kani::assume((num1 > 0 && num2 > 0 && num1 < i32::MAX - num2)
-                    || (num1 < 0 && num2 < 0 && num1 > i32::MIN - num2));
+        // Safety preconditions:
+        // - Positive number addition won't overflow
+        // - Negative number addition won't underflow
+        // Addition of two integers with different signs never overflows
+        // Undefined behavior occurs when overflow or underflow happens
+        kani::assume(
+            (num1 > 0 && num2 > 0 && num1 < i32::MAX - num2)
+                || (num1 < 0 && num2 < 0 && num1 > i32::MIN - num2),
+        );
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_i32_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i32_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i32_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i32_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i32_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/i64-proofs.rs b/library/core/tests/num/kani-proofs/i64-proofs.rs
index 822bac06eb733..658956c110dd8 100644
--- a/library/core/tests/num/kani-proofs/i64-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i64-proofs.rs
@@ -1,23 +1,50 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_i64_unchecked_add() {
-       let num1: i64 = kani::any::<i64>();
-       let num2: i64 = kani::any::<i64>();
+    #[kani::proof]
+    fn verify_i64_unchecked_add() {
+        let num1: i64 = kani::any::<i64>();
+        let num2: i64 = kani::any::<i64>();
 
-       // Safety preconditions:
-       // - Positive number addition won't overflow
-       // - Negative number addition won't underflow
-       // Addition of two integers with different signs never overflows
-       // Undefined behavior occurs when overflow or underflow happens
-       kani::assume((num1 > 0 && num2 > 0 && num1 < i64::MAX - num2)
-                    || (num1 < 0 && num2 < 0 && num1 > i64::MIN - num2));
+        // Safety preconditions:
+        // - Positive number addition won't overflow
+        // - Negative number addition won't underflow
+        // Addition of two integers with different signs never overflows
+        // Undefined behavior occurs when overflow or underflow happens
+        kani::assume(
+            (num1 > 0 && num2 > 0 && num1 < i64::MAX - num2)
+                || (num1 < 0 && num2 < 0 && num1 > i64::MIN - num2),
+        );
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_i64_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i64_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i64_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i64_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i64_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs
index edc3522f42be3..932407510ffda 100644
--- a/library/core/tests/num/kani-proofs/i8-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i8-proofs.rs
@@ -1,23 +1,50 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_i8_unchecked_add() {
-       let num1: i8 = kani::any::<i8>();
-       let num2: i8 = kani::any::<i8>();
+    #[kani::proof]
+    fn verify_i8_unchecked_add() {
+        let num1: i8 = kani::any::<i8>();
+        let num2: i8 = kani::any::<i8>();
 
-       // Safety preconditions:
-       // - Positive number addition won't overflow
-       // - Negative number addition won't underflow
-       // Addition of two integers with different signs never overflows
-       // Undefined behavior occurs when overflow or underflow happens
-       kani::assume((num1 > 0 && num2 > 0 && num1 < i8::MAX - num2)
-                    || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2));
+        // Safety preconditions:
+        // - Positive number addition won't overflow
+        // - Negative number addition won't underflow
+        // Addition of two integers with different signs never overflows
+        // Undefined behavior occurs when overflow or underflow happens
+        kani::assume(
+            (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2)
+                || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2),
+        );
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_i8_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i8_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i8_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i8_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_i8_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/u128-proofs.rs b/library/core/tests/num/kani-proofs/u128-proofs.rs
index 98d781ec024b5..4746ba6f6149d 100644
--- a/library/core/tests/num/kani-proofs/u128-proofs.rs
+++ b/library/core/tests/num/kani-proofs/u128-proofs.rs
@@ -1,21 +1,46 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_u128_unchecked_add() {
-       let num1: u128 = kani::any::<u128>();
-       let num2: u128 = kani::any::<u128>();
+    #[kani::proof]
+    fn verify_u128_unchecked_add() {
+        let num1: u128 = kani::any::<u128>();
+        let num2: u128 = kani::any::<u128>();
 
-       // Safety preconditions:
-       // - Addition won't overflow
-       // Unsigned integers are always positive, so underflow won't happen
-       // Undefined behavior occurs when overflow happens
-       kani::assume(num1 < u128::MAX - num2);
+        // Safety preconditions:
+        // - Addition won't overflow
+        // Unsigned integers are always positive, so underflow won't happen
+        // Undefined behavior occurs when overflow happens
+        kani::assume(num1 < u128::MAX - num2);
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_u128_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u128_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u128_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u128_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u128_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/u16-proofs.rs b/library/core/tests/num/kani-proofs/u16-proofs.rs
index 9dfff81d1abbb..c398cc0ee474b 100644
--- a/library/core/tests/num/kani-proofs/u16-proofs.rs
+++ b/library/core/tests/num/kani-proofs/u16-proofs.rs
@@ -1,21 +1,46 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_u16_unchecked_add() {
-       let num1: u16 = kani::any::<u16>();
-       let num2: u16 = kani::any::<u16>();
+    #[kani::proof]
+    fn verify_u16_unchecked_add() {
+        let num1: u16 = kani::any::<u16>();
+        let num2: u16 = kani::any::<u16>();
 
-       // Safety preconditions:
-       // - Addition won't overflow
-       // Unsigned integers are always positive, so underflow won't happen
-       // Undefined behavior occurs when overflow happens
-       kani::assume(num1 < u16::MAX - num2);
+        // Safety preconditions:
+        // - Addition won't overflow
+        // Unsigned integers are always positive, so underflow won't happen
+        // Undefined behavior occurs when overflow happens
+        kani::assume(num1 < u16::MAX - num2);
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_u16_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u16_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u16_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u16_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u16_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/u32-proofs.rs b/library/core/tests/num/kani-proofs/u32-proofs.rs
index 0d13bdcd2dce0..8f4dfb17949a5 100644
--- a/library/core/tests/num/kani-proofs/u32-proofs.rs
+++ b/library/core/tests/num/kani-proofs/u32-proofs.rs
@@ -1,21 +1,46 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_u32_unchecked_add() {
-       let num1: u32 = kani::any::<u32>();
-       let num2: u32 = kani::any::<u32>();
+    #[kani::proof]
+    fn verify_u32_unchecked_add() {
+        let num1: u32 = kani::any::<u32>();
+        let num2: u32 = kani::any::<u32>();
 
-       // Safety preconditions:
-       // - Addition won't overflow
-       // Unsigned integers are always positive, so underflow won't happen
-       // Undefined behavior occurs when overflow happens
-       kani::assume(num1 < u32::MAX - num2);
+        // Safety preconditions:
+        // - Addition won't overflow
+        // Unsigned integers are always positive, so underflow won't happen
+        // Undefined behavior occurs when overflow happens
+        kani::assume(num1 < u32::MAX - num2);
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_u32_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u32_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u32_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u32_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u32_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/u64-proofs.rs b/library/core/tests/num/kani-proofs/u64-proofs.rs
index 405468c96e0ba..d65c6f9178857 100644
--- a/library/core/tests/num/kani-proofs/u64-proofs.rs
+++ b/library/core/tests/num/kani-proofs/u64-proofs.rs
@@ -1,21 +1,46 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_u64_unchecked_add() {
-       let num1: u64 = kani::any::<u64>();
-       let num2: u64 = kani::any::<u64>();
+    #[kani::proof]
+    fn verify_u64_unchecked_add() {
+        let num1: u64 = kani::any::<u64>();
+        let num2: u64 = kani::any::<u64>();
 
-       // Safety preconditions:
-       // - Addition won't overflow
-       // Unsigned integers are always positive, so underflow won't happen
-       // Undefined behavior occurs when overflow happens
-       kani::assume(num1 < u64::MAX - num2);
+        // Safety preconditions:
+        // - Addition won't overflow
+        // Unsigned integers are always positive, so underflow won't happen
+        // Undefined behavior occurs when overflow happens
+        kani::assume(num1 < u64::MAX - num2);
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_u64_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u64_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u64_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u64_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u64_unchecked_neg() {
+        // TODO
+    }
+}
diff --git a/library/core/tests/num/kani-proofs/u8-proofs.rs b/library/core/tests/num/kani-proofs/u8-proofs.rs
index 89826fc292c4b..ef6569ceaa3ba 100644
--- a/library/core/tests/num/kani-proofs/u8-proofs.rs
+++ b/library/core/tests/num/kani-proofs/u8-proofs.rs
@@ -1,21 +1,46 @@
 #[cfg(kani)]
 mod verification {
-   // use super::*;
+    // use super::*;
 
-   #[kani::proof]
-   fn verify_u8_unchecked_add() {
-       let num1: u8 = kani::any::<u8>();
-       let num2: u8 = kani::any::<u8>();
+    #[kani::proof]
+    fn verify_u8_unchecked_add() {
+        let num1: u8 = kani::any::<u8>();
+        let num2: u8 = kani::any::<u8>();
 
-       // Safety preconditions:
-       // - Addition won't overflow
-       // Unsigned integers are always positive, so underflow won't happen
-       // Undefined behavior occurs when overflow happens
-       kani::assume(num1 < u8::MAX - num2);
+        // Safety preconditions:
+        // - Addition won't overflow
+        // Unsigned integers are always positive, so underflow won't happen
+        // Undefined behavior occurs when overflow happens
+        kani::assume(num1 < u8::MAX - num2);
 
         unsafe {
             let result = num1.unchecked_add(num2);
             assert_eq!(Some(result), num1.checked_add(num2));
         }
-   }
-}
\ No newline at end of file
+    }
+
+    #[kani::proof]
+    fn verify_u8_unchecked_sub() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u8_unchecked_mul() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u8_unchecked_shl() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u8_unchecked_shr() {
+        // TODO
+    }
+
+    #[kani::proof]
+    fn verify_u8_unchecked_neg() {
+        // TODO
+    }
+}

From 4db34e48f01294fcda6aa07bc21d0b268d3b951e Mon Sep 17 00:00:00 2001
From: MWDZ <jinjunfeng721@gmail.com>
Date: Wed, 11 Sep 2024 11:19:15 -0700
Subject: [PATCH 03/42] feat: add i8 uncheck shl verification

---
 library/core/tests/num/kani-proofs/i8-proofs.rs | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs
index 932407510ffda..b609bfb2335c0 100644
--- a/library/core/tests/num/kani-proofs/i8-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i8-proofs.rs
@@ -1,3 +1,4 @@
+#![feature(unchecked_shifts)]
 #[cfg(kani)]
 mod verification {
     // use super::*;
@@ -35,7 +36,16 @@ mod verification {
 
     #[kani::proof]
     fn verify_i8_unchecked_shl() {
-        // TODO
+        let num: i8 = kani::any::<i8>(); // Any value in type i8
+        let shift_amount: u32 = kani::any::<u32>(); // Any shift amount in type u32
+
+        // Assume the shift value is smaller than 8 because i8 only has 8 digits
+        kani::assume(shift_amount < 8);
+
+        unsafe {
+            let result = num.unchecked_shl(shift_amount);
+            assert_eq!(Some(result), num.checked_shl(shift_amount));
+        }
     }
 
     #[kani::proof]

From 54f550769076c522040bada869c4de27157342f1 Mon Sep 17 00:00:00 2001
From: MWDZ <jinjunfeng721@gmail.com>
Date: Wed, 11 Sep 2024 11:54:55 -0700
Subject: [PATCH 04/42] feat: add i16 and i32 uncheck shl verification

---
 library/core/tests/num/kani-proofs/i16-proofs.rs | 12 +++++++++++-
 library/core/tests/num/kani-proofs/i32-proofs.rs | 13 ++++++++++++-
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/library/core/tests/num/kani-proofs/i16-proofs.rs b/library/core/tests/num/kani-proofs/i16-proofs.rs
index f57591f6b8e07..1958805372bca 100644
--- a/library/core/tests/num/kani-proofs/i16-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i16-proofs.rs
@@ -1,3 +1,4 @@
+#![feature(unchecked_shifts)]
 #[cfg(kani)]
 mod verification {
     // use super::*;
@@ -35,7 +36,16 @@ mod verification {
 
     #[kani::proof]
     fn verify_i16_unchecked_shl() {
-        // TODO
+        let num: i16 = kani::any::<i16>(); // Any value in type i16
+        let shift_amount: u32 = kani::any::<u32>(); // Any shift amount in type u32
+    
+        // Assume the shift value is smaller than 16 because i16 only has 16 bits
+        kani::assume(shift_amount < 16);
+    
+        unsafe {
+            let result = num.unchecked_shl(shift_amount);
+            assert_eq!(Some(result), num.checked_shl(shift_amount));
+        }
     }
 
     #[kani::proof]
diff --git a/library/core/tests/num/kani-proofs/i32-proofs.rs b/library/core/tests/num/kani-proofs/i32-proofs.rs
index 0c8cca6a8d9c0..d2bce7b845002 100644
--- a/library/core/tests/num/kani-proofs/i32-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i32-proofs.rs
@@ -1,3 +1,5 @@
+#![feature(unchecked_shifts)]
+
 #[cfg(kani)]
 mod verification {
     // use super::*;
@@ -30,7 +32,16 @@ mod verification {
 
     #[kani::proof]
     fn verify_i32_unchecked_mul() {
-        // TODO
+        let num: i32 = kani::any::<i32>(); // Any value in type i32
+        let shift_amount: u32 = kani::any::<u32>(); // Any shift amount in type u32
+    
+        // Assume the shift value is smaller than 32 because i32 only has 32 bits
+        kani::assume(shift_amount < 32);
+    
+        unsafe {
+            let result = num.unchecked_shl(shift_amount);
+            assert_eq!(Some(result), num.checked_shl(shift_amount));
+        }
     }
 
     #[kani::proof]

From 472da0e1eaebdf55fb742414d03d3f1cdeb759a3 Mon Sep 17 00:00:00 2001
From: Lanfei Ma <99311320+lanfeima@users.noreply.github.com>
Date: Wed, 11 Sep 2024 17:31:20 -0700
Subject: [PATCH 05/42] added unsafe integer i8 unchecked sub following the
 template

---
 library/core/tests/num/kani-proofs/i8-proofs.rs | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs
index 932407510ffda..daa488a88a960 100644
--- a/library/core/tests/num/kani-proofs/i8-proofs.rs
+++ b/library/core/tests/num/kani-proofs/i8-proofs.rs
@@ -25,7 +25,22 @@ mod verification {
 
     #[kani::proof]
     fn verify_i8_unchecked_sub() {
-        // TODO
+        let num1: i8 = kani::any::<i8>();
+        let num2: i8 = kani::any::<i8>();
+    
+        // Safety preconditions:
+        // - Subtraction won't underflow when num1 is positive and num2 is negative
+        // - Subtraction won't overflow when num1 is negative and num2 is positive
+        // Undefined behavior occurs when overflow or underflow happens
+        kani::assume(
+            (num1 >= 0 && num2 <= 0 && num1 <= i8::MAX + num2)
+                || (num1 <= 0 && num2 >= 0 && num1 >= i8::MIN + num2),
+        );
+    
+        unsafe {
+            let result = num1.unchecked_sub(num2);
+            assert_eq!(Some(result), num1.checked_sub(num2));
+        }   
     }
 
     #[kani::proof]

From daaaf7e1c61c9cfad8a44912ca7b66ca6432ae86 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Mon, 16 Sep 2024 16:53:39 -0700
Subject: [PATCH 06/42] Experiment with two verification approaches in mod.rs
 of core::num

---
 library/core/src/num/mod.rs | 60 +++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 309e1ba958aee..bb4a8ca6e59c2 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1580,3 +1580,63 @@ from_str_radix_size_impl! { i16 isize, u16 usize }
 from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
+
+
+// #[feature(unchecked_math)]
+#[cfg(kani)]
+use crate::kani;
+
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Signed unchecked_add Safety preconditions:
+    // - Positive number addition won't overflow
+    // - Negative number addition won't underflow
+    // Addition of two integers with different signs never overflows
+    // Undefined behavior occurs when overflow or underflow happens
+    #[kani::requires(!num1.overflowing_add(num2).1)]
+    #[kani::ensures(|ret| *ret >= i8::MIN && *ret <= i8::MAX)]
+    fn i8_unchecked_add_wrapper(num1: i8, num2: i8) -> i8 {
+        unsafe { num1.unchecked_add(num2) }
+    }
+
+    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
+    #[kani::proof_for_contract(i8_unchecked_add_wrapper)]
+    pub fn check_unchecked_add_i8() {
+        let num1: i8 = kani::any::<i8>();
+        let num2: i8 = kani::any::<i8>();
+        
+        // kani::assume(
+        //     (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2)
+        //         || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2),
+        // );
+
+        unsafe {
+            // Kani ensures the inputs satisfy preconditions
+            i8_unchecked_add_wrapper(num1, num2);
+            // Kani ensures the output satisfy postconditions
+        }
+    }
+
+    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
+    #[kani::proof]
+    pub fn check_unchecked_add_i16() {
+        let num1: i16 = kani::any::<i16>();
+        let num2: i16 = kani::any::<i16>();
+        
+        // overflowing_add return (result, bool) where bool is if
+        // add will overflow. This check takes the boolean. 
+        kani::assume(!num1.overflowing_add(num2).1);
+
+        unsafe {
+            let result = num1.unchecked_add(num2);
+
+            // Either check result
+            assert_eq!(Some(result), num1.checked_add(num2));
+            
+            // Or check range of result
+            assert!(result >= i16::MIN && result <= i16::MAX);
+        }
+    }
+}

From 1c9dbde3758ae3889aa73ca491849c3303af0fc1 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Wed, 18 Sep 2024 14:27:27 -0700
Subject: [PATCH 07/42] Add contracts to unchecked_add && Add i8::unchecked_add
 proof

---
 library/core/src/num/int_macros.rs  |  2 ++
 library/core/src/num/mod.rs         | 37 ++---------------------------
 library/core/src/num/uint_macros.rs |  2 ++
 3 files changed, 6 insertions(+), 35 deletions(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 878a911dde50d..6e97b7999eef4 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -511,6 +511,8 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[kani::requires(!self.overflowing_add(rhs).1)]
+        #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index f5223023c8f2b..9cacb61a47030 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1596,48 +1596,15 @@ mod verify {
     // - Negative number addition won't underflow
     // Addition of two integers with different signs never overflows
     // Undefined behavior occurs when overflow or underflow happens
-    #[kani::requires(!num1.overflowing_add(num2).1)]
-    #[kani::ensures(|ret| *ret >= i8::MIN && *ret <= i8::MAX)]
-    fn i8_unchecked_add_wrapper(num1: i8, num2: i8) -> i8 {
-        unsafe { num1.unchecked_add(num2) }
-    }
 
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
-    #[kani::proof_for_contract(i8_unchecked_add_wrapper)]
+    #[kani::proof_for_contract(i8::unchecked_add)]
     pub fn check_unchecked_add_i8() {
         let num1: i8 = kani::any::<i8>();
         let num2: i8 = kani::any::<i8>();
-        
-        // kani::assume(
-        //     (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2)
-        //         || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2),
-        // );
-
-        unsafe {
-            // Kani ensures the inputs satisfy preconditions
-            i8_unchecked_add_wrapper(num1, num2);
-            // Kani ensures the output satisfy postconditions
-        }
-    }
-
-    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
-    #[kani::proof]
-    pub fn check_unchecked_add_i16() {
-        let num1: i16 = kani::any::<i16>();
-        let num2: i16 = kani::any::<i16>();
-        
-        // overflowing_add return (result, bool) where bool is if
-        // add will overflow. This check takes the boolean. 
-        kani::assume(!num1.overflowing_add(num2).1);
 
         unsafe {
-            let result = num1.unchecked_add(num2);
-
-            // Either check result
-            assert_eq!(Some(result), num1.checked_add(num2));
-            
-            // Or check range of result
-            assert!(result >= i16::MIN && result <= i16::MAX);
+            num1.unchecked_add(num2);
         }
     }
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index d9036abecc592..64d43c394e2b2 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -558,6 +558,8 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[kani::requires(!self.overflowing_add(rhs).1)]
+        #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From 894231fb15f248db0b76efab587e3c7cdb2ac1cb Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Wed, 18 Sep 2024 14:31:58 -0700
Subject: [PATCH 08/42] Format core::num mod.rs

---
 library/core/src/num/mod.rs | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 9cacb61a47030..1ebc09815717a 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1397,7 +1397,10 @@ const fn from_str_radix_panic_ct(_radix: u32) -> ! {
 
 #[track_caller]
 fn from_str_radix_panic_rt(radix: u32) -> ! {
-    panic!("from_str_radix_int: must lie in the range `[2, 36]` - found {}", radix);
+    panic!(
+        "from_str_radix_int: must lie in the range `[2, 36]` - found {}",
+        radix
+    );
 }
 
 #[cfg_attr(not(feature = "panic_immediate_abort"), inline(never))]
@@ -1582,7 +1585,6 @@ from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
 
-
 // #[feature(unchecked_math)]
 #[cfg(kani)]
 use crate::kani;
@@ -1596,6 +1598,9 @@ mod verify {
     // - Negative number addition won't underflow
     // Addition of two integers with different signs never overflows
     // Undefined behavior occurs when overflow or underflow happens
+    // Target contracts:
+    // #[kani::requires(!self.overflowing_add(rhs).1)]
+    // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
 
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
     #[kani::proof_for_contract(i8::unchecked_add)]

From 2bc4faf2ff544da0611eaa67e4644535a629bf8b Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Wed, 18 Sep 2024 14:41:15 -0700
Subject: [PATCH 09/42] Add comment for unchecked_add proofs

---
 library/core/src/num/mod.rs | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 1ebc09815717a..02d686519b9a2 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1593,16 +1593,27 @@ use crate::kani;
 mod verify {
     use super::*;
 
-    // Signed unchecked_add Safety preconditions:
-    // - Positive number addition won't overflow
-    // - Negative number addition won't underflow
-    // Addition of two integers with different signs never overflows
-    // Undefined behavior occurs when overflow or underflow happens
+    // `unchecked_add` proofs
+    //
     // Target contracts:
     // #[kani::requires(!self.overflowing_add(rhs).1)]
     // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
-
+    // 
+    // Target function:
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
+    // 
+    // Safety preconditions:
+    // 1. Signed integers (i8, i16, i32, i64, i128):
+    //  - Positive number addition won't overflow
+    //  - Negative number addition won't underflow
+    // Addition of two integers with different signs never overflows
+    // Undefined behavior occurs when overflow or underflow happens
+    // 
+    // 2. Unsigned integers (u8, u16, u32, u64, u128):
+    //  - Addition won't overflow
+    // Unsigned integers are always positive, so underflow won't happen
+    // Undefined behavior occurs when overflow happens
+
     #[kani::proof_for_contract(i8::unchecked_add)]
     pub fn check_unchecked_add_i8() {
         let num1: i8 = kani::any::<i8>();

From d9d4b5f377b0f6a6ca7986d371961633698262e1 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Thu, 19 Sep 2024 15:11:12 -0700
Subject: [PATCH 10/42] Add harnesses for i16,i32,i64,i128 unchecked_add

---
 library/core/src/num/mod.rs | 47 +++++++++++++++++++++++++++++++++----
 1 file changed, 43 insertions(+), 4 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 02d686519b9a2..ae9762bd72d62 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1585,7 +1585,6 @@ from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
 
-// #[feature(unchecked_math)]
 #[cfg(kani)]
 use crate::kani;
 
@@ -1598,17 +1597,17 @@ mod verify {
     // Target contracts:
     // #[kani::requires(!self.overflowing_add(rhs).1)]
     // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
-    // 
+    //
     // Target function:
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
-    // 
+    //
     // Safety preconditions:
     // 1. Signed integers (i8, i16, i32, i64, i128):
     //  - Positive number addition won't overflow
     //  - Negative number addition won't underflow
     // Addition of two integers with different signs never overflows
     // Undefined behavior occurs when overflow or underflow happens
-    // 
+    //
     // 2. Unsigned integers (u8, u16, u32, u64, u128):
     //  - Addition won't overflow
     // Unsigned integers are always positive, so underflow won't happen
@@ -1623,4 +1622,44 @@ mod verify {
             num1.unchecked_add(num2);
         }
     }
+
+    #[kani::proof_for_contract(i16::unchecked_add)]
+    pub fn check_unchecked_add_i16() {
+        let num1: i16 = kani::any::<i16>();
+        let num2: i16 = kani::any::<i16>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(i32::unchecked_add)]
+    pub fn check_unchecked_add_i32() {
+        let num1: i32 = kani::any::<i32>();
+        let num2: i32 = kani::any::<i32>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(i64::unchecked_add)]
+    pub fn check_unchecked_add_i64() {
+        let num1: i64 = kani::any::<i64>();
+        let num2: i64 = kani::any::<i64>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(i128::unchecked_add)]
+    pub fn check_unchecked_add_i128() {
+        let num1: i128 = kani::any::<i128>();
+        let num2: i128 = kani::any::<i128>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
 }

From 07c8b4a5dc06a826feee8fef416955765d197d0d Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Thu, 19 Sep 2024 15:18:50 -0700
Subject: [PATCH 11/42] Add harnesses for u8,u16,u32,u64,u128 unchecked_add

---
 library/core/src/num/mod.rs | 50 +++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index ae9762bd72d62..95984fccebc1f 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1662,4 +1662,54 @@ mod verify {
             num1.unchecked_add(num2);
         }
     }
+
+    #[kani::proof_for_contract(u8::unchecked_add)]
+    pub fn check_unchecked_add_u8() {
+        let num1: u8 = kani::any::<u8>();
+        let num2: u8 = kani::any::<u8>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u16::unchecked_add)]
+    pub fn check_unchecked_add_u16() {
+        let num1: u16 = kani::any::<u16>();
+        let num2: u16 = kani::any::<u16>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u32::unchecked_add)]
+    pub fn check_unchecked_add_u32() {
+        let num1: u32 = kani::any::<u32>();
+        let num2: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u64::unchecked_add)]
+    pub fn check_unchecked_add_u64() {
+        let num1: u64 = kani::any::<u64>();
+        let num2: u64 = kani::any::<u64>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u128::unchecked_add)]
+    pub fn check_unchecked_add_u128() {
+        let num1: u128 = kani::any::<u128>();
+        let num2: u128 = kani::any::<u128>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
 }

From 1fd4c6ae936496966b9f305906065d10b1c1b80a Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Thu, 19 Sep 2024 15:22:12 -0700
Subject: [PATCH 12/42] Cleanup misplaced proofs

---
 .../core/tests/num/kani-proofs/i128-proofs.rs | 50 -------------------
 .../core/tests/num/kani-proofs/i16-proofs.rs  | 50 -------------------
 .../core/tests/num/kani-proofs/i32-proofs.rs  | 50 -------------------
 .../core/tests/num/kani-proofs/i64-proofs.rs  | 50 -------------------
 .../core/tests/num/kani-proofs/i8-proofs.rs   | 50 -------------------
 .../core/tests/num/kani-proofs/u128-proofs.rs | 46 -----------------
 .../core/tests/num/kani-proofs/u16-proofs.rs  | 46 -----------------
 .../core/tests/num/kani-proofs/u32-proofs.rs  | 46 -----------------
 .../core/tests/num/kani-proofs/u64-proofs.rs  | 46 -----------------
 .../core/tests/num/kani-proofs/u8-proofs.rs   | 46 -----------------
 10 files changed, 480 deletions(-)
 delete mode 100644 library/core/tests/num/kani-proofs/i128-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/i16-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/i32-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/i64-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/i8-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/u128-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/u16-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/u32-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/u64-proofs.rs
 delete mode 100644 library/core/tests/num/kani-proofs/u8-proofs.rs

diff --git a/library/core/tests/num/kani-proofs/i128-proofs.rs b/library/core/tests/num/kani-proofs/i128-proofs.rs
deleted file mode 100644
index 4ac03ec8714fe..0000000000000
--- a/library/core/tests/num/kani-proofs/i128-proofs.rs
+++ /dev/null
@@ -1,50 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_i128_unchecked_add() {
-        let num1: i128 = kani::any::<i128>();
-        let num2: i128 = kani::any::<i128>();
-
-        // Safety preconditions:
-        // - Positive number addition won't overflow
-        // - Negative number addition won't underflow
-        // Addition of two integers with different signs never overflows
-        // Undefined behavior occurs when overflow or underflow happens
-        kani::assume(
-            (num1 > 0 && num2 > 0 && num1 < i128::MAX - num2)
-                || (num1 < 0 && num2 < 0 && num1 > i128::MIN - num2),
-        );
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_i128_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i128_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i128_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i128_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i128_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/i16-proofs.rs b/library/core/tests/num/kani-proofs/i16-proofs.rs
deleted file mode 100644
index f57591f6b8e07..0000000000000
--- a/library/core/tests/num/kani-proofs/i16-proofs.rs
+++ /dev/null
@@ -1,50 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_i16_unchecked_add() {
-        let num1: i16 = kani::any::<i16>();
-        let num2: i16 = kani::any::<i16>();
-
-        // Safety preconditions:
-        // - Positive number addition won't overflow
-        // - Negative number addition won't underflow
-        // Addition of two integers with different signs never overflows
-        // Undefined behavior occurs when overflow or underflow happens
-        kani::assume(
-            (num1 > 0 && num2 > 0 && num1 < i16::MAX - num2)
-                || (num1 < 0 && num2 < 0 && num1 > i16::MIN - num2),
-        );
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_i16_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i16_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i16_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i16_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i16_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/i32-proofs.rs b/library/core/tests/num/kani-proofs/i32-proofs.rs
deleted file mode 100644
index 0c8cca6a8d9c0..0000000000000
--- a/library/core/tests/num/kani-proofs/i32-proofs.rs
+++ /dev/null
@@ -1,50 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_i32_unchecked_add() {
-        let num1: i32 = kani::any::<i32>();
-        let num2: i32 = kani::any::<i32>();
-
-        // Safety preconditions:
-        // - Positive number addition won't overflow
-        // - Negative number addition won't underflow
-        // Addition of two integers with different signs never overflows
-        // Undefined behavior occurs when overflow or underflow happens
-        kani::assume(
-            (num1 > 0 && num2 > 0 && num1 < i32::MAX - num2)
-                || (num1 < 0 && num2 < 0 && num1 > i32::MIN - num2),
-        );
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_i32_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i32_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i32_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i32_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i32_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/i64-proofs.rs b/library/core/tests/num/kani-proofs/i64-proofs.rs
deleted file mode 100644
index 658956c110dd8..0000000000000
--- a/library/core/tests/num/kani-proofs/i64-proofs.rs
+++ /dev/null
@@ -1,50 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_i64_unchecked_add() {
-        let num1: i64 = kani::any::<i64>();
-        let num2: i64 = kani::any::<i64>();
-
-        // Safety preconditions:
-        // - Positive number addition won't overflow
-        // - Negative number addition won't underflow
-        // Addition of two integers with different signs never overflows
-        // Undefined behavior occurs when overflow or underflow happens
-        kani::assume(
-            (num1 > 0 && num2 > 0 && num1 < i64::MAX - num2)
-                || (num1 < 0 && num2 < 0 && num1 > i64::MIN - num2),
-        );
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_i64_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i64_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i64_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i64_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i64_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs
deleted file mode 100644
index 932407510ffda..0000000000000
--- a/library/core/tests/num/kani-proofs/i8-proofs.rs
+++ /dev/null
@@ -1,50 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_i8_unchecked_add() {
-        let num1: i8 = kani::any::<i8>();
-        let num2: i8 = kani::any::<i8>();
-
-        // Safety preconditions:
-        // - Positive number addition won't overflow
-        // - Negative number addition won't underflow
-        // Addition of two integers with different signs never overflows
-        // Undefined behavior occurs when overflow or underflow happens
-        kani::assume(
-            (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2)
-                || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2),
-        );
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/u128-proofs.rs b/library/core/tests/num/kani-proofs/u128-proofs.rs
deleted file mode 100644
index 4746ba6f6149d..0000000000000
--- a/library/core/tests/num/kani-proofs/u128-proofs.rs
+++ /dev/null
@@ -1,46 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_u128_unchecked_add() {
-        let num1: u128 = kani::any::<u128>();
-        let num2: u128 = kani::any::<u128>();
-
-        // Safety preconditions:
-        // - Addition won't overflow
-        // Unsigned integers are always positive, so underflow won't happen
-        // Undefined behavior occurs when overflow happens
-        kani::assume(num1 < u128::MAX - num2);
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_u128_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u128_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u128_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u128_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u128_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/u16-proofs.rs b/library/core/tests/num/kani-proofs/u16-proofs.rs
deleted file mode 100644
index c398cc0ee474b..0000000000000
--- a/library/core/tests/num/kani-proofs/u16-proofs.rs
+++ /dev/null
@@ -1,46 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_u16_unchecked_add() {
-        let num1: u16 = kani::any::<u16>();
-        let num2: u16 = kani::any::<u16>();
-
-        // Safety preconditions:
-        // - Addition won't overflow
-        // Unsigned integers are always positive, so underflow won't happen
-        // Undefined behavior occurs when overflow happens
-        kani::assume(num1 < u16::MAX - num2);
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_u16_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u16_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u16_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u16_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u16_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/u32-proofs.rs b/library/core/tests/num/kani-proofs/u32-proofs.rs
deleted file mode 100644
index 8f4dfb17949a5..0000000000000
--- a/library/core/tests/num/kani-proofs/u32-proofs.rs
+++ /dev/null
@@ -1,46 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_u32_unchecked_add() {
-        let num1: u32 = kani::any::<u32>();
-        let num2: u32 = kani::any::<u32>();
-
-        // Safety preconditions:
-        // - Addition won't overflow
-        // Unsigned integers are always positive, so underflow won't happen
-        // Undefined behavior occurs when overflow happens
-        kani::assume(num1 < u32::MAX - num2);
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_u32_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u32_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u32_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u32_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u32_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/u64-proofs.rs b/library/core/tests/num/kani-proofs/u64-proofs.rs
deleted file mode 100644
index d65c6f9178857..0000000000000
--- a/library/core/tests/num/kani-proofs/u64-proofs.rs
+++ /dev/null
@@ -1,46 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_u64_unchecked_add() {
-        let num1: u64 = kani::any::<u64>();
-        let num2: u64 = kani::any::<u64>();
-
-        // Safety preconditions:
-        // - Addition won't overflow
-        // Unsigned integers are always positive, so underflow won't happen
-        // Undefined behavior occurs when overflow happens
-        kani::assume(num1 < u64::MAX - num2);
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_u64_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u64_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u64_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u64_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u64_unchecked_neg() {
-        // TODO
-    }
-}
diff --git a/library/core/tests/num/kani-proofs/u8-proofs.rs b/library/core/tests/num/kani-proofs/u8-proofs.rs
deleted file mode 100644
index ef6569ceaa3ba..0000000000000
--- a/library/core/tests/num/kani-proofs/u8-proofs.rs
+++ /dev/null
@@ -1,46 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_u8_unchecked_add() {
-        let num1: u8 = kani::any::<u8>();
-        let num2: u8 = kani::any::<u8>();
-
-        // Safety preconditions:
-        // - Addition won't overflow
-        // Unsigned integers are always positive, so underflow won't happen
-        // Undefined behavior occurs when overflow happens
-        kani::assume(num1 < u8::MAX - num2);
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_u8_unchecked_sub() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u8_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u8_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u8_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_u8_unchecked_neg() {
-        // TODO
-    }
-}

From b360311c955df808f38ec2c4c5ddaa57f4f810e3 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Fri, 20 Sep 2024 12:57:35 -0700
Subject: [PATCH 13/42] Clean up comment

---
 library/core/src/num/mod.rs | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 95984fccebc1f..95fc1f394f63b 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1601,17 +1601,8 @@ mod verify {
     // Target function:
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
     //
-    // Safety preconditions:
-    // 1. Signed integers (i8, i16, i32, i64, i128):
-    //  - Positive number addition won't overflow
-    //  - Negative number addition won't underflow
-    // Addition of two integers with different signs never overflows
-    // Undefined behavior occurs when overflow or underflow happens
-    //
-    // 2. Unsigned integers (u8, u16, u32, u64, u128):
-    //  - Addition won't overflow
-    // Unsigned integers are always positive, so underflow won't happen
-    // Undefined behavior occurs when overflow happens
+    // Target types:
+    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
 
     #[kani::proof_for_contract(i8::unchecked_add)]
     pub fn check_unchecked_add_i8() {

From 8cbca87171dc3efa4264e09df094866b499ecf07 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Fri, 20 Sep 2024 12:58:16 -0700
Subject: [PATCH 14/42] Format comment

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

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 95fc1f394f63b..766b52f227ffa 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1594,16 +1594,15 @@ mod verify {
 
     // `unchecked_add` proofs
     //
+    // Target types:
+    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    //
     // Target contracts:
     // #[kani::requires(!self.overflowing_add(rhs).1)]
     // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
     //
     // Target function:
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
-    //
-    // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
-
     #[kani::proof_for_contract(i8::unchecked_add)]
     pub fn check_unchecked_add_i8() {
         let num1: i8 = kani::any::<i8>();

From 0eef8581caa0f581689307aa6c3611bde6aec4b2 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Fri, 20 Sep 2024 13:15:21 -0700
Subject: [PATCH 15/42] Remove  before contracts. Fix import in

---
 library/core/src/num/int_macros.rs  | 4 ++--
 library/core/src/num/mod.rs         | 7 ++++---
 library/core/src/num/uint_macros.rs | 4 ++--
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 6e97b7999eef4..fa0c9c98dde74 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -511,8 +511,8 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[kani::requires(!self.overflowing_add(rhs).1)]
-        #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
+        #[requires(!self.overflowing_add(rhs).1)]
+        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 766b52f227ffa..28aeb1b897149 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -5,6 +5,10 @@
 use crate::str::FromStr;
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{ascii, intrinsics, mem};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 
 // Used because the `?` operator is not allowed in a const context.
 macro_rules! try_opt {
@@ -1585,9 +1589,6 @@ from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
 
-#[cfg(kani)]
-use crate::kani;
-
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 64d43c394e2b2..48f0e2d4dc24b 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -558,8 +558,8 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[kani::requires(!self.overflowing_add(rhs).1)]
-        #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
+        #[requires(!self.overflowing_add(rhs).1)]
+        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From 4858a531de50d0a2654ab6cbf66461b78ef210a9 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Fri, 20 Sep 2024 13:43:34 -0700
Subject: [PATCH 16/42] Fix comment

---
 library/core/src/num/mod.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 28aeb1b897149..4dbce78394d9e 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1599,8 +1599,8 @@ mod verify {
     // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
     //
     // Target contracts:
-    // #[kani::requires(!self.overflowing_add(rhs).1)]
-    // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
+    // #[requires(!self.overflowing_add(rhs).1)]
+    // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
     //
     // Target function:
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self

From bbd75f7189ba5bae71febf02a94db85a6f037928 Mon Sep 17 00:00:00 2001
From: Rajath <rajathkotyal@gmail.com>
Date: Mon, 23 Sep 2024 13:01:33 -0700
Subject: [PATCH 17/42] unchecked multiplication and shift right

---
 library/core/src/num/int_macros.rs  |   6 +-
 library/core/src/num/mod.rs         | 228 ++++++++++++++++++++++++++++
 library/core/src/num/uint_macros.rs |   4 +
 3 files changed, 237 insertions(+), 1 deletion(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index fa0c9c98dde74..1f82f24c6bf27 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -817,6 +817,8 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_mul(rhs).1)]
+        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1423,8 +1425,10 @@ macro_rules! int_impl {
         #[must_use = "this returns the result of the operation, \
                       without modifying the original"]
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
-        #[inline(always)]
+        #[inline(always)]0
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
+        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 4dbce78394d9e..661c3f11cd3b6 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1703,4 +1703,232 @@ mod verify {
             num1.unchecked_add(num2);
         }
     }
+
+    // `unchecked_mul` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    //
+    // Target Files : src/num/int_macros.rs , src/num/uint_macros.rs
+    //
+    // Target contracts :
+    // #[requires(!self.overflowing_mul(rhs).1)]
+    // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
+    //
+    // Target function definition:
+    // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
+
+    #[kani::proof_for_contract(i8::unchecked_mul)]
+    pub fn check_unchecked_mul_i8() {
+        let num1: i8 = kani::any::<i8>();
+        let num2: i8 = kani::any::<i8>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(i16::unchecked_mul)]
+    pub fn check_unchecked_mul_i16() {
+        let num1: i16 = kani::any::<i16>();
+        let num2: i16 = kani::any::<i16>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(i32::unchecked_mul)]
+    pub fn check_unchecked_mul_i32() {
+        let num1: i32 = kani::any::<i32>();
+        let num2: i32 = kani::any::<i32>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(i64::unchecked_mul)]
+    pub fn check_unchecked_mul_i64() {
+        let num1: i64 = kani::any::<i64>();
+        let num2: i64 = kani::any::<i64>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(i128::unchecked_mul)]
+    pub fn check_unchecked_mul_i128() {
+        let num1: i128 = kani::any::<i128>();
+        let num2: i128 = kani::any::<i128>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u8::unchecked_mul)]
+    pub fn check_unchecked_mul_u8() {
+        let num1: u8 = kani::any::<u8>();
+        let num2: u8 = kani::any::<u8>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u16::unchecked_mul)]
+    pub fn check_unchecked_mul_u16() {
+        let num1: u16 = kani::any::<u16>();
+        let num2: u16 = kani::any::<u16>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u32::unchecked_mul)]
+    pub fn check_unchecked_mul_u32() {
+        let num1: u32 = kani::any::<u32>();
+        let num2: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u64::unchecked_mul)]
+    pub fn check_unchecked_mul_u64() {
+        let num1: u64 = kani::any::<u64>();
+        let num2: u64 = kani::any::<u64>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    #[kani::proof_for_contract(u128::unchecked_mul)]
+    pub fn check_unchecked_mul_u128() {
+        let num1: u128 = kani::any::<u128>();
+        let num2: u128 = kani::any::<u128>();
+
+        unsafe {
+            num1.unchecked_mul(num2);
+        }
+    }
+
+    // `unchecked_shr` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    //
+    // Target Files : src/num/int_macros.rs , src/num/uint_macros.rs
+    //
+    // Target contracts:
+    // #[requires(rhs < <$ActualT>::BITS)]
+    // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
+
+    #[kani::proof_for_contract(i8::unchecked_shr)]
+    pub fn check_unchecked_shr_i8() {
+        let num: i8 = kani::any::<i8>();
+        let shift: u32 = kani::any::<u32>() % i8::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(i16::unchecked_shr)]
+    pub fn check_unchecked_shr_i16() {
+        let num: i16 = kani::any::<i16>();
+        let shift: u32 = kani::any::<u32>() % i16::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(i32::unchecked_shr)]
+    pub fn check_unchecked_shr_i32() {
+        let num: i32 = kani::any::<i32>();
+        let shift: u32 = kani::any::<u32>() % i32::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(i64::unchecked_shr)]
+    pub fn check_unchecked_shr_i64() {
+        let num: i64 = kani::any::<i64>();
+        let shift: u32 = kani::any::<u32>() % i64::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(i128::unchecked_shr)]
+    pub fn check_unchecked_shr_i128() {
+        let num: i128 = kani::any::<i128>();
+        let shift: u32 = kani::any::<u32>() % i128::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u8::unchecked_shr)]
+    pub fn check_unchecked_shr_u8() {
+        let num: u8 = kani::any::<u8>();
+        let shift: u32 = kani::any::<u32>() % u8::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u16::unchecked_shr)]
+    pub fn check_unchecked_shr_u16() {
+        let num: u16 = kani::any::<u16>();
+        let shift: u32 = kani::any::<u32>() % u16::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u32::unchecked_shr)]
+    pub fn check_unchecked_shr_u32() {
+        let num: u32 = kani::any::<u32>();
+        let shift: u32 = kani::any::<u32>() % u32::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u64::unchecked_shr)]
+    pub fn check_unchecked_shr_u64() {
+        let num: u64 = kani::any::<u64>();
+        let shift: u32 = kani::any::<u32>() % u64::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u128::unchecked_shr)]
+    pub fn check_unchecked_shr_u128() {
+        let num: u128 = kani::any::<u128>();
+        let shift: u32 = kani::any::<u32>() % u128::BITS;
+
+        unsafe {
+            num.unchecked_shr(shift);
+        }
+    }
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 48f0e2d4dc24b..4ca4e2bcb08b7 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -909,6 +909,8 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_mul(rhs).1)]
+        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1614,6 +1616,8 @@ macro_rules! uint_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < <$ActualT>::BITS)]// i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
+        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From a7d3cc24514a38a538bd0c935401379354994313 Mon Sep 17 00:00:00 2001
From: MWDZ <jinjunfeng721@gmail.com>
Date: Mon, 23 Sep 2024 20:12:20 -0700
Subject: [PATCH 18/42] feat: add contract and test case for unchecked_shl in
 type int and unit

---
 library/core/src/num/int_macros.rs  |   2 +
 library/core/src/num/mod.rs         | 113 ++++++++++++++++++++++++++++
 library/core/src/num/uint_macros.rs |   2 +
 3 files changed, 117 insertions(+)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index fa0c9c98dde74..486f9493b7148 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -1299,6 +1299,8 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < Self::BITS)]
+        #[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)]
         pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 4dbce78394d9e..3d65b60b155f7 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1703,4 +1703,117 @@ mod verify {
             num1.unchecked_add(num2);
         }
     }
+
+    // `unchecked_shl` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    //
+    // Target contracts:
+    // #[requires(shift < Self::BITS)]
+    // #[ensures(|ret| *ret == self << shift)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_shl(self, shift: u32) -> Self
+    //
+    // This function performs an unchecked bitwise left shift operation.
+    #[kani::proof_for_contract(i8::unchecked_shl)]
+    pub fn check_unchecked_shl_i8() {
+        let num1: i8 = kani::any::<i8>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(i16::unchecked_shl)]
+    pub fn check_unchecked_shl_i16() {
+        let num1: i16 = kani::any::<i16>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(i32::unchecked_shl)]
+    pub fn check_unchecked_shl_i32() {
+        let num1: i32 = kani::any::<i32>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(i64::unchecked_shl)]
+    pub fn check_unchecked_shl_i64() {
+        let num1: i64 = kani::any::<i64>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(i128::unchecked_shl)]
+    pub fn check_unchecked_shl_i128() {
+        let num1: i128 = kani::any::<i128>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u8::unchecked_shl)]
+    pub fn check_unchecked_shl_u8() {
+        let num1: u8 = kani::any::<u8>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u16::unchecked_shl)]
+    pub fn check_unchecked_shl_u16() {
+        let num1: u16 = kani::any::<u16>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u32::unchecked_shl)]
+    pub fn check_unchecked_shl_u32() {
+        let num1: u32 = kani::any::<u32>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u64::unchecked_shl)]
+    pub fn check_unchecked_shl_u64() {
+        let num1: u64 = kani::any::<u64>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
+
+    #[kani::proof_for_contract(u128::unchecked_shl)]
+    pub fn check_unchecked_shl_u128() {
+        let num1: u128 = kani::any::<u128>();
+        let shift: u32 = kani::any::<u32>();
+
+        unsafe {
+            num1.unchecked_shl(shift);
+        }
+    }
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 48f0e2d4dc24b..617db39cbc220 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -1488,6 +1488,8 @@ macro_rules! uint_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < Self::BITS)]
+        #[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)]
         pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From 271afaddbee6eef41ec4d304a477adc62d1a7991 Mon Sep 17 00:00:00 2001
From: Lanfei Ma <99311320+lanfeima@users.noreply.github.com>
Date: Tue, 24 Sep 2024 00:54:07 -0700
Subject: [PATCH 19/42] added preconditions and postconditions

---
 library/core/src/num/int_macros.rs  | 2 ++
 library/core/src/num/uint_macros.rs | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index fa0c9c98dde74..8b9004ef0ee51 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -665,6 +665,8 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
+        #[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)] // Postconditions: Result must be within valid bounds
         pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 48f0e2d4dc24b..a69d393d5d389 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -752,6 +752,8 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
+        #[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)] // Postconditions: Result must be within valid bounds
         pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From c7762c269195d4290731e83fce878aa29b9ca2f6 Mon Sep 17 00:00:00 2001
From: Lanfei Ma <99311320+lanfeima@users.noreply.github.com>
Date: Tue, 24 Sep 2024 01:06:28 -0700
Subject: [PATCH 20/42] add proof functions for unchecked_sub

---
 library/core/src/num/mod.rs | 107 ++++++++++++++++++++++++++++++++++++
 1 file changed, 107 insertions(+)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 4dbce78394d9e..98df564f5c946 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1703,4 +1703,111 @@ mod verify {
             num1.unchecked_add(num2);
         }
     }
+
+
+    // `unchecked_sub` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    //
+    // Target contracts:
+    //#[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
+    //#[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)] // Postconditions: Result must be within valid bounds
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self
+
+    #[kani::proof_for_contract(i8::unchecked_sub)]
+    pub fn check_unchecked_sub_i8() {
+        let num1: i8 = kani::any::<i8>();
+        let num2: i8 = kani::any::<i8>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(i16::unchecked_sub)]
+    pub fn check_unchecked_sub_i16() {
+        let num1: i16 = kani::any::<i16>();
+        let num2: i16 = kani::any::<i16>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(i32::unchecked_sub)]
+    pub fn check_unchecked_sub_i32() {
+        let num1: i32 = kani::any::<i32>();
+        let num2: i32 = kani::any::<i32>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(i64::unchecked_sub)]
+    pub fn check_unchecked_sub_i64() {
+        let num1: i64 = kani::any::<i64>();
+        let num2: i64 = kani::any::<i64>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(i128::unchecked_sub)]
+    pub fn check_unchecked_sub_i128() {
+        let num1: i128 = kani::any::<i128>();
+        let num2: i128 = kani::any::<i128>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(u8::unchecked_sub)]
+    pub fn check_unchecked_sub_u8() {
+        let num1: u8 = kani::any::<u8>();
+        let num2: u8 = kani::any::<u8>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(u16::unchecked_sub)]
+    pub fn check_unchecked_sub_u16() {
+        let num1: u16 = kani::any::<u16>();
+        let num2: u16 = kani::any::<u16>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(u32::unchecked_sub)]
+    pub fn check_unchecked_sub_u32() {
+        let num1: u32 = kani::any::<u32>();
+        let num2: u32 = kani::any::<u32>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(u64::unchecked_sub)]
+    pub fn check_unchecked_sub_u64() {
+        let num1: u64 = kani::any::<u64>();
+        let num2: u64 = kani::any::<u64>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+    #[kani::proof_for_contract(u128::unchecked_sub)]
+    pub fn check_unchecked_sub_u128() {
+        let num1: u128 = kani::any::<u128>();
+        let num2: u128 = kani::any::<u128>();
+        unsafe {
+            num1.unchecked_sub(num2);
+        }
+    }
+    
+
+
+    
 }

From d99844df3a9f0bb24d973e250122eedd3542924e Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Tue, 24 Sep 2024 14:16:46 -0700
Subject: [PATCH 21/42] Remove ensures contracts && Undo formatting on existing
 code

---
 library/core/src/num/int_macros.rs  | 1 -
 library/core/src/num/mod.rs         | 5 +----
 library/core/src/num/uint_macros.rs | 1 -
 3 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index fa0c9c98dde74..fa3e4cef9bcb4 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -512,7 +512,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_add(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 4dbce78394d9e..526b8895e89cb 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1401,10 +1401,7 @@ const fn from_str_radix_panic_ct(_radix: u32) -> ! {
 
 #[track_caller]
 fn from_str_radix_panic_rt(radix: u32) -> ! {
-    panic!(
-        "from_str_radix_int: must lie in the range `[2, 36]` - found {}",
-        radix
-    );
+    panic!("from_str_radix_int: must lie in the range `[2, 36]` - found {}", radix);
 }
 
 #[cfg_attr(not(feature = "panic_immediate_abort"), inline(never))]
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 48f0e2d4dc24b..b12d82bdc720c 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -559,7 +559,6 @@ macro_rules! uint_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_add(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From fbcf49e631daa53e111bf750c1d3c916921a016a Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Tue, 24 Sep 2024 14:28:59 -0700
Subject: [PATCH 22/42] Add {isize, usize}::unchecked_add harnesses

---
 library/core/src/num/mod.rs | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 526b8895e89cb..159062099dbc0 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1593,11 +1593,10 @@ mod verify {
     // `unchecked_add` proofs
     //
     // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
     //
     // Target contracts:
     // #[requires(!self.overflowing_add(rhs).1)]
-    // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
     //
     // Target function:
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
@@ -1651,6 +1650,16 @@ mod verify {
         }
     }
 
+    #[kani::proof_for_contract(isize::unchecked_add)]
+    pub fn check_unchecked_add_isize() {
+        let num1: isize = kani::any::<isize>();
+        let num2: isize = kani::any::<isize>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
+
     #[kani::proof_for_contract(u8::unchecked_add)]
     pub fn check_unchecked_add_u8() {
         let num1: u8 = kani::any::<u8>();
@@ -1700,4 +1709,14 @@ mod verify {
             num1.unchecked_add(num2);
         }
     }
+
+    #[kani::proof_for_contract(usize::unchecked_add)]
+    pub fn check_unchecked_add_usize() {
+        let num1: usize = kani::any::<usize>();
+        let num2: usize = kani::any::<usize>();
+
+        unsafe {
+            num1.unchecked_add(num2);
+        }
+    }
 }

From 864afa684013af8608c43740099e75c655d83060 Mon Sep 17 00:00:00 2001
From: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com>
Date: Wed, 25 Sep 2024 03:04:12 -0700
Subject: [PATCH 23/42] Small fix typo

---
 library/core/src/num/int_macros.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 1f82f24c6bf27..07715ddaa3b70 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -1425,7 +1425,7 @@ macro_rules! int_impl {
         #[must_use = "this returns the result of the operation, \
                       without modifying the original"]
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
-        #[inline(always)]0
+        #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
         #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift

From 54a03ef0c9c301d7d3aa06a82d75e305c3ee76bf Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Fri, 27 Sep 2024 15:09:57 -0700
Subject: [PATCH 24/42] Add harness generation macros for unchecked methods &&
 Update unchecked_add harnesses

---
 library/core/src/num/mod.rs | 169 +++++++++++-------------------------
 1 file changed, 52 insertions(+), 117 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 159062099dbc0..8e31a0f434981 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1586,137 +1586,72 @@ from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
 
+#[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
 
-    // `unchecked_add` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
-    //
-    // Target contracts:
-    // #[requires(!self.overflowing_add(rhs).1)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
-    #[kani::proof_for_contract(i8::unchecked_add)]
-    pub fn check_unchecked_add_i8() {
-        let num1: i8 = kani::any::<i8>();
-        let num2: i8 = kani::any::<i8>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i16::unchecked_add)]
-    pub fn check_unchecked_add_i16() {
-        let num1: i16 = kani::any::<i16>();
-        let num2: i16 = kani::any::<i16>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i32::unchecked_add)]
-    pub fn check_unchecked_add_i32() {
-        let num1: i32 = kani::any::<i32>();
-        let num2: i32 = kani::any::<i32>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i64::unchecked_add)]
-    pub fn check_unchecked_add_i64() {
-        let num1: i64 = kani::any::<i64>();
-        let num2: i64 = kani::any::<i64>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i128::unchecked_add)]
-    pub fn check_unchecked_add_i128() {
-        let num1: i128 = kani::any::<i128>();
-        let num2: i128 = kani::any::<i128>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(isize::unchecked_add)]
-    pub fn check_unchecked_add_isize() {
-        let num1: isize = kani::any::<isize>();
-        let num2: isize = kani::any::<isize>();
+    macro_rules! generate_unchecked_math_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: $type = kani::any::<$type>();
 
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u8::unchecked_add)]
-    pub fn check_unchecked_add_u8() {
-        let num1: u8 = kani::any::<u8>();
-        let num2: u8 = kani::any::<u8>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u16::unchecked_add)]
-    pub fn check_unchecked_add_u16() {
-        let num1: u16 = kani::any::<u16>();
-        let num2: u16 = kani::any::<u16>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u32::unchecked_add)]
-    pub fn check_unchecked_add_u32() {
-        let num1: u32 = kani::any::<u32>();
-        let num2: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_add(num2);
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
         }
     }
 
-    #[kani::proof_for_contract(u64::unchecked_add)]
-    pub fn check_unchecked_add_u64() {
-        let num1: u64 = kani::any::<u64>();
-        let num2: u64 = kani::any::<u64>();
+    macro_rules! generate_unchecked_shift_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: u32 = kani::any::<u32>();
 
-        unsafe {
-            num1.unchecked_add(num2);
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
         }
     }
 
-    #[kani::proof_for_contract(u128::unchecked_add)]
-    pub fn check_unchecked_add_u128() {
-        let num1: u128 = kani::any::<u128>();
-        let num2: u128 = kani::any::<u128>();
+    macro_rules! generate_unchecked_neg_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
 
-        unsafe {
-            num1.unchecked_add(num2);
+                unsafe {
+                    num1.$method();
+                }
+            }
         }
     }
 
-    #[kani::proof_for_contract(usize::unchecked_add)]
-    pub fn check_unchecked_add_usize() {
-        let num1: usize = kani::any::<usize>();
-        let num2: usize = kani::any::<usize>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
+    // `unchecked_add` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(!self.overflowing_add(rhs).1)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
+    generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
+    generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16);
+    generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32);
+    generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64);
+    generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128);
+    generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize);
+    generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8);
+    generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16);
+    generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32);
+    generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
+    generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
+    generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
 }

From ae678de8bda63673540fd1c5a2bbb5fb776bff94 Mon Sep 17 00:00:00 2001
From: rajathkotyal <rajathkotyal@gmail.com>
Date: Sun, 29 Sep 2024 04:32:21 -0700
Subject: [PATCH 25/42] added limits to multiplication proofs, reduced
 duplicacy in code by using macros to generate proof harnesses

---
 library/core/src/num/int_macros.rs  |   3 -
 library/core/src/num/mod.rs         | 412 +++++++---------------------
 library/core/src/num/uint_macros.rs |   3 -
 3 files changed, 103 insertions(+), 315 deletions(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 07715ddaa3b70..a46e653de2bd0 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -512,7 +512,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_add(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -818,7 +817,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_mul(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1428,7 +1426,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 661c3f11cd3b6..186d05eda5a98 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1401,10 +1401,7 @@ const fn from_str_radix_panic_ct(_radix: u32) -> ! {
 
 #[track_caller]
 fn from_str_radix_panic_rt(radix: u32) -> ! {
-    panic!(
-        "from_str_radix_int: must lie in the range `[2, 36]` - found {}",
-        radix
-    );
+    panic!("from_str_radix_int: must lie in the range `[2, 36]` - found {}", radix);
 }
 
 #[cfg_attr(not(feature = "panic_immediate_abort"), inline(never))]
@@ -1589,346 +1586,143 @@ from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
 
+#[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
 
-    // `unchecked_add` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
-    //
-    // Target contracts:
-    // #[requires(!self.overflowing_add(rhs).1)]
-    // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
-    #[kani::proof_for_contract(i8::unchecked_add)]
-    pub fn check_unchecked_add_i8() {
-        let num1: i8 = kani::any::<i8>();
-        let num2: i8 = kani::any::<i8>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i16::unchecked_add)]
-    pub fn check_unchecked_add_i16() {
-        let num1: i16 = kani::any::<i16>();
-        let num2: i16 = kani::any::<i16>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i32::unchecked_add)]
-    pub fn check_unchecked_add_i32() {
-        let num1: i32 = kani::any::<i32>();
-        let num2: i32 = kani::any::<i32>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i64::unchecked_add)]
-    pub fn check_unchecked_add_i64() {
-        let num1: i64 = kani::any::<i64>();
-        let num2: i64 = kani::any::<i64>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i128::unchecked_add)]
-    pub fn check_unchecked_add_i128() {
-        let num1: i128 = kani::any::<i128>();
-        let num2: i128 = kani::any::<i128>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u8::unchecked_add)]
-    pub fn check_unchecked_add_u8() {
-        let num1: u8 = kani::any::<u8>();
-        let num2: u8 = kani::any::<u8>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u16::unchecked_add)]
-    pub fn check_unchecked_add_u16() {
-        let num1: u16 = kani::any::<u16>();
-        let num2: u16 = kani::any::<u16>();
+    macro_rules! generate_unchecked_math_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: $type = kani::any::<$type>();
 
-        unsafe {
-            num1.unchecked_add(num2);
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
         }
     }
 
-    #[kani::proof_for_contract(u32::unchecked_add)]
-    pub fn check_unchecked_add_u32() {
-        let num1: u32 = kani::any::<u32>();
-        let num2: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_add(num2);
+    macro_rules! generate_unchecked_mul_harness {
+        ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any();
+                let num2: $type = kani::any();
+    
+                // Limit the values of num1 and num2 to the specified range for multiplication
+                kani::assume(num1 >= $min && num1 <= $max);
+                kani::assume(num2 >= $min && num2 <= $max);
+    
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
         }
     }
-
-    #[kani::proof_for_contract(u64::unchecked_add)]
-    pub fn check_unchecked_add_u64() {
-        let num1: u64 = kani::any::<u64>();
-        let num2: u64 = kani::any::<u64>();
-
-        unsafe {
-            num1.unchecked_add(num2);
+    
+
+    macro_rules! generate_unchecked_shift_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: u32 = kani::any::<u32>();
+    
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
         }
     }
+    
 
-    #[kani::proof_for_contract(u128::unchecked_add)]
-    pub fn check_unchecked_add_u128() {
-        let num1: u128 = kani::any::<u128>();
-        let num2: u128 = kani::any::<u128>();
+    macro_rules! generate_unchecked_neg_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
 
-        unsafe {
-            num1.unchecked_add(num2);
+                unsafe {
+                    num1.$method();
+                }
+            }
         }
     }
 
-    // `unchecked_mul` proofs
+    // `unchecked_add` proofs
     //
     // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
     //
-    // Target Files : src/num/int_macros.rs , src/num/uint_macros.rs
+    // Target contracts:
+    // #[requires(!self.overflowing_add(rhs).1)]
     //
-    // Target contracts :
+    // Target function:
+    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
+    generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
+    generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16);
+    generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32);
+    generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64);
+    generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128);
+    generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize);
+    generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8);
+    generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16);
+    generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32);
+    generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
+    generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
+    generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
+
+    // unchecked_mul proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
+    //
+    // Target contracts:
     // #[requires(!self.overflowing_mul(rhs).1)]
-    // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
     //
-    // Target function definition:
+    // Target function:
     // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
+    // exponential state spaces for 32,64 and 128, hence provided limited range for verification.
+    generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8);
+    generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16);
+    generate_unchecked_mul_harness!(i32, unchecked_mul, checked_unchecked_mul_i32, -10_000i32, 10_000i32);
+    generate_unchecked_mul_harness!(i64, unchecked_mul, checked_unchecked_mul_i64, -1_000i64, 1_000i64);
+    generate_unchecked_mul_harness!(i128, unchecked_mul, checked_unchecked_mul_i128, -1_000_000_000_000_000i128, 1_000_000_000_000_000i128);
+    generate_unchecked_mul_harness!(isize, unchecked_mul, checked_unchecked_mul_isize, -100_000isize, 100_000isize);
 
-    #[kani::proof_for_contract(i8::unchecked_mul)]
-    pub fn check_unchecked_mul_i8() {
-        let num1: i8 = kani::any::<i8>();
-        let num2: i8 = kani::any::<i8>();
-
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i16::unchecked_mul)]
-    pub fn check_unchecked_mul_i16() {
-        let num1: i16 = kani::any::<i16>();
-        let num2: i16 = kani::any::<i16>();
-
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i32::unchecked_mul)]
-    pub fn check_unchecked_mul_i32() {
-        let num1: i32 = kani::any::<i32>();
-        let num2: i32 = kani::any::<i32>();
-
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i64::unchecked_mul)]
-    pub fn check_unchecked_mul_i64() {
-        let num1: i64 = kani::any::<i64>();
-        let num2: i64 = kani::any::<i64>();
 
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
+    generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8);
+    generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16);
+    generate_unchecked_mul_harness!(u32, unchecked_mul, checked_unchecked_mul_u32, 0u32, 20_000u32);
+    generate_unchecked_mul_harness!(u64, unchecked_mul, checked_unchecked_mul_u64, 0u64, 2_000u64);
+    generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128);
+    generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize);
 
-    #[kani::proof_for_contract(i128::unchecked_mul)]
-    pub fn check_unchecked_mul_i128() {
-        let num1: i128 = kani::any::<i128>();
-        let num2: i128 = kani::any::<i128>();
 
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u8::unchecked_mul)]
-    pub fn check_unchecked_mul_u8() {
-        let num1: u8 = kani::any::<u8>();
-        let num2: u8 = kani::any::<u8>();
-
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u16::unchecked_mul)]
-    pub fn check_unchecked_mul_u16() {
-        let num1: u16 = kani::any::<u16>();
-        let num2: u16 = kani::any::<u16>();
-
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u32::unchecked_mul)]
-    pub fn check_unchecked_mul_u32() {
-        let num1: u32 = kani::any::<u32>();
-        let num2: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u64::unchecked_mul)]
-    pub fn check_unchecked_mul_u64() {
-        let num1: u64 = kani::any::<u64>();
-        let num2: u64 = kani::any::<u64>();
-
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u128::unchecked_mul)]
-    pub fn check_unchecked_mul_u128() {
-        let num1: u128 = kani::any::<u128>();
-        let num2: u128 = kani::any::<u128>();
-
-        unsafe {
-            num1.unchecked_mul(num2);
-        }
-    }
-
-    // `unchecked_shr` proofs
+    // unchecked_shr proofs
     //
     // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
-    //
-    // Target Files : src/num/int_macros.rs , src/num/uint_macros.rs
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
     //
     // Target contracts:
     // #[requires(rhs < <$ActualT>::BITS)]
-    // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
     //
     // Target function:
     // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
+    generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8);
+    generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16);
+    generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32);
+    generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64);
+    generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128);
+    generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize);
+    generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8);
+    generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16);
+    generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32);
+    generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
+    generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
+    generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
 
-    #[kani::proof_for_contract(i8::unchecked_shr)]
-    pub fn check_unchecked_shr_i8() {
-        let num: i8 = kani::any::<i8>();
-        let shift: u32 = kani::any::<u32>() % i8::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(i16::unchecked_shr)]
-    pub fn check_unchecked_shr_i16() {
-        let num: i16 = kani::any::<i16>();
-        let shift: u32 = kani::any::<u32>() % i16::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(i32::unchecked_shr)]
-    pub fn check_unchecked_shr_i32() {
-        let num: i32 = kani::any::<i32>();
-        let shift: u32 = kani::any::<u32>() % i32::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(i64::unchecked_shr)]
-    pub fn check_unchecked_shr_i64() {
-        let num: i64 = kani::any::<i64>();
-        let shift: u32 = kani::any::<u32>() % i64::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(i128::unchecked_shr)]
-    pub fn check_unchecked_shr_i128() {
-        let num: i128 = kani::any::<i128>();
-        let shift: u32 = kani::any::<u32>() % i128::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u8::unchecked_shr)]
-    pub fn check_unchecked_shr_u8() {
-        let num: u8 = kani::any::<u8>();
-        let shift: u32 = kani::any::<u32>() % u8::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u16::unchecked_shr)]
-    pub fn check_unchecked_shr_u16() {
-        let num: u16 = kani::any::<u16>();
-        let shift: u32 = kani::any::<u32>() % u16::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u32::unchecked_shr)]
-    pub fn check_unchecked_shr_u32() {
-        let num: u32 = kani::any::<u32>();
-        let shift: u32 = kani::any::<u32>() % u32::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u64::unchecked_shr)]
-    pub fn check_unchecked_shr_u64() {
-        let num: u64 = kani::any::<u64>();
-        let shift: u32 = kani::any::<u32>() % u64::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u128::unchecked_shr)]
-    pub fn check_unchecked_shr_u128() {
-        let num: u128 = kani::any::<u128>();
-        let shift: u32 = kani::any::<u32>() % u128::BITS;
-
-        unsafe {
-            num.unchecked_shr(shift);
-        }
-    }
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 4ca4e2bcb08b7..8706ed8bd6d5f 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -559,7 +559,6 @@ macro_rules! uint_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_add(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -910,7 +909,6 @@ macro_rules! uint_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_mul(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1617,7 +1615,6 @@ macro_rules! uint_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(rhs < <$ActualT>::BITS)]// i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From 8ee56826478518f03a622803455c52af2f85f6ba Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Sun, 29 Sep 2024 19:47:07 -0700
Subject: [PATCH 26/42] Remove unused import safety::ensures

---
 library/core/src/num/mod.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 8e31a0f434981..51bc33b7b47a4 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -5,7 +5,7 @@
 use crate::str::FromStr;
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{ascii, intrinsics, mem};
-use safety::{ensures, requires};
+use safety::requires;
 
 #[cfg(kani)]
 use crate::kani;

From 02d706a2f818cdacee696763b4185458a2fc90e5 Mon Sep 17 00:00:00 2001
From: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com>
Date: Sun, 29 Sep 2024 21:15:21 -0700
Subject: [PATCH 27/42] unchecked_mul and unchecked_shr proofs (#7)

* Added harnesses for unchecked multiplication (`unchecked_mul`) and shift right (`unchecked_shr`)
* Added a macro and input limits for multiplication proofs
* Reduced duplicity in code by using macros to generate proof harnesses
---
 library/core/src/num/int_macros.rs  |  2 +
 library/core/src/num/mod.rs         | 72 ++++++++++++++++++++++++++++-
 library/core/src/num/uint_macros.rs |  2 +
 3 files changed, 75 insertions(+), 1 deletion(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index fa3e4cef9bcb4..a46e653de2bd0 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -816,6 +816,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_mul(rhs).1)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1424,6 +1425,7 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 51bc33b7b47a4..54e90d1bff0ff 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1605,19 +1605,39 @@ mod verify {
         }
     }
 
+    macro_rules! generate_unchecked_mul_harness {
+        ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any();
+                let num2: $type = kani::any();
+    
+                // Limit the values of num1 and num2 to the specified range for multiplication
+                kani::assume(num1 >= $min && num1 <= $max);
+                kani::assume(num2 >= $min && num2 <= $max);
+    
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
+        }
+    }
+    
+
     macro_rules! generate_unchecked_shift_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
             #[kani::proof_for_contract($type::$method)]
             pub fn $harness_name() {
                 let num1: $type = kani::any::<$type>();
                 let num2: u32 = kani::any::<u32>();
-
+    
                 unsafe {
                     num1.$method(num2);
                 }
             }
         }
     }
+    
 
     macro_rules! generate_unchecked_neg_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
@@ -1654,4 +1674,54 @@ mod verify {
     generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
     generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
     generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
+
+    // unchecked_mul proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(!self.overflowing_mul(rhs).1)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
+    // exponential state spaces for 32,64 and 128, hence provided limited range for verification.
+    generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8);
+    generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16);
+    generate_unchecked_mul_harness!(i32, unchecked_mul, checked_unchecked_mul_i32, -10_000i32, 10_000i32);
+    generate_unchecked_mul_harness!(i64, unchecked_mul, checked_unchecked_mul_i64, -1_000i64, 1_000i64);
+    generate_unchecked_mul_harness!(i128, unchecked_mul, checked_unchecked_mul_i128, -1_000_000_000_000_000i128, 1_000_000_000_000_000i128);
+    generate_unchecked_mul_harness!(isize, unchecked_mul, checked_unchecked_mul_isize, -100_000isize, 100_000isize);
+    generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8);
+    generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16);
+    generate_unchecked_mul_harness!(u32, unchecked_mul, checked_unchecked_mul_u32, 0u32, 20_000u32);
+    generate_unchecked_mul_harness!(u64, unchecked_mul, checked_unchecked_mul_u64, 0u64, 2_000u64);
+    generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128);
+    generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize);
+
+
+    // unchecked_shr proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(rhs < <$ActualT>::BITS)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
+    generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8);
+    generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16);
+    generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32);
+    generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64);
+    generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128);
+    generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize);
+    generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8);
+    generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16);
+    generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32);
+    generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
+    generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
+    generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
+        }
+    }
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index b12d82bdc720c..8706ed8bd6d5f 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -908,6 +908,7 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_mul(rhs).1)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1613,6 +1614,7 @@ macro_rules! uint_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < <$ActualT>::BITS)]// i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From dce9e831fca8c3109a565ef1d8423ded11eac118 Mon Sep 17 00:00:00 2001
From: yew005 <yew005@ucsd.edu>
Date: Sun, 29 Sep 2024 21:21:41 -0700
Subject: [PATCH 28/42] Add comments. Fix spacing

---
 library/core/src/num/mod.rs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 54e90d1bff0ff..3a83e75b74288 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1591,6 +1591,9 @@ from_str_radix_size_impl! { i64 isize, u64 usize }
 mod verify {
     use super::*;
 
+    // Verify `unchecked_{add, sub, mul}`
+    // However, `unchecked_mul` harnesses have bad performance, so
+    // recommend to use generate_unchecked_mul_harness! to set input limits
     macro_rules! generate_unchecked_math_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
             #[kani::proof_for_contract($type::$method)]
@@ -1605,14 +1608,15 @@ mod verify {
         }
     }
 
+    // Improve unchecked_mul performance for {32, 64, 128}-bit integer types
+    // by adding upper and lower limits for inputs
     macro_rules! generate_unchecked_mul_harness {
         ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => {
             #[kani::proof_for_contract($type::$method)]
             pub fn $harness_name() {
-                let num1: $type = kani::any();
-                let num2: $type = kani::any();
-    
-                // Limit the values of num1 and num2 to the specified range for multiplication
+                let num1: $type = kani::any::<$type>();
+                let num2: $type = kani::any::<$type>();
+
                 kani::assume(num1 >= $min && num1 <= $max);
                 kani::assume(num2 >= $min && num2 <= $max);
     
@@ -1622,8 +1626,8 @@ mod verify {
             }
         }
     }
-    
 
+    // Verify `unchecked_{shl, shr}`
     macro_rules! generate_unchecked_shift_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
             #[kani::proof_for_contract($type::$method)]
@@ -1637,7 +1641,6 @@ mod verify {
             }
         }
     }
-    
 
     macro_rules! generate_unchecked_neg_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
@@ -1699,7 +1702,6 @@ mod verify {
     generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128);
     generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize);
 
-
     // unchecked_shr proofs
     //
     // Target types:
@@ -1722,6 +1724,4 @@ mod verify {
     generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
     generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
     generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
-        }
-    }
 }

From 3880fc7b0f50b719b934eedc5497e7d59e1687e3 Mon Sep 17 00:00:00 2001
From: rajathmCMU <rajathkotyal@gmail.com>
Date: Wed, 2 Oct 2024 12:58:43 -0700
Subject: [PATCH 29/42] Revert "Add comments. Fix spacing"

This reverts commit dce9e831fca8c3109a565ef1d8423ded11eac118.
---
 library/core/src/num/mod.rs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 3a83e75b74288..54e90d1bff0ff 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1591,9 +1591,6 @@ from_str_radix_size_impl! { i64 isize, u64 usize }
 mod verify {
     use super::*;
 
-    // Verify `unchecked_{add, sub, mul}`
-    // However, `unchecked_mul` harnesses have bad performance, so
-    // recommend to use generate_unchecked_mul_harness! to set input limits
     macro_rules! generate_unchecked_math_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
             #[kani::proof_for_contract($type::$method)]
@@ -1608,15 +1605,14 @@ mod verify {
         }
     }
 
-    // Improve unchecked_mul performance for {32, 64, 128}-bit integer types
-    // by adding upper and lower limits for inputs
     macro_rules! generate_unchecked_mul_harness {
         ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => {
             #[kani::proof_for_contract($type::$method)]
             pub fn $harness_name() {
-                let num1: $type = kani::any::<$type>();
-                let num2: $type = kani::any::<$type>();
-
+                let num1: $type = kani::any();
+                let num2: $type = kani::any();
+    
+                // Limit the values of num1 and num2 to the specified range for multiplication
                 kani::assume(num1 >= $min && num1 <= $max);
                 kani::assume(num2 >= $min && num2 <= $max);
     
@@ -1626,8 +1622,8 @@ mod verify {
             }
         }
     }
+    
 
-    // Verify `unchecked_{shl, shr}`
     macro_rules! generate_unchecked_shift_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
             #[kani::proof_for_contract($type::$method)]
@@ -1641,6 +1637,7 @@ mod verify {
             }
         }
     }
+    
 
     macro_rules! generate_unchecked_neg_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
@@ -1702,6 +1699,7 @@ mod verify {
     generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128);
     generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize);
 
+
     // unchecked_shr proofs
     //
     // Target types:
@@ -1724,4 +1722,6 @@ mod verify {
     generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
     generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
     generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
+        }
+    }
 }

From 781cb87ed6976b255bc7fffa5227d2cf815ede6a Mon Sep 17 00:00:00 2001
From: rajathmCMU <rajathkotyal@gmail.com>
Date: Wed, 2 Oct 2024 12:58:47 -0700
Subject: [PATCH 30/42] Revert "unchecked_mul and unchecked_shr proofs (#7)"

This reverts commit 02d706a2f818cdacee696763b4185458a2fc90e5.
---
 library/core/src/num/int_macros.rs  |  2 -
 library/core/src/num/mod.rs         | 72 +----------------------------
 library/core/src/num/uint_macros.rs |  2 -
 3 files changed, 1 insertion(+), 75 deletions(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index a46e653de2bd0..fa3e4cef9bcb4 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -816,7 +816,6 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[requires(!self.overflowing_mul(rhs).1)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1425,7 +1424,6 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 54e90d1bff0ff..51bc33b7b47a4 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1605,39 +1605,19 @@ mod verify {
         }
     }
 
-    macro_rules! generate_unchecked_mul_harness {
-        ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => {
-            #[kani::proof_for_contract($type::$method)]
-            pub fn $harness_name() {
-                let num1: $type = kani::any();
-                let num2: $type = kani::any();
-    
-                // Limit the values of num1 and num2 to the specified range for multiplication
-                kani::assume(num1 >= $min && num1 <= $max);
-                kani::assume(num2 >= $min && num2 <= $max);
-    
-                unsafe {
-                    num1.$method(num2);
-                }
-            }
-        }
-    }
-    
-
     macro_rules! generate_unchecked_shift_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
             #[kani::proof_for_contract($type::$method)]
             pub fn $harness_name() {
                 let num1: $type = kani::any::<$type>();
                 let num2: u32 = kani::any::<u32>();
-    
+
                 unsafe {
                     num1.$method(num2);
                 }
             }
         }
     }
-    
 
     macro_rules! generate_unchecked_neg_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
@@ -1674,54 +1654,4 @@ mod verify {
     generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
     generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
     generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
-
-    // unchecked_mul proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
-    //
-    // Target contracts:
-    // #[requires(!self.overflowing_mul(rhs).1)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
-    // exponential state spaces for 32,64 and 128, hence provided limited range for verification.
-    generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8);
-    generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16);
-    generate_unchecked_mul_harness!(i32, unchecked_mul, checked_unchecked_mul_i32, -10_000i32, 10_000i32);
-    generate_unchecked_mul_harness!(i64, unchecked_mul, checked_unchecked_mul_i64, -1_000i64, 1_000i64);
-    generate_unchecked_mul_harness!(i128, unchecked_mul, checked_unchecked_mul_i128, -1_000_000_000_000_000i128, 1_000_000_000_000_000i128);
-    generate_unchecked_mul_harness!(isize, unchecked_mul, checked_unchecked_mul_isize, -100_000isize, 100_000isize);
-    generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8);
-    generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16);
-    generate_unchecked_mul_harness!(u32, unchecked_mul, checked_unchecked_mul_u32, 0u32, 20_000u32);
-    generate_unchecked_mul_harness!(u64, unchecked_mul, checked_unchecked_mul_u64, 0u64, 2_000u64);
-    generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128);
-    generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize);
-
-
-    // unchecked_shr proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
-    //
-    // Target contracts:
-    // #[requires(rhs < <$ActualT>::BITS)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
-    generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8);
-    generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16);
-    generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32);
-    generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64);
-    generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128);
-    generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize);
-    generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8);
-    generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16);
-    generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32);
-    generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
-    generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
-    generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
-        }
-    }
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 8706ed8bd6d5f..b12d82bdc720c 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -908,7 +908,6 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[requires(!self.overflowing_mul(rhs).1)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1614,7 +1613,6 @@ macro_rules! uint_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[requires(rhs < <$ActualT>::BITS)]// i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From 500e8dba61c74a9b941f97f510aba0d9db993988 Mon Sep 17 00:00:00 2001
From: rajathmCMU <rajathkotyal@gmail.com>
Date: Wed, 2 Oct 2024 13:03:51 -0700
Subject: [PATCH 31/42] Add comments. Fix spacing

---
 library/core/src/num/mod.rs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index b389468bac52e..afa9d4385fb3c 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1591,6 +1591,9 @@ from_str_radix_size_impl! { i64 isize, u64 usize }
 mod verify {
     use super::*;
 
+    // Verify `unchecked_{add, sub, mul}`
+    // However, `unchecked_mul` harnesses have bad performance, so
+    // recommend to use generate_unchecked_mul_harness! to set input limits
     macro_rules! generate_unchecked_math_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
             #[kani::proof_for_contract($type::$method)]
@@ -1605,14 +1608,15 @@ mod verify {
         }
     }
 
+    // Improve unchecked_mul performance for {32, 64, 128}-bit integer types
+    // by adding upper and lower limits for inputs
     macro_rules! generate_unchecked_mul_harness {
         ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => {
             #[kani::proof_for_contract($type::$method)]
             pub fn $harness_name() {
-                let num1: $type = kani::any();
-                let num2: $type = kani::any();
-    
-                // Limit the values of num1 and num2 to the specified range for multiplication
+                let num1: $type = kani::any::<$type>();
+                let num2: $type = kani::any::<$type>();
+
                 kani::assume(num1 >= $min && num1 <= $max);
                 kani::assume(num2 >= $min && num2 <= $max);
     
@@ -1622,8 +1626,8 @@ mod verify {
             }
         }
     }
-    
 
+    // Verify `unchecked_{shl, shr}`
     macro_rules! generate_unchecked_shift_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
             #[kani::proof_for_contract($type::$method)]
@@ -1637,7 +1641,6 @@ mod verify {
             }
         }
     }
-    
 
     macro_rules! generate_unchecked_neg_harness {
         ($type:ty, $method:ident, $harness_name:ident) => {
@@ -1699,7 +1702,6 @@ mod verify {
     generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128);
     generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize);
 
-
     // unchecked_shr proofs
     //
     // Target types:
@@ -1722,6 +1724,4 @@ mod verify {
     generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
     generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
     generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
-        }
-    }
 }

From 1c97825c7497118a4d0f27a265e0d1531cd9d3e4 Mon Sep 17 00:00:00 2001
From: Lanfei Ma <99311320+lanfeima@users.noreply.github.com>
Date: Wed, 2 Oct 2024 15:43:53 -0700
Subject: [PATCH 32/42] cleaned up code: deleted the previous attempted proofs

---
 kani                                          |  1 +
 .../core/tests/num/kani-proofs/i8-proofs.rs   | 65 -------------------
 2 files changed, 1 insertion(+), 65 deletions(-)
 create mode 160000 kani
 delete mode 100644 library/core/tests/num/kani-proofs/i8-proofs.rs

diff --git a/kani b/kani
new file mode 160000
index 0000000000000..4f75199d476c1
--- /dev/null
+++ b/kani
@@ -0,0 +1 @@
+Subproject commit 4f75199d476c10316e43171b662bf97a35cfdb29
diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs
deleted file mode 100644
index daa488a88a960..0000000000000
--- a/library/core/tests/num/kani-proofs/i8-proofs.rs
+++ /dev/null
@@ -1,65 +0,0 @@
-#[cfg(kani)]
-mod verification {
-    // use super::*;
-
-    #[kani::proof]
-    fn verify_i8_unchecked_add() {
-        let num1: i8 = kani::any::<i8>();
-        let num2: i8 = kani::any::<i8>();
-
-        // Safety preconditions:
-        // - Positive number addition won't overflow
-        // - Negative number addition won't underflow
-        // Addition of two integers with different signs never overflows
-        // Undefined behavior occurs when overflow or underflow happens
-        kani::assume(
-            (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2)
-                || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2),
-        );
-
-        unsafe {
-            let result = num1.unchecked_add(num2);
-            assert_eq!(Some(result), num1.checked_add(num2));
-        }
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_sub() {
-        let num1: i8 = kani::any::<i8>();
-        let num2: i8 = kani::any::<i8>();
-    
-        // Safety preconditions:
-        // - Subtraction won't underflow when num1 is positive and num2 is negative
-        // - Subtraction won't overflow when num1 is negative and num2 is positive
-        // Undefined behavior occurs when overflow or underflow happens
-        kani::assume(
-            (num1 >= 0 && num2 <= 0 && num1 <= i8::MAX + num2)
-                || (num1 <= 0 && num2 >= 0 && num1 >= i8::MIN + num2),
-        );
-    
-        unsafe {
-            let result = num1.unchecked_sub(num2);
-            assert_eq!(Some(result), num1.checked_sub(num2));
-        }   
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_mul() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_shl() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_shr() {
-        // TODO
-    }
-
-    #[kani::proof]
-    fn verify_i8_unchecked_neg() {
-        // TODO
-    }
-}

From e3eb36588bd38c1c0765d44dc159b9ff9edf7d70 Mon Sep 17 00:00:00 2001
From: MWDZ <jinjunfeng721@gmail.com>
Date: Wed, 2 Oct 2024 22:56:38 -0700
Subject: [PATCH 33/42] feat: merge the latest version

---
 doc/src/tools/kani.md               |  77 +++++++---
 library/core/src/num/int_macros.rs  |   3 +-
 library/core/src/num/mod.rs         | 223 +++++++++++++++-------------
 library/core/src/num/uint_macros.rs |   3 +-
 library/core/src/ptr/mod.rs         |   8 +-
 library/core/src/ptr/non_null.rs    |  34 +++++
 6 files changed, 225 insertions(+), 123 deletions(-)

diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md
index 985d507c4be33..9cfd198e9bc8e 100644
--- a/doc/src/tools/kani.md
+++ b/doc/src/tools/kani.md
@@ -5,7 +5,7 @@ Kani is designed to prove safety properties in your code as well as
 the absence of some forms of undefined behavior. It uses model checking under the hood to ensure that
 Rust programs adhere to user specified properties.
 
-You can find more information about how to install in [this section of the Kani book](https://model-checking.github.io/kani/install-guide.html).
+You can find more information about how to install in [the installation section of the Kani book](https://model-checking.github.io/kani/install-guide.html).
 
 ## Usage
 
@@ -27,7 +27,8 @@ fn harness() {
     let a = kani::any::<i32>();
     let b = kani::any::<i32>();
     let result = abs_diff(a, b);
-    kani::assert(result >= 0, "Result should always be more than 0");}
+    kani::assert(result >= 0, "Result should always be more than 0");
+}
 ```
 
 Running the command `cargo kani` in your cargo crate will give the result
@@ -46,29 +47,28 @@ Verification failed for - harness
 Complete - 0 successfully verified harnesses, 1 failures, 1 total.
 ```
 
+For a more detailed tutorial, you can refer to the [tutorial section of the Kani book](https://model-checking.github.io/kani/kani-tutorial.html).
 
 ## Using Kani to verify the Rust Standard Library
 
-To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started.
+Here is a short tutorial of how to use Kani to verify proofs for the standard library.
 
-### Step 1
+### Step 1 - Add some proofs to your copy of the model-checking std
 
-Modify your local copy of the Rust Standard Library by writing proofs for the functions/methods that you want to verify.
+Create a local copy of the [model-checking fork](https://github.com/model-checking/verify-rust-std) of the Rust Standard Library. The fork comes with Kani configured, so all you'll need to do is to call Kani's building-block APIs (such as
+`assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `modifies`, `requires` and `ensures`) directly.
 
-For example, insert this short blob into your copy of the library. This blob imports the building-block APIs such as
-`assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `proof_for_contract` and `fake_function`.
 
-``` rust
-#[cfg(kani)]
-kani_core::kani_lib!(core);
+For example, insert this module into an existing file in the core library, like `library/core/src/hint.rs` or `library/core/src/error.rs` in your copy of the library. This is just for the purpose of getting started, so you can insert in any existing file in the core library if you have other preferences.
 
+``` rust
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
 pub mod verify {
     use crate::kani;
 
     #[kani::proof]
-    pub fn harness() {
+    pub fn harness_introduction() {
         kani::assert(true, "yay");
     }
 
@@ -84,21 +84,24 @@ pub mod verify {
 }
 ```
 
-### Step 2
+### Step 2 - Run the Kani verify-std subcommand
 
-Run the following command in your local terminal:
+To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started.
+Run the following command in your local terminal (Replace "/path/to/library" and "/path/to/target" with your local paths) from the verify repository root:
 
-`kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing`.
+```
+kani verify-std -Z unstable-options "/path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z mem-predicates
+```
 
 The command `kani verify-std` is a sub-command of the `kani`. This specific sub-command is used to verify the Rust Standard Library with the following arguments.
 
-- `"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script.
-- `--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files.
+- `"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script. For example, `./library` or `/home/ubuntu/verify-rust-std/library`
+- `--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files. For example, `/tmp` or `/tmp/verify-std`
 
-Apart from these, you can use your regular `kani-args` such as `-Z function-contracts` and `-Z stubbing` depending on your verification needs.
+Apart from these, you can use your regular `kani-args` such as `-Z function-contracts`, `-Z stubbing` and `-Z mem-predicates` depending on your verification needs. If you run into a Kani error that says `Use of unstable feature`, add the corresponding feature with `-Z` to the command line.
 For more details on Kani's features, refer to [the features section in the Kani Book](https://model-checking.github.io/kani/reference/attributes.html)
 
-### Step 3
+### Step 3 - Check verification result
 
 After running the command, you can expect an output that looks like this:
 
@@ -112,6 +115,44 @@ Verification Time: 0.017101772s
 Complete - 2 successfully verified harnesses, 0 failures, 2 total.
 ```
 
+### Running on a specific harness
+
+You can specify a specific harness to be verified using the `--harness` flag.
+
+For example, in your local copy of the verify repo, run the following command.
+
+```
+kani verify-std --harness harness_introduction -Z unstable-options "./library" --target-dir "/tmp" -Z function-contracts -Z mem-predicates
+```
+
+This gives you the verification result for just `harness_introduction` from the aforementioned blob.
+
+```
+RESULTS:
+Check 1: verify::harness_introduction.assertion.1
+         - Status: SUCCESS
+         - Description: "yay"
+         - Location: library/core/src/lib.rs:479:9 in function verify::harness_introduction
+
+
+SUMMARY:
+ ** 0 of 1 failed
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01885804s
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
+```
+
+Now you can write proof harnesses to verify specific functions in the library. 
+The current convention is to keep proofs in the same module file of the verification target. 
+To run Kani for an individual proof, use `--harness [harness_function_name]`. 
+Note that Kani will batch run all proofs in the library folder if you do not supply the `--harness` flag. 
+If Kani returns the error `no harnesses matched the harness filter`, you can give the full name of the harness. 
+For example, to run the proof harness named `check_new` in `library/core/src/ptr/unique.rs`, use 
+`--harness ptr::unique::verify::check_new`. To run all proofs in `unique.rs`, use `--harness ptr::unique::verify`. 
+To find the full name of a harness, check the Kani output and find the line starting with `Checking harness [harness full name]`.
+
 ## More details
 
 You can find more information about how to install and how you can customize your use of Kani in the
diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 486f9493b7148..29c9e048bd93a 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -512,7 +512,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_add(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -817,6 +816,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_mul(rhs).1)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1427,6 +1427,7 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 3d65b60b155f7..6c96c769cc736 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1401,10 +1401,7 @@ const fn from_str_radix_panic_ct(_radix: u32) -> ! {
 
 #[track_caller]
 fn from_str_radix_panic_rt(radix: u32) -> ! {
-    panic!(
-        "from_str_radix_int: must lie in the range `[2, 36]` - found {}",
-        radix
-    );
+    panic!("from_str_radix_int: must lie in the range `[2, 36]` - found {}", radix);
 }
 
 #[cfg_attr(not(feature = "panic_immediate_abort"), inline(never))]
@@ -1589,120 +1586,144 @@ from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
 
+#[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
 
-    // `unchecked_add` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
-    //
-    // Target contracts:
-    // #[requires(!self.overflowing_add(rhs).1)]
-    // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
-    #[kani::proof_for_contract(i8::unchecked_add)]
-    pub fn check_unchecked_add_i8() {
-        let num1: i8 = kani::any::<i8>();
-        let num2: i8 = kani::any::<i8>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i16::unchecked_add)]
-    pub fn check_unchecked_add_i16() {
-        let num1: i16 = kani::any::<i16>();
-        let num2: i16 = kani::any::<i16>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i32::unchecked_add)]
-    pub fn check_unchecked_add_i32() {
-        let num1: i32 = kani::any::<i32>();
-        let num2: i32 = kani::any::<i32>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i64::unchecked_add)]
-    pub fn check_unchecked_add_i64() {
-        let num1: i64 = kani::any::<i64>();
-        let num2: i64 = kani::any::<i64>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(i128::unchecked_add)]
-    pub fn check_unchecked_add_i128() {
-        let num1: i128 = kani::any::<i128>();
-        let num2: i128 = kani::any::<i128>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
-
-    #[kani::proof_for_contract(u8::unchecked_add)]
-    pub fn check_unchecked_add_u8() {
-        let num1: u8 = kani::any::<u8>();
-        let num2: u8 = kani::any::<u8>();
-
-        unsafe {
-            num1.unchecked_add(num2);
+    // Verify `unchecked_{add, sub, mul}`
+    // However, `unchecked_mul` harnesses have bad performance, so
+    // recommend to use generate_unchecked_mul_harness! to set input limits
+    macro_rules! generate_unchecked_math_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: $type = kani::any::<$type>();
+
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
         }
     }
 
-    #[kani::proof_for_contract(u16::unchecked_add)]
-    pub fn check_unchecked_add_u16() {
-        let num1: u16 = kani::any::<u16>();
-        let num2: u16 = kani::any::<u16>();
-
-        unsafe {
-            num1.unchecked_add(num2);
+    // Improve unchecked_mul performance for {32, 64, 128}-bit integer types
+    // by adding upper and lower limits for inputs
+    macro_rules! generate_unchecked_mul_harness {
+        ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: $type = kani::any::<$type>();
+
+                kani::assume(num1 >= $min && num1 <= $max);
+                kani::assume(num2 >= $min && num2 <= $max);
+    
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
         }
     }
 
-    #[kani::proof_for_contract(u32::unchecked_add)]
-    pub fn check_unchecked_add_u32() {
-        let num1: u32 = kani::any::<u32>();
-        let num2: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_add(num2);
+    // Verify `unchecked_{shl, shr}`
+    macro_rules! generate_unchecked_shift_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: u32 = kani::any::<u32>();
+    
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
         }
     }
 
-    #[kani::proof_for_contract(u64::unchecked_add)]
-    pub fn check_unchecked_add_u64() {
-        let num1: u64 = kani::any::<u64>();
-        let num2: u64 = kani::any::<u64>();
+    macro_rules! generate_unchecked_neg_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
 
-        unsafe {
-            num1.unchecked_add(num2);
+                unsafe {
+                    num1.$method();
+                }
+            }
         }
     }
 
-    #[kani::proof_for_contract(u128::unchecked_add)]
-    pub fn check_unchecked_add_u128() {
-        let num1: u128 = kani::any::<u128>();
-        let num2: u128 = kani::any::<u128>();
-
-        unsafe {
-            num1.unchecked_add(num2);
-        }
-    }
+    // `unchecked_add` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(!self.overflowing_add(rhs).1)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
+    generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
+    generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16);
+    generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32);
+    generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64);
+    generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128);
+    generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize);
+    generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8);
+    generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16);
+    generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32);
+    generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
+    generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
+    generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
+
+    // unchecked_mul proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(!self.overflowing_mul(rhs).1)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
+    // exponential state spaces for 32,64 and 128, hence provided limited range for verification.
+    generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8);
+    generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16);
+    generate_unchecked_mul_harness!(i32, unchecked_mul, checked_unchecked_mul_i32, -10_000i32, 10_000i32);
+    generate_unchecked_mul_harness!(i64, unchecked_mul, checked_unchecked_mul_i64, -1_000i64, 1_000i64);
+    generate_unchecked_mul_harness!(i128, unchecked_mul, checked_unchecked_mul_i128, -1_000_000_000_000_000i128, 1_000_000_000_000_000i128);
+    generate_unchecked_mul_harness!(isize, unchecked_mul, checked_unchecked_mul_isize, -100_000isize, 100_000isize);
+    generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8);
+    generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16);
+    generate_unchecked_mul_harness!(u32, unchecked_mul, checked_unchecked_mul_u32, 0u32, 20_000u32);
+    generate_unchecked_mul_harness!(u64, unchecked_mul, checked_unchecked_mul_u64, 0u64, 2_000u64);
+    generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128);
+    generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize);
+
+    // unchecked_shr proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(rhs < <$ActualT>::BITS)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
+    generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8);
+    generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16);
+    generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32);
+    generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64);
+    generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128);
+    generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize);
+    generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8);
+    generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16);
+    generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32);
+    generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
+    generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
+    generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
 
     // `unchecked_shl` proofs
     //
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 617db39cbc220..44f942d0cffd9 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -559,7 +559,6 @@ macro_rules! uint_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_add(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -909,6 +908,7 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_mul(rhs).1)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1616,6 +1616,7 @@ macro_rules! uint_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < <$ActualT>::BITS)]// i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index 43d81348cb1a8..2f92443cf1656 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -2552,8 +2552,12 @@ mod verify {
     }
 
     #[kani::proof_for_contract(align_offset)]
-    fn check_align_offset_17() {
-        let p = kani::any::<usize>() as *const [char; 17];
+    // The purpose of this harness is to test align_offset with a pointee type whose stride is not a power of two
+    // Keeping the size smaller (5) and changing the solver to kissat improves verification time
+    // c.f. https://github.com/model-checking/verify-rust-std/pull/89
+    #[kani::solver(kissat)]
+    fn check_align_offset_5() {
+        let p = kani::any::<usize>() as *const [char; 5];
         check_align_offset(p);
     }
 
diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index b1429fff74434..4d6e484915dbf 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -8,6 +8,11 @@ use crate::ptr::Unique;
 use crate::slice::{self, SliceIndex};
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{fmt, hash, intrinsics, ptr};
+use safety::{ensures, requires};
+
+
+#[cfg(kani)]
+use crate::kani;
 
 /// `*mut T` but non-zero and [covariant].
 ///
@@ -192,6 +197,8 @@ impl<T: ?Sized> NonNull<T> {
     #[stable(feature = "nonnull", since = "1.25.0")]
     #[rustc_const_stable(feature = "const_nonnull_new_unchecked", since = "1.25.0")]
     #[inline]
+    #[requires(!ptr.is_null())]
+    #[ensures(|result| result.as_ptr() == ptr)]
     pub const unsafe fn new_unchecked(ptr: *mut T) -> Self {
         // SAFETY: the caller must guarantee that `ptr` is non-null.
         unsafe {
@@ -221,6 +228,8 @@ impl<T: ?Sized> NonNull<T> {
     #[stable(feature = "nonnull", since = "1.25.0")]
     #[rustc_const_unstable(feature = "const_nonnull_new", issue = "93235")]
     #[inline]
+    #[ensures(|result| result.is_some() == !ptr.is_null())]
+    #[ensures(|result| result.is_none() || result.expect("ptr is null!").as_ptr() == ptr)]
     pub const fn new(ptr: *mut T) -> Option<Self> {
         if !ptr.is_null() {
             // SAFETY: The pointer is already checked and is not null
@@ -1770,3 +1779,28 @@ impl<T: ?Sized> From<&T> for NonNull<T> {
         unsafe { NonNull { pointer: reference as *const T } }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+    use crate::ptr::null_mut;
+
+    // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
+    #[kani::proof_for_contract(NonNull::new_unchecked)]
+    pub fn non_null_check_new_unchecked() {
+        let raw_ptr = kani::any::<usize>() as *mut i32;
+        unsafe {
+            let _ = NonNull::new_unchecked(raw_ptr);
+        }
+    }
+
+    // pub const unsafe fn new(ptr: *mut T) -> Option<Self>
+    #[kani::proof_for_contract(NonNull::new)]
+    pub fn non_null_check_new() {
+        let mut x: i32 = kani::any();
+        let xptr = &mut x;
+        let maybe_null_ptr =  if kani::any() { xptr as *mut i32 } else { null_mut() };
+        let _ = NonNull::new(maybe_null_ptr);
+    }
+}

From 2b3771f64f0cb31eb652fec5aab3eb828a73ee02 Mon Sep 17 00:00:00 2001
From: MWDZ <jinjunfeng721@gmail.com>
Date: Wed, 2 Oct 2024 23:06:17 -0700
Subject: [PATCH 34/42] feat: use macro rules for unchecked_shl harness

---
 library/core/src/num/int_macros.rs  |   3 +-
 library/core/src/num/mod.rs         | 110 +++-------------------------
 library/core/src/num/uint_macros.rs |   3 +-
 3 files changed, 14 insertions(+), 102 deletions(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 29c9e048bd93a..17c9ac57b3626 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -1299,8 +1299,7 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[requires(rhs < Self::BITS)]
-        #[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)]
+        #[requires(rhs < <$ActualT>::BITS)] 
         pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 6c96c769cc736..c0ea579486d14 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1738,103 +1738,17 @@ mod verify {
     // pub const unsafe fn unchecked_shl(self, shift: u32) -> Self
     //
     // This function performs an unchecked bitwise left shift operation.
-    #[kani::proof_for_contract(i8::unchecked_shl)]
-    pub fn check_unchecked_shl_i8() {
-        let num1: i8 = kani::any::<i8>();
-        let shift: u32 = kani::any::<u32>();
+    generate_unchecked_shift_harness!(i8, unchecked_shl, checked_unchecked_shl_i8);
+    generate_unchecked_shift_harness!(i16, unchecked_shl, checked_unchecked_shl_i16);
+    generate_unchecked_shift_harness!(i32, unchecked_shl, checked_unchecked_shl_i32);
+    generate_unchecked_shift_harness!(i64, unchecked_shl, checked_unchecked_shl_i64);
+    generate_unchecked_shift_harness!(i128, unchecked_shl, checked_unchecked_shl_i128);
+    generate_unchecked_shift_harness!(isize, unchecked_shl, checked_unchecked_shl_isize);
+    generate_unchecked_shift_harness!(u8, unchecked_shl, checked_unchecked_shl_u8);
+    generate_unchecked_shift_harness!(u16, unchecked_shl, checked_unchecked_shl_u16);
+    generate_unchecked_shift_harness!(u32, unchecked_shl, checked_unchecked_shl_u32);
+    generate_unchecked_shift_harness!(u64, unchecked_shl, checked_unchecked_shl_u64);
+    generate_unchecked_shift_harness!(u128, unchecked_shl, checked_unchecked_shl_u128);
+    generate_unchecked_shift_harness!(usize, unchecked_shl, checked_unchecked_shl_usize);
 
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(i16::unchecked_shl)]
-    pub fn check_unchecked_shl_i16() {
-        let num1: i16 = kani::any::<i16>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(i32::unchecked_shl)]
-    pub fn check_unchecked_shl_i32() {
-        let num1: i32 = kani::any::<i32>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(i64::unchecked_shl)]
-    pub fn check_unchecked_shl_i64() {
-        let num1: i64 = kani::any::<i64>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(i128::unchecked_shl)]
-    pub fn check_unchecked_shl_i128() {
-        let num1: i128 = kani::any::<i128>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u8::unchecked_shl)]
-    pub fn check_unchecked_shl_u8() {
-        let num1: u8 = kani::any::<u8>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u16::unchecked_shl)]
-    pub fn check_unchecked_shl_u16() {
-        let num1: u16 = kani::any::<u16>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u32::unchecked_shl)]
-    pub fn check_unchecked_shl_u32() {
-        let num1: u32 = kani::any::<u32>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u64::unchecked_shl)]
-    pub fn check_unchecked_shl_u64() {
-        let num1: u64 = kani::any::<u64>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
-
-    #[kani::proof_for_contract(u128::unchecked_shl)]
-    pub fn check_unchecked_shl_u128() {
-        let num1: u128 = kani::any::<u128>();
-        let shift: u32 = kani::any::<u32>();
-
-        unsafe {
-            num1.unchecked_shl(shift);
-        }
-    }
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 44f942d0cffd9..fca28f5556994 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -1488,8 +1488,7 @@ macro_rules! uint_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[requires(rhs < Self::BITS)]
-        #[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)]
+        #[requires(rhs < <$ActualT>::BITS)]
         pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From 49b0a6b7d51dcbabeb8abda06a9a1dabe7837748 Mon Sep 17 00:00:00 2001
From: rajathmCMU <rajathkotyal@gmail.com>
Date: Fri, 4 Oct 2024 23:58:49 -0700
Subject: [PATCH 35/42] add interval checks to unchecked_mul

---
 library/core/src/num/mod.rs | 90 +++++++++++++++++++++++++++----------
 1 file changed, 66 insertions(+), 24 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index c07eadc1f518d..b949d2c11aca5 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1610,20 +1610,25 @@ mod verify {
 
     // Improve unchecked_mul performance for {32, 64, 128}-bit integer types
     // by adding upper and lower limits for inputs
-    macro_rules! generate_unchecked_mul_harness {
-        ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => {
-            #[kani::proof_for_contract($type::$method)]
-            pub fn $harness_name() {
-                let num1: $type = kani::any::<$type>();
-                let num2: $type = kani::any::<$type>();
-
-                kani::assume(num1 >= $min && num1 <= $max);
-                kani::assume(num2 >= $min && num2 <= $max);
+    macro_rules! generate_unchecked_mul_intervals {
+        ($type:ty, $method:ident, $($harness_name:ident, $min:expr, $max:expr),+) => {
+            $(
+                #[kani::proof_for_contract($type::$method)]
+                pub fn $harness_name() {
+                    let num1: $type = kani::any::<$type>();
+                    let num2: $type = kani::any::<$type>();
     
-                unsafe {
-                    num1.$method(num2);
+                    kani::assume(num1 >= $min && num1 <= $max);
+                    kani::assume(num2 >= $min && num2 <= $max);
+    
+                    // Ensure that multiplication does not overflow
+                    kani::assume(!num1.overflowing_mul(num2).1);
+    
+                    unsafe {
+                        num1.$method(num2);
+                    }
                 }
-            }
+            )+
         }
     }
 
@@ -1689,18 +1694,55 @@ mod verify {
     // Target function:
     // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
     // exponential state spaces for 32,64 and 128, hence provided limited range for verification.
-    generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8);
-    generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16);
-    generate_unchecked_mul_harness!(i32, unchecked_mul, checked_unchecked_mul_i32, -10_000i32, 10_000i32);
-    generate_unchecked_mul_harness!(i64, unchecked_mul, checked_unchecked_mul_i64, -1_000i64, 1_000i64);
-    generate_unchecked_mul_harness!(i128, unchecked_mul, checked_unchecked_mul_i128, -1_000_000_000_000_000i128, 1_000_000_000_000_000i128);
-    generate_unchecked_mul_harness!(isize, unchecked_mul, checked_unchecked_mul_isize, -100_000isize, 100_000isize);
-    generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8);
-    generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16);
-    generate_unchecked_mul_harness!(u32, unchecked_mul, checked_unchecked_mul_u32, 0u32, 20_000u32);
-    generate_unchecked_mul_harness!(u64, unchecked_mul, checked_unchecked_mul_u64, 0u64, 2_000u64);
-    generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128);
-    generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize);
+
+    // ====================== i128 Harnesses ======================
+    generate_unchecked_mul_intervals!(i128, unchecked_mul,
+        unchecked_mul_i128_small, -10i128, 10i128,
+        unchecked_mul_i128_large_pos, i128::MAX - 1000i128, i128::MAX,
+        unchecked_mul_i128_large_neg, i128::MIN, i128::MIN + 1000i128,
+        unchecked_mul_i128_edge_pos, i128::MAX / 2, i128::MAX,
+        unchecked_mul_i128_edge_neg, i128::MIN, i128::MIN / 2
+    );
+
+    // ====================== u128 Harnesses ======================
+    generate_unchecked_mul_intervals!(u128, unchecked_mul,
+        unchecked_mul_u128_small, 0u128, 10u128,
+        unchecked_mul_u128_large, u128::MAX - 1000u128, u128::MAX,
+        unchecked_mul_u128_edge, u128::MAX / 2, u128::MAX
+    );
+
+    // ====================== i64 Harnesses ======================
+    generate_unchecked_mul_intervals!(i64, unchecked_mul,
+        unchecked_mul_i64_small, -10i64, 10i64,
+        unchecked_mul_i64_large_pos, i64::MAX - 1000i64, i64::MAX,
+        unchecked_mul_i64_large_neg, i64::MIN, i64::MIN + 1000i64,
+        unchecked_mul_i64_edge_pos, i64::MAX / 2, i64::MAX,
+        unchecked_mul_i64_edge_neg, i64::MIN, i64::MIN / 2
+    );
+
+    // ====================== u64 Harnesses ======================
+    generate_unchecked_mul_intervals!(u64, unchecked_mul,
+        unchecked_mul_u64_small, 0u64, 10u64,
+        unchecked_mul_u64_large, u64::MAX - 1000u64, u64::MAX,
+        unchecked_mul_u64_edge, u64::MAX / 2, u64::MAX
+    );
+
+    // ====================== i32 Harnesses ======================
+    generate_unchecked_mul_intervals!(i32, unchecked_mul,
+        unchecked_mul_i32_small, -10i32, 10i32,
+        unchecked_mul_i32_large_pos, i32::MAX - 1000i32, i32::MAX,
+        unchecked_mul_i32_large_neg, i32::MIN, i32::MIN + 1000i32,
+        unchecked_mul_i32_edge_pos, i32::MAX / 2, i32::MAX,
+        unchecked_mul_i32_edge_neg, i32::MIN, i32::MIN / 2
+    );
+
+    // ====================== u32 Harnesses ======================
+    generate_unchecked_mul_intervals!(u32, unchecked_mul,
+        unchecked_mul_u32_small, 0u32, 10u32,
+        unchecked_mul_u32_large, u32::MAX - 1000u32, u32::MAX,
+        unchecked_mul_u32_edge, u32::MAX / 2, u32::MAX
+    );
+
 
     // unchecked_shr proofs
     //

From bbb9656109d7328968afd432a0f5c7f42f6f7993 Mon Sep 17 00:00:00 2001
From: rajathmCMU <rajathkotyal@gmail.com>
Date: Sat, 5 Oct 2024 00:12:59 -0700
Subject: [PATCH 36/42] unchecked neg fix

---
 library/core/src/num/mod.rs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 5db7e7444753f..46dd4e42f06b0 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1646,15 +1646,12 @@ mod verify {
     }
 
     macro_rules! generate_unchecked_neg_harness {
-        ($type:ty, $method:ident, $harness_name:ident) => {
-            #[kani::proof_for_contract($type::$method)]
         ($type:ty, $harness_name:ident) => {
             #[kani::proof_for_contract($type::unchecked_neg)]
             pub fn $harness_name() {
                 let num1: $type = kani::any::<$type>();
 
                 unsafe {
-                    num1.$method();
                     num1.unchecked_neg();
                 }
             }

From cafeea653b59e79f713649d8567d32e3f113106b Mon Sep 17 00:00:00 2001
From: rajathmCMU <rajathkotyal@gmail.com>
Date: Sat, 5 Oct 2024 00:32:38 -0700
Subject: [PATCH 37/42] add missing i8, i16 unchecked_mul

---
 library/core/src/num/mod.rs | 76 ++++++++++++++++++++++---------------
 1 file changed, 45 insertions(+), 31 deletions(-)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 46dd4e42f06b0..d38364715a730 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1684,7 +1684,7 @@ mod verify {
     // unchecked_mul proofs
     //
     // Target types:
-    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
+    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 36 types in total
     //
     // Target contracts:
     // #[requires(!self.overflowing_mul(rhs).1)]
@@ -1692,7 +1692,25 @@ mod verify {
     // Target function:
     // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
     // exponential state spaces for 32,64 and 128, hence provided limited range for verification.
+    generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8);
+    generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16);
 
+    // ====================== i32 Harnesses ======================
+    generate_unchecked_mul_intervals!(i32, unchecked_mul,
+        unchecked_mul_i32_small, -10i32, 10i32,
+        unchecked_mul_i32_large_pos, i32::MAX - 1000i32, i32::MAX,
+        unchecked_mul_i32_large_neg, i32::MIN, i32::MIN + 1000i32,
+        unchecked_mul_i32_edge_pos, i32::MAX / 2, i32::MAX,
+        unchecked_mul_i32_edge_neg, i32::MIN, i32::MIN / 2
+    );
+    // ====================== i64 Harnesses ======================
+    generate_unchecked_mul_intervals!(i64, unchecked_mul,
+        unchecked_mul_i64_small, -10i64, 10i64,
+        unchecked_mul_i64_large_pos, i64::MAX - 1000i64, i64::MAX,
+        unchecked_mul_i64_large_neg, i64::MIN, i64::MIN + 1000i64,
+        unchecked_mul_i64_edge_pos, i64::MAX / 2, i64::MAX,
+        unchecked_mul_i64_edge_neg, i64::MIN, i64::MIN / 2
+    );
     // ====================== i128 Harnesses ======================
     generate_unchecked_mul_intervals!(i128, unchecked_mul,
         unchecked_mul_i128_small, -10i128, 10i128,
@@ -1701,47 +1719,43 @@ mod verify {
         unchecked_mul_i128_edge_pos, i128::MAX / 2, i128::MAX,
         unchecked_mul_i128_edge_neg, i128::MIN, i128::MIN / 2
     );
-
-    // ====================== u128 Harnesses ======================
-    generate_unchecked_mul_intervals!(u128, unchecked_mul,
-        unchecked_mul_u128_small, 0u128, 10u128,
-        unchecked_mul_u128_large, u128::MAX - 1000u128, u128::MAX,
-        unchecked_mul_u128_edge, u128::MAX / 2, u128::MAX
+    // ====================== isize Harnesses ======================
+    generate_unchecked_mul_intervals!(isize, unchecked_mul,
+        unchecked_mul_isize_small, -10isize, 10isize,
+        unchecked_mul_isize_large_pos, isize::MAX - 1000isize, isize::MAX,
+        unchecked_mul_isize_large_neg, isize::MIN, isize::MIN + 1000isize,
+        unchecked_mul_isize_edge_pos, isize::MAX / 2, isize::MAX,
+        unchecked_mul_isize_edge_neg, isize::MIN, isize::MIN / 2
     );
 
-    // ====================== i64 Harnesses ======================
-    generate_unchecked_mul_intervals!(i64, unchecked_mul,
-        unchecked_mul_i64_small, -10i64, 10i64,
-        unchecked_mul_i64_large_pos, i64::MAX - 1000i64, i64::MAX,
-        unchecked_mul_i64_large_neg, i64::MIN, i64::MIN + 1000i64,
-        unchecked_mul_i64_edge_pos, i64::MAX / 2, i64::MAX,
-        unchecked_mul_i64_edge_neg, i64::MIN, i64::MIN / 2
-    );
+    generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8);
+    generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16);
 
+    // ====================== u32 Harnesses ======================
+    generate_unchecked_mul_intervals!(u32, unchecked_mul,
+        unchecked_mul_u32_small, 0u32, 10u32,
+        unchecked_mul_u32_large, u32::MAX - 1000u32, u32::MAX,
+        unchecked_mul_u32_edge, u32::MAX / 2, u32::MAX
+    );
     // ====================== u64 Harnesses ======================
     generate_unchecked_mul_intervals!(u64, unchecked_mul,
         unchecked_mul_u64_small, 0u64, 10u64,
         unchecked_mul_u64_large, u64::MAX - 1000u64, u64::MAX,
         unchecked_mul_u64_edge, u64::MAX / 2, u64::MAX
     );
-
-    // ====================== i32 Harnesses ======================
-    generate_unchecked_mul_intervals!(i32, unchecked_mul,
-        unchecked_mul_i32_small, -10i32, 10i32,
-        unchecked_mul_i32_large_pos, i32::MAX - 1000i32, i32::MAX,
-        unchecked_mul_i32_large_neg, i32::MIN, i32::MIN + 1000i32,
-        unchecked_mul_i32_edge_pos, i32::MAX / 2, i32::MAX,
-        unchecked_mul_i32_edge_neg, i32::MIN, i32::MIN / 2
+    // ====================== u128 Harnesses ======================
+    generate_unchecked_mul_intervals!(u128, unchecked_mul,
+        unchecked_mul_u128_small, 0u128, 10u128,
+        unchecked_mul_u128_large, u128::MAX - 1000u128, u128::MAX,
+        unchecked_mul_u128_edge, u128::MAX / 2, u128::MAX
     );
-
-    // ====================== u32 Harnesses ======================
-    generate_unchecked_mul_intervals!(u32, unchecked_mul,
-        unchecked_mul_u32_small, 0u32, 10u32,
-        unchecked_mul_u32_large, u32::MAX - 1000u32, u32::MAX,
-        unchecked_mul_u32_edge, u32::MAX / 2, u32::MAX
+    // ====================== usize Harnesses ======================
+    generate_unchecked_mul_intervals!(usize, unchecked_mul,
+        unchecked_mul_usize_small, 0usize, 10usize,
+        unchecked_mul_usize_large, usize::MAX - 1000usize, usize::MAX,
+        unchecked_mul_usize_edge, usize::MAX / 2, usize::MAX
     );
 
-
     // unchecked_shr proofs
     //
     // Target types:
@@ -1768,7 +1782,7 @@ mod verify {
     // `unchecked_shl` proofs
     //
     // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 12 types in total
     //
     // Target contracts:
     // #[requires(shift < Self::BITS)]

From 7f4421cfcc4b3f5372a509913739caf7f3bcd383 Mon Sep 17 00:00:00 2001
From: Lanfei Ma <99311320+lanfeima@users.noreply.github.com>
Date: Sat, 5 Oct 2024 23:49:14 -0700
Subject: [PATCH 38/42] deleted the postconditions of unchecked_sub

---
 library/core/src/num/int_macros.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 086f9230edc82..cf04b9fcbb707 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -665,7 +665,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
-        #[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)] // Postconditions: Result must be within valid bounds
         pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From 1331a778111d21860b7083359b1c56c6ba9b93d2 Mon Sep 17 00:00:00 2001
From: Lanfei Ma <99311320+lanfeima@users.noreply.github.com>
Date: Sat, 5 Oct 2024 23:50:28 -0700
Subject: [PATCH 39/42] deleted the postconditions for the unchecked_sub in
 uint_macros

---
 library/core/src/num/uint_macros.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 647a94bca00a8..0576e087935bb 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -752,7 +752,6 @@ macro_rules! uint_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
-        #[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)] // Postconditions: Result must be within valid bounds
         pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

From c413cac2b149dbaba334dda0d6c96a4789060dc6 Mon Sep 17 00:00:00 2001
From: Lanfei Ma <99311320+lanfeima@users.noreply.github.com>
Date: Sun, 6 Oct 2024 00:14:30 -0700
Subject: [PATCH 40/42] refacted uncheck_sub harnesses

---
 library/core/src/num/mod.rs | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index f318f72382008..231c6f7ac41d1 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1805,4 +1805,17 @@ mod verify {
     generate_unchecked_shift_harness!(u64, unchecked_shl, checked_unchecked_shl_u64);
     generate_unchecked_shift_harness!(u128, unchecked_shl, checked_unchecked_shl_u128);
     generate_unchecked_shift_harness!(usize, unchecked_shl, checked_unchecked_shl_usize);
+
+    generate_unchecked_math_harness!(i8, unchecked_sub, checked_unchecked_sub_i8);
+    generate_unchecked_math_harness!(i16, unchecked_sub, checked_unchecked_sub_i16);
+    generate_unchecked_math_harness!(i32, unchecked_sub, checked_unchecked_sub_i32);
+    generate_unchecked_math_harness!(i64, unchecked_sub, checked_unchecked_sub_i64);
+    generate_unchecked_math_harness!(i128, unchecked_sub, checked_unchecked_sub_i128);
+    generate_unchecked_math_harness!(isize, unchecked_sub, checked_unchecked_sub_isize);
+    generate_unchecked_math_harness!(u8, unchecked_sub, checked_unchecked_sub_u8);
+    generate_unchecked_math_harness!(u16, unchecked_sub, checked_unchecked_sub_u16);
+    generate_unchecked_math_harness!(u32, unchecked_sub, checked_unchecked_sub_u32);
+    generate_unchecked_math_harness!(u64, unchecked_sub, checked_unchecked_sub_u64);
+    generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128);
+    generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize);
 }

From 3dd368ed237bfd6f00f13d23ec74d06dc875880e Mon Sep 17 00:00:00 2001
From: rajathmCMU <rajathkotyal@gmail.com>
Date: Mon, 7 Oct 2024 10:01:12 -0700
Subject: [PATCH 41/42] removed empty submodule

---
 kani | 1 -
 1 file changed, 1 deletion(-)
 delete mode 160000 kani

diff --git a/kani b/kani
deleted file mode 160000
index 4f75199d476c1..0000000000000
--- a/kani
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 4f75199d476c10316e43171b662bf97a35cfdb29

From d971f5c0304fb9373c35857d85a5c1bc8e1ed07c Mon Sep 17 00:00:00 2001
From: rajathmCMU <rajathkotyal@gmail.com>
Date: Mon, 7 Oct 2024 10:12:41 -0700
Subject: [PATCH 42/42] add comments to unchecked_sub

---
 library/core/src/num/mod.rs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 231c6f7ac41d1..1668adca30905 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1806,6 +1806,18 @@ mod verify {
     generate_unchecked_shift_harness!(u128, unchecked_shl, checked_unchecked_shl_u128);
     generate_unchecked_shift_harness!(usize, unchecked_shl, checked_unchecked_shl_usize);
 
+    // `unchecked_sub` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_sub(self, rhs: Self)  -> Self
+    //
+    // This function performs an unchecked subtraction operation.
     generate_unchecked_math_harness!(i8, unchecked_sub, checked_unchecked_sub_i8);
     generate_unchecked_math_harness!(i16, unchecked_sub, checked_unchecked_sub_i16);
     generate_unchecked_math_harness!(i32, unchecked_sub, checked_unchecked_sub_i32);