From 99ea78b33b585880284c875d9818ae42a6f90a85 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 12 Aug 2025 13:58:20 +0000
Subject: [PATCH 1/2] Remove spurious comments about the need for quantifiers

None of the (three) cases where we previously claimed a need for
quantifiers actually require them.
---
 library/core/src/intrinsics/mod.rs |  6 ++++--
 library/core/src/ptr/mod.rs        | 13 ++++---------
 library/core/src/ptr/non_null.rs   |  7 +++----
 3 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs
index e099c28646015..32c0bb66024b1 100644
--- a/library/core/src/intrinsics/mod.rs
+++ b/library/core/src/intrinsics/mod.rs
@@ -3222,14 +3222,16 @@ pub const unsafe fn copysignf128(x: f128, y: f128) -> f128;
 /// initialization state.
 ///
 /// This is used for contracts only.
-///
-/// FIXME: Change this once we add support to quantifiers.
 #[allow(dead_code)]
 #[allow(unused_variables)]
 fn check_copy_untyped<T>(src: *const T, dst: *mut T, count: usize) -> bool {
     #[cfg(kani)]
     if count > 0 {
+        // Inspect a non-deterministically chosen byte in the copy.
         let byte = kani::any_where(|sz: &usize| *sz < size_of::<T>());
+        // Instead of checking each of the `count`-many copies, non-deterministically pick one of
+        // them and check it. Using quantifiers would not add value as we can rely on the solver to
+        // pick an uninitialized element if such an element exists.
         let elem = kani::any_where(|val: &usize| *val < count);
         let src_data = src as *const u8;
         let dst_data = unsafe { dst.add(elem) } as *const u8;
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index 5e1152835056d..31888b09ff839 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -2242,9 +2242,8 @@ pub unsafe fn write_volatile<T>(dst: *mut T, src: T) {
     }
 
     // Checking if the answer should indeed be usize::MAX when a % stride != 0
-    // requires computing gcd(a, stride), which is too expensive without
-    // quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html).
-    // This should be updated once quantifiers are available.
+    // requires computing gcd(a, stride), which could be done using cttz as the implementation
+    // does.
     if (a % stride != 0 && *result == usize::MAX) {
         return true;
     }
@@ -2275,12 +2274,8 @@ pub(crate) unsafe fn align_offset<T: Sized>(p: *const T, a: usize) -> usize {
     /// Implementation of this function shall not panic. Ever.
     #[safety::requires(m.is_power_of_two())]
     #[safety::requires(x < m)]
-    // TODO: add ensures contract to check that the answer is indeed correct
-    // This will require quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html)
-    // so that we can add a precondition that gcd(x, m) = 1 like so:
-    // ∀d, d > 0 ∧ x % d = 0 ∧ m % d = 0 → d = 1
-    // With this precondition, we can then write this postcondition to check the correctness of the answer:
-    // #[safety::ensures(|result| wrapping_mul(*result, x) % m == 1)]
+    #[safety::requires(x % 2 != 0)]
+    #[safety::ensures(|result| wrapping_mul(*result, x) % m == 1)]
     #[inline]
     const unsafe fn mod_inv(x: usize, m: usize) -> usize {
         /// Multiplicative modular inverse table modulo 2⁴ = 16.
diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index f932de4c05250..ac8829ee85a65 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -1434,10 +1434,9 @@ impl<T: PointeeSized> NonNull<T> {
         if (align % stride == 0) && (self.pointer.addr() % stride != 0) {
             return *result == usize::MAX;
         }
-        // Checking if the answer should indeed be usize::MAX when align % stride != 0
-        // requires computing gcd(a, stride), which is too expensive without
-        // quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html).
-        // This should be updated once quantifiers are available.
+        // Checking if the answer should indeed be usize::MAX when a % stride != 0 requires
+        // computing gcd(align, stride), which could be done using cttz as the implementation of
+        // ptr::align_offset does.
         if (align % stride != 0 && *result == usize::MAX) {
             return true;
         }

From bf3aef2c3cb03c187c4040f3b7fe374b2854de8a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 12 Aug 2025 16:32:45 +0000
Subject: [PATCH 2/2] Don't use strong post-condition with Kani just yet

---
 library/core/src/ptr/mod.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index 31888b09ff839..e7841f67ab6df 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -2275,7 +2275,9 @@ pub(crate) unsafe fn align_offset<T: Sized>(p: *const T, a: usize) -> usize {
     #[safety::requires(m.is_power_of_two())]
     #[safety::requires(x < m)]
     #[safety::requires(x % 2 != 0)]
-    #[safety::ensures(|result| wrapping_mul(*result, x) % m == 1)]
+    // for Kani (v0.65.0), the below multiplication is too costly to prove
+    #[cfg_attr(not(kani),
+        safety::ensures(|result| wrapping_mul(*result, x) % m == 1))]
     #[inline]
     const unsafe fn mod_inv(x: usize, m: usize) -> usize {
         /// Multiplicative modular inverse table modulo 2⁴ = 16.