feat: add focus command due to Verus update

README.md

@@ -29,18 +29,40 @@ pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --"
 cargo dv verify --targets <target1> <target2> ...
 ```
 
+### 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
 ```
 

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<String>,
 }
 
-#[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<String> {
     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);

src/verus.rs

@@ -179,6 +179,21 @@ pub struct VerusTarget {
     pub features: Vec<String>,
 }
 
+#[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<String>,
     /// pass-through options to the Verus verifier
     pub verus_args: Vec<String>,
-    /// 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",