`#[verus_spec]` macro errors within `impl` blocks.

[hiroki-chen]

Description

The following code does not compile

pub struct Foo;

impl Foo {
    #[verus_spec(ret =>
        with
            Tracked(c): Tracked<&mut DekoPointsTo<()>>
        requires
            true,
        ensures
            ret == 1,
    )]
    fn test(a: u64, b: u64) -> u64 {
        1
    }
}

Moving the function body outside Foo makes Rust compiler happy, however. This should have something to do with the proc_macro bug. Also a sidenote, adding a trailing comma after arguments in with block causes macro expansion error.

[hiroki-chen]

The identifier starts with _VERUS_VERIFIED_ seems to be defined in the wrong context for impl blocks.

[parno]

@ziqiaozhou Is this something you could take a look at?

[Marsman1996]

For code

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

pub struct Foo;

impl Foo {
    #[verus_spec(ret =>
        with
            Tracked(c): Tracked<&mut DekoPointsTo<()>>
        requires
            true,
        ensures
            ret == 1,
    )]
    fn test(a: u64, b: u64) -> u64 {
        1
    }
}

The generated code is

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

pub struct Foo;

impl Foo {
    #[verus::internal(verus_macro)]
    #[verus::internal(external_body)]
    fn test(a: u64, b: u64) -> u64 {
        ::vstd::prelude::requires([false]);
        unimplemented!();
    }

    #[verus::internal(verus_macro)]
    fn _VERUS_VERIFIED_test(a: u64, b: u64, verus_tmp_c: Tracked<&mut DekoPointsTo<()>>) -> u64 {
        #[verus::internal(header_unwrap_parameter)]
        let c;
        #[verifier::proof_block]
        {
            c = verus_tmp_c.get()
        };
        ::vstd::prelude::requires([true]);
        ::vstd::prelude::ensures(|ret| {
            [
                ::vstd::prelude::constrain_type(ret, _VERUS_VERIFIED_test(a, b, verus_tmp_c)),
                {
                    let ret = ret;
                    ::vstd::prelude::spec_eq(ret, ::vstd::prelude::spec_literal_nat("1"))
                },
            ]
        });
        1
    }
}

And the error message is

error[E0425]: cannot find function `_VERUS_VERIFIED_test` in this scope
  --> test-impl-1-2.rs:25:54
   |
25 |                 ::vstd::prelude::constrain_type(ret, _VERUS_VERIFIED_test(a, b, verus_tmp_c)),
   |                                                      ^^^^^^^^^^^^^^^^^^^^ not found in this scope
   |
help: consider using the associated function on `Self`
   |
25 |                 ::vstd::prelude::constrain_type(ret, Self::_VERUS_VERIFIED_test(a, b, verus_tmp_c)),
   |                                                      ++++++

error: aborting due to 2 previous errors

So the root cause is because in some cases, it calls the method _VERUS_VERIFIED_xxx in constrain_type without adding a Self::

[Marsman1996]

So a straitforward fix is to add Self:: here

[Marsman1996]

We need to tell Verus whether this is a method or function, but it is kinda hard in rewrite_verus_spec_on_fun_or_loop since we only have the function instead of the whole impl here.