Support broadcast groups in traits

dependencies/syn/src/item.rs

@@ -648,6 +648,9 @@ ast_enum_of_structs! {
         /// A macro invocation within the definition of a trait.
         Macro(TraitItemMacro),
 
+        /// A broadcast group
+        BroadcastGroup(ItemBroadcastGroup),
+
         /// Tokens within the definition of a trait not interpreted by Syn.
         Verbatim(TokenStream),
 
@@ -2531,7 +2534,9 @@ pub(crate) mod parsing {
 
             let lookahead = ahead.lookahead1();
             let allow_safe = false;
-            let mut item = if lookahead.peek(Token![fn]) || peek_signature(&ahead, allow_safe) {
+            let mut item = if lookahead.peek(Token![broadcast]) && input.peek2(Token![group]) {
+                input.parse().map(TraitItem::BroadcastGroup)
+            } else if lookahead.peek(Token![fn]) || peek_signature(&ahead, allow_safe) {
                 input.parse().map(TraitItem::Fn)
             } else if lookahead.peek(Token![const]) {
                 let publish = input.parse()?;
@@ -2602,6 +2607,7 @@ pub(crate) mod parsing {
                 TraitItem::Fn(item) => &mut item.attrs,
                 TraitItem::Type(item) => &mut item.attrs,
                 TraitItem::Macro(item) => &mut item.attrs,
+                TraitItem::BroadcastGroup(item) => &mut item.attrs,
                 TraitItem::Verbatim(_) => unreachable!(),
             };
             attrs.append(item_attrs);

source/builtin_macros/src/syntax.rs

@@ -1566,6 +1566,7 @@ impl Visitor {
     fn visit_trait_items_prefilter(&mut self, items: &mut Vec<TraitItem>) {
         if self.rustdoc {
             for trait_item in items.iter_mut() {
+                let span = trait_item.span().clone();
                 match trait_item {
                     TraitItem::Fn(trait_item_method) => {
                         crate::rustdoc::process_trait_item_method(trait_item_method);
@@ -1581,6 +1582,7 @@ impl Visitor {
                     FnMode::Spec(_) | FnMode::SpecChecked(_) | FnMode::Proof(_) => false,
                     FnMode::Exec(_) | FnMode::Default => true,
                 },
+                TraitItem::BroadcastGroup(_) => false,
                 _ => true,
             });
         }
@@ -1591,6 +1593,7 @@ impl Visitor {
                 TraitItem::Fn(ref mut fun) => {
                     split_trait_method(&mut spec_items, fun, erase_ghost);
                 }
+                TraitItem::BroadcastGroup(item_broadcast_group) => {}
                 _ => {}
             }
         }
@@ -3612,6 +3615,17 @@ impl VisitMut for Visitor {
     fn visit_item_trait_mut(&mut self, tr: &mut ItemTrait) {
         tr.attrs.push(mk_verus_attr(tr.span(), quote! { verus_macro }));
         self.visit_trait_items_prefilter(&mut tr.items);
+        for trait_item in &mut tr.items {
+            let span = trait_item.span();
+            match trait_item {
+                TraitItem::BroadcastGroup(item_broadcast_group) => {
+                    *trait_item = TraitItem::Verbatim(
+                        self.handle_broadcast_group(item_broadcast_group, span),
+                    );
+                }
+                _ => (),
+            }
+        }
         self.filter_attrs(&mut tr.attrs);
         syn_verus::visit_mut::visit_item_trait_mut(self, tr);
     }

source/rust_verify_test/tests/broadcast_forall.rs

@@ -627,3 +627,26 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "lemma_foo is not a broadcast proof fn")
 }
+
+test_verify_one_file! {
+    #[test] #[ignore] broadcast_group_in_trait verus_code! {
+        trait ATrait {
+            spec fn foo(i: int) -> bool;
+
+            broadcast proof fn lemma_foo(i: int)
+                ensures Self::foo(i)
+            {}
+
+            broadcast group group_foo {
+                // TODO see if we can auto-replace `Self` with the trait name
+                ATrait::lemma_foo,
+            }
+        }
+
+        proof fn lemma_bar<A: ATrait>() {
+            // broadcast use A::group_foo;
+
+            // assert(A::foo(0));
+        }
+    } => Ok(())
+}