Add 'kani verify-artifacts' subcommand

Cargo.toml

@@ -81,6 +81,7 @@ exclude = [
   "tests/script-based-pre/kani_lib_dep",
   "tests/script-based-pre/no_codegen",
   "tests/script-based-pre/no_codegen_error",
+  "tests/script-based-pre/verify_artifacts_cmd",
 ]
 
 [workspace.lints.clippy]

kani-driver/src/args/mod.rs

@@ -8,6 +8,7 @@ pub mod common;
 pub mod list_args;
 pub mod playback_args;
 pub mod std_args;
+pub mod verify_artifacts_args;
 
 use self::common::*;
 use crate::args::cargo::CargoTargetArgs;
@@ -175,6 +176,8 @@ pub enum StandaloneSubcommand {
     Playback(Box<playback_args::KaniPlaybackArgs>),
     /// Verify the rust standard library.
     VerifyStd(Box<std_args::VerifyStdArgs>),
+    /// Verify pre-built compiler artifacts without rebuilding.
+    VerifyArtifacts(Box<verify_artifacts_args::VerifyArtifactsArgs>),
 }
 
 #[derive(Debug, clap::Parser)]
@@ -570,6 +573,7 @@ impl ValidateArgs for StandaloneArgs {
 
         match &self.command {
             Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?,
+            Some(StandaloneSubcommand::VerifyArtifacts(args)) => args.validate()?,
             Some(StandaloneSubcommand::List(args)) => args.validate()?,
             Some(StandaloneSubcommand::Autoharness(args)) => args.validate()?,
             // TODO: Invoke PlaybackArgs::validate()
@@ -1259,4 +1263,28 @@ mod tests {
         let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
         assert_eq!(err.kind(), ErrorKind::MissingRequiredArgument);
     }
+
+    #[test]
+    fn check_verify_artifacts() {
+        let args = StandaloneArgs::try_parse_from(vec![
+            "kani",
+            "verify-artifacts",
+            "/some/artifact/dir",
+            "/another/dir",
+        ])
+        .unwrap();
+        let Some(StandaloneSubcommand::VerifyArtifacts(va)) = args.command else {
+            panic!("expected VerifyArtifacts subcommand, got {:?}", args.command);
+        };
+        assert_eq!(
+            va.artifact_dirs,
+            vec![PathBuf::from("/some/artifact/dir"), PathBuf::from("/another/dir")]
+        );
+    }
+
+    #[test]
+    fn check_verify_artifacts_requires_dir() {
+        let result = StandaloneArgs::try_parse_from(vec!["kani", "verify-artifacts"]);
+        assert!(result.is_err(), "verify-artifacts with no dirs should fail to parse");
+    }
 }

kani-driver/src/args/verify_artifacts_args.rs

@@ -0,0 +1,64 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Implements the `verify-artifacts` subcommand handling.
+
+use crate::args::{ValidateArgs, VerificationArgs};
+use clap::error::ErrorKind;
+use clap::{Error, Parser};
+use kani_metadata::UnstableFeature;
+use std::path::PathBuf;
+
+/// Verify pre-built compiler artifacts without rebuilding.
+///
+/// Reads `*.kani-metadata.json` and `*.symtab.out` files produced by a previous
+/// `kani-compiler` invocation (e.g. `cargo kani --only-codegen`, or an external
+/// build system that drives `kani-compiler` directly) and runs the verification
+/// pipeline. Artifacts must be co-located with their metadata file — this is
+/// kani-compiler's emit layout. The directory must be writable: the linker
+/// writes the linked goto binary next to each `.symtab.out`.
+///
+/// This is an **unstable option**. The artifacts must have been produced by the
+/// same kani version that verifies them; `kani-driver` does not check.
+#[derive(Debug, Parser)]
+pub struct VerifyArtifactsArgs {
+    /// Directories containing pre-built `*.kani-metadata.json` and
+    /// `*.symtab.out` artifacts.
+    #[arg(required = true)]
+    pub artifact_dirs: Vec<PathBuf>,
+
+    #[command(flatten)]
+    pub verify_opts: VerificationArgs,
+}
+
+impl ValidateArgs for VerifyArtifactsArgs {
+    fn validate(&self) -> Result<(), Error> {
+        self.verify_opts.validate()?;
+
+        if !self
+            .verify_opts
+            .common_args
+            .unstable_features
+            .contains(UnstableFeature::UnstableOptions)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `verify-artifacts` subcommand is unstable and requires -Z unstable-options",
+            ));
+        }
+
+        for dir in &self.artifact_dirs {
+            if !dir.is_dir() {
+                return Err(Error::raw(
+                    ErrorKind::InvalidValue,
+                    format!(
+                        "Artifact directory `{}` does not exist or is not a directory",
+                        dir.display()
+                    ),
+                ));
+            }
+        }
+
+        Ok(())
+    }
+}

kani-driver/src/main.rs

@@ -119,6 +119,15 @@ fn standalone_main() -> Result<()> {
             let project = project::std_project(&args.std_path, &session)?;
             (session, project)
         }
