From 32e0cf93f01e227bbd66811cdbe1bd0e26e8a0a0 Mon Sep 17 00:00:00 2001
From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com>
Date: Tue, 8 Oct 2024 09:47:17 -0700
Subject: [PATCH] Contracts and Harnesses for `unchecked_neg` (#102)

Towards #59

### Changes
* Added contracts for `unchecked_neg` (located in
`library/core/src/num/int_macros.rs`)
* Added a harness for `unchecked_neg` of each signed integer type
  * `i8`, `i16`, `i32`, `i64`, `i128`, `isize` --- 6 harnesses in total.
* Fixed comments.

### Revalidation
1. Per the discussion in #59, we have to **build and run Kani from
`feature/verify-rust-std` branch**.
2. To revalidate the verification results, run the following command.
`<harness_to_run>` can be either `num::verify` to run all harnesses or
`num::verify::<harness_name>` (e.g. `check_unchecked_neg_i8`) to run a
specific harness.
```
kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates
```

All default harnesses should pass.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: yew005 <yew005@ucsd.edu>
Co-authored-by: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com>
Co-authored-by: rajathmCMU <rajathkotyal@gmail.com>
---
 library/core/src/num/int_macros.rs |  2 ++
 library/core/src/num/mod.rs        | 37 ++++++++++++++++++++++--------
 2 files changed, 30 insertions(+), 9 deletions(-)

diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index cf04b9fcbb707..c84087172974a 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -1167,6 +1167,8 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_neg", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(self != $SelfT::MIN)]
+        #[ensures(|result| *result == -self)]
         pub const unsafe fn unchecked_neg(self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 1668adca30905..e8b7130995831 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -5,7 +5,7 @@
 use crate::str::FromStr;
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{ascii, intrinsics, mem};
-use safety::requires;
+use safety::{requires, ensures};
 
 #[cfg(kani)]
 use crate::kani;
@@ -1661,11 +1661,11 @@ mod verify {
     // `unchecked_add` proofs
     //
     // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
     //
     // Target contracts:
-    //#[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
-    //#[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)] // Postconditions: Result must be within valid bounds
+    // Preconditions: No overflow should occur
+    // #[requires(!self.overflowing_add(rhs).1)]
     //
     // Target function:
     // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
@@ -1682,12 +1682,31 @@ 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:
-    // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 36 types in total
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total, with different interval checks for each.
+    // Total types of checks including intervals -- 36
     //
     // Target contracts:
+    // Preconditions: No overflow should occur
     // #[requires(!self.overflowing_mul(rhs).1)]
     //
     // Target function:
@@ -1783,11 +1802,10 @@ mod verify {
     // `unchecked_shl` proofs
     //
     // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 12 types in total
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
     //
     // Target contracts:
     // #[requires(shift < Self::BITS)]
-    // #[ensures(|ret| *ret == self << shift)]
     //
     // Target function:
     // pub const unsafe fn unchecked_shl(self, shift: u32) -> Self
@@ -1809,10 +1827,11 @@ mod verify {
     // `unchecked_sub` proofs
     //
     // Target types:
-    // i{8,16,32,64,128} and u{8,16,32,64,128} -- 12 types in total
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
     //
     // Target contracts:
-    // #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
+    // Preconditions: No overflow should occur
+    // #[requires(!self.overflowing_sub(rhs).1)] 
     //
     // Target function:
     // pub const unsafe fn unchecked_sub(self, rhs: Self)  -> Self