diff --git a/source/rust_verify_test/tests/broadcast_forall.rs b/source/rust_verify_test/tests/broadcast_forall.rs index 0e1413a1b..9526f0f60 100644 --- a/source/rust_verify_test/tests/broadcast_forall.rs +++ b/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") +} diff --git a/source/vir/src/well_formed.rs b/source/vir/src/well_formed.rs index ed25abae7..718d46e4a 100644 --- a/source/vir/src/well_formed.rs +++ b/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)?;