Code in `src/bin` recognizes traits in lib as external, not verified

[suremarc]

Hi,

I'm brand new to this ecosystem, I just discovered Verus and Anvil a few days ago. It seems Verus is in the middle of pushing towards making things feel more out-of-the-box and cargo-native with the addition of cargo verus, which is great!

I opened an issue in the Anvil repo about supporting cargo verus and have been having a go at that, which involves moving some of the code into cargo binaries. However, I discovered a peculiar issue. I have a minimal repro, so let me explain -- here is my project layout:

test
├── Cargo.lock
├── Cargo.toml
├── src
│   ├── lib.rs
│   └── main.rs
└── test2
    ├── Cargo.lock
    ├── Cargo.toml
    └── src
        └── lib.rs

test2 has test as a dependency. test/src/lib.rs defines a trait like this:

verus! {

pub trait Foo {
    open spec fn hello() -> int {
        42
    }
}

}

And then in both src/main.rs and test2/src/lib.rs I have a trait impl like this:

verus! {

struct Bar {}
    
impl test::Foo for Bar {
    open spec fn hello() -> int {
        43
    }
}

}

As it turns out, the one in test2/src/lib.rs compiles, but the one in src/main.rs fails with the following error:

❯ cargo verus build
   Compiling test v0.1.0 (/home/suremarc/anvil/test)
error: function for external trait must have mode 'exec'
 --> src/main.rs:8:15
  |
8 |     open spec fn hello() -> int {
  |               ^^^^^^^^^^^^^^^^^

error: could not compile `test` (bin "test") due to 1 previous error

Being new to the ecosystem, I'm not 100% what's happening here, but from what I could gather reading issues and docs, traits are either marked as 'external' (not proof or spec-carrying) or verified. Since Foo comes from a verus! invocation it should be verified, and indeed, again the code in test2/src/lib.rs compiles fine even though Foo is external to test2. It seems like maybe this is a case overlooked by Verus?

I've attached the repro as a .zip file below. Thanks for reading this far!

test.zip

[parno]

When I run cargo verus verify in the test directory, I get:

 $ cargo verus verify
   Compiling proc-macro2 v1.0.101
    ...
   Compiling verus_builtin_macros v0.0.0-2025-08-12-1837
verification results:: 1147 verified, 0 errors
   Compiling test v0.1.0 (/Users/parno/tmp/gh-1905/test)
verification results:: 2 verified, 0 errors
error: extern location for test does not exist: /Users/parno/tmp/gh-1905/test/target/debug/deps/libtest-5e70bfa3defad50f.rlib
 --> src/main.rs:5:5
  |
5 | use test::{Foo,foo};
  |     ^^^^

error: could not compile `test` (bin "test") due to 1 previous error

It looks like it successfully verifies src/lib.rs (that's the "verification results:: 2 verified, 0 errors"), but it's missing info needed to verify src/main.rs against that. Interestingly, Verus did produce a meta-data file for test, but Rust didn't produce its metadata library info:

$ ls target/debug/deps/libtest*
target/debug/deps/libtest-5e70bfa3defad50f.vir

If I run cargo verus build, then the missing .rlib and .rmeta files do get generated, and we hit the error about external traits, which does look like a bug with how verus/cargo verus handles trait imports. At this point, cargo verus is still quite experimental, so it's not entirely surprising to hit issues like this.

Thanks for the bug report!