From dc862c476a98e078324999c8aa51f2ec4b6f4e1b Mon Sep 17 00:00:00 2001
From: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com>
Date: Mon, 14 Oct 2024 16:14:42 -0700
Subject: [PATCH] Contracts & Harnesses for widening_mul (#111)

Towards : issue #59

Parent branch : main

Revalidation :
Per the discussion in
https://github.com/model-checking/verify-rust-std/issues/59, we have to
build and run Kani from feature/verify-rust-std branch.
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. widening_mul_u16_small) to run a
specific harness.
```
kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates
```
---
 library/core/src/num/mod.rs | 56 +++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index e8b7130995831..91c1ccb708613 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1658,6 +1658,35 @@ mod verify {
         }
     }
 
+    // Part 2 : Nested unsafe functions Generation Macros --> https://github.com/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md
+
+    // Verify `widening_mul`, which internally uses `unchecked_mul`
+    macro_rules! generate_widening_mul_intervals {
+        ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
+            $(
+                #[kani::proof]
+                pub fn $harness_name() {
+                    let lhs: $type = kani::any::<$type>();
+                    let rhs: $type = kani::any::<$type>();
+
+                    kani::assume(lhs >= $min && lhs <= $max);
+                    kani::assume(rhs >= $min && rhs <= $max);
+
+                    let (result_low, result_high) = lhs.widening_mul(rhs);
+
+                    // Compute expected result using wider type
+                    let expected = (lhs as $wide_type) * (rhs as $wide_type);
+
+                    let expected_low = expected as $type;
+                    let expected_high = (expected >> <$type>::BITS) as $type;
+
+                    assert_eq!(result_low, expected_low);
+                    assert_eq!(result_high, expected_high);
+                }
+            )+
+        }
+    }
+
     // `unchecked_add` proofs
     //
     // Target types:
@@ -1849,4 +1878,31 @@ mod verify {
     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 : Proof harnesses 
+    
+    // ====================== u8 Harnesses ======================
+    generate_widening_mul_intervals!(u8, u16, widening_mul_u8, 0u8, u8::MAX);
+    
+    // ====================== u16 Harnesses ======================
+    generate_widening_mul_intervals!(u16, u32,
+        widening_mul_u16_small, 0u16, 10u16,
+        widening_mul_u16_large, u16::MAX - 10u16, u16::MAX,
+        widening_mul_u16_mid_edge, (u16::MAX / 2) - 10u16, (u16::MAX / 2) + 10u16
+    );
+
+    // ====================== u32 Harnesses ======================
+    generate_widening_mul_intervals!(u32, u64,
+        widening_mul_u32_small, 0u32, 10u32,
+        widening_mul_u32_large, u32::MAX - 10u32, u32::MAX,
+        widening_mul_u32_mid_edge, (u32::MAX / 2) - 10u32, (u32::MAX / 2) + 10u32
+    );
+
+    // ====================== u64 Harnesses ======================
+    generate_widening_mul_intervals!(u64, u128,
+        widening_mul_u64_small, 0u64, 10u64,
+        widening_mul_u64_large, u64::MAX - 10u64, u64::MAX,
+        widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64
+    );
 }