[cargo-verus] fix: mitigate known caching issue (#2794)

Author: mkovaxx

source/.cargo/config.toml

@@ -9,6 +9,7 @@ rustflags = [
 ]
 
 [env]
+CARGO_UNSTABLE_CHECKSUM_FRESHNESS = "true"
 RUSTC_BOOTSTRAP = "1"
 RUST_MIN_STACK = "20971520"
 VERUS_IN_VARGO = "1"

source/cargo-verus/src/subcommands.rs

@@ -15,8 +15,10 @@ use crate::toolchains::{self, TOOLCHAINS, is_matching_known_and_used};
 use crate::vstd_build::{VstdBuild, build_vstd};
 
 pub const CARGO_DEFAULT_LIB_METADATA: &str = "__CARGO_DEFAULT_LIB_METADATA";
+pub const CARGO_UNSTABLE_CHECKSUM_FRESHNESS: &str = "CARGO_UNSTABLE_CHECKSUM_FRESHNESS";
 
 pub const RUSTC_WRAPPER: &str = "RUSTC_WRAPPER";
+pub const RUSTC_BOOTSTRAP: &str = "RUSTC_BOOTSTRAP";
 
 pub const VERUS_DRIVER_ARGS: &str = " __VERUS_DRIVER_ARGS__";
 pub const VERUS_DRIVER_ARGS_FOR: &str = " __VERUS_DRIVER_ARGS_FOR_";
@@ -426,6 +428,8 @@ fn make_cargo_plan(
     env_overrides.insert(VERUS_DRIVER_VIA_CARGO.to_owned(), "1".to_owned());
     // See https://github.com/rust-lang/cargo/blob/94aa7fb1321545bbe922a87cb11f5f4559e3be63/src/cargo/core/compiler/fingerprint/mod.rs#L71
     env_overrides.insert(CARGO_DEFAULT_LIB_METADATA.to_owned(), "verus".to_owned());
+    env_overrides.insert(CARGO_UNSTABLE_CHECKSUM_FRESHNESS.to_owned(), "true".to_owned());
+    env_overrides.insert(RUSTC_BOOTSTRAP.to_owned(), "1".to_owned());
 
     let common_verus_driver_args = pack_verus_driver_args_for_env(common_verus_driver_args.iter());
 

source/cargo-verus/src/test_utils.rs

@@ -5,9 +5,9 @@ use std::path::Path;
 use crate::subcommands::CargoRunPlan;
 
 pub use crate::subcommands::{
-    CARGO_DEFAULT_LIB_METADATA, RUSTC_WRAPPER, VERUS_DRIVER_ARGS, VERUS_DRIVER_ARGS_FOR,
-    VERUS_DRIVER_ARGS_SEP, VERUS_DRIVER_IS_BUILTIN, VERUS_DRIVER_IS_BUILTIN_MACROS,
-    VERUS_DRIVER_VERIFY, VERUS_DRIVER_VIA_CARGO,
+    CARGO_DEFAULT_LIB_METADATA, CARGO_UNSTABLE_CHECKSUM_FRESHNESS, RUSTC_BOOTSTRAP, RUSTC_WRAPPER,
+    VERUS_DRIVER_ARGS, VERUS_DRIVER_ARGS_FOR, VERUS_DRIVER_ARGS_SEP, VERUS_DRIVER_IS_BUILTIN,
+    VERUS_DRIVER_IS_BUILTIN_MACROS, VERUS_DRIVER_VERIFY, VERUS_DRIVER_VIA_CARGO,
 };
 
 pub struct MockWorkspace {

source/cargo-verus/tests/test_verify.rs

@@ -1,8 +1,9 @@
 use cargo_verus::{
     BIN_NAME, ExecutionPlan, plan_execution,
     test_utils::{
-        CARGO_DEFAULT_LIB_METADATA, MockDep, MockPackage, MockWorkspace, RUSTC_WRAPPER,
-        VERUS_DRIVER_ARGS, VERUS_DRIVER_ARGS_FOR, VERUS_DRIVER_VERIFY, VERUS_DRIVER_VIA_CARGO,
+        CARGO_DEFAULT_LIB_METADATA, CARGO_UNSTABLE_CHECKSUM_FRESHNESS, MockDep, MockPackage,
+        MockWorkspace, RUSTC_BOOTSTRAP, RUSTC_WRAPPER, VERUS_DRIVER_ARGS, VERUS_DRIVER_ARGS_FOR,
+        VERUS_DRIVER_VERIFY, VERUS_DRIVER_VIA_CARGO,
     },
 };
 
@@ -23,6 +24,8 @@ fn crate_optin_workdir() {
 
     cargo_plan.assert_env_has(RUSTC_WRAPPER);
     cargo_plan.assert_env_sets(CARGO_DEFAULT_LIB_METADATA, "verus");
+    cargo_plan.assert_env_sets(CARGO_UNSTABLE_CHECKSUM_FRESHNESS, "true");
+    cargo_plan.assert_env_sets(RUSTC_BOOTSTRAP, "1");
     cargo_plan.assert_env_sets(VERUS_DRIVER_VIA_CARGO, "1");
     cargo_plan.assert_env_sets_key_prefix(&verify_crate_prefix, "1");
 }