Fix attribute macro: evaluation of constant value failed

source/builtin_macros/src/attr_rewrite.rs

@@ -41,9 +41,9 @@ use syn::{Expr, Item, parse2, spanned::Spanned};
 use crate::{
     EraseGhost,
     attr_block_trait::{AnyAttrBlock, AnyFnOrLoop},
-    syntax,
-    syntax::mk_verus_attr_syn,
+    syntax::{self, mk_verifier_attr_syn, mk_verus_attr_syn},
     syntax_trait,
+    unerased_proxies::VERUS_UNERASED_PROXY,
 };
 
 pub const VERIFIED: &str = "_VERUS_VERIFIED";
@@ -129,7 +129,7 @@ pub fn rewrite_verus_attribute(
                 spec_f.sig.ident = ident.clone();
                 spec_f.attrs = vec![mk_verus_attr_syn(f.span(), quote! { spec })];
                 // remove proof-related macros
-                spec_f.block.as_mut().stmts.retain(|stmt| !is_verus_proof_stmt(stmt));
+                replace_block(EraseGhost::Erase, spec_f.block_mut().unwrap());
                 spec_fun = Some(spec_f);
 
                 attributes
@@ -212,7 +212,9 @@ impl VisitMut for ExecReplacer {
     fn visit_block_mut(&mut self, block: &mut syn::Block) {
         syn::visit_mut::visit_block_mut(self, block);
 
+        // If we are in non-verification mode, we erase all proof-related statements.
         if !self.erase.keep() {
+            block.stmts.retain(|stmt| !is_verus_proof_stmt(stmt));
             return;
         }
 
@@ -372,6 +374,22 @@ pub fn rewrite_verus_spec_on_fun_or_loop(
                 let unverified_fun = rewrite_unverified_func(&mut fun, with.with.span());
                 unverified_fun.to_tokens(&mut new_stream);
             }
+            if fun.sig.constness.is_some() {
+                let mut const_fun = fun.clone();
+                let span = fun.sig.constness.unwrap().span();
+                // It seems that we do not need to erase anything.
+                // But just do it to be safe and consistent with verus macro.
+                replace_block(EraseGhost::Erase, const_fun.block_mut().unwrap());
+                const_fun.attrs.push(mk_verifier_attr_syn(span, quote! { external }));
+                const_fun.attrs.push(mk_verus_attr_syn(span, quote! { uses_unerased_proxy }));
+                const_fun.attrs.push(mk_verus_attr_syn(span, quote! { encoded_const }));
+                const_fun.to_tokens(&mut new_stream);
+                fun.sig.ident = syn::Ident::new(
+                    &format!("{VERUS_UNERASED_PROXY}{}", fun.sig.ident),
+                    fun.sig.ident.span(),
+                );
+                fun.attrs.push(mk_verus_attr_syn(span, quote! { unerased_proxy }));
+            }
             let spec_stmts = syntax::sig_specs_attr(erase, spec_attr, &mut fun.sig);
             let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap());
             let _ = fun.block_mut().unwrap().stmts.splice(0..0, new_stmts);

source/builtin_macros/src/syntax.rs

@@ -5024,7 +5024,7 @@ macro_rules! declare_mk_rust_attr {
 declare_mk_rust_attr!(mk_rust_attr, syn_verus);
 declare_mk_rust_attr!(mk_rust_attr_syn, syn);
 
-/// Constructs #[verus::internal(tokens)]
+/// Constructs #[verus::internal(tokens)] and #[verifier::tokens]
 macro_rules! declare_mk_verus_attr {
     ($name:ident, $name2:ident, $s:ident) => {
         pub(crate) fn $name(span: Span, tokens: TokenStream) -> $s::Attribute {
@@ -5064,18 +5064,9 @@ macro_rules! declare_mk_verus_attr {
                 ident: $s::Ident::new("verifier", span),
                 arguments: $s::PathArguments::None,
             });
+            path_segments.push($s::parse_quote_spanned!(span => #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 },
-                })
-            };
+            let meta = $s::Meta::Path(path);
             $s::Attribute {
                 pound_token: $s::token::Pound { spans: [span] },
                 style: $s::AttrStyle::Outer,

source/builtin_macros/src/unerased_proxies.rs

@@ -74,7 +74,7 @@ use syn_verus::token::{Brace, Paren};
 use syn_verus::visit_mut::VisitMut;
 use syn_verus::*;
 
-const VERUS_UNERASED_PROXY: &str = "VERUS_UNERASED_PROXY__";
+pub(crate) const VERUS_UNERASED_PROXY: &str = "VERUS_UNERASED_PROXY__";
 
 impl crate::syntax::Visitor {
     fn needs_unerased_proxies(&self) -> bool {

source/rust_verify_test/tests/syntax_attr.rs

@@ -580,7 +580,10 @@ test_verify_one_file! {
             proof!{
                 assert(true);
             }
-            x + y
+            {
+                proof!{assert(true);}
+                x + y
+            }
         }
 
         #[verus_verify(dual_spec)]
@@ -754,3 +757,24 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] test_const_fn_eval_via_proxy code!{
+        use vstd::prelude::*;
+        #[verus_spec(ret =>
+            ensures ret == x
+        )]
+        #[allow(unused_variables)]
+        pub const fn const_fn(x: u64) -> u64 {
+            proof!{
+                assert(true);
+            }
+            {
+                proof!{assert(true);}
+            }
+            x
+        }
+
+        pub const X: u64 = const_fn(1);
+    } => Ok(())
+}