Revert "Use autoharness for num::<impl *>::unchecked_{add,sub}"

This reverts commit 153f5d1.

Author: tautschnig

.github/workflows/kani.yml

@@ -82,18 +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_add" \
-            --include-pattern "num::<impl i16>::unchecked_add" \
-            --include-pattern "num::<impl i32>::unchecked_add" \
-            --include-pattern "num::<impl i64>::unchecked_add" \
-            --include-pattern "num::<impl i128>::unchecked_add" \
-            --include-pattern "num::<impl isize>::unchecked_add" \
-            --include-pattern "num::<impl u8>::unchecked_add" \
-            --include-pattern "num::<impl u16>::unchecked_add" \
-            --include-pattern "num::<impl u32>::unchecked_add" \
-            --include-pattern "num::<impl u64>::unchecked_add" \
-            --include-pattern "num::<impl u128>::unchecked_add" \
-            --include-pattern "num::<impl usize>::unchecked_add" \
             --include-pattern "num::<impl i8>::unchecked_neg" \
             --include-pattern "num::<impl i16>::unchecked_neg" \
             --include-pattern "num::<impl i32>::unchecked_neg" \
@@ -112,18 +100,6 @@ jobs:
             --include-pattern "num::<impl u64>::unchecked_sh" \
             --include-pattern "num::<impl u128>::unchecked_sh" \
             --include-pattern "num::<impl usize>::unchecked_sh" \
-            --include-pattern "num::<impl i8>::unchecked_sub" \
-            --include-pattern "num::<impl i16>::unchecked_sub" \
-            --include-pattern "num::<impl i32>::unchecked_sub" \
-            --include-pattern "num::<impl i64>::unchecked_sub" \
-            --include-pattern "num::<impl i128>::unchecked_sub" \
-            --include-pattern "num::<impl isize>::unchecked_sub" \
-            --include-pattern "num::<impl u8>::unchecked_sub" \
-            --include-pattern "num::<impl u16>::unchecked_sub" \
-            --include-pattern "num::<impl u32>::unchecked_sub" \
-            --include-pattern "num::<impl u64>::unchecked_sub" \
-            --include-pattern "num::<impl u128>::unchecked_sub" \
-            --include-pattern "num::<impl usize>::unchecked_sub" \
             --include-pattern "num::<impl i8>::wrapping_sh" \
             --include-pattern "num::<impl i16>::wrapping_sh" \
             --include-pattern "num::<impl i32>::wrapping_sh" \

library/core/src/num/mod.rs

@@ -1739,6 +1739,30 @@ mod verify {
         }
     }
 
+    // `unchecked_add` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // Preconditions: No overflow should occur
+    // #[requires(!self.overflowing_add(rhs).1)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
+    generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
+    generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16);
+    generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32);
+    generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64);
+    generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128);
+    generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize);
+    generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8);
+    generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16);
+    generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32);
+    generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
+    generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
+    generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
+
     // `unchecked_mul` proofs
     //
     // Target types:
@@ -1896,6 +1920,32 @@ mod verify {
         usize::MAX
     );
 
+    // `unchecked_sub` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // Preconditions: No overflow should occur
+    // #[requires(!self.overflowing_sub(rhs).1)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_sub(self, rhs: Self)  -> Self
+    //
+    // This function performs an unchecked subtraction operation.
+    generate_unchecked_math_harness!(i8, unchecked_sub, checked_unchecked_sub_i8);
+    generate_unchecked_math_harness!(i16, unchecked_sub, checked_unchecked_sub_i16);
+    generate_unchecked_math_harness!(i32, unchecked_sub, checked_unchecked_sub_i32);
+    generate_unchecked_math_harness!(i64, unchecked_sub, checked_unchecked_sub_i64);
+    generate_unchecked_math_harness!(i128, unchecked_sub, checked_unchecked_sub_i128);
+    generate_unchecked_math_harness!(isize, unchecked_sub, checked_unchecked_sub_isize);
+    generate_unchecked_math_harness!(u8, unchecked_sub, checked_unchecked_sub_u8);
+    generate_unchecked_math_harness!(u16, unchecked_sub, checked_unchecked_sub_u16);
+    generate_unchecked_math_harness!(u32, unchecked_sub, checked_unchecked_sub_u32);
+    generate_unchecked_math_harness!(u64, unchecked_sub, checked_unchecked_sub_u64);
+    generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128);
+    generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize);
+
     // Part_2 `carrying_mul` proofs
     //
     // ====================== u8 Harnesses ======================