From 987d76cf28b9bfceb680cb21ba3074f20ae10504 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 3 Aug 2026 16:37:38 +0000
Subject: [PATCH] Fix mod_inv precondition: any x is invertible modulo 1

The `x % 2 != 0` precondition added to `mod_inv` in commit
6be9ca4b3f1e3557d34bbaa8e4c8bb0d7bc7b6c2 ("Remove spurious comments
about the need for quantifiers (#457)") is violated by `mod_inv`'s only
caller: `align_offset::<T>(p, 1)` with `size_of::<T>() > 1` takes the
GENERAL_CASE path (since `1 % stride != 0`) and computes
`s2 = (stride & 0) >> 0 = 0`, calling `mod_inv(0, 1)`. This happens for
example via `<[u16]>::align_to::<u8>()`, so any harness reaching
`align_to` with a target alignment of 1 fails the asserted precondition
when Kani runs without --no-assert-contracts (the violation is
currently masked in CI, which passes that flag).

The call is mathematically sound: modulo `m == 1` every value is
trivially an inverse of every other (the unique residue is 0), and
`align_offset` masks the returned value with `a2 - 1 == 0`. It is the
precondition that is too strict, not the caller that is wrong: an
inverse of `x` modulo a power of two `m` exists iff
`gcd(x, m) == 1`, which for `m > 1` means odd `x`, but for `m == 1`
holds for all `x`. Weaken the precondition to `m == 1 || x % 2 != 0`
accordingly.

Also fix the (kani-disabled) postcondition for the same degenerate
case: modulo 1, `wrapping_mul(*result, x) % m` is 0, not 1, so compare
against `1 % m` instead of `1`.

Verified (Kani 152c6a8c + CBMC 6.10.0) that the four harnesses that
fail without --no-assert-contracts on this precondition
(slice::verify::align_to_from_u16::align_to_u8,
slice::verify::align_to_mut_from_char::align_to_mut_u8,
slice::verify::align_to_mut_from_u32::align_to_mut_u8,
ptr::verify::check_align_offset_u16) now pass with contracts asserted,
and that the eight ptr::verify::check_align_offset* proof harnesses
still pass in both configurations.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 library/core/src/ptr/mod.rs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index 52556a7019014..5b4fb281b68e1 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -2238,14 +2238,15 @@ pub(crate) unsafe fn align_offset<T: Sized>(p: *const T, a: usize) -> usize {
     ///
     /// * `m` is a power-of-two;
     /// * `x < m`; (if `x ≥ m`, pass in `x % m` instead)
+    /// * `x` is odd, unless `m == 1` (any `x` is an inverse modulo 1)
     ///
     /// Implementation of this function shall not panic. Ever.
     #[safety::requires(m.is_power_of_two())]
     #[safety::requires(x < m)]
-    #[safety::requires(x % 2 != 0)]
+    #[safety::requires(m == 1 || 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))]
+        safety::ensures(|result| wrapping_mul(*result, x) % m == 1 % m))]
     #[inline]
     const unsafe fn mod_inv(x: usize, m: usize) -> usize {
         /// Multiplicative modular inverse table modulo 2⁴ = 16.