add no_unwind to vec index and vec len (#1613)

Author: tjhance

source/rust_verify_test/tests/std.rs

@@ -573,3 +573,19 @@ test_verify_one_file_with_options! {
         }
     } => Err(err) => assert_vir_error_msg(err, "cannot use function `crate::X::clone` which is ignored")
 }
+
+test_verify_one_file! {
+    #[test] vec_index_nounwind verus_code! {
+        use vstd::*;
+
+        fn test(v: Vec<u64>)
+            requires v.len() > 5,
+            no_unwind
+        {
+            let x = v[0];
+            let mut v = v;
+            v[1] = 4;
+            let l = v.len();
+        }
+    } => Ok(())
+}

source/vir/src/sst_to_air.rs

@@ -1683,13 +1683,13 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result<Vec<Stmt>, Vi
                     UnwindAir::NoUnwind(ReasonForNoUnwind::Function) => error_with_label(
                         &stm.span,
                         "cannot show this call will not unwind, in function marked 'no_unwind'",
-                        "this call might unwind",
+                        format!("call to {:} might unwind", fun_as_friendly_rust_name(fun)),
                     ),
                     UnwindAir::NoUnwind(ReasonForNoUnwind::OpenInvariant(span)) => {
                         error_with_label(
                             &stm.span,
                             "cannot show this call will not unwind",
-                            "this call might unwind",
+                            format!("call to {:} might unwind", fun_as_friendly_rust_name(fun)),
                         )
                         .secondary_label(span, "unwinding is not allowed in this invariant block")
                     }

source/vstd/std_specs/core.rs

@@ -1,6 +1,7 @@
 use super::super::prelude::*;
 
-verus! {
+use verus as verus_;
+verus_! {
 
 #[verifier::external_trait_specification]
 pub trait ExIndex<Idx> where Idx: ?Sized {
@@ -216,6 +217,7 @@ pub fn index_set<T, Idx, E>(container: &mut T, index: Idx, val: E) where
         old(container).spec_index_set_requires(index),
     ensures
         old(container).spec_index_set_ensures(container, index, val),
+    no_unwind
 {
     container[index] = val;
 }

source/vstd/std_specs/vec.rs

@@ -7,7 +7,8 @@ use core::clone::Clone;
 use core::option::Option;
 use core::option::Option::None;
 
-verus! {
+use verus as verus_;
+verus_! {
 
 #[verifier::external_type_specification]
 #[verifier::external_body]
@@ -46,6 +47,7 @@ pub fn vec_index<T, A: Allocator>(vec: &Vec<T, A>, i: usize) -> (element: &T)
         i < vec.view().len(),
     ensures
         *element == vec.view().index(i as int),
+    no_unwind
 {
     &vec[i]
 }
@@ -66,6 +68,7 @@ pub broadcast proof fn axiom_spec_len<A>(v: &Vec<A>)
 pub assume_specification<T, A: Allocator>[ Vec::<T, A>::len ](vec: &Vec<T, A>) -> usize
     returns
         spec_vec_len(vec),
+    no_unwind
 ;
 
 ////// Other functions