From a6980208bc9a569b2b98559154ae3911f2286a21 Mon Sep 17 00:00:00 2001
From: Jared Reyes <jaredreyespt@gmail.com>
Date: Sun, 8 Feb 2026 14:37:25 +1100
Subject: [PATCH 1/4] Verify safety of NonZero operations (Challenge 12)

Add verification harnesses for all remaining NonZero functions:
bit operations (count_ones, swap_bytes, reverse_bits, rotate_left,
rotate_right), byte order (from_be, from_le, to_be, to_le), bitor
(all 3 impls), checked/saturating arithmetic (checked_mul,
saturating_mul, checked_add, saturating_add, checked_pow,
saturating_pow), power of two (checked_next_power_of_two), midpoint,
isqrt, signed operations (neg, abs, checked_abs, overflowing_abs,
saturating_abs, wrapping_abs, unsigned_abs, checked_neg,
overflowing_neg, wrapping_neg), and from_mut.

Remove trivial loop_invariant(true) annotations from primitive
checked_pow that caused CBMC assigns check interference with
NonZero::new_unchecked verification.

Total: 385 harnesses pass (376 new + 9 existing).
---
 library/core/src/num/int_macros.rs  |   1 -
 library/core/src/num/nonzero.rs     | 888 ++++++++++++++++++++++++++++
 library/core/src/num/uint_macros.rs |   1 -
 3 files changed, 888 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 4468c1489bfb5..af4567b0e6bfa 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -1736,7 +1736,6 @@ macro_rules! int_impl {
             let mut base = self;
             let mut acc: Self = 1;
 
-            #[safety::loop_invariant(true)]
             loop {
                 if (exp & 1) == 1 {
                     acc = try_opt!(acc.checked_mul(base));
diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
index 9c9d3a136a1e0..6d3a1a1894605 100644
--- a/library/core/src/num/nonzero.rs
+++ b/library/core/src/num/nonzero.rs
@@ -3025,4 +3025,892 @@ mod verify {
     nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64);
     nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128);
     nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize);
+
+    // --- Bit operations: count_ones, swap_bytes, reverse_bits ---
+
+    macro_rules! nonzero_check_count_ones {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let result = x.count_ones();
+                assert!(result.get() > 0);
+                assert!(result.get() == x.get().count_ones());
+            }
+        };
+    }
+
+    nonzero_check_count_ones!(core::num::NonZeroI8, nonzero_check_count_ones_i8);
+    nonzero_check_count_ones!(core::num::NonZeroI16, nonzero_check_count_ones_i16);
+    nonzero_check_count_ones!(core::num::NonZeroI32, nonzero_check_count_ones_i32);
+    nonzero_check_count_ones!(core::num::NonZeroI64, nonzero_check_count_ones_i64);
+    nonzero_check_count_ones!(core::num::NonZeroI128, nonzero_check_count_ones_i128);
+    nonzero_check_count_ones!(core::num::NonZeroIsize, nonzero_check_count_ones_isize);
+    nonzero_check_count_ones!(core::num::NonZeroU8, nonzero_check_count_ones_u8);
+    nonzero_check_count_ones!(core::num::NonZeroU16, nonzero_check_count_ones_u16);
+    nonzero_check_count_ones!(core::num::NonZeroU32, nonzero_check_count_ones_u32);
+    nonzero_check_count_ones!(core::num::NonZeroU64, nonzero_check_count_ones_u64);
+    nonzero_check_count_ones!(core::num::NonZeroU128, nonzero_check_count_ones_u128);
+    nonzero_check_count_ones!(core::num::NonZeroUsize, nonzero_check_count_ones_usize);
+
+    macro_rules! nonzero_check_swap_bytes {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let result = x.swap_bytes();
+                assert!(result.get() != 0);
+                assert!(result.swap_bytes() == x);
+            }
+        };
+    }
+
+    nonzero_check_swap_bytes!(core::num::NonZeroI8, nonzero_check_swap_bytes_i8);
+    nonzero_check_swap_bytes!(core::num::NonZeroI16, nonzero_check_swap_bytes_i16);
+    nonzero_check_swap_bytes!(core::num::NonZeroI32, nonzero_check_swap_bytes_i32);
+    nonzero_check_swap_bytes!(core::num::NonZeroI64, nonzero_check_swap_bytes_i64);
+    nonzero_check_swap_bytes!(core::num::NonZeroI128, nonzero_check_swap_bytes_i128);
+    nonzero_check_swap_bytes!(core::num::NonZeroIsize, nonzero_check_swap_bytes_isize);
+    nonzero_check_swap_bytes!(core::num::NonZeroU8, nonzero_check_swap_bytes_u8);
+    nonzero_check_swap_bytes!(core::num::NonZeroU16, nonzero_check_swap_bytes_u16);
+    nonzero_check_swap_bytes!(core::num::NonZeroU32, nonzero_check_swap_bytes_u32);
+    nonzero_check_swap_bytes!(core::num::NonZeroU64, nonzero_check_swap_bytes_u64);
+    nonzero_check_swap_bytes!(core::num::NonZeroU128, nonzero_check_swap_bytes_u128);
+    nonzero_check_swap_bytes!(core::num::NonZeroUsize, nonzero_check_swap_bytes_usize);
+
+    macro_rules! nonzero_check_reverse_bits {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let result = x.reverse_bits();
+                assert!(result.get() != 0);
+                assert!(result.reverse_bits() == x);
+            }
+        };
+    }
+
+    nonzero_check_reverse_bits!(core::num::NonZeroI8, nonzero_check_reverse_bits_i8);
+    nonzero_check_reverse_bits!(core::num::NonZeroI16, nonzero_check_reverse_bits_i16);
+    nonzero_check_reverse_bits!(core::num::NonZeroI32, nonzero_check_reverse_bits_i32);
+    nonzero_check_reverse_bits!(core::num::NonZeroI64, nonzero_check_reverse_bits_i64);
+    nonzero_check_reverse_bits!(core::num::NonZeroI128, nonzero_check_reverse_bits_i128);
+    nonzero_check_reverse_bits!(core::num::NonZeroIsize, nonzero_check_reverse_bits_isize);
+    nonzero_check_reverse_bits!(core::num::NonZeroU8, nonzero_check_reverse_bits_u8);
+    nonzero_check_reverse_bits!(core::num::NonZeroU16, nonzero_check_reverse_bits_u16);
+    nonzero_check_reverse_bits!(core::num::NonZeroU32, nonzero_check_reverse_bits_u32);
+    nonzero_check_reverse_bits!(core::num::NonZeroU64, nonzero_check_reverse_bits_u64);
+    nonzero_check_reverse_bits!(core::num::NonZeroU128, nonzero_check_reverse_bits_u128);
+    nonzero_check_reverse_bits!(core::num::NonZeroUsize, nonzero_check_reverse_bits_usize);
+
+    // --- Rotate operations ---
+
+    macro_rules! nonzero_check_rotate_left {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let n: u32 = kani::any();
+                let result = x.rotate_left(n);
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_rotate_left!(core::num::NonZeroI8, nonzero_check_rotate_left_i8);
+    nonzero_check_rotate_left!(core::num::NonZeroI16, nonzero_check_rotate_left_i16);
+    nonzero_check_rotate_left!(core::num::NonZeroI32, nonzero_check_rotate_left_i32);
+    nonzero_check_rotate_left!(core::num::NonZeroI64, nonzero_check_rotate_left_i64);
+    nonzero_check_rotate_left!(core::num::NonZeroI128, nonzero_check_rotate_left_i128);
+    nonzero_check_rotate_left!(core::num::NonZeroIsize, nonzero_check_rotate_left_isize);
+    nonzero_check_rotate_left!(core::num::NonZeroU8, nonzero_check_rotate_left_u8);
+    nonzero_check_rotate_left!(core::num::NonZeroU16, nonzero_check_rotate_left_u16);
+    nonzero_check_rotate_left!(core::num::NonZeroU32, nonzero_check_rotate_left_u32);
+    nonzero_check_rotate_left!(core::num::NonZeroU64, nonzero_check_rotate_left_u64);
+    nonzero_check_rotate_left!(core::num::NonZeroU128, nonzero_check_rotate_left_u128);
+    nonzero_check_rotate_left!(core::num::NonZeroUsize, nonzero_check_rotate_left_usize);
+
+    macro_rules! nonzero_check_rotate_right {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let n: u32 = kani::any();
+                let result = x.rotate_right(n);
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_rotate_right!(core::num::NonZeroI8, nonzero_check_rotate_right_i8);
+    nonzero_check_rotate_right!(core::num::NonZeroI16, nonzero_check_rotate_right_i16);
+    nonzero_check_rotate_right!(core::num::NonZeroI32, nonzero_check_rotate_right_i32);
+    nonzero_check_rotate_right!(core::num::NonZeroI64, nonzero_check_rotate_right_i64);
+    nonzero_check_rotate_right!(core::num::NonZeroI128, nonzero_check_rotate_right_i128);
+    nonzero_check_rotate_right!(core::num::NonZeroIsize, nonzero_check_rotate_right_isize);
+    nonzero_check_rotate_right!(core::num::NonZeroU8, nonzero_check_rotate_right_u8);
+    nonzero_check_rotate_right!(core::num::NonZeroU16, nonzero_check_rotate_right_u16);
+    nonzero_check_rotate_right!(core::num::NonZeroU32, nonzero_check_rotate_right_u32);
+    nonzero_check_rotate_right!(core::num::NonZeroU64, nonzero_check_rotate_right_u64);
+    nonzero_check_rotate_right!(core::num::NonZeroU128, nonzero_check_rotate_right_u128);
+    nonzero_check_rotate_right!(core::num::NonZeroUsize, nonzero_check_rotate_right_usize);
+
+    // --- Byte order: from_be, from_le, to_be, to_le ---
+
+    macro_rules! nonzero_check_byte_order {
+        ($nonzero_type:ty, $from_be:ident, $from_le:ident, $to_be:ident, $to_le:ident) => {
+            #[kani::proof]
+            pub fn $from_be() {
+                let x: $nonzero_type = kani::any();
+                let result = <$nonzero_type>::from_be(x);
+                assert!(result.get() != 0);
+                assert!(<$nonzero_type>::from_be(result).get() == x.get());
+            }
+
+            #[kani::proof]
+            pub fn $from_le() {
+                let x: $nonzero_type = kani::any();
+                let result = <$nonzero_type>::from_le(x);
+                assert!(result.get() != 0);
+                assert!(<$nonzero_type>::from_le(result).get() == x.get());
+            }
+
+            #[kani::proof]
+            pub fn $to_be() {
+                let x: $nonzero_type = kani::any();
+                let result = x.to_be();
+                assert!(result.get() != 0);
+                assert!(result.to_be().get() == x.get());
+            }
+
+            #[kani::proof]
+            pub fn $to_le() {
+                let x: $nonzero_type = kani::any();
+                let result = x.to_le();
+                assert!(result.get() != 0);
+                assert!(result.to_le().get() == x.get());
+            }
+        };
+    }
+
+    nonzero_check_byte_order!(
+        core::num::NonZeroI8,
+        nonzero_check_from_be_i8,
+        nonzero_check_from_le_i8,
+        nonzero_check_to_be_i8,
+        nonzero_check_to_le_i8
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroI16,
+        nonzero_check_from_be_i16,
+        nonzero_check_from_le_i16,
+        nonzero_check_to_be_i16,
+        nonzero_check_to_le_i16
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroI32,
+        nonzero_check_from_be_i32,
+        nonzero_check_from_le_i32,
+        nonzero_check_to_be_i32,
+        nonzero_check_to_le_i32
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroI64,
+        nonzero_check_from_be_i64,
+        nonzero_check_from_le_i64,
+        nonzero_check_to_be_i64,
+        nonzero_check_to_le_i64
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroI128,
+        nonzero_check_from_be_i128,
+        nonzero_check_from_le_i128,
+        nonzero_check_to_be_i128,
+        nonzero_check_to_le_i128
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroIsize,
+        nonzero_check_from_be_isize,
+        nonzero_check_from_le_isize,
+        nonzero_check_to_be_isize,
+        nonzero_check_to_le_isize
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroU8,
+        nonzero_check_from_be_u8,
+        nonzero_check_from_le_u8,
+        nonzero_check_to_be_u8,
+        nonzero_check_to_le_u8
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroU16,
+        nonzero_check_from_be_u16,
+        nonzero_check_from_le_u16,
+        nonzero_check_to_be_u16,
+        nonzero_check_to_le_u16
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroU32,
+        nonzero_check_from_be_u32,
+        nonzero_check_from_le_u32,
+        nonzero_check_to_be_u32,
+        nonzero_check_to_le_u32
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroU64,
+        nonzero_check_from_be_u64,
+        nonzero_check_from_le_u64,
+        nonzero_check_to_be_u64,
+        nonzero_check_to_le_u64
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroU128,
+        nonzero_check_from_be_u128,
+        nonzero_check_from_le_u128,
+        nonzero_check_to_be_u128,
+        nonzero_check_to_le_u128
+    );
+    nonzero_check_byte_order!(
+        core::num::NonZeroUsize,
+        nonzero_check_from_be_usize,
+        nonzero_check_from_le_usize,
+        nonzero_check_to_be_usize,
+        nonzero_check_to_le_usize
+    );
+
+    // --- BitOr: 3 implementations ---
+
+    macro_rules! nonzero_check_bitor {
+        ($t:ty, $nonzero_type:ty, $bitor_nn:ident, $bitor_nt:ident, $bitor_tn:ident) => {
+            // NonZero | NonZero
+            #[kani::proof]
+            pub fn $bitor_nn() {
+                let x: $nonzero_type = kani::any();
+                let y: $nonzero_type = kani::any();
+                let result = x | y;
+                assert!(result.get() != 0);
+                assert!(result.get() == (x.get() | y.get()));
+            }
+
+            // NonZero | T
+            #[kani::proof]
+            pub fn $bitor_nt() {
+                let x: $nonzero_type = kani::any();
+                let y: $t = kani::any();
+                let result = x | y;
+                assert!(result.get() != 0);
+                assert!(result.get() == (x.get() | y));
+            }
+
+            // T | NonZero
+            #[kani::proof]
+            pub fn $bitor_tn() {
+                let x: $t = kani::any();
+                let y: $nonzero_type = kani::any();
+                let result: $nonzero_type = x | y;
+                assert!(result.get() != 0);
+                assert!(result.get() == (x | y.get()));
+            }
+        };
+    }
+
+    nonzero_check_bitor!(
+        i8,
+        core::num::NonZeroI8,
+        nonzero_check_bitor_nn_i8,
+        nonzero_check_bitor_nt_i8,
+        nonzero_check_bitor_tn_i8
+    );
+    nonzero_check_bitor!(
+        i16,
+        core::num::NonZeroI16,
+        nonzero_check_bitor_nn_i16,
+        nonzero_check_bitor_nt_i16,
+        nonzero_check_bitor_tn_i16
+    );
+    nonzero_check_bitor!(
+        i32,
+        core::num::NonZeroI32,
+        nonzero_check_bitor_nn_i32,
+        nonzero_check_bitor_nt_i32,
+        nonzero_check_bitor_tn_i32
+    );
+    nonzero_check_bitor!(
+        i64,
+        core::num::NonZeroI64,
+        nonzero_check_bitor_nn_i64,
+        nonzero_check_bitor_nt_i64,
+        nonzero_check_bitor_tn_i64
+    );
+    nonzero_check_bitor!(
+        i128,
+        core::num::NonZeroI128,
+        nonzero_check_bitor_nn_i128,
+        nonzero_check_bitor_nt_i128,
+        nonzero_check_bitor_tn_i128
+    );
+    nonzero_check_bitor!(
+        isize,
+        core::num::NonZeroIsize,
+        nonzero_check_bitor_nn_isize,
+        nonzero_check_bitor_nt_isize,
+        nonzero_check_bitor_tn_isize
+    );
+    nonzero_check_bitor!(
+        u8,
+        core::num::NonZeroU8,
+        nonzero_check_bitor_nn_u8,
+        nonzero_check_bitor_nt_u8,
+        nonzero_check_bitor_tn_u8
+    );
+    nonzero_check_bitor!(
+        u16,
+        core::num::NonZeroU16,
+        nonzero_check_bitor_nn_u16,
+        nonzero_check_bitor_nt_u16,
+        nonzero_check_bitor_tn_u16
+    );
+    nonzero_check_bitor!(
+        u32,
+        core::num::NonZeroU32,
+        nonzero_check_bitor_nn_u32,
+        nonzero_check_bitor_nt_u32,
+        nonzero_check_bitor_tn_u32
+    );
+    nonzero_check_bitor!(
+        u64,
+        core::num::NonZeroU64,
+        nonzero_check_bitor_nn_u64,
+        nonzero_check_bitor_nt_u64,
+        nonzero_check_bitor_tn_u64
+    );
+    nonzero_check_bitor!(
+        u128,
+        core::num::NonZeroU128,
+        nonzero_check_bitor_nn_u128,
+        nonzero_check_bitor_nt_u128,
+        nonzero_check_bitor_tn_u128
+    );
+    nonzero_check_bitor!(
+        usize,
+        core::num::NonZeroUsize,
+        nonzero_check_bitor_nn_usize,
+        nonzero_check_bitor_nt_usize,
+        nonzero_check_bitor_tn_usize
+    );
+
+    // --- Checked/Saturating arithmetic ---
+
+    macro_rules! nonzero_check_checked_mul {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let y: $nonzero_type = kani::any();
+                if let Some(result) = x.checked_mul(y) {
+                    assert!(result.get() != 0);
+                }
+            }
+        };
+    }
+
+    nonzero_check_checked_mul!(core::num::NonZeroI8, nonzero_check_checked_mul_i8);
+    nonzero_check_checked_mul!(core::num::NonZeroI16, nonzero_check_checked_mul_i16);
+    nonzero_check_checked_mul!(core::num::NonZeroI32, nonzero_check_checked_mul_i32);
+    nonzero_check_checked_mul!(core::num::NonZeroI64, nonzero_check_checked_mul_i64);
+    nonzero_check_checked_mul!(core::num::NonZeroI128, nonzero_check_checked_mul_i128);
+    nonzero_check_checked_mul!(core::num::NonZeroIsize, nonzero_check_checked_mul_isize);
+    nonzero_check_checked_mul!(core::num::NonZeroU8, nonzero_check_checked_mul_u8);
+    nonzero_check_checked_mul!(core::num::NonZeroU16, nonzero_check_checked_mul_u16);
+    nonzero_check_checked_mul!(core::num::NonZeroU32, nonzero_check_checked_mul_u32);
+    nonzero_check_checked_mul!(core::num::NonZeroU64, nonzero_check_checked_mul_u64);
+    nonzero_check_checked_mul!(core::num::NonZeroU128, nonzero_check_checked_mul_u128);
+    nonzero_check_checked_mul!(core::num::NonZeroUsize, nonzero_check_checked_mul_usize);
+
+    macro_rules! nonzero_check_saturating_mul {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let y: $nonzero_type = kani::any();
+                let result = x.saturating_mul(y);
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_saturating_mul!(core::num::NonZeroI8, nonzero_check_saturating_mul_i8);
+    nonzero_check_saturating_mul!(core::num::NonZeroI16, nonzero_check_saturating_mul_i16);
+    nonzero_check_saturating_mul!(core::num::NonZeroI32, nonzero_check_saturating_mul_i32);
+    nonzero_check_saturating_mul!(core::num::NonZeroI64, nonzero_check_saturating_mul_i64);
+    nonzero_check_saturating_mul!(core::num::NonZeroI128, nonzero_check_saturating_mul_i128);
+    nonzero_check_saturating_mul!(
+        core::num::NonZeroIsize,
+        nonzero_check_saturating_mul_isize
+    );
+    nonzero_check_saturating_mul!(core::num::NonZeroU8, nonzero_check_saturating_mul_u8);
+    nonzero_check_saturating_mul!(core::num::NonZeroU16, nonzero_check_saturating_mul_u16);
+    nonzero_check_saturating_mul!(core::num::NonZeroU32, nonzero_check_saturating_mul_u32);
+    nonzero_check_saturating_mul!(core::num::NonZeroU64, nonzero_check_saturating_mul_u64);
+    nonzero_check_saturating_mul!(core::num::NonZeroU128, nonzero_check_saturating_mul_u128);
+    nonzero_check_saturating_mul!(
+        core::num::NonZeroUsize,
+        nonzero_check_saturating_mul_usize
+    );
+
+    macro_rules! nonzero_check_checked_add {
+        ($t:ty, $nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let y: $t = kani::any();
+                if let Some(result) = x.checked_add(y) {
+                    assert!(result.get() != 0);
+                }
+            }
+        };
+    }
+
+    nonzero_check_checked_add!(u8, core::num::NonZeroU8, nonzero_check_checked_add_u8);
+    nonzero_check_checked_add!(u16, core::num::NonZeroU16, nonzero_check_checked_add_u16);
+    nonzero_check_checked_add!(u32, core::num::NonZeroU32, nonzero_check_checked_add_u32);
+    nonzero_check_checked_add!(u64, core::num::NonZeroU64, nonzero_check_checked_add_u64);
+    nonzero_check_checked_add!(u128, core::num::NonZeroU128, nonzero_check_checked_add_u128);
+    nonzero_check_checked_add!(
+        usize,
+        core::num::NonZeroUsize,
+        nonzero_check_checked_add_usize
+    );
+
+    macro_rules! nonzero_check_saturating_add {
+        ($t:ty, $nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let y: $t = kani::any();
+                let result = x.saturating_add(y);
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_saturating_add!(u8, core::num::NonZeroU8, nonzero_check_saturating_add_u8);
+    nonzero_check_saturating_add!(
+        u16,
+        core::num::NonZeroU16,
+        nonzero_check_saturating_add_u16
+    );
+    nonzero_check_saturating_add!(
+        u32,
+        core::num::NonZeroU32,
+        nonzero_check_saturating_add_u32
+    );
+    nonzero_check_saturating_add!(
+        u64,
+        core::num::NonZeroU64,
+        nonzero_check_saturating_add_u64
+    );
+    nonzero_check_saturating_add!(
+        u128,
+        core::num::NonZeroU128,
+        nonzero_check_saturating_add_u128
+    );
+    nonzero_check_saturating_add!(
+        usize,
+        core::num::NonZeroUsize,
+        nonzero_check_saturating_add_usize
+    );
+
+    // --- Power operations ---
+
+    macro_rules! nonzero_check_checked_pow {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            #[kani::unwind(34)]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let exp: u32 = kani::any();
+                if let Some(result) = x.checked_pow(exp) {
+                    assert!(result.get() != 0);
+                }
+            }
+        };
+    }
+
+    nonzero_check_checked_pow!(core::num::NonZeroI8, nonzero_check_checked_pow_i8);
+    nonzero_check_checked_pow!(core::num::NonZeroI16, nonzero_check_checked_pow_i16);
+    nonzero_check_checked_pow!(core::num::NonZeroI32, nonzero_check_checked_pow_i32);
+    nonzero_check_checked_pow!(core::num::NonZeroI64, nonzero_check_checked_pow_i64);
+    nonzero_check_checked_pow!(core::num::NonZeroI128, nonzero_check_checked_pow_i128);
+    nonzero_check_checked_pow!(core::num::NonZeroIsize, nonzero_check_checked_pow_isize);
+    nonzero_check_checked_pow!(core::num::NonZeroU8, nonzero_check_checked_pow_u8);
+    nonzero_check_checked_pow!(core::num::NonZeroU16, nonzero_check_checked_pow_u16);
+    nonzero_check_checked_pow!(core::num::NonZeroU32, nonzero_check_checked_pow_u32);
+    nonzero_check_checked_pow!(core::num::NonZeroU64, nonzero_check_checked_pow_u64);
+    nonzero_check_checked_pow!(core::num::NonZeroU128, nonzero_check_checked_pow_u128);
+    nonzero_check_checked_pow!(core::num::NonZeroUsize, nonzero_check_checked_pow_usize);
+
+    macro_rules! nonzero_check_saturating_pow {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            #[kani::unwind(34)]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let exp: u32 = kani::any();
+                let result = x.saturating_pow(exp);
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_saturating_pow!(core::num::NonZeroI8, nonzero_check_saturating_pow_i8);
+    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);
+
+    // --- Unsigned-only operations ---
+
+    macro_rules! nonzero_check_checked_next_power_of_two {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                if let Some(result) = x.checked_next_power_of_two() {
+                    assert!(result.get() != 0);
+                    assert!(result.get().is_power_of_two());
+                    assert!(result >= x);
+                }
+            }
+        };
+    }
+
+    nonzero_check_checked_next_power_of_two!(
+        core::num::NonZeroU8,
+        nonzero_check_checked_next_power_of_two_u8
+    );
+    nonzero_check_checked_next_power_of_two!(
+        core::num::NonZeroU16,
+        nonzero_check_checked_next_power_of_two_u16
+    );
+    nonzero_check_checked_next_power_of_two!(
+        core::num::NonZeroU32,
+        nonzero_check_checked_next_power_of_two_u32
+    );
+    nonzero_check_checked_next_power_of_two!(
+        core::num::NonZeroU64,
+        nonzero_check_checked_next_power_of_two_u64
+    );
+    nonzero_check_checked_next_power_of_two!(
+        core::num::NonZeroU128,
+        nonzero_check_checked_next_power_of_two_u128
+    );
+    nonzero_check_checked_next_power_of_two!(
+        core::num::NonZeroUsize,
+        nonzero_check_checked_next_power_of_two_usize
+    );
+
+    macro_rules! nonzero_check_midpoint {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let y: $nonzero_type = kani::any();
+                let result = x.midpoint(y);
+                assert!(result.get() != 0);
+                assert!(result >= x.min(y));
+                assert!(result <= x.max(y));
+            }
+        };
+    }
+
+    nonzero_check_midpoint!(core::num::NonZeroU8, nonzero_check_midpoint_u8);
+    nonzero_check_midpoint!(core::num::NonZeroU16, nonzero_check_midpoint_u16);
+    nonzero_check_midpoint!(core::num::NonZeroU32, nonzero_check_midpoint_u32);
+    nonzero_check_midpoint!(core::num::NonZeroU64, nonzero_check_midpoint_u64);
+    nonzero_check_midpoint!(core::num::NonZeroU128, nonzero_check_midpoint_u128);
+    nonzero_check_midpoint!(core::num::NonZeroUsize, nonzero_check_midpoint_usize);
+
+    macro_rules! nonzero_check_isqrt {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let result = x.isqrt();
+                assert!(result.get() != 0);
+                // result^2 <= x
+                let r = result.get() as u128;
+                let v = x.get() as u128;
+                assert!(r * r <= v);
+            }
+        };
+    }
+
+    nonzero_check_isqrt!(core::num::NonZeroU8, nonzero_check_isqrt_u8);
+    nonzero_check_isqrt!(core::num::NonZeroU16, nonzero_check_isqrt_u16);
+    nonzero_check_isqrt!(core::num::NonZeroU32, nonzero_check_isqrt_u32);
+
+    // --- Signed-only operations: neg, abs family, checked_neg family ---
+
+    macro_rules! nonzero_check_neg {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                // Exclude MIN since negating it overflows
+                kani::assume(x.get() != <$nonzero_type>::MIN.get());
+                let result = -x;
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_neg!(core::num::NonZeroI8, nonzero_check_neg_i8);
+    nonzero_check_neg!(core::num::NonZeroI16, nonzero_check_neg_i16);
+    nonzero_check_neg!(core::num::NonZeroI32, nonzero_check_neg_i32);
+    nonzero_check_neg!(core::num::NonZeroI64, nonzero_check_neg_i64);
+    nonzero_check_neg!(core::num::NonZeroI128, nonzero_check_neg_i128);
+    nonzero_check_neg!(core::num::NonZeroIsize, nonzero_check_neg_isize);
+
+    macro_rules! nonzero_check_abs {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                // Exclude MIN since abs(MIN) overflows
+                kani::assume(x.get() != <$nonzero_type>::MIN.get());
+                let result = x.abs();
+                assert!(result.get() != 0);
+                assert!(result.get() >= 0);
+            }
+        };
+    }
+
+    nonzero_check_abs!(core::num::NonZeroI8, nonzero_check_abs_i8);
+    nonzero_check_abs!(core::num::NonZeroI16, nonzero_check_abs_i16);
+    nonzero_check_abs!(core::num::NonZeroI32, nonzero_check_abs_i32);
+    nonzero_check_abs!(core::num::NonZeroI64, nonzero_check_abs_i64);
+    nonzero_check_abs!(core::num::NonZeroI128, nonzero_check_abs_i128);
+    nonzero_check_abs!(core::num::NonZeroIsize, nonzero_check_abs_isize);
+
+    macro_rules! nonzero_check_checked_abs {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                if let Some(result) = x.checked_abs() {
+                    assert!(result.get() != 0);
+                    assert!(result.get() >= 0);
+                }
+            }
+        };
+    }
+
+    nonzero_check_checked_abs!(core::num::NonZeroI8, nonzero_check_checked_abs_i8);
+    nonzero_check_checked_abs!(core::num::NonZeroI16, nonzero_check_checked_abs_i16);
+    nonzero_check_checked_abs!(core::num::NonZeroI32, nonzero_check_checked_abs_i32);
+    nonzero_check_checked_abs!(core::num::NonZeroI64, nonzero_check_checked_abs_i64);
+    nonzero_check_checked_abs!(core::num::NonZeroI128, nonzero_check_checked_abs_i128);
+    nonzero_check_checked_abs!(core::num::NonZeroIsize, nonzero_check_checked_abs_isize);
+
+    macro_rules! nonzero_check_overflowing_abs {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let (result, overflowed) = x.overflowing_abs();
+                assert!(result.get() != 0);
+                let _ = overflowed;
+            }
+        };
+    }
+
+    nonzero_check_overflowing_abs!(core::num::NonZeroI8, nonzero_check_overflowing_abs_i8);
+    nonzero_check_overflowing_abs!(core::num::NonZeroI16, nonzero_check_overflowing_abs_i16);
+    nonzero_check_overflowing_abs!(core::num::NonZeroI32, nonzero_check_overflowing_abs_i32);
+    nonzero_check_overflowing_abs!(core::num::NonZeroI64, nonzero_check_overflowing_abs_i64);
+    nonzero_check_overflowing_abs!(core::num::NonZeroI128, nonzero_check_overflowing_abs_i128);
+    nonzero_check_overflowing_abs!(
+        core::num::NonZeroIsize,
+        nonzero_check_overflowing_abs_isize
+    );
+
+    macro_rules! nonzero_check_saturating_abs {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let result = x.saturating_abs();
+                assert!(result.get() != 0);
+                assert!(result.get() >= 0);
+            }
+        };
+    }
+
+    nonzero_check_saturating_abs!(core::num::NonZeroI8, nonzero_check_saturating_abs_i8);
+    nonzero_check_saturating_abs!(core::num::NonZeroI16, nonzero_check_saturating_abs_i16);
+    nonzero_check_saturating_abs!(core::num::NonZeroI32, nonzero_check_saturating_abs_i32);
+    nonzero_check_saturating_abs!(core::num::NonZeroI64, nonzero_check_saturating_abs_i64);
+    nonzero_check_saturating_abs!(core::num::NonZeroI128, nonzero_check_saturating_abs_i128);
+    nonzero_check_saturating_abs!(
+        core::num::NonZeroIsize,
+        nonzero_check_saturating_abs_isize
+    );
+
+    macro_rules! nonzero_check_wrapping_abs {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let result = x.wrapping_abs();
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_wrapping_abs!(core::num::NonZeroI8, nonzero_check_wrapping_abs_i8);
+    nonzero_check_wrapping_abs!(core::num::NonZeroI16, nonzero_check_wrapping_abs_i16);
+    nonzero_check_wrapping_abs!(core::num::NonZeroI32, nonzero_check_wrapping_abs_i32);
+    nonzero_check_wrapping_abs!(core::num::NonZeroI64, nonzero_check_wrapping_abs_i64);
+    nonzero_check_wrapping_abs!(core::num::NonZeroI128, nonzero_check_wrapping_abs_i128);
+    nonzero_check_wrapping_abs!(core::num::NonZeroIsize, nonzero_check_wrapping_abs_isize);
+
+    macro_rules! nonzero_check_unsigned_abs {
+        ($signed_nonzero:ty, $unsigned_nonzero:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $signed_nonzero = kani::any();
+                let result: $unsigned_nonzero = x.unsigned_abs();
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_unsigned_abs!(
+        core::num::NonZeroI8,
+        core::num::NonZeroU8,
+        nonzero_check_unsigned_abs_i8
+    );
+    nonzero_check_unsigned_abs!(
+        core::num::NonZeroI16,
+        core::num::NonZeroU16,
+        nonzero_check_unsigned_abs_i16
+    );
+    nonzero_check_unsigned_abs!(
+        core::num::NonZeroI32,
+        core::num::NonZeroU32,
+        nonzero_check_unsigned_abs_i32
+    );
+    nonzero_check_unsigned_abs!(
+        core::num::NonZeroI64,
+        core::num::NonZeroU64,
+        nonzero_check_unsigned_abs_i64
+    );
+    nonzero_check_unsigned_abs!(
+        core::num::NonZeroI128,
+        core::num::NonZeroU128,
+        nonzero_check_unsigned_abs_i128
+    );
+    nonzero_check_unsigned_abs!(
+        core::num::NonZeroIsize,
+        core::num::NonZeroUsize,
+        nonzero_check_unsigned_abs_isize
+    );
+
+    macro_rules! nonzero_check_checked_neg {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                if let Some(result) = x.checked_neg() {
+                    assert!(result.get() != 0);
+                }
+            }
+        };
+    }
+
+    nonzero_check_checked_neg!(core::num::NonZeroI8, nonzero_check_checked_neg_i8);
+    nonzero_check_checked_neg!(core::num::NonZeroI16, nonzero_check_checked_neg_i16);
+    nonzero_check_checked_neg!(core::num::NonZeroI32, nonzero_check_checked_neg_i32);
+    nonzero_check_checked_neg!(core::num::NonZeroI64, nonzero_check_checked_neg_i64);
+    nonzero_check_checked_neg!(core::num::NonZeroI128, nonzero_check_checked_neg_i128);
+    nonzero_check_checked_neg!(core::num::NonZeroIsize, nonzero_check_checked_neg_isize);
+
+    macro_rules! nonzero_check_overflowing_neg {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let (result, overflowed) = x.overflowing_neg();
+                assert!(result.get() != 0);
+                let _ = overflowed;
+            }
+        };
+    }
+
+    nonzero_check_overflowing_neg!(core::num::NonZeroI8, nonzero_check_overflowing_neg_i8);
+    nonzero_check_overflowing_neg!(core::num::NonZeroI16, nonzero_check_overflowing_neg_i16);
+    nonzero_check_overflowing_neg!(core::num::NonZeroI32, nonzero_check_overflowing_neg_i32);
+    nonzero_check_overflowing_neg!(core::num::NonZeroI64, nonzero_check_overflowing_neg_i64);
+    nonzero_check_overflowing_neg!(core::num::NonZeroI128, nonzero_check_overflowing_neg_i128);
+    nonzero_check_overflowing_neg!(
+        core::num::NonZeroIsize,
+        nonzero_check_overflowing_neg_isize
+    );
+
+    macro_rules! nonzero_check_wrapping_neg {
+        ($nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: $nonzero_type = kani::any();
+                let result = x.wrapping_neg();
+                assert!(result.get() != 0);
+            }
+        };
+    }
+
+    nonzero_check_wrapping_neg!(core::num::NonZeroI8, nonzero_check_wrapping_neg_i8);
+    nonzero_check_wrapping_neg!(core::num::NonZeroI16, nonzero_check_wrapping_neg_i16);
+    nonzero_check_wrapping_neg!(core::num::NonZeroI32, nonzero_check_wrapping_neg_i32);
+    nonzero_check_wrapping_neg!(core::num::NonZeroI64, nonzero_check_wrapping_neg_i64);
+    nonzero_check_wrapping_neg!(core::num::NonZeroI128, nonzero_check_wrapping_neg_i128);
+    nonzero_check_wrapping_neg!(core::num::NonZeroIsize, nonzero_check_wrapping_neg_isize);
+
+    // --- from_mut ---
+
+    macro_rules! nonzero_check_from_mut {
+        ($t:ty, $nonzero_type:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let mut x: $t = kani::any();
+                let is_zero = x == 0;
+                let result = <$nonzero_type>::from_mut(&mut x);
+                if is_zero {
+                    assert!(result.is_none());
+                } else {
+                    assert!(result.is_some());
+                }
+            }
+        };
+    }
+
+    nonzero_check_from_mut!(i8, core::num::NonZeroI8, nonzero_check_from_mut_i8);
+    nonzero_check_from_mut!(i16, core::num::NonZeroI16, nonzero_check_from_mut_i16);
+    nonzero_check_from_mut!(i32, core::num::NonZeroI32, nonzero_check_from_mut_i32);
+    nonzero_check_from_mut!(i64, core::num::NonZeroI64, nonzero_check_from_mut_i64);
+    nonzero_check_from_mut!(i128, core::num::NonZeroI128, nonzero_check_from_mut_i128);
+    nonzero_check_from_mut!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_isize);
+    nonzero_check_from_mut!(u8, core::num::NonZeroU8, nonzero_check_from_mut_u8);
+    nonzero_check_from_mut!(u16, core::num::NonZeroU16, nonzero_check_from_mut_u16);
+    nonzero_check_from_mut!(u32, core::num::NonZeroU32, nonzero_check_from_mut_u32);
+    nonzero_check_from_mut!(u64, core::num::NonZeroU64, nonzero_check_from_mut_u64);
+    nonzero_check_from_mut!(u128, core::num::NonZeroU128, nonzero_check_from_mut_u128);
+    nonzero_check_from_mut!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_usize);
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index 1dd71bfb6f7b2..706cf23417cbc 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -2078,7 +2078,6 @@ macro_rules! uint_impl {
             let mut base = self;
             let mut acc: Self = 1;
 
-            #[safety::loop_invariant(true)]
             loop {
                 if (exp & 1) == 1 {
                     acc = try_opt!(acc.checked_mul(base));

From 8267fcb7105a78f2211dde51b821c4f90a3b775c Mon Sep 17 00:00:00 2001
From: Jared Reyes <jaredreyespt@gmail.com>
Date: Wed, 11 Feb 2026 12:15:12 +1100
Subject: [PATCH 2/4] Apply upstream rustfmt formatting via check_rustc.sh
 --bless

---
 library/core/src/num/nonzero.rs | 55 ++++++---------------------------
 1 file changed, 10 insertions(+), 45 deletions(-)

diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
index 6d3a1a1894605..2662a670e4678 100644
--- a/library/core/src/num/nonzero.rs
+++ b/library/core/src/num/nonzero.rs
@@ -3444,19 +3444,13 @@ mod verify {
     nonzero_check_saturating_mul!(core::num::NonZeroI32, nonzero_check_saturating_mul_i32);
     nonzero_check_saturating_mul!(core::num::NonZeroI64, nonzero_check_saturating_mul_i64);
     nonzero_check_saturating_mul!(core::num::NonZeroI128, nonzero_check_saturating_mul_i128);
-    nonzero_check_saturating_mul!(
-        core::num::NonZeroIsize,
-        nonzero_check_saturating_mul_isize
-    );
+    nonzero_check_saturating_mul!(core::num::NonZeroIsize, nonzero_check_saturating_mul_isize);
     nonzero_check_saturating_mul!(core::num::NonZeroU8, nonzero_check_saturating_mul_u8);
     nonzero_check_saturating_mul!(core::num::NonZeroU16, nonzero_check_saturating_mul_u16);
     nonzero_check_saturating_mul!(core::num::NonZeroU32, nonzero_check_saturating_mul_u32);
     nonzero_check_saturating_mul!(core::num::NonZeroU64, nonzero_check_saturating_mul_u64);
     nonzero_check_saturating_mul!(core::num::NonZeroU128, nonzero_check_saturating_mul_u128);
-    nonzero_check_saturating_mul!(
-        core::num::NonZeroUsize,
-        nonzero_check_saturating_mul_usize
-    );
+    nonzero_check_saturating_mul!(core::num::NonZeroUsize, nonzero_check_saturating_mul_usize);
 
     macro_rules! nonzero_check_checked_add {
         ($t:ty, $nonzero_type:ty, $harness:ident) => {
@@ -3476,11 +3470,7 @@ mod verify {
     nonzero_check_checked_add!(u32, core::num::NonZeroU32, nonzero_check_checked_add_u32);
     nonzero_check_checked_add!(u64, core::num::NonZeroU64, nonzero_check_checked_add_u64);
     nonzero_check_checked_add!(u128, core::num::NonZeroU128, nonzero_check_checked_add_u128);
-    nonzero_check_checked_add!(
-        usize,
-        core::num::NonZeroUsize,
-        nonzero_check_checked_add_usize
-    );
+    nonzero_check_checked_add!(usize, core::num::NonZeroUsize, nonzero_check_checked_add_usize);
 
     macro_rules! nonzero_check_saturating_add {
         ($t:ty, $nonzero_type:ty, $harness:ident) => {
@@ -3495,26 +3485,10 @@ mod verify {
     }
 
     nonzero_check_saturating_add!(u8, core::num::NonZeroU8, nonzero_check_saturating_add_u8);
-    nonzero_check_saturating_add!(
-        u16,
-        core::num::NonZeroU16,
-        nonzero_check_saturating_add_u16
-    );
-    nonzero_check_saturating_add!(
-        u32,
-        core::num::NonZeroU32,
-        nonzero_check_saturating_add_u32
-    );
-    nonzero_check_saturating_add!(
-        u64,
-        core::num::NonZeroU64,
-        nonzero_check_saturating_add_u64
-    );
-    nonzero_check_saturating_add!(
-        u128,
-        core::num::NonZeroU128,
-        nonzero_check_saturating_add_u128
-    );
+    nonzero_check_saturating_add!(u16, core::num::NonZeroU16, nonzero_check_saturating_add_u16);
+    nonzero_check_saturating_add!(u32, core::num::NonZeroU32, nonzero_check_saturating_add_u32);
+    nonzero_check_saturating_add!(u64, core::num::NonZeroU64, nonzero_check_saturating_add_u64);
+    nonzero_check_saturating_add!(u128, core::num::NonZeroU128, nonzero_check_saturating_add_u128);
     nonzero_check_saturating_add!(
         usize,
         core::num::NonZeroUsize,
@@ -3737,10 +3711,7 @@ mod verify {
     nonzero_check_overflowing_abs!(core::num::NonZeroI32, nonzero_check_overflowing_abs_i32);
     nonzero_check_overflowing_abs!(core::num::NonZeroI64, nonzero_check_overflowing_abs_i64);
     nonzero_check_overflowing_abs!(core::num::NonZeroI128, nonzero_check_overflowing_abs_i128);
-    nonzero_check_overflowing_abs!(
-        core::num::NonZeroIsize,
-        nonzero_check_overflowing_abs_isize
-    );
+    nonzero_check_overflowing_abs!(core::num::NonZeroIsize, nonzero_check_overflowing_abs_isize);
 
     macro_rules! nonzero_check_saturating_abs {
         ($nonzero_type:ty, $harness:ident) => {
@@ -3759,10 +3730,7 @@ mod verify {
     nonzero_check_saturating_abs!(core::num::NonZeroI32, nonzero_check_saturating_abs_i32);
     nonzero_check_saturating_abs!(core::num::NonZeroI64, nonzero_check_saturating_abs_i64);
     nonzero_check_saturating_abs!(core::num::NonZeroI128, nonzero_check_saturating_abs_i128);
-    nonzero_check_saturating_abs!(
-        core::num::NonZeroIsize,
-        nonzero_check_saturating_abs_isize
-    );
+    nonzero_check_saturating_abs!(core::num::NonZeroIsize, nonzero_check_saturating_abs_isize);
 
     macro_rules! nonzero_check_wrapping_abs {
         ($nonzero_type:ty, $harness:ident) => {
@@ -3860,10 +3828,7 @@ mod verify {
     nonzero_check_overflowing_neg!(core::num::NonZeroI32, nonzero_check_overflowing_neg_i32);
     nonzero_check_overflowing_neg!(core::num::NonZeroI64, nonzero_check_overflowing_neg_i64);
     nonzero_check_overflowing_neg!(core::num::NonZeroI128, nonzero_check_overflowing_neg_i128);
-    nonzero_check_overflowing_neg!(
-        core::num::NonZeroIsize,
-        nonzero_check_overflowing_neg_isize
-    );
+    nonzero_check_overflowing_neg!(core::num::NonZeroIsize, nonzero_check_overflowing_neg_isize);
 
     macro_rules! nonzero_check_wrapping_neg {
         ($nonzero_type:ty, $harness:ident) => {

From b23d05f9f61ea6c749ab55dfc6749c8903c8ecee Mon Sep 17 00:00:00 2001
From: Jared Reyes <jaredreyespt@gmail.com>
Date: Sun, 22 Feb 2026 06:56:02 +1100
Subject: [PATCH 3/4] 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.
---
 library/core/src/num/nonzero.rs | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
index 2662a670e4678..e609b8bc95388 100644
--- a/library/core/src/num/nonzero.rs
+++ b/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 {

From 9d26114b68021d514c6ba3612cd7a2a7967a629f Mon Sep 17 00:00:00 2001
From: Jared Reyes <jaredreyespt@gmail.com>
Date: Sun, 22 Feb 2026 08:13:19 +1100
Subject: [PATCH 4/4] Fix checked_pow_i128/u128 CBMC timeout: bound exponent to
 avoid explosion

Same fix as saturating_pow_128: use a dedicated macro with exp <= 10
and #[kani::unwind(5)] for the 128-bit checked_pow harnesses.
---
 library/core/src/num/nonzero.rs | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
index e609b8bc95388..a6972475cd9d5 100644
--- a/library/core/src/num/nonzero.rs
+++ b/library/core/src/num/nonzero.rs
@@ -3515,15 +3515,33 @@ mod verify {
     nonzero_check_checked_pow!(core::num::NonZeroI16, nonzero_check_checked_pow_i16);
     nonzero_check_checked_pow!(core::num::NonZeroI32, nonzero_check_checked_pow_i32);
     nonzero_check_checked_pow!(core::num::NonZeroI64, nonzero_check_checked_pow_i64);
-    nonzero_check_checked_pow!(core::num::NonZeroI128, nonzero_check_checked_pow_i128);
     nonzero_check_checked_pow!(core::num::NonZeroIsize, nonzero_check_checked_pow_isize);
     nonzero_check_checked_pow!(core::num::NonZeroU8, nonzero_check_checked_pow_u8);
     nonzero_check_checked_pow!(core::num::NonZeroU16, nonzero_check_checked_pow_u16);
     nonzero_check_checked_pow!(core::num::NonZeroU32, nonzero_check_checked_pow_u32);
     nonzero_check_checked_pow!(core::num::NonZeroU64, nonzero_check_checked_pow_u64);
-    nonzero_check_checked_pow!(core::num::NonZeroU128, nonzero_check_checked_pow_u128);
     nonzero_check_checked_pow!(core::num::NonZeroUsize, nonzero_check_checked_pow_usize);
 
+    // 128-bit types use a bounded exponent to avoid CBMC timeout (same reason
+    // as nonzero_check_saturating_pow_128): checked_pow uses binary exponentiation
+    // with expensive 128-bit multiplications in CBMC's bitvector encoding.
+    macro_rules! nonzero_check_checked_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);
+                if let Some(result) = x.checked_pow(exp) {
+                    assert!(result.get() != 0);
+                }
+            }
+        };
+    }
+
+    nonzero_check_checked_pow_128!(core::num::NonZeroI128, nonzero_check_checked_pow_i128);
+    nonzero_check_checked_pow_128!(core::num::NonZeroU128, nonzero_check_checked_pow_u128);
+
     macro_rules! nonzero_check_saturating_pow {
         ($nonzero_type:ty, $harness:ident) => {
             #[kani::proof]