+        Some(StandaloneSubcommand::VerifyArtifacts(args)) => {
+            let session = KaniSession::new(args.verify_opts)?;
+            if !session.args.common_args.quiet {
+                print_kani_version(InvocationType::Standalone);
+            }
+
+            let project = project::prebuilt_project(&args.artifact_dirs, &session)?;
+            (session, project)
+        }
         None => {
             let session = KaniSession::new(args.verify_opts)?;
             if !session.args.common_args.quiet {

kani-driver/src/project.rs

@@ -7,11 +7,12 @@
 use crate::metadata::from_json;
 use crate::session::KaniSession;
 use crate::util::{crate_name, info_operation};
-use anyhow::{Context, Result};
+use anyhow::{Context, Result, bail};
 use kani_metadata::{
     ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, artifact::convert_type,
 };
 use std::env::current_dir;
+use std::ffi::OsStr;
 use std::fs;
 use std::ops::Deref;
 use std::path::{Path, PathBuf};
@@ -304,3 +305,172 @@ pub(crate) fn std_project(std_path: &Path, session: &KaniSession) -> Result<Proj
     let metadata = outputs.iter().map(|md_file| from_json(md_file)).collect::<Result<Vec<_>>>()?;
     Project::try_new(session, outdir, None, metadata, None)
 }
+
+/// Parse all `*.kani-metadata.json` files under the given directories, rewriting
+/// each harness's `goto_file` to be relative to the directory the metadata was
+/// found in.
+///
+/// kani-compiler records `goto_file` as the absolute path it was emitted to —
+/// which is the build machine's `OUT_DIR` and is wrong after the artifacts are
+/// relocated (a CI cache, an archive, a build-system store). The artifacts are
+/// always co-located with the metadata file (kani-compiler emits them to the
+/// same directory), so resolving by basename next to the metadata is correct.
+fn read_prebuilt_metadata(artifact_dirs: &[PathBuf]) -> Result<Vec<KaniMetadata>> {
+    let mut metadata = vec![];
+    for dir in artifact_dirs {
+        let dir = dir.canonicalize().with_context(|| {
+            format!("Failed to canonicalize artifact directory `{}`", dir.display())
+        })?;
+        let mut found_any = false;
+        for entry in fs::read_dir(&dir)
+            .with_context(|| format!("Failed to read artifact directory `{}`", dir.display()))?
+        {
+            let path = entry?.path();
+            let is_metadata = path
+                .file_name()
+                .and_then(OsStr::to_str)
+                .is_some_and(|n| n.ends_with(".kani-metadata.json"));
+            if !is_metadata {
+                continue;
+            }
+            found_any = true;
+            let mut md: KaniMetadata = from_json(&path)?;
+            for h in md.proof_harnesses.iter_mut().chain(md.test_harnesses.iter_mut()) {
+                if let Some(gf) = &h.goto_file {
+                    // Take only the basename; resolve against the directory
+                    // the metadata file was found in.
+                    let basename = gf.file_name().with_context(|| {
+                        format!(
+                            "Harness `{}` has a goto_file with no file name component",
+                            h.pretty_name
+                        )
+                    })?;
+                    h.goto_file = Some(dir.join(basename));
+                }
+            }
+            metadata.push(md);
+        }
+        if !found_any {
+            bail!(
+                "No `*.kani-metadata.json` files found in `{}`. \
+                 Was this directory produced by a `kani-compiler` build?",
+                dir.display()
+            );
+        }
+    }
+    Ok(metadata)
+}
+
+/// Generate a project from pre-built artifacts in the given directories.
+///
+/// Each directory is scanned for `*.kani-metadata.json` files. For each
+/// harness, `goto_file` is resolved relative to the directory the metadata was
+/// found in. Artifacts must be co-located with the metadata file — this is
+/// kani-compiler's emit layout, which `read_prebuilt_metadata()` documents.
+///
+/// Note: `Project::try_new()` writes the linked `.out` file next to each
+/// `.symtab.out`, so `artifact_dirs` must be writable. Callers reading from a
+/// read-only artifact source (build cache, archive) should copy to a scratch
+/// directory first.
+pub fn prebuilt_project(artifact_dirs: &[PathBuf], session: &KaniSession) -> Result<Project> {
+    let outdir = if let Some(target_dir) = &session.args.target_dir {
+        std::fs::create_dir_all(target_dir)?;
+        target_dir.canonicalize()?
+    } else {
+        current_dir()?.canonicalize()?
+    };
+    let metadata = read_prebuilt_metadata(artifact_dirs)?;
+    Project::try_new(session, outdir, None, metadata, None)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use kani_metadata::{HarnessAttributes, HarnessKind};
+    use std::fs;
+
+    /// Build a minimal `KaniMetadata` with one proof harness whose `goto_file`
+    /// is the given path. Only `goto_file` matters; everything else is filler.
+    fn metadata_with_goto_file(goto_file: Option<PathBuf>) -> KaniMetadata {
+        KaniMetadata {
+            crate_name: "fixture".to_string(),
+            proof_harnesses: vec![HarnessMetadata {
+                pretty_name: "fixture::check".to_string(),
+                mangled_name: "_RNvNtCsfixture_5check".to_string(),
+                crate_name: "fixture".to_string(),
+                original_file: "src/lib.rs".to_string(),
+                original_start_line: 1,
+                original_end_line: 5,
+                goto_file,
+                attributes: HarnessAttributes::new(HarnessKind::Proof),
+                contract: None,
+                has_loop_contracts: false,
+                is_automatically_generated: false,
+            }],
+            unsupported_features: vec![],
+            test_harnesses: vec![],
+            contracted_functions: vec![],
+            autoharness_md: None,
+        }
+    }
+
+    /// `read_prebuilt_metadata()` rewrites each harness's `goto_file` to live
+    /// next to the metadata file it was found in — the recorded build-machine
+    /// path is meaningless after relocation.
+    #[test]
+    fn prebuilt_project_relocates_goto_file() {
+        let tmp = tempfile::tempdir().unwrap();
+        let dir = tmp.path();
+        // The recorded path is an absolute path from a different machine.
+        let recorded = PathBuf::from("/build/some-other-machine/fixture__hash.symtab.out");
+        let basename = "fixture__hash.symtab.out";
+        // Co-located artifact, documenting the layout the function assumes.
+        // `read_prebuilt_metadata()` does not validate existence — it rewrites
+        // unconditionally; the symtab is only read later by `Project::try_new()`.
+        fs::write(dir.join(basename), b"").unwrap();
+        fs::write(
+            dir.join("fixture.kani-metadata.json"),
+            serde_json::to_string(&metadata_with_goto_file(Some(recorded))).unwrap(),
+        )
+        .unwrap();
+
+        let parsed = read_prebuilt_metadata(&[dir.to_path_buf()]).unwrap();
+        assert_eq!(parsed.len(), 1);
+        // The rewritten path must point inside the temp dir, not /build/....
+        // Compare against the canonicalized dir — read_prebuilt_metadata()
+        // canonicalizes the input dir before joining, and on macOS /tmp is a
+        // symlink so a non-canonicalized comparison would spuriously fail.
+        let h = &parsed[0].proof_harnesses[0];
+        assert_eq!(
+            h.goto_file.as_deref(),
+            Some(dir.canonicalize().unwrap().join(basename).as_path())
+        );
+    }
+
+    /// A harness with no `goto_file` (reachability=none deps) must not panic;
+    /// `read_prebuilt_metadata()` leaves `None` alone.
+    #[test]
+    fn prebuilt_project_skips_none_goto_file() {
+        let tmp = tempfile::tempdir().unwrap();
+        let dir = tmp.path();
+        fs::write(
+            dir.join("fixture.kani-metadata.json"),
+            serde_json::to_string(&metadata_with_goto_file(None)).unwrap(),
+        )
+        .unwrap();
+
+        let parsed = read_prebuilt_metadata(&[dir.to_path_buf()]).unwrap();
+        assert_eq!(parsed[0].proof_harnesses[0].goto_file, None);
+    }
+
+    /// An empty directory (no `*.kani-metadata.json`) is an error, not a vacuous
+    /// success — silence here would look like a verification that found nothing
+    /// to verify.
+    #[test]
+    fn prebuilt_project_errors_on_empty_dir() {
+        let tmp = tempfile::tempdir().unwrap();
+        let result = read_prebuilt_metadata(&[tmp.path().to_path_buf()]);
+        assert!(result.is_err());
+        assert!(result.unwrap_err().to_string().contains("No `*.kani-metadata.json`"));
+    }
+}

tests/script-based-pre/verify_artifacts_cmd/Cargo.toml

@@ -0,0 +1,7 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "verify_artifacts_fixture"
+version = "0.1.0"
+edition = "2024"

tests/script-based-pre/verify_artifacts_cmd/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: verify_artifacts.sh
+expected: verify_artifacts.expected

tests/script-based-pre/verify_artifacts_cmd/src/lib.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Fixture for the verify-artifacts integration test. Two harnesses: one that
+//! verifies, one that fails — proving the verdict is honest, not vacuous.
+
+#[cfg(kani)]
+mod proofs {
+    #[kani::proof]
+    fn check_add_identity() {
+        let x: u8 = kani::any();
+        assert_eq!(x.wrapping_add(0), x);
+    }
+
+    #[kani::proof]
+    fn check_intentional_failure() {
+        let x: u8 = kani::any();
+        // Fails for x == 255. The deliberate failure proves the pipeline
+        // reaches CBMC and reads the verdict — not merely that the command
+        // exited without crashing.
+        assert!(x < 255);
+    }
+}

tests/script-based-pre/verify_artifacts_cmd/verify_artifacts.expected

@@ -0,0 +1,8 @@
+[TEST] Build artifacts with --only-codegen
+[TEST] Artifacts produced
+[TEST] Verify pre-built artifacts
+Checking harness proofs::check_add_identity...
+Checking harness proofs::check_intentional_failure...
+Verification failed for - proofs::check_intentional_failure
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.
+[TEST] Exit code: 1