Post-merge fixes

dependencies/syn/src/expr.rs

@@ -3613,7 +3613,8 @@ pub(crate) mod printing {
         );
         let left_needs_group = match binop_prec {
             Precedence::Assign => left_prec <= Precedence::Range,
-            Precedence::Compare => left_prec <= binop_prec,
+            // verus supports chained comparisons:
+            // Precedence::Compare => left_prec <= binop_prec,
             _ => left_prec < binop_prec,
         };
 

dependencies/syn/src/item.rs

@@ -1126,7 +1126,7 @@ pub(crate) mod parsing {
                 (Some((eq_token, expr)), None) => {
                     (Some((Some(eq_token), Some(Box::new(expr)))), None, Some(input.parse()?))
                 }
-                (None, Some(_)) => (None, Some(input.parse()?), None),
+                (None, Some(_)) => (Some((None, None)), Some(input.parse()?), None),
                 _ => return Err(lookahead.error()),
             };
             match value {

source/builtin_macros/Cargo.toml

@@ -9,7 +9,7 @@ proc-macro = true
 [dependencies]
 proc-macro2 = "1.0.39"
 quote = "1.0"
-synstructure = "0.13"
+synstructure = { git = "https://github.com/mystor/synstructure.git", rev = "1079497eb2bea252433dac53afe41291d8779641" }
 syn = { version = "2.0", features = ["full", "visit", "visit-mut", "extra-traits"] }
 syn_verus = { path="../../dependencies/syn", features = ["full", "visit", "visit-mut", "extra-traits"] }
 prettyplease_verus = { path="../../dependencies/prettyplease" }

source/builtin_macros/src/structural.rs

@@ -1,6 +1,6 @@
 use syn_verus::spanned::Spanned;
 
-pub fn derive_structural(s: synstructure::Structure) -> proc_macro2::TokenStream {
+pub fn derive_structural(mut s: synstructure::Structure) -> proc_macro2::TokenStream {
     let assert_receiver_is_structural_body = s
         .variants()
         .iter()
@@ -12,6 +12,12 @@ pub fn derive_structural(s: synstructure::Structure) -> proc_macro2::TokenStream
             }
         })
         .collect::<proc_macro2::TokenStream>();
