From a6980208bc9a569b2b98559154ae3911f2286a21 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Sun, 8 Feb 2026 14:37:25 +1100 Subject: [PATCH 1/7] 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 Date: Wed, 11 Feb 2026 12:15:12 +1100 Subject: [PATCH 2/7] 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 Date: Sun, 22 Feb 2026 06:56:02 +1100 Subject: [PATCH 3/7] 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 Date: Sun, 22 Feb 2026 08:13:19 +1100 Subject: [PATCH 4/7] 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] From b16b2db7989d3ab607e195dab04f12cf3eec368d Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Thu, 2 Apr 2026 11:39:58 +1100 Subject: [PATCH 5/7] Add missing isqrt harnesses for u64, u128, and usize Add isqrt verification for the remaining unsigned types. u128 uses checked_mul to avoid CBMC bitvector overflow concerns. --- library/core/src/num/nonzero.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index a6972475cd9d5..0a1c536ad0be3 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -3667,6 +3667,24 @@ mod verify { 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); + nonzero_check_isqrt!(core::num::NonZeroU64, nonzero_check_isqrt_u64); + nonzero_check_isqrt!(core::num::NonZeroUsize, nonzero_check_isqrt_usize); + + // 128-bit isqrt uses checked_mul to avoid potential CBMC overflow + // concerns: while isqrt(u128::MAX)^2 fits in u128 mathematically, + // CBMC's bitvector encoding may not prove this without help. + #[kani::proof] + pub fn nonzero_check_isqrt_u128() { + let x: core::num::NonZeroU128 = kani::any(); + let result = x.isqrt(); + assert!(result.get() != 0); + let r = result.get(); + let v = x.get(); + match r.checked_mul(r) { + Some(r_sq) => assert!(r_sq <= v), + None => panic!("isqrt result squared overflowed u128"), + } + } // --- Signed-only operations: neg, abs family, checked_neg family --- From a432b6eef81edda7626f21bff79459030ae24d83 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Tue, 18 Aug 2026 20:17:27 +1000 Subject: [PATCH 6/7] Restore checked_pow loop invariants; scope workaround to pow harnesses Address review feedback: keep #327's #[safety::loop_invariant(true)] annotations on the primitive checked_pow untouched (int_macros.rs and uint_macros.rs are identical to main again) and instead scope the loop-contracts workaround to the affected NonZero harnesses. Under -Z loop-contracts, the trivial invariant makes CBMC abstract the checked_pow loop by havocking acc, so the abstracted primitive can return Some(0), spuriously reaching the unreachable zero arm of NonZero::new_unchecked inside the pow harnesses. The 24 checked_pow/ saturating_pow harnesses now stub the primitive checked_pow with a verbatim copy of its implementation (try_opt! expanded) minus the loop contract: no nondeterminism, no assumptions, fully unwound by the existing unwind bounds, so the proofs remain exhaustive over the real NonZero code including the new_unchecked safety condition. Verified with the pinned Kani (415ca50) using CI-equivalent flags: all 24 pow harnesses pass; without the stub the harnesses fail on the unreachable-code check, confirming the workaround is required. Co-Authored-By: Claude Fable 5 --- library/core/src/num/int_macros.rs | 1 + library/core/src/num/nonzero.rs | 239 ++++++++++++++++++++++++---- library/core/src/num/uint_macros.rs | 1 + 3 files changed, 213 insertions(+), 28 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index af4567b0e6bfa..4468c1489bfb5 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -1736,6 +1736,7 @@ 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 0a1c536ad0be3..d52836e061eba 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -3497,10 +3497,67 @@ mod verify { // --- Power operations --- + // The primitive `checked_pow` implementations carry a trivial + // `#[safety::loop_invariant(true)]` (added in PR #327, consumed by the + // autoharness runs). Under `-Z loop-contracts` that trivial invariant makes + // CBMC abstract the loop by havocking `acc`, so the abstracted primitive + // can return `Some(0)` — spuriously violating `NonZero::new_unchecked`'s + // nonzero precondition inside these harnesses. Per review feedback, the + // shared annotation is left untouched; instead the pow harnesses stub the + // primitive `checked_pow` with a verbatim copy of its implementation + // (`uint_macros.rs`/`int_macros.rs`, `try_opt!` expanded) minus the loop + // contract. The copy is semantically identical — no nondeterminism, no + // `kani::assume` — and the harness unwind bound fully unwinds it + // (`exp: u32` gives at most 32 squarings), so the proofs remain exhaustive + // over the real `NonZero` code, including the `new_unchecked` safety + // condition. If the primitive implementation changes, update this copy. + macro_rules! stub_checked_pow { + ($int_type:ident, $stub:ident) => { + pub const fn $stub(base: $int_type, mut exp: u32) -> Option<$int_type> { + if exp == 0 { + return Some(1); + } + let mut base = base; + let mut acc: $int_type = 1; + loop { + if (exp & 1) == 1 { + acc = match acc.checked_mul(base) { + Some(v) => v, + None => return None, + }; + // since exp!=0, finally the exp must be 1. + if exp == 1 { + return Some(acc); + } + } + exp /= 2; + base = match base.checked_mul(base) { + Some(v) => v, + None => return None, + }; + } + } + }; + } + + stub_checked_pow!(i8, stub_checked_pow_i8); + stub_checked_pow!(i16, stub_checked_pow_i16); + stub_checked_pow!(i32, stub_checked_pow_i32); + stub_checked_pow!(i64, stub_checked_pow_i64); + stub_checked_pow!(i128, stub_checked_pow_i128); + stub_checked_pow!(isize, stub_checked_pow_isize); + stub_checked_pow!(u8, stub_checked_pow_u8); + stub_checked_pow!(u16, stub_checked_pow_u16); + stub_checked_pow!(u32, stub_checked_pow_u32); + stub_checked_pow!(u64, stub_checked_pow_u64); + stub_checked_pow!(u128, stub_checked_pow_u128); + stub_checked_pow!(usize, stub_checked_pow_usize); + macro_rules! nonzero_check_checked_pow { - ($nonzero_type:ty, $harness:ident) => { + ($nonzero_type:ty, $int_type:ident, $stub:ident, $harness:ident) => { #[kani::proof] #[kani::unwind(34)] + #[kani::stub($int_type::checked_pow, $stub)] pub fn $harness() { let x: $nonzero_type = kani::any(); let exp: u32 = kani::any(); @@ -3511,24 +3568,75 @@ mod verify { }; } - 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::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::NonZeroUsize, nonzero_check_checked_pow_usize); + nonzero_check_checked_pow!( + core::num::NonZeroI8, + i8, + stub_checked_pow_i8, + nonzero_check_checked_pow_i8 + ); + nonzero_check_checked_pow!( + core::num::NonZeroI16, + i16, + stub_checked_pow_i16, + nonzero_check_checked_pow_i16 + ); + nonzero_check_checked_pow!( + core::num::NonZeroI32, + i32, + stub_checked_pow_i32, + nonzero_check_checked_pow_i32 + ); + nonzero_check_checked_pow!( + core::num::NonZeroI64, + i64, + stub_checked_pow_i64, + nonzero_check_checked_pow_i64 + ); + nonzero_check_checked_pow!( + core::num::NonZeroIsize, + isize, + stub_checked_pow_isize, + nonzero_check_checked_pow_isize + ); + nonzero_check_checked_pow!( + core::num::NonZeroU8, + u8, + stub_checked_pow_u8, + nonzero_check_checked_pow_u8 + ); + nonzero_check_checked_pow!( + core::num::NonZeroU16, + u16, + stub_checked_pow_u16, + nonzero_check_checked_pow_u16 + ); + nonzero_check_checked_pow!( + core::num::NonZeroU32, + u32, + stub_checked_pow_u32, + nonzero_check_checked_pow_u32 + ); + nonzero_check_checked_pow!( + core::num::NonZeroU64, + u64, + stub_checked_pow_u64, + nonzero_check_checked_pow_u64 + ); + nonzero_check_checked_pow!( + core::num::NonZeroUsize, + usize, + stub_checked_pow_usize, + 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) => { + ($nonzero_type:ty, $int_type:ident, $stub:ident, $harness:ident) => { #[kani::proof] #[kani::unwind(5)] + #[kani::stub($int_type::checked_pow, $stub)] pub fn $harness() { let x: $nonzero_type = kani::any(); let exp: u32 = kani::any_where(|&e| e <= 10); @@ -3539,13 +3647,27 @@ mod verify { }; } - 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); + nonzero_check_checked_pow_128!( + core::num::NonZeroI128, + i128, + stub_checked_pow_i128, + nonzero_check_checked_pow_i128 + ); + nonzero_check_checked_pow_128!( + core::num::NonZeroU128, + u128, + stub_checked_pow_u128, + nonzero_check_checked_pow_u128 + ); + // `saturating_pow` delegates to the primitive `saturating_pow`, which calls + // `checked_pow` internally — so the same `checked_pow` stub applies (see the + // comment on `stub_checked_pow` above). macro_rules! nonzero_check_saturating_pow { - ($nonzero_type:ty, $harness:ident) => { + ($nonzero_type:ty, $int_type:ident, $stub:ident, $harness:ident) => { #[kani::proof] #[kani::unwind(34)] + #[kani::stub($int_type::checked_pow, $stub)] pub fn $harness() { let x: $nonzero_type = kani::any(); let exp: u32 = kani::any(); @@ -3555,16 +3677,66 @@ mod verify { }; } - 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::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::NonZeroUsize, nonzero_check_saturating_pow_usize); + nonzero_check_saturating_pow!( + core::num::NonZeroI8, + i8, + stub_checked_pow_i8, + nonzero_check_saturating_pow_i8 + ); + nonzero_check_saturating_pow!( + core::num::NonZeroI16, + i16, + stub_checked_pow_i16, + nonzero_check_saturating_pow_i16 + ); + nonzero_check_saturating_pow!( + core::num::NonZeroI32, + i32, + stub_checked_pow_i32, + nonzero_check_saturating_pow_i32 + ); + nonzero_check_saturating_pow!( + core::num::NonZeroI64, + i64, + stub_checked_pow_i64, + nonzero_check_saturating_pow_i64 + ); + nonzero_check_saturating_pow!( + core::num::NonZeroIsize, + isize, + stub_checked_pow_isize, + nonzero_check_saturating_pow_isize + ); + nonzero_check_saturating_pow!( + core::num::NonZeroU8, + u8, + stub_checked_pow_u8, + nonzero_check_saturating_pow_u8 + ); + nonzero_check_saturating_pow!( + core::num::NonZeroU16, + u16, + stub_checked_pow_u16, + nonzero_check_saturating_pow_u16 + ); + nonzero_check_saturating_pow!( + core::num::NonZeroU32, + u32, + stub_checked_pow_u32, + nonzero_check_saturating_pow_u32 + ); + nonzero_check_saturating_pow!( + core::num::NonZeroU64, + u64, + stub_checked_pow_u64, + nonzero_check_saturating_pow_u64 + ); + nonzero_check_saturating_pow!( + core::num::NonZeroUsize, + usize, + stub_checked_pow_usize, + 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 @@ -3572,9 +3744,10 @@ mod verify { // 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) => { + ($nonzero_type:ty, $int_type:ident, $stub:ident, $harness:ident) => { #[kani::proof] #[kani::unwind(5)] + #[kani::stub($int_type::checked_pow, $stub)] pub fn $harness() { let x: $nonzero_type = kani::any(); let exp: u32 = kani::any_where(|&e| e <= 10); @@ -3584,8 +3757,18 @@ mod verify { }; } - 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); + nonzero_check_saturating_pow_128!( + core::num::NonZeroI128, + i128, + stub_checked_pow_i128, + nonzero_check_saturating_pow_i128 + ); + nonzero_check_saturating_pow_128!( + core::num::NonZeroU128, + u128, + stub_checked_pow_u128, + nonzero_check_saturating_pow_u128 + ); // --- Unsigned-only operations --- diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 706cf23417cbc..1dd71bfb6f7b2 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2078,6 +2078,7 @@ 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 049188b2cfa74a0f4c753e496b964a3b24fb4a0f Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Tue, 18 Aug 2026 21:50:07 +1000 Subject: [PATCH 7/7] Fix isqrt harness CI timeouts with bounded intervals for wide types The full-range isqrt harnesses for u64, usize, and u128 exceeded CI's 10-minute per-harness timeout in both autoharness jobs: the Karatsuba isqrt implementation performs symbolic divisions and multiplications at half the operand width, which is intractable for CBMC's bitvector encoding at widths >= 64 (full-range u32 already takes ~90s). Following the interval pattern of the carrying_mul harnesses in num/mod.rs, keep u8/u16/u32 full-range and check each wide type with kissat on three bounded windows: small ([1, 10], covering the result-zero boundary relevant to the NonZero safety property), large ([MAX - 10, MAX]), and mid-edge ([MAX/2 - 10, MAX/2 + 10]). Verified with the pinned Kani (415ca50) and CI-equivalent flags: all 12 isqrt harnesses pass, the longest in ~40s. Co-Authored-By: Claude Fable 5 --- library/core/src/num/nonzero.rs | 88 ++++++++++++++++++++++++++------- 1 file changed, 71 insertions(+), 17 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index d52836e061eba..545be98b6f575 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -3850,25 +3850,79 @@ mod verify { 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); - nonzero_check_isqrt!(core::num::NonZeroU64, nonzero_check_isqrt_u64); - nonzero_check_isqrt!(core::num::NonZeroUsize, nonzero_check_isqrt_usize); - - // 128-bit isqrt uses checked_mul to avoid potential CBMC overflow - // concerns: while isqrt(u128::MAX)^2 fits in u128 mathematically, - // CBMC's bitvector encoding may not prove this without help. - #[kani::proof] - pub fn nonzero_check_isqrt_u128() { - let x: core::num::NonZeroU128 = kani::any(); - let result = x.isqrt(); - assert!(result.get() != 0); - let r = result.get(); - let v = x.get(); - match r.checked_mul(r) { - Some(r_sq) => assert!(r_sq <= v), - None => panic!("isqrt result squared overflowed u128"), - } + + // BOUNDED verification for u64/usize/u128 isqrt. The Karatsuba isqrt + // implementation performs symbolic divisions and multiplications at half + // the operand width, which blows past CI's 10-minute per-harness timeout + // in CBMC's bitvector encoding for widths >= 64 (full-range u32 already + // takes ~90s; each doubling is far worse). Following the interval pattern + // of the `carrying_mul` harnesses in `num/mod.rs`, each wide type is + // checked with kissat on three input windows: small ([1, 10], which covers + // the result-zero boundary that matters for the NonZero safety property), + // large ([MAX - 10, MAX]), and mid-edge ([MAX/2 - 10, MAX/2 + 10]). + macro_rules! nonzero_check_isqrt_intervals { + ($nonzero_type:ty, $int_type:ty, $($harness:ident, $min:expr, $max:expr),+) => { + $( + #[kani::proof] + #[kani::solver(kissat)] + pub fn $harness() { + let x: $nonzero_type = kani::any(); + kani::assume(x.get() >= $min && x.get() <= $max); + let result = x.isqrt(); + assert!(result.get() != 0); + // result^2 <= x, via checked_mul so the harness itself + // cannot overflow for the widest types. + let r = result.get(); + let v = x.get(); + match r.checked_mul(r) { + Some(r_sq) => assert!(r_sq <= v), + None => panic!("isqrt result squared overflowed"), + } + } + )+ + }; } + nonzero_check_isqrt_intervals!( + core::num::NonZeroU64, + u64, + nonzero_check_isqrt_u64_small, + 1u64, + 10u64, + nonzero_check_isqrt_u64_large, + u64::MAX - 10u64, + u64::MAX, + nonzero_check_isqrt_u64_mid_edge, + (u64::MAX / 2) - 10u64, + (u64::MAX / 2) + 10u64 + ); + nonzero_check_isqrt_intervals!( + core::num::NonZeroUsize, + usize, + nonzero_check_isqrt_usize_small, + 1usize, + 10usize, + nonzero_check_isqrt_usize_large, + usize::MAX - 10usize, + usize::MAX, + nonzero_check_isqrt_usize_mid_edge, + (usize::MAX / 2) - 10usize, + (usize::MAX / 2) + 10usize + ); + nonzero_check_isqrt_intervals!( + core::num::NonZeroU128, + u128, + nonzero_check_isqrt_u128_small, + 1u128, + 10u128, + nonzero_check_isqrt_u128_large, + u128::MAX - 10u128, + u128::MAX, + nonzero_check_isqrt_u128_mid_edge, + (u128::MAX / 2) - 10u128, + (u128::MAX / 2) + 10u128 + ); + // --- Signed-only operations: neg, abs family, checked_neg family --- macro_rules! nonzero_check_neg {