From 4f9e4f5088a3b5fd176a40b3918bb0bff03c8837 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 2 Jul 2026 13:32:29 +0800 Subject: [PATCH 1/8] refactor: use `cargo verus` instead of Verus for verify --- src/main.rs | 11 ++++ src/verus.rs | 172 ++++++++++++++------------------------------------- 2 files changed, 57 insertions(+), 126 deletions(-) diff --git a/src/main.rs b/src/main.rs index 703e6b3..61ef195 100644 --- a/src/main.rs +++ b/src/main.rs @@ -180,6 +180,15 @@ struct VerifyArgs { )] debug: bool, + #[arg( + short = 'f', + long = "focus", + help = "Verify only the selected package contents using cargo-verus focus", + default_value = "false", + action = ArgAction::SetTrue + )] + focus: bool, + #[arg( last = true, help = "Pass-through arguments to the Verus verifier", @@ -450,6 +459,7 @@ fn verify(args: &VerifyArgs) -> Result<(), DynError> { disasm: false, pass_through: args.pass_through.clone(), count_line: args.count_line, + focus: args.focus, verify_only_module_main_only, }; @@ -492,6 +502,7 @@ fn compile(args: &CompileArgs) -> Result<(), DynError> { disasm: args.disasm, pass_through: args.pass_through.clone(), count_line: false, + focus: false, verify_only_module_main_only: false, }; diff --git a/src/verus.rs b/src/verus.rs index c911cc5..ea7ad34 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -33,6 +33,11 @@ pub const VERUS_BIN: &str = "verus.exe"; #[cfg(not(target_os = "windows"))] pub const VERUS_BIN: &str = "verus"; +#[cfg(target_os = "windows")] +pub const CARGO_VERUS_BIN: &str = "cargo-verus.exe"; +#[cfg(not(target_os = "windows"))] +pub const CARGO_VERUS_BIN: &str = "cargo-verus"; + pub const VERUS_HINT_RELEASE: &str = "tools/verus/source/target-verus/release"; pub const VERUS_HINT: &str = "tools/verus/source/target-verus/debug"; pub const VERUS_EVN: &str = "VERUS_PATH"; @@ -82,6 +87,24 @@ pub fn get_verus(release: bool) -> PathBuf { }) } +#[memoize] +pub fn get_cargo_verus(release: bool) -> PathBuf { + executable::locate( + CARGO_VERUS_BIN, + None, + if release { + &[VERUS_HINT_RELEASE, VERUS_HINT] + } else { + &[VERUS_HINT, VERUS_HINT_RELEASE] + }, + ) + .unwrap_or_else(|| { + error!( + "Cannot find the cargo-verus binary, please run `cargo dv bootstrap --upgrade` or add cargo-verus to your PATH" + ); + }) +} + #[memoize] pub fn get_rust_verify(release: bool) -> PathBuf { executable::locate( @@ -235,6 +258,8 @@ pub struct ExtraOptions { pub pass_through: Vec, /// count lines of code pub count_line: bool, + /// use cargo-verus focus instead of cargo-verus verify + pub focus: bool, /// verify-only-module should only apply to the main target, not its dependencies pub verify_only_module_main_only: bool, } @@ -276,6 +301,7 @@ impl ExtraOptions { disasm: self.disasm, pass_through, count_line: self.count_line, + focus: self.focus, verify_only_module_main_only: self.verify_only_module_main_only, } } @@ -1119,140 +1145,32 @@ pub fn compile_target_with_dependencies( pub fn exec_verify( targets: &[VerusTarget], - imports: &[VerusTarget], + _imports: &[VerusTarget], options: &ExtraOptions, ) -> Result<(), DynError> { - let verus = get_verus(options.release); - let z3 = get_z3(); - let extra_imports = imports - .iter() - .map(|target| (target.name.clone(), target.clone())) - .collect::>(); - let out_dir = get_target_dir(); - if !out_dir.exists() { - std::fs::create_dir_all(&out_dir).unwrap_or_else(|e| { - error!("Error creating target directory: {}", e); - }); - } - let deps_dir = out_dir.join(get_build_dir(options.release)).join("deps"); - - let extended_targets = get_dependent_targets_batch(targets, options.release); - - let mut compiled = std::collections::HashSet::new(); - let all_targets = verus_targets(); - - // Process each dependency in extended_targets - for target_name in extended_targets.keys() { - if let Some(target) = all_targets.get(target_name) { - compile_target_with_dependencies(target, &mut compiled, &extended_targets, options); - } - } - - let ts_start = Instant::now(); - // remove the targets that has been compiled - let remaining_targets = targets - .iter() - .filter(|target| { - let name = target.name.replace('-', "_"); - !extended_targets.contains_key(&name) - }) - .collect::>(); - - for target in remaining_targets.iter() { - prepare(target, options.release); - - let cmd = &mut Command::new(&verus); - - // setup the environment - cmd.env("VERUS_PATH", &verus).env("VERUS_Z3_PATH", &z3); - - cmd.args([ - "-L", - &format!("dependency={}", deps_dir.display()), - "-L", - &get_verus_target_dir().display().to_string(), - ]); - - if !target.gen_lifetime { - cmd.arg("--no-lifetime"); - } - - // imported dependencies - let deps = &mut get_local_dependency(target); - deps.extend(extra_imports.clone()); - let all_imports = deps.values().collect::>(); - - // Check and compile missing imports - let mut missing_targets = Vec::new(); - for imp in all_imports.iter() { - if !imp.library_proof().exists() || !imp.library_path().exists() { - missing_targets.push((*imp).clone()); - } - } - - if !missing_targets.is_empty() { - info!( - "Missing verification files for dependencies: {:?}", - missing_targets.iter().map(|t| &t.name).collect::>() - ); - info!("Automatically compiling missing dependencies..."); - - let mut compiled = std::collections::HashSet::new(); - let missing_targets_map: IndexMap = missing_targets - .iter() - .map(|t| (t.name.clone(), t.clone())) - .collect(); - - for target_item in &missing_targets { - compile_target_with_dependencies( - target_item, - &mut compiled, - &missing_targets_map, - options, - ); - } - } - - check_imports_compiled(all_imports.as_slice()).unwrap_or_else(|e| { - error!("Error during verification: {}", e); - }); - cmd_push_import(cmd, all_imports.as_slice()); - - // import external crates - let externs = get_remote_dependency(target, options.release); - check_externs(&externs).unwrap_or_else(|e| { - error!("Error during verification: {}", e); - }); - cmd_push_externs(cmd, &externs); + for target in targets.iter() { + let ts_start = Instant::now(); + let cmd = &mut Command::new(get_cargo_verus(options.release)); + cmd.arg(if options.focus { "focus" } else { "verify" }) + .arg("-p") + .arg(&target.name); - // extra options + let mut verus_args = Vec::new(); if options.log { - cmd.arg("--log-all"); + verus_args.push("--log-all".to_string()); } if options.trace { cmd.env("RUST_BACKTRACE", "full"); - cmd.arg("--trace"); + verus_args.push("--trace".to_string()); } if options.count_line { - cmd.arg("--emit=dep-info"); + verus_args.push("--emit=dep-info".to_string()); } - - // input file - let target_file = target.root_file(); - let crate_type = target.crate_type(); - cmd.arg(target_file) - .arg(format!("--crate-type={}", crate_type)) - .arg("--expand-errors") - .arg(format!("--multiple-errors={}", options.max_errors)) - .args(&options.pass_through) - .arg("--") - .arg("-C") - .arg(format!("metadata={}", target.name)); - - for feature in target.features.iter() { - cmd.args(["--cfg", &format!("feature=\"{}\"", feature)]); + verus_args.push(format!("--multiple-errors={}", options.max_errors)); + verus_args.extend(options.pass_through.clone()); + if !verus_args.is_empty() { + cmd.arg("--").args(verus_args); } - cmd.stdout(Stdio::inherit()); info!( " {} {} {}", @@ -1262,7 +1180,6 @@ pub fn exec_verify( ); debug!(">> {:?}", cmd); - // run the command let status = cmd.status().unwrap_or_else(|e| { error!("Error during verification: {}", e); }); @@ -1288,7 +1205,8 @@ pub fn exec_verify( if options.count_line { let verus_root = install::verus_dir(); let line_count_dir = verus_root.join("source/tools/line_count"); - let dependency_file = env::current_dir()?.join("lib.d"); + let current_dir = env::current_dir()?; + let dependency_file = current_dir.join("lib.d"); env::set_current_dir(&line_count_dir)?; let mut cargo_cmd = Command::new("cargo"); cargo_cmd @@ -1298,7 +1216,9 @@ pub fn exec_verify( .arg("-p"); println!("Counting lines for target: {}", target.name); - cargo_cmd.status()?; + let line_count_result = cargo_cmd.status(); + env::set_current_dir(current_dir)?; + line_count_result?; fs::remove_file(&dependency_file)?; } } From fe17683495f3e3b657da60adceb7b418f0cd6ed2 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 2 Jul 2026 15:32:16 +0800 Subject: [PATCH 2/8] refactor: use `cargo verus` for instead of Verus for compile --- src/verus.rs | 388 ++++++--------------------------------------------- 1 file changed, 41 insertions(+), 347 deletions(-) diff --git a/src/verus.rs b/src/verus.rs index ea7ad34..009444e 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -14,10 +14,7 @@ use cargo_metadata; use cargo_metadata::CrateType; use crate::commands::CargoBuildExterns; -use crate::generator::Generative; -use crate::{ - commands, dep_tree, executable, files, fingerprint, generator, projects, serialization, -}; +use crate::{commands, dep_tree, executable, files, fingerprint, projects, serialization}; pub type DynError = Box; @@ -677,34 +674,6 @@ pub fn get_local_dependency(target: &VerusTarget) -> IndexMap IndexMap { - let mut deps = get_local_dependency(target); - let order = resolve_deps_cached(target, release).full_externs; - deps.sort_by(|a, _, b, _| { - let x = order.get_index_of(a).unwrap_or(usize::MAX); - let y = order.get_index_of(b).unwrap_or(usize::MAX); - x.cmp(&y) - }); - deps -} - -pub fn get_dependent_targets_batch( - targets: &[VerusTarget], - release: bool, -) -> IndexMap { - let mut deps = IndexMap::new(); - for target in targets.iter() { - deps.extend(get_local_dependency(target)); - } - let order = resolve_deps_cached(targets.first().unwrap(), release).full_externs; - deps.sort_by(|a, _, b, _| { - let x = order.get_index_of(a).unwrap_or(usize::MAX); - let y = order.get_index_of(b).unwrap_or(usize::MAX); - x.cmp(&y) - }); - deps -} - pub fn get_remote_dependency(target: &VerusTarget, release: bool) -> IndexMap { let externs = resolve_deps_cached(target, release).renamed_full_externs(); @@ -731,37 +700,6 @@ pub fn get_remote_dependency(target: &VerusTarget, release: bool) -> IndexMap Result<(), DynError> { - for imp in imports.iter() { - if !imp.library_proof().exists() { - return Err(format!( - "Cannot find the proof file at `{}` for `{}`", - imp.library_proof().display(), - imp.name - ) - .into()); - } - if !imp.library_path().exists() { - return Err(format!( - "Cannot find the library file at `{}` for `{}`", - imp.library_path().display(), - imp.name - ) - .into()); - } - } - Ok(()) -} - pub fn check_externs(externs: &IndexMap) -> Result<(), DynError> { for (name, path) in externs.iter() { if !Path::new(path).exists() { @@ -826,45 +764,6 @@ pub fn resolve_deps_cached(target: &VerusTarget, release: bool) -> serialization } } -pub fn gen_extern_crates(target: &VerusTarget, release: bool) { - let externs = resolve_deps_cached(target, release); - let mut tmpl = generator::ExternCratesTemplate { crates: Vec::new() }; - - let local_deps = target - .dependencies - .iter() - .filter(|dep| dep.path.is_some()) - .map(|dep| dep.name.replace('-', "_")) - .collect::>(); - - for name in externs.full_externs.keys() { - if system_crates().contains(name.as_str()) { - // Skip system crates - continue; - } - - if local_deps.contains(name) { - // Skip local dependencies - continue; - } - - tmpl.crates.push(generator::CrateInfo { - name: name.clone(), - alias: None, - }); - } - - let deps_path = get_target_dir().join(format!("{}.deps.toml", target.name)); - let deps_time = files::modify_time(deps_path); - let crates_path = get_target_dir().join(format!("{}.extern_crates.rs", target.name)); - - tmpl.save_if(&crates_path, &deps_time); -} - -pub fn prepare(target: &VerusTarget, release: bool) { - gen_extern_crates(target, release); -} - /// Move files from workspace `.verus-log` root into a per-crate subdirectory. fn move_verus_log_files(crate_name: &str) { let workspace_root = get_workspace_root(); @@ -917,232 +816,6 @@ fn move_verus_log_files(crate_name: &str) { } } -fn get_build_dir(release: bool) -> &'static str { - if release { - "release" - } else { - "debug" - } -} - -/// Compile a single target using the Verus verifier. -/// -/// This function directly invokes the Verus compiler on a single target. -/// It handles dependency setup, external crate linking, and compilation options. -/// It does NOT recursively compile dependencies, an error will occur if dependencies -/// are missing. To compile a target along with its dependencies, -/// - use `compile_target_with_dependencies` for that. -/// -/// # Arguments -/// -/// * `target` - The target to compile -/// * `imports` - Additional targets to import (not auto-discovered) -/// * `options` - Compilation options (log, trace, release, max_errors, disasm, pass_through) -pub fn compile_single_target( - target: &VerusTarget, - imports: &[VerusTarget], - options: &ExtraOptions, -) -> Result<(), DynError> { - let ts_start = Instant::now(); - - let verus = get_verus(options.release); - let z3 = get_z3(); - let extra_imports = imports - .iter() - .map(|target| (target.name.clone(), target.clone())) - .collect::>(); - - let out_dir = get_target_dir(); - if !out_dir.exists() { - std::fs::create_dir_all(&out_dir).unwrap_or_else(|e| { - error!("Error creating target directory: {}", e); - }); - } - let deps_dir = out_dir.join(get_build_dir(options.release)).join("deps"); - - prepare(target, options.release); - - let mut deps = get_local_dependency(target); - let dep_rebuilt = deps.values().into_iter().any(|t| t.rebuilt == true); - - if !dep_rebuilt && target.is_fresh(&verus_targets()) { - info!( - "[Fresh] `{}` is up to date, skipping verification", - target.name - ); - return Ok(()); - } - - let cmd = &mut Command::new(&verus); - - // setup the environment - cmd.env("VERUS_PATH", &verus).env("VERUS_Z3_PATH", &z3); - cmd.args([ - "-L", - &format!("dependency={}", deps_dir.display()), - "-L", - &get_verus_target_dir().display().to_string(), - ]); - - if !target.gen_lifetime { - cmd.arg("--no-lifetime"); - } - - // output options - cmd.arg("--compile") - .arg("--export") - .arg(target.library_proof()); - - // imported dependencies - deps.extend(extra_imports.clone()); - let all_imports = deps.values().collect::>(); - check_imports_compiled(all_imports.as_slice())?; - cmd_push_import(cmd, all_imports.as_slice()); - - // import external crates - let externs = get_remote_dependency(target, options.release); - check_externs(&externs).unwrap_or_else(|e| { - error!("Error during verification: {}", e); - }); - cmd_push_externs(cmd, &externs); - - // extra options - if options.log { - cmd.arg("--log-all"); - } - - if options.trace { - cmd.env("RUST_BACKTRACE", "full"); - cmd.arg("--trace"); - } - - if options.release { - cmd.args(["-C", "opt-level=2"]); - } else { - cmd.args(["-C", "opt-level=0"]); - } - - // input file - let target_file = target.root_file(); - let crate_type = target.crate_type(); - cmd.arg(target_file) - .arg(format!("--crate-type={}", crate_type)) - .arg("--expand-errors") - .arg(format!("--multiple-errors={}", options.max_errors)) - .arg("-o") - .arg(target.library_path()) - .arg("-V") - .arg("use-crate-name") - .args(&options.pass_through) - .arg("--") - .arg("-C") - .arg(format!("metadata={}", target.name)); - - for feature in target.features.iter() { - cmd.args(["--cfg", &format!("feature=\"{}\"", feature)]); - } - cmd.stdout(Stdio::inherit()); - - info!( - " {} {} {}", - "Verifying (and compiling)".bold().green(), - target.name.white(), - target.version.white() - ); - debug!(">> {:?}", cmd); - - // run the command - let status = cmd.status().unwrap_or_else(|e| { - error!("Error during compilation: {}", e); - }); - - if status.success() { - // duration - let duration = ts_start.elapsed(); - info!( - " {} {} {} in {:.2}s", - "Verified".bold().green(), - target.name.white(), - target.version.white(), - duration.as_secs_f64() - ); - - // success - target.save_library_proof_timestamp(&verus_targets()); - - // disassemble the output - if options.disasm { - disassemble(target).unwrap_or_else(|e| { - error!("Error during disassembly: {}", e); - }); - } - - if options.log { - move_verus_log_files(&target.name); - } - - return Ok(()); - } - - // failure - Err(format!("Error during compilation: `{}`", target.name,).into()) -} - -/// Recursively compile a target and all its dependencies in the correct order. -/// -/// This function handles the recursive compilation of a target and its dependencies, -/// ensuring proper topological ordering. It ensures that all dependencies of a target -/// are compiled before the target itself. It also maintains a set of already-compiled -/// targets to avoid redundant compilation. -/// -/// # Arguments -/// -/// * `target` - The target to compile along with its dependencies -/// * `compiled` - Set tracking already-compiled target names (modified in-place) -/// * `scope_targets` - Map of targets allowed to be compiled (acts as a scope limiter). -/// Only targets in this map will actually be compiled, even if they're in dependencies. -/// * `options` - Extra compilation options -/// -/// # Behavior -/// -/// 1. Returns early if the target is already in the `compiled` set -/// 2. Recursively compiles all dependencies that are in `extended_targets` -/// 3. Compiles the target itself if it's in `extended_targets` -/// 4. Marks the target as compiled to prevent duplicate work -pub fn compile_target_with_dependencies( - target: &VerusTarget, - compiled: &mut std::collections::HashSet, - scope_targets: &IndexMap, - options: &ExtraOptions, -) { - let all_targets = verus_targets(); - - if compiled.contains(&target.name) { - return; - } - - // First compile all dependencies that exist in scope - for dep in &target.dependencies { - if scope_targets.contains_key(&dep.name) { - if let Some(dep_target) = all_targets.get(&dep.name) { - compile_target_with_dependencies(dep_target, compiled, scope_targets, options); - } - } - } - - // Then compile this target if it's in scope - if scope_targets.contains_key(&target.name) { - let target_options = options.for_dependency(); - compile_single_target(target, &vec![], &target_options).unwrap_or_else(|e| { - error!( - "Unable to build the dependent proof: `{}` ({})", - target.name, e - ); - }); - compiled.insert(target.name.clone()); - } -} - pub fn exec_verify( targets: &[VerusTarget], _imports: &[VerusTarget], @@ -1259,7 +932,7 @@ pub fn disassemble(target: &VerusTarget) -> Result<(), DynError> { pub fn exec_compile( targets: &[VerusTarget], - imports: &[VerusTarget], + _imports: &[VerusTarget], options: &ExtraOptions, ) -> Result<(), DynError> { let out_dir = get_target_dir(); @@ -1269,28 +942,49 @@ pub fn exec_compile( }); } - let extended_targets = get_dependent_targets_batch(targets, options.release); - let mut compiled = std::collections::HashSet::new(); - let all_targets = verus_targets(); + for target in targets.iter() { + let cmd = &mut Command::new(get_cargo_verus(options.release)); + cmd.arg("build").arg("-p").arg(&target.name); + if options.release { + cmd.arg("--release"); + } - // Process each dependency in extended_targets - for target_name in extended_targets.keys() { - if let Some(target) = all_targets.get(target_name) { - compile_target_with_dependencies(target, &mut compiled, &extended_targets, options); + let mut verus_args = Vec::new(); + if options.log { + verus_args.push("--log-all".to_string()); + } + if options.trace { + cmd.env("RUST_BACKTRACE", "full"); + verus_args.push("--trace".to_string()); + } + verus_args.push(format!("--multiple-errors={}", options.max_errors)); + verus_args.extend(options.pass_through.clone()); + if !verus_args.is_empty() { + cmd.arg("--").args(verus_args); } - } - // remove the targets that has been compiled - let remaining_targets = targets - .iter() - .filter(|target| { - let name = target.name.replace('-', "_"); - !extended_targets.contains_key(&name) - }) - .collect::>(); + info!( + " {} {} {}", + "Compiling".bold().green(), + target.name.white(), + target.version.white() + ); + debug!(">> {:?}", cmd); - for target in remaining_targets.iter() { - compile_single_target(target, imports, options)?; + let status = cmd.status().unwrap_or_else(|e| { + error!("Error during compilation: {}", e); + }); + + if status.success() { + info!( + " {} {} {}", + "Compiled".bold().green(), + target.name.white(), + target.version.white() + ); + } else { + error!("Compilation failed for target {}", target.name); + } } Ok(()) From 4df718e91a1b1395ef6897d6eb3bf83174aa7681 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 2 Jul 2026 16:15:42 +0800 Subject: [PATCH 3/8] fix: return early for line count --- src/verus.rs | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/verus.rs b/src/verus.rs index 009444e..f614372 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -2,7 +2,6 @@ use colored::Colorize; use indexmap::IndexMap; use memoize::memoize; use std::collections::{HashMap, HashSet}; -use std::env; use std::fs::{self, File}; use std::hash::Hash; use std::io::{Read, Write}; @@ -822,6 +821,15 @@ pub fn exec_verify( options: &ExtraOptions, ) -> Result<(), DynError> { for target in targets.iter() { + if options.count_line { + eprintln!( + "Error: --count-line is currently unsupported with cargo-verus for target {}", + target.name + ); + // TODO: Re-enable this path once cargo-verus can produce the dep-info expected by Verus' line_count tool. + return Err("--count-line is currently unsupported with cargo-verus".into()); + } + let ts_start = Instant::now(); let cmd = &mut Command::new(get_cargo_verus(options.release)); cmd.arg(if options.focus { "focus" } else { "verify" }) @@ -878,9 +886,9 @@ pub fn exec_verify( if options.count_line { let verus_root = install::verus_dir(); let line_count_dir = verus_root.join("source/tools/line_count"); - let current_dir = env::current_dir()?; + let current_dir = std::env::current_dir()?; let dependency_file = current_dir.join("lib.d"); - env::set_current_dir(&line_count_dir)?; + std::env::set_current_dir(&line_count_dir)?; let mut cargo_cmd = Command::new("cargo"); cargo_cmd .arg("run") @@ -890,7 +898,7 @@ pub fn exec_verify( println!("Counting lines for target: {}", target.name); let line_count_result = cargo_cmd.status(); - env::set_current_dir(current_dir)?; + std::env::set_current_dir(current_dir)?; line_count_result?; fs::remove_file(&dependency_file)?; } @@ -935,13 +943,6 @@ pub fn exec_compile( _imports: &[VerusTarget], options: &ExtraOptions, ) -> Result<(), DynError> { - let out_dir = get_target_dir(); - if !out_dir.exists() { - std::fs::create_dir_all(&out_dir).unwrap_or_else(|e| { - error!("Error creating target directory: {}", e); - }); - } - for target in targets.iter() { let cmd = &mut Command::new(get_cargo_verus(options.release)); cmd.arg("build").arg("-p").arg(&target.name); From 9cb7d58cbb831fe8c71d8eaca95b79de096929a7 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 2 Jul 2026 16:47:57 +0800 Subject: [PATCH 4/8] chore: remove unused args --- src/main.rs | 8 +++----- src/verus.rs | 12 ++---------- 2 files changed, 5 insertions(+), 15 deletions(-) diff --git a/src/main.rs b/src/main.rs index 61ef195..0151f57 100644 --- a/src/main.rs +++ b/src/main.rs @@ -183,7 +183,7 @@ struct VerifyArgs { #[arg( short = 'f', long = "focus", - help = "Verify only the selected package contents using cargo-verus focus", + help = "Run verification even if it is verified before", default_value = "false", action = ArgAction::SetTrue )] @@ -443,7 +443,6 @@ struct FmtArgs { fn verify(args: &VerifyArgs) -> Result<(), DynError> { let targets = args.targets.clone(); - let imports = args.imports.clone(); // verify-only-module should only apply to the main target // Conditions: exactly one target AND pass_through contains "--verify-only-module" let verify_only_module_main_only = targets.len() == 1 @@ -463,7 +462,7 @@ fn verify(args: &VerifyArgs) -> Result<(), DynError> { verify_only_module_main_only, }; - verus::exec_verify(&targets, &imports, &options) + verus::exec_verify(&targets, &options) } fn doc(args: &DocArgs) -> Result<(), DynError> { @@ -493,7 +492,6 @@ fn bootstrap(args: &BootstrapArgs) -> Result<(), DynError> { fn compile(args: &CompileArgs) -> Result<(), DynError> { let targets = args.targets.clone(); - let imports = args.imports.clone(); let options = verus::ExtraOptions { max_errors: args.max_errors, log: args.log, @@ -506,7 +504,7 @@ fn compile(args: &CompileArgs) -> Result<(), DynError> { verify_only_module_main_only: false, }; - verus::exec_compile(&targets, &imports, &options) + verus::exec_compile(&targets, &options) } fn fingerprint(args: &FingerprintArgs) -> Result<(), DynError> { diff --git a/src/verus.rs b/src/verus.rs index f614372..3ed25c7 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -815,11 +815,7 @@ fn move_verus_log_files(crate_name: &str) { } } -pub fn exec_verify( - targets: &[VerusTarget], - _imports: &[VerusTarget], - options: &ExtraOptions, -) -> Result<(), DynError> { +pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> { for target in targets.iter() { if options.count_line { eprintln!( @@ -938,11 +934,7 @@ pub fn disassemble(target: &VerusTarget) -> Result<(), DynError> { Ok(()) } -pub fn exec_compile( - targets: &[VerusTarget], - _imports: &[VerusTarget], - options: &ExtraOptions, -) -> Result<(), DynError> { +pub fn exec_compile(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> { for target in targets.iter() { let cmd = &mut Command::new(get_cargo_verus(options.release)); cmd.arg("build").arg("-p").arg(&target.name); From 71c7efc279be2ca21e907d5ed09decb7d7478934 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 2 Jul 2026 17:10:42 +0800 Subject: [PATCH 5/8] refactor: use `cargo clean` for clean --- src/main.rs | 29 ++++-------------------- src/verus.rs | 62 +++++----------------------------------------------- 2 files changed, 9 insertions(+), 82 deletions(-) diff --git a/src/main.rs b/src/main.rs index 0151f57..01b5cee 100644 --- a/src/main.rs +++ b/src/main.rs @@ -46,7 +46,7 @@ enum Commands { #[command( name = "clean", - about = "Clean build artefacts produced by `cargo dv compile`", + about = "Run `cargo clean` for the workspace", alias = "cl" )] Clean(CleanArgs), @@ -309,22 +309,7 @@ struct CompileArgs { } #[derive(Parser, Debug)] -struct CleanArgs { - #[arg( - short = 't', - long = "targets", - value_parser = verus::find_target, - help = "The targets to clean", - num_args = 0.., - action = ArgAction::Append)] - targets: Vec, - #[arg( - long = "all", - help = "Clean verification artifacts for all workspace targets", - default_value = "false", - action = ArgAction::SetTrue)] - all: bool, -} +struct CleanArgs {} #[derive(Parser, Debug)] struct FingerprintArgs { @@ -515,14 +500,8 @@ fn fingerprint(args: &FingerprintArgs) -> Result<(), DynError> { Ok(()) } -fn clean(args: &CleanArgs) -> Result<(), DynError> { - let targets = args.targets.clone(); - // if --all provided, pass empty targets with all=true to verus - if args.all { - verus::exec_clean(&[], true) - } else { - verus::exec_clean(&targets, false) - } +fn clean(_args: &CleanArgs) -> Result<(), DynError> { + verus::exec_clean() } fn list_targets(_args: &ListTargetsArgs) -> Result<(), DynError> { diff --git a/src/verus.rs b/src/verus.rs index 3ed25c7..79e58d5 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -983,65 +983,13 @@ pub fn exec_compile(targets: &[VerusTarget], options: &ExtraOptions) -> Result<( Ok(()) } -/// Clean build artefacts produced by `exec_compile`. -pub fn exec_clean(targets: &[VerusTarget], all: bool) -> Result<(), DynError> { - let out_dir = get_target_dir(); - - let to_clean: Vec = if all || targets.is_empty() { - // clean all known targets - verus_targets().values().cloned().collect() +pub fn exec_clean() -> Result<(), DynError> { + let status = Command::new("cargo").arg("clean").status()?; + if status.success() { + Ok(()) } else { - targets.iter().cloned().collect() - }; - - for target in to_clean.iter() { - // remove .verusdata - let proof = target.library_proof(); - if proof.exists() { - info!("Removing {}", proof.display()); - std::fs::remove_file(&proof).unwrap_or_else(|e| { - warn!("Failed to remove {}: {}", proof.display(), e); - }); - } - - // remove .verusdata.timestamp - let proof_ts = target.library_proof_timestamp(); - if proof_ts.exists() { - info!("Removing {}", proof_ts.display()); - std::fs::remove_file(&proof_ts).unwrap_or_else(|e| { - warn!("Failed to remove {}: {}", proof_ts.display(), e); - }); - } - - // remove lib{name}.rlib - let lib = target.library_path(); - if lib.exists() { - info!("Removing {}", lib.display()); - std::fs::remove_file(&lib).unwrap_or_else(|e| { - warn!("Failed to remove {}: {}", lib.display(), e); - }); - } - - // remove generated extern_crates - let extern_crates_path = out_dir.join(format!("{}.extern_crates.rs", target.name)); - if extern_crates_path.exists() { - info!("Removing {}", extern_crates_path.display()); - std::fs::remove_file(&extern_crates_path).unwrap_or_else(|e| { - warn!("Failed to remove {}: {}", extern_crates_path.display(), e); - }); - } - - // remove deps.toml - let deps_toml_path = out_dir.join(format!("{}.deps.toml", target.name)); - if deps_toml_path.exists() { - info!("Removing {}", deps_toml_path.display()); - std::fs::remove_file(&deps_toml_path).unwrap_or_else(|e| { - warn!("Failed to remove {}: {}", deps_toml_path.display(), e); - }); - } + Err("cargo clean failed".into()) } - - Ok(()) } pub mod install { From 3f34c41d18859dab8cc2e987612f04c5357def09 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 2 Jul 2026 17:36:28 +0800 Subject: [PATCH 6/8] doc: update help doc for `focus` --- src/main.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main.rs b/src/main.rs index 01b5cee..8de236c 100644 --- a/src/main.rs +++ b/src/main.rs @@ -183,7 +183,7 @@ struct VerifyArgs { #[arg( short = 'f', long = "focus", - help = "Run verification even if it is verified before", + help = "Verify root crates without re-checking dependency proofs", default_value = "false", action = ArgAction::SetTrue )] From 6f54e0757b42926b9f4cfe918714dda40e722021 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 2 Jul 2026 17:43:39 +0800 Subject: [PATCH 7/8] feat: align with `cargo verus` when no target given --- src/verus.rs | 63 ++++++++++++++++++++++++++++++++++------------------ 1 file changed, 42 insertions(+), 21 deletions(-) diff --git a/src/verus.rs b/src/verus.rs index 79e58d5..dd146c0 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -37,6 +37,7 @@ pub const CARGO_VERUS_BIN: &str = "cargo-verus"; pub const VERUS_HINT_RELEASE: &str = "tools/verus/source/target-verus/release"; pub const VERUS_HINT: &str = "tools/verus/source/target-verus/debug"; pub const VERUS_EVN: &str = "VERUS_PATH"; +pub const CARGO_VERUS_ENV: &str = "CARGO_VERUS_PATH"; #[cfg(target_os = "windows")] pub const VERUSFMT_BIN: &str = "verusfmt.exe"; @@ -87,7 +88,7 @@ pub fn get_verus(release: bool) -> PathBuf { pub fn get_cargo_verus(release: bool) -> PathBuf { executable::locate( CARGO_VERUS_BIN, - None, + Some(CARGO_VERUS_ENV), if release { &[VERUS_HINT_RELEASE, VERUS_HINT] } else { @@ -96,7 +97,7 @@ pub fn get_cargo_verus(release: bool) -> PathBuf { ) .unwrap_or_else(|| { error!( - "Cannot find the cargo-verus binary, please run `cargo dv bootstrap --upgrade` or add cargo-verus to your PATH" + "Cannot find the cargo-verus binary, please run `cargo dv bootstrap --upgrade`, set CARGO_VERUS_PATH, or add cargo-verus to your PATH" ); }) } @@ -816,21 +817,19 @@ fn move_verus_log_files(crate_name: &str) { } pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> { - for target in targets.iter() { - if options.count_line { - eprintln!( - "Error: --count-line is currently unsupported with cargo-verus for target {}", - target.name - ); - // TODO: Re-enable this path once cargo-verus can produce the dep-info expected by Verus' line_count tool. - return Err("--count-line is currently unsupported with cargo-verus".into()); - } + if options.count_line { + eprintln!("Error: --count-line is currently unsupported with cargo-verus"); + // TODO: Re-enable this path once cargo-verus can produce the dep-info expected by Verus' line_count tool. + return Err("--count-line is currently unsupported with cargo-verus".into()); + } + let run = |target: Option<&VerusTarget>| -> Result<(), DynError> { let ts_start = Instant::now(); let cmd = &mut Command::new(get_cargo_verus(options.release)); - cmd.arg(if options.focus { "focus" } else { "verify" }) - .arg("-p") - .arg(&target.name); + cmd.arg(if options.focus { "focus" } else { "verify" }); + if let Some(target) = target { + cmd.arg("-p").arg(&target.name); + } let mut verus_args = Vec::new(); if options.log { @@ -852,8 +851,11 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<() info!( " {} {} {}", "Verifying".bold().green(), - target.name.white(), - target.version.white() + target + .map(|t| t.name.as_str()) + .unwrap_or("workspace") + .white(), + target.map(|t| t.version.as_str()).unwrap_or("").white() ); debug!(">> {:?}", cmd); @@ -867,16 +869,23 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<() info!( " {} {} {} in {:.2}s", "Verified".bold().green(), - target.name.white(), - target.version.white(), + target + .map(|t| t.name.as_str()) + .unwrap_or("workspace") + .white(), + target.map(|t| t.version.as_str()).unwrap_or("").white(), duration.as_secs_f64() ); - if options.log { + if options.log && target.is_some() { + let target = target.unwrap(); move_verus_log_files(&target.name); } } else { - error!("Verification failed for target {}", target.name); + error!( + "Verification failed for {}", + target.map(|t| t.name.as_str()).unwrap_or("workspace") + ); } if options.count_line { @@ -892,12 +901,24 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<() .arg(&dependency_file) .arg("-p"); - println!("Counting lines for target: {}", target.name); + println!( + "Counting lines for {}", + target.map(|t| t.name.as_str()).unwrap_or("workspace") + ); let line_count_result = cargo_cmd.status(); std::env::set_current_dir(current_dir)?; line_count_result?; fs::remove_file(&dependency_file)?; } + Ok(()) + }; + + if targets.is_empty() { + run(None)?; + } else { + for target in targets.iter() { + run(Some(target))?; + } } Ok(()) } From dd97863013c038b0b58474104a8af4aa427e5693 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 2 Jul 2026 17:48:02 +0800 Subject: [PATCH 8/8] doc: update README --- README.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 4830f54..d87a94c 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,12 @@ # Rust Deductive Verifier +`cargo dv` is a thin project-specific wrapper around `cargo-verus`. +Verification and build commands are delegated to `cargo-verus verify`, +`cargo-verus focus`, and `cargo-verus build`, +while `cargo dv` keeps a few repository conveniences on top, +such as bootstrapping the Verus toolchain, formatting Verus/Rust sources, +generating docs, and running pre-commit checks. + ## Deployment 1. Put this repository as a directory `dv` in the root of your Rust project. @@ -37,4 +44,3 @@ pre-commit = "cargo pre-commit" [logging] verbose = true ``` -