Use autoharness for num::nonzero::NonZero::<*>::count_ones

Author: tautschnig

.github/workflows/kani.yml

@@ -137,6 +137,18 @@ jobs:
             --include-pattern "num::<impl u64>::wrapping_sh" \
             --include-pattern "num::<impl u128>::wrapping_sh" \
             --include-pattern "num::<impl usize>::wrapping_sh" \
+            --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i64>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i128>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<isize>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u8>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u16>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u32>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u64>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u128>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<usize>::count_ones" \
             --include-pattern ptr::align_offset::mod_inv \
             --include-pattern ptr::alignment::Alignment::as_nonzero \
             --include-pattern ptr::alignment::Alignment::as_usize \

library/core/src/num/nonzero.rs

@@ -721,6 +721,7 @@ macro_rules! nonzero_integer {
             #[must_use = "this returns the result of the operation, \
                         without modifying the original"]
             #[inline(always)]
+            #[ensures(|result| result.get() > 0)]
             pub const fn count_ones(self) -> NonZero<u32> {
                 // SAFETY:
                 // `self` is non-zero, which means it has at least one bit set, which means
@@ -2572,32 +2573,6 @@ mod verify {
     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]