+
+    // TODO: this feature has disappeared in the latest version of synstructure
+    // (this is why we still use a specific commit of synstructure)
+    // see 'path.segments.iter().find(|s| s.starts_with("_DERIVE_builtin_Structural_FOR_")).is_some()' in rust_to_vir
+    s.underscore_const(false);
+
     s.gen_impl(quote_spanned_builtin! { builtin, s.ast().span() =>
         #[automatically_derived]
         gen impl #builtin::Structural for @Self {

source/builtin_macros/src/syntax.rs

@@ -3199,20 +3199,21 @@ impl VisitMut for Visitor {
                             };
                             let mut path_segments = path_verifier(span);
                             path_segments.push(second_segment.clone());
-                            let list = syn_verus::MetaList {
-                                path: Path { leading_colon: None, segments: path_segments },
-                                delimiter: syn_verus::MacroDelimiter::Paren(token::Paren { span: into_spans(span) }),
-                                tokens: if let Some(nested) = nested {
-                                    quote! { #nested }
-                                } else {
-                                    quote! {}
-                                },
+                            let path = Path { leading_colon: None, segments: path_segments };
+                            let meta = if let Some(nested) = nested {
+                                syn_verus::Meta::List(syn_verus::MetaList {
+                                    path,
+                                    delimiter: syn_verus::MacroDelimiter::Paren(token::Paren { span: into_spans(span) }),
+                                    tokens: quote! { #nested }
+                                })
+                            } else {
+                                syn_verus::Meta::Path(path)
                             };
                             *attr = Attribute {
                                 pound_token: token::Pound { spans: [span] },
                                 style: syn_verus::AttrStyle::Outer,
                                 bracket_token: token::Bracket { span: into_spans(span) },
-                                meta: syn_verus::Meta::List(list),
+                                meta,
                             };
                         }
                         _ => {
@@ -3620,6 +3621,7 @@ enum MacroElement {
     Comma(Token![,]),
     Semi(Token![;]),
     FatArrow(Token![=>]),
+    Colon(Token![:]),
     Expr(Expr),
 }
 
@@ -3628,6 +3630,7 @@ enum MacroElementExplicitExpr {
     Comma(Token![,]),
     Semi(Token![;]),
     FatArrow(Token![=>]),
+    Colon(Token![:]),
     ExplicitExpr(Token![@], Token![@], Expr),
     TT(TokenTree),
 }
@@ -3673,6 +3676,8 @@ impl Parse for MacroElement {
             Ok(MacroElement::Semi(input.parse()?))
         } else if input.peek(Token![=>]) {
             Ok(MacroElement::FatArrow(input.parse()?))
+        } else if input.peek(Token![:]) {
+            Ok(MacroElement::Colon(input.parse()?))
         } else {
             Ok(MacroElement::Expr(input.parse()?))
         }
@@ -3687,6 +3692,8 @@ impl Parse for MacroElementExplicitExpr {
             Ok(MacroElementExplicitExpr::Semi(input.parse()?))
         } else if input.peek(Token![=>]) {
             Ok(MacroElementExplicitExpr::FatArrow(input.parse()?))
+        } else if input.peek(Token![:]) {
+            Ok(MacroElementExplicitExpr::Colon(input.parse()?))
         } else if input.peek(Token![@]) && input.peek2(Token![@]) {
             let at1 = input.parse()?;
             let at2 = input.parse()?;
@@ -3771,6 +3778,7 @@ impl ToTokens for MacroElement {
             MacroElement::Comma(e) => e.to_tokens(tokens),
             MacroElement::Semi(e) => e.to_tokens(tokens),
             MacroElement::FatArrow(e) => e.to_tokens(tokens),
+            MacroElement::Colon(e) => e.to_tokens(tokens),
             MacroElement::Expr(e) => e.to_tokens(tokens),
         }
     }
@@ -3782,6 +3790,7 @@ impl ToTokens for MacroElementExplicitExpr {
             MacroElementExplicitExpr::Comma(e) => e.to_tokens(tokens),
             MacroElementExplicitExpr::Semi(e) => e.to_tokens(tokens),
             MacroElementExplicitExpr::FatArrow(e) => e.to_tokens(tokens),
+            MacroElementExplicitExpr::Colon(e) => e.to_tokens(tokens),
             MacroElementExplicitExpr::ExplicitExpr(_at1, _at2, e) => e.to_tokens(tokens),
             MacroElementExplicitExpr::TT(e) => e.to_tokens(tokens),
         }
@@ -4186,16 +4195,21 @@ macro_rules! declare_mk_rust_attr {
                 ident: $s::Ident::new(name, span),
                 arguments: $s::PathArguments::None,
             });
-            let list = $s::MetaList {
-                path: $s::Path { leading_colon: None, segments: path_segments },
-                delimiter: $s::MacroDelimiter::Paren($s::token::Paren { span: into_spans(span) }),
-                tokens: quote! { #tokens },
+            let path = $s::Path { leading_colon: None, segments: path_segments };
+            let meta = if tokens.is_empty() {
+                $s::Meta::Path(path)
+            } else {
+                $s::Meta::List($s::MetaList {
+                    path,
+                    delimiter: $s::MacroDelimiter::Paren($s::token::Paren { span: into_spans(span) }),
+                    tokens: quote! { #tokens },
+                })
             };
             $s::Attribute {
                 pound_token: $s::token::Pound { spans: [span] },
                 style: $s::AttrStyle::Outer,
                 bracket_token: $s::token::Bracket { span: into_spans(span) },
-                meta: $s::Meta::List(list),
+                meta,
             }
         }
     };
@@ -4216,16 +4230,21 @@ macro_rules! declare_mk_verus_attr {
                 ident: $s::Ident::new("internal", span),
                 arguments: $s::PathArguments::None,
             });
-            let list = $s::MetaList {
-                path: $s::Path { leading_colon: None, segments: path_segments },
-                delimiter: $s::MacroDelimiter::Paren($s::token::Paren { span: into_spans(span) }),
-                tokens: quote! { #tokens },
+            let path = $s::Path { leading_colon: None, segments: path_segments };
+            let meta = if tokens.is_empty() {
+                $s::Meta::Path(path)
+            } else {
+                $s::Meta::List($s::MetaList {
+                    path,
+                    delimiter: $s::MacroDelimiter::Paren($s::token::Paren { span: into_spans(span) }),
+                    tokens: quote! { #tokens },
+                })
             };
             $s::Attribute {
                 pound_token: $s::token::Pound { spans: [span] },
                 style: $s::AttrStyle::Outer,
                 bracket_token: $s::token::Bracket { span: into_spans(span) },
-                meta: $s::Meta::List(list),
+                meta,
             }
         }
     };

source/rust_verify_test/tests/regression.rs

@@ -535,7 +535,7 @@ test_verify_one_file! {
         pub struct Y {
             y: int
         }
-    } => Err(err) => assert_vir_error_msg(err, "expected one of")
+    } => Err(err) => assert_vir_error_msg(err, "unexpected token, expected `]`")
 }
 
 test_verify_one_file! {
@@ -552,7 +552,7 @@ test_verify_one_file! {
         #[verifier(external),verifier(external_body)]
         proof fn bar() {
         }
-    } => Err(err) => assert_vir_error_msg(err, "expected `]`, found `,`")
+    } => Err(err) => assert_vir_error_msg(err, "unexpected token, expected `]`")
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/triggers.rs

@@ -18,8 +18,8 @@ test_verify_one_file! {
                 forall|i: nat, j: nat|
                     i < self.nodes.len() && j < self.nodes.index(spec_cast_integer::<nat, int>(i)).values.len() ==>
                     {
-                        let values = #[verifier(trigger)] self.nodes.index(spec_cast_integer::<nat, int>(i)).values;
-                        self.base_v <= #[verifier(trigger)] values.index(spec_cast_integer::<nat, int>(j))
+                        let values = #[trigger] self.nodes.index(spec_cast_integer::<nat, int>(i)).values;
+                        self.base_v <= #[trigger] values.index(spec_cast_integer::<nat, int>(j))
                     }
             }
         }