Add support for broadcast proof, broadcast group, and broadcast use

src/lib.rs

@@ -738,7 +738,10 @@ fn to_doc<'a>(
         | Rule::where_str
         | Rule::while_str
         | Rule::yeet_str
-        | Rule::yield_str => s.append(arena.space()),
+        | Rule::yield_str
+        | Rule::broadcast_str
+        | Rule::group_str
+        | Rule::broadcast_group_identifier => s.append(arena.space()),
 
         Rule::as_str
         | Rule::by_str_inline
@@ -821,6 +824,8 @@ fn to_doc<'a>(
         Rule::r#use => map_to_doc(ctx, arena, pair),
         Rule::use_tree => map_to_doc(ctx, arena, pair),
         Rule::use_tree_list => comma_delimited(ctx, arena, pair, false).braces().group(),
+        Rule::broadcast_use_list => comma_delimited(ctx, arena, pair, false).group(),
+        Rule::broadcast_group_list => comma_delimited(ctx, arena, pair, false).braces(),
         Rule::fn_qualifier => map_to_doc(ctx, arena, pair),
         Rule::fn_terminator => map_to_doc(ctx, arena, pair),
         Rule::r#fn => {
@@ -985,6 +990,8 @@ fn to_doc<'a>(
         }
         Rule::attr_inner => map_to_doc(ctx, arena, pair),
         Rule::meta => unsupported(pair),
+        Rule::broadcast_use => map_to_doc(ctx, arena, pair),
+        Rule::broadcast_group => map_to_doc(ctx, arena, pair),
 
         //****************************//
         // Statements and Expressions //

src/verus.pest

@@ -334,6 +334,8 @@ where_str = ${ "where" ~ !("_" | ASCII_ALPHANUMERIC) }
 while_str = ${ "while" ~ !("_" | ASCII_ALPHANUMERIC) }
 yeet_str = ${ "yeet" ~ !("_" | ASCII_ALPHANUMERIC) }
 yield_str = ${ "yield" ~ !("_" | ASCII_ALPHANUMERIC) }
