From cbd05387f6df5c95e220b07d8506a7b3f07fafd4 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Sun, 1 Dec 2024 17:28:39 -0500 Subject: [PATCH 1/8] rotates --- library/core/src/num/nonzero.rs | 88 +++++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index ac7b1fca9fa8..2c606afe4e92 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2265,3 +2265,91 @@ mod verify { nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); } + +#[cfg(kani)] +mod macro_nonzero_check_rotate_left { + use super::*; + macro_rules! nonzero_check_rotate_left { + ($t:ty, $nonzero_type:ty, $nonzero_check_rotate_left_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_rotate_left_for() { + let x: $t = kani::any(); + let n: u32 = kani::any(); + kani::assume(x != 0); // x must be non-zero + + // Ensure that n is within a valid range for rotating + // kani::assume(n < (std::mem::size_of::<$t>() as u32 * 8)); + // need to use core::mem instead of std::mem + kani::assume(n < (core::mem::size_of::<$t>() as u32 * 8)); + kani::assume(n >= 0); + + unsafe { + let x = <$nonzero_type>::new_unchecked(x); + } + + // Perform rotate_left + let result = x.rotate_left(n); + + // Ensure the result is still non-zero + assert!(result != 0); + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_rotate_left!(i8, core::num::NonZeroI8, nonzero_check_rotate_left_for_i8); + nonzero_check_rotate_left!(i16, core::num::NonZeroI16, nonzero_check_rotate_left_for_16); + nonzero_check_rotate_left!(i32, core::num::NonZeroI32, nonzero_check_rotate_left_for_32); + nonzero_check_rotate_left!(i64, core::num::NonZeroI64, nonzero_check_rotate_left_for_64); + nonzero_check_rotate_left!(i128, core::num::NonZeroI128, nonzero_check_rotate_left_for_128); + nonzero_check_rotate_left!(isize, core::num::NonZeroIsize, nonzero_check_rotate_left_for_isize); + nonzero_check_rotate_left!(u8, core::num::NonZeroU8, nonzero_check_rotate_left_for_u8); + nonzero_check_rotate_left!(u16, core::num::NonZeroU16, nonzero_check_rotate_left_for_u16); + nonzero_check_rotate_left!(u32, core::num::NonZeroU32, nonzero_check_rotate_left_for_u32); + nonzero_check_rotate_left!(u64, core::num::NonZeroU64, nonzero_check_rotate_left_for_u64); + nonzero_check_rotate_left!(u128, core::num::NonZeroU128, nonzero_check_rotate_left_for_u128); + nonzero_check_rotate_left!(usize, core::num::NonZeroUsize, nonzero_check_rotate_left_for_usize); +} + +#[cfg(kani)] +mod macro_nonzero_check_rotate_right { + use super::*; + macro_rules! nonzero_check_rotate_right { + ($t:ty, $nonzero_type:ty, $nonzero_check_rotate_right_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_rotate_right_for() { + let x: $t = kani::any(); + let n: u32 = kani::any(); + kani::assume(x != 0); // x must be non-zero + + // Ensure that n is within a valid range for rotating + kani::assume(n < (core::mem::size_of::<$t>() as u32 * 8)); + kani::assume(n >= 0); + + unsafe { + let x = <$nonzero_type>::new_unchecked(x); + } + + // Perform rotate_right + let result = x.rotate_right(n); + + // Ensure the result is still non-zero + assert!(result != 0); + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_rotate_right!(i8, core::num::NonZeroI8, nonzero_check_rotate_right_for_i8); + nonzero_check_rotate_right!(i16, core::num::NonZeroI16, nonzero_check_rotate_right_for_16); + nonzero_check_rotate_right!(i32, core::num::NonZeroI32, nonzero_check_rotate_right_for_32); + nonzero_check_rotate_right!(i64, core::num::NonZeroI64, nonzero_check_rotate_right_for_64); + nonzero_check_rotate_right!(i128, core::num::NonZeroI128, nonzero_check_rotate_right_for_128); + nonzero_check_rotate_right!(isize, core::num::NonZeroIsize, nonzero_check_rotate_right_for_isize); + nonzero_check_rotate_right!(u8, core::num::NonZeroU8, nonzero_check_rotate_right_for_u8); + nonzero_check_rotate_right!(u16, core::num::NonZeroU16, nonzero_check_rotate_right_for_u16); + nonzero_check_rotate_right!(u32, core::num::NonZeroU32, nonzero_check_rotate_right_for_u32); + nonzero_check_rotate_right!(u64, core::num::NonZeroU64, nonzero_check_rotate_right_for_u64); + nonzero_check_rotate_right!(u128, core::num::NonZeroU128, nonzero_check_rotate_right_for_u128); + nonzero_check_rotate_right!(usize, core::num::NonZeroUsize, nonzero_check_rotate_right_for_usize); +} \ No newline at end of file From 81acb67caf1c31a43171b8a7140e2412daade267 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 01:02:42 -0500 Subject: [PATCH 2/8] rotate right refrain from re-using names --- library/core/src/num/nonzero.rs | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 2c606afe4e92..0ddf40671aa4 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2318,23 +2318,25 @@ mod macro_nonzero_check_rotate_right { ($t:ty, $nonzero_type:ty, $nonzero_check_rotate_right_for:ident) => { #[kani::proof] pub fn $nonzero_check_rotate_right_for() { - let x: $t = kani::any(); + let int_x: $t = kani::any(); let n: u32 = kani::any(); - kani::assume(x != 0); // x must be non-zero + kani::assume(int_x != 0); // x must be non-zero // Ensure that n is within a valid range for rotating kani::assume(n < (core::mem::size_of::<$t>() as u32 * 8)); kani::assume(n >= 0); unsafe { - let x = <$nonzero_type>::new_unchecked(x); + let x = <$nonzero_type>::new_unchecked(int_x); + + // Perform rotate_right + let result = x.rotate_right(n); + + // Ensure the result is still non-zero + assert!(result.get() != 0); } - // Perform rotate_right - let result = x.rotate_right(n); - // Ensure the result is still non-zero - assert!(result != 0); } }; } @@ -2352,4 +2354,4 @@ mod macro_nonzero_check_rotate_right { nonzero_check_rotate_right!(u64, core::num::NonZeroU64, nonzero_check_rotate_right_for_u64); nonzero_check_rotate_right!(u128, core::num::NonZeroU128, nonzero_check_rotate_right_for_u128); nonzero_check_rotate_right!(usize, core::num::NonZeroUsize, nonzero_check_rotate_right_for_usize); -} \ No newline at end of file +} From 38163161f931fdecbe87eb6b72bfe65e74748445 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 01:04:31 -0500 Subject: [PATCH 3/8] rotate_left refrain from re-using names --- library/core/src/num/nonzero.rs | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 0ddf40671aa4..65eb8b1ffe48 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2273,9 +2273,9 @@ mod macro_nonzero_check_rotate_left { ($t:ty, $nonzero_type:ty, $nonzero_check_rotate_left_for:ident) => { #[kani::proof] pub fn $nonzero_check_rotate_left_for() { - let x: $t = kani::any(); + let int_x: $t = kani::any(); let n: u32 = kani::any(); - kani::assume(x != 0); // x must be non-zero + kani::assume(int_x != 0); // x must be non-zero // Ensure that n is within a valid range for rotating // kani::assume(n < (std::mem::size_of::<$t>() as u32 * 8)); @@ -2284,14 +2284,13 @@ mod macro_nonzero_check_rotate_left { kani::assume(n >= 0); unsafe { - let x = <$nonzero_type>::new_unchecked(x); + let x = <$nonzero_type>::new_unchecked(int_x); + // Perform rotate_left + let result = x.rotate_left(n); + + // Ensure the result is still non-zero + assert!(result.get() != 0); } - - // Perform rotate_left - let result = x.rotate_left(n); - - // Ensure the result is still non-zero - assert!(result != 0); } }; } From ae8d17c5c38a74ec75106aa0d00bc18573ccd7e6 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 16:46:53 -0500 Subject: [PATCH 4/8] merge rotate left and right macros, remove comments, assume not need --- library/core/src/num/nonzero.rs | 90 +++++++-------------------------- 1 file changed, 18 insertions(+), 72 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 65eb8b1ffe48..7d0644573b93 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2267,90 +2267,36 @@ mod verify { } #[cfg(kani)] -mod macro_nonzero_check_rotate_left { +mod macro_nonzero_check_rotate_left_and_right { use super::*; - macro_rules! nonzero_check_rotate_left { - ($t:ty, $nonzero_type:ty, $nonzero_check_rotate_left_for:ident) => { - #[kani::proof] - pub fn $nonzero_check_rotate_left_for() { - let int_x: $t = kani::any(); - let n: u32 = kani::any(); - kani::assume(int_x != 0); // x must be non-zero - - // Ensure that n is within a valid range for rotating - // kani::assume(n < (std::mem::size_of::<$t>() as u32 * 8)); - // need to use core::mem instead of std::mem - kani::assume(n < (core::mem::size_of::<$t>() as u32 * 8)); - kani::assume(n >= 0); - - unsafe { - let x = <$nonzero_type>::new_unchecked(int_x); - // Perform rotate_left - let result = x.rotate_left(n); - - // Ensure the result is still non-zero - assert!(result.get() != 0); - } - } - }; - } - - // Use the macro to generate different versions of the function for multiple types - nonzero_check_rotate_left!(i8, core::num::NonZeroI8, nonzero_check_rotate_left_for_i8); - nonzero_check_rotate_left!(i16, core::num::NonZeroI16, nonzero_check_rotate_left_for_16); - nonzero_check_rotate_left!(i32, core::num::NonZeroI32, nonzero_check_rotate_left_for_32); - nonzero_check_rotate_left!(i64, core::num::NonZeroI64, nonzero_check_rotate_left_for_64); - nonzero_check_rotate_left!(i128, core::num::NonZeroI128, nonzero_check_rotate_left_for_128); - nonzero_check_rotate_left!(isize, core::num::NonZeroIsize, nonzero_check_rotate_left_for_isize); - nonzero_check_rotate_left!(u8, core::num::NonZeroU8, nonzero_check_rotate_left_for_u8); - nonzero_check_rotate_left!(u16, core::num::NonZeroU16, nonzero_check_rotate_left_for_u16); - nonzero_check_rotate_left!(u32, core::num::NonZeroU32, nonzero_check_rotate_left_for_u32); - nonzero_check_rotate_left!(u64, core::num::NonZeroU64, nonzero_check_rotate_left_for_u64); - nonzero_check_rotate_left!(u128, core::num::NonZeroU128, nonzero_check_rotate_left_for_u128); - nonzero_check_rotate_left!(usize, core::num::NonZeroUsize, nonzero_check_rotate_left_for_usize); -} - -#[cfg(kani)] -mod macro_nonzero_check_rotate_right { - use super::*; - macro_rules! nonzero_check_rotate_right { + macro_rules! nonzero_check_rotate_left_and_right { ($t:ty, $nonzero_type:ty, $nonzero_check_rotate_right_for:ident) => { #[kani::proof] pub fn $nonzero_check_rotate_right_for() { let int_x: $t = kani::any(); let n: u32 = kani::any(); - kani::assume(int_x != 0); // x must be non-zero - - // Ensure that n is within a valid range for rotating + kani::assume(int_x != 0); kani::assume(n < (core::mem::size_of::<$t>() as u32 * 8)); - kani::assume(n >= 0); - unsafe { let x = <$nonzero_type>::new_unchecked(int_x); - - // Perform rotate_right - let result = x.rotate_right(n); - - // Ensure the result is still non-zero - assert!(result.get() != 0); - } - - + let result = x.rotate_left(n).rotate_right(n); + assert!(result == x); + } } }; } // Use the macro to generate different versions of the function for multiple types - nonzero_check_rotate_right!(i8, core::num::NonZeroI8, nonzero_check_rotate_right_for_i8); - nonzero_check_rotate_right!(i16, core::num::NonZeroI16, nonzero_check_rotate_right_for_16); - nonzero_check_rotate_right!(i32, core::num::NonZeroI32, nonzero_check_rotate_right_for_32); - nonzero_check_rotate_right!(i64, core::num::NonZeroI64, nonzero_check_rotate_right_for_64); - nonzero_check_rotate_right!(i128, core::num::NonZeroI128, nonzero_check_rotate_right_for_128); - nonzero_check_rotate_right!(isize, core::num::NonZeroIsize, nonzero_check_rotate_right_for_isize); - nonzero_check_rotate_right!(u8, core::num::NonZeroU8, nonzero_check_rotate_right_for_u8); - nonzero_check_rotate_right!(u16, core::num::NonZeroU16, nonzero_check_rotate_right_for_u16); - nonzero_check_rotate_right!(u32, core::num::NonZeroU32, nonzero_check_rotate_right_for_u32); - nonzero_check_rotate_right!(u64, core::num::NonZeroU64, nonzero_check_rotate_right_for_u64); - nonzero_check_rotate_right!(u128, core::num::NonZeroU128, nonzero_check_rotate_right_for_u128); - nonzero_check_rotate_right!(usize, core::num::NonZeroUsize, nonzero_check_rotate_right_for_usize); + nonzero_check_rotate_left_and_right!(i8, core::num::NonZeroI8, nonzero_check_rotate_for_i8); + nonzero_check_rotate_left_and_right!(i16, core::num::NonZeroI16, nonzero_check_rotate_for_16); + nonzero_check_rotate_left_and_right!(i32, core::num::NonZeroI32, nonzero_check_rotate_for_32); + nonzero_check_rotate_left_and_right!(i64, core::num::NonZeroI64, nonzero_check_rotate_for_64); + nonzero_check_rotate_left_and_right!(i128, core::num::NonZeroI128, nonzero_check_rotate_for_128); + nonzero_check_rotate_left_and_right!(isize, core::num::NonZeroIsize, nonzero_check_rotate_for_isize); + nonzero_check_rotate_left_and_right!(u8, core::num::NonZeroU8, nonzero_check_rotate_for_u8); + nonzero_check_rotate_left_and_right!(u16, core::num::NonZeroU16, nonzero_check_rotate_for_u16); + nonzero_check_rotate_left_and_right!(u32, core::num::NonZeroU32, nonzero_check_rotate_for_u32); + nonzero_check_rotate_left_and_right!(u64, core::num::NonZeroU64, nonzero_check_rotate_for_u64); + nonzero_check_rotate_left_and_right!(u128, core::num::NonZeroU128, nonzero_check_rotate_for_u128); + nonzero_check_rotate_left_and_right!(usize, core::num::NonZeroUsize, nonzero_check_rotate_for_usize); } From 2e89dfd35901657b5ee0ee3211daa22c36a14a2f Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 17:28:45 -0500 Subject: [PATCH 5/8] remove kani::assume(n < (core::mem::size_of::<$t>() as u32 * 8)); --- library/core/src/num/nonzero.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 7d0644573b93..a8ee3e50c521 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2276,7 +2276,6 @@ mod macro_nonzero_check_rotate_left_and_right { let int_x: $t = kani::any(); let n: u32 = kani::any(); kani::assume(int_x != 0); - kani::assume(n < (core::mem::size_of::<$t>() as u32 * 8)); unsafe { let x = <$nonzero_type>::new_unchecked(int_x); let result = x.rotate_left(n).rotate_right(n); From ca4b9d0c8a5453981dc26cb373e32787063008b2 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 21:20:25 -0500 Subject: [PATCH 6/8] avoid unsafe code block by use any() directly with nonezero --- library/core/src/num/nonzero.rs | 40 +++++++++++++++------------------ 1 file changed, 18 insertions(+), 22 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index a8ee3e50c521..cac8a3fe7ca9 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2270,32 +2270,28 @@ mod verify { mod macro_nonzero_check_rotate_left_and_right { use super::*; macro_rules! nonzero_check_rotate_left_and_right { - ($t:ty, $nonzero_type:ty, $nonzero_check_rotate_right_for:ident) => { + ($nonzero_type:ty, $nonzero_check_rotate_for:ident) => { #[kani::proof] - pub fn $nonzero_check_rotate_right_for() { - let int_x: $t = kani::any(); + pub fn $nonzero_check_rotate_for() { + let x: $nonzero_type = kani::any(); let n: u32 = kani::any(); - kani::assume(int_x != 0); - unsafe { - let x = <$nonzero_type>::new_unchecked(int_x); - let result = x.rotate_left(n).rotate_right(n); - assert!(result == x); - } + let result = x.rotate_left(n).rotate_right(n); + assert!(result == x); } }; } - // Use the macro to generate different versions of the function for multiple types - nonzero_check_rotate_left_and_right!(i8, core::num::NonZeroI8, nonzero_check_rotate_for_i8); - nonzero_check_rotate_left_and_right!(i16, core::num::NonZeroI16, nonzero_check_rotate_for_16); - nonzero_check_rotate_left_and_right!(i32, core::num::NonZeroI32, nonzero_check_rotate_for_32); - nonzero_check_rotate_left_and_right!(i64, core::num::NonZeroI64, nonzero_check_rotate_for_64); - nonzero_check_rotate_left_and_right!(i128, core::num::NonZeroI128, nonzero_check_rotate_for_128); - nonzero_check_rotate_left_and_right!(isize, core::num::NonZeroIsize, nonzero_check_rotate_for_isize); - nonzero_check_rotate_left_and_right!(u8, core::num::NonZeroU8, nonzero_check_rotate_for_u8); - nonzero_check_rotate_left_and_right!(u16, core::num::NonZeroU16, nonzero_check_rotate_for_u16); - nonzero_check_rotate_left_and_right!(u32, core::num::NonZeroU32, nonzero_check_rotate_for_u32); - nonzero_check_rotate_left_and_right!(u64, core::num::NonZeroU64, nonzero_check_rotate_for_u64); - nonzero_check_rotate_left_and_right!(u128, core::num::NonZeroU128, nonzero_check_rotate_for_u128); - nonzero_check_rotate_left_and_right!(usize, core::num::NonZeroUsize, nonzero_check_rotate_for_usize); + // 为多种类型生成不同的函数版本 + nonzero_check_rotate_left_and_right!(core::num::NonZeroI8, nonzero_check_rotate_for_i8); + nonzero_check_rotate_left_and_right!(core::num::NonZeroI16, nonzero_check_rotate_for_i16); + nonzero_check_rotate_left_and_right!(core::num::NonZeroI32, nonzero_check_rotate_for_i32); + nonzero_check_rotate_left_and_right!(core::num::NonZeroI64, nonzero_check_rotate_for_i64); + nonzero_check_rotate_left_and_right!(core::num::NonZeroI128, nonzero_check_rotate_for_i128); + nonzero_check_rotate_left_and_right!(core::num::NonZeroIsize, nonzero_check_rotate_for_isize); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU8, nonzero_check_rotate_for_u8); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU16, nonzero_check_rotate_for_u16); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU32, nonzero_check_rotate_for_u32); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU64, nonzero_check_rotate_for_u64); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU128, nonzero_check_rotate_for_u128); + nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize); } From af13803633226120d98d40175384ab2b77b07236 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Wed, 4 Dec 2024 21:30:50 -0500 Subject: [PATCH 7/8] adjust comment language --- library/core/src/num/nonzero.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index cac8a3fe7ca9..e506596cdd54 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2281,7 +2281,7 @@ mod macro_nonzero_check_rotate_left_and_right { }; } - // 为多种类型生成不同的函数版本 + // Use the macro to generate different versions of the function for multiple types nonzero_check_rotate_left_and_right!(core::num::NonZeroI8, nonzero_check_rotate_for_i8); nonzero_check_rotate_left_and_right!(core::num::NonZeroI16, nonzero_check_rotate_for_i16); nonzero_check_rotate_left_and_right!(core::num::NonZeroI32, nonzero_check_rotate_for_i32); From 5860a5c0371a5f5cafe49d32350d7dab2dd4e72a Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 10 Dec 2024 02:15:33 -0500 Subject: [PATCH 8/8] Merge all of these harnesses inside of mod verify --- library/core/src/num/nonzero.rs | 198 +++++++++++++++++++++++++++++++- 1 file changed, 194 insertions(+), 4 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index e506596cdd54..c03021f00970 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2264,11 +2264,201 @@ mod verify { nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); -} -#[cfg(kani)] -mod macro_nonzero_check_rotate_left_and_right { - use super::*; + macro_rules! nonzero_check_cmp { + ($nonzero_type:ty, $nonzero_check_cmp_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_cmp_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + if x < y { + assert!(x.cmp(&y) == core::cmp::Ordering::Less); + } else if x > y { + assert!(x.cmp(&y) == core::cmp::Ordering::Greater); + } else { + assert!(x.cmp(&y) == core::cmp::Ordering::Equal); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_cmp!(core::num::NonZeroI8, nonzero_check_cmp_for_i8); + nonzero_check_cmp!(core::num::NonZeroI16, nonzero_check_cmp_for_i16); + nonzero_check_cmp!(core::num::NonZeroI32, nonzero_check_cmp_for_i32); + nonzero_check_cmp!(core::num::NonZeroI64, nonzero_check_cmp_for_i64); + nonzero_check_cmp!(core::num::NonZeroI128, nonzero_check_cmp_for_i128); + nonzero_check_cmp!(core::num::NonZeroIsize, nonzero_check_cmp_for_isize); + nonzero_check_cmp!(core::num::NonZeroU8, nonzero_check_cmp_for_u8); + nonzero_check_cmp!(core::num::NonZeroU16, nonzero_check_cmp_for_u16); + nonzero_check_cmp!(core::num::NonZeroU32, nonzero_check_cmp_for_u32); + nonzero_check_cmp!(core::num::NonZeroU64, nonzero_check_cmp_for_u64); + nonzero_check_cmp!(core::num::NonZeroU128, nonzero_check_cmp_for_u128); + nonzero_check_cmp!(core::num::NonZeroUsize, nonzero_check_cmp_for_usize); + + + macro_rules! nonzero_check_max { + ($nonzero_type:ty, $nonzero_check_max_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_max_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.max(y); + if x > y { + assert!(result == x); + } else { + assert!(result == y); + } + } + }; + } + + nonzero_check_max!(core::num::NonZeroI8, nonzero_check_max_for_i8); + nonzero_check_max!(core::num::NonZeroI16, nonzero_check_max_for_i16); + nonzero_check_max!(core::num::NonZeroI32, nonzero_check_max_for_i32); + nonzero_check_max!(core::num::NonZeroI64, nonzero_check_max_for_i64); + nonzero_check_max!(core::num::NonZeroI128, nonzero_check_max_for_i128); + nonzero_check_max!(core::num::NonZeroIsize, nonzero_check_max_for_isize); + nonzero_check_max!(core::num::NonZeroU8, nonzero_check_max_for_u8); + nonzero_check_max!(core::num::NonZeroU16, nonzero_check_max_for_u16); + nonzero_check_max!(core::num::NonZeroU32, nonzero_check_max_for_u32); + nonzero_check_max!(core::num::NonZeroU64, nonzero_check_max_for_u64); + nonzero_check_max!(core::num::NonZeroU128, nonzero_check_max_for_u128); + nonzero_check_max!(core::num::NonZeroUsize, nonzero_check_max_for_usize); + + + macro_rules! nonzero_check_min { + ($nonzero_type:ty, $nonzero_check_min_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_min_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.min(y); + if x < y { + assert!(result == x); + } else { + assert!(result == y); + } + } + }; + } + + nonzero_check_min!(core::num::NonZeroI8, nonzero_check_min_for_i8); + nonzero_check_min!(core::num::NonZeroI16, nonzero_check_min_for_i16); + nonzero_check_min!(core::num::NonZeroI32, nonzero_check_min_for_i32); + nonzero_check_min!(core::num::NonZeroI64, nonzero_check_min_for_i64); + nonzero_check_min!(core::num::NonZeroI128, nonzero_check_min_for_i128); + nonzero_check_min!(core::num::NonZeroIsize, nonzero_check_min_for_isize); + nonzero_check_min!(core::num::NonZeroU8, nonzero_check_min_for_u8); + nonzero_check_min!(core::num::NonZeroU16, nonzero_check_min_for_u16); + nonzero_check_min!(core::num::NonZeroU32, nonzero_check_min_for_u32); + nonzero_check_min!(core::num::NonZeroU64, nonzero_check_min_for_u64); + nonzero_check_min!(core::num::NonZeroU128, nonzero_check_min_for_u128); + nonzero_check_min!(core::num::NonZeroUsize, nonzero_check_min_for_usize); + + + macro_rules! nonzero_check_clamp { + ($nonzero_type:ty, $nonzero_check_clamp_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_clamp_for() { + let x: $nonzero_type = kani::any(); + let min: $nonzero_type = kani::any(); + let max: $nonzero_type = kani::any(); + // Ensure min <= max, so the function should no panic + kani::assume(min <= max); + // Use the clamp function and check the result + let result = x.clamp(min, max); + if x < min { + assert!(result == min); + } else if x > max { + assert!(result == max); + } else { + assert!(result == x); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_clamp!(core::num::NonZeroI8, nonzero_check_clamp_for_i8); + nonzero_check_clamp!(core::num::NonZeroI16, nonzero_check_clamp_for_16); + nonzero_check_clamp!(core::num::NonZeroI32, nonzero_check_clamp_for_32); + nonzero_check_clamp!(core::num::NonZeroI64, nonzero_check_clamp_for_64); + nonzero_check_clamp!(core::num::NonZeroI128, nonzero_check_clamp_for_128); + nonzero_check_clamp!(core::num::NonZeroIsize, nonzero_check_clamp_for_isize); + nonzero_check_clamp!(core::num::NonZeroU8, nonzero_check_clamp_for_u8); + nonzero_check_clamp!(core::num::NonZeroU16, nonzero_check_clamp_for_u16); + nonzero_check_clamp!(core::num::NonZeroU32, nonzero_check_clamp_for_u32); + nonzero_check_clamp!(core::num::NonZeroU64, nonzero_check_clamp_for_u64); + nonzero_check_clamp!(core::num::NonZeroU128, nonzero_check_clamp_for_u128); + nonzero_check_clamp!(core::num::NonZeroUsize, nonzero_check_clamp_for_usize); + + + macro_rules! nonzero_check_clamp_panic { + ($nonzero_type:ty, $nonzero_check_clamp_for:ident) => { + #[kani::proof] + #[kani::should_panic] + pub fn $nonzero_check_clamp_for() { + let x: $nonzero_type = kani::any(); + let min: $nonzero_type = kani::any(); + let max: $nonzero_type = kani::any(); + // Ensure min > max, so the function should panic + kani::assume(min > max); + // Use the clamp function and check the result + let result = x.clamp(min, max); + if x < min { + assert!(result == min); + } else if x > max { + assert!(result == max); + } else { + assert!(result == x); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_clamp_panic!(core::num::NonZeroI8, nonzero_check_clamp_panic_for_i8); + nonzero_check_clamp_panic!(core::num::NonZeroI16, nonzero_check_clamp_panic_for_16); + nonzero_check_clamp_panic!(core::num::NonZeroI32, nonzero_check_clamp_panic_for_32); + nonzero_check_clamp_panic!(core::num::NonZeroI64, nonzero_check_clamp_panic_for_64); + nonzero_check_clamp_panic!(core::num::NonZeroI128, nonzero_check_clamp_panic_for_128); + nonzero_check_clamp_panic!(core::num::NonZeroIsize, nonzero_check_clamp_panic_for_isize); + nonzero_check_clamp_panic!(core::num::NonZeroU8, nonzero_check_clamp_panic_for_u8); + nonzero_check_clamp_panic!(core::num::NonZeroU16, nonzero_check_clamp_panic_for_u16); + nonzero_check_clamp_panic!(core::num::NonZeroU32, nonzero_check_clamp_panic_for_u32); + nonzero_check_clamp_panic!(core::num::NonZeroU64, nonzero_check_clamp_panic_for_u64); + nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128); + nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize); + + + macro_rules! nonzero_check_count_ones { + ($nonzero_type:ty, $nonzero_check_count_ones_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_count_ones_for() { + let x: $nonzero_type = kani::any(); + let result = x.count_ones(); + // Since x is non-zero, count_ones should never return 0 + assert!(result.get() > 0); + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_count_ones!(core::num::NonZeroI8, nonzero_check_count_ones_for_i8); + nonzero_check_count_ones!(core::num::NonZeroI16, nonzero_check_count_ones_for_i16); + nonzero_check_count_ones!(core::num::NonZeroI32, nonzero_check_count_ones_for_i32); + nonzero_check_count_ones!(core::num::NonZeroI64, nonzero_check_count_ones_for_i64); + nonzero_check_count_ones!(core::num::NonZeroI128, nonzero_check_count_ones_for_i128); + nonzero_check_count_ones!(core::num::NonZeroIsize, nonzero_check_count_ones_for_isize); + nonzero_check_count_ones!(core::num::NonZeroU8, nonzero_check_count_ones_for_u8); + nonzero_check_count_ones!(core::num::NonZeroU16, nonzero_check_count_ones_for_u16); + nonzero_check_count_ones!(core::num::NonZeroU32, nonzero_check_count_ones_for_u32); + nonzero_check_count_ones!(core::num::NonZeroU64, nonzero_check_count_ones_for_u64); + nonzero_check_count_ones!(core::num::NonZeroU128, nonzero_check_count_ones_for_u128); + nonzero_check_count_ones!(core::num::NonZeroUsize, nonzero_check_count_ones_for_usize); + + macro_rules! nonzero_check_rotate_left_and_right { ($nonzero_type:ty, $nonzero_check_rotate_for:ident) => { #[kani::proof]