[cargo-verus] feat: check verus and vstd compatibility (#2584)

Author: mkovaxx

source/cargo-verus/src/cli.rs

@@ -70,6 +70,10 @@ pub struct VerifyCommand {
     #[arg(short, long, action = ArgAction::Count)]
     pub verbosity: u8,
 
+    /// Check toolchain components, e.g. version compatibility of verus and vstd.
+    #[arg(long)]
+    pub check_toolchain: bool,
+
     /// Crates to receive forwarded Verus args
     #[arg(
         long,

source/cargo-verus/src/lib.rs

@@ -1,5 +1,5 @@
 mod cli;
-mod metadata;
+pub mod metadata;
 mod plan;
 mod subcommands;
 pub mod test_utils;

source/cargo-verus/src/metadata.rs

@@ -4,7 +4,7 @@ use std::{
 };
 
 use anyhow::{Context, Result};
-use cargo_metadata::{Metadata, MetadataCommand, Package, PackageId};
+use cargo_metadata::{Metadata, MetadataCommand, Package, PackageId, Source, semver::Version};
 use serde::Deserialize;
 use sha2::{Digest, Sha256};
 
@@ -38,13 +38,13 @@ impl VerusMetadata {
 }
 
 pub struct MetadataIndex<'a> {
-    entries: BTreeMap<&'a PackageId, MetadataIndexEntry<'a>>,
+    pub entries: BTreeMap<&'a PackageId, MetadataIndexEntry<'a>>,
 }
 
 pub struct MetadataIndexEntry<'a> {
-    package: &'a Package,
-    verus_metadata: VerusMetadata,
-    deps: BTreeMap<&'a PackageId, &'a cargo_metadata::NodeDep>,
+    pub package: &'a Package,
+    pub verus_metadata: VerusMetadata,
+    pub deps: BTreeMap<&'a PackageId, &'a cargo_metadata::NodeDep>,
 }
 
 impl<'a> MetadataIndex<'a> {
@@ -77,6 +77,10 @@ impl<'a> MetadataIndex<'a> {
         Ok(Self { entries })
     }
 
+    pub fn iter_package_ids(&self) -> impl Iterator<Item = &PackageId> {
+        self.entries.keys().map(|package_id| *package_id)
+    }
+
     pub fn get(&self, id: &PackageId) -> &MetadataIndexEntry<'a> {
         self.entries.get(id).unwrap()
     }
@@ -132,15 +136,92 @@ impl<'a> MetadataIndex<'a> {
         }
         names
     }
+
+    /// Collect sources of `vstd` that appear in the verified part of the build.
+    pub fn collect_vstd_metadata(
+        &self,
+        packages_to_verify: &Set<PackageId>,
+    ) -> Set<PackageMetadata> {
+        // Packages that verification will run on.
+        let packages_will_verify = Set::from_iter(
+            packages_to_verify
+                .iter()
+                .filter(|package_id| self.get(package_id).verus_metadata.verify)
+                .cloned(),
+        );
+        // Transitive closure of packages that verification will run on.
+        let tclosure_will_verify = self.get_transitive_closure(packages_will_verify);
+
+        // Metadata of all `vstd` instances that appear anywhere in the transitive closure.
+        let vstd_metadata: Set<PackageMetadata> = tclosure_will_verify
+            .iter()
+            .flat_map(|package_id| {
+                let entry = self.get(package_id);
+                if entry.verus_metadata.is_vstd {
+                    Some(PackageMetadata::from(entry.package))
+                } else {
+                    None
+                }
+            })
+            .collect();
+
+        assert!(
+            vstd_metadata.len() <= 1,
+            "The `vstd` versioning scheme prevents multiple instances in a resolve set.",
+            // This is a consequence of the current `vstd` versioning scheme.
+            // In the current scheme, each version matches `0.0.0-*`.
+            // By definition, *all* such versions are semver-compatible.
+            // Cargo disallows different *compatible* versions in a resolve set.
+            // https://doc.rust-lang.org/cargo/reference/resolver.html#semver-compatibility
+        );
+
+        vstd_metadata
+    }
+}
+
+/// Metadata about a package.
+#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
+pub struct PackageMetadata {
+    pub version: Version,
+    pub source: PackageSource,
 }
 
