Use bounded exponent for NonZeroI128/U128 saturating_pow harnesses

The 128-bit saturating_pow harnesses with unbounded u32 exponents hit
CBMC's 10-minute timeout because 128-bit bitvector multiplication is
extremely expensive. Add a dedicated macro that constrains exp <= 10
with unwind(5), sufficient to cover both the non-saturating and
saturating code paths while keeping verification tractable.

Author: jrey8343

library/core/src/num/nonzero.rs

@@ -3541,15 +3541,34 @@ mod verify {
     nonzero_check_saturating_pow!(core::num::NonZeroI16, nonzero_check_saturating_pow_i16);
     nonzero_check_saturating_pow!(core::num::NonZeroI32, nonzero_check_saturating_pow_i32);
     nonzero_check_saturating_pow!(core::num::NonZeroI64, nonzero_check_saturating_pow_i64);
-    nonzero_check_saturating_pow!(core::num::NonZeroI128, nonzero_check_saturating_pow_i128);
     nonzero_check_saturating_pow!(core::num::NonZeroIsize, nonzero_check_saturating_pow_isize);
     nonzero_check_saturating_pow!(core::num::NonZeroU8, nonzero_check_saturating_pow_u8);
     nonzero_check_saturating_pow!(core::num::NonZeroU16, nonzero_check_saturating_pow_u16);
     nonzero_check_saturating_pow!(core::num::NonZeroU32, nonzero_check_saturating_pow_u32);
     nonzero_check_saturating_pow!(core::num::NonZeroU64, nonzero_check_saturating_pow_u64);
-    nonzero_check_saturating_pow!(core::num::NonZeroU128, nonzero_check_saturating_pow_u128);
     nonzero_check_saturating_pow!(core::num::NonZeroUsize, nonzero_check_saturating_pow_usize);
 
+    // 128-bit types use a bounded exponent to avoid CBMC timeout: saturating_pow
+    // uses binary exponentiation (O(log2(exp)) 128-bit multiplications), which is
+    // extremely expensive for CBMC's bitvector encoding. Bounding exp <= 10 is
+    // sufficient to exercise both the non-saturating and saturating code paths
+    // while keeping verification tractable (ceil(log2(10)) ≈ 4 loop iterations).
+    macro_rules! nonzero_check_saturating_pow_128 {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            #[kani::unwind(5)]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let exp: u32 = kani::any_where(|&e| e <= 10);
+                let result = x.saturating_pow(exp);
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_saturating_pow_128!(core::num::NonZeroI128, nonzero_check_saturating_pow_i128);
+    nonzero_check_saturating_pow_128!(core::num::NonZeroU128, nonzero_check_saturating_pow_u128);
+
     // --- Unsigned-only operations ---
 
     macro_rules! nonzero_check_checked_next_power_of_two {