`cargo verus` passes arguments like `--verify-module` to dependencies too

[jaybosamiya-ms]

cargo verus's implementation seems to pass along the parameters after the -- to all dependencies (including vstd), so something like cargo verus verify -- --verify-module bar for the following files will fail on the vstd build.

Cargo.toml

[package]
name = "foo"
version = "0.1.0"
edition = "2021"
[dependencies]
vstd = "=0.0.0-2025-08-12-1837"
[package.metadata.verus]
verify = true

src/lib.rs

use vstd::prelude::*;

verus! {

mod bar {
    use vstd::prelude::*;

    fn baz() {
        assert(1 == 0 + 1);
    }

}

} // verus!

The workaround for this is fairly straightforward, just run cargo verus verify first (so that vstd finishes; although you'll have to delete target/ first to clear out the cache), followed by cargo verus verify -- --verify-module bar, which then works as expected.

However, this workaround works fine only for single-crate situations. If we are in a multi-crate workspace (e.g., https://github.com/verus-lang/verus-mode.el/tree/main/verus-examples/cv-workspace), then the there is no way to restrict the --verify-module to just a single one of the crates in the workspace. Thus, we cannot benefit from partial verification which can be a performance bottleneck especially when working on a file (you can prob see why I hit this issue when adding support for cargo verus on workspaces within verus-mode.el).

[parno]

This came up w.r.t. verus-analyzer as well. Chris proposed adding a --verify-crate C option, which would skip verification of all crates except C. We could also have cargo verus complain if you tried to use --verify-module without using --verify-crate (with a helpful suggestion, of course). One subtlety is that we'd have to remember that we skipped verification, so that subsequent uses of cargo verus without --verify-crate would go back and verify any unverified crates.

[jaybosamiya-ms]

I like --verify-crate.

As a concrete implementation option, --verify-crate CRATE could set its TARGET_DIR to target/verus-partial-verification/CRATE/... or similar, which means cargo verus (when --verify-crate is not passed) does not need to explicitly remember that verification was skipped, it just isn't even aware of the verus-partial-verification/ dirs and "trivially" behaves as it currently does.

Slightly wasteful in terms of disk usage, but cargo clean clears that up, and also the wastage happens only if you are actively using --verify-crate CRATE. Also, if we're really concerned, we could set TARGET_DIR to /tmp/verus/{sha256(pwd())}/CRATE/, and then it is on tmpfs to handle it, but I think that would be more surprising to people than just a new folder showing up inside target/.