a broadcast group member should be a broadcasted proof fn, fixes #1355

source/rust_verify_test/tests/broadcast_forall.rs

@@ -611,3 +611,19 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] broadcast_group_should_check_member_is_broadcast_regression_1355 verus_code! {
+        proof fn lemma_foo()
+            ensures true
+        {}
+
+        broadcast group group_foo {
+            lemma_foo,
+        }
+
+        proof fn lemma_bar() {
+            broadcast use group_foo;
+        }
+    } => Err(err) => assert_vir_error_msg(err, "lemma_foo is not a broadcast proof fn")
+}

source/vir/src/well_formed.rs

@@ -1396,6 +1396,23 @@ pub fn check_crate(
             }
         }
     }
+
+    for reveal_group in krate.reveal_groups.iter() {
+        for member in reveal_group.x.members.iter() {
+            if let Some(function) = funs.get(member) {
+                if !function.x.attrs.broadcast_forall {
+                    return Err(error(
+                        &reveal_group.span,
+                        format!(
+                            "{} is not a broadcast proof fn",
+                            fun_as_friendly_rust_name(member)
+                        ),
+                    ));
+                }
+            }
+        }
+    }
+
     let ctxt = Ctxt { funs, reveal_groups, dts, krate: krate.clone(), unpruned_krate };
     for function in krate.functions.iter() {
         check_function(&ctxt, function, diags, no_verify)?;