-impl<'a> MetadataIndexEntry<'a> {
-    pub fn package(&self) -> &'a Package {
-        self.package
+/// Details of a package source.
+#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
+pub enum PackageSource {
+    Registry { url: String },
+    Git { url: String, rev: Option<String> },
+    Unsupported,
+}
+
+impl From<&Package> for PackageMetadata {
+    fn from(package: &Package) -> Self {
+        let version = package.version.clone();
+        let source =
+            package.source.as_ref().map(PackageSource::from).unwrap_or(PackageSource::Unsupported);
+        PackageMetadata { version, source }
     }
+}
 
-    pub fn verus_metadata(&self) -> &VerusMetadata {
-        &self.verus_metadata
+/// NOTE: This code relies on Cargo internals because there's no stable API.
+/// The tests in `test_vstd_sources.rs` should be able to detect if these assumptions break.
+impl From<&Source> for PackageSource {
+    fn from(source: &Source) -> Self {
+        let repr = &source.repr;
+        if let Some(registry) = repr.strip_prefix("registry+") {
+            PackageSource::Registry { url: registry.to_string() }
+        } else if let Some(git_source) = repr.strip_prefix("git+") {
+            let (url, rev) = if let Some((url, rev)) = git_source.rsplit_once('#') {
+                (url, Some(rev.to_owned()))
+            } else {
+                (git_source, None)
+            };
+            // Trim the query part of the URL.
+            let url = url.split_once('?').map_or(url, |(trimmed_url, _query)| trimmed_url);
+            PackageSource::Git { url: url.to_string(), rev }
+        } else {
+            PackageSource::Unsupported
+        }
     }
 }
 

source/cargo-verus/src/subcommands.rs

@@ -11,7 +11,7 @@ use colored::Colorize;
 
 use crate::cli::{CargoOptions, VerifyCommand, VerusArgFwdSelector};
 use crate::metadata::{MetadataIndex, fetch_metadata, make_package_id};
-use crate::toolchains::TOOLCHAINS;
+use crate::toolchains::{self, TOOLCHAINS, is_matching_known_and_used};
 
 pub const CARGO_DEFAULT_LIB_METADATA: &str = "__CARGO_DEFAULT_LIB_METADATA";
 
@@ -170,6 +170,39 @@ pub fn plan_cargo_run(cfg: VerusConfig) -> Result<CargoRunPlan> {
         VerusArgFwdSelector::Deps => &dep_packages,
     };
 
+    if cfg.options.check_toolchain {
+        if cfg.options.verbosity > 0 {
+            println!("Checking toolchain components...");
+        }
+
+        let vstd_metadata = metadata_index.collect_vstd_metadata(packages_to_verify);
+        let verus_version = get_verus_driver_version()?;
+
+        if cfg.options.verbosity > 0 {
+            println!("verus version: {verus_version:?}");
+            println!("`vstd` instances:");
+            for vstd in &vstd_metadata {
+                println!("version = {:?}", vstd.version.to_string());
+                println!("source = {:?}", vstd.source);
+                println!();
+            }
+        }
+
+        for used_vstd in &vstd_metadata {
+            let is_compatible = toolchains::TOOLCHAINS.iter().any(|toolchain| {
+                toolchain.verus == verus_version
+                    && is_matching_known_and_used(&toolchain.vstd, used_vstd)
+            });
+            if !is_compatible {
+                bail!(
+                    "Components are incompatible:\n\
+                    * verus = {verus_version}\n\
+                    * vstd = {used_vstd:?}\n"
+                );
+            }
+        }
+    }
+
     /////////////////////////////////////////////////////////
     // Phase 2: plan to run Verus via `cargo {subcommand}` //
     /////////////////////////////////////////////////////////
@@ -375,12 +408,12 @@ fn make_cargo_plan(
         let receives_fwd_verus_args = fwd_verus_args_packages.contains(&pkg_id);
 
         let entry = metadata_index.get(pkg_id);
-        let package = entry.package();
+        let package = entry.package;
 
         let package_id =
             make_package_id(&package.name, package.version.to_string(), &package.manifest_path);
 
-        let verus_metadata = entry.verus_metadata();
+        let verus_metadata = &entry.verus_metadata;
 
         // The is_builtin, is_builtin_macro, and verify fields are passed as env vars as they
         // are relevant for crates which are skipped by Verus. In such cases, the driver avoids
@@ -491,3 +524,31 @@ fn get_verus_driver_path() -> PathBuf {
 
     path
 }
+
+/// Run `verus --version` and capture its output.
+fn get_verus_driver_version() -> Result<String> {
+    let command = get_verus_driver_path();
+    let output = Command::new(&command)
+        .arg("--version")
+        .output()
+        .context(format!("running `{} --version`", command.display()))?;
+
+    if !output.status.success() {
+        bail!(
+            "`{} --version` failed with status {}.\n\
+            stdout:\n{}\n\
+            stderr:\n{}",
+            command.display(),
+            output.status,
+            String::from_utf8_lossy(&output.stdout),
+            String::from_utf8_lossy(&output.stderr),
+        );
+    }
+
+    let stdout = String::from_utf8(output.stdout)
+        .context(format!("`{} --version` produced non-UTF-8 stdout", command.display()))?;
+
+    stdout.lines().find_map(|line| line.strip_prefix("  Version: ").map(ToOwned::to_owned)).context(
+        format!("Failed to parse version from `{}` output:\n{}", command.display(), stdout),
+    )
+}