Use autoharness for ptr::align_offset::mod_inv

This also solves the problem that we cannot write a harness for a nested
function, and hence previously had to copy it.

Author: tautschnig

.github/workflows/kani.yml

@@ -79,6 +79,7 @@ jobs:
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern ptr::align_offset::mod_inv \
             --include-pattern time::Duration::from_micros \
             --include-pattern time::Duration::from_millis \
             --include-pattern time::Duration::from_nanos \

library/core/src/ptr/mod.rs

@@ -1901,6 +1901,14 @@ pub(crate) unsafe fn align_offset<T: Sized>(p: *const T, a: usize) -> usize {
     /// * `x < m`; (if `x ≥ m`, pass in `x % m` instead)
     ///
     /// 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)]
     #[inline]
     const unsafe fn mod_inv(x: usize, m: usize) -> usize {
         /// Multiplicative modular inverse table modulo 2⁴ = 16.
@@ -2509,67 +2517,4 @@ mod verify {
         let p = kani::any::<usize>() as *const [char; 5];
         check_align_offset(p);
     }
-
-    // This function lives inside align_offset, so it is not publicly accessible (hence this copy).
-    #[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)]
-    const unsafe fn mod_inv_copy(x: usize, m: usize) -> usize {
-        /// Multiplicative modular inverse table modulo 2⁴ = 16.
-        ///
-        /// Note, that this table does not contain values where inverse does not exist (i.e., for
-        /// `0⁻¹ mod 16`, `2⁻¹ mod 16`, etc.)
-        const INV_TABLE_MOD_16: [u8; 8] = [1, 11, 13, 7, 9, 3, 5, 15];
-        /// Modulo for which the `INV_TABLE_MOD_16` is intended.
-        const INV_TABLE_MOD: usize = 16;
-
-        // SAFETY: `m` is required to be a power-of-two, hence non-zero.
-        let m_minus_one = unsafe { unchecked_sub(m, 1) };
-        let mut inverse = INV_TABLE_MOD_16[(x & (INV_TABLE_MOD - 1)) >> 1] as usize;
-        let mut mod_gate = INV_TABLE_MOD;
-        // We iterate "up" using the following formula:
-        //
-        // $$ xy ≡ 1 (mod 2ⁿ) → xy (2 - xy) ≡ 1 (mod 2²ⁿ) $$
-        //
-        // This application needs to be applied at least until `2²ⁿ ≥ m`, at which point we can
-        // finally reduce the computation to our desired `m` by taking `inverse mod m`.
-        //
-        // This computation is `O(log log m)`, which is to say, that on 64-bit machines this loop
-        // will always finish in at most 4 iterations.
-        loop {
-            // y = y * (2 - xy) mod n
-            //
-            // Note, that we use wrapping operations here intentionally – the original formula
-            // uses e.g., subtraction `mod n`. It is entirely fine to do them `mod
-            // usize::MAX` instead, because we take the result `mod n` at the end
-            // anyway.
-            if mod_gate >= m {
-                break;
-            }
-            inverse = wrapping_mul(inverse, wrapping_sub(2usize, wrapping_mul(x, inverse)));
-            let (new_gate, overflow) = mul_with_overflow(mod_gate, mod_gate);
-            if overflow {
-                break;
-            }
-            mod_gate = new_gate;
-        }
-        inverse & m_minus_one
-    }
-
-    // The specification for mod_inv states that it cannot ever panic.
-    // Verify that is the case, given that the function's safety preconditions are met.
-
-    // TODO: Once https://github.com/model-checking/kani/issues/3467 is fixed,
-    // move this harness inside `align_offset` and delete `mod_inv_copy`
-    #[kani::proof_for_contract(mod_inv_copy)]
-    fn check_mod_inv() {
-        let x = kani::any::<usize>();
-        let m = kani::any::<usize>();
-        unsafe { mod_inv_copy(x, m) };
-    }
 }