Use autoharness for num::<impl i*>::unchecked_neg

Author: tautschnig

.github/workflows/kani.yml

@@ -82,6 +82,12 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern "num::<impl i8>::unchecked_neg" \
+            --include-pattern "num::<impl i16>::unchecked_neg" \
+            --include-pattern "num::<impl i32>::unchecked_neg" \
+            --include-pattern "num::<impl i64>::unchecked_neg" \
+            --include-pattern "num::<impl i128>::unchecked_neg" \
+            --include-pattern "num::<impl isize>::unchecked_neg" \
             --include-pattern "num::<impl i8>::unchecked_sh" \
             --include-pattern "num::<impl i16>::unchecked_sh" \
             --include-pattern "num::<impl i32>::unchecked_sh" \

library/core/src/num/mod.rs

@@ -1651,19 +1651,6 @@ mod verify {
         }
     }
 
-    macro_rules! generate_unchecked_neg_harness {
-        ($type:ty, $harness_name:ident) => {
-            #[kani::proof_for_contract($type::unchecked_neg)]
-            pub fn $harness_name() {
-                let num1: $type = kani::any::<$type>();
-
-                unsafe {
-                    num1.unchecked_neg();
-                }
-            }
-        };
-    }
-
     /// A macro to generate Kani proof harnesses for the `carrying_mul` method,
     ///
     /// The macro creates multiple harnesses for different ranges of input values,
@@ -1776,23 +1763,6 @@ mod verify {
     generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
     generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
 
-    // `unchecked_neg` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} -- 6 types in total
-    //
-    // Target contracts:
-    // #[requires(self != $SelfT::MIN)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_neg(self) -> Self
-    generate_unchecked_neg_harness!(i8, checked_unchecked_neg_i8);
-    generate_unchecked_neg_harness!(i16, checked_unchecked_neg_i16);
-    generate_unchecked_neg_harness!(i32, checked_unchecked_neg_i32);
-    generate_unchecked_neg_harness!(i64, checked_unchecked_neg_i64);
-    generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128);
-    generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize);
-
     // `unchecked_mul` proofs
     //
     // Target types: