Support irc11 build args

README.md

@@ -1,10 +1,10 @@
 # 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, 
+`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
@@ -29,6 +29,33 @@ pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --"
 cargo dv verify --targets <target1> <target2> ...
 ```
 
+## Bootstrapping Verus
+
+By default, `cargo dv bootstrap` builds the `main` branch of
+`asterinas/verus`. Use `--branch` to select another branch and repeat
+`--build-arg` to pass additional arguments to `cargo-verus` when it builds
+vstd.
+
+The `irc11` branch is hosted by `verus-lang/verus`, rather than the default
+`asterinas/verus` remote, and requires its weak-memory vstd modules to be
+enabled explicitly:
+
+```bash
+cargo dv bootstrap --upstream-verus --branch irc11 \
+  --build-arg=--vstd-weak-memory
+```
+
+For compatibility with the `irc11` branch's vargo spelling, DV translates
+`--vstd-weak-memory` to the vstd feature arguments
+`--features weak-memory` used by the current cargo-verus bootstrap path.
+
+The same arguments are honored by upgrades:
+
+```bash
+cargo dv bootstrap --upgrade --upstream-verus --branch irc11 \
+  --build-arg=--vstd-weak-memory
+```
+
 Optionally, if you want to use the pre-commit hook, you can add the rusty-hook to your project:
 
 ```bash

src/main.rs

@@ -113,6 +113,15 @@ struct BootstrapArgs {
         value_name = "BRANCH_NAME"
     )]
     branch: Option<String>,
+
+    #[arg(
+        long = "build-arg",
+        help = "An extra argument passed to `cargo-verus` when building vstd",
+        value_name = "ARG",
+        action = ArgAction::Append,
+        allow_hyphen_values = true
+    )]
+    build_args: Vec<String>,
 }
 
 #[derive(Parser, Debug)]
@@ -433,6 +442,7 @@ fn bootstrap(args: &BootstrapArgs) -> Result<(), DynError> {
         release: !args.debug,
         restart: args.restart,
         branch: args.branch.clone(),
+        build_args: args.build_args.clone(),
         force_reset: args.upgrade,
         upstream_verus: args.upstream_verus,
     };
@@ -540,3 +550,28 @@ fn main() {
         error!("Error when executing command `{:?}`: {}", cli.command, e);
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn bootstrap_accepts_upstream_irc11_build_argument() {
+        let cli = Cli::try_parse_from([
+            "dv",
+            "bootstrap",
+            "--upstream-verus",
+            "--branch",
+            "irc11",
+            "--build-arg=--vstd-weak-memory",
+        ])
+        .unwrap();
+
+        let Commands::Bootstrap(args) = cli.command else {
+            panic!("expected bootstrap command");
+        };
+        assert!(args.upstream_verus);
+        assert_eq!(args.branch.as_deref(), Some("irc11"));
+        assert_eq!(args.build_args, ["--vstd-weak-memory"]);
+    }
+}

src/verus.rs

@@ -970,6 +970,7 @@ pub mod install {
         pub restart: bool,
         pub release: bool,
         pub branch: Option<String>,
+        pub build_args: Vec<String>,
         pub force_reset: bool,
         pub upstream_verus: bool,
     }
@@ -1264,7 +1265,29 @@ pub mod install {
         Ok(())
     }
 
-    pub fn build_verus(release: bool) -> Result<(), DynError> {
+    fn vstd_build_args(release: bool, extra_args: &[String]) -> Vec<String> {
+        let mut args = vec![
+            "-p".to_string(),
+            "cargo-verus".to_string(),
+            "--".to_string(),
+            "build".to_string(),
+        ];
+        if release {
+            args.push("--release".to_string());
+        }
+        args.extend(["--manifest-path".to_string(), "vstd/Cargo.toml".to_string()]);
+
+        for arg in extra_args {
+            if arg == "--vstd-weak-memory" {
+                args.extend(["--features".to_string(), "weak-memory".to_string()]);
+            } else {
+                args.push(arg.clone());
+            }
+        }
+        args
+    }
+
+    pub fn build_verus(release: bool, extra_args: &[String]) -> Result<(), DynError> {
         let toolchain = verus_dir().join("rust-toolchain.toml");
         let toolchain_name = toolchain::load_toolchain(&toolchain);
         let source_dir = verus_source_dir();
@@ -1290,11 +1313,7 @@ pub mod install {
         if release {
             vstd_cmd.arg("--release");
         }
-        vstd_cmd.args(["-p", "cargo-verus", "--", "build"]);
-        if release {
-            vstd_cmd.arg("--release");
-        }
-        vstd_cmd.args(["--manifest-path", "vstd/Cargo.toml"]);
+        vstd_cmd.args(vstd_build_args(release, extra_args));
 
         for (mut cmd, description) in [
             (clean_cmd, "Cleaning the Verus workspace"),
@@ -1341,7 +1360,7 @@ pub mod install {
         install_z3()?;
 
         // Build Verus
-        build_verus(options.release)?;
+        build_verus(options.release, &options.build_args)?;
 
         // Update the workspace toolchain
         toolchain::sync_toolchain(
@@ -1547,7 +1566,7 @@ pub mod install {
         status!("Verus repo updated to the latest version");
 
         // Build Verus
-        build_verus(options.release)?;
+        build_verus(options.release, &options.build_args)?;
 
         // Update the workspace toolchain
         toolchain::sync_toolchain(
@@ -1561,4 +1580,45 @@ pub mod install {
         status!("Verus upgrade complete");
         Ok(())
     }
+
+    #[cfg(test)]
+    mod tests {
+        use super::*;
+
+        #[test]
+        fn irc11_build_argument_enables_weak_memory_for_vstd() {
+            let extra_args = vec!["--vstd-weak-memory".to_string()];
+            assert_eq!(
+                vstd_build_args(true, &extra_args),
+                [
+                    "-p",
+                    "cargo-verus",
+                    "--",
+                    "build",
+                    "--release",
+                    "--manifest-path",
+                    "vstd/Cargo.toml",
+                    "--features",
+                    "weak-memory",
+                ]
+            );
+        }
+
+        #[test]
+        fn extra_vstd_build_arguments_are_forwarded() {
+            let extra_args = vec!["--locked".to_string()];
+            assert_eq!(
+                vstd_build_args(false, &extra_args),
+                [
+                    "-p",
+                    "cargo-verus",
+                    "--",
+                    "build",
+                    "--manifest-path",
+                    "vstd/Cargo.toml",
+                    "--locked",
+                ]
+            );
+        }
+    }
 }