+broadcast_str = ${ "broadcast" ~ !("_" | ASCII_ALPHANUMERIC) }
+group_str = ${ "group" ~ !("_" | ASCII_ALPHANUMERIC) }
 
 verusfmt_skip_attribute = {
     "#" ~ "[" ~ "verusfmt" ~ "::" ~ "skip"  ~ "]"
@@ -587,6 +589,8 @@ item_no_macro_call = _{
   | type_alias
   | union
   | use
+  | broadcast_group
+  | broadcast_use
 }
 
 verusfmt_skipped_item = {
@@ -658,7 +662,7 @@ fn_terminator = {
 
 fn = {
     attr* ~ visibility? ~ publish? ~
-    default_str? ~ const_str? ~ async_str? ~ unsafe_str? ~ abi? ~ fn_mode? ~
+    default_str? ~ const_str? ~ async_str? ~ unsafe_str? ~ abi? ~ broadcast_str? ~ fn_mode? ~
     fn_str ~ name ~ generic_param_list? ~ param_list ~ ret_type? ~
     prover? ~ where_clause? ~
     fn_qualifier ~
@@ -808,6 +812,7 @@ assoc_item = {
   | fn
   | macro_call
   | type_alias
+  | broadcast_group
 }
 
 impl = {
@@ -894,6 +899,26 @@ meta = {
     path ~ (eq_str ~ expr | token_tree)?
 }
 
+broadcast_use_list = {
+    (path ~ ("," ~ path)* ~ ","?)
+}
+
+broadcast_use = {
+    broadcast_str ~ use_str ~ broadcast_use_list ~ semi_str
+}
+
+broadcast_group_identifier = {
+    identifier
+}
+
+broadcast_group_list = {
+    "{" ~ (path ~ ("," ~ path)* ~ ","?)? ~ "}"
+}
+
+broadcast_group = {
+    visibility? ~ broadcast_str ~ group_str ~ broadcast_group_identifier ~ broadcast_group_list
+}
+
 //****************************//
 // Statements and Expressions //
 //****************************//

tests/verus-consistency.rs

@@ -1807,3 +1807,202 @@ verus!{
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_broadcast_proof() {
+    let file = r#"
+verus!{
+    broadcast proof fn property() { }
+    pub broadcast proof fn property() { }
+} // verus!
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    broadcast proof fn property() {
+    }
+
+    pub broadcast proof fn property() {
+    }
+
+    } // verus!
+    "###);
+}
+
+#[test]
+fn verus_broadcast_use() {
+    let file = r#"
+verus! {
+mod ring {
+    use builtin::*;
+
+    pub struct Ring {
+        pub i: u64,
+    }
+
+    impl Ring {
+        pub closed spec fn inv(&self) -> bool {
+            self.i < 10
+        }
+
+        pub closed spec fn spec_succ(&self) -> Ring {
+            Ring { i: if self.i == 9 { 0 } else { (self.i + 1) as u64 } }
+        }
+
+        pub closed spec fn spec_prev(&self) -> Ring {
+            Ring { i: if self.i == 0 { 9 } else { (self.i - 1) as u64 } }
+        }
+
+        pub broadcast proof fn spec_succ_ensures(p: Ring)
+            requires p.inv()
+            ensures p.inv() && (#[trigger] p.spec_succ()).spec_prev() == p
+        { }
+
+        pub broadcast proof fn spec_prev_ensures(p: Ring)
+            requires p.inv()
+            ensures p.inv() && (#[trigger] p.spec_prev()).spec_succ() == p
+        { }
+
+        pub    broadcast    group    properties {
+        Ring::spec_succ_ensures,
+                Ring::spec_prev_ensures,
+        }
+    }
+
+    pub    broadcast    group    properties {
+    Ring::spec_succ_ensures,
+            Ring::spec_prev_ensures,
+    }
+}
+
+mod m2 {
+    use builtin::*;
+    use crate::ring::*;
+
+    fn t2(p: Ring) requires p.inv() {
+           broadcast    use     Ring::properties;
+        assert(p.spec_succ().spec_prev() == p);
+        assert(p.spec_prev().spec_succ() == p);
+    }
+}
+
+mod m3 {
+    use builtin::*;
+    use crate::ring::*;
+
+        broadcast   use    Ring::properties;
+
+        fn a() { }
+}
+
+mod m4 {
+    use builtin::*;
+    use crate::ring::*;
+
+        broadcast   use    
+                    Ring::spec_succ_ensures,
+            Ring::spec_prev_ensures;
+}
+} // verus!
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    mod ring {
+        use builtin::*;
+
+        pub struct Ring {
+            pub i: u64,
+        }
+
+        impl Ring {
+            pub closed spec fn inv(&self) -> bool {
+                self.i < 10
+            }
+
+            pub closed spec fn spec_succ(&self) -> Ring {
+                Ring {
+                    i: if self.i == 9 {
+                        0
+                    } else {
+                        (self.i + 1) as u64
+                    },
+                }
+            }
+
+            pub closed spec fn spec_prev(&self) -> Ring {
+                Ring {
+                    i: if self.i == 0 {
+                        9
+                    } else {
+                        (self.i - 1) as u64
+                    },
+                }
+            }
+
+            pub broadcast proof fn spec_succ_ensures(p: Ring)
+                requires
+                    p.inv(),
+                ensures
+                    p.inv() && (#[trigger] p.spec_succ()).spec_prev() == p,
+            {
+            }
+
+            pub broadcast proof fn spec_prev_ensures(p: Ring)
+                requires
+                    p.inv(),
+                ensures
+                    p.inv() && (#[trigger] p.spec_prev()).spec_succ() == p,
+            {
+            }
+
+            pub broadcast group properties {
+                Ring::spec_succ_ensures,
+                Ring::spec_prev_ensures,
+            }
+        }
+
+        pub broadcast group properties {
+            Ring::spec_succ_ensures,
+            Ring::spec_prev_ensures,
+        }
+
+    }
+
+    mod m2 {
+        use builtin::*;
+        use crate::ring::*;
+
+        fn t2(p: Ring)
+            requires
+                p.inv(),
+        {
+            broadcast use Ring::properties;
+            assert(p.spec_succ().spec_prev() == p);
+            assert(p.spec_prev().spec_succ() == p);
+        }
+
+    }
+
+    mod m3 {
+        use builtin::*;
+        use crate::ring::*;
+
+        broadcast use Ring::properties;
+
+        fn a() {
+        }
+
+    }
+
+    mod m4 {
+        use builtin::*;
+        use crate::ring::*;
+
+        broadcast use Ring::spec_succ_ensures, Ring::spec_prev_ensures;
+
+    }
+
+    } // verus!
+    "###);
+}