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

This reverts commit e7b0dc4.

Author: tautschnig

.github/workflows/kani.yml

@@ -82,12 +82,6 @@ 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,6 +1651,19 @@ 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,
@@ -1763,6 +1776,23 @@ 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: