From 81ce2a4ecfbffd7ec4c4bcfe760154beb45f9cbc Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 20 Aug 2026 16:05:23 +0800 Subject: [PATCH] feat: add `focus` command due to Verus update --- README.md | 28 +++++++++++++++++++++++++--- src/main.rs | 38 ++++++++++++++++++-------------------- src/verus.rs | 42 ++++++++++++++++++++---------------------- 3 files changed, 63 insertions(+), 45 deletions(-) diff --git a/README.md b/README.md index 009a45e..4a84204 100644 --- a/README.md +++ b/README.md @@ -29,18 +29,40 @@ pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --" cargo dv verify --targets ... ``` +### Verification modes + +Use `verify` for complete verification of the selected targets and their +verification dependencies: + +```bash +cargo dv verify --targets ostd +``` + +Use `focus` while iterating on root targets. Dependencies are still built so +their types and specifications are available, but their proofs are not +re-checked: + +```bash +cargo dv focus --targets ostd +``` + +Focused artifacts are kept separate by `cargo-verus`; run a complete `verify` +before committing. + ### Cargo features and Verus arguments -The `verify` and `build` commands accept Cargo's standard feature options: +The `verify`, `focus`, and `build` commands accept Cargo's standard feature options: `-F`/`--features`, `--all-features`, and `--no-default-features`. DV forwards these options to `cargo-verus` before the verifier argument separator. Arguments after `--` continue to be passed directly to Verus. For example, this enables the `irc11` Cargo feature while asking Verus to check -only one module: +only one module. Partial verification selectors such as `--verify-module`, +`--verify-only-module`, `--verify-function`, and `--verify-root` require the +`focus` command: ```bash -cargo dv verify --targets ostd --features irc11 -- \ +cargo dv focus --targets ostd --features irc11 -- \ --verify-only-module sync::rcu ``` diff --git a/src/main.rs b/src/main.rs index 33482d3..a79cc41 100644 --- a/src/main.rs +++ b/src/main.rs @@ -22,7 +22,13 @@ enum Commands { about = "Verify the verification targets", alias = "v" )] - Verify(VerifyArgs), + Verify(VerificationArgs), + + #[command( + name = "focus", + about = "Verify root targets without re-checking dependency proofs" + )] + Focus(VerificationArgs), #[command( name = "count", @@ -131,8 +137,8 @@ struct BootstrapArgs { build_args: Vec, } -#[derive(Parser, Debug)] -struct VerifyArgs { +#[derive(clap::Args, Debug)] +struct VerificationArgs { #[arg( short = 't', long = "targets", @@ -185,15 +191,6 @@ struct VerifyArgs { )] debug: bool, - #[arg( - short = 'f', - long = "focus", - help = "Verify root crates without re-checking dependency proofs", - default_value = "false", - action = ArgAction::SetTrue - )] - focus: bool, - #[command(flatten, next_help_heading = "Cargo feature options")] cargo_features: clap_cargo::Features, @@ -465,7 +462,7 @@ fn cargo_feature_args(features: &clap_cargo::Features) -> Vec { args } -fn verify(args: &VerifyArgs) -> Result<(), DynError> { +fn verify(args: &VerificationArgs, mode: verus::VerificationMode) -> Result<(), DynError> { let targets = args.targets.clone(); let options = verus::ExtraOptions { max_errors: args.max_errors, @@ -475,7 +472,7 @@ fn verify(args: &VerifyArgs) -> Result<(), DynError> { disasm: false, cargo_args: cargo_feature_args(&args.cargo_features), verus_args: args.verus_args.clone(), - focus: args.focus, + verification_mode: mode, }; verus::exec_verify(&targets, &options) @@ -521,7 +518,7 @@ fn build(args: &BuildArgs) -> Result<(), DynError> { disasm: args.disasm, cargo_args: cargo_feature_args(&args.cargo_features), verus_args: args.verus_args.clone(), - focus: false, + verification_mode: verus::VerificationMode::Verify, }; verus::exec_build(&targets, &options) @@ -594,7 +591,8 @@ fn format(args: &FmtArgs) -> Result<(), DynError> { fn main() { let cli = Cli::parse(); if let Err(e) = match &cli.command { - Commands::Verify(args) => verify(args), + Commands::Verify(args) => verify(args, verus::VerificationMode::Verify), + Commands::Focus(args) => verify(args, verus::VerificationMode::Focus), Commands::Count(args) => count(args), Commands::Doc(args) => doc(args), Commands::Bootstrap(args) => bootstrap(args), @@ -614,10 +612,10 @@ mod tests { use super::*; #[test] - fn verify_separates_cargo_features_from_verus_arguments() { + fn focus_separates_cargo_features_from_verus_arguments() { let cli = Cli::try_parse_from([ "dv", - "verify", + "focus", "--features", "irc11 alloc", "--no-default-features", @@ -627,8 +625,8 @@ mod tests { ]) .unwrap(); - let Commands::Verify(args) = cli.command else { - panic!("expected verify command"); + let Commands::Focus(args) = cli.command else { + panic!("expected focus command"); }; assert_eq!(args.cargo_features.features, ["irc11", "alloc"]); assert!(args.cargo_features.no_default_features); diff --git a/src/verus.rs b/src/verus.rs index 046bf2b..1150d93 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -179,6 +179,21 @@ pub struct VerusTarget { pub features: Vec, } +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum VerificationMode { + Verify, + Focus, +} + +impl VerificationMode { + fn cargo_verus_subcommand(&self) -> &'static str { + match self { + Self::Verify => "verify", + Self::Focus => "focus", + } + } +} + #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct ExtraOptions { /// if log is enabled @@ -195,8 +210,8 @@ pub struct ExtraOptions { pub cargo_args: Vec, /// pass-through options to the Verus verifier pub verus_args: Vec, - /// use cargo-verus focus instead of cargo-verus verify - pub focus: bool, + /// whether cargo-verus performs full or focused verification + pub verification_mode: VerificationMode, } #[derive(Clone, Debug, PartialEq, Eq, Hash)] @@ -616,10 +631,7 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<() let cmd = &mut Command::new(get_cargo_verus(options.release)); cmd.env("RUSTC_BOOTSTRAP", "1") .env("VERUS_Z3_PATH", &z3) - .arg(if options.focus { "focus" } else { "verify" }); - if !options.focus && verus_args_should_apply_to_roots_only(&options.verus_args) { - cmd.arg("--fwd-verus-args-to").arg("roots"); - } + .arg(options.verification_mode.cargo_verus_subcommand()); push_cargo_args( cmd, target.map(|target| target.name.as_str()), @@ -797,17 +809,6 @@ fn strip_ansi_escape_codes(line: &str) -> String { plain } -fn verus_args_should_apply_to_roots_only(args: &[String]) -> bool { - args.iter().any(|arg| { - matches!( - arg.as_str(), - "--verify-root" | "--verify-module" | "--verify-only-module" | "--verify-function" - ) || arg.starts_with("--verify-module=") - || arg.starts_with("--verify-only-module=") - || arg.starts_with("--verify-function=") - }) -} - fn push_cargo_args(cmd: &mut Command, package: Option<&str>, cargo_args: &[String], release: bool) { if let Some(package) = package { cmd.arg("-p").arg(package); @@ -866,9 +867,6 @@ pub fn exec_build(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), cmd.env("RUSTC_BOOTSTRAP", "1") .env("VERUS_Z3_PATH", &z3) .arg("build"); - if verus_args_should_apply_to_roots_only(&options.verus_args) { - cmd.arg("--fwd-verus-args-to").arg("roots"); - } push_cargo_args( cmd, target.map(|target| target.name.as_str()), @@ -946,7 +944,7 @@ mod argument_tests { #[test] fn cargo_features_precede_target_and_verus_args() { let mut cmd = Command::new("cargo-verus"); - cmd.arg("verify"); + cmd.arg(VerificationMode::Focus.cargo_verus_subcommand()); push_cargo_args( &mut cmd, Some("ostd"), @@ -962,7 +960,7 @@ mod argument_tests { assert_eq!( args, [ - "verify", + "focus", "-p", "ostd", "--features",