cannot recognize constants as an exec value across multi crates

[rikosellic]

Verus does recognize constants defined in another verified crate in spec mode, but cannot recognize it as an exec value. For example, suppose I define constant ONE in the library crate mylibrary/lib.rs and compile it following the instructions in this Zulip conversation.

use vstd::prelude::*;
verus!
{
    pub const ONE: usize = 1;
}

Later when I want to use ONE as a spec value in my main crate mymain/lib.rs, everything works smoothly :

use mylibrary::ONE;
use vstd::prelude::*;

verus!{
    proof fn test() 
    {
        assert(ONE+ONE==2);
    }
}

But if I attempt to treat it as an exec value, like defining another constant:

verus!{
    pub const TWO : usize = ONE + ONE;
}

or using it as a return value:

verus!{
    fn f() -> usize
    {
        ONE
    }
}

verus will report an error indicating that it can not find a function:

error: cannot find function `f472_ONE` in this scope
  --> mylibrary\src\lib.rs:19:29
   |
19 |     pub const TWO : usize = ONE + ONE;
   |                             ^^^

error: cannot find function `f472_ONE` in this scope
  --> mylibrary\src\lib.rs:19:35
   |
19 |     pub const TWO : usize = ONE + ONE;
   |                                   ^^^

error: aborting due to 2 previous errors

note: This error was found in Verus pass: ownership checking of tracked code

It seems this problem is that the underlying representation of constants in exec mode is not passed between crates, is there a proper solution for this situation?

[chrihop]

I've encountered this issue as well. Constants from imported crates do not appear as the corresponding function definitions in the crate-lifetime.rs file when logging is enabled, yet they are referenced in the function body of the callers.

// crate-lifetime.rs
...
fn main() {}



fn f31_main(
)
{
    let x24_x: u32 = f25_ONE();
}