`#[verus_spec]` misuse error after formatting by verusfmt

[Marsman1996]

Verusfmt may introduce verification errors when formatting code that uses the #[verus_spec] attribute.

Description

Original code:

        let ptr = vstd_extra::array_ptr::ArrayPtr::<C::E, CONST_NR_ENTRIES>::from_addr(
            paddr_to_vaddr(
                #[verus_spec(with Tracked(&slot_own), Tracked(slot_perm))]
                self.start_paddr()
            ),
        );

Formatted code:

        let ptr = vstd_extra::array_ptr::ArrayPtr::<C::E, CONST_NR_ENTRIES>::from_addr(
            paddr_to_vaddr(
                #[verus_spec(with Tracked(&slot_own), Tracked(slot_perm))]
                self.start_paddr(),
            ),
        );

The extra comma in self.start_paddr(), introduces the error

error: macro expansion ignores `;` and any tokens following
   --> /home/yuwei/ruzykaller/kverus/database/verified/code/ostd/src/mm/page_table/node/mod.rs:322:35
    |
321 |                 #[verus_spec(with Tracked(&slot_own), Tracked(slot_perm))]
    |                 ---------------------------------------------------------- caused by the macro expansion here
322 |                 self.start_paddr(),
    |                                   ^
    |
    = note: the usage of `verus_spec!` is likely invalid in expression context
help: you might be missing a semicolon here
    |
321 |                 #[verus_spec(with Tracked(&slot_own), Tracked(slot_perm))];
    |                                                                           +

error: Misuse of #[verus_spec]
   --> /home/yuwei/ruzykaller/kverus/database/verified/code/ostd/src/mm/page_table/node/mod.rs:322:35
    |
322 |                 self.start_paddr(),
    |                                   ^

error: aborting due to 2 previous errors

More details can be referred to the GitHub workflow here
https://github.com/Marsman1996/vostd/actions/runs/18524524440/job/52792021540

The code can be referred in
Marsman1996/vostd@d94c101

[parno]

Just a note that this should probably be fixed within the verus_spec macro.

[parno]

@ziqiaozhou Does this seem fixable in the verus_spec macro?

[Marsman1996]

Minimal PoC:

use vstd::prelude::*;
use vstd::simple_pptr::*;

verus! {
    use vstd_extra::array_ptr::ArrayPtr;
    use crate::mem::{paddr_to_vaddr};

    impl<C: Config> PageSlot<C> {
        pub const CONST_NR_ENTRIES: usize = 512;

        pub fn get_array_ptr(
            &self,
            Tracked(slot_own): Tracked<&SlotOwnership>,
            Tracked(slot_perm): Tracked<&SlotPerm>,
        ) -> (ptr: ArrayPtr<C::E, Self::CONST_NR_ENTRIES>)
        requires
            self.is_valid(),
            slot_own.is_owned_by(self),
            slot_perm.allows_read_write(self.start_paddr()),
        ensures
            ptr@.len() == Self::CONST_NR_ENTRIES,
            ptr@.base_addr() == paddr_to_vaddr(self.start_paddr()),
        {
            let ptr = vstd_extra::array_ptr::ArrayPtr::<C::E, Self::CONST_NR_ENTRIES>::from_addr(
                paddr_to_vaddr(
                    #[verus_spec(with Tracked(&slot_own), Tracked(slot_perm))]
                    self.start_paddr(),
                ),
            );
            ptr
        }
    }
}

And playground link:
https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=0e757f2c4340babc8fcdd1f75d467aca

(Please ignore the unresolved import errors)

[hiroki-chen]

This should be the expansion bug caused by the macro which generates syntactically wrong code.

[Marsman1996]

This error is because in rewrite_verus_spec function, it checks whther the input is VerusSpecTarget, which are either FnOrLoop or an Expr.
As a result, self.start_paddr() is Expr and self.start_paddr(), is not.

verus/source/builtin_macros/src/attr_rewrite.rs

Lines 282 to 301 in ab74a6d

	pub(crate) fn rewrite_verus_spec(
	erase: EraseGhost,
	outer_attr_tokens: proc_macro::TokenStream,
	input: proc_macro::TokenStream,
	) -> proc_macro::TokenStream {
	if !erase.keep() {
	return input;
	}
	let f = match syn::parse::<VerusSpecTarget>(input) {
	Ok(f) => f,
	Err(err) => {
	// Make sure at least one error is reported, just in case Rust parses the function
	// successfully but syn fails to parse it.
	// (In the normal case, this results in a redundant extra error message after
	// the normal Rust syntax error, but it's a reasonable looking error message.)
	return proc_macro::TokenStream::from(
	quote_spanned!(err.span() => compile_error!("Misuse of #[verus_spec]");),
	);
	}
	};

verus/source/builtin_macros/src/attr_rewrite.rs

Lines 53 to 60 in ab74a6d

	enum VerusIOTarget {
	Local(syn::Local),
	Expr(syn::Expr),
	}
	enum VerusSpecTarget {
	IOTarget(VerusIOTarget),
	FnOrLoop(AnyFnOrLoop),
	}

So a possible solution is to remove the last , in rewrite_verus_spec.
Is it a good solution?
@parno