From e0d7f69da8102fe15f56bc697ded7693eed8455a Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Wed, 27 Mar 2024 09:27:08 +0100 Subject: [PATCH 1/2] Add support for `broadcast proof fn` syntax --- src/lib.rs | 3 ++- src/verus.pest | 3 ++- tests/verus-consistency.rs | 21 +++++++++++++++++++++ 3 files changed, 25 insertions(+), 2 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 58576ee..ef8e25e 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -738,7 +738,8 @@ 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 => s.append(arena.space()), Rule::as_str | Rule::by_str_inline diff --git a/src/verus.pest b/src/verus.pest index f076fff..21fc8d2 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -334,6 +334,7 @@ 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) } verusfmt_skip_attribute = { "#" ~ "[" ~ "verusfmt" ~ "::" ~ "skip" ~ "]" @@ -658,7 +659,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 ~ diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index b4834fd..c7e6980 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1807,3 +1807,24 @@ 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! + "###); +} From 43b625f9a79561269092d0e7e0a3f6bb040558af Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Wed, 27 Mar 2024 10:29:48 +0100 Subject: [PATCH 2/2] add support for `broadcast use` and `broadcast group` syntax --- src/lib.rs | 8 +- src/verus.pest | 24 +++++ tests/verus-consistency.rs | 178 +++++++++++++++++++++++++++++++++++++ 3 files changed, 209 insertions(+), 1 deletion(-) diff --git a/src/lib.rs b/src/lib.rs index ef8e25e..41d046a 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -739,7 +739,9 @@ fn to_doc<'a>( | Rule::while_str | Rule::yeet_str | Rule::yield_str - | Rule::broadcast_str => s.append(arena.space()), + | Rule::broadcast_str + | Rule::group_str + | Rule::broadcast_group_identifier => s.append(arena.space()), Rule::as_str | Rule::by_str_inline @@ -822,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 => { @@ -986,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 // diff --git a/src/verus.pest b/src/verus.pest index 21fc8d2..9542318 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -335,6 +335,7 @@ 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" ~ "]" @@ -588,6 +589,8 @@ item_no_macro_call = _{ | type_alias | union | use + | broadcast_group + | broadcast_use } verusfmt_skipped_item = { @@ -809,6 +812,7 @@ assoc_item = { | fn | macro_call | type_alias + | broadcast_group } impl = { @@ -895,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 // //****************************// diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index c7e6980..9838555 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1828,3 +1828,181 @@ verus!{ } // 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! + "###); +}