Add spec for unsigned saturating_mul (#2809)

Author: HertelP

source/rust_verify_test/tests/std.rs

@@ -182,6 +182,23 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    #[test] unsigned_saturating_mul verus_code! {
+        use vstd::*;
+
+        fn test() {
+            let i = 10u64.saturating_mul(20);
+            assert(i == 200);
+
+            let i = 0u64.saturating_mul(u64::MAX);
+            assert(i == 0);
+
+            let i = u64::MAX.saturating_mul(2);
+            assert(i == u64::MAX);
+        }
+    } => Ok(())
+}
+
 test_verify_one_file! {
     #[test] signed_wrapping_mul verus_code! {
         use vstd::*;

source/vstd/std_specs/num.rs

@@ -259,6 +259,17 @@ macro_rules! num_specs {
                     }
                 );
 
+            #[verifier::allow_in_spec]
+            #[cfg(not(verus_verify_core))]
+            pub assume_specification[<$uN>::saturating_mul](x: $uN, y: $uN) -> $uN
+                returns (
+                    if x * y > <$uN>::MAX {
+                        <$uN>::MAX
+                    } else {
+                        (x * y) as $uN
+                    }
+                );
+
             #[verifier::allow_in_spec]
             #[cfg(not(verus_verify_core))]
             pub assume_specification[<$uN>::is_multiple_of](x: $uN, y: $uN) -> bool