vstd: finish proving lemmas for Seq (#2669)

Author: bsdinis

source/rust_verify_test/tests/mut_refs_patterns.rs

@@ -2374,7 +2374,7 @@ test_verify_one_file_with_options! {
                 }
             }
         }
-    } => Err(err) => assert_vir_error_msg(err, "a 'mut ref' binding in a pattern is only allowed for exec mode")
+    } => Err(err) => assert_vir_error_msg(err, "a 'mut ref' binding in a pattern is not allowed in spec mode")
 }
 
 test_verify_one_file_with_options! {
@@ -2393,7 +2393,7 @@ test_verify_one_file_with_options! {
                 }
             }
         }
-    } => Err(err) => assert_vir_error_msg(err, "a 'mut ref' binding in a pattern is only allowed for exec mode")
+    } => Err(err) => assert_vir_error_msg(err, "a 'mut ref' binding in a pattern is not allowed in spec mode")
 }
 
 test_verify_one_file_with_options! {
@@ -2402,13 +2402,13 @@ test_verify_one_file_with_options! {
             tracked a: u64
         }
 
-        proof fn test(tracked x: X) {
+        proof fn test(tracked mut x: X) {
             match x {
                 X { a: ref mut y } => {
                 }
             }
         }
-    } => Err(err) => assert_vir_error_msg(err, "a 'mut ref' binding in a pattern is only allowed for exec mode")
+    } => Ok(())
 }
 
 test_verify_one_file_with_options! {
@@ -2421,13 +2421,13 @@ test_verify_one_file_with_options! {
             tracked x: X
         }
 
-        proof fn test(tracked y: Y) {
+        proof fn test(tracked mut y: Y) {
             match y {
                 Y { x: ref mut x0 @ X { a: _ } } => {
                 }
             }
         }
-    } => Err(err) => assert_vir_error_msg(err, "a 'mut ref' binding in a pattern is only allowed for exec mode")
+    } => Ok(())
 }
 
 test_verify_one_file_with_options! {
@@ -2464,7 +2464,7 @@ test_verify_one_file_with_options! {
                 Opt::None => { }
             }
         }
-    } => Err(err) => assert_vir_error_msg(err, "a 'mut ref' binding in a pattern is only allowed for exec mode")
+    } => Err(err) => assert_vir_error_msg(err, "a 'mut ref' binding in a pattern is not allowed in spec mode")
 }
 
 test_verify_one_file_with_options! {

source/vir/src/modes.rs

@@ -1026,12 +1026,11 @@ fn add_pattern_rec(
 
 fn check_binding(span: &Span, by_ref: &ByRef, mode: Mode) -> Result<(), VirErr> {
     match (by_ref, mode) {
-        (ByRef::MutRef, Mode::Spec | Mode::Proof) => {
-            // Supporting this for Mode::Proof would be nice but requires thought for how
-            // to implement.
-            Err(error(span, "a 'mut ref' binding in a pattern is only allowed for exec mode"))
+        (ByRef::MutRef, Mode::Spec) => {
+            Err(error(span, "a 'mut ref' binding in a pattern is not allowed in spec mode"))
         }
         (ByRef::No | ByRef::ImmutRef, _) => Ok(()),
+        (_, Mode::Proof) => Ok(()),
         (_, Mode::Exec) => Ok(()),
     }
 }