Merge branch 'verus-lang:main' into main

source/docs/publications-and-projects/_projects/hance-thesis.md

@@ -0,0 +1,10 @@
+---
+title: "Verifying Concurrent Systems Code"
+authors: "Travis Hance"
+venue: "PhD Thesis, Carnegie Mellon University"
+date: 2024-08-07
+type: internal
+category: "Language and Verification"
+pdf: https://www.andrew.cmu.edu/user/bparno/papers/hance_thesis.pdf
+---
+

source/docs/publications-and-projects/_projects/vest.md

@@ -0,0 +1,7 @@
+---
+title: "Vest: Verified Parsers and Serializers"
+date: 2024-09-01
+type: project
+code: https://github.com/secure-foundations/vest
+---
+High-assurance and performant parsing and serialization of binary data formats.

source/docs/state_machines/src/intro.md

@@ -44,3 +44,7 @@ This guide expects general familiarity with Verus, so readers unfamiliar with Ve
 should check out the general [Verus user guide](https://verus-lang.github.io/verus/guide/)
 first and become proficient at coding within its `spec`, `proof`, and `exec` modes,
 using `ghost` and `exec` variables.
+
+### Further Reading
+
+For a fully comprehensive account, please see [Verifying Concurrent Systems Code](https://www.andrew.cmu.edu/user/bparno/papers/hance_thesis.pdf).

source/rust_verify/src/verifier.rs

@@ -1878,7 +1878,9 @@ impl Verifier {
                 None,
                 Some(bucket_id.module().clone()),
                 bucket_id.function(),
+                true,
             );
+        let mono_abstract_datatypes = mono_abstract_datatypes.unwrap();
         let module = pruned_krate
             .modules
             .iter()
@@ -2629,6 +2631,7 @@ impl Verifier {
             Some(&current_vir_crate),
             None,
             None,
+            false,
         );
         let vir_crate =
             vir::traits::merge_external_traits(vir_crate).map_err(map_err_diagnostics)?;

source/rust_verify_test/tests/consts.rs

@@ -60,7 +60,7 @@ test_verify_one_file! {
     #[test] test1_fails5 verus_code! {
         fn f() -> u64 { 1 }
         const S: u64 = 1 + f();
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode exec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::f` with mode exec")
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/exec_closures.rs

@@ -582,7 +582,7 @@ test_verify_one_file_with_options! {
             {
             };
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode exec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `test_crate::some_exec_fn` with mode exec")
 }
 
 test_verify_one_file_with_options! {
@@ -597,7 +597,7 @@ test_verify_one_file_with_options! {
             {
             };
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode exec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `test_crate::some_exec_fn` with mode exec")
 }
 
 test_verify_one_file_with_options! {
@@ -611,7 +611,7 @@ test_verify_one_file_with_options! {
                 some_spec_fn()
             };
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode spec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `test_crate::some_spec_fn` with mode spec")
 }
 
 test_verify_one_file_with_options! {
@@ -625,7 +625,7 @@ test_verify_one_file_with_options! {
                 return some_spec_fn();
             };
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode spec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `test_crate::some_spec_fn` with mode spec")
 }
 
 test_verify_one_file_with_options! {

source/rust_verify_test/tests/lifetime.rs

@@ -102,7 +102,7 @@ test_verify_one_file! {
         proof fn h<A>(tracked a: A) {
             g(f(a), f(a))
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode proof")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::f` with mode proof")
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/modes.rs

@@ -155,7 +155,7 @@ test_verify_one_file! {
         fn test(s: Ghost<S>) -> bool {
             s@.get_j()
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode spec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::S::get_j` with mode spec")
 }
 
 test_verify_one_file! {
@@ -172,7 +172,7 @@ test_verify_one_file! {
         fn test(s: &Ghost<S>) -> bool {
             s@.get_j()
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode spec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::S::get_j` with mode spec")
 }
 
 test_verify_one_file! {
@@ -189,7 +189,7 @@ test_verify_one_file! {
         fn test(s: Ghost<&S>) -> bool {
             s@.get_j()
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode spec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::S::get_j` with mode spec")
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/open_invariant.rs

@@ -168,7 +168,7 @@ test_both! {
           open_atomic_invariant_in_proof!(credit => &i => inner => {
           });
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode proof")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `vstd::invariant::spend_open_invariant_credit_in_proof` with mode proof")
 }
 
 test_both! {
@@ -552,7 +552,7 @@ test_verify_one_file! {
             opens_invariants [ exec_int_fn() ]
         {
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode exec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::exec_int_fn` with mode exec")
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/regression.rs

@@ -278,7 +278,7 @@ test_verify_one_file! {
             let lock = opt_lock.get_SomeX_0();   // This line triggers panic
             true
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode spec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::OptionX::get_SomeX_0` with mode spec")
 }
 
 test_verify_one_file! {
@@ -1271,3 +1271,15 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] slice_of_tuple_issue1259 verus_code! {
+        use vstd::*;
+        pub fn run(val: &[(u32, u32)]) -> u64
+            requires
+                val.len() > 0,
+        {
+            val[0].0 as u64 + val[0].1 as u64
+        }
+    } => Ok(())
+}

source/rust_verify_test/tests/unwind.rs

@@ -399,7 +399,7 @@ test_verify_one_file! {
             no_unwind when some_exec_fn(j)
         {
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode exec")
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::some_exec_fn` with mode exec")
 }
 
 test_verify_one_file! {

source/vir/src/ast_to_sst_crate.rs

@@ -62,6 +62,7 @@ pub fn ast_to_sst_krate(
         traits: krate.traits.clone(),
         trait_impls: krate.trait_impls.clone(),
         assoc_type_impls: krate.assoc_type_impls.clone(),
+        reveal_groups: krate.reveal_groups.clone(),
     });
     Ok(krate_sst)
 }

source/vir/src/modes.rs

@@ -827,7 +827,8 @@ fn check_expr_handle_mut_arg(
                 if ctxt.special_paths.is_exec_nonstatic_call_path(&x.path) {
                     format!("to call a non-static function in ghost code, it must be a spec_fn")
                 } else {
-                    format!("cannot call function with mode {}", function.x.mode)
+                    let name = crate::ast_util::path_as_friendly_rust_name(&x.path);
+                    format!("cannot call function `{}` with mode {}", name, function.x.mode)
                 }
             };
             if ctxt.check_ghost_blocks {

source/vir/src/prune.rs

@@ -95,7 +95,7 @@ struct State {
     worklist_trait_impls: Vec<ImplName>,
     worklist_assoc_type_decls: Vec<(Path, Ident)>,
     worklist_assoc_type_impls: Vec<AssocTypeGroup>,
-    mono_abstract_datatypes: HashSet<MonoTyp>,
+    mono_abstract_datatypes: Option<HashSet<MonoTyp>>,
     spec_fn_types: HashSet<usize>,
     uses_array: bool,
     fndef_types: HashSet<Fun>,
@@ -135,12 +135,14 @@ fn record_datatype(ctxt: &Ctxt, state: &mut State, typ: &Typ, path: &Path) {
     } else {
         return;
     };
-    if let Some(d) = ctxt.datatype_map.get(path) {
-        let is_vis = is_visible_to(&d.x.visibility, module);
-        let is_transparent = is_datatype_transparent(module, &d);
-        if is_vis && !is_transparent {
-            if let Some(monotyp) = crate::poly::typ_as_mono(typ) {
-                state.mono_abstract_datatypes.insert(monotyp);
+    if let Some(mono_abstract_datatypes) = &mut state.mono_abstract_datatypes {
+        if let Some(d) = ctxt.datatype_map.get(path) {
+            let is_vis = is_visible_to(&d.x.visibility, module);
+            let is_transparent = is_datatype_transparent(module, &d);
+            if is_vis && !is_transparent {
+                if let Some(monotyp) = crate::poly::typ_as_mono(typ) {
+                    mono_abstract_datatypes.insert(monotyp);
+                }
             }
         }
     }
@@ -315,8 +317,10 @@ fn traverse_typ(ctxt: &Ctxt, state: &mut State, t: &Typ) {
     match &**t {
         TypX::Datatype(path, _, _) => record_datatype(ctxt, state, t, path),
         TypX::Primitive(_, _) => {
-            if let Some(monotyp) = crate::poly::typ_as_mono(t) {
-                state.mono_abstract_datatypes.insert(monotyp);
+            if let Some(mono_abstract_datatypes) = &mut state.mono_abstract_datatypes {
+                if let Some(monotyp) = crate::poly::typ_as_mono(t) {
+                    mono_abstract_datatypes.insert(monotyp);
+                }
             }
         }
         _ => {}
@@ -659,16 +663,20 @@ fn collect_broadcast_triggers(f: &Function) -> Vec<(Vec<Fun>, Vec<ReachedType>)>
     trigs
 }
 
-// module is none: prune to keep what's reachable from current_crate
-// module is some and fun is none: prune to keep what's reachable from module
-// module is some and fun is some: prune to keep what's reachable from fun
+//  - module is none: prune to keep what's reachable from current_crate
+//    module is some and fun is none: prune to keep what's reachable from module
+//    module is some and fun is some: prune to keep what's reachable from fun
+//  - collect_monotyps: if true, return a Vec<MonoTyp>; otherwise, return None
+//    this should only be done post-simplification
+
 pub fn prune_krate_for_module_or_krate(
     krate: &Krate,
     crate_name: &Ident,
     current_crate: Option<&Krate>,
     module: Option<Path>,
     fun: Option<&Fun>,
-) -> (Krate, Vec<MonoTyp>, Vec<usize>, bool, Vec<Fun>) {
+    collect_monotyps: bool,
+) -> (Krate, Option<Vec<MonoTyp>>, Vec<usize>, bool, Vec<Fun>) {
     assert!(module.is_some() != current_crate.is_some());
 
     let mut root_modules: HashSet<Path> = HashSet::new();
@@ -701,6 +709,9 @@ pub fn prune_krate_for_module_or_krate(
     let is_root_function = |function: &Function| root_functions.contains(&function.x.name);
 
     let mut state: State = Default::default();
+    if collect_monotyps {
+        state.mono_abstract_datatypes = Some(HashSet::new());
+    }
     if let Some(current_crate) = current_crate {
         // Make sure we keep all of current_crate,
         // so that all of current_crate is sent to the well-formedness checks.
@@ -1089,8 +1100,13 @@ pub fn prune_krate_for_module_or_krate(
     spec_fn_types.sort();
     let mut fndef_types: Vec<Fun> = state.fndef_types.into_iter().collect();
     fndef_types.sort();
-    let mut mono_abstract_datatypes: Vec<MonoTyp> =
-        state.mono_abstract_datatypes.into_iter().collect();
-    mono_abstract_datatypes.sort();
+    let mono_abstract_datatypes = match state.mono_abstract_datatypes {
+        Some(mono) => {
+            let mut mono: Vec<MonoTyp> = mono.into_iter().collect();
+            mono.sort();
+            Some(mono)
+        }
+        _ => None,
+    };
     (Arc::new(kratex), mono_abstract_datatypes, spec_fn_types, state.uses_array, fndef_types)
 }

source/vir/src/sst.rs

@@ -313,4 +313,5 @@ pub struct KrateSstX {
     pub traits: Vec<crate::ast::Trait>,
     pub trait_impls: Vec<crate::ast::TraitImpl>,
     pub assoc_type_impls: Vec<crate::ast::AssocTypeImpl>,
+    pub reveal_groups: Vec<crate::ast::RevealGroup>,
 }