support Result based on Chris's suggestion

Author: tjhance

source/pervasive/std_specs/control_flow.rs

@@ -47,19 +47,26 @@ pub fn ex_option_from_residual<T>(option: Option<Infallible>) -> (option2: Optio
     Option::from_residual(option)
 }
 
+pub spec fn spec_from<S, T>(value: T, ret: S) -> bool;
 
+#[verifier::broadcast_forall]
+#[verifier::external_body]
+pub proof fn spec_from_blanket_identity<T>(t: T, s: T)
+    ensures
+        spec_from::<T, T>(t, s) ==> t == s
+{
+}
 
-/*#[verifier::external_fn_specification]
-pub fn ex_result_from_residual<T, E>(result: Result<Convert::Infallible, E>)
-      -> (cf: ControlFlow<<Result<T, E> as Try>::Residual, <Result<T, E> as Try>::Output>)
+#[verifier::external_fn_specification]
+pub fn ex_result_from_residual<T, E, F: From<E>>(result: Result<Infallible, E>)
+      -> (result2: Result<T, F>)
     ensures
-        cf === match result {
-            Ok(v) => ControlFlow::Continue(v),
-            Err(e) => ControlFlow::Break(Err(e)),
+        match (result, result2) {
+            (Err(e), Err(e2)) => spec_from::<F, E>(e, e2),
+            _ => false,
         },
 {
-    result.branch()
-}*/
-
+    Result::from_residual(result)
+}
 
 }

source/rust_verify_test/tests/std.rs

@@ -240,3 +240,48 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_fails(err, 2)
 }
+
+test_verify_one_file! {
+    #[test] question_mark_result verus_code! {
+        use vstd::*;
+
+        fn test() -> (res: Result<u32, bool>)
+            ensures res === Err(false),
+        {
+            let x: Result<u8, bool> = Err(false);
+            let y = x?;
+
+            assert(false);
+            return Err(true);
+        }
+
+        fn test2() -> (res: Result<u32, bool>)
+        {
+            let x: Result<u8, bool> = Ok(5);
+            let y = x?;
+
+            assert(false); // FAILS
+            return Err(false);
+        }
+
+        fn test3() -> (res: Result<u32, bool>)
+            ensures res.is_ok(),
+        {
+            let x: Result<u8, bool> = Err(false);
+            let y = x?; // FAILS
+
+            return Ok(13);
+        }
+
+        fn test4() -> (res: Result<u32, bool>)
+            ensures false,
+        {
+            let x: Result<u8, bool> = Ok(12);
+            let y = x?;
+
+            assert(y == 12);
+
+            loop { }
+        }
+    } => Err(err) => assert_fails(err, 2)
+}