From 501ee0a8e26c786841e23e4d3665afe5768e2fb0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 29 Aug 2024 14:06:12 -0400 Subject: [PATCH] add TODO comment for mod_inv postcondition --- library/core/src/ptr/mod.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index eb64352709d55..930e3105e901d 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -2472,6 +2472,12 @@ mod verify { // 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. ///