vstd: unsigned wrapping_mul spec (#1829)

* vstd: add wrapping mul spec

* unsigned_wrapping_mul test

Author: mmcloughlin

source/rust_verify_test/tests/std.rs

@@ -177,6 +177,23 @@ test_verify_one_file! {
     } => Err(err) => assert_vir_error_msg(err, "index for &mut not supported")
 }
 
+test_verify_one_file! {
+    #[test] unsigned_wrapping_mul verus_code! {
+        use vstd::*;
+
+        fn test() {
+            let i = 255u16.wrapping_mul(253);
+            assert(i == 64515);
+
+            let i = 256u16.wrapping_mul(256);
+            assert(i == 0);
+
+            let i = 257u16.wrapping_mul(259);
+            assert(i == 1027);
+        }
+    } => Ok(())
+}
+
 test_verify_one_file! {
     #[test] signed_wrapping_mul verus_code! {
         use vstd::*;

source/vstd/std_specs/num.rs

@@ -107,6 +107,10 @@ macro_rules! num_specs {
                     }
                 );
 
+            #[verifier::allow_in_spec]
+            pub assume_specification[<$uN>::wrapping_mul](x: $uN, y: $uN) -> $uN
+                returns ((x as nat * y as nat) % $range as nat) as $uN;
+
             #[verifier::allow_in_spec]
             pub assume_specification[<$uN>::checked_add](x: $uN, y: $uN) -> Option<$uN>
                 returns (