Verifying with `--verify-module` makes `cargo`'s cache think all modules are OK

[jaylorch]

The following code, divided into a Cargo.toml and two .rs files, verifies with cargo verus verify. However, if you then comment out the assume_specification in the second file, and rerun cargo verus verify, the output indicates no error. Verus should realize that main.rs is dependent on that change, and try to re-verify it (and fail). But you have to do cargo clean to see the error.

Cargo.toml:

[package]
name = "test1"
version = "0.1.0"
edition = "2024"

[package.metadata.verus]
verify = true

[dependencies]
vstd = { version = "=0.0.0-2026-08-09-0044" }
num-bigint = { version = "0.5", default-features = false }

src/main.rs:

use vstd::prelude::*;
use num_bigint::BigInt;

mod b;

use crate::b::*;

verus! {

pub fn convert_integer(i: i16)
{
    let m = BigInt::from(i);
    assert(m@ == i);
}

}

fn main() {
    convert_integer(3i16);
    println!("Hello, world!");
}

src/b.rs:

use vstd::prelude::*;
use num_bigint::BigInt;

verus! {

#[verifier::external_type_specification]
#[verifier::external_body]
pub struct ExNumBigInt(num_bigint::BigInt);

pub trait BigIntAdditionalSpecFns {
    spec fn view(&self) -> int;
}

impl BigIntAdditionalSpecFns for BigInt {
    uninterp spec fn view(&self) -> int;
}

pub assume_specification[ <BigInt as core::convert::From<i16>>::from ](i: i16) -> (res: BigInt)
    ensures
        res@ == i,
;

}

[jaylorch]

I'm only able to reproduce this when making the edit to src/b.rs with emacs. If I do it with vi, it doesn't repro. I'm investigating.

[jaylorch]

Aha! Sol figured it out. The issue wasn't with emacs per se, it was with verus-mode / flycheck. Whenever I saved b.rs, flycheck would automatically launch: cargo verus verify --message-format=json -- --verify-module b --expand-errors. That module-only run succeeded and poisoned Cargo’s freshness cache. The subsequent full cargo verus verify reused it and reported success. After cargo clean, full verification failed correctly in main.rs.

So the issue is that a module-only run poisons Cargo's freshness cache, making it think that every module is OK when only the verified module is.

[tjhance]

Is cargo verus verify ... --verify-module supposed to work? I had thought the intent was to only allow --verify-module for cargo verus focus.

[mkovaxx]

Currently focus differs from verify in three aspects:

• verify verifies all (eligible) packages in the build graph, whereas focus only verifies roots.
• verify forwards Verus arguments to all packages, whereas focus defaults to roots only.
• focus places its outputs in a separate directory to prevent "poisoning" full verify runs.

Different but related question: What outputs of the --verify-module run interfere with subsequent full verify runs? Is it the .vir files, or something else?

[parno]

The consensus at today's Verus meeting was that the solution is to have cargo verus verify prohibit the use of --verify-function, --verify-module and --verify-root.