broadcast use in a method body is automatically proof mode

verus-lang · Mar 4, 2024 · 852db35 · 852db35
1 parent f442fa1
commit 852db35
Show file tree

Hide file tree

Showing 3 changed files with 60 additions and 1 deletion.
diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs
@@ -826,8 +826,12 @@ impl Visitor {
                     let stmts: Vec<Stmt> = paths.iter().map(|path| Stmt::Expr(Expr::Verbatim(
                         quote_spanned!(span => ::builtin::reveal_hide_({#[verus::internal(reveal_fn)] fn __VERUS_REVEAL_INTERNAL__() { ::builtin::reveal_hide_internal_path_(#path) } #[verus::internal(broadcast_use_reveal)] __VERUS_REVEAL_INTERNAL__}, 1); )
                     ))).collect();
+                    let mut attrs = attrs.clone();
+                    if self.inside_ghost == 0 {
+                        attrs.push(mk_verus_attr(span, quote! { proof_block }));
+                    }
                     let block = Stmt::Expr(Expr::Block(ExprBlock {
-                        attrs: attrs.clone(),
+                        attrs: attrs,
                         label: None,
                         block: Block { brace_token: token::Brace(span), stmts },
                     }));

diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs
@@ -528,6 +528,9 @@ pub(crate) fn parse_attrs(
                         v.push(Attr::AllTriggers)
                     }
                     AttrTree::Fun(_, arg, None) if arg == "verus_macro" => v.push(Attr::VerusMacro),
+                    AttrTree::Fun(_, arg, None) if arg == "proof_block" => {
+                        v.push(Attr::GhostBlock(GhostBlockAttr::Proof))
+                    }
                     AttrTree::Fun(_, arg, None) if arg == "external_body" => {
                         v.push(Attr::ExternalBody)
                     }

diff --git a/source/rust_verify_test/tests/broadcast_forall.rs b/source/rust_verify_test/tests/broadcast_forall.rs
@@ -502,3 +502,55 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] test_ring_algebra_exec verus_code! {
+        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,
+                }
+            }
+        }
+
+        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);
+            }
+        }
+    } => Ok(())
+}