Remove spurious comments about the need for quantifiers

library/core/src/intrinsics/mod.rs

@@ -2820,14 +2820,16 @@ pub const fn ptr_metadata<P: ptr::Pointee<Metadata = M> + PointeeSized, M>(ptr:
 /// 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;

library/core/src/ptr/mod.rs

@@ -2206,9 +2206,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;
     }
@@ -2239,12 +2238,10 @@ 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)]
+    // 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.

library/core/src/ptr/non_null.rs

@@ -1441,10 +1441,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;
         }